SETH ⇒ OVC sparsification bundle 33: 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_32

set_option autoImplicit true

/-! Assemble and normalize a child formula from two stored clause tables. -/
namespace WordRAM.Conjectures.Sparsification.NormalizeConcat

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

def bridge : Algorithm :=
  ⟨[.binary .add (.direct 11) (reg 29) (reg 30), .copy (.direct 12) (reg 28),
    .copy (.direct 13) (reg 31), .halt], 1, by decide⟩

/-- Controls 26–30 are those of `RecordConcat`; 31 points to normalization
workspace above the concatenated raw table. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code RecordConcat.algorithm.code
    (SourceChain.code bridge.code NormalizeMachine.initialized.code), 1, by decide⟩

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 11 = s.mem 29 + s.mem 30 ∧
      t.mem 12 = s.mem 28 ∧ t.mem 13 = s.mem 31 ∧ (∀ a, 16 ≤ a → 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, BinOp.eval, pc, live, Nat.add_assoc]
  intro a ha
  have h : a ≠ 11 ∧ a ≠ 12 ∧ a ≠ 13 := by omega
  simp [h]

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

/-- Full table assembly and normalization, with explicit space and time bounds.
The result pointer and count are returned in 22 and 24. -/
theorem normalizes (left right : CNF n) (s : State w) (first second destination workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false)
    (firstBase : 32 ≤ first) (secondBase : 32 ≤ second)
    (firstEnd : first + 3 * left.length ≤ destination)
    (secondEnd : second + 3 * right.length ≤ destination)
    (workspaceBase : destination + 3 * (left.length + right.length) ≤ workspace)
    (fits : workspace + (left.length + right.length) * (3 * (left.length + right.length + 1)) < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (firstPointer : s.mem 26 = BitVec.ofNat w.bits first)
    (secondPointer : s.mem 27 = BitVec.ofNat w.bits second)
    (outputPointer : s.mem 28 = BitVec.ofNat w.bits destination)
    (firstCount : s.mem 29 = BitVec.ofNat w.bits left.length)
    (secondCount : s.mem 30 = BitVec.ofNat w.bits right.length)
    (workspacePointer : s.mem 31 = BitVec.ofNat w.bits workspace)
    (firstInput : VectorBuilder.Stored s.mem first (RecordTable.words w left))
    (secondInput : VectorBuilder.Stored s.mem second (RecordTable.words w right)) :
    ∃ time final resultAddress,
      time ≤ (left.length + right.length) * (35 * (left.length + right.length) + 55) + 30 ∧
      Runs widthConstant (algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem resultAddress (RecordTable.words w (Normalize.normalize (left ++ right))) ∧
      final.mem 22 = BitVec.ofNat w.bits resultAddress ∧
      final.mem 24 = BitVec.ofNat w.bits (Normalize.normalize (left ++ right)).length ∧
      destination + 3 * (left.length + right.length) ≤ resultAddress ∧
      resultAddress + 3 * (Normalize.normalize (left ++ right)).length ≤
        workspace + (left.length + right.length) * (3 * (left.length + right.length + 1)) ∧
      (∀ a, 32 ≤ a →
        (a < destination ∨ destination + 3 * (left.length + right.length) ≤ a) →
        (a < workspace ∨ workspace + (left.length + right.length) * (3 * (left.length + right.length + 1)) ≤ a) →
        final.mem a = s.mem a) := by
  have destinationBase : 32 ≤ destination := by omega
  obtain ⟨concatenated, ct, ch, table, cf⟩ := RecordConcat.concatenates left right s first second destination
    pc live firstBase secondBase firstEnd secondEnd (by omega)
    firstPointer secondPointer outputPointer firstCount secondCount firstInput secondInput
  have saved : ∀ a, 16 ≤ a → a < 32 → concatenated.mem a = s.mem a := by
    intro a ha hb; exact cf a (by omega) (Or.inl (by omega))
  let middle := run widthConstant (bridge.program w) 4 (SourceChain.resume concatenated)
  obtain ⟨mh, mt, mc, mp, mw, mf⟩ := bridges (SourceChain.resume concatenated) rfl rfl
  have total : middle.mem 11 = BitVec.ofNat w.bits (left ++ right).length := by
    calc
      middle.mem 11 = concatenated.mem 29 + concatenated.mem 30 := mc
      _ = BitVec.ofNat w.bits left.length + BitVec.ofNat w.bits right.length := by
        rw [saved 29 (by decide) (by decide), saved 30 (by decide) (by decide), firstCount, secondCount]
      _ = BitVec.ofNat w.bits (left ++ right).length := by rw [← BitVec.ofNat_add, List.length_append]
  have input : VectorBuilder.Stored middle.mem destination (RecordTable.words w (left ++ right)) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact mf a (by omega)
  obtain ⟨time, out, resultAddress, bound, trace, halted, result, resultPointer, resultCount, lower, upper, frame⟩ :=
    NormalizeMachine.normalizes (left ++ right) (SourceChain.resume middle) destination workspace rfl rfl
      destinationBase (by simpa only [List.length_append] using workspaceBase)
      (by simpa only [List.length_append] using fits) variablesFit total
      (mp.trans ((saved 28 (by decide) (by decide)).trans outputPointer))
      (mw.trans ((saved 31 (by decide) (by decide)).trans workspacePointer)) input
  have tail := SourceChain.traces bridge.code NormalizeMachine.initialized.code (SourceChain.resume concatenated)
    middle out 4 time rfl mh (trace_of_ticks _ _ 4 mt) trace
  have full := SourceChain.traces RecordConcat.algorithm.code (SourceChain.code bridge.code NormalizeMachine.initialized.code)
    s concatenated _ (21 * (left.length + right.length) + 13) (4 + time) live ch ct tail
  refine ⟨(21 * (left.length + right.length) + 13) + (4 + time),
    (out.relocate bridge.code.length).relocate RecordConcat.algorithm.code.length, resultAddress,
    ?_, full, halted, result, resultPointer, resultCount, ?_, ?_, ?_⟩
  · simp only [List.length_append] at bound
    simp only [Nat.mul_add] at bound ⊢
    omega
  · simpa only [List.length_append] using lower
  · simpa only [List.length_append] using upper
  · intro a ha outsideRaw outsideWork
    exact (frame a ha (by simpa only [List.length_append] using outsideWork)).trans
      ((mf a (by omega)).trans (cf a (by omega) outsideRaw))

end WordRAM.Conjectures.Sparsification.NormalizeConcat

/-! Materialize the selected core as a clause-table record. -/
namespace WordRAM.Conjectures.Sparsification.CoreRecord

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 9) (reg 20), .copy (.direct 10) (reg 21),
    .copy (.direct 1) (reg 20), .copy (.direct 5) (reg 21),
    .copy (.direct 13) (reg 31), .copy (.direct 14) (.immediate 0), .halt], 1, by decide⟩

/-- Core masks in 20/21, destination in 31. Count the distinct literals and
write the complete record, preserving all persistent controls 16–31. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code SizeMachine.algorithm.code RecordAppend.algorithm.code), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧ t.mem 9 = s.mem 20 ∧ t.mem 10 = s.mem 21 ∧
      t.mem 1 = s.mem 20 ∧ t.mem 5 = s.mem 21 ∧ t.mem 13 = s.mem 31 ∧ t.mem 14 = 0#w.bits ∧
      (∀ a, 16 ≤ a → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a ha
  have h : a ≠ 9 ∧ a ≠ 10 ∧ a ≠ 1 ∧ a ≠ 5 ∧ a ≠ 13 ∧ a ≠ 14 := by omega
  simp [h]

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 builds (core : Clause n) (s : State w) (destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits)
    (base : 32 ≤ destination) (fits : destination + 2 < 2 ^ w.bits)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (pointer : s.mem 31 = BitVec.ofNat w.bits destination) :
    ∃ final, Runs widthConstant (algorithm.program w) (12 * w.bits + 28) s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem destination (RecordTable.words w [core]) ∧
      (∀ a, 16 ≤ a → (a < destination ∨ destination + 3 ≤ a) → final.mem a = s.mem a) := by
  let prepared := run widthConstant (prepare.program w) 7 s
  obtain ⟨ph, pt, pp, pn, cp, cn, dp, _, pf⟩ := prepares s pc live
  obtain ⟨counted, ct, ch, count, cf⟩ := SizeMachine.counts (Masks.encode w core true) (Masks.encode w core false)
    (SourceChain.resume prepared) rfl rfl (cp.trans qp) (cn.trans qn)
  have countedSize : counted.mem 0 = BitVec.ofNat w.bits (Normalize.clean core).length := by
    rw [count]
    apply BitVec.eq_of_toNat_eq
    simp only [BitVec.toNat_add, BitVec.toNat_ofNat, MaskCardinality.count_distinct core variablesFit]
  have savedPositive : counted.mem 9 = Masks.encode w core true :=
    (cf 9 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (pp.trans qp)
  have savedNegative : counted.mem 10 = Masks.encode w core false :=
    (cf 10 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (pn.trans qn)
  have destinationPointer : counted.mem 13 = BitVec.ofNat w.bits destination :=
    (cf 13 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (dp.trans pointer)
  let out := run widthConstant (RecordAppend.algorithm.program w) 8 (SourceChain.resume counted)
  obtain ⟨oh, ot, _, _, op, on, os, ofr⟩ := RecordAppend.executes (SourceChain.resume counted)
    destination rfl rfl (by omega) fits destinationPointer
  have tail := SourceChain.traces SizeMachine.algorithm.code RecordAppend.algorithm.code (SourceChain.resume prepared)
    counted out (12 * w.bits + 13) 8 rfl ch ct (trace_of_ticks _ _ 8 ot)
  have full := SourceChain.traces prepare.code (SourceChain.code SizeMachine.algorithm.code RecordAppend.algorithm.code)
    s prepared _ 7 ((12 * w.bits + 13) + 8) live ph (trace_of_ticks _ s 7 pt) tail
  have cost : 7 + ((12 * w.bits + 13) + 8) = 12 * w.bits + 28 := by omega
  refine ⟨(out.relocate SizeMachine.algorithm.code.length).relocate prepare.code.length, ?_, oh,
    ⟨op.trans savedPositive, on.trans savedNegative, os.trans countedSize, trivial⟩, ?_⟩
  · simpa only [algorithm, Algorithm.program, cost] using full
  · intro a ha outside
    exact (ofr a (by omega) (by omega) (by omega) (by omega) (by omega)).trans
      ((cf a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans (pf a ha))

end WordRAM.Conjectures.Sparsification.CoreRecord

/-! Load child-construction metadata and save the normalized child's descriptor. -/
namespace WordRAM.Conjectures.Sparsification.ChildAssembly

structure Config where
  first : Nat
  second : Nat
  destination : Nat
  firstCount : Nat
  secondCount : Nat
  workspace : Nat
  resultPointer : Nat
  resultCount : Nat

/-- Metadata are kept above scratch registers and below clause buffers. -/
structure Valid (c : Config) : Prop where
  first : 32 ≤ c.first
  second : 32 ≤ c.second
  destination : 32 ≤ c.destination
  firstCount : 32 ≤ c.firstCount
  secondCount : 32 ≤ c.secondCount
  workspace : 32 ≤ c.workspace
  resultPointerBase : 32 ≤ c.resultPointer
  resultPointerEnd : c.resultPointer < 64
  resultCountBase : 32 ≤ c.resultCount
  resultCountEnd : c.resultCount < 64
  distinct : c.resultPointer ≠ c.resultCount

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

def prepare (c : Config) : Algorithm :=
  ⟨[.copy (.direct 26) (reg c.first), .copy (.direct 27) (reg c.second),
    .copy (.direct 28) (reg c.destination), .copy (.direct 29) (reg c.firstCount),
    .copy (.direct 30) (reg c.secondCount), .copy (.direct 31) (reg c.workspace), .halt], 1, by decide⟩

def save (c : Config) : Algorithm :=
  ⟨[.copy (.direct c.resultPointer) (reg 22), .copy (.direct c.resultCount) (reg 24), .halt], 1, by decide⟩

def algorithm (c : Config) : Algorithm :=
  ⟨SourceChain.code (prepare c).code (SourceChain.code NormalizeConcat.algorithm.code (save c).code), 1, by decide⟩

def left : Config := ⟨34, 38, 39, 36, 48, 40, 43, 44⟩
def right : Config := ⟨34, 35, 41, 36, 37, 42, 45, 46⟩

theorem left_valid : Valid left := by constructor <;> decide
theorem right_valid : Valid right := by constructor <;> decide

theorem prepares (c : Config) (valid : Valid c) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((prepare c).program w) 7 s
    t.halted = true ∧ t.ticks = s.ticks + 7 ∧ t.mem 26 = s.mem c.first ∧ t.mem 27 = s.mem c.second ∧
      t.mem 28 = s.mem c.destination ∧ t.mem 29 = s.mem c.firstCount ∧
      t.mem 30 = s.mem c.secondCount ∧ t.mem 31 = s.mem c.workspace ∧
      (∀ a, 32 ≤ a → t.mem a = s.mem a) := by
  have low : ∀ a, 32 ≤ a → a ≠ 26 ∧ a ≠ 27 ∧ a ≠ 28 ∧ a ≠ 29 ∧ a ≠ 30 ∧ a ≠ 31 := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc,
    low c.second valid.second, low c.destination valid.destination,
    low c.firstCount valid.firstCount, low c.secondCount valid.secondCount, low c.workspace valid.workspace]
  intro a ha; simp [low a ha]

theorem saves (c : Config) (valid : Valid c) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((save c).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem c.resultPointer = s.mem 22 ∧
      t.mem c.resultCount = s.mem 24 ∧
      (∀ a, a ≠ c.resultPointer → a ≠ c.resultCount → t.mem a = s.mem a) := by
  have h : 24 ≠ c.resultPointer := by have := valid.resultPointerBase; omega
  simp [save, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc, h, valid.distinct]
  intro a hp hc; simp [hp, hc]

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

/-- The descriptor is saved in metadata cells, beyond the scratch registers
used by a subsequent child-construction call. -/
theorem assembles (c : Config) (valid : Valid c) (firstClauses secondClauses : CNF n)
    (s : State w) (first second destination workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false)
    (firstBase : 64 ≤ first) (secondBase : 64 ≤ second)
    (firstEnd : first + 3 * firstClauses.length ≤ destination)
    (secondEnd : second + 3 * secondClauses.length ≤ destination)
    (workspaceBase : destination + 3 * (firstClauses.length + secondClauses.length) ≤ workspace)
    (fits : workspace + (firstClauses.length + secondClauses.length) *
      (3 * (firstClauses.length + secondClauses.length + 1)) < 2 ^ w.bits)
    (variablesFit : n ≤ w.bits)
    (firstPointer : s.mem c.first = BitVec.ofNat w.bits first)
    (secondPointer : s.mem c.second = BitVec.ofNat w.bits second)
    (outputPointer : s.mem c.destination = BitVec.ofNat w.bits destination)
    (firstCount : s.mem c.firstCount = BitVec.ofNat w.bits firstClauses.length)
    (secondCount : s.mem c.secondCount = BitVec.ofNat w.bits secondClauses.length)
    (workspacePointer : s.mem c.workspace = BitVec.ofNat w.bits workspace)
    (firstInput : VectorBuilder.Stored s.mem first (RecordTable.words w firstClauses))
    (secondInput : VectorBuilder.Stored s.mem second (RecordTable.words w secondClauses)) :
    ∃ time final resultAddress,
      time ≤ (firstClauses.length + secondClauses.length) * (35 * (firstClauses.length + secondClauses.length) + 55) + 40 ∧
      Runs widthConstant ((algorithm c).program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem resultAddress (RecordTable.words w (Normalize.normalize (firstClauses ++ secondClauses))) ∧
      final.mem c.resultPointer = BitVec.ofNat w.bits resultAddress ∧
      final.mem c.resultCount = BitVec.ofNat w.bits (Normalize.normalize (firstClauses ++ secondClauses)).length ∧
      destination + 3 * (firstClauses.length + secondClauses.length) ≤ resultAddress ∧
      resultAddress + 3 * (Normalize.normalize (firstClauses ++ secondClauses)).length ≤
        workspace + (firstClauses.length + secondClauses.length) * (3 * (firstClauses.length + secondClauses.length + 1)) ∧
      (∀ a, 32 ≤ a → a ≠ c.resultPointer → a ≠ c.resultCount →
        (a < destination ∨ destination + 3 * (firstClauses.length + secondClauses.length) ≤ a) →
        (a < workspace ∨ workspace + (firstClauses.length + secondClauses.length) *
          (3 * (firstClauses.length + secondClauses.length + 1)) ≤ a) → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare c).program w) 7 s
  obtain ⟨ph, pt, pp, ps, pd, pn, pm, pw, pf⟩ := prepares c valid s pc live
  have input1 : VectorBuilder.Stored prepared.mem first (RecordTable.words w firstClauses) := by
    apply MemoryCopy.stored_frame _ _ firstInput
    intro a ha _; exact pf a (by omega)
  have input2 : VectorBuilder.Stored prepared.mem second (RecordTable.words w secondClauses) := by
    apply MemoryCopy.stored_frame _ _ secondInput
    intro a ha _; exact pf a (by omega)
  obtain ⟨time, normalized, address, bound, trace, halted, table, pointer, count, lower, upper, frame⟩ :=
    NormalizeConcat.normalizes firstClauses secondClauses (SourceChain.resume prepared) first second destination workspace
      rfl rfl (by omega) (by omega) firstEnd secondEnd workspaceBase fits variablesFit
      (pp.trans firstPointer) (ps.trans secondPointer) (pd.trans outputPointer) (pn.trans firstCount)
      (pm.trans secondCount) (pw.trans workspacePointer) input1 input2
  let out := run widthConstant ((save c).program w) 3 (SourceChain.resume normalized)
  obtain ⟨oh, ot, op, oc, ofr⟩ := saves c valid (SourceChain.resume normalized) rfl rfl
  have tail := SourceChain.traces NormalizeConcat.algorithm.code (save c).code (SourceChain.resume prepared)
    normalized out time 3 rfl halted trace (trace_of_ticks _ _ 3 ot)
  have full := SourceChain.traces (prepare c).code (SourceChain.code NormalizeConcat.algorithm.code (save c).code)
    s prepared _ 7 (time + 3) live ph (trace_of_ticks _ s 7 pt) tail
  refine ⟨7 + (time + 3), (out.relocate NormalizeConcat.algorithm.code.length).relocate (prepare c).code.length,
    address, by omega, full, oh, ?_, op.trans pointer, oc.trans count, lower, upper, ?_⟩
  · apply MemoryCopy.stored_frame _ _ table
    intro a ha _
    have := valid.resultPointerEnd
    have := valid.resultCountEnd
    exact ofr a (by omega) (by omega)
  · intro a ha hp hc raw work
    exact (ofr a hp hc).trans ((frame a ha raw work).trans (pf a ha))

end WordRAM.Conjectures.Sparsification.ChildAssembly