ci(kani,clippy): enforce the orphaned relay-mix-quad proofs (MIX-P05..08)

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

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

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

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