From 8684c17533fe630beaccecbc75131803cc138fb5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 22:08:27 +0200 Subject: [PATCH 1/2] =?UTF-8?q?fix(main):=20waive=20#973's=20selector=20gr?= =?UTF-8?q?owth=20=E2=80=94=20the=20subtraction=20gate=20caught=20its=20fi?= =?UTF-8?q?rst=20real=20event?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit main went red the moment #991 (the subtraction metric) and #992 (the #973 ARM miscompile fix) were both on it. Not a conflict: both were green on their own bases, #992 merged first and grew the selector, and #991's pins were measured against the pre-#992 file. The classic stale-base merge — except this time something noticed, which is the entire point of the lane. selector_lines_code 18,480 -> 18,582 ceiling, moved WRONG way selector_wildcard_arms_code 62 -> 63 ceiling, moved WRONG way selector_lines_total 29,616 -> 29,839 track selector_wildcard_arms_total 105 -> 106 track THE GROWTH IS CORRECT AND THE WAIVER SAYS SO. #973 was a real miscompile: an i64 compare needs a register PAIR, so `alloc_consecutive_pair` spilled the then-arm and `pop_operand` reloaded it into the register still holding the else-arm — both `it` arms then moved the same source and the then-value always won. The fix reserves the just-popped operand (`pop_operand_committed`), generalizing #677's discipline. This is a SOUNDNESS INVARIANT, not a lowering patch — there is no hand-written arm to delete against it, so "grew without deleting" is the right outcome and the waiver records why rather than the ceiling being quietly moved. Evidence carried in the reason: 264/360 -> 360/360 executed vs wasmtime on both ARM legs, 10/10 frozen anchors unchanged, and where bytes move they SHRINK (sel_i64_lt_s 68 B -> 64 B). The added `_ =>` is in the reservation helper's match over operand provenance, where the fallback is the CONSERVATIVE answer (reserve it) rather than a silent skip. Counted honestly rather than written to dodge the pin. Both ceilings RE-BANK at the new value, so the next unexplained growth still reds — a waiver is bound to a value, not an amnesty. claim_check 47/47. status.json regenerated. Refs #242, #973 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- artifacts/status.json | 8 ++++---- claims.yaml | 28 ++++++++++++++++++++++++---- 2 files changed, 28 insertions(+), 8 deletions(-) diff --git a/artifacts/status.json b/artifacts/status.json index 4a018c7e..d6365d7a 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -23,10 +23,10 @@ "sel_dsl_rule_qed": 50, "sel_dsl_rules": 50, "sel_rules_simplified_basis": 50, - "selector_lines_code": 18480, - "selector_lines_total": 29616, - "selector_wildcard_arms_code": 62, - "selector_wildcard_arms_total": 105, + "selector_lines_code": 18582, + "selector_lines_total": 29839, + "selector_wildcard_arms_code": 63, + "selector_wildcard_arms_total": 106, "version": "0.57.0", "verus_spec_fns": 8, "wasmcert_bridge_qed": 104 diff --git a/claims.yaml b/claims.yaml index 040a8df5..6d4675ce 100644 --- a/claims.yaml +++ b/claims.yaml @@ -804,8 +804,21 @@ claims: - kind: ratchet name: selector_lines_code direction: down - value: 18480 + value: 18582 baseline: 18480 + waivers: + - to: 18582 + reason: >- + #973 (PR #992) — the ARM `select`-on-i64-compare MISCOMPILE fix. `pop_operand` + reloaded a spilled operand into the register still holding the OTHER arm, so + both `it` arms moved the same source and the then-value always won. The fix + reserves the just-popped operand (`pop_operand_committed`), generalizing + #677's discipline. GROWTH IS THE CORRECT OUTCOME HERE: this is a soundness + invariant, not a lowering patch — there is no hand-written arm to delete + against it. Evidence: 264/360 -> 360/360 executed vs wasmtime on both ARM + legs, 10/10 frozen anchors unchanged, and where bytes move they SHRINK + (sel_i64_lt_s 68 B -> 64 B). The ceiling re-banks at the new value, so the + next unexplained growth still reds. # The whole-file figures the release plan and the sibling lanes quote. An # unpinned quoted number is the drift class this release is about — but # they are `track`, not `down`, and the distinction is deliberate. Both @@ -819,7 +832,7 @@ claims: - kind: ratchet name: selector_lines_total direction: track - value: 29616 + value: 29839 # RQ-58-WILDCARD's real denominator, and THE directed wildcard pin. 62 # absorbing arms are in the lowering code; the other 43 of the plan's 105 # are assertion helpers in the test module, where a `_ =>` is not a @@ -828,12 +841,19 @@ claims: - kind: ratchet name: selector_wildcard_arms_code direction: down - value: 62 + value: 63 baseline: 62 + waivers: + - to: 63 + reason: >- + #973 (PR #992) — same fix. The added `_ =>` is in the reservation helper's + match over operand provenance, where the fallback is the CONSERVATIVE answer + (reserve it) rather than a silent skip. Counted honestly rather than written + to dodge the pin. - kind: ratchet name: selector_wildcard_arms_total direction: track - value: 105 + value: 106 # The other half of the same trade: the verified path must GROW as the # hand-written one shrinks. Pinned as a FLOOR so a rule can never be quietly From 70e8d63ce67525153f6701a6cbdf72fd16200bf6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Tue, 18 Aug 2026 22:33:31 +0200 Subject: [PATCH 2/2] fix(ci): restore the MC/DC rustc pin that #984 silently defeated MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit #978 pinned the MC/DC job to `dtolnay/rust-toolchain@1.96.1` for a stated reason: its floors (decisions / conditions / proved / dead) are derived from that exact compiler on the CI host, and the pin exists so a Rust release cannot red the gate with no code change. #984 bumped it to @1.100.0 — as if it were a routine action-version update. FOR THIS ACTION THE REF IS THE COMPILER. So a bot bump that reads like "dependabot: bump action from X to Y" silently changes which rustc the MC/DC surface is built with, and every subsequent run measures a DIFFERENT compiler against 1.96.1-derived floors. The pin was defeated by the one update shape nobody inspects. It is already biting: PR #994 (this branch, before this commit) failed exactly one check — MC/DC — for no reason other than being based on a main that now installs 1.100.0. Two changes: * .github/workflows/ci.yml — restored @1.96.1, with the reason inline at the pin so the next reader does not have to reconstruct it from two issues. * .github/dependabot.yml — `ignore: dtolnay/rust-toolchain` for the github-actions ecosystem. Bumping it is a deliberate act that must RE-MEASURE the floors, which is not a bot's job. This is the same class as the 0.x-minor rule (#849/#965): an update whose CATEGORY is wrong, so the automation's category-based judgement is wrong too. There the fix was "hold 0.x-minor because minor IS major for 0.x"; here it is "this action's ref is not an action version at all". claim_check 47/47. Refs #242, #912, #978 Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .github/dependabot.yml | 11 +++++++++++ .github/workflows/ci.yml | 9 ++++++++- 2 files changed, 19 insertions(+), 1 deletion(-) diff --git a/.github/dependabot.yml b/.github/dependabot.yml index db10aca5..ec5f9ac1 100644 --- a/.github/dependabot.yml +++ b/.github/dependabot.yml @@ -6,6 +6,17 @@ updates: interval: weekly labels: - dependencies + ignore: + # dtolnay/rust-toolchain is NOT an ordinary action pin — for this action + # THE REF IS THE COMPILER VERSION. #978 pinned the MC/DC job to @1.96.1 + # precisely so a Rust release could not red that gate with no code + # change; its floors (decisions/conditions/proved/dead) are derived from + # that exact compiler on the CI host. #984 bumped it to @1.100.0 as if it + # were a routine action version, which silently defeated the pin and + # would have measured a different compiler against 1.96.1 floors. + # Bumping it is a deliberate act that must RE-MEASURE the floors, so it + # does not belong to a bot. + - dependency-name: dtolnay/rust-toolchain - package-ecosystem: cargo directory: / schedule: diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index b7fcf5c3..69c8ed43 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -3705,7 +3705,14 @@ jobs: # sensitive to how `std` inlines. `@stable` is a moving target and a Rust # release could red this gate with no code change. Bumping this version is # allowed — it obliges a RE-MEASURE of the floors, not a lowering. - - uses: dtolnay/rust-toolchain@1.100.0 + # PINNED, and dependabot must NOT bump this (see .github/dependabot.yml). + # For this action the REF IS THE COMPILER VERSION, so a routine-looking + # "action bump" silently changes what rustc the MC/DC surface is built + # with. #978 pinned 1.96.1 precisely so a Rust release cannot red this + # gate with no code change; #984 bumped it to 1.100.0 as if it were an + # action version, which would have measured a different compiler against + # 1.96.1-derived floors. Restored. + - uses: dtolnay/rust-toolchain@1.96.1 with: targets: wasm32-wasip1 - name: Cache Cargo dependencies