SETH ⇒ OVC sparsification bundle 45: 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_44

set_option autoImplicit true

/-! One complete sparse-leaf call: serialize the clause table in fresh memory,
compute all scan/width parameters, simulate the supplied SAT solver, and return
its answer while preserving other leaves and the unused memory tail. -/
namespace WordRAM.Conjectures.Sparsification.LeafCall
open SimulationExecution

def satInput (formula : CNF n) : SATInstance := ⟨n, Canonical.formula formula⟩

def algorithm (solver : Algorithm) (baseCell : Nat) : Algorithm :=
  ⟨SourceChain.code SATSerialize.algorithm.code
    (SourceChain.code (ScanCallSetup.algorithm baseCell).code (ScannedSolverCall.algorithm solver).code), 1, by decide⟩

theorem decides (solver : Algorithm) (formula : CNF n) (solverTime : Nat)
    (decision : DecidesIn solver (satInput formula).encode n solverTime (satInput formula).Satisfiable)
    (baseCell source base budget : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (sourceBase : 32 ≤ source)
    (cellBase : 32 ≤ baseCell) (cellBefore : baseCell < base)
    (before : source + 3 * formula.length ≤ base)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 2 ≤ w.bits)
    (space : base + 3 + formula.length * (1 + 4 * n) ≤ budget)
    (width : (solver.width (satInput formula).encode n).bits ≤ w.bits)
    (fixed : ∀ i ∈ solver.code, Fits base w i)
    (dynamic : base + 2 ^ (solver.width (satInput formula).encode n).bits ≤ 2 ^ w.bits)
    (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 (base + 1))
    (savedBase : s.mem baseCell = BitVec.ofNat w.bits base)
    (fresh : ∀ a, base ≤ a → s.mem a = 0#w.bits) :
    ∃ total final, total ≤ formula.length * (22 * n + 29) + 7 * (satInput formula).encode.length +
        4 * (inputMagnitude (satInput formula).encode).log2 + 19 * solverTime + 30 ∧
      Runs widthConstant ((algorithm solver baseCell).program w) total s final ∧ final.halted = true ∧
      (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ (SATInstance.mk n formula).Satisfiable) ∧
      SimulationBounded.Preserved s.mem final.mem base
        (base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code) ∧
      (∀ a, base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code ≤ a → final.mem a = 0#w.bits) ∧
      final.mem 31 = WidthSimulation.lift w
        (BitVec.ofNat (solver.width (satInput formula).encode n).bits (solver.width (satInput formula).encode n).bits :
          Word (solver.width (satInput formula).encode n)) := by
  obtain ⟨serializeTime, serialized, serializeBound, serializeTrace, serializeHalt, stored, memory, endpoint, vars, sf⟩ :=
    FreshSerialize.prepares formula source base budget s pc live sourceBase before fits variablesFit space nodup
      input variables count pointer output fresh
  have lengthBound := SATSerialize.length_le formula
  have endFits : base + 1 + (satInput formula).encode.length < 2 ^ w.bits := by
    change (satInput formula).encode.length ≤ _ at lengthBound
    omega
  have keptBase : serialized.mem baseCell = BitVec.ofNat w.bits base :=
    (sf baseCell cellBase (Or.inl (by omega))).trans savedBase
  let prepared := run widthConstant ((ScanCallSetup.algorithm baseCell).program w) 4 (SourceChain.resume serialized)
  obtain ⟨ph, _, pp, sp, cnt, pf⟩ := ScanCallSetup.prepares baseCell base (satInput formula).encode.length
    (SourceChain.resume serialized) rfl rfl cellBase endFits keptBase endpoint
  have setupTrace := ScanCallSetup.trace baseCell base (satInput formula).encode.length
    (SourceChain.resume serialized) rfl rfl cellBase endFits keptBase endpoint
  have preparedInput : VectorBuilder.Stored prepared.mem (base + 1) ((satInput formula).encode.map (BitVec.ofNat w.bits)) := by
    apply MemoryCopy.stored_frame _ _ stored
    intro a ha _; exact pf a (by omega) (by omega) (by omega)
  have preparedMemory : ∀ address, prepared.mem (base + address) = (initialState w (satInput formula).encode).mem address := by
    intro address
    exact (pf (base + address) (by omega) (by omega) (by omega)).trans (memory address)
  obtain ⟨callTime, out, callBound, callTrace, halted, boolean, correct, frame, native⟩ :=
    ScannedSolverCall.decides solver (satInput formula).encode n solverTime (satInput formula).Satisfiable decision
      (SourceChain.resume prepared) base (base + 1) rfl rfl large (by omega) (by omega) endFits width fixed dynamic
      preparedMemory preparedInput pp sp cnt ((pf 16 (by decide) (by decide) (by decide)).trans vars)
  have tail := SourceChain.traces (ScanCallSetup.algorithm baseCell).code (ScannedSolverCall.algorithm solver).code
    (SourceChain.resume serialized) prepared out 4 callTime rfl ph setupTrace callTrace
  have full := SourceChain.traces SATSerialize.algorithm.code
    (SourceChain.code (ScanCallSetup.algorithm baseCell).code (ScannedSolverCall.algorithm solver).code)
    s serialized (out.relocate (ScanCallSetup.algorithm baseCell).code.length) serializeTime (4 + callTime)
    live serializeHalt serializeTrace tail
  change ∀ a, 32 ≤ a → (a < base + 1 ∨ base + 1 + (satInput formula).encode.length ≤ a) → serialized.mem a = s.mem a at sf
  have inputSpan := SimulationFootprint.input_length solver (satInput formula).encode n
  have finalFrame : SimulationBounded.Preserved s.mem out.mem base
      (base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code) := by
    intro a ha outside
    exact (frame a ha outside).trans ((pf a (by omega) (by omega) (by omega)).trans (sf a ha (by omega)))
  refine ⟨serializeTime + (4 + callTime),
    (out.relocate (ScanCallSetup.algorithm baseCell).code.length).relocate SATSerialize.algorithm.code.length,
    by omega, full, halted, boolean, correct.trans (Canonical.satisfiable formula), finalFrame, ?_, native⟩
  intro a ha
  have baseLe : base ≤ a := by omega
  exact (finalFrame a (by omega) (Or.inr ha)).trans (fresh a baseLe)

end WordRAM.Conjectures.Sparsification.LeafCall

/-! Advance a persistent free pointer past the actual solver write region. -/
namespace WordRAM.Conjectures.SimulationAllocate
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

/-- Width is in 31; the persistent cell holds the simulation base. Preserve the
answer in 0. The larger of the indirect range and fixed bound determines size. -/
def algorithm (baseCell fixed : Nat) : Algorithm :=
  ⟨[.binary .shl (.direct 29) (.immediate 1) (reg 31),
    .branch .le (reg 29) (.immediate fixed) 4,
    .binary .add (.direct baseCell) (reg baseCell) (reg 29), .halt,
    .copy (.direct 29) (.immediate fixed), .jump 2], 1, by decide⟩

private theorem shift_one (w : Width) (bits : Nat) :
    (1#w.bits <<< bits) = BitVec.ofNat w.bits (2 ^ bits) := by
  apply BitVec.eq_of_toNat_eq
  have positive : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by have := w.positive; omega)
  simp [BitVec.toNat_shiftLeft, Nat.shiftLeft_eq, Nat.mod_eq_of_lt positive]

theorem allocates (baseCell base bits fixed : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (cell : 32 ≤ baseCell)
    (width : bits ≤ w.bits) (fits : base + max (2 ^ bits) fixed < 2 ^ w.bits)
    (pointer : s.mem baseCell = BitVec.ofNat w.bits base)
    (native : s.mem 31 = BitVec.ofNat w.bits bits) :
    ∃ time final, time ≤ 6 ∧ Runs widthConstant ((algorithm baseCell fixed).program w) time s final ∧
      final.halted = true ∧ final.mem baseCell = BitVec.ofNat w.bits (base + max (2 ^ bits) fixed) ∧
      (∀ a, a ≠ 29 → a ≠ baseCell → final.mem a = s.mem a) := by
  have bitsFit : bits < 2 ^ w.bits := Nat.lt_of_le_of_lt width (Nat.lt_pow_self (by decide))
  have bitsValue : (BitVec.ofNat w.bits bits).toNat = bits := Nat.mod_eq_of_lt bitsFit
  have rangeValue : (BitVec.ofNat w.bits (2 ^ bits)).toNat = 2 ^ bits := Nat.mod_eq_of_lt (by omega)
  have fixedValue : (BitVec.ofNat w.bits fixed).toNat = fixed := Nat.mod_eq_of_lt (by omega)
  have distinct : baseCell ≠ 29 := by omega
  by_cases order : 2 ^ bits ≤ fixed
  · have result :
        let t := run widthConstant ((algorithm baseCell fixed).program w) 6 s
        t.ticks = s.ticks + 6 ∧ t.halted = true ∧ t.mem baseCell = BitVec.ofNat w.bits (base + fixed) ∧
        (∀ a, a ≠ 29 → a ≠ baseCell → t.mem a = s.mem a) := by
      simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
        Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, pointer, native,
        bitsValue, shift_one, rangeValue, fixedValue, order, distinct, Nat.add_assoc, ← BitVec.ofNat_add]
      intro a h29 hb; simp [h29, hb]
    obtain ⟨time, _, trace⟩ := run_has_trace widthConstant ((algorithm baseCell fixed).program w) 6 s
    have cost := runs_cost trace
    have eq : time = 6 := by have := result.1; omega
    subst time
    exact ⟨6, _, by decide, trace, result.2.1, by simpa only [Nat.max_eq_right order] using result.2.2.1, result.2.2.2⟩
  · have result :
        let t := run widthConstant ((algorithm baseCell fixed).program w) 4 s
        t.ticks = s.ticks + 4 ∧ t.halted = true ∧ t.mem baseCell = BitVec.ofNat w.bits (base + 2 ^ bits) ∧
        (∀ a, a ≠ 29 → a ≠ baseCell → t.mem a = s.mem a) := by
      simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
        Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, pointer, native,
        bitsValue, shift_one, rangeValue, fixedValue, order, distinct, Nat.add_assoc, ← BitVec.ofNat_add]
      intro a h29 hb; simp [h29, hb]
    obtain ⟨time, _, trace⟩ := run_has_trace widthConstant ((algorithm baseCell fixed).program w) 4 s
    have cost := runs_cost trace
    have eq : time = 4 := by have := result.1; omega
    subst time
    exact ⟨4, _, by decide, trace, result.2.1, by simpa only [Nat.max_eq_left (by omega : fixed ≤ 2 ^ bits)] using result.2.2.1, result.2.2.2⟩

end WordRAM.Conjectures.SimulationAllocate

/-! A complete leaf decision advances the allocator to a new zero region. -/
namespace WordRAM.Conjectures.Sparsification.AllocatedLeafCall
open SimulationExecution LeafCall

def algorithm (solver : Algorithm) (baseCell : Nat) : Algorithm :=
  ⟨SourceChain.code (LeafCall.algorithm solver baseCell).code
    (SimulationAllocate.algorithm baseCell (SimulationBounds.programBound solver.code + 1)).code, 1, by decide⟩

theorem decides (solver : Algorithm) (formula : CNF n) (solverTime : Nat)
    (decision : DecidesIn solver (satInput formula).encode n solverTime (satInput formula).Satisfiable)
    (baseCell source base budget : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (sourceBase : 32 ≤ source)
    (cellBase : 32 ≤ baseCell) (cellBefore : baseCell < base)
    (before : source + 3 * formula.length ≤ base)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 2 ≤ w.bits)
    (space : base + 3 + formula.length * (1 + 4 * n) ≤ budget)
    (width : (solver.width (satInput formula).encode n).bits ≤ w.bits)
    (fixed : ∀ i ∈ solver.code, Fits base w i)
    (dynamic : base + 2 ^ (solver.width (satInput formula).encode n).bits ≤ 2 ^ w.bits)
    (endpointFits : base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code < 2 ^ w.bits)
    (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 (base + 1))
    (savedBase : s.mem baseCell = BitVec.ofNat w.bits base)
    (fresh : ∀ a, base ≤ a → s.mem a = 0#w.bits) :
    ∃ total final, total ≤ formula.length * (22 * n + 29) + 7 * (satInput formula).encode.length +
        4 * (inputMagnitude (satInput formula).encode).log2 + 19 * solverTime + 36 ∧
      Runs widthConstant ((algorithm solver baseCell).program w) total s final ∧ final.halted = true ∧
      (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ (SATInstance.mk n formula).Satisfiable) ∧
      (∀ a, 32 ≤ a → a ≠ baseCell →
        (a < base ∨ base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code ≤ a) →
        final.mem a = s.mem a) ∧
      (∀ a, base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code ≤ a → final.mem a = 0#w.bits) ∧
      final.mem baseCell = BitVec.ofNat w.bits
        (base + SimulationFootprint.span (solver.width (satInput formula).encode n) solver.code) := by
  obtain ⟨time, called, bound, trace, halted, boolean, correct, frame, zero, native⟩ :=
    LeafCall.decides solver formula solverTime decision baseCell source base budget s pc live sourceBase cellBase cellBefore
      before fits variablesFit large space width fixed dynamic nodup input variables count pointer output savedBase fresh
  have baseValue : called.mem baseCell = BitVec.ofNat w.bits base :=
    (frame baseCell cellBase (Or.inl cellBefore)).trans savedBase
  have widthValue : called.mem 31 = BitVec.ofNat w.bits (solver.width (satInput formula).encode n).bits := by
    rw [native]
    exact BitVec.setWidth_ofNat_of_le_of_lt width (Nat.lt_pow_self (by decide))
  obtain ⟨allocateTime, out, allocateBound, allocateTrace, outHalt, free, af⟩ :=
    SimulationAllocate.allocates baseCell base (solver.width (satInput formula).encode n).bits
      (SimulationBounds.programBound solver.code + 1) (SourceChain.resume called) rfl rfl cellBase width endpointFits
      baseValue widthValue
  have full := SourceChain.traces (LeafCall.algorithm solver baseCell).code
    (SimulationAllocate.algorithm baseCell (SimulationBounds.programBound solver.code + 1)).code
    s called out time allocateTime live halted trace allocateTrace
  have answer : out.mem 0 = called.mem 0 := af 0 (by decide) (by omega)
  refine ⟨time + allocateTime, out.relocate (LeafCall.algorithm solver baseCell).code.length,
    by omega, full, outHalt, ?_, ?_, ?_, ?_, free⟩
  · simpa only [State.relocate, answer] using boolean
  · simpa only [State.relocate, answer] using correct
  · intro a ha different outside
    exact (af a (by omega) different).trans (frame a ha outside)
  · intro a ha
    have baseLe : base ≤ a := by omega
    exact (af a (by omega) (by omega)).trans (zero a ha)

end WordRAM.Conjectures.Sparsification.AllocatedLeafCall

/-! Register preparation and Boolean accumulation for the leaf-stack loop.
The exhausted DFS todo cell is reused as the accumulated answer. -/
namespace WordRAM.Conjectures.Sparsification.LeafControls
open TraversalBody
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def prepare (k : Nat) : Algorithm :=
  ⟨[.copy (.direct 16) (reg (variableCell k)), .copy (.direct 11) (reg 17),
    .copy (.direct 12) (reg 18), .binary .add (.direct 13) (reg (freeCell k)) (.immediate 1), .halt], 1, by decide⟩

def accumulate (k : Nat) : Algorithm :=
  ⟨[.binary .bor (.direct (todoCell k)) (reg (todoCell k)) (reg 0), .halt], 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) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 16 = s.mem (variableCell k) ∧
      t.mem 11 = s.mem 17 ∧ t.mem 12 = s.mem 18 ∧ t.mem 13 = s.mem (freeCell k) + 1#w.bits ∧
      (∀ a, 32 ≤ a → t.mem a = s.mem a) := by
  have different : freeCell k ≠ 11 ∧ freeCell k ≠ 12 ∧ freeCell k ≠ 16 := by
    dsimp [freeCell, variableCell]; omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, different, Nat.add_assoc]
  intro a ha
  have h : a ≠ 11 ∧ a ≠ 12 ∧ a ≠ 13 ∧ a ≠ 16 := by omega
  simp [h]

theorem accumulates (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((accumulate k).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem (todoCell k) = s.mem (todoCell k) ||| s.mem 0 ∧
      (∀ a, a ≠ todoCell k → t.mem a = s.mem a) := by
  simp [accumulate, 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]

theorem or_boolean (a b : Word w) (ha : a = 0 ∨ a = 1) (hb : b = 0 ∨ b = 1) :
    (a ||| b = 0 ∨ a ||| b = 1) ∧ (a ||| b = 1 ↔ a = 1 ∨ b = 1) := by
  rcases ha with rfl | rfl <;> rcases hb with rfl | rfl <;> simp

end WordRAM.Conjectures.Sparsification.LeafControls

/-! A complete iteration over the emitted leaf stack, including its SAT call. -/
namespace WordRAM.Conjectures.Sparsification.LeafBody
open TraversalBody SimulationExecution

def endpoint (solver : Algorithm) (formula : CNF n) (base : Nat) : Nat :=
  base + SimulationFootprint.span (solver.width (LeafCall.satInput formula).encode n) solver.code

def algorithm (solver : Algorithm) (k : Nat) : Algorithm :=
  ⟨SourceChain.code (StackMachine.pop (outputCell k)).code
    (SourceChain.code (LeafControls.prepare k).code
      (SourceChain.code (AllocatedLeafCall.algorithm solver (freeCell k)).code (LeafControls.accumulate k).code)), 1, by decide⟩

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

set_option maxRecDepth 4096 in
theorem step (solver : Algorithm) (k : Nat) (task : StackInvariant.Task n) (tasks : List (StackInvariant.Task n))
    (head base budget solverTime : Nat) (s : State w)
    (decision : DecidesIn solver (LeafCall.satInput task.formula).encode n solverTime (LeafCall.satInput task.formula).Satisfiable)
    (pc : s.pc = 0) (live : s.halted = false)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 2 ≤ w.bits)
    (space : base + 3 + task.formula.length * (1 + 4 * n) ≤ budget)
    (width : (solver.width (LeafCall.satInput task.formula).encode n).bits ≤ w.bits)
    (fixed : ∀ i ∈ solver.code, Fits base w i)
    (dynamic : base + 2 ^ (solver.width (LeafCall.satInput task.formula).encode n).bits ≤ 2 ^ w.bits)
    (endpointFits : endpoint solver task.formula base < 2 ^ w.bits)
    (nodup : ∀ clause ∈ task.formula, clause.Nodup)
    (pending : StackInvariant.Stored s.mem (dataBase k) base head (task :: tasks))
    (variables : s.mem (variableCell k) = BitVec.ofNat w.bits n)
    (headPointer : s.mem (outputCell k) = BitVec.ofNat w.bits head)
    (freePointer : s.mem (freeCell k) = BitVec.ofNat w.bits base)
    (answer : s.mem (todoCell k) = 0 ∨ s.mem (todoCell k) = 1)
    (fresh : ∀ a, base ≤ a → s.mem a = 0#w.bits) :
    ∃ time final next, time ≤ task.formula.length * (22 * n + 29) + 7 * (LeafCall.satInput task.formula).encode.length +
        4 * (inputMagnitude (LeafCall.satInput task.formula).encode).log2 + 19 * solverTime + 50 ∧
      Runs widthConstant ((algorithm solver k).program w) time s final ∧ final.halted = true ∧
      StackInvariant.Stored final.mem (dataBase k) (endpoint solver task.formula base) next tasks ∧
      final.mem (variableCell k) = BitVec.ofNat w.bits n ∧ final.mem (outputCell k) = BitVec.ofNat w.bits next ∧
      final.mem (freeCell k) = BitVec.ofNat w.bits (endpoint solver task.formula base) ∧
      (final.mem (todoCell k) = 0 ∨ final.mem (todoCell k) = 1) ∧
      (final.mem (todoCell k) = 1 ↔ s.mem (todoCell k) = 1 ∨ (SATInstance.mk n task.formula).Satisfiable) ∧
      (∀ a, endpoint solver task.formula base ≤ a → final.mem a = 0#w.bits) ∧
      (∀ a, dataBase k ≤ a → (a < base ∨ endpoint solver task.formula base ≤ a) → final.mem a = s.mem a) := by
  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
  have taskBase := pending.2.2.1
  have taskEnd := pending.2.2.2.1
  have grows : base ≤ endpoint solver task.formula base := Nat.le_add_right _ _
  obtain ⟨next, popped, popTrace, popHalt, ptr, cnt, head', pending', table, popFrame⟩ :=
    StackInvariant.pop tasks task s (outputCell k) (dataBase k) base head pc live (by omega) (by omega)
      (by omega) pending headPointer
  let prepared := run widthConstant ((LeafControls.prepare k).program w) 5 (SourceChain.resume popped)
  obtain ⟨ph, pt, pv, pn, pp, pd, pf⟩ := LeafControls.prepares k (SourceChain.resume popped) rfl rfl
  have same (a : Nat) (ha : dataBase k ≤ a) : prepared.mem a = s.mem a :=
    (pf a (by omega)).trans (popFrame a (by omega) (by omega) (by omega) (by omega))
  have high (a : Nat) (ha : 32 ≤ a) (different : a ≠ outputCell k) : prepared.mem a = s.mem a :=
    (pf a ha).trans (popFrame a (by omega) (by omega) (by omega) different)
  have input : 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)
  have vars : prepared.mem 16 = BitVec.ofNat w.bits n :=
    pv.trans ((popFrame (variableCell k) (by omega) (by omega) (by omega) (by omega)).trans variables)
  have free : prepared.mem (freeCell k) = BitVec.ofNat w.bits base := (high _ (by omega) (by omega)).trans freePointer
  have dest : prepared.mem 13 = BitVec.ofNat w.bits (base + 1) := by
    rw [pd, SourceChain.resume, popFrame (freeCell k) (by omega) (by omega) (by omega) (by omega), freePointer, ← BitVec.ofNat_add]
  obtain ⟨callTime, called, callBound, callTrace, callHalt, boolean, correct, frame, zero, allocated⟩ :=
    AllocatedLeafCall.decides solver task.formula solverTime decision (freeCell k) task.address base budget
      (SourceChain.resume prepared) rfl rfl (by omega) (by omega) (by omega) taskEnd fits variablesFit large space
      width fixed dynamic endpointFits nodup input vars (pn.trans cnt) (pp.trans ptr) dest free
      (fun a ha => (same a (by omega)).trans (fresh a ha))
  have calledAnswer : called.mem (todoCell k) = s.mem (todoCell k) :=
    (frame _ (by omega) (by omega) (Or.inl (by omega))).trans (high _ (by omega) (by omega))
  let final := run widthConstant ((LeafControls.accumulate k).program w) 2 (SourceChain.resume called)
  obtain ⟨fh, ft, accumulated, ff⟩ := LeafControls.accumulates k (SourceChain.resume called) rfl rfl
  have orFacts := LeafControls.or_boolean (s.mem (todoCell k)) (called.mem 0) answer boolean
  have finalAnswer : final.mem (todoCell k) = s.mem (todoCell k) ||| called.mem 0 := by
    change final.mem (todoCell k) = called.mem (todoCell k) ||| called.mem 0 at accumulated
    rw [accumulated, calledAnswer]
  have finalFrame (a : Nat) (ha : dataBase k ≤ a) (outside : a < base ∨ endpoint solver task.formula base ≤ a) :
      final.mem a = s.mem a :=
    (ff a (by omega)).trans ((frame a (by omega) (by omega) outside).trans (same a ha))
  have finalPending : StackInvariant.Stored final.mem (dataBase k) (endpoint solver task.formula base) next tasks := by
    apply StackInvariant.weaken tasks final.mem (dataBase k) base _ next _ grows
    apply StackInvariant.frame tasks popped.mem final.mem (dataBase k) base next pending'
    intro a ha hb
    exact (ff a (by omega)).trans ((frame a (by omega) (by omega) (Or.inl hb)).trans (pf a (by omega)))
  have finalVariables : final.mem (variableCell k) = BitVec.ofNat w.bits n :=
    (ff _ (by omega)).trans ((frame _ (by omega) (by omega) (Or.inl (by omega))).trans
      ((high _ (by omega) (by omega)).trans variables))
  have finalHead : final.mem (outputCell k) = BitVec.ofNat w.bits next :=
    (ff _ (by omega)).trans ((frame _ (by omega) (by omega) (Or.inl (by omega))).trans ((pf _ (by omega)).trans head'))
  have finalFree : final.mem (freeCell k) = BitVec.ofNat w.bits (endpoint solver task.formula base) :=
    (ff _ (by omega)).trans allocated
  have tailTrace := SourceChain.traces (AllocatedLeafCall.algorithm solver (freeCell k)).code (LeafControls.accumulate k).code
    (SourceChain.resume prepared) called final callTime 2 rfl callHalt callTrace (trace_of_ticks _ _ 2 ft)
  have middleTrace := SourceChain.traces (LeafControls.prepare k).code
    (SourceChain.code (AllocatedLeafCall.algorithm solver (freeCell k)).code (LeafControls.accumulate k).code)
    (SourceChain.resume popped) prepared (final.relocate (AllocatedLeafCall.algorithm solver (freeCell k)).code.length)
    5 (callTime + 2) rfl ph (trace_of_ticks _ _ 5 pt) tailTrace
  have full := SourceChain.traces (StackMachine.pop (outputCell k)).code
    (SourceChain.code (LeafControls.prepare k).code
      (SourceChain.code (AllocatedLeafCall.algorithm solver (freeCell k)).code (LeafControls.accumulate k).code))
    s popped ((final.relocate (AllocatedLeafCall.algorithm solver (freeCell k)).code.length).relocate (LeafControls.prepare k).code.length)
    7 (5 + (callTime + 2)) live popHalt popTrace middleTrace
  refine ⟨7 + (5 + (callTime + 2)),
    (((final.relocate (AllocatedLeafCall.algorithm solver (freeCell k)).code.length).relocate (LeafControls.prepare k).code.length).relocate
      (StackMachine.pop (outputCell k)).code.length), next, by omega, full, fh, finalPending,
      finalVariables, finalHead, finalFree, ?_, ?_, ?_, finalFrame⟩
  · simpa only [State.relocate, finalAnswer] using orFacts.1
  · simpa only [State.relocate, finalAnswer, correct] using orFacts.2
  · intro a ha
    exact (ff a (by omega)).trans (zero a ha)

end WordRAM.Conjectures.Sparsification.LeafBody