SETH ⇒ OVC sparsification bundle 31: 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_30

set_option autoImplicit true

/-! One actual wordRAM step of stable branch-table partitioning. -/
namespace WordRAM.Conjectures.Sparsification.BranchRoute

def cursor (petal : Bool) : Nat := if petal then 19 else 18

def count (petal : Bool) : Nat := if petal then 17 else 16

def dispatch : Algorithm :=
  ⟨SourceIf.code 0 (BranchEmit.algorithm false 18 16).code (BranchEmit.algorithm true 19 17).code, 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code RecordMatches.algorithm.code dispatch.code, 1, by decide⟩

/-- Persistent controls: counts 16,17; cursors 18,19; core masks 20,21;
selected size 22; input cursor 23. The selected output is an original record
for a non-family clause and its petal record for a family clause. -/
theorem dispatches (petal : Bool) (core clause : Clause n) (s : State w)
    (address destination : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 32 ≤ address) (fits : address + 2 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 23 = BitVec.ofNat w.bits address)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w [clause]))
    (destinationBase : 32 ≤ destination) (destinationFits : destination + 2 < 2 ^ w.bits)
    (destinationPointer : s.mem (cursor petal) = BitVec.ofNat w.bits destination)
    (test : s.mem 0 = if petal then 1#w.bits else 0#w.bits) :
    ∃ final, Runs widthConstant (dispatch.program w)
        (26 + if petal then 12 * w.bits + 23 else 0) s final ∧ final.halted = true ∧
      final.mem (cursor petal) = BitVec.ofNat w.bits (destination + 3) ∧
      final.mem (count petal) = s.mem (count petal) + 1#w.bits ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w [BranchEmit.output petal core clause]) ∧
      (∀ a, 16 ≤ a → a ≠ cursor petal → a ≠ count petal → a ≠ destination →
        a ≠ destination + 1 → a ≠ destination + 2 → final.mem a = s.mem a) := by
  have cb : 16 ≤ cursor petal := by cases petal <;> decide
  have ce : cursor petal < 32 := by cases petal <;> decide
  have nb : 16 ≤ count petal := by cases petal <;> decide
  have ne : count petal < 32 := by cases petal <;> decide
  have cn : cursor petal ≠ count petal := by cases petal <;> decide
  obtain ⟨out, trace, halted, outPointer, outCount, stored, frame⟩ :=
    BranchEmit.emits petal core clause (s.addTicks 1) address destination (cursor petal) (count petal)
      pc live base fits variablesFit pointer qp qn input cb ce nb ne cn destinationBase destinationFits destinationPointer
  cases petal with
  | false =>
    have full := SourceIf.zero_trace 0 (BranchEmit.algorithm false 18 16).code
      (BranchEmit.algorithm true 19 17).code s out 25 pc live test trace
    exact ⟨out.relocate (1 + (BranchEmit.algorithm true 19 17).code.length), full, halted,
      outPointer, outCount, stored, frame⟩
  | true =>
    have nonzero : s.mem 0 ≠ 0#w.bits := by
      rw [test]
      have positive := w.positive
      intro h
      have h' := congrArg BitVec.toNat h
      have oneFits : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by omega)
      simp [Nat.mod_eq_of_lt oneFits] at h'
    have full := SourceIf.nonzero_trace 0 (BranchEmit.algorithm false 18 16).code
      (BranchEmit.algorithm true 19 17).code s out (25 + (12 * w.bits + 23)) pc live nonzero trace
    refine ⟨out.relocate 1, ?_, halted, outPointer, outCount, stored, frame⟩
    have cost : 1 + (25 + (12 * w.bits + 23)) = 26 + (12 * w.bits + 23) := by omega
    simpa only [dispatch, Algorithm.program, cost, if_true] using full

/-- Classification and both emission paths are justified by concrete execution
traces. The memory frame in particular preserves the other output buffer. -/
theorem routes (core clause : Clause n) (size : Nat) (s : State w)
    (address remainingDestination petalDestination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ address)
    (fits : address + 3 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : clause.Nodup)
    (pointer : s.mem 23 = BitVec.ofNat w.bits address)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (target : s.mem 22 = BitVec.ofNat w.bits size)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w [clause]))
    (remainingBase : 32 ≤ remainingDestination) (remainingFits : remainingDestination + 2 < 2 ^ w.bits)
    (remainingPointer : s.mem 18 = BitVec.ofNat w.bits remainingDestination)
    (petalBase : 32 ≤ petalDestination) (petalFits : petalDestination + 2 < 2 ^ w.bits)
    (petalPointer : s.mem 19 = BitVec.ofNat w.bits petalDestination) :
    let eligible := decide (clause.length = size ∧ core ⊆ clause)
    let destination := if eligible then petalDestination else remainingDestination
    ∃ time final, time ≤ 12 * w.bits + 79 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.halted = true ∧ final.mem (cursor eligible) = BitVec.ofNat w.bits (destination + 3) ∧
      final.mem (count eligible) = s.mem (count eligible) + 1#w.bits ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w [BranchEmit.output eligible core clause]) ∧
      (∀ a, 16 ≤ a → a ≠ cursor eligible → a ≠ count eligible → a ≠ destination →
        a ≠ destination + 1 → a ≠ destination + 2 → final.mem a = s.mem a) := by
  let eligible := decide (clause.length = size ∧ core ⊆ clause)
  let destination := if eligible then petalDestination else remainingDestination
  obtain ⟨time, classified, bound, ct, ch, test, cf⟩ := RecordMatches.classifies core clause size s address
    pc live (by omega) fits variablesFit width sizeFits nodup qp qn target pointer input
  have ci : VectorBuilder.Stored classified.mem address (RecordTable.words w [clause]) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a ha _; exact cf a (by omega)
  have db : 32 ≤ destination := by dsimp [destination]; split <;> assumption
  have df : destination + 2 < 2 ^ w.bits := by dsimp [destination]; split <;> assumption
  have dp : classified.mem (cursor eligible) = BitVec.ofNat w.bits destination := by
    have cb : 16 ≤ cursor eligible := by cases eligible <;> decide
    rw [cf _ cb]
    dsimp [cursor, destination]
    split <;> assumption
  have flag : classified.mem 0 = if eligible then 1#w.bits else 0#w.bits := by simpa [eligible] using test
  obtain ⟨out, trace, halted, outPointer, outCount, stored, frame⟩ :=
    dispatches eligible core clause (SourceChain.resume classified) address destination rfl rfl base
      (by omega) variablesFit ((cf 23 (by decide)).trans pointer) ((cf 20 (by decide)).trans qp)
      ((cf 21 (by decide)).trans qn) ci db df dp flag
  have full := SourceChain.traces RecordMatches.algorithm.code dispatch.code s classified out
    time (26 + if eligible then 12 * w.bits + 23 else 0) live ch ct trace
  refine ⟨time + (26 + if eligible then 12 * w.bits + 23 else 0),
    out.relocate RecordMatches.algorithm.code.length, ?_, full, halted, outPointer, ?_, stored, ?_⟩
  · split <;> omega
  · have cb : 16 ≤ count eligible := by cases eligible <;> decide
    exact outCount.trans (congrArg (fun v => v + 1#w.bits) (cf _ cb))
  · intro a ha hc hn h0 h1 h2
    exact (frame a ha hc hn h0 h1 h2).trans (cf a ha)

end WordRAM.Conjectures.Sparsification.BranchRoute

/-! Bounded iteration with an invariant indexed by the number of completed steps. -/
namespace WordRAM.Conjectures.SourceFor

open SourceSearch

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time
  exact trace

/-- Iterate the actual source body once at each index. Unlike search, the
invariant advances after each body execution. A zero result keeps the loop
running; initialization, guards, updates, and exit all contribute to cost. -/
theorem iterates (index limit : Nat) (body : List SourceInstruction) (stop cost : Nat)
    (invariant : Nat → Memory w → Prop)
    (limitNonzero : limit ≠ 0) (separate : limit ≠ index) (stopFits : stop < 2 ^ w.bits)
    (stable : ∀ i mem cell value, invariant i mem → (cell = 0 ∨ cell = index) → invariant i (mem.write cell value))
    (bodyCorrect : ∀ i, i < stop → ∀ s : State w, s.pc = 0 → s.halted = false → invariant i s.mem →
      s.mem index = BitVec.ofNat w.bits i → s.mem limit = BitVec.ofNat w.bits stop →
      ∃ time out, time ≤ cost ∧ Runs widthConstant (body.map (SourceInstruction.compile w)) time s out ∧
        out.halted = true ∧ invariant (i + 1) out.mem ∧ out.mem 0 = 0#w.bits ∧
        out.mem index = BitVec.ofNat w.bits i ∧ out.mem limit = BitVec.ofNat w.bits stop)
    (start count : Nat) (s : State w) (extent : start + count = stop)
    (pc : s.pc = 0) (live : s.halted = false) (initial : invariant start s.mem)
    (current : s.mem index = BitVec.ofNat w.bits start) (bound : s.mem limit = BitVec.ofNat w.bits stop) :
    ∃ time final, time ≤ count * (cost + 4) + 3 ∧
      Runs widthConstant ((SourceSearch.algorithm index limit body).program w) time s final ∧ final.halted = true ∧
      invariant stop final.mem ∧ final.mem limit = BitVec.ofNat w.bits stop ∧ final.mem 0 = 0#w.bits := by
  induction count generalizing start s with
  | zero =>
    have eq : start = stop := by omega
    have done : s.mem index = s.mem limit := by rw [current, bound, eq]
    obtain ⟨halted, ticks, mem⟩ := exits index limit body s pc live done
    refine ⟨3, run widthConstant ((SourceSearch.algorithm index limit body).program w) 3 s, by simp,
      trace_of_ticks _ s 3 ticks, halted, ?_, ?_, ?_⟩
    · rw [mem, ← eq]; exact stable start s.mem 0 (0#w.bits) initial (Or.inl rfl)
    · rw [mem]; simpa [Memory.write, limitNonzero] using bound
    · simp [mem, Memory.write]
  | succ count ih =>
    have active : start < stop := by omega
    have startFits : start < 2 ^ w.bits := by omega
    have different : s.mem index ≠ s.mem limit := by
      rw [current, bound]
      intro eq
      have values := congrArg BitVec.toNat eq
      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt startFits, Nat.mod_eq_of_lt stopFits] at values
      omega
    let head := run widthConstant ((algorithm index limit body).program w) 1 s
    obtain ⟨hpc, hlive, hticks, hmem⟩ := enters index limit body s pc live different
    let entry : State w := { head with pc := 0 }
    have entryLive : entry.halted = false := hlive
    have entryMem : entry.mem = s.mem := hmem
    obtain ⟨bodyTime, out, bodyBound, bodyTrace, halted, outInvariant, answer, outIndex, outLimit⟩ :=
      bodyCorrect start active entry rfl entryLive (by rw [entryMem]; exact initial)
        ((congrFun entryMem index).trans current) ((congrFun entryMem limit).trans bound)
    have embedded : EmbedsAt ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        ((algorithm index limit body).program w) 1 := by
      simp only [SourceSearch.algorithm, Algorithm.program, List.map_append, List.map_map,
        Function.comp_def, compile_relocate, compile_returnTo, List.append_assoc]
      simpa only [List.map_map, Function.comp_def, header, List.map_cons, List.map_nil, List.length_cons, List.length_nil] using embeds_append ((header index limit body.length).map (SourceInstruction.compile w))
        ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        ((trailer index body.length).map (SourceInstruction.compile w))
    let returned := (out.returnTo body.length).relocate 1
    have linked : Runs widthConstant ((algorithm index limit body).program w) bodyTime head returned := by
      have h := (bodyTrace.returnTo body.length).relocate embedded
      have he : (entry.returnTo body.length).relocate 1 = head := by
        simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
        change { head with pc := 1 } = head
        have hpc' : head.pc = 1 := hpc
        rw [← hpc']
      simpa only [he] using h
    have rmem : returned.mem = out.mem := by simp [returned, State.returnTo, State.relocate, halted]
    have rpc : returned.pc = body.length + 1 := by simp [returned, State.returnTo, State.relocate, halted, Nat.add_comm]
    have rlive : returned.halted = false := by simp [returned, State.returnTo, State.relocate, halted]
    have result : returned.mem 0 = 0#w.bits := by rw [rmem]; exact answer
    obtain ⟨npc, nlive, nticks, nmem⟩ := advances index limit body returned rpc rlive result
    let next := run widthConstant ((algorithm index limit body).program w) 3 returned
    have mem : next.mem = out.mem.write index (out.mem index + 1#w.bits) := by
      simpa only [rmem] using nmem
    have nextInvariant : invariant (start + 1) next.mem := by
      rw [mem]; exact stable (start + 1) out.mem index _ outInvariant (Or.inr rfl)
    have nextIndex : next.mem index = BitVec.ofNat w.bits (start + 1) := by
      rw [mem]
      simp only [Memory.write, ↓reduceIte, outIndex]
      rw [← BitVec.ofNat_add]
    have nextLimit : next.mem limit = BitVec.ofNat w.bits stop := by
      rw [mem]; simpa only [Memory.write, if_neg separate] using outLimit
    obtain ⟨time, final, timeBound, trace, finalHalt, finalInvariant, finalLimit, finalZero⟩ :=
      ih (start + 1) next (by omega) npc nlive nextInvariant nextIndex nextLimit
    refine ⟨1 + bodyTime + 3 + time, final, ?_,
      (((trace_of_ticks _ s 1 hticks).append linked).append (trace_of_ticks _ returned 3 nticks)).append trace,
      finalHalt, finalInvariant, finalLimit, finalZero⟩
    · simp only [Nat.add_mul, Nat.one_mul]; omega

/-- Execute indices `0, …, stop - 1`, resetting a possibly stale index word. -/
theorem iterates_from_zero (index limit : Nat) (body : List SourceInstruction) (stop cost : Nat)
    (invariant : Nat → Memory w → Prop)
    (limitNonzero : limit ≠ 0) (separate : limit ≠ index) (stopFits : stop < 2 ^ w.bits)
    (stable : ∀ i mem cell value, invariant i mem → (cell = 0 ∨ cell = index) → invariant i (mem.write cell value))
    (bodyCorrect : ∀ i, i < stop → ∀ s : State w, s.pc = 0 → s.halted = false → invariant i s.mem →
      s.mem index = BitVec.ofNat w.bits i → s.mem limit = BitVec.ofNat w.bits stop →
      ∃ time out, time ≤ cost ∧ Runs widthConstant (body.map (SourceInstruction.compile w)) time s out ∧
        out.halted = true ∧ invariant (i + 1) out.mem ∧ out.mem 0 = 0#w.bits ∧
        out.mem index = BitVec.ofNat w.bits i ∧ out.mem limit = BitVec.ofNat w.bits stop)
    (s : State w) (pc : s.pc = 0) (live : s.halted = false) (initial : invariant 0 s.mem)
    (bound : s.mem limit = BitVec.ofNat w.bits stop) :
    ∃ time final, time ≤ stop * (cost + 4) + 5 ∧
      Runs widthConstant ((SourceSearch.initialized index limit body).program w) time s final ∧ final.halted = true ∧
      invariant stop final.mem ∧ final.mem limit = BitVec.ofNat w.bits stop ∧ final.mem 0 = 0#w.bits := by
  let middle := run widthConstant ((setup index).program w) 2 s
  obtain ⟨halted, ticks, mem⟩ := initializes index s pc live
  have nextInvariant : invariant 0 middle.mem := by
    rw [mem]; exact stable 0 s.mem index _ initial (Or.inr rfl)
  have nextIndex : middle.mem index = BitVec.ofNat w.bits 0 := by simp [middle, mem, Memory.write]
  have nextLimit : middle.mem limit = BitVec.ofNat w.bits stop := by
    rw [mem]; simpa only [Memory.write, if_neg separate] using bound
  obtain ⟨time, out, timeBound, trace, outHalt, finalInvariant, finalLimit, finalZero⟩ :=
    iterates index limit body stop cost invariant limitNonzero separate stopFits stable bodyCorrect
      0 stop (SourceChain.resume middle) (by omega) rfl rfl nextInvariant nextIndex nextLimit
  have full := SourceChain.traces (setup index).code (SourceSearch.algorithm index limit body).code s middle out 2 time
    live halted (trace_of_ticks _ s 2 ticks) trace
  exact ⟨2 + time, out.relocate (setup index).code.length, by omega, full, outHalt,
    finalInvariant, finalLimit, finalZero⟩

end WordRAM.Conjectures.SourceFor

/-! Stable partition into remaining-clause and petal record buffers. -/
namespace WordRAM.Conjectures.Sparsification.BranchPartition

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

def advance : Algorithm :=
  ⟨[.binary .add (.direct 23) (reg 23) (.immediate 3), .copy (.direct 0) (.immediate 0), .halt], 1, by decide⟩

def body : Algorithm := ⟨SourceChain.code BranchRoute.algorithm.code advance.code, 1, by decide⟩

def setup : Algorithm :=
  ⟨[.copy (.direct 25) (reg 24), .copy (.direct 16) (.immediate 0),
    .copy (.direct 17) (.immediate 0), .halt], 1, by decide⟩

/-- Input count 24, input cursor 23, selected size 22, core masks 20/21,
remaining/petal destinations 18/19. Output counts 16/17 are initialized here.
The index 24 is reused after its input count is saved in 25. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code setup.code (SourceSearch.initialized 24 25 body.code).code, 1, by decide⟩

theorem advances (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (advance.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 23 = s.mem 23 + 3#w.bits ∧
      t.mem 0 = 0#w.bits ∧ (∀ a, a ≠ 0 → a ≠ 23 → t.mem a = s.mem a) := by
  simp [advance, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, Nat.add_assoc]
  intro a h0 h23; simp [h0, h23]

theorem initializes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (setup.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 25 = s.mem 24 ∧
      t.mem 16 = 0#w.bits ∧ t.mem 17 = 0#w.bits ∧
      (∀ a, a ≠ 25 → a ≠ 16 → a ≠ 17 → t.mem a = s.mem a) := by
  simp [setup, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h25 h16 h17; simp [h25, h16, h17]

private theorem trace_of_ticks (program : Program w .multiplication 1) (s : State w) (fuel : Nat)
    (cost : (run widthConstant program fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant program fuel s (run widthConstant program fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant program fuel s
  have ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time; exact trace

/-- One partition iteration, including the input-cursor update and the zero
return flag required by the bounded loop. -/
theorem iteration (core clause : Clause n) (size : Nat) (s : State w)
    (address remainingDestination petalDestination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ address)
    (fits : address + 3 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : clause.Nodup)
    (pointer : s.mem 23 = BitVec.ofNat w.bits address)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (target : s.mem 22 = BitVec.ofNat w.bits size)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w [clause]))
    (remainingBase : 32 ≤ remainingDestination) (remainingFits : remainingDestination + 2 < 2 ^ w.bits)
    (remainingPointer : s.mem 18 = BitVec.ofNat w.bits remainingDestination)
    (petalBase : 32 ≤ petalDestination) (petalFits : petalDestination + 2 < 2 ^ w.bits)
    (petalPointer : s.mem 19 = BitVec.ofNat w.bits petalDestination) :
    let eligible := decide (clause.length = size ∧ core ⊆ clause)
    let destination := if eligible then petalDestination else remainingDestination
    ∃ time final, time ≤ 12 * w.bits + 82 ∧ Runs widthConstant (body.program w) time s final ∧
      final.halted = true ∧ final.mem 0 = 0#w.bits ∧ final.mem 23 = BitVec.ofNat w.bits (address + 3) ∧
      final.mem (BranchRoute.cursor eligible) = BitVec.ofNat w.bits (destination + 3) ∧
      final.mem (BranchRoute.count eligible) = s.mem (BranchRoute.count eligible) + 1#w.bits ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w [BranchEmit.output eligible core clause]) ∧
      (∀ a, 16 ≤ a → a ≠ 23 → a ≠ BranchRoute.cursor eligible → a ≠ BranchRoute.count eligible →
        a ≠ destination → a ≠ destination + 1 → a ≠ destination + 2 → final.mem a = s.mem a) := by
  let eligible := decide (clause.length = size ∧ core ⊆ clause)
  let destination := if eligible then petalDestination else remainingDestination
  obtain ⟨time, routed, bound, trace, halted, outPointer, outCount, stored, frame⟩ :=
    BranchRoute.routes core clause size s address remainingDestination petalDestination pc live base fits
      variablesFit width sizeFits nodup pointer qp qn target input remainingBase remainingFits remainingPointer
      petalBase petalFits petalPointer
  have db : 32 ≤ destination := by dsimp [destination]; split <;> assumption
  have cursorBounds : 18 ≤ BranchRoute.cursor eligible ∧ BranchRoute.cursor eligible ≤ 19 := by cases eligible <;> decide
  have countBounds : 16 ≤ BranchRoute.count eligible ∧ BranchRoute.count eligible ≤ 17 := by cases eligible <;> decide
  dsimp [eligible, destination] at db cursorBounds countBounds
  let out := run widthConstant (advance.program w) 3 (SourceChain.resume routed)
  obtain ⟨oh, ot, op, oz, ofr⟩ := advances (SourceChain.resume routed) rfl rfl
  have full := SourceChain.traces BranchRoute.algorithm.code advance.code s routed out time 3 live halted trace (trace_of_ticks _ _ 3 ot)
  refine ⟨time + 3, out.relocate BranchRoute.algorithm.code.length, by omega, full, oh, oz, ?_, ?_, ?_, ?_, ?_⟩
  · have rp : routed.mem 23 = s.mem 23 := frame 23 (by decide) (by omega) (by omega) (by omega) (by omega) (by omega)
    exact op.trans ((congrArg (fun v => v + 3#w.bits) (rp.trans pointer)).trans (BitVec.ofNat_add _ _).symm)
  · exact (ofr _ (by omega) (by omega)).trans outPointer
  · exact (ofr _ (by omega) (by omega)).trans outCount
  · apply MemoryCopy.stored_frame _ _ stored
    intro a ha _; exact ofr a (by omega) (by omega)
  · intro a ha h23 hc hn h0 h1 h2
    exact (ofr a (by omega) h23).trans (frame a ha hc hn h0 h1 h2)

end WordRAM.Conjectures.Sparsification.BranchPartition

/-! Prefix identities and serialized-table facts for the partition-loop invariant. -/
namespace WordRAM.Conjectures.Sparsification.BranchTables

def petals (formula : CNF n) (core : Clause n) (size : Nat) : CNF n :=
  (Flowers.family formula core size).map (Branch.petal core)

theorem words_append (w : Width) (left right : CNF n) :
    RecordTable.words w (left ++ right) = RecordTable.words w left ++ RecordTable.words w right := by
  induction left with
  | nil => rfl
  | cons clause rest ih => simp only [List.cons_append, RecordTable.words, ih]

theorem stored_append (left right : List (Word w)) (mem : Memory w) (address : Nat) :
    VectorBuilder.Stored mem address (left ++ right) ↔
      VectorBuilder.Stored mem address left ∧ VectorBuilder.Stored mem (address + left.length) right := by
  induction left generalizing address with
  | nil => simp [VectorBuilder.Stored]
  | cons word rest ih => simp [VectorBuilder.Stored, ih, Nat.add_comm, Nat.add_left_comm, and_assoc]

theorem records_append (left right : CNF n) (mem : Memory w) (address : Nat) :
    VectorBuilder.Stored mem address (RecordTable.words w (left ++ right)) ↔
      VectorBuilder.Stored mem address (RecordTable.words w left) ∧
      VectorBuilder.Stored mem (address + 3 * left.length) (RecordTable.words w right) := by
  rw [words_append, stored_append, RecordTable.words_length]

theorem stored_get (formula : CNF n) (mem : Memory w) (address i : Nat) (hi : i < formula.length)
    (input : VectorBuilder.Stored mem address (RecordTable.words w formula)) :
    VectorBuilder.Stored mem (address + 3 * i) (RecordTable.words w [formula[i]]) := by
  induction formula generalizing address i with
  | nil => simp at hi
  | cons clause rest ih =>
    rcases input with ⟨pos, neg, size, tail⟩
    cases i with
    | zero => exact ⟨pos, neg, size, trivial⟩
    | succ i =>
      have out := ih (address + 3) i (by simpa using hi) tail
      simpa only [List.getElem_cons_succ, Nat.mul_add, Nat.mul_one, Nat.add_assoc,
        Nat.add_left_comm, Nat.add_comm] using out

theorem remaining_length (formula : CNF n) (core : Clause n) (size : Nat) :
    (Branch.remaining formula core size).length ≤ formula.length := List.length_filter_le _ _

theorem petals_length (formula : CNF n) (core : Clause n) (size : Nat) :
    (petals formula core size).length ≤ formula.length := by
  simpa only [petals, List.length_map, Flowers.family] using
    List.length_filter_le (fun clause : Clause n => decide (clause.length = size ∧ core ⊆ clause)) formula

theorem remaining_snoc (formula : CNF n) (core clause : Clause n) (size : Nat) :
    Branch.remaining (formula ++ [clause]) core size = Branch.remaining formula core size ++
      (if clause.length = size ∧ core ⊆ clause then [] else [clause]) := by
  by_cases hs : clause.length = size <;> by_cases hc : core ⊆ clause <;>
    simp [Branch.remaining, List.filter_append, hs, hc]

theorem petals_snoc (formula : CNF n) (core clause : Clause n) (size : Nat) :
    petals (formula ++ [clause]) core size = petals formula core size ++
      (if clause.length = size ∧ core ⊆ clause then [Branch.petal core clause] else []) := by
  by_cases h : clause.length = size ∧ core ⊆ clause <;> simp [petals, Flowers.family, List.filter_append, h]

theorem take_succ (formula : CNF n) (i : Nat) (hi : i < formula.length) :
    formula.take (i + 1) = formula.take i ++ [formula[i]] := by
  induction formula generalizing i with
  | nil => simp at hi
  | cons clause rest ih =>
    cases i with
    | zero => rfl
    | succ i => simpa only [List.take_succ_cons, List.getElem_cons_succ, List.cons_append] using
        congrArg (List.cons clause) (ih i (by simpa using hi))

/-- Each original clause contributes to exactly one of the two output tables. -/
theorem partition_length (formula : CNF n) (core : Clause n) (size : Nat) :
    (Branch.remaining formula core size).length + (petals formula core size).length = formula.length := by
  induction formula with
  | nil => rfl
  | cons clause rest ih =>
    cases h : decide (clause.length = size ∧ core ⊆ clause) <;>
      simp only [Branch.remaining, petals, Flowers.family, List.filter_cons, List.length_map, h,
        Bool.not_true, Bool.not_false, Bool.false_eq_true, ↓reduceIte,
        List.length_cons] at ih ⊢ <;> omega

end WordRAM.Conjectures.Sparsification.BranchTables