From 71447e5bf96fdcf44c1c792be9aaf826facccb57 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 8 Jul 2026 19:34:49 +0200 Subject: [PATCH] =?UTF-8?q?feat(vcr-sel):=20increment=203=20=E2=80=94=20th?= =?UTF-8?q?e=20i64=20register-pair=20rule=20family,=206=20rules=20/=206=20?= =?UTF-8?q?Qed,=20flag-off=20(#242)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The DSL steps into the family where this week's miscompiles clustered (#615/#632/#633/#643/#599 — all hand-written i64 paths; zero bugs in DSL-covered ops): i64 add/sub/and/or/xor as two-instruction pair rules (ADDS+ADC / SUBS+SBC / ANDx2 / ORRx2 / EORx2 over six register variables) plus i64.eqz (the I64SetCondZ shape). Model finding: the Rocq flat model needed ZERO extension for pairs — ADDS/ADC carry coupling and combine_i32/lo_of_i64/hi_of_i64 have carried the pair convention since v0.8.0. The increment is the pilot's fixed-to-universal register lift applied to CorrectnessI64.v's ancestors, with what was 'discriminate' on concrete registers becoming three explicit aliasing hypotheses per pair rule (the #632 lesson made structural): rd_hi<>rd_lo, rd_lo<>rn_hi, rd_lo<>rm_hi — runtime Ok-or-Err in the generated lowerings, never a silent misassemble. In-place rd=rn reuse stays admitted, so one Qed covers both selectors. - coq/Synth/Synth/VcrSelRules.v: +6 pair-result T1 theorems (both words proven), 27/27 Qed, no new axiom (carry/borrow via the existing ArmFlagLemmas lemmas; combine lemmas imported from CorrectnessI64). - sel_dsl: RegVar pair variables, Adds/Adc/Subs/Sbc/I64SetCondZ templates, i64_pair_rule dispatch, generator learns wrapped signatures; generated.rs regenerated (rustfmt fixpoint). - Delegation::Both behind SYNTH_SEL_DSL (default OFF): select_default's fixed R0:R1 op= R2:R3 arms + select_with_stack's allocated-pair arms. - Mirror-pins: select_default loop now 17 rules; dedicated sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242 (i64-typed probes, RMW-vacuity window check); side-condition Err test. - OFF ≡ baseline by construction; frozen .text byte gate 10/10 green both flag-off AND under SYNTH_SEL_DSL=1. Part of #242 (VCR-SEL-001). Co-Authored-By: Claude Fable 5 --- artifacts/verified-codegen-roadmap.yaml | 38 +- coq/BUILD.bazel | 9 +- coq/Synth/Synth/VcrSelRules.v | 230 ++++++- coq/vcr_sel_rules.manifest | 6 + .../src/instruction_selector.rs | 569 ++++++++++++++---- .../synth-synthesis/src/sel_dsl/generated.rs | 233 ++++++- crates/synth-synthesis/src/sel_dsl/mod.rs | 340 ++++++++++- docs/design/vcr-sel-001-increment-3.md | 113 ++++ 8 files changed, 1381 insertions(+), 157 deletions(-) create mode 100644 docs/design/vcr-sel-001-increment-3.md diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 9988d55a..3896fc7f 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -426,11 +426,43 @@ artifacts: select_with_stack-delegated rules, with a non-vacuity window check that the delegation actually fired) + sel_dsl_cmp_imm_fold_path_stays_handwritten_and_byte_identical_242. - FLIP EVIDENCE: with all 21 rules mirror-pinned byte-identical, nothing + INCREMENT 3 LANDED (2026-07-08, flag-off, + docs/design/vcr-sel-001-increment-3.md): +6 rules = 27 total, each with + its 1:1 Qed (27/27, 0 Admitted, 0 holdouts among attempted rules). The + i64 register-pair family — add/sub/and/or/xor (two-instruction pair + shapes ADDS+ADC / SUBS+SBC / ANDx2 / ORRx2 / EORx2 over SIX register + variables rd_lo..rm_hi) + eqz (single I64SetCondZ). Chosen deliberately: + the #615/#632/#633/#643/#599 miscompile cluster is all hand-written i64 + paths, zero bugs in DSL-covered ops. MODEL FINDING: the Rocq flat model + needed ZERO extension for pairs — ADDS/ADC carry coupling + + combine_i32/lo_of_i64/hi_of_i64 have carried the pair convention since + v0.8.0; the increment is the pilot's fixed-to-universal register lift + applied to CorrectnessI64.v's ancestors. SIDE-CONDITION DESIGN (the + #632 lesson made structural): each pair rule carries THREE explicit + aliasing hypotheses (rd_hi<>rd_lo, rd_lo<>rn_hi, rd_lo<>rm_hi — the + low-half write must not clobber the high-half operands still to be + read, and the high write must not destroy the low result), runtime + Ok-or-Err in the generated Rust; in-place rd=rn reuse (select_default's + fixed R0:R1 op= R2:R3) is deliberately admitted, so one Qed covers both + selectors. Theorems are pair-result T1: BOTH words proven + (rd_lo=lo_of_i64, rd_hi=hi_of_i64 post-conditions), discharged by + synth_i64_carry_pair_proof_poly (via the existing i64_add_via_adds_adc + / i64_sub_via_subs_sbc, no new axiom) and + synth_i64_bitwise_pair_proof_poly (combine lemmas imported from + CorrectnessI64, not duplicated); eqz via i64_setcondz_bits_spec. + Delegation::Both — select_default fixed-register arms + the + select_with_stack allocated-pair arms (alloc_consecutive_pair's + extra_avoid satisfies the side conditions by construction). Mirror-pins: + the select_default loop now covers 17 rules; the dedicated + sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242 probes i64-typed + stacks with the RMW-vacuity window check; + i64_pair_side_conditions_are_enforced pins all three Errs per rule. + FLIP EVIDENCE: with all 27 rules mirror-pinned byte-identical, nothing byte-visible remains before the SYNTH_SEL_DSL default-on flip — the flip is a later PR with the standard re-freeze ritual. NOT yet done - (hence not verified): that default flip; optimizer_bridge + the - remaining select_with_stack families; div/rem (VCR-ISA-001-gated). + (hence not verified): that default flip; i64 + mul/div/shifts/rotates/comparisons (I64SetCond) + optimizer_bridge + + the remaining select_with_stack families; div/rem (VCR-ISA-001-gated). status: implemented tags: [codegen, selector, isle, verified-dsl, rocq, track-a, novel, release-v0.12.1] links: diff --git a/coq/BUILD.bazel b/coq/BUILD.bazel index 166bd10c..d806618f 100644 --- a/coq/BUILD.bazel +++ b/coq/BUILD.bazel @@ -204,7 +204,14 @@ rocq_library( name = "vcr_sel_rules", srcs = ["Synth/Synth/VcrSelRules.v"], include_path = "Synth", - deps = _CORRECTNESS_FULL_DEPS + [":tactics", ":arm_flag_lemmas"], + # :correctness_tactics provides CorrectnessI64 — increment 3's i64 pair + # theorems import its halves-distribute combine lemmas rather than + # duplicating them. + deps = _CORRECTNESS_FULL_DEPS + [ + ":tactics", + ":arm_flag_lemmas", + ":correctness_tactics", + ], ) # Master index: imports all correctness proofs diff --git a/coq/Synth/Synth/VcrSelRules.v b/coq/Synth/Synth/VcrSelRules.v index 717c44af..f4fbc172 100644 --- a/coq/Synth/Synth/VcrSelRules.v +++ b/coq/Synth/Synth/VcrSelRules.v @@ -1,4 +1,4 @@ -(** * VCR-SEL-001 increments 1+2: Rocq obligations of the wired selector rule table +(** * VCR-SEL-001 increments 1+2+3: Rocq obligations of the wired selector rule table One universally-quantified T1 theorem per rule in the checked-in DSL table [crates/synth-synthesis/src/sel_dsl/mod.rs] (RULES), naming 1:1: @@ -39,7 +39,36 @@ generalized to universally-quantified registers ([synth_cmp_binop_proof_poly] below), with the same three manual variants (ne / lt_s / lt_u) the fixed-register proofs in - CorrectnessI32.v use, parameterized over registers verbatim. *) + CorrectnessI32.v use, parameterized over registers verbatim. + + INCREMENT 3 extends the DSL into the i64 register-pair family — the + two-instruction pair shapes (ADDS+ADC / SUBS+SBC / ANDx2 / ORRx2 / + EORx2) plus the single-instruction [I64SetCondZ] shape for i64.eqz. + An i64 value lives in a (lo, hi) register pair, so each pair rule is + quantified over SIX registers and its theorem proves BOTH result + words. The pair shapes are where register generalization earns its + keep: the low-half instruction writes [rdlo] before the high-half + instruction reads [rnhi]/[rmhi], so a rule that could not state + "the destination must not be clobbered before use" would be exactly + how #632-class bugs happen. Three explicit aliasing hypotheses per + pair rule (carried as [SideCondition::NotAlias] in the Rust table and + enforced Ok-or-Err in the generated lowering): + + - [rdhi <> rdlo] — the high write must not destroy the low result; + - [rdlo <> rnhi] and [rdlo <> rmhi] — the low write must not + clobber a high-half operand the second instruction still reads. + + In-place lowering ([rdlo = rnlo], [rdhi = rnhi] — what + [select_default]'s fixed R0:R1 += R2:R3 arms emit) satisfies all + three, so one Qed per rule covers both selectors' assignments. + Discharge: the value-level carry/borrow lemmas already proven for the + fixed-register ancestors ([i64_add_via_adds_adc] / + [i64_sub_via_subs_sbc] in ArmFlagLemmas.v; the halves-distribute + combine lemmas in CorrectnessI64.v), applied under the generalized + register bookkeeping — no new axiom. The theorem shape follows the + CorrectnessI64.v ancestors: a value-level correspondence between the + WASM-spec function ([I64.add] etc. on [combine_i32]-combined + operands) and the ARM execution result, both halves pinned. *) From Stdlib Require Import List. From Stdlib Require Import ZArith. @@ -54,6 +83,10 @@ Require Import Synth.WASM.WasmSemantics. Require Import Synth.Synth.Compilation. Require Import Synth.Synth.Tactics. Require Import Synth.ARM.ArmFlagLemmas. +(* Increment 3: the halves-distribute combine lemmas + ({and,or,xor}_{lo,hi}_combine) proven for the fixed-register i64 + bitwise ancestors live in CorrectnessI64.v — imported, not duplicated. *) +Require Import Synth.Synth.CorrectnessI64. Import ListNotations. Open Scope Z_scope. @@ -455,3 +488,196 @@ Theorem rule_i32_ge_u_correct : forall wstate astate v1 v2 stack' rd rn rm, exec_program (rule_i32_ge_u rd rn rm) astate = Some astate' /\ get_reg astate' rd = (if I32.geu v1 v2 then I32.one else I32.zero). Proof. synth_cmp_binop_proof_poly flags_geu. Qed. + +(** ** Increment 3: the i64 register-pair rule lowerings — 1:1 with + sel_dsl::RULES / sel_dsl::generated. An i64 value is a (lo, hi) + register pair; operand 1 is (rnlo, rnhi), operand 2 is (rmlo, rmhi), + the result pair is (rdlo, rdhi). *) + +Definition rule_i64_add (rdlo rdhi rnlo rnhi rmlo rmhi : arm_reg) : arm_program := + [ADDS rdlo rnlo (Reg rmlo); ADC rdhi rnhi (Reg rmhi)]. +Definition rule_i64_sub (rdlo rdhi rnlo rnhi rmlo rmhi : arm_reg) : arm_program := + [SUBS rdlo rnlo (Reg rmlo); SBC rdhi rnhi (Reg rmhi)]. +Definition rule_i64_and (rdlo rdhi rnlo rnhi rmlo rmhi : arm_reg) : arm_program := + [AND rdlo rnlo (Reg rmlo); AND rdhi rnhi (Reg rmhi)]. +Definition rule_i64_or (rdlo rdhi rnlo rnhi rmlo rmhi : arm_reg) : arm_program := + [ORR rdlo rnlo (Reg rmlo); ORR rdhi rnhi (Reg rmhi)]. +Definition rule_i64_xor (rdlo rdhi rnlo rnhi rmlo rmhi : arm_reg) : arm_program := + [EOR rdlo rnlo (Reg rmlo); EOR rdhi rnhi (Reg rmhi)]. + +(** i64.eqz — unary, single [I64SetCondZ] pseudo-op (the SetCondZ shape); + the 0/1 result is a single i32 register, so no pair side conditions. *) +Definition rule_i64_eqz (rd rnlo rnhi : arm_reg) : arm_program := + [I64SetCondZ rd rnlo rnhi]. + +(** ** Increment-3 discharge tactics. + + [synth_i64_carry_pair_proof_poly] — the flags-coupled pair shapes + (ADDS+ADC / SUBS+SBC): verbatim the stepped structure of the + fixed-register [i64_add_correct] / [i64_sub_correct] proofs + (CorrectnessI64.v) modulo (a) the six register binders, (b) the + lowering-unfold target, and (c) the three aliasing hypotheses standing + in for what was [discriminate] on concrete registers. Parameterized by + the ArmFlagLemmas.v carry/borrow-propagation lemma. + + [synth_i64_bitwise_pair_proof_poly] — the flag-free parallel-halves + shapes (ANDx2/ORRx2/EORx2), parameterized by the lo/hi + halves-distribute lemmas from CorrectnessI64.v. *) + +Ltac synth_i64_carry_pair_proof_poly carry_lemma := + intros astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi + Hdd Hdnh Hdmh HR0 HR1 HR2 HR3; + unfold rule_i64_add, rule_i64_sub; + cbn [exec_program exec_instr eval_operand2]; + rewrite flags_set_flags_set_reg; + rewrite flag_c_update_flags_arith; + let Hpair := fresh "Hpair" in + pose proof (carry_lemma lo1 hi1 lo2 hi2) as Hpair; + let Hlo := fresh "Hlo" in + let Hhi := fresh "Hhi" in + destruct Hpair as [Hlo Hhi]; + eexists; split; + [ reflexivity + | split; + [ (* lo word: the high-half write must not have destroyed it. *) + rewrite (get_set_reg_neq _ rdhi rdlo) by exact Hdd; + rewrite get_reg_set_flags; + rewrite get_set_reg_eq; + rewrite HR0, HR2; exact Hlo + | (* hi word: the high-half instruction read its operands from the + post-low-half state, where rdlo was already written. *) + rewrite get_set_reg_eq; + rewrite !get_reg_set_flags; + rewrite (get_set_reg_neq astate rdlo rnhi) by exact Hdnh; + rewrite (get_set_reg_neq astate rdlo rmhi) by exact Hdmh; + rewrite HR0, HR1, HR2, HR3; exact Hhi ] ]. + +Ltac synth_i64_bitwise_pair_proof_poly lo_lemma hi_lemma := + intros astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi + Hdd Hdnh Hdmh HR0 HR1 HR2 HR3; + unfold rule_i64_and, rule_i64_or, rule_i64_xor; + cbn [exec_program exec_instr eval_operand2]; + eexists; split; + [ reflexivity + | split; + [ rewrite (get_set_reg_neq _ rdhi rdlo) by exact Hdd; + rewrite get_set_reg_eq; + rewrite HR0, HR2; apply lo_lemma + | rewrite get_set_reg_eq; + rewrite (get_set_reg_neq astate rdlo rnhi) by exact Hdnh; + rewrite (get_set_reg_neq astate rdlo rmhi) by exact Hdmh; + rewrite HR1, HR3; apply hi_lemma ] ]. + +(** ** Increment-3 pair theorems — quantified over all SIX registers, + under the three explicit aliasing hypotheses the rule table carries. + Pair-result T1: BOTH words of the result are proven. *) + +Theorem rule_i64_add_correct : + forall astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi, + rdhi <> rdlo -> (* high write must not destroy the low result *) + rdlo <> rnhi -> (* low write must not clobber operand-1's high half *) + rdlo <> rmhi -> (* low write must not clobber operand-2's high half *) + get_reg astate rnlo = lo1 -> + get_reg astate rnhi = hi1 -> + get_reg astate rmlo = lo2 -> + get_reg astate rmhi = hi2 -> + exists astate', + exec_program (rule_i64_add rdlo rdhi rnlo rnhi rmlo rmhi) astate + = Some astate' /\ + get_reg astate' rdlo = lo_of_i64 (I64.add (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)) /\ + get_reg astate' rdhi = hi_of_i64 (I64.add (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)). +Proof. synth_i64_carry_pair_proof_poly i64_add_via_adds_adc. Qed. + +Theorem rule_i64_sub_correct : + forall astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi, + rdhi <> rdlo -> + rdlo <> rnhi -> + rdlo <> rmhi -> + get_reg astate rnlo = lo1 -> + get_reg astate rnhi = hi1 -> + get_reg astate rmlo = lo2 -> + get_reg astate rmhi = hi2 -> + exists astate', + exec_program (rule_i64_sub rdlo rdhi rnlo rnhi rmlo rmhi) astate + = Some astate' /\ + get_reg astate' rdlo = lo_of_i64 (I64.sub (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)) /\ + get_reg astate' rdhi = hi_of_i64 (I64.sub (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)). +Proof. synth_i64_carry_pair_proof_poly i64_sub_via_subs_sbc. Qed. + +Theorem rule_i64_and_correct : + forall astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi, + rdhi <> rdlo -> + rdlo <> rnhi -> + rdlo <> rmhi -> + get_reg astate rnlo = lo1 -> + get_reg astate rnhi = hi1 -> + get_reg astate rmlo = lo2 -> + get_reg astate rmhi = hi2 -> + exists astate', + exec_program (rule_i64_and rdlo rdhi rnlo rnhi rmlo rmhi) astate + = Some astate' /\ + get_reg astate' rdlo = lo_of_i64 (I64.and (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)) /\ + get_reg astate' rdhi = hi_of_i64 (I64.and (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)). +Proof. synth_i64_bitwise_pair_proof_poly and_lo_combine and_hi_combine. Qed. + +Theorem rule_i64_or_correct : + forall astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi, + rdhi <> rdlo -> + rdlo <> rnhi -> + rdlo <> rmhi -> + get_reg astate rnlo = lo1 -> + get_reg astate rnhi = hi1 -> + get_reg astate rmlo = lo2 -> + get_reg astate rmhi = hi2 -> + exists astate', + exec_program (rule_i64_or rdlo rdhi rnlo rnhi rmlo rmhi) astate + = Some astate' /\ + get_reg astate' rdlo = lo_of_i64 (I64.or (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)) /\ + get_reg astate' rdhi = hi_of_i64 (I64.or (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)). +Proof. synth_i64_bitwise_pair_proof_poly or_lo_combine or_hi_combine. Qed. + +Theorem rule_i64_xor_correct : + forall astate lo1 hi1 lo2 hi2 rdlo rdhi rnlo rnhi rmlo rmhi, + rdhi <> rdlo -> + rdlo <> rnhi -> + rdlo <> rmhi -> + get_reg astate rnlo = lo1 -> + get_reg astate rnhi = hi1 -> + get_reg astate rmlo = lo2 -> + get_reg astate rmhi = hi2 -> + exists astate', + exec_program (rule_i64_xor rdlo rdhi rnlo rnhi rmlo rmhi) astate + = Some astate' /\ + get_reg astate' rdlo = lo_of_i64 (I64.xor (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)) /\ + get_reg astate' rdhi = hi_of_i64 (I64.xor (combine_i32 lo1 hi1) + (combine_i32 lo2 hi2)). +Proof. synth_i64_bitwise_pair_proof_poly xor_lo_combine xor_hi_combine. Qed. + +(** i64.eqz — the SetCondZ shape. Single instruction, no pair side + conditions (the pseudo-op reads both operand halves before writing + [rd], so every rd/rnlo/rnhi aliasing is admitted). Value-level T1 via + the [i64_setcondz_bits_spec] axiom, exactly like the fixed-register + bit-manipulation ancestors (i64_clz/ctz/popcnt in CorrectnessI64.v). *) +Theorem rule_i64_eqz_correct : forall astate lo hi rd rnlo rnhi, + get_reg astate rnlo = lo -> + get_reg astate rnhi = hi -> + exists astate', + exec_program (rule_i64_eqz rd rnlo rnhi) astate = Some astate' /\ + get_reg astate' rd = + (if I64.eq (combine_i32 lo hi) I64.zero then I32.one else I32.zero). +Proof. + intros astate lo hi rd rnlo rnhi HR0 HR1. + unfold rule_i64_eqz; simpl. + rewrite HR0, HR1. + rewrite i64_setcondz_bits_spec. + eexists. split; [reflexivity | apply get_set_reg_eq]. +Qed. diff --git a/coq/vcr_sel_rules.manifest b/coq/vcr_sel_rules.manifest index 4333f8dd..c91cf8aa 100644 --- a/coq/vcr_sel_rules.manifest +++ b/coq/vcr_sel_rules.manifest @@ -24,3 +24,9 @@ rule_i32_le_s rule_i32_le_u rule_i32_ge_s rule_i32_ge_u +rule_i64_add +rule_i64_sub +rule_i64_and +rule_i64_or +rule_i64_xor +rule_i64_eqz diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 9add0b47..b20f518a 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -3240,90 +3240,162 @@ impl InstructionSelector { }] } - // i64 arithmetic: ADDS/ADC for add, SUBS/SBC for sub + // i64 arithmetic: ADDS/ADC for add, SUBS/SBC for sub. + // VCR-SEL-001 increment 3 (#242): the i64 pair arms delegate to + // the Rocq-proved pair rules behind SYNTH_SEL_DSL (default OFF), + // byte-identical by construction — the fixed R0:R1 += R2:R3 + // in-place shape satisfies all three pair aliasing side + // conditions (rd_hi≠rd_lo, rd_lo≠rn_hi, rd_lo≠rm_hi), so the + // Err arm is unreachable here but stays loud, never silent. I64Add => { - vec![ - ArmOp::Adds { - rd: Reg::R0, - rn: Reg::R0, - op2: Operand2::Reg(Reg::R2), - }, - ArmOp::Adc { - rd: Reg::R1, - rn: Reg::R1, - op2: Operand2::Reg(Reg::R3), - }, - ] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_add( + Reg::R0, + Reg::R1, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .map_err(synth_core::Error::synthesis)? + } else { + vec![ + ArmOp::Adds { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }, + ArmOp::Adc { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Reg(Reg::R3), + }, + ] + } } I64Sub => { - vec![ - ArmOp::Subs { - rd: Reg::R0, - rn: Reg::R0, - op2: Operand2::Reg(Reg::R2), - }, - ArmOp::Sbc { - rd: Reg::R1, - rn: Reg::R1, - op2: Operand2::Reg(Reg::R3), - }, - ] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_sub( + Reg::R0, + Reg::R1, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .map_err(synth_core::Error::synthesis)? + } else { + vec![ + ArmOp::Subs { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }, + ArmOp::Sbc { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Reg(Reg::R3), + }, + ] + } } // i64 bitwise: operate on each half independently I64And => { - vec![ - ArmOp::And { - rd: Reg::R0, - rn: Reg::R0, - op2: Operand2::Reg(Reg::R2), - }, - ArmOp::And { - rd: Reg::R1, - rn: Reg::R1, - op2: Operand2::Reg(Reg::R3), - }, - ] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_and( + Reg::R0, + Reg::R1, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .map_err(synth_core::Error::synthesis)? + } else { + vec![ + ArmOp::And { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }, + ArmOp::And { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Reg(Reg::R3), + }, + ] + } } I64Or => { - vec![ - ArmOp::Orr { - rd: Reg::R0, - rn: Reg::R0, - op2: Operand2::Reg(Reg::R2), - }, - ArmOp::Orr { - rd: Reg::R1, - rn: Reg::R1, - op2: Operand2::Reg(Reg::R3), - }, - ] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_or( + Reg::R0, + Reg::R1, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .map_err(synth_core::Error::synthesis)? + } else { + vec![ + ArmOp::Orr { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }, + ArmOp::Orr { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Reg(Reg::R3), + }, + ] + } } I64Xor => { - vec![ - ArmOp::Eor { - rd: Reg::R0, - rn: Reg::R0, - op2: Operand2::Reg(Reg::R2), - }, - ArmOp::Eor { - rd: Reg::R1, - rn: Reg::R1, - op2: Operand2::Reg(Reg::R3), - }, - ] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_xor( + Reg::R0, + Reg::R1, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .map_err(synth_core::Error::synthesis)? + } else { + vec![ + ArmOp::Eor { + rd: Reg::R0, + rn: Reg::R0, + op2: Operand2::Reg(Reg::R2), + }, + ArmOp::Eor { + rd: Reg::R1, + rn: Reg::R1, + op2: Operand2::Reg(Reg::R3), + }, + ] + } } - // i64 comparisons: compare register pairs, result 0/1 in R0 + // i64 comparisons: compare register pairs, result 0/1 in R0. + // i64.eqz is increment 3's SetCondZ-shape rule (no side + // conditions — the pseudo-op reads both halves before writing). I64Eqz => { - vec![ArmOp::I64SetCondZ { - rd: Reg::R0, - rn_lo: Reg::R0, - rn_hi: Reg::R1, - }] + if self.sel_dsl { + crate::sel_dsl::generated::rule_i64_eqz(Reg::R0, Reg::R0, Reg::R1) + } else { + vec![ArmOp::I64SetCondZ { + rd: Reg::R0, + rn_lo: Reg::R0, + rn_hi: Reg::R1, + }] + } } I64Eq => { @@ -10211,27 +10283,48 @@ impl InstructionSelector { idx, )?; - // ADDS dst_lo, a_lo, b_lo (sets carry flag) - instructions.push(ArmInstruction { - op: ArmOp::Adds { - rd: dst_lo, - rn: a_lo, - op2: Operand2::Reg(b_lo), - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // VCR-SEL-001 increment 3 (#242): behind SYNTH_SEL_DSL + // (default OFF) the ADDS+ADC pair comes from the + // generated Rocq-proved rule — byte-identical to the + // hand-written emission below (mirror-pinned). The pair + // aliasing side conditions hold by construction here: + // alloc_consecutive_pair avoids every operand half and a + // consecutive pair never self-aliases. + if self.sel_dsl { + let rule_ops = crate::sel_dsl::generated::rule_i64_add( + dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, + ) + .map_err(synth_core::Error::synthesis)?; + for rule_op in rule_ops { + instructions.push(ArmInstruction { + op: rule_op, + source_line: Some(idx), + }); + cf.add_instruction(); + } + } else { + // ADDS dst_lo, a_lo, b_lo (sets carry flag) + instructions.push(ArmInstruction { + op: ArmOp::Adds { + rd: dst_lo, + rn: a_lo, + op2: Operand2::Reg(b_lo), + }, + source_line: Some(idx), + }); + cf.add_instruction(); - // ADC dst_hi, a_hi, b_hi (adds with carry) - instructions.push(ArmInstruction { - op: ArmOp::Adc { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // ADC dst_hi, a_hi, b_hi (adds with carry) + instructions.push(ArmInstruction { + op: ArmOp::Adc { + rd: dst_hi, + rn: a_hi, + op2: Operand2::Reg(b_hi), + }, + source_line: Some(idx), + }); + cf.add_instruction(); + } stack.push(StackVal::i64(dst_lo)); } @@ -10269,27 +10362,43 @@ impl InstructionSelector { idx, )?; - // SUBS dst_lo, a_lo, b_lo (sets borrow flag) - instructions.push(ArmInstruction { - op: ArmOp::Subs { - rd: dst_lo, - rn: a_lo, - op2: Operand2::Reg(b_lo), - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // VCR-SEL-001 increment 3 (#242): same delegation as + // I64Add — the SUBS+SBC pair rule, byte-identical. + if self.sel_dsl { + let rule_ops = crate::sel_dsl::generated::rule_i64_sub( + dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, + ) + .map_err(synth_core::Error::synthesis)?; + for rule_op in rule_ops { + instructions.push(ArmInstruction { + op: rule_op, + source_line: Some(idx), + }); + cf.add_instruction(); + } + } else { + // SUBS dst_lo, a_lo, b_lo (sets borrow flag) + instructions.push(ArmInstruction { + op: ArmOp::Subs { + rd: dst_lo, + rn: a_lo, + op2: Operand2::Reg(b_lo), + }, + source_line: Some(idx), + }); + cf.add_instruction(); - // SBC dst_hi, a_hi, b_hi (subtracts with borrow) - instructions.push(ArmInstruction { - op: ArmOp::Sbc { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // SBC dst_hi, a_hi, b_hi (subtracts with borrow) + instructions.push(ArmInstruction { + op: ArmOp::Sbc { + rd: dst_hi, + rn: a_hi, + op2: Operand2::Reg(b_hi), + }, + source_line: Some(idx), + }); + cf.add_instruction(); + } stack.push(StackVal::i64(dst_lo)); } @@ -10335,6 +10444,27 @@ impl InstructionSelector { &live_params, idx, )?; + // VCR-SEL-001 increment 3 (#242): behind SYNTH_SEL_DSL + // (default OFF) the per-half bitwise pair comes from the + // generated Rocq-proved rule — byte-identical to the + // hand-written emission below (mirror-pinned; side + // conditions hold by construction, see I64Add). + if self.sel_dsl { + let rule_ops = crate::sel_dsl::i64_pair_rule( + op, dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, + ) + .expect("i64 bitwise op has a pair rule") + .map_err(synth_core::Error::synthesis)?; + for rule_op in rule_ops { + instructions.push(ArmInstruction { + op: rule_op, + source_line: Some(idx), + }); + cf.add_instruction(); + } + stack.push(StackVal::i64(dst_lo)); + continue; + } let (lo_op, hi_op) = match op { I64Or => ( ArmOp::Orr { @@ -10632,15 +10762,29 @@ impl InstructionSelector { idx, )?; - instructions.push(ArmInstruction { - op: ArmOp::I64SetCondZ { - rd: dst, - rn_lo: src_lo, - rn_hi: src_hi, - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // VCR-SEL-001 increment 3 (#242): the SetCondZ-shape rule + // behind SYNTH_SEL_DSL (default OFF) — single identical + // pseudo-op, byte-identical by construction. + if self.sel_dsl { + for rule_op in crate::sel_dsl::generated::rule_i64_eqz(dst, src_lo, src_hi) + { + instructions.push(ArmInstruction { + op: rule_op, + source_line: Some(idx), + }); + cf.add_instruction(); + } + } else { + instructions.push(ArmInstruction { + op: ArmOp::I64SetCondZ { + rd: dst, + rn_lo: src_lo, + rn_hi: src_hi, + }, + source_line: Some(idx), + }); + cf.add_instruction(); + } // I64Eqz produces an i32 result (single register) stack.push(StackVal::i32(dst)); @@ -12202,7 +12346,7 @@ mod tests { } } - /// VCR-SEL-001 increments 1+2 (#242) — gate 1, the #511/#513 + /// VCR-SEL-001 increments 1+2+3 (#242) — gate 1, the #511/#513 /// mirror-pinning pattern: for every rule delegated in `select_default` /// (`Delegation::SelectDefault`/`Both`), lower its op through BOTH the /// hand-written `select_default` arm (flag OFF) and the generated @@ -12211,7 +12355,10 @@ mod tests { /// bytes, so the two must-agree implementations are pinned before the /// `SYNTH_SEL_DSL` flag can matter — the migration moves structure, /// never bytes. Uses `set_sel_dsl` (not the env var) so parallel tests - /// never race on the process environment. + /// never race on the process environment. Since increment 3 this loop + /// also pins the six i64 pair rules: `select_default`'s fixed + /// `R0:R1 op= R2:R3` arms are in-place instances of the pair rules + /// (the single-op probe is exactly that shape). /// /// Comparison rules (`Delegation::SelectWithStack`) are NOT probed here: /// `select_default`'s comparison arms are a blind bare-`Cmp` lowering @@ -12257,8 +12404,9 @@ mod tests { rule.name ); } - // Non-vacuity: increment 1's seven + increment 2's four shifts. - assert_eq!(probed, 11, "unexpected select_default-delegated rule count"); + // Non-vacuity: increment 1's seven + increment 2's four shifts + + // increment 3's six i64 pair-family rules. + assert_eq!(probed, 17, "unexpected select_default-delegated rule count"); } /// VCR-SEL-001 increment 2 (#242) — gate 1 for the rules delegated in @@ -12281,6 +12429,12 @@ mod tests { if rule.delegation == Delegation::SelectDefault { continue; } + // The i64 pair rules (increment 3) need i64-typed probes and a + // pair-shaped emission window — pinned by the dedicated + // `sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242`. + if rule.name.starts_with("rule_i64_") { + continue; + } probed += 1; let ops = vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), rule.op.clone()]; @@ -12376,6 +12530,181 @@ mod tests { ); } + /// VCR-SEL-001 increment 3 (#242) — gate 1 for the i64 pair-family rules + /// in `select_with_stack` (all `Delegation::Both`; their `select_default` + /// half is pinned by the loop above). Each binary rule is probed with + /// `i64.const; i64.const; ` so the selector allocates real register + /// pairs; `i64.eqz` with a single constant. OFF vs ON full-sequence + /// equality, plus the RMW-vacuity-proof window check: extract the SIX + /// registers the hand-written arm chose from the OFF sequence and assert + /// the emission window equals the generated rule's output for exactly + /// those registers — proving the delegation fired and satisfied the pair + /// aliasing side conditions with the selector's own assignment. + #[test] + fn sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242() { + use synth_core::WasmOp; + let mut probed = 0; + for rule in crate::sel_dsl::RULES { + if !rule.name.starts_with("rule_i64_") { + continue; + } + probed += 1; + let ops = if matches!(rule.op, WasmOp::I64Eqz) { + vec![WasmOp::I64Const(0x1_0000_0005), rule.op.clone()] + } else { + vec![ + WasmOp::I64Const(0x1_0000_0005), + WasmOp::I64Const(0x2_0000_0007), + rule.op.clone(), + ] + }; + + let mut handwritten = InstructionSelector::new(vec![]); + handwritten.set_sel_dsl(false); + let baseline: Vec = handwritten + .select_with_stack(&ops, 0) + .unwrap_or_else(|e| panic!("{}: hand-written arm failed: {e}", rule.name)) + .into_iter() + .map(|i| i.op) + .collect(); + + let mut dsl = InstructionSelector::new(vec![]); + dsl.set_sel_dsl(true); + let generated: Vec = dsl + .select_with_stack(&ops, 0) + .unwrap_or_else(|e| panic!("{}: generated rule failed: {e}", rule.name)) + .into_iter() + .map(|i| i.op) + .collect(); + + assert_eq!( + baseline, generated, + "{}: SYNTH_SEL_DSL=1 diverges from the hand-written \ + select_with_stack arm — the migration moves structure, never bytes", + rule.name + ); + + // Non-vacuity: locate the hand-written emission window, extract + // the registers the selector chose, and check the window equals + // the rule's own output for them. + let (window, rule_ops) = if matches!(rule.op, WasmOp::I64Eqz) { + let i = baseline + .iter() + .position(|o| matches!(o, ArmOp::I64SetCondZ { .. })) + .unwrap_or_else(|| panic!("{}: no I64SetCondZ in probe output", rule.name)); + let (rd, rn_lo, rn_hi) = match &baseline[i] { + ArmOp::I64SetCondZ { rd, rn_lo, rn_hi } => (*rd, *rn_lo, *rn_hi), + _ => unreachable!(), + }; + ( + baseline[i..i + 1].to_vec(), + crate::sel_dsl::generated::rule_i64_eqz(rd, rn_lo, rn_hi), + ) + } else { + // The pair window is the two-instruction sequence starting at + // the first lo-half data-processing op (the probe's constant + // materializations are I64Const pseudo-ops, never Adds/Subs/ + // And/Orr/Eor, so the first match is the rule window). + let i = baseline + .iter() + .position(|o| { + matches!( + o, + ArmOp::Adds { .. } + | ArmOp::Subs { .. } + | ArmOp::And { .. } + | ArmOp::Orr { .. } + | ArmOp::Eor { .. } + ) + }) + .unwrap_or_else(|| panic!("{}: no pair lo-half op in probe output", rule.name)); + assert!( + baseline.len() >= i + 2, + "{}: probe output too short for a pair window", + rule.name + ); + let (rd_lo, rn_lo, rm_lo) = match &baseline[i] { + ArmOp::Adds { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Subs { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::And { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Orr { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Eor { + rd, + rn, + op2: Operand2::Reg(rm), + } => (*rd, *rn, *rm), + other => panic!("{}: unexpected lo-half op {other:?}", rule.name), + }; + let (rd_hi, rn_hi, rm_hi) = match &baseline[i + 1] { + ArmOp::Adc { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Sbc { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::And { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Orr { + rd, + rn, + op2: Operand2::Reg(rm), + } + | ArmOp::Eor { + rd, + rn, + op2: Operand2::Reg(rm), + } => (*rd, *rn, *rm), + other => panic!("{}: unexpected hi-half op {other:?}", rule.name), + }; + ( + baseline[i..i + 2].to_vec(), + crate::sel_dsl::i64_pair_rule( + &rule.op, rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi, + ) + .unwrap_or_else(|| panic!("{}: pair dispatch missing", rule.name)) + .unwrap_or_else(|e| { + panic!( + "{}: selector-chosen registers violate a pair side \ + condition: {e}", + rule.name + ) + }), + ) + }; + assert_eq!( + window, rule_ops, + "{}: the hand-written emission window does not equal the \ + generated rule's output for the same registers", + rule.name + ); + } + // Five binary pair rules + i64.eqz. + assert_eq!(probed, 6, "unexpected i64 pair rule count"); + } + /// VCR-SEL-001 increment 2 (#242): the #258 imm-fold comparison peephole /// (`cmp a, #C` / `cmn a, #-C`) is OUTSIDE the reg-reg rule's shape — the /// delegation must skip it and stay byte-identical with the flag ON. diff --git a/crates/synth-synthesis/src/sel_dsl/generated.rs b/crates/synth-synthesis/src/sel_dsl/generated.rs index 0e4560f5..7ec9a709 100644 --- a/crates/synth-synthesis/src/sel_dsl/generated.rs +++ b/crates/synth-synthesis/src/sel_dsl/generated.rs @@ -1,17 +1,18 @@ //! GENERATED FILE — DO NOT EDIT BY HAND. //! //! Emitted by `crate::sel_dsl::generate_lowering_source()` from the declarative -//! rule table [`crate::sel_dsl::RULES`] (VCR-SEL-001 increments 1+2, #242, +//! rule table [`crate::sel_dsl::RULES`] (VCR-SEL-001 increments 1+2+3, #242, //! `docs/design/vcr-sel-001-first-increment.md` + -//! `docs/design/vcr-sel-001-increment-2.md`). Pinned up-to-date by the +//! `docs/design/vcr-sel-001-increment-2.md` + +//! `docs/design/vcr-sel-001-increment-3.md`). Pinned up-to-date by the //! `generated_lowering_is_up_to_date` test; regenerate with //! `SYNTH_SEL_DSL_REGEN=1 cargo test -p synth-synthesis sel_dsl`. //! //! Every function here carries a 1:1 Rocq T1 theorem in //! `coq/Synth/Synth/VcrSelRules.v` (all Qed — coverage-gated by //! `//coq:vcr_sel_rules_coverage`): the emitted sequence computes the op's -//! result in `rd` for EVERY register assignment satisfying the stated side -//! conditions. +//! result in `rd` (both words of the pair for the i64 pair rules) for EVERY +//! register assignment satisfying the stated side conditions. use crate::rules::{ArmOp, Condition, Operand2, Reg}; @@ -85,7 +86,7 @@ pub fn rule_i32_xor(rd: Reg, rn: Reg, rm: Reg) -> Vec { /// violation is a loud `Err`, never a silent misassemble). pub fn rule_i32_rotl(rd: Reg, rn: Reg, rm: Reg, rs: Reg) -> Result, &'static str> { if rs == rn { - return Err("rule_i32_rotl: side condition violated: scratch rs must not alias rn"); + return Err("rule_i32_rotl: side condition violated: rs must not alias rn"); } Ok(vec![ ArmOp::Rsb { @@ -284,3 +285,225 @@ pub fn rule_i32_ge_u(rd: Reg, rn: Reg, rm: Reg) -> Vec { }, ] } + +/// `i64.add`: (rd_hi:rd_lo) = (rn_hi:rn_lo) + (rm_hi:rm_lo), carry via ADDS+ADC +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_add_correct` (Qed). +/// +/// Side condition: `rd_hi` must not alias `rd_lo` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rn_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rm_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +pub fn rule_i64_add( + rd_lo: Reg, + rd_hi: Reg, + rn_lo: Reg, + rn_hi: Reg, + rm_lo: Reg, + rm_hi: Reg, +) -> Result, &'static str> { + if rd_hi == rd_lo { + return Err("rule_i64_add: side condition violated: rd_hi must not alias rd_lo"); + } + if rd_lo == rn_hi { + return Err("rule_i64_add: side condition violated: rd_lo must not alias rn_hi"); + } + if rd_lo == rm_hi { + return Err("rule_i64_add: side condition violated: rd_lo must not alias rm_hi"); + } + Ok(vec![ + ArmOp::Adds { + rd: rd_lo, + rn: rn_lo, + op2: Operand2::Reg(rm_lo), + }, + ArmOp::Adc { + rd: rd_hi, + rn: rn_hi, + op2: Operand2::Reg(rm_hi), + }, + ]) +} + +/// `i64.sub`: (rd_hi:rd_lo) = (rn_hi:rn_lo) - (rm_hi:rm_lo), borrow via SUBS+SBC +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_sub_correct` (Qed). +/// +/// Side condition: `rd_hi` must not alias `rd_lo` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rn_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rm_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +pub fn rule_i64_sub( + rd_lo: Reg, + rd_hi: Reg, + rn_lo: Reg, + rn_hi: Reg, + rm_lo: Reg, + rm_hi: Reg, +) -> Result, &'static str> { + if rd_hi == rd_lo { + return Err("rule_i64_sub: side condition violated: rd_hi must not alias rd_lo"); + } + if rd_lo == rn_hi { + return Err("rule_i64_sub: side condition violated: rd_lo must not alias rn_hi"); + } + if rd_lo == rm_hi { + return Err("rule_i64_sub: side condition violated: rd_lo must not alias rm_hi"); + } + Ok(vec![ + ArmOp::Subs { + rd: rd_lo, + rn: rn_lo, + op2: Operand2::Reg(rm_lo), + }, + ArmOp::Sbc { + rd: rd_hi, + rn: rn_hi, + op2: Operand2::Reg(rm_hi), + }, + ]) +} + +/// `i64.and`: (rd_hi:rd_lo) = (rn_hi:rn_lo) & (rm_hi:rm_lo), per-half AND +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_and_correct` (Qed). +/// +/// Side condition: `rd_hi` must not alias `rd_lo` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rn_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rm_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +pub fn rule_i64_and( + rd_lo: Reg, + rd_hi: Reg, + rn_lo: Reg, + rn_hi: Reg, + rm_lo: Reg, + rm_hi: Reg, +) -> Result, &'static str> { + if rd_hi == rd_lo { + return Err("rule_i64_and: side condition violated: rd_hi must not alias rd_lo"); + } + if rd_lo == rn_hi { + return Err("rule_i64_and: side condition violated: rd_lo must not alias rn_hi"); + } + if rd_lo == rm_hi { + return Err("rule_i64_and: side condition violated: rd_lo must not alias rm_hi"); + } + Ok(vec![ + ArmOp::And { + rd: rd_lo, + rn: rn_lo, + op2: Operand2::Reg(rm_lo), + }, + ArmOp::And { + rd: rd_hi, + rn: rn_hi, + op2: Operand2::Reg(rm_hi), + }, + ]) +} + +/// `i64.or`: (rd_hi:rd_lo) = (rn_hi:rn_lo) | (rm_hi:rm_lo), per-half ORR +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_or_correct` (Qed). +/// +/// Side condition: `rd_hi` must not alias `rd_lo` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rn_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rm_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +pub fn rule_i64_or( + rd_lo: Reg, + rd_hi: Reg, + rn_lo: Reg, + rn_hi: Reg, + rm_lo: Reg, + rm_hi: Reg, +) -> Result, &'static str> { + if rd_hi == rd_lo { + return Err("rule_i64_or: side condition violated: rd_hi must not alias rd_lo"); + } + if rd_lo == rn_hi { + return Err("rule_i64_or: side condition violated: rd_lo must not alias rn_hi"); + } + if rd_lo == rm_hi { + return Err("rule_i64_or: side condition violated: rd_lo must not alias rm_hi"); + } + Ok(vec![ + ArmOp::Orr { + rd: rd_lo, + rn: rn_lo, + op2: Operand2::Reg(rm_lo), + }, + ArmOp::Orr { + rd: rd_hi, + rn: rn_hi, + op2: Operand2::Reg(rm_hi), + }, + ]) +} + +/// `i64.xor`: (rd_hi:rd_lo) = (rn_hi:rn_lo) ^ (rm_hi:rm_lo), per-half EOR +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_xor_correct` (Qed). +/// +/// Side condition: `rd_hi` must not alias `rd_lo` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rn_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +/// +/// Side condition: `rd_lo` must not alias `rm_hi` (hypothesis of the theorem; +/// violation is a loud `Err`, never a silent misassemble). +pub fn rule_i64_xor( + rd_lo: Reg, + rd_hi: Reg, + rn_lo: Reg, + rn_hi: Reg, + rm_lo: Reg, + rm_hi: Reg, +) -> Result, &'static str> { + if rd_hi == rd_lo { + return Err("rule_i64_xor: side condition violated: rd_hi must not alias rd_lo"); + } + if rd_lo == rn_hi { + return Err("rule_i64_xor: side condition violated: rd_lo must not alias rn_hi"); + } + if rd_lo == rm_hi { + return Err("rule_i64_xor: side condition violated: rd_lo must not alias rm_hi"); + } + Ok(vec![ + ArmOp::Eor { + rd: rd_lo, + rn: rn_lo, + op2: Operand2::Reg(rm_lo), + }, + ArmOp::Eor { + rd: rd_hi, + rn: rn_hi, + op2: Operand2::Reg(rm_hi), + }, + ]) +} + +/// `i64.eqz`: rd = if (rn_hi:rn_lo) == 0 {1} else {0} +/// +/// Rocq obligation: `Synth.Synth.VcrSelRules.rule_i64_eqz_correct` (Qed). +pub fn rule_i64_eqz(rd: Reg, rn_lo: Reg, rn_hi: Reg) -> Vec { + vec![ArmOp::I64SetCondZ { rd, rn_lo, rn_hi }] +} diff --git a/crates/synth-synthesis/src/sel_dsl/mod.rs b/crates/synth-synthesis/src/sel_dsl/mod.rs index 8fdf0295..552485ed 100644 --- a/crates/synth-synthesis/src/sel_dsl/mod.rs +++ b/crates/synth-synthesis/src/sel_dsl/mod.rs @@ -1,7 +1,8 @@ -//! VCR-SEL-001 increments 1+2 (#242) — the Rocq-discharged selector rule DSL. +//! VCR-SEL-001 increments 1+2+3 (#242) — the Rocq-discharged selector rule DSL. //! -//! Scope: `docs/design/vcr-sel-001-first-increment.md` (increment 1) and -//! `docs/design/vcr-sel-001-increment-2.md` (increment 2). This module is the +//! Scope: `docs/design/vcr-sel-001-first-increment.md` (increment 1), +//! `docs/design/vcr-sel-001-increment-2.md` (increment 2) and +//! `docs/design/vcr-sel-001-increment-3.md` (increment 3). This module is the //! **checked-in rule table**: a declarative `op → parameterized ARM sequence` //! (registers as variables, side conditions explicit) for: //! @@ -14,7 +15,16 @@ //! i32 comparisons (`eq/ne/lt_s/lt_u/gt_s/gt_u/le_s/le_u/ge_s/ge_u`, the //! CMP+SetCond shape — no side conditions either: the flags transfer through //! NZCV, not a register, so every rd/rn/rm aliasing is admitted by the -//! universal quantifier). +//! universal quantifier); +//! - increment 3: the i64 register-pair family — `i64.add/sub/and/or/xor` +//! (the two-instruction pair shapes ADDS+ADC / SUBS+SBC / AND×2 / ORR×2 / +//! EOR×2, an i64 value living in a (lo, hi) register pair) plus `i64.eqz` +//! (the single-instruction `I64SetCondZ` shape). The pair shapes carry +//! THREE explicit aliasing side conditions each — the low-half instruction +//! writes `rd_lo` before the high-half instruction reads `rn_hi`/`rm_hi`, +//! so a rule format that could not state "the destination must not be +//! clobbered before use" is exactly how #632-class bugs happen. Each pair +//! theorem proves BOTH result words. //! //! The table is turned into plain Rust lowering functions by //! [`generate_lowering_source`] and the output is **committed to the tree** at @@ -53,6 +63,18 @@ pub enum RegVar { Rm, /// Scratch register (tier-B shapes only). Rs, + /// Destination pair, low word (i64 pair rules). + RdLo, + /// Destination pair, high word (i64 pair rules). + RdHi, + /// First operand pair, low word (i64 pair rules). + RnLo, + /// First operand pair, high word (i64 pair rules). + RnHi, + /// Second operand pair, low word (i64 pair rules). + RmLo, + /// Second operand pair, high word (i64 pair rules). + RmHi, } impl RegVar { @@ -64,6 +86,12 @@ impl RegVar { RegVar::Rn => "rn", RegVar::Rm => "rm", RegVar::Rs => "rs", + RegVar::RdLo => "rd_lo", + RegVar::RdHi => "rd_hi", + RegVar::RnLo => "rn_lo", + RegVar::RnHi => "rn_hi", + RegVar::RmLo => "rm_lo", + RegVar::RmHi => "rm_hi", } } } @@ -181,6 +209,20 @@ pub enum TemplateOp { CmpReg { rn: RegVar, rm: RegVar }, /// `ArmOp::SetCond { rd, cond }` — rd = if cond over current NZCV {1} else {0} SetCond { rd: RegVar, cond: CondCode }, + /// `ArmOp::Adds { rd, rn, op2: Reg(rm) }` — ADD setting flags (C = carry-out) + AddsReg { rd: RegVar, rn: RegVar, rm: RegVar }, + /// `ArmOp::Adc { rd, rn, op2: Reg(rm) }` — ADD with carry-in from C + AdcReg { rd: RegVar, rn: RegVar, rm: RegVar }, + /// `ArmOp::Subs { rd, rn, op2: Reg(rm) }` — SUB setting flags (C = no-borrow) + SubsReg { rd: RegVar, rn: RegVar, rm: RegVar }, + /// `ArmOp::Sbc { rd, rn, op2: Reg(rm) }` — SUB with borrow-in from NOT(C) + SbcReg { rd: RegVar, rn: RegVar, rm: RegVar }, + /// `ArmOp::I64SetCondZ { rd, rn_lo, rn_hi }` — rd = if (rn_hi:rn_lo) == 0 {1} else {0} + I64SetCondZ { + rd: RegVar, + rn_lo: RegVar, + rn_hi: RegVar, + }, } /// One declarative lowering rule: `op → parameterized ARM sequence`. @@ -213,7 +255,33 @@ impl SelRule { } } -use RegVar::{Rd, Rm, Rn, Rs}; +use RegVar::{Rd, RdHi, RdLo, Rm, RmHi, RmLo, Rn, RnHi, RnLo, Rs}; + +/// The three aliasing side conditions every two-instruction i64 pair rule +/// carries (increment 3 — the #632 lesson made explicit): the low-half +/// instruction writes `rd_lo` BEFORE the high-half instruction reads +/// `rn_hi`/`rm_hi` and writes `rd_hi`, so +/// +/// - `rd_hi` must not alias `rd_lo` (the high write would destroy the low +/// result word), +/// - `rd_lo` must not alias `rn_hi` (the low write would clobber operand 1's +/// high half before it is read), +/// - `rd_lo` must not alias `rm_hi` (same for operand 2). +/// +/// In-place lowering (`rd_lo = rn_lo`, `rd_hi = rn_hi` — `select_default`'s +/// fixed `R0:R1 += R2:R3` shape) satisfies all three; so does +/// `select_with_stack`'s `alloc_consecutive_pair` destination (avoids every +/// operand half, and a consecutive pair is never self-aliased). Each is a +/// hypothesis of the paired Rocq theorem and a runtime `Err` in the generated +/// lowering. +const I64_PAIR_SIDE_CONDITIONS: &[SideCondition] = &[ + SideCondition::NotAlias(RdHi, RdLo), + SideCondition::NotAlias(RdLo, RnHi), + SideCondition::NotAlias(RdLo, RmHi), +]; + +/// The parameter order shared by every binary i64 pair rule. +const I64_PAIR_PARAMS: &[RegVar] = &[RdLo, RdHi, RnLo, RnHi, RmLo, RmHi]; /// The increment-1 rule table: the tier-A six + tier-B `i32.rotl`. /// @@ -529,6 +597,132 @@ pub const RULES: &[SelRule] = &[ delegation: Delegation::SelectWithStack, doc: "`i32.ge_u`: rd = if rn >= rm (unsigned) {1} else {0}", }, + // ---- increment 3: the i64 register-pair family. An i64 value lives in + // a (lo, hi) register pair; each binary rule is parameterized over SIX + // registers and emits the two-instruction pair shape. All carry the + // three explicit aliasing side conditions (I64_PAIR_SIDE_CONDITIONS) — + // the low-half instruction writes rd_lo before the high-half + // instruction reads rn_hi/rm_hi. Delegated in BOTH selectors: + // select_default's fixed R0:R1 += R2:R3 arms and select_with_stack's + // allocated-pair arms are instances of the same rule (both satisfy the + // side conditions — see I64_PAIR_SIDE_CONDITIONS). ---- + SelRule { + name: "rule_i64_add", + op: WasmOp::I64Add, + params: I64_PAIR_PARAMS, + side_conditions: I64_PAIR_SIDE_CONDITIONS, + seq: &[ + TemplateOp::AddsReg { + rd: RdLo, + rn: RnLo, + rm: RmLo, + }, + TemplateOp::AdcReg { + rd: RdHi, + rn: RnHi, + rm: RmHi, + }, + ], + delegation: Delegation::Both, + doc: "`i64.add`: (rd_hi:rd_lo) = (rn_hi:rn_lo) + (rm_hi:rm_lo), carry via ADDS+ADC", + }, + SelRule { + name: "rule_i64_sub", + op: WasmOp::I64Sub, + params: I64_PAIR_PARAMS, + side_conditions: I64_PAIR_SIDE_CONDITIONS, + seq: &[ + TemplateOp::SubsReg { + rd: RdLo, + rn: RnLo, + rm: RmLo, + }, + TemplateOp::SbcReg { + rd: RdHi, + rn: RnHi, + rm: RmHi, + }, + ], + delegation: Delegation::Both, + doc: "`i64.sub`: (rd_hi:rd_lo) = (rn_hi:rn_lo) - (rm_hi:rm_lo), borrow via SUBS+SBC", + }, + SelRule { + name: "rule_i64_and", + op: WasmOp::I64And, + params: I64_PAIR_PARAMS, + side_conditions: I64_PAIR_SIDE_CONDITIONS, + seq: &[ + TemplateOp::AndReg { + rd: RdLo, + rn: RnLo, + rm: RmLo, + }, + TemplateOp::AndReg { + rd: RdHi, + rn: RnHi, + rm: RmHi, + }, + ], + delegation: Delegation::Both, + doc: "`i64.and`: (rd_hi:rd_lo) = (rn_hi:rn_lo) & (rm_hi:rm_lo), per-half AND", + }, + SelRule { + name: "rule_i64_or", + op: WasmOp::I64Or, + params: I64_PAIR_PARAMS, + side_conditions: I64_PAIR_SIDE_CONDITIONS, + seq: &[ + TemplateOp::OrrReg { + rd: RdLo, + rn: RnLo, + rm: RmLo, + }, + TemplateOp::OrrReg { + rd: RdHi, + rn: RnHi, + rm: RmHi, + }, + ], + delegation: Delegation::Both, + doc: "`i64.or`: (rd_hi:rd_lo) = (rn_hi:rn_lo) | (rm_hi:rm_lo), per-half ORR", + }, + SelRule { + name: "rule_i64_xor", + op: WasmOp::I64Xor, + params: I64_PAIR_PARAMS, + side_conditions: I64_PAIR_SIDE_CONDITIONS, + seq: &[ + TemplateOp::EorReg { + rd: RdLo, + rn: RnLo, + rm: RmLo, + }, + TemplateOp::EorReg { + rd: RdHi, + rn: RnHi, + rm: RmHi, + }, + ], + delegation: Delegation::Both, + doc: "`i64.xor`: (rd_hi:rd_lo) = (rn_hi:rn_lo) ^ (rm_hi:rm_lo), per-half EOR", + }, + // i64.eqz — the SetCondZ shape: single pseudo-op, reads both operand + // halves before writing the single i32 result register, so NO side + // conditions (every rd/rn_lo/rn_hi aliasing is admitted by the + // universal quantifier in rule_i64_eqz_correct). + SelRule { + name: "rule_i64_eqz", + op: WasmOp::I64Eqz, + params: &[Rd, RnLo, RnHi], + side_conditions: &[], + seq: &[TemplateOp::I64SetCondZ { + rd: Rd, + rn_lo: RnLo, + rn_hi: RnHi, + }], + delegation: Delegation::Both, + doc: "`i64.eqz`: rd = if (rn_hi:rn_lo) == 0 {1} else {0}", + }, ]; /// Dispatch an i32 comparison op to its generated Rocq-proved rule @@ -573,6 +767,31 @@ pub fn i32_shift_rule( }) } +/// Dispatch a binary i64 pair-family op (`add/sub/and/or/xor`) to its +/// generated Rocq-proved rule (increment 3). `None` for ops outside the +/// family (the caller's hand-written arm keeps ownership); `Some(Err(_))` +/// when the register assignment violates a pair aliasing side condition — +/// a loud error, never a silent misassemble. +#[allow(clippy::too_many_arguments)] +pub fn i64_pair_rule( + op: &WasmOp, + rd_lo: crate::rules::Reg, + rd_hi: crate::rules::Reg, + rn_lo: crate::rules::Reg, + rn_hi: crate::rules::Reg, + rm_lo: crate::rules::Reg, + rm_hi: crate::rules::Reg, +) -> Option, &'static str>> { + Some(match op { + WasmOp::I64Add => generated::rule_i64_add(rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi), + WasmOp::I64Sub => generated::rule_i64_sub(rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi), + WasmOp::I64And => generated::rule_i64_and(rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi), + WasmOp::I64Or => generated::rule_i64_or(rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi), + WasmOp::I64Xor => generated::rule_i64_xor(rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi), + _ => return None, + }) +} + /// Render a struct field, using field-init shorthand when the bound variable /// name matches the field name (keeps the generated file rustfmt/clippy-clean). fn field(name: &str, var: RegVar) -> String { @@ -609,6 +828,16 @@ fn template_expr(t: &TemplateOp, indent: usize) -> String { TemplateOp::AndReg { rd, rn, rm } => dp_reg_expr("And", rd, rn, rm, indent), TemplateOp::OrrReg { rd, rn, rm } => dp_reg_expr("Orr", rd, rn, rm, indent), TemplateOp::EorReg { rd, rn, rm } => dp_reg_expr("Eor", rd, rn, rm, indent), + TemplateOp::AddsReg { rd, rn, rm } => dp_reg_expr("Adds", rd, rn, rm, indent), + TemplateOp::AdcReg { rd, rn, rm } => dp_reg_expr("Adc", rd, rn, rm, indent), + TemplateOp::SubsReg { rd, rn, rm } => dp_reg_expr("Subs", rd, rn, rm, indent), + TemplateOp::SbcReg { rd, rn, rm } => dp_reg_expr("Sbc", rd, rn, rm, indent), + TemplateOp::I64SetCondZ { rd, rn_lo, rn_hi } => format!( + "ArmOp::I64SetCondZ {{ {}, {}, {} }}", + field("rd", rd), + field("rn_lo", rn_lo), + field("rn_hi", rn_hi) + ), TemplateOp::Mul { rd, rn, rm } => format!( "ArmOp::Mul {{ {}, {}, {} }}", field("rd", rd), @@ -680,17 +909,18 @@ pub fn generate_lowering_source() -> String { "//! GENERATED FILE — DO NOT EDIT BY HAND.\n\ //!\n\ //! Emitted by `crate::sel_dsl::generate_lowering_source()` from the declarative\n\ - //! rule table [`crate::sel_dsl::RULES`] (VCR-SEL-001 increments 1+2, #242,\n\ + //! rule table [`crate::sel_dsl::RULES`] (VCR-SEL-001 increments 1+2+3, #242,\n\ //! `docs/design/vcr-sel-001-first-increment.md` +\n\ - //! `docs/design/vcr-sel-001-increment-2.md`). Pinned up-to-date by the\n\ + //! `docs/design/vcr-sel-001-increment-2.md` +\n\ + //! `docs/design/vcr-sel-001-increment-3.md`). Pinned up-to-date by the\n\ //! `generated_lowering_is_up_to_date` test; regenerate with\n\ //! `SYNTH_SEL_DSL_REGEN=1 cargo test -p synth-synthesis sel_dsl`.\n\ //!\n\ //! Every function here carries a 1:1 Rocq T1 theorem in\n\ //! `coq/Synth/Synth/VcrSelRules.v` (all Qed — coverage-gated by\n\ //! `//coq:vcr_sel_rules_coverage`): the emitted sequence computes the op's\n\ - //! result in `rd` for EVERY register assignment satisfying the stated side\n\ - //! conditions.\n\n\ + //! result in `rd` (both words of the pair for the i64 pair rules) for EVERY\n\ + //! register assignment satisfying the stated side conditions.\n\n\ use crate::rules::{ArmOp, Condition, Operand2, Reg};\n", ); @@ -718,26 +948,34 @@ pub fn generate_lowering_source() -> String { b.rust_name() )); } - if rule.side_conditions.is_empty() { - out.push_str(&format!( - "pub fn {}({params}) -> Vec {{\n", - rule.name - )); + let ret = if rule.side_conditions.is_empty() { + "Vec" } else { + "Result, &'static str>" + }; + // Emit the signature in whichever of rustfmt's two shapes it would + // settle on (the committed file must be a rustfmt fixpoint): one line + // when it fits max_width, otherwise one parameter per line. + let one_line = format!("pub fn {}({params}) -> {ret} {{\n", rule.name); + if one_line.len() <= 101 { + // <= 100 chars + '\n' + out.push_str(&one_line); + } else { + out.push_str(&format!("pub fn {}(\n", rule.name)); + for p in rule.params { + out.push_str(&format!(" {}: Reg,\n", p.rust_name())); + } + out.push_str(&format!(") -> {ret} {{\n")); + } + for sc in rule.side_conditions { + let SideCondition::NotAlias(a, b) = sc; out.push_str(&format!( - "pub fn {}({params}) -> Result, &'static str> {{\n", - rule.name + " if {a} == {b} {{\n return Err(\"{name}: side condition violated: \ + {a} must not alias {b}\");\n }}\n", + a = a.rust_name(), + b = b.rust_name(), + name = rule.name )); - for sc in rule.side_conditions { - let SideCondition::NotAlias(a, b) = sc; - out.push_str(&format!( - " if {a} == {b} {{\n return Err(\"{name}: side condition violated: \ - scratch {a} must not alias {b}\");\n }}\n", - a = a.rust_name(), - b = b.rust_name(), - name = rule.name - )); - } } let (open, close) = if rule.side_conditions.is_empty() { ("vec![", "]") @@ -863,4 +1101,54 @@ mod tests { let ops = generated::rule_i32_rotl(Reg::R0, Reg::R1, Reg::R2, Reg::R3).unwrap(); assert_eq!(ops.len(), 2); } + + /// Increment 3: every i64 pair rule enforces all three aliasing side + /// conditions as a loud Err (the #632 lesson: the rule format must be + /// able to state "the destination must not be clobbered before use" — + /// and the generated lowering must refuse an assignment that violates + /// it, never silently misassemble). + #[test] + fn i64_pair_side_conditions_are_enforced() { + use crate::rules::Reg; + use synth_core::WasmOp; + for op in [ + WasmOp::I64Add, + WasmOp::I64Sub, + WasmOp::I64And, + WasmOp::I64Or, + WasmOp::I64Xor, + ] { + // rd_hi aliases rd_lo: the high write destroys the low result. + assert!( + i64_pair_rule(&op, Reg::R0, Reg::R0, Reg::R1, Reg::R2, Reg::R3, Reg::R4) + .unwrap() + .is_err(), + "{op:?}: rd_hi == rd_lo must be rejected" + ); + // rd_lo aliases rn_hi: the low write clobbers operand 1's high + // half before the second instruction reads it. + assert!( + i64_pair_rule(&op, Reg::R2, Reg::R3, Reg::R1, Reg::R2, Reg::R4, Reg::R5) + .unwrap() + .is_err(), + "{op:?}: rd_lo == rn_hi must be rejected" + ); + // rd_lo aliases rm_hi: same for operand 2. + assert!( + i64_pair_rule(&op, Reg::R5, Reg::R6, Reg::R1, Reg::R2, Reg::R4, Reg::R5) + .unwrap() + .is_err(), + "{op:?}: rd_lo == rm_hi must be rejected" + ); + // The in-place shape select_default emits (R0:R1 += R2:R3) + // satisfies all three and lowers to the two-instruction pair. + let ops = i64_pair_rule(&op, Reg::R0, Reg::R1, Reg::R0, Reg::R1, Reg::R2, Reg::R3) + .unwrap() + .unwrap(); + assert_eq!(ops.len(), 2, "{op:?}: pair rule must emit two instructions"); + } + // i64.eqz has no side conditions — single-instruction shape. + let ops = generated::rule_i64_eqz(Reg::R0, Reg::R0, Reg::R1); + assert_eq!(ops.len(), 1); + } } diff --git a/docs/design/vcr-sel-001-increment-3.md b/docs/design/vcr-sel-001-increment-3.md new file mode 100644 index 00000000..c50d5438 --- /dev/null +++ b/docs/design/vcr-sel-001-increment-3.md @@ -0,0 +1,113 @@ +# VCR-SEL-001 — Increment 3 scope (the i64 register-pair family) + +Status: **implemented, flag-off** (2026-07-08). Extends the increment-1/2 DSL +(`docs/design/vcr-sel-001-first-increment.md`, +`docs/design/vcr-sel-001-increment-2.md`; PRs #623/#639) into the i64 +register-pair family. Epic #242. + +## Why this family, now + +This week's miscompile cluster (#615 A32 NOPs, #632 popcnt clobber, #633 +div_s overflow, #643 globals, #599 pair shifts) sits entirely in hand-written +i64 paths — and zero bugs landed in DSL-covered ops. The pair shapes are also +where the rule format's side-condition machinery earns its keep: the #632 +lesson is that a rule that cannot state "the result must not be clobbered +before use" is how those bugs happen. + +## Op families + +- **In:** + - `i64.add` / `i64.sub` / `i64.and` / `i64.or` / `i64.xor` — the natural + first pair rules, each a two-instruction pair (ADDS+ADC / SUBS+SBC / + AND×2 / ORR×2 / EOR×2) over SIX register variables + (`rd_lo rd_hi rn_lo rn_hi rm_lo rm_hi`); + - `i64.eqz` — the single-instruction `I64SetCondZ` shape (the "SetCondZ + shape"; it discharges directly against the `i64_setcondz_bits_spec` + axiom, no comparison tactic needed). +- **Out (increment-4 territory):** i64 mul/div/rem/shifts/rotates (pseudo-ops + or multi-instruction sequences with scratch + branches), the full i64 + comparison family (`I64SetCond` — same pseudo-op pattern as eqz, deferred + to keep this increment bounded), memory, globals. + +## Model-extension finding: none needed + +The go/no-go question — can the Rocq model express register pairs? — came +back **yes, with zero model extension**. The flat model has carried the pair +convention since v0.8.0 (`ADDS/ADC/SUBS/SBC` with real NZCV carry coupling in +`ArmSemantics.v`; value-pair correspondence via `combine_i32` / +`lo_of_i64` / `hi_of_i64`), and `CorrectnessI64.v` already proves the +fixed-register ancestors T1 at `R0:R1 op= R2:R3`. Increment 3 is exactly the +pilot's move applied to pairs: lift fixed registers to universally-quantified +ones, and turn what was `discriminate` on concrete register pairs into +explicit aliasing hypotheses. + +## The aliasing side-condition design (the #632 lesson, made structural) + +Every two-instruction pair rule writes `rd_lo` (low half) BEFORE the second +instruction reads `rn_hi`/`rm_hi` and writes `rd_hi`. Three explicit side +conditions per pair rule (`I64_PAIR_SIDE_CONDITIONS` in `sel_dsl/mod.rs`, +hypotheses of the paired theorems, 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 + before the second instruction reads it; +3. `rd_lo ≠ rm_hi` — same for operand 2. + +Deliberately NOT required: `rd_lo = rn_lo` / `rd_hi = rn_hi` in-place reuse +(what `select_default`'s fixed `R0:R1 op= R2:R3` arms emit) and every other +aliasing — the universal quantifier admits them, so one Qed per rule covers +both selectors' assignments. `i64.eqz` carries no side conditions (the +pseudo-op reads both halves before writing `rd`). + +## Rocq obligations + +27 rules ↔ 27 Qed (7 + 14 + 6), 1:1 naming, coverage gated by +`//coq:vcr_sel_rules_coverage` against `coq/vcr_sel_rules.manifest`. The six +new theorems are **pair-result T1**: both words of the result are proven +(post-conditions on `rd_lo` AND `rd_hi`), value-level against the WASM-spec +functions (`I64.add` etc. on `combine_i32`-combined operands) — the same +honest shape as their `CorrectnessI64.v` ancestors. Discharge: + +- 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` carry/borrow lemmas + (ArmFlagLemmas.v). **No new axiom.** +- and/or/xor — `synth_i64_bitwise_pair_proof_poly`, fed by the + halves-distribute combine lemmas imported from `CorrectnessI64.v` + (not duplicated). +- eqz — direct `i64_setcondz_bits_spec` rewrite, like the clz/ctz/popcnt + ancestors. + +**0 holdouts: 6/6 attempted rules discharged.** (The kill-criterion's ≥70% +auto-discharge bar is met at 100% again.) + +## Where the delegation lands + +All six rules are `Delegation::Both`: + +- `select_default`'s fixed-register arms (in-place `R0:R1 op= R2:R3`, + `I64SetCondZ R0, R0, R1`) — in-place instances of the rules; +- `select_with_stack`'s allocated-pair arms — `alloc_consecutive_pair` + destinations avoid every operand half (its `extra_avoid` argument), so the + side conditions hold by construction; a violation would surface as a loud + `Err`, never a silent misassemble. + +## Gates (same two as increments 1–2, in order) + +1. **Mirror-pinning per op** — the select_default loop + (`sel_dsl_mirror_pin_generated_rules_match_handwritten_arms_242`, now 17 + rules) plus the dedicated pair test + (`sel_dsl_mirror_pin_i64_pair_rules_select_with_stack_242`: i64-typed + probes, OFF≡ON full-sequence equality, and the RMW-vacuity window check — + the emission window must equal the rule's output for the selector's own + six chosen registers). +2. **Frozen fixtures under the flag** — OFF ≡ baseline holds by construction + (every delegation is flag-gated); the frozen `.text` byte gate + (`frozen_codegen_bytes.rs`) stays green flag-off. + +## What remains before the SYNTH_SEL_DSL default flip + +Unchanged from increment 2: nothing byte-visible — the flip changes which +*code* serves the arms, not what they emit. The flip itself is a later PR +with the standard re-freeze ritual, one release, never bundled with a +byte-changing lever.