v1.108 — complete the orphaned-proof sweep (11 crates / 26 Kani harnesses gated)#247
Merged
Merged
Conversation
… 26 Kani harnesses gated) Closes the systemic orphaned-proof gap begun in v1.104. The workspace scan found 36/142 Kani harnesses unenforced; v1.104 gated the 8 flight-critical control/estimator ones. This gates the remaining tractable sweep — 26 harnesses across 11 crates (relay-avoid/flowrange/mix-multi/nid/offboard/sensvote, falcon-baromag/esc-dshot/gnss-ubx, relay-log/modextra) — all VERIFICATION SUCCESSFUL locally. The Kani gate now enforces 33 of 34 previously-orphaned harnesses. DEFERRED (logged): relay-traj is NOT gated — verify_peak_jerk_sound hangs CBMC (>1200s, f32 intractability); gating it would hang the Kani CI job. Needs unwind bounds + input concretisation first. Only remaining unenforced Kani crate. FV-RELAY-KANICI-003 (verifies 11 requirements). Kani-only gate this slice; clippy gating for these diverse infra/driver crates is a separate scope. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Completing the orphaned-proof closure
The workspace scan found 36/142 Kani harnesses (25%) unenforced. v1.104 gated the 8 flight-critical control/estimator proofs; this PR gates the remaining tractable sweep — 26 harnesses across 11 crates, all
VERIFICATION SUCCESSFULlocally (cargo kani):The Kani gate now enforces 33 of 34 previously-orphaned harnesses.
Deferred (logged — not silently dropped)
relay-traj is not gated:
verify_peak_jerk_soundhangs CBMC (>1200 s local timeout — the known f32/symbolic-slice intractability). Gating it would hang the Kani CI job. It needs unwind bounds + input concretisation first; that's the follow-up. It's the only remaining unenforced Kani crate after this release.Verification
VERIFICATION SUCCESSFULlocally.rivet validate: PASS.FV-RELAY-KANICI-003verifies 11 requirements.kani.yml) is the enforcing oracle — the newly-gated matrix legs must go green.Kani-only this slice; clippy gating for these diverse infra/driver crates is separate scope (avoids pulling out-of-scope cFS-adjacent lint noise).
🤖 Generated with Claude Code