SETH ⇒ OVC sparsification bundle 28: 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_27

set_option autoImplicit true

/-! Disjoint counters, serialized core prefixes, and immutable formula records. -/
namespace WordRAM.Conjectures.Sparsification.CoreSearchLayout

variable {w : Width} {before middle after mem : Memory w}

def index (depth : Nat) := 32 + depth

def coreBase (length : Nat) := 32 + length

def slot (length depth : Nat) := coreBase length + 2 * depth

/-- Cells outside the current and deeper search's writable regions. -/
def Preserved (length depth address : Nat) : Prop :=
  16 ≤ address ∧ (address < 20 ∨ 24 ≤ address) ∧
    (address < index depth ∨ index length ≤ address) ∧
    (address < slot length depth ∨ slot length length ≤ address)

def Frame (length depth : Nat) (before after : Memory w) : Prop :=
  ∀ a, Preserved length depth a → after a = before a

theorem preserved_mono (length depth next a : Nat) (h : depth ≤ next)
    (keep : Preserved length depth a) : Preserved length next a := by
  unfold Preserved index slot coreBase at *
  omega

theorem control (length depth a : Nat) (lo : 16 ≤ a) (hi : a < 20) : Preserved length depth a := by
  unfold Preserved index slot coreBase; omega

theorem outer_index (length depth next : Nat) (lt : depth < next) (_bound : next ≤ length) :
    Preserved length next (index depth) := by
  unfold Preserved index slot coreBase; omega

theorem prefix_word (length depth a : Nat) (lo : coreBase length ≤ a) (hi : a < slot length depth) :
    Preserved length depth a := by
  unfold Preserved index slot coreBase at *; omega

theorem table_word (length depth a : Nat) (lo : slot length length ≤ a) : Preserved length depth a := by
  unfold Preserved index slot coreBase at *; omega

theorem not_index (length depth : Nat) (bound : depth < length) : ¬ Preserved length depth (index depth) := by
  unfold Preserved index slot coreBase; omega

theorem not_slot (length depth : Nat) (bound : depth < length) (offset : Nat) (small : offset < 2) :
    ¬ Preserved length depth (slot length depth + offset) := by
  unfold Preserved index slot coreBase; omega

theorem Frame.refl (length depth : Nat) (mem : Memory w) : Frame length depth mem mem := fun _ _ => rfl

theorem Frame.trans (first : Frame length depth before middle) (second : Frame length depth middle after) :
    Frame length depth before after := fun a ha => (second a ha).trans (first a ha)

theorem Frame.outer (h : depth ≤ next) (frame : Frame length next before after) : Frame length depth before after :=
  fun a ha => frame a (preserved_mono _ _ _ _ h ha)

theorem Frame.write (frame : Frame length depth before mem) (bound : depth < length)
    (cell : Nat) (value : Word w) (allowed : cell = 0 ∨ cell = index depth) :
    Frame length depth before (mem.write cell value) := by
  intro a ha
  have different : a ≠ cell := by
    rcases allowed with rfl | rfl
    · have := ha.1; omega
    · intro eq; subst a; exact not_index length depth bound ha
  simpa only [Memory.write, if_neg different] using frame a ha

theorem Frame.prefix (frame : Frame length depth before after) (prefixCore : Clause n)
    (lengthEq : prefixCore.length = depth)
    (input : MaskBuilder.Encoded before (coreBase length) (prefixCore.map (MaskBuilder.wordLiteral w))) :
    MaskBuilder.Encoded after (coreBase length) (prefixCore.map (MaskBuilder.wordLiteral w)) := by
  apply MaskTable.pair_frame _ _ input
  intro a lo hi
  rw [List.length_map, lengthEq] at hi
  exact frame a (prefix_word length depth a lo hi)

theorem Frame.table (frame : Frame length depth before after) (clauses : CNF n) (address : Nat)
    (base : slot length length ≤ address)
    (input : VectorBuilder.Stored before address (RecordTable.words w clauses)) :
    VectorBuilder.Stored after address (RecordTable.words w clauses) := by
  apply MemoryCopy.stored_frame _ _ input
  intro a lo _
  exact frame a (table_word length depth a (by omega))

theorem encoded_append (xs ys : List (Word w × Word w)) (address : Nat) :
    MaskBuilder.Encoded mem address (xs ++ ys) ↔
      MaskBuilder.Encoded mem address xs ∧ MaskBuilder.Encoded mem (address + 2 * xs.length) ys := by
  induction xs generalizing address with
  | nil => simp [MaskBuilder.Encoded]
  | cons x xs ih =>
    simp [MaskBuilder.Encoded, ih, Nat.mul_add, Nat.add_assoc, Nat.add_comm, and_assoc]

theorem extend_prefix (prefixCore : Clause n) (literal : Literal n) (length depth : Nat)
    (lengthEq : prefixCore.length = depth)
    (input : MaskBuilder.Encoded mem (coreBase length) (prefixCore.map (MaskBuilder.wordLiteral w)))
    (positive : mem (slot length depth) = BitVec.ofNat w.bits literal.index.val)
    (polarity : mem (slot length depth + 1) = (if literal.positive then 1#w.bits else 0#w.bits)) :
    MaskBuilder.Encoded mem (coreBase length) ((prefixCore ++ [literal]).map (MaskBuilder.wordLiteral w)) := by
  rw [List.map_append, encoded_append]
  refine ⟨input, ?_⟩
  simp only [List.length_map, lengthEq, List.map_cons, List.map_nil]
  exact ⟨positive, polarity, trivial⟩

theorem writer_frame (length depth : Nat) (bound : depth < length)
    (frame : ∀ a, a ≠ 20 → a ≠ 21 → a ≠ 22 → a ≠ 23 →
      a ≠ slot length depth → a ≠ slot length depth + 1 → after a = before a) :
    Frame length depth before after := by
  intro a ha
  have low := ha.2.1
  apply frame a (by omega) (by omega) (by omega) (by omega)
  · intro eq; subst a
    exact not_slot length depth bound 0 (by decide) (by simpa using ha)
  · intro eq; subst a
    exact not_slot length depth bound 1 (by decide) ha

end WordRAM.Conjectures.Sparsification.CoreSearchLayout

/-! Nested, ordered core enumeration linked to the actual candidate tester. -/
namespace WordRAM.Conjectures.Sparsification.CoreSearch

open CoreSearchLayout

/-- One search loop per unwritten literal. The fixed core length determines
the disjoint counter and literal-array layout; the input variable count is read
from the saved controls, rather than built into the instruction sequence. -/
def algorithm (length size threshold depth : Nat) : Nat → Algorithm
  | 0 => CoreLeaf.algorithm length size threshold (coreBase length)
  | remaining + 1 =>
      SourceSearch.initialized (index depth) 19
        (SourceChain.code (LiteralWriter.algorithm (index depth) (slot length depth)).code
          (algorithm length size threshold (depth + 1) remaining).code)

def cost (n length bits clauses : Nat) : Nat → Nat
  | 0 => 10 * length + 12 * bits + 18 * clauses + 42
  | remaining + 1 => (n + n) * (10 + cost n length bits clauses remaining + 4) + 5

/-- The successful core remains serialized in the shared core buffer. -/
def Outcome (length : Nat) (result : Option (Clause n)) (mem : Memory w) : Prop :=
  match result with
  | none => mem 0 = 0#w.bits
  | some core => mem 0 = 1#w.bits ∧
      MaskBuilder.Encoded mem (coreBase length) (core.map (MaskBuilder.wordLiteral w))

theorem Outcome.answer {mem : Memory w} {result : Option (Clause n)} (h : Outcome length result mem) :
    mem 0 = (if result.isSome then 1#w.bits else 0#w.bits) := by
  cases result with
  | none => exact h
  | some core => exact h.1

/-- The complete nested program finds the first valid completion in exactly
the existing enumeration order. Its frame preserves formula records, saved
controls, outer counters, and the already-written core prefix. -/
theorem searches (clauses : CNF n) (length size : Nat) (threshold : Nat → Nat)
    (depth remaining : Nat) (prefixCore : Clause n) (s : State w) (tableAddress : Nat)
    (pc : s.pc = 0) (live : s.halted = false)
    (extent : depth + remaining = length) (prefixLength : prefixCore.length = depth)
    (positive : 0 < length) (proper : length < size)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (arrayFits : slot length length < 2 ^ w.bits)
    (tableBase : slot length length ≤ tableAddress)
    (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits)
    (sizeFits : size < 2 ^ w.bits) (thresholdFits : threshold (size - length) < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 17 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits tableAddress)
    (limit : s.mem 19 = BitVec.ofNat w.bits (n + n))
    (prefixInput : MaskBuilder.Encoded s.mem (coreBase length) (prefixCore.map (MaskBuilder.wordLiteral w)))
    (tableInput : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ cost n length w.bits clauses.length remaining ∧
      Runs widthConstant ((algorithm length size (threshold (size - length)) depth remaining).program w) time s final ∧
      final.halted = true ∧
      Outcome length ((CoreEnumeration.completions prefixCore remaining).find?
        (fun core => decide (Flowers.Candidate clauses threshold core size))) final.mem ∧
      Frame length depth s.mem final.mem := by
  induction remaining generalizing depth prefixCore s with
  | zero =>
    have fullLength : prefixCore.length = length := by omega
    obtain ⟨time, out, bound, trace, halted, result, frame⟩ :=
      CoreLeaf.tests_candidate prefixCore clauses length size threshold s (coreBase length) tableAddress pc live
        (by unfold coreBase; omega) (by unfold slot coreBase at tableBase; omega)
        (by simpa only [fullLength, slot] using arrayFits) tableFits variablesFit width fullLength positive proper
        sizeFits thresholdFits nodup count pointer prefixInput tableInput
    have preserved : Frame length depth s.mem out.mem := fun a ha => frame a ha.1
    have encoded := preserved.prefix prefixCore prefixLength prefixInput
    refine ⟨time, out, bound, trace, halted, ?_, preserved⟩
    by_cases valid : Flowers.Candidate clauses threshold prefixCore size
    · have yes : out.mem 0 = 1#w.bits := by simpa only [if_pos valid] using result
      simpa [CoreEnumeration.completions_zero, Outcome, valid] using And.intro yes encoded
    · simpa [CoreEnumeration.completions_zero, Outcome, valid] using result
  | succ remaining ih =>
    have active : depth < length := by omega
    have stopFits : n + n < 2 ^ w.bits := by
      have room := SizeMachine.double_width_fits w.bits width
      omega
    let candidate : Clause n → Bool := fun core => decide (Flowers.Candidate clauses threshold core size)
    let choices : Nat → Option (Clause n) := fun i => (CoreEnumeration.block prefixCore remaining i).find? candidate
    let test : Nat → Bool := fun i => (choices i).isSome
    let invariant : Memory w → Prop := Frame length depth s.mem
    let found : Nat → Memory w → Prop := fun i mem => Outcome length (choices i) mem
    let body := SourceChain.code (LiteralWriter.algorithm (index depth) (slot length depth)).code
      (algorithm length size (threshold (size - length)) (depth + 1) remaining).code
    have bodyCorrect : ∀ i, i < n + n → ∀ start : State w,
        start.pc = 0 → start.halted = false → invariant start.mem →
        start.mem (index depth) = BitVec.ofNat w.bits i → start.mem 19 = BitVec.ofNat w.bits (n + n) →
        ∃ time out, time ≤ 10 + cost n length w.bits clauses.length remaining ∧
          Runs widthConstant (body.map (SourceInstruction.compile w)) time start out ∧ out.halted = true ∧
          invariant out.mem ∧ out.mem 0 = (if test i then 1#w.bits else 0#w.bits) ∧
          out.mem (index depth) = BitVec.ofNat w.bits i ∧ out.mem 19 = BitVec.ofNat w.bits (n + n) ∧
          (test i = true → found i out.mem) := by
      intro i hi start startPC startLive initial current _
      let literal := CoreEnumeration.literal n ⟨i, hi⟩
      obtain ⟨written, writeTrace, writtenHalt, literalIndex, literalPolarity, writeFrame⟩ :=
        LiteralWriter.writes n ⟨i, hi⟩ (index depth) (slot length depth) start startPC startLive
          (by unfold slot coreBase; omega) width variablesFit current
          ((initial 16 (control length depth 16 (by decide) (by decide))).trans variables)
      have wf : Frame length depth start.mem written.mem := writer_frame length depth active writeFrame
      have combined : Frame length depth s.mem written.mem := initial.trans wf
      have oldPrefix := combined.prefix prefixCore prefixLength prefixInput
      have newPrefix : MaskBuilder.Encoded written.mem (coreBase length)
          ((prefixCore ++ [literal]).map (MaskBuilder.wordLiteral w)) :=
        extend_prefix prefixCore literal length depth prefixLength oldPrefix literalIndex literalPolarity
      have nextTable := combined.table clauses tableAddress tableBase tableInput
      obtain ⟨time, out, bound, trace, halted, outcome, frame⟩ :=
        ih (depth + 1) (prefixCore ++ [literal]) (SourceChain.resume written) rfl rfl (by omega)
          (by simp only [List.length_append, List.length_cons, List.length_nil, prefixLength] <;> omega)
          ((combined 16 (control length depth 16 (by decide) (by decide))).trans variables)
          ((combined 17 (control length depth 17 (by decide) (by decide))).trans count)
          ((combined 18 (control length depth 18 (by decide) (by decide))).trans pointer)
          ((combined 19 (control length depth 19 (by decide) (by decide))).trans limit) newPrefix nextTable
      have choiceEq : choices i = (CoreEnumeration.completions (prefixCore ++ [literal]) remaining).find? candidate := by
        simp only [choices, CoreEnumeration.block, dif_pos hi, literal]
      have selected : Outcome length (choices i) out.mem := by
        rw [choiceEq]; exact outcome
      have full := SourceChain.traces (LiteralWriter.algorithm (index depth) (slot length depth)).code
        (algorithm length size (threshold (size - length)) (depth + 1) remaining).code
        start written out 10 time startLive writtenHalt writeTrace trace
      have finalFrame : Frame length depth s.mem out.mem := combined.trans (frame.outer (by omega))
      have keptIndex : out.mem (index depth) = BitVec.ofNat w.bits i := by
        rw [frame (index depth) (outer_index length depth (depth + 1) (by omega) (by omega))]
        exact (writeFrame (index depth) (by unfold index; omega) (by unfold index; omega)
          (by unfold index; omega) (by unfold index; omega)
          (by unfold index slot coreBase; omega) (by unfold index slot coreBase; omega)).trans current
      refine ⟨10 + time, out.relocate (LiteralWriter.algorithm (index depth) (slot length depth)).code.length,
        by omega, full, halted, finalFrame, Outcome.answer selected, keptIndex, ?_, ?_⟩
      · exact (finalFrame 19 (control length depth 19 (by decide) (by decide))).trans limit
      · intro _; exact selected
    have stable : ∀ mem cell value, invariant mem → (cell = 0 ∨ cell = index depth) → invariant (mem.write cell value) := by
      intro mem cell value frame allowed
      exact frame.write active cell value allowed
    obtain ⟨time, out, bound, trace, halted, frame, _, outcome⟩ :=
      SourceSearch.searches_from_zero (index depth) 19 body (n + n)
        (10 + cost n length w.bits clauses.length remaining) test invariant found
        (by decide) (by unfold index; omega) stopFits stable bodyCorrect
        s pc live (Frame.refl length depth s.mem) limit
    refine ⟨time, out, bound, trace, halted, ?_, frame⟩
    change Outcome length ((CoreEnumeration.completions prefixCore (remaining + 1)).find? candidate) out.mem
    rw [CoreEnumeration.first_completion]
    change Outcome length (((List.range' 0 (n + n)).find? test).bind choices) out.mem
    cases result : (List.range' 0 (n + n)).find? test with
    | none => simpa only [result, SourceSearch.Outcome, Outcome, Option.bind_none] using outcome
    | some i =>
      have witness : found i out.mem := by
        rw [result] at outcome
        exact outcome.2.2
      exact witness

theorem cost_at_least_five (n length bits clauses remaining : Nat) :
    5 ≤ cost n length bits clauses remaining := by
  cases remaining <;> simp only [cost] <;> omega

/-- The nested loop cost is polynomial in n for every fixed core length. -/
theorem cost_bound (n length bits clauses remaining : Nat) :
    cost n length bits clauses remaining ≤
      (10 * length + 12 * bits + 18 * clauses + 61) * (2 * n + 1) ^ remaining := by
  have stronger : cost n length bits clauses remaining + 19 ≤
      (10 * length + 12 * bits + 18 * clauses + 61) * (2 * n + 1) ^ remaining := by
    induction remaining with
    | zero => simp only [cost, Nat.pow_zero, Nat.mul_one]; omega
    | succ remaining ih =>
      have positive := cost_at_least_five n length bits clauses remaining
      have step : cost n length bits clauses (remaining + 1) + 19 ≤
          (2 * n + 1) * (cost n length bits clauses remaining + 19) := by
        change (n + n) * (10 + cost n length bits clauses remaining + 4) + 5 + 19 ≤ _
        simp only [Nat.two_mul, Nat.add_mul, Nat.mul_add, Nat.one_mul]
        omega
      have scaled := Nat.mul_le_mul_left (2 * n + 1) ih
      apply Nat.le_trans step
      simpa only [Nat.pow_succ, Nat.mul_assoc, Nat.mul_comm, Nat.mul_left_comm] using scaled
  omega

/-- Search every core of the fixed length, with every counter initialized by
its corresponding loop. On success the raw core is retained at `coreBase`. -/
theorem finds_core (clauses : CNF n) (length size : Nat) (threshold : Nat → Nat)
    (s : State w) (tableAddress : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (positive : 0 < length) (proper : length < size)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (arrayFits : slot length length < 2 ^ w.bits)
    (tableBase : slot length length ≤ tableAddress)
    (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits)
    (sizeFits : size < 2 ^ w.bits) (thresholdFits : threshold (size - length) < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 17 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits tableAddress)
    (limit : s.mem 19 = BitVec.ofNat w.bits (n + n))
    (tableInput : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ (10 * length + 12 * w.bits + 18 * clauses.length + 61) * (2 * n + 1) ^ length ∧
      Runs widthConstant ((algorithm length size (threshold (size - length)) 0 length).program w) time s final ∧
      final.halted = true ∧
      Outcome length ((Selection.cores n length).find? (fun core => decide (Flowers.Candidate clauses threshold core size))) final.mem ∧
      Frame length 0 s.mem final.mem := by
  obtain ⟨time, final, bound, trace, halted, outcome, frame⟩ :=
    searches clauses length size threshold 0 length [] s tableAddress pc live (by omega) rfl positive proper
      width variablesFit arrayFits tableBase tableFits sizeFits thresholdFits nodup variables count pointer limit trivial tableInput
  refine ⟨time, final, Nat.le_trans bound (cost_bound n length w.bits clauses.length length), trace, halted, ?_, frame⟩
  simpa [CoreEnumeration.completions] using outcome

end WordRAM.Conjectures.Sparsification.CoreSearch