//! Kani proof that [`crate::number::is_strong_probable_prime`] is **sound**
//! over the 8-bit slice: every prime passes every base — the same direction as
//! the Lean `is_strong_probable_prime_spec` (prime ⟹ passes), which proves it
//! unbounded. Primality of `n` is established independently in the harness by
//! odd trial division (concrete divisors per unrolled iteration — cheap), so
//! the assertion makes the SAT solver certify the Miller–Rabin theory itself
//! (Fermat + the square-root chain) on the real compiled `modpow` composition,
//! bit-blasted exhaustively over all 8-bit primes and all bases.
//!
//! No completeness clause: a composite may legitimately pass a strong-liar
//! base (`2047`/base-2 is the doctest example), so `composite ⟹ fails` is not
//! a theorem. The quantitative liar bound is the Lean side's
//! `spp_base_count_le` (Rabin ¾, `MillerRabin/SppCount.lean`).
//!
//! The base stays full-width symbolic: `is_strong_probable_prime` reduces
//! `a % n` first, so slicing `a` would only shadow the reduction. The 8-bit
//! `n` matches `modpow_naive`/`mulmod_widening` — the `u128` mul/mod circuits
//! inside `modpow` are the cost driver (see `mulmod_widening.rs`).
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/PrimalitySpec.lean` proves the
//! corollary `sprp_passes_all_primes` — the identical statement (prime ⟹
//! passes, every base), on the extracted model, unbounded over all of `u64`.
//! 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::is_strong_probable_prime;

#[kani::proof]
#[kani::unwind(12)] // modpow walks <= 8 exponent bits; the trial sweep <= 7 odd q; squarings <= 6
fn sprp_passes_all_primes() {
    let n: u64 = kani::any();
    let a: u64 = kani::any();
    kani::assume(n < (1 << 8));
    // n prime, by the independent definition: 2, or odd with no odd divisor in
    // 3..=isqrt(n). q is concrete in each unrolled iteration.
    if n != 2 {
        kani::assume(n > 2 && n % 2 == 1);
        let mut q = 3u64;
        while q * q <= n {
            kani::assume(n % q != 0);
            q += 2;
        }
    }
    kani::assert(
        is_strong_probable_prime(n, a),
        "every prime passes every Miller-Rabin base",
    );
}
