SETH ⇒ OVC sparsification bundle 29: 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_28

set_option autoImplicit true

/-! Ordered clause-size/petal-size search around the verified core enumerator. -/
namespace WordRAM.Conjectures.Sparsification.FlowerSearch

/-- Pairs are (clause size, core length), in the existing petal-priority order. -/
def tasks (k : Nat) : List (Nat × Nat) :=
  (List.range (k + 1)).flatMap (fun size => (List.range size).map (fun petals => (size, size - petals)))

theorem task_bounds (member : (size, length) ∈ tasks k) : 0 < length ∧ length ≤ size ∧ size ≤ k := by
  obtain ⟨s, hs, member⟩ := List.mem_flatMap.mp member
  obtain ⟨petals, hp, eq⟩ := List.mem_map.mp member
  have sizes : s = size := congrArg Prod.fst eq
  have lengths : s - petals = length := congrArg Prod.snd eq
  have := List.mem_range.mp hs
  have := List.mem_range.mp hp
  omega

theorem tasks_length (k : Nat) : (tasks k).length ≤ (k + 1) * (k + 1) := by
  have bound := CoreEnumeration.flatMap_length_le (List.range (k + 1))
    (fun size => (List.range size).map (fun petals => (size, size - petals))) (k + 1) ?_
  · simpa only [tasks, List.length_range] using bound
  · intro size member
    have := List.mem_range.mp member
    simp only [List.length_map, List.length_range]
    omega

def group (n : Nat) (task : Nat × Nat) : List (Nat × Clause n) :=
  (Selection.cores n task.2).map (fun core => (task.1, core))

theorem groups_eq_choices (n k : Nat) : ((tasks k).flatMap (group n)) = Selection.choices n k := by
  simp [tasks, group, Selection.choices, List.flatMap_assoc, List.flatMap_map]

def result (clauses : CNF n) (threshold : Nat → Nat) : List (Nat × Nat) → Option (Nat × Clause n)
  | [] => none
  | task :: rest =>
      match (Selection.cores n task.2).find? (fun core => decide (Flowers.Candidate clauses threshold core task.1)) with
      | some core => some (task.1, core)
      | none => result clauses threshold rest

theorem result_eq_find (clauses : CNF n) (threshold : Nat → Nat) (ts : List (Nat × Nat)) :
    result clauses threshold ts = (ts.flatMap (group n)).find? (fun pair => decide (Flowers.Candidate clauses threshold pair.2 pair.1)) := by
  induction ts with
  | nil => rfl
  | cons task rest ih =>
    simp only [result, List.flatMap_cons, List.find?_append, group, List.find?_map, Function.comp_def]
    cases found : (Selection.cores n task.2).find? (fun core => decide (Flowers.Candidate clauses threshold core task.1)) <;> simp [ih]

theorem result_eq_select (clauses : CNF n) (threshold : Nat → Nat) (k : Nat) :
    result clauses threshold (tasks k) = Selection.select clauses threshold k := by
  rw [result_eq_find, groups_eq_choices]
  rfl

theorem improper_none (clauses : CNF n) (threshold : Nat → Nat) (size length : Nat) (improper : size ≤ length) :
    (Selection.cores n length).find? (fun core => decide (Flowers.Candidate clauses threshold core size)) = none := by
  apply List.find?_eq_none.mpr
  intro core member yes
  have lengthEq := (Selection.mem_cores core length).mp member
  have candidate := of_decide_eq_true yes
  have proper := candidate.2.2.1
  omega

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

/-- Publish the successful search's size, core length, and core-buffer pointer. -/
def finish (size length : Nat) : Algorithm :=
  ⟨[.copy (.direct 24) (.immediate size), .copy (.direct 25) (.immediate length),
    .copy (.direct 26) (.immediate (CoreSearchLayout.coreBase length)), .halt], 1, by decide⟩

def algorithm (threshold : Nat → Nat) : List (Nat × Nat) → Algorithm
  | [] => CandidateMachine.reject
  | task :: rest =>
      if task.2 < task.1 then
        ⟨SourceChain.code (CoreSearch.algorithm task.2 task.1 (threshold (task.1 - task.2)) 0 task.2).code
          (SourceIf.code 0 (algorithm threshold rest).code (finish task.1 task.2).code), 1, by decide⟩
      else algorithm threshold rest

def Keep (k a : Nat) : Prop := (16 ≤ a ∧ a < 20) ∨ 32 + 3 * k ≤ a

def Frame (k : Nat) (before after : Memory w) : Prop := ∀ a, Keep k a → after a = before a

theorem core_keeps (length k a : Nat) (bound : length ≤ k) (keep : Keep k a) : CoreSearchLayout.Preserved length 0 a := by
  rcases keep with low | high
  · exact CoreSearchLayout.control length 0 a low.1 low.2
  · apply CoreSearchLayout.table_word
    unfold CoreSearchLayout.slot CoreSearchLayout.coreBase
    omega

def Outcome (result : Option (Nat × Clause n)) (mem : Memory w) : Prop :=
  match result with
  | none => mem 0 = 0#w.bits
  | some (size, core) => mem 0 = 1#w.bits ∧ mem 24 = BitVec.ofNat w.bits size ∧
      mem 25 = BitVec.ofNat w.bits core.length ∧ mem 26 = BitVec.ofNat w.bits (CoreSearchLayout.coreBase core.length) ∧
      MaskBuilder.Encoded mem (CoreSearchLayout.coreBase core.length) (core.map (MaskBuilder.wordLiteral w))

def coreBound (n k bits clauses : Nat) : Nat :=
  (10 * k + 12 * bits + 18 * clauses + 61) * (2 * n + 1) ^ k

theorem core_bound (n k bits clauses length : Nat) (bound : length ≤ k) :
    (10 * length + 12 * bits + 18 * clauses + 61) * (2 * n + 1) ^ length ≤ coreBound n k bits clauses := by
  apply Nat.mul_le_mul (by omega)
  exact Nat.pow_le_pow_right (by omega) bound

theorem finishes (size length : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((finish size length).program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 24 = BitVec.ofNat w.bits size ∧
      t.mem 25 = BitVec.ofNat w.bits length ∧ t.mem 26 = BitVec.ofNat w.bits (CoreSearchLayout.coreBase length) ∧
      (∀ a, a ≠ 24 → a ≠ 25 → a ≠ 26 → t.mem a = s.mem a) := by
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, run, step, execute,
    Address.resolve, Operand.read, Memory.write, pc, live, Nat.add_assoc]
  intro a h24 h25 h26; simp [h24, h25, h26]

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

/-- Link all fixed size/core-length searches, retaining the first successful
core and its metadata. The formula and saved controls survive every failed search. -/
theorem searches_tasks (clauses : CNF n) (threshold : Nat → Nat) (k : Nat) (ts : List (Nat × Nat))
    (s : State w) (tableAddress : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (valid : ∀ task ∈ ts, 0 < task.2 ∧ task.2 ≤ task.1 ∧ task.1 ≤ k)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (tableBase : 32 + 3 * k ≤ tableAddress) (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 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))
    (input : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ ts.length * (coreBound n k w.bits clauses.length + 5) + 2 ∧
      Runs widthConstant ((algorithm threshold ts).program w) time s final ∧ final.halted = true ∧
      Outcome (result clauses threshold ts) final.mem ∧ Frame k s.mem final.mem := by
  induction ts generalizing s with
  | nil =>
    obtain ⟨halted, ticks, answer, frame⟩ := CandidateMachine.rejects s pc live
    refine ⟨2, run widthConstant (CandidateMachine.reject.program w) 2 s, by simp,
      trace_of_ticks _ s 2 ticks, halted, answer, ?_⟩
    intro a ha
    apply frame a
    unfold Keep at ha; omega
  | cons task rest ih =>
    rcases task with ⟨size, length⟩
    obtain ⟨positive, lengthBound, sizeBound⟩ := valid (size, length) (by simp)
    have restValid : ∀ task ∈ rest, 0 < task.2 ∧ task.2 ≤ task.1 ∧ task.1 ≤ k :=
      fun task h => valid task (by simp [h])
    by_cases proper : length < size
    · obtain ⟨coreTime, searched, bound, trace, halted, outcome, frame⟩ :=
        CoreSearch.finds_core clauses length size threshold s tableAddress pc live positive proper width variablesFit
          (by unfold CoreSearchLayout.slot CoreSearchLayout.coreBase; omega)
          (by unfold CoreSearchLayout.slot CoreSearchLayout.coreBase; omega)
          tableFits (by omega) (thresholdFits (size - length) (by omega)) nodup variables count pointer limit input
      have coreTimeBound : coreTime ≤ coreBound n k w.bits clauses.length :=
        Nat.le_trans bound (core_bound n k w.bits clauses.length length (by omega))
      have cf : Frame k s.mem searched.mem := fun a ha => frame a (core_keeps length k a (by omega) ha)
      let entry := (SourceChain.resume searched).addTicks 1
      cases selected : (Selection.cores n length).find? (fun core => decide (Flowers.Candidate clauses threshold core size)) with
      | none =>
        have zero : (SourceChain.resume searched).mem 0 = 0#w.bits := by
          rw [selected] at outcome
          exact outcome
        have nextInput : VectorBuilder.Stored entry.mem tableAddress (RecordTable.words w clauses) := by
          apply MemoryCopy.stored_frame _ _ input
          intro a lo _; exact cf a (Or.inr (by omega))
        obtain ⟨time, out, bound, tailTrace, outHalt, tailOutcome, tailFrame⟩ :=
          ih entry rfl rfl restValid
            ((cf 16 (Or.inl ⟨by decide, by decide⟩)).trans variables)
            ((cf 17 (Or.inl ⟨by decide, by decide⟩)).trans count)
            ((cf 18 (Or.inl ⟨by decide, by decide⟩)).trans pointer)
            ((cf 19 (Or.inl ⟨by decide, by decide⟩)).trans limit) nextInput
        have branch := SourceIf.zero_trace 0 (algorithm threshold rest).code (finish size length).code
          (SourceChain.resume searched) out time rfl rfl zero tailTrace
        have full := SourceChain.traces (CoreSearch.algorithm length size (threshold (size - length)) 0 length).code
          (SourceIf.code 0 (algorithm threshold rest).code (finish size length).code)
          s searched _ coreTime (1 + time) live halted trace branch
        let final := (out.relocate (1 + (finish size length).code.length)).relocate
          (CoreSearch.algorithm length size (threshold (size - length)) 0 length).code.length
        refine ⟨coreTime + (1 + time), final, ?_, ?_, outHalt, ?_, ?_⟩
        · simp only [List.length_cons, Nat.add_mul, Nat.one_mul]; omega
        · simpa only [algorithm, if_pos proper, Algorithm.program] using full
        · simpa only [result, selected, final, State.relocate] using tailOutcome
        · intro a ha; exact (tailFrame a ha).trans (cf a ha)
      | some core =>
        have coreLength : core.length = length :=
          (Selection.mem_cores core length).mp (List.mem_of_find?_eq_some selected)
        have success : searched.mem 0 = 1#w.bits ∧
            MaskBuilder.Encoded searched.mem (CoreSearchLayout.coreBase length) (core.map (MaskBuilder.wordLiteral w)) := by
          rw [selected] at outcome
          exact outcome
        have nonzero : (SourceChain.resume searched).mem 0 ≠ 0#w.bits := by
          change searched.mem 0 ≠ _
          rw [success.1]
          intro eq
          have values := congrArg BitVec.toNat eq
          have oneFits : 1 < 2 ^ w.bits := by omega
          simp [Nat.mod_eq_of_lt oneFits] at values
        let out := run widthConstant ((finish size length).program w) 4 entry
        obtain ⟨outHalt, ticks, outSize, outLength, outPointer, outFrame⟩ := finishes size length entry rfl rfl
        have branch := SourceIf.nonzero_trace 0 (algorithm threshold rest).code (finish size length).code
          (SourceChain.resume searched) out 4 rfl rfl nonzero (trace_of_ticks _ entry 4 ticks)
        have full := SourceChain.traces (CoreSearch.algorithm length size (threshold (size - length)) 0 length).code
          (SourceIf.code 0 (algorithm threshold rest).code (finish size length).code)
          s searched _ coreTime (1 + 4) live halted trace branch
        let final := (out.relocate 1).relocate (CoreSearch.algorithm length size (threshold (size - length)) 0 length).code.length
        refine ⟨coreTime + 5, final, ?_, ?_, outHalt, ?_, ?_⟩
        · simp only [List.length_cons, Nat.add_mul, Nat.one_mul]; omega
        · simpa only [algorithm, if_pos proper, Algorithm.program] using full
        · simp only [result, selected, Outcome]
          refine ⟨(outFrame 0 (by decide) (by decide) (by decide)).trans success.1, outSize, ?_, ?_, ?_⟩
          · simpa only [coreLength, final, State.relocate, out] using outLength
          · simpa only [coreLength, final, State.relocate, out] using outPointer
          · rw [coreLength]
            apply MaskTable.pair_frame _ _ success.2
            intro a lo _
            have low : 32 ≤ a := by unfold CoreSearchLayout.coreBase at lo; omega
            exact outFrame a (by omega) (by omega) (by omega)
        · intro a ha
          have low : a ≠ 24 ∧ a ≠ 25 ∧ a ≠ 26 := by unfold Keep at ha; omega
          exact (outFrame a low.1 low.2.1 low.2.2).trans (cf a ha)
    · obtain ⟨time, out, bound, trace, halted, outcome, frame⟩ :=
        ih s pc live restValid variables count pointer limit input
      have absent := improper_none clauses threshold size length (by omega)
      refine ⟨time, out, ?_, ?_, halted, ?_, frame⟩
      · simp only [List.length_cons, Nat.add_mul, Nat.one_mul]; omega
      · simpa only [algorithm, if_neg proper] using trace
      · simpa only [result, absent] using outcome

/-- The complete machine implements the original `Selection.select` function,
including size/petal priorities and the order of cores within each group. -/
theorem selects (clauses : CNF n) (threshold : Nat → Nat) (k : Nat)
    (s : State w) (tableAddress : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (tableBase : 32 + 3 * k ≤ tableAddress) (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 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))
    (input : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ ((k + 1) * (k + 1)) * (coreBound n k w.bits clauses.length + 5) + 2 ∧
      Runs widthConstant ((algorithm threshold (tasks k)).program w) time s final ∧ final.halted = true ∧
      Outcome (Selection.select clauses threshold k) final.mem ∧ Frame k s.mem final.mem := by
  obtain ⟨time, final, bound, trace, halted, outcome, frame⟩ :=
    searches_tasks clauses threshold k (tasks k) s tableAddress pc live
      (fun task h => task_bounds h) width variablesFit tableBase tableFits thresholdFits nodup
      variables count pointer limit input
  refine ⟨time, final, ?_, trace, halted, ?_, frame⟩
  · exact Nat.le_trans bound (Nat.add_le_add_right (Nat.mul_le_mul_right _ (tasks_length k)) 2)
  · simpa only [result_eq_select] using outcome

def setup : Algorithm := ⟨[.binary .add (.direct 19) (reg 16) (reg 16), .halt], 1, by decide⟩

def initialized (threshold : Nat → Nat) (k : Nat) : Algorithm :=
  ⟨SourceChain.code setup.code (algorithm threshold (tasks k)).code, 1, by decide⟩

theorem initializes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (setup.program w) 2 s
    t.halted = true ∧ t.ticks = s.ticks + 2 ∧ t.mem 19 = s.mem 16 + s.mem 16 ∧
      (∀ a, a ≠ 19 → t.mem a = s.mem a) := by
  simp [setup, 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 h; simp [h]

/-- Complete selector with the literal-code bound initialized from n. -/
theorem selects_initialized (clauses : CNF n) (threshold : Nat → Nat) (k : Nat)
    (s : State w) (tableAddress : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (width : 3 ≤ w.bits) (variablesFit : n ≤ w.bits)
    (tableBase : 32 + 3 * k ≤ tableAddress) (tableFits : tableAddress + 3 * clauses.length < 2 ^ w.bits)
    (thresholdFits : ∀ i, i ≤ k → threshold i < 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)
    (input : VectorBuilder.Stored s.mem tableAddress (RecordTable.words w clauses)) :
    ∃ time final, time ≤ ((k + 1) * (k + 1)) * (coreBound n k w.bits clauses.length + 5) + 4 ∧
      Runs widthConstant ((initialized threshold k).program w) time s final ∧ final.halted = true ∧
      Outcome (Selection.select clauses threshold k) final.mem ∧
      final.mem 19 = BitVec.ofNat w.bits (n + n) ∧
      (∀ a, Keep k a → a ≠ 19 → final.mem a = s.mem a) := by
  let middle := run widthConstant (setup.program w) 2 s
  obtain ⟨halted, ticks, limit, frame⟩ := initializes s pc live
  have bound : middle.mem 19 = BitVec.ofNat w.bits (n + n) := by rw [limit, variables, ← BitVec.ofNat_add]
  have nextInput : VectorBuilder.Stored middle.mem tableAddress (RecordTable.words w clauses) := by
    apply MemoryCopy.stored_frame _ _ input
    intro a lo _; exact frame a (by omega)
  obtain ⟨time, out, boundTime, trace, outHalt, outcome, preserved⟩ :=
    selects clauses threshold k (SourceChain.resume middle) tableAddress rfl rfl width variablesFit tableBase tableFits thresholdFits nodup
      ((frame 16 (by decide)).trans variables) ((frame 17 (by decide)).trans count)
      ((frame 18 (by decide)).trans pointer) bound nextInput
  have full := SourceChain.traces setup.code (algorithm threshold (tasks k)).code s middle out 2 time
    live halted (trace_of_ticks _ s 2 ticks) trace
  refine ⟨2 + time, out.relocate setup.code.length, by omega, full, outHalt, outcome, ?_, ?_⟩
  · exact (preserved 19 (Or.inl ⟨by decide, by decide⟩)).trans bound
  · intro a ha h19; exact (preserved a ha).trans (frame a h19)

end WordRAM.Conjectures.Sparsification.FlowerSearch

/-! Load a branch-construction record and its selected core into scratch words. -/
namespace WordRAM.Conjectures.Sparsification.BranchLoad

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

def algorithm : Algorithm :=
  ⟨[.copy (.direct 12) (reg 23),
    .copy (.direct 1) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 2) (.memory (.indirect 12)),
    .binary .add (.direct 12) (reg 12) (.immediate 1),
    .copy (.direct 0) (.memory (.indirect 12)),
    .copy (.direct 9) (reg 1), .copy (.direct 10) (reg 2),
    .copy (.direct 3) (reg 20), .copy (.direct 4) (reg 21), .halt], 1, by decide⟩

theorem executes (s : State w) (address : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (base : 32 ≤ address) (fits : address + 2 < 2 ^ w.bits)
    (pointer : s.mem 23 = BitVec.ofNat w.bits address) :
    let t := run widthConstant (algorithm.program w) 11 s
    t.halted = true ∧ t.ticks = s.ticks + 11 ∧
      t.mem 1 = s.mem address ∧ t.mem 2 = s.mem (address + 1) ∧
      t.mem 0 = s.mem (address + 2) ∧ t.mem 9 = s.mem address ∧
      t.mem 10 = s.mem (address + 1) ∧ t.mem 3 = s.mem 20 ∧ t.mem 4 = s.mem 21 ∧
      (∀ a, 16 ≤ a → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits address).toNat = address := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits address + 1#w.bits).toNat = address + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt (by omega)
  have d2 : (BitVec.ofNat w.bits address + 1#w.bits + 1#w.bits).toNat = address + 2 := by
    rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low0 : ∀ i, i ≤ 15 → address ≠ i := by omega
  have low1 : ∀ i, i ≤ 15 → address + 1 ≠ i := by omega
  have low2 : ∀ i, i ≤ 15 → address + 2 ≠ i := by omega
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, pointer, d0, d1, d2,
    low0, low1, low2, Nat.add_assoc, -BitVec.toNat_add]
  intro a ha
  have h : a ≠ 0 ∧ a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 4 ∧ a ≠ 9 ∧ a ≠ 10 ∧ a ≠ 12 := by omega
  simp [h]

theorem loads (core clause : Clause n) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 32 ≤ address)
    (fits : address + 2 < 2 ^ w.bits) (pointer : s.mem 23 = BitVec.ofNat w.bits address)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (input : VectorBuilder.Stored s.mem address (RecordTable.words w [clause])) :
    ∃ final, Runs widthConstant (algorithm.program w) 11 s final ∧ final.halted = true ∧
      final.mem 1 = Masks.encode w clause true ∧ final.mem 2 = Masks.encode w clause false ∧
      final.mem 0 = BitVec.ofNat w.bits (Normalize.clean clause).length ∧
      final.mem 9 = Masks.encode w clause true ∧ final.mem 10 = Masks.encode w clause false ∧
      final.mem 3 = Masks.encode w core true ∧ final.mem 4 = Masks.encode w core false ∧
      (∀ a, 16 ≤ a → final.mem a = s.mem a) := by
  obtain ⟨halted, ticks, pos, neg, size, savedPos, savedNeg, corePos, coreNeg, frame⟩ := executes s address pc live base fits pointer
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) 11 s
  have cost := runs_cost trace
  have eq : time = 11 := by omega
  subst time
  rcases input with ⟨ip, ine, il, _⟩
  refine ⟨_, trace, halted, pos.trans ip, neg.trans ine, ?_, savedPos.trans ip, savedNeg.trans ine,
    corePos.trans qp, coreNeg.trans qn, frame⟩
  exact size.trans il

end WordRAM.Conjectures.Sparsification.BranchLoad