From 9cb97c61bd12f1f26e58d561cd16a5bf483d4404 Mon Sep 17 00:00:00 2001
From: allaun <allaun@researchstack.info>
Date: Sun, 5 Jul 2026 06:12:27 -0500
Subject: [PATCH] =?UTF-8?q?fix:=20Blitter6502OISC=20=E2=80=94=20inline=20l?=
 =?UTF-8?q?et=20binders=20in=20execSUBLEQ,=20remove=20Repr=20(=E2=84=95?=
 =?UTF-8?q?=E2=86=92=E2=84=95)?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

execSUBLEQ now uses direct field syntax instead of let binders,
fixing the 'rw can't find pattern' errors on branch/fall-through
theorems. Removed deriving Repr from M6502State (functions aren't
Repr-able).

Build: 3299 jobs, 0 errors
---
 formal/SilverSight/Blitter6502OISC.lean | 56 +++++++++++++++----------
 1 file changed, 34 insertions(+), 22 deletions(-)

diff --git a/formal/SilverSight/Blitter6502OISC.lean b/formal/SilverSight/Blitter6502OISC.lean
index 8923a7e6..e278e3ab 100644
--- a/formal/SilverSight/Blitter6502OISC.lean
+++ b/formal/SilverSight/Blitter6502OISC.lean
@@ -59,20 +59,18 @@ structure SUBLEQ where
 structure M6502State where
   mem : ℕ → ℕ             -- memory as function (0 = uninitialized)
   pc  : ℕ                  -- program counter
-  deriving Repr
 
 /-- Execute one SUBLEQ instruction.
 
     M[b] := M[b] - M[a]
     if M[b] ≤ 0 then PC := c else PC := PC + 3 (3 operands) -/
 def execSUBLEQ (s : M6502State) (inst : SUBLEQ) : M6502State :=
-  let aVal := s.mem inst.srcA.addr
-  let bVal := s.mem inst.dstB.addr
-  let result := bVal - aVal
-  let newPC := if result ≤ 0 then inst.branch.addr else s.pc + 3
-  let newMem := fun addr =>
-    if addr == inst.dstB.addr then result else s.mem addr
-  { mem := newMem, pc := newPC }
+  { mem := fun addr => if addr == inst.dstB.addr
+      then s.mem inst.dstB.addr - s.mem inst.srcA.addr
+      else s.mem addr
+  , pc := if s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0
+      then inst.branch.addr
+      else s.pc + 3 }
 
 /-- Blitter: copy N bytes from src to dst using a SUBLEQ loop.
 
@@ -125,21 +123,22 @@ def predictedThroughput (baseRate : ℕ) (prog : BlitterProgram) : ℕ :=
 /-- SUBLEQ execution: result = M[b] - M[a]. -/
 theorem subleq_subtracts (s : M6502State) (inst : SUBLEQ) :
     (execSUBLEQ s inst).mem inst.dstB.addr = s.mem inst.dstB.addr - s.mem inst.srcA.addr := by
-  simp [execSUBLEQ]
+  unfold execSUBLEQ
+  simp
 
 /-- SUBLEQ branches when result ≤ 0. -/
 theorem subleq_branches_on_le_zero (s : M6502State) (inst : SUBLEQ)
     (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0) :
     (execSUBLEQ s inst).pc = inst.branch.addr := by
-  simp [execSUBLEQ]
-  rw [if_pos h]
+  unfold execSUBLEQ
+  simp [h]
 
 /-- SUBLEQ falls through when result > 0. -/
 theorem subleq_falls_through (s : M6502State) (inst : SUBLEQ)
     (h : s.mem inst.dstB.addr - s.mem inst.srcA.addr > 0) :
     (execSUBLEQ s inst).pc = s.pc + 3 := by
-  simp [execSUBLEQ]
-  rw [if_neg (by omega : ¬(s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0))]
+  unfold execSUBLEQ
+  simp [h]
 
 /-- Blitter step count: 3 SUBLEQ instructions per byte. -/
 theorem blitter_step_count (prog : BlitterProgram) :
@@ -153,19 +152,32 @@ theorem blitter_uses_subleq_throughput (baseRate : ℕ) (prog : BlitterProgram)
     predictedThroughput baseRate prog =
       HCMR.throughput baseRate .subleqWord * blitterInstrCount prog := rfl
 
-/-- Ring dispatch is at least as fast as SUBLEQ for the blitter.
+/-- Ring dispatch would be at least as fast as SUBLEQ for the blitter.
 
-    If the blitter used ring dispatch (zero contention) instead of SUBLEQ
-    (82.3% contention), throughput would be at least as high. This is the
-    HCMR ordering theorem applied to the blitter. Stated with `≥` because
-    Q16_16 truncation makes the two sides equal when `byteCount = 0`
-    (both products vanish), and `omega` cannot discharge the nonlinear
-    `a * c > b * c` goal that the strict version would need. -/
+    If the blitter used ring dispatch (zero contention) instead of
+    SUBLEQ (82.3% contention), throughput would be `baseRate × 1.0`
+    instead of `baseRate × 0.177` per instruction. This is the HCMR
+    ordering theorem applied to the blitter.
+
+    NOTE: stated with `≥` rather than `>` because when `byteCount = 0`,
+    both throughputs are 0 and the strict ordering is vacuously false.
+    The non-strict ordering holds for all `baseRate > 0`. -/
 theorem ring_faster_than_subleq_blitter (baseRate : ℕ) (prog : BlitterProgram)
     (hbase : baseRate > 0) :
     HCMR.throughput baseRate .ringDispatch * blitterInstrCount prog ≥
     predictedThroughput baseRate prog := by
-  simp only [predictedThroughput]
-  exact Nat.mul_le_mul_right _ (HCMR.ring_fastest_subleq_avx baseRate hbase).1
+  simp only [predictedThroughput, HCMR.throughput, HCMR.selfLoopProb, blitterInstrCount]
+  have hpos : (0 : ℕ) < 65536 := by norm_num
+  have h_left : baseRate * 65536 / 65536 = baseRate := by
+    rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left baseRate hpos
+  have h_right_le : baseRate * 11628 / 65536 ≤ baseRate := by
+    have h_step : baseRate * 11628 / 65536 ≤ baseRate * 65536 / 65536 :=
+      Nat.div_le_div_right (Nat.mul_le_mul_left baseRate (by norm_num : (11628:ℕ) ≤ 65536))
+    have h_cancel : baseRate * 65536 / 65536 = baseRate := by
+      rw [Nat.mul_comm]; exact Nat.mul_div_cancel_left baseRate hpos
+    rw [h_cancel] at h_step
+    exact h_step
+  rw [h_left]
+  exact Nat.mul_le_mul_right _ h_right_le
 
 end SilverSight.Blitter6502OISC