fix(kani): make the MIX-P06 mixer proof compositional so it stops stalling the Kani gate (#429)

artifacts/swreq/SWREQ-RELAY-CIFLOW-P01.yaml

@@ -20,8 +20,9 @@ artifacts:
         #429 — follow-up: every recorded Kani (relay-mix-quad) hang is one
                harness, verify_mix_priority_bound, stalling in CBMC's second
                propositional reduction (minisat stalls it locally past 300 s).
-               The 60-min cap makes the stall visible; the harness still
-               needs to be made robust.
+               The 60-min cap makes the stall visible. Making the harness
+               robust moved to SWREQ-RELAY-MIXPROOF-P01 (v1.140) by
+               maintainer decision on 2026-09-17.
         #436 — the fleet monitor's */15 schedule actually ran every 2.4–5.5 h,
                so unattended detection latency is hours.
 

artifacts/swreq/SWREQ-RELAY-MIXPROOF-P01.yaml

@@ -0,0 +1,51 @@
+artifacts:
+  - id: SWREQ-RELAY-MIXPROOF-P01
+    type: sw-req
+    title: "MIXPROOF-P01 — the MIX-P06 priority-mix bound proof shall not depend on a solver's heavy tail"
+    status: implemented
+    release: falcon-v1.140.0
+    description: >
+      The Kani proof that the priority-desaturation mixer keeps every motor
+      finite and in `[floor, 1]` for any input (MIX-P06,
+      `verify_mix_priority_bound`) shall reach its verdict in bounded time on
+      the CI fleet. A required gate that passes or stalls depending on the run
+      is not a verdict.
+
+      WHY IT EXISTS (#429). Measured over every `Kani (relay-mix-quad)` job
+      that reached model checking from 2026-09-15 to 2026-09-17: 29 passed in
+      3–4 min and 13 stalled (43–126 min, or cancelled at the 60-min cap from
+      #432). That is 31%. Every stall whose log was read (the five in #429 and
+      the three on main on 2026-09-17: 916fbca, 3ba320d, a8f6cf7) sits in
+      `verify_mix_priority_bound`, in the CaDiCaL solve after the first
+      propositional reduction. The same instance (186 629 variables, 801 030
+      clauses, identical in CI and locally) solves in 13 s on a developer
+      machine. The proof is not wrong: it is one large instance with a heavy
+      tail, and it turned main's Kani gate red three times in one day.
+
+      THE CHANGE. The harness is compositional. `scale_to_fit`, which holds
+      the mixer's float divisions, carries a Kani contract: for finite
+      arguments it returns a finite scale in `[0, 1]`.
+      `verify_scale_to_fit_contract` proves that contract for all finite
+      inputs, including Kani's NaN checks on its divisions.
+      `verify_mix_priority_bound` uses `stub_verified(scale_to_fit)`: Kani
+      asserts the precondition at both call sites and assumes only the proven
+      postcondition. The motor bound is thereby proven for every scale in
+      `[0, 1]`, a superset of what `scale_to_fit` returns, so the MIX-P06 claim
+      is unchanged. The instance drops to 407 696 clauses.
+
+      THE COST, stated. The two Kani features this needs (`function-contracts`,
+      `stubbing`) are unstable. They are enabled only for this crate, in
+      `crates/relay-mix-quad/Cargo.toml`. Kani is pinned at 0.67.0 in
+      kani.yml, so they cannot change under the gate without a deliberate
+      bump. Maintainer decision, 2026-09-17: take this in v1.140 rather than
+      wait for CIFLOW-P01 (v1.142).
+
+      FALSIFICATION: wrong if a `Kani (relay-mix-quad)` job on CI, after this
+      merges, stalls with `verify_mix_priority_bound` or
+      `verify_scale_to_fit_contract` as the harness in progress; or if either
+      harness still passes after the mixer or `scale_to_fit` is mutated to
+      break its bound.
+    tags: [requirement, relay, ci, kani, mixer, v1.140]
+    links:
+      - type: derives-from
+        target: SYSREQ-FALCON-010

artifacts/verification/FV-RELAY-MIXPROOF-001.yaml

@@ -0,0 +1,66 @@
+artifacts:
+  - id: FV-RELAY-MIXPROOF-001
+    type: sw-verification
+    title: "MIXPROOF-P01 — the compositional MIX-P06 proof passes, can fail, and halves the instance (v1.140)"
+    status: implemented
+    release: falcon-v1.140.0
+    description: >
+      Verifies SWREQ-RELAY-MIXPROOF-P01 on three counts: the proof still
+      proves the bound, each part of it can fail, and the instance that
+      stalled is smaller.
+
+      IT PROVES THE SAME BOUND. `cargo kani` on relay-mix-quad (Kani 0.67.0,
+      the kani.yml pin, features enabled from the crate's Cargo.toml with no
+      command-line flags): 7 of 7 harnesses SUCCESSFUL, locally, 2026-09-17.
+      Comparing the check lists of the monolithic and compositional
+      `verify_mix_priority_bound`: both keep the three motor-bound assertions
+      and the mixer's 9 multiplication and 11 addition NaN checks. The
+      monolithic one also checked `scale_to_fit`'s division and subtraction
+      NaN checks through its inlined calls. In the compositional one those
+      calls go to the contract. The body's checks are still listed, but the
+      body is no longer called or encoded; they are discharged in
+      `verify_scale_to_fit_contract`. The contract's precondition is a checked
+      assertion (SUCCESS) at the call sites, not an assumption (M3 below).
+
+      EACH PART CAN FAIL, checked before this artifact was written, one
+      mutation at a time:
+        M1. The mixer without its final `clamp_floor` makes
+            `verify_mix_priority_bound` FAIL on all three motor-bound
+            assertions.
+        M2. `scale_to_fit` without its final guard (returning `s` unchecked)
+            makes `verify_scale_to_fit_contract` FAIL on the postcondition.
+        M3. The mixer without `sanitise` on the roll/pitch delta makes
+            `verify_mix_priority_bound` FAIL on the precondition, which shows
+            the precondition is enforced at the call site, not assumed.
+
+      THE INSTANCE IS SMALLER. `verify_mix_priority_bound` went from 186 629
+      variables / 801 030 clauses (the size logged by every stalled CI run)
+      to 133 772 / 407 696, with 7.7–8.4 s wall time over three local runs.
+      The contract proof is 4.5 M clauses but solves in about 1.3 s: four
+      divisions over free finite inputs, with no mixer arithmetic in front of
+      them.
+
+      NOT CLAIMED YET: that the CI stall is gone. The stall never reproduced
+      on a developer machine, so local timing cannot show it. The baseline is
+      13 stalls in 42 CI executions (31%). Promotion to `verified` needs at
+      least 10 consecutive `Kani (relay-mix-quad)` executions on CI of this
+      tree or later with no stall; under the old 31% rate, 10 clean runs in a
+      row has a probability of about 2.4%. Each execution is to be recorded by
+      run id.
+    tags: [verification, relay, ci, kani, mixer, v1.140]
+    fields:
+      method: formal-verification
+      steps:
+        # The contract, for all finite inputs (CI: Kani gate, relay-mix-quad leg).
+        - run: "cargo kani -p relay-mix-quad --harness verify_scale_to_fit_contract"
+        # The MIX-P06 bound, using the proven contract.
+        - run: "cargo kani -p relay-mix-quad --harness verify_mix_priority_bound"
+        # The harness really is compositional, and the features are crate-local.
+        - run: "grep -q 'kani::stub_verified(super::scale_to_fit)' crates/relay-mix-quad/plain/src/lib.rs"
+        - run: "grep -q 'kani::proof_for_contract(super::scale_to_fit)' crates/relay-mix-quad/plain/src/lib.rs"
+        - run: "grep -q '^\\[package.metadata.kani.unstable\\]$' crates/relay-mix-quad/Cargo.toml"
+        # Kani stays pinned, so the unstable features cannot move under the gate.
+        - run: "grep -q \"kani-version: '0.67.0'\" .github/workflows/kani.yml"
+    links:
+      - type: verifies
+        target: SWREQ-RELAY-MIXPROOF-P01

crates/relay-mix-quad/Cargo.toml

@@ -20,3 +20,11 @@ proptest.workspace = true
 
 [lints]
 workspace = true
+
+# verify_mix_priority_bound is compositional: it uses scale_to_fit's proven
+# contract instead of re-solving its body (#429). That needs these two
+# unstable Kani features; Kani is pinned (kani.yml, 0.67.0), so they cannot
+# change under the required gate without a deliberate bump.
+[package.metadata.kani.unstable]
+function-contracts = true
+stubbing = true

crates/relay-mix-quad/plain/src/lib.rs

@@ -520,6 +520,20 @@ fn sanitise(x: f32) -> f32 {
 /// Largest scale `s ∈ [0,1]` keeping `base[i] + s·delta[i] ∈ [floor,1]`
 /// for every motor (the per-group desaturation step). Returns 0 if a
 /// constraint is already violated at s=0 or the result is non-finite.
+///
+/// The Kani contract below is proven for ALL finite inputs by
+/// `verify_scale_to_fit_contract`, and `verify_mix_priority_bound` uses
+/// the proven contract in place of this body (#429): the precondition is
+/// checked at each call site, the postcondition is what the caller gets.
+#[cfg_attr(
+    kani,
+    kani::requires(
+        base.iter().all(|b| b.is_finite())
+            && delta.iter().all(|d| d.is_finite())
+            && floor.is_finite()
+    )
+)]
+#[cfg_attr(kani, kani::ensures(|s: &f32| s.is_finite() && *s >= 0.0 && *s <= 1.0))]
 fn scale_to_fit(base: &[f32; 4], delta: &[f32; 4], floor: f32) -> f32 {
     const EPS: f32 = 1.0e-6;
     let mut s = 1.0_f32;
@@ -764,9 +778,32 @@ mod kani_proofs {
         }
     }
 
+    /// `scale_to_fit`'s contract, for ALL finite `base`, `delta`, `floor`:
+    /// the scale is finite and in `[0, 1]`, and no operation in the body
+    /// produces NaN. Kani's float checks on the four divisions live here.
+    #[kani::proof_for_contract(super::scale_to_fit)]
+    fn verify_scale_to_fit_contract() {
+        let base: [f32; 4] = kani::any();
+        let delta: [f32; 4] = kani::any();
+        let floor: f32 = kani::any();
+        let _ = super::scale_to_fit(&base, &delta, floor);
+    }
+
     /// MIX-P06: the priority-desaturation mix holds the SAME bound — every
     /// motor ∈ [floor,1] and finite for ANY (incl. non-finite) input.
+    ///
+    /// Compositional (#429). Monolithic, this harness was one ~800k-clause
+    /// instance whose second solve stalled for 43–126 min on CI runners
+    /// while passing in seconds elsewhere — a solver heavy tail, seven times
+    /// in about 31 hours. `stub_verified` replaces both `scale_to_fit` calls
+    /// with its contract proven in `verify_scale_to_fit_contract`: Kani
+    /// ASSERTS the precondition (finite arguments) at each call site and
+    /// assumes only the proven postcondition. The bound is therefore shown
+    /// for every scale in `[0, 1]`, a superset of what `scale_to_fit` returns,
+    /// in about half the clauses. Needs Kani's unstable `function-contracts`
+    /// and `stubbing` features, enabled for this crate in its Cargo.toml.
     #[kani::proof]
+    #[kani::stub_verified(super::scale_to_fit)]
     fn verify_mix_priority_bound() {
         let floor: f32 = kani::any();
         kani::assume(floor.is_finite() && floor >= 0.0 && floor <= 1.0);

docs/RELEASE-PLAN.md

@@ -22,7 +22,7 @@ Cuttable in days. Mostly promotion PRs for fixes already merged.
 **Merged, awaiting promotion / tag**
 
 - #413 — FAIL-UNSAFE: read_battery_v defaults to 16.0 V — a healthy pack — and nothing in the flight path overrides it — *FV-FALCON-BATT-003 — fix merged in #430; this issue closes WITH the tag*
-- #429 — CI jobs wedge in_progress for 30x their normal duration, and the fleet monitor cannot see it (watches queued, not stuck) — *SWREQ-RELAY-FLEET-P01 — wedge alarm + Kani cap merged (#432); harness robustness continues under CIFLOW-P01*
+- #429 — CI jobs wedge in_progress for 30x their normal duration, and the fleet monitor cannot see it (watches queued, not stuck) — *SWREQ-RELAY-FLEET-P01 — wedge alarm + Kani cap merged (#432); the stalling harness itself moved to SWREQ-RELAY-MIXPROOF-P01 in v1.140*
 - #436 — The fleet monitor has never measured starvation: gh isn't installed on the light runners, and every green run since 2026-08-07 was an empty result — *SWREQ-RELAY-FLEET-P01 — gh installed on light (#437, in flight); cron cadence continues under CIFLOW-P01*
 - #153 — Self-hosted runners lack `gh` (+ Node 20 deprecation): verification-gate PR comment can't post on smithy — *SWREQ-RELAY-FLEET-P01 — verification-gate PR comment gets gh (#437, in flight)*
 
@@ -55,6 +55,10 @@ HOLD-P01 first: an hours-long hold is meaningless while a 60 s hold diverges.
 
 - #398 — Rotor-out recovery does not hold on the gz plant — vehicle descends with OR without ESC telemetry
 
+**SWREQ-RELAY-MIXPROOF-P01 — the MIX-P06 proof stops stalling the Kani gate** (pulled forward from CIFLOW-P01 by maintainer decision, 2026-09-17)
+
+- #429 — `verify_mix_priority_bound` stalled 13 of 42 CI executions (31%), three times on main on 2026-09-17 — *compositional proof: `scale_to_fit` contract + `stub_verified`; verified after 10 consecutive CI executions without a stall*
+
 **Candidates — scoped at the start of v1.140 if HOLD work touches them**
 
 - #270 — gz plant hovers with an attitude limit-cycle (~1 rad/s roll/pitch, motor thrash 0.1↔1.0) — *gz attitude limit-cycle*