SETH ⇒ OVC sparsification bundle 30: 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_29

set_option autoImplicit true

/-! Complete mask-and-size records for a sparsification petal. -/
namespace WordRAM.Conjectures.Sparsification.PetalRecord

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

def bridge : Algorithm :=
  ⟨[.copy (.direct 9) (reg 6), .copy (.direct 10) (reg 7),
    .copy (.direct 1) (reg 6), .copy (.direct 5) (reg 7), .halt], 1, by decide⟩

/-- Clause masks in 1,2; core masks in 3,4. Output record is in 9,10,0.
The population count handles repeated literals without an extra hypothesis. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code PetalMachine.algorithm.code (SourceChain.code bridge.code SizeMachine.algorithm.code), 1, by decide⟩

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 9 = s.mem 6 ∧ t.mem 10 = s.mem 7 ∧
      t.mem 1 = s.mem 6 ∧ t.mem 5 = s.mem 7 ∧
      (∀ a, a ≠ 9 → a ≠ 10 → a ≠ 1 → a ≠ 5 → t.mem a = s.mem a) := by
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h9 h10 h1 h5; simp [h9, h10, h1, h5]

private theorem bridge_trace (s : State w)
    (ticks : (run widthConstant (bridge.program w) 5 s).ticks = s.ticks + 5) :
    Runs widthConstant (bridge.program w) 5 s (run widthConstant (bridge.program w) 5 s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (bridge.program w) 5 s
  have cost := runs_cost trace
  have eq : time = 5 := by omega
  subst time; exact trace

/-- The record represents exactly the list-filter petal used by `Branch`.
Mask construction, register transfers, both population counts, and halting are
included in the exact instruction count. -/
theorem builds (core clause : Clause n) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (cp : s.mem 1 = Masks.encode w clause true) (cn : s.mem 2 = Masks.encode w clause false)
    (qp : s.mem 3 = Masks.encode w core true) (qn : s.mem 4 = Masks.encode w core false) :
    ∃ final, Runs widthConstant (algorithm.program w) (12 * w.bits + 23) s final ∧ final.halted = true ∧
      final.mem 9 = Masks.encode w (Branch.petal core clause) true ∧
      final.mem 10 = Masks.encode w (Branch.petal core clause) false ∧
      final.mem 0 = BitVec.ofNat w.bits (Normalize.clean (Branch.petal core clause)).length ∧
      (∀ a, 11 ≤ a → final.mem a = s.mem a) := by
  let petal := PetalMachine.result s
  obtain ⟨petalTrace, petalHalt, positive, negative⟩ := PetalMachine.builds_petal core clause s pc live cp cn qp qn
  let middle := run widthConstant (bridge.program w) 5 (SourceChain.resume petal)
  obtain ⟨middleHalt, ticks, savedPos, savedNeg, stagedPos, stagedNeg, frame⟩ := bridges (SourceChain.resume petal) rfl rfl
  obtain ⟨out, countTrace, halted, count, countFrame⟩ :=
    SizeMachine.counts (Masks.encode w (Branch.petal core clause) true) (Masks.encode w (Branch.petal core clause) false)
      (SourceChain.resume middle) rfl rfl (stagedPos.trans positive) (stagedNeg.trans negative)
  have counted : out.mem 0 = BitVec.ofNat w.bits (Normalize.clean (Branch.petal core clause)).length := by
    rw [count]
    apply BitVec.eq_of_toNat_eq
    simp only [BitVec.toNat_add, BitVec.toNat_ofNat, MaskCardinality.count_distinct (Branch.petal core clause) variablesFit]
  have tail := SourceChain.traces bridge.code SizeMachine.algorithm.code (SourceChain.resume petal) middle out
    5 (12 * w.bits + 13) rfl middleHalt (bridge_trace _ ticks) countTrace
  have full := SourceChain.traces PetalMachine.algorithm.code (SourceChain.code bridge.code SizeMachine.algorithm.code)
    s petal _ 5 (5 + (12 * w.bits + 13)) live petalHalt petalTrace tail
  refine ⟨(out.relocate bridge.code.length).relocate PetalMachine.algorithm.code.length, ?_, halted, ?_, ?_, counted, ?_⟩
  · have cost : 5 + (5 + (12 * w.bits + 13)) = 12 * w.bits + 23 := by omega
    simpa only [algorithm, Algorithm.program, cost] using full
  · exact (countFrame 9 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedPos.trans positive)
  · exact (countFrame 10 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedNeg.trans negative)
  · intro a ha
    exact (countFrame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
      ((frame a (by omega) (by omega) (by omega) (by omega)).trans
        (PetalMachine.frame s pc live a (by omega) (by omega) (by omega)))

end WordRAM.Conjectures.Sparsification.PetalRecord

/-! Append one three-word record to a clause buffer. -/
namespace WordRAM.Conjectures.Sparsification.RecordAppend

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

/-- Record words in 9,10,0; destination cursor in 13 and record count in 14. -/
def algorithm : Algorithm :=
  ⟨[.copy (.indirect 13) (reg 9), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.indirect 13) (reg 10), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.indirect 13) (reg 0), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .binary .add (.direct 14) (reg 14) (.immediate 1), .halt], 1, by decide⟩

theorem executes (s : State w) (destination : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 16 ≤ destination) (fits : destination + 2 < 2 ^ w.bits)
    (pointer : s.mem 13 = BitVec.ofNat w.bits destination) :
    let t := run widthConstant (algorithm.program w) 8 s
    t.halted = true ∧ t.ticks = s.ticks + 8 ∧ t.mem 13 = BitVec.ofNat w.bits (destination + 3) ∧
      t.mem 14 = s.mem 14 + 1#w.bits ∧ t.mem destination = s.mem 9 ∧
      t.mem (destination + 1) = s.mem 10 ∧ t.mem (destination + 2) = s.mem 0 ∧
      (∀ a, a ≠ 13 → a ≠ 14 → a ≠ destination → a ≠ destination + 1 → a ≠ destination + 2 → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits destination).toNat = destination := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits destination + 1#w.bits).toNat = destination + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt (by omega)
  have d2 : (BitVec.ofNat w.bits destination + 1#w.bits + 1#w.bits).toNat = destination + 2 := by
    rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low0 : ∀ i, i ≤ 15 → destination ≠ i ∧ i ≠ destination := by omega
  have low1 : ∀ i, i ≤ 15 → destination + 1 ≠ i ∧ i ≠ destination + 1 := by omega
  have low2 : ∀ i, i ≤ 15 → destination + 2 ≠ i ∧ i ≠ destination + 2 := by omega
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, d0, d1, d2, low0, low1, low2,
    Nat.add_assoc, -BitVec.toNat_add]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h13 h14 h0 h1 h2; simp [h13, h14, h0, h1, h2]

end WordRAM.Conjectures.Sparsification.RecordAppend

/-! Append a record while retaining the branch buffers' persistent controls. -/
namespace WordRAM.Conjectures.Sparsification.BufferedAppend

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

def prepare (cursor count : Nat) : Algorithm :=
  ⟨[.copy (.direct 13) (reg cursor), .copy (.direct 14) (reg count), .halt], 1, by decide⟩

def finish (cursor count : Nat) : Algorithm :=
  ⟨[.copy (.direct cursor) (reg 13), .copy (.direct count) (reg 14), .halt], 1, by decide⟩

def algorithm (cursor count : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare cursor count).code
    (SourceChain.code RecordAppend.algorithm.code (finish cursor count).code), 1, by decide⟩

theorem prepares (cursor count : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (countBase : 16 ≤ count) :
    let t := run widthConstant ((prepare cursor count).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 13 = s.mem cursor ∧ t.mem 14 = s.mem count ∧
      (∀ a, a ≠ 13 → a ≠ 14 → t.mem a = s.mem a) := by
  have h : count ≠ 13 := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, h, Nat.add_assoc]
  intro a h13 h14; simp [h13, h14]

theorem finishes (cursor count : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (cursorBase : 16 ≤ cursor) (distinct : cursor ≠ count) :
    let t := run widthConstant ((finish cursor count).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem cursor = s.mem 13 ∧ t.mem count = s.mem 14 ∧
      (∀ a, a ≠ cursor → a ≠ count → t.mem a = s.mem a) := by
  have h : 14 ≠ cursor := by omega
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, h, distinct, Nat.add_assoc]
  intro a hc hn; simp [hc, hn]

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

/-- Actual stores plus saving and restoring the persistent cursor and count.
Only these two controls and the new record change above scratch register 15. -/
theorem appends (cursor count destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (cursorBase : 16 ≤ cursor) (cursorEnd : cursor < 32)
    (countBase : 16 ≤ count) (countEnd : count < 32) (distinct : cursor ≠ count)
    (base : 32 ≤ destination) (fits : destination + 2 < 2 ^ w.bits)
    (pointer : s.mem cursor = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant ((algorithm cursor count).program w) 14 s final ∧ final.halted = true ∧
      final.mem cursor = BitVec.ofNat w.bits (destination + 3) ∧
      final.mem count = s.mem count + 1#w.bits ∧
      final.mem destination = s.mem 9 ∧ final.mem (destination + 1) = s.mem 10 ∧
      final.mem (destination + 2) = s.mem 0 ∧
      (∀ a, 16 ≤ a → a ≠ cursor → a ≠ count → a ≠ destination →
        a ≠ destination + 1 → a ≠ destination + 2 → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare cursor count).program w) 3 s
  obtain ⟨ph, pt, pp, pn, pf⟩ := prepares cursor count s pc live countBase
  let appended := run widthConstant (RecordAppend.algorithm.program w) 8 (SourceChain.resume prepared)
  obtain ⟨ah, aticks, ap, an, a0, a1, a2, af⟩ :=
    RecordAppend.executes (SourceChain.resume prepared) destination rfl rfl (by omega) fits (pp.trans pointer)
  let out := run widthConstant ((finish cursor count).program w) 3 (SourceChain.resume appended)
  obtain ⟨oh, ot, op, on, ofr⟩ := finishes cursor count (SourceChain.resume appended) rfl rfl cursorBase distinct
  have tail := SourceChain.traces RecordAppend.algorithm.code (finish cursor count).code
    (SourceChain.resume prepared) appended out 8 3 rfl ah (trace_of_ticks _ _ 8 aticks) (trace_of_ticks _ _ 3 ot)
  have full := SourceChain.traces (prepare cursor count).code
    (SourceChain.code RecordAppend.algorithm.code (finish cursor count).code)
    s prepared _ 3 (8 + 3) live ph (trace_of_ticks _ _ 3 pt) tail
  refine ⟨(out.relocate RecordAppend.algorithm.code.length).relocate (prepare cursor count).code.length,
    full, oh, op.trans ap, ?_, ?_, ?_, ?_, ?_⟩
  · exact on.trans (an.trans (congrArg (fun v => v + 1#w.bits) pn))
  · exact (ofr destination (by omega) (by omega)).trans (a0.trans (pf 9 (by decide) (by decide)))
  · exact (ofr (destination + 1) (by omega) (by omega)).trans (a1.trans (pf 10 (by decide) (by decide)))
  · exact (ofr (destination + 2) (by omega) (by omega)).trans (a2.trans (pf 0 (by decide) (by decide)))
  · intro a ha hc hn h0 h1 h2
    exact (ofr a hc hn).trans ((af a (by omega) (by omega) h0 h1 h2).trans (pf a (by omega) (by omega)))

end WordRAM.Conjectures.Sparsification.BufferedAppend

/-! Emit an unchanged clause or its petal into a persistent branch buffer. -/
namespace WordRAM.Conjectures.Sparsification.BranchEmit

def output (petal : Bool) (core clause : Clause n) : Clause n :=
  if petal then Branch.petal core clause else clause

def recordAlgorithm (petal : Bool) : Algorithm :=
  if petal then
    ⟨SourceChain.code BranchLoad.algorithm.code PetalRecord.algorithm.code, 1, by decide⟩
  else BranchLoad.algorithm

def algorithm (petal : Bool) (cursor count : Nat) : Algorithm :=
  ⟨SourceChain.code (recordAlgorithm petal).code (BufferedAppend.algorithm cursor count).code, 1, by decide⟩

theorem builds_record (petal : Bool) (core clause : Clause n) (s : State w) (address : 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])) :
    ∃ final, Runs widthConstant ((recordAlgorithm petal).program w)
        (11 + if petal then 12 * w.bits + 23 else 0) s final ∧ final.halted = true ∧
      final.mem 9 = Masks.encode w (output petal core clause) true ∧
      final.mem 10 = Masks.encode w (output petal core clause) false ∧
      final.mem 0 = BitVec.ofNat w.bits (Normalize.clean (output petal core clause)).length ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨loaded, lt, lh, lp, ln, ls, lsp, lsn, lcp, lcn, lf⟩ :=
    BranchLoad.loads core clause s address pc live base fits pointer qp qn input
  cases petal with
  | false => exact ⟨loaded, lt, lh, lsp, lsn, ls, lf⟩
  | true =>
    obtain ⟨out, trace, halted, pos, neg, size, frame⟩ :=
      PetalRecord.builds core clause (SourceChain.resume loaded) rfl rfl variablesFit lp ln lcp lcn
    have full := SourceChain.traces BranchLoad.algorithm.code PetalRecord.algorithm.code s loaded out
      11 (12 * w.bits + 23) live lh lt trace
    refine ⟨out.relocate BranchLoad.algorithm.code.length, full, halted, pos, neg, size, ?_⟩
    intro a ha
    exact (frame a (by omega)).trans (lf a ha)

/-- The appended record is precisely `clause` or `Branch.petal core clause`.
The bound includes loads, petal construction when requested, stores, and both
persistent buffer controls. -/
theorem emits (petal : Bool) (core clause : Clause n) (s : State w)
    (address destination cursor count : 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]))
    (cursorBase : 16 ≤ cursor) (cursorEnd : cursor < 32)
    (countBase : 16 ≤ count) (countEnd : count < 32) (distinct : cursor ≠ count)
    (destinationBase : 32 ≤ destination) (destinationFits : destination + 2 < 2 ^ w.bits)
    (destinationPointer : s.mem cursor = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant ((algorithm petal cursor count).program w)
        (25 + if petal then 12 * w.bits + 23 else 0) s final ∧ final.halted = true ∧
      final.mem cursor = BitVec.ofNat w.bits (destination + 3) ∧
      final.mem count = s.mem count + 1#w.bits ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w [output petal core clause]) ∧
      (∀ a, 16 ≤ a → a ≠ cursor → a ≠ count → a ≠ destination →
        a ≠ destination + 1 → a ≠ destination + 2 → final.mem a = s.mem a) := by
  obtain ⟨record, rt, rh, rp, rn, rs, rf⟩ :=
    builds_record petal core clause s address pc live base fits variablesFit pointer qp qn input
  obtain ⟨out, trace, halted, outPointer, outCount, op, on, os, frame⟩ :=
    BufferedAppend.appends cursor count destination (SourceChain.resume record) rfl rfl
      cursorBase cursorEnd countBase countEnd distinct destinationBase destinationFits
      ((rf cursor cursorBase).trans destinationPointer)
  have full := SourceChain.traces (recordAlgorithm petal).code (BufferedAppend.algorithm cursor count).code
    s record out (11 + if petal then 12 * w.bits + 23 else 0) 14 live rh rt trace
  have cost : (11 + if petal then 12 * w.bits + 23 else 0) + 14 =
      25 + if petal then 12 * w.bits + 23 else 0 := by omega
  refine ⟨out.relocate (recordAlgorithm petal).code.length, ?_, halted, outPointer, ?_, ?_, ?_⟩
  · simpa only [algorithm, Algorithm.program, cost] using full
  · exact outCount.trans (congrArg (fun v => v + 1#w.bits) (rf count countBase))
  · exact ⟨op.trans rp, on.trans rn, os.trans rs, trivial⟩
  · intro a ha hc hn h0 h1 h2
    exact (frame a ha hc hn h0 h1 h2).trans (rf a ha)

end WordRAM.Conjectures.Sparsification.BranchEmit

/-! Eligibility test for one clause during branch-table construction. -/
namespace WordRAM.Conjectures.Sparsification.RecordMatches

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 1) (reg 20), .copy (.direct 2) (reg 21), .copy (.direct 8) (reg 22),
    .copy (.direct 11) (.immediate 1), .copy (.direct 12) (reg 23), .halt], 1, by decide⟩

def finish : Algorithm := ⟨[.copy (.direct 0) (reg 14), .halt], 1, by decide⟩

/-- Core masks 20,21; selected clause size 22; current record pointer 23.
Return whether the record belongs to the selected flower family in Boolean 0. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code FamilyScan.initialized.code finish.code), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 6 s
    t.halted = true ∧ t.ticks = s.ticks + 6 ∧ t.mem 1 = s.mem 20 ∧ t.mem 2 = s.mem 21 ∧
      t.mem 8 = s.mem 22 ∧ t.mem 11 = 1#w.bits ∧ t.mem 12 = s.mem 23 ∧
      (∀ a, 16 ≤ a → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a ha
  have neq : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 8 ∧ a ≠ 11 ∧ a ≠ 12 := by omega
  simp [neq]

theorem finishes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (finish.program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 0 = s.mem 14 ∧
      (∀ a, a ≠ 0 → t.mem a = s.mem a) := by
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h; simp [h]

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

/-- The test is exactly the predicate defining `Flowers.family`, with the
serialized record read from memory and all initialization included. -/
theorem classifies (core clause : Clause n) (size : Nat) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (fits : address + 3 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (nodup : clause.Nodup)
    (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)
    (pointer : s.mem 23 = BitVec.ofNat w.bits address)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w [clause])) :
    ∃ time final, time ≤ 30 ∧ Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if clause.length = size ∧ core ⊆ clause then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  let prepared := run widthConstant (prepare.program w) 6 s
  obtain ⟨preparedHalt, preparedTicks, pos, neg, starget, one, sp, pf⟩ := prepares s pc live
  have nextInput : VectorBuilder.Stored prepared.mem address (RecordTable.words w [clause]) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact pf a (by omega)
  obtain ⟨time, counted, bound, trace, countedHalt, countedValue, frame⟩ :=
    FamilyScan.counts_family core [clause] size (SourceChain.resume prepared) address rfl rfl base
      (by simpa using fits) variablesFit width sizeFits (by intro c h; simpa using (List.mem_singleton.mp h) ▸ nodup)
      (pos.trans qp) (neg.trans qn) (starget.trans target) (sp.trans pointer) one nextInput
  have numeric : (counted.mem 14).toNat = (if clause.length = size ∧ core ⊆ clause then 1 else 0) := by
    by_cases member : clause.length = size ∧ core ⊆ clause
    · simpa [Flowers.family, member] using countedValue
    · simpa [Flowers.family, member] using countedValue
  have word : counted.mem 14 = (if clause.length = size ∧ core ⊆ clause then 1#w.bits else 0#w.bits) := by
    apply BitVec.eq_of_toNat_eq
    rw [numeric]
    have oneFits : 1 < 2 ^ w.bits := by omega
    by_cases h : clause.length = size ∧ core ⊆ clause <;> simp [h, Nat.mod_eq_of_lt oneFits]
  let out := run widthConstant (finish.program w) 2 (SourceChain.resume counted)
  obtain ⟨halted, ticks, result, preserved⟩ := finishes (SourceChain.resume counted) rfl rfl
  have tail := SourceChain.traces FamilyScan.initialized.code finish.code (SourceChain.resume prepared) counted out
    time 2 rfl countedHalt trace (trace_of_ticks _ _ 2 ticks)
  have full := SourceChain.traces prepare.code (SourceChain.code FamilyScan.initialized.code finish.code)
    s prepared _ 6 (time + 2) live preparedHalt (trace_of_ticks _ s 6 preparedTicks) tail
  refine ⟨6 + (time + 2), (out.relocate FamilyScan.initialized.code.length).relocate prepare.code.length,
    by simp only [List.length_cons, List.length_nil] at bound; omega, full, halted, result.trans word, ?_⟩
  intro a ha
  exact (preserved a (by omega)).trans ((frame a ha).trans (pf a ha))

end WordRAM.Conjectures.Sparsification.RecordMatches