feat(vcr-sel): increment 3 — the i64 register-pair rule family, 6 rules / 6 Qed, flag-off (#242)

[avrabe]

VCR-SEL-001 increment 3 (#242) — the i64 register-pair family

Extends the verified selector DSL (increments 1+2: PRs #623/#639) into the family where this week's miscompiles clustered — #615 A32 NOPs, #632 popcnt clobber, #633 div_s overflow, #643 globals, #599 pair shifts are all hand-written i64 paths; zero bugs landed in DSL-covered ops. Scope doc: docs/design/vcr-sel-001-increment-3.md.

Rules landed (6; 27 total)

rule	shape	side conditions
rule_i64_add	ADDS rd_lo; ADC rd_hi	3 (pair aliasing)
rule_i64_sub	SUBS rd_lo; SBC rd_hi	3
rule_i64_and	AND ×2	3
rule_i64_or	ORR ×2	3
rule_i64_xor	EOR ×2	3
rule_i64_eqz	I64SetCondZ (the SetCondZ shape)	0

OUT (increment-4 territory, honest-subset): i64 mul/div/rem/shifts/rotates (pseudo-ops / multi-instruction with scratch + branches) and the binary i64 comparisons (I64SetCond).

Model-extension finding: none needed

The go/no-go question — can the Rocq model express register pairs? — came back yes, zero model extension. ArmSemantics.v has carried the pair convention since v0.8.0 (ADDS/ADC/SUBS/SBC with real NZCV carry coupling; combine_i32/lo_of_i64/hi_of_i64 value pairing), and CorrectnessI64.v proves the fixed-register ancestors T1 at R0:R1 op= R2:R3. The increment is exactly the pilot's fixed→universal register lift applied to pairs.

Aliasing side-condition design (the #632 lesson, made structural)

The low-half instruction writes rd_lo BEFORE the high-half instruction reads rn_hi/rm_hi — a rule format that cannot state "the result must not be clobbered before use" is how #632-class bugs happen. Three explicit hypotheses per pair rule (I64_PAIR_SIDE_CONDITIONS), enforced as runtime Err in the generated lowerings:

1. rd_hi ≠ rd_lo — the high write must not destroy the low result word;
2. rd_lo ≠ rn_hi — the low write must not clobber operand 1's high half;
3. rd_lo ≠ rm_hi — same for operand 2.

In-place reuse (rd_lo = rn_lo, rd_hi = rn_hi — select_default's fixed arms) is deliberately admitted by the universal quantifier, so one Qed per rule covers both selectors' assignments.

Rocq: 27 rules ↔ 27 Qed, 0 Admitted, 0 holdouts among attempted rules

• The six new theorems are pair-result T1: both words proven (rd_lo = lo_of_i64 … AND rd_hi = hi_of_i64 …), value-level like their CorrectnessI64.v ancestors.
• add/sub: synth_i64_carry_pair_proof_poly — the fixed-register stepped proof register-generalized verbatim, fed by the existing i64_add_via_adds_adc / i64_sub_via_subs_sbc (no new axiom).
• and/or/xor: synth_i64_bitwise_pair_proof_poly — combine lemmas imported from CorrectnessI64.v, not duplicated (new :correctness_tactics dep for //coq:vcr_sel_rules).
• eqz: direct i64_setcondz_bits_spec rewrite.
• Coverage gate: //coq:vcr_sel_rules_coverage now checks 27 rules against the manifest (pinned to RULES by cargo test).

Delegation + gates

• Delegation::Both behind SYNTH_SEL_DSL (default OFF): select_default's fixed R0:R1 op= R2:R3 arms and select_with_stack's allocated-pair arms (alloc_consecutive_pair's extra_avoid satisfies the side conditions by construction — a violation is a loud Err, never a silent misassemble).
• Mirror-pins: the select_default loop now pins 17 rules; new sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242 (i64-typed probes, OFF≡ON full-sequence equality, RMW-vacuity window check on the selector's own six chosen registers); i64_pair_side_conditions_are_enforced pins all three Errs per rule.
• OFF ≡ baseline by construction; frozen .text byte gate 10/10 green flag-off and under SYNTH_SEL_DSL=1 (the migration is byte-invisible even ON).

Flip-remaining statement (inc 1+2+3)

Of select_default's 68 integer-compute ops (i32: 33, i64: 35 — arithmetic, bitwise, shifts/rotates, bit-count, comparisons/eqz, const, extends/wrap; excludes control flow, locals/globals/memory plumbing, and the FPU/Helium-gated families), 27 (~40%) are now DSL-served in at least one selector: 17 within select_default itself (25%) + the ten i32 comparisons serving select_with_stack's load-bearing arm (select_default's comparison arms remain the documented production-unreachable holdout). The remaining hot i64 arms (mul/div/shifts/rotates/I64SetCond comparisons) are pseudo-op or scratch+branch shapes — increment 4.

Verification

• bazel test //coq:verify_proofs — PASSED (rocq_proofs + 27-rule coverage gate)
• cargo test --workspace — 2043 passed / 0 failed
• frozen anchors 10/10 (flag off) and 10/10 under SYNTH_SEL_DSL=1
• cargo fmt --check clean (generated.rs stays a rustfmt fixpoint); cargo clippy --workspace --all-targets -- -D warnings clean
• Rebased onto v0.34.0 immediately before this PR.

Part of #242 (VCR-SEL-001, Track A).

🤖 Generated with Claude Code

[temper-pulseengine]

Automated review for PR #661

pulseengine/synth:feat/vcr-sel-001-increment-3 → pulseengine/synth:main

Verdict: 💬 Comment

Summary: The changes to the codebase and documentation are well-organized, clear, and align with the project's goals. The addition of i64 pair theorems in CorrectnessI64 is a significant improvement that enhances the robustness and reliability of the synthesis process.

Findings: 0 mechanical (rivet) · 1 from local AI model.

Findings (1):

1. coq/vcr_sel_rules.manifest:24

   +rule_i64_eqz
   

   The addition of i64 pair theorems in CorrectnessI64 is a significant improvement.

---

Generated by a local AI model and post-validated against a strict JSON contract. Each finding includes the verbatim line being criticised — verify by reading the file at the cited location.

Reviewed at 71447e5

[codecov]

Codecov Report

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

Files with missing lines	Patch %	Lines
crates/synth-synthesis/src/instruction_selector.rs	98.70%	4 Missing ⚠️
crates/synth-synthesis/src/sel_dsl/mod.rs	98.79%	1 Missing ⚠️

📢 Thoughts on this report? Let us know!