SETH ⇒ OVC sparsification bundle 39: 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_38

set_option autoImplicit true

/-! A source-level while loop with an explicitly decreasing semantic measure. -/
namespace WordRAM.Conjectures.SourceWhile

private def header (cell length : Nat) : List SourceInstruction :=
  [.branch .eq (.memory (.direct cell)) (.immediate 0) (length + 2)]

private def trailer : List SourceInstruction := [.jump 0, .halt]

def algorithm (cell : Nat) (body : List SourceInstruction) : Algorithm :=
  ⟨header cell body.length ++
    (body.map (SourceInstruction.returnTo body.length)).map (SourceInstruction.relocate 1) ++ trailer, 1, by decide⟩

private theorem program_eq (w : Width) (cell : Nat) (body : List SourceInstruction) :
    (algorithm cell body).program w =
      (header cell body.length).map (SourceInstruction.compile w) ++
      ((((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length)).map (Instruction.relocate 1)) ++
        trailer.map (SourceInstruction.compile w)) := by
  simp only [algorithm, Algorithm.program, List.map_append, List.map_map, Function.comp_def,
    compile_relocate, compile_returnTo, List.append_assoc]

private theorem tail_fetch (w : Width) (cell : Nat) (body : List SourceInstruction) (i : Nat) :
    ((algorithm cell body).program w)[body.length + 1 + i]? =
      (trailer.map (SourceInstruction.compile w))[i]? := by
  rw [program_eq]
  have address : body.length + 1 + i = (body.length + i) + 1 := by omega
  rw [address]
  simp only [header, List.map_cons, List.map_nil, List.cons_append, List.nil_append, List.getElem?_cons_succ]
  rw [List.getElem?_append_right (by simp)]
  simp

theorem enters (cell : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem cell ≠ 0#w.bits) :
    let t := run widthConstant ((algorithm cell body).program w) 1 s
    t.pc = 1 ∧ t.halted = false ∧ t.ticks = s.ticks + 1 ∧ t.mem = s.mem := by
  have fetch : ((algorithm cell body).program w)[0]? =
      some (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (body.length + 2)) := by
    simp [algorithm, header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile]
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, nonzero, fetch]

theorem advances (cell : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = body.length + 1) (live : s.halted = false) :
    let t := run widthConstant ((algorithm cell body).program w) 1 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 1 ∧ t.mem = s.mem := by
  have fetch : ((algorithm cell body).program w)[body.length + 1]? = some (.jump 0) := by
    simpa [trailer, SourceInstruction.compile] using tail_fetch w cell body 0
  simp [run, step, execute, pc, live, fetch]

theorem exits (cell : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (zero : s.mem cell = 0#w.bits) :
    let t := run widthConstant ((algorithm cell body).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem = s.mem := by
  have first : ((algorithm cell body).program w)[0]? =
      some (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (body.length + 2)) := by
    simp [algorithm, header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile]
  have last : ((algorithm cell body).program w)[body.length + 2]? = some .halt := by
    simpa [trailer, SourceInstruction.compile, Nat.add_assoc] using tail_fetch w cell body 1
  simp [run, step, execute, pc, live, zero, first, last, Address.resolve, Operand.read, Comparison.test, Nat.add_assoc]

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

/-- Repeat a verified source body while the guard cell is nonzero. The semantic
measure need not be stored in a word; actual machine traces must establish its
one-step decrease. Guards, back jumps, and the final halt are counted. -/
theorem loops (cell : Nat) (body : List SourceInstruction) (cost : Nat)
    (invariant : Nat → Memory w → Prop)
    (guard : ∀ i mem, invariant i mem → (mem cell = 0#w.bits ↔ i = 0))
    (bodyCorrect : ∀ i, ∀ s : State w, s.pc = 0 → s.halted = false → invariant (i + 1) s.mem →
      ∃ time out, time ≤ cost ∧ Runs widthConstant (body.map (SourceInstruction.compile w)) time s out ∧
        out.halted = true ∧ invariant i out.mem)
    (fuel : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) (initial : invariant fuel s.mem) :
    ∃ time final, time ≤ fuel * (cost + 2) + 2 ∧ Runs widthConstant ((algorithm cell body).program w) time s final ∧
      final.halted = true ∧ invariant 0 final.mem ∧ final.mem cell = 0#w.bits := by
  induction fuel generalizing s with
  | zero =>
    have zero := (guard 0 s.mem initial).mpr rfl
    obtain ⟨halted, ticks, mem⟩ := exits cell body s pc live zero
    refine ⟨2, run widthConstant ((algorithm cell body).program w) 2 s, by simp,
      trace_of_ticks _ _ 2 ticks, halted, ?_, ?_⟩
    · rw [mem]; exact initial
    · rw [mem]; exact zero
  | succ fuel ih =>
    have nonzero : s.mem cell ≠ 0#w.bits := by
      intro h
      have impossible := (guard (fuel + 1) s.mem initial).mp h
      omega
    let head := run widthConstant ((algorithm cell body).program w) 1 s
    obtain ⟨hpc, hlive, hticks, hmem⟩ := enters cell body s pc live nonzero
    let entry : State w := { head with pc := 0 }
    have entryLive : entry.halted = false := hlive
    have entryMem : entry.mem = s.mem := hmem
    obtain ⟨bodyTime, out, bound, trace, halted, nextInvariant⟩ := bodyCorrect fuel entry rfl entryLive
      (by rw [entryMem]; exact initial)
    have embedded : EmbedsAt ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        ((algorithm cell body).program w) 1 := by
      rw [program_eq]
      exact embeds_append ((header cell body.length).map (SourceInstruction.compile w))
        ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        (trailer.map (SourceInstruction.compile w))
    let returned := (out.returnTo body.length).relocate 1
    have linked : Runs widthConstant ((algorithm cell body).program w) bodyTime head returned := by
      have h := (trace.returnTo body.length).relocate embedded
      have he : (entry.returnTo body.length).relocate 1 = head := by
        simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
        change { head with pc := 1 } = head
        have hpc' : head.pc = 1 := hpc
        rw [← hpc']
      simpa only [he] using h
    have rmem : returned.mem = out.mem := by simp [returned, State.returnTo, State.relocate, halted]
    have rpc : returned.pc = body.length + 1 := by simp [returned, State.returnTo, State.relocate, halted, Nat.add_comm]
    have rlive : returned.halted = false := by simp [returned, State.returnTo, State.relocate, halted]
    obtain ⟨npc, nlive, nticks, nmem⟩ := advances cell body returned rpc rlive
    let next := run widthConstant ((algorithm cell body).program w) 1 returned
    have nextMem : next.mem = out.mem := nmem.trans rmem
    obtain ⟨time, final, timeBound, finalTrace, finalHalt, finalInvariant, finalZero⟩ :=
      ih next npc nlive (by rw [nextMem]; exact nextInvariant)
    refine ⟨1 + bodyTime + 1 + time, final, ?_,
      (((trace_of_ticks _ _ 1 hticks).append linked).append (trace_of_ticks _ _ 1 nticks)).append finalTrace,
      finalHalt, finalInvariant, finalZero⟩
    simp only [Nat.add_mul, Nat.one_mul]
    omega

end WordRAM.Conjectures.SourceWhile

/-! Formula and work invariants preserved by every DFS transition. -/
namespace WordRAM.Conjectures.Sparsification.TraversalFacts

structure Ready (k capacity : Nat) (formula : CNF n) : Prop where
  normalized : Normalize.normalize formula = formula
  nonempty : [] ∉ formula
  width : ∀ clause ∈ formula, clause.length ≤ k
  weight : Sparsification.weight formula ≤ capacity

theorem Ready.nodup (h : Ready k capacity formula) : ∀ clause ∈ formula, clause.Nodup := by
  simpa only [h.normalized] using Normalize.normalize_nodup_literals formula

theorem Ready.length (h : Ready k capacity formula) : formula.length ≤ capacity := by
  apply Nat.le_trans (Counting.length_le_weight formula _) h.weight
  intro clause member eq
  exact h.nonempty (eq ▸ member)

theorem Ready.children (h : Ready k capacity formula) (threshold : Nat → Nat)
    (large : ∀ i, 2 ≤ threshold i)
    (selected : Selection.select formula threshold k = some (size, core)) :
    Ready k capacity (Branch.left formula core size) ∧ Ready k capacity (Branch.right formula core size) := by
  have sound := Selection.select_sound formula threshold k selected
  have small := Branch.smaller formula core size sound.1.1 h.nodup sound.1.2.1
    (Nat.le_trans (large _) sound.1.2.2.2)
  have nonempty := Work.children_no_empty formula threshold k h.nodup h.nonempty selected
  have widths := Branch.width formula core size k h.width (by have := sound.1.2.2.1; omega)
  exact ⟨⟨Normalize.normalize_idempotent _, nonempty.1, widths.1, by have := h.weight; omega⟩,
    ⟨Normalize.normalize_idempotent _, nonempty.2, widths.2, by have := h.weight; omega⟩⟩

theorem calls_positive (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    0 < Work.calls formula threshold k large := by
  rw [Work.calls]
  split
  · omega
  · split <;> omega

theorem work_zero_iff (formulas : List (CNF n)) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    Frontier.work threshold k large formulas = 0 ↔ formulas = [] := by
  cases formulas with
  | nil => simp [Frontier.work]
  | cons formula rest =>
    have positive := calls_positive formula threshold k large
    simp only [Frontier.work, List.cons_ne_nil, iff_false]
    omega

/-- The machine's null link test agrees with emptiness of the semantic stack;
explicit address bounds rule out a nonzero address wrapping to the zero word. -/
theorem head_zero_iff (tasks : List (StackInvariant.Task n)) (mem : Memory w) (base limit head : Nat)
    (positive : 0 < base) (fits : limit < 2 ^ w.bits) (stored : StackInvariant.Stored mem base limit head tasks) :
    BitVec.ofNat w.bits head = 0#w.bits ↔ tasks = [] := by
  cases tasks with
  | nil =>
    have zero : head = 0 := stored
    simp [zero]
  | cons task rest =>
    have lower := stored.1
    have upper := stored.2.1
    have headFits : head < 2 ^ w.bits := by omega
    simp only [List.cons_ne_nil, iff_false]
    intro eq
    have values := congrArg BitVec.toNat eq
    simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt headFits, Nat.zero_mod] at values
    omega

end WordRAM.Conjectures.Sparsification.TraversalFacts

/-! Uniform per-iteration time and allocation bounds for the traversal invariant. -/
namespace WordRAM.Conjectures.Sparsification.TraversalBounds

def stride (capacity : Nat) : Nat := 48 * (capacity + 1) ^ 2 + 6

def bodyCost (n k bits capacity : Nat) : Nat := SelectBranch.cost n k bits capacity + 21 * capacity + 63

theorem cost_mono (n k bits m capacity : Nat) (le : m ≤ capacity) :
    SelectBranch.cost n k bits m + 21 * m + 63 ≤ bodyCost n k bits capacity := by
  have core := Nat.mul_le_mul_right ((2 * n + 1) ^ k)
    (show 10 * k + 12 * bits + 18 * m + 61 ≤ 10 * k + 12 * bits + 18 * capacity + 61 by omega)
  have selection := Nat.mul_le_mul_left ((k + 1) * (k + 1)) (Nat.add_le_add_right core 5)
  have square := Nat.pow_le_pow_left (show m + 1 ≤ capacity + 1 by omega) 2
  have branch := Nat.mul_le_mul_left (12 * bits + 396) square
  unfold bodyCost SelectBranch.cost FlowerSearch.coreBound
  omega

theorem allocation (source m capacity : Nat) (le : m ≤ capacity) :
    BranchLayout.finish source m + 6 ≤ source + stride capacity := by
  have space := BranchLayout.space_bound source m
  have square := Nat.pow_le_pow_left (show m + 1 ≤ capacity + 1 by omega) 2
  have bound := Nat.mul_le_mul_left 48 square
  unfold stride
  omega

end WordRAM.Conjectures.Sparsification.TraversalBounds

/-! The actual DFS loop, with exact leaf order and a decreasing work budget. -/
namespace WordRAM.Conjectures.Sparsification.Traversal
open TraversalBody TraversalFacts TraversalBounds

def Invariant (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (target : List (CNF n)) (fuel : Nat) (mem : Memory w) : Prop :=
  ∃ (tasks emitted : List (StackInvariant.Task n)) (head outputHead limit : Nat),
  StackInvariant.Stored mem (dataBase k) limit head tasks ∧
  StackInvariant.Stored mem (dataBase k) limit outputHead emitted ∧
  (∀ formula ∈ tasks.map StackInvariant.Task.formula, Ready k capacity formula) ∧
  mem (variableCell k) = BitVec.ofNat w.bits n ∧
  mem (todoCell k) = BitVec.ofNat w.bits head ∧
  mem (outputCell k) = BitVec.ofNat w.bits outputHead ∧
  mem (freeCell k) = BitVec.ofNat w.bits limit ∧
  Frontier.work threshold k large (tasks.map StackInvariant.Task.formula) = fuel ∧
  (emitted.map StackInvariant.Task.formula).reverse ++
    Frontier.leaves threshold k large (tasks.map StackInvariant.Task.formula) = target ∧
  limit + fuel * stride capacity ≤ budget

theorem guard (fits : budget < 2 ^ w.bits)
    (h : Invariant threshold k capacity budget large target fuel (mem : Memory w)) :
    mem (todoCell k) = 0#w.bits ↔ fuel = 0 := by
  obtain ⟨tasks, emitted, head, outputHead, limit, pending, outputs, ready, variables,
    todoPointer, outputPointer, freePointer, work, order, space⟩ := h
  rw [todoPointer, head_zero_iff tasks mem (dataBase k) limit head
    (by simp [dataBase, variableCell]) (by omega) pending]
  rw [← work, work_zero_iff]
  simp

set_option maxRecDepth 4096 in
theorem iteration_framed (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (target : List (CNF n)) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits) (fits : budget < 2 ^ w.bits)
    (fuel : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (h : Invariant threshold k capacity budget large target (fuel + 1) s.mem) :
    ∃ time final, time ≤ bodyCost n k w.bits capacity ∧
      Runs widthConstant ((TraversalBody.algorithm threshold k).program w) time s final ∧
      final.halted = true ∧ Invariant threshold k capacity budget large target fuel final.mem ∧
      (∀ a, dataBase k ≤ a → budget ≤ a → final.mem a = s.mem a) := by
  obtain ⟨tasks, emitted, head, outputHead, limit, pending, outputs, ready, variables,
    todoPointer, outputPointer, freePointer, work, order, space⟩ := h
  cases tasks with
  | nil => simp [Frontier.work] at work
  | cons task rest =>
    have current : Ready k capacity task.formula := ready _ (by simp)
    have allocation := TraversalBounds.allocation limit task.formula.length capacity current.length
    have stepFits : BranchLayout.finish limit task.formula.length + 6 < 2 ^ w.bits := by
      simp only [Nat.add_mul, Nat.one_mul] at space
      omega
    obtain ⟨time, final, tasks', emitted', head', outputHead', limit', bound, trace, halted,
      pending', outputs', variables', todo', output', free', labels, emittedLabels, lower, upper, frame⟩ :=
      TraversalBody.step threshold k task rest emitted head outputHead limit s pc live variablesFit width
        thresholdFits current.nodup stepFits pending outputs variables todoPointer outputPointer freePointer
    refine ⟨time, final, Nat.le_trans bound (cost_mono n k w.bits _ capacity current.length), trace, halted,
      ⟨tasks', emitted', head', outputHead', limit', pending', outputs', ?_, variables', todo', output', free', ?_, ?_, ?_⟩, ?_⟩
    · rw [labels]
      cases selected : Selection.select task.formula threshold k with
      | none =>
        simp only [StoreResult.pendingLabels]
        intro formula member
        exact ready formula (by simp [member])
      | some choice =>
        obtain ⟨size, core⟩ := choice
        simp only [StoreResult.pendingLabels]
        have children := current.children threshold large selected
        intro formula member
        simp only [List.mem_cons] at member
        rcases member with eq | eq | member
        · exact eq ▸ children.1
        · exact eq ▸ children.2
        · exact ready formula (by simp [member])
    · rw [labels]
      simp only [List.map_cons] at work
      cases selected : Selection.select task.formula threshold k with
      | none =>
        simp only [StoreResult.pendingLabels]
        have decrease := Frontier.leaf_work task.formula (rest.map StackInvariant.Task.formula)
          threshold k large current.normalized current.nonempty selected
        omega
      | some choice =>
        obtain ⟨size, core⟩ := choice
        simp only [StoreResult.pendingLabels]
        have decrease := Frontier.branch_work task.formula (rest.map StackInvariant.Task.formula) core size
          threshold k large current.normalized current.nonempty selected
        omega
    · rw [labels, emittedLabels]
      simp only [List.map_cons] at order
      cases selected : Selection.select task.formula threshold k with
      | none =>
        simp only [StoreResult.pendingLabels, StoreResult.outputLabels]
        rw [← Frontier.leaf_output task.formula (rest.map StackInvariant.Task.formula)
          (emitted.map StackInvariant.Task.formula) threshold k large current.normalized current.nonempty selected]
        exact order
      | some choice =>
        obtain ⟨size, core⟩ := choice
        simp only [StoreResult.pendingLabels, StoreResult.outputLabels]
        rw [← Frontier.branch_leaves task.formula (rest.map StackInvariant.Task.formula) core size
          threshold k large current.normalized current.nonempty selected]
        exact order
    · simp only [Nat.add_mul, Nat.one_mul] at space
      omega
    · intro a data tail
      apply frame a data (Or.inr ?_)
      simp only [Nat.add_mul, Nat.one_mul] at space
      omega

def algorithm (threshold : Nat → Nat) (k : Nat) : Algorithm :=
  SourceWhile.algorithm (todoCell k) (TraversalBody.algorithm threshold k).code

end WordRAM.Conjectures.Sparsification.Traversal

/-! Initialize persistent traversal controls and the singleton root stack. -/
namespace WordRAM.Conjectures.Sparsification.RootStack
open TraversalBody
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

/-- Inputs: variable count 16, normalized table 22/24, allocation endpoint 27. -/
def prepare (k : Nat) : Algorithm :=
  ⟨[.copy (.direct (variableCell k)) (reg 16),
    .copy (.direct (todoCell k)) (.immediate 0),
    .copy (.direct (outputCell k)) (.immediate 0),
    .copy (.direct (freeCell k)) (reg 27),
    .copy (.direct 18) (reg 22), .copy (.direct 17) (reg 24), .halt], 1, by decide⟩

def algorithm (k : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare k).code (StackMachine.push (todoCell k) (freeCell k)).code, 1, by decide⟩

theorem prepares (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((prepare k).program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧
    t.mem (variableCell k) = s.mem 16 ∧ t.mem (todoCell k) = 0#w.bits ∧
    t.mem (outputCell k) = 0#w.bits ∧ t.mem (freeCell k) = s.mem 27 ∧
    t.mem 18 = s.mem 22 ∧ t.mem 17 = s.mem 24 ∧
    (∀ a, dataBase k ≤ a → t.mem a = s.mem a) := by
  have separation : 22 ≠ 64 + 3 * k ∧
      22 ≠ 64 + (3 * k + 1) ∧
      22 ≠ 64 + (3 * k + 2) ∧
      22 ≠ 64 + (3 * k + 3) ∧
      24 ≠ 64 + 3 * k ∧
      24 ≠ 64 + (3 * k + 1) ∧
      24 ≠ 64 + (3 * k + 2) ∧
      24 ≠ 64 + (3 * k + 3) ∧
      27 ≠ 64 + 3 * k ∧
      27 ≠ 64 + (3 * k + 1) ∧
      27 ≠ 64 + (3 * k + 2) ∧
      27 ≠ 64 + (3 * k + 3) ∧
      64 + 3 * k ≠ 17 ∧
      64 + (3 * k + 1) ≠ 17 ∧
      64 + (3 * k + 2) ≠ 17 ∧
      64 + (3 * k + 3) ≠ 17 ∧
      64 + 3 * k ≠ 18 ∧
      64 + (3 * k + 1) ≠ 18 ∧
      64 + (3 * k + 2) ≠ 18 ∧
      64 + (3 * k + 3) ≠ 18 := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live,
    variableCell, todoCell, outputCell, freeCell, dataBase, Nat.add_assoc, separation]
  intro a ha
  have h : a ≠ 64 + 3 * k ∧ a ≠ 64 + (3 * k + 1) ∧ a ≠ 64 + (3 * k + 2) ∧
      a ≠ 64 + (3 * k + 3) ∧ a ≠ 17 ∧ a ≠ 18 := by omega
  simp [h]

theorem initializes_framed (k : Nat) (task : StackInvariant.Task n) (limit : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (base : dataBase k ≤ task.address) (endBound : task.address + 3 * task.formula.length ≤ limit)
    (fits : limit + 3 < 2 ^ w.bits)
    (table : VectorBuilder.Stored s.mem task.address (RecordTable.words w task.formula))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (pointer : s.mem 22 = BitVec.ofNat w.bits task.address)
    (count : s.mem 24 = BitVec.ofNat w.bits task.formula.length)
    (free : s.mem 27 = BitVec.ofNat w.bits limit) :
    ∃ final, Runs widthConstant ((algorithm k).program w) 24 s final ∧ final.halted = true ∧
      StackInvariant.Stored final.mem (dataBase k) (limit + 3) limit [task] ∧
      final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
      final.mem (todoCell k) = BitVec.ofNat w.bits limit ∧
      final.mem (outputCell k) = 0#w.bits ∧ final.mem (freeCell k) = BitVec.ofNat w.bits (limit + 3) ∧
      (∀ a, limit + 3 ≤ a → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare k).program w) 7 s
  obtain ⟨ph, pt, pv, th, oh, fp, tp, tc, frame⟩ := prepares k s pc live
  have stored : VectorBuilder.Stored prepared.mem task.address (RecordTable.words w task.formula) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact frame a (by omega)
  have coords : 64 ≤ variableCell k ∧ todoCell k = variableCell k + 1 ∧
      outputCell k = variableCell k + 2 ∧ freeCell k = variableCell k + 3 ∧ dataBase k = variableCell k + 4 := by
    dsimp [variableCell, todoCell, outputCell, freeCell, dataBase]; omega
  obtain ⟨out, trace, halted, head, free', pending, preserved⟩ :=
    StackInvariant.push [] task (SourceChain.resume prepared) (todoCell k) (freeCell k) (dataBase k)
      limit 0 limit rfl rfl (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) fits rfl
      base endBound stored (tp.trans pointer) (tc.trans count) th (fp.trans free)
  obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant ((prepare k).program w) 7 s
  have cost := runs_cost setupTrace
  have exactTicks : ticks = 7 := by omega
  subst ticks
  have full := SourceChain.traces (prepare k).code (StackMachine.push (todoCell k) (freeCell k)).code
    s prepared out 7 17 live ph setupTrace trace
  refine ⟨out.relocate (prepare k).code.length, full, halted, pending, ?_, head, ?_, free', ?_⟩
  · exact (preserved (variableCell k) (by omega) (by omega) (by omega) (Or.inl (by omega))).trans (pv.trans variables)
  · exact (preserved (outputCell k) (by omega) (by omega) (by omega) (Or.inl (by omega))).trans oh
  · intro a ha
    exact (preserved a (by omega) (by omega) (by omega) (Or.inr ha)).trans (frame a (by omega))

end WordRAM.Conjectures.Sparsification.RootStack