//! Kani proof — [`crate::number::lcm`] computes the least common multiple, as a
//! *symbolic* check over every pair of 8-bit operands.
//!
//! The oracle is algebra **over the output** — the defining identity
//! `gcd(a, b) * lcm(a, b) == a * b` (formed in `u128`, distinct from `lcm`'s own
//! `a / gcd * b` computation) and that the result is a common multiple of both
//! inputs — not a re-run of `lcm`'s steps.
//!
//! Scope: `lcm` calls `gcd` (a `u64`-division loop) plus one `checked_mul`; it
//! has **no `i128`**, so it bit-blasts far more cheaply than `extended_gcd` and
//! 8-bit verifies quickly. The `None` (overflow) boundary sits near `2^32` and is
//! out of this slice — covered by the concrete `lcm` doctests / property tests;
//! this harness is the machine-checked proof of the value identity over the
//! symbolic interior, and a regression anchor.
//!
//! **Congruent Lean twin:** `verify-lean/Coprime/LcmSpec.lean` proves the
//! corollary `lcm_satisfies_gcd_identity` — the same clauses (the identity and
//! common-multiple checks on `Some`; the `None` arm's unreachability as the
//! slice-guarded clause), on the extracted model, unbounded over all of `u64`.
//! Keep the two in sync by name and clause.
#![allow(clippy::arithmetic_side_effects)] // arithmetic is the subject under test

use crate::number::{gcd, lcm};

// BOUNDS: unwind = 15; reason = `gcd`'s Euclid loop on operands `< 2^8` takes at
// most ~12 steps — its worst case is consecutive Fibonacci numbers
// (F_13 = 233 < 2^8 < F_14 = 377) — so 15 covers the recurrence plus the
// loop-exit assertion. 8-bit is the committed bound: no `i128`, so it verifies
// fast; the overflow boundary near `2^32` is out of slice (tested concretely).
#[kani::proof]
#[kani::unwind(15)]
fn lcm_satisfies_gcd_identity() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    kani::assume(a < (1 << 8));
    kani::assume(b < (1 << 8));

    let g = gcd(a, b);
    match lcm(a, b) {
        Some(l) => {
            // Defining identity, computed in u128 over the output (so the product
            // never overflows): gcd and lcm are complementary cofactors of a*b.
            kani::assert(
                u128::from(g) * u128::from(l) == u128::from(a) * u128::from(b),
                "gcd(a, b) * lcm(a, b) == a * b",
            );
            // The result is a common multiple of both inputs.
            kani::assert(
                (a == 0 || l % a == 0) && (b == 0 || l % b == 0),
                "lcm(a, b) is a common multiple of a and b",
            );
        }
        None => {
            // For 8-bit operands `a*b < 2^16` always fits `u64`, so `lcm` never
            // overflows in this slice: the model checker confirms this arm is
            // unreachable. (The overflow path is exercised by the concrete tests.)
            kani::assert(false, "lcm cannot overflow for 8-bit operands");
        }
    }
}
