//! Kani proof that [`crate::number::next_prime`] returns the **smallest** prime
//! `>= n`, over the slice `n <= 36` — the clauses of the Lean `NextPrimeSpec`
//! (`some q` ⟹ `q` prime, `q >= n`, nothing in `[n, q)` prime), mirrored on the
//! real compiled code. Primality/compositeness in the checker is independent
//! trial division with concrete divisors per unrolled iteration.
//!
//! **Why `n <= 36`:** every candidate the scan can visit is then `<= 37`, the
//! last hard-coded Miller–Rabin witness, so `is_prime` always decides in its
//! witness equality/divisibility fast path (every odd composite `<= 37` has a
//! prime factor `<= 5`; every prime `<= 37` is a witness). The SPRP tail —
//! `modpow`, the CBMC-intractable part — is *mathematically* unreachable, and
//! the stub below pins that with a panic instead of assuming it, exactly as in
//! `factorize_correct.rs` (anti-vacuity + keeps the call graph small).
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/NextPrimeSpec.lean` proves the
//! corollary `next_prime_is_smallest_prime_geq` — the same clauses (the
//! `q <= 37` ceiling and the `Some` totality slice-guarded by `n <= 36`), on
//! the extracted model, for all of `u64`, conditional on `DET12` like
//! `next_prime_spec`. Keep the two in sync by name and clause.
#![allow(clippy::arithmetic_side_effects)] // checker arithmetic is the harness, not the subject

use crate::number::next_prime;

/// The slice bound: keeps every scanned candidate inside the witness fast path.
const BOUND: u64 = 36;

/// Stub for `is_strong_probable_prime`: unreachable on this slice. Reaching it
/// fails the proof.
fn sprp_unreachable(_n: u64, _a: u64) -> bool {
    unreachable!("SPRP tail entered on n <= 36: candidate escaped the witness fast path")
}

#[kani::proof]
#[kani::unwind(15)] // is_prime's witness loop is the longest: 12 iterations + exit
#[kani::stub(crate::number::is_strong_probable_prime, sprp_unreachable)]
fn next_prime_is_smallest_prime_geq() {
    let n: u64 = kani::any();
    kani::assume(n <= BOUND);
    let q = match next_prime(n) {
        Some(q) => q,
        None => {
            // 37 >= n is always prime, so the scan cannot run out of u64.
            kani::assert(false, "next_prime(n <= 36) is always Some");
            return;
        }
    };
    kani::assert(n <= q && q <= 37, "result in [n, 37]");
    // q prime: 2, or odd with no divisor in 2..=isqrt(q). d is concrete in
    // each unrolled iteration.
    kani::assert(q == 2 || q % 2 == 1, "prime parity");
    let mut d = 2u64;
    while d * d <= q {
        kani::assert(q % d != 0, "the returned value is prime");
        d += 1;
    }
    // Minimality: everything in [n, q) is composite (or < 2). The walk is
    // bounded by the widest prime gap under 37 (24 -> 29), well inside unwind.
    let mut k = n;
    while k < q {
        if k >= 2 {
            let mut has_factor = false;
            let mut e = 2u64;
            while e * e <= k {
                if k % e == 0 {
                    has_factor = true;
                }
                e += 1;
            }
            kani::assert(has_factor, "nothing in [n, q) is prime");
        }
        k += 1;
    }
}
