SETH ⇒ OVC sparsification bundle 27: 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_26

set_option autoImplicit true

/-! The leaf predicate of the nested core-enumeration loops. -/
namespace WordRAM.Conjectures.Sparsification.CoreLeaf

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

def setup (length address : Nat) : Algorithm :=
  ⟨[.copy (.direct 1) (.immediate address), .copy (.direct 2) (.immediate length), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 1) (reg 3), .copy (.direct 2) (reg 4),
    .copy (.direct 11) (reg 17), .copy (.direct 12) (reg 18), .halt], 1, by decide⟩

/-- Construct the core masks from the enumerated literal array, restore the
saved formula count/pointer from 17,18, and test the candidate. -/
def algorithm (length size threshold address : Nat) : Algorithm :=
  ⟨SourceChain.code (setup length address).code (SourceChain.code MaskBuilder.initialized.code
    (SourceChain.code bridge.code (CandidateMachine.algorithm length size threshold).code)), 1, by decide⟩

theorem initializes (length address : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((setup length address).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem 1 = BitVec.ofNat w.bits address ∧
      t.mem 2 = BitVec.ofNat w.bits length ∧ (∀ a, a ≠ 1 → a ≠ 2 → t.mem a = s.mem a) := by
  simp [setup, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h1 h2; simp [h1, h2]

theorem bridges (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧ t.mem 1 = s.mem 3 ∧ t.mem 2 = s.mem 4 ∧
      t.mem 11 = s.mem 17 ∧ t.mem 12 = s.mem 18 ∧
      (∀ a, a ≠ 1 → a ≠ 2 → a ≠ 11 → a ≠ 12 → 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, pc, live, Nat.add_assoc]
  intro a h1 h2 h11 h12; simp [h1, h2, h11, h12]

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

/-- Complete leaf execution, including mask construction, data movement,
duplicate detection, family counting, and threshold comparison. The literal
array and every search-loop cell at addresses ≥16 are preserved. -/
theorem tests_candidate (core : Clause n) (clauses : CNF n) (length size : Nat) (threshold : Nat → Nat)
    (s : State w) (coreAddress tableAddress : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (coreBase : 16 ≤ coreAddress) (tableBase : 16 ≤ tableAddress)
    (coreFits : coreAddress + 2 * core.length < 2 ^ w.bits)
    (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (width : 3 ≤ w.bits) (lengthEq : core.length = length) (positive : 0 < length) (proper : length < size)
    (sizeFits : size < 2 ^ w.bits) (thresholdFits : threshold (size - length) < 2 ^ w.bits)
    (nodup : ∀ clause ∈ clauses, clause.Nodup)
    (count : s.mem 17 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 18 = BitVec.ofNat w.bits tableAddress)
    (coreInput : MaskBuilder.Encoded s.mem coreAddress (core.map (MaskBuilder.wordLiteral w)))
    (tableInput : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ 10 * length + 12 * w.bits + 18 * clauses.length + 42 ∧
      Runs widthConstant ((algorithm length size (threshold (size - length)) coreAddress).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
  let prepared := run widthConstant ((setup length coreAddress).program w) 3 s
  obtain ⟨preparedHalt, preparedTicks, pp, pcnt, pf⟩ := initializes length coreAddress s pc live
  have coreInput' : MaskBuilder.Encoded prepared.mem coreAddress (core.map (MaskBuilder.wordLiteral w)) := by
    apply MaskTable.pair_frame _ _ coreInput
    intro a lo _; exact pf a (by omega) (by omega)
  obtain ⟨parsed, parseTrace, parsedHalt, pos, neg, parseFrame⟩ :=
    MaskBuilder.initialized_builds_clause core (SourceChain.resume prepared) coreAddress rfl rfl (by omega)
      coreFits variablesFit pp (by simpa only [lengthEq, SourceChain.resume, prepared] using pcnt) coreInput'
  have parsedFrame : ∀ a, 16 ≤ a → parsed.mem a = s.mem a := by
    intro a ha; exact (parseFrame a (by omega)).trans (pf a (by omega) (by omega))
  let staged := run widthConstant (bridge.program w) 5 (SourceChain.resume parsed)
  obtain ⟨stagedHalt, stagedTicks, qp, qn, stagedCount, stagedPointer, stagedFrame⟩ := bridges (SourceChain.resume parsed) rfl rfl
  have stagedInput : VectorBuilder.Stored staged.mem tableAddress (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ tableInput
    intro a lo _
    exact (stagedFrame a (by omega) (by omega) (by omega) (by omega)).trans (parsedFrame a (by omega))
  obtain ⟨time, out, bound, trace, halted, result, frame⟩ :=
    CandidateMachine.tests_candidate core clauses length size threshold (SourceChain.resume staged) tableAddress rfl rfl tableBase
      tableFits variablesFit width lengthEq positive proper (by omega) sizeFits thresholdFits nodup
      (qp.trans pos) (qn.trans neg)
      (stagedPointer.trans ((parsedFrame 18 (by decide)).trans pointer))
      (stagedCount.trans ((parsedFrame 17 (by decide)).trans count)) stagedInput
  have tail := SourceChain.traces bridge.code (CandidateMachine.algorithm length size (threshold (size - length))).code
    (SourceChain.resume parsed) staged out 5 time rfl stagedHalt (trace_of_ticks _ _ 5 stagedTicks) trace
  have body := SourceChain.traces MaskBuilder.initialized.code
    (SourceChain.code bridge.code (CandidateMachine.algorithm length size (threshold (size - length))).code)
    (SourceChain.resume prepared) parsed _ (10 * core.length + 4) (5 + time) rfl parsedHalt parseTrace tail
  have full := SourceChain.traces (setup length coreAddress).code
    (SourceChain.code MaskBuilder.initialized.code (SourceChain.code bridge.code (CandidateMachine.algorithm length size (threshold (size - length))).code))
    s prepared _ 3 ((10 * core.length + 4) + (5 + time)) live preparedHalt (trace_of_ticks _ s 3 preparedTicks) body
  refine ⟨3 + ((10 * core.length + 4) + (5 + time)),
    ((out.relocate bridge.code.length).relocate MaskBuilder.initialized.code.length).relocate (setup length coreAddress).code.length,
    by omega, full, halted, result, ?_⟩
  intro a ha
  exact (frame a ha).trans ((stagedFrame a (by omega) (by omega) (by omega) (by omega)).trans (parsedFrame a ha))

end WordRAM.Conjectures.Sparsification.CoreLeaf

/-! A finite ordered search loop, linking a verified predicate subroutine. -/
namespace WordRAM.Conjectures.SourceSearch

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

def header (index limit length : Nat) : List SourceInstruction :=
  [.branch .eq (reg index) (reg limit) (length + 4)]

def trailer (index length : Nat) : List SourceInstruction :=
  [.branch .eq (reg 0) (.immediate 1) (length + 5),
   .binary .add (.direct index) (reg index) (.immediate 1), .jump 0,
   .copy (.direct 0) (.immediate 0), .halt]

/-- Start with an index less than or equal to the exclusive limit. The body
returns its Boolean answer in 0. Success preserves its witness memory; failure
increments the index and repeats. The body must preserve the two loop cells. -/
def algorithm (index limit : Nat) (body : List SourceInstruction) : Algorithm :=
  ⟨header index limit body.length ++
    (body.map (SourceInstruction.returnTo body.length)).map (SourceInstruction.relocate 1) ++
    trailer index body.length, 1, by decide⟩

private theorem program_eq (w : Width) (index limit : Nat) (body : List SourceInstruction) :
    (algorithm index limit body).program w =
      (header index limit body.length).map (SourceInstruction.compile w) ++
      ((((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length)).map (Instruction.relocate 1)) ++
        (trailer index body.length).map (SourceInstruction.compile w)) := by
  simp only [algorithm, Algorithm.program, List.map_append, List.map_map, Function.comp_def,
    compile_relocate, compile_returnTo, List.append_assoc]

private theorem tail_fetch (w : Width) (index limit : Nat) (body : List SourceInstruction) (i : Nat) :
    ((algorithm index limit body).program w)[body.length + 1 + i]? =
      ((trailer index body.length).map (SourceInstruction.compile w))[i]? := by
  rw [program_eq]
  have address : body.length + 1 + i = (body.length + i) + 1 := by omega
  rw [address]
  simp only [header, List.map_cons, List.map_nil, List.cons_append, List.nil_append, List.getElem?_cons_succ]
  rw [List.getElem?_append_right (by simp)]
  simp

theorem enters (index limit : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (different : s.mem index ≠ s.mem limit) :
    let t := run widthConstant ((algorithm index limit body).program w) 1 s
    t.pc = 1 ∧ t.halted = false ∧ t.ticks = s.ticks + 1 ∧ t.mem = s.mem := by
  have fetch : ((algorithm index limit body).program w)[0]? =
      some (.branch .eq (.memory (.direct index)) (.memory (.direct limit)) (body.length + 4)) := by
    simp [algorithm, header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg]
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, different, fetch]

theorem succeeds (index limit : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = body.length + 1) (live : s.halted = false) (yes : s.mem 0 = 1#w.bits) :
    let t := run widthConstant ((algorithm index limit body).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem = s.mem := by
  have f0 : ((algorithm index limit body).program w)[body.length + 1]? =
      some (.branch .eq (.memory (.direct 0)) (.immediate 1) (body.length + 5)) := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg] using tail_fetch w index limit body 0
  have f4 : ((algorithm index limit body).program w)[body.length + 5]? = some .halt := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg, Nat.add_assoc] using tail_fetch w index limit body 4
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, yes, f0, f4, Nat.add_assoc]

theorem advances (index limit : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = body.length + 1) (live : s.halted = false) (no : s.mem 0 = 0#w.bits) :
    let t := run widthConstant ((algorithm index limit body).program w) 3 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 3 ∧
      t.mem = s.mem.write index (s.mem index + 1#w.bits) := by
  have f0 : ((algorithm index limit body).program w)[body.length + 1]? =
      some (.branch .eq (.memory (.direct 0)) (.immediate 1) (body.length + 5)) := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg] using tail_fetch w index limit body 0
  have f1 : ((algorithm index limit body).program w)[body.length + 2]? =
      some (.binary .add (.direct index) (.memory (.direct index)) (.immediate 1)) := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg, Nat.add_assoc] using tail_fetch w index limit body 1
  have f2 : ((algorithm index limit body).program w)[body.length + 3]? = some (.jump 0) := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg, Nat.add_assoc] using tail_fetch w index limit body 2
  have nonzero : (0#w.bits) ≠ 1#w.bits := by
    intro eq
    have values := congrArg BitVec.toNat eq
    have fits : 1 < 2 ^ w.bits := Nat.one_lt_two_pow (by have := w.positive; omega)
    simp [Nat.mod_eq_of_lt fits] at values
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, BinOp.eval,
    pc, live, no, nonzero, f0, f1, f2, Nat.add_assoc]

theorem exits (index limit : Nat) (body : List SourceInstruction) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (done : s.mem index = s.mem limit) :
    let t := run widthConstant ((algorithm index limit body).program w) 3 s
    t.halted = true ∧ t.ticks = s.ticks + 3 ∧ t.mem = s.mem.write 0 (0#w.bits) := by
  have f0 : ((algorithm index limit body).program w)[0]? =
      some (.branch .eq (.memory (.direct index)) (.memory (.direct limit)) (body.length + 4)) := by
    simp [algorithm, header, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg]
  have f3 : ((algorithm index limit body).program w)[body.length + 4]? =
      some (.copy (.direct 0) (.immediate 0)) := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg, Nat.add_assoc] using tail_fetch w index limit body 3
  have f4 : ((algorithm index limit body).program w)[body.length + 5]? = some .halt := by
    simpa [trailer, SourceInstruction.compile, SourceOperand.compile, reg, Nat.add_assoc] using tail_fetch w index limit body 4
  simp [run, step, execute, Address.resolve, Operand.read, Comparison.test, pc, live, done, f0, f3, f4, Nat.add_assoc]

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

/-- On success the witness index and the body's witness data are retained. -/
def Outcome (index : Nat) (found : Nat → Memory w → Prop) (result : Option Nat) (mem : Memory w) : Prop :=
  match result with
  | none => mem 0 = 0#w.bits
  | some i => mem 0 = 1#w.bits ∧ mem index = BitVec.ofNat w.bits i ∧ found i mem

/-- Ordered search with a verified body. This proves the first successful
index, retains the body's witness, and counts guard/update/exit instructions.
The supplied body proof must be an actual trace for the given source code. -/
theorem searches (index limit : Nat) (body : List SourceInstruction) (stop cost : Nat)
    (test : Nat → Bool) (invariant : Memory w → Prop) (found : Nat → Memory w → Prop)
    (limitNonzero : limit ≠ 0) (separate : limit ≠ index) (stopFits : stop < 2 ^ w.bits)
    (stable : ∀ mem cell value, invariant mem → (cell = 0 ∨ cell = index) → invariant (mem.write cell value))
    (bodyCorrect : ∀ i, i < stop → ∀ s : State w, s.pc = 0 → s.halted = false → invariant s.mem →
      s.mem index = BitVec.ofNat w.bits i → s.mem limit = BitVec.ofNat w.bits stop →
      ∃ time out, time ≤ cost ∧ Runs widthConstant (body.map (SourceInstruction.compile w)) time s out ∧
        out.halted = true ∧ invariant out.mem ∧
        out.mem 0 = (if test i then 1#w.bits else 0#w.bits) ∧
        out.mem index = BitVec.ofNat w.bits i ∧ out.mem limit = BitVec.ofNat w.bits stop ∧
        (test i = true → found i out.mem))
    (start count : Nat) (s : State w) (extent : start + count = stop)
    (pc : s.pc = 0) (live : s.halted = false) (initial : invariant s.mem)
    (current : s.mem index = BitVec.ofNat w.bits start) (bound : s.mem limit = BitVec.ofNat w.bits stop) :
    ∃ time final, time ≤ count * (cost + 4) + 3 ∧
      Runs widthConstant ((algorithm index limit body).program w) time s final ∧ final.halted = true ∧
      invariant final.mem ∧ final.mem limit = BitVec.ofNat w.bits stop ∧
      Outcome index found ((List.range' start count).find? test) final.mem := by
  induction count generalizing start s with
  | zero =>
    have eq : start = stop := by omega
    have done : s.mem index = s.mem limit := by rw [current, bound, eq]
    obtain ⟨halted, ticks, mem⟩ := exits index limit body s pc live done
    refine ⟨3, run widthConstant ((algorithm index limit body).program w) 3 s, by simp,
      trace_of_ticks _ s 3 ticks, halted, ?_, ?_, ?_⟩
    · rw [mem]; exact stable s.mem 0 (0#w.bits) initial (Or.inl rfl)
    · rw [mem]; simpa [Memory.write, limitNonzero] using bound
    · simp [Outcome, mem, Memory.write]
  | succ count ih =>
    have active : start < stop := by omega
    have startFits : start < 2 ^ w.bits := by omega
    have different : s.mem index ≠ s.mem limit := by
      rw [current, bound]
      intro eq
      have values := congrArg BitVec.toNat eq
      simp only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt startFits, Nat.mod_eq_of_lt stopFits] at values
      omega
    let head := run widthConstant ((algorithm index limit body).program w) 1 s
    obtain ⟨hpc, hlive, hticks, hmem⟩ := enters index limit body s pc live different
    let entry : State w := { head with pc := 0 }
    have entryLive : entry.halted = false := hlive
    have entryMem : entry.mem = s.mem := hmem
    obtain ⟨bodyTime, out, bodyBound, bodyTrace, halted, outInvariant, answer, outIndex, outLimit, witness⟩ :=
      bodyCorrect start active entry rfl entryLive (by rw [entryMem]; exact initial)
        ((congrFun entryMem index).trans current) ((congrFun entryMem limit).trans bound)
    have embedded : EmbedsAt ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        ((algorithm index limit body).program w) 1 := by
      rw [program_eq]
      exact embeds_append ((header index limit body.length).map (SourceInstruction.compile w))
        ((body.map (SourceInstruction.compile w)).map (Instruction.returnTo body.length))
        ((trailer index body.length).map (SourceInstruction.compile w))
    let returned := (out.returnTo body.length).relocate 1
    have linked : Runs widthConstant ((algorithm index limit body).program w) bodyTime head returned := by
      have h := (bodyTrace.returnTo body.length).relocate embedded
      have he : (entry.returnTo body.length).relocate 1 = head := by
        simp only [State.returnTo, entryLive, Bool.false_eq_true, ↓reduceIte]
        change { head with pc := 1 } = head
        have hpc' : head.pc = 1 := hpc
        rw [← hpc']
      simpa only [he] using h
    have rmem : returned.mem = out.mem := by simp [returned, State.returnTo, State.relocate, halted]
    have rpc : returned.pc = body.length + 1 := by simp [returned, State.returnTo, State.relocate, halted, Nat.add_comm]
    have rlive : returned.halted = false := by simp [returned, State.returnTo, State.relocate, halted]
    by_cases yes : test start = true
    · have result : returned.mem 0 = 1#w.bits := by rw [rmem, answer]; simp [yes]
      obtain ⟨finalHalt, finalTicks, finalMem⟩ := succeeds index limit body returned rpc rlive result
      let final := run widthConstant ((algorithm index limit body).program w) 2 returned
      have mem : final.mem = out.mem := finalMem.trans rmem
      refine ⟨1 + bodyTime + 2, final, ?_,
        ((trace_of_ticks _ s 1 hticks).append linked).append (trace_of_ticks _ returned 2 finalTicks),
        finalHalt, ?_, ?_, ?_⟩
      · have lower := Nat.le_mul_of_pos_left (cost + 4) (by omega : 0 < count + 1)
        omega
      · rw [mem]; exact outInvariant
      · rw [mem]; exact outLimit
      · simp only [List.range'_succ, List.find?_cons, yes, Outcome]
        rw [mem]
        exact ⟨by simpa only [yes, ↓reduceIte] using answer, outIndex, witness yes⟩
    · have no : test start = false := Bool.eq_false_iff.mpr yes
      have result : returned.mem 0 = 0#w.bits := by rw [rmem, answer]; simp [no]
      obtain ⟨npc, nlive, nticks, nmem⟩ := advances index limit body returned rpc rlive result
      let next := run widthConstant ((algorithm index limit body).program w) 3 returned
      have mem : next.mem = out.mem.write index (out.mem index + 1#w.bits) := by
        simpa only [rmem] using nmem
      have nextInvariant : invariant next.mem := by
        rw [mem]; exact stable out.mem index _ outInvariant (Or.inr rfl)
      have nextIndex : next.mem index = BitVec.ofNat w.bits (start + 1) := by
        rw [mem]
        simp only [Memory.write, ↓reduceIte, outIndex]
        rw [← BitVec.ofNat_add]
      have nextLimit : next.mem limit = BitVec.ofNat w.bits stop := by
        rw [mem]; simpa only [Memory.write, if_neg separate] using outLimit
      obtain ⟨time, final, timeBound, trace, finalHalt, finalInvariant, finalLimit, finalOutcome⟩ :=
        ih (start + 1) next (by omega) npc nlive nextInvariant nextIndex nextLimit
      refine ⟨1 + bodyTime + 3 + time, final, ?_,
        (((trace_of_ticks _ s 1 hticks).append linked).append (trace_of_ticks _ returned 3 nticks)).append trace,
        finalHalt, finalInvariant, finalLimit, ?_⟩
      · simp only [Nat.add_mul, Nat.one_mul]; omega
      · simpa only [List.range'_succ, List.find?_cons, no, Bool.false_eq_true, ↓reduceIte] using finalOutcome

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

def initialized (index limit : Nat) (body : List SourceInstruction) : Algorithm :=
  ⟨SourceChain.code (setup index).code (algorithm index limit body).code, 1, by decide⟩

theorem initializes (index : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((setup index).program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem = s.mem.write index (0#w.bits) := by
  simp [setup, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step, execute,
    Address.resolve, Operand.read, pc, live, Nat.add_assoc]

/-- Initialization is included, so nested invocations restart at zero even
when their index cells contain results left by a previous search. -/
theorem searches_from_zero (index limit : Nat) (body : List SourceInstruction) (stop cost : Nat)
    (test : Nat → Bool) (invariant : Memory w → Prop) (found : Nat → Memory w → Prop)
    (limitNonzero : limit ≠ 0) (separate : limit ≠ index) (stopFits : stop < 2 ^ w.bits)
    (stable : ∀ mem cell value, invariant mem → (cell = 0 ∨ cell = index) → invariant (mem.write cell value))
    (bodyCorrect : ∀ i, i < stop → ∀ s : State w, s.pc = 0 → s.halted = false → invariant s.mem →
      s.mem index = BitVec.ofNat w.bits i → s.mem limit = BitVec.ofNat w.bits stop →
      ∃ time out, time ≤ cost ∧ Runs widthConstant (body.map (SourceInstruction.compile w)) time s out ∧
        out.halted = true ∧ invariant out.mem ∧
        out.mem 0 = (if test i then 1#w.bits else 0#w.bits) ∧
        out.mem index = BitVec.ofNat w.bits i ∧ out.mem limit = BitVec.ofNat w.bits stop ∧
        (test i = true → found i out.mem))
    (s : State w) (pc : s.pc = 0) (live : s.halted = false) (initial : invariant s.mem)
    (bound : s.mem limit = BitVec.ofNat w.bits stop) :
    ∃ time final, time ≤ stop * (cost + 4) + 5 ∧
      Runs widthConstant ((initialized index limit body).program w) time s final ∧ final.halted = true ∧
      invariant final.mem ∧ final.mem limit = BitVec.ofNat w.bits stop ∧
      Outcome index found ((List.range' 0 stop).find? test) final.mem := by
  let middle := run widthConstant ((setup index).program w) 2 s
  obtain ⟨halted, ticks, mem⟩ := initializes index s pc live
  have nextInvariant : invariant middle.mem := by
    rw [mem]; exact stable s.mem index _ initial (Or.inr rfl)
  have nextIndex : middle.mem index = BitVec.ofNat w.bits 0 := by simp [middle, mem, Memory.write]
  have nextLimit : middle.mem limit = BitVec.ofNat w.bits stop := by
    rw [mem]; simpa only [Memory.write, if_neg separate] using bound
  obtain ⟨time, out, timeBound, trace, outHalt, finalInvariant, finalLimit, finalOutcome⟩ :=
    searches index limit body stop cost test invariant found limitNonzero separate stopFits stable bodyCorrect
      0 stop (SourceChain.resume middle) (by omega) rfl rfl nextInvariant nextIndex nextLimit
  have full := SourceChain.traces (setup index).code (algorithm index limit body).code s middle out 2 time
    live halted (trace_of_ticks _ s 2 ticks) trace
  exact ⟨2 + time, out.relocate (setup index).code.length, by omega, full, outHalt,
    finalInvariant, finalLimit, finalOutcome⟩

end WordRAM.Conjectures.SourceSearch