//! Kani proof — the Jacobi symbol is multiplicative in its top argument,
//! `(a | n)·(b | n) == (a·b mod n | n)`, over a symbolic 4-bit slice.
//!
//! This is the defining homomorphism of the symbol, checked
//! against itself across three independent evaluations rather than re-deriving
//! the reciprocity steps — a genuine algebraic invariant, not a tautology.
//! `jacobi` is `u64`-only (shifts, `%`, compares in a Euclid-like loop), so unlike
//! the `u128` Miller–Rabin / Garner paths CBMC can bit-blast it; breadth lives in
//! the concrete `jacobi_*` tests in [`crate::number`] (n up to 400).
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/JacobiSpec.lean` proves the
//! corollary `jacobi_multiplicative` — the same three-`Some` hypotheses and the
//! same `ja·jb == jab` clause, on the extracted model, unbounded over all of
//! `u64` (the reduced product carried as a `u64` equal to `a·b mod n`, which
//! this slice computes directly). Keep the two in sync by name and clause.
#![allow(clippy::arithmetic_side_effects)] // arithmetic is the subject under test

use crate::number::jacobi;

// BOUNDS: unwind = 16; reason = with operands < 2^4 the inner 2-stripping and the
// outer reciprocity loop each iterate < ~5 times (a Euclid-like descent); 16 is
// headroom. 4-bit keeps a·b < 2^8 (no u64 overflow) and the SAT instance small —
// it matches the committed bound of the extended_gcd / modinv harnesses.
#[kani::proof]
#[kani::unwind(16)]
fn jacobi_multiplicative() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    let n: u64 = kani::any();
    kani::assume(n >= 3);
    kani::assume(n % 2 == 1); // the Jacobi symbol requires odd n
    kani::assume(n < (1 << 4));
    kani::assume(a < (1 << 4));
    kani::assume(b < (1 << 4));

    // n is odd, so each call returns Some; the product a*b < 2^10 fits u64.
    let (Some(ja), Some(jb), Some(jab)) = (jacobi(a, n), jacobi(b, n), jacobi(a * b % n, n)) else {
        return;
    };
    kani::assert(ja * jb == jab, "(a|n)(b|n) == (a*b mod n | n)");
}
