SETH ⇒ OVC sparsification bundle 2: 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_01

set_option autoImplicit true

/-! A uniform mask-construction loop over the literal-pair encoding. -/
namespace WordRAM.Conjectures.MaskBuilder

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

/-- Cells 1 and 2 hold the input pointer and remaining literal count; cells
3 and 4 accumulate positive and negative masks. Cells 5, 6, 7 are scratch.
The input consists of consecutive (variable index, polarity) pairs at addresses
at least 8. A zero polarity denotes a negative literal. -/
def algorithm : Algorithm :=
  ⟨[.branch .eq (reg 2) (.immediate 0) 12,
    .copy (.direct 5) (.memory (.indirect 1)),
    .binary .add (.direct 1) (reg 1) (.immediate 1),
    .copy (.direct 6) (.memory (.indirect 1)),
    .binary .add (.direct 1) (reg 1) (.immediate 1),
    .binary .sub (.direct 2) (reg 2) (.immediate 1),
    .binary .shl (.direct 7) (.immediate 1) (reg 5),
    .branch .eq (reg 6) (.immediate 0) 10,
    .binary .bor (.direct 3) (reg 3) (reg 7),
    .jump 0,
    .binary .bor (.direct 4) (reg 4) (reg 7),
    .jump 0,
    .halt], 1, by decide⟩

/-- An iteration reads precisely the two input cells and returns to the loop
header after ten instructions. This statement permits arbitrary bit patterns
in the index and polarity input words. -/
theorem iteration (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 2 ≠ 0#w.bits)
    (_ptr : 8 ≤ (s.mem 1).toNat)
    (nextPtr : 8 ≤ (s.mem 1 + 1#w.bits).toNat) :
    let t := run widthConstant (algorithm.program w) 10 s
    let index := s.mem (s.mem 1).toNat
    let polarity := s.mem (s.mem 1 + 1#w.bits).toNat
    let bit : Word w := 1#w.bits <<< index.toNat
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 10 ∧
    t.mem 1 = s.mem 1 + 1#w.bits + 1#w.bits ∧ t.mem 2 = s.mem 2 - 1 ∧
    t.mem 3 = (if polarity = 0 then s.mem 3 else s.mem 3 ||| bit) ∧
    t.mem 4 = (if polarity = 0 then s.mem 4 ||| bit else s.mem 4) ∧
    (∀ a, 8 ≤ a → t.mem a = s.mem a) := by
  have h5 : (s.mem 1 + 1#w.bits).toNat ≠ 5 := by omega
  have h6 : (s.mem 1 + 1#w.bits).toNat ≠ 1 := by omega
  by_cases hp : s.mem (s.mem 1 + 1#w.bits).toNat = 0#w.bits
  all_goals
    simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
      reg, run, step, execute, Operand.read, Address.resolve, Memory.write,
      BinOp.eval, Comparison.test, pc, live, nonzero, h5, h6,
      hp, Nat.add_assoc, -BitVec.toNat_add]
    intro a ha
    have : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 ∧ a ≠ 5 ∧ a ≠ 6 ∧ a ≠ 7 := by omega
    simp_all

/-- Empty input takes the exit branch followed by halt. -/
theorem exit_loop (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (empty : s.mem 2 = 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, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Operand.read, Address.resolve,
    BinOp.eval, Comparison.test, pc, live, empty, Nat.add_assoc]

/-- Representation of a list of literal words in consecutive memory cells. -/
def Encoded (mem : Memory w) (address : Nat) : List (Word w × Word w) → Prop
  | [] => True
  | (index, polarity) :: xs =>
      mem address = index ∧ mem (address + 1) = polarity ∧ Encoded mem (address + 2) xs

def update (masks : Word w × Word w) (literal : Word w × Word w) : Word w × Word w :=
  let bit := 1#w.bits <<< literal.1.toNat
  if literal.2 = 0 then (masks.1, masks.2 ||| bit)
  else (masks.1 ||| bit, masks.2)

theorem Encoded.frame (xs : List (Word w × Word w)) (address : Nat)
    (ha : 8 ≤ address) (h : Encoded mem address xs)
    (frame : ∀ a, 8 ≤ a → other a = mem a) : Encoded other address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    exact ⟨(frame address ha).trans h.1,
      (frame (address + 1) (by omega)).trans h.2.1,
      ih (address + 2) (by omega) h.2.2⟩

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 ⟨t, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) fuel s
  have hc := runs_cost trace
  have : t = fuel := by omega
  subst t
  exact trace

/-- The complete loop processes an arbitrary length input. Pointer arithmetic
cannot wrap under `fits`. Its cost is exactly ten instructions per literal plus
two for exit, and all input cells are preserved. No input-dependent code is used. -/
theorem builds (xs : List (Word w × Word w)) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 8 ≤ address)
    (fits : address + 2 * xs.length < 2 ^ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (count : s.mem 2 = BitVec.ofNat w.bits xs.length)
    (input : Encoded s.mem address xs) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) (10 * xs.length + 2) s final ∧
      final.halted = true ∧
      (final.mem 3, final.mem 4) = xs.foldl update (s.mem 3, s.mem 4) ∧
      (∀ a, 8 ≤ a → final.mem a = s.mem a) := by
  induction xs generalizing s address with
  | nil =>
    have empty : s.mem 2 = 0#w.bits := by simpa using count
    have he := exit_loop s pc live empty
    refine ⟨run widthConstant (algorithm.program w) 2 s,
      trace_of_ticks s 2 he.2.2, he.1, ?_, ?_⟩
    · simp [he.2.1]
    · intro a _; exact congrFun he.2.1 a
  | cons x xs ih =>
    have addrFit : address < 2 ^ w.bits := by simp only [List.length_cons] at fits; omega
    have nextFit : address + 1 < 2 ^ w.bits := by simp only [List.length_cons] at fits; omega
    have countFit : xs.length + 1 < 2 ^ w.bits := by simp only [List.length_cons] at fits; omega
    have pn : (s.mem 1).toNat = address := by simp [pointer, Nat.mod_eq_of_lt addrFit]
    have pn1 : (s.mem 1 + 1#w.bits).toNat = address + 1 := by
      rw [pointer, ← BitVec.ofNat_add]
      exact Nat.mod_eq_of_lt nextFit
    have cn : (s.mem 2).toNat = xs.length + 1 := by simp [count, Nat.mod_eq_of_lt countFit]
    have nz : s.mem 2 ≠ 0#w.bits := by intro h; simp [h] at cn
    let t := run widthConstant (algorithm.program w) 10 s
    have it := iteration s pc live nz (by omega) (by omega)
    rcases it with ⟨tpc, tlive, tticks, tp, tc, tpos, tneg, frame⟩
    have tp' : t.mem 1 = BitVec.ofNat w.bits (address + 2) := by
      rw [tp, pointer, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
    have tc' : t.mem 2 = BitVec.ofNat w.bits xs.length := by
      rw [tc, count]
      change BitVec.ofNat w.bits (xs.length + 1) - BitVec.ofNat w.bits 1 = _
      rw [BitVec.ofNat_sub_ofNat_of_le  _ _ (by omega) (by omega)]
      simp
    have masks : (t.mem 3, t.mem 4) = update (s.mem 3, s.mem 4) x := by
      rw [pn, pn1, input.1, input.2.1] at tpos tneg
      simp only [t, tpos, tneg, update]
      split <;> rfl
    obtain ⟨final, trace, halted, result, preserved⟩ := ih t (address + 2) tpc tlive
      (by omega) (by simp only [List.length_cons] at fits; omega) tp' tc'
      (Encoded.frame xs (address + 2) (by omega) input.2.2 frame)
    refine ⟨final, ?_, halted, ?_, ?_⟩
    · have tr := (trace_of_ticks s 10 tticks).append trace
      simpa [Nat.mul_add, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using tr
    · simpa only [List.foldl_cons, masks] using result
    · intro a ha; exact (preserved a ha).trans (frame a ha)

/-- The exact word representation of SATInstance.encode's literal pairs. -/
def wordLiteral (w : Width) (l : Literal n) : Word w × Word w :=
  (BitVec.ofNat w.bits l.index.val, if l.positive then 1 else 0)

theorem mask_nil (w : Width) (polarity : Bool) :
    ClauseMasks.mask w (fun _ : Fin n => true) [] polarity = 0 := by
  apply BitVec.eq_of_getLsbD_eq
  intro i hi
  simp [ClauseMasks.mask, Reduction.pack_bit _ _ hi]

theorem mask_cons (w : Width) (l : Literal n) (xs : List (Literal n)) (polarity : Bool) :
    ClauseMasks.mask w (fun _ => true) (l :: xs) polarity =
      (if l.positive = polarity then BitVec.twoPow w.bits l.index.val else 0) |||
        ClauseMasks.mask w (fun _ => true) xs polarity := by
  apply BitVec.eq_of_getLsbD_eq
  intro i hi
  by_cases hp : l.positive = polarity
  · simp only [hp, ↓reduceIte, BitVec.getLsbD_or, ClauseMasks.mask,
      Reduction.pack_bit _ _ hi, BitVec.getLsbD_twoPow]
    by_cases he : l.index.val = i
    · simp [hp, he, hi]
    · simp [hp, he]
  · simp only [hp, ↓reduceIte, BitVec.getLsbD_or, ClauseMasks.mask,
      Reduction.pack_bit _ _ hi]
    simp [hp]

/-- The loop's fold equals the masks used in the SAT-to-OV reduction, with
arbitrary initial accumulators. This also covers duplicate literals. -/
theorem fold_masks (xs : List (Literal n)) (fits : n ≤ w.bits)
    (positive negative : Word w) :
    ((xs.map (wordLiteral w)).foldl update (positive, negative)) =
      (positive ||| ClauseMasks.mask w (fun _ => true) xs true,
       negative ||| ClauseMasks.mask w (fun _ => true) xs false) := by
  induction xs generalizing positive negative with
  | nil => simp [mask_nil]
  | cons l xs ih =>
    have indexFit : l.index.val < 2 ^ w.bits :=
      Nat.lt_trans (Nat.lt_of_lt_of_le l.index.isLt fits) (Nat.lt_pow_self (by decide))
    have oneNonzero : (1#w.bits) ≠ 0#w.bits := by
      have : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by have := w.positive; omega)
      intro h
      have hn := congrArg BitVec.toNat h
      simp [Nat.mod_eq_of_lt this] at hn
    simp only [List.map_cons, List.foldl_cons]
    cases hp : l.positive <;>
      simp [wordLiteral, update, hp, oneNonzero,
        Nat.mod_eq_of_lt indexFit, ih, mask_cons, BitVec.twoPow, BitVec.or_assoc]

/-- The ordinary consecutive-word representation used by the loop. -/
def flatWords (xs : List (Word w × Word w)) : List (Word w) :=
  xs.flatMap fun x => [x.1, x.2]

theorem flatWords_length (xs : List (Word w × Word w)) :
    (flatWords xs).length = 2 * xs.length := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    simp only [flatWords, List.flatMap_cons, List.length_append,
      List.length_cons, List.length_nil] at ih ⊢
    omega

/-- Connect the recursive memory invariant to ordinary array indexing. -/
theorem encoded_of_flatWords (xs : List (Word w × Word w)) (address : Nat)
    (h : ∀ i, i < (flatWords xs).length →
      mem (address + i) = ((flatWords xs)[i]?).getD 0) :
    Encoded mem address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    refine ⟨?_, ?_, ?_⟩
    · simpa [flatWords] using h 0 (by simp [flatWords])
    · simpa [flatWords] using h 1 (by simp [flatWords])
    · apply ih (address + 2)
      intro i hi
      have bound : i + 2 < (flatWords (x :: xs)).length := by
        simp only [flatWords, List.flatMap_cons, List.length_append, List.length_cons,
          List.length_nil] at hi ⊢
        omega
      have hh := h (i + 2) bound
      simpa [flatWords, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hh

/-- Flat mask-builder input is exactly the literal segment of SATInstance.encode,
converted word by word, with the same polarity convention. -/
theorem flatWords_literals (clause : List (Literal n)) :
    flatWords (clause.map (wordLiteral w)) =
      (clause.flatMap fun l => [l.index.val, if l.positive then 1 else 0]).map
        (BitVec.ofNat w.bits) := by
  induction clause with
  | nil => rfl
  | cons l xs ih =>
    cases hp : l.positive <;> simpa [flatWords, wordLiteral, hp] using
      congrArg (fun tail => BitVec.ofNat w.bits l.index.val ::
        (if l.positive then (1 : Word w) else 0) :: tail) ih

/-- From zero accumulators the actual loop constructs precisely the two
mathematical clause masks, with an exact linear running-time bound. -/
theorem builds_clause (clause : List (Literal n)) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 8 ≤ address)
    (fits : address + 2 * clause.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (count : s.mem 2 = BitVec.ofNat w.bits clause.length)
    (positive : s.mem 3 = 0) (negative : s.mem 4 = 0)
    (input : Encoded s.mem address (clause.map (wordLiteral w))) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) (10 * clause.length + 2) s final ∧
      final.halted = true ∧
      final.mem 3 = ClauseMasks.mask w (fun _ => true) clause true ∧
      final.mem 4 = ClauseMasks.mask w (fun _ => true) clause false ∧
      (∀ a, 8 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨final, trace, halted, masks, frame⟩ := builds (clause.map (wordLiteral w)) s address
    pc live base (by simpa using fits) pointer (by simpa using count) input
  rw [fold_masks clause variablesFit, positive, negative] at masks
  simp only [Prod.mk.injEq] at masks
  simp at masks
  exact ⟨final, by simpa using trace, halted, masks.1, masks.2, frame⟩

/-- The standalone source program clears both accumulators before entering
the loop. The input pointer and count are the only register inputs. -/
def initialized : Algorithm :=
  ⟨[.copy (.direct 3) (.immediate 0), .copy (.direct 4) (.immediate 0)] ++
    algorithm.code.map (SourceInstruction.relocate 2), 1, by decide⟩

private theorem initialized_program (w : Width) :
    initialized.program w =
      ([.copy (.direct 3) (.immediate 0), .copy (.direct 4) (.immediate 0)] :
        Program w .multiplication 1) ++
      (algorithm.program w).map (Instruction.relocate 2) := by
  rfl

/-- End-to-end mask construction from encoded literal pairs. Arbitrary initial
scratch and accumulator contents are allowed. The program's source is fixed
for every width, clause length, and input formula. -/
theorem initialized_builds_clause (clause : List (Literal n)) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 8 ≤ address)
    (fits : address + 2 * clause.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (count : s.mem 2 = BitVec.ofNat w.bits clause.length)
    (input : Encoded s.mem address (clause.map (wordLiteral w))) :
    ∃ final : State w,
      Runs widthConstant (initialized.program w) (10 * clause.length + 4) s final ∧
      final.halted = true ∧
      final.mem 3 = ClauseMasks.mask w (fun _ => true) clause true ∧
      final.mem 4 = ClauseMasks.mask w (fun _ => true) clause false ∧
      (∀ a, 8 ≤ a → final.mem a = s.mem a) := by
  let entry : State w :=
    { mem := (s.mem.write 3 0).write 4 0, pc := 0, ticks := s.ticks + 2 }
  have frame : ∀ a, 8 ≤ a → entry.mem a = s.mem a := by
    intro a ha
    have : a ≠ 3 ∧ a ≠ 4 := by omega
    simp [entry, Memory.write, this.1, this.2]
  have init : Runs widthConstant (initialized.program w) 2 s (entry.relocate 2) := by
    apply Runs.cons (t := execute widthConstant (.copy (.direct 3) (.immediate 0)) s)
    · simp [step, initialized_program, pc, live]
      rfl
    apply Runs.cons (t := entry.relocate 2)
    · simp [step, initialized_program, execute, pc, live, entry, State.relocate,
        Operand.read, Address.resolve, Nat.add_assoc]
    · exact Runs.refl _
  obtain ⟨final, trace, halted, pos, neg, preserved⟩ := builds_clause clause entry address
    rfl rfl base fits variablesFit (by simpa [entry, Memory.write] using pointer)
    (by simpa [entry, Memory.write] using count)
    (by simp [entry, Memory.write]) (by simp [entry, Memory.write])
    (Encoded.frame _ _ base input frame)
  have embedded : EmbedsAt (algorithm.program w) (initialized.program w) 2 := by
    rw [initialized_program]
    simpa using embeds_append
      ([.copy (.direct 3) (.immediate 0), .copy (.direct 4) (.immediate 0)] :
        Program w .multiplication 1) (algorithm.program w) []
  refine ⟨final.relocate 2, ?_, halted, pos, neg, ?_⟩
  · have tr := init.append (trace.relocate embedded)
    have eqCost : 2 + (10 * clause.length + 2) = 10 * clause.length + 4 := by omega
    rw [eqCost] at tr
    exact tr
  · intro a ha; exact (preserved a ha).trans (frame a ha)

end WordRAM.Conjectures.MaskBuilder

/-! A fixed program for writing a whole clause vector from a mask table. -/
namespace WordRAM.Conjectures.VectorBuilder

/-- Consecutive output words, including the empty vector. -/
def Stored (mem : Memory w) (address : Nat) : List (Word w) → Prop
  | [] => True
  | x :: xs => mem address = x ∧ Stored mem (address + 1) xs

/-- Reading the vector back at any valid coordinate gives the stored word. -/
theorem Stored.get (xs : List (Word w)) (address : Nat) (h : Stored mem address xs)
    (i : Nat) (hi : i < xs.length) : mem (address + i) = xs[i] := by
  induction xs generalizing address i with
  | nil => simp at hi
  | cons x xs ih =>
    cases i with
    | zero => simpa using h.1
    | succ i =>
      simpa [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using
        ih (address + 1) h.2 i (by simpa using hi)

end WordRAM.Conjectures.VectorBuilder