SETH ⇒ OVC sparsification bundle 44: concrete word-RAM formalization
DefinitionSETHOV_Sparsification_44fine-grained-complexityorthogonal-vectorssethsparsificationword-ram
Bundle 44 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 uniform public solver, leaf-solver simulation, runtime polynomials and the final exponent aggregation. 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_43
set_option autoImplicit true
/-! Width setup and execution of a solver with an arbitrary extra-bit parameter.
The caller must supply the serialized translated memory and exact magnitude. -/
namespace WordRAM.Conjectures.ParameterizedSolverCall
open SimulationExecution
def algorithm (solver : Algorithm) : Algorithm :=
⟨SourceChain.code (ExtraWidthSetup.fromMagnitude solver).code (SimulationOutput.code solver), 1, by decide⟩
theorem decides (solver : Algorithm) (input : List Nat) (extra time : Nat) (answer : Prop)
(decision : DecidesIn solver input extra time answer) (s : State wide) (base : Nat)
(pc : s.pc = 0) (live : s.halted = false) (large : 2 ≤ wide.bits) (baseBound : 32 ≤ base)
(width : (solver.width input extra).bits ≤ wide.bits)
(fixed : ∀ i ∈ solver.code, Fits base wide i)
(dynamic : base + 2 ^ (solver.width input extra).bits ≤ 2 ^ wide.bits)
(memory : ∀ address, s.mem (base + address) = (initialState wide input).mem address)
(pointer : s.mem 24 = BitVec.ofNat wide.bits base)
(magnitude : s.mem 25 = BitVec.ofNat wide.bits (inputMagnitude input))
(zero : s.mem 26 = 0#wide.bits) (extraInput : s.mem 16 = BitVec.ofNat wide.bits extra) :
∃ total final, total ≤ 4 * (inputMagnitude input).log2 + 19 * time + 13 ∧
Runs widthConstant ((algorithm solver).program wide) total s final ∧ final.halted = true ∧
(final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ answer) ∧
SimulationBounded.Preserved s.mem final.mem base
(base + SimulationFootprint.span (solver.width input extra) solver.code) ∧
final.mem 31 = WidthSimulation.lift wide
(BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)) := by
obtain ⟨prepared, setupTrace, setupHalt, native, mask, frame⟩ :=
ExtraWidthSetup.computes solver input extra s pc live large width magnitude zero extraInput
have ready : Related (initialState (solver.width input extra) input) (SourceChain.resume prepared) base := by
apply ParameterizedSimulation.ready solver input extra (SourceChain.resume prepared) base width
· intro address
exact (frame (base + address) (by omega) (by omega) (by omega) (by omega) (by omega)).trans (memory address)
· exact (frame 24 (by decide) (by decide) (by decide) (by decide) (by decide)).trans pointer
· exact mask
· exact native
· rfl
· rfl
obtain ⟨callTime, bound, final, trace, halted, boolean, correct, callFrame, callNative⟩ :=
ProtectedSolverOutput.output_decision solver input extra time answer decision (SourceChain.resume prepared)
base width baseBound ready fixed dynamic
have full := SourceChain.traces (ExtraWidthSetup.fromMagnitude solver).code (SimulationOutput.code solver)
s prepared final (4 * (inputMagnitude input).log2 + 11) callTime live setupHalt setupTrace trace
refine ⟨4 * (inputMagnitude input).log2 + 11 + callTime,
final.relocate (ExtraWidthSetup.fromMagnitude solver).code.length, by omega, full, halted, boolean, correct, ?_, callNative⟩
intro a ha hb
exact (callFrame a ha hb).trans (frame a (by omega) (by omega) (by omega) (by omega) (by omega))
end WordRAM.Conjectures.ParameterizedSolverCall
/-! Compute the maximum serialized input word with an actual RAM scan. -/
namespace WordRAM.Conjectures.InputMagnitudeScan
private def reg (i : Nat) : SourceOperand := .memory (.direct i)
/-- 21=input cursor, 22=remaining words, 25=maximum so far. On exit, add one
and clear logarithm accumulator 26. Scratch cell 27 holds the current word. -/
def algorithm : Algorithm :=
⟨[.branch .eq (reg 22) (.immediate 0) 7,
.copy (.direct 27) (.memory (.indirect 21)),
.branch .le (reg 27) (reg 25) 4, .copy (.direct 25) (reg 27),
.binary .add (.direct 21) (reg 21) (.immediate 1),
.binary .sub (.direct 22) (reg 22) (.immediate 1), .jump 0,
.binary .add (.direct 25) (reg 25) (.immediate 1), .copy (.direct 26) (.immediate 0), .halt], 1, by decide⟩
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
theorem iteration (s : State w) (source : Nat) (pc : s.pc = 0) (live : s.halted = false)
(_base : 32 ≤ source) (fits : source < 2 ^ w.bits)
(pointer : s.mem 21 = BitVec.ofNat w.bits source) (nonzero : s.mem 22 ≠ 0#w.bits) :
∃ time next, time ≤ 7 ∧ Runs widthConstant (algorithm.program w) time s next ∧
next.pc = 0 ∧ next.halted = false ∧ next.mem 21 = BitVec.ofNat w.bits (source + 1) ∧
next.mem 22 = s.mem 22 - 1#w.bits ∧
next.mem 25 = (if s.mem source ≤ s.mem 25 then s.mem 25 else s.mem source) ∧
(∀ a, a ≠ 21 → a ≠ 22 → a ≠ 25 → a ≠ 27 → next.mem a = s.mem a) := by
have address : (BitVec.ofNat w.bits source).toNat = source := Nat.mod_eq_of_lt fits
by_cases order : s.mem source ≤ s.mem 25
· change (s.mem source).toNat ≤ (s.mem 25).toNat at order
have result :
let t := run widthConstant (algorithm.program w) 6 s
t.ticks = s.ticks + 6 ∧ t.pc = 0 ∧ t.halted = false ∧
t.mem 21 = BitVec.ofNat w.bits (source + 1) ∧ t.mem 22 = s.mem 22 - 1#w.bits ∧
t.mem 25 = s.mem 25 ∧ (∀ a, a ≠ 21 → a ≠ 22 → a ≠ 25 → a ≠ 27 → t.mem a = s.mem a) := by
simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, pointer, nonzero,
address, order, Nat.add_assoc, ← BitVec.ofNat_add]
intro a h21 h22 _ h27; simp [h21, h22, h27]
exact ⟨6, _, by decide, trace_of_ticks s 6 result.1, result.2.1, result.2.2.1, result.2.2.2.1,
result.2.2.2.2.1, by simpa only [if_pos (show s.mem source ≤ s.mem 25 from order)] using result.2.2.2.2.2.1, result.2.2.2.2.2.2⟩
· change ¬ (s.mem source).toNat ≤ (s.mem 25).toNat at order
have result :
let t := run widthConstant (algorithm.program w) 7 s
t.ticks = s.ticks + 7 ∧ t.pc = 0 ∧ t.halted = false ∧
t.mem 21 = BitVec.ofNat w.bits (source + 1) ∧ t.mem 22 = s.mem 22 - 1#w.bits ∧
t.mem 25 = s.mem source ∧ (∀ a, a ≠ 21 → a ≠ 22 → a ≠ 25 → a ≠ 27 → t.mem a = s.mem a) := by
simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, pointer, nonzero,
address, order, Nat.add_assoc, ← BitVec.ofNat_add]
intro a h21 h22 h25 h27; simp [h21, h22, h25, h27]
exact ⟨7, _, by decide, trace_of_ticks s 7 result.1, result.2.1, result.2.2.1, result.2.2.2.1,
result.2.2.2.2.1, by simpa only [if_neg (show ¬ s.mem source ≤ s.mem 25 from order)] using result.2.2.2.2.2.1, result.2.2.2.2.2.2⟩
theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false) (zero : s.mem 22 = 0#w.bits) :
let t := run widthConstant (algorithm.program w) 4 s
t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 25 = s.mem 25 + 1#w.bits ∧ t.mem 26 = 0#w.bits ∧
(∀ a, a ≠ 25 → a ≠ 26 → t.mem a = s.mem a) := by
simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, zero, Nat.add_assoc]
intro a h25 h26; simp [h25, h26]
/-- Scan all supplied words, with no truncation of data, count, or addresses. -/
theorem computes (xs : List Nat) (seed cap source : Nat) (s : State w)
(pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
(addressFits : source + xs.length < 2 ^ w.bits) (valueFits : cap + 1 < 2 ^ w.bits)
(seedBound : seed ≤ cap) (values : ∀ x ∈ xs, x ≤ cap)
(input : VectorBuilder.Stored s.mem source (xs.map (BitVec.ofNat w.bits)))
(pointer : s.mem 21 = BitVec.ofNat w.bits source)
(count : s.mem 22 = BitVec.ofNat w.bits xs.length)
(maximum : s.mem 25 = BitVec.ofNat w.bits seed) :
∃ time final, time ≤ 7 * xs.length + 4 ∧ Runs widthConstant (algorithm.program w) time s final ∧
final.halted = true ∧ final.mem 25 = BitVec.ofNat w.bits (xs.foldl max seed + 1) ∧ final.mem 26 = 0#w.bits ∧
(∀ a, a ≠ 21 → a ≠ 22 → a ≠ 25 → a ≠ 26 → a ≠ 27 → final.mem a = s.mem a) := by
induction xs generalizing seed source s with
| nil =>
have zero : s.mem 22 = 0#w.bits := count
obtain ⟨halted, ticks, value, cleared, frame⟩ := exits s pc live zero
refine ⟨4, _, by simp, trace_of_ticks s 4 ticks, halted, ?_, cleared, ?_⟩
· simpa only [maximum, List.foldl_nil, ← BitVec.ofNat_add] using value
· intro a _ _ h25 h26 _; exact frame a h25 h26
| cons x xs ih =>
have xBound := values x (by simp)
have countFits : xs.length + 1 < 2 ^ w.bits := by simp only [List.length_cons] at addressFits; omega
have nonzero : s.mem 22 ≠ 0#w.bits := by
intro eq
have vals := congrArg BitVec.toNat eq
simp only [count, List.length_cons, BitVec.toNat_ofNat, Nat.mod_eq_of_lt countFits, Nat.zero_mod] at vals
omega
obtain ⟨time, next, bound, trace, npc, nlive, ptr, cnt, value, frame⟩ :=
iteration s source pc live base (by omega) pointer nonzero
have nextCount : next.mem 22 = BitVec.ofNat w.bits xs.length := by
rw [cnt, count]
simp only [List.length_cons]
rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
simp
have nextMaximum : next.mem 25 = BitVec.ofNat w.bits (max seed x) := by
have cell : s.mem source = BitVec.ofNat w.bits x := input.1
rw [value, cell, maximum]
have test : BitVec.ofNat w.bits x ≤ BitVec.ofNat w.bits seed ↔ x ≤ seed := by
change (BitVec.ofNat w.bits x).toNat ≤ (BitVec.ofNat w.bits seed).toNat ↔ _
simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (show x < 2 ^ w.bits by omega),
Nat.mod_eq_of_lt (show seed < 2 ^ w.bits by omega)]
split
· rename_i h; rw [Nat.max_eq_left (test.mp h)]
· rename_i h
have hn : ¬ x ≤ seed := fun le => h (test.mpr le)
rw [Nat.max_eq_right (by omega)]
have nextInput : VectorBuilder.Stored next.mem (source + 1) (xs.map (BitVec.ofNat w.bits)) := by
apply MemoryCopy.stored_frame _ _ input.2
intro a ha _; exact frame a (by omega) (by omega) (by omega) (by omega)
obtain ⟨restTime, final, restBound, restTrace, halted, result, cleared, preserved⟩ :=
ih (max seed x) (source + 1) next npc nlive (by omega) (by simp only [List.length_cons] at addressFits; omega)
(Nat.max_le.mpr ⟨seedBound, xBound⟩) (fun y hy => values y (by simp [hy])) nextInput ptr nextCount nextMaximum
refine ⟨time + restTime, final, ?_, trace.append restTrace, halted, result, cleared, ?_⟩
· simp only [List.length_cons]; omega
· intro a h21 h22 h25 h26 h27
exact (preserved a h21 h22 h25 h26 h27).trans (frame a h21 h22 h25 h27)
end WordRAM.Conjectures.InputMagnitudeScan
/-! Initialize the maximum with the input length, matching `inputMagnitude`. -/
namespace WordRAM.Conjectures.InputMagnitudeSetup
def prepare : Algorithm :=
⟨[.copy (.direct 25) (.memory (.direct 22)), .halt], 1, by decide⟩
def algorithm : Algorithm :=
⟨SourceChain.code prepare.code InputMagnitudeScan.algorithm.code, 1, by decide⟩
private theorem seed_le (xs : List Nat) (seed : Nat) : seed ≤ xs.foldl max seed := by
induction xs generalizing seed with
| nil => simp
| cons x xs ih => exact Nat.le_trans (Nat.le_max_left seed x) (ih (max seed x))
private theorem member_le (xs : List Nat) (seed x : Nat) (member : x ∈ xs) : x ≤ xs.foldl max seed := by
induction xs generalizing seed with
| nil => simp at member
| cons y ys ih =>
rcases List.mem_cons.mp member with rfl | member
· exact Nat.le_trans (Nat.le_max_right seed x) (seed_le ys (max seed x))
· exact ih (max seed y) member
theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
let t := run widthConstant (prepare.program w) 2 s
t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 25 = s.mem 22 ∧
(∀ a, a ≠ 25 → t.mem a = s.mem a) := by
simp [prepare, 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]
/-- Read the actual serialized words and compute the exact magnitude, including
its input-length seed and final increment. All source memory is preserved. -/
theorem computes (input : List Nat) (source : Nat) (s : State w)
(pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
(addressFits : source + input.length < 2 ^ w.bits) (valueFits : inputMagnitude input < 2 ^ w.bits)
(stored : VectorBuilder.Stored s.mem source (input.map (BitVec.ofNat w.bits)))
(pointer : s.mem 21 = BitVec.ofNat w.bits source)
(count : s.mem 22 = BitVec.ofNat w.bits input.length) :
∃ time final, time ≤ 7 * input.length + 6 ∧ Runs widthConstant (algorithm.program w) time s final ∧
final.halted = true ∧ final.mem 25 = BitVec.ofNat w.bits (inputMagnitude input) ∧ final.mem 26 = 0#w.bits ∧
(∀ a, a ≠ 21 → a ≠ 22 → a ≠ 25 → a ≠ 26 → a ≠ 27 → final.mem a = s.mem a) := by
let prepared := run widthConstant (prepare.program w) 2 s
obtain ⟨ph, pt, maximum, frame⟩ := prepares s pc live
have preparedInput : VectorBuilder.Stored prepared.mem source (input.map (BitVec.ofNat w.bits)) := by
apply MemoryCopy.stored_frame _ _ stored
intro a ha _; exact frame a (by omega)
obtain ⟨time, out, bound, trace, halted, magnitude, zero, preserved⟩ :=
InputMagnitudeScan.computes input input.length (input.foldl max input.length) source (SourceChain.resume prepared)
rfl rfl base addressFits valueFits (seed_le input input.length)
(fun x member => member_le input input.length x member) preparedInput
((frame 21 (by decide)).trans pointer) ((frame 22 (by decide)).trans count) (maximum.trans count)
obtain ⟨ticks, _, setupTrace⟩ := run_has_trace widthConstant (prepare.program w) 2 s
have cost := runs_cost setupTrace
have eq : ticks = 2 := by omega
subst ticks
have full := SourceChain.traces prepare.code InputMagnitudeScan.algorithm.code s prepared out 2 time live ph setupTrace trace
refine ⟨2 + time, out.relocate prepare.code.length, by omega, full, halted, magnitude, zero, ?_⟩
intro a h21 h22 h25 h26 h27
exact (preserved a h21 h22 h25 h26 h27).trans (frame a h25)
end WordRAM.Conjectures.InputMagnitudeSetup
/-! Compute the input magnitude and then run the parameterized solver. -/
namespace WordRAM.Conjectures.ScannedSolverCall
open SimulationExecution
def algorithm (solver : Algorithm) : Algorithm :=
⟨SourceChain.code InputMagnitudeSetup.algorithm.code (ParameterizedSolverCall.algorithm solver).code, 1, by decide⟩
/-- Magnitude scanning, logarithm, width/mask setup, compiled execution, and
answer extraction are all charged. Translated input-memory initialization is an
explicit remaining caller obligation. -/
theorem decides (solver : Algorithm) (input : List Nat) (extra time : Nat) (answer : Prop)
(decision : DecidesIn solver input extra time answer) (s : State wide) (base source : Nat)
(pc : s.pc = 0) (live : s.halted = false) (large : 2 ≤ wide.bits)
(baseBound : 32 ≤ base) (sourceBound : 32 ≤ source)
(sourceFits : source + input.length < 2 ^ wide.bits)
(width : (solver.width input extra).bits ≤ wide.bits)
(fixed : ∀ i ∈ solver.code, Fits base wide i)
(dynamic : base + 2 ^ (solver.width input extra).bits ≤ 2 ^ wide.bits)
(memory : ∀ address, s.mem (base + address) = (initialState wide input).mem address)
(stored : VectorBuilder.Stored s.mem source (input.map (BitVec.ofNat wide.bits)))
(pointer : s.mem 24 = BitVec.ofNat wide.bits base)
(scanPointer : s.mem 21 = BitVec.ofNat wide.bits source)
(count : s.mem 22 = BitVec.ofNat wide.bits input.length)
(extraInput : s.mem 16 = BitVec.ofNat wide.bits extra) :
∃ total final, total ≤ 7 * input.length + 4 * (inputMagnitude input).log2 + 19 * time + 19 ∧
Runs widthConstant ((algorithm solver).program wide) total s final ∧ final.halted = true ∧
(final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ answer) ∧
SimulationBounded.Preserved s.mem final.mem base
(base + SimulationFootprint.span (solver.width input extra) solver.code) ∧
final.mem 31 = WidthSimulation.lift wide
(BitVec.ofNat (solver.width input extra).bits (solver.width input extra).bits : Word (solver.width input extra)) := by
have logBound : (inputMagnitude input).log2 + 1 ≤ (solver.width input extra).bits := by
have h := Nat.le_mul_of_pos_left (extra + (inputMagnitude input).log2 + 1) solver.wordFactor_pos
change _ ≤ solver.wordFactor * (extra + (inputMagnitude input).log2 + 1)
omega
have magnitudeFits : inputMagnitude input < 2 ^ wide.bits :=
Nat.lt_of_lt_of_le Nat.lt_log2_self (Nat.pow_le_pow_right (by decide) (Nat.le_trans logBound width))
obtain ⟨scanTime, scanned, scanBound, scanTrace, scanHalt, magnitude, zero, frame⟩ :=
InputMagnitudeSetup.computes input source s pc live sourceBound sourceFits magnitudeFits stored scanPointer count
have memory' : ∀ address, scanned.mem (base + address) = (initialState wide input).mem address := by
intro address
exact (frame (base + address) (by omega) (by omega) (by omega) (by omega) (by omega)).trans (memory address)
obtain ⟨callTime, final, bound, trace, halted, boolean, correct, callFrame, callNative⟩ :=
ParameterizedSolverCall.decides solver input extra time answer decision (SourceChain.resume scanned) base rfl rfl
large baseBound width fixed dynamic memory'
((frame 24 (by decide) (by decide) (by decide) (by decide) (by decide)).trans pointer)
magnitude zero ((frame 16 (by decide) (by decide) (by decide) (by decide) (by decide)).trans extraInput)
have full := SourceChain.traces InputMagnitudeSetup.algorithm.code (ParameterizedSolverCall.algorithm solver).code
s scanned final scanTime callTime live scanHalt scanTrace trace
refine ⟨scanTime + callTime, final.relocate InputMagnitudeSetup.algorithm.code.length,
by omega, full, halted, boolean, correct, ?_, callNative⟩
intro a ha hb
exact (callFrame a ha hb).trans (frame a (by omega) (by omega) (by omega) (by omega) (by omega))
end WordRAM.Conjectures.ScannedSolverCall
/-! Recover the complete translated initial-state relation from a finite input
buffer, zero output cell, and an untouched zero tail. -/
namespace WordRAM.Conjectures.TranslatedInput
theorem stored_get (xs : List (Word w)) (mem : Memory w) (base i : Nat)
(stored : VectorBuilder.Stored mem base xs) (bound : i < xs.length) : mem (base + i) = xs[i] := by
induction xs generalizing base i with
| nil => simp at bound
| cons x xs ih =>
cases i with
| zero => simpa using stored.1
| succ i =>
simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm, List.getElem_cons_succ] using
(ih (base + 1) i stored.2 (by simpa using bound))
theorem of_stored (input : List Nat) (mem : Memory w) (base : Nat)
(stored : VectorBuilder.Stored mem (base + 1) (input.map (BitVec.ofNat w.bits)))
(outputZero : mem base = 0#w.bits)
(tailZero : ∀ a, base + 1 + input.length ≤ a → mem a = 0#w.bits) :
∀ address, mem (base + address) = (initialState w input).mem address := by
intro address
by_cases zero : address = 0
· subst address; simpa [initialState] using outputZero
· by_cases inside : address - 1 < input.length
· have h := stored_get (input.map (BitVec.ofNat w.bits)) mem (base + 1) (address - 1) stored
(by simpa using inside)
have location : base + 1 + (address - 1) = base + address := by omega
simpa only [location, List.getElem_map, initialState, if_neg zero, List.getElem?_eq_getElem inside,
Option.getD_some] using h
· have h := tailZero (base + address) (by omega)
simpa only [initialState, if_neg zero, List.getElem?_eq_none (by omega : input.length ≤ address - 1),
Option.getD_none] using h
/-- A serializer that writes only its finite input interval turns a fresh zero
region into an entire translated initial memory, including all out-of-input cells. -/
theorem from_fresh (input : List Nat) (before after : Memory w) (base : Nat)
(stored : VectorBuilder.Stored after (base + 1) (input.map (BitVec.ofNat w.bits)))
(fresh : ∀ a, base ≤ a → before a = 0#w.bits)
(frame : ∀ a, base ≤ a → (a < base + 1 ∨ base + 1 + input.length ≤ a) → after a = before a) :
∀ address, after (base + address) = (initialState w input).mem address := by
apply of_stored input after base stored
· exact (frame base (by omega) (Or.inl (by omega))).trans (fresh base (by omega))
· intro a ha
exact (frame a (by omega) (Or.inr ha)).trans (fresh a (by omega))
end WordRAM.Conjectures.TranslatedInput
/-! Serialize a leaf directly into a fresh solver region and establish its
complete initial memory, without clearing an exponential address range. -/
namespace WordRAM.Conjectures.Sparsification.FreshSerialize
theorem prepares (formula : CNF n) (source base budget : Nat) (s : State w)
(pc : s.pc = 0) (live : s.halted = false) (sourceBase : 32 ≤ source)
(before : source + 3 * formula.length ≤ base)
(fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
(space : base + 3 + formula.length * (1 + 4 * n) ≤ budget)
(nodup : ∀ clause ∈ formula, clause.Nodup)
(input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
(variables : s.mem 16 = BitVec.ofNat w.bits n)
(count : s.mem 11 = BitVec.ofNat w.bits formula.length)
(pointer : s.mem 12 = BitVec.ofNat w.bits source)
(output : s.mem 13 = BitVec.ofNat w.bits (base + 1))
(fresh : ∀ a, base ≤ a → s.mem a = 0#w.bits) :
∃ time final, time ≤ formula.length * (22 * n + 29) + 7 ∧
Runs widthConstant (SATSerialize.algorithm.program w) time s final ∧ final.halted = true ∧
VectorBuilder.Stored final.mem (base + 1)
((SATInstance.mk n (Canonical.formula formula)).encode.map (BitVec.ofNat w.bits)) ∧
(∀ address, final.mem (base + address) = (initialState w (SATInstance.mk n (Canonical.formula formula)).encode).mem address) ∧
final.mem 13 = BitVec.ofNat w.bits (base + 1 + (SATInstance.mk n (Canonical.formula formula)).encode.length) ∧
final.mem 16 = BitVec.ofNat w.bits n ∧
(∀ a, 32 ≤ a → (a < base + 1 ∨ base + 1 + (SATInstance.mk n (Canonical.formula formula)).encode.length ≤ a) →
final.mem a = s.mem a) := by
obtain ⟨time, final, bound, trace, halted, stored, cursor, _, vars, frame⟩ :=
SATSerialize.serializes formula source (base + 1) budget s pc live sourceBase (by omega) fits variablesFit
(by omega) nodup input variables count pointer output
refine ⟨time, final, bound, trace, halted, stored, ?_, cursor, vars, frame⟩
apply TranslatedInput.from_fresh _ s.mem final.mem base stored fresh
intro a ha outside
exact frame a (by omega) outside
end WordRAM.Conjectures.Sparsification.FreshSerialize
/-! Recover scan length from a serializer end pointer and persistent base cell. -/
namespace WordRAM.Conjectures.ScanCallSetup
private def reg (i : Nat) : SourceOperand := .memory (.direct i)
def algorithm (baseCell : Nat) : Algorithm :=
⟨[.copy (.direct 24) (reg baseCell), .binary .add (.direct 21) (reg 24) (.immediate 1),
.binary .sub (.direct 22) (reg 13) (reg 21), .halt], 1, by decide⟩
theorem prepares (baseCell base length : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
(_cell : 32 ≤ baseCell) (fits : base + 1 + length < 2 ^ w.bits)
(pointer : s.mem baseCell = BitVec.ofNat w.bits base)
(endpoint : s.mem 13 = BitVec.ofNat w.bits (base + 1 + length)) :
let t := run widthConstant ((algorithm baseCell).program w) 4 s
t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 24 = BitVec.ofNat w.bits base ∧
t.mem 21 = BitVec.ofNat w.bits (base + 1) ∧ t.mem 22 = BitVec.ofNat w.bits length ∧
(∀ a, a ≠ 21 → a ≠ 22 → a ≠ 24 → t.mem a = s.mem a) := by
have sub : BitVec.ofNat w.bits (base + 1 + length) - BitVec.ofNat w.bits (base + 1) = BitVec.ofNat w.bits length := by
rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
simp
simp only [Nat.add_assoc] at sub
simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, endpoint,
← BitVec.ofNat_add, sub, Nat.add_assoc]
intro a h21 h22 h24; simp [h21, h22, h24]
theorem trace (baseCell base length : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
(cell : 32 ≤ baseCell) (fits : base + 1 + length < 2 ^ w.bits)
(pointer : s.mem baseCell = BitVec.ofNat w.bits base)
(endpoint : s.mem 13 = BitVec.ofNat w.bits (base + 1 + length)) :
Runs widthConstant ((algorithm baseCell).program w) 4 s (run widthConstant ((algorithm baseCell).program w) 4 s) := by
have ticks := (prepares baseCell base length s pc live cell fits pointer endpoint).2.1
obtain ⟨time, _, trace⟩ := run_has_trace widthConstant ((algorithm baseCell).program w) 4 s
have cost := runs_cost trace
have eq : time = 4 := by omega
subst time; exact trace
end WordRAM.Conjectures.ScanCallSetup
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).