//! Kani proof that [`crate::number::modular::mulmod`]'s `u128` widening is the
//! modular product, over the **8-bit slice** — checked against an independent
//! all-`u64` reference, which exists exactly on the slice where `a * b` cannot
//! overflow 64 bits. `mulmod`'s whole reason to exist is the widening (its
//! `u128` product/reduction never truncates); the reference computes the same
//! value through 64-bit circuits only, so a widening or truncation bug cannot
//! cancel out of both sides. The SAT core of this proof is the **equivalence
//! of a 128-bit and a 64-bit division circuit** under a symbolic modulus —
//! observed not to converge at 64- or even 16-bit moduli (CBMC parks in one
//! solver call indefinitely); division is as hard for SAT as the multiply
//! `isqrt_floor.rs` slices around. 8 bits matches the `modpow_naive` slice,
//! and `modpow` exercises the same widened-reduction shape inline on every
//! iteration, so the two slices cross-check the same arithmetic idiom.
//!
//! The Lean `MulmodSpec` proves the same function unbounded on the extracted
//! model; this leg pins the real compiled `u128` intrinsics.
#![allow(clippy::arithmetic_side_effects)] // checker arithmetic is the harness, not the subject

use crate::number::mulmod;

#[kani::proof]
fn mulmod_matches_u64_reference() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    let m: u64 = kani::any();
    kani::assume(a < (1 << 8) && b < (1 << 8)); // a*b fits u64: the reference's domain
    kani::assume(m >= 1 && m < (1 << 8)); // >= 1 keeps the reference's `%` defined (mulmod itself is total: m <= 1 returns 0)
    let r = mulmod(a, b, m);
    kani::assert(r == (a * b) % m, "mulmod equals the in-u64 modular product");
    kani::assert(r < m, "mulmod reduces below the modulus");
}
