SETH ⇒ OVC sparsification bundle 3: 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_02

set_option autoImplicit true

/-! A uniform loop over length-prefixed clauses. -/
namespace WordRAM.Conjectures.MaskTable

/-- Number of input words occupied by a length-prefixed clause sequence. -/
def span : List (List (Literal n)) → Nat
  | [] => 0
  | clause :: rest => 1 + 2 * clause.length + span rest

/-- Actual clause-list encoding, without the instance's two-word header. -/
def Encoded (mem : Memory w) (address : Nat) : List (List (Literal n)) → Prop
  | [] => True
  | clause :: rest =>
      mem address = BitVec.ofNat w.bits clause.length ∧
      MaskBuilder.Encoded mem (address + 1) (clause.map (MaskBuilder.wordLiteral w)) ∧
      Encoded mem (address + 1 + 2 * clause.length) rest

theorem pair_frame (xs : List (Word w × Word w)) (address : Nat)
    (input : MaskBuilder.Encoded mem address xs)
    (frame : ∀ a, address ≤ a → a < address + 2 * xs.length → other a = mem a) :
    MaskBuilder.Encoded other address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    refine ⟨(frame address (by omega) (by simp <;> omega)).trans input.1,
      (frame (address + 1) (by omega) (by simp <;> omega)).trans input.2.1, ?_⟩
    apply ih (address + 2) input.2.2
    intro a lo hi
    apply frame a (by omega)
    simp only [List.length_cons]
    omega

theorem Encoded.frame (clauses : List (List (Literal n))) (address : Nat)
    (input : Encoded mem address clauses)
    (frame : ∀ a, address ≤ a → a < address + span clauses → other a = mem a) :
    Encoded other address clauses := by
  induction clauses generalizing address with
  | nil => trivial
  | cons clause rest ih =>
    refine ⟨(frame address (by omega) (by simp [span]; omega)).trans input.1, ?_, ?_⟩
    · apply pair_frame _ _ input.2.1
      intro a lo hi
      apply frame a (by omega)
      simp only [List.length_map] at hi
      simp only [span]
      omega
    · apply ih _ input.2.2
      intro a lo hi
      apply frame a (by omega)
      simp only [span]
      omega

theorem span_eq (clauses : List (List (Literal n))) :
    span clauses = clauses.length + 2 * (clauses.map List.length).sum := by
  induction clauses with
  | nil => rfl
  | cons clause rest ih =>
    simp only [span, List.map_cons, List.sum_cons, List.length_cons, ih, Nat.mul_add]
    omega

/-- Clause input serialized as machine words, in the same order as SATInstance.encode. -/
def words (w : Width) : List (List (Literal n)) → List (Word w)
  | [] => []
  | clause :: rest => BitVec.ofNat w.bits clause.length ::
      (MaskBuilder.flatWords (clause.map (MaskBuilder.wordLiteral w)) ++ words w rest)

theorem words_length (w : Width) (clauses : List (List (Literal n))) :
    (words w clauses).length = span clauses := by
  induction clauses with
  | nil => rfl
  | cons clause rest ih =>
    simp only [words, List.length_cons, List.length_append, MaskBuilder.flatWords_length,
      List.length_map, ih, span]
    omega

theorem words_encode (w : Width) (f : SATInstance) :
    (BitVec.ofNat w.bits f.variables :: BitVec.ofNat w.bits f.clauses.length :: words w f.clauses) =
      f.encode.map (BitVec.ofNat w.bits) := by
  have clausesEq (clauses : List (List (Literal f.variables))) :
      words w clauses = (clauses.flatMap fun clause => clause.length ::
        clause.flatMap fun l => [l.index.val, if l.positive then 1 else 0]).map (BitVec.ofNat w.bits) := by
    induction clauses with
    | nil => rfl
    | cons clause rest ih =>
      simp only [words, List.flatMap_cons, List.map_append, List.map_cons,
        List.cons_append, MaskBuilder.flatWords_literals, ih]
  simpa [SATInstance.encode] using congrArg
    (fun tail => BitVec.ofNat w.bits f.variables :: BitVec.ofNat w.bits f.clauses.length :: tail)
    (clausesEq f.clauses)

/-- Establish the clause-loop input invariant directly from the serialized array. -/
theorem encoded_of_words (clauses : List (List (Literal n))) (address : Nat)
    (h : ∀ i, i < (words w clauses).length →
      mem (address + i) = ((words w clauses)[i]?).getD 0) :
    Encoded mem address clauses := by
  induction clauses generalizing address with
  | nil => trivial
  | cons clause rest ih =>
    have literalLength : (MaskBuilder.flatWords (clause.map (MaskBuilder.wordLiteral w))).length =
        2 * clause.length := by simp [MaskBuilder.flatWords_length]
    refine ⟨?_, ?_, ?_⟩
    · simpa [words, List.getElem?_cons_zero] using h 0 (by simp [words])
    · apply MaskBuilder.encoded_of_flatWords
      intro i hi
      have hh := h (i + 1) (by simp only [words, List.length_cons, List.length_append]; omega)
      simp only [words, List.getElem?_cons_succ, List.getElem?_append_left hi] at hh
      simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hh
    · apply ih (address + 1 + 2 * clause.length)
      intro i hi
      have hh := h (2 * clause.length + i + 1)
        (by simp only [words, List.length_cons, List.length_append]; omega)
      simp only [words, List.getElem?_cons_succ] at hh
      rw [List.getElem?_append_right (by omega)] at hh
      rw [literalLength, Nat.add_sub_cancel_left] at hh
      simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using hh

end WordRAM.Conjectures.MaskTable

/-! Uniform copying of a consecutive input buffer to disjoint higher memory. -/
namespace WordRAM.Conjectures.MemoryCopy

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

/-- Registers 1=source, 2=destination, 3=count, 4=scratch. -/
def algorithm : Algorithm :=
  ⟨[.branch .eq (reg 3) (.immediate 0) 7,
    .copy (.direct 4) (.memory (.indirect 1)),
    .copy (.indirect 2) (reg 4),
    .binary .add (.direct 1) (reg 1) (.immediate 1),
    .binary .add (.direct 2) (reg 2) (.immediate 1),
    .binary .sub (.direct 3) (reg 3) (.immediate 1),
    .jump 0, .halt], 1, by decide⟩

theorem iteration (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 3 ≠ 0#w.bits) (base : 5 ≤ (s.mem 2).toNat) :
    let t := run widthConstant (algorithm.program w) 7 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 7 ∧
    t.mem 1 = s.mem 1 + 1#w.bits ∧ t.mem 2 = s.mem 2 + 1#w.bits ∧
    t.mem 3 = s.mem 3 - 1#w.bits ∧
    t.mem (s.mem 2).toNat = s.mem (s.mem 1).toNat ∧
    (∀ a, 5 ≤ a → a ≠ (s.mem 2).toNat → t.mem a = s.mem a) := by
  have d1 : (s.mem 2).toNat ≠ 1 ∧ 1 ≠ (s.mem 2).toNat := by omega
  have d2 : (s.mem 2).toNat ≠ 2 ∧ 2 ≠ (s.mem 2).toNat := by omega
  have d3 : (s.mem 2).toNat ≠ 3 ∧ 3 ≠ (s.mem 2).toNat := 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, d1, d2, d3, Nat.add_assoc, -BitVec.toNat_add]
  intro a ha hd
  have : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 := by omega
  simp_all

theorem exits (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (empty : s.mem 3 = 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, Address.resolve, Operand.read, Comparison.test,
    pc, live, empty, Nat.add_assoc]

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

theorem stored_frame (xs : List (Word w)) (address : Nat)
    (h : VectorBuilder.Stored mem address xs)
    (frame : ∀ a, address ≤ a → a < address + xs.length → other a = mem a) :
    VectorBuilder.Stored other address xs := by
  induction xs generalizing address with
  | nil => trivial
  | cons x xs ih =>
    refine ⟨(frame address (by omega) (by simp)).trans h.1, ?_⟩
    apply ih (address + 1) h.2
    intro a lo hi
    apply frame a (by omega)
    simp only [List.length_cons]
    omega

/-- Exact linear-time buffer copying, including preservation of the source.
The destination begins after the source, and all pointers remain representable. -/
theorem copies (xs : List (Word w)) (s : State w) (source destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 5 ≤ source)
    (separate : source + xs.length ≤ destination)
    (fits : destination + xs.length < 2 ^ w.bits)
    (sp : s.mem 1 = BitVec.ofNat w.bits source)
    (dp : s.mem 2 = BitVec.ofNat w.bits destination)
    (count : s.mem 3 = BitVec.ofNat w.bits xs.length)
    (input : VectorBuilder.Stored s.mem source xs) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) (7 * xs.length + 2) s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination xs ∧
      (∀ a, 5 ≤ a → (a < destination ∨ destination + xs.length ≤ a) → final.mem a = s.mem a) := by
  induction xs generalizing s source destination with
  | nil =>
    have empty : s.mem 3 = 0#w.bits := by simpa using count
    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 x xs ih =>
    have sourceFit : source < 2 ^ w.bits := by omega
    have destFit : destination < 2 ^ w.bits := by omega
    have countFit : xs.length + 1 < 2 ^ w.bits := by simp only [List.length_cons] at fits; omega
    have sn : (s.mem 1).toNat = source := by simp [sp, Nat.mod_eq_of_lt sourceFit]
    have dn : (s.mem 2).toNat = destination := by simp [dp, Nat.mod_eq_of_lt destFit]
    have nz : s.mem 3 ≠ 0#w.bits := by
      intro h
      have hn := congrArg BitVec.toNat h
      simp [count, Nat.mod_eq_of_lt countFit] at hn
    have stepInfo := iteration s pc live nz (by omega)
    rw [sn, dn, input.1] at stepInfo
    obtain ⟨npc, nlive, ticks, ns, nd, nc, written, frame⟩ := stepInfo
    let next := run widthConstant (algorithm.program w) 7 s
    have ns' : next.mem 1 = BitVec.ofNat w.bits (source + 1) := by rw [ns, sp, ← BitVec.ofNat_add]
    have nd' : next.mem 2 = BitVec.ofNat w.bits (destination + 1) := by rw [nd, dp, ← BitVec.ofNat_add]
    have nc' : next.mem 3 = BitVec.ofNat w.bits xs.length := by
      rw [nc, 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 tailInput : VectorBuilder.Stored next.mem (source + 1) xs := by
      apply stored_frame _ _ input.2
      intro a lo hi
      apply frame a (by omega)
      simp only [List.length_cons] at separate
      omega
    obtain ⟨final, trace, halted, output, preserved⟩ :=
      ih next (source + 1) (destination + 1) npc nlive (by omega)
        (by simp only [List.length_cons] at separate; omega)
        (by simp only [List.length_cons] at fits; omega) ns' nd' nc' tailInput
    refine ⟨final, ?_, halted, ⟨?_, output⟩, ?_⟩
    · have tr := (trace_of_ticks s 7 ticks).append trace
      have cost : 7 + (7 * xs.length + 2) = 7 * (x :: xs).length + 2 := by simp; omega
      rw [cost] at tr
      exact tr
    · exact (preserved destination (by omega) (Or.inl (by omega))).trans written
    · intro a ha outside
      simp only [List.length_cons] at outside
      exact (preserved a ha (by omega)).trans (frame a ha (by omega))

end WordRAM.Conjectures.MemoryCopy

/-! Fixed straight-line saving of low input cells, using cell zero alone. -/
namespace WordRAM.Conjectures.SavePrefix

/-- This is a family of finite source blocks. Bootstrap uses the single fixed
member `code 1 15`; its length never depends on the input. -/
def code (first : Nat) : Nat → List SourceInstruction
  | 0 => [.halt]
  | count + 1 =>
      .copy (.indirect 0) (.memory (.direct first)) ::
      .binary .add (.direct 0) (.memory (.direct 0)) (.immediate 1) ::
      code (first + 1) count

def program (w : Width) (first count : Nat) : Program w .multiplication 1 :=
  (code first count).map (SourceInstruction.compile w)

theorem relocated (w : Width) (first count offset : Nat) :
    (program w first count).map (Instruction.relocate offset) = program w first count := by
  induction count generalizing first with
  | zero => rfl
  | succ count ih =>
    simp only [program, code, List.map_cons, SourceInstruction.compile, SourceOperand.compile,
      Instruction.relocate] at ih ⊢
    exact congrArg (fun tail =>
      Instruction.copy (.indirect 0) (.memory (.direct first)) ::
      Instruction.binary .add (.direct 0) (.memory (.direct 0)) (.immediate 1) :: tail)
      (ih (first + 1))

/-- Saves a fixed prefix without touching any source cell. The only working
register is cell zero, which is outside the initial input representation. -/
theorem saves (count first destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (sourcePositive : 1 ≤ first)
    (separate : first + count ≤ destination)
    (fits : destination + count < 2 ^ w.bits)
    (pointer : s.mem 0 = BitVec.ofNat w.bits destination) :
    ∃ final : State w,
      Runs widthConstant (program w first count) (2 * count + 1) s final ∧
      final.halted = true ∧ final.mem 0 = BitVec.ofNat w.bits (destination + count) ∧
      (∀ i, i < count → final.mem (destination + i) = s.mem (first + i)) ∧
      (∀ a, a ≠ 0 → (a < destination ∨ destination + count ≤ a) → final.mem a = s.mem a) := by
  induction count generalizing first destination s with
  | zero =>
    let final := execute (m := .multiplication) widthConstant (.halt : Instruction w .multiplication 1) s
    refine ⟨final, ?_, rfl, ?_, ?_, ?_⟩
    · apply runs_instruction
      · exact live
      · simp [program, code, pc, SourceInstruction.compile]
    · simpa [final, execute] using pointer
    · intro i hi; omega
    · intro a _ _; rfl
  | succ count ih =>
    have dn : (s.mem 0).toNat = destination := by
      rw [pointer]; exact Nat.mod_eq_of_lt (by omega)
    have d0 : destination ≠ 0 := by omega
    let next : State w :=
      { mem := (s.mem.write destination (s.mem first)).write 0 (BitVec.ofNat w.bits (destination + 1)),
        ticks := s.ticks + 2 }
    have head : Runs widthConstant (program w first (count + 1)) 2 s (next.relocate 2) := by
      apply Runs.cons (t := execute (m := .multiplication) widthConstant (.copy (.indirect 0) (.memory (.direct first))) s)
      · simp [step, program, code, SourceInstruction.compile, SourceOperand.compile, pc, live]
      apply Runs.cons (t := next.relocate 2)
      · simp [step, program, code, SourceInstruction.compile, SourceOperand.compile, pc, live,
          execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, dn, Ne.symm d0,
          next, State.relocate, Nat.add_assoc]
        rw [pointer, ← BitVec.ofNat_add]
      · exact Runs.refl _
    obtain ⟨final, trace, halted, fp, written, frame⟩ :=
      ih (first + 1) (destination + 1) next rfl rfl (by omega) (by omega) (by omega)
        (by simp [next, Memory.write])
    have embedded : EmbedsAt (program w (first + 1) count) (program w first (count + 1)) 2 := by
      have h := embeds_append
        ([.copy (.indirect 0) (.memory (.direct first)),
          .binary .add (.direct 0) (.memory (.direct 0)) (.immediate (1#w.bits))] : Program w .multiplication 1)
        (program w (first + 1) count) []
      rw [relocated] at h
      simpa only [List.length_cons, List.length_nil, List.append_nil,
        program, code, List.map_cons, SourceInstruction.compile, SourceOperand.compile,
        List.cons_append, List.nil_append, Nat.reduceAdd] using h
    refine ⟨final.relocate 2, ?_, halted, ?_, ?_, ?_⟩
    · have allSteps := head.append (trace.relocate embedded)
      have cost : 2 + (2 * count + 1) = 2 * (count + 1) + 1 := by omega
      rw [cost] at allSteps
      exact allSteps
    · simpa [State.relocate, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using fp
    · intro i hi
      cases i with
      | zero =>
        have h := frame destination d0 (Or.inl (by omega))
        simpa [State.relocate, next, Memory.write, d0] using h
      | succ i =>
        have h := written i (by omega)
        have src0 : first + 1 + i ≠ 0 := by omega
        have srcDest : first + 1 + i ≠ destination := by omega
        simp only [next, Memory.write, src0, srcDest, ↓reduceIte] at h
        simpa [State.relocate, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h
    · intro a ha outside
      have h := frame a ha (by omega)
      have hd : a ≠ destination := by omega
      simpa [State.relocate, next, Memory.write, ha, hd] using h

end WordRAM.Conjectures.SavePrefix