//! Kani proof of the Kronecker symbol's complete multiplicativity in the lower
//! argument — `(a | n1) * (a | n2) == (a | n1*n2)` — over a 4-bit slice. This
//! exercises the `(a | 2)` supplement and the `n = 2^e * m` split symbolically
//! (the part `jacobi` does not cover): `n1, n2 in {1, 2, 3}` hits even moduli,
//! `(a|2)^2` (at `n1*n2 = 4`), and odd moduli. `kronecker` reuses `jacobi_odd`,
//! which uses no `u128`, so the slice is CBMC-tractable.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/KroneckerSpec.lean` proves the
//! corollary `kronecker_multiplicative_in_n` — the same multiplicativity clause
//! under the same `n1, n2 >= 1` assumptions, on the extracted model, unbounded
//! over all of `u64` (the product carried as a `u64` equal to `n1·n2`, which
//! this slice computes directly). Keep the two in sync by name and clause.

use crate::number::kronecker;

#[kani::proof]
#[kani::unwind(16)]
fn kronecker_multiplicative_in_n() {
    let a: u64 = kani::any();
    let n1: u64 = kani::any();
    let n2: u64 = kani::any();
    kani::assume(a < 16);
    kani::assume(n1 >= 1 && n1 < 4);
    kani::assume(n2 >= 1 && n2 < 4);
    // Symbols are in {-1, 0, 1}; the product cannot overflow i8, and n1*n2 < 16.
    kani::assert(
        kronecker(a, n1) * kronecker(a, n2) == kronecker(a, n1 * n2),
        "Kronecker symbol is multiplicative in n",
    );
}
