//! Kani proof of the two structural invariants of `continued_fraction`'s
//! convergents, over the input slice `a, b < 2^8`:
//!   • the determinant identity `hₖ·kₖ₋₁ − hₖ₋₁·kₖ = ±1` for every consecutive
//!     pair — the cofactor relation that makes the convergents best rational
//!     approximations; and
//!   • reconstruction — the last convergent is `a/b` in lowest terms.
//!
//! `continued_fraction` is division-only and bit-blasts cleanly over the whole
//! domain, but the convergent recurrence and the identity *multiply*, and a
//! symbolic 64-bit multiply is SAT-hard. Slicing to `a, b < 2^8` keeps every
//! product below `2^16` (and the expansion to ≤ 12 terms). The full domain is
//! covered by the 100k-pair differential test and the determinant/reconstruction
//! fuzz target.

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

#[kani::proof]
#[kani::unwind(14)] // ≤ 12 partial quotients for a, b < 2^8; +margin for the exit check
fn continued_fraction_convergent_identity() {
    let a: u64 = kani::any();
    let b: u64 = kani::any();
    kani::assume(a < (1u64 << 8));
    kani::assume(b < (1u64 << 8));

    let cf = continued_fraction(a, b);

    let mut prev: Option<(u64, u64)> = None;
    let mut last = (0u64, 0u64);
    for (h, k) in cf.convergents() {
        if let Some((ph, pk)) = prev {
            // |hₖ·kₖ₋₁ − hₖ₋₁·kₖ| = 1; both products are below 2^16 in this slice.
            kani::assert((h * pk).abs_diff(ph * k) == 1, "determinant identity");
        }
        prev = Some((h, k));
        last = (h, k);
    }

    // Reconstruction: the last convergent equals a/b in lowest terms, i.e.
    // (a/g, b/g) with g = gcd(a, b). (Skip b = 0, the a/0 ↦ [a] convention.)
    if b >= 1 {
        let g = gcd(a, b);
        kani::assert(last.0 * g == a, "last numerator · gcd == a");
        kani::assert(last.1 * g == b, "last denominator · gcd == b");
    }
}
