SETH ⇒ OVC sparsification bundle 22: 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_21

set_option autoImplicit true

/-! Actual wordRAM implementation of subsumption-normalization insertion. -/
namespace WordRAM.Conjectures.Sparsification.InsertMachine

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

/-- Save the original table extent across the early-exiting subsumption scan. -/
def save : Algorithm :=
  ⟨[.copy (.direct 8) (reg 11), .copy (.direct 9) (reg 12), .halt], 1, by decide⟩

/-- A subsumed query leaves the logical table unchanged; copy it to the output. -/
def copySetup : Algorithm :=
  ⟨[.copy (.direct 1) (reg 9), .copy (.direct 2) (reg 13), .copy (.direct 3) (reg 8),
    .binary .add (.direct 3) (reg 3) (reg 3), .binary .add (.direct 3) (reg 3) (reg 8),
    .copy (.direct 14) (reg 8), .halt], 1, by decide⟩

def copyOld : Algorithm :=
  ⟨SourceChain.code copySetup.code MemoryCopy.algorithm.code, 1, by decide⟩

/-- Emit the new clause, then remove every old clause containing it. -/
def filterSetup : Algorithm :=
  ⟨[.copy (.indirect 13) (reg 1), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.indirect 13) (reg 2), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.indirect 13) (reg 7), .binary .add (.direct 13) (reg 13) (.immediate 1),
    .copy (.direct 11) (reg 8), .copy (.direct 12) (reg 9), .copy (.direct 14) (.immediate 1), .halt], 1, by decide⟩

def filterNew : Algorithm :=
  ⟨SourceChain.code filterSetup.code RecordFilter.algorithm.code, 1, by decide⟩

/-- Inputs: query masks 1,2, query size 7, clause count 11, table pointer 12,
output pointer 13. Output count is 14. All table writes are explicit. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code save.code (SourceChain.code (SubsumptionScan.algorithm false).code
      (SourceIf.code 0 filterNew.code copyOld.code)), 1, by decide⟩

theorem saves (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (save.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 8 = s.mem 11 ∧ t.mem 9 = s.mem 12 ∧
      (∀ a, a ≠ 8 → a ≠ 9 → t.mem a = s.mem a) := by
  simp [save, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h8 h9; simp [h8, h9]

theorem copy_setup (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (copySetup.program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧ t.mem 1 = s.mem 9 ∧ t.mem 2 = s.mem 13 ∧
      t.mem 3 = s.mem 8 + s.mem 8 + s.mem 8 ∧ t.mem 14 = s.mem 8 ∧
      (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 3 → a ≠ 14 → t.mem a = s.mem a) := by
  simp [copySetup, 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 h1 h2 h3 h14; simp [h1, h2, h3, h14]

theorem filter_setup (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 (filterSetup.program w) 10 s
    t.halted = true ∧ t.ticks = s.ticks + 10 ∧ t.mem 11 = s.mem 8 ∧ t.mem 12 = s.mem 9 ∧
      t.mem 14 = 1#w.bits ∧ t.mem 13 = BitVec.ofNat w.bits (destination + 3) ∧
      t.mem destination = s.mem 1 ∧ t.mem (destination + 1) = s.mem 2 ∧ t.mem (destination + 2) = s.mem 7 ∧
      (∀ a, a ≠ 11 → a ≠ 12 → 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 [filterSetup, 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 h11 h12 h13 h14 h0 h1 h2; simp [h11, h12, h13, h14, h0, h1, h2]

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

theorem copies_old (clauses : CNF n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (separate : address + 3 * clauses.length ≤ destination)
    (fits : destination + 3 * clauses.length < 2 ^ w.bits)
    (count : s.mem 8 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 9 = BitVec.ofNat w.bits address)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ final, Runs widthConstant (copyOld.program w) (21 * clauses.length + 9) s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (RecordTable.words w clauses) ∧
      final.mem 14 = BitVec.ofNat w.bits clauses.length ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 * clauses.length ≤ a) → final.mem a = s.mem a) := by
  let middle := run widthConstant (copySetup.program w) 7 s
  obtain ⟨halted, ticks, sp, dp, len, outputCount, frame⟩ := copy_setup s pc live
  have wordCount : middle.mem 3 = BitVec.ofNat w.bits (RecordTable.words w clauses).length := by
    rw [len, count, ← BitVec.ofNat_add, ← BitVec.ofNat_add, RecordTable.words_length]
    congr 1; omega
  have nextInput : VectorBuilder.Stored middle.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact frame a (by omega) (by omega) (by omega) (by omega)
  obtain ⟨out, trace, outHalt, table, preserved⟩ := MemoryCopy.copies (RecordTable.words w clauses)
    (SourceChain.resume middle) address destination rfl rfl (by omega)
    (by simpa only [RecordTable.words_length] using separate)
    (by simpa only [RecordTable.words_length] using fits)
    (sp.trans pointer) (dp.trans outputPointer) wordCount nextInput
  have full := SourceChain.traces copySetup.code MemoryCopy.algorithm.code s middle out
    7 (7 * (RecordTable.words w clauses).length + 2) live halted
    (trace_of_ticks _ s 7 ticks) trace
  refine ⟨out.relocate copySetup.code.length, ?_, outHalt, table, ?_, ?_⟩
  · have cost : 7 + (7 * (RecordTable.words w clauses).length + 2) = 21 * clauses.length + 9 := by
      rw [RecordTable.words_length]; omega
    simpa only [copyOld, Algorithm.program, cost] using full
  · exact (preserved 14 (by decide) (Or.inl (by omega))).trans (outputCount.trans count)
  · intro a ha outside
    exact (preserved a (by omega) (by simpa only [RecordTable.words_length] using outside)).trans
      (frame a (by omega) (by omega) (by omega) (by omega))

theorem filters_new (query : Clause n) (clauses : CNF n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (separate : address + 3 * clauses.length ≤ destination)
    (fits : destination + 3 * (clauses.length + 1) < 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)
    (size : s.mem 7 = BitVec.ofNat w.bits (Normalize.clean query).length)
    (count : s.mem 8 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 9 = BitVec.ofNat w.bits address)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    let result := query :: clauses.filter (fun larger => !decide (query ⊆ larger))
    ∃ time final, time ≤ 23 * clauses.length + 12 ∧ Runs widthConstant (filterNew.program w) time s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (RecordTable.words w result) ∧
      final.mem 14 = BitVec.ofNat w.bits result.length ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 * (clauses.length + 1) ≤ a) → final.mem a = s.mem a) := by
  let middle := run widthConstant (filterSetup.program w) 10 s
  obtain ⟨halted, ticks, count', pointer', outCount, dest, pos, neg, len, frame⟩ :=
    filter_setup s destination pc live (by omega) (by omega) outputPointer
  have nextInput : VectorBuilder.Stored middle.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo hi
    rw [RecordTable.words_length] at hi
    exact frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)
  obtain ⟨time, out, bound, trace, outHalt, table, _, _, _, total, preserved⟩ :=
    RecordFilter.builds query clauses (SourceChain.resume middle) address (destination + 3) rfl rfl base (by omega)
      (Or.inr (by omega)) (by omega) (by omega) variablesFit
      ((frame 1 (by decide) (by decide) (by decide) (by decide) (by omega) (by omega) (by omega)).trans qp)
      ((frame 2 (by decide) (by decide) (by decide) (by decide) (by omega) (by omega) (by omega)).trans qn)
      (pointer'.trans pointer) dest (count'.trans count) nextInput
  have full := SourceChain.traces filterSetup.code RecordFilter.algorithm.code s middle out
    10 time live halted (trace_of_ticks _ s 10 ticks) trace
  refine ⟨10 + time, out.relocate filterSetup.code.length, by omega, full, outHalt, ?_, ?_, ?_⟩
  · refine ⟨?_, ?_, ?_, table⟩
    · exact (preserved destination (by omega) (Or.inl (by omega))).trans (pos.trans qp)
    · exact (preserved (destination + 1) (by omega) (Or.inl (by omega))).trans (neg.trans qn)
    · exact (preserved (destination + 2) (by omega) (Or.inl (by omega))).trans (len.trans size)
  · change out.mem 14 = _
    rw [total]
    change middle.mem 14 + _ = _
    rw [outCount, ← BitVec.ofNat_add]
    congr 1
    simp only [List.length_cons]; omega
  · intro a ha outside
    exact (preserved a ha (by omega)).trans
      (frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega))

/-- The linked program implements the existing logical insertion definition;
its bound includes scanning, dispatch, copying/filtering, and every setup step. -/
theorem inserts (query : Clause n) (clauses : CNF n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (separate : address + 3 * clauses.length ≤ destination)
    (fits : destination + 3 * (clauses.length + 1) < 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)
    (size : s.mem 7 = BitVec.ofNat w.bits (Normalize.clean query).length)
    (count : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 35 * clauses.length + 19 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (RecordTable.words w (Normalize.insert query clauses)) ∧
      final.mem 14 = BitVec.ofNat w.bits (Normalize.insert query clauses).length ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 * (clauses.length + 1) ≤ a) → final.mem a = s.mem a) := by
  let saved := run widthConstant (save.program w) 3 s
  obtain ⟨savedHalt, savedTicks, savedCount, savedPointer, savedFrame⟩ := saves s pc live
  have savedInput : VectorBuilder.Stored saved.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact savedFrame a (by omega) (by omega)
  obtain ⟨scanTime, scanned, scanBound, scanTrace, scanHalt, scanResult, scanFrame⟩ :=
    SubsumptionScan.scans false query clauses (SourceChain.resume saved) address rfl rfl base (by omega) variablesFit
      ((savedFrame 1 (by decide) (by decide)).trans qp)
      ((savedFrame 2 (by decide) (by decide)).trans qn)
      ((savedFrame 12 (by decide) (by decide)).trans pointer)
      ((savedFrame 11 (by decide) (by decide)).trans count) savedInput
  have scannedFrame : ∀ a, 16 ≤ a → scanned.mem a = s.mem a := by
    intro a ha
    exact (scanFrame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
      (savedFrame a (by omega) (by omega))
  let entry := (SourceChain.resume scanned).addTicks 1
  have entryPC : entry.pc = 0 := rfl
  have entryLive : entry.halted = false := rfl
  have ep : entry.mem 1 = Masks.encode w query true :=
    (scanFrame 1 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans
      ((savedFrame 1 (by decide) (by decide)).trans qp)
  have en : entry.mem 2 = Masks.encode w query false :=
    (scanFrame 2 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans
      ((savedFrame 2 (by decide) (by decide)).trans qn)
  have es : entry.mem 7 = BitVec.ofNat w.bits (Normalize.clean query).length :=
    (scanFrame 7 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans
      ((savedFrame 7 (by decide) (by decide)).trans size)
  have ec : entry.mem 8 = BitVec.ofNat w.bits clauses.length :=
    (scanFrame 8 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedCount.trans count)
  have ei : entry.mem 9 = BitVec.ofNat w.bits address :=
    (scanFrame 9 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedPointer.trans pointer)
  have ed : entry.mem 13 = BitVec.ofNat w.bits destination :=
    (scanFrame 13 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans
      ((savedFrame 13 (by decide) (by decide)).trans outputPointer)
  have entryInput : VectorBuilder.Stored entry.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact scannedFrame a (by omega)
  have branch : ∃ time out, time ≤ 23 * clauses.length + 13 ∧
      Runs widthConstant ((SourceIf.code 0 filterNew.code copyOld.code).map (SourceInstruction.compile w))
        time (SourceChain.resume scanned) out ∧ out.halted = true ∧
      VectorBuilder.Stored out.mem destination (RecordTable.words w (Normalize.insert query clauses)) ∧
      out.mem 14 = BitVec.ofNat w.bits (Normalize.insert query clauses).length ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 * (clauses.length + 1) ≤ a) → out.mem a = scanned.mem a) := by
    by_cases subsumed : ∃ clause ∈ clauses, clause ⊆ query
    · have yes : (SourceChain.resume scanned).mem 0 ≠ 0#w.bits := by
        have result : scanned.mem 0 = 1#w.bits := by
          simpa only [SubsumptionScan.Related, Bool.false_eq_true, ↓reduceIte, if_pos subsumed] using scanResult
        change scanned.mem 0 ≠ _
        rw [result]
        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 ⟨out, trace, halted, table, outCount, frame⟩ :=
        copies_old clauses entry address destination entryPC entryLive base separate (by omega) ec ei ed entryInput
      have linked := SourceIf.nonzero_trace 0 filterNew.code copyOld.code (SourceChain.resume scanned)
        out (21 * clauses.length + 9) rfl rfl yes trace
      refine ⟨1 + (21 * clauses.length + 9), out.relocate 1, by omega, linked, halted, ?_, ?_, ?_⟩
      · simpa only [Normalize.insert, if_pos subsumed, State.relocate] using table
      · simpa only [Normalize.insert, if_pos subsumed, State.relocate] using outCount
      · intro a ha outside
        exact frame a ha (by omega)
    · have no : (SourceChain.resume scanned).mem 0 = 0#w.bits := by
        simpa only [SubsumptionScan.Related, Bool.false_eq_true, ↓reduceIte, if_neg subsumed, SourceChain.resume] using scanResult
      obtain ⟨time, out, bound, trace, halted, table, outCount, frame⟩ :=
        filters_new query clauses entry address destination entryPC entryLive base separate fits variablesFit ep en es ec ei ed entryInput
      have linked := SourceIf.zero_trace 0 filterNew.code copyOld.code (SourceChain.resume scanned) out time rfl rfl no trace
      refine ⟨1 + time, out.relocate (1 + copyOld.code.length), by omega, linked, halted, ?_, ?_, ?_⟩
      · simpa only [Normalize.insert, if_neg subsumed, State.relocate] using table
      · simpa only [Normalize.insert, if_neg subsumed, State.relocate] using outCount
      · intro a ha outside; exact frame a ha outside
  obtain ⟨branchTime, out, branchBound, branchTrace, outHalt, table, outCount, frame⟩ := branch
  have tail := SourceChain.traces (SubsumptionScan.algorithm false).code (SourceIf.code 0 filterNew.code copyOld.code)
    (SourceChain.resume saved) scanned out scanTime branchTime rfl scanHalt scanTrace branchTrace
  have full := SourceChain.traces save.code
    (SourceChain.code (SubsumptionScan.algorithm false).code (SourceIf.code 0 filterNew.code copyOld.code))
    s saved _ 3 (scanTime + branchTime) live savedHalt (trace_of_ticks _ s 3 savedTicks) tail
  refine ⟨3 + (scanTime + branchTime), (out.relocate (SubsumptionScan.algorithm false).code.length).relocate save.code.length,
    by omega, full, outHalt, table, outCount, ?_⟩
  intro a ha outside
  exact (frame a ha outside).trans (scannedFrame a ha)

end WordRAM.Conjectures.Sparsification.InsertMachine