SETH ⇒ OVC sparsification bundle 20: 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_19

set_option autoImplicit true

/-! Actual scans of a clause-record table for a subsumption witness. -/
namespace WordRAM.Conjectures.Sparsification.SubsumptionScan

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

/-- If `inside` is true, test query ⊆ record; otherwise test record ⊆ query.
Query masks are in 1,2; remaining count in 11; record cursor in 12.
The Boolean result is in 0. Record size is skipped, not interpreted. -/
def algorithm (inside : Bool) : Algorithm :=
  ⟨[.branch .eq (reg 11) (.immediate 0) 15,
    .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 2),
    .binary .band (.direct 5) (reg 1) (reg 3),
    .branch .eq (reg 5) (reg (if inside then 1 else 3)) 8,
    .jump 13,
    .binary .band (.direct 6) (reg 2) (reg 4),
    .branch .eq (reg 6) (reg (if inside then 2 else 4)) 11,
    .jump 13,
    .copy (.direct 0) (.immediate 1),
    .halt,
    .binary .sub (.direct 11) (reg 11) (.immediate 1),
    .jump 0,
    .copy (.direct 0) (.immediate 0),
    .halt], 1, by decide⟩

def first (inside : Bool) (s : State w) : Prop :=
  s.mem 1 &&& s.mem 3 = if inside then s.mem 1 else s.mem 3

def second (inside : Bool) (s : State w) : Prop :=
  s.mem 2 &&& s.mem 4 = if inside then s.mem 2 else s.mem 4

instance (inside : Bool) (s : State w) : Decidable (first inside s) := inferInstanceAs (Decidable (_ = _))
instance (inside : Bool) (s : State w) : Decidable (second inside s) := inferInstanceAs (Decidable (_ = _))

theorem enters (inside : Bool) (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 + 1 < 2 ^ w.bits)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address) :
    let t := run widthConstant ((algorithm inside).program w) 5 s
    t.pc = 5 ∧ t.halted = false ∧ t.ticks = s.ticks + 5 ∧
      t.mem 3 = s.mem address ∧ t.mem 4 = s.mem (address + 1) ∧
      t.mem 12 = BitVec.ofNat w.bits (address + 3) ∧
      (∀ a, a ≠ 3 → a ≠ 4 → 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 fits
  have a3 : address + 1 ≠ 3 := by omega
  have a12 : address + 1 ≠ 12 := by omega
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test,
    pc, live, nonzero, pointer, d0, d1, a3, a12, Nat.add_assoc, -BitVec.toNat_add]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h3 h4 h12; simp [h3, h4, h12]

theorem hit (inside : Bool) (s : State w) (pc : s.pc = 5) (live : s.halted = false)
    (hfirst : first inside s) (hsecond : second inside s) :
    let t := run widthConstant ((algorithm inside).program w) 6 s
    t.halted = true ∧ t.ticks = s.ticks + 6 ∧ t.mem 0 = 1#w.bits ∧
      (∀ a, a ≠ 0 → a ≠ 5 → a ≠ 6 → t.mem a = s.mem a) := by
  cases inside <;>
    simp only [first, second, Bool.false_eq_true, ↓reduceIte] at hfirst hsecond <;>
    simp [hfirst, hsecond, pc, live, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
      reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, Nat.add_assoc]
  all_goals intro a h0 h5 h6; simp [h0, h5, h6]

theorem miss (inside : Bool) (s : State w) (pc : s.pc = 5) (live : s.halted = false)
    (absent : ¬ (first inside s ∧ second inside s)) :
    let fuel := if first inside s then 7 else 5
    let t := run widthConstant ((algorithm inside).program w) fuel s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + fuel ∧
      t.mem 11 = s.mem 11 - 1#w.bits ∧
      (∀ a, a ≠ 5 → a ≠ 6 → a ≠ 11 → t.mem a = s.mem a) := by
  by_cases hf : first inside s <;> by_cases hs : second inside s
  · exact False.elim (absent ⟨hf, hs⟩)
  all_goals cases inside
  all_goals simp only [first, second, Bool.false_eq_true, ↓reduceIte] at hf hs
  all_goals simp [first, hf, hs, pc, live, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, Nat.add_assoc]
  all_goals intro a h5 h6 h11; simp [h5, h6, h11]

theorem exits (inside : Bool) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (empty : s.mem 11 = 0#w.bits) :
    let t := run widthConstant ((algorithm inside).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 0 = 0#w.bits ∧
      (∀ a, a ≠ 0 → t.mem a = s.mem a) := by
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Address.resolve, Operand.read, Memory.write, Comparison.test, pc, live, empty, Nat.add_assoc]
  intro a h; simp [h]

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

/-- Direction of subsumption checked by the chosen program. -/
def Related (inside : Bool) (query clause : Clause n) : Prop :=
  if inside then query ⊆ clause else clause ⊆ query

instance (inside : Bool) (query clause : Clause n) : Decidable (Related inside query clause) := by
  unfold Related
  infer_instance

theorem matches_iff (inside : Bool) (query clause : Clause n) (s : State w)
    (fits : n ≤ w.bits)
    (qp : s.mem 1 = Masks.encode w query true) (qn : s.mem 2 = Masks.encode w query false)
    (cp : s.mem 3 = Masks.encode w clause true) (cn : s.mem 4 = Masks.encode w clause false) :
    first inside s ∧ second inside s ↔ Related inside query clause := by
  cases inside
  · simpa [first, second, Related, qp, qn, cp, cn, BitVec.and_comm] using
      (Masks.subset_iff (w := w) clause query fits).symm
  · simpa [first, second, Related, qp, qn, cp, cn] using
      (Masks.subset_iff (w := w) query clause fits).symm

private theorem stored_frame (xs : List (Word w)) (address : Nat)
    (input : VectorBuilder.Stored mem address xs)
    (frame : ∀ a, address ≤ a → other a = mem a) : VectorBuilder.Stored other address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    exact ⟨(frame address (by omega)).trans input.1,
      ih (address + 1) input.2 (fun a ha => frame a (by omega))⟩

/-- Scan a complete table for a subsumption witness, including early success,
all failed comparisons, cursor updates, and the final empty-table exit. -/
theorem scans (inside : Bool) (query : Clause n) (clauses : CNF n)
    (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 16 ≤ address) (fits : address + 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)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 12 * clauses.length + 3 ∧
      Runs widthConstant ((algorithm inside).program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if ∃ clause ∈ clauses, Related inside query clause then 1#w.bits else 0#w.bits) ∧
      (∀ a, a ≠ 0 → a ≠ 3 → a ≠ 4 → a ≠ 5 → a ≠ 6 → a ≠ 11 → a ≠ 12 → final.mem a = s.mem a) := by
  induction clauses generalizing s address with
  | nil =>
    have empty : s.mem 11 = 0#w.bits := by simpa using remaining
    obtain ⟨halted, ticks, result, frame⟩ := exits inside s pc live empty
    refine ⟨3, run widthConstant ((algorithm inside).program w) 3 s, by simp,
      trace_of_ticks inside s 3 ticks, halted, ?_, ?_⟩
    · simpa using result
    · intro a h0 _ _ _ _ _ _; exact frame a h0
  | cons clause rest ih =>
    have countFits : rest.length + 1 < 2 ^ w.bits := by
      simp only [List.length_cons] at fits
      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 ⟨hpc, hlive, hticks, hp, hn, hnext, hf⟩ :=
      enters inside s address pc live nonzero base
        (by simp only [List.length_cons] at fits; omega) pointer
    let head := run widthConstant ((algorithm inside).program w) 5 s
    have headQP : head.mem 1 = Masks.encode w query true :=
      (hf 1 (by decide) (by decide) (by decide)).trans qp
    have headQN : head.mem 2 = Masks.encode w query false :=
      (hf 2 (by decide) (by decide) (by decide)).trans qn
    have matching := matches_iff inside query clause head variablesFit headQP headQN
      (hp.trans input.1) (hn.trans input.2.1)
    by_cases related : Related inside query clause
    · obtain ⟨firstOK, secondOK⟩ := matching.mpr related
      obtain ⟨halted, ticks, result, frame⟩ := hit inside head hpc hlive firstOK secondOK
      have existsClause : ∃ c ∈ clause :: rest, Related inside query c := ⟨clause, by simp, related⟩
      refine ⟨11, run widthConstant ((algorithm inside).program w) 6 head,
        by simp only [List.length_cons]; omega,
        (trace_of_ticks inside s 5 hticks).append (trace_of_ticks inside head 6 ticks), halted, ?_, ?_⟩
      · simpa only [if_pos existsClause] using result
      · intro a h0 h3 h4 h5 h6 _ h12
        exact (frame a h0 h5 h6).trans (hf a h3 h4 h12)
    · have absent : ¬ (first inside head ∧ second inside head) := fun h => related (matching.mp h)
      let fuel := if first inside head then 7 else 5
      let next := run widthConstant ((algorithm inside).program w) fuel head
      obtain ⟨npc, nlive, nticks, ncount, nf⟩ := miss inside head hpc hlive absent
      have nextFrame : ∀ a, a ≠ 3 → a ≠ 4 → a ≠ 5 → a ≠ 6 → a ≠ 11 → a ≠ 12 → next.mem a = s.mem a := by
        intro a h3 h4 h5 h6 h11 h12
        exact (nf a h5 h6 h11).trans (hf a h3 h4 h12)
      have nc : next.mem 11 = BitVec.ofNat w.bits rest.length := by
        rw [ncount, hf 11 (by decide) (by decide) (by decide), 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 np : next.mem 12 = BitVec.ofNat w.bits (address + 3) :=
        (nf 12 (by decide) (by decide) (by decide)).trans hnext
      have nextInput : VectorBuilder.Stored next.mem (address + 3) (RecordTable.words w rest) := by
        apply stored_frame _ _ input.2.2.2
        intro a ha
        exact nextFrame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)
      obtain ⟨time, final, bound, trace, halted, result, frame⟩ :=
        ih next (address + 3) npc nlive (by omega)
          (by simp only [List.length_cons] at fits; omega)
          ((nextFrame 1 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qp)
          ((nextFrame 2 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans qn)
          np nc nextInput
      refine ⟨5 + fuel + time, final, ?_,
        ((trace_of_ticks inside s 5 hticks).append (trace_of_ticks inside head fuel nticks)).append trace,
        halted, ?_, ?_⟩
      · have small : fuel ≤ 7 := by unfold fuel; split <;> omega
        simp only [List.length_cons]; omega
      · simpa only [List.mem_cons, exists_eq_or_imp, related, false_or] using result
      · intro a h0 h3 h4 h5 h6 h11 h12
        exact (frame a h0 h3 h4 h5 h6 h11 h12).trans (nextFrame a h3 h4 h5 h6 h11 h12)

end WordRAM.Conjectures.Sparsification.SubsumptionScan