fix(main): waive #973's selector growth — the subtraction gate caught its first real event

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

.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

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

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