feat(VCR-ISA-001): extend generate-not-mirror Rocq ISA model to nine i64 pseudo-ops (41→50)

[avrabe]

Summary

Wave-2 extension of the VCR-ISA-001 "generate, don't mirror" Rocq ISA model (#667 lineage, #242 epic): add the nine single-pseudo-op i64 register-pair shapes the selector already emits but were DSL-uncovered — 41 → 50 rules / Qed.

New ops (each a single flat-model pseudo-op with a fixed-register ancestor in CorrectnessI64.v, so the DSL work is pure register-generalization + re-export, exactly like i64.eqz #767):

family	ops	pseudo-op
unary bit counts	i64.clz / i64.ctz / i64.popcnt	I64{Clz,Ctz,Popcnt}Pseudo
binary pairs	i64.mul / i64.shl / i64.shr_u / i64.shr_s	I64{Mul,Shl,ShrU,ShrS}Pseudo
rotates	i64.rotl / i64.rotr	I64{Rotl,Rotr}Pseudo

Architecture (#667)

The shipped sel_dsl::RULES table EMITS VcrSelRulesGenerated.v (Module Gen) + generated.rs; VcrSelRules.v DEFINES rule_X := Gen.rule_X and states the 9 new correctness Qed directly about the generated sequences. A table change regenerates Gen and breaks the matching proof — drift is unrepresentable at the instruction-sequence level. Demonstrated: flipping Gen.rule_i64_mul from I64MulPseudo to I64ShlPseudo makes rule_i64_mul_correct fail to compile (//coq:rocq_proofs FAILED TO BUILD); reverted.

Side conditions (minimal, and correct)

Each pseudo-op reads every operand half into a local BEFORE any set_reg, so:

• unary counts: none (rd may alias rn_lo — the R0,R0,R1 in-place emit is admitted);
• binary pairs / rotates: a single rd_hi <> rd_lo (the high write must not destroy the low result word).

NOT the increment-3 three-condition pair set — those were flags-coupled ADDS+ADC pairs. Every select_with_stack emit site uses alloc_consecutive_pair, so rd_hi <> rd_lo holds by construction. Statements are value-level like the i64.eqz ancestor (no exec_wasm_instr hypothesis — the i64 ops aren't in WasmSemantics.v); shift/rotate count is the low half only (combine_i32 cnt I32.zero), matching the _bits_spec axioms.

Verification

• Rocq green: bazel test //coq:verify_proofs — //coq:rocq_proofs + //coq:vcr_sel_rules_coverage both PASS (all 50 rules, 50 Qed, 0 Admitted in the rule table).
• Drift-guard: flipping a generated rule breaks its Qed (shown above).
• Byte-invisibility: SYNTH_NO_SEL_DSL=1 vs default is bit-identical for these ops — mirror-pinned by sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242, extended with dedicated count/rotate/pair-bin probe windows (probed 16→25, each a byte-equality assert). The nine select_default blind arms are the holdout, unchanged (Delegation::SelectWithStack).
• No regression: frozen anchors (cargo test -p synth-cli --test frozen_codegen_bytes) 10/10 intact; cargo test -p synth-synthesis --lib 624/624.
• Claim gate: python3 scripts/claim_check.py claims.yaml → 19/19 hold (476→485 Qed, 41→50 rules, STATUS coverage 26%→32%).
• fmt + clippy --workspace --all-targets -D warnings clean.

Refs #667 (VCR-ISA-001), #242. Do not merge without review.

🤖 Generated with Claude Code

https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L

[codecov]

Codecov Report

❌ Patch coverage is 96.17978% with 17 lines in your changes missing coverage. Please review.

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	95.40%	8 Missing ⚠️
crates/synth-synthesis/src/sel_dsl/generated.rs	95.62%	6 Missing ⚠️
crates/synth-synthesis/src/sel_dsl/mod.rs	97.76%	3 Missing ⚠️

📢 Thoughts on this report? Let us know!