//! Kani proof that [`crate::number::sort_factors`] establishes its postcondition
//! — the output is non-decreasing by prime AND a permutation of the input — over
//! symbolic arrays of length `N = 4`.
//!
//! Unlike the other harnesses in this crate, the bound here is on the array
//! *length*, not the value width. The sort performs only key comparisons and
//! element swaps — no arithmetic on the values — so it bit-blasts cleanly at full
//! `u64` key width; there is no SAT-hard multiply to slice around (contrast
//! `isqrt`/`cfrac`, bounded by the multiply in their postconditions). `N = 4`
//! admits every up-to-three-step bubble, which is exactly what discriminates the
//! load-bearing inner-loop decrement (`j -= 1`) from a mutation that leaves `j`
//! unchanged: such a mutation half-finishes a multi-element bubble and breaks
//! sortedness, so the proof fails on a counterexample a single nearly-sorted KAT
//! would miss. The realized array is `<= 15` entries of distinct primes, covered
//! concretely by the `factorize` differential tests; permutation-preservation
//! also holds by construction here (the body only swaps), and the proof pins it
//! so a future edit cannot silently drop or duplicate a factor while staying
//! sorted.
#![allow(clippy::arithmetic_side_effects)] // index/counter arithmetic is the harness, not the subject

use crate::number::sort_factors;

const N: usize = 4;

/// Count occurrences of the exact `(prime, exponent)` pair `key` in `arr` — the
/// multiset primitive for the permutation clause. Full-pair (not key-only) so a
/// mutation that scrambled an exponent off its prime would also be caught.
fn count(arr: &[(u64, u32); N], key: (u64, u32)) -> usize {
    let mut c = 0usize;
    let mut i = 0usize;
    while i < N {
        if arr[i] == key {
            c += 1;
        }
        i += 1;
    }
    c
}

#[kani::proof]
#[kani::unwind(6)] // every loop here trips at most N = 4 times; +margin for the exit check
fn sort_factors_ascending_perm() {
    // Build a fully symbolic [(u64, u32); 4] elementwise (no reliance on a tuple
    // `Arbitrary` impl). The exponents are symbolic too, so they must ride their
    // primes through every swap.
    let mut a: [(u64, u32); N] = [(0, 0); N];
    let mut i = 0usize;
    while i < N {
        a[i] = (kani::any(), kani::any());
        i += 1;
    }
    let input = a; // snapshot before sorting

    sort_factors(&mut a);

    // (1) Sorted: non-decreasing by prime. This is the clause the `-= → /=`
    //     inner-loop mutation breaks (it leaves a multi-step bubble half-done),
    //     and under which the `> → >=` guard mutation is equivalent (distinct or
    //     equal keys both terminate sorted) — so the proof catches one and
    //     vindicates the other, which is the whole point of proving over output.
    let mut i = 1usize;
    while i < N {
        kani::assert(a[i - 1].0 <= a[i].0, "non-decreasing by prime");
        i += 1;
    }

    // (2) Permutation: every pair occurs the same number of times after sorting
    //     as before. A sort that dropped or duplicated a factor would corrupt the
    //     factorization while still being sorted, so sortedness alone is not the
    //     full postcondition.
    let mut v = 0usize;
    while v < N {
        kani::assert(
            count(&input, input[v]) == count(&a, input[v]),
            "multiset of (prime, exponent) pairs preserved",
        );
        v += 1;
    }
}
