Add Kani harnesses for stream-transformer state machines (LC, SCH, SC, HS, CFDP)

[avrabe]

Part of the V&V coverage initiative.

Problem

Relay engines are bounded stream transformers. The mathematical backpressure proof exists in Lean (proofs/lean/BackpressureSafety.lean — proves output_count ≤ n·K per engine). What's missing is the Rust-level state-machine verification: Kani harnesses that bound the actual implementation against the Lean spec.

Known per-cycle output bounds:

• LC: 32 violations / cycle
• SCH: 16 actions / tick
• SC: 8 dispatches / tick
• HS: 8 alerts / check
• CFDP: 4 PDU actions / event

Acceptance

• Kani harness per engine verifying per-cycle output bound never exceeded
• Kani harness for state-machine transitions (illegal transitions unreachable)
• Kani harness for error-path closure (every error branch returns Result::Err without panicking)
• Harnesses co-located in each engine crate under tests/kani_<engine>.rs
• CI gate via cargo kani (or cargo-kiln kani-verify)
• Link each harness to the corresponding Lean theorem in rivet.yaml (traceability: Lean spec → Kani harness → Rust impl)

Notes

• Model after kiln-foundation/src/verus_proofs/static_vec_proofs.rs
• Keep the verified subset discipline: no trait objects, no closures in harness bodies