//! The Chinese Remainder Theorem — pairwise and k-ary congruence solving.

use crate::number::modinv;

/// Chinese remainder for two congruences: the unique `x` in `[0, m1*m2)` with
/// `x ≡ r1 (mod m1)` and `x ≡ r2 (mod m2)`, by Garner's method
/// `x = r1 + m1 * ((r2 - r1) * (m1⁻¹ mod m2) mod m2)`.
///
/// Returns `None` unless the moduli are coprime with `m2 >= 2`, and the product
/// `m1*m2` fits `u64` (so the answer is representable). Inputs are reduced mod
/// their modulus first, so any `r1, r2` are accepted.
///
/// Verified exhaustively over coprime moduli against a `[0, m1*m2)` scan, plus
/// 100k full-range checks of the defining congruences. Like `is_prime`, it has no
/// Kani harness: it composes `modinv`'s `i128` division with `u128` products,
/// which CBMC cannot bit-blast tractably, so the exhaustive / property tests are
/// the verification tier.
///
/// # Examples
///
/// ```
/// use coprime::number::crt2;
///
/// // the unique x in [0, 15) with x ≡ 2 (mod 3) and x ≡ 3 (mod 5)
/// assert_eq!(crt2(2, 3, 3, 5), Some(8));
/// assert_eq!(crt2(1, 4, 2, 6), None); // moduli 4, 6 are not coprime
/// ```
#[must_use]
#[allow(clippy::cast_possible_truncation)] // x < m1*m2 <= u64::MAX fits u64
pub fn crt2(r1: u64, m1: u64, r2: u64, m2: u64) -> Option<u64> {
    let m = m1.checked_mul(m2)?; // product must fit u64
    let inv = modinv(m1, m2)?; // m1^-1 mod m2; None unless gcd(m1,m2)=1 and m2>1
    let (r1, r2) = (r1 % m1, r2 % m2);
    let m2u = u128::from(m2);
    // Garner: t = (r2 - r1) * inv (mod m2); then x = r1 + m1*t in [0, m1*m2).
    let diff = (u128::from(r2) + m2u - u128::from(r1 % m2)) % m2u;
    let t = diff * u128::from(inv) % m2u;
    let x = (u128::from(r1) + u128::from(m1) * t) % u128::from(m);
    Some(x as u64)
}

/// Chinese remainder for any list of congruences `[(r_i, m_i)]` with pairwise
/// coprime moduli: the unique `x` in `[0, ∏ m_i)` with `x ≡ r_i (mod m_i)` for
/// every `i`, by folding [`crt2`]. An empty list yields `0`.
///
/// Returns `None` if some modulus is `< 2`, the moduli are not pairwise coprime,
/// or the running product overflows `u64`.
///
/// # Examples
///
/// ```
/// use coprime::number::crt;
///
/// // the unique x in [0, 105) congruent to 2, 3, 2 modulo 3, 5, 7
/// assert_eq!(crt(&[(2, 3), (3, 5), (2, 7)]), Some(23));
/// assert_eq!(crt(&[]), Some(0)); // no constraints
/// assert_eq!(crt(&[(2, 4), (3, 6)]), None); // 4 and 6 share the factor 2
/// ```
#[must_use]
pub fn crt(congruences: &[(u64, u64)]) -> Option<u64> {
    let mut x = 0u64;
    let mut m = 1u64;
    for &(r, mi) in congruences {
        x = crt2(x, m, r, mi)?; // combine (x mod m) with (r mod mi)
        m = m.checked_mul(mi)?;
    }
    Some(x)
}
