v1.104 — enforce the 8 orphaned flight-critical control+estimator Kani proofs

.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:

.github/workflows/kani.yml

@@ -61,16 +61,30 @@ 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 }}
         uses: model-checking/kani-github-action@v1
         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]

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:

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

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);