SETH ⇒ OVC sparsification bundle 26: 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_25

set_option autoImplicit true

/-! Testing one enumerated flower core using actual wordRAM instructions. -/
namespace WordRAM.Conjectures.Sparsification.CandidateMachine

/-- Equal cleaned and original lengths characterize the absence of duplicates. -/
theorem clean_length_iff (clause : Clause n) :
    (Normalize.clean clause).length = clause.length ↔ clause.Nodup := by
  induction clause with
  | nil => simp [Normalize.clean]
  | cons literal rest ih =>
    by_cases member : literal ∈ rest
    · have bound := Normalize.clean_length rest
      simp only [Normalize.clean, if_pos member, List.length_cons, List.nodup_cons]
      constructor
      · intro eq; omega
      · rintro ⟨absent, _⟩; exact False.elim (absent member)
    · simpa [Normalize.clean, member, List.nodup_cons] using ih

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 9) (reg 1), .copy (.direct 10) (reg 2), .copy (.direct 5) (reg 2), .halt], 1, by decide⟩

def restore (length size : Nat) : Algorithm :=
  ⟨[.binary .sub (.direct 0) (reg 0) (.immediate length),
    .copy (.direct 1) (reg 9), .copy (.direct 2) (reg 10), .copy (.direct 8) (.immediate size), .halt], 1, by decide⟩

def reject : Algorithm := ⟨[.copy (.direct 0) (.immediate 0), .halt], 1, by decide⟩

def compare (threshold : Nat) : Algorithm :=
  ⟨[.branch .le (.immediate threshold) (reg 14) 3, .copy (.direct 0) (.immediate 0), .halt,
    .copy (.direct 0) (.immediate 1), .halt], 1, by decide⟩

def countAndCompare (threshold : Nat) : Algorithm :=
  ⟨SourceChain.code FamilyScan.initialized.code (compare threshold).code, 1, by decide⟩

def lengthCheck (length size : Nat) : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code SizeMachine.algorithm.code (restore length size).code), 1, by decide⟩

/-- Parameters are fixed for a particular position in the core enumeration.
Input core masks are 1,2; table count and cursor are 11,12. Result is Boolean 0. -/
def algorithm (length size threshold : Nat) : Algorithm :=
  ⟨SourceChain.code (lengthCheck length size).code
    (SourceIf.code 0 (countAndCompare threshold).code reject.code), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 9 = s.mem 1 ∧ t.mem 10 = s.mem 2 ∧
      t.mem 5 = s.mem 2 ∧ (∀ a, a ≠ 9 → a ≠ 10 → a ≠ 5 → 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 h9 h10 h5; simp [h9, h10, h5]

theorem restores (length size : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((restore length size).program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 0 = s.mem 0 - BitVec.ofNat w.bits length ∧
      t.mem 1 = s.mem 9 ∧ t.mem 2 = s.mem 10 ∧ t.mem 8 = BitVec.ofNat w.bits size ∧
      (∀ a, a ≠ 0 → a ≠ 1 → a ≠ 2 → a ≠ 8 → t.mem a = s.mem a) := by
  simp [restore, 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 h0 h1 h2 h8; simp [h0, h1, h2, h8]

theorem rejects (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (reject.program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 0 = 0#w.bits ∧
      (∀ a, a ≠ 0 → t.mem a = s.mem a) := by
  simp [reject, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h; simp [h]

theorem compares (threshold : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (fits : threshold < 2 ^ w.bits) :
    let t := run widthConstant ((compare threshold).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧
      t.mem 0 = (if threshold ≤ (s.mem 14).toNat then 1#w.bits else 0#w.bits) ∧
      (∀ a, a ≠ 0 → t.mem a = s.mem a) := by
  by_cases enough : threshold ≤ (s.mem 14).toNat
  all_goals simp [compare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, Comparison.test, pc, live,
    Nat.mod_eq_of_lt fits, enough, Nat.add_assoc]
  all_goals intro a h; 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 counts_and_compares (core : Clause n) (clauses : CNF n) (size threshold : Nat)
    (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (fits : address + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits) (thresholdFits : threshold < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
    (target : s.mem 8 = BitVec.ofNat w.bits size)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 18 * clauses.length + 7 ∧
      Runs widthConstant ((countAndCompare threshold).program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if threshold ≤ (Flowers.family clauses core size).length then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨time, counted, bound, trace, halted, result, frame⟩ :=
    FamilyScan.counts_family core clauses size s address pc live base fits variablesFit width sizeFits nodup
      qp qn target pointer remaining input
  let out := run widthConstant ((compare threshold).program w) 3 (SourceChain.resume counted)
  obtain ⟨outHalt, ticks, decision, preserved⟩ := compares threshold (SourceChain.resume counted) rfl rfl thresholdFits
  have full := SourceChain.traces FamilyScan.initialized.code (compare threshold).code s counted out time 3
    live halted trace (trace_of_ticks _ _ 3 ticks)
  refine ⟨time + 3, out.relocate FamilyScan.initialized.code.length, by omega, full, outHalt, ?_, ?_⟩
  · simpa only [SourceChain.resume, result, out, State.relocate] using decision
  · intro a ha; exact (preserved a (by omega)).trans (frame a ha)

/-- Population counts detect duplicate literals in a candidate core. The
original masks and table control registers are restored for the family scan. -/
theorem checks_length (core : Clause n) (length size : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits)
    (lengthEq : core.length = length) (lengthFits : length < 2 ^ w.bits)
    (qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false) :
    ∃ final, Runs widthConstant ((lengthCheck length size).program w) (12 * w.bits + 22) s final ∧
      final.halted = true ∧ final.mem 1 = Masks.encode w core true ∧ final.mem 2 = Masks.encode w core false ∧
      final.mem 8 = BitVec.ofNat w.bits size ∧ (final.mem 0 = 0#w.bits ↔ core.Nodup) ∧
      (∀ a, 11 ≤ a → final.mem a = s.mem a) := by
  let saved := run widthConstant (prepare.program w) 4 s
  obtain ⟨savedHalt, savedTicks, savedPos, savedNeg, loadedNeg, savedFrame⟩ := prepares s pc live
  obtain ⟨counted, countTrace, countedHalt, countedWord, countFrame⟩ :=
    SizeMachine.counts (Masks.encode w core true) (Masks.encode w core false) (SourceChain.resume saved) rfl rfl
      ((savedFrame 1 (by decide) (by decide) (by decide)).trans qp) (loadedNeg.trans qn)
  have exactWord : counted.mem 0 = BitVec.ofNat w.bits (Normalize.clean core).length := by
    rw [countedWord]
    apply BitVec.eq_of_toNat_eq
    simp only [BitVec.toNat_add, BitVec.toNat_ofNat, MaskCardinality.count_distinct core variablesFit]
  have keptPos : counted.mem 9 = Masks.encode w core true :=
    (countFrame 9 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedPos.trans qp)
  have keptNeg : counted.mem 10 = Masks.encode w core false :=
    (countFrame 10 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (savedNeg.trans qn)
  let out := run widthConstant ((restore length size).program w) 5 (SourceChain.resume counted)
  obtain ⟨outHalt, outTicks, difference, pos, neg, target, outFrame⟩ := restores length size (SourceChain.resume counted) rfl rfl
  have tail := SourceChain.traces SizeMachine.algorithm.code (restore length size).code
    (SourceChain.resume saved) counted out (12 * w.bits + 13) 5 rfl countedHalt countTrace (trace_of_ticks _ _ 5 outTicks)
  have full := SourceChain.traces prepare.code (SourceChain.code SizeMachine.algorithm.code (restore length size).code)
    s saved _ 4 ((12 * w.bits + 13) + 5) live savedHalt (trace_of_ticks _ s 4 savedTicks) tail
  refine ⟨(out.relocate SizeMachine.algorithm.code.length).relocate prepare.code.length,
    ?_, outHalt, pos.trans keptPos, neg.trans keptNeg, target, ?_, ?_⟩
  · have cost : 4 + ((12 * w.bits + 13) + 5) = 12 * w.bits + 22 := by omega
    simpa only [lengthCheck, Algorithm.program, cost] using full
  · change out.mem 0 = 0#w.bits ↔ _
    rw [difference]
    change counted.mem 0 - BitVec.ofNat w.bits length = 0#w.bits ↔ _
    rw [exactWord, BitVec.sub_eq_iff_eq_add, BitVec.zero_add]
    constructor
    · intro eq
      have values := congrArg BitVec.toNat eq
      have cleanFits := SizeMachine.size_fits core variablesFit width
      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt cleanFits, Nat.mod_eq_of_lt lengthFits] at values
      exact (clean_length_iff core).mp (values.trans lengthEq.symm)
    · intro nodup
      rw [Normalize.clean_eq core nodup, lengthEq]
  · intro a ha
    exact (outFrame a (by omega) (by omega) (by omega) (by omega)).trans
      ((countFrame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
        (savedFrame a (by omega) (by omega) (by omega)))

/-- Uniform test of duplicate-freeness and the required family cardinality. -/
theorem tests (core : Clause n) (clauses : CNF n) (length size threshold : Nat)
    (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (fits : address + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (lengthEq : core.length = length) (lengthFits : length < 2 ^ w.bits)
    (sizeFits : size < 2 ^ w.bits) (thresholdFits : threshold < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 12 * w.bits + 18 * clauses.length + 30 ∧
      Runs widthConstant ((algorithm length size threshold).program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if core.Nodup ∧ threshold ≤ (Flowers.family clauses core size).length then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨checked, prefixTrace, checkedHalt, cp, cn, target, zeroIff, prefixFrame⟩ :=
    checks_length core length size s pc live variablesFit width lengthEq lengthFits qp qn
  let entry := (SourceChain.resume checked).addTicks 1
  have entryInput : VectorBuilder.Stored entry.mem address (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact prefixFrame a (by omega)
  have branch : ∃ time out, time ≤ 18 * clauses.length + 8 ∧
      Runs widthConstant ((SourceIf.code 0 (countAndCompare threshold).code reject.code).map (SourceInstruction.compile w))
        time (SourceChain.resume checked) out ∧ out.halted = true ∧
      out.mem 0 = (if core.Nodup ∧ threshold ≤ (Flowers.family clauses core size).length then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → out.mem a = checked.mem a) := by
    by_cases coreNodup : core.Nodup
    · obtain ⟨time, out, bound, trace, halted, result, frame⟩ :=
        counts_and_compares core clauses size threshold entry address rfl rfl base fits variablesFit width sizeFits thresholdFits nodup
          cp cn target ((prefixFrame 12 (by decide)).trans pointer) ((prefixFrame 11 (by decide)).trans remaining) entryInput
      have linked := SourceIf.zero_trace 0 (countAndCompare threshold).code reject.code
        (SourceChain.resume checked) out time rfl rfl (zeroIff.mpr coreNodup) trace
      refine ⟨1 + time, out.relocate (1 + reject.code.length), by omega, linked, halted, ?_, ?_⟩
      · simpa only [coreNodup, true_and, State.relocate] using result
      · intro a ha; exact frame a ha
    · have nonzero : (SourceChain.resume checked).mem 0 ≠ 0#w.bits := fun h => coreNodup (zeroIff.mp h)
      let out := run widthConstant (reject.program w) 2 entry
      obtain ⟨halted, ticks, result, frame⟩ := rejects entry rfl rfl
      have linked := SourceIf.nonzero_trace 0 (countAndCompare threshold).code reject.code
        (SourceChain.resume checked) out 2 rfl rfl nonzero (trace_of_ticks _ entry 2 ticks)
      refine ⟨3, out.relocate 1, by omega, linked, halted, ?_, ?_⟩
      · simpa only [coreNodup, false_and, ↓reduceIte, State.relocate, out] using result
      · intro a ha; exact frame a (by omega)
  obtain ⟨time, out, bound, trace, halted, result, frame⟩ := branch
  have full := SourceChain.traces (lengthCheck length size).code (SourceIf.code 0 (countAndCompare threshold).code reject.code)
    s checked out (12 * w.bits + 22) time live checkedHalt prefixTrace trace
  refine ⟨12 * w.bits + 22 + time, out.relocate (lengthCheck length size).code.length,
    by omega, full, halted, result, ?_⟩
  intro a ha; exact (frame a ha).trans (prefixFrame a (by omega))

/-- The tested proposition is exactly the flower candidate from the existing
sparsification development. Positive proper core lengths are fixed by the
surrounding enumeration; the instruction sequence is independent of the core. -/
theorem tests_candidate (core : Clause n) (clauses : CNF n) (length size : Nat) (threshold : Nat → Nat)
    (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false) (base : 16 ≤ address)
    (fits : address + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (lengthEq : core.length = length) (positive : 0 < length) (proper : length < size)
    (lengthFits : length < 2 ^ w.bits) (sizeFits : size < 2 ^ w.bits)
    (thresholdFits : threshold (size - length) < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (qp : s.mem 1 = Masks.encode w core true) (qn : s.mem 2 = Masks.encode w core false)
    (pointer : s.mem 12 = BitVec.ofNat w.bits address)
    (remaining : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 12 * w.bits + 18 * clauses.length + 30 ∧
      Runs widthConstant ((algorithm length size (threshold (size - length))).program w) time s final ∧ final.halted = true ∧
      final.mem 0 = (if Flowers.Candidate clauses threshold core size then 1#w.bits else 0#w.bits) ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨time, final, bound, trace, halted, result, frame⟩ :=
    tests core clauses length size (threshold (size - length)) s address pc live base fits variablesFit width
      lengthEq lengthFits sizeFits thresholdFits nodup qp qn pointer remaining input
  refine ⟨time, final, bound, trace, halted, ?_, frame⟩
  simpa only [Flowers.Candidate, lengthEq, positive, proper, true_and] using result

end WordRAM.Conjectures.Sparsification.CandidateMachine

/-! Ordered literal codes and the finite search bound for core enumeration. -/
namespace WordRAM.Conjectures.Sparsification.CoreEnumeration

/-- Codes first enumerate all positive literals, then all negative literals,
matching `Counting.literals` rather than interleaving the polarities. -/
def literal (n : Nat) (code : Fin (n + n)) : Literal n :=
  if h : code.val < n then ⟨⟨code.val, h⟩, true⟩
  else ⟨⟨code.val - n, by have := code.isLt; omega⟩, false⟩

theorem literal_order (n : Nat) : List.ofFn (literal n) = Counting.literals n := by
  rw [List.ofFn_add]
  unfold Counting.literals
  congr 1
  · congr 1
    funext i
    simp [literal, i.isLt]
  · congr 1
    funext i
    simp [literal]

theorem flatMap_length_le (xs : List α) (f : α → List β) (bound : Nat)
    (lengths : ∀ x ∈ xs, (f x).length ≤ bound) : (xs.flatMap f).length ≤ xs.length * bound := by
  induction xs with
  | nil => simp
  | cons x xs ih =>
    have first := lengths x (by simp)
    have rest := ih (fun y h => lengths y (by simp [h]))
    simp only [List.flatMap_cons, List.length_append, List.length_cons, Nat.add_mul, Nat.one_mul]
    omega

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

/-- Translate a literal code in 20 using n in 21. The serialized literal's
index and polarity are returned in 22 and 23, respectively. -/
def decoder : Algorithm :=
  ⟨[.branch .lt (reg 20) (reg 21) 4,
    .binary .sub (.direct 22) (reg 20) (reg 21), .copy (.direct 23) (.immediate 0), .halt,
    .copy (.direct 22) (reg 20), .copy (.direct 23) (.immediate 1), .halt], 1, by decide⟩

theorem decodes (n : Nat) (code : Fin (n + n)) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (input : s.mem 20 = BitVec.ofNat w.bits code.val) (variables : s.mem 21 = BitVec.ofNat w.bits n) :
    let t := run widthConstant (decoder.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧
      t.mem 22 = BitVec.ofNat w.bits (literal n code).index.val ∧
      t.mem 23 = (if (literal n code).positive then 1#w.bits else 0#w.bits) ∧
      (∀ a, a ≠ 22 → a ≠ 23 → t.mem a = s.mem a) := by
  have room := SizeMachine.double_width_fits w.bits width
  have codeFits : code.val < 2 ^ w.bits := by have := code.isLt; omega
  have nFits : n < 2 ^ w.bits := by omega
  by_cases positive : code.val < n
  · simp [decoder, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
      Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, input, variables,
      literal, positive, Nat.mod_eq_of_lt codeFits, Nat.mod_eq_of_lt nFits, Nat.add_assoc]
    intro a h22 h23; simp [h22, h23]
  · have sub : BitVec.ofNat w.bits code.val - BitVec.ofNat w.bits n = BitVec.ofNat w.bits (code.val - n) :=
      BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)
    simp [decoder, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
      Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test, pc, live, input, variables,
      literal, positive, sub, Nat.mod_eq_of_lt codeFits, Nat.mod_eq_of_lt nFits, Nat.add_assoc]
    intro a h22 h23; simp [h22, h23]

/-- All suffixes of a partially written core, retaining the original order. -/
def completions (prefixCore : Clause n) (remaining : Nat) : CNF n :=
  (Selection.cores n remaining).map (prefixCore ++ ·)

@[simp] theorem completions_zero (prefixCore : Clause n) : completions prefixCore 0 = [prefixCore] := by
  simp [completions, Selection.cores]

/-- The group explored after selecting a literal code at the current depth. -/
def block (prefixCore : Clause n) (remaining code : Nat) : CNF n :=
  if h : code < n + n then completions (prefixCore ++ [literal n ⟨code, h⟩]) remaining else []

private theorem code_range (n : Nat) :
    (List.ofFn (fun i : Fin n => i)).map Fin.val = List.range' 0 n := by
  apply List.ext_getElem
  · simp
  · intro i hi hj; simp

/-- Flattening nested literal-code loops gives exactly `Selection.cores`'s
ordering, with the already-written prefix attached to every candidate. -/
theorem completions_succ (prefixCore : Clause n) (remaining : Nat) :
    completions prefixCore (remaining + 1) =
      (List.range' 0 (n + n)).flatMap (block prefixCore remaining) := by
  have literals : Counting.literals n = (List.ofFn (fun i : Fin (n + n) => i)).map (literal n) := by
    simp only [List.map_ofFn, Function.comp_def, literal_order]
  rw [completions, Selection.cores, List.map_flatMap, literals, ← code_range, List.flatMap_map, List.flatMap_map]
  congr 1
  funext code
  simp [block, code.isLt, completions, List.map_map, Function.comp_def, List.append_assoc]

/-- A nested ordered search may stop at the first nonempty successful group;
its answer is the same as searching the flattened candidate list. -/
theorem find_flatMap (xs : List α) (groups : α → List β) (test : β → Bool) :
    (xs.flatMap groups).find? test =
      (xs.find? (fun x => ((groups x).find? test).isSome)).bind (fun x => (groups x).find? test) := by
  induction xs with
  | nil => rfl
  | cons x xs ih =>
    rw [List.flatMap_cons, List.find?_append, List.find?_cons]
    cases result : (groups x).find? test <;> simp [result, ih]

theorem first_completion (prefixCore : Clause n) (remaining : Nat) (test : Clause n → Bool) :
    (completions prefixCore (remaining + 1)).find? test =
      ((List.range' 0 (n + n)).find? (fun code => ((block prefixCore remaining code).find? test).isSome)).bind
        (fun code => (block prefixCore remaining code).find? test) := by
  rw [completions_succ, find_flatMap]

end WordRAM.Conjectures.Sparsification.CoreEnumeration

/-! Writing the literal selected by one level of the ordered core search. -/
namespace WordRAM.Conjectures.Sparsification.LiteralWriter

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

def prepare (index : Nat) : Algorithm :=
  ⟨[.copy (.direct 20) (reg index), .copy (.direct 21) (reg 16), .halt], 1, by decide⟩

def store (address : Nat) : Algorithm :=
  ⟨[.copy (.direct address) (reg 22), .copy (.direct (address + 1)) (reg 23), .halt], 1, by decide⟩

/-- The current literal code is read from a loop cell; n is saved in 16.
Write the serialized literal pair at the fixed core-buffer address. -/
def algorithm (index address : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare index).code
    (SourceChain.code CoreEnumeration.decoder.code (store address).code), 1, by decide⟩

theorem prepares (index : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((prepare index).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 20 = s.mem index ∧ t.mem 21 = s.mem 16 ∧
      (∀ a, a ≠ 20 → a ≠ 21 → 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 h20 h21; simp [h20, h21]

theorem stores (address : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) (base : 24 ≤ address) :
    let t := run widthConstant ((store address).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem address = s.mem 22 ∧ t.mem (address + 1) = s.mem 23 ∧
      (∀ a, a ≠ address → a ≠ address + 1 → t.mem a = s.mem a) := by
  have different : address ≠ 23 ∧ 23 ≠ address ∧ address + 1 ≠ address ∧ address ≠ address + 1 := by omega
  simp [store, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, different, Nat.add_assoc]
  intro a h0 h1; simp [h0, h1]

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 writes (n : Nat) (code : Fin (n + n)) (index address : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 24 ≤ address)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (input : s.mem index = BitVec.ofNat w.bits code.val) (variables : s.mem 16 = BitVec.ofNat w.bits n) :
    ∃ final, Runs widthConstant ((algorithm index address).program w) 10 s final ∧ final.halted = true ∧
      final.mem address = BitVec.ofNat w.bits (CoreEnumeration.literal n code).index.val ∧
      final.mem (address + 1) = (if (CoreEnumeration.literal n code).positive then 1#w.bits else 0#w.bits) ∧
      (∀ a, a ≠ 20 → a ≠ 21 → a ≠ 22 → a ≠ 23 → a ≠ address → a ≠ address + 1 → final.mem a = s.mem a) := by
  let prepared := run widthConstant ((prepare index).program w) 3 s
  obtain ⟨preparedHalt, preparedTicks, digit, size, pf⟩ := prepares index s pc live
  let decoded := run widthConstant (CoreEnumeration.decoder.program w) 4 (SourceChain.resume prepared)
  obtain ⟨decodedHalt, decodedTicks, literalIndex, polarity, df⟩ :=
    CoreEnumeration.decodes n code (SourceChain.resume prepared) rfl rfl width variablesFit (digit.trans input) (size.trans variables)
  let out := run widthConstant ((store address).program w) 3 (SourceChain.resume decoded)
  obtain ⟨halted, ticks, first, second, frame⟩ := stores address (SourceChain.resume decoded) rfl rfl base
  have tail := SourceChain.traces CoreEnumeration.decoder.code (store address).code
    (SourceChain.resume prepared) decoded out 4 3 rfl decodedHalt (trace_of_ticks _ _ 4 decodedTicks) (trace_of_ticks _ _ 3 ticks)
  have full := SourceChain.traces (prepare index).code (SourceChain.code CoreEnumeration.decoder.code (store address).code)
    s prepared _ 3 (4 + 3) live preparedHalt (trace_of_ticks _ s 3 preparedTicks) tail
  refine ⟨(out.relocate CoreEnumeration.decoder.code.length).relocate (prepare index).code.length,
    full, halted, first.trans literalIndex, second.trans polarity, ?_⟩
  intro a h20 h21 h22 h23 h0 h1
  exact (frame a h0 h1).trans ((df a h22 h23).trans (pf a h20 h21))

end WordRAM.Conjectures.Sparsification.LiteralWriter