SETH ⇒ OVC sparsification bundle 42: 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_41

set_option autoImplicit true

/-! Serialize a whole leaf table into length-prefixed canonical clauses. -/
namespace WordRAM.Conjectures.Sparsification.TableSerialize

def words (w : Width) (formula : CNF n) : List (Word w) :=
  formula.flatMap fun clause =>
    BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)

theorem length_le (formula : CNF n) : (words w formula).length ≤ formula.length * (1 + 4 * n) := by
  induction formula with
  | nil => simp [words]
  | cons clause rest ih =>
    have bound : (Canonical.clause clause).length ≤ 2 * n := by
      have h := List.length_filter_le (fun literal => decide (literal ∈ clause)) (Counting.literals n)
      simpa only [Canonical.clause, Counting.literals_length] using h
    simp only [words, List.flatMap_cons, List.length_append, List.length_cons,
      SerializedWords.literals_length, Nat.add_mul, Nat.one_mul] at *
    omega

def Invariant (target : List (Word w)) (initial : Memory w) (original budget : Nat) (n fuel : Nat) (mem : Memory w) : Prop :=
  ∃ (rest : CNF n) (written : List (Word w)) (source destination : Nat),
    rest.length = fuel ∧ (∀ clause ∈ rest, clause.Nodup) ∧
    32 ≤ source ∧ source + 3 * rest.length ≤ destination ∧
    destination + rest.length * (1 + 4 * n) ≤ budget ∧
    VectorBuilder.Stored mem source (RecordTable.words w rest) ∧
    VectorBuilder.Stored mem original written ∧ written ++ words w rest = target ∧ original + written.length = destination ∧
    mem 11 = BitVec.ofNat w.bits fuel ∧ mem 12 = BitVec.ofNat w.bits source ∧
    mem 13 = BitVec.ofNat w.bits destination ∧ mem 16 = BitVec.ofNat w.bits n ∧
    (∀ a, 32 ≤ a → (a < original ∨ destination ≤ a) → mem a = initial a)

theorem guard {target : List (Word w)} (h : Invariant target initial original budget n fuel (mem : Memory w)) (fits : budget < 2 ^ w.bits) :
    mem 11 = 0#w.bits ↔ fuel = 0 := by
  obtain ⟨rest, written, source, destination, len, _, _, before, space, _, _, _, _, count, _⟩ := h
  have fuelFits : fuel < 2 ^ w.bits := by omega
  rw [count]
  constructor
  · intro eq
    have values := congrArg BitVec.toNat eq
    simpa only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt fuelFits, Nat.zero_mod] using values
  · intro eq; simp [eq]

set_option maxRecDepth 4096 in
theorem iteration (original budget : Nat) (target : List (Word w)) (initial : Memory w)
    (base : 32 ≤ original) (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (fuel : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (h : Invariant target initial original budget n (fuel + 1) s.mem) :
    ∃ time final, time ≤ 22 * n + 27 ∧ Runs widthConstant (SerializeBody.algorithm.program w) time s final ∧
      final.halted = true ∧ Invariant target initial original budget n fuel final.mem := by
  obtain ⟨rest, written, source, destination, len, nodup, sourceBase, before, space, input,
    prior, order, cursor, count, pointer, output, variables, oldFrame⟩ := h
  cases rest with
  | nil => simp at len
  | cons clause rest =>
    have clauseNodup := nodup clause (by simp)
    have clauseBound : clause.length ≤ 2 * n := by
      have h := clauseNodup.length_le_of_subset (l₂ := Counting.literals n) (fun literal _ => Counting.mem_literals literal)
      simpa only [Counting.literals_length] using h
    have remaining : rest.length = fuel := by simp only [List.length_cons] at len; omega
    have room : destination + 1 + 4 * n < 2 ^ w.bits := by
      simp only [List.length_cons, Nat.add_mul, Nat.one_mul] at space
      omega
    obtain ⟨time, final, bound, trace, halted, table, tail, fc, fp, fd, fv, frame⟩ :=
      SerializeBody.serializes clause rest source destination s pc live sourceBase before room variablesFit clauseNodup
        input variables (by simpa only [remaining] using count) pointer output
    let current := BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)
    have currentLength : current.length = 1 + 2 * clause.length := by
      simp only [current, List.length_cons, SerializedWords.canonical_length clause clauseNodup]; omega
    have kept : VectorBuilder.Stored final.mem original written := by
      apply MemoryCopy.stored_frame _ _ prior
      intro a ha hb
      exact frame a (by omega) (Or.inl (by omega))
    have appended : VectorBuilder.Stored final.mem original (written ++ current) := by
      apply (BranchTables.stored_append written current final.mem original).mpr
      exact ⟨kept, by rw [cursor]; exact table⟩
    refine ⟨time, final, bound, trace, halted, rest, written ++ current, source + 3,
      destination + 1 + 2 * clause.length, remaining, ?_, by omega, ?_, ?_, tail, appended, ?_, ?_, ?_, fp, fd, fv, ?_⟩
    · intro c member; exact nodup c (by simp [member])
    · simp only [List.length_cons] at before; omega
    · simp only [List.length_cons, Nat.add_mul, Nat.one_mul] at space
      omega
    · simpa only [words, List.flatMap_cons, List.append_assoc, current] using order
    · rw [List.length_append, currentLength]; omega
    · simpa only [remaining] using fc
    · intro a ha outside
      exact (frame a ha (by omega)).trans (oldFrame a ha (by omega))

def algorithm : Algorithm := SourceWhile.algorithm 11 SerializeBody.algorithm.code

/-- The entire clause table is serialized by one uniform wordRAM program. -/
theorem serializes (formula : CNF n) (source destination budget : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
    (before : source + 3 * formula.length ≤ destination)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (space : destination + formula.length * (1 + 4 * n) ≤ budget)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (output : s.mem 13 = BitVec.ofNat w.bits destination) :
    ∃ time final, time ≤ formula.length * (22 * n + 29) + 2 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination (words w formula) ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + (words w formula).length) ∧
      final.mem 11 = 0#w.bits ∧ final.mem 16 = BitVec.ofNat w.bits n ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + (words w formula).length ≤ a) → final.mem a = s.mem a) := by
  have initial : Invariant (words w formula) s.mem destination budget n formula.length s.mem :=
    ⟨formula, [], source, destination, rfl, nodup, base, before, space, input, trivial, rfl, by simp,
      count, pointer, output, variables, fun _ _ _ => rfl⟩
  obtain ⟨time, final, bound, trace, halted, invariant, zero⟩ :=
    SourceWhile.loops 11 SerializeBody.algorithm.code (22 * n + 27)
      (Invariant (words w formula) s.mem destination budget n)
      (fun _ _ h => guard h fits)
      (iteration destination budget (words w formula) s.mem (by omega) fits variablesFit)
      formula.length s pc live initial
  obtain ⟨rest, written, src, dst, len, _, _, _, _, _, table, order, cursor, _, _, output', variables', frame⟩ := invariant
  have empty : rest = [] := List.length_eq_zero_iff.mp len
  subst rest
  simp only [words, List.flatMap_nil, List.append_nil] at order
  subst written
  rw [← cursor] at output' frame
  exact ⟨time, final, bound, trace, halted, table, output', zero, variables', frame⟩

end WordRAM.Conjectures.Sparsification.TableSerialize

/-! Serialize a leaf table into the exact public SAT instance encoding. -/
namespace WordRAM.Conjectures.Sparsification.SATSerialize
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def header : Algorithm :=
  ⟨[.copy (.indirect 13) (reg 16), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.indirect 13) (reg 11), .binary .add (.direct 13) (reg 13) (.immediate 1), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code header.code TableSerialize.algorithm.code, 1, by decide⟩

theorem encoding (formula : CNF n) :
    (SATInstance.mk n (Canonical.formula formula)).encode.map (BitVec.ofNat w.bits) =
      [BitVec.ofNat w.bits n, BitVec.ofNat w.bits formula.length] ++ TableSerialize.words w formula := by
  have polarity (b : Bool) : BitVec.ofNat w.bits (if b then 1 else 0) = (if b then 1 else 0 : Word w) := by
    cases b <;> simp
  simp [SATInstance.encode, Canonical.formula, TableSerialize.words, SerializedWords.literals,
    MaskBuilder.wordLiteral, List.map_flatMap, List.flatMap_map, polarity]

theorem length_le (formula : CNF n) :
    (SATInstance.mk n (Canonical.formula formula)).encode.length ≤ 2 + formula.length * (1 + 4 * n) := by
  have h := congrArg List.length (encoding (w := ⟨1, by decide⟩) formula)
  have bound := TableSerialize.length_le (w := ⟨1, by decide⟩) formula
  simp only [List.length_map, List.length_append, List.length_cons, List.length_nil] at h
  omega

theorem writes_header (s : State w) (destination : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 32 ≤ destination) (fits : destination + 1 < 2 ^ w.bits)
    (pointer : s.mem 13 = BitVec.ofNat w.bits destination) :
    let t := run widthConstant (header.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 13 = BitVec.ofNat w.bits (destination + 2) ∧
      t.mem destination = s.mem 16 ∧ t.mem (destination + 1) = s.mem 11 ∧
      (∀ a, a ≠ 13 → a ≠ destination → a ≠ destination + 1 → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits destination).toNat = destination := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits destination + 1#w.bits).toNat = destination + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low0 : ∀ i, i ≤ 31 → destination ≠ i ∧ i ≠ destination := by omega
  have low1 : ∀ i, i ≤ 31 → destination + 1 ≠ i ∧ i ≠ destination + 1 := by omega
  simp [header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, d0, d1, low0, low1,
    Nat.add_assoc, -BitVec.toNat_add]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h13 h0 h1; simp [h13, h0, h1]

/-- The output is the exact input of the SAT solver on a satisfiability-equivalent
canonical formula. No encoding conversion is hidden in a solver oracle. -/
theorem serializes (formula : CNF n) (source destination budget : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
    (before : source + 3 * formula.length ≤ destination)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (space : destination + 2 + formula.length * (1 + 4 * n) ≤ budget)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (output : s.mem 13 = BitVec.ofNat w.bits destination) :
    ∃ time final, time ≤ formula.length * (22 * n + 29) + 7 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination ((SATInstance.mk n (Canonical.formula formula)).encode.map (BitVec.ofNat w.bits)) ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + (SATInstance.mk n (Canonical.formula formula)).encode.length) ∧
      final.mem 11 = 0#w.bits ∧ final.mem 16 = BitVec.ofNat w.bits n ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + (SATInstance.mk n (Canonical.formula formula)).encode.length ≤ a) →
        final.mem a = s.mem a) := by
  let prepared := run widthConstant (header.program w) 5 s
  obtain ⟨ph, pt, pd, hv, hc, pf⟩ := writes_header s destination pc live (by omega) (by omega) output
  have preparedInput : VectorBuilder.Stored prepared.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact pf a (by omega) (by omega) (by omega)
  obtain ⟨time, out, bound, trace, halted, table, cursor, zero, vars, frame⟩ :=
    TableSerialize.serializes formula source (destination + 2) budget (SourceChain.resume prepared) rfl rfl base
      (by omega) fits variablesFit space nodup preparedInput
      ((pf 16 (by decide) (by omega) (by omega)).trans variables)
      ((pf 11 (by decide) (by omega) (by omega)).trans count)
      ((pf 12 (by decide) (by omega) (by omega)).trans pointer) pd
  have first : out.mem destination = BitVec.ofNat w.bits n :=
    (frame destination (by omega) (Or.inl (by omega))).trans (hv.trans variables)
  have second : out.mem (destination + 1) = BitVec.ofNat w.bits formula.length :=
    (frame (destination + 1) (by omega) (Or.inl (by omega))).trans (hc.trans count)
  have complete : VectorBuilder.Stored out.mem destination
      ((SATInstance.mk n (Canonical.formula formula)).encode.map (BitVec.ofNat w.bits)) := by
    rw [encoding]
    exact ⟨first, second, table⟩
  have length : (SATInstance.mk n (Canonical.formula formula)).encode.length = 2 + (TableSerialize.words w formula).length := by
    have h := congrArg List.length (encoding (w := w) formula)
    simp only [List.length_map, List.length_append, List.length_cons, List.length_nil] at h
    omega
  obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant (header.program w) 5 s
  have cost := runs_cost setupTrace
  have eq : ticks = 5 := by omega
  subst ticks
  have full := SourceChain.traces header.code TableSerialize.algorithm.code s prepared out 5 time live ph setupTrace trace
  refine ⟨5 + time, out.relocate header.code.length, by omega, full, halted, complete, ?_, zero, vars, ?_⟩
  · simpa only [length, Nat.add_assoc, State.relocate] using cursor
  · intro a ha outside
    rw [length] at outside
    exact (frame a ha (by omega)).trans (pf a (by omega) (by omega) (by omega))

end WordRAM.Conjectures.Sparsification.SATSerialize

/-! Solver simulation for arbitrary extra-width parameters, including SAT's
variable-count parameter. The original OV interface remains unchanged. -/
namespace WordRAM.Conjectures.ParameterizedSimulation
open SimulationMemory SimulationExecution SimulationInterface
variable {narrow wide : Width}

/-- The actual word-size convention guarantees the input-fit premise. -/
theorem solver_initial_memory (solver : Algorithm) (input : List Nat) (extra : Nat)
    (h : (solver.width input extra).bits ≤ wide.bits) (address : Nat) :
    (initialState wide input).mem address =
      WidthSimulation.lift wide ((initialState (solver.width input extra) input).mem address) := by
  exact initial_memory input h (fun value member => encoded_value_fits solver input extra value member) address

/-- Given prepared base/mask/width registers, the wide serialized input
establishes the full invariant required by the arbitrary-trace theorem. -/
theorem ready (solver : Algorithm) (input : List Nat) (extra : Nat) (host : State wide) (base : Nat)
    (h : (solver.width input extra).bits ≤ wide.bits)
    (memory : ∀ address, host.mem (base + address) = (initialState wide input).mem address)
    (pointer : host.mem 24 = BitVec.ofNat wide.bits base)
    (mask : host.mem 30 = WidthSimulation.mask (solver.width input extra) wide)
    (native : host.mem 31 = WidthSimulation.lift wide
      (BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)))
    (pc : host.pc = 0) (live : host.halted = false) :
    Related (initialState (solver.width input extra) input) host base := by
  refine ⟨?_, pointer, mask, native, live, fun _ => pc⟩
  intro address
  rw [memory]
  exact solver_initial_memory solver input extra h address

end WordRAM.Conjectures.ParameterizedSimulation

/-! Compute the solver width with the extra-bit parameter required by SAT. -/
namespace WordRAM.Conjectures.ExtraWidthSetup

private def reg (cell : Nat) : SourceOperand := .memory (.direct cell)

def addExtra : Algorithm :=
  ⟨[.binary .add (.direct 26) (reg 16) (reg 26), .halt], 1, by decide⟩

def algorithm (factor : Nat) : Algorithm :=
  ⟨SourceChain.code addExtra.code (SolverSetupParts.widthAlgorithm factor).code, 1, by decide⟩

theorem adds (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (addExtra.program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 26 = s.mem 16 + s.mem 26 ∧
      (∀ a, a ≠ 26 → t.mem a = s.mem a) := by
  simp [addExtra, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, Nat.add_assoc]
  intro a h; simp [h]

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time; exact trace

/-- Construct the narrow-width native constant and truncation mask from the
actual extra-bit and logarithm registers, counting all nine instructions. -/
theorem prepares (narrow wide : Width) (s : State wide) (factor extra logarithm : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (width : narrow.bits ≤ wide.bits)
    (formula : narrow.bits = factor * (extra + logarithm + 1))
    (extraInput : s.mem 16 = BitVec.ofNat wide.bits extra)
    (logInput : s.mem 26 = BitVec.ofNat wide.bits logarithm) :
    ∃ final, Runs widthConstant ((algorithm factor).program wide) 9 s final ∧ final.halted = true ∧
      final.mem 31 = WidthSimulation.lift wide (BitVec.ofNat narrow.bits narrow.bits : Word narrow) ∧
      final.mem 30 = WidthSimulation.mask narrow wide ∧
      (∀ a, a ≠ 26 → a ≠ 27 → a ≠ 30 → a ≠ 31 → final.mem a = s.mem a) := by
  let added := run widthConstant (addExtra.program wide) 2 s
  obtain ⟨ah, aticks, av, af⟩ := adds s pc live
  have value : added.mem 26 = BitVec.ofNat wide.bits (extra + logarithm) := by
    rw [av, extraInput, logInput, ← BitVec.ofNat_add]
  let out := run widthConstant ((SolverSetupParts.widthAlgorithm factor).program wide) 7 (SourceChain.resume added)
  obtain ⟨halted, ticks, native, mask, frame⟩ := SolverSetupParts.width_run narrow wide
    (SourceChain.resume added) factor (extra + logarithm) rfl rfl width formula value
  have trace := SourceChain.traces addExtra.code (SolverSetupParts.widthAlgorithm factor).code s added out 2 7
    live ah (trace_of_ticks _ _ 2 aticks) (trace_of_ticks _ _ 7 ticks)
  refine ⟨out.relocate addExtra.code.length, trace, halted, native, mask, ?_⟩
  intro a h26 h27 h30 h31
  exact (frame a h27 h30 h31).trans (af a h26)

def fromMagnitude (solver : Algorithm) : Algorithm :=
  ⟨SourceChain.code LogarithmMachine.algorithm.code (algorithm solver.wordFactor).code, 1, by decide⟩

/-- From the exact input magnitude and extra-width registers, compute the
solver's actual word convention and mask. The magnitude scan is separate. -/
theorem computes (solver : Algorithm) (input : List Nat) (extra : Nat) (s : State wide)
    (pc : s.pc = 0) (live : s.halted = false) (large : 2 ≤ wide.bits)
    (width : (solver.width input extra).bits ≤ wide.bits)
    (magnitude : s.mem 25 = BitVec.ofNat wide.bits (inputMagnitude input))
    (zero : s.mem 26 = 0#wide.bits) (extraInput : s.mem 16 = BitVec.ofNat wide.bits extra) :
    ∃ final, Runs widthConstant ((fromMagnitude solver).program wide)
        (4 * (inputMagnitude input).log2 + 11) s final ∧ final.halted = true ∧
      final.mem 31 = WidthSimulation.lift wide
        (BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)) ∧
      final.mem 30 = WidthSimulation.mask (solver.width input extra) wide ∧
      (∀ a, a ≠ 25 → a ≠ 26 → a ≠ 27 → a ≠ 30 → a ≠ 31 → final.mem a = s.mem a) := by
  have logBound : (inputMagnitude input).log2 + 1 ≤ (solver.width input extra).bits := by
    have h := Nat.le_mul_of_pos_left (extra + (inputMagnitude input).log2 + 1) solver.wordFactor_pos
    change _ ≤ solver.wordFactor * (extra + (inputMagnitude input).log2 + 1)
    omega
  have magnitudeFits : inputMagnitude input < 2 ^ wide.bits :=
    Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (Nat.le_trans logBound width))
  obtain ⟨logged, logTrace, logHalt, logValue, logFrame⟩ :=
    LogarithmMachine.computes (inputMagnitude input) 0 s pc live large magnitudeFits
      (by have := Nat.log2_le_self (inputMagnitude input); omega) magnitude zero
  obtain ⟨out, trace, halted, native, mask, frame⟩ := prepares (solver.width input extra) wide
    (SourceChain.resume logged) solver.wordFactor extra (inputMagnitude input).log2 rfl rfl width rfl
      ((logFrame 16 (by decide) (by decide)).trans extraInput) (by simpa only [Nat.zero_add, SourceChain.resume] using logValue)
  have full := SourceChain.traces LogarithmMachine.algorithm.code (algorithm solver.wordFactor).code s logged out
    (4 * (inputMagnitude input).log2 + 2) 9 live logHalt logTrace trace
  refine ⟨out.relocate LogarithmMachine.algorithm.code.length, ?_, halted, native, mask, ?_⟩
  · simpa [fromMagnitude, Algorithm.program, Nat.add_assoc] using full
  · intro a h25 h26 h27 h30 h31
    exact (frame a h26 h27 h30 h31).trans (logFrame a h25 h26)

end WordRAM.Conjectures.ExtraWidthSetup

/-! The write-block simulation also preserves caller data outside its one translated write. -/
namespace WordRAM.Conjectures.BoundedInstruction
open SimulationMemory SimulationInstruction
variable {narrow wide : Width}

theorem simulates (h : narrow.bits ≤ wide.bits) (source : State narrow)
    (s : State wide) (base : Nat) (instruction : SourceInstruction) (spec : WriteSpec)
    (decoded : decode instruction = some spec)
    (pc : s.pc = 0) (live : s.halted = false) (large : 32 ≤ base)
    (represented : Represents source.mem 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 spec.left wide)
    (yfits : SimulationOperand.FixedFits base spec.right wide)
    (dfits : base + staticCell spec.destination < 2 ^ wide.bits)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    cost spec ≤ 18 ∧ ∃ final,
      Runs widthConstant ((algorithm spec).program wide) (cost spec) s final ∧
      final.halted = true ∧
      Represents (execute widthConstant (instruction.compile narrow) source).mem final.mem base ∧
      final.mem 24 = s.mem 24 ∧ final.mem 30 = s.mem 30 ∧ final.mem 31 = s.mem 31 ∧
      (∀ a, 32 ≤ a → a ≠ base + spec.destination.resolve source.mem → final.mem a = s.mem a) := by
  obtain ⟨bound, final, trace, halted, memory, frame⟩ := SimulationWrite.simulates h source.mem s base
    spec.operation spec.destination spec.left spec.right pc live large represented pointer mask native
    xfits yfits dfits dynamic
  refine ⟨bound, final, trace, halted, ?_, ?_, ?_, ?_, ?_⟩
  · rw [← decode_source instruction spec decoded, execute_memory]
    exact memory
  · exact frame 24 (Or.inl (by decide)) (by omega)
  · exact frame 30 (Or.inr (by decide)) (by omega)
  · exact frame 31 (Or.inr (by decide)) (by omega)

  · intro a ha hb
    exact frame a (Or.inr (by omega)) (by omega)

end WordRAM.Conjectures.BoundedInstruction