SETH ⇒ OVC sparsification bundle 19: 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_18

set_option autoImplicit true

/-! A wordRAM loop constructing three-word records for a serialized formula. -/
namespace WordRAM.Conjectures.Sparsification.RecordTable

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

def setupPrefix : List SourceInstruction :=
  [.branch .eq (reg 11) (.immediate 0) 56,
   .copy (.direct 2) (.memory (.indirect 12)),
   .binary .add (.direct 1) (reg 12) (.immediate 1),
   .binary .add (.direct 15) (reg 2) (reg 2),
   .binary .add (.direct 15) (reg 1) (reg 15)]

def epilogue : List SourceInstruction :=
  [.copy (.indirect 13) (reg 7),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .copy (.indirect 13) (reg 5),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .copy (.indirect 13) (reg 0),
   .binary .add (.direct 13) (reg 13) (.immediate 1),
   .copy (.direct 12) (reg 15),
   .binary .sub (.direct 11) (reg 11) (.immediate 1),
   .jump 0, .halt]

/-- Inputs: 11=number of clauses, 12=input cursor, 13=output cursor.
Cell 15 saves the next input address; cells 0..7 are record-builder scratch.
Each output record is positive mask, negative mask, distinct-literal count. -/
def algorithm : Algorithm :=
  ⟨setupPrefix ++ (RecordBuilder.algorithm.code.map (SourceInstruction.returnTo 42)).map
    (SourceInstruction.relocate 5) ++ epilogue, 1, by decide⟩

private theorem program_eq (w : Width) : algorithm.program w =
    setupPrefix.map (SourceInstruction.compile w) ++
    (((RecordBuilder.algorithm.program w).map (Instruction.returnTo 42)).map (Instruction.relocate 5) ++
      epilogue.map (SourceInstruction.compile w)) := rfl

theorem enters (s : State w) (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 11 ≠ 0#w.bits) :
    let t := run widthConstant (algorithm.program w) 5 s
    t.pc = 5 ∧ t.halted = false ∧ t.ticks = s.ticks + 5 ∧
      t.mem 1 = s.mem 12 + 1#w.bits ∧ t.mem 2 = s.mem (s.mem 12).toNat ∧
      t.mem 15 = s.mem 12 + 1#w.bits + (s.mem (s.mem 12).toNat + s.mem (s.mem 12).toNat) ∧
      (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 15 → t.mem a = s.mem a) := by
  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,
    Nat.add_assoc, List.getElem?_cons_zero, List.getElem?_cons_succ]
  intro a h1 h2 h15
  simp [h1, h2, h15]

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, RecordBuilder.algorithm, RecordBuilder.bridge, SizeMachine.algorithm,
    SizeMachine.bridge, SizeMachine.finish, SourceChain.code, PopcountMachine.initialized, PopcountMachine.algorithm,
    MaskBuilder.initialized, MaskBuilder.algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    SourceInstruction.relocate, SourceInstruction.returnTo, reg, run, step, execute,
    Address.resolve, Operand.read, Comparison.test, pc, live, empty, Nat.add_assoc]

theorem leaves (s : State w) (destination : Nat) (pc : s.pc = 47) (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) 9 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 9 ∧
      t.mem 11 = s.mem 11 - 1#w.bits ∧ t.mem 12 = s.mem 15 ∧
      t.mem 13 = BitVec.ofNat w.bits (destination + 3) ∧
      t.mem destination = s.mem 7 ∧ t.mem (destination + 1) = s.mem 5 ∧ t.mem (destination + 2) = s.mem 0 ∧
      (∀ a, a ≠ 11 → a ≠ 12 → a ≠ 13 → 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, RecordBuilder.algorithm, RecordBuilder.bridge, SizeMachine.algorithm,
    SizeMachine.bridge, SizeMachine.finish, SourceChain.code, PopcountMachine.initialized, PopcountMachine.algorithm,
    MaskBuilder.initialized, MaskBuilder.algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    SourceInstruction.relocate, SourceInstruction.returnTo, 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 h0 h1 h2
    simp [h11, h12, h13, h0, h1, h2]

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

/-- One complete iteration, including parsing, counting, and storing the record. -/
theorem iteration (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)
    (inputFits : address + 1 + 2 * clause.length < 2 ^ w.bits)
    (outputFits : destination + 2 < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (lengthWord : s.mem address = BitVec.ofNat w.bits clause.length)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : MaskBuilder.Encoded s.mem (address + 1) (clause.map (MaskBuilder.wordLiteral w))) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) (10 * clause.length + 12 * w.bits + 35) s final ∧
      final.pc = 0 ∧ final.halted = false ∧
      final.mem 11 = s.mem 11 - 1#w.bits ∧
      final.mem 12 = BitVec.ofNat w.bits (address + 1 + 2 * clause.length) ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + 3) ∧
      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 → a ≠ destination + 1 → a ≠ destination + 2 →
        final.mem a = s.mem a) := by
  let head := run widthConstant (algorithm.program w) 5 s
  obtain ⟨hpc, hlive, ticks, hp, hc, hn, hf⟩ := enters s pc live nonzero
  have pn : (s.mem 12).toNat = address := by
    rw [pointer]; exact Nat.mod_eq_of_lt (by omega)
  rw [pn, lengthWord] at hc hn
  let entry : State w := { head with pc := 0 }
  have entryLive : entry.halted = false := hlive
  have entryPointer : entry.mem 1 = BitVec.ofNat w.bits (address + 1) := by
    change head.mem 1 = _
    rw [hp, pointer, ← BitVec.ofNat_add]
  have entryFrame : ∀ a, 16 ≤ a → entry.mem a = s.mem a := by
    intro a ha
    exact hf a (by omega) (by omega) (by omega)
  have input' : MaskBuilder.Encoded entry.mem (address + 1)
      (clause.map (MaskBuilder.wordLiteral w)) := by
    apply MaskTable.pair_frame _ _ input
    intro a lo _
    exact entryFrame a (by omega)
  obtain ⟨built, trace, halted, bpos, bneg, bsize, bf⟩ :=
    RecordBuilder.builds clause entry (address + 1) rfl entryLive (by omega)
      inputFits variablesFit entryPointer hc input'
  have embedded : EmbedsAt ((RecordBuilder.algorithm.program w).map (Instruction.returnTo 42))
      (algorithm.program w) 5 := by
    rw [program_eq]
    exact embeds_append (setupPrefix.map (SourceInstruction.compile w))
      ((RecordBuilder.algorithm.program w).map (Instruction.returnTo 42))
      (epilogue.map (SourceInstruction.compile w))
  let returned := (built.returnTo 42).relocate 5
  have linked : Runs widthConstant (algorithm.program w) (10 * clause.length + 12 * w.bits + 21)
      head returned := by
    have h := (trace.returnTo 42).relocate embedded
    have he : (entry.returnTo 42).relocate 5 = head := by
      simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
      change { head with pc := 5 } = head
      have hpc' : head.pc = 5 := hpc
      rw [← hpc']
    simpa only [he] using h
  have returnedFrame : ∀ a, 8 ≤ a → returned.mem a = entry.mem a := by
    intro a ha; simpa [returned, State.returnTo, State.relocate, halted] using bf a ha
  have returnedPointer : returned.mem 13 = BitVec.ofNat w.bits destination := by
    rw [returnedFrame 13 (by decide)]
    exact (hf 13 (by decide) (by decide) (by decide)).trans outputPointer
  have retPC : returned.pc = 47 := by simp [returned, State.returnTo, State.relocate, halted]
  have retLive : returned.halted = false := by simp [returned, State.returnTo, State.relocate, halted]
  obtain ⟨fpc, flive, fticks, fc, fn, fp, fpos, fneg, fsize, ff⟩ :=
    leaves returned destination retPC retLive outputBase outputFits returnedPointer
  let final := run widthConstant (algorithm.program w) 9 returned
  have finCount : final.mem 11 = s.mem 11 - 1#w.bits := by
    rw [fc, returnedFrame 11 (by decide)]
    rw [show entry.mem 11 = s.mem 11 from hf 11 (by decide) (by decide) (by decide)]
  have finNext : final.mem 12 = BitVec.ofNat w.bits (address + 1 + 2 * clause.length) := by
    rw [fn, returnedFrame 15 (by decide)]
    change head.mem 15 = _
    rw [hn, pointer, ← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
    congr 1
    omega
  refine ⟨final, ?_, fpc, flive, finCount, finNext, fp, ?_, ?_, ?_, ?_⟩
  · have allSteps := ((trace_of_ticks s 5 ticks).append linked).append
      (trace_of_ticks returned 9 fticks)
    have cost : (5 + (10 * clause.length + 12 * w.bits + 21)) + 9 =
        10 * clause.length + 12 * w.bits + 35 := by omega
    rw [cost] at allSteps
    exact allSteps
  · simpa [final, returned, State.returnTo, State.relocate, halted, bpos] using fpos
  · simpa [final, returned, State.returnTo, State.relocate, halted, bneg] using fneg
  · simpa [final, returned, State.returnTo, State.relocate, halted, bsize] using fsize
  · intro a ha h0 h1 h2
    exact (ff a (by omega) (by omega) (by omega) h0 h1 h2).trans
      ((returnedFrame a (by omega)).trans (entryFrame a ha))

/-- Three words per clause, in the original clause order. -/
def words (w : Width) : CNF n → List (Word w)
  | [] => []
  | clause :: rest => Masks.encode w clause true :: Masks.encode w clause false ::
      BitVec.ofNat w.bits (Normalize.clean clause).length :: words w rest

theorem words_length (w : Width) (clauses : CNF n) :
    (words w clauses).length = 3 * clauses.length := by
  induction clauses with
  | nil => rfl
  | cons clause rest ih => simp only [words, List.length_cons, ih, Nat.mul_add] <;> omega

/-- Includes all parsing, population counts, loop control, stores, and final halt. -/
def cost (w : Width) : CNF n → Nat
  | [] => 2
  | clause :: rest => 10 * clause.length + 12 * w.bits + 35 + cost w rest

/-- Construct the entire record table from the actual serialized formula.
Input and output regions are disjoint; the frame assertion preserves every
non-register cell outside the output table. -/
theorem builds (clauses : CNF n) (s : State w) (address destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (inputBefore : address + MaskTable.span clauses ≤ destination)
    (fits : destination + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (outputPointer : s.mem 13 = BitVec.ofNat w.bits destination)
    (input : MaskTable.Encoded s.mem address clauses) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) (cost w clauses) s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (words w clauses) ∧
      (∀ 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
    have he := exits s pc live empty
    refine ⟨run widthConstant (algorithm.program w) 2 s, trace_of_ticks s 2 he.2.2,
      he.1, trivial, ?_⟩
    intro a _ _; exact congrFun he.2.1 a
  | cons clause rest ih =>
    have countFits : rest.length + 1 < 2 ^ w.bits := by
      simp only [List.length_cons] at fits
      omega
    have nz : 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 ⟨next, stepTrace, npc, nlive, ncount, np, nd, pos, neg, size, frame⟩ :=
      iteration clause s address destination pc live nz base
        (by simp only [MaskTable.span] at inputBefore; omega)
        (by simp only [MaskTable.span] at inputBefore; omega)
        (by simp only [List.length_cons] at fits; omega)
        variablesFit pointer input.1 outputPointer input.2.1
    have nc : next.mem 11 = BitVec.ofNat w.bits rest.length := by
      rw [ncount, 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 : MaskTable.Encoded next.mem (address + 1 + 2 * clause.length) rest := by
      apply MaskTable.Encoded.frame _ _ input.2.2
      intro a lo hi
      apply frame a (by omega)
      all_goals simp only [MaskTable.span] at inputBefore
      all_goals omega
    obtain ⟨final, trace, halted, table, preserved⟩ :=
      ih next (address + 1 + 2 * clause.length) (destination + 3) npc nlive (by omega)
        (by simp only [MaskTable.span] at inputBefore; omega)
        (by simp only [List.length_cons] at fits; omega)
        np nc nd nextInput
    refine ⟨final, stepTrace.append trace, halted, ?_, ?_⟩
    · refine ⟨?_, ?_, ?_, table⟩
      · exact (preserved destination (by omega) (by omega)).trans pos
      · exact (preserved (destination + 1) (by omega) (by omega)).trans neg
      · exact (preserved (destination + 2) (by omega) (by omega)).trans size
    · intro a ha outside
      simp only [List.length_cons] at outside
      exact (preserved a ha (by omega)).trans (frame a ha (by omega) (by omega) (by omega))

/-- Record construction already removes literal multiplicity. Cleaning the
logical clauses therefore leaves the entire table unchanged. -/
theorem words_clean (w : Width) (clauses : CNF n) :
    words w (clauses.map Normalize.clean) = words w clauses := by
  induction clauses with
  | nil => rfl
  | cons clause rest ih =>
    simp only [List.map_cons, words, MaskCardinality.clean_mask, ih,
      Normalize.clean_eq (Normalize.clean clause) (Normalize.clean_nodup clause)]

end WordRAM.Conjectures.Sparsification.RecordTable