SETH ⇒ OVC sparsification bundle 25: concrete word-RAM formalization
DefinitionSETHOV_Sparsification_25fine-grained-complexityorthogonal-vectorssethsparsificationword-ram
Bundle 25 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_24
set_option autoImplicit true
/-! Counting clauses of a specified size containing a core, on wordRAM. -/
namespace WordRAM.Conjectures.Sparsification.FamilyScan
private def reg (i : Nat) : SourceOperand := .memory (.direct i)
def setupPrefix : List SourceInstruction :=
[.branch .eq (reg 11) (.immediate 0) 23,
.copy (.direct 3) (.memory (.indirect 12)),
.binary .add (.direct 12) (reg 12) (.immediate 1),
.copy (.direct 4) (.memory (.indirect 12)),
.binary .add (.direct 12) (reg 12) (.immediate 1),
.copy (.direct 7) (.memory (.indirect 12)),
.binary .add (.direct 12) (reg 12) (.immediate 1),
.branch .eq (reg 7) (reg 8) 9, .jump 21]
def epilogue : List SourceInstruction :=
[.branch .eq (reg 0) (.immediate 0) 21,
.binary .add (.direct 14) (reg 14) (.immediate 1),
.binary .sub (.direct 11) (reg 11) (.immediate 1), .jump 0, .halt]
/-- Core masks in 1,2; desired clause size in 8; table count/cursor in 11,12.
Each matching record increments 14. The whole table is preserved. -/
def algorithm : Algorithm :=
⟨setupPrefix ++ (SubsetMachine.algorithm.code.map (SourceInstruction.returnTo 10)).map
(SourceInstruction.relocate 9) ++ epilogue, 1, by decide⟩
private theorem program_eq (w : Width) : algorithm.program w =
setupPrefix.map (SourceInstruction.compile w) ++
(((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10)).map (Instruction.relocate 9) ++
epilogue.map (SourceInstruction.compile w)) := rfl
theorem enters (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false)
(nonzero : s.mem 11 ≠ 0#w.bits) (base : 16 ≤ address)
(fits : address + 2 < 2 ^ w.bits) (pointer : s.mem 12 = BitVec.ofNat w.bits address) :
let t := run widthConstant (algorithm.program w) 7 s
t.pc = 7 ∧ t.halted = false ∧ t.ticks = s.ticks + 7 ∧
t.mem 3 = s.mem address ∧ t.mem 4 = s.mem (address + 1) ∧ t.mem 7 = s.mem (address + 2) ∧
t.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
(∀ a, a ≠ 3 → a ≠ 4 → a ≠ 7 → a ≠ 12 → 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 low1 : ∀ i, i ≤ 15 → address + 1 ≠ i := by omega
have low2 : ∀ i, i ≤ 15 → address + 2 ≠ i := by omega
rw [program_eq]
simp [setupPrefix, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, nonzero,
pointer, d0, d1, d2, low1, low2, Nat.add_assoc, -BitVec.toNat_add,
List.getElem?_cons_zero, List.getElem?_cons_succ]
constructor
· rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
· intro a h3 h4 h7 h12; simp [h3, h4, h7, h12]
theorem selects (s : State w) (pc : s.pc = 7) (live : s.halted = false) (same : s.mem 7 = s.mem 8) :
let t := run widthConstant (algorithm.program w) 1 s
t.pc = 9 ∧ t.halted = false ∧ t.ticks = s.ticks + 1 ∧ t.mem = s.mem := by
have f7 : (algorithm.program w)[7]? = some (.branch .eq (.memory (.direct 7)) (.memory (.direct 8)) 9) := rfl
simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, same, f7]
theorem skips (s : State w) (pc : s.pc = 7) (live : s.halted = false) (different : s.mem 7 ≠ s.mem 8) :
let t := run widthConstant (algorithm.program w) 4 s
t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 4 ∧
t.mem 11 = s.mem 11 - 1#w.bits ∧ (∀ a, a ≠ 11 → t.mem a = s.mem a) := by
have f7 : (algorithm.program w)[7]? = some (.branch .eq (.memory (.direct 7)) (.memory (.direct 8)) 9) := rfl
have f8 : (algorithm.program w)[8]? = some (.jump 21) := rfl
have f21 : (algorithm.program w)[21]? = some (.binary .sub (.direct 11) (.memory (.direct 11)) (.immediate 1)) := rfl
have f22 : (algorithm.program w)[22]? = some (.jump 0) := rfl
simp [run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test,
pc, live, different, f7, f8, f21, f22, Nat.add_assoc]
intro a h; simp [h]
theorem leaves (s : State w) (pc : s.pc = 19) (live : s.halted = false) :
let fuel := if s.mem 0 = 0#w.bits then 3 else 4
let t := run widthConstant (algorithm.program w) fuel s
t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + fuel ∧
t.mem 11 = s.mem 11 - 1#w.bits ∧
t.mem 14 = s.mem 14 + (if s.mem 0 = 0#w.bits then 0#w.bits else 1#w.bits) ∧
(∀ a, a ≠ 11 → a ≠ 14 → t.mem a = s.mem a) := by
have f19 : (algorithm.program w)[19]? = some (.branch .eq (.memory (.direct 0)) (.immediate 0) 21) := rfl
have f20 : (algorithm.program w)[20]? = some (.binary .add (.direct 14) (.memory (.direct 14)) (.immediate 1)) := rfl
have f21 : (algorithm.program w)[21]? = some (.binary .sub (.direct 11) (.memory (.direct 11)) (.immediate 1)) := rfl
have f22 : (algorithm.program w)[22]? = some (.jump 0) := rfl
by_cases zero : s.mem 0 = 0#w.bits
all_goals simp [run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test,
pc, live, zero, f19, f20, f21, f22, Nat.add_assoc]
· intro a h11 _; simp [h11]
· intro a h11 h14; simp [h11, h14]
theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false) (empty : s.mem 11 = 0#w.bits) :
let t := run widthConstant (algorithm.program w) 2 s
t.halted = true ∧ t.mem = s.mem ∧ t.ticks = s.ticks + 2 := by
have f0 : (algorithm.program w)[0]? = some (.branch .eq (.memory (.direct 11)) (.immediate 0) 23) := rfl
have f23 : (algorithm.program w)[23]? = some .halt := rfl
simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, empty, f0, f23, Nat.add_assoc]
private theorem trace_of_ticks (s : State w) (fuel : Nat)
(cost : (run widthConstant (algorithm.program w) fuel s).ticks = s.ticks + fuel) :
Runs widthConstant (algorithm.program w) fuel s (run widthConstant (algorithm.program w) fuel s) := by
obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) fuel s
have ticks := runs_cost trace
have eq : time = fuel := by omega
subst time
exact trace
/-- The size-matching path loads a record and executes the linked subset test. -/
theorem compares (core clause : Clause n) (s : State w) (address : Nat)
(pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 11 ≠ 0#w.bits)
(base : 16 ≤ address) (fits : address + 2 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
(qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
(pointer : s.mem 12 = BitVec.ofNat w.bits address)
(positive : s.mem address = Masks.encode w clause true)
(negative : s.mem (address + 1) = Masks.encode w clause false)
(sizeMatch : s.mem (address + 2) = s.mem 8) :
∃ time final, time ≤ 14 ∧ Runs widthConstant (algorithm.program w) time s final ∧
final.pc = 19 ∧ final.halted = false ∧
final.mem 0 = (if core ⊆ clause then 1#w.bits else 0#w.bits) ∧
final.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
(∀ a, a ≠ 0 → a ≠ 3 → a ≠ 4 → a ≠ 5 → a ≠ 6 → a ≠ 7 → a ≠ 12 → final.mem a = s.mem a) := by
let head := run widthConstant (algorithm.program w) 7 s
obtain ⟨hpc, hlive, hticks, hp, hn, hsize, hnext, hf⟩ := enters s address pc live nonzero base fits pointer
have same : head.mem 7 = head.mem 8 :=
(hsize.trans sizeMatch).trans (hf 8 (by decide) (by decide) (by decide) (by decide)).symm
let selected := run widthConstant (algorithm.program w) 1 head
obtain ⟨spc, slive, sticks, smem⟩ := selects head hpc hlive same
let entry : State w := { selected with pc := 0 }
have entryLive : entry.halted = false := slive
have ef : ∀ a, entry.mem a = head.mem a := fun a => congrFun smem a
obtain ⟨time, bound, trace, halted, result⟩ :=
SubsetMachine.decides_subset core clause variablesFit entry rfl entryLive
((ef 1).trans ((hf 1 (by decide) (by decide) (by decide) (by decide)).trans qp))
((ef 2).trans ((hf 2 (by decide) (by decide) (by decide) (by decide)).trans qn))
((ef 3).trans (hp.trans positive)) ((ef 4).trans (hn.trans negative))
have embedded : EmbedsAt ((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10))
(algorithm.program w) 9 := by
rw [program_eq]
exact embeds_append (setupPrefix.map (SourceInstruction.compile w))
((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10))
(epilogue.map (SourceInstruction.compile w))
let returned := ((SubsetMachine.result entry).returnTo 10).relocate 9
have linked : Runs widthConstant (algorithm.program w) time selected returned := by
have h := (trace.returnTo 10).relocate embedded
have he : (entry.returnTo 10).relocate 9 = selected := by
simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
change { selected with pc := 9 } = selected
have spc' : selected.pc = 9 := spc
rw [← spc']
simpa only [he] using h
have rf : ∀ a, a ≠ 0 → a ≠ 5 → a ≠ 6 → returned.mem a = head.mem a := by
intro a h0 h5 h6
have h := (SubsetMachine.frame entry rfl entryLive a h0 h5 h6).trans (ef a)
simpa [returned, State.returnTo, State.relocate, halted] using h
refine ⟨7 + 1 + time, returned, by omega,
((trace_of_ticks s 7 hticks).append (trace_of_ticks head 1 sticks)).append linked, ?_, ?_, ?_, ?_, ?_⟩
· simp [returned, State.returnTo, State.relocate, halted]
· simp [returned, State.returnTo, State.relocate, halted]
· simpa [returned, State.returnTo, State.relocate, halted] using result
· exact (rf 12 (by decide) (by decide) (by decide)).trans hnext
· intro a h0 h3 h4 h5 h6 h7 h12
exact (rf a h0 h5 h6).trans (hf a h3 h4 h7 h12)
/-- One complete family-counting iteration on a clause with distinct literals. -/
theorem iteration (core clause : Clause n) (size : Nat) (s : State w) (address : Nat)
(pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 11 ≠ 0#w.bits)
(base : 16 ≤ address) (fits : address + 2 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
(width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : clause.Nodup)
(qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
(target : s.mem 8 = BitVec.ofNat w.bits size)
(pointer : s.mem 12 = BitVec.ofNat w.bits address)
(positive : s.mem address = Masks.encode w clause true)
(negative : s.mem (address + 1) = Masks.encode w clause false)
(lengthWord : s.mem (address + 2) = BitVec.ofNat w.bits (Normalize.clean clause).length) :
∃ time final, time ≤ 18 ∧ Runs widthConstant (algorithm.program w) time s final ∧
final.pc = 0 ∧ final.halted = false ∧
final.mem 1 = Masks.encode w core true ∧ final.mem 2 = Masks.encode w core false ∧
final.mem 8 = BitVec.ofNat w.bits size ∧ final.mem 11 = s.mem 11 - 1#w.bits ∧
final.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
final.mem 14 = s.mem 14 + (if clause.length = size ∧ core ⊆ clause then 1#w.bits else 0#w.bits) ∧
(∀ a, 16 ≤ a → final.mem a = s.mem a) := by
have clean : Normalize.clean clause = clause := Normalize.clean_eq clause nodup
have clauseFits : clause.length < 2 ^ w.bits := by
simpa only [clean] using SizeMachine.size_fits clause variablesFit width
by_cases sizeEq : clause.length = size
· have sizeMatch : s.mem (address + 2) = s.mem 8 := by rw [lengthWord, clean, sizeEq, target]
obtain ⟨time, middle, bound, trace, mpc, mlive, result, next, frame⟩ :=
compares core clause s address pc live nonzero base fits variablesFit qp qn pointer positive negative sizeMatch
obtain ⟨fpc, flive, ticks, remaining, counted, ff⟩ := leaves middle mpc mlive
let fuel := if middle.mem 0 = 0#w.bits then 3 else 4
have fuelBound : fuel ≤ 4 := by unfold fuel; split <;> omega
refine ⟨time + fuel, run widthConstant (algorithm.program w) fuel middle, by omega,
trace.append (trace_of_ticks middle fuel ticks), fpc, flive, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· exact (ff 1 (by decide) (by decide)).trans
((frame 1 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qp)
· exact (ff 2 (by decide) (by decide)).trans
((frame 2 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qn)
· exact (ff 8 (by decide) (by decide)).trans
((frame 8 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans target)
· rw [remaining, frame 11 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)]
· exact (ff 12 (by decide) (by decide)).trans next
· rw [counted, frame 14 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide), result]
have oneNonzero : (1#w.bits) ≠ 0#w.bits := by
intro eq
have values := congrArg BitVec.toNat eq
have oneFits : 1 < 2 ^ w.bits := by omega
simp [Nat.mod_eq_of_lt oneFits] at values
by_cases subset : core ⊆ clause <;> simp [sizeEq, subset, oneNonzero]
· intro a ha
exact (ff a (by omega) (by omega)).trans
(frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega))
· let head := run widthConstant (algorithm.program w) 7 s
obtain ⟨hpc, hlive, hticks, hp, hn, hsize, hnext, hf⟩ := enters s address pc live nonzero base fits pointer
have different : head.mem 7 ≠ head.mem 8 := by
rw [hsize, hf 8 (by decide) (by decide) (by decide) (by decide), lengthWord, clean, target]
intro eq
have values := congrArg BitVec.toNat eq
simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt clauseFits, Nat.mod_eq_of_lt sizeFits] at values
exact sizeEq values
obtain ⟨fpc, flive, ticks, remaining, ff⟩ := skips head hpc hlive different
refine ⟨11, run widthConstant (algorithm.program w) 4 head, by decide,
(trace_of_ticks s 7 hticks).append (trace_of_ticks head 4 ticks), fpc, flive, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
· exact (ff 1 (by decide)).trans ((hf 1 (by decide) (by decide) (by decide) (by decide)).trans qp)
· exact (ff 2 (by decide)).trans ((hf 2 (by decide) (by decide) (by decide) (by decide)).trans qn)
· exact (ff 8 (by decide)).trans ((hf 8 (by decide) (by decide) (by decide) (by decide)).trans target)
· rw [remaining, hf 11 (by decide) (by decide) (by decide) (by decide)]
· exact (ff 12 (by decide)).trans hnext
· simpa only [sizeEq, false_and, ↓reduceIte, BitVec.add_zero] using
(ff 14 (by decide)).trans (hf 14 (by decide) (by decide) (by decide) (by decide))
· intro a ha
exact (ff a (by omega)).trans (hf a (by omega) (by omega) (by omega) (by omega))
/-- Count the complete family, accumulating into the existing word in 14. -/
theorem scans (core : Clause n) (clauses : CNF n) (size : Nat) (s : State w) (address : Nat)
(pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
(fits : address + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
(width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : ∀ clause ∈ clauses, clause.Nodup)
(qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
(target : s.mem 8 = BitVec.ofNat w.bits size)
(pointer : s.mem 12 = BitVec.ofNat w.bits address)
(remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
(input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
∃ time final, time ≤ 18 * clauses.length + 2 ∧ Runs widthConstant (algorithm.program w) time s final ∧
final.halted = true ∧ final.mem 14 = s.mem 14 + BitVec.ofNat w.bits (Flowers.family clauses core size).length ∧
(∀ a, 16 ≤ a → final.mem a = s.mem a) := by
induction clauses generalizing s address with
| nil =>
have empty : s.mem 11 = 0#w.bits := by simpa using remaining
obtain ⟨halted, mem, ticks⟩ := exits s pc live empty
refine ⟨2, run widthConstant (algorithm.program w) 2 s, by simp,
trace_of_ticks s 2 ticks, halted, ?_, ?_⟩
· simpa [Flowers.family] using congrFun mem 14
· intro a _; exact congrFun mem a
| cons clause rest ih =>
have countFits : rest.length + 1 < 2 ^ w.bits := by simp only [List.length_cons] at fits; omega
have nonzero : s.mem 11 ≠ 0#w.bits := by
intro h
have hn := congrArg BitVec.toNat h
simp [remaining, Nat.mod_eq_of_lt countFits] at hn
obtain ⟨stepTime, next, stepBound, stepTrace, npc, nlive, nqp, nqn, ntarget, ncount, np, total, frame⟩ :=
iteration core clause size s address pc live nonzero base
(by simp only [List.length_cons] at fits; omega) variablesFit width sizeFits (nodup clause (by simp))
qp qn target pointer input.1 input.2.1 input.2.2.1
have nc : next.mem 11 = BitVec.ofNat w.bits rest.length := by
rw [ncount, remaining]
change BitVec.ofNat w.bits (rest.length + 1) - BitVec.ofNat w.bits 1 = _
rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]; simp
have nextInput : VectorBuilder.Stored next.mem (address + 3) (RecordTable.words w rest) := by
apply MemoryCopy.stored_frame _ _ input.2.2.2
intro a lo _; exact frame a (by omega)
obtain ⟨time, final, bound, trace, halted, result, preserved⟩ :=
ih next (address + 3) npc nlive (by omega)
(by simp only [List.length_cons] at fits; omega)
(fun c h => nodup c (by simp [h])) nqp nqn ntarget np nc nextInput
refine ⟨stepTime + time, final, by simp only [List.length_cons]; omega,
stepTrace.append trace, halted, ?_, ?_⟩
· rw [result, total]
by_cases member : clause.length = size ∧ core ⊆ clause
· simp only [if_pos member, Flowers.family, List.filter_cons, decide_eq_true member, ↓reduceIte,
List.length_cons, BitVec.add_assoc]
rw [← BitVec.ofNat_add]
congr 2; omega
· simp [member, Flowers.family]
· intro a ha; exact (preserved a ha).trans (frame a ha)
def setup : Algorithm := ⟨[.copy (.direct 14) (.immediate 0), .halt], 1, by decide⟩
def initialized : Algorithm := ⟨SourceChain.code setup.code algorithm.code, 1, by decide⟩
theorem initializes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
let t := run widthConstant (setup.program w) 2 s
t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 14 = 0#w.bits ∧
(∀ a, a ≠ 14 → t.mem a = s.mem a) := by
simp [setup, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step, execute,
Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
intro a h; simp [h]
/-- The initialized scan returns the exact natural family size, not a wrapped
word count, and includes initialization and the terminal halt in its bound. -/
theorem counts_family (core : Clause n) (clauses : CNF n) (size : Nat) (s : State w) (address : Nat)
(pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
(fits : address + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
(width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : ∀ clause ∈ clauses, clause.Nodup)
(qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
(target : s.mem 8 = BitVec.ofNat w.bits size)
(pointer : s.mem 12 = BitVec.ofNat w.bits address)
(remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
(input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
∃ time final, time ≤ 18 * clauses.length + 4 ∧ Runs widthConstant (initialized.program w) time s final ∧
final.halted = true ∧ (final.mem 14).toNat = (Flowers.family clauses core size).length ∧
(∀ a, 16 ≤ a → final.mem a = s.mem a) := by
let middle := run widthConstant (setup.program w) 2 s
obtain ⟨halted, ticks, zero, frame⟩ := initializes s pc live
have nextInput : VectorBuilder.Stored middle.mem address (RecordTable.words w clauses) := by
apply MemoryCopy.stored_frame _ _ input
intro a lo _; exact frame a (by omega)
obtain ⟨time, out, bound, trace, outHalt, result, preserved⟩ :=
scans core clauses size (SourceChain.resume middle) address rfl rfl base fits variablesFit width sizeFits nodup
((frame 1 (by decide)).trans qp) ((frame 2 (by decide)).trans qn) ((frame 8 (by decide)).trans target)
((frame 12 (by decide)).trans pointer) ((frame 11 (by decide)).trans remaining) nextInput
have setupTrace : Runs widthConstant (setup.program w) 2 s middle := by
obtain ⟨t, _, h⟩ := run_has_trace widthConstant (setup.program w) 2 s
have cost := runs_cost h
have eq : t = 2 := by omega
subst t; exact h
have full := SourceChain.traces setup.code algorithm.code s middle out 2 time live halted setupTrace trace
refine ⟨2 + time, out.relocate setup.code.length, by omega, full, outHalt, ?_, ?_⟩
· change (out.mem 14).toNat = _
rw [result]
change (middle.mem 14 + _).toNat = _
rw [zero, BitVec.zero_add, BitVec.toNat_ofNat]
apply Nat.mod_eq_of_lt
have bound : (Flowers.family clauses core size).length ≤ clauses.length := List.length_filter_le ..
omega
· intro a ha; exact (preserved a ha).trans (frame a (by omega))
end WordRAM.Conjectures.Sparsification.FamilyScan
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).