From e77ad780b6473383e2dc176aa959bf3288c72d12 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Thu, 17 Sep 2026 19:00:44 +0200 Subject: [PATCH] fix(kani): make the MIX-P06 mixer proof compositional so it stops stalling the Kani gate (#429) verify_mix_priority_bound stalled 13 of 42 CI executions of the relay-mix-quad leg (31%) since 2026-09-15, three times on main on 2026-09-17, always in the CaDiCaL solve of the same 801 030-clause instance that solves in 13 s locally. scale_to_fit now carries a Kani contract (finite arguments -> finite scale in [0, 1]), proven for all finite inputs by verify_scale_to_fit_contract. verify_mix_priority_bound uses stub_verified: the precondition is asserted at both call sites and only the proven postcondition is assumed, so the MIX-P06 bound is proven for every scale in [0, 1]. The instance drops to 407 696 clauses. Mutations checked before committing: dropping the mixer's final clamp, dropping scale_to_fit's final guard, and dropping sanitise on the roll/pitch delta each make the matching harness FAIL. The two unstable Kani features this needs are enabled for this crate only, in its Cargo.toml; Kani stays pinned at 0.67.0. SWREQ-RELAY-MIXPROOF-P01 / FV-RELAY-MIXPROOF-001 (v1.140, implemented). Refs #429 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG --- artifacts/swreq/SWREQ-RELAY-CIFLOW-P01.yaml | 5 +- artifacts/swreq/SWREQ-RELAY-MIXPROOF-P01.yaml | 51 ++++++++++++++ .../verification/FV-RELAY-MIXPROOF-001.yaml | 66 +++++++++++++++++++ crates/relay-mix-quad/Cargo.toml | 8 +++ crates/relay-mix-quad/plain/src/lib.rs | 37 +++++++++++ docs/RELEASE-PLAN.md | 6 +- 6 files changed, 170 insertions(+), 3 deletions(-) create mode 100644 artifacts/swreq/SWREQ-RELAY-MIXPROOF-P01.yaml create mode 100644 artifacts/verification/FV-RELAY-MIXPROOF-001.yaml diff --git a/artifacts/swreq/SWREQ-RELAY-CIFLOW-P01.yaml b/artifacts/swreq/SWREQ-RELAY-CIFLOW-P01.yaml index 1ac1afcc..24b09c93 100644 --- a/artifacts/swreq/SWREQ-RELAY-CIFLOW-P01.yaml +++ b/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. diff --git a/artifacts/swreq/SWREQ-RELAY-MIXPROOF-P01.yaml b/artifacts/swreq/SWREQ-RELAY-MIXPROOF-P01.yaml new file mode 100644 index 00000000..2c97c3b7 --- /dev/null +++ b/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 diff --git a/artifacts/verification/FV-RELAY-MIXPROOF-001.yaml b/artifacts/verification/FV-RELAY-MIXPROOF-001.yaml new file mode 100644 index 00000000..495c1217 --- /dev/null +++ b/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 diff --git a/crates/relay-mix-quad/Cargo.toml b/crates/relay-mix-quad/Cargo.toml index b8097a8a..62105647 100644 --- a/crates/relay-mix-quad/Cargo.toml +++ b/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 diff --git a/crates/relay-mix-quad/plain/src/lib.rs b/crates/relay-mix-quad/plain/src/lib.rs index d3a67d01..31dab2de 100644 --- a/crates/relay-mix-quad/plain/src/lib.rs +++ b/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); diff --git a/docs/RELEASE-PLAN.md b/docs/RELEASE-PLAN.md index 5209a838..5893e257 100644 --- a/docs/RELEASE-PLAN.md +++ b/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*