SETH ⇒ OVC sparsification bundle 43: 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_42

set_option autoImplicit true

/-! A finite region bounds both indirect writes and arbitrary fixed direct
addresses in a compiled solver, even when those exceed the narrow word range. -/
namespace WordRAM.Conjectures.SimulationFootprint
open SimulationMemory SimulationInstruction

def span (narrow : Width) (program : List SourceInstruction) : Nat :=
  max (2 ^ narrow.bits) (SimulationBounds.programBound program + 1)

theorem destination_bound (instruction : SourceInstruction) (spec : WriteSpec)
    (decoded : decode instruction = some spec) :
    staticCell spec.destination ≤ SimulationBounds.instructionBound instruction := by
  rw [← decode_source instruction spec decoded]
  cases spec with
  | mk op dst x y => cases op <;> simp [WriteSpec.source, SimulationBounds.instructionBound] <;> omega

theorem resolves (narrow : Width) (program : List SourceInstruction) (instruction : SourceInstruction)
    (spec : WriteSpec) (mem : Memory narrow)
    (member : instruction ∈ program) (decoded : decode instruction = some spec) :
    spec.destination.resolve mem < span narrow program := by
  have bound := Nat.le_trans (destination_bound instruction spec decoded) (SimulationBounds.member_bound program instruction member)
  cases addr : spec.destination with
  | direct cell =>
    simp only [addr, staticCell] at bound
    simp only [Address.resolve]
    unfold span; omega
  | indirect cell =>
    have dynamic := (mem cell).isLt
    simp only [Address.resolve]
    unfold span; omega

private theorem fold_ge (xs : List Nat) (seed : Nat) : seed ≤ xs.foldl max seed := by
  induction xs generalizing seed with
  | nil => simp
  | cons x xs ih => exact Nat.le_trans (Nat.le_max_left seed x) (ih (max seed x))

/-- The zero output cell and the whole serialized input fit inside the region
reserved for the narrow solver, including the empty-input boundary case. -/
theorem input_length (solver : Algorithm) (input : List Nat) (extra : Nat) :
    1 + input.length ≤ span (solver.width input extra) solver.code := by
  have seed := fold_ge input input.length
  have magnitude : input.length < inputMagnitude input := by unfold inputMagnitude; omega
  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 fits := Nat.lt_of_lt_of_le (Nat.lt_log2_self (n := inputMagnitude input))
    (Nat.pow_le_pow_right (by decide : 0 < 2) logBound)
  unfold span; omega

end WordRAM.Conjectures.SimulationFootprint

/-! Complete compiled executions preserve caller memory outside a finite
translated region, allowing older tables and a fresh zero tail to coexist. -/
namespace WordRAM.Conjectures.SimulationBounded
open SimulationMemory SimulationCompiler SimulationExecution
variable {narrow wide : Width}

def Preserved (before after : Memory wide) (base limit : Nat) : Prop :=
  ∀ a, 32 ≤ a → (a < base ∨ limit ≤ a) → after a = before a

private theorem write_control (spec : SimulationInstruction.WriteSpec) (s : State narrow) :
    (execute widthConstant (spec.source.compile narrow) s).pc = s.pc + 1 ∧
    (execute widthConstant (spec.source.compile narrow) s).halted = s.halted := by
  cases spec with
  | mk op dst x y => cases op <;> exact ⟨rfl, rfl⟩

private theorem write_tail (spec : SimulationInstruction.WriteSpec) (pc : Nat) :
    tail pc spec.source = [.jump (stride * (pc + 1))] := by
  cases spec with
  | mk op dst x y => cases op <;> rfl

/-- Each writing instruction in the full compiled program takes at most 19
steps, including its final transfer to the next source instruction. -/
theorem write_step (h : narrow.bits ≤ wide.bits) (program : List SourceInstruction)
    (source : State narrow) (host : State wide) (base : Nat) (pc : Fin program.length)
    (sourcePC : source.pc = pc.val) (live : source.halted = false)
    (related : Related source host base) (large : 32 ≤ base)
    (spec : SimulationInstruction.WriteSpec) (decoded : SimulationInstruction.decode program[pc.val] = some spec)
    (fits : Fits base wide program[pc.val])
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    ∃ n, n ≤ 19 ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related (execute widthConstant (program[pc.val].compile narrow) source) final base ∧
      Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  have fits' : SimulationOperand.FixedFits base spec.left wide ∧
      SimulationOperand.FixedFits base spec.right wide ∧ base + staticCell spec.destination < 2 ^ wide.bits := by
    simpa only [Fits, decoded] using fits
  obtain ⟨bound, built, trace, halted, memory, bp, bm, bn, writeFrame⟩ := BoundedInstruction.simulates h source
    (SourceChain.resume host) base program[pc.val] spec decoded rfl rfl large related.memory
    related.pointer related.mask related.native fits'.1 fits'.2.1 fits'.2.2 dynamic
  have bodyEq : body program[pc.val] = (SimulationInstruction.algorithm spec).code := by simp [body, decoded]
  obtain ⟨ready, readyTrace, readyPC, readyLive, readyMem⟩ := call_body program pc host built _
    (by rw [related.pc live, sourcePC]) (related.halted.trans live) halted (by simpa only [bodyEq, Algorithm.program] using trace)
  have tailEq : tail pc.val program[pc.val] = [.jump (stride * (pc.val + 1))] := by
    rw [← SimulationInstruction.decode_source _ spec decoded]
    exact write_tail spec pc.val
  have fetch : ((code program).map (SourceInstruction.compile wide))[ready.pc]? =
      some (.jump (stride * (pc.val + 1))) := by
    have hh := tail_fetch program pc wide 0 (by rw [tailEq]; simp)
    simpa only [tailEq, List.map_cons, List.map_nil, SourceInstruction.compile, List.getElem?_cons_zero,
      Nat.add_zero, ← readyPC] using hh
  have last := runs_instruction widthConstant ((code program).map (SourceInstruction.compile wide)) ready
    (.jump (stride * (pc.val + 1))) readyLive fetch
  have ctrl := write_control spec source
  rw [SimulationInstruction.decode_source _ spec decoded] at ctrl
  refine ⟨SimulationInstruction.cost spec + 1, by omega, _, readyTrace.append last, ?_⟩
  constructor
  · constructor
    · simpa only [execute, readyMem] using memory
    · simpa only [execute, readyMem] using bp.trans related.pointer
    · simpa only [execute, readyMem] using bm.trans related.mask
    · simpa only [execute, readyMem] using bn.trans related.native
    · rw [ctrl.2]; exact readyLive.trans live.symm
    · intro _
      rw [ctrl.1, sourcePC]; rfl
  · intro a ha hb
    change ready.mem a = host.mem a
    rw [readyMem]
    have bound := SimulationFootprint.resolves narrow program program[pc.val] spec source.mem (List.getElem_mem _) decoded
    exact writeFrame a ha (by omega)

private theorem branch_tail (program : Program wide .multiplication 1) (s : State wide)
    (condition : Bool) (taken next : Nat) (live : s.halted = false)
    (value : s.mem 29 = if condition then 1 else 0)
    (first : program[s.pc]? = some (.branch .eq (.memory (.direct 29)) (.immediate (1#wide.bits)) taken))
    (second : program[s.pc + 1]? = some (.jump next)) :
    ∃ n, n ≤ 2 ∧ ∃ final, Runs widthConstant program n s final ∧
      final.halted = false ∧ final.pc = (if condition then taken else next) ∧ final.mem = s.mem := by
  have positive : wide.bits ≠ 0 := by have := wide.positive; omega
  let fuel := if condition then 1 else 2
  have result :
      let final := run widthConstant program fuel s
      final.halted = false ∧ final.ticks = s.ticks + fuel ∧
      final.pc = (if condition then taken else next) ∧ final.mem = s.mem := by
    cases condition <;>
      simp [fuel, run, step, first, second, execute, live, Operand.read, Address.resolve,
        Comparison.test, value, positive, Nat.add_assoc]
  obtain ⟨halted, ticks, pc, memory⟩ := result
  obtain ⟨n, _, trace⟩ := run_has_trace widthConstant program fuel s
  have hc := runs_cost trace
  have eq : n = fuel := by omega
  subst n
  refine ⟨fuel, ?_, _, trace, halted, pc, memory⟩
  unfold fuel; split <;> omega

/-- Conditional branches execute a complete comparison body and an absolute
control transfer, preserving the simulation invariant in either direction. -/
theorem branch_step (h : narrow.bits ≤ wide.bits) (program : List SourceInstruction)
    (source : State narrow) (host : State wide) (base : Nat) (pc : Fin program.length)
    (sourcePC : source.pc = pc.val) (live : source.halted = false)
    (related : Related source host base) (large : 32 ≤ base)
    (cmp : Comparison) (x y : SourceOperand) (target : Nat)
    (instruction : program[pc.val] = .branch cmp x y target)
    (fits : Fits base wide program[pc.val])
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits) :
    ∃ n, n ≤ 19 ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related (execute widthConstant (program[pc.val].compile narrow) source) final base ∧
      Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  have fits' : SimulationOperand.FixedFits base x wide ∧ SimulationOperand.FixedFits base y wide := by
    simpa only [Fits, instruction, SimulationInstruction.decode] using fits
  obtain ⟨bound, built, trace, halted, memory, value, frame⟩ := SimulationCompare.simulates h source.mem
    (SourceChain.resume host) base cmp x y rfl rfl large related.memory related.pointer related.mask
    fits'.1 fits'.2 dynamic
  have bodyEq : body program[pc.val] = (SimulationCompare.algorithm cmp x y).code := by
    simp [body, instruction, SimulationInstruction.decode]
  obtain ⟨ready, readyTrace, readyPC, readyLive, readyMem⟩ := call_body program pc host built _
    (by rw [related.pc live, sourcePC]) (related.halted.trans live) halted
    (by simpa only [bodyEq, Algorithm.program] using trace)
  rw [instruction] at readyPC
  have first : ((code program).map (SourceInstruction.compile wide))[ready.pc]? =
      some (.branch .eq (.memory (.direct 29)) (.immediate (1#wide.bits)) (stride * target)) := by
    have hh := tail_fetch program pc wide 0 (by simp [instruction, tail])
    simpa only [instruction, tail, List.map_cons, List.map_nil, SourceInstruction.compile, SourceOperand.compile,
      List.getElem?_cons_zero, Nat.add_zero, ← readyPC] using hh
  have second : ((code program).map (SourceInstruction.compile wide))[ready.pc + 1]? =
      some (.jump (stride * (pc.val + 1))) := by
    have hh := tail_fetch program pc wide 1 (by simp [instruction, tail])
    simpa only [instruction, tail, List.map_cons, List.map_nil, SourceInstruction.compile, SourceOperand.compile,
      List.getElem?_cons_succ, List.getElem?_cons_zero, ← readyPC] using hh
  obtain ⟨n, nb, final, last, finalLive, finalPC, finalMem⟩ := branch_tail _ ready
    (cmp.test ((x.compile narrow).read source.mem) ((y.compile narrow).read source.mem))
    (stride * target) (stride * (pc.val + 1)) readyLive (by rw [readyMem]; exact value) first second
  refine ⟨SimulationCompare.cost x y + n, by omega, final, readyTrace.append last, ?_⟩
  constructor
  · constructor
    · simpa only [instruction, SourceInstruction.compile, execute, finalMem, readyMem] using memory
    · rw [finalMem, readyMem, frame 24 (Or.inl (by decide))]; exact related.pointer
    · rw [finalMem, readyMem, frame 30 (Or.inr (by decide))]; exact related.mask
    · rw [finalMem, readyMem, frame 31 (Or.inr (by decide))]; exact related.native
    · simpa only [instruction, SourceInstruction.compile, execute, live] using finalLive
    · intro _
      rw [finalPC]
      simp only [instruction, SourceInstruction.compile, execute, sourcePC]
      split <;> rfl
  · intro a ha _
    rw [finalMem, readyMem]
    exact frame a (Or.inr (by omega))

theorem jump_step (program : List SourceInstruction) (source : State narrow) (host : State wide)
    (base : Nat) (pc : Fin program.length) (sourcePC : source.pc = pc.val)
    (live : source.halted = false) (related : Related source host base)
    (target : Nat) (instruction : program[pc.val] = .jump target) :
    ∃ n, n ≤ 19 ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related (execute widthConstant (program[pc.val].compile narrow) source) final base ∧
      Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  have hostPC : host.pc = stride * pc.val := by rw [related.pc live, sourcePC]
  have fetched : ((code program).map (SourceInstruction.compile wide))[host.pc]? =
      some (.jump (stride * target)) := by
    have hh := tail_fetch program pc wide 0 (by simp [instruction, tail])
    simpa [instruction, body, SimulationInstruction.decode, tail, SourceInstruction.compile, ← hostPC] using hh
  have trace := runs_instruction widthConstant ((code program).map (SourceInstruction.compile wide))
    host (.jump (stride * target)) (related.halted.trans live) fetched
  refine ⟨1, by decide, _, trace, ?_⟩
  constructor
  · rw [instruction]
    exact ⟨related.memory, related.pointer, related.mask, related.native, related.halted, fun _ => rfl⟩
  · intro _ _ _; rfl

theorem halt_step (program : List SourceInstruction) (source : State narrow) (host : State wide)
    (base : Nat) (pc : Fin program.length) (sourcePC : source.pc = pc.val)
    (live : source.halted = false) (related : Related source host base)
    (instruction : program[pc.val] = .halt) :
    ∃ n, n ≤ 19 ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related (execute widthConstant (program[pc.val].compile narrow) source) final base ∧
      Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  have hostPC : host.pc = stride * pc.val := by rw [related.pc live, sourcePC]
  have fetched : ((code program).map (SourceInstruction.compile wide))[host.pc]? = some .halt := by
    have hh := tail_fetch program pc wide 0 (by simp [instruction, tail])
    simpa [instruction, body, SimulationInstruction.decode, tail, SourceInstruction.compile, ← hostPC] using hh
  have trace := runs_instruction widthConstant ((code program).map (SourceInstruction.compile wide))
    host .halt (related.halted.trans live) fetched
  refine ⟨1, by decide, _, trace, ?_⟩
  constructor
  · rw [instruction]
    refine ⟨related.memory, related.pointer, related.mask, related.native, rfl, ?_⟩
    intro impossible
    cases impossible
  · intro _ _ _; rfl

/-- Every successful source step is simulated; invalid fetches are not
silently converted into successful steps or accepted computations. -/
theorem step_simulates (h : narrow.bits ≤ wide.bits) (program : List SourceInstruction)
    (source next : State narrow) (host : State wide) (base : Nat)
    (related : Related source host base) (large : 32 ≤ base)
    (fits : ∀ i ∈ program, Fits base wide i)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits)
    (executed : step widthConstant (program.map (SourceInstruction.compile narrow)) source = some next) :
    ∃ n, n ≤ 19 ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related next final base ∧ Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  have live : source.halted = false := by
    cases hh : source.halted
    · rfl
    · simp [step, hh] at executed
  cases fetched : program[source.pc]? with
  | none => simp [step, live, List.getElem?_map, fetched] at executed
  | some instruction =>
    have bound : source.pc < program.length := (List.getElem?_eq_some_iff.mp fetched).1
    let pc : Fin program.length := ⟨source.pc, bound⟩
    have identity : program[pc.val] = instruction := (List.getElem?_eq_some_iff.mp fetched).2
    have eligible : Fits base wide program[pc.val] := fits _ (List.getElem_mem _)
    simp only [step, live, Bool.false_eq_true, ↓reduceIte, List.getElem?_map, fetched,
      Option.map_some, Option.some.injEq] at executed
    subst next
    rw [← identity]
    cases decoded : SimulationInstruction.decode program[pc.val] with
    | some spec => exact write_step h program source host base pc rfl live related large spec decoded eligible dynamic
    | none =>
      cases instruction with
      | copy dst src => simp [identity, SimulationInstruction.decode] at decoded
      | binary op dst x y => simp [identity, SimulationInstruction.decode] at decoded
      | bitNot dst src => simp [identity, SimulationInstruction.decode] at decoded
      | wordWidth dst => simp [identity, SimulationInstruction.decode] at decoded
      | branch cmp x y target =>
        exact branch_step h program source host base pc rfl live related large cmp x y target identity eligible dynamic
      | jump target => exact jump_step program source host base pc rfl live related target identity
      | halt => exact halt_step program source host base pc rfl live related identity

/-- An arbitrary finite source trace has a compiled trace with at most a
constant-factor instruction overhead, preserving memory, halt status and PC. -/
theorem traces (h : narrow.bits ≤ wide.bits) (program : List SourceInstruction)
    (base : Nat) (large : 32 ≤ base) (fits : ∀ i ∈ program, Fits base wide i)
    (dynamic : base + 2 ^ narrow.bits ≤ 2 ^ wide.bits)
    {source target : State narrow} {steps : Nat}
    (trace : Runs widthConstant (program.map (SourceInstruction.compile narrow)) steps source target)
    (host : State wide) (related : Related source host base) :
    ∃ n, n ≤ 19 * steps ∧ ∃ final,
      Runs widthConstant ((code program).map (SourceInstruction.compile wide)) n host final ∧
      Related target final base ∧ Preserved host.mem final.mem base (base + SimulationFootprint.span narrow program) := by
  induction trace generalizing host with
  | refl source => exact ⟨0, by omega, host, .refl host, related, fun _ _ _ => rfl⟩
  | @cons source next steps target executed rest ih =>
    obtain ⟨n, bound, middle, first, invariant, firstFrame⟩ := step_simulates h program source next host base
      related large fits dynamic executed
    obtain ⟨m, mb, final, last, finalRelated, lastFrame⟩ := ih middle invariant
    refine ⟨n + m, by omega, final, first.append last, finalRelated, ?_⟩
    intro a ha hb
    exact (lastFrame a ha hb).trans (firstFrame a ha hb)

end WordRAM.Conjectures.SimulationBounded

/-! Preserve the caller's memory through solver execution and output extraction. -/
namespace WordRAM.Conjectures.ProtectedSolverOutput
open SimulationMemory SimulationExecution SimulationInterface
variable {narrow wide : Width}

theorem decision (solver : Algorithm) (input : List Nat) (extra : Nat) (time : Nat) (answer : Prop)
    (decides : DecidesIn solver input extra time answer) (host : State wide) (base : Nat)
    (h : (solver.width input extra).bits ≤ wide.bits) (large : 32 ≤ base)
    (related : Related (initialState (solver.width input extra) input) host base)
    (fits : ∀ i ∈ solver.code, Fits base wide i)
    (dynamic : base + 2 ^ (solver.width input extra).bits ≤ 2 ^ wide.bits) :
    ∃ n, n ≤ 19 * time ∧ ∃ final,
      Runs widthConstant ((SimulationCompiler.code solver.code).map (SourceInstruction.compile wide)) n host final ∧
      final.halted = true ∧ (final.mem base = 0 ∨ final.mem base = 1) ∧
      (final.mem base = 1 ↔ answer) ∧ final.mem 24 = BitVec.ofNat wide.bits base ∧
      SimulationBounded.Preserved host.mem final.mem base
        (base + SimulationFootprint.span (solver.width input extra) solver.code) ∧
      final.mem 31 = WidthSimulation.lift wide
        (BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)) := by
  obtain ⟨source, sourceTrace, halted, boolean, correct⟩ := decides
  obtain ⟨n, bound, final, trace, result, frame⟩ := SimulationBounded.traces h solver.code base large fits dynamic sourceTrace host related
  have value : final.mem base = WidthSimulation.lift wide (source.mem 0) := by
    simpa only [Nat.add_zero] using result.memory 0
  have iffOne : final.mem base = 1 ↔ source.mem 0 = 1 := by
    rw [value]
    constructor
    · intro one
      rw [← lift_one h] at one
      have projected := congrArg (fun x : Word wide => x.setWidth (solver.width input extra).bits) one
      simpa only [WidthSimulation.project_lift h] using projected
    · intro one
      rw [one, lift_one h]
  refine ⟨n, bound, final, trace, result.halted.trans halted, ?_, iffOne.trans correct, result.pointer, frame, result.native⟩
  rcases boolean with zero | one
  · left; rw [value, zero, lift_zero]
  · right; exact iffOne.mpr one

private theorem finish (solver : Algorithm) (s : State wide)
    (pc : s.pc = (SimulationCompiler.code solver.code).length) (live : s.halted = false) :
    let final := run widthConstant ((SimulationOutput.code solver).map (SourceInstruction.compile wide)) 2 s
    final.halted = true ∧ final.ticks = s.ticks + 2 ∧ final.mem 0 = s.mem (s.mem 24).toNat ∧
      (∀ a, a ≠ 0 → final.mem a = s.mem a) := by
  have first : ((SimulationOutput.code solver).map (SourceInstruction.compile wide))[s.pc]? =
      some (.copy (.direct 0) (.memory (.indirect 24))) := by
    simp [SimulationOutput.code, SimulationOutput.suffix, pc, SourceInstruction.compile, SourceOperand.compile]
  have second : ((SimulationOutput.code solver).map (SourceInstruction.compile wide))[s.pc + 1]? = some .halt := by
    simp [SimulationOutput.code, SimulationOutput.suffix, pc, SourceInstruction.compile, SourceOperand.compile]
  simp [run, step, first, second, execute, live, Operand.read, Address.resolve, Memory.write, Nat.add_assoc]
  intro a h; simp [h]

/-- All simulated steps and output extraction are counted. This still begins
at a host state with the solver input, mask and narrow width already prepared. -/
theorem output_decision (solver : Algorithm) (input : List Nat) (extra : Nat) (time : Nat) (answer : Prop)
    (decides : DecidesIn solver input extra time answer) (host : State wide) (base : Nat)
    (h : (solver.width input extra).bits ≤ wide.bits) (large : 32 ≤ base)
    (related : Related (initialState (solver.width input extra) input) host base)
    (fits : ∀ i ∈ solver.code, Fits base wide i)
    (dynamic : base + 2 ^ (solver.width input extra).bits ≤ 2 ^ wide.bits) :
    ∃ n, n ≤ 19 * time + 2 ∧ ∃ final,
      Runs widthConstant ((SimulationOutput.code solver).map (SourceInstruction.compile wide)) n host final ∧
      final.halted = true ∧ (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ answer) ∧ SimulationBounded.Preserved host.mem final.mem base
        (base + SimulationFootprint.span (solver.width input extra) solver.code) ∧
      final.mem 31 = WidthSimulation.lift wide
        (BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)) := by
  obtain ⟨n, bound, built, trace, halted, boolean, correct, pointer, frame, native⟩ :=
    ProtectedSolverOutput.decision solver input extra time answer decides host base h large related fits dynamic
  let length := (SimulationCompiler.code solver.code).length
  let ready := built.returnTo length
  have readyPC : ready.pc = length := by simp [ready, State.returnTo, halted]
  have readyLive : ready.halted = false := by simp [ready, State.returnTo, halted]
  have readyMem : ready.mem = built.mem := by simp [ready, State.returnTo, halted]
  have hostLive : host.halted = false := related.halted
  have first : Runs widthConstant ((SimulationOutput.code solver).map (SourceInstruction.compile wide)) n host ready := by
    have hh := (trace.returnTo length).append_code (SimulationOutput.suffix.map (SourceInstruction.compile wide))
    have start : host.returnTo length = host := by simp [State.returnTo, hostLive]
    simpa only [SimulationOutput.code, List.map_append, List.map_map, Function.comp_def, compile_returnTo, start] using hh
  obtain ⟨finalHalt, ticks, value, finishFrame⟩ := finish solver ready readyPC readyLive
  have pointerValue : (ready.mem 24).toNat = base := by
    rw [readyMem, pointer]
    exact Nat.mod_eq_of_lt (by have := Nat.two_pow_pos (solver.width input extra).bits; omega)
  rw [pointerValue, readyMem] at value
  obtain ⟨m, _, last⟩ := run_has_trace widthConstant ((SimulationOutput.code solver).map (SourceInstruction.compile wide)) 2 ready
  have hc := runs_cost last
  have eq : m = 2 := by omega
  subst m
  refine ⟨n + 2, by omega, _, first.append last, finalHalt, ?_, ?_, ?_, ?_⟩
  · simpa only [value] using boolean
  · simpa only [value] using correct

  · intro a ha hb
    exact (finishFrame a (by omega)).trans (by rw [readyMem]; exact frame a ha hb)

  · exact (finishFrame 31 (by decide)).trans (by rw [readyMem]; exact native)

end WordRAM.Conjectures.ProtectedSolverOutput