//! Kani proof that `isqrt` is the integer floor square root, over the **32-bit
//! input slice** `n < 2^32`. `isqrt` itself is pure-`u64` (shifts, compares, a
//! guarded subtract — no `u128`), so the *function* bit-blasts cleanly over the
//! whole domain; the bound is on the *postcondition*, which squares the result —
//! a symbolic 64-bit multiply is SAT-hard (multiplication is the classic hard
//! case). Slicing to `n < 2^32` makes `r < 2^16`, so `r*r` is a tractable 16-bit
//! multiply. This is still by far the widest Kani slice in the crate (`2^32`
//! inputs symbolically vs the 4–8-bit slices elsewhere); the full domain is
//! covered by the exhaustive boundary-lattice + 200k differential tests. The
//! upper bound uses the `u64`-safe form `n - r*r <= 2*r`.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/RootsSpec.lean` proves the
//! corollary `isqrt_is_floor_sqrt` — the exact same clauses, on the extracted
//! model, unbounded over all of `u64`. Keep the two in sync by name and clause.

use crate::number::isqrt;

#[kani::proof]
#[kani::unwind(33)] // the loop runs exactly 32 times: bit = 4^31, 4^30, …, 4^0
fn isqrt_is_floor_sqrt() {
    let n: u64 = kani::any();
    kani::assume(n < (1u64 << 32)); // keep the postcondition's r*r a 16-bit multiply
    let r = isqrt(n);
    kani::assert(r <= 0xFFFF, "isqrt(n<2^32) fits 2^16 - 1");
    let rr = r * r;
    kani::assert(rr <= n, "r*r <= n (lower bound)");
    kani::assert(n - rr <= 2 * r, "n < (r+1)^2 (upper bound, u64-safe)");
}
