SETH ⇒ OVC sparsification bundle 41: 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_40

set_option autoImplicit true

/-! The mask serializer's output is exactly the SAT literal-pair encoding of
canonical clauses, rather than merely a set-equivalent collection of words. -/
namespace WordRAM.Conjectures.Sparsification.SerializedWords

def literals (w : Width) (clause : Clause n) : List (Word w) :=
  clause.flatMap fun literal => [(MaskBuilder.wordLiteral w literal).1, (MaskBuilder.wordLiteral w literal).2]

theorem words_ofFn (mask polarity : Word w) (index count : Nat) :
    MaskSerialize.words mask polarity index count =
      (List.ofFn fun i : Fin count =>
        if mask.getLsbD (index + i.val) then [BitVec.ofNat w.bits (index + i.val), polarity] else []).flatten := by
  induction count generalizing index with
  | zero => simp [MaskSerialize.words]
  | succ count ih =>
    rw [MaskSerialize.words, List.ofFn_succ, List.flatten_cons, ih]
    simp only [Fin.val_zero, Nat.add_zero, Fin.val_succ]
    simp only [Nat.add_comm, Nat.add_left_comm]
    rfl

private theorem filter_flatMap (xs : List α) (p : α → Bool) (f : α → List β) :
    (xs.filter p).flatMap f = (xs.map fun x => if p x then f x else []).flatten := by
  induction xs with
  | nil => simp
  | cons x xs ih => cases h : p x <;> simp [h, ih]

/-- Positive literals precede negative literals, matching the canonical finite
enumeration used in its satisfiability and width proofs. -/
theorem clause_words (input : Clause n) (fits : n ≤ w.bits) :
    literals w (Canonical.clause input) =
      MaskSerialize.words (Masks.encode w input true) (1#w.bits) 0 n ++
      MaskSerialize.words (Masks.encode w input false) (0#w.bits) 0 n := by
  rw [← Canonical.mask_filter input fits]
  unfold literals
  rw [Counting.literals, List.filter_append, List.flatMap_append]
  congr 1 <;>
    rw [filter_flatMap, List.map_ofFn, words_ofFn] <;>
    simp [Function.comp_def, MaskBuilder.wordLiteral]

theorem literals_length (input : Clause n) : (literals w input).length = 2 * input.length := by
  induction input with
  | nil => simp [literals]
  | cons literal rest ih => simp [literals, List.flatMap_cons] at *; omega

theorem canonical_length (input : Clause n) (nodup : input.Nodup) :
    (literals w (Canonical.clause input)).length = 2 * input.length := by
  rw [literals_length, Canonical.length_eq input nodup]

end WordRAM.Conjectures.Sparsification.SerializedWords

/-! Serialize both masks and the length prefix of one clause. -/
namespace WordRAM.Conjectures.Sparsification.ClauseSerialize
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

/-- Inputs 9/10 are the masks, 16 is n, 17 the literal count, 18 the destination. -/
def prepare : Algorithm :=
  ⟨[.copy (.indirect 18) (reg 17), .copy (.direct 1) (reg 9),
    .copy (.direct 2) (.immediate 0), .copy (.direct 3) (reg 16),
    .binary .add (.direct 4) (reg 18) (.immediate 1), .copy (.direct 5) (.immediate 1), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 1) (reg 10), .copy (.direct 2) (.immediate 0),
    .copy (.direct 3) (reg 16), .copy (.direct 5) (.immediate 0), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code MaskSerialize.algorithm.code
    (SourceChain.code bridge.code MaskSerialize.algorithm.code)), 1, by decide⟩

theorem prepares (s : State w) (destination : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 32 ≤ destination) (fits : destination < 2 ^ w.bits)
    (pointer : s.mem 18 = BitVec.ofNat w.bits destination) :
    let t := run widthConstant (prepare.program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧
    t.mem 1 = s.mem 9 ∧ t.mem 2 = 0#w.bits ∧ t.mem 3 = s.mem 16 ∧
    t.mem 4 = BitVec.ofNat w.bits (destination + 1) ∧ t.mem 5 = 1#w.bits ∧
    t.mem destination = s.mem 17 ∧ (∀ a, 8 ≤ a → a ≠ destination → t.mem a = s.mem a) := by
  have dest : (BitVec.ofNat w.bits destination).toNat = destination := Nat.mod_eq_of_lt fits
  have low : ∀ i, i ≤ 31 → destination ≠ i ∧ i ≠ destination := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, dest, low, Nat.add_assoc]
  constructor
  · rw [← BitVec.ofNat_add]
  · intro a ha hd
    have h : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 ∧ a ≠ 5 := by omega
    simp [h, hd]

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧
      t.mem 1 = s.mem 10 ∧ t.mem 2 = 0#w.bits ∧ t.mem 3 = s.mem 16 ∧ t.mem 5 = 0#w.bits ∧
      (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 3 → a ≠ 5 → t.mem a = s.mem a) := by
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h1 h2 h3 h5; simp [h1, h2, h3, h5]

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

/-- Both literal polarities, including tautologies, are serialized in canonical
order. The output has the exact length prefix required by SAT input encoding. -/
theorem serializes (clause : Clause n) (destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ destination)
    (fits : destination + 1 + 4 * n < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (nodup : clause.Nodup)
    (pos : s.mem 9 = Masks.encode w clause true) (neg : s.mem 10 = Masks.encode w clause false)
    (variables : s.mem 16 = BitVec.ofNat w.bits n) (count : s.mem 17 = BitVec.ofNat w.bits clause.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits destination) :
    ∃ time final, time ≤ 22 * n + 16 ∧ Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination
        (BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)) ∧
      final.mem 4 = BitVec.ofNat w.bits (destination + 1 + 2 * clause.length) ∧
      (∀ a, 8 ≤ a → (a < destination ∨ destination + 1 + 2 * clause.length ≤ a) → final.mem a = s.mem a) := by
  let positive := MaskSerialize.words (Masks.encode w clause true) (1#w.bits) 0 n
  let negative := MaskSerialize.words (Masks.encode w clause false) (0#w.bits) 0 n
  have plen : positive.length ≤ 2 * n := MaskSerialize.length_le _ _ _ _
  have nlen : negative.length ≤ 2 * n := MaskSerialize.length_le _ _ _ _
  have combined : SerializedWords.literals w (Canonical.clause clause) = positive ++ negative :=
    SerializedWords.clause_words clause variablesFit
  have length : positive.length + negative.length = 2 * clause.length := by
    rw [← List.length_append, ← combined, SerializedWords.canonical_length clause nodup]
  let prepared := run widthConstant (prepare.program w) 7 s
  obtain ⟨ph, pt, pp, pi, pn, pd, pol, header, pf⟩ := prepares s destination pc live base (by omega) pointer
  obtain ⟨positiveTime, first, positiveBound, positiveTrace, firstHalt, firstTable, _, _, firstPointer, _, _, firstFrame⟩ :=
    MaskSerialize.serializes (Masks.encode w clause true) (1#w.bits) 0 n (destination + 1)
      (SourceChain.resume prepared) rfl rfl (by omega) (by omega) (by omega)
      (pp.trans pos) pi (pn.trans variables) pd pol
  let middle := run widthConstant (bridge.program w) 5 (SourceChain.resume first)
  obtain ⟨mh, mt, mp, mi, mn, mpol, mf⟩ := bridges (SourceChain.resume first) rfl rfl
  have negativeInput : middle.mem 1 = Masks.encode w clause false :=
    mp.trans ((firstFrame 10 (by decide) (Or.inl (by omega))).trans ((pf 10 (by decide) (by omega)).trans neg))
  have variableCount : middle.mem 3 = BitVec.ofNat w.bits n :=
    mn.trans ((firstFrame 16 (by decide) (Or.inl (by omega))).trans ((pf 16 (by decide) (by omega)).trans variables))
  have nextPointer : middle.mem 4 = BitVec.ofNat w.bits (destination + 1 + positive.length) :=
    (mf 4 (by decide) (by decide) (by decide) (by decide)).trans firstPointer
  obtain ⟨negativeTime, out, negativeBound, negativeTrace, outHalt, secondTable, _, _, outPointer, _, _, secondFrame⟩ :=
    MaskSerialize.serializes (Masks.encode w clause false) (0#w.bits) 0 n (destination + 1 + positive.length)
      (SourceChain.resume middle) rfl rfl (by omega) (by omega) (by omega) negativeInput mi variableCount nextPointer mpol
  have keptFirst : VectorBuilder.Stored out.mem (destination + 1) positive := by
    apply MemoryCopy.stored_frame _ _ firstTable
    intro a ha hb
    exact (secondFrame a (by omega) (Or.inl hb)).trans (mf a (by omega) (by omega) (by omega) (by omega))
  have keptHeader : out.mem destination = BitVec.ofNat w.bits clause.length :=
    (secondFrame destination (by omega) (Or.inl (by omega))).trans
      ((mf destination (by omega) (by omega) (by omega) (by omega)).trans
        ((firstFrame destination (by omega) (Or.inl (by omega))).trans (header.trans count)))
  have table : VectorBuilder.Stored out.mem destination
      (BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)) := by
    rw [Canonical.length_eq clause nodup, combined]
    refine ⟨keptHeader, ?_⟩
    exact (BranchTables.stored_append positive negative out.mem (destination + 1)).mpr ⟨keptFirst, secondTable⟩
  have tail := SourceChain.traces bridge.code MaskSerialize.algorithm.code (SourceChain.resume first) middle out
    5 negativeTime rfl mh (trace_of_ticks _ _ 5 mt) negativeTrace
  have body := SourceChain.traces MaskSerialize.algorithm.code (SourceChain.code bridge.code MaskSerialize.algorithm.code)
    (SourceChain.resume prepared) first (out.relocate bridge.code.length) positiveTime (5 + negativeTime)
    rfl firstHalt positiveTrace tail
  have full := SourceChain.traces prepare.code
    (SourceChain.code MaskSerialize.algorithm.code (SourceChain.code bridge.code MaskSerialize.algorithm.code))
    s prepared ((out.relocate bridge.code.length).relocate MaskSerialize.algorithm.code.length)
    7 (positiveTime + (5 + negativeTime)) live ph (trace_of_ticks _ _ 7 pt) body
  refine ⟨7 + (positiveTime + (5 + negativeTime)),
    ((out.relocate bridge.code.length).relocate MaskSerialize.algorithm.code.length).relocate prepare.code.length,
    by omega, full, outHalt, table, ?_, ?_⟩
  · change out.mem 4 = _
    change out.mem 4 = BitVec.ofNat w.bits (destination + 1 + positive.length + negative.length) at outPointer
    simpa only [Nat.add_assoc, length] using outPointer
  · intro a ha outside
    have firstOutside : a < destination + 1 ∨ destination + 1 + positive.length ≤ a := by omega
    have secondOutside : a < destination + 1 + positive.length ∨
        destination + 1 + positive.length + negative.length ≤ a := by omega
    exact (secondFrame a ha secondOutside).trans
      ((mf a (by omega) (by omega) (by omega) (by omega)).trans
        ((firstFrame a ha firstOutside).trans (pf a ha (by omega))))

end WordRAM.Conjectures.Sparsification.ClauseSerialize

/-! One iteration of the clause-table serializer, including record loads and
persistent input/output cursor updates. -/
namespace WordRAM.Conjectures.Sparsification.SerializeBody
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def prepare : Algorithm :=
  ⟨[.copy (.direct 9) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 10) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 17) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 18) (reg 13), .halt], 1, by decide⟩

def finish : Algorithm :=
  ⟨[.copy (.direct 13) (reg 4), .binary .sub (.direct 11) (reg 11) (.immediate 1), .halt], 1, by decide⟩

def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code ClauseSerialize.algorithm.code finish.code), 1, by decide⟩

theorem prepares (s : State w) (source : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 32 ≤ source) (fits : source + 2 < 2 ^ w.bits)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source) :
    let t := run widthConstant (prepare.program w) 8 s
    t.halted = true ∧ t.ticks = s.ticks + 8 ∧
      t.mem 9 = s.mem source ∧ t.mem 10 = s.mem (source + 1) ∧ t.mem 17 = s.mem (source + 2) ∧
      t.mem 12 = BitVec.ofNat w.bits (source + 3) ∧ t.mem 18 = s.mem 13 ∧
      (∀ a, a ≠ 9 → a ≠ 10 → a ≠ 12 → a ≠ 17 → a ≠ 18 → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits source).toNat = source := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits source + 1#w.bits).toNat = source + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt (by omega)
  have d2 : (BitVec.ofNat w.bits source + 1#w.bits + 1#w.bits).toNat = source + 2 := by
    rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low1 : ∀ i, i ≤ 31 → source + 1 ≠ i := by omega
  have low2 : ∀ i, i ≤ 31 → source + 2 ≠ i := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, d0, d1, d2, low1, low2,
    Nat.add_assoc, -BitVec.toNat_add]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h9 h10 h12 h17 h18; simp [h9, h10, h12, h17, h18]

theorem finishes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (finish.program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 13 = s.mem 4 ∧ t.mem 11 = s.mem 11 - 1#w.bits ∧
      (∀ a, a ≠ 11 → a ≠ 13 → t.mem a = s.mem a) := by
  simp [finish, 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 h11 h13; simp [h11, h13]

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 serializes (clause : Clause n) (rest : CNF n) (source destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ source)
    (before : source + 3 * (clause :: rest).length ≤ destination)
    (fits : destination + 1 + 4 * n < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (nodup : clause.Nodup)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w (clause :: rest)))
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits (rest.length + 1))
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (output : s.mem 13 = BitVec.ofNat w.bits destination) :
    ∃ time final, time ≤ 22 * n + 27 ∧ Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination
        (BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)) ∧
      VectorBuilder.Stored final.mem (source + 3) (RecordTable.words w rest) ∧
      final.mem 11 = BitVec.ofNat w.bits rest.length ∧ final.mem 12 = BitVec.ofNat w.bits (source + 3) ∧
      final.mem 13 = BitVec.ofNat w.bits (destination + 1 + 2 * clause.length) ∧
      final.mem 16 = BitVec.ofNat w.bits n ∧
      (∀ a, 32 ≤ a → (a < destination ∨ destination + 1 + 2 * clause.length ≤ a) → final.mem a = s.mem a) := by
  have sourceEnd : source + 3 ≤ destination := by simp only [List.length_cons] at before; omega
  let prepared := run widthConstant (prepare.program w) 8 s
  obtain ⟨ph, pt, pp, pn, plen, pcursor, pd, pf⟩ := prepares s source pc live base (by omega) pointer
  rcases input with ⟨ip, ine, ilen, tail⟩
  have preparedCount : prepared.mem 17 = BitVec.ofNat w.bits clause.length := by
    rw [Normalize.clean_eq clause nodup] at ilen
    exact plen.trans ilen
  obtain ⟨time, out, bound, trace, halted, table, cursor, frame⟩ :=
    ClauseSerialize.serializes clause destination (SourceChain.resume prepared) rfl rfl (by omega) fits variablesFit nodup
      (pp.trans ip) (pn.trans ine) ((pf 16 (by decide) (by decide) (by decide) (by decide) (by decide)).trans variables)
      preparedCount (pd.trans output)
  let final := run widthConstant (finish.program w) 3 (SourceChain.resume out)
  obtain ⟨fh, ft, fp, fc, ff⟩ := finishes (SourceChain.resume out) rfl rfl
  have old (a : Nat) (ha : 32 ≤ a) (outside : a < destination ∨ destination + 1 + 2 * clause.length ≤ a) :
      final.mem a = s.mem a :=
    (ff a (by omega) (by omega)).trans ((frame a (by omega) outside).trans
      (pf a (by omega) (by omega) (by omega) (by omega) (by omega)))
  have finalTable : VectorBuilder.Stored final.mem destination
      (BitVec.ofNat w.bits (Canonical.clause clause).length :: SerializedWords.literals w (Canonical.clause clause)) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact ff a (by omega) (by omega)
  have restTable : VectorBuilder.Stored final.mem (source + 3) (RecordTable.words w rest) := by
    apply MemoryCopy.stored_frame _ _ (show VectorBuilder.Stored s.mem (source + 3) (RecordTable.words w rest) from tail)
    intro a ha hb
    rw [RecordTable.words_length] at hb
    apply old a (by omega) (Or.inl (by simp only [List.length_cons] at before; omega))
  have remaining : final.mem 11 = BitVec.ofNat w.bits rest.length := by
    have kept := (frame 11 (by decide) (Or.inl (by omega))).trans
      ((pf 11 (by decide) (by decide) (by decide) (by decide) (by decide)).trans count)
    change final.mem 11 = out.mem 11 - 1#w.bits at fc
    rw [fc, kept, BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by simp only [List.length_cons] at before; omega)]
    simp
  have inputCursor : final.mem 12 = BitVec.ofNat w.bits (source + 3) :=
    (ff 12 (by decide) (by decide)).trans ((frame 12 (by decide) (Or.inl (by omega))).trans pcursor)
  have keptVariables : final.mem 16 = BitVec.ofNat w.bits n :=
    (ff 16 (by decide) (by decide)).trans ((frame 16 (by decide) (Or.inl (by omega))).trans
      ((pf 16 (by decide) (by decide) (by decide) (by decide) (by decide)).trans variables))
  have tailTrace := SourceChain.traces ClauseSerialize.algorithm.code finish.code (SourceChain.resume prepared)
    out final time 3 rfl halted trace (trace_of_ticks _ _ 3 ft)
  have full := SourceChain.traces prepare.code (SourceChain.code ClauseSerialize.algorithm.code finish.code)
    s prepared (final.relocate ClauseSerialize.algorithm.code.length) 8 (time + 3) live ph (trace_of_ticks _ _ 8 pt) tailTrace
  exact ⟨8 + (time + 3), (final.relocate ClauseSerialize.algorithm.code.length).relocate prepare.code.length,
    by omega, full, fh, finalTable, restTable, remaining, inputCursor, fp.trans cursor, keptVariables, old⟩

end WordRAM.Conjectures.Sparsification.SerializeBody