SETH ⇒ OVC sparsification bundle 18: 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_17

set_option autoImplicit true

/-! An actual wordRAM loop counting set bits, without a popcount instruction. -/
namespace WordRAM.Conjectures.Sparsification.PopcountMachine

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

/-- Cell 1 is the input mask and is preserved. Cell 3 is the number of low bits
to scan; cell 2 is an accumulator. Cell 4 is scratch. Scan order is high to low. -/
def algorithm : Algorithm :=
  ⟨[.branch .eq (reg 3) (.immediate 0) 6,
    .binary .sub (.direct 3) (reg 3) (.immediate 1),
    .binary .shr (.direct 4) (reg 1) (reg 3),
    .binary .band (.direct 4) (reg 4) (.immediate 1),
    .binary .add (.direct 2) (reg 2) (reg 4),
    .jump 0, .halt], 1, by decide⟩

theorem iteration (s : State w) (pc : s.pc = 0) (live : s.halted = false) (nonzero : s.mem 3 ≠ 0#w.bits) :
    let t := run widthConstant (algorithm.program w) 6 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 6 ∧
    t.mem 3 = s.mem 3 - 1 ∧
    t.mem 2 = s.mem 2 + ((s.mem 1 >>> (s.mem 3 - 1).toNat) &&& 1#w.bits) ∧
    (∀ cell, cell ≠ 2 → cell ≠ 3 → cell ≠ 4 → t.mem cell = s.mem cell) := by
  simp [algorithm, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, Comparison.test,
    pc, live, nonzero, Nat.add_assoc, -BitVec.toNat_add]
  intro cell h2 h3 h4
  simp [h2, h3, h4]

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

theorem low_bit (mask : Word w) (index : Nat) :
    (mask >>> index) &&& 1#w.bits = BitVec.ofNat w.bits (mask.getLsbD index).toNat := by
  rw [BitVec.and_one_eq_setWidth_ofBool_getLsbD, BitVec.getLsbD_ushiftRight]
  simp only [Nat.add_zero]
  cases mask.getLsbD index <;> apply BitVec.eq_of_toNat_eq <;> simp [BitVec.toNat_setWidth]

private theorem trace_of_ticks (s : State w) (fuel : Nat)
    (ticks : (run widthConstant (algorithm.program w) fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant (algorithm.program w) fuel s (run widthConstant (algorithm.program w) fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (algorithm.program w) fuel s
  have cost := runs_cost trace
  have eq : time = fuel := by omega
  subst time
  exact trace

/-- Exact running time and result for an arbitrary bit count and accumulator.
The result is represented modulo the word width; the full-width count from zero
fits because the population count is at most the word width. -/
theorem computes (mask : Word w) (bits offset : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (fits : bits < 2 ^ w.bits)
    (input : s.mem 1 = mask) (counter : s.mem 3 = BitVec.ofNat w.bits bits)
    (accumulator : s.mem 2 = BitVec.ofNat w.bits offset) :
    ∃ final, Runs widthConstant (algorithm.program w) (6 * bits + 2) s final ∧
      final.halted = true ∧ final.mem 2 = BitVec.ofNat w.bits (mask.cpopNatRec bits offset) ∧
      (∀ cell, cell ≠ 2 → cell ≠ 3 → cell ≠ 4 → final.mem cell = s.mem cell) := by
  induction bits generalizing offset s with
  | zero =>
    have empty : s.mem 3 = 0#w.bits := by simpa using counter
    obtain ⟨halted, ticks, memory⟩ := exits s pc live empty
    refine ⟨_, trace_of_ticks s 2 ticks, halted, ?_, ?_⟩
    · simpa only [memory, BitVec.cpopNatRec_zero_self] using accumulator
    · intro cell _ _ _; rw [memory]
  | succ bits ih =>
    have nonzero : s.mem 3 ≠ 0#w.bits := by
      intro zero
      have eq := congrArg BitVec.toNat zero
      simp [counter, Nat.mod_eq_of_lt fits] at eq
    obtain ⟨nextPC, nextLive, ticks, decremented, added, frame⟩ := iteration s pc live nonzero
    let next := run widthConstant (algorithm.program w) 6 s
    have smaller : s.mem 3 - 1#w.bits = BitVec.ofNat w.bits bits := by
      rw [counter]
      change BitVec.ofNat w.bits (bits + 1) - BitVec.ofNat w.bits 1 = _
      rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
      simp
    have shiftIndex : (s.mem 3 - 1#w.bits).toNat = bits := by
      rw [smaller]; exact Nat.mod_eq_of_lt (by omega)
    have nextInput : next.mem 1 = mask := (frame 1 (by decide) (by decide) (by decide)).trans input
    have nextCounter : next.mem 3 = BitVec.ofNat w.bits bits := decremented.trans smaller
    have nextAccumulator : next.mem 2 = BitVec.ofNat w.bits (offset + (mask.getLsbD bits).toNat) := by
      change next.mem 2 = s.mem 2 + ((s.mem 1 >>> (s.mem 3 - 1#w.bits).toNat) &&& 1#w.bits) at added
      rw [added, input, shiftIndex, low_bit, accumulator, ← BitVec.ofNat_add]
    obtain ⟨final, trace, halted, output, preserved⟩ := ih (offset + (mask.getLsbD bits).toNat) next
      nextPC nextLive (by omega) nextInput nextCounter nextAccumulator
    refine ⟨final, ?_, halted, output, ?_⟩
    · have full := (trace_of_ticks s 6 ticks).append trace
      have cost : 6 + (6 * bits + 2) = 6 * (bits + 1) + 2 := by omega
      simpa only [cost] using full
    · intro cell h2 h3 h4
      exact (preserved cell h2 h3 h4).trans (frame cell h2 h3 h4)

/-- Initialize the count and obtain the scan length from the machine's native
word-width constant, rather than requiring the caller to supply it. -/
def initialized : Algorithm :=
  ⟨[.copy (.direct 2) (.immediate 0), .wordWidth (.direct 3)] ++
    algorithm.code.map (SourceInstruction.relocate 2), 1, by decide⟩

private theorem initialized_program (w : Width) :
    initialized.program w =
      ([.copy (.direct 2) (.immediate 0), .native (.direct 3) ⟨0, by decide⟩] : Program w .multiplication 1) ++
      (algorithm.program w).map (Instruction.relocate 2) := rfl

/-- The complete standalone subroutine counts all bits in exactly 6w+4
instructions, preserving the mask and all non-scratch memory. -/
theorem initialized_counts (mask : Word w) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (input : s.mem 1 = mask) :
    ∃ final, Runs widthConstant (initialized.program w) (6 * w.bits + 4) s final ∧
      final.halted = true ∧ final.mem 2 = mask.cpop ∧
      (∀ cell, cell ≠ 2 → cell ≠ 3 → cell ≠ 4 → final.mem cell = s.mem cell) := by
  let entry : State w :=
    { mem := (s.mem.write 2 0).write 3 (BitVec.ofNat w.bits w.bits), pc := 0, ticks := s.ticks + 2 }
  have frame : ∀ cell, cell ≠ 2 → cell ≠ 3 → entry.mem cell = s.mem cell := by
    intro cell h2 h3
    simp [entry, Memory.write, h2, h3]
  have init : Runs widthConstant (initialized.program w) 2 s (entry.relocate 2) := by
    apply Runs.cons (t := execute widthConstant (.copy (.direct 2) (.immediate 0)) s)
    · simp [step, initialized_program, pc, live]; rfl
    apply Runs.cons (t := entry.relocate 2)
    · simp [step, initialized_program, execute, pc, live, entry, State.relocate,
        Operand.read, Address.resolve, widthConstant, Nat.add_assoc]
    · exact Runs.refl _
  obtain ⟨final, trace, halted, output, preserved⟩ := computes mask w.bits 0 entry rfl rfl
    (Nat.lt_pow_self (by decide)) ((frame 1 (by decide) (by decide)).trans input)
    (by simp [entry, Memory.write]) (by simp [entry, Memory.write])
  have embedded : EmbedsAt (algorithm.program w) (initialized.program w) 2 := by
    rw [initialized_program]
    simpa using embeds_append
      ([.copy (.direct 2) (.immediate 0), .native (.direct 3) ⟨0, by decide⟩] : Program w .multiplication 1)
      (algorithm.program w) []
  refine ⟨final.relocate 2, ?_, halted, output, ?_⟩
  · have full := init.append (trace.relocate embedded)
    have cost : 2 + (6 * w.bits + 2) = 6 * w.bits + 4 := by omega
    simpa only [cost] using full
  · intro cell h2 h3 h4
    exact (preserved cell h2 h3 h4).trans (frame cell h2 h3)

end WordRAM.Conjectures.Sparsification.PopcountMachine

/-! Population counts of the clause masks recover deduplicated clause sizes. -/
namespace WordRAM.Conjectures.Sparsification.MaskCardinality

def indices (clause : Clause n) (polarity : Bool) : List Nat :=
  (clause.filter (fun literal => decide (literal.positive = polarity))).map (fun literal => literal.index.val)

theorem index_bit (clause : Clause n) (polarity : Bool) (index : Nat) (bounded : index < w.bits) :
    (Masks.encode w clause polarity).getLsbD index = true ↔ index ∈ indices clause polarity := by
  rw [Masks.encode, ClauseMasks.mask_bit _ _ _ _ bounded]
  constructor
  · rintro ⟨literal, member, _, pol, eq⟩
    exact List.mem_map.mpr ⟨literal, List.mem_filter.mpr ⟨member, decide_eq_true pol⟩, eq⟩
  · intro member
    obtain ⟨literal, member, eq⟩ := List.mem_map.mp member
    obtain ⟨member, pol⟩ := List.mem_filter.mp member
    exact ⟨literal, member, rfl, of_decide_eq_true pol, eq⟩

theorem indices_nodup (clause : Clause n) (nodup : clause.Nodup) (polarity : Bool) :
    (indices clause polarity).Nodup := by
  apply List.pairwise_map.mpr
  apply (nodup.filter (fun literal => decide (literal.positive = polarity))).imp_of_mem
  intro a b ha hb different eq
  have pa := of_decide_eq_true (List.mem_filter.mp ha).2
  have pb := of_decide_eq_true (List.mem_filter.mp hb).2
  exact different (Masks.literal_eq a b eq (pa.trans pb.symm))

theorem cpop_range (word : Word w) (bits : Nat) :
    word.cpopNatRec bits 0 = ((List.range bits).filter word.getLsbD).length := by
  induction bits with
  | zero => simp
  | succ bits ih =>
    rw [BitVec.cpopNatRec_succ, BitVec.cpopNatRec_eq]
    rw [ih]
    cases bit : word.getLsbD bits <;> simp [List.range_succ, List.filter_append, bit]

theorem count_indices (clause : Clause n) (polarity : Bool) (fits : n ≤ w.bits) (nodup : clause.Nodup) :
    (Masks.encode w clause polarity).cpop.toNat = (indices clause polarity).length := by
  rw [BitVec.toNat_cpop, cpop_range]
  apply Nat.le_antisymm
  · apply List.Nodup.length_le_of_subset (List.nodup_range.filter _)
    intro index member
    obtain ⟨present, bit⟩ := List.mem_filter.mp member
    exact (index_bit clause polarity index (List.mem_range.mp present)).mp bit
  · apply (indices_nodup clause nodup polarity).length_le_of_subset
    intro index member
    have bounded : index < w.bits := by
      obtain ⟨literal, _, eq⟩ := List.mem_map.mp member
      rw [← eq]
      exact Nat.lt_of_lt_of_le literal.index.isLt fits
    exact List.mem_filter.mpr ⟨List.mem_range.mpr bounded, (index_bit clause polarity index bounded).mpr member⟩

/-- Both polarities count separately, including tautological clauses. -/
theorem count_clause (clause : Clause n) (fits : n ≤ w.bits) (nodup : clause.Nodup) :
    (Masks.encode w clause true).cpop.toNat + (Masks.encode w clause false).cpop.toNat = clause.length := by
  rw [count_indices clause true fits nodup, count_indices clause false fits nodup]
  have partition := Branch.filter_lengths clause (fun literal => literal.positive)
  simpa [indices] using partition

theorem clean_mask (clause : Clause n) (polarity : Bool) :
    Masks.encode w (Normalize.clean clause) polarity = Masks.encode w clause polarity := by
  have forward : Normalize.clean clause ⊆ clause := fun literal member => (Normalize.mem_clean literal clause).mp member
  have backward : clause ⊆ Normalize.clean clause := fun literal member => (Normalize.mem_clean literal clause).mpr member
  have a := Masks.subset_and (w := w) _ _ forward polarity
  have b := Masks.subset_and (w := w) _ _ backward polarity
  rw [BitVec.and_comm] at b
  exact a.symm.trans b

/-- Population counts recover the number of distinct literals, even when the
serialized input contains duplicates or both polarities of the same variable. -/
theorem count_distinct (clause : Clause n) (fits : n ≤ w.bits) :
    (Masks.encode w clause true).cpop.toNat + (Masks.encode w clause false).cpop.toNat =
      (Normalize.clean clause).length := by
  have result := count_clause (Normalize.clean clause) fits (Normalize.clean_nodup clause)
  simpa only [clean_mask] using result

theorem distinct_length_bound (clause : Clause n) : (Normalize.clean clause).length ≤ 2 * n := by
  have bound := (Normalize.clean_nodup clause).length_le_of_subset
    (l₂ := Counting.literals n) (fun literal _ => Counting.mem_literals literal)
  simpa only [Counting.literals_length] using bound

end WordRAM.Conjectures.Sparsification.MaskCardinality

/-! Linked wordRAM computation of a clause's number of distinct literals. -/
namespace WordRAM.Conjectures.Sparsification.SizeMachine

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

/-- Save the first count and load the other mask. -/
def bridge : Algorithm :=
  ⟨[.copy (.direct 6) (reg 2), .copy (.direct 1) (reg 5), .halt], 1, by decide⟩

def finish : Algorithm :=
  ⟨[.binary .add (.direct 0) (reg 6) (reg 2), .halt], 1, by decide⟩

/-- Positive mask in cell 1, negative mask in cell 5, size returned in cell 0.
Cells 1,2,3,4,6 are scratch; cell 5 and every other non-output cell are preserved. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code PopcountMachine.initialized.code
    (SourceChain.code bridge.code (SourceChain.code PopcountMachine.initialized.code finish.code)), 1, by decide⟩

theorem bridge_executes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 3 s
    t.mem 6 = s.mem 2 ∧ t.mem 1 = s.mem 5 ∧ t.halted = true ∧ t.ticks = s.ticks + 3 ∧
      (∀ cell, cell ≠ 1 → cell ≠ 6 → t.mem cell = s.mem cell) := 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 cell h1 h6
  simp [h1, h6]

theorem finish_executes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (finish.program w) 2 s
    t.mem 0 = s.mem 6 + s.mem 2 ∧ t.halted = true ∧ t.ticks = s.ticks + 2 ∧
      (∀ cell, cell ≠ 0 → t.mem cell = s.mem cell) := by
  simp [finish, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, Nat.add_assoc]
  intro cell absent eq
  exact False.elim (absent eq)

private theorem exact_trace (a : Algorithm) (s : State w) (fuel : Nat)
    (ticks : (run widthConstant (a.program w) fuel s).ticks = s.ticks + fuel) :
    Runs widthConstant (a.program w) fuel s (run widthConstant (a.program w) fuel s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (a.program w) fuel s
  have cost := runs_cost trace
  have eq : time = fuel := by omega
  subst time
  exact trace

/-- Both counts, the register transfers, and the final addition have actual
linked traces. No subroutine call or data movement is treated as free. -/
theorem counts (positive negative : Word w) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (pos : s.mem 1 = positive) (neg : s.mem 5 = negative) :
    ∃ final, Runs widthConstant (algorithm.program w) (12 * w.bits + 13) s final ∧
      final.halted = true ∧ final.mem 0 = positive.cpop + negative.cpop ∧
      (∀ cell, cell ≠ 0 → cell ≠ 1 → cell ≠ 2 → cell ≠ 3 → cell ≠ 4 → cell ≠ 6 → final.mem cell = s.mem cell) := by
  obtain ⟨first, firstTrace, firstHalt, firstCount, firstFrame⟩ :=
    PopcountMachine.initialized_counts positive s pc live pos
  let middle := run widthConstant (bridge.program w) 3 (SourceChain.resume first)
  obtain ⟨saved, loaded, middleHalt, middleTicks, middleFrame⟩ := bridge_executes (SourceChain.resume first) rfl rfl
  have negativeInput : middle.mem 1 = negative := loaded.trans ((firstFrame 5 (by decide) (by decide) (by decide)).trans neg)
  obtain ⟨second, secondTrace, secondHalt, secondCount, secondFrame⟩ :=
    PopcountMachine.initialized_counts negative (SourceChain.resume middle) rfl rfl negativeInput
  have savedCount : second.mem 6 = positive.cpop :=
    (secondFrame 6 (by decide) (by decide) (by decide)).trans (saved.trans firstCount)
  let out := run widthConstant (finish.program w) 2 (SourceChain.resume second)
  obtain ⟨answer, outHalt, outTicks, outFrame⟩ := finish_executes (SourceChain.resume second) rfl rfl
  have output : out.mem 0 = positive.cpop + negative.cpop := by
    change out.mem 0 = second.mem 6 + second.mem 2 at answer
    rw [answer, savedCount, secondCount]
  have tail := SourceChain.traces PopcountMachine.initialized.code finish.code
    (SourceChain.resume middle) second out (6 * w.bits + 4) 2 rfl secondHalt secondTrace
    (exact_trace finish _ 2 outTicks)
  have mid := SourceChain.traces bridge.code (SourceChain.code PopcountMachine.initialized.code finish.code)
    (SourceChain.resume first) middle _ 3 (6 * w.bits + 4 + 2) rfl middleHalt
    (exact_trace bridge _ 3 middleTicks) tail
  have full := SourceChain.traces PopcountMachine.initialized.code
    (SourceChain.code bridge.code (SourceChain.code PopcountMachine.initialized.code finish.code))
    s first _ (6 * w.bits + 4) (3 + (6 * w.bits + 4 + 2)) live firstHalt firstTrace mid
  let final := ((out.relocate PopcountMachine.initialized.code.length).relocate bridge.code.length).relocate
    PopcountMachine.initialized.code.length
  refine ⟨final, ?_, outHalt, output, ?_⟩
  · have cost : (6 * w.bits + 4) + (3 + (6 * w.bits + 4 + 2)) = 12 * w.bits + 13 := by omega
    simpa only [algorithm, Algorithm.program, cost, final] using full
  · intro cell h0 h1 h2 h3 h4 h6
    exact (outFrame cell h0).trans ((secondFrame cell h2 h3 h4).trans
      ((middleFrame cell h1 h6).trans (firstFrame cell h2 h3 h4)))

theorem double_width_fits (bits : Nat) (large : 3 ≤ bits) : 2 * bits < 2 ^ bits := by
  induction bits with
  | zero => omega
  | succ bits ih =>
    by_cases previous : 3 ≤ bits
    · have bound := ih previous
      rw [Nat.pow_succ]
      omega
    · have eq : bits + 1 = 3 := by omega
      rw [eq]
      decide

/-- Width at least three and room for variable indices suffice to avoid
wrapping the count, including clauses containing both polarities. -/
theorem size_fits {w : Width} (clause : Clause n) (fits : n ≤ w.bits) (large : 3 ≤ w.bits) :
    (Normalize.clean clause).length < 2 ^ w.bits :=
  Nat.lt_of_le_of_lt (Nat.le_trans (MaskCardinality.distinct_length_bound clause) (Nat.mul_le_mul_left 2 fits))
    (double_width_fits w.bits large)

end WordRAM.Conjectures.Sparsification.SizeMachine

/-! Parsing serialized literal pairs into a clause mask/size record on wordRAM. -/
namespace WordRAM.Conjectures.Sparsification.RecordBuilder

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

/-- Preserve the positive mask and stage both masks for size computation. -/
def bridge : Algorithm :=
  ⟨[.copy (.direct 7) (reg 3), .copy (.direct 1) (reg 3), .copy (.direct 5) (reg 4), .halt], 1, by decide⟩

/-- Input: pointer in 1, literal count in 2. Output: positive mask in 7,
negative mask in 5, distinct-literal count in 0. Input data at addresses ≥8
are preserved. All initialization, parsing, and counting is included. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code MaskBuilder.initialized.code (SourceChain.code bridge.code SizeMachine.algorithm.code), 1, by decide⟩

theorem bridge_executes (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (bridge.program w) 4 s
    t.mem 7 = s.mem 3 ∧ t.mem 1 = s.mem 3 ∧ t.mem 5 = s.mem 4 ∧
      t.halted = true ∧ t.ticks = s.ticks + 4 ∧
      (∀ cell, cell ≠ 1 → cell ≠ 5 → cell ≠ 7 → t.mem cell = s.mem cell) := by
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg,
    run, step, execute, Operand.read, Address.resolve, Memory.write, pc, live, Nat.add_assoc]
  intro cell h1 h5 h7
  simp [h1, h5, h7]

private theorem bridge_trace (s : State w)
    (ticks : (run widthConstant (bridge.program w) 4 s).ticks = s.ticks + 4) :
    Runs widthConstant (bridge.program w) 4 s (run widthConstant (bridge.program w) 4 s) := by
  obtain ⟨time, _, trace⟩ := run_has_trace widthConstant (bridge.program w) 4 s
  have cost := runs_cost trace
  have eq : time = 4 := by omega
  subst time
  exact trace

/-- End-to-end record construction from the original serialized literals.
Repeated literals are counted once; the two polarities remain distinct. -/
theorem builds (clause : Clause n) (s : State w) (address : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : 8 ≤ address)
    (fits : address + 2 * clause.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (pointer : s.mem 1 = BitVec.ofNat w.bits address)
    (count : s.mem 2 = BitVec.ofNat w.bits clause.length)
    (input : MaskBuilder.Encoded s.mem address (clause.map (MaskBuilder.wordLiteral w))) :
    ∃ final, Runs widthConstant (algorithm.program w) (10 * clause.length + 12 * w.bits + 21) s final ∧
      final.halted = true ∧ final.mem 7 = Masks.encode w clause true ∧
      final.mem 5 = Masks.encode w clause false ∧
      final.mem 0 = BitVec.ofNat w.bits (Normalize.clean clause).length ∧
      (∀ cell, 8 ≤ cell → final.mem cell = s.mem cell) := by
  obtain ⟨parsed, parseTrace, parseHalt, positive, negative, parseFrame⟩ :=
    MaskBuilder.initialized_builds_clause clause s address pc live base fits variablesFit pointer count input
  let middle := run widthConstant (bridge.program w) 4 (SourceChain.resume parsed)
  obtain ⟨saved, loadedPos, loadedNeg, middleHalt, middleTicks, middleFrame⟩ :=
    bridge_executes (SourceChain.resume parsed) rfl rfl
  have pos : middle.mem 1 = Masks.encode w clause true := loadedPos.trans positive
  have neg : middle.mem 5 = Masks.encode w clause false := loadedNeg.trans negative
  obtain ⟨out, countTrace, outHalt, counted, countFrame⟩ :=
    SizeMachine.counts (Masks.encode w clause true) (Masks.encode w clause false)
      (SourceChain.resume middle) rfl rfl pos neg
  have outPos : out.mem 7 = Masks.encode w clause true :=
    (countFrame 7 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans (saved.trans positive)
  have outNeg : out.mem 5 = Masks.encode w clause false :=
    (countFrame 5 (by decide) (by decide) (by decide) (by decide) (by decide) (by decide)).trans neg
  have outCount : out.mem 0 = BitVec.ofNat w.bits (Normalize.clean clause).length := by
    rw [counted]
    apply BitVec.eq_of_toNat_eq
    simp only [BitVec.toNat_add, BitVec.toNat_ofNat, MaskCardinality.count_distinct clause variablesFit]
  have tail := SourceChain.traces bridge.code SizeMachine.algorithm.code
    (SourceChain.resume parsed) middle out 4 (12 * w.bits + 13) rfl middleHalt
    (bridge_trace _ middleTicks) countTrace
  have full := SourceChain.traces MaskBuilder.initialized.code (SourceChain.code bridge.code SizeMachine.algorithm.code)
    s parsed _ (10 * clause.length + 4) (4 + (12 * w.bits + 13)) live parseHalt parseTrace tail
  let final := (out.relocate bridge.code.length).relocate MaskBuilder.initialized.code.length
  refine ⟨final, ?_, outHalt, outPos, outNeg, outCount, ?_⟩
  · have cost : (10 * clause.length + 4) + (4 + (12 * w.bits + 13)) = 10 * clause.length + 12 * w.bits + 21 := by omega
    simpa only [algorithm, Algorithm.program, cost, final] using full
  · intro cell bound
    exact (countFrame cell (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)).trans
      ((middleFrame cell (by omega) (by omega) (by omega)).trans (parseFrame cell bound))

end WordRAM.Conjectures.Sparsification.RecordBuilder