From 3ac383e2525a7106ed8633618b6f0113e124f2fc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Sat, 27 Jun 2026 06:37:12 +0200 Subject: [PATCH] ci(kani,clippy): enforce the orphaned relay-mix-quad proofs (MIX-P05..08) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Caught while scoping motor-failure reallocation: relay-mix-quad has six Kani harnesses (MIX-P05..P08 — the X-mixer bound, saturation-direction, thrust-floor, and the MIX-P08 single-rotor-out allocator that pins the failed rotor to 0 and keeps healthy rotors in [floor,1]) but the crate was NOT in the dedicated Kani matrix. MIX-P08 ran only via FV-FALCON-FAULT-002's verification step; the rest ran nowhere in CI. Same orphaned-proof pattern closed this session for relay-param / relay-fsm / relay-preflight / relay-calib / relay-fsafe. Add relay-mix-quad to .github/workflows/kani.yml + the -D warnings clippy gate (3 test-fn #[allow(clippy::needless_range_loop)] where the index is used in the failure message — the verified mixer logic is untouched). All six harnesses verify 6/6; 23 tests; clippy clean. FV-FALCON-FAULT-002 notes the enforcement. (Note: the rotor-loss FEATURE is already implemented + verified — RotorFaultDetector + mix_rotor_out + moment_reduced + the end-to-end SITL chain test all pass. This is the gate-enforcement gap, not new feature code.) Co-Authored-By: Claude Opus 4.8 --- .github/workflows/ci.yml | 2 +- .github/workflows/kani.yml | 1 + artifacts/verification/FV-FALCON-FAULT-002.yaml | 7 +++++++ crates/relay-mix-quad/plain/src/lib.rs | 3 +++ 4 files changed, 12 insertions(+), 1 deletion(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 629a1f5..6caf534 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -63,7 +63,7 @@ jobs: run: | 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 falcon-core -p relay-mix-quad \ --all-targets -- -D warnings test: diff --git a/.github/workflows/kani.yml b/.github/workflows/kani.yml index 48ae1cf..5224558 100644 --- a/.github/workflows/kani.yml +++ b/.github/workflows/kani.yml @@ -60,6 +60,7 @@ jobs: - relay-preflight - relay-calib - relay-fsafe + - relay-mix-quad steps: - uses: actions/checkout@v7 - name: Kani verify ${{ matrix.engine }} diff --git a/artifacts/verification/FV-FALCON-FAULT-002.yaml b/artifacts/verification/FV-FALCON-FAULT-002.yaml index 9416df1..d216aba 100644 --- a/artifacts/verification/FV-FALCON-FAULT-002.yaml +++ b/artifacts/verification/FV-FALCON-FAULT-002.yaml @@ -31,6 +31,13 @@ artifacts: reduced-attitude + MIX-P08, MIX-P08 holds every step, and the body does not tumble (peak tilt <80°) and settles upright (final <29°). + + v1.102 ENFORCEMENT: relay-mix-quad was added to the Kani CI + matrix (.github/workflows/kani.yml) + the -D warnings clippy + gate. Its six harnesses (MIX-P05..P08, incl the MIX-P08 + rotor-out allocator above) ran only via this artifact's step + before; now the dedicated Kani gate runs all six on every PR + (belt-and-suspenders), closing the orphaned-proof gap. tags: [verification, falcon, fault-tolerance, rotor-loss, kani, v0.26] fields: method: formal-verification diff --git a/crates/relay-mix-quad/plain/src/lib.rs b/crates/relay-mix-quad/plain/src/lib.rs index f3895ce..e80266d 100644 --- a/crates/relay-mix-quad/plain/src/lib.rs +++ b/crates/relay-mix-quad/plain/src/lib.rs @@ -991,6 +991,7 @@ mod tests { /// from_geometry(quad-X angles) reproduces the hand-tuned MIXER_X matrix. #[test] + #[allow(clippy::needless_range_loop)] // index used in failure messages fn mixern_from_geometry_reproduces_quad_matrix() { let g = MixerN::from_geometry(&[ (deg(45.0), false), // front-right CW @@ -1013,6 +1014,7 @@ mod tests { /// Hexa-X: at zero torque every one of the 6 rotors carries the same /// (collective) command — rotational symmetry of a balanced airframe. #[test] + #[allow(clippy::needless_range_loop)] // index used in failure messages fn mixern_hexa_zero_torque_is_uniform() { let h = MixerN::hexa_x(); assert_eq!(h.n(), 6); @@ -1028,6 +1030,7 @@ mod tests { /// Hexa-X resolves a pure yaw command using its 6 rotors (CW vs CCW /// split), staying in [0,1]. #[test] + #[allow(clippy::needless_range_loop)] // index used in failure messages fn mixern_hexa_yaw_uses_spin_split() { let h = MixerN::hexa_x(); let out = h.mix([0.0, 0.0, 0.15], 0.5);