SETH ⇒ OVC sparsification bundle 40: 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_39

set_option autoImplicit true

/-! Concrete root-stack initialization followed by the verified DFS generator. -/
namespace WordRAM.Conjectures.Sparsification.Generate
open TraversalBody TraversalBounds

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

end WordRAM.Conjectures.Sparsification.Generate

/-! Reject empty clauses before running the DFS leaf generator. -/
namespace WordRAM.Conjectures.Sparsification.CheckedGenerate
open TraversalBody TraversalBounds

def dispatch (threshold : Nat → Nat) (k : Nat) : Algorithm :=
  ⟨SourceIf.code 0 (Generate.algorithm threshold k).code (RootStack.prepare k).code, 1, by decide⟩

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

end WordRAM.Conjectures.Sparsification.CheckedGenerate

/-! Recovering a canonical literal order from clause masks preserves SAT and
clause sizes. A mask table need not retain the original literal order. -/
namespace WordRAM.Conjectures.Sparsification.Canonical

def clause (input : Clause n) : Clause n :=
  (Counting.literals n).filter (fun literal => decide (literal ∈ input))

def formula (input : CNF n) : CNF n := input.map clause

@[simp] theorem mem_clause (literal : Literal n) (input : Clause n) :
    literal ∈ clause input ↔ literal ∈ input := by
  simp [clause, Counting.mem_literals]

theorem literals_nodup (n : Nat) : (Counting.literals n).Nodup := by
  have side (polarity : Bool) : (List.ofFn fun i : Fin n => Literal.mk i polarity).Nodup := by
    have h := List.pairwise_map.mpr ((List.nodup_finRange n).imp
      (show ∀ {a b : Fin n}, a ≠ b → Literal.mk a polarity ≠ Literal.mk b polarity from
        fun {_ _} ne eq => ne (congrArg Literal.index eq)))
    simpa only [List.Nodup, List.finRange, List.map_ofFn, Function.comp_def] using h
  rw [Counting.literals, List.nodup_append]
  refine ⟨side true, side false, ?_⟩
  intro positive hp negative hn eq
  obtain ⟨a, ha⟩ := List.mem_ofFn.mp hp
  obtain ⟨b, hb⟩ := List.mem_ofFn.mp hn
  have impossible := congrArg Literal.positive (ha.trans (eq.trans hb.symm))
  contradiction

theorem nodup (input : Clause n) : (clause input).Nodup :=
  (literals_nodup n).filter _

theorem length_le (input : Clause n) : (clause input).length ≤ input.length :=
  (nodup input).length_le_of_subset (fun _ h => (mem_clause _ _).mp h)

theorem length_eq (input : Clause n) (h : input.Nodup) : (clause input).length = input.length := by
  apply Nat.le_antisymm (length_le input)
  exact h.length_le_of_subset (fun _ h => (mem_clause _ _).mpr h)

theorem clause_holds (assignment : Fin n → Bool) (input : Clause n) :
    ClauseHolds assignment (clause input) ↔ ClauseHolds assignment input := by
  simp only [ClauseHolds, mem_clause]

theorem holds (assignment : Fin n → Bool) (input : CNF n) :
    Holds assignment (formula input) ↔ Holds assignment input := by
  simp [Holds, formula, clause_holds]

theorem satisfiable (input : CNF n) :
    (SATInstance.mk n (formula input)).Satisfiable ↔ (SATInstance.mk n input).Satisfiable := by
  change (∃ a, Holds a (formula input)) ↔ ∃ a, Holds a input
  simp only [holds]

theorem width (input : CNF n) (bounded : ∀ c ∈ input, c.length ≤ k) :
    ∀ c ∈ formula input, c.length ≤ k := by
  intro c member
  change c ∈ input.map clause at member
  obtain ⟨original, hm, eq⟩ : ∃ original ∈ input, clause original = c := List.mem_map.mp member
  subst c
  exact Nat.le_trans (length_le original) (bounded original hm)

@[simp] theorem formula_length (input : CNF n) : (formula input).length = input.length := List.length_map _

/-- Filtering the finite literal enumeration by actual mask bits returns exactly
this canonical representation, including both polarities of tautologies. -/
theorem mask_filter (input : Clause n) (fits : n ≤ w.bits) :
    (Counting.literals n).filter (fun literal =>
      (Masks.encode w input literal.positive).getLsbD literal.index.val) = clause input := by
  apply List.filter_congr
  intro literal _
  apply Bool.eq_iff_iff.mpr
  simpa using Masks.bit_mem input literal fits

end WordRAM.Conjectures.Sparsification.Canonical

/-! Preserve the variable count and compute the normalization allocation endpoint
before scratch registers are reused by the parser and normalizer. -/
namespace WordRAM.Conjectures.Sparsification.NormalizeSetup
open TraversalBody
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

def endpoint (workspace count : Nat) : Nat := workspace + count * (3 * (count + 1))

def prepare (k : Nat) : Algorithm :=
  ⟨[.copy (.direct (variableCell k)) (reg 16),
    .binary .add (.direct 30) (reg 11) (.immediate 1),
    .binary (.mul rfl) (.direct 30) (reg 30) (.immediate 3),
    .binary (.mul rfl) (.direct 30) (reg 11) (reg 30),
    .binary .add (.direct (freeCell k)) (reg 27) (reg 30), .halt], 1, by decide⟩

def bridge (k : Nat) : Algorithm :=
  ⟨[.copy (.direct 16) (reg (variableCell k)),
    .copy (.direct 18) (reg 22), .copy (.direct 17) (reg 24),
    .copy (.direct 27) (reg (freeCell k)), .halt], 1, by decide⟩

theorem prepares (k m workspace : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (count : s.mem 11 = BitVec.ofNat w.bits m) (pointer : s.mem 27 = BitVec.ofNat w.bits workspace) :
    let t := run widthConstant ((prepare k).program w) 6 s
    t.halted = true ∧ t.ticks = s.ticks + 6 ∧
      t.mem (variableCell k) = s.mem 16 ∧ t.mem (freeCell k) = BitVec.ofNat w.bits (endpoint workspace m) ∧
      (∀ a, a ≠ variableCell k → a ≠ freeCell k → a ≠ 30 → t.mem a = s.mem a) := by
  have separation : 11 ≠ 64 + k * 3 ∧ 27 ≠ 64 + k * 3 ∧ 64 + k * 3 ≠ 30 ∧
      64 + (k * 3 + 3) ≠ 30 := by omega
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, variableCell, freeCell,
    Nat.add_assoc, separation, count, pointer, endpoint, ← BitVec.ofNat_add, ← BitVec.ofNat_mul, Nat.mul_comm]
  intro a hv hf h30
  simp [hv, hf, h30]

theorem bridges (k : Nat) (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant ((bridge k).program w) 5 s
    t.halted = true ∧ t.ticks = s.ticks + 5 ∧
      t.mem 16 = s.mem (variableCell k) ∧ t.mem 18 = s.mem 22 ∧ t.mem 17 = s.mem 24 ∧
      t.mem 27 = s.mem (freeCell k) ∧ t.mem 22 = s.mem 22 ∧ t.mem 24 = s.mem 24 ∧
      (∀ a, 32 ≤ a → t.mem a = s.mem a) := by
  have separation : 64 + (3 * k + 3) ≠ 16 ∧ 64 + (3 * k + 3) ≠ 17 ∧ 64 + (3 * k + 3) ≠ 18 := by omega
  simp [bridge, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, pc, live, variableCell, freeCell, Nat.add_assoc, separation]
  intro a ha
  have h : a ≠ 16 ∧ a ≠ 17 ∧ a ≠ 18 ∧ a ≠ 27 := by omega
  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

def algorithm (k : Nat) : Algorithm :=
  ⟨SourceChain.code (prepare k).code (SourceChain.code SerializedNormalize.algorithm.code (bridge k).code), 1, by decide⟩

/-- Parse and normalize the protected serialized input, while constructing all
register arguments and an allocation endpoint for `CheckedGenerate`. -/
theorem normalizes_framed (clauses : CNF n) (k : Nat) (s : State w) (source records workspace : Nat)
    (pc : s.pc = 0) (live : s.halted = false) (base : dataBase k ≤ source)
    (inputBefore : source + MaskTable.span clauses ≤ records)
    (recordsBefore : records + 3 * clauses.length ≤ workspace)
    (fits : endpoint workspace clauses.length < 2 ^ w.bits) (variablesFit : n ≤ w.bits)
    (variables : s.mem 16 = BitVec.ofNat w.bits n)
    (count : s.mem 11 = BitVec.ofNat w.bits clauses.length)
    (pointer : s.mem 12 = BitVec.ofNat w.bits source)
    (recordPointer : s.mem 13 = BitVec.ofNat w.bits records)
    (workspacePointer : s.mem 27 = BitVec.ofNat w.bits workspace)
    (input : MaskTable.Encoded s.mem source clauses) :
    ∃ time final address,
      time ≤ RecordTable.cost w clauses + clauses.length * (35 * clauses.length + 34) + 31 ∧
      Runs widthConstant ((algorithm k).program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem address (RecordTable.words w (Normalize.normalize clauses)) ∧
      dataBase k ≤ address ∧ address + 3 * (Normalize.normalize clauses).length ≤ endpoint workspace clauses.length ∧
      final.mem 16 = BitVec.ofNat w.bits n ∧ final.mem 22 = BitVec.ofNat w.bits address ∧
      final.mem 24 = BitVec.ofNat w.bits (Normalize.normalize clauses).length ∧
      final.mem 18 = BitVec.ofNat w.bits address ∧ final.mem 17 = BitVec.ofNat w.bits (Normalize.normalize clauses).length ∧
      final.mem 27 = BitVec.ofNat w.bits (endpoint workspace clauses.length) ∧
      (∀ a, endpoint workspace clauses.length ≤ a → final.mem a = s.mem a) := by
  have coords : 64 ≤ variableCell k ∧ freeCell k = variableCell k + 3 ∧ dataBase k = variableCell k + 4 := by
    dsimp [variableCell, freeCell, dataBase]; omega
  let prepared := run widthConstant ((prepare k).program w) 6 s
  obtain ⟨ph, pt, pv, pe, pf⟩ := prepares k clauses.length workspace s pc live count workspacePointer
  have preparedInput : MaskTable.Encoded prepared.mem source clauses := by
    apply MaskTable.Encoded.frame _ _ input
    intro a ha _; exact pf a (by omega) (by omega) (by omega)
  obtain ⟨time, out, address, bound, trace, halted, table, ptr, cnt, lower, upper, frame⟩ :=
    SerializedNormalize.normalizes clauses (SourceChain.resume prepared) source records workspace rfl rfl (by omega)
      inputBefore recordsBefore fits variablesFit
      ((pf 11 (by omega) (by omega) (by decide)).trans count)
      ((pf 12 (by omega) (by omega) (by decide)).trans pointer)
      ((pf 13 (by omega) (by omega) (by decide)).trans recordPointer)
      ((pf 27 (by omega) (by omega) (by decide)).trans workspacePointer) preparedInput
  let final := run widthConstant ((bridge k).program w) 5 (SourceChain.resume out)
  obtain ⟨fh, ft, fv, fptr, fcnt, fe, f22, f24, ff⟩ := bridges k (SourceChain.resume out) rfl rfl
  have keptVariables : out.mem (variableCell k) = BitVec.ofNat w.bits n :=
    (frame (variableCell k) (by omega) (Or.inl (by omega)) (Or.inl (by omega))).trans (pv.trans variables)
  have keptEndpoint : out.mem (freeCell k) = BitVec.ofNat w.bits (endpoint workspace clauses.length) :=
    (frame (freeCell k) (by omega) (Or.inl (by omega)) (Or.inl (by omega))).trans pe
  have finalTable : VectorBuilder.Stored final.mem address (RecordTable.words w (Normalize.normalize clauses)) := by
    apply MemoryCopy.stored_frame _ _ table
    intro a ha _; exact ff a (by omega)
  have tail := SourceChain.traces SerializedNormalize.algorithm.code (bridge k).code (SourceChain.resume prepared)
    out final time 5 rfl halted trace (trace_of_ticks _ _ 5 ft)
  have full := SourceChain.traces (prepare k).code (SourceChain.code SerializedNormalize.algorithm.code (bridge k).code)
    s prepared (final.relocate SerializedNormalize.algorithm.code.length) 6 (time + 5) live ph (trace_of_ticks _ _ 6 pt) tail
  refine ⟨6 + (time + 5), (final.relocate SerializedNormalize.algorithm.code.length).relocate (prepare k).code.length,
    address, by omega, full, fh, finalTable, by omega, upper,
    fv.trans keptVariables, f22.trans ptr, f24.trans cnt, fptr.trans ptr, fcnt.trans cnt, fe.trans keptEndpoint, ?_⟩
  intro a ha
  have above : workspace ≤ a := by unfold endpoint at ha; omega
  exact (ff a (by omega)).trans
    ((frame a (by omega) (Or.inr (by omega)) (Or.inr ha)).trans
      (pf a (by omega) (by omega) (by omega)))

end WordRAM.Conjectures.Sparsification.NormalizeSetup

/-! From protected serialized clauses to the exact sparsification leaf stack. -/
namespace WordRAM.Conjectures.Sparsification.SerializedGenerate
open TraversalBody TraversalBounds

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

theorem normalized_leaves (clauses : CNF n) (threshold : Nat → Nat) (k : Nat) (large : ∀ i, 2 ≤ threshold i) :
    Tree.leaves (Normalize.normalize clauses) threshold k large = Tree.leaves clauses threshold k large := by
  conv => lhs; rw [Tree.leaves]
  conv => rhs; rw [Tree.leaves]
  simp only [Normalize.normalize_idempotent]
  split
  · rfl
  · split <;> split <;> simp_all only [Normalize.normalize_idempotent, Option.some.injEq, Prod.mk.injEq] <;> simp_all

end WordRAM.Conjectures.Sparsification.SerializedGenerate

/-! Serialize the set bits of a mask as index/polarity pairs, in increasing
index order, using only ordinary wordRAM instructions. -/
namespace WordRAM.Conjectures.Sparsification.MaskSerialize
private def reg (i : Nat) : SourceOperand := .memory (.direct i)

/-- 1=mask, 2=index, 3=remaining indices, 4=output cursor, 5=polarity.
Only 2,3,4,6 and the output buffer are modified. -/
def algorithm : Algorithm :=
  ⟨[.branch .eq (reg 3) (.immediate 0) 11,
    .binary .shr (.direct 6) (reg 1) (reg 2),
    .binary .band (.direct 6) (reg 6) (.immediate 1),
    .branch .eq (reg 6) (.immediate 0) 8,
    .copy (.indirect 4) (reg 2), .binary .add (.direct 4) (reg 4) (.immediate 1),
    .copy (.indirect 4) (reg 5), .binary .add (.direct 4) (reg 4) (.immediate 1),
    .binary .add (.direct 2) (reg 2) (.immediate 1),
    .binary .sub (.direct 3) (reg 3) (.immediate 1), .jump 0, .halt], 1, by decide⟩

def words (mask polarity : Word w) (index : Nat) : Nat → List (Word w)
  | 0 => []
  | count + 1 => (if mask.getLsbD index then [BitVec.ofNat w.bits index, polarity] else []) ++
    words mask polarity (index + 1) count

theorem length_le (mask polarity : Word w) (index count : Nat) :
    (words mask polarity index count).length ≤ 2 * count := by
  induction count generalizing index with
  | zero => simp [words]
  | succ count ih =>
    have h := ih (index + 1)
    cases bit : mask.getLsbD index <;> simp [words, bit] <;> omega

theorem misses (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 3 ≠ 0#w.bits)
    (off : (s.mem 1 >>> (s.mem 2).toNat) &&& 1#w.bits = 0#w.bits) :
    let t := run widthConstant (algorithm.program w) 7 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 7 ∧
      t.mem 2 = s.mem 2 + 1#w.bits ∧ t.mem 3 = s.mem 3 - 1#w.bits ∧
      (∀ a, a ≠ 2 → a ≠ 3 → a ≠ 6 → t.mem a = s.mem a) := 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, off, Nat.add_assoc]
  intro a h2 h3 h6; simp [h2, h3, h6]

theorem hits (s : State w) (destination : Nat) (pc : s.pc = 0) (live : s.halted = false)
    (nonzero : s.mem 3 ≠ 0#w.bits)
    (on : (s.mem 1 >>> (s.mem 2).toNat) &&& 1#w.bits ≠ 0#w.bits)
    (base : 8 ≤ destination) (fits : destination + 1 < 2 ^ w.bits)
    (pointer : s.mem 4 = BitVec.ofNat w.bits destination) :
    let t := run widthConstant (algorithm.program w) 11 s
    t.pc = 0 ∧ t.halted = false ∧ t.ticks = s.ticks + 11 ∧
      t.mem 2 = s.mem 2 + 1#w.bits ∧ t.mem 3 = s.mem 3 - 1#w.bits ∧
      t.mem 4 = BitVec.ofNat w.bits (destination + 2) ∧
      t.mem destination = s.mem 2 ∧ t.mem (destination + 1) = s.mem 5 ∧
      (∀ a, a ≠ 2 → a ≠ 3 → a ≠ 4 → a ≠ 6 → a ≠ destination → a ≠ destination + 1 → t.mem a = s.mem a) := by
  have d0 : (BitVec.ofNat w.bits destination).toNat = destination := Nat.mod_eq_of_lt (by omega)
  have d1 : (BitVec.ofNat w.bits destination + 1#w.bits).toNat = destination + 1 := by
    rw [← BitVec.ofNat_add]; exact Nat.mod_eq_of_lt fits
  have low0 : ∀ i, i ≤ 7 → destination ≠ i ∧ i ≠ destination := by omega
  have low1 : ∀ i, i ≤ 7 → destination + 1 ≠ i ∧ i ≠ destination + 1 := by omega
  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, on,
    pointer, d0, d1, low0, low1, Nat.add_assoc, -BitVec.toNat_add]
  constructor
  · rw [← BitVec.ofNat_add, ← BitVec.ofNat_add]
  · intro a h2 h3 h4 h6 h0 h1; simp [h2, h3, h4, h6, h0, h1]

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]

private theorem trace_of_ticks (s : State w) (fuel : Nat)
    (cost : (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 ticks := runs_cost trace
  have eq : time = fuel := by omega
  subst time; exact trace

/-- Exact output contents, bounded instruction count, and a memory frame for the
entire mask scan. Both index and destination arithmetic have explicit no-wrap
bounds; masks and polarity words are unrestricted. -/
theorem serializes (mask polarity : Word w) (index count destination : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false) (base : 8 ≤ destination)
    (indexFits : index + count < 2 ^ w.bits) (outputFits : destination + 2 * count < 2 ^ w.bits)
    (input : s.mem 1 = mask) (cursor : s.mem 2 = BitVec.ofNat w.bits index)
    (remaining : s.mem 3 = BitVec.ofNat w.bits count)
    (pointer : s.mem 4 = BitVec.ofNat w.bits destination) (pol : s.mem 5 = polarity) :
    ∃ time final, time ≤ 11 * count + 2 ∧ Runs widthConstant (algorithm.program w) time s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (words mask polarity index count) ∧
      final.mem 2 = BitVec.ofNat w.bits (index + count) ∧ final.mem 3 = 0#w.bits ∧
      final.mem 4 = BitVec.ofNat w.bits (destination + (words mask polarity index count).length) ∧
      final.mem 1 = mask ∧ final.mem 5 = polarity ∧
      (∀ a, 8 ≤ a → (a < destination ∨ destination + (words mask polarity index count).length ≤ a) →
        final.mem a = s.mem a) := by
  induction count generalizing index destination s with
  | zero =>
    have zero : s.mem 3 = 0#w.bits := by simpa using remaining
    obtain ⟨halted, ticks, mem⟩ := exits s pc live zero
    refine ⟨2, _, by omega, trace_of_ticks s 2 ticks, halted, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    · simp [words, VectorBuilder.Stored]
    · simpa only [mem, Nat.add_zero] using cursor
    · rw [mem]; exact zero
    · simpa only [mem, words, List.length_nil, Nat.add_zero] using pointer
    · rw [mem]; exact input
    · rw [mem]; exact pol
    · intro a _ _; rw [mem]
  | succ count ih =>
    have nonzero : s.mem 3 ≠ 0#w.bits := by
      intro eq
      have values := congrArg BitVec.toNat eq
      simp only [remaining, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (show count + 1 < 2 ^ w.bits by omega), Nat.zero_mod] at values
      omega
    have decremented : s.mem 3 - 1#w.bits = BitVec.ofNat w.bits count := by
      rw [remaining]
      rw [BitVec.ofNat_sub_ofNat_of_le _ _ (by omega) (by omega)]
      simp
    have incremented : s.mem 2 + 1#w.bits = BitVec.ofNat w.bits (index + 1) := by
      rw [cursor, ← BitVec.ofNat_add]
    have selected : (s.mem 1 >>> (s.mem 2).toNat) &&& 1#w.bits =
        BitVec.ofNat w.bits (mask.getLsbD index).toNat := by
      rw [input, cursor, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (show index < 2 ^ w.bits by omega), PopcountMachine.low_bit]
    cases bit : mask.getLsbD index with
    | false =>
      have off : (s.mem 1 >>> (s.mem 2).toNat) &&& 1#w.bits = 0#w.bits := by simpa only [bit, Bool.toNat_false] using selected
      let next := run widthConstant (algorithm.program w) 7 s
      obtain ⟨npc, nlive, ticks, nc, nr, frame⟩ := misses s pc live nonzero off
      obtain ⟨time, final, bound, trace, halted, stored, fc, fr, fp, fi, fpol, ff⟩ :=
        ih (index + 1) destination next npc nlive base (by omega) (by omega)
          ((frame 1 (by decide) (by decide) (by decide)).trans input)
          (nc.trans incremented) (nr.trans decremented)
          ((frame 4 (by decide) (by decide) (by decide)).trans pointer)
          ((frame 5 (by decide) (by decide) (by decide)).trans pol)
      refine ⟨7 + time, final, by omega, (trace_of_ticks s 7 ticks).append trace, halted, ?_, ?_, fr, ?_, fi, fpol, ?_⟩
      · simpa only [words, bit, Bool.false_eq_true, ↓reduceIte, List.nil_append] using stored
      · simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using fc
      · simpa only [words, bit, Bool.false_eq_true, ↓reduceIte, List.nil_append] using fp
      · intro a ha outside
        have outside' : a < destination ∨ destination + (words mask polarity (index + 1) count).length ≤ a := by
          simpa only [words, bit, Bool.false_eq_true, ↓reduceIte, List.nil_append] using outside
        exact (ff a ha outside').trans (frame a (by omega) (by omega) (by omega))
    | true =>
      have on : (s.mem 1 >>> (s.mem 2).toNat) &&& 1#w.bits ≠ 0#w.bits := by
        rw [selected, bit]
        intro eq
        have values := congrArg BitVec.toNat eq
        have modulus : 1 < 2 ^ w.bits := by omega
        simp only [Bool.toNat_true, BitVec.toNat_ofNat, Nat.mod_eq_of_lt modulus, Nat.zero_mod] at values
        omega
      let next := run widthConstant (algorithm.program w) 11 s
      obtain ⟨npc, nlive, ticks, nc, nr, np, first, second, frame⟩ :=
        hits s destination pc live nonzero on base (by omega) pointer
      obtain ⟨time, final, bound, trace, halted, stored, fc, fr, fp, fi, fpol, ff⟩ :=
        ih (index + 1) (destination + 2) next npc nlive (by omega) (by omega) (by omega)
          ((frame 1 (by decide) (by decide) (by decide) (by decide) (by omega) (by omega)).trans input)
          (nc.trans incremented) (nr.trans decremented) np
          ((frame 5 (by decide) (by decide) (by decide) (by decide) (by omega) (by omega)).trans pol)
      have first' : final.mem destination = BitVec.ofNat w.bits index :=
        (ff destination base (Or.inl (by omega))).trans (first.trans cursor)
      have second' : final.mem (destination + 1) = polarity :=
        (ff (destination + 1) (by omega) (Or.inl (by omega))).trans (second.trans pol)
      have hlen : (words mask polarity index (count + 1)).length =
          2 + (words mask polarity (index + 1) count).length := by
        simp [words, bit]; omega
      refine ⟨11 + time, final, by omega, (trace_of_ticks s 11 ticks).append trace, halted, ?_, ?_, fr, ?_, fi, fpol, ?_⟩
      · simpa only [words, bit, ↓reduceIte, List.cons_append, List.nil_append, VectorBuilder.Stored, Nat.add_assoc] using
          (show final.mem destination = BitVec.ofNat w.bits index ∧ final.mem (destination + 1) = polarity ∧
            VectorBuilder.Stored final.mem (destination + 2) (words mask polarity (index + 1) count) from ⟨first', second', stored⟩)
      · simpa only [Nat.add_assoc, Nat.add_comm, Nat.add_left_comm] using fc
      · simpa only [hlen, Nat.add_assoc] using fp
      · intro a ha outside
        have outside' : a < destination ∨ destination + 2 + (words mask polarity (index + 1) count).length ≤ a := by
          simpa only [hlen, Nat.add_assoc] using outside
        exact (ff a ha (by omega)).trans (frame a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega))

end WordRAM.Conjectures.Sparsification.MaskSerialize