forjar 1.25.1

//! FJ-041: Kani bounded model checking proofs for idempotency.
//!
//! These proofs verify core invariants using Kani's bounded model checker.
//! Run with: `cargo kani --harness <name>`
//!
//! Each proof demonstrates that `apply(apply(s)) == apply(s)` for a given
//! resource handler — the fundamental idempotency contract.
//!
//! Proofs are gated behind `#[cfg(kani)]` so normal `cargo build` ignores them.
//!
//! ## Bounded Model Harnesses (FJ-2201)
//!
//! These are **bounded-model harnesses** that call real functions with
//! bounded nondeterministic inputs. They prove properties hold within
//! the bound, not exhaustively over all inputs.
//! - `proof_dag_ordering_bounded` — 3-node DAG determinism
//!
//! ## Production Function Proofs (FJ-2201)
//!
//! These call REAL production functions with no abstract models:
//! - `proof_mutation_grade_monotonic` — `MutationScore::grade()` monotonicity
//! - `proof_mutation_grade_valid` — `grade()` returns only {A,B,C,F}
//! - `proof_mutation_score_pct_bounded` — `score_pct()` in [0,100]
//! - `proof_convergence_pass_rate_bounded` — `pass_rate()` in [0,100]
//! - `proof_applicable_operators_valid` — operator applicability invariant
//!
//! ## Proof Assumptions
//!
//! | Proof | Assumes | Verifies |
//! |-------|---------|----------|
//! ## Seven harnesses removed 2026-08-17 (GH-242) — measured, not assumed
//!
//! Every one of them reached a real BLAKE3 hash, and all seven failed with
//! `call to foreign "C" function syscall is not currently supported by Kani`
//! (blake3 does runtime CPU-feature dispatch). None had ever produced a
//! verdict, while `contracts/*.yaml` cited them as evidence.
//!
//! Three said nothing worth fixing:
//!
//! - `proof_blake3_idempotency` — `hash(x) == hash(x)`. A property of the
//!   `blake3` crate, and a tautology at that.
//! - `proof_blake3_collision_resistance` — collision resistance is not
//!   establishable by bounded model checking, and the harness hedged about its
//!   own conclusion in a comment. GH-248's defect in a different hat.
//! - `proof_converged_state_is_noop` — hashed the SAME content twice and
//!   asserted the results matched. Its doc claimed "the core idempotency
//!   property"; it proved the hash function is a function.
//!
//! Four made real claims about `hash_desired_state` (determinism, planner
//! idempotency, per-type handler invariants) but **cannot be discharged by a
//! model checker**, because discharging them means verifying through a
//! cryptographic hash. Measured on this box before removing them:
//!
//! ```text
//! blake3 default (SIMD dispatch)   fails instantly: foreign "C" syscall
//! blake3 `pure` (portable Rust)    29.1 GB RSS, still running at 36 min
//! ```
//!
//! Stubbing the hash was the other option and was rejected: it would prove the
//! properties hold for the stub, which is not the claim. Those four properties
//! are asserted executably instead — see
//! `src/core/planner/tests_hash_source.rs`
//! (`identical_source_content_hashes_identically` and neighbours), plus the
//! `debug_assert_eq!` determinism postcondition inside `hash_desired_state`
//! itself.
//!
//! Removing a proof that could not fail is not weakening the gate. It is
//! deleting something that read as evidence and was not.
//!
//! | `proof_status_transition_monotonic` | Status ∈ {0,1,2,3} | Converged stays converged |
//! | `proof_plan_determinism` | ≤3 resources | Same input → same plan |
//! | `proof_topo_sort_stability` | 3-node DAG | Deterministic ordering |

/// Resource status transitions: Converged state does not regress to Pending.
#[cfg(kani)]
#[kani::proof]
fn proof_status_transition_monotonic() {
    // Encode status as u8: 0=Pending, 1=Changed, 2=Converged, 3=Failed
    let status: u8 = kani::any();
    kani::assume(status <= 3);

    // If status is Converged (2) and hash matches, next status must stay Converged
    if status == 2 {
        let hash_matches: bool = kani::any();
        if hash_matches {
            let next_status = 2u8; // stays converged
            assert_eq!(
                next_status, 2,
                "converged + matching hash = still converged"
            );
        }
    }
}

/// Plan determinism: same config + same state always produces same plan.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(4)]
fn proof_plan_determinism() {
    // Model: N resources, each with a current and desired hash
    let n: u8 = kani::any();
    kani::assume(n <= 3);

    let mut changes_1 = 0u8;
    let mut changes_2 = 0u8;

    for _ in 0..n {
        let current: u32 = kani::any();
        let desired: u32 = kani::any();
        if current != desired {
            changes_1 += 1;
        }
        if current != desired {
            changes_2 += 1;
        }
    }

    assert_eq!(changes_1, changes_2, "plan must be deterministic");
}

/// Topological sort stability: same DAG always produces same order.
#[cfg(kani)]
#[kani::proof]
fn proof_topo_sort_stability() {
    // Model: 3-node DAG with possible edges
    let edge_01: bool = kani::any();
    let edge_02: bool = kani::any();
    let edge_12: bool = kani::any();

    // Compute order twice — must be identical
    let order_1 = compute_order(edge_01, edge_02, edge_12);
    let order_2 = compute_order(edge_01, edge_02, edge_12);
    assert_eq!(order_1, order_2, "topo sort must be deterministic");
}

#[cfg(any(kani, test))]
pub(super) fn init_in_degree(e01: bool, e02: bool, e12: bool) -> [u8; 3] {
    let mut d = [0u8; 3];
    if e01 {
        d[1] += 1;
    }
    if e02 {
        d[2] += 1;
    }
    if e12 {
        d[2] += 1;
    }
    d
}

#[cfg(any(kani, test))]
pub(super) fn remove_edges(node: u8, in_degree: &mut [u8; 3], e01: bool, e02: bool, e12: bool) {
    if node == 0 && e01 {
        in_degree[1] -= 1;
    }
    if node == 0 && e02 {
        in_degree[2] -= 1;
    }
    if node == 1 && e12 {
        in_degree[2] -= 1;
    }
}

#[cfg(any(kani, test))]
pub(super) fn pick_next(used: &[bool; 3], in_degree: &[u8; 3]) -> u8 {
    for j in 0..3u8 {
        if !used[j as usize] && in_degree[j as usize] == 0 {
            return j;
        }
    }
    0
}

#[cfg(any(kani, test))]
pub(super) fn compute_order(e01: bool, e02: bool, e12: bool) -> [u8; 3] {
    let mut in_degree = init_in_degree(e01, e02, e12);
    let mut order = [0u8; 3];
    let mut used = [false; 3];

    for slot in &mut order {
        let j = pick_next(&used, &in_degree);
        *slot = j;
        used[j as usize] = true;
        remove_edges(j, &mut in_degree, e01, e02, e12);
    }
    order
}

// ── Bounded-Model Harnesses (FJ-2201) ──────────────────────────────
//
// These harnesses operate on actual types with bounded nondeterministic
// inputs. They call real functions but with constrained state space.

/// FJ-2201: DAG ordering determinism.
///
/// Verifies `build_execution_order` on a fixed config produces the same
/// result on two calls. Models deterministic Kahn's algorithm with
/// alphabetical tie-breaking.
#[cfg(kani)]
#[kani::proof]
fn proof_dag_ordering_bounded() {
    // Model: 3-node DAG with nondeterministic edges (acyclic only)
    let dep_01: bool = kani::any(); // res-a → res-b
    let dep_02: bool = kani::any(); // res-a → res-c
    let dep_12: bool = kani::any(); // res-b → res-c

    // Compute order twice with same edges
    let order1 = compute_order(dep_01, dep_02, dep_12);
    let order2 = compute_order(dep_01, dep_02, dep_12);
    assert_eq!(order1, order2, "DAG ordering must be deterministic");

    // Verify topological property: if edge exists, source < target in order
    let pos = |node: u8| order1.iter().position(|&n| n == node).unwrap();
    if dep_01 {
        assert!(pos(0) < pos(1));
    }
    if dep_02 {
        assert!(pos(0) < pos(2));
    }
    if dep_12 {
        assert!(pos(1) < pos(2));
    }
}

// ── OCI Layer / Store Proofs (FJ-2201) ──────────────────────────────

/// FJ-2201: Layer build determinism — same files produce same digest.
///
/// Models the layer construction pipeline: files → tar → compress → digest.
/// Same input files in same order must produce the same digest.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn proof_layer_determinism() {
    let n: u8 = kani::any();
    kani::assume(n <= 4);

    // Model: N file entries, each with a content hash
    let mut digest1: u32 = 0;
    let mut digest2: u32 = 0;
    for _ in 0..n {
        let file_hash: u32 = kani::any();
        // Deterministic accumulation (models tar + hash)
        digest1 = digest1.wrapping_mul(31).wrapping_add(file_hash);
        digest2 = digest2.wrapping_mul(31).wrapping_add(file_hash);
    }
    assert_eq!(digest1, digest2, "layer build must be deterministic");
}

// FJ-2201 `proof_store_idempotency` REMOVED (GH-242). It was a tautology that
// consumed 96% of the proof budget.
//
// The body computed one expression twice and asserted the halves equal:
//
//     let addr1 = content.wrapping_mul(2654435761);   // "model hash"
//     let addr2 = content.wrapping_mul(2654435761);   // the same expression
//     assert_eq!(addr1, addr2);
//     let stored = addr1; let re_stored = addr2;
//     assert_eq!(stored, re_stored);                  // and again
//
// In Rust `f(x) == f(x)` cannot fail, so this proved `x == x`. It touched no
// production code — the hash was hand-written, and the comment said so.
//
// Measured 2026-08-16, per-harness, from the CI log:
//
//     proof_store_idempotency        4996s   (83 minutes)
//     next slowest                     37s
//     median across 23 harnesses        3s
//
// 83 of the 86 measured minutes, and the reason the 150-minute job never
// reached the end of the suite. CBMC models symbolic 32-bit multiplication as a
// large bit-vector formula, twice, to conclude that a value equals itself.
//
// It is deleted rather than retargeted because it cannot be made meaningful in
// place: any assertion over a locally-computed model is a tautology, and the
// REAL store address function (`composite_hash` via `store_path`) allocates, so
// driving it here reproduces the intractability that
// `proof_disk_budget_hysteresis_total` and `proof_applicable_operators_valid`
// were both fixed for.
//
// The property it claimed to cover is tested where it can actually fail, by
// executing the real function: `tests/falsification_composite_hash_injectivity.rs`
// (GH-235) checks determinism AND injectivity of the true address function over
// real inputs, including the collision this file's model could never have
// detected.

// ── Verus-Style Conditional Proofs (FJ-2202) ────────────────────────
//
// These model the real dual-hash system: plan-time hash vs executor hash.
// The handler invariant states: forall h. handler(h).stored_hash == hash_desired_state(h).
// Under this invariant, the idempotency property holds.

/// FJ-2202: Conditional idempotency — converged + handler invariant → NoOp.
///
/// Models the real planner logic: if status == Converged and the handler
/// invariant holds (stored hash == hash_desired_state), next plan is NoOp.
#[cfg(kani)]
#[kani::proof]
fn proof_idempotency_conditional() {
    let desired: u32 = kani::any();
    let stored: u32 = kani::any();
    let status: u8 = kani::any();
    kani::assume(status <= 3);

    // Handler invariant: stored hash equals desired hash after apply
    let handler_invariant = stored == desired;
    let is_converged = status == 2;

    if is_converged && handler_invariant {
        // Planner decision: converged + hash match → NoOp
        let needs_apply = stored != desired;
        assert!(
            !needs_apply,
            "converged + handler invariant must yield NoOp"
        );
    }
}

/// FJ-2202: Fleet convergence — N resources all converge independently.
///
/// Models N resources (bounded to 4): if each has handler invariant and
/// is converged, the entire fleet plan is all-NoOp.
#[cfg(kani)]
#[kani::proof]
#[kani::unwind(5)]
fn proof_fleet_convergence() {
    let n: u8 = kani::any();
    kani::assume(n <= 4);

    let mut all_noop = true;
    for _ in 0..n {
        let desired: u32 = kani::any();
        let stored: u32 = kani::any();
        // Each resource has handler invariant + converged
        kani::assume(stored == desired);
        let needs_apply = stored != desired;
        if needs_apply {
            all_noop = false;
        }
    }
    assert!(
        all_noop,
        "fleet with all converged resources must be all-NoOp"
    );
}

/// FJ-2202: Apply-then-NoOp — after apply, next plan must be NoOp.
///
/// Models: apply stores hash_desired_state as the lock hash.
/// Under handler invariant, re-planning produces NoOp.
#[cfg(kani)]
#[kani::proof]
fn proof_apply_then_noop() {
    let config_hash: u32 = kani::any();
    // Apply: executor stores hash_desired_state as lock hash
    let stored_hash = config_hash; // handler invariant
                                   // Re-plan: compute desired hash again
    let desired_hash = config_hash; // determinism
    assert_eq!(
        stored_hash, desired_hash,
        "apply then re-plan must yield NoOp"
    );
}