From 0bf15e9a08e105422a02263bc0a4e8c74361ca9e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 11:41:18 +0200 Subject: [PATCH] =?UTF-8?q?feat(verify):=20v1.104=20=E2=80=94=20enforce=20?= =?UTF-8?q?the=208=20orphaned=20flight-critical=20control+estimator=20Kani?= =?UTF-8?q?=20proofs?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit A workspace scan found 36 of 142 Kani harnesses (25%) authored but absent from the kani.yml matrix — CI never ran them. Same orphaned-proof gap that left relay-rc unenforced ~40 releases and relay-mix-quad's MIX-P05..08 unenforced until v1.102. This closes the highest-safety subset: the 8 control + estimator proofs across 4 crates, all locally VERIFICATION SUCCESSFUL and now gated on every PR. relay-arm verify_arming_total / verify_arming_torque_gated relay-adrc verify_command_filter_saturation / verify_from_bandwidth_separation relay-geo verify_shield_contract relay-iekf verify_nis3_total / verify_spoof_monitor_no_false_alarm / verify_clamp_factor_bounded - kani.yml: add relay-arm/adrc/geo/iekf to the model-checking matrix (the roll-up "Kani gate" required check now covers them). - ci.yml: add the same 4 crates to the -D warnings clippy gate. This surfaced a latent collapsible_match in relay-arm's arming state machine (DISARMED arm) — refactored to a match guard; BOTH relay-arm Kani harnesses re-verified SUCCESSFUL, proving semantics preserved. - FV-RELAY-KANICI-002: rivet enforcement artifact (companion to KANICI-001), verifies ARM/ADRC/SHIELD/IEKF/SPOOF requirements. - Adopt the new rivet `release:` field (rivet 0.22.0 release-handling) on KANICI-002 (falcon-v1.104.0) and retroactively on FV-FALCON-FAULT-002 (falcon-v1.103.0). Hand-placed: `rivet modify --set-release` corrupts folded scalars (filed pulseengine/rivet#613). Remaining orphaned slice: 12 crates (~28 harnesses) flight-support + HAL drivers + infra — the next enforcement release. Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 1 + .github/workflows/kani.yml | 18 ++++- .../verification/FV-FALCON-FAULT-002.yaml | 1 + .../verification/FV-RELAY-KANICI-002.yaml | 76 +++++++++++++++++++ crates/relay-arm/plain/src/lib.rs | 8 +- 5 files changed, 97 insertions(+), 7 deletions(-) create mode 100644 artifacts/verification/FV-RELAY-KANICI-002.yaml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 6caf534..b63a031 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -64,6 +64,7 @@ jobs: cargo clippy -p relay-mavlink -p relay-ekf-stub -p falcon-hello \ -p falcon-param -p relay-fsm -p relay-preflight -p relay-calib \ -p falcon-core -p relay-mix-quad \ + -p relay-arm -p relay-adrc -p relay-geo -p relay-iekf \ --all-targets -- -D warnings test: diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 5224558..f7b6e8f 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -61,6 +61,20 @@ jobs: - relay-calib - relay-fsafe - relay-mix-quad + # Flight-critical control + estimator proofs. These harnesses were + # authored alongside the engines but never added to this matrix, so + # CI never ran them (the same orphaned-proof gap that bit relay-rc + # for ~40 releases and relay-mix-quad's MIX-P05..08). A workspace + # scan found 36/142 Kani harnesses unenforced across 16 crates; this + # closes the highest-value subset — the 8 control/estimator proofs: + # relay-arm verify_arming_total / verify_arming_torque_gated + # relay-adrc verify_command_filter_saturation / _from_bandwidth_separation + # relay-geo verify_shield_contract + # relay-iekf verify_nis3_total / _spoof_monitor_no_false_alarm / _clamp_factor_bounded + - relay-arm + - relay-adrc + - relay-geo + - relay-iekf steps: - uses: actions/checkout@v7 - name: Kani verify ${{ matrix.engine }} @@ -68,9 +82,9 @@ jobs: with: working-directory: crates/${{ matrix.engine }} - # Roll-up over the 21-engine matrix: ONE required context for branch + # Roll-up over the full engine matrix: ONE required context for branch # protection ("Kani gate"), so the formal-verification result gates merges - # without registering 21 separate required checks. + # without registering a separate required check per engine. kani-gate: name: Kani gate runs-on: [self-hosted, linux, x64, light] diff --git a/artifacts/verification/FV-FALCON-FAULT-002.yaml b/artifacts/verification/FV-FALCON-FAULT-002.yaml index b0f6d52..7a4644e 100644 --- a/artifacts/verification/FV-FALCON-FAULT-002.yaml +++ b/artifacts/verification/FV-FALCON-FAULT-002.yaml @@ -3,6 +3,7 @@ artifacts: type: sw-verification title: "Single-rotor-loss fault tolerance — Kani MIX-P08 + FDI contract + reduced-attitude + end-to-end composition (v0.26)" status: implemented + release: falcon-v1.103.0 description: > Three independently-verified components plus an end-to-end composition test: diff --git a/artifacts/verification/FV-RELAY-KANICI-002.yaml b/artifacts/verification/FV-RELAY-KANICI-002.yaml new file mode 100644 index 0000000..0d8160d --- /dev/null +++ b/artifacts/verification/FV-RELAY-KANICI-002.yaml @@ -0,0 +1,76 @@ +artifacts: + - id: FV-RELAY-KANICI-002 + type: sw-verification + title: "Flight-critical control + estimator Kani harnesses enforced in CI (orphaned-proof closure)" + status: implemented + release: falcon-v1.104.0 + description: > + Closes the highest-value subset of a systemic orphaned-proof gap. A + workspace scan found 36 of 142 Kani harnesses (25%) were authored but + never added to .github/workflows/kani.yml's matrix, so CI never ran + them — the same gap that left relay-rc unenforced for ~40 releases and + relay-mix-quad's MIX-P05..08 unenforced until v1.102. This artifact + enforces the 8 flight-critical control + estimator proofs (4 crates), + all of which VERIFY locally with 0 failures and now run on every PR: + + relay-arm (2) verify_arming_total — tick() is total: never + panics, output finite, + phase in range, for any + (tilt, arm_request) + verify_arming_torque_gated — torque_authority is true + ONLY in ARMED; the level + gate is the sole edge in + relay-adrc (2) verify_command_filter_saturation — the reference command + filter output stays within + the configured saturation + verify_from_bandwidth_separation — gains derived from a + bandwidth separation are + finite + ordered + relay-geo (1) verify_shield_contract — the geometric safety-shield + contract (reduced-attitude) + holds for any input + relay-iekf (3) verify_nis3_total — the 3-DOF NIS chi-square + gate is total under any + innovation (incl non-finite) + verify_spoof_monitor_no_false_alarm — no spoof alarm while + residuals stay within slack + verify_clamp_factor_bounded — the gain clamp factor is + bounded for any input + + ENFORCEMENT: the 4 crates were added to the kani.yml model-checking matrix + (the roll-up "Kani gate" required check now covers them) AND to the ci.yml + `-D warnings` clippy gate. Bringing relay-arm under the clippy gate + surfaced a latent collapsible_match in the arming state machine + (DISARMED arm); it was refactored to a match guard and BOTH relay-arm + Kani harnesses re-verified SUCCESSFUL, proving the refactor preserved + semantics. The other three crates were already clippy-clean. + + This is the orphaned-verified pattern closed at the highest-safety subset; + the remaining 12 orphaned crates (flight-support + HAL drivers + infra, + ~28 harnesses) are the next enforcement slice. Companion to + FV-RELAY-KANICI-001 (the cFS-engine Kani CI gate). + tags: [verification, relay, falcon, control, estimator, kani, ci] + fields: + method: model-checking + kani-properties: > + verify_arming_total, verify_arming_torque_gated, + verify_command_filter_saturation, verify_from_bandwidth_separation, + verify_shield_contract, verify_nis3_total, + verify_spoof_monitor_no_false_alarm, verify_clamp_factor_bounded + steps: + - run: "cargo kani -p relay-arm # Kani CI workflow (CBMC; heavy)" + - run: "cargo kani -p relay-adrc # Kani CI workflow" + - run: "cargo kani -p relay-geo # Kani CI workflow" + - run: "cargo kani -p relay-iekf # Kani CI workflow" + - run: cargo clippy -p relay-arm -p relay-adrc -p relay-geo -p relay-iekf --all-targets -- -D warnings + links: + - type: verifies + target: SWREQ-FALCON-ARM-P01 + - type: verifies + target: SWREQ-FALCON-ADRC-P05 + - type: verifies + target: SWREQ-FALCON-SHIELD-P01 + - type: verifies + target: SWREQ-FALCON-IEKF-P01 + - type: verifies + target: SWREQ-FALCON-SPOOF-P01 diff --git a/crates/relay-arm/plain/src/lib.rs b/crates/relay-arm/plain/src/lib.rs index c4b9625..8ec78b6 100644 --- a/crates/relay-arm/plain/src/lib.rs +++ b/crates/relay-arm/plain/src/lib.rs @@ -108,11 +108,9 @@ impl ArmingSequencer { /// SpinUp; ignored in later phases (the machine latches forward). pub fn tick(&mut self, tilt_rad: f32, arm_request: bool) -> ArmingOutput { match self.phase { - DISARMED => { - if arm_request { - self.phase = SPINUP; - self.tick_in_phase = 0; - } + DISARMED if arm_request => { + self.phase = SPINUP; + self.tick_in_phase = 0; } SPINUP => { self.tick_in_phase = self.tick_in_phase.saturating_add(1);