SETH ⇒ OVC sparsification bundle 6: 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_05

set_option autoImplicit true

/-! Memory representation for a narrow machine simulated in a wide machine. -/
namespace WordRAM.Conjectures.SimulationMemory

variable {narrow wide : Width}

/-- The entire virtual memory, including addresses beyond the narrow word
range, is represented at a translated physical address. -/
def Represents (source : Memory narrow) (target : Memory wide) (base : Nat) : Prop :=
  ∀ address, target (base + address) = WidthSimulation.lift wide (source address)

theorem Represents.frame (h : Represents source target base)
    (frame : ∀ address, base ≤ address → other address = target address) :
    Represents source other base := by
  intro address
  rw [frame _ (by omega)]
  exact h address

/-- An actual store to a translated address simulates a virtual store, also
when the virtual cell is itself used as an indirect pointer. -/
theorem Represents.write (h : Represents source target base) (address : Nat) (value : Word narrow) :
    Represents (Memory.write source address value)
      (Memory.write target (base + address) (WidthSimulation.lift wide value)) base := by
  intro cell
  by_cases eq : cell = address
  · subst cell; simp [Memory.write]
  · simp [Memory.write, eq, h cell]

/-- The source cell appearing literally in an address instruction. Direct
addresses need not fit a narrow word; their translated addresses must fit wide. -/
def staticCell : Address → Nat
  | .direct cell | .indirect cell => cell

theorem translated_fits (_h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (address : Address) (base : Nat)
    (fixed : base + staticCell address < 2 ^ wide.bits)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    base + address.resolve source < 2 ^ wide.bits := by
  cases address with
  | direct cell => exact fixed
  | indirect cell =>
    have range := (source cell).isLt
    change base + (source cell).toNat < 2 ^ wide.bits
    omega

/-- Registers 24, 25 and 30 are reserved for base, address scratch and mask. -/
def addressCode : Address → List SourceInstruction
  | .direct cell =>
      [.binary .add (.direct 25) (.memory (.direct 24)) (.immediate cell), .halt]
  | .indirect cell =>
      [.binary .add (.direct 25) (.memory (.direct 24)) (.immediate cell),
       .copy (.direct 25) (.memory (.indirect 25)),
       .binary .add (.direct 25) (.memory (.direct 24)) (.memory (.direct 25)), .halt]

def addressAlgorithm (address : Address) : Algorithm := ⟨addressCode address, 1, by decide⟩

def addressCost : Address → Nat
  | .direct _ => 2
  | .indirect _ => 4

theorem address_run (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base : Nat) (address : Address)
    (pc : s.pc = 0) (live : s.halted = false) (large : 31 ≤ base)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (fixed : base + staticCell address < 2 ^ wide.bits)
    (_dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    let t := run widthConstant ((addressAlgorithm address).program wide) (addressCost address) s
    t.halted = true ∧ t.ticks = s.ticks + addressCost address ∧
    t.mem 25 = BitVec.ofNat wide.bits (base + address.resolve source) ∧
    (∀ cell, cell ≠ 25 → t.mem cell = s.mem cell) := by
  cases address with
  | direct cell =>
    simp [addressAlgorithm, addressCode, addressCost, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer,
      ← BitVec.ofNat_add, -BitVec.toNat_ofNat]
    intro cell ne; simp [ne]
  | indirect cell =>
    have fixed' : base + cell < 2 ^ wide.bits := fixed
    have location : (BitVec.ofNat wide.bits (base + cell)).toNat = base + cell :=
      Nat.mod_eq_of_lt fixed'
    have ne : base + cell ≠ 25 := by omega
    have value : BitVec.ofNat wide.bits base + WidthSimulation.lift wide (source cell) =
        BitVec.ofNat wide.bits (base + (source cell).toNat) := by
      have hv : WidthSimulation.lift wide (source cell) = BitVec.ofNat wide.bits (source cell).toNat := by
        apply BitVec.eq_of_toNat_eq
        rw [WidthSimulation.lift_value h, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
        exact Nat.lt_of_lt_of_le (source cell).isLt (Nat.pow_le_pow_right (by decide) h)
      rw [hv, ← BitVec.ofNat_add]
    simp [addressAlgorithm, addressCode, addressCost, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer,
      ← BitVec.ofNat_add, location, ne, represented cell, value,
      Nat.add_assoc, -BitVec.toNat_ofNat]
    intro cell ne; simp [ne]

/-- Exact instruction trace and preservation of the entire virtual memory. -/
theorem address_trace (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base : Nat) (address : Address)
    (pc : s.pc = 0) (live : s.halted = false) (large : 31 ≤ base)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (fixed : base + staticCell address < 2 ^ wide.bits)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    ∃ final, Runs widthConstant ((addressAlgorithm address).program wide) (addressCost address) s final ∧
      final.halted = true ∧
      final.mem 25 = BitVec.ofNat wide.bits (base + address.resolve source) ∧
      Represents source final.mem base ∧
      (∀ cell, cell ≠ 25 → final.mem cell = s.mem cell) := by
  obtain ⟨halted, ticks, result, frame⟩ := address_run h source s base address pc live large represented pointer fixed dynamic
  obtain ⟨cost, _, trace⟩ := run_has_trace widthConstant ((addressAlgorithm address).program wide) (addressCost address) s
  have hc := runs_cost trace
  have eq : cost = addressCost address := by omega
  subst cost
  exact ⟨_, trace, halted, result, represented.frame (fun cell lo => frame cell (by omega)), frame⟩

end WordRAM.Conjectures.SimulationMemory

/-! Uniform operand-loading blocks for the cross-width solver simulation. -/
namespace WordRAM.Conjectures.SimulationOperand

open SimulationMemory
variable {narrow wide : Width}

/-- Cells 26 through 29 are value registers; cell 25 is address scratch.
The stored mask in cell 30 truncates arbitrary immediate literals. -/
def code (dst : Nat) : SourceOperand → List SourceInstruction
  | .immediate literal =>
      [.copy (.direct dst) (.immediate literal),
       .binary .band (.direct dst) (.memory (.direct dst)) (.memory (.direct 30)), .halt]
  | .memory address => (addressCode address).dropLast ++
      [.copy (.direct dst) (.memory (.indirect 25)), .halt]

def algorithm (dst : Nat) (operand : SourceOperand) : Algorithm := ⟨code dst operand, 1, by decide⟩

def cost : SourceOperand → Nat
  | .immediate _ => 3
  | .memory address => addressCost address + 1

def FixedFits (base : Nat) (operand : SourceOperand) (wide : Width) : Prop :=
  match operand with
  | .immediate _ => True
  | .memory address => base + staticCell address < 2 ^ wide.bits

private theorem lift_word (h : narrow.bits ≤ wide.bits) (x : Word narrow) :
    WidthSimulation.lift wide x = BitVec.ofNat wide.bits x.toNat := by
  apply BitVec.eq_of_toNat_eq
  rw [WidthSimulation.lift_value h, BitVec.toNat_ofNat, Nat.mod_eq_of_lt]
  exact Nat.lt_of_lt_of_le x.isLt (Nat.pow_le_pow_right (by decide) h)

/-- All three operand modes load the original narrow value; scratch writes
preserve every other physical cell. -/
theorem loads (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base dst : Nat) (operand : SourceOperand)
    (pc : s.pc = 0) (live : s.halted = false) (large : 31 ≤ base)
    (dstLow : 26 ≤ dst) (dstHigh : dst ≤ 29)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (fixed : FixedFits base operand wide)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    let t := run widthConstant ((algorithm dst operand).program wide) (cost operand) s
    t.halted = true ∧ t.ticks = s.ticks + cost operand ∧
    t.mem dst = WidthSimulation.lift wide ((operand.compile narrow).read source) ∧
    (∀ cell, cell ≠ 25 → cell ≠ dst → t.mem cell = s.mem cell) := by
  have dstNe : dst ≠ 24 ∧ dst ≠ 25 ∧ dst ≠ 30 ∧ 30 ≠ dst := by omega
  cases operand with
  | immediate literal =>
    simp [algorithm, code, cost, Algorithm.program, SourceInstruction.compile,
      SourceOperand.compile, run, step, execute, Address.resolve, Operand.read,
      Memory.write, BinOp.eval, pc, live, dstNe, mask, WidthSimulation.immediate h,
      Nat.add_assoc]
    intro cell _ hd; simp [hd]
  | memory address =>
    cases address with
    | direct cell =>
      have fixed' : base + cell < 2 ^ wide.bits := fixed
      have location : (BitVec.ofNat wide.bits (base + cell)).toNat = base + cell :=
        Nat.mod_eq_of_lt fixed'
      have cellNe : base + cell ≠ 25 := by omega
      simp [algorithm, code, cost, addressCode, addressCost, Algorithm.program,
        SourceInstruction.compile, SourceOperand.compile, run, step, execute,
        Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer,
        ← BitVec.ofNat_add, location, cellNe, represented cell,
        Nat.add_assoc, -BitVec.toNat_ofNat]
      intro address h25 hd; simp [h25, hd]
    | indirect cell =>
      have fixed' : base + cell < 2 ^ wide.bits := fixed
      have location : (BitVec.ofNat wide.bits (base + cell)).toNat = base + cell :=
        Nat.mod_eq_of_lt fixed'
      have cellNe : base + cell ≠ 25 := by omega
      have targetNe : base + (source cell).toNat ≠ 25 := by omega
      have targetFits : base + (source cell).toNat < 2 ^ wide.bits := by
        have := (source cell).isLt; omega
      have targetLocation : (BitVec.ofNat wide.bits (base + (source cell).toNat)).toNat =
          base + (source cell).toNat := Nat.mod_eq_of_lt targetFits
      have value : BitVec.ofNat wide.bits base + WidthSimulation.lift wide (source cell) =
          BitVec.ofNat wide.bits (base + (source cell).toNat) := by
        rw [lift_word h, ← BitVec.ofNat_add]
      simp [algorithm, code, cost, addressCode, addressCost, Algorithm.program,
        SourceInstruction.compile, SourceOperand.compile, run, step, execute,
        Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer,
        ← BitVec.ofNat_add, location, cellNe, represented cell, value,
        targetLocation, targetNe, represented (source cell).toNat,
        Nat.add_assoc, -BitVec.toNat_ofNat]
      intro address h25 hd; simp [h25, hd]

/-- Operand evaluation takes at most five actual instructions, with no change
to any virtual memory cell. -/
theorem loads_trace (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base dst : Nat) (operand : SourceOperand)
    (pc : s.pc = 0) (live : s.halted = false) (large : 31 ≤ base)
    (dstLow : 26 ≤ dst) (dstHigh : dst ≤ 29)
    (represented : Represents source s.mem base)
    (pointer : s.mem 24 = BitVec.ofNat wide.bits base)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (fixed : FixedFits base operand wide)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    cost operand ≤ 5 ∧ ∃ final,
      Runs widthConstant ((algorithm dst operand).program wide) (cost operand) s final ∧
      final.halted = true ∧
      final.mem dst = WidthSimulation.lift wide ((operand.compile narrow).read source) ∧
      Represents source final.mem base ∧
      (∀ cell, cell ≠ 25 → cell ≠ dst → final.mem cell = s.mem cell) := by
  have bound : cost operand ≤ 5 := by
    cases operand with
    | immediate _ => simp [cost]
    | memory address => cases address <;> simp [cost, addressCost]
  obtain ⟨halted, ticks, value, frame⟩ := loads h source s base dst operand pc live large
    dstLow dstHigh represented pointer mask fixed dynamic
  obtain ⟨n, _, trace⟩ := run_has_trace widthConstant ((algorithm dst operand).program wide) (cost operand) s
  have hc := runs_cost trace
  have eq : n = cost operand := by omega
  subst n
  exact ⟨bound, _, trace, halted, value,
    represented.frame (fun cell lo => frame cell (by omega) (by omega)), frame⟩

end WordRAM.Conjectures.SimulationOperand

/-! Arithmetic and store blocks for the narrow-word simulation. Operand and
address setup are separate verified blocks; all source values are read first. -/
namespace WordRAM.Conjectures.SimulationStore

open SimulationMemory
variable {narrow wide : Width}

inductive Operation where
  | copy
  | binary (op : BinOp .multiplication)
  | bitNot
  | wordWidth

def Operation.value (op : Operation) (x y : Word w) : Word w :=
  match op with
  | .copy => x
  | .binary bin => bin.eval x y
  | .bitNot => ~~~x
  | .wordWidth => BitVec.ofNat w.bits w.bits

/-- The simulated native constant is supplied in cell 31. Loading the host's
native width here would give the wrong answer. -/
def Operation.instruction : Operation → SourceInstruction
  | .copy => .copy (.direct 28) (.memory (.direct 26))
  | .binary bin => .binary bin (.direct 28) (.memory (.direct 26)) (.memory (.direct 27))
  | .bitNot => .bitNot (.direct 28) (.memory (.direct 26))
  | .wordWidth => .copy (.direct 28) (.memory (.direct 31))

def algorithm (op : Operation) : Algorithm :=
  ⟨[op.instruction,
    .binary .band (.direct 28) (.memory (.direct 28)) (.memory (.direct 30)),
    .copy (.indirect 25) (.memory (.direct 28)), .halt], 1, by decide⟩

private theorem mask_lift (h : narrow.bits ≤ wide.bits) (x : Word narrow) :
    WidthSimulation.lift wide x &&& WidthSimulation.mask narrow wide = WidthSimulation.lift wide x := by
  rw [WidthSimulation.mask_project h, WidthSimulation.project_lift h]

/-- With operands and destination prepared, arithmetic and the final store
use four instructions and change exactly the intended virtual memory cell. -/
theorem stores (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base address : Nat) (op : Operation) (x y : Word narrow)
    (pc : s.pc = 0) (live : s.halted = false) (large : 32 ≤ base)
    (represented : Represents source s.mem base)
    (destination : s.mem 25 = BitVec.ofNat wide.bits (base + address))
    (fits : base + address < 2 ^ wide.bits)
    (left : s.mem 26 = WidthSimulation.lift wide x)
    (right : s.mem 27 = WidthSimulation.lift wide y)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (native : s.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow)) :
    let t := run widthConstant ((algorithm op).program wide) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧
    Represents (Memory.write source address (op.value x y)) t.mem base ∧
    (∀ cell, cell ≠ 28 → cell ≠ base + address → t.mem cell = s.mem cell) := by
  have location : (BitVec.ofNat wide.bits (base + address)).toNat = base + address :=
    Nat.mod_eq_of_lt fits
  have result (old : Word wide) (value : Word narrow) :
      Represents (Memory.write source address value)
        (Memory.write (Memory.write (Memory.write s.mem 28 old) 28 (WidthSimulation.lift wide value))
          (base + address) (WidthSimulation.lift wide value)) base := by
    apply Represents.write
    apply represented.frame
    intro cell lo
    simp [Memory.write, show cell ≠ 28 by omega]
  cases op with
  | copy =>
    simp [algorithm, Operation.instruction, Operation.value, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Operand.read, Address.resolve, BinOp.eval, Memory.write, pc, live,
      destination, left, mask, location, mask_lift h, Nat.add_assoc]
    exact ⟨by simpa [Memory.write] using result _ x, fun cell h28 ht => by simp [h28, ht]⟩
  | binary bin =>
    simp [algorithm, Operation.instruction, Operation.value, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Operand.read, Address.resolve, Memory.write, pc, live,
      destination, left, right, mask, location,
      show BinOp.eval (w := wide) .band = (fun x y => x &&& y) from rfl,
      WidthSimulation.binary h, Nat.add_assoc]
    exact ⟨by simpa [Memory.write] using result _ (bin.eval x y), fun cell h28 ht => by simp [h28, ht]⟩
  | bitNot =>
    simp [algorithm, Operation.instruction, Operation.value, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Operand.read, Address.resolve, BinOp.eval, Memory.write, pc, live,
      destination, left, mask, location, WidthSimulation.bitNot h, Nat.add_assoc]
    exact ⟨by simpa [Memory.write] using result _ (~~~x), fun cell h28 ht => by simp [h28, ht]⟩
  | wordWidth =>
    simp [algorithm, Operation.instruction, Operation.value, Algorithm.program,
      SourceInstruction.compile, SourceOperand.compile, run, step, execute,
      Operand.read, Address.resolve, BinOp.eval, Memory.write, pc, live,
      destination, mask, native, location, mask_lift h, Nat.add_assoc]
    exact ⟨by simpa [Memory.write] using result _ (BitVec.ofNat narrow.bits narrow.bits),
      fun cell h28 ht => by simp [h28, ht]⟩

/-- The store block's exact trace can be linked after the operand/address blocks. -/
theorem stores_trace (h : narrow.bits ≤ wide.bits) (source : Memory narrow)
    (s : State wide) (base address : Nat) (op : Operation) (x y : Word narrow)
    (pc : s.pc = 0) (live : s.halted = false) (large : 32 ≤ base)
    (represented : Represents source s.mem base)
    (destination : s.mem 25 = BitVec.ofNat wide.bits (base + address))
    (fits : base + address < 2 ^ wide.bits)
    (left : s.mem 26 = WidthSimulation.lift wide x)
    (right : s.mem 27 = WidthSimulation.lift wide y)
    (mask : s.mem 30 = WidthSimulation.mask narrow wide)
    (native : s.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow)) :
    ∃ final, Runs widthConstant ((algorithm op).program wide) 4 s final ∧
      final.halted = true ∧
      Represents (Memory.write source address (op.value x y)) final.mem base ∧
      (∀ cell, cell ≠ 28 → cell ≠ base + address → final.mem cell = s.mem cell) := by
  obtain ⟨halted, ticks, result, frame⟩ := stores h source s base address op x y
    pc live large represented destination fits left right mask native
  obtain ⟨n, _, trace⟩ := run_has_trace widthConstant ((algorithm op).program wide) 4 s
  have hc := runs_cost trace
  have eq : n = 4 := by omega
  subst n
  exact ⟨_, trace, halted, result, frame⟩

end WordRAM.Conjectures.SimulationStore

/-! Linking uniform source subroutines with verified additive execution cost. -/
namespace WordRAM.Conjectures.SourceChain

/-- Replace the first subroutine's halts by jumps to the relocated second one. -/
def code (first second : List SourceInstruction) : List SourceInstruction :=
  first.map (SourceInstruction.returnTo first.length) ++
    second.map (SourceInstruction.relocate first.length)

def resume (s : State w) : State w := { s with pc := 0, halted := false }

@[simp] theorem length (first second : List SourceInstruction) :
    (code first second).length = first.length + second.length := by simp [code]

/-- The source transformation is independent of width and input. Both complete
traces are preserved, including their sum of instruction costs. -/
theorem traces (first second : List SourceInstruction) (s middle final : State w)
    (n m : Nat) (live : s.halted = false) (halted : middle.halted = true)
    (left : Runs widthConstant (first.map (SourceInstruction.compile w)) n s middle)
    (right : Runs widthConstant (second.map (SourceInstruction.compile w)) m (resume middle) final) :
    Runs widthConstant ((code first second).map (SourceInstruction.compile w)) (n + m)
      s (final.relocate first.length) := by
  have left' := (left.returnTo first.length).append_code
    ((second.map (SourceInstruction.compile w)).map (Instruction.relocate first.length))
  have start : s.returnTo first.length = s := by simp [State.returnTo, live]
  have meet : middle.returnTo first.length = (resume middle).relocate first.length := by
    simp [State.returnTo, State.relocate, resume, halted]
  have embed := embeds_append
    ((first.map (SourceInstruction.compile w)).map (Instruction.returnTo first.length))
    (second.map (SourceInstruction.compile w)) []
  simp only [List.length_map, List.append_nil] at embed
  have right' := right.relocate embed
  rw [start, meet] at left'
  have result := left'.append right'
  simpa only [code, List.map_append, List.map_map, Function.comp_def,
    compile_returnTo, compile_relocate] using result

end WordRAM.Conjectures.SourceChain