SETH ⇒ OVC sparsification bundle 21: 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_20

set_option autoImplicit true

/-! Filtering clause-record tables using actual wordRAM instructions. -/
namespace WordRAM.Conjectures.Sparsification.RecordFilter

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

def setupPrefix : List SourceInstruction :=
  [.branch .eq (reg 11) (.immediate 0) 27,
   .copy (.direct 3) (.memory (.indirect 12)),
   .binary .add (.direct 12) (reg 12) (.immediate 1),
   .copy (.direct 4) (.memory (.indirect 12)),
   .binary .add (.direct 12) (reg 12) (.immediate 1),
   .copy (.direct 7) (.memory (.indirect 12)),
   .binary .add (.direct 12) (reg 12) (.immediate 1)]

def epilogue : List SourceInstruction :=
  [.branch .eq (reg 0) (.immediate 1) 25,
   .copy (.indirect 13) (reg 3),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .copy (.indirect 13) (reg 4),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .copy (.indirect 13) (reg 7),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .binary .add (.direct 14) (reg 14) (.immediate 1),
   .binary .sub (.direct 11) (reg 11) (.immediate 1),
   .jump 0, .halt]

/-- Remove all records containing the query clause. Query masks: 1,2;
input count: 11; input cursor: 12; output cursor: 13; output count: 14. -/
def algorithm : Algorithm :=
  ⟨setupPrefix ++ (SubsetMachine.algorithm.code.map (SourceInstruction.returnTo 10)).map
    (SourceInstruction.relocate 7) ++ epilogue, 1, by decide⟩

private theorem program_eq (w : Width) : algorithm.program w =
    setupPrefix.map (SourceInstruction.compile w) ++
    (((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10)).map (Instruction.relocate 7) ++
      epilogue.map (SourceInstruction.compile w)) := rfl

theorem enters (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 11 ≠ 0#w.bits) (base : 16 ≤ address)
    (fits : address + 2 < 2 ^ w.bits) (pointer : s.mem 12 = BitVec.ofNat w.bits address) :
    let t := run widthConstant (algorithm.program w) 7 s
    t.pc = 7 ∧ t.halted = false ∧ t.ticks = s.ticks + 7 ∧
      t.mem 3 = s.mem address ∧ t.mem 4 = s.mem (address + 1) ∧ t.mem 7 = s.mem (address + 2) ∧
      t.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
      (∀ a, a ≠ 3 → a ≠ 4 → a ≠ 7 → a ≠ 12 → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits address).toNat = address := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits address + 1#w.bits).toNat = address + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt (by omega)
  have d2 : (BitVec.ofNat w.bits address + 1#w.bits + 1#w.bits).toNat = address + 2 := by
    rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low1 : ∀ i, i ≤ 15 → address + 1 ≠ i := by omega
  have low2 : ∀ i, i ≤ 15 → address + 2 ≠ i := by omega
  rw [program_eq]
  simp [setupPrefix, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, nonzero,
    pointer, d0, d1, d2, low1, low2, Nat.add_assoc, -BitVec.toNat_add,
    List.getElem?_cons_zero, List.getElem?_cons_succ]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h3 h4 h7 h12; simp [h3, h4, h7, h12]

theorem drops (s : State w) (pc : s.pc = 17) (live : s.halted = false) (yes : s.mem 0 = 1#w.bits) :
    let t := run widthConstant (algorithm.program w) 3 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 3 ∧
      t.mem 11 = s.mem 11 - 1#w.bits ∧ (∀ a, a ≠ 11 → t.mem a = s.mem a) := by
  simp [algorithm, setupPrefix, epilogue, SubsetMachine.algorithm, Algorithm.program, SourceInstruction.compile,
    SourceInstruction.returnTo, SourceInstruction.relocate, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, yes, Nat.add_assoc]
  intro a h; simp [h]

theorem keeps (s : State w) (destination : Nat) (pc : s.pc = 17) (live : s.halted = false)
    (no : s.mem 0 ≠ 1#w.bits) (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) 10 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 10 ∧
      t.mem 11 = s.mem 11 - 1#w.bits ∧ t.mem 14 = s.mem 14 + 1#w.bits ∧ t.mem 13 = BitVec.ofNat w.bits (destination + 3) ∧
      t.mem destination = s.mem 3 ∧ t.mem (destination + 1) = s.mem 4 ∧ t.mem (destination + 2) = s.mem 7 ∧
      (∀ a, a ≠ 11 → 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, setupPrefix, epilogue, SubsetMachine.algorithm, Algorithm.program, SourceInstruction.compile,
    SourceInstruction.returnTo, SourceInstruction.relocate, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, no,
    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 h11 h13 h14 h0 h1 h2; simp [h11, h13, h14, h0, h1, h2]

theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false) (empty : s.mem 11 = 0#w.bits) :
    let t := run widthConstant (algorithm.program w) 2 s
    t.halted = true ∧ t.mem = s.mem ∧ t.ticks = s.ticks + 2 := by
  simp [algorithm, setupPrefix, epilogue, SubsetMachine.algorithm, Algorithm.program, SourceInstruction.compile,
    SourceInstruction.returnTo, SourceInstruction.relocate, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Comparison.test, pc, live, empty, Nat.add_assoc]

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

/-- Load and compare one complete record, linking the verified subset routine. -/
theorem compares (query clause : Clause n) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 11 ≠ 0#w.bits)
    (base : 16 ≤ address) (fits : address + 2 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (qp : s.mem 1 = Masks.encode w query true) (qn : s.mem 2 = Masks.encode w query false)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (positive : s.mem address = Masks.encode w clause true)
    (negative : s.mem (address + 1) = Masks.encode w clause false)
    (size : s.mem (address + 2) = BitVec.ofNat w.bits (Normalize.clean clause).length) :
    ∃ time final, time ≤ 13 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.pc = 17 ∧ final.halted = false ∧
      final.mem 0 = (if query ⊆ clause then 1#w.bits else 0#w.bits) ∧
      final.mem 3 = Masks.encode w clause true ∧ final.mem 4 = Masks.encode w clause false ∧
      final.mem 7 = BitVec.ofNat w.bits (Normalize.clean clause).length ∧
      final.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
      (∀ a, a ≠ 0 → a ≠ 3 → a ≠ 4 → a ≠ 5 → a ≠ 6 → a ≠ 7 → a ≠ 12 → final.mem a = s.mem a) := by
  let head := run widthConstant (algorithm.program w) 7 s
  obtain ⟨hpc, hlive, hticks, hp, hn, hsize, hnext, hf⟩ := enters s address pc live nonzero base fits pointer
  let entry : State w := { head with pc := 0 }
  have entryLive : entry.halted = false := hlive
  obtain ⟨time, bound, trace, halted, result⟩ :=
    SubsetMachine.decides_subset query clause variablesFit entry rfl entryLive
      ((hf 1 (by decide) (by decide) (by decide) (by decide)).trans qp)
      ((hf 2 (by decide) (by decide) (by decide) (by decide)).trans qn)
      (hp.trans positive) (hn.trans negative)
  have embedded : EmbedsAt ((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10))
      (algorithm.program w) 7 := by
    rw [program_eq]
    exact embeds_append (setupPrefix.map (SourceInstruction.compile w))
      ((SubsetMachine.algorithm.program w).map (Instruction.returnTo 10))
      (epilogue.map (SourceInstruction.compile w))
  let returned := ((SubsetMachine.result entry).returnTo 10).relocate 7
  have linked : Runs widthConstant (algorithm.program w) time head returned := by
    have h := (trace.returnTo 10).relocate embedded
    have he : (entry.returnTo 10).relocate 7 = head := by
      simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
      change { head with pc := 7 } = head
      have hpc' : head.pc = 7 := hpc
      rw [← hpc']
    simpa only [he] using h
  have rf : ∀ a, a ≠ 0 → a ≠ 5 → a ≠ 6 → returned.mem a = entry.mem a := by
    intro a h0 h5 h6
    simpa [returned, State.returnTo, State.relocate, halted] using SubsetMachine.frame entry rfl entryLive a h0 h5 h6
  refine ⟨7 + time, returned, by omega, (trace_of_ticks s 7 hticks).append linked, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · simp [returned, State.returnTo, State.relocate, halted]
  · simp [returned, State.returnTo, State.relocate, halted]
  · simpa [returned, State.returnTo, State.relocate, halted] using result
  · exact (rf 3 (by decide) (by decide) (by decide)).trans (hp.trans positive)
  · exact (rf 4 (by decide) (by decide) (by decide)).trans (hn.trans negative)
  · exact (rf 7 (by decide) (by decide) (by decide)).trans (hsize.trans size)
  · exact (rf 12 (by decide) (by decide) (by decide)).trans hnext
  · intro a h0 h3 h4 h5 h6 h7 h12
    exact (rf a h0 h5 h6).trans (hf a h3 h4 h7 h12)

/-- One complete filtering iteration. Zero or three output words are written. -/
theorem iteration (query clause : Clause n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 11 ≠ 0#w.bits)
    (base : 16 ≤ address) (outputBase : 16 ≤ destination)
    (fits : address + 2 < 2 ^ w.bits) (outputFits : destination + 2 < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (qp : s.mem 1 = Masks.encode w query true) (qn : s.mem 2 = Masks.encode w query false)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (positive : s.mem address = Masks.encode w clause true)
    (negative : s.mem (address + 1) = Masks.encode w clause false)
    (size : s.mem (address + 2) = BitVec.ofNat w.bits (Normalize.clean clause).length) :
    let advance := if query ⊆ clause then 0 else 3
    ∃ time final, time ≤ 23 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.pc = 0 ∧ final.halted = false ∧
      final.mem 1 = Masks.encode w query true ∧ final.mem 2 = Masks.encode w query false ∧
      final.mem 11 = s.mem 11 - 1#w.bits ∧
      final.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + advance) ∧
      final.mem 14 = s.mem 14 + (if query ⊆ clause then 0#w.bits else 1#w.bits) ∧
      (¬ query ⊆ clause → final.mem destination = Masks.encode w clause true ∧
        final.mem (destination + 1) = Masks.encode w clause false ∧
        final.mem (destination + 2) = BitVec.ofNat w.bits (Normalize.clean clause).length) ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + advance ≤ a) → final.mem a = s.mem a) := by
  obtain ⟨time, middle, bound, trace, mpc, mlive, result, pos, neg, len, next, frame⟩ :=
    compares query clause s address pc live nonzero base fits variablesFit qp qn pointer positive negative size
  have mq : middle.mem 1 = Masks.encode w query true :=
    (frame 1 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qp
  have mn : middle.mem 2 = Masks.encode w query false :=
    (frame 2 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qn
  have mc : middle.mem 11 = s.mem 11 := frame 11 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)
  have md : middle.mem 13 = BitVec.ofNat w.bits destination :=
    (frame 13 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans outputPointer
  have mout : middle.mem 14 = s.mem 14 := frame 14 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)
  by_cases subset : query ⊆ clause
  · simp only [if_pos subset, Nat.add_zero]
    have yes : middle.mem 0 = 1#w.bits := by simpa only [if_pos subset] using result
    obtain ⟨fpc, flive, ticks, count, ff⟩ := drops middle mpc mlive yes
    refine ⟨time + 3, run widthConstant (algorithm.program w) 3 middle, by omega,
      trace.append (trace_of_ticks middle 3 ticks), fpc, flive,
      (ff 1 (by decide)).trans mq, (ff 2 (by decide)).trans mn, ?_,
      (ff 12 (by decide)).trans next, (ff 13 (by decide)).trans md, ?_, ?_, ?_⟩
    · simpa only [mc] using count
    · simpa only [BitVec.add_zero] using (ff 14 (by decide)).trans mout
    · intro no; exact False.elim (no subset)
    · intro a ha _
      exact (ff a (by omega)).trans (frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega))
  · simp only [if_neg subset]
    have no : middle.mem 0 ≠ 1#w.bits := by
      rw [result, if_neg subset]
      intro eq
      have values := congrArg BitVec.toNat eq
      have oneFits : 1 < 2 ^ w.bits := by omega
      simp [Nat.mod_eq_of_lt oneFits] at values
    obtain ⟨fpc, flive, ticks, count, outCount, dest, fpos, fneg, fsize, ff⟩ :=
      keeps middle destination mpc mlive no outputBase outputFits md
    refine ⟨time + 10, run widthConstant (algorithm.program w) 10 middle, by omega,
      trace.append (trace_of_ticks middle 10 ticks), fpc, flive, ?_, ?_, ?_, ?_, dest, ?_, ?_, ?_⟩
    · exact (ff 1 (by decide) (by decide) (by decide) (by omega) (by omega) (by omega)).trans mq
    · exact (ff 2 (by decide) (by decide) (by decide) (by omega) (by omega) (by omega)).trans mn
    · simpa only [mc] using count
    · exact (ff 12 (by decide) (by decide) (by decide) (by omega) (by omega) (by omega)).trans next
    · simpa only [mout] using outCount
    · intro _; exact ⟨fpos.trans pos, fneg.trans neg, fsize.trans len⟩
    · intro a ha outside
      exact (ff a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
        (frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega))

private theorem stored_frame (xs : List (Word w)) (address : Nat)
    (input : VectorBuilder.Stored mem address xs)
    (frame : ∀ a, address ≤ a → a < address + xs.length → other a = mem a) :
    VectorBuilder.Stored other address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    refine ⟨(frame address (by omega) (by simp)).trans input.1, ?_⟩
    apply ih (address + 1) input.2
    intro a lo hi
    apply frame a (by omega)
    simp only [List.length_cons]; omega

/-- The complete stable filter, with explicit disjoint buffers and all costs.
The output count is added to cell 14, so initialization can be composed separately. -/
theorem builds (query : Clause n) (clauses : CNF n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address) (outputBase : 16 ≤ destination)
    (separate : destination + 3 * clauses.length ≤ address ∨ address + 3 * clauses.length ≤ destination)
    (inputFits : address + 3 * clauses.length < 2 ^ w.bits)
    (outputFits : destination + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (qp : s.mem 1 = Masks.encode w query true) (qn : s.mem 2 = Masks.encode w query false)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    let filtered := clauses.filter (fun larger => !decide (query ⊆ larger))
    ∃ time final, time ≤ 23 * clauses.length + 2 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (RecordTable.words w filtered) ∧
      final.mem 1 = Masks.encode w query true ∧ final.mem 2 = Masks.encode w query false ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + 3 * filtered.length) ∧
      final.mem 14 = s.mem 14 + BitVec.ofNat w.bits filtered.length ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 * clauses.length ≤ a) → final.mem a = s.mem a) := by
  induction clauses generalizing s address destination with
  | nil =>
    have empty : s.mem 11 = 0#w.bits := by simpa using remaining
    obtain ⟨halted, mem, ticks⟩ := exits s pc live empty
    refine ⟨2, run widthConstant (algorithm.program w) 2 s, by simp, trace_of_ticks s 2 ticks,
      halted, trivial, (congrFun mem 1).trans qp, (congrFun mem 2).trans qn, ?_, ?_, ?_⟩
    · simpa using (congrFun mem 13).trans outputPointer
    · simpa using congrFun mem 14
    · intro a _ _; exact congrFun mem a
  | cons clause rest ih =>
    have countFits : rest.length + 1 < 2 ^ w.bits := by
      simp only [List.length_cons] at inputFits
      omega
    have nonzero : s.mem 11 ≠ 0#w.bits := by
      intro h
      have hn := congrArg BitVec.toNat h
      simp [remaining, Nat.mod_eq_of_lt countFits] at hn
    obtain ⟨stepTime, next, stepBound, stepTrace, npc, nlive, nqp, nqn, nc, np, nd, nout, record, frame⟩ :=
      iteration query clause s address destination pc live nonzero base outputBase
        (by simp only [List.length_cons] at inputFits; omega)
        (by simp only [List.length_cons] at outputFits; omega)
        variablesFit qp qn pointer outputPointer input.1 input.2.1 input.2.2.1
    let advance := if query ⊆ clause then 0 else 3
    have advanceBound : advance ≤ 3 := by unfold advance; split <;> omega
    have count : next.mem 11 = BitVec.ofNat w.bits rest.length := by
      rw [nc, remaining]
      change BitVec.ofNat w.bits (rest.length + 1) - BitVec.ofNat w.bits 1 = _
      rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
      simp
    have nextInput : VectorBuilder.Stored next.mem (address + 3) (RecordTable.words w rest) := by
      apply stored_frame _ _ input.2.2.2
      intro a lo hi
      apply frame a (by omega)
      rw [RecordTable.words_length] at hi
      simp only [List.length_cons] at separate
      change a < destination ∨ destination + advance ≤ a
      omega
    obtain ⟨time, final, bound, trace, halted, table, fqp, fqn, dest, total, preserved⟩ :=
      ih next (address + 3) (destination + advance) npc nlive (by omega) (by omega)
        (by simp only [List.length_cons] at separate; omega)
        (by simp only [List.length_cons] at inputFits; omega)
        (by simp only [List.length_cons] at outputFits; omega)
        nqp nqn np nd count nextInput
    refine ⟨stepTime + time, final, ?_, stepTrace.append trace, halted, ?_, fqp, fqn, ?_, ?_, ?_⟩
    · simp only [List.length_cons]; omega
    · by_cases subset : query ⊆ clause
      · simpa [subset, advance] using table
      · obtain ⟨positive, negative, size⟩ := record subset
        simp only [List.filter_cons, subset, decide_false, Bool.not_false, ↓reduceIte]
        refine ⟨?_, ?_, ?_, ?_⟩
        · exact (preserved destination (by omega) (by simp [advance, subset])).trans positive
        · exact (preserved (destination + 1) (by omega) (by simp [advance, subset])).trans negative
        · exact (preserved (destination + 2) (by omega) (by simp [advance, subset])).trans size
        · simpa [advance, subset] using table
    · by_cases subset : query ⊆ clause
      · simpa [subset, advance] using dest
      · simpa [subset, advance, Nat.mul_add, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using dest
    · rw [total, nout]
      by_cases subset : query ⊆ clause
      · simp [subset]
      · simp only [List.filter_cons, subset, decide_false, Bool.not_false, ↓reduceIte, List.length_cons, BitVec.add_assoc]
        rw [← BitVec.ofNat_add]
        congr 2
        omega
    · intro a ha outside
      simp only [List.length_cons] at outside
      exact (preserved a ha (by omega)).trans (frame a ha (by change a < destination ∨ destination + advance ≤ a; omega))

end WordRAM.Conjectures.Sparsification.RecordFilter

/-! A source-level conditional with explicit one-instruction dispatch cost. -/
namespace WordRAM.Conjectures.SourceIf

/-- Execute `zero` if the selected word is zero, otherwise `nonzero`.
Both bodies retain their terminal halts. -/
def code (cell : Nat) (zero nonzero : List SourceInstruction) : List SourceInstruction :=
  [.branch .eq (.memory (.direct cell)) (.immediate 0) (1 + nonzero.length)] ++
    nonzero.map (SourceInstruction.relocate 1) ++
    zero.map (SourceInstruction.relocate (1 + nonzero.length))

private theorem nonzero_embedded (cell : Nat) (zero nonzero : List SourceInstruction) (w : Width) :
    EmbedsAt (nonzero.map (SourceInstruction.compile w)) ((code cell zero nonzero).map (SourceInstruction.compile w)) 1 := by
  have h := embeds_append
    ([SourceInstruction.branch .eq (.memory (.direct cell)) (.immediate 0) (1 + nonzero.length)].map (SourceInstruction.compile w))
    (nonzero.map (SourceInstruction.compile w))
    ((zero.map (SourceInstruction.relocate (1 + nonzero.length))).map (SourceInstruction.compile w))
  simpa [code, List.map_map, Function.comp_def, compile_relocate, List.append_assoc, Nat.add_comm] using h

private theorem zero_embedded (cell : Nat) (zero nonzero : List SourceInstruction) (w : Width) :
    EmbedsAt (zero.map (SourceInstruction.compile w)) ((code cell zero nonzero).map (SourceInstruction.compile w)) (1 + nonzero.length) := by
  have h := embeds_append
    (([SourceInstruction.branch .eq (.memory (.direct cell)) (.immediate 0) (1 + nonzero.length)] ++
      nonzero.map (SourceInstruction.relocate 1)).map (SourceInstruction.compile w))
    (zero.map (SourceInstruction.compile w)) []
  simpa [code, List.map_map, Function.comp_def, compile_relocate, List.append_assoc, Nat.add_comm] using h

theorem nonzero_trace (cell : Nat) (zero nonzero : List SourceInstruction) (s final : State w) (time : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (test : s.mem cell ≠ 0#w.bits)
    (body : Runs widthConstant (nonzero.map (SourceInstruction.compile w)) time (s.addTicks 1) final) :
    Runs widthConstant ((code cell zero nonzero).map (SourceInstruction.compile w)) (1 + time) s (final.relocate 1) := by
  have fetch : ((code cell zero nonzero).map (SourceInstruction.compile w))[s.pc]? =
      some (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (1 + nonzero.length)) := by
    simp [pc, code, SourceInstruction.compile, SourceOperand.compile]
  have head := runs_instruction widthConstant ((code cell zero nonzero).map (SourceInstruction.compile w)) s _ live fetch
  have next : execute (m := .multiplication) widthConstant
      (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (1 + nonzero.length)) s =
      (s.addTicks 1).relocate 1 := by
    simp [execute, Comparison.test, Operand.read, Address.resolve, test, State.addTicks, State.relocate, pc, Nat.add_comm]
  rw [next] at head
  exact head.append (body.relocate (nonzero_embedded cell zero nonzero w))

theorem zero_trace (cell : Nat) (zero nonzero : List SourceInstruction) (s final : State w) (time : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (test : s.mem cell = 0#w.bits)
    (body : Runs widthConstant (zero.map (SourceInstruction.compile w)) time (s.addTicks 1) final) :
    Runs widthConstant ((code cell zero nonzero).map (SourceInstruction.compile w)) (1 + time) s
      (final.relocate (1 + nonzero.length)) := by
  have fetch : ((code cell zero nonzero).map (SourceInstruction.compile w))[s.pc]? =
      some (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (1 + nonzero.length)) := by
    simp [pc, code, SourceInstruction.compile, SourceOperand.compile]
  have head := runs_instruction widthConstant ((code cell zero nonzero).map (SourceInstruction.compile w)) s _ live fetch
  have next : execute (m := .multiplication) widthConstant
      (.branch .eq (.memory (.direct cell)) (.immediate (0#w.bits)) (1 + nonzero.length)) s =
      (s.addTicks 1).relocate (1 + nonzero.length) := by
    simp [execute, Comparison.test, Operand.read, Address.resolve, test, State.addTicks, State.relocate, pc, Nat.add_comm]
  rw [next] at head
  exact head.append (body.relocate (zero_embedded cell zero nonzero w))

end WordRAM.Conjectures.SourceIf