//! Kani proof that [`crate::number::crt2`] solves the pairwise Chinese
//! remainder problem, over **4-bit moduli** with **full-width symbolic
//! residues** — the clauses of the Lean `crt2_spec` (`CrtSpec.lean`): on
//! `Some(x)`, the defining congruences `x ≡ r1 (mod m1)`, `x ≡ r2 (mod m2)`
//! and the range `x < m1·m2`; and `Some`/`None` exactly characterized by
//! coprimality (checked independently and loop-free: two moduli `< 16` share a
//! divisor `> 1` iff they share one of the six primes `< 16` — keeping the
//! harness's own loops out lets the global unwind stay at `extended_gcd`'s
//! 4-bit chain length, which is what bounds the `i128` divider copies in the
//! formula). Uniqueness inside the range is the congruences + range clauses
//! (the CRT bijection), so this is the whole contract.
//!
//! The 4-bit slice matches `modinv_invariant`'s: `crt2` composes `modinv` —
//! `extended_gcd`'s chain of `i128` divisions with symbolic divisors, the
//! SAT-hard shape (see `gcd_correct.rs`) — with `u128` Garner arithmetic. The
//! residues are sliced to 4 bits as well: full-width residues only add the
//! entry reductions (64-bit dividers) to the formula, and with them the solver
//! parks (observed at ~16M clauses); `crt2` reduces residues mod `m` first,
//! so 4-bit residues still cover every residue class the Garner core can see.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/CrtSpec.lean` proves the
//! corollary `crt2_solves_both_congruences` — the same clauses under the same
//! `2 <= m` assumptions (with the `u64` product-overflow disjunct this slice
//! makes vacuous spelled out in the `None` arm), on the extracted model,
//! unbounded over all of `u64`. Keep the two in sync by name and clause.
#![allow(clippy::arithmetic_side_effects)] // checker arithmetic is the harness, not the subject

use crate::number::crt2;

/// `true` iff `a` and `b` (both `< 16`) share a divisor `> 1`: equivalently a
/// common prime divisor, and every prime `< 16` is listed. Loop-free on purpose.
fn share_a_prime_below_16(a: u64, b: u64) -> bool {
    (a % 2 == 0 && b % 2 == 0)
        || (a % 3 == 0 && b % 3 == 0)
        || (a % 5 == 0 && b % 5 == 0)
        || (a % 7 == 0 && b % 7 == 0)
        || (a % 11 == 0 && b % 11 == 0)
        || (a % 13 == 0 && b % 13 == 0)
}

#[kani::proof]
#[kani::unwind(9)] // extended_gcd on 4-bit moduli: at most ~7 iterations (Lamé) + margin
fn crt2_solves_both_congruences() {
    let r1: u64 = kani::any();
    let r2: u64 = kani::any();
    let m1: u64 = kani::any();
    let m2: u64 = kani::any();
    kani::assume(2 <= m1 && m1 < 16 && 2 <= m2 && m2 < 16);
    kani::assume(r1 < 16 && r2 < 16); // see the residue-width note above

    let has_common = share_a_prime_below_16(m1, m2);

    match crt2(r1, m1, r2, m2) {
        Some(x) => {
            kani::assert(!has_common, "Some only for coprime moduli");
            kani::assert(x % m1 == r1 % m1, "x solves the first congruence");
            kani::assert(x % m2 == r2 % m2, "x solves the second congruence");
            kani::assert(x < m1 * m2, "x is the canonical representative");
        }
        None => {
            kani::assert(has_common, "None only for non-coprime moduli");
        }
    }
}
