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

import Definitions.Def_WordRAMEquivalence_Foundation1
import Definitions.Def_WordRAM_Conjectures
import Definitions.Def_WordRAM_SETHOV_Reduction
import Definitions.Def_SETHOV_Sparsification_45

set_option autoImplicit true

/-! Consume the entire leaf stack, with explicit solver eligibility and uniform
per-leaf resource budgets, and return the disjunction of leaf answers. -/
namespace WordRAM.Conjectures.Sparsification.LeafLoop
open TraversalBody SimulationExecution

def AnySAT (tasks : List (StackInvariant.Task n)) : Prop :=
  ∃ task ∈ tasks, (SATInstance.mk n task.formula).Satisfiable

structure Eligible (solver : Algorithm) (w : Width) (cost reserve : Nat) (formula : CNF n) : Prop where
  nodup : ∀ clause ∈ formula, clause.Nodup
  width : (solver.width (LeafCall.satInput formula).encode n).bits ≤ w.bits
  span : SimulationFootprint.span (solver.width (LeafCall.satInput formula).encode n) solver.code ≤ reserve
  space : 3 + formula.length * (1 + 4 * n) ≤ reserve
  decision : ∃ time, DecidesIn solver (LeafCall.satInput formula).encode n time (LeafCall.satInput formula).Satisfiable ∧
    formula.length * (22 * n + 29) + 7 * (LeafCall.satInput formula).encode.length +
      4 * (inputMagnitude (LeafCall.satInput formula).encode).log2 + 19 * time + 50 ≤ cost

def Invariant (solver : Algorithm) (k cost reserve budget n fuel : Nat) (target : Prop) (mem : Memory w) : Prop :=
  ∃ (tasks : List (StackInvariant.Task n)) (head base : Nat),
    tasks.length = fuel ∧ StackInvariant.Stored mem (dataBase k) base head tasks ∧
    (∀ task ∈ tasks, Eligible solver w cost reserve task.formula) ∧
    mem (variableCell k) = BitVec.ofNat w.bits n ∧ mem (outputCell k) = BitVec.ofNat w.bits head ∧
    mem (freeCell k) = BitVec.ofNat w.bits base ∧
    (mem (todoCell k) = 0 ∨ mem (todoCell k) = 1) ∧
    ((mem (todoCell k) = 1 ∨ AnySAT tasks) ↔ target) ∧
    (∀ a, base ≤ a → mem a = 0#w.bits) ∧ base + fuel * reserve ≤ budget

theorem guard (h : Invariant solver k cost reserve budget n fuel target (mem : Memory w))
    (fits : budget < 2 ^ w.bits) : mem (outputCell k) = 0#w.bits ↔ fuel = 0 := by
  obtain ⟨tasks, head, base, len, stored, _, _, pointer, _, _, _, _, space⟩ := h
  rw [pointer, TraversalFacts.head_zero_iff tasks mem (dataBase k) base head
    (by simp [dataBase, variableCell]) (by omega) stored, ← len]
  exact List.length_eq_zero_iff.symm

set_option maxRecDepth 4096 in
theorem iteration (solver : Algorithm) (k cost reserve budget : Nat) (target : Prop)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 2 ≤ w.bits)
    (fuel : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (h : Invariant solver k cost reserve budget n (fuel + 1) target s.mem) :
    ∃ time final, time ≤ cost ∧ Runs widthConstant ((LeafBody.algorithm solver k).program w) time s final ∧
      final.halted = true ∧ Invariant solver k cost reserve budget n fuel target final.mem := by
  obtain ⟨tasks, head, base, len, pending, eligible, variables, pointer, free, answer, meaning, fresh, space⟩ := h
  cases tasks with
  | nil => simp at len
  | cons task tasks =>
    have current := eligible task (by simp)
    obtain ⟨solverTime, decision, costBound⟩ := current.decision
    have room : base + reserve ≤ budget := by simp only [Nat.add_mul, Nat.one_mul] at space; omega
    have span := current.span
    have serialization := current.space
    have endpointFits : LeafBody.endpoint solver task.formula base < 2 ^ w.bits := by
      unfold LeafBody.endpoint; omega
    have fixed : ∀ i ∈ solver.code, Fits base w i := by
      apply SimulationBounds.program_fits
      unfold SimulationFootprint.span at span
      omega
    have dynamic : base + 2 ^ (solver.width (LeafCall.satInput task.formula).encode n).bits ≤ 2 ^ w.bits := by
      unfold SimulationFootprint.span at span
      omega
    obtain ⟨time, final, next, bound, trace, halted, pending', variables', pointer', free', answer', meaning', fresh', _⟩ :=
      LeafBody.step solver k task tasks head base budget solverTime s decision pc live fits variablesFit large
        (by omega) current.width fixed dynamic endpointFits current.nodup pending variables pointer free answer fresh
    have remaining : tasks.length = fuel := by simp only [List.length_cons] at len; omega
    refine ⟨time, final, Nat.le_trans bound costBound, trace, halted, tasks, next, LeafBody.endpoint solver task.formula base,
      remaining, pending', ?_, variables', pointer', free', answer', ?_, fresh', ?_⟩
    · intro t member; exact eligible t (by simp [member])
    · rw [meaning']
      have alternatives : AnySAT (task :: tasks) ↔ (SATInstance.mk n task.formula).Satisfiable ∨ AnySAT tasks := by
        simp [AnySAT]
      rw [alternatives] at meaning
      simpa only [or_assoc] using meaning
    · unfold LeafBody.endpoint
      simp only [Nat.add_mul, Nat.one_mul] at space
      omega

def loop (solver : Algorithm) (k : Nat) : Algorithm :=
  SourceWhile.algorithm (outputCell k) (LeafBody.algorithm solver k).code

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

def algorithm (solver : Algorithm) (k : Nat) : Algorithm :=
  ⟨SourceChain.code (loop solver k).code (finish k).code, 1, by decide⟩

theorem finishes (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((finish k).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 0 = s.mem (todoCell k) ∧
      (∀ 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 h; simp [h]

/-- Decide the disjunction of all initial leaves using actual calls to the
supplied solver. The resource bounds and solver decisions are explicit hypotheses
on those leaves; neither the calls nor their memory preparation are abstract. -/
theorem decides (solver : Algorithm) (k cost reserve budget : Nat)
    (tasks : List (StackInvariant.Task n)) (head base : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (large : 2 ≤ w.bits)
    (pending : StackInvariant.Stored s.mem (dataBase k) base head tasks)
    (eligible : ∀ task ∈ tasks, Eligible solver w cost reserve task.formula)
    (variables : s.mem (variableCell k) = BitVec.ofNat w.bits n)
    (pointer : s.mem (outputCell k) = BitVec.ofNat w.bits head)
    (free : s.mem (freeCell k) = BitVec.ofNat w.bits base)
    (answer : s.mem (todoCell k) = 0#w.bits)
    (fresh : ∀ a, base ≤ a → s.mem a = 0#w.bits)
    (space : base + tasks.length * reserve ≤ budget) :
    ∃ time final, time ≤ tasks.length * (cost + 2) + 4 ∧
      Runs widthConstant ((algorithm solver k).program w) time s final ∧ final.halted = true ∧
      (final.mem 0 = 0 ∨ final.mem 0 = 1) ∧ (final.mem 0 = 1 ↔ AnySAT tasks) ∧
      final.mem (outputCell k) = 0#w.bits := by
  have oneNeZero : (1 : Word w) ≠ 0 := by
    have positive : w.bits ≠ 0 := Nat.ne_of_gt w.positive
    simp [positive]
  have initial : Invariant solver k cost reserve budget n tasks.length (AnySAT tasks) s.mem := by
    refine ⟨tasks, head, base, rfl, pending, eligible, variables, pointer, free, Or.inl answer, ?_, fresh, space⟩
    rw [answer]
    exact or_iff_right (Ne.symm oneNeZero)
  obtain ⟨time, out, bound, trace, halted, invariant, zero⟩ :=
    SourceWhile.loops (outputCell k) (LeafBody.algorithm solver k).code cost
      (Invariant solver k cost reserve budget n · (AnySAT tasks))
      (fun _ _ h => guard h fits)
      (iteration solver k cost reserve budget (AnySAT tasks) fits variablesFit large)
      tasks.length s pc live initial
  obtain ⟨remaining, head', base', length, _, _, _, _, _, boolean, meaning, _, _⟩ := invariant
  have empty : remaining = [] := List.length_eq_zero_iff.mp length
  have correct : out.mem (todoCell k) = 1 ↔ AnySAT tasks := by simpa [empty, AnySAT] using meaning
  let final := run widthConstant ((finish k).program w) 2 (SourceChain.resume out)
  obtain ⟨fh, ft, value, frame⟩ := finishes k (SourceChain.resume out) rfl rfl
  obtain ⟨ticks, _, finishTrace⟩ := run_has_trace widthConstant ((finish k).program w) 2 (SourceChain.resume out)
  have tickCost := runs_cost finishTrace
  have eq : ticks = 2 := by omega
  subst ticks
  have full := SourceChain.traces (loop solver k).code (finish k).code s out final time 2 live halted trace finishTrace
  refine ⟨time + 2, final.relocate (loop solver k).code.length, by omega, full, fh, ?_, ?_, ?_⟩
  · change final.mem 0 = 0 ∨ final.mem 0 = 1
    change final.mem 0 = out.mem (todoCell k) at value
    rw [value]
    exact boolean
  · change final.mem 0 = 1 ↔ AnySAT tasks
    change final.mem 0 = out.mem (todoCell k) at value
    rw [value]
    exact correct
  · exact (frame (outputCell k) (by dsimp [outputCell, variableCell]; omega)).trans zero

end WordRAM.Conjectures.Sparsification.LeafLoop

/-! DFS preserves every address beyond its reserved workspace. -/
namespace WordRAM.Conjectures.Sparsification.TraversalFresh
open TraversalBody TraversalFacts TraversalBounds Traversal

/-- Every iteration is an actual wordRAM execution. The loop stops after exactly
all remaining recursive work is consumed, with the leaf sequence represented in
reverse by its output stack. -/
theorem traverses (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (target : List (CNF n)) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits) (fits : budget < 2 ^ w.bits)
    (fuel : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (initial : Invariant threshold k capacity budget large target fuel s.mem) :
    ∃ time final, time ≤ fuel * (bodyCost n k w.bits capacity + 2) + 2 ∧
      Runs widthConstant ((Traversal.algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      ∃ emitted head limit, StackInvariant.Stored final.mem (dataBase k) limit head emitted ∧
        (emitted.map StackInvariant.Task.formula).reverse = target ∧
        final.mem (todoCell k) = 0#w.bits ∧ final.mem (outputCell k) = BitVec.ofNat w.bits head ∧
        final.mem (freeCell k) = BitVec.ofNat w.bits limit ∧ limit ≤ budget ∧
        final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
        (∀ a, dataBase k ≤ a → budget ≤ a → final.mem a = s.mem a) := by
  obtain ⟨time, final, bound, trace, halted, invariant, zero⟩ :=
    SourceWhile.loops (todoCell k) (TraversalBody.algorithm threshold k).code (bodyCost n k w.bits capacity)
      (fun fuel mem => Invariant threshold k capacity budget large target fuel mem ∧
        ∀ a, dataBase k ≤ a → budget ≤ a → mem a = s.mem a)
      (fun _ _ h => guard fits h.1)
      (by
        intro fuel state pc live h
        obtain ⟨time, final, bound, trace, halted, invariant, frame⟩ :=
          iteration_framed threshold k capacity budget large target variablesFit width thresholdFits fits fuel state pc live h.1
        refine ⟨time, final, bound, trace, halted, invariant, ?_⟩
        intro a ha hb
        exact (frame a ha hb).trans (h.2 a ha hb))
      fuel s pc live ⟨initial, by intros; rfl⟩
  obtain ⟨invariant, frame⟩ := invariant
  obtain ⟨tasks, emitted, head, outputHead, limit, pending, outputs, ready, variables,
    todoPointer, outputPointer, freePointer, work, order, space⟩ := invariant
  have empty : tasks.map StackInvariant.Task.formula = [] :=
    (work_zero_iff _ threshold k large).mp work
  rw [empty] at order
  simp only [Frontier.leaves, List.append_nil] at order
  exact ⟨time, final, bound, trace, halted, emitted, outputHead, limit,
    outputs, order, zero, outputPointer, freePointer, by omega, variables, frame⟩

/-- A single ready root generates precisely the recursive sparsification leaves. -/
theorem root (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (task : StackInvariant.Task n) (head limit : Nat) (s : State w)
    (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits) (fits : budget < 2 ^ w.bits)
    (pc : s.pc = 0) (live : s.halted = false) (ready : Ready k capacity task.formula)
    (pending : StackInvariant.Stored s.mem (dataBase k) limit head [task])
    (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) = 0#w.bits)
    (freePointer : s.mem (freeCell k) = BitVec.ofNat w.bits limit)
    (space : limit + Work.calls task.formula threshold k large * stride capacity ≤ budget) :
    ∃ time final, time ≤ Work.calls task.formula threshold k large * (bodyCost n k w.bits capacity + 2) + 2 ∧
      Runs widthConstant ((Traversal.algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      ∃ emitted head limit, StackInvariant.Stored final.mem (dataBase k) limit head emitted ∧
        (emitted.map StackInvariant.Task.formula).reverse = Tree.leaves task.formula threshold k large ∧
        final.mem (todoCell k) = 0#w.bits ∧ final.mem (outputCell k) = BitVec.ofNat w.bits head ∧
        final.mem (freeCell k) = BitVec.ofNat w.bits limit ∧ limit ≤ budget ∧
        final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
        (∀ a, dataBase k ≤ a → budget ≤ a → final.mem a = s.mem a) := by
  apply traverses threshold k capacity budget large _ variablesFit width thresholdFits fits _ s pc live
  refine ⟨[task], [], head, 0, limit, pending, rfl, ?_, variables, todoPointer, outputPointer, freePointer, ?_, ?_, space⟩
  · simpa using ready
  · simp [Frontier.work]
  · simp [Frontier.leaves]

end WordRAM.Conjectures.Sparsification.TraversalFresh

/-! Concrete root-stack initialization followed by the verified DFS generator. -/
namespace WordRAM.Conjectures.Sparsification.GenerateFresh
open TraversalBody TraversalBounds

/-- Generate all sparse leaves from a ready normalized table. The caller supplies
actual table contents and register values, not an abstract sparsification oracle. -/
theorem generates (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (task : StackInvariant.Task n) (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) (fits : budget < 2 ^ w.bits)
    (base : dataBase k ≤ task.address) (endBound : task.address + 3 * task.formula.length ≤ limit)
    (table : VectorBuilder.Stored s.mem task.address (RecordTable.words w task.formula))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (pointer : s.mem 22 = BitVec.ofNat w.bits task.address)
    (count : s.mem 24 = BitVec.ofNat w.bits task.formula.length)
    (free : s.mem 27 = BitVec.ofNat w.bits limit)
    (ready : TraversalFacts.Ready k capacity task.formula)
    (space : limit + 3 + Work.calls task.formula threshold k large * stride capacity ≤ budget) :
    ∃ time final, time ≤ Work.calls task.formula threshold k large * (bodyCost n k w.bits capacity + 2) + 26 ∧
      Runs widthConstant ((Generate.algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      ∃ emitted head limit, StackInvariant.Stored final.mem (dataBase k) limit head emitted ∧
        (emitted.map StackInvariant.Task.formula).reverse = Tree.leaves task.formula threshold k large ∧
        final.mem (todoCell k) = 0#w.bits ∧ final.mem (outputCell k) = BitVec.ofNat w.bits head ∧
        final.mem (freeCell k) = BitVec.ofNat w.bits limit ∧ limit ≤ budget ∧
        final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
        (∀ a, budget ≤ a → final.mem a = s.mem a) := by
  obtain ⟨initialized, initTrace, initHalt, pending, variables', todo', output', free', initFrame⟩ :=
    RootStack.initializes_framed k task limit s pc live base endBound (by omega) table variables pointer count free
  obtain ⟨time, out, bound, trace, halted, emitted, head, limit', stored, order, todo, output, free'', space', finalVariables, frame⟩ :=
    TraversalFresh.root threshold k capacity budget large task limit (limit + 3) (SourceChain.resume initialized)
      variablesFit width thresholdFits fits rfl rfl ready pending variables' todo' output' free' space
  have full := SourceChain.traces (RootStack.algorithm k).code (Traversal.algorithm threshold k).code
    s initialized out 24 time live initHalt initTrace trace
  refine ⟨24 + time, out.relocate (RootStack.algorithm k).code.length, by omega, full, halted,
    emitted, head, limit', stored, order, todo, output, free'', space', finalVariables, ?_⟩
  intro a ha
  exact (frame a (by omega) ha).trans (initFrame a (by omega))

end WordRAM.Conjectures.Sparsification.GenerateFresh

/-! Reject empty clauses before running the DFS leaf generator. -/
namespace WordRAM.Conjectures.Sparsification.CheckedGenerateFresh
open TraversalBody TraversalBounds

/-- An empty clause produces no leaves. Every other normalized root is traversed
by the concrete stack machine. Both cases agree with `Tree.leaves`. -/
theorem generates (threshold : Nat → Nat) (k capacity budget : Nat) (large : ∀ i, 2 ≤ threshold i)
    (task : StackInvariant.Task n) (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) (fits : budget < 2 ^ w.bits)
    (base : dataBase k ≤ task.address) (endBound : task.address + 3 * task.formula.length ≤ limit)
    (table : VectorBuilder.Stored s.mem task.address (RecordTable.words w task.formula))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (pointer : s.mem 22 = BitVec.ofNat w.bits task.address)
    (count : s.mem 24 = BitVec.ofNat w.bits task.formula.length)
    (scanPointer : s.mem 18 = BitVec.ofNat w.bits task.address)
    (scanCount : s.mem 17 = BitVec.ofNat w.bits task.formula.length)
    (free : s.mem 27 = BitVec.ofNat w.bits limit)
    (normalized : Normalize.normalize task.formula = task.formula)
    (clauseWidth : ∀ clause ∈ task.formula, clause.length ≤ k)
    (weight : Sparsification.weight task.formula ≤ capacity)
    (space : limit + 3 + Work.calls task.formula threshold k large * stride capacity ≤ budget) :
    ∃ time final, time ≤ Work.calls task.formula threshold k large * (bodyCost n k w.bits capacity + 2) +
        12 * task.formula.length + 35 ∧
      Runs widthConstant ((CheckedGenerate.algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      ∃ emitted head limit, StackInvariant.Stored final.mem (dataBase k) limit head emitted ∧
        (emitted.map StackInvariant.Task.formula).reverse = Tree.leaves task.formula threshold k large ∧
        final.mem (todoCell k) = 0#w.bits ∧ final.mem (outputCell k) = BitVec.ofNat w.bits head ∧
        final.mem (freeCell k) = BitVec.ofNat w.bits limit ∧ limit ≤ budget ∧
        final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
        (∀ a, budget ≤ a → final.mem a = s.mem a) := by
  have base16 : 16 ≤ task.address := by dsimp [dataBase, variableCell] at base; omega
  obtain ⟨scanTime, scanned, scanBound, scanTrace, scanHalt, flag, frame⟩ :=
    EmptyClause.detects task.formula s task.address pc live base16 (by omega) variablesFit scanCount scanPointer table
  let next := (SourceChain.resume scanned).addTicks 1
  have nextInput : VectorBuilder.Stored next.mem task.address (RecordTable.words w task.formula) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact frame a (by omega)
  have nv : next.mem 16 = BitVec.ofNat w.bits n := (frame 16 (by decide)).trans variables
  have np : next.mem 22 = BitVec.ofNat w.bits task.address := (frame 22 (by decide)).trans pointer
  have nc : next.mem 24 = BitVec.ofNat w.bits task.formula.length := (frame 24 (by decide)).trans count
  have nf : next.mem 27 = BitVec.ofNat w.bits limit := (frame 27 (by decide)).trans free
  by_cases empty : [] ∈ task.formula
  · have leaves : Tree.leaves task.formula threshold k large = [] := by
      rw [Tree.leaves, normalized]; simp only [if_pos empty]
    let out := run widthConstant ((RootStack.prepare k).program w) 7 next
    obtain ⟨halted, ticks, var, todo, output, free', _, _, prepareFrame⟩ := RootStack.prepares k next rfl rfl
    obtain ⟨time, _, trace⟩ := run_has_trace widthConstant ((RootStack.prepare k).program w) 7 next
    have cost := runs_cost trace
    have exactTime : time = 7 := by omega
    subst time
    have nonzero : scanned.mem 0 ≠ 0#w.bits := by
      rw [flag, if_pos empty]
      intro eq
      have values := congrArg BitVec.toNat eq
      have modulus : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by omega)
      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt modulus, Nat.zero_mod] at values
      omega
    have dispatched := SourceIf.nonzero_trace 0 (Generate.algorithm threshold k).code (RootStack.prepare k).code
      (SourceChain.resume scanned) out 7 rfl rfl nonzero trace
    have full := SourceChain.traces EmptyClause.algorithm.code (CheckedGenerate.dispatch threshold k).code s scanned
      (out.relocate 1) scanTime 8 live scanHalt scanTrace dispatched
    refine ⟨scanTime + 8, (out.relocate 1).relocate EmptyClause.algorithm.code.length, by omega,
      full, halted, [], 0, limit, rfl, ?_, todo, output, ?_, by omega, var.trans nv, ?_⟩
    · simpa using leaves.symm
    · exact free'.trans nf
    · intro a ha
      exact (prepareFrame a (by omega)).trans (frame a (by dsimp [dataBase, variableCell] at base; omega))
  · obtain ⟨time, out, bound, trace, halted, emitted, head, limit', stored, order, todo, output, free', space', finalVariables, generateFrame⟩ :=
      GenerateFresh.generates threshold k capacity budget large task limit next rfl rfl variablesFit width thresholdFits fits
        base endBound nextInput nv np nc nf ⟨normalized, empty, clauseWidth, weight⟩ space
    have zero : scanned.mem 0 = 0#w.bits := by simpa only [if_neg empty] using flag
    have dispatched := SourceIf.zero_trace 0 (Generate.algorithm threshold k).code (RootStack.prepare k).code
      (SourceChain.resume scanned) out time rfl rfl zero trace
    have full := SourceChain.traces EmptyClause.algorithm.code (CheckedGenerate.dispatch threshold k).code s scanned
      (out.relocate (1 + (RootStack.prepare k).code.length)) scanTime (1 + time) live scanHalt scanTrace dispatched
    refine ⟨scanTime + (1 + time), (out.relocate (1 + (RootStack.prepare k).code.length)).relocate EmptyClause.algorithm.code.length,
      by omega, full, halted, emitted, head, limit', stored, order, todo, output, free', space', finalVariables, ?_⟩
    intro a ha
    exact (generateFrame a ha).trans (frame a (by dsimp [dataBase, variableCell] at base; omega))

end WordRAM.Conjectures.Sparsification.CheckedGenerateFresh

/-! From protected serialized clauses to the exact sparsification leaf stack. -/
namespace WordRAM.Conjectures.Sparsification.SerializedGenerateFresh
open TraversalBody TraversalBounds

/-- Includes mask construction, normalization, empty-clause rejection, root
initialization, and the complete traversal. The input must already be protected
above the scratch/control region. -/
theorem generates (clauses : CNF n) (threshold : Nat → Nat) (k capacity budget : Nat)
    (large : ∀ i, 2 ≤ threshold i) (s : State w) (source records workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : dataBase k ≤ source)
    (inputBefore : source + MaskTable.span clauses ≤ records)
    (recordsBefore : records + 3 * clauses.length ≤ workspace)
    (fits : budget < 2 ^ w.bits) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 2 ^ w.bits)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (recordPointer : s.mem 13 = BitVec.ofNat w.bits records)
    (workspacePointer : s.mem 27 = BitVec.ofNat w.bits workspace)
    (input : MaskTable.Encoded s.mem source clauses)
    (clauseWidth : ∀ clause ∈ clauses, clause.length ≤ k)
    (weight : Sparsification.weight clauses ≤ capacity)
    (space : NormalizeSetup.endpoint workspace clauses.length + 3 +
      Work.calls (Normalize.normalize clauses) threshold k large * stride capacity ≤ budget) :
    ∃ time final, time ≤ RecordTable.cost w clauses + clauses.length * (35 * clauses.length + 34) +
        Work.calls (Normalize.normalize clauses) threshold k large * (bodyCost n k w.bits capacity + 2) +
        12 * clauses.length + 66 ∧
      Runs widthConstant ((SerializedGenerate.algorithm threshold k).program w) time s final ∧ final.halted = true ∧
      ∃ emitted head limit, StackInvariant.Stored final.mem (dataBase k) limit head emitted ∧
        (emitted.map StackInvariant.Task.formula).reverse = Tree.leaves clauses threshold k large ∧
        final.mem (todoCell k) = 0#w.bits ∧ final.mem (outputCell k) = BitVec.ofNat w.bits head ∧
        final.mem (freeCell k) = BitVec.ofNat w.bits limit ∧ limit ≤ budget ∧
        final.mem (variableCell k) = BitVec.ofNat w.bits n ∧
        (∀ a, budget ≤ a → final.mem a = s.mem a) := by
  obtain ⟨normalizeTime, normalized, address, normalizeBound, normalizeTrace, normalizeHalt,
    table, lower, upper, nv, np, nc, nsp, nsc, nf, normalizeFrame⟩ :=
    NormalizeSetup.normalizes_framed clauses k s source records workspace pc live base inputBefore recordsBefore
      (by omega) variablesFit variables count pointer recordPointer workspacePointer input
  let task : StackInvariant.Task n := ⟨Normalize.normalize clauses, address⟩
  have normalizedWidth := Normalize.normalize_kcnf (SATInstance.mk n clauses) clauseWidth
  have normalizedWeight := Nat.le_trans (Normalize.normalize_weight clauses) weight
  obtain ⟨time, out, bound, trace, halted, emitted, head, limit, stored, order, todo, output, free, space', finalVariables, generateFrame⟩ :=
    CheckedGenerateFresh.generates threshold k capacity budget large task (NormalizeSetup.endpoint workspace clauses.length)
      (SourceChain.resume normalized) rfl rfl variablesFit width thresholdFits fits lower upper table
      nv np nc nsp nsc nf (Normalize.normalize_idempotent clauses) normalizedWidth normalizedWeight space
  have full := SourceChain.traces (NormalizeSetup.algorithm k).code (CheckedGenerate.algorithm threshold k).code
    s normalized out normalizeTime time live normalizeHalt normalizeTrace trace
  have lengthBound := Normalize.normalize_length clauses
  refine ⟨normalizeTime + time, out.relocate (NormalizeSetup.algorithm k).code.length, ?_, full, halted,
    emitted, head, limit, stored, order.trans (SerializedGenerate.normalized_leaves clauses threshold k large), todo, output, free, space', finalVariables, ?_⟩
  · change time ≤ Work.calls (Normalize.normalize clauses) threshold k large *
      (bodyCost n k w.bits capacity + 2) + 12 * (Normalize.normalize clauses).length + 35 at bound
    omega
  · intro a ha
    exact (generateFrame a ha).trans (normalizeFrame a (by omega))

end WordRAM.Conjectures.Sparsification.SerializedGenerateFresh