SETH ⇒ OVC sparsification bundle 17: 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_16

set_option autoImplicit true

/-! Counting every recursive invocation, including internal nodes and rejection. -/
namespace WordRAM.Conjectures.Sparsification.Work

theorem clean_nonempty (clause : Clause n) (nonempty : clause ≠ []) : Normalize.clean clause ≠ [] := by
  intro empty
  obtain ⟨literal, member⟩ := List.exists_mem_of_ne_nil clause nonempty
  have present := (Normalize.mem_clean literal clause).mpr member
  rw [empty] at present
  simp at present

theorem normalize_no_empty (formula : CNF n) (nonempty : [] ∉ formula) : [] ∉ Normalize.normalize formula := by
  intro member
  obtain ⟨original, present, eq⟩ := List.mem_map.mp (Normalize.minimize_member _ member)
  exact clean_nonempty original (fun empty => nonempty (empty ▸ present)) eq

theorem children_no_empty (formula : CNF n) (threshold : Nat → Nat) (k : Nat)
    (nodup : ∀ clause ∈ formula, clause.Nodup) (nonempty : [] ∉ formula)
    (found : Selection.select formula threshold k = some (size, core)) :
    [] ∉ Branch.left formula core size ∧ [] ∉ Branch.right formula core size := by
  have candidate := (Selection.select_sound formula threshold k found).1
  constructor
  · apply normalize_no_empty
    intro member
    rcases List.mem_append.mp member with member | member
    · exact nonempty (List.mem_filter.mp member).1
    · have empty := List.mem_singleton.mp member
      have positive := candidate.2.1
      rw [← empty] at positive
      contradiction
  · apply normalize_no_empty
    intro member
    rcases List.mem_append.mp member with member | member
    · exact nonempty (List.mem_filter.mp member).1
    · obtain ⟨original, present, eq⟩ := List.mem_map.mp member
      obtain ⟨old, properties⟩ := List.mem_filter.mp present
      have properties := of_decide_eq_true properties
      have length := Branch.petal_length core original candidate.1 (nodup original old) properties.2
      rw [eq] at length
      have proper := candidate.2.2.1
      simp only [List.length_nil, Nat.add_zero] at length
      omega

/-- Number of invocations of the recursive procedure, not a wordRAM cost yet. -/
def calls (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) : Nat :=
  let normalized := Normalize.normalize formula
  if [] ∈ normalized then 1
  else match _found : Selection.select normalized threshold k with
    | none => 1
    | some (size, core) =>
      1 + calls (Branch.left normalized core size) threshold k large +
        calls (Branch.right normalized core size) threshold k large
termination_by weight formula
decreasing_by
  · exact (Tree.selected_smaller formula threshold k large _found).1
  · exact (Tree.selected_smaller formula threshold k large _found).2

/-- A non-rejected tree is full binary: nodes plus one equal twice its leaves. -/
theorem calls_nonempty (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i)
    (nonempty : [] ∉ Normalize.normalize formula) :
    calls formula threshold k large + 1 = 2 * (Tree.leaves formula threshold k large).length := by
  revert nonempty
  induction formula using Tree.leaves.induct threshold k large with
  | case1 formula normalized empty =>
    intro nonempty
    exact False.elim (nonempty empty)
  | case2 formula normalized nonempty found =>
    intro _
    dsimp only [normalized] at *
    rw [calls, Tree.leaves]
    simp only [if_neg nonempty]
    split <;> split <;> simp_all
  | case3 formula normalized nonempty size core found leftIH rightIH =>
    intro _
    have children := children_no_empty normalized threshold k (Normalize.normalize_nodup_literals formula) nonempty found
    have leftEq := leftIH (normalize_no_empty _ children.1)
    have rightEq := rightIH (normalize_no_empty _ children.2)
    dsimp only [normalized] at *
    rw [calls, Tree.leaves]
    simp only [if_neg nonempty]
    split <;> split <;> simp_all <;> omega

/-- Rejection at the root costs one invocation; otherwise nodes are controlled
by output leaves. No uncounted rejection subtree is hidden in the bound. -/
theorem calls_bound (formula : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    calls formula threshold k large ≤ 2 * (Tree.leaves formula threshold k large).length + 1 := by
  by_cases empty : [] ∈ Normalize.normalize formula
  · rw [calls, Tree.leaves]
    simp only [if_pos empty, List.length_nil]
    decide
  · have exactCount := calls_nonempty formula threshold k large empty
    omega

end WordRAM.Conjectures.Sparsification.Work

/-! Two-word clause representations for the sparsification machine. -/
namespace WordRAM.Conjectures.Sparsification.Masks

def encode (w : Width) (clause : Clause n) (polarity : Bool) : Word w :=
  ClauseMasks.mask w (fun _ => true) clause polarity

theorem literal_eq (a b : Literal n) (index : a.index.val = b.index.val) (polarity : a.positive = b.positive) : a = b := by
  have indices : a.index = b.index := Fin.ext index
  cases a; cases b
  simp_all

theorem bit_mem (clause : Clause n) (literal : Literal n) (fits : n ≤ w.bits) :
    (encode w clause literal.positive).getLsbD literal.index.val = true ↔ literal ∈ clause := by
  rw [encode, ClauseMasks.mask_bit _ _ _ _ (Nat.lt_of_lt_of_le literal.index.isLt fits)]
  constructor
  · rintro ⟨other, member, _, polarity, index⟩
    simpa only [literal_eq other literal index polarity] using member
  · intro member
    exact ⟨literal, member, rfl, rfl, rfl⟩

theorem subset_and (a b : Clause n) (subset : a ⊆ b) (polarity : Bool) :
    encode w a polarity &&& encode w b polarity = encode w a polarity := by
  apply BitVec.eq_of_getLsbD_eq
  intro i hi
  by_cases bit : (encode w a polarity).getLsbD i = true
  · obtain ⟨literal, member, side, pol, index⟩ := (ClauseMasks.mask_bit _ _ _ _ hi).mp bit
    have other := (ClauseMasks.mask_bit (w := w) (fun _ => true) b polarity i hi).mpr
      ⟨literal, subset member, side, pol, index⟩
    change (encode w b polarity).getLsbD i = true at other
    simp only [BitVec.getLsbD_and, bit, other, Bool.true_and]
  · have off : (encode w a polarity).getLsbD i = false := Bool.eq_false_iff.mpr bit
    simp only [BitVec.getLsbD_and, off, Bool.false_and]

/-- Subsumption is exactly two machine-word AND/equality tests. -/
theorem subset_iff (a b : Clause n) (fits : n ≤ w.bits) :
    a ⊆ b ↔
      (encode w a true &&& encode w b true = encode w a true) ∧
      (encode w a false &&& encode w b false = encode w a false) := by
  constructor
  · intro subset
    exact ⟨subset_and a b subset true, subset_and a b subset false⟩
  · rintro ⟨positive, negative⟩ literal member
    have bit := (bit_mem a literal fits).mpr member
    have eq : encode w a literal.positive &&& encode w b literal.positive = encode w a literal.positive := by
      cases literal.positive
      · exact negative
      · exact positive
    have bits := congrArg (fun word : Word w => word.getLsbD literal.index.val) eq
    simp only [BitVec.getLsbD_and, bit, Bool.true_and] at bits
    exact (bit_mem b literal fits).mp bits

/-- Removing the core is exactly bitwise AND with the complemented core mask,
separately for each polarity. Literal ordering and duplicates do not affect it. -/
theorem petal_mask (core clause : Clause n) (polarity : Bool) :
    encode w (Branch.petal core clause) polarity = encode w clause polarity &&& ~~~encode w core polarity := by
  apply BitVec.eq_of_getLsbD_eq
  intro i hi
  apply Bool.eq_iff_iff.mpr
  constructor
  · intro present
    obtain ⟨literal, member, side, pol, index⟩ := (ClauseMasks.mask_bit _ _ _ _ hi).mp present
    obtain ⟨old, outside⟩ := List.mem_filter.mp member
    have outside : literal ∉ core := by simpa using outside
    have clauseBit : (encode w clause polarity).getLsbD i = true :=
      (ClauseMasks.mask_bit _ _ _ _ hi).mpr ⟨literal, old, side, pol, index⟩
    have coreBit : (encode w core polarity).getLsbD i = false := by
      apply Bool.eq_false_iff.mpr
      intro present
      obtain ⟨other, member, _, otherPol, otherIndex⟩ := (ClauseMasks.mask_bit _ _ _ _ hi).mp present
      have same := literal_eq other literal (otherIndex.trans index.symm) (otherPol.trans pol.symm)
      exact outside (same ▸ member)
    simp only [BitVec.getLsbD_and, BitVec.getLsbD_not, clauseBit, coreBit, hi,
      decide_true, Bool.not_false, Bool.true_and]
  · intro present
    have parts : (encode w clause polarity).getLsbD i = true ∧ (encode w core polarity).getLsbD i = false := by
      simpa only [BitVec.getLsbD_and, BitVec.getLsbD_not, hi, decide_true,
        Bool.true_and, Bool.and_eq_true, Bool.not_eq_true'] using present
    obtain ⟨literal, member, side, pol, index⟩ := (ClauseMasks.mask_bit _ _ _ _ hi).mp parts.1
    have outside : literal ∉ core := by
      intro member
      have bit := (ClauseMasks.mask_bit (w := w) (fun _ => true) core polarity i hi).mpr
        ⟨literal, member, side, pol, index⟩
      change (encode w core polarity).getLsbD i = true at bit
      rw [parts.2] at bit
      contradiction
    apply (ClauseMasks.mask_bit _ _ _ _ hi).mpr
    exact ⟨literal, by simp [Branch.petal, member, outside], side, pol, index⟩

end WordRAM.Conjectures.Sparsification.Masks

/-! Actual wordRAM clause-subsumption subroutine on positive/negative masks. -/
namespace WordRAM.Conjectures.Sparsification.SubsetMachine

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

/-- Cells 1,2 hold the candidate subset's positive/negative masks; 3,4 hold
those of the containing clause. Result is Boolean cell 0; scratch is 5,6. -/
def algorithm : Algorithm :=
  ⟨[.binary .band (.direct 5) (reg 1) (reg 3),
    .branch .eq (reg 5) (reg 1) 4,
    .copy (.direct 0) (.immediate 0),
    .halt,
    .binary .band (.direct 6) (reg 2) (reg 4),
    .branch .eq (reg 6) (reg 2) 8,
    .copy (.direct 0) (.immediate 0),
    .halt,
    .copy (.direct 0) (.immediate 1),
    .halt], 1, by decide⟩

def result (s : State w) : State w := run widthConstant (algorithm.program w) 6 s

theorem executes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    (result s).mem 0 =
      (if (s.mem 1 &&& s.mem 3 = s.mem 1) ∧ (s.mem 2 &&& s.mem 4 = s.mem 2) then 1 else 0) ∧
    (result s).halted = true ∧ (result s).ticks ≤ s.ticks + 6 := by
  by_cases first : s.mem 1 &&& s.mem 3 = s.mem 1
  all_goals by_cases second : s.mem 2 &&& s.mem 4 = s.mem 2
  all_goals simp [result, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Operand.read, Address.resolve, Memory.write, BinOp.eval, Comparison.test,
    pc, live, first, second, Nat.add_assoc]

theorem frame (s : State w) (pc : s.pc = 0) (live : s.halted = false) (address : Nat)
    (notOutput : address ≠ 0) (notScratch1 : address ≠ 5) (notScratch2 : address ≠ 6) :
    (result s).mem address = s.mem address := by
  by_cases first : s.mem 1 &&& s.mem 3 = s.mem 1
  all_goals by_cases second : s.mem 2 &&& s.mem 4 = s.mem 2
  all_goals simp [result, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Operand.read, Address.resolve, Memory.write, BinOp.eval, Comparison.test,
    pc, live, first, second, notOutput, notScratch1, notScratch2]

theorem trace (s : State w) :
    ∃ time, time ≤ 6 ∧ Runs widthConstant (algorithm.program w) time s (result s) :=
  run_has_trace widthConstant (algorithm.program w) 6 s

/-- This is an actual instruction trace for clause subsumption. Loading masks
and constructing the containing formula's representation are separate costs. -/
theorem decides_subset (a b : Clause n) (fits : n ≤ w.bits) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (aPos : s.mem 1 = Masks.encode w a true) (aNeg : s.mem 2 = Masks.encode w a false)
    (bPos : s.mem 3 = Masks.encode w b true) (bNeg : s.mem 4 = Masks.encode w b false) :
    ∃ time, time ≤ 6 ∧ Runs widthConstant (algorithm.program w) time s (result s) ∧
      (result s).halted = true ∧ (result s).mem 0 = (if a ⊆ b then 1 else 0) := by
  obtain ⟨time, bound, run⟩ := trace s
  have correct := executes s pc live
  refine ⟨time, bound, run, correct.2.1, ?_⟩
  rw [correct.1, aPos, aNeg, bPos, bNeg]
  simp only [← Masks.subset_iff a b fits]

end WordRAM.Conjectures.Sparsification.SubsetMachine

/-! Actual wordRAM construction of a petal from clause and core masks. -/
namespace WordRAM.Conjectures.Sparsification.PetalMachine

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

/-- Clause masks are in cells 1,2; core masks in 3,4. Output masks are in
cells 6,7. Cell 5 is scratch; all input cells are preserved. -/
def algorithm : Algorithm :=
  ⟨[.bitNot (.direct 5) (reg 3),
    .binary .band (.direct 6) (reg 1) (reg 5),
    .bitNot (.direct 5) (reg 4),
    .binary .band (.direct 7) (reg 2) (reg 5),
    .halt], 1, by decide⟩

def result (s : State w) : State w := run widthConstant (algorithm.program w) 5 s

theorem executes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    (result s).mem 6 = s.mem 1 &&& ~~~s.mem 3 ∧
    (result s).mem 7 = s.mem 2 &&& ~~~s.mem 4 ∧
    (result s).halted = true ∧ (result s).ticks = s.ticks + 5 := by
  simp [result, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Operand.read, Address.resolve, Memory.write, BinOp.eval, pc, live, Nat.add_assoc]

theorem frame (s : State w) (pc : s.pc = 0) (live : s.halted = false) (address : Nat)
    (notScratch : address ≠ 5) (notPositive : address ≠ 6) (notNegative : address ≠ 7) :
    (result s).mem address = s.mem address := by
  simp [result, algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile,
    reg, run, step, execute, Operand.read, Address.resolve, Memory.write, BinOp.eval, pc, live,
    notScratch, notPositive, notNegative]

theorem trace (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    Runs widthConstant (algorithm.program w) 5 s (result s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) 5 s
  change Runs widthConstant (algorithm.program w) time s (result s) at trace
  have cost := runs_cost trace
  have exactCost := (executes s pc live).2.2.2
  have eq : time = 5 := by omega
  simpa only [eq] using trace

/-- The output represents the very same list-filter petal used by the
combinatorial procedure. Input mask construction is a separate stage. -/
theorem builds_petal (core clause : Clause n) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (clausePos : s.mem 1 = Masks.encode w clause true) (clauseNeg : s.mem 2 = Masks.encode w clause false)
    (corePos : s.mem 3 = Masks.encode w core true) (coreNeg : s.mem 4 = Masks.encode w core false) :
    Runs widthConstant (algorithm.program w) 5 s (result s) ∧ (result s).halted = true ∧
      (result s).mem 6 = Masks.encode w (Branch.petal core clause) true ∧
      (result s).mem 7 = Masks.encode w (Branch.petal core clause) false := by
  have correct := executes s pc live
  refine ⟨trace s pc live, correct.2.2.1, ?_, ?_⟩
  · rw [correct.1, clausePos, corePos, Masks.petal_mask]
  · rw [correct.2.1, clauseNeg, coreNeg, Masks.petal_mask]

end WordRAM.Conjectures.Sparsification.PetalMachine