RQ-59-SUBTRACT (#242): increment 6 — six Rocq-proved rules (74 -> 80), every superseded arm DELETED; selector 18,291 -> 18,278, wildcards 56 -> 55

[avrabe]

VCR-SEL-001 increment 6. Six new Rocq-proved rules (74 → 80, all Qed, stated
directly about the generated model per #667), each landing WITH the deletion
of the hand-written emission it supersedes — never alongside. One delegation
attempt was REFUSED on the byte-identity rule and is documented below.

Ratchet, before → after

metric	before (this lane's base)	after	Δ
selector_lines_code (must FALL)	18,291	18,278	−13
selector_lines_total (track)	28,912	28,899	−13
selector_wildcard_arms_code (must FALL)	56	55	−1 (back at baseline)
selector_wildcard_arms_total (track)	91	90	−1
sel_dsl_rules (must RISE)	74	80	+6

All movements banked in claims.yaml in the commits that caused them (the
lines waiver re-derived at 18,278, carrying forward the two waived v0.59
soundness growths #989/#990 minus this fall).

Per commit

1. db7e0e2 — increment-6 rules, byte-neutral. 5 new rules + 5 Qed:
   rule_i32_extend8_s / rule_i32_extend16_s (new SXTB/SXTH model
   constructors; semantics are Definitions via I32 shifts, not axioms —
   axiom count unchanged at 93) and rule_i64_extend{8,16,32}_s (new
   I64Extend{8,16,32}SPseudo constructors, rd_hi <> rd_lo Ok-or-Err).
   Selector untouched; model coverage re-banked (simplified-only 68 → 73,
   uncovered stays 4: B/BL/BX/VMOV).
2. f16724d — delete the family's hand-written arms (one group commit per
   the RETIRE one-op-or-group rule; per-op commits would each carry a
   wrong-way waiver the next commit obsoletes). Deleted: sws
   I32Extend8S/I32Extend16S ArmOp::Sxtb/Sxth pushes; the sws
   I64Extend{8,16,32}S construction match including its
   _ => unreachable!() wildcard; sd's five fixed-register vec arms.
   Byte-identity: the prior corpus had zero extendN_s coverage — the
   manifest could not have discriminated exactly these arms — so
   sign_extend_family.wat was added first (every converted arm fires,
   both selector paths, baseline rows captured at the pre-deletion binary).
   Then: 704-row corpus manifest (176 fixtures × 4 configs — m4f/m4/r5
   relocatable + m4f self-contained; 633 OK .text sha256 + 67 declines
   pinned with exit code and reason) identical to the pre-deletion baseline,
   704/704; 10/10 frozen anchors green.
3. fe19fd2 — sd I64ExtendI32S / I32WrapI64 delegated to their
   existing increment-5 rules (structurally identical ArmOp values; rules'
   delegation → Both). Corpus manifest 704/704 again — with the honest note
   that these sd arms are production-unreachable via compile paths (live via
   the pub select() API), so the structural identity plus the pinned
   generated-rule fixpoint carry the evidence there.
4. 3af9e50 — rule_i64_const (80th rule). First rule over a dynamic i64
   immediate (new imm64 DSL concept: value: i64 / (v : I64.int) binder).
   Both selectors' hand-written ArmOp::I64Const constructions deleted.
   Corpus manifest 704/704 — and this one is a discriminating result:
   i64.const fires across the corpus's many i64 fixtures.
5. 33278d2 — extraction snapshots refreshed. Found stale since feat(coq): flat-executor upgrade — SBCS, CMPcc, branching BCondOffset; I64SetCond expansion-tier T1; first #73 admit discharged (#242) #697
   (Integers.ml was missing the coq: i32_const_correct is Admitted (false as stated) — and BIN-VERIFY defers Const to it, so nothing covers i32.const #933 I32Const normalization and the
   signed-divs guard): regenerated with the same nix rocq CI uses, now
   carrying increment 6. No consumer, no freshness gate — wiring one is a
   policy call left to the hub.
6. 4ede08a — rivet: RQ-59-SUBTRACT implemented.

Attempted and REFUSED (the rule working, not an omission)

• sd I64ExtendI32U delegation — its rule lowers to the two-instruction
  MOV + MOVW form select_with_stack ships, while the sd path emits the single
  I64ExtendI32U pseudo. Different bytes, no execution oracle on that path →
  refused; the hand-written arm stays, refusal documented at the arm.
• i64.extend32_s → rule_i64_extend_i32_s reuse (considered before
  building the pseudo rule): the encoders' ASR source registers differ
  (rnlo vs rdlo) — same value, different bytes when rdlo != rnlo →
  refused; the family got its own pseudo-tier rules emitting the exact
  shipped ArmOps instead.

Execution evidence beyond byte-identity

#973 ARM corpus sweep run locally on the branch head: PASS —
compiled 148/160, 2,502 emulated vectors (unicorn vs wasmtime), 0 mismatches,
0 faults, including sign_extend_family.wat's all-i32 export. Emulation floor
2,335 still cleared. EXPECTED_DECLINES untouched (declines byte-for-byte
identical in the manifest).

Gates (run before every push)

cargo fmt --check · cargo clippy --workspace --all-targets -- -D warnings
· cargo test --workspace (true exit 0; includes the 10 frozen anchors) ·
python3 scripts/claim_check.py claims.yaml 50/50 (+ --metric table above,
--emit-status surfaces regenerated) · python3 scripts/model_coverage_audit.py --check ok · bazel test //coq:verify_proofs
green (80-rule coverage gate included).

Refs #242

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 95.78313% with 7 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/sel_dsl/generated.rs	91.30%	4 Missing ⚠️
crates/synth-synthesis/src/sel_dsl/mod.rs	95.83%	3 Missing ⚠️

📢 Thoughts on this report? Let us know!