//! Kani proof that `iroot(n, 3)` is the integer floor **cube root** over the
//! slice `n < 2^24` (so `r < 2^8`, keeping `r^3` and `(r+1)^3` small multiplies;
//! a symbolic full-width `r^k` would be SAT-hard, the same constraint that bounds
//! `isqrt`). `iroot` is pure-`u64` (binary search + `checked_pow`), so the
//! function bit-blasts cleanly — the bound is on the postcondition's product
//! width, not the algorithm. The cube root is the case that unlocks the
//! low-exponent RSA attacks, so it is the one proved here.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/IrootSpec.lean` proves the
//! corollary `iroot_cube_is_floor` — the exact same clauses (the fit guarded
//! by this slice, the cube bounds unguarded), on the extracted model,
//! unbounded over all of `u64`. Keep the two in sync by name and clause.

use crate::number::iroot;

#[kani::proof]
#[kani::unwind(20)]
fn iroot_cube_is_floor() {
    let n: u64 = kani::any();
    kani::assume(n < (1 << 24)); // r < 2^8 ⇒ r^3, (r+1)^3 <= 2^24, no overflow
    let r = iroot(n, 3);
    kani::assert(r <= 0xFF, "cube root of n < 2^24 fits 2^8 - 1");
    kani::assert(r * r * r <= n, "r^3 <= n (lower bound)");
    kani::assert(n < (r + 1) * (r + 1) * (r + 1), "n < (r+1)^3 (upper bound)");
}
