SETH ⇒ OVC sparsification bundle 32: 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_31

set_option autoImplicit true

/-! The memory invariant for stable partition of a whole clause table. -/
namespace WordRAM.Conjectures.Sparsification.PartitionInvariant

/-- Each output buffer reserves one record per input clause. -/
structure Layout (w : Width) (length source left right : Nat) : Prop where
  sourceBase : 32 ≤ source
  sourceEnd : source + 3 * length ≤ left
  leftEnd : left + 3 * length ≤ right
  fits : right + 3 * length < 2 ^ w.bits

def Outside (length left right a : Nat) : Prop :=
  32 ≤ a ∧ (a < left ∨ left + 3 * length ≤ a) ∧ (a < right ∨ right + 3 * length ≤ a)

structure Holds (formula : CNF n) (core : Clause n) (size source left right : Nat)
    (original : Memory w) (i : Nat) (mem : Memory w) : Prop where
  bound : i ≤ formula.length
  input : VectorBuilder.Stored mem source (RecordTable.words w formula)
  remaining : VectorBuilder.Stored mem left (RecordTable.words w (Branch.remaining (formula.take i) core size))
  petals : VectorBuilder.Stored mem right (RecordTable.words w (BranchTables.petals (formula.take i) core size))
  leftCount : mem 16 = BitVec.ofNat w.bits (Branch.remaining (formula.take i) core size).length
  rightCount : mem 17 = BitVec.ofNat w.bits (BranchTables.petals (formula.take i) core size).length
  leftPointer : mem 18 = BitVec.ofNat w.bits (left + 3 * (Branch.remaining (formula.take i) core size).length)
  rightPointer : mem 19 = BitVec.ofNat w.bits (right + 3 * (BranchTables.petals (formula.take i) core size).length)
  corePositive : mem 20 = Masks.encode w core true
  coreNegative : mem 21 = Masks.encode w core false
  target : mem 22 = BitVec.ofNat w.bits size
  inputPointer : mem 23 = BitVec.ofNat w.bits (source + 3 * i)
  frame : ∀ a, Outside formula.length left right a → mem a = original a

variable {formula : CNF n} {core : Clause n} {size source left right i : Nat}
  {original before after : Memory w}

theorem frame (layout : Layout w formula.length source left right)
    (h : Holds formula core size source left right original i before)
    (same : ∀ a, (16 ≤ a ∧ a ≤ 23) ∨ 32 ≤ a → after a = before a) :
    Holds formula core size source left right original i after := by
  have leftBase : 32 ≤ left := by have := layout.sourceBase; have := layout.sourceEnd; omega
  have rightBase : 32 ≤ right := by have := layout.leftEnd; omega
  refine ⟨h.bound, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
  · apply MemoryCopy.stored_frame _ _ h.input
    intro a ha _; exact same a (Or.inr (Nat.le_trans layout.sourceBase ha))
  · apply MemoryCopy.stored_frame _ _ h.remaining
    intro a ha _; exact same a (Or.inr (by omega))
  · apply MemoryCopy.stored_frame _ _ h.petals
    intro a ha _; exact same a (Or.inr (by omega))
  · exact (same 16 (Or.inl (by decide))).trans h.leftCount
  · exact (same 17 (Or.inl (by decide))).trans h.rightCount
  · exact (same 18 (Or.inl (by decide))).trans h.leftPointer
  · exact (same 19 (Or.inl (by decide))).trans h.rightPointer
  · exact (same 20 (Or.inl (by decide))).trans h.corePositive
  · exact (same 21 (Or.inl (by decide))).trans h.coreNegative
  · exact (same 22 (Or.inl (by decide))).trans h.target
  · exact (same 23 (Or.inl (by decide))).trans h.inputPointer
  · intro a ha; exact (same a (Or.inr ha.1)).trans (h.frame a ha)

theorem stable (layout : Layout w formula.length source left right)
    (mem : Memory w) (cell : Nat) (value : Word w)
    (h : Holds formula core size source left right original i mem) (which : cell = 0 ∨ cell = 24) :
    Holds formula core size source left right original i (mem.write cell value) := by
  apply frame layout h
  intro a ha
  have different : a ≠ cell := by rcases ha with ha | ha <;> rcases which with rfl | rfl <;> omega
  simp [Memory.write, different]

/-- Processing a record advances the exact prefix invariant by one. -/
theorem step (layout : Layout w formula.length source left right)
    (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (active : i < formula.length) (s : State w) (pc : s.pc = 0) (live : s.halted = false)
    (h : Holds formula core size source left right original i s.mem) :
    ∃ time out, time ≤ 12 * w.bits + 82 ∧ Runs widthConstant (BranchPartition.body.program w) time s out ∧
      out.halted = true ∧ Holds formula core size source left right original (i + 1) out.mem ∧
      out.mem 0 = 0#w.bits ∧ out.mem 24 = s.mem 24 ∧ out.mem 25 = s.mem 25 := by
  let clause := formula[i]
  let l := Branch.remaining (formula.take i) core size
  let r := BranchTables.petals (formula.take i) core size
  let eligible := decide (clause.length = size ∧ core ⊆ clause)
  let dest := if eligible then right + 3 * r.length else left + 3 * l.length
  have sourceBase := layout.sourceBase
  have sourceEnd := layout.sourceEnd
  have leftEnd := layout.leftEnd
  have fits := layout.fits
  have lb : l.length ≤ i := Nat.le_trans (BranchTables.remaining_length _ core size) (List.length_take_le _ _)
  have rb : r.length ≤ i := Nat.le_trans (BranchTables.petals_length _ core size) (List.length_take_le _ _)
  have leftBase : 32 ≤ left := by omega
  have rightBase : 32 ≤ right := by omega
  have input := BranchTables.stored_get formula s.mem source i active h.input
  obtain ⟨time, out, timeBound, trace, halted, zero, pointer, selectedPointer, selectedCount, newRecord, changed⟩ :=
    BranchPartition.iteration core clause size s (source + 3 * i) (left + 3 * l.length) (right + 3 * r.length)
      pc live (by omega) (by omega) variablesFit width sizeFits (nodup clause (List.getElem_mem active))
      h.inputPointer h.corePositive h.coreNegative h.target input (by omega) (by omega) h.leftPointer
      (by omega) (by omega) h.rightPointer
  change out.mem (BranchRoute.cursor eligible) = BitVec.ofNat w.bits (dest + 3) at selectedPointer
  change out.mem (BranchRoute.count eligible) = s.mem (BranchRoute.count eligible) + 1#w.bits at selectedCount
  change VectorBuilder.Stored out.mem dest (RecordTable.words w [BranchEmit.output eligible core clause]) at newRecord
  change ∀ a, 16 ≤ a → a ≠ 23 → a ≠ BranchRoute.cursor eligible → a ≠ BranchRoute.count eligible →
    a ≠ dest → a ≠ dest + 1 → a ≠ dest + 2 → out.mem a = s.mem a at changed
  have cursorBounds : 18 ≤ BranchRoute.cursor eligible ∧ BranchRoute.cursor eligible ≤ 19 := by cases eligible <;> decide
  have countBounds : 16 ≤ BranchRoute.count eligible ∧ BranchRoute.count eligible ≤ 17 := by cases eligible <;> decide
  have destBase : 32 ≤ dest := by dsimp [dest]; split <;> omega
  have lowFrame : ∀ a, 16 ≤ a → a < 32 → a ≠ 23 → a ≠ BranchRoute.cursor eligible →
      a ≠ BranchRoute.count eligible → out.mem a = s.mem a := by
    intro a ha hb h23 hc hn
    exact changed a ha h23 hc hn (by omega) (by omega) (by omega)
  have highFrame : ∀ a, 32 ≤ a → (a < dest ∨ dest + 3 ≤ a) → out.mem a = s.mem a := by
    intro a ha outside
    exact changed a (by omega) (by omega) (by omega) (by omega) (by omega) (by omega) (by omega)
  have oldInput : VectorBuilder.Stored out.mem source (RecordTable.words w formula) := by
    apply MemoryCopy.stored_frame _ _ h.input
    intro a ha hb
    rw [RecordTable.words_length] at hb
    apply highFrame a (by omega)
    left
    dsimp [dest]; split <;> omega
  have oldLeft : VectorBuilder.Stored out.mem left (RecordTable.words w l) := by
    apply MemoryCopy.stored_frame _ _ h.remaining
    intro a ha hb
    rw [RecordTable.words_length] at hb
    change a < left + 3 * l.length at hb
    apply highFrame a (by omega)
    left
    dsimp [dest]; split <;> omega
  have oldRight : VectorBuilder.Stored out.mem right (RecordTable.words w r) := by
    apply MemoryCopy.stored_frame _ _ h.petals
    intro a ha hb
    rw [RecordTable.words_length] at hb
    change a < right + 3 * r.length at hb
    apply highFrame a (by omega)
    dsimp [dest]; split
    · left; omega
    · right; omega
  have outsideFrame : ∀ a, Outside formula.length left right a → out.mem a = original a := by
    intro a ha
    apply Eq.trans (highFrame a ha.1 ?_) (h.frame a ha)
    rcases ha with ⟨_, hl, hr⟩
    dsimp [dest]; split
    · rcases hr with hr | hr
      · left; omega
      · right; omega
    · rcases hl with hl | hl
      · left; omega
      · right; omega
  have lp : Branch.remaining (formula.take (i + 1)) core size =
      l ++ (if clause.length = size ∧ core ⊆ clause then [] else [clause]) := by
    rw [BranchTables.take_succ formula i active, BranchTables.remaining_snoc]
  have rp : BranchTables.petals (formula.take (i + 1)) core size =
      r ++ (if clause.length = size ∧ core ⊆ clause then [Branch.petal core clause] else []) := by
    rw [BranchTables.take_succ formula i active, BranchTables.petals_snoc]
  have invariant : Holds formula core size source left right original (i + 1) out.mem := by
    refine ⟨by omega, oldInput, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, outsideFrame⟩
    · rw [lp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · simpa [member] using oldLeft
      · rw [if_neg member]
        apply (BranchTables.records_append l [clause] out.mem left).mpr
        exact ⟨oldLeft, by simpa [dest, eligible, member, BranchEmit.output] using newRecord⟩
    · rw [rp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · rw [if_pos member]
        apply (BranchTables.records_append r [Branch.petal core clause] out.mem right).mpr
        exact ⟨oldRight, by simpa [dest, eligible, member, BranchEmit.output] using newRecord⟩
      · simpa [member] using oldRight
    · rw [lp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · simpa [member] using (lowFrame 16 (by decide) (by decide) (by decide)
          (by simp [BranchRoute.cursor, eligible, member]) (by simp [BranchRoute.count, eligible, member])).trans h.leftCount
      · have result : out.mem 16 = BitVec.ofNat w.bits l.length + 1#w.bits := by
          simpa [BranchRoute.count, eligible, member, h.leftCount] using selectedCount
        simpa [member, BitVec.ofNat_add] using result
    · rw [rp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · have result : out.mem 17 = BitVec.ofNat w.bits r.length + 1#w.bits := by
          simpa [BranchRoute.count, eligible, member, h.rightCount] using selectedCount
        simpa [member, BitVec.ofNat_add] using result
      · simpa [member] using (lowFrame 17 (by decide) (by decide) (by decide)
          (by simp [BranchRoute.cursor, eligible, member]) (by simp [BranchRoute.count, eligible, member])).trans h.rightCount
    · rw [lp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · simpa [member] using (lowFrame 18 (by decide) (by decide) (by decide)
          (by simp [BranchRoute.cursor, eligible, member]) (by simp [BranchRoute.count, eligible, member])).trans h.leftPointer
      · simpa [BranchRoute.cursor, dest, eligible, member, List.length_append, Nat.mul_add, Nat.add_assoc] using selectedPointer
    · rw [rp]
      by_cases member : clause.length = size ∧ core ⊆ clause
      · simpa [BranchRoute.cursor, dest, eligible, member, List.length_append, Nat.mul_add, Nat.add_assoc] using selectedPointer
      · simpa [member] using (lowFrame 19 (by decide) (by decide) (by decide)
          (by simp [BranchRoute.cursor, eligible, member]) (by simp [BranchRoute.count, eligible, member])).trans h.rightPointer
    · exact (lowFrame 20 (by decide) (by decide) (by decide) (by omega) (by omega)).trans h.corePositive
    · exact (lowFrame 21 (by decide) (by decide) (by decide) (by omega) (by omega)).trans h.coreNegative
    · exact (lowFrame 22 (by decide) (by decide) (by decide) (by omega) (by omega)).trans h.target
    · simpa only [Nat.mul_add, Nat.mul_one, Nat.add_assoc] using pointer
  exact ⟨time, out, timeBound, trace, halted, invariant, zero,
    lowFrame 24 (by decide) (by decide) (by decide) (by omega) (by omega),
    lowFrame 25 (by decide) (by decide) (by decide) (by omega) (by omega)⟩

end WordRAM.Conjectures.Sparsification.PartitionInvariant

/-! Correctness and running time of the complete branch-table partition program. -/
namespace WordRAM.Conjectures.Sparsification.PartitionMachine

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

/-- Stable partition of every input record. The first output is exactly
`Branch.remaining`; the second is exactly the selected family's petals, in
original clause order. All initialization and loop-control instructions count. -/
theorem partitions (formula : CNF n) (core : Clause n) (size : Nat)
    (source left right : Nat) (s : State w)
    (pc : s.pc = 0) (live : s.halted = false)
    (layout : PartitionInvariant.Layout w formula.length source left right)
    (variablesFit : n ≤ w.bits) (width : 3 ≤ w.bits) (sizeFits : size < 2 ^ w.bits)
    (nodup : ∀ clause ∈ formula, clause.Nodup)
    (input : VectorBuilder.Stored s.mem source (RecordTable.words w formula))
    (count : s.mem 24 = BitVec.ofNat w.bits formula.length)
    (pointer : s.mem 23 = BitVec.ofNat w.bits source)
    (leftPointer : s.mem 18 = BitVec.ofNat w.bits left)
    (rightPointer : s.mem 19 = BitVec.ofNat w.bits right)
    (qp : s.mem 20 = Masks.encode w core true) (qn : s.mem 21 = Masks.encode w core false)
    (target : s.mem 22 = BitVec.ofNat w.bits size) :
    ∃ time final, time ≤ formula.length * (12 * w.bits + 86) + 9 ∧
      Runs widthConstant (BranchPartition.algorithm.program w) time s final ∧ final.halted = true ∧
      VectorBuilder.Stored final.mem left (RecordTable.words w (Branch.remaining formula core size)) ∧
      VectorBuilder.Stored final.mem right (RecordTable.words w (BranchTables.petals formula core size)) ∧
      final.mem 16 = BitVec.ofNat w.bits (Branch.remaining formula core size).length ∧
      final.mem 17 = BitVec.ofNat w.bits (BranchTables.petals formula core size).length ∧
      final.mem 18 = BitVec.ofNat w.bits (left + 3 * (Branch.remaining formula core size).length) ∧
      final.mem 19 = BitVec.ofNat w.bits (right + 3 * (BranchTables.petals formula core size).length) ∧
      final.mem 20 = Masks.encode w core true ∧ final.mem 21 = Masks.encode w core false ∧
      final.mem 22 = BitVec.ofNat w.bits size ∧
      final.mem 23 = BitVec.ofNat w.bits (source + 3 * formula.length) ∧
      VectorBuilder.Stored final.mem source (RecordTable.words w formula) ∧
      (∀ a, PartitionInvariant.Outside formula.length left right a → final.mem a = s.mem a) := by
  let prepared := run widthConstant (BranchPartition.setup.program w) 4 s
  obtain ⟨ph, pt, pm, pl, pr, pf⟩ := BranchPartition.initializes s pc live
  let invariant := PartitionInvariant.Holds formula core size source left right s.mem
  have initial : invariant 0 prepared.mem := by
    refine ⟨by omega, ?_, trivial, trivial, pl, pr, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
    · apply MemoryCopy.stored_frame _ _ input
      intro a ha _
      have := layout.sourceBase
      exact pf a (by omega) (by omega) (by omega)
    · exact (pf 18 (by decide) (by decide) (by decide)).trans leftPointer
    · exact (pf 19 (by decide) (by decide) (by decide)).trans rightPointer
    · exact (pf 20 (by decide) (by decide) (by decide)).trans qp
    · exact (pf 21 (by decide) (by decide) (by decide)).trans qn
    · exact (pf 22 (by decide) (by decide) (by decide)).trans target
    · exact (pf 23 (by decide) (by decide) (by decide)).trans pointer
    · intro a ha
      exact pf a (by have := ha.1; omega) (by have := ha.1; omega) (by have := ha.1; omega)
  have stable : ∀ i mem cell value, invariant i mem → (cell = 0 ∨ cell = 24) → invariant i (mem.write cell value) := by
    intro i mem cell value h which
    exact PartitionInvariant.stable layout mem cell value h which
  have bodyCorrect : ∀ i, i < formula.length → ∀ state : State w,
      state.pc = 0 → state.halted = false → invariant i state.mem →
      state.mem 24 = BitVec.ofNat w.bits i → state.mem 25 = BitVec.ofNat w.bits formula.length →
      ∃ time out, time ≤ 12 * w.bits + 82 ∧
        Runs widthConstant (BranchPartition.body.code.map (SourceInstruction.compile w)) time state out ∧
        out.halted = true ∧ invariant (i + 1) out.mem ∧ out.mem 0 = 0#w.bits ∧
        out.mem 24 = BitVec.ofNat w.bits i ∧ out.mem 25 = BitVec.ofNat w.bits formula.length := by
    intro i hi state statePc stateLive inv index limit
    obtain ⟨time, out, bound, trace, halted, next, zero, sameIndex, sameLimit⟩ :=
      PartitionInvariant.step layout variablesFit width sizeFits nodup hi state statePc stateLive inv
    exact ⟨time, out, bound, trace, halted, next, zero, sameIndex.trans index, sameLimit.trans limit⟩
  have countFits : formula.length < 2 ^ w.bits := by have := layout.fits; omega
  obtain ⟨time, out, bound, trace, halted, finalInvariant, _, _⟩ :=
    SourceFor.iterates_from_zero 24 25 BranchPartition.body.code formula.length (12 * w.bits + 82)
      invariant (by decide) (by decide) countFits stable bodyCorrect (SourceChain.resume prepared)
      rfl rfl initial (pm.trans count)
  have full := SourceChain.traces BranchPartition.setup.code
    (SourceSearch.initialized 24 25 BranchPartition.body.code).code s prepared out 4 time live ph
    (trace_of_ticks _ s 4 pt) trace
  have align : 12 * w.bits + 82 + 4 = 12 * w.bits + 86 := by omega
  rw [align] at bound
  refine ⟨4 + time, out.relocate BranchPartition.setup.code.length, by omega, full, halted, ?_, ?_, ?_, ?_,
    ?_, ?_, finalInvariant.corePositive, finalInvariant.coreNegative, finalInvariant.target,
    finalInvariant.inputPointer, finalInvariant.input, finalInvariant.frame⟩
  · simpa only [List.take_length, State.relocate] using finalInvariant.remaining
  · simpa only [List.take_length, State.relocate] using finalInvariant.petals
  · simpa only [List.take_length, State.relocate] using finalInvariant.leftCount
  · simpa only [List.take_length, State.relocate] using finalInvariant.rightCount
  · simpa only [List.take_length, State.relocate] using finalInvariant.leftPointer
  · simpa only [List.take_length, State.relocate] using finalInvariant.rightPointer

end WordRAM.Conjectures.Sparsification.PartitionMachine

/-! Actual concatenation of two serialized clause tables into higher memory. -/
namespace WordRAM.Conjectures.Sparsification.RecordConcat

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

def prepare : Algorithm :=
  ⟨[.copy (.direct 1) (reg 26), .copy (.direct 2) (reg 28),
    .binary (.mul rfl) (.direct 3) (reg 29) (.immediate 3), .halt], 1, by decide⟩

def bridge : Algorithm :=
  ⟨[.copy (.direct 1) (reg 27), .binary (.mul rfl) (.direct 5) (reg 29) (.immediate 3),
    .binary .add (.direct 2) (reg 28) (reg 5),
    .binary (.mul rfl) (.direct 3) (reg 30) (.immediate 3), .halt], 1, by decide⟩

/-- Source pointers 26/27, destination 28, record counts 29/30.
Both sources must end before the destination. -/
def algorithm : Algorithm :=
  ⟨SourceChain.code prepare.code (SourceChain.code MemoryCopy.algorithm.code
    (SourceChain.code bridge.code MemoryCopy.algorithm.code)), 1, by decide⟩

theorem prepares (s : State w) (pc : s.pc = 0) (live : s.halted = false) :
    let t := run widthConstant (prepare.program w) 4 s
    t.halted = true ∧ t.ticks = s.ticks + 4 ∧ t.mem 1 = s.mem 26 ∧ t.mem 2 = s.mem 28 ∧
      t.mem 3 = s.mem 29 * 3#w.bits ∧ (∀ a, 4 ≤ a → t.mem a = s.mem a) := by
  simp [prepare, Algorithm.program, SourceInstruction.compile, SourceOperand.compile, reg, run, step,
    execute, Address.resolve, Operand.read, Memory.write, BinOp.eval, pc, live, Nat.add_assoc]
  intro a ha
  have h : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 := by omega
  simp [h]

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 27 ∧
      t.mem 2 = s.mem 28 + s.mem 29 * 3#w.bits ∧ t.mem 3 = s.mem 30 * 3#w.bits ∧
      (∀ a, 6 ≤ a → 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, BinOp.eval, pc, live, Nat.add_assoc]
  intro a ha
  have h : a ≠ 1 ∧ a ≠ 2 ∧ a ≠ 3 ∧ a ≠ 5 := 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

/-- Copy both tables in order. No assumption about literal distinctness or SAT
semantics is needed: every stored record word is preserved exactly. -/
theorem concatenates (left right : CNF n) (s : State w) (first second destination : Nat)
    (pc : s.pc = 0) (live : s.halted = false)
    (firstBase : 32 ≤ first) (secondBase : 32 ≤ second)
    (firstEnd : first + 3 * left.length ≤ destination)
    (secondEnd : second + 3 * right.length ≤ destination)
    (fits : destination + 3 * (left.length + right.length) < 2 ^ w.bits)
    (firstPointer : s.mem 26 = BitVec.ofNat w.bits first)
    (secondPointer : s.mem 27 = BitVec.ofNat w.bits second)
    (outputPointer : s.mem 28 = BitVec.ofNat w.bits destination)
    (firstCount : s.mem 29 = BitVec.ofNat w.bits left.length)
    (secondCount : s.mem 30 = BitVec.ofNat w.bits right.length)
    (firstInput : VectorBuilder.Stored s.mem first (RecordTable.words w left))
    (secondInput : VectorBuilder.Stored s.mem second (RecordTable.words w right)) :
    ∃ final, Runs widthConstant (algorithm.program w) (21 * (left.length + right.length) + 13) s final ∧
      final.halted = true ∧ VectorBuilder.Stored final.mem destination (RecordTable.words w (left ++ right)) ∧
      (∀ a, 6 ≤ a → (a < destination ∨ destination + 3 * (left.length + right.length) ≤ a) → final.mem a = s.mem a) := by
  have destinationBase : 32 ≤ destination := by omega
  let prepared := run widthConstant (prepare.program w) 4 s
  obtain ⟨ph, pt, pp, pd, pn, pf⟩ := prepares s pc live
  have input1 : VectorBuilder.Stored prepared.mem first (RecordTable.words w left) := by
    apply MemoryCopy.stored_frame _ _ firstInput
    intro a ha _; exact pf a (by omega)
  have count1 : prepared.mem 3 = BitVec.ofNat w.bits (RecordTable.words w left).length := by
    rw [RecordTable.words_length]
    exact pn.trans (by rw [firstCount, ← BitVec.ofNat_mul, Nat.mul_comm])
  obtain ⟨copied, ct, ch, co, cf⟩ := MemoryCopy.copies (RecordTable.words w left) (SourceChain.resume prepared)
    first destination rfl rfl (by omega) (by simpa only [RecordTable.words_length] using firstEnd)
    (by rw [RecordTable.words_length]; omega) (pp.trans firstPointer) (pd.trans outputPointer) count1 input1
  have copiedLow : ∀ a, 6 ≤ a → a < 32 → copied.mem a = s.mem a := by
    intro a ha hb
    exact (cf a (by omega) (Or.inl (by omega))).trans (pf a (by omega))
  let middle := run widthConstant (bridge.program w) 5 (SourceChain.resume copied)
  obtain ⟨mh, mt, mp, md, mn, mf⟩ := bridges (SourceChain.resume copied) rfl rfl
  have pointer2 : middle.mem 1 = BitVec.ofNat w.bits second := mp.trans ((copiedLow 27 (by decide) (by decide)).trans secondPointer)
  have destination2 : middle.mem 2 = BitVec.ofNat w.bits (destination + 3 * left.length) := by
    calc
      middle.mem 2 = copied.mem 28 + copied.mem 29 * 3#w.bits := md
      _ = BitVec.ofNat w.bits destination + BitVec.ofNat w.bits left.length * 3#w.bits := by
        rw [copiedLow 28 (by decide) (by decide), copiedLow 29 (by decide) (by decide), outputPointer, firstCount]
      _ = BitVec.ofNat w.bits (destination + 3 * left.length) := by rw [← BitVec.ofNat_mul, ← BitVec.ofNat_add, Nat.mul_comm left.length]
  have count2 : middle.mem 3 = BitVec.ofNat w.bits (RecordTable.words w right).length := by
    calc
      middle.mem 3 = copied.mem 30 * 3#w.bits := mn
      _ = BitVec.ofNat w.bits right.length * 3#w.bits := by rw [copiedLow 30 (by decide) (by decide), secondCount]
      _ = BitVec.ofNat w.bits (RecordTable.words w right).length := by rw [← BitVec.ofNat_mul, RecordTable.words_length, Nat.mul_comm right.length]
  have input2 : VectorBuilder.Stored middle.mem second (RecordTable.words w right) := by
    apply MemoryCopy.stored_frame _ _ secondInput
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact (mf a (by omega)).trans ((cf a (by omega) (Or.inl (by omega))).trans (pf a (by omega)))
  obtain ⟨out, ot, oh, oo, ofr⟩ := MemoryCopy.copies (RecordTable.words w right) (SourceChain.resume middle)
    second (destination + 3 * left.length) rfl rfl (by omega)
    (by rw [RecordTable.words_length]; omega) (by rw [RecordTable.words_length]; omega)
    pointer2 destination2 count2 input2
  have firstOutput : VectorBuilder.Stored out.mem destination (RecordTable.words w left) := by
    apply MemoryCopy.stored_frame _ _ co
    intro a ha hb
    rw [RecordTable.words_length] at hb
    exact (ofr a (by omega) (Or.inl hb)).trans (mf a (by omega))
  have tail := SourceChain.traces bridge.code MemoryCopy.algorithm.code (SourceChain.resume copied) middle out
    5 (7 * (RecordTable.words w right).length + 2) rfl mh (trace_of_ticks _ _ 5 mt) ot
  have mid := SourceChain.traces MemoryCopy.algorithm.code (SourceChain.code bridge.code MemoryCopy.algorithm.code)
    (SourceChain.resume prepared) copied _ (7 * (RecordTable.words w left).length + 2)
    (5 + (7 * (RecordTable.words w right).length + 2)) rfl ch ct tail
  have full := SourceChain.traces prepare.code (SourceChain.code MemoryCopy.algorithm.code
      (SourceChain.code bridge.code MemoryCopy.algorithm.code)) s prepared _ 4
    ((7 * (RecordTable.words w left).length + 2) + (5 + (7 * (RecordTable.words w right).length + 2))) live ph
    (trace_of_ticks _ s 4 pt) mid
  have cost : 4 + ((7 * (RecordTable.words w left).length + 2) + (5 + (7 * (RecordTable.words w right).length + 2))) =
      21 * (left.length + right.length) + 13 := by rw [RecordTable.words_length, RecordTable.words_length]; omega
  refine ⟨((out.relocate bridge.code.length).relocate MemoryCopy.algorithm.code.length).relocate prepare.code.length,
    ?_, oh, ?_, ?_⟩
  · simpa only [algorithm, Algorithm.program, cost] using full
  · exact (BranchTables.records_append left right out.mem destination).mpr ⟨firstOutput, oo⟩
  · intro a ha outside
    have o1 : a < destination ∨ destination + (RecordTable.words w left).length ≤ a := by rw [RecordTable.words_length]; omega
    have o2 : a < destination + 3 * left.length ∨ destination + 3 * left.length + (RecordTable.words w right).length ≤ a := by
      rw [RecordTable.words_length]; omega
    exact (ofr a (by omega) o2).trans ((mf a ha).trans ((cf a (by omega) o1).trans (pf a (by omega))))

end WordRAM.Conjectures.Sparsification.RecordConcat