SETH ⇒ OVC sparsification bundle 38: concrete word-RAM formalization
DefinitionSETHOV_Sparsification_38fine-grained-complexityorthogonal-vectorssethsparsificationword-ram
Bundle 38 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_37
set_option autoImplicit true
/-! Push right then left so the pending list follows the original DFS order. -/
namespace WordRAM.Conjectures.Sparsification.PushChildren
def algorithm (headCell freeCell : Nat) : Algorithm :=
⟨SourceChain.code (TaskPush.algorithm false headCell freeCell).code
(TaskPush.algorithm true headCell freeCell).code, 1, by decide⟩
theorem pushes (tasks : List (StackInvariant.Task n)) (left right : 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 + 6 < 2 ^ w.bits)
(pending : StackInvariant.Stored s.mem base limit head tasks)
(leftBase : base ≤ left.address) (leftEnd : left.address + 3 * left.formula.length ≤ limit)
(rightBase : base ≤ right.address) (rightEnd : right.address + 3 * right.formula.length ≤ limit)
(leftTable : VectorBuilder.Stored s.mem left.address (RecordTable.words w left.formula))
(rightTable : VectorBuilder.Stored s.mem right.address (RecordTable.words w right.formula))
(leftPointer : s.mem 43 = BitVec.ofNat w.bits left.address)
(leftCount : s.mem 44 = BitVec.ofNat w.bits left.formula.length)
(rightPointer : s.mem 45 = BitVec.ofNat w.bits right.address)
(rightCount : s.mem 46 = BitVec.ofNat w.bits right.formula.length)
(headPointer : s.mem headCell = BitVec.ofNat w.bits head)
(freePointer : s.mem freeCell = BitVec.ofNat w.bits destination) :
∃ final, Runs widthConstant ((algorithm headCell freeCell).program w) 40 s final ∧ final.halted = true ∧
final.mem headCell = BitVec.ofNat w.bits (destination + 3) ∧
final.mem freeCell = BitVec.ofNat w.bits (destination + 6) ∧
StackInvariant.Stored final.mem base (destination + 6) (destination + 3) (left :: right :: tasks) ∧
(∀ a, 32 ≤ a → a ≠ headCell → a ≠ freeCell → (a < destination ∨ destination + 6 ≤ a) → final.mem a = s.mem a) := by
obtain ⟨first, firstTrace, firstHalt, firstHead, firstFree, firstStack, firstFrame⟩ :=
TaskPush.pushes false tasks right s headCell freeCell base limit head destination pc live hb fb distinct
headBefore freeBefore fresh (by omega) pending rightBase rightEnd rightTable rightPointer rightCount headPointer freePointer
have retainedLeft : VectorBuilder.Stored first.mem left.address (RecordTable.words w left.formula) := by
apply MemoryCopy.stored_frame _ _ leftTable
intro a ha ha'
rw [RecordTable.words_length] at ha'
exact firstFrame a (by omega) (by omega) (by omega) (Or.inl (by omega))
have lp : first.mem 43 = BitVec.ofNat w.bits left.address :=
(firstFrame 43 (by decide) (by omega) (by omega) (Or.inl (by omega))).trans leftPointer
have lc : first.mem 44 = BitVec.ofNat w.bits left.formula.length :=
(firstFrame 44 (by decide) (by omega) (by omega) (Or.inl (by omega))).trans leftCount
obtain ⟨out, trace, halted, head, free, stored, frame⟩ :=
TaskPush.pushes true (right :: tasks) left (SourceChain.resume first) headCell freeCell base (destination + 3)
destination (destination + 3) rfl rfl hb fb distinct headBefore freeBefore (by omega) (by omega)
firstStack leftBase (by omega) retainedLeft lp lc firstHead firstFree
have full := SourceChain.traces (TaskPush.algorithm false headCell freeCell).code
(TaskPush.algorithm true headCell freeCell).code s first out 20 20 live firstHalt firstTrace trace
refine ⟨out.relocate (TaskPush.algorithm false headCell freeCell).code.length, full, halted, head, ?_, ?_, ?_⟩
· simpa only [Nat.add_assoc, State.relocate] using free
· simpa only [Nat.add_assoc, State.relocate] using stored
· intro a ha hh hf outside
exact (frame a ha hh hf (by omega)).trans (firstFrame a ha hh hf (by omega))
end WordRAM.Conjectures.Sparsification.PushChildren
/-! Dispatch a processed task to the pending stack or the emitted-leaf stack. -/
namespace WordRAM.Conjectures.Sparsification.StoreResult
open StackInvariant
def algorithm (todoCell outputCell freeCell : Nat) : Algorithm :=
⟨SourceIf.code 0 (StackMachine.push outputCell freeCell).code (PushChildren.algorithm todoCell freeCell).code, 1, by decide⟩
def pendingLabels (formula : CNF n) (choice : Option (Nat × Clause n)) (tasks : List (Task n)) : List (CNF n) :=
match choice with
| none => tasks.map Task.formula
| some (size, core) => Branch.left formula core size :: Branch.right formula core size :: tasks.map Task.formula
def outputLabels (formula : CNF n) (choice : Option (Nat × Clause n)) (emitted : List (Task n)) : List (CNF n) :=
match choice with
| none => formula :: emitted.map Task.formula
| some _ => emitted.map Task.formula
set_option maxRecDepth 4096 in
/-- The flag produced by selection controls a genuine machine dispatch. Both
stacks retain their semantic formula lists, and new links use only fresh space. -/
theorem stores (formula : CNF n) (choice : Option (Nat × Clause n)) (tasks emitted : List (Task n))
(s : State w) (todoCell outputCell freeCell base source head outputHead free : Nat)
(pc : s.pc = 0) (live : s.halted = false)
(tb : 64 ≤ todoCell) (ob : 64 ≤ outputCell) (fb : 64 ≤ freeCell)
(toDistinct : todoCell ≠ outputCell) (tfDistinct : todoCell ≠ freeCell) (ofDistinct : outputCell ≠ freeCell)
(todoBefore : todoCell < base) (outputBefore : outputCell < base) (freeBefore : freeCell < base)
(sourceBase : base ≤ source) (fits : free + 6 < 2 ^ w.bits)
(pending : Stored s.mem base free head tasks) (outputs : Stored s.mem base free outputHead emitted)
(todoPointer : s.mem todoCell = BitVec.ofNat w.bits head)
(outputPointer : s.mem outputCell = BitVec.ofNat w.bits outputHead)
(freePointer : s.mem freeCell = BitVec.ofNat w.bits free)
(result : SelectBranch.Outcome formula source choice s.mem)
(endpoint : free = FinishAllocation.endpoint source formula.length choice) :
∃ time final tasks' emitted' head' outputHead' free',
time ≤ 41 ∧ Runs widthConstant ((algorithm todoCell outputCell freeCell).program w) time s final ∧ final.halted = true ∧
Stored final.mem base free' head' tasks' ∧ Stored final.mem base free' outputHead' emitted' ∧
final.mem todoCell = BitVec.ofNat w.bits head' ∧ final.mem outputCell = BitVec.ofNat w.bits outputHead' ∧
final.mem freeCell = BitVec.ofNat w.bits free' ∧
tasks'.map Task.formula = pendingLabels formula choice tasks ∧
emitted'.map Task.formula = outputLabels formula choice emitted ∧
free' = free + (if choice.isSome then 6 else 3) ∧
(∀ a, 32 ≤ a → a ≠ todoCell → a ≠ outputCell → a ≠ freeCell →
(a < free ∨ free + 6 ≤ a) → final.mem a = s.mem a) := by
cases choice with
| none =>
rcases result with ⟨flag, _, count, pointer, table⟩
let task : Task n := ⟨formula, source⟩
obtain ⟨out, trace, halted, hp, fp, stored, frame⟩ := StackInvariant.push emitted task (s.addTicks 1)
outputCell freeCell base free outputHead free pc live ob fb ofDistinct outputBefore freeBefore (by omega)
(by omega) outputs sourceBase (by dsimp [task]; simpa only [FinishAllocation.endpoint] using Nat.le_of_eq endpoint.symm)
table pointer count outputPointer freePointer
have full := SourceIf.zero_trace 0 (StackMachine.push outputCell freeCell).code
(PushChildren.algorithm todoCell freeCell).code s out 17 pc live flag trace
have kept : Stored out.mem base free head tasks := by
apply StackInvariant.frame tasks s.mem out.mem base free head pending
intro a ha hb
exact frame a (by omega) (by omega) (by omega) (Or.inl hb)
have region : base ≤ free := by dsimp [FinishAllocation.endpoint] at endpoint; omega
refine ⟨18, out.relocate (1 + (PushChildren.algorithm todoCell freeCell).code.length), tasks, task :: emitted,
head, free, free + 3, by decide, full, halted,
StackInvariant.weaken tasks out.mem base free (free + 3) head kept (by omega), stored,
?_, hp, fp, rfl, rfl, rfl, ?_⟩
· exact (frame todoCell (by omega) toDistinct tfDistinct (Or.inl (by omega))).trans todoPointer
· intro a ha ht ho hf outside
exact frame a (by omega) ho hf (by omega)
| some pair =>
rcases pair with ⟨size, core⟩
rcases result.tables with ⟨la, ra, lt, rt, lp, lc, rp, rc, lower, separated, upper⟩
let left : Task n := ⟨Branch.left formula core size, la⟩
let right : Task n := ⟨Branch.right formula core size, ra⟩
have endEq : free = BranchLayout.finish source formula.length := endpoint
obtain ⟨out, trace, halted, hp, fp, stored, frame⟩ := PushChildren.pushes tasks left right (s.addTicks 1)
todoCell freeCell base free head free pc live tb fb tfDistinct todoBefore freeBefore (by omega) fits
pending (by dsimp [left]; omega) (by dsimp [left]; omega) (by dsimp [right]; omega)
(by dsimp [right]; omega) lt rt lp lc rp rc todoPointer freePointer
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 (StackMachine.push outputCell freeCell).code
(PushChildren.algorithm todoCell freeCell).code s out 40 pc live nonzero trace
have kept : Stored out.mem base free outputHead emitted := by
apply StackInvariant.frame emitted s.mem out.mem base free outputHead outputs
intro a ha hb
exact frame a (by omega) (by omega) (by omega) (Or.inl hb)
refine ⟨41, out.relocate 1, left :: right :: tasks, emitted, free + 3, outputHead, free + 6,
by decide, full, halted, stored,
StackInvariant.weaken emitted out.mem base free (free + 6) outputHead kept (by omega), hp,
?_, fp, rfl, rfl, rfl, ?_⟩
· exact (frame outputCell (by omega) (Ne.symm toDistinct) ofDistinct (Or.inl (by omega))).trans outputPointer
· intro a ha ht ho hf outside
exact frame a ha ht hf outside
end WordRAM.Conjectures.Sparsification.StoreResult
/-! One concrete DFS iteration: pop, process, and store its children or leaf. -/
namespace WordRAM.Conjectures.Sparsification.TraversalBody
open StackInvariant
def variableCell (k : Nat) : Nat := 64 + 3 * k
def todoCell (k : Nat) : Nat := variableCell k + 1
def outputCell (k : Nat) : Nat := variableCell k + 2
def freeCell (k : Nat) : Nat := variableCell k + 3
def dataBase (k : Nat) : Nat := variableCell k + 4
def loadVariables (k : Nat) : Algorithm :=
⟨[.copy (.direct 16) (.memory (.direct (variableCell k))), .halt], 1, by decide⟩
def algorithm (threshold : Nat → Nat) (k : Nat) : Algorithm :=
⟨SourceChain.code (StackMachine.pop (todoCell k)).code
(SourceChain.code (loadVariables k).code
(SourceChain.code (PendingStep.algorithm threshold k (freeCell k)).code
(StoreResult.algorithm (todoCell k) (outputCell k) (freeCell k)).code)), 1, by decide⟩
theorem loads (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
let t := run widthConstant ((loadVariables k).program w) 2 s
t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 16 = s.mem (variableCell k) ∧
(∀ a, a ≠ 16 → t.mem a = s.mem a) := by
simp [loadVariables, 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]
set_option maxRecDepth 4096 in
/-- Both stacks represent the exact next pending/output formula lists. All
previously allocated table and link memory is preserved during this iteration. -/
theorem step (threshold : Nat → Nat) (k : Nat) (task : StackInvariant.Task n) (tasks emitted : List (StackInvariant.Task n))
(head outputHead limit : Nat) (s : State w)
(pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
(thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits)
(nodup : ∀ clause ∈ task.formula, clause.Nodup)
(fits : BranchLayout.finish limit task.formula.length + 6 < 2 ^ w.bits)
(pending : Stored s.mem (dataBase k) limit head (task :: tasks))
(outputs : Stored s.mem (dataBase k) limit outputHead emitted)
(variables : s.mem (variableCell k) = BitVec.ofNat w.bits n)
(todoPointer : s.mem (todoCell k) = BitVec.ofNat w.bits head)
(outputPointer : s.mem (outputCell k) = BitVec.ofNat w.bits outputHead)
(freePointer : s.mem (freeCell k) = BitVec.ofNat w.bits limit) :
∃ time final tasks' emitted' head' outputHead' limit',
time ≤ SelectBranch.cost n k w.bits task.formula.length + 21 * task.formula.length + 63 ∧
Runs widthConstant ((algorithm threshold k).program w) time s final ∧ final.halted = true ∧
Stored final.mem (dataBase k) limit' head' tasks' ∧ Stored final.mem (dataBase k) limit' outputHead' emitted' ∧
final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
final.mem (todoCell k) = BitVec.ofNat w.bits head' ∧ final.mem (outputCell k) = BitVec.ofNat w.bits outputHead' ∧
final.mem (freeCell k) = BitVec.ofNat w.bits limit' ∧
tasks'.map Task.formula = StoreResult.pendingLabels task.formula (Selection.select task.formula threshold k) tasks ∧
emitted'.map Task.formula = StoreResult.outputLabels task.formula (Selection.select task.formula threshold k) emitted ∧
limit ≤ limit' ∧ limit' ≤ BranchLayout.finish limit task.formula.length + 6 ∧
(∀ a, dataBase k ≤ a → (a < limit ∨ BranchLayout.finish limit task.formula.length + 6 ≤ 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 safe : 32 + 3 * k ≤ variableCell k := by dsimp [variableCell]; omega
have taskBase := pending.2.2.1
have taskEnd := pending.2.2.2.1
have order := BranchLayout.ordered limit task.formula.length
obtain ⟨next, popped, popTrace, popHalt, pp, pn, ph, poppedStack, poppedTable, popFrame⟩ :=
StackInvariant.pop tasks task s (todoCell k) (dataBase k) limit head pc live
(by omega) (by omega) (by omega) pending todoPointer
let loaded := run widthConstant ((loadVariables k).program w) 2 (SourceChain.resume popped)
obtain ⟨lh, lticks, lv, lf⟩ := loads k (SourceChain.resume popped) rfl rfl
have low : ∀ a, 32 ≤ a → a ≠ todoCell k → loaded.mem a = s.mem a := by
intro a ha ht
exact (lf a (by omega)).trans (popFrame a (by omega) (by omega) (by omega) ht)
have loadedInput : VectorBuilder.Stored loaded.mem task.address (RecordTable.words w task.formula) := by
apply MemoryCopy.stored_frame _ _ poppedTable
intro a ha _; exact lf a (by omega)
have loadedVariables : loaded.mem 16 = BitVec.ofNat w.bits n := lv.trans
((popFrame (variableCell k) (by omega) (by omega) (by omega) (by omega)).trans variables)
obtain ⟨processTime, processed, processBound, processTrace, processHalt, result, processFree, _, processFrame⟩ :=
PendingStep.processes task.formula threshold k (freeCell k) task.address limit (SourceChain.resume loaded)
rfl rfl (by omega) (by omega) (by omega) taskEnd (by omega) variablesFit width thresholdFits nodup loadedVariables
((lf 17 (by decide)).trans pn) ((lf 18 (by decide)).trans pp)
((low (freeCell k) (by omega) (by omega)).trans freePointer) loadedInput
let endpoint := FinishAllocation.endpoint limit task.formula.length (Selection.select task.formula threshold k)
have endpointBounds : limit ≤ endpoint ∧ endpoint ≤ BranchLayout.finish limit task.formula.length := by
dsimp [endpoint, FinishAllocation.endpoint]
split
· change limit ≤ BranchLayout.remaining limit task.formula.length ∧
BranchLayout.remaining limit task.formula.length ≤ BranchLayout.finish limit task.formula.length
omega
· omega
have processedLow : ∀ a, 32 + 3 * k ≤ a → 64 ≤ a → a < dataBase k → a ≠ freeCell k →
processed.mem a = loaded.mem a := by
intro a hs ha hb hf
exact processFrame a ha hs hf (Or.inl (by omega))
have oldRegion : ∀ a, dataBase k ≤ a → a < limit → processed.mem a = popped.mem a := by
intro a ha hb
exact (processFrame a (by omega) (by omega) (by omega) (Or.inl hb)).trans (lf a (by omega))
have keptPending : Stored processed.mem (dataBase k) endpoint next tasks :=
StackInvariant.weaken tasks processed.mem (dataBase k) limit endpoint next
(StackInvariant.frame tasks popped.mem processed.mem (dataBase k) limit next poppedStack oldRegion) endpointBounds.1
have keptOutputs : Stored processed.mem (dataBase k) endpoint outputHead emitted := by
apply StackInvariant.weaken emitted processed.mem (dataBase k) limit endpoint outputHead _ endpointBounds.1
apply StackInvariant.frame emitted s.mem processed.mem (dataBase k) limit outputHead outputs
intro a ha hb
exact (oldRegion a ha hb).trans (popFrame a (by omega) (by omega) (by omega) (by omega))
have hp : processed.mem (todoCell k) = BitVec.ofNat w.bits next :=
(processedLow (todoCell k) (by omega) (by omega) (by omega) (by omega)).trans ((lf _ (by omega)).trans ph)
have op : processed.mem (outputCell k) = BitVec.ofNat w.bits outputHead :=
(processedLow (outputCell k) (by omega) (by omega) (by omega) (by omega)).trans
((low _ (by omega) (by omega)).trans outputPointer)
obtain ⟨storeTime, out, tasks', emitted', head', outputHead', limit', storeBound, storeTrace, storeHalt,
storedTasks, storedOutputs, finalHead, finalOutput, finalFree, taskLabels, outputLabels, endEq, storeFrame⟩ :=
StoreResult.stores task.formula (Selection.select task.formula threshold k) tasks emitted (SourceChain.resume processed)
(todoCell k) (outputCell k) (freeCell k) (dataBase k) limit next outputHead endpoint rfl rfl
(by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)
(by omega) (by omega) keptPending keptOutputs hp op processFree result rfl
have finalVariables : out.mem (variableCell k) = BitVec.ofNat w.bits n :=
(storeFrame (variableCell k) (by omega) (by omega) (by omega) (by omega) (Or.inl (by omega))).trans
((processedLow (variableCell k) safe (by omega) (by omega) (by omega)).trans
((low _ (by omega) (by omega)).trans variables))
obtain ⟨setupTime, _, setupTrace⟩ := run_has_trace widthConstant ((loadVariables k).program w) 2 (SourceChain.resume popped)
have setupCost := runs_cost setupTrace
have setupEq : setupTime = 2 := by omega
subst setupTime
have tail := SourceChain.traces (PendingStep.algorithm threshold k (freeCell k)).code
(StoreResult.algorithm (todoCell k) (outputCell k) (freeCell k)).code
(SourceChain.resume loaded) processed out processTime storeTime rfl processHalt processTrace storeTrace
have middle := SourceChain.traces (loadVariables k).code
(SourceChain.code (PendingStep.algorithm threshold k (freeCell k)).code
(StoreResult.algorithm (todoCell k) (outputCell k) (freeCell k)).code)
(SourceChain.resume popped) loaded _ 2 (processTime + storeTime) rfl lh setupTrace tail
have full := SourceChain.traces (StackMachine.pop (todoCell k)).code
(SourceChain.code (loadVariables k).code (SourceChain.code (PendingStep.algorithm threshold k (freeCell k)).code
(StoreResult.algorithm (todoCell k) (outputCell k) (freeCell k)).code))
s popped _ 7 (2 + (processTime + storeTime)) live popHalt popTrace middle
have limitBounds : limit ≤ limit' ∧ limit' ≤ BranchLayout.finish limit task.formula.length + 6 := by
rw [endEq]
split <;> omega
refine ⟨7 + (2 + (processTime + storeTime)),
((out.relocate (PendingStep.algorithm threshold k (freeCell k)).code.length).relocate (loadVariables k).code.length).relocate
(StackMachine.pop (todoCell k)).code.length,
tasks', emitted', head', outputHead', limit', by omega, full, storeHalt, storedTasks, storedOutputs,
finalVariables, finalHead, finalOutput, finalFree, taskLabels, outputLabels, limitBounds.1, limitBounds.2, ?_⟩
intro a ha outside
exact (storeFrame a (by omega) (by omega) (by omega) (by omega) (by omega)).trans
((processFrame a (by omega) (by omega) (by omega) (by omega)).trans
((lf a (by omega)).trans (popFrame a (by omega) (by omega) (by omega) (by omega))))
end WordRAM.Conjectures.Sparsification.TraversalBody
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).