feat(rivet-hygiene): gate integrity + first-flight infrastructure plan (v1.116)#263
Merged
Conversation
… plan (v1.116) Turns the 2026-07 honest assessment (audit vs PX4 1.16 / ArduPilot 4.6 / research frontier) into enforced process + a planned, hardware-targeted requirements ladder. GATE INTEGRITY (SWREQ-RELAY-VGATE-P01, implemented — promotion to verified comes in a SEPARATE PR, per the very rule it introduces): - Orphaned-proof cross-check: run-falcon-verification.py now cross-checks `cargo kani -p <crate>` steps against the kani.yml matrix instead of blindly skipping them — in-matrix ⇒ enforced-by-kani-gate, out-of-matrix ⇒ FAIL. Found one real orphan on first run: relay-traj (CBMC hang, known) — now an explicit LOUD waiver carrying its retirement issue (#260); any NEW orphan fails the gate. - Two-commit rule: check-verification-independence.sh (wired as the gate's first step) fails any PR that changes crates/examples code AND promotes an artifact to verified/accepted in the same change. Tested against the v1.115 range, which it correctly catches. Break-glass env override stays visible in the CI log. FIRST-FLIGHT INFRASTRUCTURE PLAN (SYSREQ-FALCON-021 + 10 swreqs, all release-tagged so `rivet release status` answers "when can we cut"): - v1.117 PARAM-P03 persistence (keystone) + CALIB-P02 flows (+ FAULT-P04 moved from v1.116 — logged scope move) - v1.118 LOG-P02 blackbox + LOG-P03 bit-exact estimator replay - v1.119 MAVLINK-P06 telemetry streaming + in-flight tuning (SiK 433) - v1.120 BATTERY-P02 current/mAh/sag (PM02D) - v1.121 GNSS-P02 dual-M9N blending/failover + RANGEDRV-P01 TF02 Pro - v1.122 NOTCH-P01 RPM-notch + PREARM-P03 check breadth Target vehicle: Pixhawk 6X-RT + Holybro X500 V2 (BOM in FEAT-FALCON-first-flight-hw). OS/silicon integration (RTOS, watchdog, bootloader, bus bindings) is JESS's side per relay#214/jess#62 — the requirements carry the boundary explicitly. Backlog issues: #260 relay-traj proof bounding, #261 swarch decomposition, #262 release-field + named-test backfill. rivet validate PASS; release ladder v1.116–v1.122 queryable. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
- PARAM-P03: byte seam over FM25V02A FRAM (jess DD-016) — wear layer dropped for the FRAM path (no erase pages, ~10^12 endurance). - LOG-P02: block/append seam split made explicit (jess REQ-PIX-022 owns flush ordering + torn-record detectability; relay owns codec/replay). - NOTCH-P01: RPM source decided — bidir-DShot eRPM primary (jess DD-024, FlexIO+eDMA capture), DroneCAN esc.Status alternate. - FEAT umbrella: settled seam decisions + the read-only-until-greenlight HIL constraint + frame confirmed X500 V2 (jess DD-022 said S500). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…ART-P01/P02, v1.123) - PART-P01: separable estimator partition (M4) — grounded (zero f64 in relay-iekf + falcon-core; NavState = 16xf32 sole boundary) with the honest teeth: cascade must be proven robust to 1-2 ticks of NavState transport delay (measured, not asserted). - PART-P02: F100 failsafe partition constraints relay's properties depend on — pass-through fidelity (no re-mixing downstream of the rank-3 allocation) + motors-off on M7 silence; relay specifies + provides conformance fixtures, gale implements (gale#65). - FEAT ladder extended to v1.123. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…et again Timed out at 45m21s all-PASS on 2026-07-11 (cold rivet install + the fetch-depth:0 clone the two-commit rule needs + sweep growth); a timeout reports as 'cancelled' which reads like a gate failure. Durable shrink tracked in #262 (named-test steps). Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
…sting, tracked in #262) Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
avrabe
added a commit
that referenced
this pull request
Jul 11, 2026
…cation PR (#264) Code-free promotion PR, per the rule VGATE-P01 itself introduces: the implementation landed in #263 (main ac57b2c); this PR runs the cited evidence and promotes. Evidence (run 2026-07-11 on ac57b2c, recorded in FV-RELAY-VGATE-001): - kani cross-check: in-matrix steps report enforced-by-kani-gate, exit 0; the pre-waiver run FAILED on the real relay-traj orphan (created #260) — the detector detects; fail-closed on unreadable kani.yml. - waiver loudness: exactly 2 WAIVED-kani-gate lines, each carrying #260. - two-commit detection: the v1.115 violating range (23fc92f...) exits non-zero with both halves listed; compliant range exits 0; ran live on PR #263's gate as its first step. rivet: PASS; `rivet release status falcon-v1.116.0` → ✓ Cuttable. 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.
Verify-Filter: (has-tag "rotor-loss")
Turns the 2026-07 honest assessment (vs PX4 v1.16 / ArduPilot 4.6 / research frontier) into enforced process + a planned, hardware-targeted requirements ladder.
Gate integrity (the audit's top findings, now enforced)
cargo kani -p <crate>steps in FV artifacts are cross-checked against the kani.yml matrix (in-matrix ⇒enforced-by-kani-gate; out-of-matrix ⇒ FAIL). First run found a real orphan: relay-traj (known CBMC hang) — now a loud tracked waiver (relay-traj Kani harnesses hang CBMC — bound and enroll in the kani.yml matrix #260); any new orphan fails.crates//examples/code cannot also promote an artifact toverified/accepted(first step of this required gate; correctly catches the v1.115 range; visible break-glass override).SWREQ-RELAY-VGATE-P01lands asimplemented— its own promotion to verified will come in a separate PR, per the rule it introduces.First-flight infrastructure plan (SYSREQ-FALCON-021 + 10 swreqs)
Release ladder, all queryable via
rivet release status:Target vehicle (BOM in
FEAT-FALCON-first-flight-hw): Pixhawk 6X-RT + Holybro X500 V2, 2× M9N GNSS, TF02 Pro LiDAR, SiK 433 telemetry, 4S 5000 mAh/PM02D. OS + silicon integration is Jess's side (relay#214 ↔ jess#62); requirements carry the boundary explicitly and verify against mock backends until the bindings land.Backlog: #260 (relay-traj proof bounding), #261 (swarch decomposition), #262 (release/named-test backfill).
rivet validate PASS. No flight-code changes in this PR.
🤖 Generated with Claude Code