feat(vcr-sel): increment 4 — i32 bit-manip + binary I64SetCond comparison rules, 40/40 Qed (#242)

[avrabe]

VCR-SEL-001 increment 4 (epic #242)

Extends the Rocq-discharged selector DSL into the scratch-using and multi-instruction tier the pilot called out and increments 1–3 deferred, plus the binary i64 comparison family — the highest-value target (the shape #615 re-implemented on A32, where cond-mapping bugs live). Design doc: docs/design/vcr-sel-001-increment-4.md.

Rules (27 → 40, all 1:1 Qed, 0 Admitted)

Rule	Shape	Discharge
rule_i32_clz	single CLZ (first unary rule)	synth_unop_proof_poly
rule_i32_ctz	two-instruction RBIT rd, rm; CLZ rd, rd — the scratch=dest trick: no extra scratch register, no aliasing side condition (RBIT reads before writing; instr 2 only reads rd)	stepped proof closing with I32.clz_rbit
rule_i32_popcnt	pseudo-op tier (mirrors the single ArmOp::Popcnt the selector emits)	synth_unop_proof_poly
rule_i64_{eq,ne,lt_s,lt_u,gt_s,gt_u,le_s,le_u,ge_s,ge_u}	the single-I64SetCond-pseudo-op shape both selectors emit, over FIVE register variables, no side conditions (the pseudo-op reads all four operand halves before writing rd)	synth_i64_setcond_proof_poly against i64_setcond_bits_spec — the register-generalized CorrectnessI64Comparisons.v ancestors

i32 rotr-by-register: already served since increment 2 (checked, nothing re-added).

The I64SetCond verdict (honest bound, documented)

Verified: the condition-code mapping (which Condition serves which WASM op — the selector-level #615 bug class) for every register assignment, in both selectors, pseudo-op-tier T1.
Not expressible in the flat executor — the encoder's CMP lo,lo; SBCS rd,hi,hi; MOVcc expansion (with the GT/LE/HI/LS operand swap) needs three things ArmSemantics.v lacks: (a) SBCS (flag-setting SBC — the model's SBC writes no flags), (b) conditionally-executed flags-writers (CMPEQ for the EQ/NE chain; only MOVcc exists), (c) three-operand borrow-aware C/V helpers. Same executor gap as the VCR-ISA-001 BCondOffset spike — pseudo-op tier is the honest ceiling until the Sail model lands. Fully documented in the design doc + VcrSelRules.v header.

Same asterisk for popcnt: the theorem covers the selector's ArmOp emission; the encoder's shift-and-add expansion (where #632 lived) stays oracle-covered, not Rocq-covered.

#667: DSL-coverage vs model-relevance metric

coq/STATUS.md gains the per-op-family table — DSL-served (rule+Qed) / compile_wasm_to_arm-model-only / unverified — so #73's retirement-by-subtraction of the divergent monolithic model is measurable per release. Current: 40 ops DSL-served (~26%), ~96 model-only (~62%), ~19 unverified (~12%); retirement criterion stated (a model arm may be deleted once its family is DSL-served).

Gates

• Rocq: bazel test //coq:verify_proofs green (proofs + vcr_sel_rules_coverage, manifest 27→40)
• Mirror-pins (gate 1): select_default loop 17→30 probes; select_with_stack loop 14→17 (new unary window branch); i64 loop 6→16 (new I64SetCond window branch) — all with the RMW-vacuity window check (hand-written emission window ≡ rule output for the selector's own registers)
• OFF ≡ baseline by construction (every delegation flag-gated, SYNTH_SEL_DSL default OFF)
• Frozen anchors 10/10 flag-OFF and flag-ON (SYNTH_SEL_DSL=1 moves no fixture byte)
• fmt --check clean, clippy -D warnings clean (all 17 crates), full per-crate test sweep green

Flip status

Unchanged ritual: 40/40 rules (100%) serve behind the default-OFF flag; the flip is a later dedicated PR, never bundled with a byte-changing lever.

Part of #242; metric from #667.

🤖 Generated with Claude Code

[codecov]

Codecov Report

❌ Patch coverage is 98.51190% with 5 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	98.18%	3 Missing ⚠️
crates/synth-synthesis/src/sel_dsl/mod.rs	96.77%	2 Missing ⚠️

📢 Thoughts on this report? Let us know!