//! Kani proof — the Bézout identity for [`crate::number::extended_gcd`] as a
//! *symbolic* check over every pair of 4-bit operands.
//!
//! The oracle is algebra **over the output** — the Bézout combination
//! `s*a + t*b == d` and the divisibility `d | a`, `d | b` — not a re-run of the
//! Euclidean steps, so it exercises the production recurrence against a
//! computationally distinct check.
//!
//! Scope: this harness *verifies* — every check (the Bézout
//! identity, divisibility, and the auto-generated overflow / divide-by-zero
//! checks) passes. The limit is *time*, not soundness or memory: `extended_gcd`'s
//! `i128` division bit-blasts to a large SAT instance (~17M clauses at 4 bits,
//! ~28M at 8, ~51M at 16), so CBMC's per-check encoding dominates — 4-bit
//! verifies in ~2 min and grows fast: wider slices stay sound but quickly become
//! impractical to encode, so 4-bit is the committed bound. Because
//! the slice is bounded, breadth lives in the concrete `extended_gcd_bezout_wide`
//! test in [`crate::number`] (dense grid + every Fibonacci worst-case pair to
//! `u64::MAX` + 200k full-range pairs); this harness is the machine-checked
//! *proof* of the recurrence over the symbolic interior, and a regression anchor.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/ExtGcdSpec.lean` proves the
//! corollary `extended_gcd_satisfies_bezout` — the exact same clauses (Bézout
//! over the exact integers, then the zero-guarded divisibility), on the
//! extracted model, unbounded over all of `u64`. Keep the two in sync by name
//! and clause.
#![allow(clippy::arithmetic_side_effects)] // arithmetic is the subject under test

use crate::number::extended_gcd;

// BOUNDS: unwind = 10; reason = with both operands `< 2^4`, Euclid's worst case
// is consecutive Fibonacci numbers (F_7 = 13 < 2^4 < F_8 = 21), so at most 6
// division steps (ceil(log_phi(sqrt5 * 2^4)) - 2 = 6); 10 gives headroom for the
// loop-exit assertion. 4-bit is the committed bound because it verifies fast
// (~2 min); wider bounds verify but slowly (see the module note above).
#[kani::proof]
#[kani::unwind(10)]
fn extended_gcd_satisfies_bezout() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    kani::assume(a < (1 << 4));
    kani::assume(b < (1 << 4));
    let (d, s, t) = extended_gcd(a, b);

    // Bézout identity, computed in i128 over the output. The signed products
    // `s*a`, `t*b` have opposite signs and sum to `d`, and are each bounded by
    // `a*b/2 < 2^127` (terminal cofactors `|s| <= b/2`, `|t| <= a/2` for
    // `a, b > 1`), so they fit i128.
    kani::assert(
        s * i128::from(a) + t * i128::from(b) == i128::from(d),
        "s*a + t*b == gcd(a, b)",
    );

    // The gcd divides both inputs. `d == 0` only when `a == b == 0`; the
    // short-circuit keeps the `% d` well-defined for the model checker.
    kani::assert(
        d == 0 || (a % d == 0 && b % d == 0),
        "gcd(a, b) divides both a and b",
    );
}
