//! Kani proof — [`crate::number::modpow`] agrees with naive
//! repeated-multiplication exponentiation over a symbolic 8-bit slice.
//!
//! The oracle is *linear* exponentiation — `exp` repeated modular
//! multiplications, no squaring — a computationally distinct route to
//! `base^exp mod modulus`; a bug in the square-and-multiply bit walk produces a
//! different residue and the equality breaks.
//!
//! Scope: modpow's inner arithmetic is `u128` (two 128-bit
//! `% m` per exponent bit), which CBMC bit-blasts; only a small slice is
//! tractable, and an 8-bit symbolic slice is dominated by the concrete
//! `modpow_differential_wide` test in [`crate::number`] (right-to-left vs an
//! independent left-to-right oracle over a dense grid + 200k full-range
//! triples). This harness is a machine-checked proof over a small symbolic
//! domain and a regression anchor, not the breadth tier.
#![allow(
    clippy::arithmetic_side_effects, // arithmetic is the subject under test
    clippy::cast_possible_truncation // acc < modulus <= u64::MAX fits u64
)]

use crate::number::modpow;

/// Naive modular exponentiation — independent of square-and-multiply; mirrors
/// the unit-test oracle.
fn naive_modpow(base: u64, exp: u64, modulus: u64) -> u64 {
    if modulus <= 1 {
        return 0;
    }
    let m = u128::from(modulus);
    let b = u128::from(base) % m;
    let mut acc: u128 = 1;
    for _ in 0..exp {
        acc = acc * b % m;
    }
    acc as u64
}

// BOUNDS: unwind = 12; reason = the linear oracle loops `exp` times and exp < 8,
// so <= 7 iterations (square-and-multiply does <= 3); 12 gives headroom for the
// loop-exit assertion. The `assume`s bound base/modulus to 8 bits so CBMC can
// discharge the u128 arithmetic.
#[kani::proof]
#[kani::unwind(12)]
fn modpow_matches_naive() {
    let base: u64 = kani::any();
    let exp: u64 = kani::any();
    let modulus: u64 = kani::any();
    kani::assume(base < (1 << 8));
    kani::assume(exp < 8);
    kani::assume(modulus < (1 << 8));
    kani::assert(
        modpow(base, exp, modulus) == naive_modpow(base, exp, modulus),
        "modpow == naive repeated-multiplication modpow",
    );
}
