fix(kani): make the MIX-P06 mixer proof compositional so it stops stalling the Kani gate (#429) - #451
Merged
Merged
Conversation
…lling 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 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG
avrabe
enabled auto-merge (squash)
September 17, 2026 17:01
✅ Rivet verification gate — falcon1/1 passed
Source of truth: |
avrabe
added a commit
that referenced
this pull request
Sep 17, 2026
…thout stalling — promote MIXPROOF-P01 (#429) (#453) Baseline before the change: 13 stalls in 42 executions of Kani (relay-mix-quad) (31%). After it: 11 consecutive executions with no stall — 10 re-runs of #451's Kani run 35250155750 plus the push run on main bd74cfe — across seven runners, four of which had held a stall of this harness. Slowest 7m04s against the 60-minute cap. Under the old rate, 11 clean runs in a row has probability 0.69^11 = 1.6%. Code-free promotion (the two-commit rule): SWREQ-RELAY-MIXPROOF-P01 and FV-RELAY-MIXPROOF-001 implemented -> verified, with every job id, runner and duration recorded. Not claimed: that no Kani harness can stall again. Kani (relay-param) was cancelled at 52 min on main bd74cfe, its log no longer retrievable; that belongs to CIFLOW-P01 (v1.142). Refs #429 Claude-Session: https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG Co-authored-by: Claude Opus 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Verify-Filter: (= id "FV-RELAY-MIXPROOF-001")
Refs #429. SWREQ-RELAY-MIXPROOF-P01, v1.140, pulled forward from CIFLOW-P01 by maintainer decision on 2026-09-17.
What was wrong (measured)
Kani (relay-mix-quad)jobs from 2026-09-15 to 2026-09-17 that reached model checking: 29 passed in 3–4 min, 13 stalled (43–126 min, or cancelled at #432's 60-min cap), so 31%. Every stall log read so far sits inverify_mix_priority_bound. That is the five in #429, plus main's own runs on 916fbca, 3ba320d and a8f6cf7 today, which turned the Kani gate on main red three times.The stalled instance is the same size in CI and locally (186 629 variables, 801 030 clauses). The first solve finishes in about 5 s; the second never returns. On a developer machine the whole harness takes 13 s. The proof is not wrong. It is one large SAT instance with a heavy tail.
The change
scale_to_fit(the mixer's float divisions): for finite arguments it returns a finite scale in[0, 1].verify_scale_to_fit_contractproves it for all finite inputs, including Kani's NaN checks on the divisions.verify_mix_priority_boundusesstub_verified(scale_to_fit). Kani asserts the precondition at both call sites and assumes only the proven postcondition. The motor bound is proven for every scale in[0, 1], a superset of whatscale_to_fitreturns, so the MIX-P06 claim does not change. Instance size: 407 696 clauses (was 801 030).function-contracts,stubbing) are enabled incrates/relay-mix-quad/Cargo.tomlonly. There are no workflow changes, and Kani stays pinned at 0.67.0.Evidence (local, Kani 0.67.0)
cargo kanion the crate, with no command-line flags: 7/7 harnesses SUCCESSFUL.verify_mix_priority_bound: 7.7–8.4 s over 3 runs.verify_scale_to_fit_contract: about 4 s.clamp_floor→ three motor-bound assertions fail.scale_to_fit's final guard → postcondition fails.sanitiseon the roll/pitch delta → precondition fails at the call site, so it is enforced, not assumed.cargo test -p relay-mix-quad: 26 passed. Clippy is clean, andrivet validatepasses.Not claimed yet
That the CI stall is gone. It never reproduced locally, so only CI runs can show it.
FV-RELAY-MIXPROOF-001staysimplementeduntil 10 consecutiveKani (relay-mix-quad)executions on CI finish without a stall. At the old 31% rate, 10 clean runs in a row would happen by chance about 2.4% of the time. The runs will be re-run on this PR and recorded by run id in the code-free promotion PR.🤖 Generated with Claude Code
https://claude.ai/code/session_01HvusAXYbHLyv3uTzfBcMbG