Context
The v1.116 verification-gate cross-check (orphaned-proof detector) flagged the only crate whose cited Kani proofs CI cannot run: relay-traj. Its two harnesses (verify_gate_factor_bounded, verify_peak_jerk_sound) are cited by FV-FALCON-TRAJ-001/002 but the crate is deliberately not in the kani.yml matrix — verify_peak_jerk_sound hangs CBMC (>1200 s, f32 intractability; noted in kani.yml since the v1.108 orphaned-proof sweep).
Why it matters
An out-of-matrix cited proof is exactly how MIX-P05..08 went unenforced for ~40 releases. The gate now carries an explicit WAIVER for relay-traj (visible in every run, referencing this issue) — but a waiver is a debt, not a resolution.
Scope
Bound the harness so CBMC terminates (unwind bounds, concretization, or splitting the f32 arithmetic — the same pattern used for other f32-heavy harnesses), verify locally, add relay-traj to the kani.yml matrix, and REMOVE the waiver from scripts/run-falcon-verification.py. Done = gate cross-check green with zero waivers.
Context
The v1.116 verification-gate cross-check (orphaned-proof detector) flagged the only crate whose cited Kani proofs CI cannot run:
relay-traj. Its two harnesses (verify_gate_factor_bounded,verify_peak_jerk_sound) are cited by FV-FALCON-TRAJ-001/002 but the crate is deliberately not in the kani.yml matrix —verify_peak_jerk_soundhangs CBMC (>1200 s, f32 intractability; noted in kani.yml since the v1.108 orphaned-proof sweep).Why it matters
An out-of-matrix cited proof is exactly how MIX-P05..08 went unenforced for ~40 releases. The gate now carries an explicit WAIVER for relay-traj (visible in every run, referencing this issue) — but a waiver is a debt, not a resolution.
Scope
Bound the harness so CBMC terminates (unwind bounds, concretization, or splitting the f32 arithmetic — the same pattern used for other f32-heavy harnesses), verify locally, add
relay-trajto the kani.yml matrix, and REMOVE the waiver from scripts/run-falcon-verification.py. Done = gate cross-check green with zero waivers.