Prove2Me

SETH ⇒ OVC sparsification bundle 36: concrete word-RAM formalization

Definition
SETHOV_Sparsification_36

by wurtle · Nov 2, 2026 · Mathlib 0df444a (Lean v4.33.1)

fine-grained-complexityorthogonal-vectorssethsparsificationword-ram

Bundle 36 of the machine-checked formalization of the algorithmic sparsification transfer used in the proof that SETH implies the Orthogonal Vectors Conjecture on a concrete word RAM. It contains the fixed word-RAM programs that normalize, serialize, search, allocate and emit the sparsified leaf family. The bundle is self-contained over the preceding bundles and the platform WordRAM definitions, and every declaration is proved with no axioms or placeholders.

Definition code
import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_35

set_option autoImplicit true

/-! One complete flower-selection and branching stage. -/
namespace WordRAM.Conjectures.Sparsification.SelectBranch

def leaf : Algorithm := ⟨[.halt], 1, by decide⟩

def dispatch : Algorithm :=
  ⟨SourceIf.code 0 leaf.code SelectedBranch.algorithm.code, 1, by decide⟩

def algorithm (threshold : Nat → Nat) (k : Nat) : Algorithm :=
  ⟨SourceChain.code (FlowerSearch.initialized threshold k).code dispatch.code, 1, by decide⟩

def Outcome (formula : CNF n) (source : Nat) (choice : Option (Nat × Clause n)) (mem : Memory w) : Prop :=
  match choice with
  | none => mem 0 = 0#w.bits ∧ mem 16 = BitVec.ofNat w.bits n ∧
      mem 17 = BitVec.ofNat w.bits formula.length ∧ mem 18 = BitVec.ofNat w.bits source ∧
      VectorBuilder.Stored mem source (RecordTable.words w formula)
  | some (size, core) => SelectedBranch.Children formula core size source mem

def cost (n k bits m : Nat) : Nat :=
  ((k + 1) * (k + 1)) * (FlowerSearch.coreBound n k bits m + 5) +
    10 * k + (12 * bits + 396) * (m + 1) ^ 2 + 35

theorem leaf_trace (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (leaf.program w) 1 s
    Runs widthConstant (leaf.program w) 1 s t ∧ t.halted = true ∧ t.mem = s.mem := by
  have ticks : (run widthConstant (leaf.program w) 1 s).ticks = s.ticks + 1 := by
    simp [leaf, Algorithm.program, SourceInstruction.compile, run, step, execute, pc, live]
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (leaf.program w) 1 s
  have cost := runs_cost trace
  have eq : time = 1 := by omega
  subst time
  refine ⟨trace, ?_, ?_⟩ <;> simp [leaf, Algorithm.program, SourceInstruction.compile, run, step, execute, pc, live]

set_option maxRecDepth 4096 in
/-- Exact agreement with the original ordered selector. A zero flag denotes
no flower; a one flag accompanies the two exact mathematical child tables.
No abstract search or branch oracle is assumed. -/
theorem selects_and_branches (formula : CNF n) (threshold : Nat → Nat) (k source : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (sourceBase : 64 ≤ source) (searchSpace : 32 + 3 * k ≤ source)
    (fits : BranchLayout.finish source formula.length < 2 ^ 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)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula)) :
    ∃ time final, time ≤ cost n k w.bits formula.length ∧
      Runs widthConstant ((algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      Outcome formula source (Selection.select formula threshold k) final.mem ∧
      (∀ a, 64 ≤ a → 32 + 3 * k ≤ a →
        (a < source + 3 * formula.length ∨ BranchLayout.finish source formula.length ≤ a) → final.mem a = s.mem a) := by
  have order := BranchLayout.ordered source formula.length
  have tableFits : source + 3 * formula.length < 2 ^ w.bits := by
    change BranchLayout.remaining source formula.length < 2 ^ w.bits
    omega
  obtain ⟨time, selected, bound, trace, halted, outcome, _, frame⟩ :=
    FlowerSearch.selects_initialized formula threshold k s source pc live width variablesFit searchSpace tableFits
      thresholdFits nodup variables count pointer input
  have selectedInput : VectorBuilder.Stored selected.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact frame a (Or.inr (by omega)) (by omega)
  have selectedVariables : selected.mem 16 = BitVec.ofNat w.bits n :=
    (frame 16 (Or.inl ⟨by decide, by decide⟩) (by decide)).trans variables
  have selectedCount : selected.mem 17 = BitVec.ofNat w.bits formula.length :=
    (frame 17 (Or.inl ⟨by decide, by decide⟩) (by decide)).trans count
  have selectedPointer : selected.mem 18 = BitVec.ofNat w.bits source :=
    (frame 18 (Or.inl ⟨by decide, by decide⟩) (by decide)).trans pointer
  cases choice : Selection.select formula threshold k with
  | none =>
    have zero : selected.mem 0 = 0#w.bits := by simpa only [choice, FlowerSearch.Outcome] using outcome
    let entry := SourceChain.resume selected
    let out := run widthConstant (leaf.program w) 1 (entry.addTicks 1)
    obtain ⟨lt, lh, lm⟩ := leaf_trace (entry.addTicks 1) rfl rfl
    have dispatched := SourceIf.zero_trace 0 leaf.code SelectedBranch.algorithm.code entry out 1 rfl rfl zero lt
    have full := SourceChain.traces (FlowerSearch.initialized threshold k).code dispatch.code s selected _ time 2
      live halted trace dispatched
    refine ⟨time + 2, (out.relocate (1 + SelectedBranch.algorithm.code.length)).relocate
      (FlowerSearch.initialized threshold k).code.length, ?_, full, lh, ?_, ?_⟩
    · unfold cost; omega
    · change out.mem 0 = 0#w.bits ∧ out.mem 16 = BitVec.ofNat w.bits n ∧
        out.mem 17 = BitVec.ofNat w.bits formula.length ∧ out.mem 18 = BitVec.ofNat w.bits source ∧
        VectorBuilder.Stored out.mem source (RecordTable.words w formula)
      rw [show out.mem = selected.mem from lm]
      exact ⟨zero, selectedVariables, selectedCount, selectedPointer, selectedInput⟩
    · intro a ha hs _
      exact (congrFun lm a).trans (frame a (Or.inr hs) (by omega))
  | some pair =>
    rcases pair with ⟨size, core⟩
    have sound := Selection.select_sound formula threshold k choice
    have lengthBound : core.length < size := sound.1.2.2.1
    have sizeBound : size ≤ k := sound.2
    have coreFits : CoreSearchLayout.coreBase core.length + 2 * core.length < 2 ^ w.bits := by
      dsimp [CoreSearchLayout.coreBase]
      omega
    have sizeFits : size < 2 ^ w.bits := by omega
    have chosen : FlowerSearch.Outcome (some (size, core)) selected.mem := by simpa only [choice] using outcome
    let entry := SourceChain.resume selected
    obtain ⟨branchTime, out, branchBound, branchTrace, branchHalt, children, branchFrame⟩ :=
      SelectedBranch.builds formula core size source (entry.addTicks 1) rfl rfl variablesFit width sizeFits nodup
        sourceBase fits coreFits chosen selectedInput selectedCount selectedPointer
    have nonzero : entry.mem 0 ≠ 0#w.bits := by
      change selected.mem 0 ≠ 0#w.bits
      rw [chosen.1]
      intro h
      have values := congrArg BitVec.toNat h
      have oneFits : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by omega)
      simp [Nat.mod_eq_of_lt oneFits] at values
    have dispatched := SourceIf.nonzero_trace 0 leaf.code SelectedBranch.algorithm.code entry out branchTime rfl rfl nonzero branchTrace
    have full := SourceChain.traces (FlowerSearch.initialized threshold k).code dispatch.code s selected _
      time (1 + branchTime) live halted trace dispatched
    refine ⟨time + (1 + branchTime), (out.relocate 1).relocate (FlowerSearch.initialized threshold k).code.length,
      ?_, full, branchHalt, children, ?_⟩
    · unfold cost; omega
    · intro a ha hs outside
      exact (branchFrame a ha outside).trans (frame a (Or.inr hs) (by omega))

end WordRAM.Conjectures.Sparsification.SelectBranch

/-! Reject an input containing an empty clause before sparse-leaf processing. -/
namespace WordRAM.Conjectures.Sparsification.EmptyClause

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 1) (.immediate 0), .copy (.direct 2) (.immediate 0),
    .copy (.direct 11) (reg 17), .copy (.direct 12) (reg 18), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SubsumptionScan.algorithm false).code, 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 1 = 0#w.bits ∧ t.mem 2 = 0#w.bits ∧
      t.mem 11 = s.mem 17 ∧ t.mem 12 = s.mem 18 ∧ (∀ a, 16 ≤ a → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a ha
  have h : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 11 ∧ a ≠ 12 := by omega
  simp [h]

/-- The scan recognizes exactly membership of the empty clause, including
non-normalized formulas, and preserves all formula and persistent-control memory. -/
theorem detects (formula : CNF n) (s : State w) (source : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ source)
    (fits : source + 3 * formula.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (count : s.mem 17 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits source)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula)) :
    ∃ time final, time ≤ 12 * formula.length + 8 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if [] ∈ formula then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  let prepared := run widthConstant (prepare.program w) 5 s
  obtain ⟨ph, pt, pp, pn, pcnt, pptr, pf⟩ := prepares s pc live
  have preparedInput : VectorBuilder.Stored prepared.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact pf a (by omega)
  have pos : prepared.mem 1 = Masks.encode w ([] : Clause n) true := by simpa [Masks.encode, MaskBuilder.mask_nil] using pp
  have neg : prepared.mem 2 = Masks.encode w ([] : Clause n) false := by simpa [Masks.encode, MaskBuilder.mask_nil] using pn
  obtain ⟨time, out, bound, trace, halted, value, frame⟩ := SubsumptionScan.scans false [] formula
    (SourceChain.resume prepared) source rfl rfl base fits variablesFit pos neg (pptr.trans pointer) (pcnt.trans count) preparedInput
  have criterion : (∃ clause ∈ formula, SubsumptionScan.Related false ([] : Clause n) clause) ↔ [] ∈ formula := by
    simp [SubsumptionScan.Related]
  obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant (prepare.program w) 5 s
  have cost := runs_cost setupTrace
  have exactTicks : ticks = 5 := by omega
  subst ticks
  have full := SourceChain.traces prepare.code (SubsumptionScan.algorithm false).code s prepared out 5 time
    live ph setupTrace trace
  refine ⟨5 + time, out.relocate prepare.code.length, by omega, full, halted, ?_, ?_⟩
  · simpa only [criterion, State.relocate] using value
  · intro a ha
    exact (frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans (pf a ha)

end WordRAM.Conjectures.Sparsification.EmptyClause

/-! Move a pending table to fresh memory before allocating branch workspaces. -/
namespace WordRAM.Conjectures.Sparsification.RelocateTable

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

def prepare (freeCell : Nat) : Algorithm :=
  ⟨[.copy (.direct 1) (reg 18), .copy (.direct 2) (reg freeCell),
    .binary (.mul rfl) (.direct 3) (reg 17) (.immediate 3), .halt], 1, by decide⟩

def finish (freeCell : Nat) : Algorithm :=
  ⟨[.copy (.direct 18) (reg freeCell), .binary (.mul rfl) (.direct 0) (reg 17) (.immediate 3),
    .binary .add (.direct freeCell) (reg freeCell) (reg 0), .halt], 1, by decide⟩

def algorithm (freeCell : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare freeCell).code
    (SourceChain.code MemoryCopy.algorithm.code (finish freeCell).code), 1, by decide⟩

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

theorem finishes (freeCell : Nat) (base : 64 ≤ freeCell) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((finish freeCell).program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 18 = s.mem freeCell ∧
      t.mem freeCell = s.mem freeCell + s.mem 17 * 3#w.bits ∧
      (∀ a, a ≠ 0 → a ≠ 18 → a ≠ freeCell → t.mem a = s.mem a) := by
  have h : freeCell ≠ 18 ∧ freeCell ≠ 0 ∧ 18 ≠ freeCell := by omega
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, h, Nat.add_assoc]
  intro a h0 h18 hf; simp [h0, h18, hf]

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

/-- Preserve the old table and all other high memory, update the source pointer,
and advance the allocator past the fresh copy. Thus an older sibling can be
retained while this copy's following memory is used for branch construction. -/
theorem relocates (formula : CNF n) (freeCell source destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 64 ≤ freeCell) (controlBefore : freeCell < source)
    (separate : source + 3 * formula.length ≤ destination)
    (fits : destination + 3 * formula.length < 2 ^ w.bits)
    (pointer : s.mem 18 = BitVec.ofNat w.bits source)
    (count : s.mem 17 = BitVec.ofNat w.bits formula.length)
    (free : s.mem freeCell = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula)) :
    ∃ final, Runs widthConstant ((algorithm freeCell).program w) (21 * formula.length + 10) s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w formula) ∧
      VectorBuilder.Stored final.mem source (RecordTable.words w formula) ∧
      final.mem 18 = BitVec.ofNat w.bits destination ∧ final.mem 17 = BitVec.ofNat w.bits formula.length ∧
      final.mem freeCell = BitVec.ofNat w.bits (destination + 3 * formula.length) ∧
      (∀ a, 16 ≤ a → a ≠ 18 → a ≠ freeCell →
        (a < destination ∨ destination + 3 * formula.length ≤ a) → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare freeCell).program w) 4 s
  obtain ⟨ph, pt, pp, pd, pn, pf⟩ := prepares freeCell base s pc live
  have preparedInput : VectorBuilder.Stored prepared.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact pf a (by omega)
  have wordsCount : prepared.mem 3 = BitVec.ofNat w.bits (RecordTable.words w formula).length := by
    calc
      prepared.mem 3 = s.mem 17 * 3#w.bits := pn
      _ = BitVec.ofNat w.bits (RecordTable.words w formula).length := by
        rw [count, ← BitVec.ofNat_mul, RecordTable.words_length, Nat.mul_comm]
  obtain ⟨copied, ct, ch, table, cf⟩ := MemoryCopy.copies (RecordTable.words w formula) (SourceChain.resume prepared)
    source destination rfl rfl (by omega) (by simpa only [RecordTable.words_length] using separate)
    (by simpa only [RecordTable.words_length] using fits) (pp.trans pointer) (pd.trans free) wordsCount preparedInput
  have preservedFree : copied.mem freeCell = BitVec.ofNat w.bits destination :=
    (cf freeCell (by omega) (Or.inl (by omega))).trans ((pf freeCell (by omega)).trans free)
  have preservedCount : copied.mem 17 = BitVec.ofNat w.bits formula.length :=
    (cf 17 (by decide) (Or.inl (by omega))).trans ((pf 17 (by decide)).trans count)
  let out := run widthConstant ((finish freeCell).program w) 4 (SourceChain.resume copied)
  obtain ⟨oh, ot, op, ofree, ofr⟩ := finishes freeCell base (SourceChain.resume copied) rfl rfl
  have tail := SourceChain.traces MemoryCopy.algorithm.code (finish freeCell).code (SourceChain.resume prepared)
    copied out (7 * (RecordTable.words w formula).length + 2) 4 rfl ch ct (trace_of_ticks _ _ 4 ot)
  have full := SourceChain.traces (prepare freeCell).code (SourceChain.code MemoryCopy.algorithm.code (finish freeCell).code)
    s prepared _ 4 ((7 * (RecordTable.words w formula).length + 2) + 4) live ph (trace_of_ticks _ s 4 pt) tail
  have cost : 4 + ((7 * (RecordTable.words w formula).length + 2) + 4) = 21 * formula.length + 10 := by
    rw [RecordTable.words_length]; omega
  have finalFrame : ∀ a, 16 ≤ a → a ≠ 18 → a ≠ freeCell →
      (a < destination ∨ destination + 3 * formula.length ≤ a) → out.mem a = s.mem a := by
    intro a ha h18 hf outside
    exact (ofr a (by omega) h18 hf).trans
      ((cf a (by omega) (by simpa only [RecordTable.words_length] using outside)).trans (pf a (by omega)))
  refine ⟨(out.relocate MemoryCopy.algorithm.code.length).relocate (prepare freeCell).code.length,
    ?_, oh, ?_, ?_, op.trans preservedFree, ?_, ?_, finalFrame⟩
  · simpa only [algorithm, Algorithm.program, cost] using full
  · apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact ofr a (by omega) (by omega) (by omega)
  · apply MemoryCopy.stored_frame _ _ input
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact finalFrame a (by omega) (by omega) (by omega) (Or.inl (by omega))
  · exact (ofr 17 (by decide) (by decide) (by omega)).trans preservedCount
  · calc
      out.mem freeCell = copied.mem freeCell + copied.mem 17 * 3#w.bits := ofree
      _ = BitVec.ofNat w.bits (destination + 3 * formula.length) := by
        rw [preservedFree, preservedCount, ← BitVec.ofNat_mul, ← BitVec.ofNat_add, Nat.mul_comm formula.length]

end WordRAM.Conjectures.Sparsification.RelocateTable

/-! Linked pending-task stack stored outside the branch routine's scratch area. -/
namespace WordRAM.Conjectures.Sparsification.StackMachine

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

def prepare (headCell freeCell : Nat) : Algorithm :=
  ⟨[.copy (.direct 9) (reg 18), .copy (.direct 10) (reg 17), .copy (.direct 0) (reg headCell),
    .copy (.direct 13) (reg freeCell), .copy (.direct 14) (.immediate 0), .halt], 1, by decide⟩

def finish (headCell freeCell : Nat) : Algorithm :=
  ⟨[.copy (.direct headCell) (reg freeCell), .copy (.direct freeCell) (reg 13), .halt], 1, by decide⟩

/-- Push the table pointer/count in 18/17 and link the old head as the third word. -/
def push (headCell freeCell : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare headCell freeCell).code
    (SourceChain.code RecordAppend.algorithm.code (finish headCell freeCell).code), 1, by decide⟩

/-- Pop a nonempty head node, loading table pointer/count into 18/17. -/
def pop (headCell : Nat) : Algorithm :=
  ⟨[.copy (.direct 12) (reg headCell), .copy (.direct 18) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 17) (.memory (.indirect 12)), .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct headCell) (.memory (.indirect 12)), .halt], 1, by decide⟩

theorem prepares (headCell freeCell : Nat) (hb : 64 ≤ headCell) (fb : 64 ≤ freeCell)
    (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((prepare headCell freeCell).program w) 6 s
    t.halted = true ∧ t.ticks = s.ticks + 6 ∧ t.mem 9 = s.mem 18 ∧ t.mem 10 = s.mem 17 ∧
      t.mem 0 = s.mem headCell ∧ t.mem 13 = s.mem freeCell ∧ t.mem 14 = 0#w.bits ∧
      (∀ a, 16 ≤ a → t.mem a = s.mem a) := by
  have h : headCell ≠ 9 ∧ headCell ≠ 10 ∧ freeCell ≠ 9 ∧ freeCell ≠ 10 ∧ freeCell ≠ 0 := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, h, Nat.add_assoc]
  intro a ha
  have h : a ≠ 9 ∧ a ≠ 10 ∧ a ≠ 0 ∧ a ≠ 13 ∧ a ≠ 14 := by omega
  simp [h]

theorem finishes (headCell freeCell : Nat) (hb : 64 ≤ headCell) (distinct : headCell ≠ freeCell)
    (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((finish headCell freeCell).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem headCell = s.mem freeCell ∧ t.mem freeCell = s.mem 13 ∧
      (∀ a, a ≠ headCell → a ≠ freeCell → t.mem a = s.mem a) := by
  have h : 13 ≠ headCell := by omega
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, h, distinct, Nat.add_assoc]
  intro a hh hf; simp [hh, hf]

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

theorem pushes (headCell freeCell destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (fb : 64 ≤ freeCell)
    (distinct : headCell ≠ freeCell) (headBefore : headCell < destination) (freeBefore : freeCell < destination)
    (fits : destination + 2 < 2 ^ w.bits) (pointer : s.mem freeCell = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant ((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) ∧
      VectorBuilder.Stored final.mem destination [s.mem 18, s.mem 17, s.mem headCell] ∧
      (∀ a, 16 ≤ a → a ≠ headCell → a ≠ freeCell → (a < destination ∨ destination + 3 ≤ a) → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare headCell freeCell).program w) 6 s
  obtain ⟨ph, pt, pp, pn, pl, pd, _, pf⟩ := prepares headCell freeCell hb fb s pc live
  let appended := run widthConstant (RecordAppend.algorithm.program w) 8 (SourceChain.resume prepared)
  obtain ⟨ah, aticks, ap, _, a0, a1, a2, af⟩ := RecordAppend.executes (SourceChain.resume prepared)
    destination rfl rfl (by omega) fits (pd.trans pointer)
  have savedFree : appended.mem freeCell = BitVec.ofNat w.bits destination :=
    (af freeCell (by omega) (by omega) (by omega) (by omega) (by omega)).trans ((pf freeCell (by omega)).trans pointer)
  let out := run widthConstant ((finish headCell freeCell).program w) 3 (SourceChain.resume appended)
  obtain ⟨oh, ot, op, ofree, ofr⟩ := finishes headCell freeCell hb distinct (SourceChain.resume appended) rfl rfl
  have tail := SourceChain.traces RecordAppend.algorithm.code (finish headCell freeCell).code
    (SourceChain.resume prepared) appended out 8 3 rfl ah (trace_of_ticks _ _ 8 aticks) (trace_of_ticks _ _ 3 ot)
  have full := SourceChain.traces (prepare headCell freeCell).code
    (SourceChain.code RecordAppend.algorithm.code (finish headCell freeCell).code) s prepared _ 6 (8 + 3)
    live ph (trace_of_ticks _ s 6 pt) tail
  refine ⟨(out.relocate RecordAppend.algorithm.code.length).relocate (prepare headCell freeCell).code.length,
    full, oh, op.trans savedFree, ofree.trans ap, ?_, ?_⟩
  · exact ⟨(ofr destination (by omega) (by omega)).trans (a0.trans pp),
      (ofr (destination + 1) (by omega) (by omega)).trans (a1.trans pn),
      (ofr (destination + 2) (by omega) (by omega)).trans (a2.trans pl), trivial⟩
  · intro a ha hh hf outside
    exact (ofr a hh hf).trans ((af a (by omega) (by omega) (by omega) (by omega) (by omega)).trans (pf a ha))

theorem pops (headCell address : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (headBefore : headCell < address)
    (fits : address + 2 < 2 ^ w.bits) (pointer : s.mem headCell = BitVec.ofNat w.bits address) :
    let t := run widthConstant ((pop headCell).program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧ t.mem 18 = s.mem address ∧
      t.mem 17 = s.mem (address + 1) ∧ t.mem headCell = s.mem (address + 2) ∧
      (∀ a, a ≠ 12 → a ≠ 17 → a ≠ 18 → a ≠ headCell → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits address).toNat = address := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits address + 1#w.bits).toNat = address + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt (by omega)
  have d2 : (BitVec.ofNat w.bits address + 1#w.bits + 1#w.bits).toNat = address + 2 := by
    rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low0 : ∀ i, i ≤ 18 → address ≠ i := by omega
  have low1 : ∀ i, i ≤ 18 → address + 1 ≠ i := by omega
  have low2 : ∀ i, i ≤ 18 → address + 2 ≠ i := by omega
  have hh : headCell ≠ 17 ∧ headCell ≠ 18 ∧ 17 ≠ headCell ∧ 18 ≠ headCell := by omega
  simp [pop, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, d0, d1, d2,
    low0, low1, low2, hh, Nat.add_assoc, -BitVec.toNat_add]
  intro a h12 h17 h18 hh; simp [h12, h17, h18, hh]

theorem pop_trace (headCell address : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (hb : 64 ≤ headCell) (headBefore : headCell < address)
    (fits : address + 2 < 2 ^ w.bits) (pointer : s.mem headCell = BitVec.ofNat w.bits address) :
    Runs widthConstant ((pop headCell).program w) 7 s (run widthConstant ((pop headCell).program w) 7 s) :=
  trace_of_ticks _ _ 7 (pops headCell address s pc live hb headBefore fits pointer).2.1

end WordRAM.Conjectures.Sparsification.StackMachine
Source
Impagliazzo, Paturi and Zane, Which problems have strongly exponential complexity?, J. Comput. Syst. Sci. 63(4):512–530, 2001, Corollary 1 (p. 523), https://doi.org/10.1006/jcss.2001.1774; user-supplied WordRAM project, git commit 68be5b4418cf34d8d990686d0b9c09a85cfc641b (sparsification transfer development).

View graph