SETH ⇒ OVC sparsification bundle 7: concrete word-RAM formalization

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_06

set_option autoImplicit true

/-! Complete finite source-code simulation of a memory-writing instruction. -/
namespace WordRAM.Conjectures.SimulationWrite

open SimulationMemory
variable {narrow wide : Width}

/-- Load both source operands before resolving and writing the destination.
This order preserves the original instruction's old-memory aliasing semantics. -/
def algorithm (op : SimulationStore.Operation) (dst : Address) (x y : SourceOperand) : Algorithm :=
  ⟨SourceChain.code (SimulationOperand.algorithm 26 x).code
    (SourceChain.code (SimulationOperand.algorithm 27 y).code
      (SourceChain.code (addressAlgorithm dst).code (SimulationStore.algorithm op).code)),
    1, by decide⟩

def cost (dst : Address) (x y : SourceOperand) : Nat :=
  SimulationOperand.cost x + (SimulationOperand.cost y + (addressCost dst + 4))

/-- A complete simulation block takes at most eighteen instructions, even
when both operands and the destination use indirect addressing. -/
theorem simulates (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base : Nat) (op : SimulationStore.Operation)
    (dst : Address) (x y : SourceOperand)
    (pc : s.pc = 0) (live : s.halted = false) (large : 32 ≤ base)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (native : s.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow))
    (xfits : SimulationOperand.FixedFits base x wide)
    (yfits : SimulationOperand.FixedFits base y wide)
    (dfits : base + staticCell dst < 2 ^ wide.bits)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    cost dst x y ≤ 18 ∧ ∃ final,
      Runs widthConstant ((algorithm op dst x y).program wide) (cost dst x y) s final ∧
      final.halted = true ∧
      Represents (Memory.write source (dst.resolve source)
        (op.value ((x.compile narrow).read source) ((y.compile narrow).read source))) final.mem base ∧
      (∀ cell, (cell < 25 ∨ 29 ≤ cell) → cell ≠ base + dst.resolve source →
        final.mem cell = s.mem cell) := by
  obtain ⟨xb, tx, xt, xhalt, xv, xr, xf⟩ := SimulationOperand.loads_trace h source s base 26 x
    pc live (by omega) (by decide) (by decide) represented pointer mask xfits dynamic
  let sy := SourceChain.resume tx
  obtain ⟨yb, ty, yt, yhalt, yv, yr, yf⟩ := SimulationOperand.loads_trace h source sy base 27 y
    rfl rfl (by omega) (by decide) (by decide) xr
    ((xf 24 (by decide) (by decide)).trans pointer)
    ((xf 30 (by decide) (by decide)).trans mask) yfits dynamic
  let sd := SourceChain.resume ty
  obtain ⟨td, dt, dhalt, dv, dr, df⟩ := address_trace h source sd base dst
    rfl rfl (by omega) yr
    ((yf 24 (by decide) (by decide)).trans ((xf 24 (by decide) (by decide)).trans pointer)) dfits dynamic
  let so := SourceChain.resume td
  have ox : so.mem 26 = WidthSimulation.lift wide ((x.compile narrow).read source) :=
    (df 26 (by decide)).trans ((yf 26 (by decide) (by decide)).trans xv)
  have oy : so.mem 27 = WidthSimulation.lift wide ((y.compile narrow).read source) :=
    (df 27 (by decide)).trans yv
  have om : so.mem 30 = WidthSimulation.mask narrow wide :=
    (df 30 (by decide)).trans ((yf 30 (by decide) (by decide)).trans ((xf 30 (by decide) (by decide)).trans mask))
  have on : so.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow) :=
    (df 31 (by decide)).trans ((yf 31 (by decide) (by decide)).trans ((xf 31 (by decide) (by decide)).trans native))
  obtain ⟨out, ot, ohalt, result, oframe⟩ := SimulationStore.stores_trace h source so base
    (dst.resolve source) op ((x.compile narrow).read source) ((y.compile narrow).read source)
    rfl rfl large dr dv (translated_fits h source dst base dfits dynamic) ox oy om on
  have dot := SourceChain.traces (addressAlgorithm dst).code (SimulationStore.algorithm op).code
    sd td out (addressCost dst) 4 rfl dhalt dt ot
  have ydot := SourceChain.traces (SimulationOperand.algorithm 27 y).code
    (SourceChain.code (addressAlgorithm dst).code (SimulationStore.algorithm op).code)
    sy ty _ (SimulationOperand.cost y) (addressCost dst + 4) rfl yhalt yt dot
  have all := SourceChain.traces (SimulationOperand.algorithm 26 x).code
    (SourceChain.code (SimulationOperand.algorithm 27 y).code
      (SourceChain.code (addressAlgorithm dst).code (SimulationStore.algorithm op).code))
    s tx _ (SimulationOperand.cost x) (SimulationOperand.cost y + (addressCost dst + 4)) live xhalt xt ydot
  have db : addressCost dst ≤ 4 := by cases dst <;> simp [addressCost]
  refine ⟨by unfold cost; omega, _, all, ohalt, result, ?_⟩
  intro cell outside ne
  exact (oframe cell (by omega) ne).trans
    ((df cell (by omega)).trans ((yf cell (by omega) (by omega)).trans (xf cell (by omega) (by omega))))

end WordRAM.Conjectures.SimulationWrite

/-! Connecting complete simulation blocks to the original instruction semantics. -/
namespace WordRAM.Conjectures.SimulationInstruction

open SimulationMemory
variable {narrow wide : Width}

/-- Uniform description of any instruction that writes a memory cell. Unused
operands for unary/native instructions are normalized to the literal zero. -/
structure WriteSpec where
  operation : SimulationStore.Operation
  destination : Address
  left : SourceOperand
  right : SourceOperand

def WriteSpec.source (spec : WriteSpec) : SourceInstruction :=
  match spec.operation with
  | .copy => .copy spec.destination spec.left
  | .binary op => .binary op spec.destination spec.left spec.right
  | .bitNot => .bitNot spec.destination spec.left
  | .wordWidth => .wordWidth spec.destination

def decode : SourceInstruction → Option WriteSpec
  | .copy dst src => some ⟨.copy, dst, src, .immediate 0⟩
  | .binary op dst x y => some ⟨.binary op, dst, x, y⟩
  | .bitNot dst src => some ⟨.bitNot, dst, src, .immediate 0⟩
  | .wordWidth dst => some ⟨.wordWidth, dst, .immediate 0, .immediate 0⟩
  | .jump _ | .branch _ _ _ _ | .halt => none

theorem decode_source (instruction : SourceInstruction) (spec : WriteSpec)
    (decoded : decode instruction = some spec) : spec.source = instruction := by
  cases instruction <;> simp only [decode, Option.some.injEq] at decoded
  all_goals first | contradiction | (subst spec; rfl)

theorem execute_memory (spec : WriteSpec) (s : State narrow) :
    (execute widthConstant (spec.source.compile narrow) s).mem =
      Memory.write s.mem (spec.destination.resolve s.mem)
        (spec.operation.value ((spec.left.compile narrow).read s.mem) ((spec.right.compile narrow).read s.mem)) := by
  cases spec with
  | mk operation dst x y => cases operation <;> rfl

def algorithm (spec : WriteSpec) : Algorithm :=
  SimulationWrite.algorithm spec.operation spec.destination spec.left spec.right

def cost (spec : WriteSpec) : Nat := SimulationWrite.cost spec.destination spec.left spec.right

end WordRAM.Conjectures.SimulationInstruction

/-! A complete branch-condition computation with a Boolean result in cell 29.
The surrounding compiler can then use absolute program-counter targets. -/
namespace WordRAM.Conjectures.SimulationCompare

open SimulationMemory
variable {narrow wide : Width}

def finish (cmp : Comparison) : Algorithm :=
  ⟨[.branch cmp (.memory (.direct 26)) (.memory (.direct 27)) 3,
    .copy (.direct 29) (.immediate 0), .halt,
    .copy (.direct 29) (.immediate 1), .halt], 1, by decide⟩

theorem finishes (h : narrow.bits ≤ wide.bits) (s : State wide) (cmp : Comparison)
    (x y : Word narrow) (pc : s.pc = 0) (live : s.halted = false)
    (left : s.mem 26 = WidthSimulation.lift wide x)
    (right : s.mem 27 = WidthSimulation.lift wide y) :
    let t := run widthConstant ((finish cmp).program wide) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧
    t.mem 29 = (if cmp.test x y then 1 else 0) ∧
    (∀ cell, cell ≠ 29 → t.mem cell = s.mem cell) := by
  cases test : cmp.test x y <;>
    simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
      run, step, execute, Operand.read, Address.resolve, Memory.write,
      pc, live, left, right, WidthSimulation.comparison h, test, Nat.add_assoc]
  all_goals intro cell ne; simp [ne]

def algorithm (cmp : Comparison) (x y : SourceOperand) : Algorithm :=
  ⟨SourceChain.code (SimulationOperand.algorithm 26 x).code
    (SourceChain.code (SimulationOperand.algorithm 27 y).code (finish cmp).code), 1, by decide⟩

def cost (x y : SourceOperand) : Nat := SimulationOperand.cost x + (SimulationOperand.cost y + 3)

/-- Both operand loads and the comparison are included in the cost. The
result represents the original narrow comparison, with virtual memory intact. -/
theorem simulates (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base : Nat) (cmp : Comparison) (x y : SourceOperand)
    (pc : s.pc = 0) (live : s.halted = false) (large : 32 ≤ base)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (xfits : SimulationOperand.FixedFits base x wide)
    (yfits : SimulationOperand.FixedFits base y wide)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    cost x y ≤ 13 ∧ ∃ final,
      Runs widthConstant ((algorithm cmp x y).program wide) (cost x y) s final ∧
      final.halted = true ∧ Represents source final.mem base ∧
      final.mem 29 = (if cmp.test ((x.compile narrow).read source) ((y.compile narrow).read source) then 1 else 0) ∧
      (∀ cell, cell < 25 ∨ 30 ≤ cell → final.mem cell = s.mem cell) := by
  obtain ⟨xb, tx, xt, xhalt, xv, xr, xf⟩ := SimulationOperand.loads_trace h source s base 26 x
    pc live (by omega) (by decide) (by decide) represented pointer mask xfits dynamic
  let sy := SourceChain.resume tx
  obtain ⟨yb, ty, yt, yhalt, yv, yr, yf⟩ := SimulationOperand.loads_trace h source sy base 27 y
    rfl rfl (by omega) (by decide) (by decide) xr
    ((xf 24 (by decide) (by decide)).trans pointer)
    ((xf 30 (by decide) (by decide)).trans mask) yfits dynamic
  let sf := SourceChain.resume ty
  obtain ⟨ohalt, ticks, value, frame⟩ := finishes h sf cmp ((x.compile narrow).read source)
    ((y.compile narrow).read source) rfl rfl
    ((yf 26 (by decide) (by decide)).trans xv) yv
  let out := run widthConstant ((finish cmp).program wide) 3 sf
  have ot : Runs widthConstant ((finish cmp).program wide) 3 sf out := by
    obtain ⟨n, _, trace⟩ := run_has_trace widthConstant ((finish cmp).program wide) 3 sf
    have hc := runs_cost trace
    have eq : n = 3 := by omega
    subst n
    exact trace
  have yt' := SourceChain.traces (SimulationOperand.algorithm 27 y).code (finish cmp).code
    sy ty out (SimulationOperand.cost y) 3 rfl yhalt yt ot
  have all := SourceChain.traces (SimulationOperand.algorithm 26 x).code
    (SourceChain.code (SimulationOperand.algorithm 27 y).code (finish cmp).code)
    s tx _ (SimulationOperand.cost x) (SimulationOperand.cost y + 3) live xhalt xt yt'
  refine ⟨by unfold cost; omega, _, all, ohalt, ?_, value, ?_⟩
  · exact yr.frame (fun cell lo => frame cell (by omega))
  · intro cell outside
    exact (frame cell (by omega)).trans ((yf cell (by omega) (by omega)).trans (xf cell (by omega) (by omega)))

end WordRAM.Conjectures.SimulationCompare

/-! A uniform compiler with fixed-size instruction blocks. Control targets are
absolute addresses in the compiled program, so backward jumps need no subtraction. -/
namespace WordRAM.Conjectures.SimulationCompiler

/-- Each original instruction occupies 32 source instructions. Padding is
unreachable on a correctly simulated step because the tail transfers control. -/
def stride : Nat := 32

def body (instruction : SourceInstruction) : List SourceInstruction :=
  match SimulationInstruction.decode instruction with
  | some spec => (SimulationInstruction.algorithm spec).code
  | none => match instruction with
    | .branch cmp x y _ => (SimulationCompare.algorithm cmp x y).code
    | _ => []

def tail (pc : Nat) : SourceInstruction → List SourceInstruction
  | .branch _ _ _ target =>
      [.branch .eq (.memory (.direct 29)) (.immediate 1) (stride * target), .jump (stride * (pc + 1))]
  | .jump target => [.jump (stride * target)]
  | .halt => [.halt]
  | _ => [.jump (stride * (pc + 1))]

def padding : SourceInstruction := .copy (.direct 29) (.memory (.direct 29))

def block (pc : Nat) (instruction : SourceInstruction) : List SourceInstruction :=
  ((body instruction).map (SourceInstruction.returnTo (body instruction).length)).map
      (SourceInstruction.relocate (stride * pc)) ++
    tail pc instruction ++ List.replicate (stride - ((body instruction).length + (tail pc instruction).length)) padding

def code (source : List SourceInstruction) : List SourceInstruction :=
  (List.ofFn fun pc : Fin source.length => block pc.val source[pc.val]).flatten

theorem operand_length (dst : Nat) (operand : SourceOperand) :
    (SimulationOperand.algorithm dst operand).code.length = SimulationOperand.cost operand := by
  cases operand with
  | immediate literal => rfl
  | memory address => cases address <;> rfl

theorem operand_length_le (dst : Nat) (operand : SourceOperand) :
    (SimulationOperand.algorithm dst operand).code.length ≤ 5 := by
  rw [operand_length]
  cases operand with
  | immediate literal => simp [SimulationOperand.cost]
  | memory address => cases address <;> simp [SimulationOperand.cost, SimulationMemory.addressCost]

theorem write_length (spec : SimulationInstruction.WriteSpec) :
    (SimulationInstruction.algorithm spec).code.length = SimulationInstruction.cost spec := by
  simp only [SimulationInstruction.algorithm, SimulationWrite.algorithm, SourceChain.length,
    operand_length, SimulationInstruction.cost, SimulationWrite.cost]
  cases spec.destination <;> rfl

theorem write_length_le (spec : SimulationInstruction.WriteSpec) :
    (SimulationInstruction.algorithm spec).code.length ≤ 18 := by
  have hx := operand_length_le 26 spec.left
  have hy := operand_length_le 27 spec.right
  rw [operand_length] at hx hy
  rw [write_length]
  unfold SimulationInstruction.cost SimulationWrite.cost
  have hd : SimulationMemory.addressCost spec.destination ≤ 4 := by
    cases spec.destination <;> simp [SimulationMemory.addressCost]
  omega

theorem compare_length_le (cmp : Comparison) (x y : SourceOperand) :
    (SimulationCompare.algorithm cmp x y).code.length ≤ 15 := by
  have hx := operand_length_le 26 x
  have hy := operand_length_le 27 y
  simp only [SimulationCompare.algorithm, SourceChain.length]
  change (SimulationOperand.algorithm 26 x).code.length +
    ((SimulationOperand.algorithm 27 y).code.length + 5) ≤ 15
  omega

theorem body_length_le (instruction : SourceInstruction) : (body instruction).length ≤ 18 := by
  cases decoded : SimulationInstruction.decode instruction with
  | some spec => simpa only [body, decoded] using write_length_le spec
  | none =>
    cases instruction <;> simp only [body, decoded, List.length_nil]
    all_goals first | omega | (exact Nat.le_trans (compare_length_le _ _ _) (by decide))

theorem tail_length_le (pc : Nat) (instruction : SourceInstruction) : (tail pc instruction).length ≤ 2 := by
  cases instruction <;> simp [tail]

theorem block_length (pc : Nat) (instruction : SourceInstruction) :
    (block pc instruction).length = stride := by
  have hb := body_length_le instruction
  have ht := tail_length_le pc instruction
  simp only [block, List.length_append, List.length_map, List.length_replicate]
  unfold stride
  omega

private theorem flatten_fetch (f : Fin n → List α) (size : Nat)
    (lengths : ∀ i, (f i).length = size) (i : Fin n) (j : Nat) (hj : j < size) :
    (List.ofFn f).flatten[i.val * size + j]? = (f i)[j]? := by
  induction n with
  | zero => exact Fin.elim0 i
  | succ n ih =>
    rw [List.ofFn_succ, List.flatten_cons]
    cases i with
    | mk index bound =>
      cases index with
      | zero =>
        simp only [Nat.zero_mul, Nat.zero_add]
        exact List.getElem?_append_left (by rw [lengths]; exact hj)
      | succ index =>
        rw [List.getElem?_append_right (by rw [lengths]; simp [Nat.add_mul]; omega)]
        rw [lengths]
        have eq : (index + 1) * size + j - size = index * size + j := by
          simp [Nat.add_mul]; omega
        rw [eq]
        exact ih (fun k => f k.succ) (fun k => lengths k.succ) ⟨index, by omega⟩

theorem code_fetch (source : List SourceInstruction) (pc : Fin source.length)
    (offset : Nat) (small : offset < stride) :
    (code source)[stride * pc.val + offset]? = (block pc.val source[pc.val])[offset]? := by
  rw [Nat.mul_comm stride pc.val]
  exact flatten_fetch _ stride (fun pc => block_length pc.val source[pc.val]) pc offset small

/-- Every local body is embedded in the full program with exactly the intended
return continuation and relocation. This covers its internal loops and jumps. -/
theorem body_embedded (source : List SourceInstruction) (pc : Fin source.length) (w : Width) :
    EmbedsAt
      (((body source[pc.val]).map (SourceInstruction.compile w)).map
        (Instruction.returnTo (body source[pc.val]).length))
      ((code source).map (SourceInstruction.compile w)) (stride * pc.val) := by
  intro offset instruction fetch
  have small : offset < (body source[pc.val]).length := by
    have := (List.getElem?_eq_some_iff.mp fetch).1
    simpa using this
  have hbound : offset < stride := by
    have := body_length_le source[pc.val]
    unfold stride
    omega
  simp only [List.getElem?_map, code_fetch source pc offset hbound]
  rw [block, List.getElem?_append_left (by simp; omega),
    List.getElem?_append_left (by simp; exact small)]
  simp only [List.getElem?_map, Option.map_map, Function.comp_def] at fetch ⊢
  simp only [compile_relocate, compile_returnTo]
  simpa only [Option.map_map, Function.comp_def, Option.map_some] using
    congrArg (Option.map (Instruction.relocate (stride * pc.val))) fetch

/-- Tail instructions retain their absolute global targets; unlike body
instructions they must not be relocated again. -/
theorem tail_fetch (source : List SourceInstruction) (pc : Fin source.length) (w : Width)
    (offset : Nat) (small : offset < (tail pc.val source[pc.val]).length) :
    ((code source).map (SourceInstruction.compile w))[stride * pc.val + (body source[pc.val]).length + offset]? =
      ((tail pc.val source[pc.val]).map (SourceInstruction.compile w))[offset]? := by
  have hb := body_length_le source[pc.val]
  have ht := tail_length_le pc.val source[pc.val]
  have inside : (body source[pc.val]).length + offset < stride := by unfold stride; omega
  rw [Nat.add_assoc]
  simp only [List.getElem?_map, code_fetch source pc _ inside]
  rw [block, List.getElem?_append_left (by simp; omega)]
  rw [List.getElem?_append_right (by simp)]
  simp

end WordRAM.Conjectures.SimulationCompiler

/-! Step and trace invariants for the complete compiled program. -/
namespace WordRAM.Conjectures.SimulationExecution

open SimulationMemory SimulationCompiler
variable {narrow wide : Width}

/-- The PC condition is needed only while live. A halt increments the two
physical PCs differently, but preserves the same halted memory and result. -/
structure Related (source : State narrow) (host : State wide) (base : Nat) : Prop where
  memory : Represents source.mem host.mem base
  pointer : host.mem 24 = BitVec.ofNat wide.bits base
  mask : host.mem 30 = WidthSimulation.mask narrow wide
  native : host.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow)
  halted : host.halted = source.halted
  pc : source.halted = false → host.pc = stride * source.pc

def Fits (base : Nat) (wide : Width) (instruction : SourceInstruction) : Prop :=
  match SimulationInstruction.decode instruction with
  | some spec => SimulationOperand.FixedFits base spec.left wide ∧
      SimulationOperand.FixedFits base spec.right wide ∧ base + staticCell spec.destination < 2 ^ wide.bits
  | none => match instruction with
    | .branch _ x y _ => SimulationOperand.FixedFits base x wide ∧ SimulationOperand.FixedFits base y wide
    | _ => True

/-- Move a verified standalone body into its actual compiled program block. -/
theorem call_body (source : List SourceInstruction) (pc : Fin source.length)
    (host built : State wide) (n : Nat)
    (atPC : host.pc = stride * pc.val) (live : host.halted = false)
    (halted : built.halted = true)
    (trace : Runs widthConstant ((body source[pc.val]).map (SourceInstruction.compile wide)) n
      (SourceChain.resume host) built) :
    ∃ ready, Runs widthConstant ((code source).map (SourceInstruction.compile wide)) n host ready ∧
      ready.pc = stride * pc.val + (body source[pc.val]).length ∧ ready.halted = false ∧ ready.mem = built.mem := by
  let ready := (built.returnTo (body source[pc.val]).length).relocate (stride * pc.val)
  have start : ((SourceChain.resume host).returnTo (body source[pc.val]).length).relocate (stride * pc.val) = host := by
    simp only [State.returnTo, SourceChain.resume, Bool.false_eq_true, ↓reduceIte, State.relocate, Nat.add_zero]
    rw [← atPC, ← live]
  refine ⟨ready, ?_, ?_, ?_, ?_⟩
  · simpa only [start] using (trace.returnTo (body source[pc.val]).length).relocate (body_embedded source pc wide)
  all_goals simp [ready, State.returnTo, State.relocate, halted]

end WordRAM.Conjectures.SimulationExecution