From 74dd59c02e2af1d11ca7c6477d1cc1f2449fe64d Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:53:38 +0200 Subject: [PATCH 01/35] =?UTF-8?q?retire(#242):=20i32.add=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Rocq-proved rule_i32_add is the shipped lowering since the default-on flip; the superseded arm is deleted. Byte-identity: 688-row corpus manifest (156 fixtures x 4 configs incl. declines) identical to origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 26 ++++++------------- 1 file changed, 8 insertions(+), 18 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 72a3844e..40334ef9 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6272,24 +6272,14 @@ impl InstructionSelector { let rm = self.regs.alloc_reg(); let instrs = match wasm_op { - // VCR-SEL-001 increment 1 (#242): the tier-A i32 ALU arms (and - // I32Rotl below) are migrated to the Rocq-proved rule table — - // behind `SYNTH_SEL_DSL` (default OFF) they delegate to - // `crate::sel_dsl::generated::rule_*`; OFF keeps the original - // hand-written body, byte-identical by construction. The two are - // mirror-pinned per op, and every `rule_*` has its 1:1 Qed theorem - // in coq/Synth/Synth/VcrSelRules.v. - I32Add => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_add(rd, rn, rm) - } else { - vec![ArmOp::Add { - rd, - rn, - op2: Operand2::Reg(rm), - }] - } - } + // VCR-SEL-001 / RQ-58-RETIRE (#242): the tier-A i32 ALU ops (and + // I32Rotl below) lower through the Rocq-proved rule table + // (`crate::sel_dsl::generated::rule_*`) as the ONLY path — the + // hand-written arms the rules superseded were byte-identical by + // construction (mirror-pinned since the flip) and are DELETED. + // Every `rule_*` has its 1:1 Qed theorem in + // coq/Synth/Synth/VcrSelRules.v. + I32Add => crate::sel_dsl::generated::rule_i32_add(rd, rn, rm), I32Sub => { if self.sel_dsl { From 506f3467ec7b3c9c377ae1f430554c0aa9395739 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:54:05 +0200 Subject: [PATCH 02/35] =?UTF-8?q?retire(#242):=20i32.sub=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Same evidence as i32.add: 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 40334ef9..58ee8848 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6281,17 +6281,7 @@ impl InstructionSelector { // coq/Synth/Synth/VcrSelRules.v. I32Add => crate::sel_dsl::generated::rule_i32_add(rd, rn, rm), - I32Sub => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_sub(rd, rn, rm) - } else { - vec![ArmOp::Sub { - rd, - rn, - op2: Operand2::Reg(rm), - }] - } - } + I32Sub => crate::sel_dsl::generated::rule_i32_sub(rd, rn, rm), I32Mul => { if self.sel_dsl { From a55c17057070e60e2b654500b7d7e3ded1a90c0c Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:54:28 +0200 Subject: [PATCH 03/35] =?UTF-8?q?retire(#242):=20i32.mul=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 58ee8848..496321af 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6283,13 +6283,7 @@ impl InstructionSelector { I32Sub => crate::sel_dsl::generated::rule_i32_sub(rd, rn, rm), - I32Mul => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_mul(rd, rn, rm) - } else { - vec![ArmOp::Mul { rd, rn, rm }] - } - } + I32Mul => crate::sel_dsl::generated::rule_i32_mul(rd, rn, rm), I32And => { if self.sel_dsl { From 7d1a2ecf51ec1ed6df7940f41fc9c15b107f2408 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:54:50 +0200 Subject: [PATCH 04/35] =?UTF-8?q?retire(#242):=20i32.and=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 496321af..b488a832 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6285,17 +6285,7 @@ impl InstructionSelector { I32Mul => crate::sel_dsl::generated::rule_i32_mul(rd, rn, rm), - I32And => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_and(rd, rn, rm) - } else { - vec![ArmOp::And { - rd, - rn, - op2: Operand2::Reg(rm), - }] - } - } + I32And => crate::sel_dsl::generated::rule_i32_and(rd, rn, rm), I32Or => { if self.sel_dsl { From 896808e76fdf4dce9f5509632d1a861d6e4e7b58 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:55:13 +0200 Subject: [PATCH 05/35] =?UTF-8?q?retire(#242):=20i32.or=20=E2=80=94=20dele?= =?UTF-8?q?te=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index b488a832..3e593a50 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6287,17 +6287,7 @@ impl InstructionSelector { I32And => crate::sel_dsl::generated::rule_i32_and(rd, rn, rm), - I32Or => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_or(rd, rn, rm) - } else { - vec![ArmOp::Orr { - rd, - rn, - op2: Operand2::Reg(rm), - }] - } - } + I32Or => crate::sel_dsl::generated::rule_i32_or(rd, rn, rm), I32Xor => { if self.sel_dsl { From b4b54678fc241138250cff12969495eaaf6517fc Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:55:36 +0200 Subject: [PATCH 06/35] =?UTF-8?q?retire(#242):=20i32.xor=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 3e593a50..cf8256a8 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6289,17 +6289,7 @@ impl InstructionSelector { I32Or => crate::sel_dsl::generated::rule_i32_or(rd, rn, rm), - I32Xor => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_xor(rd, rn, rm) - } else { - vec![ArmOp::Eor { - rd, - rn, - op2: Operand2::Reg(rm), - }] - } - } + I32Xor => crate::sel_dsl::generated::rule_i32_xor(rd, rn, rm), // Shifts: WASM pops both value (rn) and shift amount (rm) from stack. // #682: ARMv7-M register shifts use Rm[7:0] (>= 32 yields 0/sign) From fa655f2efd0e840a33fe2a8196743b3e72897e3e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:56:07 +0200 Subject: [PATCH 07/35] =?UTF-8?q?retire(#242):=20i32.shl=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The Rocq-proved rule carries the #682 mod-32 R12 mask. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 29 ++++--------------- 1 file changed, 6 insertions(+), 23 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index cf8256a8..a4c50a64 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6293,29 +6293,12 @@ impl InstructionSelector { // Shifts: WASM pops both value (rn) and shift amount (rm) from stack. // #682: ARMv7-M register shifts use Rm[7:0] (>= 32 yields 0/sign) - // while WASM requires amount mod 32 — mask into R12 first (encoder - // scratch, never allocatable per #212, so no liveness hazard; the - // same pattern the optimized path always used). Flag-on delegates - // to the Rocq-proved masked rules, byte-identical by construction. - I32Shl => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_shl(rd, rn, rm, Reg::R12) - .map_err(synth_core::Error::synthesis)? - } else { - vec![ - ArmOp::And { - rd: Reg::R12, - rn: rm, - op2: Operand2::Imm(31), - }, - ArmOp::LslReg { - rd, - rn, - rm: Reg::R12, - }, - ] - } - } + // while WASM requires amount mod 32 — the Rocq-proved masked rules + // mask into R12 first (encoder scratch, never allocatable per #212, + // so no liveness hazard; the same pattern the optimized path always + // used). + I32Shl => crate::sel_dsl::generated::rule_i32_shl(rd, rn, rm, Reg::R12) + .map_err(synth_core::Error::synthesis)?, I32ShrS => { if self.sel_dsl { crate::sel_dsl::generated::rule_i32_shr_s(rd, rn, rm, Reg::R12) From 81999ad8905b592d69c684c2a09730a0cb87fdbd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:56:32 +0200 Subject: [PATCH 08/35] =?UTF-8?q?retire(#242):=20i32.shr=5Fs=20=E2=80=94?= =?UTF-8?q?=20delete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 21 ++----------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index a4c50a64..2a96c51e 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6299,25 +6299,8 @@ impl InstructionSelector { // used). I32Shl => crate::sel_dsl::generated::rule_i32_shl(rd, rn, rm, Reg::R12) .map_err(synth_core::Error::synthesis)?, - I32ShrS => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_shr_s(rd, rn, rm, Reg::R12) - .map_err(synth_core::Error::synthesis)? - } else { - vec![ - ArmOp::And { - rd: Reg::R12, - rn: rm, - op2: Operand2::Imm(31), - }, - ArmOp::AsrReg { - rd, - rn, - rm: Reg::R12, - }, - ] - } - } + I32ShrS => crate::sel_dsl::generated::rule_i32_shr_s(rd, rn, rm, Reg::R12) + .map_err(synth_core::Error::synthesis)?, I32ShrU => { if self.sel_dsl { crate::sel_dsl::generated::rule_i32_shr_u(rd, rn, rm, Reg::R12) From 7cb009ef477d7560cce35b9e7a19583134d02fb7 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:56:57 +0200 Subject: [PATCH 09/35] =?UTF-8?q?retire(#242):=20i32.shr=5Fu=20=E2=80=94?= =?UTF-8?q?=20delete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 21 ++----------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 2a96c51e..66efb2c0 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6301,25 +6301,8 @@ impl InstructionSelector { .map_err(synth_core::Error::synthesis)?, I32ShrS => crate::sel_dsl::generated::rule_i32_shr_s(rd, rn, rm, Reg::R12) .map_err(synth_core::Error::synthesis)?, - I32ShrU => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_shr_u(rd, rn, rm, Reg::R12) - .map_err(synth_core::Error::synthesis)? - } else { - vec![ - ArmOp::And { - rd: Reg::R12, - rn: rm, - op2: Operand2::Imm(31), - }, - ArmOp::LsrReg { - rd, - rn, - rm: Reg::R12, - }, - ] - } - } + I32ShrU => crate::sel_dsl::generated::rule_i32_shr_u(rd, rn, rm, Reg::R12) + .map_err(synth_core::Error::synthesis)?, // Rotate operations: shift amount from stack register I32Rotl => { From 703033aab373f1426c01dd6f89ebf48ff368b282 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:57:24 +0200 Subject: [PATCH 10/35] =?UTF-8?q?retire(#242):=20i32.rotl=20=E2=80=94=20de?= =?UTF-8?q?lete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 23 +++++-------------- 1 file changed, 6 insertions(+), 17 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 66efb2c0..192d4ca8 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6308,24 +6308,13 @@ impl InstructionSelector { I32Rotl => { // Rotate left by N = Rotate right by (32 - N) // RSB rtmp, rm, #32; ROR rd, rn, rtmp + // Tier-B rule: carries the explicit `rs <> rn` scratch + // non-aliasing side condition (hypothesis of + // rule_i32_rotl_correct) — Ok-or-Err, never a silent + // misassemble. let rtmp = self.regs.alloc_reg(); - if self.sel_dsl { - // Tier-B rule: carries the explicit `rs <> rn` scratch - // non-aliasing side condition (hypothesis of - // rule_i32_rotl_correct) — Ok-or-Err, never a silent - // misassemble. - crate::sel_dsl::generated::rule_i32_rotl(rd, rn, rm, rtmp) - .map_err(synth_core::Error::synthesis)? - } else { - vec![ - ArmOp::Rsb { - rd: rtmp, - rn: rm, - imm: 32, - }, - ArmOp::RorReg { rd, rn, rm: rtmp }, - ] - } + crate::sel_dsl::generated::rule_i32_rotl(rd, rn, rm, rtmp) + .map_err(synth_core::Error::synthesis)? } I32Rotr => { From 5db9549767475b71507e27e092b89d41a7523ca3 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:57:48 +0200 Subject: [PATCH 11/35] =?UTF-8?q?retire(#242):=20i32.rotr=20=E2=80=94=20de?= =?UTF-8?q?lete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 8 +------- 1 file changed, 1 insertion(+), 7 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 192d4ca8..282b5a9f 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6317,13 +6317,7 @@ impl InstructionSelector { .map_err(synth_core::Error::synthesis)? } - I32Rotr => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_rotr(rd, rn, rm) - } else { - vec![ArmOp::RorReg { rd, rn, rm }] - } - } + I32Rotr => crate::sel_dsl::generated::rule_i32_rotr(rd, rn, rm), // Bit count operations — VCR-SEL-001 increment 4 (#242): behind // SYNTH_SEL_DSL (default OFF) these delegate to the Rocq-proved From 4f9567bc5a82aa7a40abee1fbdce5613afea69dd Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:58:13 +0200 Subject: [PATCH 12/35] =?UTF-8?q?retire(#242):=20i32.clz=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../synth-synthesis/src/instruction_selector.rs | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 282b5a9f..320261bd 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6319,18 +6319,10 @@ impl InstructionSelector { I32Rotr => crate::sel_dsl::generated::rule_i32_rotr(rd, rn, rm), - // Bit count operations — VCR-SEL-001 increment 4 (#242): behind - // SYNTH_SEL_DSL (default OFF) these delegate to the Rocq-proved - // rules (clz single-CLZ; ctz the two-instruction RBIT+CLZ - // scratch=dest shape; popcnt the pseudo-op), byte-identical by - // construction (mirror-pinned per op). - I32Clz => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_clz(rd, rm) - } else { - vec![ArmOp::Clz { rd, rm }] - } - } + // Bit count operations — Rocq-proved rules are the only path + // (RQ-58-RETIRE): clz single-CLZ; ctz the two-instruction RBIT+CLZ + // scratch=dest shape; popcnt the pseudo-op. + I32Clz => crate::sel_dsl::generated::rule_i32_clz(rd, rm), I32Ctz => { if self.sel_dsl { From 062af02e71d51e4617136fc9be5d83e264a915d6 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:58:36 +0200 Subject: [PATCH 13/35] =?UTF-8?q?retire(#242):=20i32.ctz=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 320261bd..2758619b 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6324,14 +6324,7 @@ impl InstructionSelector { // scratch=dest shape; popcnt the pseudo-op. I32Clz => crate::sel_dsl::generated::rule_i32_clz(rd, rm), - I32Ctz => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_ctz(rd, rm) - } else { - // Count trailing zeros: RBIT + CLZ - vec![ArmOp::Rbit { rd, rm }, ArmOp::Clz { rd, rm: rd }] - } - } + I32Ctz => crate::sel_dsl::generated::rule_i32_ctz(rd, rm), I32Popcnt => { if self.sel_dsl { From f86aa5bd76582888e92adc5aad32c1f130492ab5 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:59:00 +0200 Subject: [PATCH 14/35] =?UTF-8?q?retire(#242):=20i32.popcnt=20=E2=80=94=20?= =?UTF-8?q?delete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- crates/synth-synthesis/src/instruction_selector.rs | 11 +---------- 1 file changed, 1 insertion(+), 10 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 2758619b..8aecdbc2 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6326,16 +6326,7 @@ impl InstructionSelector { I32Ctz => crate::sel_dsl::generated::rule_i32_ctz(rd, rm), - I32Popcnt => { - if self.sel_dsl { - crate::sel_dsl::generated::rule_i32_popcnt(rd, rm) - } else { - // Population count - no native ARM instruction - // Use Popcnt pseudo-op which the encoder expands to a parallel - // bit-count algorithm (shift-and-add with masks) - vec![ArmOp::Popcnt { rd, rm }] - } - } + I32Popcnt => crate::sel_dsl::generated::rule_i32_popcnt(rd, rm), I32Const(val) => { let uval = *val as u32; From 9f615aea92fdda32c02325cf5ef23f85b0962ebf Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 05:59:42 +0200 Subject: [PATCH 15/35] =?UTF-8?q?retire(#242):=20i64.add=20=E2=80=94=20del?= =?UTF-8?q?ete=20both=20hand-written=20arms=20(default=20+=20direct)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One op, both selectors: the select_default fixed-pair arm and the select_with_stack allocated-pair arm each collapse to the Rocq-proved rule_i64_add call that has been the shipped path since the flip. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 92 +++++-------------- 1 file changed, 24 insertions(+), 68 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 8aecdbc2..2f890ba2 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6962,39 +6962,21 @@ impl InstructionSelector { }] } - // 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 => { - 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), - }, - ] - } - } + // i64 arithmetic: ADDS/ADC for add, SUBS/SBC for sub — the + // Rocq-proved pair rules are the only path (RQ-58-RETIRE). 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 => 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)?, I64Sub => { if self.sel_dsl { @@ -15957,44 +15939,18 @@ impl InstructionSelector { idx, )?; - // 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: + // The ADDS+ADC pair comes from the generated Rocq-proved + // rule — the only path (RQ-58-RETIRE). 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) + 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: ArmOp::Adc { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From d6af7027bfc81c0fea668543783992e5f695cb48 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:00:14 +0200 Subject: [PATCH 16/35] =?UTF-8?q?retire(#242):=20i64.sub=20=E2=80=94=20del?= =?UTF-8?q?ete=20both=20hand-written=20arms=20(default=20+=20direct)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 75 +++++-------------- 1 file changed, 17 insertions(+), 58 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 2f890ba2..86e16667 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6978,32 +6978,15 @@ impl InstructionSelector { ) .map_err(synth_core::Error::synthesis)?, - I64Sub => { - 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), - }, - ] - } - } + I64Sub => 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)?, // i64 bitwise: operate on each half independently I64And => { @@ -15992,39 +15975,15 @@ impl InstructionSelector { idx, )?; - // 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) + // Same as I64Add — the Rocq-proved SUBS+SBC pair rule is + // the only path (RQ-58-RETIRE). + 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: ArmOp::Sbc { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From c3e834c8125c4ee10e976551edece96f62622578 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:00:41 +0200 Subject: [PATCH 17/35] =?UTF-8?q?retire(#242):=20i64.and=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 86e16667..00ad40e9 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6989,32 +6989,15 @@ impl InstructionSelector { .map_err(synth_core::Error::synthesis)?, // i64 bitwise: operate on each half independently - I64And => { - 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), - }, - ] - } - } + I64And => 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)?, I64Or => { if self.sel_dsl { From 091e1ef13a926b465034faa1d80479c909a8e154 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:01:06 +0200 Subject: [PATCH 18/35] =?UTF-8?q?retire(#242):=20i64.or=20=E2=80=94=20dele?= =?UTF-8?q?te=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 00ad40e9..67534833 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -6999,32 +6999,15 @@ impl InstructionSelector { ) .map_err(synth_core::Error::synthesis)?, - I64Or => { - 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), - }, - ] - } - } + I64Or => 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)?, I64Xor => { if self.sel_dsl { From 36874fbbefeb4f88f9156860f9285b045b34e6d8 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:01:31 +0200 Subject: [PATCH 19/35] =?UTF-8?q?retire(#242):=20i64.xor=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20select=5Fdefault=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 35 +++++-------------- 1 file changed, 9 insertions(+), 26 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 67534833..88bceaa1 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -7009,32 +7009,15 @@ impl InstructionSelector { ) .map_err(synth_core::Error::synthesis)?, - I64Xor => { - 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), - }, - ] - } - } + I64Xor => 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)?, // i64 comparisons: compare register pairs, result 0/1 in R0. // i64.eqz is increment 3's SetCondZ-shape rule (no side From 62cd76b13bd4f05bddc1f2c388c51a52f1363030 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:02:15 +0200 Subject: [PATCH 20/35] =?UTF-8?q?retire(#242):=20i64.{or,and,xor}=20?= =?UTF-8?q?=E2=80=94=20delete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves the three i64 bitwise ops via the shared i64_pair_rule dispatch, so the deletion unit is the group (its select_default counterparts were retired per-op in the three previous commits). Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 81 +++---------------- 1 file changed, 13 insertions(+), 68 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 88bceaa1..35a21015 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -15982,76 +15982,21 @@ 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 + // The per-half bitwise pair comes from the generated + // Rocq-proved rule — the only path (RQ-58-RETIRE; 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 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(); } - let (lo_op, hi_op) = match op { - I64Or => ( - ArmOp::Orr { - rd: dst_lo, - rn: a_lo, - op2: Operand2::Reg(b_lo), - }, - ArmOp::Orr { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, - ), - I64And => ( - ArmOp::And { - rd: dst_lo, - rn: a_lo, - op2: Operand2::Reg(b_lo), - }, - ArmOp::And { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, - ), - I64Xor => ( - ArmOp::Eor { - rd: dst_lo, - rn: a_lo, - op2: Operand2::Reg(b_lo), - }, - ArmOp::Eor { - rd: dst_hi, - rn: a_hi, - op2: Operand2::Reg(b_hi), - }, - ), - _ => unreachable!(), - }; - instructions.push(ArmInstruction { - op: lo_op, - source_line: Some(idx), - }); - cf.add_instruction(); - instructions.push(ArmInstruction { - op: hi_op, - source_line: Some(idx), - }); - cf.add_instruction(); stack.push(StackVal::i64(dst_lo)); } From 90e0dabf4c3c85e267ef7c7d2087f1e4103c4c61 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:02:53 +0200 Subject: [PATCH 21/35] =?UTF-8?q?retire(#242):=20i64.eqz=20=E2=80=94=20del?= =?UTF-8?q?ete=20both=20hand-written=20arms=20(default=20+=20direct)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 38 ++++--------------- 1 file changed, 7 insertions(+), 31 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 35a21015..9f0b5c9e 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -7020,19 +7020,9 @@ impl InstructionSelector { .map_err(synth_core::Error::synthesis)?, // 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 => { - 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, - }] - } - } + // i64.eqz is the SetCondZ-shape rule (no side conditions — the + // pseudo-op reads both halves before writing). + I64Eqz => crate::sel_dsl::generated::rule_i64_eqz(Reg::R0, Reg::R0, Reg::R1), // Binary i64 comparisons — VCR-SEL-001 increment 4 (#242): one // I64SetCond pseudo-op over the fixed (R0:R1, R2:R3) pairs. @@ -16349,25 +16339,11 @@ impl InstructionSelector { idx, )?; - // 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 { + // The SetCondZ-shape Rocq-proved rule is the only path + // (RQ-58-RETIRE). + for rule_op in crate::sel_dsl::generated::rule_i64_eqz(dst, src_lo, src_hi) { instructions.push(ArmInstruction { - op: ArmOp::I64SetCondZ { - rd: dst, - rn_lo: src_lo, - rn_hi: src_hi, - }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 99949af3e9ba5be099051fa78e91555c5cd698ec Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:03:40 +0200 Subject: [PATCH 22/35] =?UTF-8?q?retire(#242):=20i64=20comparisons=20x10?= =?UTF-8?q?=20=E2=80=94=20delete=20the=20hand-written=20select=5Fdefault?= =?UTF-8?q?=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped arm serves the ten binary i64 comparisons via the shared i64_setcond_rule dispatch, so the deletion unit is the group. Also removes the group's '_ => unreachable!()' condition-map wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 53 +++++-------------- 1 file changed, 12 insertions(+), 41 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 9f0b5c9e..11a0e1b6 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -7024,48 +7024,19 @@ impl InstructionSelector { // pseudo-op reads both halves before writing). I64Eqz => crate::sel_dsl::generated::rule_i64_eqz(Reg::R0, Reg::R0, Reg::R1), - // Binary i64 comparisons — VCR-SEL-001 increment 4 (#242): one - // I64SetCond pseudo-op over the fixed (R0:R1, R2:R3) pairs. - // Behind SYNTH_SEL_DSL (default OFF) the pseudo-op comes from - // the generated Rocq-proved rule (mirror-pinned per op); OFF - // keeps the hand-written emission, byte-identical by - // construction. + // Binary i64 comparisons: one I64SetCond pseudo-op over the fixed + // (R0:R1, R2:R3) pairs, from the generated Rocq-proved rule — the + // only path (RQ-58-RETIRE). I64Eq | I64Ne | I64LtS | I64LtU | I64LeS | I64LeU | I64GtS | I64GtU | I64GeS - | I64GeU => { - if self.sel_dsl { - crate::sel_dsl::i64_setcond_rule( - wasm_op, - Reg::R0, - Reg::R0, - Reg::R1, - Reg::R2, - Reg::R3, - ) - .expect("binary i64 comparison has a generated rule") - } else { - let cond = match wasm_op { - I64Eq => Condition::EQ, - I64Ne => Condition::NE, - I64LtS => Condition::LT, - I64LtU => Condition::LO, - I64LeS => Condition::LE, - I64LeU => Condition::LS, - I64GtS => Condition::GT, - I64GtU => Condition::HI, - I64GeS => Condition::GE, - I64GeU => Condition::HS, - _ => unreachable!(), - }; - vec![ArmOp::I64SetCond { - rd: Reg::R0, - rn_lo: Reg::R0, - rn_hi: Reg::R1, - rm_lo: Reg::R2, - rm_hi: Reg::R3, - cond, - }] - } - } + | I64GeU => crate::sel_dsl::i64_setcond_rule( + wasm_op, + Reg::R0, + Reg::R0, + Reg::R1, + Reg::R2, + Reg::R3, + ) + .expect("binary i64 comparison has a generated rule"), // i64 multiply: UMULL + MLA cross products I64Mul => { From 90ed348b70d68bc1f2822d26401bac8ee4d16f1f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:04:24 +0200 Subject: [PATCH 23/35] =?UTF-8?q?retire(#242):=20i64.{shl,shr=5Fu,shr=5Fs}?= =?UTF-8?q?=20=E2=80=94=20delete=20the=20hand-written=20direct-selector=20?= =?UTF-8?q?arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves the three i64 variable shifts via the shared i64_pair_bin_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 56 ++++--------------- 1 file changed, 12 insertions(+), 44 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 11a0e1b6..a3f49e99 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16079,50 +16079,18 @@ impl InstructionSelector { &live_params, idx, )?; - // VCR-ISA-001 wave-2 (v0.45): behind SYNTH_SEL_DSL the - // single i64 shift pseudo-op comes from the generated - // Rocq-proved rule — byte-identical to the hand-written - // emission below (mirror-pinned). The `rd_hi <> rd_lo` side - // condition holds by construction: alloc_consecutive_pair - // returns a distinct pair. - let shift_op = if self.sel_dsl { - crate::sel_dsl::i64_pair_bin_rule( - op, dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, - ) - .expect("i64 shift op dispatch") - .map_err(synth_core::Error::synthesis)? - .into_iter() - .next() - .expect("i64 shift rule emits one op") - } else { - match op { - I64Shl => ArmOp::I64Shl { - rd_lo: dst_lo, - rd_hi: dst_hi, - rn_lo: a_lo, - rn_hi: a_hi, - rm_lo: b_lo, - rm_hi: b_hi, - }, - I64ShrU => ArmOp::I64ShrU { - rd_lo: dst_lo, - rd_hi: dst_hi, - rn_lo: a_lo, - rn_hi: a_hi, - rm_lo: b_lo, - rm_hi: b_hi, - }, - I64ShrS => ArmOp::I64ShrS { - rd_lo: dst_lo, - rd_hi: dst_hi, - rn_lo: a_lo, - rn_hi: a_hi, - rm_lo: b_lo, - rm_hi: b_hi, - }, - _ => unreachable!(), - } - }; + // The single i64 shift pseudo-op comes from the generated + // Rocq-proved rule — the only path (RQ-58-RETIRE). The + // `rd_hi <> rd_lo` side condition holds by construction: + // alloc_consecutive_pair returns a distinct pair. + let shift_op = crate::sel_dsl::i64_pair_bin_rule( + op, dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, + ) + .expect("i64 shift op dispatch") + .map_err(synth_core::Error::synthesis)? + .into_iter() + .next() + .expect("i64 shift rule emits one op"); instructions.push(ArmInstruction { op: shift_op, source_line: Some(idx), From dd2a3e383328199fdfead5d1ace601e18ad8c8ba Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:05:15 +0200 Subject: [PATCH 24/35] =?UTF-8?q?retire(#242):=20i32=20comparisons=20x10?= =?UTF-8?q?=20=E2=80=94=20retire=20the=20flag=20conditioning=20on=20the=20?= =?UTF-8?q?direct=20selector?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit PARTIAL by design, and named as residual: this grouped arm is dual-use. The reg-reg case now takes the Rocq-proved i32_cmp_rule unconditionally; the #258 cmp/cmn imm-fold case has no DSL rule (no CmpImm-shaped rule exists), so its hand-written Cmp+SetCond fallback emission STAYS and is enumerated in the RQ-58-SPLIT residual set rather than deleted. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 19 ++++++++----------- 1 file changed, 8 insertions(+), 11 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index a3f49e99..81578da9 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16405,17 +16405,14 @@ impl InstructionSelector { I32GeU => Condition::HS, _ => unreachable!(), }; - // VCR-SEL-001 increment 2 (#242): behind SYNTH_SEL_DSL - // (default OFF) the reg-reg pair comes from the generated - // Rocq-proved rule — [Cmp {rn:a, Reg(b)}, SetCond {dst, - // cond}], byte-identical to the hand-written emission - // below (mirror-pinned per op). OFF, or on the imm-fold - // path, keeps the original hand-written body. - let dsl_ops = if self.sel_dsl { - reg_operands.and_then(|(a, b)| crate::sel_dsl::i32_cmp_rule(op, dst, a, b)) - } else { - None - }; + // The reg-reg pair comes from the generated Rocq-proved + // rule — [Cmp {rn:a, Reg(b)}, SetCond {dst, cond}] — as + // the only reg-reg path (RQ-58-RETIRE). RESIDUAL, not + // superseded: the #258 cmp/cmn IMM-FOLD case below has no + // DSL rule (no CmpImm-shaped rule exists), so its + // hand-written Cmp+SetCond emission stays. + let dsl_ops = + reg_operands.and_then(|(a, b)| crate::sel_dsl::i32_cmp_rule(op, dst, a, b)); if let Some(rule_ops) = dsl_ops { for rule_op in rule_ops { instructions.push(ArmInstruction { From bb45eb9fccb358ce07612080e404f074218c0f73 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:05:49 +0200 Subject: [PATCH 25/35] =?UTF-8?q?retire(#242):=20i32.eqz=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 40 ++++--------------- 1 file changed, 8 insertions(+), 32 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 81578da9..5180db74 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16460,39 +16460,15 @@ impl InstructionSelector { idx, )? }; - // VCR-SEL-001 (#242): behind SYNTH_SEL_DSL (default ON, - // opt out SYNTH_NO_SEL_DSL) the CMP+SetCond pair comes from - // the generated Rocq-proved rule — byte-identical to the - // hand-written emission below (mirror-pinned). Same holdout - // story as the i32 comparisons: select_with_stack owns the - // materializing lowering, so the rule is wired here only. - let dsl_ops = if self.sel_dsl { - crate::sel_dsl::i32_eqz_rule(op, dst, a) - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { - instructions.push(ArmInstruction { - op: ArmOp::Cmp { - rn: a, - op2: Operand2::Imm(0), - }, - source_line: Some(idx), - }); - cf.add_instruction(); + // The CMP+SetCond pair comes from the generated + // Rocq-proved rule — the only path (RQ-58-RETIRE). + // select_with_stack owns the materializing lowering, so + // the rule is wired here only. + let rule_ops = crate::sel_dsl::i32_eqz_rule(op, dst, a) + .expect("i32.eqz has a generated rule"); + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: ArmOp::SetCond { - rd: dst, - cond: Condition::EQ, - }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 43a29420275f12275f0bd68b9ec84cd56659fc9e Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:06:34 +0200 Subject: [PATCH 26/35] =?UTF-8?q?retire(#242):=20i32.{shl,shr=5Fs,shr=5Fu,?= =?UTF-8?q?rotr}=20=E2=80=94=20delete=20the=20hand-written=20direct-select?= =?UTF-8?q?or=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves the four register shifts/rotates via the shared i32_shift_rule dispatch; the deletion unit is the group. The generated rules carry the #682 mod-32 R12 mask themselves. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 70 +++---------------- 1 file changed, 8 insertions(+), 62 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 5180db74..fdbf2e29 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16510,70 +16510,16 @@ impl InstructionSelector { }; // #682: LSL/LSR/ASR mask the amount mod 32 through R12 // (ARM uses Rm[7:0]; WASM requires mod 32). ROR is cyclic, - // so Rm[7:0] already agrees with WASM — no mask. The mask - // is emitted in the hand-written branch below; the DSL - // branch's generated rules carry their own. - let masked_amt = if matches!(op, I32Rotr) { - shift_amt - } else { - Reg::R12 - }; - let shift_op = match op { - I32Shl => ArmOp::LslReg { - rd: dst, - rn: value, - rm: masked_amt, - }, - I32ShrU => ArmOp::LsrReg { - rd: dst, - rn: value, - rm: masked_amt, - }, - I32ShrS => ArmOp::AsrReg { - rd: dst, - rn: value, - rm: masked_amt, - }, - I32Rotr => ArmOp::RorReg { - rd: dst, - rn: value, - rm: shift_amt, - }, - _ => unreachable!(), - }; - // VCR-SEL-001 increment 2 (#242): behind SYNTH_SEL_DSL the - // single shift instruction comes from the generated - // Rocq-proved rule — the identical ArmOp, byte-identical - // by construction (mirror-pinned per op). - let dsl_ops = if self.sel_dsl { + // so Rm[7:0] already agrees with WASM — no mask. The + // generated Rocq-proved rules carry the mask themselves + // and are the only path (RQ-58-RETIRE). + let rule_ops = crate::sel_dsl::i32_shift_rule(op, dst, value, shift_amt, Reg::R12) - .map(|r| r.map_err(synth_core::Error::synthesis)) - .transpose()? - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { - if !matches!(op, I32Rotr) { - instructions.push(ArmInstruction { - op: ArmOp::And { - rd: Reg::R12, - rn: shift_amt, - op2: Operand2::Imm(31), - }, - source_line: Some(idx), - }); - cf.add_instruction(); - } + .expect("i32 shift/rotate op has a generated rule") + .map_err(synth_core::Error::synthesis)?; + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: shift_op, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 5d41ddc1be172c7687848821e0cc76ff3346c98a Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:07:10 +0200 Subject: [PATCH 27/35] =?UTF-8?q?retire(#242):=20i32.clz=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 25 +++++-------------- 1 file changed, 6 insertions(+), 19 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index fdbf2e29..ac35ea14 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16611,26 +16611,13 @@ impl InstructionSelector { idx, )? }; - // VCR-SEL-001 increment 4 (#242): behind SYNTH_SEL_DSL the - // single CLZ comes from the generated Rocq-proved rule — - // the identical ArmOp, byte-identical by construction - // (mirror-pinned per op). - let dsl_ops = if self.sel_dsl { - crate::sel_dsl::i32_unary_rule(op, dst, src) - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { + // The single CLZ comes from the generated Rocq-proved + // rule — the only path (RQ-58-RETIRE). + let rule_ops = crate::sel_dsl::i32_unary_rule(op, dst, src) + .expect("i32.clz has a generated rule"); + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: ArmOp::Clz { rd: dst, rm: src }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From e311e27eba3ae864647013273cf82270a1da2c91 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:07:38 +0200 Subject: [PATCH 28/35] =?UTF-8?q?retire(#242):=20i32.ctz=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 31 +++++-------------- 1 file changed, 7 insertions(+), 24 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index ac35ea14..a61da231 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16647,31 +16647,14 @@ impl InstructionSelector { idx, )? }; - // VCR-SEL-001 increment 4 (#242): behind SYNTH_SEL_DSL the - // two-instruction RBIT+CLZ scratch=dest shape comes from - // the generated Rocq-proved rule, byte-identical by - // construction (mirror-pinned per op). - let dsl_ops = if self.sel_dsl { - crate::sel_dsl::i32_unary_rule(op, dst, src) - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { - instructions.push(ArmInstruction { - op: ArmOp::Rbit { rd: dst, rm: src }, - source_line: Some(idx), - }); - cf.add_instruction(); + // The two-instruction RBIT+CLZ scratch=dest shape comes + // from the generated Rocq-proved rule — the only path + // (RQ-58-RETIRE). + let rule_ops = crate::sel_dsl::i32_unary_rule(op, dst, src) + .expect("i32.ctz has a generated rule"); + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: ArmOp::Clz { rd: dst, rm: dst }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 0950f6bdd3d673b7a729c2304fb4db7ace6fff21 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:08:04 +0200 Subject: [PATCH 29/35] =?UTF-8?q?retire(#242):=20i32.popcnt=20=E2=80=94=20?= =?UTF-8?q?delete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 24 +++++-------------- 1 file changed, 6 insertions(+), 18 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index a61da231..69d429f7 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16685,25 +16685,13 @@ impl InstructionSelector { idx, )? }; - // VCR-SEL-001 increment 4 (#242): pseudo-op-tier rule — - // the identical ArmOp::Popcnt, byte-identical by - // construction (mirror-pinned per op). - let dsl_ops = if self.sel_dsl { - crate::sel_dsl::i32_unary_rule(op, dst, src) - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { + // Pseudo-op-tier Rocq-proved rule (ArmOp::Popcnt) — the + // only path (RQ-58-RETIRE). + let rule_ops = crate::sel_dsl::i32_unary_rule(op, dst, src) + .expect("i32.popcnt has a generated rule"); + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: ArmOp::Popcnt { rd: dst, rm: src }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 069f9747754d35a844fc564d8a04eaa21502fa62 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:08:41 +0200 Subject: [PATCH 30/35] =?UTF-8?q?retire(#242):=20i64=20comparisons=20x10?= =?UTF-8?q?=20=E2=80=94=20delete=20the=20hand-written=20direct-selector=20?= =?UTF-8?q?arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves the ten binary i64 comparisons via the shared i64_setcond_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' condition-map wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 47 +++---------------- 1 file changed, 7 insertions(+), 40 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 69d429f7..71282a87 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16813,47 +16813,14 @@ impl InstructionSelector { idx, )? }; - let cond = match op { - I64Eq => Condition::EQ, - I64Ne => Condition::NE, - I64LtS => Condition::LT, - I64LtU => Condition::LO, - I64LeS => Condition::LE, - I64LeU => Condition::LS, - I64GtS => Condition::GT, - I64GtU => Condition::HI, - I64GeS => Condition::GE, - I64GeU => Condition::HS, - _ => unreachable!(), - }; - // VCR-SEL-001 increment 4 (#242): behind SYNTH_SEL_DSL the - // I64SetCond pseudo-op comes from the generated - // Rocq-proved rule — the identical ArmOp (same condition - // mapping), byte-identical by construction (mirror-pinned - // per op). - let dsl_ops = if self.sel_dsl { - crate::sel_dsl::i64_setcond_rule(op, dst, a_lo, a_hi, b_lo, b_hi) - } else { - None - }; - if let Some(rule_ops) = dsl_ops { - for rule_op in rule_ops { - instructions.push(ArmInstruction { - op: rule_op, - source_line: Some(idx), - }); - cf.add_instruction(); - } - } else { + // The I64SetCond pseudo-op (condition mapping included) + // comes from the generated Rocq-proved rule — the only + // path (RQ-58-RETIRE). + let rule_ops = crate::sel_dsl::i64_setcond_rule(op, dst, a_lo, a_hi, b_lo, b_hi) + .expect("binary i64 comparison has a generated rule"); + for rule_op in rule_ops { instructions.push(ArmInstruction { - op: ArmOp::I64SetCond { - rd: dst, - rn_lo: a_lo, - rn_hi: a_hi, - rm_lo: b_lo, - rm_hi: b_hi, - cond, - }, + op: rule_op, source_line: Some(idx), }); cf.add_instruction(); From 82ff232236b577868e7352ce093206f0ba46932b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:09:09 +0200 Subject: [PATCH 31/35] =?UTF-8?q?retire(#242):=20i64.mul=20=E2=80=94=20del?= =?UTF-8?q?ete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 36 +++++++------------ 1 file changed, 12 insertions(+), 24 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 71282a87..26e7c418 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -16867,30 +16867,18 @@ impl InstructionSelector { &live_params, idx, )?; - // VCR-ISA-001 wave-2 (v0.45): behind SYNTH_SEL_DSL the - // single I64Mul pseudo-op comes from the generated - // Rocq-proved rule — byte-identical to the hand-written - // emission below (mirror-pinned; `rd_hi <> rd_lo` holds by - // construction via alloc_consecutive_pair). - let mul_op = if self.sel_dsl { - crate::sel_dsl::i64_pair_bin_rule( - op, dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, - ) - .expect("i64 mul op dispatch") - .map_err(synth_core::Error::synthesis)? - .into_iter() - .next() - .expect("i64 mul rule emits one op") - } else { - ArmOp::I64Mul { - rd_lo: dst_lo, - rd_hi: dst_hi, - rn_lo: a_lo, - rn_hi: a_hi, - rm_lo: b_lo, - rm_hi: b_hi, - } - }; + // The single I64Mul pseudo-op comes from the generated + // Rocq-proved rule — the only path (RQ-58-RETIRE; + // `rd_hi <> rd_lo` holds by construction via + // alloc_consecutive_pair). + let mul_op = crate::sel_dsl::i64_pair_bin_rule( + op, dst_lo, dst_hi, a_lo, a_hi, b_lo, b_hi, + ) + .expect("i64 mul op dispatch") + .map_err(synth_core::Error::synthesis)? + .into_iter() + .next() + .expect("i64 mul rule emits one op"); instructions.push(ArmInstruction { op: mul_op, source_line: Some(idx), From f58639413eec6e7c1bbca97a31bca08a4a298d24 Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:09:44 +0200 Subject: [PATCH 32/35] =?UTF-8?q?retire(#242):=20i64.{rotl,rotr}=20?= =?UTF-8?q?=E2=80=94=20delete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves both rotates via the shared i64_rot_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 37 ++++--------------- 1 file changed, 8 insertions(+), 29 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 26e7c418..e9530947 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -17016,36 +17016,15 @@ impl InstructionSelector { &live_params, idx, )?; - // VCR-ISA-001 wave-2 (v0.45): behind SYNTH_SEL_DSL the - // single i64 rotate pseudo-op comes from the generated - // Rocq-proved rule — byte-identical (mirror-pinned; + // The single i64 rotate pseudo-op comes from the generated + // Rocq-proved rule — the only path (RQ-58-RETIRE; // `rd_hi <> rd_lo` holds by construction). - let arm_op = if self.sel_dsl { - crate::sel_dsl::i64_rot_rule(op, dst_lo, dst_hi, a_lo, a_hi, b_lo) - .expect("i64 rotate op dispatch") - .map_err(synth_core::Error::synthesis)? - .into_iter() - .next() - .expect("i64 rotate rule emits one op") - } else { - match op { - I64Rotl => ArmOp::I64Rotl { - rdlo: dst_lo, - rdhi: dst_hi, - rnlo: a_lo, - rnhi: a_hi, - shift: b_lo, - }, - I64Rotr => ArmOp::I64Rotr { - rdlo: dst_lo, - rdhi: dst_hi, - rnlo: a_lo, - rnhi: a_hi, - shift: b_lo, - }, - _ => unreachable!(), - } - }; + let arm_op = crate::sel_dsl::i64_rot_rule(op, dst_lo, dst_hi, a_lo, a_hi, b_lo) + .expect("i64 rotate op dispatch") + .map_err(synth_core::Error::synthesis)? + .into_iter() + .next() + .expect("i64 rotate rule emits one op"); instructions.push(ArmInstruction { op: arm_op, source_line: Some(idx), From 55bcbdc67dcc5afd9d9592a8808bb0af8241220f Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:10:15 +0200 Subject: [PATCH 33/35] =?UTF-8?q?retire(#242):=20i64.{clz,ctz,popcnt}=20?= =?UTF-8?q?=E2=80=94=20delete=20the=20hand-written=20direct-selector=20arm?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit One grouped select_with_stack arm serves the three i64 bit-counts via the shared i64_unary_count_rule dispatch; the deletion unit is the group. Also removes the group's '_ => unreachable!()' wildcard arm. 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 43 +++++-------------- 1 file changed, 11 insertions(+), 32 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index e9530947..028fe291 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -17062,38 +17062,17 @@ impl InstructionSelector { &live_params, idx, )?; - // VCR-ISA-001 wave-2 (v0.45): behind SYNTH_SEL_DSL the - // single i64 bit-count pseudo-op comes from the generated - // Rocq-proved rule — byte-identical (mirror-pinned). The - // trailing `Movw dst_hi, 0` (hi-half zeroing) is outside the - // rule's single-pseudo-op scope, exactly as the flat-model - // ancestor proves only the count pseudo-op. - let arm_op = if self.sel_dsl { - crate::sel_dsl::i64_unary_count_rule(op, dst_lo, src_lo, src_hi) - .expect("i64 count op dispatch") - .into_iter() - .next() - .expect("i64 count rule emits one op") - } else { - match op { - I64Clz => ArmOp::I64Clz { - rd: dst_lo, - rnlo: src_lo, - rnhi: src_hi, - }, - I64Ctz => ArmOp::I64Ctz { - rd: dst_lo, - rnlo: src_lo, - rnhi: src_hi, - }, - I64Popcnt => ArmOp::I64Popcnt { - rd: dst_lo, - rnlo: src_lo, - rnhi: src_hi, - }, - _ => unreachable!(), - } - }; + // The single i64 bit-count pseudo-op comes from the + // generated Rocq-proved rule — the only path + // (RQ-58-RETIRE). The trailing `Movw dst_hi, 0` (hi-half + // zeroing) is outside the rule's single-pseudo-op scope, + // exactly as the flat-model ancestor proves only the count + // pseudo-op. + let arm_op = crate::sel_dsl::i64_unary_count_rule(op, dst_lo, src_lo, src_hi) + .expect("i64 count op dispatch") + .into_iter() + .next() + .expect("i64 count rule emits one op"); instructions.push(ArmInstruction { op: arm_op, source_line: Some(idx), From 8dc2c55a780156f7287a819bc15a90fa3a9fa6eb Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:14:39 +0200 Subject: [PATCH 34/35] retire(#242): the SYNTH_SEL_DSL lever itself + the now-vacuous mirror-pin gates MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit With every superseded arm deleted there is no second implementation for the flag to select: the sel_dsl field, sel_dsl_from_env (SYNTH_SEL_DSL / SYNTH_NO_SEL_DSL), and set_sel_dsl are dead code and go. The four mirror-pin tests (sd + sws + i64-pair + defaults-on) compared the two paths byte-for-byte; with one path left they are vacuous — retired on the same grounds as the VcrSelRulesGenCheck reflexivity gate (see coq/STATUS.md). The #258 imm-fold holdout test is REWRITTEN, not deleted: the residual hand-written Cmp/Cmn+SetCond emission it pins survived the retirement (cmp_imm_fold_residual_path_stays_handwritten_258). The RULES table — including its Delegation wiring metadata that the Rocq generation and the manifest gates consume — is untouched. Byte-identity: 688-row corpus manifest identical to the origin/main baseline; all 10 frozen anchors green; synth-synthesis suite 732+ green. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- .../src/instruction_selector.rs | 784 +----------------- crates/synth-synthesis/src/sel_dsl/mod.rs | 13 +- 2 files changed, 44 insertions(+), 753 deletions(-) diff --git a/crates/synth-synthesis/src/instruction_selector.rs b/crates/synth-synthesis/src/instruction_selector.rs index 028fe291..14708d10 100644 --- a/crates/synth-synthesis/src/instruction_selector.rs +++ b/crates/synth-synthesis/src/instruction_selector.rs @@ -5081,22 +5081,6 @@ pub struct InstructionSelector { /// compiles with the default pool keeps its frame byte-identical by /// construction. i64_spill_slots: usize, - /// VCR-SEL-001 increments 1+2 (#242): serve the migrated selector arms - /// from the generated, Rocq-proved rule table - /// [`crate::sel_dsl::generated`] instead of the hand-written lowering — - /// increment 1: `select_default`'s tier-A i32 ALU six + `i32.rotl`; - /// increment 2: the i32 register shifts + `rotr` (both selectors) and - /// the ten i32 comparisons (`select_with_stack`'s reg-reg CMP+SetCond - /// arm — `select_default`'s blind bare-`Cmp` comparison arms never - /// materialize the 0/1 result and stay hand-written). Default OFF (read - /// from `SYNTH_SEL_DSL`) — OFF keeps every arm on its original - /// hand-written body, and ON is byte-identical by construction. The two - /// implementations are mirror-pinned per op - /// (`sel_dsl_mirror_pin_generated_rules_match_handwritten_arms_242`, - /// `sel_dsl_mirror_pin_select_with_stack_rules_byte_identical_242`). - /// See `docs/design/vcr-sel-001-first-increment.md` and - /// `docs/design/vcr-sel-001-increment-2.md`. - sel_dsl: bool, /// #494 phase 2b (divisor-nonzero fact): op indices (into the stream fed /// to `select_with_stack`) of `div`/`rem` ops whose DIVIDE-BY-ZERO trap /// guard is proven dead — the fact-spec pass discharged @@ -5126,28 +5110,6 @@ pub struct InstructionSelector { call_indirect_guards: synth_core::CallIndirectGuards, } -/// `SYNTH_SEL_DSL` (VCR-SEL-001, #242): **default ON** since the increment-1..4 -/// default-on flip — the 50 Rocq-proved rules are the SHIPPED lowering path for -/// their covered ops. The op list is `sel_dsl::RULES` itself (the single -/// source — it also emits the Rocq model, `VcrSelRulesGenerated.v`, and is -/// 1:1 coverage-gated against `coq/vcr_sel_rules.manifest`); a hand -/// enumeration here said "40" and omitted nine i64 ops (#946), so it was -/// replaced by this pointer. The -/// flip is byte-invisible by construction: every rule was mirror-pinned -/// byte-identical to the hand-written arm it replaces. -/// -/// Opt-out (CI-gated back to the hand-written path): `SYNTH_NO_SEL_DSL=1` -/// (mirrors every other default-on lever's opt-out) or the back-compat -/// `SYNTH_SEL_DSL=0`. `SYNTH_NO_SEL_DSL` wins if both are set. -fn sel_dsl_from_env() -> bool { - // Opt-out escape hatch takes precedence over any opt-in. - if std::env::var("SYNTH_NO_SEL_DSL").is_ok_and(|v| v != "0") { - return false; - } - // Default ON; only an explicit `SYNTH_SEL_DSL=0` forces the old path. - !std::env::var("SYNTH_SEL_DSL").is_ok_and(|v| v == "0") -} - /// #642/#650/#664/#676: resolved `call_indirect` guard inputs — /// `(table_size, table_byte_offset, null_check, type_check)`. `type_check` /// is `Some((expected_class_id, type_id_byte_offset))` when the dispatched @@ -5200,7 +5162,6 @@ impl InstructionSelector { vfp_spill_on_exhaustion: false, local_promote: false, i64_spill_slots: I64_SPILL_SLOTS, - sel_dsl: sel_dsl_from_env(), fact_div_zero_elide: Vec::new(), fact_div_ovf_elide: Vec::new(), fact_mem_bounds_elide: Vec::new(), @@ -5252,7 +5213,6 @@ impl InstructionSelector { vfp_spill_on_exhaustion: false, local_promote: false, i64_spill_slots: I64_SPILL_SLOTS, - sel_dsl: sel_dsl_from_env(), fact_div_zero_elide: Vec::new(), fact_div_ovf_elide: Vec::new(), fact_mem_bounds_elide: Vec::new(), @@ -5314,16 +5274,6 @@ impl InstructionSelector { self.local_promote = enabled; } - /// VCR-SEL-001 increment 1 (#242): serve the migrated `select_default` - /// arms from the generated, Rocq-proved rule table instead of the - /// hand-written lowering. Off ⇒ hand-written path, byte-identical by - /// construction. See the `sel_dsl` field; default comes from - /// `SYNTH_SEL_DSL` — this setter exists so the mirror-pin tests can flip - /// the lever without racing on the process environment. - pub fn set_sel_dsl(&mut self, enabled: bool) { - self.sel_dsl = enabled; - } - /// #494 phase 2b (divisor-nonzero fact): per-site trap-guard elision marks /// for `div`/`rem` ops, keyed by op index into the stream fed to /// `select_with_stack`. `zero` = sites whose divide-by-zero guard was @@ -15946,11 +15896,10 @@ impl InstructionSelector { // The per-half bitwise pair comes from the generated // Rocq-proved rule — the only path (RQ-58-RETIRE; side // conditions hold by construction, see I64Add). - 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)?; + 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, @@ -16319,14 +16268,13 @@ impl InstructionSelector { } else { None }; - // VCR-SEL-001 increment 2 (#242): the plain reg-reg - // CMP+SetCond pair is served from the Rocq-proved rule - // table behind SYNTH_SEL_DSL — `reg_operands` records the - // operand registers so the delegation below can call the - // rule with the exact registers the hand-written arm - // uses (byte-identical by construction; the #258 - // imm-fold peephole stays hand-written, outside the - // reg-reg rule's shape). + // The plain reg-reg CMP+SetCond pair is served from the + // Rocq-proved rule table (the only reg-reg path, + // RQ-58-RETIRE) — `reg_operands` records the operand + // registers so the dispatch below can call the rule with + // the registers the selector chose (the #258 imm-fold + // peephole stays hand-written, outside the reg-reg + // rule's shape). let mut reg_operands = None; let cmp_op = if let Some((is_neg, mag)) = fold { let _b = pop_operand( @@ -16816,8 +16764,9 @@ impl InstructionSelector { // The I64SetCond pseudo-op (condition mapping included) // comes from the generated Rocq-proved rule — the only // path (RQ-58-RETIRE). - let rule_ops = crate::sel_dsl::i64_setcond_rule(op, dst, a_lo, a_hi, b_lo, b_hi) - .expect("binary i64 comparison has a generated rule"); + let rule_ops = + crate::sel_dsl::i64_setcond_rule(op, dst, a_lo, a_hi, b_lo, b_hi) + .expect("binary i64 comparison has a generated rule"); for rule_op in rule_ops { instructions.push(ArmInstruction { op: rule_op, @@ -18041,699 +17990,28 @@ mod tests { } } - /// 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 - /// Rocq-proved rule (flag ON) from identical selector state, and assert - /// the emitted `ArmOp` sequences are EQUAL. Same-ArmOps ⇒ same encoded - /// 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. 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 - /// (never materializes the 0/1 result; production-unreachable — - /// `select_with_stack` owns comparisons) and stay hand-written. Their - /// mirror-pin is - /// `sel_dsl_mirror_pin_select_with_stack_rules_byte_identical_242`. - /// Positive default-on guard for the VCR-SEL-001 flip (#242): the mirror-pin - /// tests use `set_sel_dsl` explicitly and the frozen/differential gates are - /// byte-identical by design, so NONE of them would notice if the default - /// silently reverted to OFF (a construction site hardcoding `false`, or the - /// env logic inverting). This asserts the shipped default actually routes - /// the covered ops through the DSL: a freshly constructed selector — the - /// exact object the compile path builds — has `sel_dsl` set with no env. - #[test] - fn sel_dsl_defaults_on_after_flip_242() { - // Guard against a polluted test-process environment (no test sets these, - // but be explicit): the assertion is only meaningful when neither the - // opt-out nor the back-compat disable is present. - if std::env::var("SYNTH_NO_SEL_DSL").is_ok() || std::env::var("SYNTH_SEL_DSL").is_ok() { - return; - } - assert!( - sel_dsl_from_env(), - "VCR-SEL-001 flip: sel_dsl_from_env() must default ON" - ); - // Both public constructors must carry the default onto the live path. - assert!( - InstructionSelector::new(vec![]).sel_dsl, - "InstructionSelector::new must default sel_dsl ON" - ); - assert!( - InstructionSelector::with_bounds_check(vec![], BoundsCheckConfig::None).sel_dsl, - "InstructionSelector::with_bounds_check must default sel_dsl ON" - ); - } - - #[test] - fn sel_dsl_mirror_pin_generated_rules_match_handwritten_arms_242() { - use crate::sel_dsl::Delegation; - let mut probed = 0; - for rule in crate::sel_dsl::RULES { - if rule.delegation == Delegation::SelectWithStack { - continue; - } - probed += 1; - let ops = vec![rule.op.clone()]; - - // Empty rule set ⇒ the pattern matcher never fires and every op - // takes the select_default path under test. - let mut handwritten = InstructionSelector::new(vec![]); - handwritten.set_sel_dsl(false); - let baseline: Vec = handwritten - .select(&ops) - .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(&ops) - .unwrap_or_else(|e| panic!("{}: generated rule failed: {e}", rule.name)) - .into_iter() - .map(|i| i.op) - .collect(); - - assert_eq!( - baseline, generated, - "{}: generated rule diverges from the hand-written arm — \ - the migration moves structure, never bytes", - rule.name - ); - } - // Non-vacuity: increment 1's seven + increment 2's four shifts + - // increment 3's six i64 pair-family rules + increment 4's three i32 - // bit-manipulation and ten binary I64SetCond comparison rules. - assert_eq!(probed, 30, "unexpected select_default-delegated rule count"); - } - - /// VCR-SEL-001 increment 2 (#242) — gate 1 for the rules delegated in - /// `select_with_stack` (the ten comparisons: `Delegation::SelectWithStack`; - /// the four register shifts: `Delegation::Both`). For each, lower a - /// two-param probe (`local.get 0; local.get 1; `) through - /// `select_with_stack` with the flag OFF and ON and assert the FULL - /// emitted sequences are equal. Non-vacuity (the RMW-vacuity gotcha): - /// locate the hand-written emission window in the OFF sequence, extract - /// the registers the selector chose, and assert the window equals the - /// generated rule's output for exactly those registers — proving the - /// delegation actually fired and the rule reproduces the hand-written - /// arm byte-for-byte. - #[test] - fn sel_dsl_mirror_pin_select_with_stack_rules_byte_identical_242() { - use crate::sel_dsl::Delegation; - use synth_core::WasmOp; - let mut probed = 0; - for rule in crate::sel_dsl::RULES { - 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; - } - // i32.eqz is the sole UNARY compare-with-zero rule (CmpImm + - // SetCond); it needs a single-operand probe and a CmpImm window, - // pinned separately below. - if rule.name == "rule_i32_eqz" { - continue; - } - probed += 1; - let ops = vec![WasmOp::LocalGet(0), WasmOp::LocalGet(1), rule.op.clone()]; - - let mut handwritten = InstructionSelector::new(vec![]); - handwritten.set_sel_dsl(false); - let baseline: Vec = handwritten - .select_with_stack(&ops, 2) - .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, 2) - .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: find the hand-written window, extract the chosen - // registers, and check it equals the rule's own output for them. - let is_cmp_rule = rule - .seq - .iter() - .any(|t| matches!(t, crate::sel_dsl::TemplateOp::SetCond { .. })); - let is_unary_rule = rule.seq.iter().any(|t| { - matches!( - t, - crate::sel_dsl::TemplateOp::Clz { .. } - | crate::sel_dsl::TemplateOp::Rbit { .. } - | crate::sel_dsl::TemplateOp::Popcnt { .. } - ) - }); - let (window, rule_ops) = if is_unary_rule { - // Increment 4's i32 bit-manipulation shapes: the window starts - // at the first Clz/Rbit/Popcnt and spans the rule's length - // (ctz is the two-instruction RBIT+CLZ scratch=dest shape). - let i = baseline - .iter() - .position(|o| { - matches!( - o, - ArmOp::Clz { .. } | ArmOp::Rbit { .. } | ArmOp::Popcnt { .. } - ) - }) - .unwrap_or_else(|| panic!("{}: no bit-manip op in probe output", rule.name)); - let (rd, rm) = match &baseline[i] { - ArmOp::Clz { rd, rm } | ArmOp::Rbit { rd, rm } | ArmOp::Popcnt { rd, rm } => { - (*rd, *rm) - } - _ => unreachable!(), - }; - let rule_ops = crate::sel_dsl::i32_unary_rule(&rule.op, rd, rm) - .unwrap_or_else(|| panic!("{}: unary dispatch missing", rule.name)); - assert!( - baseline.len() >= i + rule_ops.len(), - "{}: probe output too short for the rule window", - rule.name - ); - (baseline[i..i + rule_ops.len()].to_vec(), rule_ops) - } else if is_cmp_rule { - let i = baseline - .iter() - .position(|o| matches!(o, ArmOp::Cmp { .. })) - .unwrap_or_else(|| panic!("{}: no Cmp in probe output", rule.name)); - let (rn, rm) = match &baseline[i] { - ArmOp::Cmp { - rn, - op2: Operand2::Reg(rm), - } => (*rn, *rm), - other => panic!("{}: probe Cmp is not reg-reg: {other:?}", rule.name), - }; - let rd = match &baseline[i + 1] { - ArmOp::SetCond { rd, .. } => *rd, - other => panic!("{}: no SetCond after Cmp: {other:?}", rule.name), - }; - ( - baseline[i..i + 2].to_vec(), - crate::sel_dsl::i32_cmp_rule(&rule.op, rd, rn, rm) - .unwrap_or_else(|| panic!("{}: cmp dispatch missing", rule.name)), - ) - } else { - let i = baseline - .iter() - .position(|o| { - matches!( - o, - ArmOp::LslReg { .. } - | ArmOp::LsrReg { .. } - | ArmOp::AsrReg { .. } - | ArmOp::RorReg { .. } - ) - }) - .unwrap_or_else(|| panic!("{}: no shift op in probe output", rule.name)); - let (rd, rn, rm) = match &baseline[i] { - ArmOp::LslReg { rd, rn, rm } - | ArmOp::LsrReg { rd, rn, rm } - | ArmOp::AsrReg { rd, rn, rm } - | ArmOp::RorReg { rd, rn, rm } => (*rd, *rn, *rm), - _ => unreachable!(), - }; - // #682: LSL/LSR/ASR windows are two instructions (And #31 into - // R12, then the shift by R12); the rule is invoked with the - // ORIGINAL amount register (the And's rn). ROR stays unmasked. - let is_masked = !matches!(&baseline[i], ArmOp::RorReg { .. }); - let (window, orig_rm) = if is_masked { - let orig = match &baseline[i - 1] { - ArmOp::And { rn, .. } => *rn, - other => panic!( - "{}: expected the #682 mask before the shift, found {:?}", - rule.name, other - ), - }; - (baseline[i - 1..=i].to_vec(), orig) - } else { - (baseline[i..i + 1].to_vec(), rm) - }; - ( - window, - crate::sel_dsl::i32_shift_rule(&rule.op, rd, rn, orig_rm, Reg::R12) - .unwrap_or_else(|| panic!("{}: shift dispatch missing", rule.name)) - .unwrap_or_else(|e| panic!("{}: 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 - ); - } - // Ten comparisons + four shifts + increment 4's three i32 - // bit-manipulation rules. - assert_eq!( - probed, 17, - "unexpected select_with_stack-delegated rule count" - ); - - // i32.eqz — the unary compare-with-zero rule, probed with a single - // operand. OFF vs ON full-sequence equality, plus the CmpImm+SetCond - // window RMW-vacuity check for the registers the selector chose. - let eqz_ops = vec![WasmOp::LocalGet(0), WasmOp::I32Eqz]; - let mut hw = InstructionSelector::new(vec![]); - hw.set_sel_dsl(false); - let eqz_baseline: Vec = hw - .select_with_stack(&eqz_ops, 1) - .expect("i32.eqz hand-written arm failed") - .into_iter() - .map(|i| i.op) - .collect(); - let mut dsl = InstructionSelector::new(vec![]); - dsl.set_sel_dsl(true); - let eqz_generated: Vec = dsl - .select_with_stack(&eqz_ops, 1) - .expect("i32.eqz generated rule failed") - .into_iter() - .map(|i| i.op) - .collect(); - assert_eq!( - eqz_baseline, eqz_generated, - "rule_i32_eqz: SYNTH_SEL_DSL=1 diverges from the hand-written \ - select_with_stack arm" - ); - let i = eqz_baseline - .iter() - .position(|o| { - matches!( - o, - ArmOp::Cmp { - op2: Operand2::Imm(_), - .. - } - ) - }) - .expect("rule_i32_eqz: no CMP #imm in probe output"); - let rn = match &eqz_baseline[i] { - ArmOp::Cmp { rn, .. } => *rn, - _ => unreachable!(), - }; - let rd = match &eqz_baseline[i + 1] { - ArmOp::SetCond { rd, .. } => *rd, - other => panic!("rule_i32_eqz: no SetCond after CMP: {other:?}"), - }; - let eqz_rule = crate::sel_dsl::i32_eqz_rule(&WasmOp::I32Eqz, rd, rn) - .expect("rule_i32_eqz: dispatch missing"); - assert_eq!( - eqz_baseline[i..i + 2].to_vec(), - eqz_rule, - "rule_i32_eqz: the hand-written emission window does not equal the \ - generated rule's output for the same registers" - ); - } - - /// 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 if rule - .seq - .iter() - .any(|t| matches!(t, crate::sel_dsl::TemplateOp::I64SetCond { .. })) - { - // Increment 4's binary comparison family: the window is the - // single I64SetCond pseudo-op; extract the FIVE registers the - // hand-written arm chose (result + both operand pairs). - let i = baseline - .iter() - .position(|o| matches!(o, ArmOp::I64SetCond { .. })) - .unwrap_or_else(|| panic!("{}: no I64SetCond in probe output", rule.name)); - let (rd, rn_lo, rn_hi, rm_lo, rm_hi) = match &baseline[i] { - ArmOp::I64SetCond { - rd, - rn_lo, - rn_hi, - rm_lo, - rm_hi, - .. - } => (*rd, *rn_lo, *rn_hi, *rm_lo, *rm_hi), - _ => unreachable!(), - }; - ( - baseline[i..i + 1].to_vec(), - crate::sel_dsl::i64_setcond_rule(&rule.op, rd, rn_lo, rn_hi, rm_lo, rm_hi) - .unwrap_or_else(|| panic!("{}: setcond dispatch missing", rule.name)), - ) - } else if matches!(rule.op, WasmOp::I64Clz | WasmOp::I64Ctz | WasmOp::I64Popcnt) { - // VCR-ISA-001 wave-2: the unary bit-count single-pseudo-op - // window. Extract the three registers the hand-written arm - // chose (rd + operand pair). - let i = baseline - .iter() - .position(|o| { - matches!( - o, - ArmOp::I64Clz { .. } | ArmOp::I64Ctz { .. } | ArmOp::I64Popcnt { .. } - ) - }) - .unwrap_or_else(|| panic!("{}: no i64 count op in probe output", rule.name)); - let (rd, rn_lo, rn_hi) = match &baseline[i] { - ArmOp::I64Clz { rd, rnlo, rnhi } - | ArmOp::I64Ctz { rd, rnlo, rnhi } - | ArmOp::I64Popcnt { rd, rnlo, rnhi } => (*rd, *rnlo, *rnhi), - _ => unreachable!(), - }; - ( - baseline[i..i + 1].to_vec(), - crate::sel_dsl::i64_unary_count_rule(&rule.op, rd, rn_lo, rn_hi) - .unwrap_or_else(|| panic!("{}: count dispatch missing", rule.name)), - ) - } else if matches!(rule.op, WasmOp::I64Rotl | WasmOp::I64Rotr) { - // VCR-ISA-001 wave-2: the i64 rotate single-pseudo-op window - // (five registers: result pair + operand pair + single shift). - let i = baseline - .iter() - .position(|o| matches!(o, ArmOp::I64Rotl { .. } | ArmOp::I64Rotr { .. })) - .unwrap_or_else(|| panic!("{}: no i64 rotate op in probe output", rule.name)); - let (rd_lo, rd_hi, rn_lo, rn_hi, shift) = match &baseline[i] { - ArmOp::I64Rotl { - rdlo, - rdhi, - rnlo, - rnhi, - shift, - } - | ArmOp::I64Rotr { - rdlo, - rdhi, - rnlo, - rnhi, - shift, - } => (*rdlo, *rdhi, *rnlo, *rnhi, *shift), - _ => unreachable!(), - }; - ( - baseline[i..i + 1].to_vec(), - crate::sel_dsl::i64_rot_rule(&rule.op, rd_lo, rd_hi, rn_lo, rn_hi, shift) - .unwrap_or_else(|| panic!("{}: rotate dispatch missing", rule.name)) - .unwrap_or_else(|e| { - panic!( - "{}: selector regs violate rotate side condition: {e}", - rule.name - ) - }), - ) - } else if matches!( - rule.op, - WasmOp::I64Mul | WasmOp::I64Shl | WasmOp::I64ShrU | WasmOp::I64ShrS - ) { - // VCR-ISA-001 wave-2: the i64 binary register-pair - // single-pseudo-op window (six registers). - let i = baseline - .iter() - .position(|o| { - matches!( - o, - ArmOp::I64Mul { .. } - | ArmOp::I64Shl { .. } - | ArmOp::I64ShrU { .. } - | ArmOp::I64ShrS { .. } - ) - }) - .unwrap_or_else(|| panic!("{}: no i64 pair-bin op in probe output", rule.name)); - let (rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi) = match &baseline[i] { - ArmOp::I64Mul { - rd_lo, - rd_hi, - rn_lo, - rn_hi, - rm_lo, - rm_hi, - } - | ArmOp::I64Shl { - rd_lo, - rd_hi, - rn_lo, - rn_hi, - rm_lo, - rm_hi, - } - | ArmOp::I64ShrU { - rd_lo, - rd_hi, - rn_lo, - rn_hi, - rm_lo, - rm_hi, - } - | ArmOp::I64ShrS { - rd_lo, - rd_hi, - rn_lo, - rn_hi, - rm_lo, - rm_hi, - } => (*rd_lo, *rd_hi, *rn_lo, *rn_hi, *rm_lo, *rm_hi), - _ => unreachable!(), - }; - ( - baseline[i..i + 1].to_vec(), - crate::sel_dsl::i64_pair_bin_rule( - &rule.op, rd_lo, rd_hi, rn_lo, rn_hi, rm_lo, rm_hi, - ) - .unwrap_or_else(|| panic!("{}: pair-bin dispatch missing", rule.name)) - .unwrap_or_else(|e| { - panic!( - "{}: selector regs violate pair-bin side condition: {e}", - rule.name - ) - }), - ) - } 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 + increment 4's ten binary - // I64SetCond comparison rules + VCR-ISA-001 wave-2's nine - // single-pseudo-op i64 shapes (clz/ctz/popcnt/mul/shl/shr_u/shr_s/ - // rotl/rotr). - assert_eq!(probed, 25, "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. + /// RQ-58-RETIRE residual pin (#242/#258): the imm-fold comparison + /// peephole (`cmp a, #C` / `cmn a, #-C`) is OUTSIDE the reg-reg + /// `i32_cmp_rule`'s shape and its hand-written Cmp/Cmn+SetCond emission + /// deliberately SURVIVED the arm retirement (no CmpImm-shaped rule + /// exists). This pins that the fold still fires — if a future rule + /// covers the imm shape, this test is the one to retire with it. #[test] - fn sel_dsl_cmp_imm_fold_path_stays_handwritten_and_byte_identical_242() { + fn cmp_imm_fold_residual_path_stays_handwritten_258() { use synth_core::WasmOp; for (c, opv) in [(5i32, WasmOp::I32Eq), (-7i32, WasmOp::I32LtS)] { let ops = vec![WasmOp::LocalGet(0), WasmOp::I32Const(c), opv]; - let mut handwritten = InstructionSelector::new(vec![]); - handwritten.set_sel_dsl(false); - let baseline: Vec = handwritten + let emitted: Vec = InstructionSelector::new(vec![]) .select_with_stack(&ops, 1) - .expect("hand-written fold path failed") + .expect("imm-fold comparison probe failed") .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, 1) - .expect("fold path with flag ON failed") - .into_iter() - .map(|i| i.op) - .collect(); - - assert_eq!( - baseline, generated, - "imm-fold comparison path must stay byte-identical under SYNTH_SEL_DSL=1" - ); - // The fold actually fired (imm cmp/cmn present, no reg-reg Cmp). + // The fold actually fired (imm cmp/cmn present)... assert!( - baseline.iter().any(|o| matches!( + emitted.iter().any(|o| matches!( o, ArmOp::Cmp { op2: Operand2::Imm(_), @@ -18745,6 +18023,18 @@ mod tests { )), "probe did not exercise the imm-fold path" ); + // ...and the reg-reg rule shape did NOT (no reg-reg Cmp), i.e. + // the probe really took the residual hand-written emission. + assert!( + !emitted.iter().any(|o| matches!( + o, + ArmOp::Cmp { + op2: Operand2::Reg(_), + .. + } + )), + "imm-fold probe unexpectedly took the reg-reg rule path" + ); } } diff --git a/crates/synth-synthesis/src/sel_dsl/mod.rs b/crates/synth-synthesis/src/sel_dsl/mod.rs index 2158e19c..858cb743 100644 --- a/crates/synth-synthesis/src/sel_dsl/mod.rs +++ b/crates/synth-synthesis/src/sel_dsl/mod.rs @@ -39,10 +39,11 @@ //! //! The table is turned into plain Rust lowering functions by //! [`generate_lowering_source`] and the output is **committed to the tree** at -//! [`generated`] (reviewable diffs, no build-time codegen). `select_default` -//! keeps dispatch ownership: a migrated arm delegates to the generated rule -//! behind `SYNTH_SEL_DSL` (default ON since v0.39.0; opt out with SYNTH_NO_SEL_DSL), so OFF ≡ baseline byte-identical by -//! construction. +//! [`generated`] (reviewable diffs, no build-time codegen). The selectors keep +//! dispatch ownership: a covered op's arm calls the generated rule as its ONLY +//! lowering — RQ-58-RETIRE (#242, v0.58) deleted the hand-written arms the +//! rules had superseded (and with them the `SYNTH_SEL_DSL`/`SYNTH_NO_SEL_DSL` +//! lever, which had been byte-invisible since the default-on flip). //! //! Every rule carries a **1:1 Rocq obligation**: rule `rule_i32_add` ↔ theorem //! `rule_i32_add_correct` in `coq/Synth/Synth/VcrSelRules.v` (T1, discharged by @@ -140,8 +141,8 @@ pub enum SideCondition { NotAlias(RegVar, RegVar), } -/// Which hand-written selector arm delegates to this rule behind -/// `SYNTH_SEL_DSL` — i.e. where the rule is byte-identically wired. +/// Which selector arm(s) the rule is wired into as the sole lowering +/// (RQ-58-RETIRE deleted the hand-written alternatives). /// /// Increment 1 wired `select_default` only. Increment 2 steps the comparison /// family into `select_with_stack` because that is where the load-bearing From 2ed949ba4ef534fe943aef717242e5d46223a48b Mon Sep 17 00:00:00 2001 From: Ralf Anton Beier Date: Wed, 19 Aug 2026 06:17:55 +0200 Subject: [PATCH 35/35] docs+ledger(#242): re-bank the subtraction ratchet for RQ-58-RETIRE claims.yaml: selector_lines_code 18582 -> 17897 (banked), wildcard_arms_code 63 -> 56 (banked), totals tracked 29839 -> 28495 / 106 -> 91; the two former #992 waivers deleted with the re-bank (a waiver above the new baseline is a standing licence to grow back). status.json regenerated via --emit-status. CLAUDE.md / coq/STATUS.md / verified-codegen-roadmap.yaml no longer claim the SYNTH_NO_SEL_DSL opt-out exists; rivet RQ-58-RETIRE -> implemented with evidence + the measured residual set. claim_check 49/49. Co-Authored-By: Claude Opus 5 Claude-Session: https://claude.ai/code/session_01YJK5LZZEkV5smCY1jKn18L --- CLAUDE.md | 8 ++-- artifacts/release-v0.58.yaml | 21 +++++++++- artifacts/status.json | 8 ++-- artifacts/verified-codegen-roadmap.yaml | 16 +++++++ claims.yaml | 55 +++++++++++-------------- coq/STATUS.md | 15 +++---- 6 files changed, 77 insertions(+), 46 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index 14907668..7ed73916 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -187,9 +187,11 @@ frozen and oracle-gated every step: - **Track A (core):** `VCR-RA-001` allocator with Belady spilling — **verified, default-on since v0.24.0** (`SYNTH_SPILL_REALLOC`; `SYNTH_SPILL_ON_EXHAUST` built flag-off, silicon-gated #580). Next: `VCR-SEL-001` Rocq-discharged - verified selector DSL (increments 1–4 shipped **default-on**, 50 rules / 50 Qed, - `SYNTH_SEL_DSL`; the Rocq-proved rules are the SHIPPED lowering path for their - 50 covered ops, opt-out `SYNTH_NO_SEL_DSL=1`, byte-invisible flip) and + verified selector DSL (increments 1–4 shipped **default-on**, 50 rules / 50 Qed; + the Rocq-proved rules are the ONLY lowering path for their 50 covered ops — + RQ-58-RETIRE (v0.58) deleted the superseded hand-written arms byte-identically, + and with them the `SYNTH_SEL_DSL`/`SYNTH_NO_SEL_DSL` lever and the mirror-pin + gates, both vacuous once the second implementation was gone) and `VCR-PERF-002` proof-carrying specialization (#494, 0.45× floor; phase 1 facts ingestion landed, PR #624). - **Track B (semantics):** `VCR-ISA-001` Sail-generated Rocq ISA model — diff --git a/artifacts/release-v0.58.yaml b/artifacts/release-v0.58.yaml index ad4721a5..3ef0eb7b 100644 --- a/artifacts/release-v0.58.yaml +++ b/artifacts/release-v0.58.yaml @@ -146,7 +146,26 @@ artifacts: `select_with_stack`). An arm that is dead on one path and live on the other is NOT deletable yet; say which those are rather than deleting them and discovering it downstream. That set is the input to RQ-58-SPLIT. - status: proposed + LANDED (v0.58): all 36 flag-guarded sites deleted (21 select_default + + 15 select_with_stack; one op/group per commit), each commit gated on a + 688-row corpus byte-identity manifest (156 scripts/repro fixtures x 4 + configs — m4f/m4 relocatable, m4f self-contained, r5 relocatable — + declines pinned too) against the pre-deletion origin/main baseline plus + the 10 frozen anchors. BYTE-IDENTICAL THROUGHOUT — no finding of the + "flip does not cover what it claims" class surfaced. The SYNTH_SEL_DSL + lever and the four mirror-pin tests retired as vacuous in the final + functional commit; the #258 imm-fold holdout re-pinned as + cmp_imm_fold_residual_path_stays_handwritten_258. Selector code region + 18,582 -> 17,897 (-685), absorbing wildcards 63 -> 56 (-7), whole file + 29,839 -> 28,495; ratchet re-banked. RESIDUAL (the RQ-58-SPLIT input, + measured not guessed): select_with_stack's i32 add/sub/mul/and/or/xor + arms (hand-written imm-fold shapes, never DSL-wired), its i32.rotl arm, + and its i32-comparison imm-fold (#258 cmp/cmn) fallback emission; + select_default's blind-Cmp i32 comparison + i32.eqz arms and its + fixed-pair i64 mul/shl/shr_u/shr_s/rotl/rotr/clz/ctz/popcnt arms + (production-unreachable via compile paths — select_with_stack matches + those ops before its fallthrough — but live via the pub select() API). + status: implemented release: v0.58 tags: [north-star, subtraction, vcr-sel-001, byte-identical] links: diff --git a/artifacts/status.json b/artifacts/status.json index 1e00b157..167ca946 100644 --- a/artifacts/status.json +++ b/artifacts/status.json @@ -28,10 +28,10 @@ "sel_dsl_rule_qed": 50, "sel_dsl_rules": 50, "sel_rules_simplified_basis": 50, - "selector_lines_code": 18582, - "selector_lines_total": 29839, - "selector_wildcard_arms_code": 63, - "selector_wildcard_arms_total": 106, + "selector_lines_code": 17897, + "selector_lines_total": 28495, + "selector_wildcard_arms_code": 56, + "selector_wildcard_arms_total": 91, "version": "0.57.0", "verus_spec_fns": 8, "wasmcert_bridge_qed": 104 diff --git a/artifacts/verified-codegen-roadmap.yaml b/artifacts/verified-codegen-roadmap.yaml index 3fc8a1ed..fe8eaf3e 100644 --- a/artifacts/verified-codegen-roadmap.yaml +++ b/artifacts/verified-codegen-roadmap.yaml @@ -474,6 +474,22 @@ artifacts: verified) — i64 mul/div/shifts/rotates/comparisons (I64SetCond) + optimizer_bridge + the remaining select_with_stack families; div/rem (VCR-ISA-001-gated). + RQ-58-RETIRE LANDED (v0.58): the hand-written arms the 50 rules had + superseded are DELETED — 36 flag-guarded sites across both selectors + (21 select_default + 15 select_with_stack), one op/group per commit, + each gated on a 688-row corpus byte-identity manifest (156 fixtures x + 4 configs vs the pre-deletion baseline) + the 10 frozen anchors. The + SYNTH_SEL_DSL/SYNTH_NO_SEL_DSL lever and the four mirror-pin tests + went with them (vacuous once the second implementation was gone — the + VcrSelRulesGenCheck precedent); the #258 cmp/cmn imm-fold holdout is + re-pinned as cmp_imm_fold_residual_path_stays_handwritten_258. + Selector non-test code 18,582 -> 17,897 lines, absorbing wildcards + 63 -> 56 (ratchet re-banked in claims.yaml). Residual (RQ-58-SPLIT + input): select_with_stack's i32 add/sub/mul/and/or/xor (imm-fold + shapes) + i32.rotl arms; select_default's blind-Cmp i32 comparison + + i32.eqz arms and its fixed-pair i64 mul/shift/rotate/bit-count + arms — covered ops whose per-path arms were never DSL-wired, so + nothing there was superseded or deletable. status: implemented tags: [codegen, selector, isle, verified-dsl, rocq, track-a, novel, release-v0.12.1] links: diff --git a/claims.yaml b/claims.yaml index a3978958..19c0f211 100644 --- a/claims.yaml +++ b/claims.yaml @@ -1226,22 +1226,18 @@ claims: # THE LOAD-BEARING PIN: hand-written lowering code, test module excluded. # RQ-58-RETIRE (delete the arms the 50 DSL rules replaced) is measured # here, and so is any lane that adds an arm without deleting one. + # RQ-58-RETIRE (v0.58): first downward movement — the 50 DSL rules' + # superseded hand-written arms deleted (36 flag-guarded sites across + # both selectors) plus the then-dead SYNTH_SEL_DSL lever, each deletion + # byte-identity-gated (688-row corpus manifest + 10 frozen anchors). + # 18,582 -> 17,897; banked. The former #992 waiver (to: 18582) is + # deleted with the re-bank — a surviving waiver above the new baseline + # would be a standing licence to grow back to it. - kind: ratchet name: selector_lines_code direction: down - value: 18582 - baseline: 18480 - waivers: - - to: 18582 - reason: >- - Growth is #992's, not this lane's: the ARM select-on-i64-comparison - miscompile fix (#973) added 102 code-region lines (an operand- - classification helper + two guarded call sites). #992 merged at - 19:50 UTC and #991 pinned these values at 20:07 from a PR base - that predated it (strict=false stale-base cross), so main itself - derives 18582 against a ledger saying 18480 — this PR is the - first to carry the union and the ledger moves here, with the - growth attributed to the correctness fix that caused it. + value: 17897 + baseline: 17897 # The whole-file figures the release plan and the sibling lanes quote. An # unpinned quoted number is the drift class this release is about — but # they are `track`, not `down`, and the distinction is deliberate. Both @@ -1255,35 +1251,32 @@ claims: - kind: ratchet name: selector_lines_total direction: track - # 29616 -> 29839: #992 (+102 code-region lines, +121 test-module lines) - # crossed with #991's pin measurement on a stale base; see the - # selector_lines_code waiver above for the attribution. - value: 29839 + # 29839 -> 28495 (RQ-58-RETIRE): -685 code-region lines (the arm + # deletions) and -659 test-module lines (the four mirror-pin tests, + # vacuous once the hand-written mirror was gone — the + # VcrSelRulesGenCheck precedent). + value: 28495 # RQ-58-WILDCARD's real denominator, and THE directed wildcard pin. 62 # absorbing arms are in the lowering code; the other 43 of the plan's 105 # are assertion helpers in the test module, where a `_ =>` is not a # miscompile risk. Red-first demonstrated on the REAL file, not only # against a synthetic fixture: see scripts/repro/rq_58_metric_gate.md §1b. + # RQ-58-RETIRE (v0.58): 63 -> 56. Seven '_ => unreachable!()' arms + # lived INSIDE deleted hand-written bodies (the sd/sws i64-comparison + # condition maps, the sws i64 bitwise/shift/rotate/bit-count group + # dispatches, the sws i32 shift dispatch); they went with their arms. + # Banked; the former #992 waiver (to: 63) deleted with the re-bank. - kind: ratchet name: selector_wildcard_arms_code direction: down - value: 63 - baseline: 62 - waivers: - - to: 63 - reason: >- - The one new absorbing arm is `_ => None` in #992's i64-comparison - operand-classification helper (a total function over WasmOp whose - non-comparison arms decline, feeding the #973 miscompile fix) — - added on main by #992 after #991 measured this pin on a stale - base. Same cross as the selector_lines_code waiver. + value: 56 + baseline: 56 - kind: ratchet name: selector_wildcard_arms_total direction: track - # 105 -> 106: the same #992 `_ => None` helper arm the code-region - # waiver above covers (the arm is in the CODE region; both counts - # include it), crossed with #991's stale-base pin measurement. - value: 106 + # 106 -> 91 (RQ-58-RETIRE): the 7 code-region arms above plus 8 + # assertion-helper '_ =>' arms inside the retired mirror-pin tests. + value: 91 # The other half of the same trade: the verified path must GROW as the # hand-written one shrinks. Pinned as a FLOOR so a rule can never be quietly diff --git a/coq/STATUS.md b/coq/STATUS.md index 77a6d341..2469c2ad 100644 --- a/coq/STATUS.md +++ b/coq/STATUS.md @@ -600,10 +600,11 @@ The Rocq suite proves things in two very different places, and #73's measurable if they are counted separately: - **DSL-served** — the op's *shipped* lowering is a `sel_dsl` rule with a - 1:1 Qed theorem in `VcrSelRules.v`, register-polymorphic, mirror-pinned - byte-identical to the hand-written arm(s) (`SYNTH_SEL_DSL`, **default ON** - since the increment-1..4 flip — opt-out `SYNTH_NO_SEL_DSL=1`). These proofs - are about the code that ships — and now, by default, the code that DOES ship. + 1:1 Qed theorem in `VcrSelRules.v`, register-polymorphic, and since + RQ-58-RETIRE (v0.58) the ONLY lowering for the op: the hand-written arms + the rules had mirrored byte-identically were deleted, along with the + `SYNTH_SEL_DSL`/`SYNTH_NO_SEL_DSL` lever. These proofs are about the code + that ships — now the only code there is. - **model-only** — the op is proven only against `compile_wasm_to_arm` (Compilation.v), the fixed-register model that diverges from the shipped Rust selector in documented ways (#73). Evidence about a model, not the @@ -655,9 +656,9 @@ additionally gates FPU ops behind the #369/GI-FPU work. **Retirement criterion (#73):** a `compile_wasm_to_arm` arm may be deleted (and its Correctness* theorem retired) once its family is DSL-served — the -DSL theorem is strictly stronger (register-polymorphic, mirror-pinned to -the shipped bytes). The model-only column is the shrinking measure; report -it per release. +DSL theorem is strictly stronger (register-polymorphic, and since v0.58 the +rule IS the shipped lowering, no mirror in between). The model-only column +is the shrinking measure; report it per release. ## Phase History