//! Kani proof that [`crate::number::factorize`] returns the prime factorization,
//! over the slice `n <= 40` — the clauses of the Lean `factorize_spec`
//! (`verify-lean/Coprime/FactorizeSpec.lean`), mirrored on the real compiled
//! code exactly where the Lean leg is weakest (that proof is *partial*
//! correctness, conditional on `DET12`):
//!
//!   1. `len <= 15` (the capacity claim);
//!   2. `n < 2` ⟹ the empty factorization;
//!   3. `2 <= n` ⟹ the product of the entries' `p^e` recovers `n`;
//!   4. every entry's `p` is prime (checked by trial division to the square
//!      root — exact, not probabilistic) and every exponent is `>= 1`;
//!   5. entries strictly ascending by prime.
//!
//! **Why `n <= 40`:** every prime factor of `n <= 40` is `<= 37`, the last
//! hard-coded Miller–Rabin witness, so `is_prime` on the surviving trial-division
//! residual always decides in its witness equality/divisibility fast path. The
//! SPRP tail (`modpow`'s symbolic 64-bit multiplies — the SAT-hard case, see
//! `isqrt_floor.rs`) and the Brent–Pollard splitter (recursive, with `mulmod` in
//! every loop) are then *mathematically* unreachable. The two stubs below pin
//! that with a panic: if a future edit ever routes this slice into either one,
//! the proof goes red instead of silently bit-blasting forever — the same
//! anti-vacuity discipline as the Lean proof's pin, and what keeps the call
//! graph CBMC must encode small enough to converge.
//!
//! The checker loops are capped at 3 distinct primes and exponent 5; the caps
//! are themselves asserted first (`2·3·5·7 > 40`, `2^6 > 40`), so they cannot
//! mask a violation — an over-long or over-tall factorization fails the cap
//! assert before the cap trims the walk.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/FactorizeSpec.lean` proves the
//! corollary `factorize_is_prime_factorization` — the same clauses (1)–(5) in
//! the same order, on the extracted model, for all `u64` (partial-correctness
//! style, conditional on `DET12`, like `factorize_spec` itself). The `len <= 3`
//! / `e <= 5` asserts here are slice-licensing for the capped walk, not spec
//! content, and are not mirrored. 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::factorize;

/// The slice bound: keeps every residual prime inside the witness fast path.
const BOUND: u64 = 40;

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

/// Stub for `pollard_split`: unreachable on this slice (every residual is
/// prime, so `factor_recurse` never splits). Reaching it fails the proof.
fn pollard_unreachable(_n: u64) -> u64 {
    unreachable!("pollard_split entered on n <= 40: composite residual survived trial division")
}

#[kani::proof]
#[kani::unwind(14)] // is_prime's witness loop is the longest: 12 iterations + exit
#[kani::stub(crate::number::is_strong_probable_prime, sprp_unreachable)]
#[kani::stub(crate::number::factor::pollard_split, pollard_unreachable)]
fn factorize_is_prime_factorization() {
    let n: u64 = kani::any();
    kani::assume(n <= BOUND);
    let f = factorize(n);
    let s = f.as_slice();

    // (1) capacity, and the slice-specific tightening that licenses the capped
    //     walk below: 2·3·5·7 = 210 > 40, so at most 3 distinct primes; 2^6 = 64
    //     > 40, so every exponent is at most 5.
    kani::assert(s.len() <= 15, "at most fifteen distinct primes (capacity)");
    kani::assert(s.len() <= 3, "at most three distinct primes for n <= 40");

    // (2) 0 and 1: the empty product.
    if n < 2 {
        kani::assert(s.is_empty(), "0 and 1 have no prime factors");
    }

    // (3)-(5) one walk over the entries.
    let mut prod: u64 = 1;
    let mut i = 0usize;
    while i < s.len() && i < 3 {
        let (p, e) = s[i];
        kani::assert(2 <= p && p <= BOUND, "factor in 2..=n range");
        kani::assert(1 <= e && e <= 5, "exponent in 1..=5 on this slice");
        // (4) exact primality: no q in 2..=isqrt(p) divides p. q is concrete in
        //     each unrolled iteration, so q*q and p % q are cheap circuits.
        let mut q = 2u64;
        while q * q <= p {
            kani::assert(p % q != 0, "every factor is prime");
            q += 1;
        }
        // (5) strict ascent (distinctness included).
        if i > 0 {
            kani::assert(s[i - 1].0 < p, "strictly ascending by prime");
        }
        let mut j = 0u32;
        while j < e && j < 5 {
            prod = prod.saturating_mul(p);
            j += 1;
        }
        i += 1;
    }
    // (3) the entries multiply back to n. Saturation cannot mask a mismatch:
    //     u64::MAX > 40 >= n.
    if n >= 2 {
        kani::assert(prod == n, "product of p^e over the entries recovers n");
    }
}
