SETH ⇒ OVC sparsification bundle 23: 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_22

set_option autoImplicit true

/-! Repeated insertion, scanning the original clause table from right to left. -/
namespace WordRAM.Conjectures.Sparsification.NormalizeMachine

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

def setupPrefix : List SourceInstruction :=
  [.branch .eq (reg 20) (.immediate 0) 89,
   .binary .sub (.direct 21) (reg 21) (.immediate 3),
   .copy (.direct 1) (.memory (.indirect 21)),
   .binary .add (.direct 23) (reg 21) (.immediate 1),
   .copy (.direct 2) (.memory (.indirect 23)),
   .binary .add (.direct 23) (reg 23) (.immediate 1),
   .copy (.direct 7) (.memory (.indirect 23)),
   .copy (.direct 11) (reg 24),
   .copy (.direct 12) (reg 22),
   .copy (.direct 13) (reg 18)]

def epilogue : List SourceInstruction :=
  [.copy (.direct 24) (reg 14),
   .copy (.direct 22) (reg 18),
   .binary .add (.direct 18) (reg 18) (reg 19),
   .binary .sub (.direct 20) (reg 20) (.immediate 1),
   .jump 0, .halt]

/-- Cells 18=next output buffer, 19=buffer stride, 20=pending clause count,
21=one-past input cursor, 22=current result table, 24=current result count.
Cells 0..24 are scratch/control; all clause data start at or above 32. -/
def algorithm : Algorithm :=
  ⟨setupPrefix ++ (InsertMachine.algorithm.code.map (SourceInstruction.returnTo 74)).map
    (SourceInstruction.relocate 10) ++ epilogue, 1, by decide⟩

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

theorem enters (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 20 ≠ 0#w.bits) (base : 32 ≤ address)
    (fits : address + 3 < 2 ^ w.bits) (pointer : s.mem 21 = BitVec.ofNat w.bits (address + 3)) :
    let t := run widthConstant (algorithm.program w) 10 s
    t.pc = 10 ∧ t.halted = false ∧ t.ticks = s.ticks + 10 ∧
      t.mem 1 = s.mem address ∧ t.mem 2 = s.mem (address + 1) ∧ t.mem 7 = s.mem (address + 2) ∧
      t.mem 11 = s.mem 24 ∧ t.mem 12 = s.mem 22 ∧ t.mem 13 = s.mem 18 ∧
      t.mem 21 = BitVec.ofNat w.bits address ∧
      (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 7 → a ≠ 11 → a ≠ 12 → a ≠ 13 → a ≠ 21 → a ≠ 23 → t.mem a = s.mem a) := by
  have sub : BitVec.ofNat w.bits (address + 3) - 3#w.bits = BitVec.ofNat w.bits address := by
    rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]; simp
  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 (by omega)
  have low0 : ∀ i, i ≤ 24 → address ≠ i := by omega
  have low1 : ∀ i, i ≤ 24 → address + 1 ≠ i := by omega
  have low2 : ∀ i, i ≤ 24 → 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,
    sub, d0, d1, d2, low0, low1, low2, Nat.add_assoc, -BitVec.toNat_add,
    List.getElem?_cons_zero, List.getElem?_cons_succ]
  intro a h1 h2 h7 h11 h12 h13 h21 h23; simp [h1, h2, h7, h11, h12, h13, h21, h23]

theorem leaves (s : State w) (pc : s.pc = 84) (live : s.halted = false) :
    let t := run widthConstant (algorithm.program w) 5 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 5 ∧
      t.mem 24 = s.mem 14 ∧ t.mem 22 = s.mem 18 ∧ t.mem 18 = s.mem 18 + s.mem 19 ∧
      t.mem 20 = s.mem 20 - 1#w.bits ∧
      (∀ a, a ≠ 24 → a ≠ 22 → a ≠ 18 → a ≠ 20 → t.mem a = s.mem a) := by
  have f84 : (algorithm.program w)[84]? = some (.copy (.direct 24) (.memory (.direct 14))) := rfl
  have f85 : (algorithm.program w)[85]? = some (.copy (.direct 22) (.memory (.direct 18))) := rfl
  have f86 : (algorithm.program w)[86]? = some (.binary .add (.direct 18) (.memory (.direct 18)) (.memory (.direct 19))) := rfl
  have f87 : (algorithm.program w)[87]? = some (.binary .sub (.direct 20) (.memory (.direct 20)) (.immediate 1)) := rfl
  have f88 : (algorithm.program w)[88]? = some (.jump 0) := rfl
  simp [run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live,
    f84, f85, f86, f87, f88, Nat.add_assoc]
  intro a h24 h22 h18 h20; simp [h24, h22, h18, h20]

theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false) (empty : s.mem 20 = 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
  have f0 : (algorithm.program w)[0]? = some (.branch .eq (.memory (.direct 20)) (.immediate 0) 89) := rfl
  have f89 : (algorithm.program w)[89]? = some .halt := rfl
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, empty, f0, f89, 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

/-- Process one clause from the right end of the pending input. -/
theorem iteration (query : Clause n) (clauses : CNF n) (s : State w)
    (queryAddress address destination stride : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 20 ≠ 0#w.bits)
    (queryBase : 32 ≤ queryAddress) (base : 32 ≤ address)
    (queryFits : queryAddress + 3 < 2 ^ w.bits)
    (separate : address + 3 * clauses.length ≤ destination)
    (fits : destination + 3 * (clauses.length + 1) < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 21 = BitVec.ofNat w.bits (queryAddress + 3))
    (tablePointer : s.mem 22 = BitVec.ofNat w.bits address)
    (count : s.mem 24 = BitVec.ofNat w.bits clauses.length)
    (outputPointer : s.mem 18 = BitVec.ofNat w.bits destination)
    (stepSize : s.mem 19 = BitVec.ofNat w.bits stride)
    (positive : s.mem queryAddress = Masks.encode w query true)
    (negative : s.mem (queryAddress + 1) = Masks.encode w query false)
    (size : s.mem (queryAddress + 2) = BitVec.ofNat w.bits (Normalize.clean query).length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 35 * clauses.length + 34 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.pc = 0 ∧ final.halted = false ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w (Normalize.insert query clauses)) ∧
      final.mem 24 = BitVec.ofNat w.bits (Normalize.insert query clauses).length ∧
      final.mem 22 = BitVec.ofNat w.bits destination ∧
      final.mem 18 = BitVec.ofNat w.bits (destination + stride) ∧
      final.mem 19 = BitVec.ofNat w.bits stride ∧ final.mem 20 = s.mem 20 - 1#w.bits ∧
      final.mem 21 = BitVec.ofNat w.bits queryAddress ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + 3 * (clauses.length + 1) ≤ a) → final.mem a = s.mem a) := by
  let head := run widthConstant (algorithm.program w) 10 s
  obtain ⟨hpc, hlive, hticks, hp, hn, hsize, hc, hi, hd, hquery, hf⟩ :=
    enters s queryAddress pc live nonzero queryBase queryFits pointer
  let entry : State w := { head with pc := 0 }
  have entryLive : entry.halted = false := hlive
  have entryInput : VectorBuilder.Stored entry.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _
    exact hf a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)
  obtain ⟨time, built, bound, trace, halted, table, resultCount, bf⟩ :=
    InsertMachine.inserts query clauses entry address destination rfl entryLive (by omega) separate fits variablesFit
      (hp.trans positive) (hn.trans negative) (hsize.trans size) (hc.trans count)
      (hi.trans tablePointer) (hd.trans outputPointer) entryInput
  have embedded : EmbedsAt ((InsertMachine.algorithm.program w).map (Instruction.returnTo 74))
      (algorithm.program w) 10 := by
    rw [program_eq]
    exact embeds_append (setupPrefix.map (SourceInstruction.compile w))
      ((InsertMachine.algorithm.program w).map (Instruction.returnTo 74))
      (epilogue.map (SourceInstruction.compile w))
  let returned := (built.returnTo 74).relocate 10
  have linked : Runs widthConstant (algorithm.program w) time head returned := by
    have h := (trace.returnTo 74).relocate embedded
    have he : (entry.returnTo 74).relocate 10 = head := by
      simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
      change { head with pc := 10 } = head
      have hpc' : head.pc = 10 := hpc
      rw [← hpc']
    simpa only [he] using h
  have retPC : returned.pc = 84 := by simp [returned, State.returnTo, State.relocate, halted]
  have retLive : returned.halted = false := by simp [returned, State.returnTo, State.relocate, halted]
  have rf : ∀ a, 16 ≤ a → a < 32 → returned.mem a = entry.mem a := by
    intro a lo hi
    simpa [returned, State.returnTo, State.relocate, halted] using bf a lo (Or.inl (by omega))
  have rd : returned.mem 18 = BitVec.ofNat w.bits destination := by
    rw [rf 18 (by decide) (by decide)]
    exact (hf 18 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans outputPointer
  have rs : returned.mem 19 = BitVec.ofNat w.bits stride := by
    rw [rf 19 (by decide) (by decide)]
    exact (hf 19 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans stepSize
  have rc : returned.mem 20 = s.mem 20 := by
    rw [rf 20 (by decide) (by decide)]
    exact hf 20 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)
  have rq : returned.mem 21 = BitVec.ofNat w.bits queryAddress :=
    (rf 21 (by decide) (by decide)).trans hquery
  obtain ⟨fpc, flive, fticks, fc, fa, fd, fn, ff⟩ := leaves returned retPC retLive
  let final := run widthConstant (algorithm.program w) 5 returned
  refine ⟨10 + time + 5, final, by omega,
    ((trace_of_ticks s 10 hticks).append linked).append (trace_of_ticks returned 5 fticks),
    fpc, flive, ?_, ?_, fa.trans rd, ?_, ?_, ?_, ?_, ?_⟩
  · apply MemoryCopy.stored_frame _ _ table
    intro a lo _
    have same := ff a (by omega) (by omega) (by omega) (by omega)
    simpa [final, returned, State.returnTo, State.relocate, halted] using same
  · simpa [final, returned, State.returnTo, State.relocate, halted, resultCount] using fc
  · rw [fd, rd, rs, ← BitVec.ofNat_add]
  · exact (ff 19 (by decide) (by decide) (by decide) (by decide)).trans rs
  · simpa only [rc] using fn
  · exact (ff 21 (by decide) (by decide) (by decide) (by decide)).trans rq
  · intro a ha outside
    have preserved : returned.mem a = entry.mem a := by
      simpa [returned, State.returnTo, State.relocate, halted] using bf a (by omega) outside
    exact (ff a (by omega) (by omega) (by omega) (by omega)).trans
      (preserved.trans (hf a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)))

/-- Insert the pending clauses in precisely the order used by `minimize`. -/
def reduce : CNF n → CNF n → CNF n
  | [], accumulated => accumulated
  | clause :: rest, accumulated => Normalize.insert clause (reduce rest accumulated)

theorem reduce_snoc (pending : CNF n) (query : Clause n) (accumulated : CNF n) :
    reduce (pending ++ [query]) accumulated = reduce pending (Normalize.insert query accumulated) := by
  induction pending with
  | nil => rfl
  | cons clause rest ih => simp only [List.cons_append, reduce, ih]

theorem reduce_nil (pending : CNF n) : reduce pending [] = Normalize.minimize pending := by
  induction pending with
  | nil => rfl
  | cons clause rest ih => simp only [reduce, Normalize.minimize, ih]

private 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]

private theorem stored_append (left right : List (Word 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]

private theorem reverse_induction {α : Type} {motive : List α → Prop} (xs : List α)
    (nil : motive []) (append_singleton : ∀ xs x, motive xs → motive (xs ++ [x])) : motive xs := by
  have all : ∀ ys : List α, motive ys.reverse := by
    intro ys
    induction ys with
    | nil => exact nil
    | cons x ys ih => simpa only [List.reverse_cons] using append_singleton ys.reverse x ih
  simpa only [List.reverse_reverse] using all xs.reverse

/-- Full repeated-insertion loop. Buffers have a fixed stride large enough for
any intermediate table. The explicit address bound includes every allocated
buffer, and the time bound is quadratic when capacity is the input length. -/
theorem reduces (pending accumulated : CNF n) (capacity : Nat) (s : State w)
    (source address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (sourceBase : 32 ≤ source) (base : 32 ≤ address)
    (capacityBound : pending.length + accumulated.length ≤ capacity)
    (inputBefore : source + 3 * pending.length ≤ address)
    (separate : address + 3 * accumulated.length ≤ destination)
    (fits : destination + pending.length * (3 * (capacity + 1)) < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (remaining : s.mem 20 = BitVec.ofNat w.bits pending.length)
    (cursor : s.mem 21 = BitVec.ofNat w.bits (source + 3 * pending.length))
    (pointer : s.mem 22 = BitVec.ofNat w.bits address)
    (count : s.mem 24 = BitVec.ofNat w.bits accumulated.length)
    (outputPointer : s.mem 18 = BitVec.ofNat w.bits destination)
    (stride : s.mem 19 = BitVec.ofNat w.bits (3 * (capacity + 1)))
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w pending))
    (table : VectorBuilder.Stored s.mem address (RecordTable.words w accumulated)) :
    ∃ time final resultAddress,
      time ≤ pending.length * (35 * capacity + 34) + 2 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.halted = true ∧
      VectorBuilder.Stored final.mem resultAddress (RecordTable.words w (reduce pending accumulated)) ∧
      final.mem 22 = BitVec.ofNat w.bits resultAddress ∧ final.mem 24 = BitVec.ofNat w.bits (reduce pending accumulated).length ∧
      address ≤ resultAddress ∧ resultAddress + 3 * (reduce pending accumulated).length ≤ destination + pending.length * (3 * (capacity + 1)) ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + pending.length * (3 * (capacity + 1)) ≤ a) → final.mem a = s.mem a) := by
  induction pending using reverse_induction generalizing accumulated s address destination with
  | nil =>
    have empty : s.mem 20 = 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, address, by simp,
      trace_of_ticks s 2 ticks, halted, ?_, (congrFun mem 22).trans pointer,
      (congrFun mem 24).trans count, Nat.le_refl _, ?_, ?_⟩
    · simpa only [mem, reduce] using table
    · simpa only [reduce, List.length_nil, Nat.zero_mul, Nat.add_zero] using separate
    · intro a _ _; exact congrFun mem a
  | append_singleton pending query ih =>
    have length : (pending ++ [query]).length = pending.length + 1 := by simp
    have space : destination + (pending.length + 1) * (3 * (capacity + 1)) < 2 ^ w.bits := by
      simpa only [length] using fits
    have pendingFits : pending.length + 1 < 2 ^ w.bits := by
      have lower := Nat.le_mul_of_pos_right (pending.length + 1) (by omega : 0 < 3 * (capacity + 1))
      omega
    have nonzero : s.mem 20 ≠ 0#w.bits := by
      intro h
      have hn := congrArg BitVec.toNat h
      simp [remaining, length, Nat.mod_eq_of_lt pendingFits] at hn
    have splitInput : VectorBuilder.Stored s.mem source (RecordTable.words w pending) ∧
        VectorBuilder.Stored s.mem (source + 3 * pending.length) (RecordTable.words w [query]) := by
      rw [words_append, stored_append, RecordTable.words_length] at input
      exact input
    have queryPointer : s.mem 21 = BitVec.ofNat w.bits (source + 3 * pending.length + 3) := by
      rw [cursor, length]
      congr 1 <;> omega
    have firstBuffer : destination + 3 * (accumulated.length + 1) < 2 ^ w.bits := by
      have lower := Nat.le_mul_of_pos_left (3 * (capacity + 1)) (by omega : 0 < pending.length + 1)
      simp only [length] at capacityBound
      omega
    obtain ⟨stepTime, next, stepBound, stepTrace, npc, nlive, nextTable, nextCount, nextPointer,
        nextOutput, nextStride, nextRemaining, nextCursor, frame⟩ :=
      iteration query accumulated s (source + 3 * pending.length) address destination (3 * (capacity + 1)) pc live nonzero
        (by omega) base (by simp only [length] at inputBefore; omega) separate firstBuffer variablesFit
        queryPointer pointer count outputPointer stride splitInput.2.1 splitInput.2.2.1 splitInput.2.2.2.1 table
    have insertBound := Normalize.insert_length query accumulated
    have nextCapacity : pending.length + (Normalize.insert query accumulated).length ≤ capacity := by
      simp only [length] at capacityBound; omega
    have nextInput : VectorBuilder.Stored next.mem source (RecordTable.words w pending) := by
      apply MemoryCopy.stored_frame _ _ splitInput.1
      intro a lo hi
      apply frame a (by omega) (Or.inl ?_)
      rw [RecordTable.words_length] at hi
      simp only [length] at inputBefore; omega
    have nr : next.mem 20 = BitVec.ofNat w.bits pending.length := by
      rw [nextRemaining, remaining, length]
      change BitVec.ofNat w.bits (pending.length + 1) - BitVec.ofNat w.bits 1 = _
      rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]; simp
    have nextFits : destination + 3 * (capacity + 1) + pending.length * (3 * (capacity + 1)) < 2 ^ w.bits := by
      rw [Nat.add_mul, Nat.one_mul] at space; omega
    obtain ⟨time, final, resultAddress, bound, trace, halted, resultTable, resultPointer, resultCount,
        lower, upper, preserved⟩ :=
      ih (Normalize.insert query accumulated) next destination (destination + 3 * (capacity + 1))
        npc nlive (by omega) nextCapacity (by simp only [length] at inputBefore; omega) (by omega)
        nextFits nr nextCursor nextPointer nextCount nextOutput nextStride nextInput nextTable
    refine ⟨stepTime + time, final, resultAddress, ?_, stepTrace.append trace, halted, ?_, resultPointer, ?_, ?_, ?_, ?_⟩
    · rw [length, Nat.add_mul, Nat.one_mul]
      simp only [length] at capacityBound
      omega
    · simpa only [reduce_snoc] using resultTable
    · simpa only [reduce_snoc] using resultCount
    · omega
    · rw [reduce_snoc, length, Nat.add_mul, Nat.one_mul]; omega
    · intro a ha outside
      rw [length, Nat.add_mul, Nat.one_mul] at outside
      apply Eq.trans (preserved a ha (by omega))
      apply frame a ha
      simp only [length] at capacityBound
      have lower := Nat.le_mul_of_pos_left (3 * (capacity + 1)) (by omega : 0 < pending.length + 1)
      rw [Nat.add_mul, Nat.one_mul] at lower
      omega

/-- Initialize the loop from count 11, input pointer 12, and output pointer 13. -/
def setup : Algorithm :=
  ⟨[.copy (.direct 20) (reg 11),
    .binary .add (.direct 21) (reg 11) (reg 11),
    .binary .add (.direct 21) (reg 21) (reg 11),
    .binary .add (.direct 21) (reg 21) (reg 12),
    .copy (.direct 22) (reg 21), .copy (.direct 24) (.immediate 0),
    .copy (.direct 18) (reg 13),
    .binary .add (.direct 23) (reg 11) (.immediate 1),
    .binary .add (.direct 19) (reg 23) (reg 23),
    .binary .add (.direct 19) (reg 19) (reg 23), .halt], 1, by decide⟩

def initialized : Algorithm := ⟨SourceChain.code setup.code algorithm.code, 1, by decide⟩

theorem initializes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (setup.program w) 11 s
    t.halted = true ∧ t.ticks = s.ticks + 11 ∧ t.mem 20 = s.mem 11 ∧
      t.mem 21 = s.mem 11 + s.mem 11 + s.mem 11 + s.mem 12 ∧
      t.mem 22 = s.mem 11 + s.mem 11 + s.mem 11 + s.mem 12 ∧ t.mem 24 = 0#w.bits ∧
      t.mem 18 = s.mem 13 ∧
      t.mem 19 = (s.mem 11 + 1#w.bits) + (s.mem 11 + 1#w.bits) + (s.mem 11 + 1#w.bits) ∧
      (∀ a, 32 ≤ a → 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, BinOp.eval, pc, live, Nat.add_assoc]
  intro a ha
  have neq : a ≠ 20 ∧ a ≠ 21 ∧ a ≠ 22 ∧ a ≠ 24 ∧ a ≠ 18 ∧ a ≠ 23 ∧ a ≠ 19 := by omega
  simp [neq]

/-- Complete initialized normalization of a formula-record table. Literal
multiplicity is removed by its mask representation; the insertion loop removes
subsumed clauses in exactly the order specified by `Normalize.normalize`. -/
theorem normalizes (clauses : CNF n) (s : State w) (source destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
    (separate : source + 3 * clauses.length ≤ destination)
    (fits : destination + clauses.length * (3 * (clauses.length + 1)) < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (count : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w clauses)) :
    ∃ time final resultAddress,
      time ≤ clauses.length * (35 * clauses.length + 34) + 13 ∧
      Runs widthConstant (initialized.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem resultAddress (RecordTable.words w (Normalize.normalize clauses)) ∧
      final.mem 22 = BitVec.ofNat w.bits resultAddress ∧
      final.mem 24 = BitVec.ofNat w.bits (Normalize.normalize clauses).length ∧
      source + 3 * clauses.length ≤ resultAddress ∧
      resultAddress + 3 * (Normalize.normalize clauses).length ≤ destination + clauses.length * (3 * (clauses.length + 1)) ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + clauses.length * (3 * (clauses.length + 1)) ≤ a) → final.mem a = s.mem a) := by
  let middle := run widthConstant (setup.program w) 11 s
  obtain ⟨halted, ticks, pending, cursor, current, empty, dest, stride, frame⟩ := initializes s pc live
  have cursorValue : middle.mem 21 = BitVec.ofNat w.bits (source + 3 * clauses.length) := by
    rw [cursor, count, pointer, ← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
    congr 1 <;> omega
  have currentValue : middle.mem 22 = BitVec.ofNat w.bits (source + 3 * clauses.length) := by
    rw [current, count, pointer, ← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
    congr 1 <;> omega
  have strideValue : middle.mem 19 = BitVec.ofNat w.bits (3 * (clauses.length + 1)) := by
    rw [stride, count, ← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
    congr 1 <;> omega
  have input' : VectorBuilder.Stored middle.mem source (RecordTable.words w (clauses.map Normalize.clean)) := by
    rw [RecordTable.words_clean]
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact frame a (by omega)
  obtain ⟨time, out, resultAddress, bound, trace, outHalt, table, resultPointer, resultCount, lower, upper, preserved⟩ :=
    reduces (clauses.map Normalize.clean) [] clauses.length (SourceChain.resume middle)
      source (source + 3 * clauses.length) destination rfl rfl base (by omega)
      (by simp) (by simp) (by simpa using separate) (by simpa using fits) variablesFit
      (by simpa only [List.length_map, SourceChain.resume, middle] using pending.trans count)
      (by simpa only [List.length_map, SourceChain.resume] using cursorValue) currentValue empty (dest.trans outputPointer)
      strideValue input' trivial
  have setupTrace : Runs widthConstant (setup.program w) 11 s middle := by
    obtain ⟨t, _, h⟩ := run_has_trace widthConstant (setup.program w) 11 s
    have cost := runs_cost h
    have eq : t = 11 := by omega
    subst t; exact h
  have full := SourceChain.traces setup.code algorithm.code s middle out 11 time live halted setupTrace trace
  refine ⟨11 + time, out.relocate setup.code.length, resultAddress, ?_, full, outHalt, ?_, resultPointer, ?_, lower, ?_, ?_⟩
  · simp only [List.length_map] at bound; omega
  · simpa only [reduce_nil, Normalize.normalize, State.relocate] using table
  · simpa only [reduce_nil, Normalize.normalize, State.relocate] using resultCount
  · simpa only [reduce_nil, Normalize.normalize, List.length_map] using upper
  · intro a ha outside
    exact (preserved a ha (by simpa only [List.length_map] using outside)).trans (frame a ha)

end WordRAM.Conjectures.Sparsification.NormalizeMachine