//! Kani proof — [`crate::number::modinv`] satisfies its postcondition over a
//! symbolic 4-bit slice: it returns `None` exactly when `a` is not invertible
//! modulo `modulus`, and otherwise a true inverse reduced into `[0, modulus)`.
//!
//! The oracle is the *defining property* — `a * inv ≡ 1 (mod modulus)` and the
//! gcd-based existence condition — not a re-run of extended Euclid, so it checks
//! production code against a computationally distinct spec. A brute-force inverse
//! oracle is avoided on purpose: it would loop `modulus` times and explode the
//! unwind.
//!
//! Scope: this harness rides on `extended_gcd`'s `i128` division,
//! whose bit-blasting makes wide bounds slow (time, not memory); breadth lives in
//! the concrete `modinv_matches_brute` / `modinv_inverts_wide` tests in
//! [`crate::number`].
#![allow(clippy::arithmetic_side_effects)] // arithmetic is the subject under test

use crate::number::{gcd, modinv};

// BOUNDS: unwind = 10; reason = extended_gcd on operands `< 2^4` terminates in
// <= 6 division steps (consecutive-Fibonacci worst case, F_7 = 13 < 2^4 < F_8);
// 10 gives headroom. 4-bit committed bound — verifies fast; wider is slow (the
// `i128` division in extended_gcd, which this rides on, explodes the SAT size).
#[kani::proof]
#[kani::unwind(10)]
fn modinv_satisfies_postcondition() {
    let a: u64 = kani::any();
    let modulus: u64 = kani::any();
    kani::assume(modulus >= 2);
    kani::assume(modulus < (1 << 4));
    kani::assume(a < (1 << 4));

    match modinv(a, modulus) {
        // `None` cross-check: modinv returns None iff extended_gcd's d != 1; this
        // checks that against `gcd`, a separately-written Euclid. The fully
        // independent witness that None is correct (no `x` inverts `a`) is the
        // [0, modulus) scan in the concrete `modinv_matches_brute` test.
        None => kani::assert(
            gcd(a % modulus, modulus) != 1,
            "modinv is None only when a is not invertible",
        ),
        Some(inv) => {
            kani::assert(inv < modulus, "inverse is reduced into [0, modulus)");
            kani::assert(
                u128::from(a % modulus) * u128::from(inv) % u128::from(modulus) == 1,
                "a * inv == 1 (mod modulus)",
            );
        }
    }
}
