/-
  Blitter6502OISC.lean — 6502 OISC Blitter

  Concrete OISC (One Instruction Set Computer) ISA on 6502 architecture.
  Connects HCMR's abstract throughput predictions to concrete instruction
  semantics.

  Clean rewrite for SilverSight — not a port from Research Stack.

  The single instruction is SUBLEQ (Subtract and Branch if Less than or
  Equal to zero):
    SUBLEQ a, b, c:  M[b] := M[b] - M[a];  if M[b] ≤ 0 then PC := c

  Components:
  - 6502 addressing modes (zero page, absolute, indexed)
  - SUBLEQ semantics (subtract, store, conditional branch)
  - Blitter: memory-to-memory copy via SUBLEQ loop
  - Throughput prediction via HCMR

  Connection to HCMR:
  - Each SUBLEQ instruction has self-loop prob 0.823 (measured)
  - Blitter throughput = base_rate × (1 - 0.823) = base_rate × 0.177
  - The blitter is the "word SUBLEQ" regime from HCMR

  Connection to CRT multiplexer:
  - The SUBLEQ loop IS a braid: each iteration is a crossing
  - The branch condition (M[b] ≤ 0) is the chiral selector (over/under)
  - The blitter copies data through a braid of SUBLEQ crossings
-/

import Mathlib.Data.Real.Basic
import Mathlib.Tactic
import SilverSight.HCMR

namespace SilverSight.Blitter6502OISC

/-- 6502 addressing mode. -/
inductive AddrMode where
  | zeroPage   : AddrMode    -- zero page (0x00-0xFF, fast)
  | absolute   : AddrMode    -- absolute (16-bit address)
  | indexed    : AddrMode    -- indexed (absolute + register offset)
  | indirect   : AddrMode    -- indirect (pointer dereference)
  deriving Repr, DecidableEq

/-- Memory address with addressing mode. -/
structure M6502Addr where
  mode   : AddrMode
  addr   : ℕ              -- the address (or base for indexed)
  deriving Repr

/-- The single OISC instruction: SUBLEQ a, b, c. -/
structure SUBLEQ where
  srcA   : M6502Addr      -- source A (subtrahend)
  dstB   : M6502Addr      -- destination B (minuend and result)
  branch : M6502Addr      -- branch target if result ≤ 0
  deriving Repr

/-- 6502 machine state: memory + program counter. -/
structure M6502State where
  mem : ℕ → ℕ             -- memory as function (0 = uninitialized)
  pc  : ℕ                  -- program counter

/-- 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 :=
  { 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.

    The loop:
      loop: SUBLEQ src, dst, end    -- dst := dst - src (but we negate src first)
             SUBLEQ zero, src, loop  -- restore src (src := src - 0 = src... no)
    Actually, a proper SUBLEQ blitter uses a negation trick:
      SUBLEQ src, tmp, +3   -- tmp := tmp - src = -src
      SUBLEQ tmp, dst, +3   -- dst := dst - (-src) = dst + src
      SUBLEQ zero, tmp, loop -- tmp := tmp - 0 = 0 (reset for next iteration)
    This copies M[src] to M[dst] in 3 SUBLEQ instructions per byte. -/
structure BlitterProgram where
  srcAddr    : ℕ           -- source address
  dstAddr    : ℕ           -- destination address
  tmpAddr    : ℕ           -- temporary address for negation
  byteCount  : ℕ           -- number of bytes to copy
  deriving Repr

/-- Build the SUBLEQ blitter program for one byte copy. -/
def buildBlitterStep (prog : BlitterProgram) : List SUBLEQ :=
  [ -- Step 1: tmp := tmp - src = -src (assuming tmp starts at 0)
    { srcA := { mode := .absolute, addr := prog.srcAddr },
      dstB := { mode := .absolute, addr := prog.tmpAddr },
      branch := { mode := .absolute, addr := 0 } },  -- never branch
    -- Step 2: dst := dst - tmp = dst - (-src) = dst + src
    { srcA := { mode := .absolute, addr := prog.tmpAddr },
      dstB := { mode := .absolute, addr := prog.dstAddr },
      branch := { mode := .absolute, addr := 0 } },  -- never branch
    -- Step 3: tmp := tmp - 0 = 0 (reset tmp for next iteration)
    -- Actually: tmp is currently -src, so we need tmp := 0
    -- SUBLEQ tmp, tmp, loop: tmp := tmp - tmp = 0
    { srcA := { mode := .absolute, addr := prog.tmpAddr },
      dstB := { mode := .absolute, addr := prog.tmpAddr },
      branch := { mode := .absolute, addr := 0 } }   -- never branch
  ]

/-- Total instruction count for a blitter: 3 × byteCount. -/
def blitterInstrCount (prog : BlitterProgram) : ℕ :=
  3 * prog.byteCount

/-- Predicted blitter throughput using HCMR.

    SUBLEQ self-loop prob = 0.823 → throughput = baseRate × 0.177
    Total cycles = blitterInstrCount / throughput -/
def predictedThroughput (baseRate : ℕ) (prog : BlitterProgram) : ℕ :=
  HCMR.throughput baseRate .subleqWord * blitterInstrCount prog

-- ── Theorems ──────────────────────────────────────────────────────────

/-- 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
  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
  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
  unfold execSUBLEQ
  have h_not_le : ¬ (s.mem inst.dstB.addr - s.mem inst.srcA.addr ≤ 0) := by omega
  simp [h_not_le]

/-- Blitter step count: 3 SUBLEQ instructions per byte. -/
theorem blitter_step_count (prog : BlitterProgram) :
    blitterInstrCount prog = 3 * prog.byteCount := rfl

/-- HCMR connection: blitter throughput uses SUBLEQ self-loop probability.

    The blitter operates in the "word SUBLEQ" regime from HCMR.
    Throughput = baseRate × (1 - 0.823) = baseRate × 0.177 per instruction. -/
theorem blitter_uses_subleq_throughput (baseRate : ℕ) (prog : BlitterProgram) :
    predictedThroughput baseRate prog =
      HCMR.throughput baseRate .subleqWord * blitterInstrCount prog := rfl

/-- 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 `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, 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
