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

[avrabe]

RQ-58-RETIRE (#242) — delete the hand-written arms the 50 Rocq-proved DSL rules replaced

The headline deletion, and it was byte-identical throughout — no finding of the
"flip does not cover what it claims" class surfaced. All 36 flag-guarded sites
(21 select_default + 15 select_with_stack) collapsed to their Rocq-proved
sel_dsl rule call, one op/group per commit so a bisect lands on a single op;
then the SYNTH_SEL_DSL/SYNTH_NO_SEL_DSL lever and the four mirror-pin tests
retired as vacuous (the VcrSelRulesGenCheck precedent — a byte-equality gate
with one implementation left proves reflexivity).

The ratchet moves DOWN for the first time

metric	main	this PR	Δ
selector_lines_code (ceiling)	18,582	17,897	−685
selector_wildcard_arms_code (ceiling)	63	56	−7
selector_lines_total (track)	29,839	28,495	−1,344
selector_wildcard_arms_total (track)	106	91	−15
sel_dsl_rules (floor)	50	50	0

claims.yaml carries the live values, both improvements banked into
baseline:, and the two former #992 waivers are deleted with the re-bank (a
surviving waiver above the new baseline is a standing licence to grow back to
it). status.json regenerated via --emit-status. claim_check 49/49.

Byte-identity evidence, per commit

Every commit was gated on:

• a 688-row corpus manifest — all 156 scripts/repro/*.wat + the 4 frozen
  .wasm anchors × 4 configs (cortex-m4f/cortex-m4 relocatable,
  cortex-m4f self-contained, cortex-r5 relocatable), sha256 of the full
  output ELF, declines pinned as rows too — diff-identical against the
  origin/main baseline binary on every one of the 35 commits;
• the 10 frozen anchors (frozen_codegen_bytes, 10 passed; 0 failed
  asserted non-vacuously per commit).

The 7 wildcard arms deleted from the code region were all _ => unreachable!()
arms inside deleted hand-written bodies (condition maps and group dispatches);
the other 8 total-count wildcards were assertion helpers inside the retired
mirror-pin tests.

Ops retired (lines deleted per commit, selector file only)

select_default (all 30 DSL-wired sd ops): i32 add −18/+8 (incl. the block-comment
rewrite), sub −11, mul −7, and −11, or −11, xor −11, shl −23/+6, shr_s −19/+2,
shr_u −19/+2, rotl −17/+6, rotr −7, clz −12/+4, ctz −8, popcnt −10; i64 and −26/+9,
or −26/+9, xor −26/+9, comparisons×10 (group arm) −41/+12.

Both selectors in one commit (same op): i64 add −68/+24, sub −58/+17,
eqz −31/+7.

select_with_stack group/single arms: i64 {or,and,xor} −68/+13,
{shl,shr_u,shr_s} −44/+12, comparisons×10 −40/+7, mul −24/+12, {rotl,rotr} −29/+8,
{clz,ctz,popcnt} −32/+11; i32 comparisons×10 (flag conditioning only, see
residual) −11/+8, eqz −32/+8, {shl,shr_s,shr_u,rotr} −62/+8, clz −19/+6,
ctz −24/+7, popcnt −18/+6.

Final functional commit (lever + mirror-pins): −753/+44. Whole PR:
+345/−1,657 (net −1,312).

The not-yet-deletable residual (RQ-58-SPLIT input) — measured, complete

Covered ops whose per-path arm was never DSL-wired, so nothing there was
superseded (deleting them would change bytes, which this lane refuses):

• select_with_stack (the direct/--relocatable path — live in production):
  • I32Add/Sub/Mul/And/Or/Xor — large hand-written arms carrying the
    foldable_addsub_imm/foldable_bitwise_imm immediate folds; the DSL's
    reg-reg rules don't express the imm shapes, so no hook was ever wired.
  • I32Rotl — hand-written RSB+ROR with an allocated scratch; rule_i32_rotl
    exists (it is the sd lowering) but was never wired here.
  • the i32-comparison imm-fold fallback (selector: emit cmp/cmn immediates for compare bounds instead of materializing — flat_flight clamps (lever #3) #258 cmp a,#C / cmn a,#-C +
    SetCond) — the reg-reg case of the shared arm now takes i32_cmp_rule
    unconditionally, but no CmpImm-shaped rule exists, so the fold's emission
    stays hand-written; re-pinned by the rewritten
    cmp_imm_fold_residual_path_stays_handwritten_258 (fold fires, reg-reg
    rule path provably not taken).
• select_default (production-unreachable for these ops — select_with_stack
  matches all 50 covered ops before its _ => fallthrough, so they can only be
  reached via the pub select() API used by tests/benchmarks):
  • blind bare-Cmp I32Eq..I32GeU and I32Eqz arms (never materialize the
    0/1 result — the documented increment-2 holdout; a rule byte-matching them
    would be unprovable as T1);
  • fixed-pair I64Mul/Shl/ShrU/ShrS/Rotl/Rotr/Clz/Ctz/Popcnt pseudo-op arms.

Note the direction: --relocatable forces the direct selector
(select_with_stack, #197) — direct ≠ default; the residual above is stated
against the correct path assignment.

Step 5 — witness MC/DC (#978): checked, not assumed

The harness links synth-synthesis (via synth-backend-riscv), so the wasm
binary DOES change — the counts were measured, not waved off. Ran the real gate
(scripts/mcdc_run.sh + scripts/mcdc_gate.py, witness-mcdc, rustc 1.96.1
— the pinned measurement compiler) on this branch AND on a pristine
git archive origin/main export, same host:

• TOTAL identical in both runs: 26 dec · 9 full · 122 cond · 50 proved ·
  21 gap · 51 dead. The only diff between the two gate outputs is witness's
  internal row indices (wasm layout shifted); every scored count, every
  per-function row and every gap row (read, per the loop's rule) is
  identical. No decision moved: the deleted decisions live in
  synth_synthesis::instruction_selector, which mcdc_gate.py names as
  explicitly out of scope (its SCORED_PREFIXES).
• The local absolutes differ from the CI floors (130/57/50) on both main
  and branch equally — the documented darwin-vs-CI platform delta the gate's
  own doc anticipates ("read the DELTA locally; the floors are the CI
  platform's baseline"). Delta = zero; the CI job scores the same tree-state
  inputs it scores on main.

Step 6 — sigil: not applicable, with the reason stated

This lane lands no new build artifact and no new build stage — it deletes
code inside an existing crate and proves the shipped binaries byte-identical to
baseline across the 688-row corpus. There is nothing new to sign and the
attestation surface is unchanged. Stated per the loop's rule rather than marked
N/A silently; if this reason recurs a third lane running, file it.

Gates (all run without pipes, rc captured)

• cargo test --workspace — rc=0, 2,826 tests / 142 suites, 0 failures
• cargo clippy --workspace --all-targets -- -D warnings — rc=0
• cargo fmt --check — rc=0
• python3 scripts/claim_check.py claims.yaml — rc=0, 49/49
• No CHANGELOG edit, no version bump, no hand-edited generated files
  (status.json via --emit-status; sel_dsl/generated.rs and the emitted
  Rocq model untouched — the RULES table, including its Delegation metadata
  the generation consumes, is unchanged). No new .wat → fix(#973): ARM select on an i64-comparison returns the then-arm — and an ARM leg for the corpus CI never compiled #992's
  EXPECTED_DECLINES exact set unaffected.

rivet: RQ-58-RETIRE → implemented with evidence + the residual set;
verified-codegen-roadmap.yaml VCR-SEL-001 entry carries the dated landing
paragraph.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.

📢 Thoughts on this report? Let us know!