SETH ⇒ OVC sparsification bundle 37: 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_36

set_option autoImplicit true

/-! A semantic representation of pending formulas in the machine's linked stack. -/
namespace WordRAM.Conjectures.Sparsification.StackInvariant

structure Task (n : Nat) where
  formula : CNF n
  address : Nat

def Stored (mem : Memory w) (base limit head : Nat) : List (Task n) → Prop
  | [] => head = 0
  | task :: rest =>
    base ≤ head ∧ head + 3 ≤ limit ∧ base ≤ task.address ∧ task.address + 3 * task.formula.length ≤ limit ∧
      VectorBuilder.Stored mem task.address (RecordTable.words w task.formula) ∧
      ∃ next, VectorBuilder.Stored mem head
        [BitVec.ofNat w.bits task.address, BitVec.ofNat w.bits task.formula.length, BitVec.ofNat w.bits next] ∧
        Stored mem base limit next rest

theorem frame (tasks : List (Task n)) (before after : Memory w) (base limit head : Nat)
    (h : Stored before base limit head tasks)
    (same : ∀ a, base ≤ a → a < limit → after a = before a) : Stored after base limit head tasks := by
  induction tasks generalizing head with
  | nil => exact h
  | cons task rest ih =>
    rcases h with ⟨hb, he, tb, te, table, next, node, tail⟩
    refine ⟨hb, he, tb, te, ?_, next, ?_, ih next tail⟩
    · apply MemoryCopy.stored_frame _ _ table
      intro a ha ha'
      rw [RecordTable.words_length] at ha'
      exact same a (by omega) (by omega)
    · apply MemoryCopy.stored_frame _ _ node
      intro a ha ha'
      simp only [List.length_cons, List.length_nil] at ha'
      exact same a (by omega) (by omega)

theorem weaken (tasks : List (Task n)) (mem : Memory w) (base limit larger head : Nat)
    (h : Stored mem base limit head tasks) (le : limit ≤ larger) : Stored mem base larger head tasks := by
  induction tasks generalizing head with
  | nil => exact h
  | cons task rest ih =>
    rcases h with ⟨hb, he, tb, te, table, next, node, tail⟩
    exact ⟨hb, by omega, tb, by omega, table, next, node, ih next tail⟩

/-- Pushing preserves every previously pending formula and adds the fresh task
at the front of the semantic list. The new link is allocated above old data. -/
theorem push (tasks : List (Task n)) (task : Task n) (s : State w)
    (headCell freeCell base limit head destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (fb : 64 ≤ freeCell)
    (distinct : headCell ≠ freeCell) (headBefore : headCell < base) (freeBefore : freeCell < base)
    (fresh : limit ≤ destination) (fits : destination + 3 < 2 ^ w.bits)
    (pending : Stored s.mem base limit head tasks)
    (taskBase : base ≤ task.address) (taskEnd : task.address + 3 * task.formula.length ≤ limit)
    (table : VectorBuilder.Stored s.mem task.address (RecordTable.words w task.formula))
    (sourcePointer : s.mem 18 = BitVec.ofNat w.bits task.address)
    (sourceCount : s.mem 17 = BitVec.ofNat w.bits task.formula.length)
    (headPointer : s.mem headCell = BitVec.ofNat w.bits head)
    (freePointer : s.mem freeCell = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant ((StackMachine.push headCell freeCell).program w) 17 s final ∧ final.halted = true ∧
      final.mem headCell = BitVec.ofNat w.bits destination ∧
      final.mem freeCell = BitVec.ofNat w.bits (destination + 3) ∧
      Stored final.mem base (destination + 3) destination (task :: tasks) ∧
      (∀ a, 16 ≤ a → a ≠ headCell → a ≠ freeCell → (a < destination ∨ destination + 3 ≤ a) → final.mem a = s.mem a) := by
  obtain ⟨out, trace, halted, hp, fp, node, preserved⟩ := StackMachine.pushes headCell freeCell destination s
    pc live hb fb distinct (by omega) (by omega) (by omega) freePointer
  have same : ∀ a, base ≤ a → a < limit → out.mem a = s.mem a := by
    intro a ha ha'
    exact preserved a (by omega) (by omega) (by omega) (Or.inl (by omega))
  have old := frame tasks s.mem out.mem base limit head pending same
  have retained := weaken tasks out.mem base limit (destination + 3) head old (by omega)
  have taskTable : VectorBuilder.Stored out.mem task.address (RecordTable.words w task.formula) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha ha'
    rw [RecordTable.words_length] at ha'
    exact same a (by omega) (by omega)
  refine ⟨out, trace, halted, hp, fp, ?_, preserved⟩
  refine ⟨by omega, by omega, taskBase, by omega, taskTable, head, ?_, retained⟩
  simpa only [sourcePointer, sourceCount, headPointer] using node

/-- Popping the concrete head yields the corresponding semantic task, with its
formula table intact, and leaves the semantic tail represented in memory. -/
theorem pop (tasks : List (Task n)) (task : Task n) (s : State w)
    (headCell base limit head : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (headBefore : headCell < base)
    (fits : limit < 2 ^ w.bits) (pending : Stored s.mem base limit head (task :: tasks))
    (headPointer : s.mem headCell = BitVec.ofNat w.bits head) :
    ∃ next final, Runs widthConstant ((StackMachine.pop headCell).program w) 7 s final ∧ final.halted = true ∧
      final.mem 18 = BitVec.ofNat w.bits task.address ∧ final.mem 17 = BitVec.ofNat w.bits task.formula.length ∧
      final.mem headCell = BitVec.ofNat w.bits next ∧ Stored final.mem base limit next tasks ∧
      VectorBuilder.Stored final.mem task.address (RecordTable.words w task.formula) ∧
      (∀ a, a ≠ 12 → a ≠ 17 → a ≠ 18 → a ≠ headCell → final.mem a = s.mem a) := by
  rcases pending with ⟨nodeBase, nodeEnd, taskBase, taskEnd, table, next, node, tail⟩
  let out := run widthConstant ((StackMachine.pop headCell).program w) 7 s
  obtain ⟨halted, _, addressValue, countValue, nextValue, preserved⟩ :=
    StackMachine.pops headCell head s pc live hb (by omega) (by omega) headPointer
  rcases node with ⟨np, nc, nn, _⟩
  have same : ∀ a, base ≤ a → a < limit → out.mem a = s.mem a := by
    intro a ha _
    exact preserved a (by omega) (by omega) (by omega) (by omega)
  refine ⟨next, out, StackMachine.pop_trace headCell head s pc live hb (by omega) (by omega) headPointer,
    halted, addressValue.trans np, countValue.trans nc, nextValue.trans nn,
    frame tasks s.mem out.mem base limit next tail same, ?_, preserved⟩
  apply MemoryCopy.stored_frame _ _ table
  intro a ha ha'
  rw [RecordTable.words_length] at ha'
  exact same a (by omega) (by omega)

end WordRAM.Conjectures.Sparsification.StackInvariant

/-! Preserve a node result while updating allocator metadata below its tables. -/
namespace WordRAM.Conjectures.Sparsification.SelectBranchFrame

variable {formula : CNF n} {core : Clause n} {size source : Nat} {before after : Memory w}

theorem children (h : SelectedBranch.Children formula core size source before)
    (same : ∀ a, a < 64 ∨ source ≤ a → after a = before a) :
    SelectedBranch.Children formula core size source after := by
  rcases h with ⟨flag, ⟨left, right, lt, rt, lp, lc, rp, rc, lower, separated, upper⟩, free, input⟩
  refine ⟨(same 0 (Or.inl (by decide))).trans flag,
    ⟨left, right, ?_, ?_, ?_, ?_, ?_, ?_, lower, separated, upper⟩, ?_, ?_⟩
  · apply MemoryCopy.stored_frame _ _ lt
    intro a ha _; exact same a (Or.inr (by omega))
  · apply MemoryCopy.stored_frame _ _ rt
    intro a ha _; exact same a (Or.inr (by omega))
  · exact (same 43 (Or.inl (by decide))).trans lp
  · exact (same 44 (Or.inl (by decide))).trans lc
  · exact (same 45 (Or.inl (by decide))).trans rp
  · exact (same 46 (Or.inl (by decide))).trans rc
  · exact (same 49 (Or.inl (by decide))).trans free
  · apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact same a (Or.inr ha)

theorem outcome (choice : Option (Nat × Clause n)) (h : SelectBranch.Outcome formula source choice before)
    (same : ∀ a, a < 64 ∨ source ≤ a → after a = before a) :
    SelectBranch.Outcome formula source choice after := by
  cases choice with
  | none =>
    rcases h with ⟨flag, variables, count, pointer, input⟩
    refine ⟨(same 0 (Or.inl (by decide))).trans flag, (same 16 (Or.inl (by decide))).trans variables,
      (same 17 (Or.inl (by decide))).trans count, (same 18 (Or.inl (by decide))).trans pointer, ?_⟩
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact same a (Or.inr ha)
  | some pair => exact children h same

end WordRAM.Conjectures.Sparsification.SelectBranchFrame

/-! Commit the allocator endpoint after either a leaf or a branching result. -/
namespace WordRAM.Conjectures.Sparsification.FinishAllocation

def endpoint (source count : Nat) : Option (Nat × Clause n) → Nat
  | none => source + 3 * count
  | some _ => BranchLayout.finish source count

def save (freeCell : Nat) : Algorithm :=
  ⟨[.copy (.direct freeCell) (.memory (.direct 49)), .halt], 1, by decide⟩

def algorithm (freeCell : Nat) : Algorithm :=
  ⟨SourceIf.code 0 SelectBranch.leaf.code (save freeCell).code, 1, by decide⟩

theorem saves (freeCell : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((save freeCell).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem freeCell = s.mem 49 ∧
      (∀ a, a ≠ freeCell → t.mem a = s.mem a) := by
  simp [save, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a ha; simp [ha]

theorem commits (formula : CNF n) (source freeCell : Nat) (choice : Option (Nat × Clause n)) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 64 ≤ freeCell) (before : freeCell < source)
    (result : SelectBranch.Outcome formula source choice s.mem)
    (oldFree : s.mem freeCell = BitVec.ofNat w.bits (source + 3 * formula.length)) :
    ∃ time final, time ≤ 3 ∧ Runs widthConstant ((algorithm freeCell).program w) time s final ∧ final.halted = true ∧
      SelectBranch.Outcome formula source choice final.mem ∧
      final.mem freeCell = BitVec.ofNat w.bits (endpoint source formula.length choice) ∧
      (∀ a, a ≠ freeCell → final.mem a = s.mem a) := by
  cases choice with
  | none =>
    let out := run widthConstant (SelectBranch.leaf.program w) 1 (s.addTicks 1)
    obtain ⟨trace, halted, mem⟩ := SelectBranch.leaf_trace (s.addTicks 1) pc live
    have full := SourceIf.zero_trace 0 SelectBranch.leaf.code (save freeCell).code s out 1 pc live result.1 trace
    refine ⟨2, out.relocate (1 + (save freeCell).code.length), by decide, full, halted, ?_, ?_, ?_⟩
    · apply SelectBranchFrame.outcome none result
      intro a _; exact congrFun mem a
    · exact (congrFun mem freeCell).trans oldFree
    · intro a _; exact congrFun mem a
  | some pair =>
    rcases pair with ⟨size, core⟩
    let out := run widthConstant ((save freeCell).program w) 2 (s.addTicks 1)
    obtain ⟨halted, ticks, free, frame⟩ := saves freeCell (s.addTicks 1) pc live
    obtain ⟨time, _, trace⟩ := run_has_trace widthConstant ((save freeCell).program w) 2 (s.addTicks 1)
    have cost := runs_cost trace
    have eq : time = 2 := by omega
    subst time
    have nonzero : s.mem 0 ≠ 0#w.bits := by
      rw [result.flag]
      intro h
      have values := congrArg BitVec.toNat h
      have oneFits : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by have := w.positive; omega)
      simp [Nat.mod_eq_of_lt oneFits] at values
    have full := SourceIf.nonzero_trace 0 SelectBranch.leaf.code (save freeCell).code s out 2 pc live nonzero trace
    refine ⟨3, out.relocate 1, by decide, full, halted, ?_, free.trans result.free, frame⟩
    apply SelectBranchFrame.outcome (some (size, core)) result
    intro a ha
    exact frame a (by rcases ha with ha | ha <;> omega)

end WordRAM.Conjectures.Sparsification.FinishAllocation

/-! Process a pending table without overwriting siblings or stack nodes. -/
namespace WordRAM.Conjectures.Sparsification.PendingStep

def algorithm (threshold : Nat → Nat) (k freeCell : Nat) : Algorithm :=
  ⟨SourceChain.code (RelocateTable.algorithm freeCell).code
    (SourceChain.code (SelectBranch.algorithm threshold k).code (FinishAllocation.algorithm freeCell).code), 1, by decide⟩

set_option maxRecDepth 4096 in
/-- Copy a pending formula to fresh space, select/branch there, and commit the
new allocator endpoint. Older tables and pending stack nodes remain untouched. -/
theorem processes (formula : CNF n) (threshold : Nat → Nat) (k freeCell source destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 64 ≤ freeCell)
    (searchSafe : 32 + 3 * k ≤ freeCell) (controlBefore : freeCell < source)
    (separate : source + 3 * formula.length ≤ destination)
    (fits : BranchLayout.finish destination formula.length < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 17 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits source)
    (free : s.mem freeCell = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula)) :
    ∃ time final, time ≤ SelectBranch.cost n k w.bits formula.length + 21 * formula.length + 13 ∧
      Runs widthConstant ((algorithm threshold k freeCell).program w) time s final ∧ final.halted = true ∧
      SelectBranch.Outcome formula destination (Selection.select formula threshold k) final.mem ∧
      final.mem freeCell = BitVec.ofNat w.bits
        (FinishAllocation.endpoint destination formula.length (Selection.select formula threshold k)) ∧
      VectorBuilder.Stored final.mem source (RecordTable.words w formula) ∧
      (∀ a, 64 ≤ a → 32 + 3 * k ≤ a → a ≠ freeCell →
        (a < destination ∨ BranchLayout.finish destination formula.length ≤ a) → final.mem a = s.mem a) := by
  have order := BranchLayout.ordered destination formula.length
  have copyFits : destination + 3 * formula.length < 2 ^ w.bits := by
    change BranchLayout.remaining destination formula.length < 2 ^ w.bits
    omega
  obtain ⟨copied, ct, ch, table, oldTable, cp, cc, cf, frame⟩ := RelocateTable.relocates formula freeCell source destination
    s pc live base controlBefore separate copyFits pointer count free input
  have cv : copied.mem 16 = BitVec.ofNat w.bits n :=
    (frame 16 (by decide) (by decide) (by omega) (Or.inl (by omega))).trans variables
  obtain ⟨time, selected, bound, trace, halted, result, sf⟩ := SelectBranch.selects_and_branches formula threshold k destination
    (SourceChain.resume copied) rfl rfl variablesFit width (by omega) (by omega) fits thresholdFits nodup cv cc cp table
  have selectedFree : selected.mem freeCell = BitVec.ofNat w.bits (destination + 3 * formula.length) :=
    (sf freeCell base searchSafe (Or.inl (by omega))).trans cf
  obtain ⟨finishTime, out, finishBound, finishTrace, finishHalt, finalResult, finalFree, ff⟩ :=
    FinishAllocation.commits formula destination freeCell (Selection.select formula threshold k)
      (SourceChain.resume selected) rfl rfl base (by omega) result selectedFree
  have tail := SourceChain.traces (SelectBranch.algorithm threshold k).code (FinishAllocation.algorithm freeCell).code
    (SourceChain.resume copied) selected out time finishTime rfl halted trace finishTrace
  have full := SourceChain.traces (RelocateTable.algorithm freeCell).code
    (SourceChain.code (SelectBranch.algorithm threshold k).code (FinishAllocation.algorithm freeCell).code)
    s copied _ (21 * formula.length + 10) (time + finishTime) live ch ct tail
  have preserved : ∀ a, 64 ≤ a → 32 + 3 * k ≤ a → a ≠ freeCell →
      (a < destination ∨ BranchLayout.finish destination formula.length ≤ a) → out.mem a = s.mem a := by
    intro a ha hs hf outside
    have outsideCopy : a < destination ∨ destination + 3 * formula.length ≤ a := by
      change a < destination ∨ BranchLayout.remaining destination formula.length ≤ a
      omega
    exact (ff a hf).trans ((sf a ha hs (by omega)).trans (frame a (by omega) (by omega) hf outsideCopy))
  refine ⟨(21 * formula.length + 10) + (time + finishTime),
    (out.relocate (SelectBranch.algorithm threshold k).code.length).relocate (RelocateTable.algorithm freeCell).code.length,
    by omega, full, finishHalt, finalResult, finalFree, ?_, preserved⟩
  apply MemoryCopy.stored_frame _ _ input
  intro a ha hb
  rw [RecordTable.words_length] at hb
  exact preserved a (by omega) (by omega) (by omega) (Or.inl (by omega))

end WordRAM.Conjectures.Sparsification.PendingStep

/-! Exact work and output identities for depth-first traversal of pending formulas. -/
namespace WordRAM.Conjectures.Sparsification.Frontier

def work (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) : List (CNF n) → Nat
  | [] => 0
  | formula :: rest => Work.calls formula threshold k large + work threshold k large rest

def leaves (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) : List (CNF n) → List (CNF n)
  | [] => []
  | formula :: rest => Tree.leaves formula threshold k large ++ leaves threshold k large rest

/-- Each processed task consumes exactly one invocation from the remaining
recursive work, even when it replaces one task by two children. -/
theorem branch_work (formula : CNF n) (rest : List (CNF n)) (core : Clause n) (size : Nat)
    (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (normalized : Normalize.normalize formula = formula) (nonempty : [] ∉ formula)
    (selected : Selection.select formula threshold k = some (size, core)) :
    work threshold k large (formula :: rest) =
      1 + work threshold k large (Branch.left formula core size :: Branch.right formula core size :: rest) := by
  have calls : Work.calls formula threshold k large =
      1 + Work.calls (Branch.left formula core size) threshold k large +
        Work.calls (Branch.right formula core size) threshold k large := by
    rw [Work.calls, normalized]
    simp only [if_neg nonempty]
    split <;> simp_all
  simp only [work, calls]
  omega

theorem leaf_work (formula : CNF n) (rest : List (CNF n))
    (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (normalized : Normalize.normalize formula = formula) (nonempty : [] ∉ formula)
    (selected : Selection.select formula threshold k = none) :
    work threshold k large (formula :: rest) = 1 + work threshold k large rest := by
  have calls : Work.calls formula threshold k large = 1 := by
    rw [Work.calls, normalized]
    simp only [if_neg nonempty]
    split <;> simp_all
  simp only [work, calls]

theorem branch_leaves (formula : CNF n) (rest : List (CNF n)) (core : Clause n) (size : Nat)
    (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (normalized : Normalize.normalize formula = formula) (nonempty : [] ∉ formula)
    (selected : Selection.select formula threshold k = some (size, core)) :
    leaves threshold k large (formula :: rest) =
      leaves threshold k large (Branch.left formula core size :: Branch.right formula core size :: rest) := by
  have outputs : Tree.leaves formula threshold k large =
      Tree.leaves (Branch.left formula core size) threshold k large ++
        Tree.leaves (Branch.right formula core size) threshold k large := by
    rw [Tree.leaves, normalized]
    simp only [if_neg nonempty]
    split <;> simp_all
  simp only [leaves, outputs, List.append_assoc]

/-- Emitted leaves are pushed onto a second stack, hence their reversal in the
ordered output invariant. This identity accounts for one sparse-leaf emission. -/
theorem leaf_output (formula : CNF n) (rest emitted : List (CNF n))
    (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (normalized : Normalize.normalize formula = formula) (nonempty : [] ∉ formula)
    (selected : Selection.select formula threshold k = none) :
    emitted.reverse ++ leaves threshold k large (formula :: rest) =
      (formula :: emitted).reverse ++ leaves threshold k large rest := by
  have outputs : Tree.leaves formula threshold k large = [formula] := by
    rw [Tree.leaves, normalized]
    simp only [if_neg nonempty]
    split <;> simp_all
  simp only [leaves, outputs, List.reverse_cons, List.append_assoc]

end WordRAM.Conjectures.Sparsification.Frontier

/-! Stage a returned child descriptor and push the corresponding formula task. -/
namespace WordRAM.Conjectures.Sparsification.TaskPush

private def pointerCell (left : Bool) : Nat := if left then 43 else 45
private def countCell (left : Bool) : Nat := if left then 44 else 46

def stage (left : Bool) : Algorithm :=
  ⟨[.copy (.direct 18) (.memory (.direct (pointerCell left))),
    .copy (.direct 17) (.memory (.direct (countCell left))), .halt], 1, by decide⟩

def algorithm (left : Bool) (headCell freeCell : Nat) : Algorithm :=
  ⟨SourceChain.code (stage left).code (StackMachine.push headCell freeCell).code, 1, by decide⟩

theorem stages (left : Bool) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((stage left).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 18 = s.mem (pointerCell left) ∧
      t.mem 17 = s.mem (countCell left) ∧ (∀ a, 32 ≤ a → t.mem a = s.mem a) := by
  have h : countCell left ≠ 18 := by cases left <;> decide
  simp [stage, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, h, Nat.add_assoc]
  intro a ha
  have h : a ≠ 17 ∧ a ≠ 18 := by omega
  simp [h]

theorem pushes (left : Bool) (tasks : List (StackInvariant.Task n)) (task : StackInvariant.Task n) (s : State w)
    (headCell freeCell base limit head destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (fb : 64 ≤ freeCell)
    (distinct : headCell ≠ freeCell) (headBefore : headCell < base) (freeBefore : freeCell < base)
    (fresh : limit ≤ destination) (fits : destination + 3 < 2 ^ w.bits)
    (pending : StackInvariant.Stored s.mem base limit head tasks)
    (taskBase : base ≤ task.address) (taskEnd : task.address + 3 * task.formula.length ≤ limit)
    (table : VectorBuilder.Stored s.mem task.address (RecordTable.words w task.formula))
    (sourcePointer : s.mem (if left then 43 else 45) = BitVec.ofNat w.bits task.address)
    (sourceCount : s.mem (if left then 44 else 46) = BitVec.ofNat w.bits task.formula.length)
    (headPointer : s.mem headCell = BitVec.ofNat w.bits head)
    (freePointer : s.mem freeCell = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant ((algorithm left headCell freeCell).program w) 20 s final ∧ final.halted = true ∧
      final.mem headCell = BitVec.ofNat w.bits destination ∧ final.mem freeCell = BitVec.ofNat w.bits (destination + 3) ∧
      StackInvariant.Stored final.mem base (destination + 3) destination (task :: tasks) ∧
      (∀ a, 32 ≤ a → a ≠ headCell → a ≠ freeCell → (a < destination ∨ destination + 3 ≤ a) → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((stage left).program w) 3 s
  obtain ⟨ph, pt, pp, pn, pf⟩ := stages left s pc live
  have preparedStack := StackInvariant.frame tasks s.mem prepared.mem base limit head pending
    (by intro a ha _; exact pf a (by omega))
  have preparedTable : VectorBuilder.Stored prepared.mem task.address (RecordTable.words w task.formula) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact pf a (by omega)
  obtain ⟨out, trace, halted, hp, fp, stored, frame⟩ := StackInvariant.push tasks task (SourceChain.resume prepared)
    headCell freeCell base limit head destination rfl rfl hb fb distinct headBefore freeBefore fresh fits preparedStack
      taskBase taskEnd preparedTable (pp.trans sourcePointer) (pn.trans sourceCount)
      ((pf headCell (by omega)).trans headPointer) ((pf freeCell (by omega)).trans freePointer)
  obtain ⟨time, _, setupTrace⟩ := run_has_trace widthConstant ((stage left).program w) 3 s
  have cost := runs_cost setupTrace
  have eq : time = 3 := by omega
  subst time
  have full := SourceChain.traces (stage left).code (StackMachine.push headCell freeCell).code s prepared out
    3 17 live ph setupTrace trace
  refine ⟨out.relocate (stage left).code.length, full, halted, hp, fp, stored, ?_⟩
  intro a ha hh hf outside
  exact (frame a (by omega) hh hf outside).trans (pf a ha)

end WordRAM.Conjectures.Sparsification.TaskPush