Prove2Me

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

Definition
SETHOV_Sparsification_35

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

fine-grained-complexityorthogonal-vectorssethsparsificationword-ram

Bundle 35 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_34

set_option autoImplicit true

/-! A uniform polynomial bound for one complete branching operation. -/
namespace WordRAM.Conjectures.Sparsification.BranchCost

theorem children (a b m : Nat) (partition : a + b ≤ m) :
    BothChildren.cost a b ≤ 260 * (m + 1) ^ 2 := by
  have first := Nat.mul_le_mul (show a + 1 ≤ m + 1 by omega)
    (show 35 * (a + 1) + 55 ≤ 35 * (m + 1) + 55 by omega)
  have second := Nat.mul_le_mul (show a + b ≤ m + 1 by omega)
    (show 35 * (a + b) + 55 ≤ 35 * (m + 1) + 55 by omega)
  have linear : m + 1 ≤ (m + 1) * (m + 1) := Nat.le_mul_of_pos_left (m + 1) (by omega)
  have normal : (m + 1) * (35 * (m + 1) + 55) =
      35 * ((m + 1) * (m + 1)) + 55 * (m + 1) := by
    rw [Nat.mul_add]
    ac_rfl
  rw [normal] at first second
  unfold BothChildren.cost
  rw [Nat.pow_two]
  omega

/-- The bound depends only on the input clause count and word width, not the
selected core or the sizes of the two partition outputs. -/
theorem branch (formula : CNF n) (core : Clause n) (size bits : Nat) :
    formula.length * (12 * bits + 86) + 12 * bits + 50 +
      BothChildren.cost (Branch.remaining formula core size).length (BranchTables.petals formula core size).length ≤
    (12 * bits + 396) * (formula.length + 1) ^ 2 := by
  have partition := BranchTables.partition_length formula core size
  have childBound := children _ _ formula.length (Nat.le_of_eq partition)
  have linear : formula.length + 1 ≤ (formula.length + 1) ^ 2 := by
    rw [Nat.pow_two]
    exact Nat.le_mul_of_pos_left _ (by omega)
  have timesWidth := Nat.mul_le_mul_left (12 * bits) linear
  have normal : formula.length * (12 * bits + 86) + 12 * bits + 50 =
      12 * bits * (formula.length + 1) + 86 * formula.length + 50 := by
    simp only [Nat.mul_add, Nat.mul_one]
    ac_rfl
  rw [normal, Nat.add_mul]
  omega

end WordRAM.Conjectures.Sparsification.BranchCost

/-! A uniform memory allocation for branching, based only on input size. -/
namespace WordRAM.Conjectures.Sparsification.BranchLayout

def remaining (source m : Nat) : Nat := source + 3 * m
def petals (source m : Nat) : Nat := remaining source m + 3 * m
def core (source m : Nat) : Nat := petals source m + 3 * m
def leftRaw (source m : Nat) : Nat := core source m + 3
def leftWork (source m : Nat) : Nat := leftRaw source m + 3 * (m + 1)
def rightRaw (source m : Nat) : Nat := leftWork source m + (m + 1) * (3 * (m + 2))
def rightWork (source m : Nat) : Nat := rightRaw source m + 3 * m
def finish (source m : Nat) : Nat := rightWork source m + m * (3 * (m + 1))

theorem ordered (source m : Nat) :
    source ≤ remaining source m ∧ remaining source m ≤ petals source m ∧
      petals source m ≤ core source m ∧ core source m ≤ leftRaw source m ∧
      leftRaw source m ≤ leftWork source m ∧ leftWork source m ≤ rightRaw source m ∧
      rightRaw source m ≤ rightWork source m ∧ rightWork source m ≤ finish source m := by
  simp only [remaining, petals, core, leftRaw, leftWork, rightRaw, rightWork, finish]
  omega

theorem partition (w : Width) (source m : Nat) (base : 64 ≤ source) (fits : finish source m < 2 ^ w.bits) :
    PartitionInvariant.Layout w m source (remaining source m) (petals source m) := by
  have order := ordered source m
  refine ⟨by omega, by simp [remaining], by simp [petals], ?_⟩
  change core source m < 2 ^ w.bits
  omega

/-- Actual partition counts need not be known when reserving the buffers. -/
theorem children (w : Width) (source m a b : Nat) (base : 64 ≤ source)
    (total : a + b = m) (fits : finish source m < 2 ^ w.bits) :
    BothChildren.Layout w a b (remaining source m) (petals source m) (core source m)
      (leftRaw source m) (leftWork source m) (rightRaw source m) (rightWork source m) := by
  have order := ordered source m
  have al : a ≤ m := by omega
  have bl : b ≤ m := by omega
  have capacity := Nat.mul_le_mul (show a + 1 ≤ m + 1 by omega)
    (show 3 * (a + 2) ≤ 3 * (m + 2) by omega)
  refine ⟨by omega, by omega, by omega, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · simp only [remaining, petals, core, leftRaw]; omega
  · simp only [petals, core, leftRaw]; omega
  · simp [leftRaw]
  · simp only [leftWork]; omega
  · simp only [rightRaw]; omega
  · simp only [rightWork]; omega
  · simpa only [total, finish] using fits

/-- Quadratic workspace, including both partition buffers, the core record,
both raw children, and both normalization regions. -/
theorem space_bound (source m : Nat) : finish source m ≤ source + 48 * (m + 1) ^ 2 := by
  simp only [finish, rightWork, rightRaw, leftWork, leftRaw, core, petals, remaining,
    Nat.pow_two, Nat.mul_add, Nat.add_mul, Nat.mul_one, Nat.one_mul]
  simp only [← Nat.mul_assoc]
  have three : m * 3 * m = 3 * (m * m) := by ac_rfl
  have fortyEight : 48 * m * m = 48 * (m * m) := by ac_rfl
  rw [three, fortyEight]
  omega

end WordRAM.Conjectures.Sparsification.BranchLayout

/-! Compute the uniform branch-buffer addresses with actual word arithmetic. -/
namespace WordRAM.Conjectures.Sparsification.BranchAllocate

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

def algorithm : Algorithm :=
  ⟨[.binary (.mul rfl) (.direct 0) (reg 24) (.immediate 3),
    .binary .add (.direct 18) (reg 23) (reg 0),
    .binary .add (.direct 19) (reg 18) (reg 0),
    .binary .add (.direct 38) (reg 19) (reg 0),
    .binary .add (.direct 39) (reg 38) (.immediate 3),
    .binary .add (.direct 1) (reg 24) (.immediate 1),
    .binary (.mul rfl) (.direct 2) (reg 1) (.immediate 3),
    .binary .add (.direct 40) (reg 39) (reg 2),
    .binary .add (.direct 3) (reg 24) (.immediate 2),
    .binary (.mul rfl) (.direct 4) (reg 2) (reg 3),
    .binary .add (.direct 41) (reg 40) (reg 4),
    .binary .add (.direct 42) (reg 41) (reg 0),
    .binary (.mul rfl) (.direct 5) (reg 24) (reg 2),
    .binary .add (.direct 49) (reg 42) (reg 5), .halt], 1, by decide⟩

theorem allocates (source m : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (pointer : s.mem 23 = BitVec.ofNat w.bits source) (count : s.mem 24 = BitVec.ofNat w.bits m) :
    let t := run widthConstant (algorithm.program w) 15 s
    t.halted = true ∧ t.ticks = s.ticks + 15 ∧
      t.mem 18 = BitVec.ofNat w.bits (BranchLayout.remaining source m) ∧
      t.mem 19 = BitVec.ofNat w.bits (BranchLayout.petals source m) ∧
      t.mem 38 = BitVec.ofNat w.bits (BranchLayout.core source m) ∧
      t.mem 39 = BitVec.ofNat w.bits (BranchLayout.leftRaw source m) ∧
      t.mem 40 = BitVec.ofNat w.bits (BranchLayout.leftWork source m) ∧
      t.mem 41 = BitVec.ofNat w.bits (BranchLayout.rightRaw source m) ∧
      t.mem 42 = BitVec.ofNat w.bits (BranchLayout.rightWork source m) ∧
      t.mem 49 = BitVec.ofNat w.bits (BranchLayout.finish source m) ∧
      (∀ a, (20 ≤ a ∧ a ≤ 24) ∨ 64 ≤ a → 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, pc, live, Nat.add_assoc,
    pointer, count, BranchLayout.remaining, BranchLayout.petals, BranchLayout.core, BranchLayout.leftRaw,
    BranchLayout.leftWork, BranchLayout.rightRaw, BranchLayout.rightWork, BranchLayout.finish,
    ← BitVec.ofNat_add, ← BitVec.ofNat_mul, Nat.mul_comm, Nat.mul_left_comm]
  intro a ha
  have h : a ≠ 0 ∧ a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 ∧ a ≠ 5 ∧ a ≠ 18 ∧ a ≠ 19 ∧
      a ≠ 38 ∧ a ≠ 39 ∧ a ≠ 40 ∧ a ≠ 41 ∧ a ≠ 42 ∧ a ≠ 49 := by rcases ha with ha | ha <;> omega
  simp [h]

theorem trace (source m : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (pointer : s.mem 23 = BitVec.ofNat w.bits source) (count : s.mem 24 = BitVec.ofNat w.bits m) :
    Runs widthConstant (algorithm.program w) 15 s (run widthConstant (algorithm.program w) 15 s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) 15 s
  have ticks := runs_cost trace
  have cost := (allocates source m s pc live pointer count).2.1
  have eq : time = 15 := by omega
  subst time; exact trace

end WordRAM.Conjectures.Sparsification.BranchAllocate

/-! Branch construction with all workspace addresses computed by the machine. -/
namespace WordRAM.Conjectures.Sparsification.InitializedBranch

def algorithm : Algorithm :=
  ⟨SourceChain.code BranchAllocate.algorithm.code BranchMachine.algorithm.code, 1, by decide⟩

set_option maxRecDepth 4096 in
/-- Only the source table, count, selected core masks, and selected size must
be supplied. The program allocates its own buffers and returns both child
pointers/counts plus the first free address in word 49. -/
theorem branches (formula : CNF n) (core : Clause n) (size source : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (sourceBase : 64 ≤ source)
    (fits : BranchLayout.finish source formula.length < 2 ^ w.bits)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (count : s.mem 24 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 23 = BitVec.ofNat w.bits source)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (target : s.mem 22 = BitVec.ofNat w.bits size) :
    ∃ time final leftAddress rightAddress,
      time ≤ (12 * w.bits + 396) * (formula.length + 1) ^ 2 + 15 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem leftAddress (RecordTable.words w (Branch.left formula core size)) ∧
      VectorBuilder.Stored final.mem rightAddress (RecordTable.words w (Branch.right formula core size)) ∧
      final.mem 43 = BitVec.ofNat w.bits leftAddress ∧ final.mem 44 = BitVec.ofNat w.bits (Branch.left formula core size).length ∧
      final.mem 45 = BitVec.ofNat w.bits rightAddress ∧ final.mem 46 = BitVec.ofNat w.bits (Branch.right formula core size).length ∧
      final.mem 49 = BitVec.ofNat w.bits (BranchLayout.finish source formula.length) ∧
      source + 3 * formula.length ≤ leftAddress ∧
      leftAddress + 3 * (Branch.left formula core size).length ≤ rightAddress ∧
      rightAddress + 3 * (Branch.right formula core size).length ≤ BranchLayout.finish source formula.length ∧
      VectorBuilder.Stored final.mem source (RecordTable.words w formula) ∧
      (∀ a, 64 ≤ a → (a < source + 3 * formula.length ∨ BranchLayout.finish source formula.length ≤ a) →
        final.mem a = s.mem a) := by
  let prepared := run widthConstant (BranchAllocate.algorithm.program w) 15 s
  obtain ⟨ph, _, remp, petp, cp, lrp, lwp, rrp, rwp, free, pf⟩ :=
    BranchAllocate.allocates source formula.length s pc live pointer count
  have input' : VectorBuilder.Stored prepared.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact pf a (Or.inr (by omega))
  have partition := BranchLayout.partition w source formula.length sourceBase fits
  have total := BranchTables.partition_length formula core size
  have children := BranchLayout.children w source formula.length
    (Branch.remaining formula core size).length (BranchTables.petals formula core size).length sourceBase total fits
  obtain ⟨time, out, la, ra, bound, trace, halted, leftTable, rightTable, lp, lc, rp, rc, ll, lu, rl, ru, unchanged, frame⟩ :=
    BranchMachine.branches formula core size (SourceChain.resume prepared) source
      (BranchLayout.remaining source formula.length) (BranchLayout.petals source formula.length)
      (BranchLayout.core source formula.length) (BranchLayout.leftRaw source formula.length)
      (BranchLayout.leftWork source formula.length) (BranchLayout.rightRaw source formula.length)
      (BranchLayout.rightWork source formula.length) rfl rfl variablesFit width sizeFits nodup sourceBase
      partition children (by simp [BranchLayout.core]) input'
      ((pf 24 (Or.inl (by decide))).trans count) ((pf 23 (Or.inl (by decide))).trans pointer)
      remp petp ((pf 20 (Or.inl (by decide))).trans qp) ((pf 21 (Or.inl (by decide))).trans qn)
      ((pf 22 (Or.inl (by decide))).trans target) cp lrp lwp rrp rwp
  have full := SourceChain.traces BranchAllocate.algorithm.code BranchMachine.algorithm.code s prepared out 15 time
    live ph (BranchAllocate.trace source formula.length s pc live pointer count) trace
  have polynomial := BranchCost.branch formula core size w.bits
  have order := BranchLayout.ordered source formula.length
  have rightUpper : ra + 3 * (Branch.right formula core size).length ≤ BranchLayout.finish source formula.length := by
    simpa only [total, BranchLayout.finish] using ru
  refine ⟨15 + time, out.relocate BranchAllocate.algorithm.code.length, la, ra, by omega, full, halted,
    leftTable, rightTable, lp, lc, rp, rc, ?_, ?_, by omega, rightUpper, ?_, ?_⟩
  · exact (frame 49 (by decide) (Or.inl (by omega))).trans free
  · change BranchLayout.remaining source formula.length ≤ la
    omega
  · apply MemoryCopy.stored_frame _ _ unchanged
    intro a _ _; rfl
  · intro a ha outside
    have outside' : a < BranchLayout.remaining source formula.length ∨
        BranchLayout.rightWork source formula.length +
          ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length) *
            (3 * ((Branch.remaining formula core size).length + (BranchTables.petals formula core size).length + 1)) ≤ a := by
      simpa only [total, BranchLayout.remaining, BranchLayout.finish] using outside
    exact (frame a (by omega) outside').trans (pf a (Or.inr ha))

end WordRAM.Conjectures.Sparsification.InitializedBranch

/-! Decode the selector's raw core and stage the branch routine's controls. -/
namespace WordRAM.Conjectures.Sparsification.SelectedCore

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 1) (reg 26), .copy (.direct 2) (reg 25), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 20) (reg 3), .copy (.direct 21) (reg 4),
    .copy (.direct 22) (reg 24), .copy (.direct 23) (reg 18),
    .copy (.direct 24) (reg 17), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code MaskBuilder.initialized.code bridge.code), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 1 = s.mem 26 ∧ t.mem 2 = s.mem 25 ∧
      (∀ a, 8 ≤ 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 := by omega
  simp [h]

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 6 s
    t.halted = true ∧ t.ticks = s.ticks + 6 ∧ t.mem 20 = s.mem 3 ∧ t.mem 21 = s.mem 4 ∧
      t.mem 22 = s.mem 24 ∧ t.mem 23 = s.mem 18 ∧ t.mem 24 = s.mem 17 ∧
      (∀ a, a < 20 ∨ 25 ≤ a → t.mem a = s.mem a) := by
  simp [bridge, 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 ≠ 20 ∧ a ≠ 21 ∧ a ≠ 22 ∧ a ≠ 23 ∧ a ≠ 24 := by omega
  simp [h]

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

/-- The selector's descriptor is decoded by `MaskBuilder`, rather than
assuming that raw literals are already available as machine masks. -/
theorem decodes (core : Clause n) (size source count : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (fits : CoreSearchLayout.coreBase core.length + 2 * core.length < 2 ^ w.bits)
    (outcome : FlowerSearch.Outcome (some (size, core)) s.mem)
    (sourcePointer : s.mem 18 = BitVec.ofNat w.bits source)
    (sourceCount : s.mem 17 = BitVec.ofNat w.bits count) :
    ∃ final, Runs widthConstant (algorithm.program w) (10 * core.length + 13) s final ∧ final.halted = true ∧
      final.mem 20 = Masks.encode w core true ∧ final.mem 21 = Masks.encode w core false ∧
      final.mem 22 = BitVec.ofNat w.bits size ∧ final.mem 23 = BitVec.ofNat w.bits source ∧
      final.mem 24 = BitVec.ofNat w.bits count ∧
      (∀ a, (8 ≤ a ∧ a < 20) ∨ 25 ≤ a → final.mem a = s.mem a) := by
  rcases outcome with ⟨_, sizeValue, lengthValue, pointer, encoded⟩
  let prepared := run widthConstant (prepare.program w) 3 s
  obtain ⟨ph, pt, pp, pn, pf⟩ := prepares s pc live
  have input : MaskBuilder.Encoded prepared.mem (CoreSearchLayout.coreBase core.length) (core.map (MaskBuilder.wordLiteral w)) := by
    apply MaskTable.pair_frame _ _ encoded
    intro a ha _
    exact pf a (by dsimp [CoreSearchLayout.coreBase] at ha; omega)
  obtain ⟨decoded, trace, halted, pos, neg, frame⟩ := MaskBuilder.initialized_builds_clause core
    (SourceChain.resume prepared) (CoreSearchLayout.coreBase core.length) rfl rfl
      (by dsimp [CoreSearchLayout.coreBase]; omega) fits variablesFit (pp.trans pointer) (pn.trans lengthValue) input
  let out := run widthConstant (bridge.program w) 6 (SourceChain.resume decoded)
  obtain ⟨oh, ot, op, on, os, oi, oc, ofr⟩ := bridges (SourceChain.resume decoded) rfl rfl
  have tail := SourceChain.traces MaskBuilder.initialized.code bridge.code (SourceChain.resume prepared) decoded out
    (10 * core.length + 4) 6 rfl halted trace (trace_of_ticks _ _ 6 ot)
  have full := SourceChain.traces prepare.code (SourceChain.code MaskBuilder.initialized.code bridge.code) s prepared _
    3 ((10 * core.length + 4) + 6) live ph (trace_of_ticks _ s 3 pt) tail
  have cost : 3 + ((10 * core.length + 4) + 6) = 10 * core.length + 13 := by omega
  refine ⟨(out.relocate MaskBuilder.initialized.code.length).relocate prepare.code.length, ?_, oh,
    op.trans pos, on.trans neg, ?_, ?_, ?_, ?_⟩
  · simpa only [algorithm, Algorithm.program, cost] using full
  · exact os.trans ((frame 24 (by decide)).trans ((pf 24 (by decide)).trans sizeValue))
  · exact oi.trans ((frame 18 (by decide)).trans ((pf 18 (by decide)).trans sourcePointer))
  · exact oc.trans ((frame 17 (by decide)).trans ((pf 17 (by decide)).trans sourceCount))
  · intro a ha
    exact (ofr a (by omega)).trans ((frame a (by omega)).trans (pf a (by omega)))

end WordRAM.Conjectures.Sparsification.SelectedCore

/-! Execute the selector's successful result and return both child descriptors. -/
namespace WordRAM.Conjectures.Sparsification.SelectedBranch

structure Children (formula : CNF n) (core : Clause n) (size source : Nat) (mem : Memory w) : Prop where
  flag : mem 0 = 1#w.bits
  tables : ∃ left right,
    VectorBuilder.Stored mem left (RecordTable.words w (Branch.left formula core size)) ∧
    VectorBuilder.Stored mem right (RecordTable.words w (Branch.right formula core size)) ∧
    mem 43 = BitVec.ofNat w.bits left ∧ mem 44 = BitVec.ofNat w.bits (Branch.left formula core size).length ∧
    mem 45 = BitVec.ofNat w.bits right ∧ mem 46 = BitVec.ofNat w.bits (Branch.right formula core size).length ∧
    source + 3 * formula.length ≤ left ∧ left + 3 * (Branch.left formula core size).length ≤ right ∧
    right + 3 * (Branch.right formula core size).length ≤ BranchLayout.finish source formula.length
  free : mem 49 = BitVec.ofNat w.bits (BranchLayout.finish source formula.length)
  input : VectorBuilder.Stored mem source (RecordTable.words w formula)

def finish : Algorithm := ⟨[.copy (.direct 0) (.immediate 1), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code SelectedCore.algorithm.code
    (SourceChain.code InitializedBranch.algorithm.code finish.code), 1, by decide⟩

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

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
/-- A successful selector result is decoded and branched on entirely inside
the machine, including the final explicit successful-branch flag. -/
theorem builds (formula : CNF n) (core : Clause n) (size source : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (sourceBase : 64 ≤ source)
    (fits : BranchLayout.finish source formula.length < 2 ^ w.bits)
    (coreFits : CoreSearchLayout.coreBase core.length + 2 * core.length < 2 ^ w.bits)
    (selected : FlowerSearch.Outcome (some (size, core)) s.mem)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (count : s.mem 17 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits source) :
    ∃ time final, time ≤ 10 * core.length + (12 * w.bits + 396) * (formula.length + 1) ^ 2 + 30 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      Children formula core size source final.mem ∧
      (∀ a, 64 ≤ a → (a < source + 3 * formula.length ∨ BranchLayout.finish source formula.length ≤ a) →
        final.mem a = s.mem a) := by
  obtain ⟨decoded, dt, dh, dp, dn, ds, di, dc, df⟩ :=
    SelectedCore.decodes core size source formula.length s pc live variablesFit coreFits selected pointer count
  have decodedInput : VectorBuilder.Stored decoded.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact df a (Or.inr (by omega))
  obtain ⟨time, built, la, ra, bound, trace, halted, lt, rt, lp, lc, rp, rc, free, lower, separated, upper, original, frame⟩ :=
    InitializedBranch.branches formula core size source (SourceChain.resume decoded) rfl rfl variablesFit width sizeFits
      nodup sourceBase fits decodedInput dc di dp dn ds
  let out := run widthConstant (finish.program w) 2 (SourceChain.resume built)
  obtain ⟨oh, ot, flag, ofr⟩ := finishes (SourceChain.resume built) rfl rfl
  have tail := SourceChain.traces InitializedBranch.algorithm.code finish.code (SourceChain.resume decoded)
    built out time 2 rfl halted trace (trace_of_ticks _ _ 2 ot)
  have full := SourceChain.traces SelectedCore.algorithm.code (SourceChain.code InitializedBranch.algorithm.code finish.code)
    s decoded _ (10 * core.length + 13) (time + 2) live dh dt tail
  refine ⟨(10 * core.length + 13) + (time + 2),
    (out.relocate InitializedBranch.algorithm.code.length).relocate SelectedCore.algorithm.code.length,
    by omega, full, oh, ?_, ?_⟩
  · refine ⟨flag, ⟨la, ra, ?_, ?_, ?_, ?_, ?_, ?_, lower, separated, upper⟩, ?_, ?_⟩
    · apply MemoryCopy.stored_frame _ _ lt
      intro a ha _; exact ofr a (by omega)
    · apply MemoryCopy.stored_frame _ _ rt
      intro a ha _; exact ofr a (by omega)
    · exact (ofr 43 (by decide)).trans lp
    · exact (ofr 44 (by decide)).trans lc
    · exact (ofr 45 (by decide)).trans rp
    · exact (ofr 46 (by decide)).trans rc
    · exact (ofr 49 (by decide)).trans free
    · apply MemoryCopy.stored_frame _ _ original
      intro a ha _; exact ofr a (by omega)
  · intro a ha outside
    exact (ofr a (by omega)).trans ((frame a ha outside).trans (df a (Or.inr (by omega))))

end WordRAM.Conjectures.Sparsification.SelectedBranch
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