SETH ⇒ OVC sparsification bundle 4: 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_03

set_option autoImplicit true

/-! Protect the low input cells before allocating working registers. -/
namespace WordRAM.Conjectures.InputBootstrap

def base (w : Width) : Nat := 2 ^ (w.bits - 1)

def header : List SourceInstruction :=
  [.wordWidth (.direct 0),
   .binary .sub (.direct 0) (.memory (.direct 0)) (.immediate 1),
   .binary .shl (.direct 0) (.immediate 1) (.memory (.direct 0))]

/-- This source program is fixed: it saves exactly cells 1 through 15. Only
cell zero is used to compute the high-memory destination. -/
def algorithm : Algorithm := ⟨header ++ SavePrefix.code 1 15, 1, by decide⟩

theorem base_bounds (wide : 6 ≤ w.bits) : 32 ≤ base w ∧ base w + 15 < 2 ^ w.bits := by
  have h : 2 ^ 5 ≤ 2 ^ (w.bits - 1) := Nat.pow_le_pow_right (by decide) (by omega)
  have hp : 2 ^ w.bits = base w * 2 := by
    have he : w.bits = (w.bits - 1) + 1 := by omega
    calc
      2 ^ w.bits = 2 ^ ((w.bits - 1) + 1) := congrArg (fun k => 2 ^ k) he
      _ = base w * 2 := Nat.pow_succ 2 (w.bits - 1)
  change 32 ≤ base w at h
  omega

private theorem pointer_value (w : Width) :
    (1#w.bits) <<< (BitVec.ofNat w.bits w.bits - 1#w.bits).toNat = BitVec.ofNat w.bits (base w) := by
  have oneFit : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by have := w.positive; omega)
  have widthFit : w.bits < 2 ^ w.bits := Nat.lt_pow_self (by decide)
  rw [BitVec.ofNat_sub_ofNat_of_le _ _ oneFit w.positive]
  have predFit : w.bits - 1 < 2 ^ w.bits := by omega
  simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt predFit]
  change BitVec.twoPow w.bits (w.bits - 1) = BitVec.ofNat w.bits (base w)
  apply BitVec.eq_of_toNat_eq
  exact BitVec.toNat_twoPow _ _

theorem enters (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (algorithm.program w) 3 s
    t.pc = 3 ∧ t.halted = false ∧ t.ticks = s.ticks + 3 ∧
    t.mem 0 = BitVec.ofNat w.bits (base w) ∧ (∀ a, a ≠ 0 → t.mem a = s.mem a) := by
  simp [algorithm, header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
    widthConstant, pc, live, Nat.add_assoc, pointer_value,
    -BitVec.toNat_sub, -BitVec.toNat_ofNat]
  intro a ha
  simp [ha]

/-- Save the first fifteen input words in a fixed number of steps, without
changing any input cell below the reserved high-memory buffer. This theorem
starts with arbitrary memory, including the conjecture's initialState. -/
theorem protects (s : State w) (pc : s.pc = 0) (live : s.halted = false) (wide : 6 ≤ w.bits) :
    ∃ final : State w,
      Runs widthConstant (algorithm.program w) 34 s final ∧ final.halted = true ∧
      final.mem 0 = BitVec.ofNat w.bits (base w + 15) ∧
      (∀ i, i < 15 → final.mem (base w + i) = s.mem (i + 1)) ∧
      (∀ a, a ≠ 0 → (a < base w ∨ base w + 15 ≤ a) → final.mem a = s.mem a) := by
  let head := run widthConstant (algorithm.program w) 3 s
  obtain ⟨hpc, hlive, ticks, pointer, frame⟩ := enters s pc live
  obtain ⟨t, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) 3 s
  have hc := runs_cost trace
  have cost : t = 3 := by omega
  subst t
  let entry : State w := { head with pc := 0 }
  have bounds := base_bounds wide
  obtain ⟨final, saved, halted, fp, words, preserved⟩ :=
    SavePrefix.saves 15 1 (base w) entry rfl hlive (by decide) (by omega) bounds.2 pointer
  have embedded : EmbedsAt (SavePrefix.program w 1 15) (algorithm.program w) 3 := by
    have h := embeds_append (header.map (SourceInstruction.compile w)) (SavePrefix.program w 1 15) []
    rw [SavePrefix.relocated] at h
    simpa [algorithm, Algorithm.program, SavePrefix.program, List.map_append, header] using h
  have he : entry.relocate 3 = head := by
    change { head with pc := 3 } = head
    have hp : head.pc = 3 := hpc
    rw [← hp]
  have linked : Runs widthConstant (algorithm.program w) 31 head (final.relocate 3) := by
    simpa only [he] using saved.relocate embedded
  refine ⟨final.relocate 3, trace.append linked, halted, fp, ?_, ?_⟩
  · intro i hi
    have h := (words i hi).trans (frame (1 + i) (by omega))
    simpa [State.relocate, Nat.add_comm] using h
  · intro a ha outside
    exact (preserved a ha outside).trans (frame a ha)

end WordRAM.Conjectures.InputBootstrap

/-! Find the serialized input's end after the low input cells have been saved. -/
namespace WordRAM.Conjectures.InputScan

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

/-- Read low input cells from their backup and all later cells in place. -/
def logicalMemory (mem : Memory w) (backup : Nat) : Memory w :=
  fun address => if address ≤ 15 then mem (backup + address - 1) else mem address

/-- Registers 1=original clause cursor, 2=remaining clauses, 3,4=scratch,
5=backup base. This scans clause lengths without touching any literal words. -/
def algorithm : Algorithm :=
  ⟨[.branch .eq (reg 2) (.immediate 0) 12,
    .branch .le (reg 1) (.immediate 15) 4,
    .copy (.direct 4) (.memory (.indirect 1)),
    .jump 7,
    .binary .add (.direct 3) (reg 5) (reg 1),
    .binary .sub (.direct 3) (reg 3) (.immediate 1),
    .copy (.direct 4) (.memory (.indirect 3)),
    .binary .add (.direct 4) (reg 4) (reg 4),
    .binary .add (.direct 1) (reg 1) (reg 4),
    .binary .add (.direct 1) (reg 1) (.immediate 1),
    .binary .sub (.direct 2) (reg 2) (.immediate 1),
    .jump 0, .halt], 1, by decide⟩

def iterationCost (address : Nat) : Nat := if address ≤ 15 then 10 else 9

theorem iteration (s : State w) (address backup length : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 2 ≠ 0#w.bits)
    (positive : 1 ≤ address) (base : 16 ≤ backup)
    (backupFits : backup + 15 < 2 ^ w.bits) (addressFits : address < 2 ^ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (saved : s.mem 5 = BitVec.ofNat w.bits backup)
    (header : logicalMemory s.mem backup address = BitVec.ofNat w.bits length) :
    let t := run widthConstant (algorithm.program w) (iterationCost address) s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + iterationCost address ∧
    t.mem 1 = BitVec.ofNat w.bits (address + 1 + 2 * length) ∧
    t.mem 2 = s.mem 2 - 1#w.bits ∧ (∀ a, 5 ≤ a → t.mem a = s.mem a) := by
  have smallFit : 15 < 2 ^ w.bits := by omega
  have pointerNat : (s.mem 1).toNat = address := by simp [pointer, Nat.mod_eq_of_lt addressFits]
  by_cases low : address ≤ 15
  · have sumFit : backup + address < 2 ^ w.bits := by omega
    have mapped : (BitVec.ofNat w.bits backup + BitVec.ofNat w.bits address - 1#w.bits).toNat =
        backup + address - 1 := by
      rw [← BitVec.ofNat_add, BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
      exact Nat.mod_eq_of_lt (by omega)
    have m3 : backup + address - 1 ≠ 3 := by omega
    have loaded : s.mem (backup + address - 1) = BitVec.ofNat w.bits length := by
      simpa [logicalMemory, low] using header
    simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
      reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
      Comparison.test, iterationCost, low, pc, live, nonzero, pointer, saved,
      Nat.mod_eq_of_lt addressFits, Nat.mod_eq_of_lt smallFit, mapped, m3, loaded,
      Nat.add_assoc, -BitVec.toNat_add, -BitVec.toNat_sub]
    constructor
    · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
      congr 1
      omega
    · intro a ha
      have : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 := by omega
      simp_all
  · have loaded : s.mem address = BitVec.ofNat w.bits length := by
      simpa [logicalMemory, low] using header
    simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
      reg, run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval,
      Comparison.test, iterationCost, low, pc, live, nonzero, pointer,
      Nat.mod_eq_of_lt addressFits, Nat.mod_eq_of_lt smallFit, loaded,
      Nat.add_assoc, -BitVec.toNat_add, -BitVec.toNat_sub]
    constructor
    · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add, ← BitVec.ofNat_add]
      congr 1
      omega
    · intro a ha
      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 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, Address.resolve, Operand.read, Comparison.test,
    pc, live, empty, Nat.add_assoc]

theorem logicalMemory_frame (backup : Nat) (base : 16 ≤ backup)
    (frame : ∀ a, 5 ≤ a → other a = mem a) :
    logicalMemory other backup = logicalMemory mem backup := by
  funext address
  unfold logicalMemory
  split
  · apply frame; omega
  · apply frame; omega

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 scan locates the end of the encoded clause sequence in at most ten
instructions per clause. The backup and unmodified input tail are preserved. -/
theorem scans (clauses : List (List (Literal n))) (s : State w) (address backup : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (positive : 1 ≤ address)
    (base : 16 ≤ backup) (backupFits : backup + 15 < 2 ^ w.bits)
    (inputFits : address + MaskTable.span clauses < 2 ^ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (remaining : s.mem 2 = BitVec.ofNat w.bits clauses.length)
    (saved : s.mem 5 = BitVec.ofNat w.bits backup)
    (input : MaskTable.Encoded (logicalMemory s.mem backup) address clauses) :
    ∃ cost, cost ≤ 10 * clauses.length + 2 ∧ ∃ final : State w,
      Runs widthConstant (algorithm.program w) cost s final ∧ final.halted = true ∧
      final.mem 1 = BitVec.ofNat w.bits (address + MaskTable.span clauses) ∧ final.mem 2 = 0 ∧
      (∀ a, 5 ≤ a → final.mem a = s.mem a) := by
  induction clauses generalizing s address with
  | nil =>
    have empty : s.mem 2 = 0#w.bits := by simpa using remaining
    have he := exits s pc live empty
    refine ⟨2, by simp, run widthConstant (algorithm.program w) 2 s,
      trace_of_ticks s 2 he.2.2, he.1, ?_, ?_, ?_⟩
    · simpa [he.2.1, MaskTable.span] using pointer
    · simpa [he.2.1] using empty
    · intro a _; exact congrFun he.2.1 a
  | cons clause rest ih =>
    have countFit : rest.length + 1 < 2 ^ w.bits := by
      have span := MaskTable.span_eq (clause :: rest)
      simp only [List.length_cons] at span
      omega
    have nz : s.mem 2 ≠ 0#w.bits := by
      intro h
      have hn := congrArg BitVec.toNat h
      simp [remaining, Nat.mod_eq_of_lt countFit] at hn
    obtain ⟨npc, nlive, ticks, np, nc, frame⟩ := iteration s address backup clause.length
      pc live nz positive base backupFits (by omega) pointer saved input.1
    let next := run widthConstant (algorithm.program w) (iterationCost address) s
    have nextCount : next.mem 2 = BitVec.ofNat w.bits rest.length := by
      rw [nc, 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 (logicalMemory next.mem backup)
        (address + 1 + 2 * clause.length) rest := by
      rw [logicalMemory_frame backup base frame]
      exact input.2.2
    obtain ⟨cost, bound, final, trace, halted, endPointer, zeroCount, preserved⟩ :=
      ih next (address + 1 + 2 * clause.length) npc nlive (by omega)
        (by simp only [MaskTable.span] at inputFits; omega) np nextCount
        ((frame 5 (by decide)).trans saved) nextInput
    refine ⟨iterationCost address + cost, ?_, final,
      (trace_of_ticks s (iterationCost address) ticks).append trace, halted, ?_, zeroCount, ?_⟩
    · have : iterationCost address ≤ 10 := by unfold iterationCost; split <;> omega
      simp only [List.length_cons]
      omega
    · simpa [MaskTable.span, Nat.add_assoc] using endPointer
    · intro a ha; exact (preserved a ha).trans (frame a ha)

theorem encoding_length (f : SATInstance) : f.encode.length = 2 + MaskTable.span f.clauses := by
  have h := congrArg List.length (MaskTable.words_encode (⟨1, by decide⟩ : Width) f)
  simp only [List.length_cons, List.length_map] at h
  have len := MaskTable.words_length (⟨1, by decide⟩ : Width) f.clauses
  omega

/-- The ordinary initialState contains exactly the input representation used
by the length scanner and mask-table builder. -/
theorem encoded_initial (w : Width) (f : SATInstance) :
    MaskTable.Encoded (initialState w f.encode).mem 3 f.clauses := by
  apply MaskTable.encoded_of_words
  intro i _
  have h := congrArg (fun words : List (Word w) => (words[i + 2]?).getD 0)
    (MaskTable.words_encode w f)
  simp only [List.getElem?_cons_succ, List.getElem?_map] at h
  have mapDefault : ((f.encode[i + 2]?).map (BitVec.ofNat w.bits)).getD 0 =
      BitVec.ofNat w.bits ((f.encode[i + 2]?).getD 0) := by
    cases f.encode[i + 2]? <;> rfl
  rw [mapDefault] at h
  simpa [initialState, Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using h.symm

/-- Saving the prefix and preserving the remaining input suffices for the
scanner's logical-memory invariant, despite later reuse of the low registers. -/
theorem encoded_protected (w : Width) (f : SATInstance) (mem : Memory w) (backup : Nat)
    (saved : ∀ i, i < 15 → mem (backup + i) = (initialState w f.encode).mem (i + 1))
    (tail : ∀ address, 15 < address → address ≤ f.encode.length →
      mem address = (initialState w f.encode).mem address) :
    MaskTable.Encoded (logicalMemory mem backup) 3 f.clauses := by
  apply MaskTable.Encoded.frame _ _ (encoded_initial w f)
  intro address lo hi
  have endBound : address ≤ f.encode.length := by rw [encoding_length]; omega
  unfold logicalMemory
  split
  · rename_i low
    have h := saved (address - 1) (by omega)
    have restore : address - 1 + 1 = address := by omega
    rw [restore] at h
    have rearrange : backup + address - 1 = backup + (address - 1) := by omega
    simpa only [rearrange] using h
  · rename_i high
    exact tail address (by omega) endBound

end WordRAM.Conjectures.InputScan