prd-8 phase 0: first Kani harnesses — InvoiceConstraintSolver, VendorConstraintSet, CommitGate

[promptexecutionerr]

Context

PRD-8 specifies a Kani bit-precise model-checking suite. Three types introduced or hardened in PRD-7 Phase 0 are immediate proof targets with bounded, finite domains:

Type	Location	Property to prove
InvoiceConstraintSolver::validate()	constraints.rs:128	total = subtotal + gst within 1¢; no overflow at f64 extremes
VendorConstraintSet::evaluate()	constraints.rs:74	required_pass = false iff amount == 0.0; strong_ratio ∈ [0.0, 1.0]
evaluate_commit_gate()	pipeline.rs	Every PipelineState<Reconciled> maps to exactly one CommitGate variant; no panic path

Decimal Proxy Pattern

rust_decimal::Decimal is not a Kani primitive. Use i64 mantissa at scale 2 (cents):

let mantissa: i64 = kani::any();
kani::assume(mantissa > 0 && mantissa < 1_000_000_00); // $0.01 – $1,000,000.00
let amount = Decimal::new(mantissa, 2);

For f64 fields (current constraints.rs uses f64): constrain with kani::assume(amount.is_finite() && amount >= 0.0).

Harness Sketches

// kani-proofs/src/invoice_arithmetic.rs
#[kani::proof]
fn invoice_required_pass_iff_arithmetic_holds() {
    let total: f64 = kani::any();
    let subtotal: f64 = kani::any();
    let gst: f64 = kani::any();
    kani::assume(total.is_finite() && subtotal.is_finite() && gst.is_finite());
    kani::assume(total > 0.0 && total < 1_000_000.0);
    let solver = InvoiceConstraintSolver::new();
    let result = solver.validate(total, subtotal, gst);
    // required_pass ↔ |total - subtotal - gst| < 0.01
    let arith_ok = (total - subtotal - gst).abs() < 0.01;
    assert_eq!(result.required_pass, arith_ok);
}

#[kani::proof]
fn commit_gate_is_total() {
    // Every reconciled state routes to exactly one variant — no panic, no unreachable
    let confidence: f32 = kani::any();
    kani::assume(confidence >= 0.0 && confidence <= 1.0);
    let state = PipelineState::<Reconciled>::new_for_kani(confidence);
    let gate = evaluate_commit_gate(&state, 0.85);
    // Assert it is one of the three variants (exhaustiveness — no panic path)
    assert!(matches!(gate,
        CommitGate::Approved { .. } | CommitGate::PendingOperator { .. } | CommitGate::Blocked { .. }
    ));
}

Infrastructure Required

1. kani-proofs/ crate at workspace root with [lib] only, no [[bin]].
2. kani-toolchain.toml pinning a nightly that ships Kani (separate from rust-toolchain.toml channel "1.95").
3. .github/workflows/kani.yml — model-checking/kani-github-action@v1, runs cargo kani --tests on kani-proofs.
4. PipelineState::<Reconciled>::new_for_kani(confidence: f32) test constructor (cfg-gated #[cfg(any(test, kani))]) that constructs the struct without going through the full transition chain — needed because _state: PhantomData<S> is private and transitions require real issue vecs.

Acceptance Criteria

• cargo kani on kani-proofs passes all three harnesses with 0 failures.
• kani.yml CI job runs and is green.
• No changes to rust-toolchain.toml — Kani uses its own toolchain pin.
• kani-proofs/INVENTORY.md lists every harness with status column.

Files

• kani-proofs/ (new crate)
• .github/workflows/kani.yml (new)
• kani-toolchain.toml (new, workspace root)
• crates/ledger-core/src/pipeline.rs — add new_for_kani() constructor

Dependency

Independent of #55. Establishes the CI infrastructure that PRD-6-FUTURE's kani_proof: KaniProofStatus field will reference.