RQ-58-RETIRE (#242): delete the hand-written arms the 50 Rocq-proved DSL rules replaced (-1,312 lines, byte-identical)

CLAUDE.md

@@ -187,9 +187,11 @@ frozen and oracle-gated every step:
 - **Track A (core):** `VCR-RA-001` allocator with Belady spilling — **verified,
   default-on since v0.24.0** (`SYNTH_SPILL_REALLOC`; `SYNTH_SPILL_ON_EXHAUST`
   built flag-off, silicon-gated #580). Next: `VCR-SEL-001` Rocq-discharged
-  verified selector DSL (increments 1–4 shipped **default-on**, 50 rules / 50 Qed,
-  `SYNTH_SEL_DSL`; the Rocq-proved rules are the SHIPPED lowering path for their
-  50 covered ops, opt-out `SYNTH_NO_SEL_DSL=1`, byte-invisible flip) and
+  verified selector DSL (increments 1–4 shipped **default-on**, 50 rules / 50 Qed;
+  the Rocq-proved rules are the ONLY lowering path for their 50 covered ops —
+  RQ-58-RETIRE (v0.58) deleted the superseded hand-written arms byte-identically,
+  and with them the `SYNTH_SEL_DSL`/`SYNTH_NO_SEL_DSL` lever and the mirror-pin
+  gates, both vacuous once the second implementation was gone) and
   `VCR-PERF-002` proof-carrying specialization (#494,
   0.45× floor; phase 1 facts ingestion landed, PR #624).
 - **Track B (semantics):** `VCR-ISA-001` Sail-generated Rocq ISA model —

artifacts/release-v0.58.yaml

@@ -146,7 +146,26 @@ artifacts:
       `select_with_stack`). An arm that is dead on one path and live on the
       other is NOT deletable yet; say which those are rather than deleting them
       and discovering it downstream. That set is the input to RQ-58-SPLIT.
-    status: proposed
+      LANDED (v0.58): all 36 flag-guarded sites deleted (21 select_default +
+      15 select_with_stack; one op/group per commit), each commit gated on a
+      688-row corpus byte-identity manifest (156 scripts/repro fixtures x 4
+      configs — m4f/m4 relocatable, m4f self-contained, r5 relocatable —
+      declines pinned too) against the pre-deletion origin/main baseline plus
+      the 10 frozen anchors. BYTE-IDENTICAL THROUGHOUT — no finding of the
+      "flip does not cover what it claims" class surfaced. The SYNTH_SEL_DSL
+      lever and the four mirror-pin tests retired as vacuous in the final
+      functional commit; the #258 imm-fold holdout re-pinned as
+      cmp_imm_fold_residual_path_stays_handwritten_258. Selector code region
+      18,582 -> 17,897 (-685), absorbing wildcards 63 -> 56 (-7), whole file
+      29,839 -> 28,495; ratchet re-banked. RESIDUAL (the RQ-58-SPLIT input,
+      measured not guessed): select_with_stack's i32 add/sub/mul/and/or/xor
+      arms (hand-written imm-fold shapes, never DSL-wired), its i32.rotl arm,
+      and its i32-comparison imm-fold (#258 cmp/cmn) fallback emission;
+      select_default's blind-Cmp i32 comparison + i32.eqz arms and its
+      fixed-pair i64 mul/shl/shr_u/shr_s/rotl/rotr/clz/ctz/popcnt arms
+      (production-unreachable via compile paths — select_with_stack matches
+      those ops before its fallthrough — but live via the pub select() API).
+    status: implemented
     release: v0.58
     tags: [north-star, subtraction, vcr-sel-001, byte-identical]
     links:

artifacts/status.json

@@ -28,10 +28,10 @@
   "sel_dsl_rule_qed": 50,
   "sel_dsl_rules": 50,
   "sel_rules_simplified_basis": 50,
-  "selector_lines_code": 18582,
-  "selector_lines_total": 29839,
-  "selector_wildcard_arms_code": 63,
-  "selector_wildcard_arms_total": 106,
+  "selector_lines_code": 17897,
+  "selector_lines_total": 28495,
+  "selector_wildcard_arms_code": 56,
+  "selector_wildcard_arms_total": 91,
   "version": "0.57.0",
   "verus_spec_fns": 8,
   "wasmcert_bridge_qed": 104

artifacts/verified-codegen-roadmap.yaml

@@ -474,6 +474,22 @@ artifacts:
       verified) — i64 mul/div/shifts/rotates/comparisons (I64SetCond) +
       optimizer_bridge + the remaining select_with_stack families; div/rem
       (VCR-ISA-001-gated).
+      RQ-58-RETIRE LANDED (v0.58): the hand-written arms the 50 rules had
+      superseded are DELETED — 36 flag-guarded sites across both selectors
+      (21 select_default + 15 select_with_stack), one op/group per commit,
+      each gated on a 688-row corpus byte-identity manifest (156 fixtures x
+      4 configs vs the pre-deletion baseline) + the 10 frozen anchors. The
+      SYNTH_SEL_DSL/SYNTH_NO_SEL_DSL lever and the four mirror-pin tests
+      went with them (vacuous once the second implementation was gone — the
+      VcrSelRulesGenCheck precedent); the #258 cmp/cmn imm-fold holdout is
+      re-pinned as cmp_imm_fold_residual_path_stays_handwritten_258.
+      Selector non-test code 18,582 -> 17,897 lines, absorbing wildcards
+      63 -> 56 (ratchet re-banked in claims.yaml). Residual (RQ-58-SPLIT
+      input): select_with_stack's i32 add/sub/mul/and/or/xor (imm-fold
+      shapes) + i32.rotl arms; select_default's blind-Cmp i32 comparison
+      + i32.eqz arms and its fixed-pair i64 mul/shift/rotate/bit-count
+      arms — covered ops whose per-path arms were never DSL-wired, so
+      nothing there was superseded or deletable.
     status: implemented
     tags: [codegen, selector, isle, verified-dsl, rocq, track-a, novel, release-v0.12.1]
     links:

claims.yaml

@@ -1226,22 +1226,18 @@ claims:
       # THE LOAD-BEARING PIN: hand-written lowering code, test module excluded.
       # RQ-58-RETIRE (delete the arms the 50 DSL rules replaced) is measured
       # here, and so is any lane that adds an arm without deleting one.
+      # RQ-58-RETIRE (v0.58): first downward movement — the 50 DSL rules'
+      # superseded hand-written arms deleted (36 flag-guarded sites across
+      # both selectors) plus the then-dead SYNTH_SEL_DSL lever, each deletion
+      # byte-identity-gated (688-row corpus manifest + 10 frozen anchors).
+      # 18,582 -> 17,897; banked. The former #992 waiver (to: 18582) is
+      # deleted with the re-bank — a surviving waiver above the new baseline
+      # would be a standing licence to grow back to it.
       - kind: ratchet
         name: selector_lines_code
         direction: down
-        value: 18582
-        baseline: 18480
-        waivers:
-          - to: 18582
-            reason: >-
-              Growth is #992's, not this lane's: the ARM select-on-i64-comparison
-              miscompile fix (#973) added 102 code-region lines (an operand-
-              classification helper + two guarded call sites). #992 merged at
-              19:50 UTC and #991 pinned these values at 20:07 from a PR base
-              that predated it (strict=false stale-base cross), so main itself
-              derives 18582 against a ledger saying 18480 — this PR is the
-              first to carry the union and the ledger moves here, with the
-              growth attributed to the correctness fix that caused it.
+        value: 17897
+        baseline: 17897
       # 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
@@ -1255,35 +1251,32 @@ claims:
       - kind: ratchet
         name: selector_lines_total
         direction: track
-        # 29616 -> 29839: #992 (+102 code-region lines, +121 test-module lines)
-        # crossed with #991's pin measurement on a stale base; see the
-        # selector_lines_code waiver above for the attribution.
-        value: 29839
+        # 29839 -> 28495 (RQ-58-RETIRE): -685 code-region lines (the arm
+        # deletions) and -659 test-module lines (the four mirror-pin tests,
+        # vacuous once the hand-written mirror was gone — the
+        # VcrSelRulesGenCheck precedent).
+        value: 28495
       # 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
       # miscompile risk. Red-first demonstrated on the REAL file, not only
       # against a synthetic fixture: see scripts/repro/rq_58_metric_gate.md §1b.
+      # RQ-58-RETIRE (v0.58): 63 -> 56. Seven '_ => unreachable!()' arms
+      # lived INSIDE deleted hand-written bodies (the sd/sws i64-comparison
+      # condition maps, the sws i64 bitwise/shift/rotate/bit-count group
+      # dispatches, the sws i32 shift dispatch); they went with their arms.
+      # Banked; the former #992 waiver (to: 63) deleted with the re-bank.
       - kind: ratchet
         name: selector_wildcard_arms_code
         direction: down
-        value: 63
-        baseline: 62
-        waivers:
-          - to: 63
-            reason: >-
-              The one new absorbing arm is `_ => None` in #992's i64-comparison
-              operand-classification helper (a total function over WasmOp whose
-              non-comparison arms decline, feeding the #973 miscompile fix) —
-              added on main by #992 after #991 measured this pin on a stale
-              base. Same cross as the selector_lines_code waiver.
+        value: 56
+        baseline: 56
       - kind: ratchet
         name: selector_wildcard_arms_total
         direction: track
-        # 105 -> 106: the same #992 `_ => None` helper arm the code-region
-        # waiver above covers (the arm is in the CODE region; both counts
-        # include it), crossed with #991's stale-base pin measurement.
-        value: 106
+        # 106 -> 91 (RQ-58-RETIRE): the 7 code-region arms above plus 8
+        # assertion-helper '_ =>' arms inside the retired mirror-pin tests.
+        value: 91
 
   # 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

coq/STATUS.md

@@ -600,10 +600,11 @@ The Rocq suite proves things in two very different places, and #73's
 measurable if they are counted separately:
 
 - **DSL-served** — the op's *shipped* lowering is a `sel_dsl` rule with a
-  1:1 Qed theorem in `VcrSelRules.v`, register-polymorphic, mirror-pinned
-  byte-identical to the hand-written arm(s) (`SYNTH_SEL_DSL`, **default ON**
-  since the increment-1..4 flip — opt-out `SYNTH_NO_SEL_DSL=1`). These proofs
-  are about the code that ships — and now, by default, the code that DOES ship.
+  1:1 Qed theorem in `VcrSelRules.v`, register-polymorphic, and since
+  RQ-58-RETIRE (v0.58) the ONLY lowering for the op: the hand-written arms
+  the rules had mirrored byte-identically were deleted, along with the
+  `SYNTH_SEL_DSL`/`SYNTH_NO_SEL_DSL` lever. These proofs are about the code
+  that ships — now the only code there is.
 - **model-only** — the op is proven only against `compile_wasm_to_arm`
   (Compilation.v), the fixed-register model that diverges from the shipped
   Rust selector in documented ways (#73). Evidence about a model, not the
@@ -655,9 +656,9 @@ additionally gates FPU ops behind the #369/GI-FPU work.
 
 **Retirement criterion (#73):** a `compile_wasm_to_arm` arm may be deleted
 (and its Correctness* theorem retired) once its family is DSL-served — the
-DSL theorem is strictly stronger (register-polymorphic, mirror-pinned to
-the shipped bytes). The model-only column is the shrinking measure; report
-it per release.
+DSL theorem is strictly stronger (register-polymorphic, and since v0.58 the
+rule IS the shipped lowering, no mirror in between). The model-only column
+is the shrinking measure; report it per release.
 
 ## Phase History