//! Kani proofs that [`crate::number::gcd`] is the greatest common divisor — the
//! defining clauses, not a no-panic tautology (a `%` loop cannot overflow; see
//! VERIFICATION.md's note on why a bare no-panic harness would prove nothing).
//! The Lean `GcdSpec` proves `≡ Nat.gcd` unbounded; these check the same
//! mathematical content on the real compiled code, split by what each clause
//! costs CBMC:
//!
//! - `gcd_divides_both` — the *divisor* clauses (`g | a`, `g | b`, `g = 0` only
//!   for `gcd(0,0)`) over the **8-bit slice**. The cost driver is the Euclid
//!   loop itself: each unrolled iteration is a division with a *symbolic*
//!   divisor, and a chain of those is the SAT-hard case (like the symbolic
//!   multiply `isqrt_floor.rs` slices around) — observed not to converge at 16
//!   bits (~23 chained dividers, Lamé) and beyond, while 8 bits (≤ 13) proves
//!   in seconds. Same slice width as `modpow_naive` and `mulmod_widening`.
//! - `gcd_is_greatest` — the *greatest* clause (every common divisor of `a` and
//!   `b` divides `g` — the gcd lattice property, stronger than `<=`) over a
//!   **6-bit slice**. The sweep variable is concrete in each unrolled
//!   iteration, so the three `% d` checks are division-by-constant circuits;
//!   this clause quantifies over divisors, so the sweep must cover the whole
//!   slice and the width stays a notch lower.
//!
//! **Congruent Lean twins:** `verify-lean/Coprime/GcdSpec.lean` proves the
//! corollaries `gcd_divides_both` and `gcd_is_greatest` — the same clauses, on
//! the extracted model, unbounded over all of `u64` (the greatest clause over
//! all divisors `d >= 1`, not a sweep). Keep each pair in sync by name and
//! clause.
#![allow(clippy::arithmetic_side_effects)] // checker arithmetic is the harness, not the subject

use crate::number::gcd;

#[kani::proof]
#[kani::unwind(16)] // Lamé: 8-bit Euclid terminates within 13 steps; +margin
fn gcd_divides_both() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    kani::assume(a < (1u64 << 8) && b < (1u64 << 8));
    let g = gcd(a, b);
    if a == 0 && b == 0 {
        kani::assert(g == 0, "gcd(0, 0) == 0");
    } else {
        kani::assert(g >= 1, "gcd is positive when an argument is");
        kani::assert(a % g == 0, "gcd divides a");
        kani::assert(b % g == 0, "gcd divides b");
    }
}

#[kani::proof]
#[kani::unwind(66)] // the divisor sweep walks d = 1..64; the Euclid loop is far shorter
fn gcd_is_greatest() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    kani::assume(a < 64 && b < 64);
    let g = gcd(a, b);
    // Every common divisor divides g (so in particular none exceeds it). With
    // a, b < 64 every candidate divisor is < 64, so the sweep is exhaustive.
    let mut d: u64 = 1;
    while d < 64 {
        if a % d == 0 && b % d == 0 {
            kani::assert(g % d == 0, "every common divisor divides the gcd");
        }
        d += 1;
    }
}
