From addb04d8e741187f0cd1530e58638d79a9e073c5 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 1 Nov 2026 20:36:09 -0500
Subject: [PATCH 1/2] feat(WordRAM): derive the framed memory queue
 implementation

Build the existing local native target from one global typed method certificate,
actual semantic invariant and G<=7M+80. Native body charge is amortized153*factor,
potential48*factor*rearCount. Fresh13/linear dirtyclear4*space+19 are distinct
from literal source allocation, which remains separate under #2213/#2205.

Codex authoring: mathlib_cache_retry_1730, BPL empty-representation proof;
roadmap_algorithms integration/self-review. All24 immutable providers and two
new source/test packet hashes remain exact. M1a412ad source/credit preserved.
Focused strict native FIFO/C0/dirty-clear tests and hygiene pass; fullsix to
follow at this frozen revision. Outside-authoring-fleet API/correctness review
required. No selected abstracts/catalogue/rendering impact or M1 improvement.
---
 Complexity.lean                               |   1 +
 .../Client/MemoryQueueAdapter.lean            | 762 ++++++++++++++++++
 .../WordRAMRealizationQueueAdapter.lean       | 186 +++++
 ROADMAP.md                                    |   6 +-
 UPSTREAM.md                                   |  10 +-
 5 files changed, 961 insertions(+), 4 deletions(-)
 create mode 100644 Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
 create mode 100644 ComplexityTests/WordRAMRealizationQueueAdapter.lean

diff --git a/Complexity.lean b/Complexity.lean
index bac187b2dd..91cb87a947 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2560,6 +2560,7 @@ public import Complexity.Computability.WordRAM.Realization.Basic
 public import Complexity.Computability.WordRAM.Realization.Bind
 public import Complexity.Computability.WordRAM.Realization.Branch
 public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueue
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueAdapter
 public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueDispatch
 public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueFrame
 public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueInit
diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
new file mode 100644
index 0000000000..6bcfac178b
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
@@ -0,0 +1,762 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+module
+-- upstream: candidate
+
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueMethod
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueFrame
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueInit
+public import Complexity.Computability.WordRAM.Realization.Module
+
+/-!
+# A framed native queue from the memory-client kernel
+
+The existing semantic queue invariant discharges the complete native method's actual-state
+domains. The global emitter consumes runtime layouts and the typed operation, so its code,
+register count, scratch and exchange factor precede the queue's base, capacity and word width.
+The result representation uses a presence tag and an unshifted word, including the largest
+fitting payload.
+
+`implementation` fills the existing `SubroutineBase` and `WordRAM.StateTransitionImpl` APIs.
+Its representation adds bounded native data and persistent layout registers to the original
+M1a queue representation. Finite-block support, argument encoding, typed decoding, fresh
+initialization and the full method memory footprint are proved at this boundary.
+
+The certified method work satisfies `G ≤ 7 M + 80` on queue states. Scaling the existing
+nine-memory-unit queue inequality gives an amortized native body charge `153 * factor` and a
+potential
+`48 * factor * rearCount`. The existing flat-call API adds its trailing halt separately.
+Register argument delivery follows that API's `prepareRegs` convention; arbitrary host-client
+pure computations are not part of this operation-sequence clock.
+
+Initialization reserves `2 * (C + 1)` cells at an arbitrary base. Its fresh native body costs
+thirteen steps under the existing zero-block hypothesis. The reusable dirty-clear body costs
+at most `4 * space + 19`; it zeros the entire owned block. These local framed initializers are
+separate from the source `allocLayout` sequence, which clears only count cells and reserves
+dirty item arrays. No whole-client allocation cost is absorbed into the method charge.
+
+## Main definitions
+
+* `frontLayout`, `rearLayout`, `space`: the consecutive two-stack storage layout.
+* `program`: one global native code body and register ABI.
+* `implementation`: the existing framed queue certificate, with explicit initialization bounds.
+
+## Main results
+
+* `dequeue_safe`, `method_safe`: existing invariants discharge actual runtime domains.
+* `method_work_bound`, `method_pay`: all memory, glue, dispatch and result-staging work is paid.
+* `implementation_rep_iff`: the precise local representation and persistent register condition.
+* `implementation_charge`, `implementation_initTime`, `implementation_decode_dequeue`: usable
+  resource and typed-result facts without unfolding private certificate plumbing.
+
+## References
+
+The semantic programs and their queue potential are reused unchanged from the two-stack queue
+of [CLRS2009], Exercise 10.1-6 and Chapter 17. The native composition and its explicit local-work
+accounting are original infrastructure over those existing programs.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.MemoryQueueAdapter
+
+open Cslib.DataStructure
+
+/-- The front count cell and item array, relative to the queue's runtime base. -/
+def frontLayout (base C : ℕ) : Stack.Memory.Layout := ⟨⟨base, 1⟩, ⟨base + 1, C⟩⟩
+
+/-- The rear follows the complete front layout. -/
+def rearLayout (base C : ℕ) : Stack.Memory.Layout :=
+  ⟨⟨base + 1 + C, 1⟩, ⟨base + 1 + C + 1, C⟩⟩
+
+/-- The two count cells and two capacity-sized arrays. -/
+def space (C : ℕ) : ℕ := 2 * (C + 1)
+
+/-- A fitting end address supplies the capacity fit and two disjoint well-formed layouts. -/
+theorem layouts_valid {w base C : ℕ} (hf : Fits w (base + space C)) :
+    (frontLayout base C).Valid w C ∧ (rearLayout base C).Valid w C ∧
+      Disjoint (frontLayout base C).footprint (rearLayout base C).footprint := by
+  have hC : Fits w C := hf.of_le (by unfold space; omega)
+  refine ⟨⟨rfl, ?_, rfl, hC⟩, ⟨rfl, ?_, rfl, hC⟩, ?_⟩
+  · simp [frontLayout, Block.Owns]
+  · simp [rearLayout, Block.Owns]
+  · rw [Finset.disjoint_left]
+    intro a ha hb
+    simp only [Stack.Memory.Layout.footprint, frontLayout, rearLayout, Finset.mem_union,
+      Block.mem_footprint, Block.Owns] at ha hb
+    omega
+
+/-- Exactly the existing single owned block is occupied by the two layouts. -/
+theorem layouts_footprint (base C : ℕ) :
+    (frontLayout base C).footprint ∪ (rearLayout base C).footprint =
+      (Block.mk base (space C)).footprint := by
+  ext a
+  simp only [Stack.Memory.Layout.footprint, frontLayout, rearLayout, Finset.mem_union,
+    Block.mem_footprint, Block.Owns, space]
+  omega
+
+/-- A zeroed owned queue span represents the empty queue. The proof reads only its count cells;
+no global well-formedness assumption is required for an empty list. -/
+theorem empty_rep {w base C : ℕ} (hf : Fits w (base + space C)) (e : Memory.State)
+    (hfront : e.frontier = base + space C)
+    (hzero : ∀ a ∈ (Block.mk base (space C)).footprint, e.mem a = 0) :
+    (Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+      (layouts_valid hf).2.2).toModule.rep [] e := by
+  have h₀ : e.mem base = 0 := hzero base (by
+    simp only [Block.mem_footprint, Block.Owns, space]
+    omega)
+  have h₁ : e.mem (base + 1 + C) = 0 := hzero (base + 1 + C) (by
+    simp only [Block.mem_footprint, Block.Owns, space]
+    omega)
+  have hi₀ : Stack.Memory.Inv (frontLayout base C) e := by
+    refine ⟨?_, ?_, ?_⟩
+    · change base + 1 ≤ e.frontier
+      rw [hfront]
+      unfold space
+      omega
+    · change base + 1 + C ≤ e.frontier
+      rw [hfront]
+      unfold space
+      omega
+    · change e.mem base ≤ C
+      rw [h₀]
+      exact Nat.zero_le C
+  have hi₁ : Stack.Memory.Inv (rearLayout base C) e := by
+    refine ⟨?_, ?_, ?_⟩
+    · change base + 1 + C + 1 ≤ e.frontier
+      rw [hfront]
+      unfold space
+      omega
+    · change base + 1 + C + 1 + C ≤ e.frontier
+      rw [hfront]
+      unfold space
+      omega
+    · change e.mem (base + 1 + C) ≤ C
+      rw [h₁]
+      exact Nat.zero_le C
+  have ha₀ : Stack.Memory.abs (frontLayout base C) e = [] := by
+    simp only [Stack.Memory.abs, frontLayout, h₀, Block.entries_zero, List.reverse_nil]
+  have ha₁ : Stack.Memory.abs (rearLayout base C) e = [] := by
+    simp only [Stack.Memory.abs, rearLayout, h₁, Block.entries_zero, List.reverse_nil]
+  change ((Stack.Memory.Inv (frontLayout base C) e ∧
+    Stack.Memory.Inv (rearLayout base C) e) ∧
+    Queue.Memory.Inv w C (Queue.WordRAM.contents
+      (Stack.Memory.abs (frontLayout base C) e, Stack.Memory.abs (rearLayout base C) e))) ∧
+    Queue.WordRAM.contents
+      (Stack.Memory.abs (frontLayout base C) e, Stack.Memory.abs (rearLayout base C) e) = []
+  refine ⟨⟨⟨hi₀, hi₁⟩, ?_⟩, ?_⟩
+  · rw [ha₀, ha₁]
+    exact ⟨by simp [Queue.WordRAM.contents], by simp [Queue.WordRAM.contents]⟩
+  · rw [ha₀, ha₁]
+    rfl
+
+/-- Disjoint allocated stacks within total capacity satisfy the exact native dequeue domain.
+On an empty front, its pop and the rear-size query preserve the state, and the generic transfer
+invariant supplies both the reached loop domains and the final front-pop invariant. -/
+theorem dequeue_safe {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    MemoryQueueDispatch.dequeueSafe w (L₁, L₂) s := by
+  change L₁.Valid w L₁.items.length ∧ Stack.Memory.Inv L₁ s ∧ _
+  refine ⟨by simpa only [h₁.items_length] using h₁, hs₁, ?_⟩
+  by_cases h0 : s.mem L₁.count.base = 0
+  · have hpop := Stack.Memory.runClient_pop_of_eq_zero (w := 0) L₁ s h0
+    have hresult : (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) = none :=
+      congrArg Prod.fst hpop
+    rw [hresult]
+    have hmid : (Memory.spec 0).clientState
+        ((Memory.spec 0).clientState s (Stack.Memory.pop L₁)) (Stack.Memory.size L₂) = s := by
+      simp only [StateTransitionSpec.clientState, hpop, Stack.Memory.runClient_size]
+    have hfuel : MemoryQueueDispatch.dequeueFuel (L₁, L₂) s = s.mem L₂.count.base := by
+      simp only [MemoryQueueDispatch.dequeueFuel, StateTransitionSpec.clientResult,
+        StateTransitionSpec.clientState, hpop, Stack.Memory.runClient_size]
+    rw [hmid, hfuel]
+    obtain ⟨hsafe, _, hfront, _, _, _, _⟩ :=
+      MemoryQueue.transfer_invariant h₁ h₂ hd hw hs₁ hs₂ rfl hlen
+    refine ⟨hsafe, ?_⟩
+    have hstate : (Memory.spec 0).clientState s
+        (link (Stack.Memory.pairMethods L₁ L₂ 0 0) (Queue.transfer (s.mem L₂.count.base))) =
+        (Memory.spec 0).clientState s
+          (iterate MemoryQueue.transferBody (L₁, L₂) (s.mem L₂.count.base) true) := by
+      rw [MemoryQueue.transfer_eq_iterate]
+      simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind]
+      rfl
+    exact hstate.symm ▸ hfront
+  · have hpop := Stack.Memory.runClient_pop_of_pos (w := 0) L₁ s h0
+    have hresult : (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) =
+        some (s.mem (L₁.items.base + (s.mem L₁.count.base - 1))) := congrArg Prod.fst hpop
+    rw [hresult]
+    trivial
+
+/-- On the fallback path the complete source dequeue pays at least the six memory units for
+each transferred rear item, in addition to its other queries. -/
+theorem dequeue_cost_ge_transfer {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C)
+    (h0 : s.mem L₁.count.base = 0) :
+    6 * s.mem L₂.count.base ≤
+      memoryCost (Queue.Memory.memMethods L₁ L₂ w C .dequeue) s := by
+  have hpop := Stack.Memory.runClient_pop_of_eq_zero (w := 0) L₁ s h0
+  have hresult : (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) = none :=
+    congrArg Prod.fst hpop
+  have hstate : (Memory.spec 0).clientState s (Stack.Memory.pop L₁) = s :=
+    congrArg (fun t => t.2.1) hpop
+  obtain ⟨_, _, _, _, _, _, hcost⟩ :=
+    MemoryQueue.transfer_invariant h₁ h₂ hd hw hs₁ hs₂ rfl hlen
+  rw [MemoryQueue.memMethods_dequeue]
+  change _ ≤ memoryCost ((Stack.Memory.pop L₁).bind _) s
+  rw [memoryCost_bind, hresult, hstate]
+  change _ ≤ memoryCost (Stack.Memory.pop L₁) s + memoryCost
+    ((Stack.Memory.size L₂).bind (fun n => (iterate MemoryQueue.transferBody
+      (L₁, L₂) n true).bind (fun _ => Stack.Memory.pop L₁))) s
+  rw [memoryCost_bind]
+  change _ ≤ memoryCost (Stack.Memory.pop L₁) s +
+    (memoryCost (Stack.Memory.size L₂) s + memoryCost ((iterate MemoryQueue.transferBody
+      (L₁, L₂) (s.mem L₂.count.base) true).bind (fun _ => Stack.Memory.pop L₁)) s)
+  rw [memoryCost_bind, hcost]
+  omega
+
+/-- The dispatch's certified local work is paid by the actual source memory cost under the
+queue storage invariants. The bound keeps the explicit constant for short and empty paths. -/
+theorem dequeue_work_bound {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hs₁ : Stack.Memory.Inv L₁ s) (hs₂ : Stack.Memory.Inv L₂ s)
+    (hlen : s.mem L₁.count.base + s.mem L₂.count.base ≤ C) :
+    MemoryQueueDispatch.dequeueWork (L₁, L₂) s ≤
+      7 * memoryCost (Queue.Memory.memMethods L₁ L₂ w C .dequeue) s + 69 := by
+  by_cases h0 : s.mem L₁.count.base = 0
+  · have hpop := Stack.Memory.runClient_pop_of_eq_zero (w := 0) L₁ s h0
+    have hcost := dequeue_cost_ge_transfer h₁ h₂ hd hw hs₁ hs₂ hlen h0
+    change (match (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) with
+      | some _ => 28
+      | none => 40 * MemoryQueueDispatch.dequeueFuel (L₁, L₂) s + 69) ≤ _
+    have hresult : (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) = none :=
+      congrArg Prod.fst hpop
+    rw [hresult]
+    have hfuel : MemoryQueueDispatch.dequeueFuel (L₁, L₂) s = s.mem L₂.count.base := by
+      simp only [MemoryQueueDispatch.dequeueFuel, StateTransitionSpec.clientResult,
+        StateTransitionSpec.clientState, hpop, Stack.Memory.runClient_size]
+    rw [hfuel]
+    dsimp only
+    nlinarith only [hcost]
+  · have hpop := Stack.Memory.runClient_pop_of_pos (w := 0) L₁ s h0
+    have hresult : (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) =
+        some (s.mem (L₁.items.base + (s.mem L₁.count.base - 1))) := congrArg Prod.fst hpop
+    change (match (Memory.spec 0).clientResult s (Stack.Memory.pop L₁) with
+      | some _ => 28
+      | none => 40 * MemoryQueueDispatch.dequeueFuel (L₁, L₂) s + 69) ≤ _
+    rw [hresult]
+    dsimp only
+    omega
+
+/-- The composite's storage invariant supplies the two component invariants and total count
+bound. This unfolds only the existing composed refinement, not a replacement queue model. -/
+theorem invariant_fields {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hi : (Queue.Memory.memRefinement h₁ h₂ hd).inv s) :
+    Stack.Memory.Inv L₁ s ∧ Stack.Memory.Inv L₂ s ∧
+      s.mem L₁.count.base + s.mem L₂.count.base ≤ C := by
+  change (Stack.Memory.Inv L₁ s ∧ Stack.Memory.Inv L₂ s) ∧
+    Queue.Memory.Inv w C (Queue.WordRAM.contents (Stack.Memory.abs L₁ s, Stack.Memory.abs L₂ s))
+    at hi
+  refine ⟨hi.1.1, hi.1.2, ?_⟩
+  have h := hi.2.length_le
+  simpa only [Queue.WordRAM.contents, List.length_append, List.length_reverse,
+    Stack.Memory.length_abs] using h
+
+/-- The existing composite queue invariant and an admissible operation discharge the domain of
+one global native method certificate before any runtime layout is selected. -/
+theorem method_safe {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hi : (Queue.Memory.memRefinement h₁ h₂ hd).inv s) (o : Queue.QueueOp ℕ)
+    (hv : (Queue.WordRAM.spec w C).valid ((Queue.Memory.memRefinement h₁ h₂ hd).abs s) o) :
+    MemoryQueueMethod.methodSafe w ((L₁, L₂), o) s := by
+  obtain ⟨hs₁, hs₂, hlen⟩ := invariant_fields h₁ h₂ hd hi
+  cases o with
+  | enqueue v =>
+    change ((Stack.Memory.abs L₁ s) ++ (Stack.Memory.abs L₂ s).reverse).length < C ∧ Fits w v
+      at hv
+    simp only [List.length_append, List.length_reverse, Stack.Memory.length_abs] at hv
+    exact ⟨by simpa only [h₂.items_length] using h₂, hs₂,
+      by simpa only [h₂.items_length] using (show s.mem L₂.count.base < C by omega)⟩
+  | dequeue => exact dequeue_safe h₁ h₂ hd hw hs₁ hs₂ hlen
+
+private theorem method_memoryCost (L₁ L₂ : Stack.Memory.Layout) (w C : ℕ) (o : Queue.QueueOp ℕ)
+    (s : Memory.State) :
+    memoryCost (MemoryQueueMethod.method ((L₁, L₂), o)) s =
+      memoryCost (Queue.Memory.memMethods L₁ L₂ w C o) s := by
+  rw [MemoryQueueMethod.method_source_eq ((L₁, L₂), o) w C]
+  change memoryCost ((Queue.Memory.memMethods L₁ L₂ w C o).bind _) s = _
+  rw [memoryCost_bind]
+  rfl
+
+/-- The global method's actual grading, including typed-result staging and operation dispatch,
+is uniformly dominated on queue states. The constant 80 is retained on empty and short paths. -/
+theorem method_work_bound {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hi : (Queue.Memory.memRefinement h₁ h₂ hd).inv s) (o : Queue.QueueOp ℕ) :
+    MemoryQueueMethod.methodWork ((L₁, L₂), o) s ≤
+      7 * memoryCost (MemoryQueueMethod.method ((L₁, L₂), o)) s + 80 := by
+  obtain ⟨hs₁, hs₂, hlen⟩ := invariant_fields h₁ h₂ hd hi
+  rw [method_memoryCost L₁ L₂ w C o s]
+  cases o with
+  | enqueue v => change 21 ≤ _; omega
+  | dequeue =>
+    have h := dequeue_work_bound h₁ h₂ hd hw hs₁ hs₂ hlen
+    change MemoryQueueDispatch.dequeueWork (L₁, L₂) s + 11 ≤ _
+    omega
+
+private theorem totalCost_width (w : ℕ) (os : List Memory.Op) (s : Memory.State) :
+    (Memory.spec w).totalCost Memory.charge s os =
+      (Memory.spec 0).totalCost Memory.charge s os := by
+  induction os generalizing s with
+  | nil => rfl
+  | cons o os ih =>
+    simpa only [StateTransitionSpec.totalCost_cons] using
+      congrArg (Memory.charge s o + ·) (ih (Memory.step s o).1)
+
+/-- The existing memory amortization lifts to the global native certificate's complete grading.
+The factor is selected globally before runtime layouts; the resulting potential and charge
+retain all memory, glue, result-staging and dispatch work. -/
+theorem method_pay {L₁ L₂ : Stack.Memory.Layout} {w C : ℕ}
+    (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) (hd : Disjoint L₁.footprint L₂.footprint)
+    {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hi : (Queue.Memory.memRefinement h₁ h₂ hd).inv s) (o : Queue.QueueOp ℕ)
+    (hv : (Queue.WordRAM.spec w C).valid ((Queue.Memory.memRefinement h₁ h₂ hd).abs s) o)
+    (factor : ℕ) :
+    factor * (memoryCost (MemoryQueueMethod.method ((L₁, L₂), o)) s +
+        MemoryQueueMethod.methodWork ((L₁, L₂), o) s + 1) +
+        48 * factor * ((Memory.spec 0).clientState s
+          (MemoryQueueMethod.method ((L₁, L₂), o))).mem L₂.count.base ≤
+      153 * factor + 48 * factor * s.mem L₂.count.base := by
+  let M := Queue.Memory.memRefinement h₁ h₂ hd
+  have hvalid := ((Memory.spec w).demonicValid_iff_validHistory_runClient _ _).mp
+    (M.valid o hi hv)
+  have hpay := (Queue.Memory.mem_amortized h₁ h₂ hd).step o hi hv
+    ((Memory.spec w).clientRun_canonical s _ hvalid)
+  rw [StateTransitionSpec.totalCostTranscript_canonicalTranscript] at hpay
+  change (Memory.spec w).totalCost Memory.charge s
+      ((Memory.spec w).clientHistory s (M.methods o)) +
+      6 * (Stack.Memory.abs L₂ ((Memory.spec w).clientState s (M.methods o))).length ≤
+    9 + 6 * (Stack.Memory.abs L₂ s).length at hpay
+  have hm : M.methods = Queue.Memory.memMethods L₁ L₂ w C :=
+    Queue.Memory.memRefinement_methods h₁ h₂ hd
+  rw [hm, clientState_width w] at hpay
+  have hhistory : (Memory.spec w).clientHistory s (Queue.Memory.memMethods L₁ L₂ w C o) =
+      (Memory.spec 0).clientHistory s (Queue.Memory.memMethods L₁ L₂ w C o) :=
+    congrArg (fun t => t.2.2) (runClient_width w (Queue.Memory.memMethods L₁ L₂ w C o) s)
+  rw [hhistory, totalCost_width w] at hpay
+  change memoryCost (Queue.Memory.memMethods L₁ L₂ w C o) s +
+      6 * (Stack.Memory.abs L₂ ((Memory.spec 0).clientState s
+        (Queue.Memory.memMethods L₁ L₂ w C o))).length ≤
+    9 + 6 * (Stack.Memory.abs L₂ s).length at hpay
+  have hstate : (Memory.spec 0).clientState s (MemoryQueueMethod.method ((L₁, L₂), o)) =
+      (Memory.spec 0).clientState s (Queue.Memory.memMethods L₁ L₂ w C o) := by
+    rw [MemoryQueueMethod.method_source_eq ((L₁, L₂), o) w C]
+    change (Memory.spec 0).clientState s ((Queue.Memory.memMethods L₁ L₂ w C o).bind _) = _
+    simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind]
+    rfl
+  rw [← method_memoryCost L₁ L₂ w C o s, ← hstate] at hpay
+  simp only [Stack.Memory.length_abs] at hpay
+  have h := scaled_potential_pay
+    (memoryCost (MemoryQueueMethod.method ((L₁, L₂), o)) s)
+    (MemoryQueueMethod.methodWork ((L₁, L₂), o) s)
+    (factor * (memoryCost (MemoryQueueMethod.method ((L₁, L₂), o)) s +
+      MemoryQueueMethod.methodWork ((L₁, L₂), o) s + 1))
+    (6 * s.mem L₂.count.base)
+    (6 * ((Memory.spec 0).clientState s
+      (MemoryQueueMethod.method ((L₁, L₂), o))).mem L₂.count.base)
+    9 factor 7 80 le_rfl (method_work_bound h₁ h₂ hd hw hi o) hpay
+  convert h using 1 <;> ring
+
+/-- The register count is fixed by the global method certificate, before base, capacity or width. -/
+noncomputable def registers : ℕ := 16 + (4 + MemoryQueueMethod.realizes_method.scratchSize + 1)
+
+/-- The fixed ABI reserves the first sixteen registers; the global method's scratch follows. -/
+noncomputable def register : Fin 16 ↪ Fin registers where
+  toFun i := ⟨i.val, by have := i.isLt; unfold registers; omega⟩
+  inj' := by
+    intro i j h
+    apply Fin.ext
+    exact congrArg (fun x : Fin registers => x.val) h
+
+/-- Source registers are the fixed eleven-word global method ABI. -/
+noncomputable def source : Fin 11 → Fin registers :=
+  fun i => register (Fin.castLE (by decide) i)
+
+/-- The complete output and scratch bank follows the persistent ABI and controls. -/
+noncomputable def scratch :
+    Fin (4 + MemoryQueueMethod.realizes_method.scratchSize + 1) → Fin registers :=
+  fun i => ⟨16 + i.val, by have := i.isLt; unfold registers; omega⟩
+
+/-- The four typed-label words occupy the first four result-bank registers. -/
+noncomputable def outputRegister (i : Fin 4) : Fin registers :=
+  scratch (Fin.castAdd (MemoryQueueMethod.realizes_method.scratchSize + 1) i)
+
+/-- One fixed code body and initialization ABI for all runtime bases and capacities. The first
+three operation words alone are caller inputs; all eight layout words are persistent state. -/
+noncomputable def program : SubroutineCode .exact registers 1 where
+  allocSpan := MemoryQueueInit.spanCode register
+  initSetup := MemoryQueueInit.setupCode register
+  code := MemoryQueueMethod.realizes_method.code (register 11) source scratch
+  frontierReg := register 11
+  baseReg := register 12
+  initParams _ := register 3
+  curReg := register 13
+  zeroReg := register 14
+  oneReg := register 15
+  incCur := .exactBin .add (register 13) (register 13) (register 15)
+  input i := decide (8 ≤ i.val ∧ i.val < 11)
+  output := outputRegister 3
+
+private def semanticModule (w base C : ℕ) (hf : Fits w (base + space C)) :
+    Module (Queue.WordRAM.spec w C) (Memory.spec w) :=
+  (Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+    (layouts_valid hf).2.2).toModule
+
+private noncomputable def layoutMatch (base C : ℕ) (regs : Fin registers → ℕ) : Prop :=
+  ∀ i : Fin 8, regs (register (Fin.castLE (by decide) i)) =
+    MemoryQueue.layoutWords (frontLayout base C, rearLayout base C) i
+
+private noncomputable def representation (w base C : ℕ) (hf : Fits w (base + space C))
+    (q : List ℕ) (x : Data registers) : Prop :=
+  x.Bounded w ∧ layoutMatch base C x.regs ∧
+    (semanticModule w base C hf).rep q (memoryState (register 11) x)
+
+private noncomputable def operationMatch (o : Queue.QueueOp ℕ) (regs : Fin registers → ℕ) : Prop :=
+  ∀ i : Fin 3, regs (register (Fin.natAdd 8 i |>.castLE (by decide))) =
+    MemoryQueueMethod.opWords o i
+
+private noncomputable def encode (o : Queue.QueueOp ℕ) (i : Fin registers) : ℕ :=
+  if h : 8 ≤ i.val ∧ i.val < 11 then
+    MemoryQueueMethod.opWords o ⟨i.val - 8, by omega⟩ else 0
+
+private noncomputable def decode : (o : Queue.QueueOp ℕ) →
+    (Fin registers → ℕ) → Option ((Queue.WordRAM.spec 0 0).Result o)
+  | .enqueue _, _ => some ()
+  | .dequeue, regs =>
+      some (if regs (outputRegister 2) = 0 then none else some (regs (outputRegister 3)))
+
+private theorem scratch_injective : Function.Injective scratch := by
+  intro i j h
+  apply Fin.ext
+  have := congrArg Fin.val h
+  change 16 + i.val = 16 + j.val at this
+  omega
+
+private theorem source_scratch (i : Fin 11) (j) : source i ≠ scratch j := by
+  intro h
+  have := congrArg Fin.val h
+  change i.val = 16 + j.val at this
+  have := i.isLt
+  omega
+
+private theorem scratch_frontier (j) : scratch j ≠ register 11 := by
+  intro h
+  have := congrArg Fin.val h
+  change 16 + j.val = 11 at this
+  omega
+
+private theorem source_frontier (i : Fin 11) : source i ≠ register 11 := by
+  intro h
+  have := congrArg Fin.val h
+  change i.val = 11 at this
+  have := i.isLt
+  omega
+
+private theorem layoutWords_relative (base C : ℕ) :
+    MemoryQueue.layoutWords (frontLayout base C, rearLayout base C) =
+      ![base, 1, base + 1, C, base + 1 + C, 1, base + 1 + C + 1, C] := by
+  funext i
+  fin_cases i <;> rfl
+
+private theorem op_words_fit {w C : ℕ} {q : List ℕ} (h1 : Fits w 1) (o : Queue.QueueOp ℕ)
+    (hv : (Queue.WordRAM.spec w C).valid q o) (i : Fin 3) :
+    Fits w (MemoryQueueMethod.opWords o i) := by
+  cases o with
+  | enqueue v => fin_cases i <;> first | exact fits_zero w | exact hv.2
+  | dequeue => fin_cases i <;> first | exact h1 | exact fits_zero w
+
+private noncomputable def baseCertificate (w base C : ℕ) (hf : Fits w (base + space C)) :
+    SubroutineBase program (Queue.WordRAM.spec w C).Result (Queue.WordRAM.spec w C).valid
+      w base (fun _ => C) [] where
+  space := space C
+  spanTime := 6
+  setupTime := 7
+  initPotential := 0
+  charge _ _ := 153 * MemoryQueueMethod.realizes_method.factor
+  rep := representation w base C hf
+  potential x := 48 * MemoryQueueMethod.realizes_method.factor * x.mem (base + 1 + C)
+  encode := encode
+  argMatch := operationMatch
+  decode := decode
+  bounded hr := hr.1
+  arguments_fit := by
+    intro q o hv i hi
+    change decide (8 ≤ i.val ∧ i.val < 11) = true at hi
+    have hh := of_decide_eq_true hi
+    change Fits w (if h : 8 ≤ i.val ∧ i.val < 11 then
+      MemoryQueueMethod.opWords o ⟨i.val - 8, by omega⟩ else 0)
+    rw [dite_eq_left hh]
+    exact op_words_fit (hf.of_le (by unfold space; omega)) o hv _
+  encode_matches := by
+    intro o regs i
+    fin_cases i <;> simp [program, encode, register]
+  rep_supported := by
+    intro q x x' hregs hmem hbound hr
+    rcases hr with ⟨hx, hLayout, hM⟩
+    have hf' : (memoryState (register 11) x).frontier ≤
+        (memoryState (register 11) x').frontier := by
+      have h := hregs (register 11) (by simp [program, register])
+      change x.regs (register 11) ≤ x'.regs (register 11)
+      omega
+    have hm' : ∀ a ∈ (frontLayout base C).footprint ∪ (rearLayout base C).footprint,
+        (memoryState (register 11) x').mem a = (memoryState (register 11) x).mem a := by
+      intro a ha
+      rw [layouts_footprint] at ha
+      exact hmem a ha
+    have hInv := MemoryQueueFrame.inv_congr (layouts_valid hf).1 (layouts_valid hf).2.1
+      (layouts_valid hf).2.2 hM.1 hm' hf'
+    have hAbs := MemoryQueueFrame.abs_congr (layouts_valid hf).1 (layouts_valid hf).2.1
+      (layouts_valid hf).2.2 hM.1 hm'
+    refine ⟨hbound, ?_, hInv, hAbs.trans hM.2⟩
+    intro i
+    exact (hregs _ (by
+      simp only [program]
+      apply decide_eq_false_iff_not.mpr
+      change ¬(8 ≤ i.val ∧ i.val < 11)
+      have := i.isLt
+      omega)).trans (hLayout i)
+  potential_supported := by
+    intro q x x' _ hmem _
+    have h := hmem (base + 1 + C) (by
+      simp only [Block.mem_footprint, Block.Owns, space]
+      omega)
+    rw [h]
+  clear_nodup := by simp [program, register]
+  params_not_clear j := by simp [program, register]
+  incCur_eval := by
+    intro x ho hfit
+    change x.regs (register 15) = 1 at ho
+    change Fits w (x.regs (register 13) + 1) at hfit
+    change (Op.exactBin .add (register 13) (register 13) (register 15)).eval w x =
+      some (x.set (register 13) (x.regs (register 13) + 1))
+    rw [Op.eval_exactBin, ho]
+    exact Data.put_of_fits hfit
+  span_exec := by
+    intro x hx hfront hparam
+    have hcap : x.regs (register 3) = C := hparam 0
+    obtain ⟨y, he, hm, _, hb, hfr, hc, _, _⟩ :=
+      MemoryQueueInit.span_exec register w base C x hx hfront hcap hf
+    exact ⟨y, he, hm, hb, hfr, fun _ => hc⟩
+  setup_exec := by
+    intro x hx hbase hfront hparam hzero
+    have hcap : x.regs (register 3) = C := hparam 0
+    obtain ⟨y, he, hm, hy, hLayout, hfr, _, _, _⟩ :=
+      MemoryQueueInit.setup_exec register w base C x hx hbase hcap hf
+    have hfrontY : y.regs (register 11) = base + space C := hfr.trans hfront
+    have hzeroY : ∀ a ∈ (Block.mk base (space C)).footprint, y.mem a = 0 := by
+      intro a ha
+      rw [hm]
+      exact hzero a ha
+    have hM := empty_rep hf (memoryState (register 11) y) hfrontY hzeroY
+    have hlayout : layoutMatch base C y.regs := by
+      intro i
+      rw [layoutWords_relative]
+      exact hLayout i
+    refine ⟨y, he, hfrontY, ⟨hy, hlayout, hM⟩, ?_, ?_⟩
+    · have hcount := hzeroY (base + 1 + C) (by
+        simp only [Block.mem_footprint, Block.Owns, space]
+        omega)
+      simp only [hcount, Nat.mul_zero, Nat.zero_le]
+    · intro a _
+      exact congrFun hm a
+
+/-- A framed native implementation of the bounded FIFO queue, with one globally selected code
+body for every runtime base, capacity and word width. Initialization uses the existing fresh
+zero-block contract; `initClear` has its explicit linear cost on dirty owned memory. -/
+@[no_expose] noncomputable def implementation (w base C : ℕ) (hf : Fits w (base + space C)) :
+    DataStructure.WordRAM.StateTransitionImpl program (Queue.WordRAM.spec w C)
+      w base (fun _ => C) [] := by
+  let M := semanticModule w base C hf
+  refine Realizes.toStateTransitionImplWithArgs M MemoryQueueMethod.realizes_method
+    (fun o => ((frontLayout base C, rearLayout base C), o)) ?_
+    (register 11) source scratch scratch_injective source_scratch scratch_frontier source_frontier
+    (baseCertificate w base C hf) rfl ?_ ?_ ?_ ?_ ?_
+  · intro o
+    rw [MemoryQueueMethod.method_source_eq _ w C]
+    change _ = (do
+      let a ← (Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+        (layouts_valid hf).2.2).methods o
+      pure (⟨o, a⟩ : (Queue.queue ℕ).Label))
+    rw [Queue.Memory.memRefinement_methods]
+  · intro q x o hr hv ha
+    change representation w base C hf q x at hr
+    refine ⟨?_, ?_, hr.2.2⟩
+    · funext i
+      refine Fin.addCases (motive := fun i => x.regs (source i) =
+        MemoryQueueMethod.methodWords ((frontLayout base C, rearLayout base C), o) i)
+        (fun j : Fin 8 => ?_) (fun j : Fin 3 => ?_) i
+      · have hidx : (Fin.castLE (by decide : 11 ≤ 16) (Fin.castAdd 3 j) : Fin 16) =
+            Fin.castLE (by decide : 8 ≤ 16) j := Fin.ext rfl
+        have hsrc : source (Fin.castAdd 3 j) = register (Fin.castLE (by decide) j) :=
+          congrArg register hidx
+        have hj := hr.2.1 j
+        rw [← hsrc] at hj
+        simpa [MemoryQueueMethod.methodWords, Fin.appendEquiv] using hj
+      · simpa [MemoryQueueMethod.methodWords, Fin.appendEquiv, source] using ha j
+    · apply method_safe (layouts_valid hf).1 (layouts_valid hf).2.1 (layouts_valid hf).2.2
+        (wellFormed_memoryState hr.1) hr.2.2.1 o
+      simpa only [hr.2.2.2] using hv
+  · intro o a regs hout
+    cases o with
+    | enqueue v => cases a; rfl
+    | dequeue =>
+      have htag := hout 2
+      have hval := hout 3
+      cases a with
+      | none =>
+        change regs (outputRegister 2) = 0 at htag
+        change some (if regs (outputRegister 2) = 0 then none else
+          some (regs (outputRegister 3))) = some none
+        rw [htag]
+        rfl
+      | some v =>
+        change regs (outputRegister 2) = 1 at htag
+        change regs (outputRegister 3) = v at hval
+        change some (if regs (outputRegister 2) = 0 then none else
+          some (regs (outputRegister 3))) = some (some v)
+        simp only [htag, hval, one_ne_zero, ↓reduceIte]
+  · intro q q' x y o a hr _ _ _ hM hy hframe
+    change representation w base C hf q x at hr
+    change representation w base C hf q' y
+    refine ⟨hy, ?_, hM⟩
+    intro i
+    have he := hframe (register (Fin.castLE (by decide) i)) (by
+      intro h
+      have := congrArg Fin.val h
+      change i.val = 11 at this
+      have := i.isLt
+      omega) (by
+        intro j h
+        have := congrArg Fin.val h
+        change 16 + j.val = i.val at this
+        have := i.isLt
+        omega)
+    exact he.trans (hr.2.1 i)
+  · intro q e o hr hv
+    change (Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+      (layouts_valid hf).2.2).toModule.rep q e at hr
+    have hv' : (Queue.WordRAM.spec w C).valid
+        ((Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+          (layouts_valid hf).2.2).abs e) o := by simpa only [hr.2] using hv
+    have h := MemoryQueueFrame.modifies_methods (layouts_valid hf).1 (layouts_valid hf).2.1
+      (layouts_valid hf).2.2 o hr.1 hv'
+    rw [layouts_footprint] at h
+    change Modifies (Block.mk base (space C)).footprint e.mem ((Memory.spec w).clientState e
+      ((Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+        (layouts_valid hf).2.2).methods o)).mem
+    rw [Queue.Memory.memRefinement_methods]
+    exact h.1
+  · intro q q' x y o a hr hv _ _ _ hm _
+    change representation w base C hf q x at hr
+    have hv' : (Queue.WordRAM.spec w C).valid
+        ((Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+          (layouts_valid hf).2.2).abs (memoryState (register 11) x)) o := by
+      simpa only [hr.2.2.2] using hv
+    have hp := method_pay (layouts_valid hf).1 (layouts_valid hf).2.1 (layouts_valid hf).2.2
+      (wellFormed_memoryState hr.1) hr.2.2.1 o hv' MemoryQueueMethod.realizes_method.factor
+    have hs : (Memory.spec 0).clientState (memoryState (register 11) x)
+        (MemoryQueueMethod.method ((frontLayout base C, rearLayout base C), o)) =
+        memoryState (register 11) y := by
+      have hw' := (clientState_width w
+        (MemoryQueueMethod.method ((frontLayout base C, rearLayout base C), o))
+        (memoryState (register 11) x)).symm
+      apply hw'.trans
+      rw [MemoryQueueMethod.method_source_eq _ w C]
+      change (Memory.spec w).clientState (memoryState (register 11) x)
+        ((Queue.Memory.memMethods (frontLayout base C) (rearLayout base C) w C o).bind _) = _
+      have htag : (Memory.spec w).clientState (memoryState (register 11) x)
+          ((Queue.Memory.memMethods (frontLayout base C) (rearLayout base C) w C o).bind
+            (fun a => pure (⟨o, a⟩ : (Queue.queue ℕ).Label))) =
+          (Memory.spec w).clientState (memoryState (register 11) x)
+            (Queue.Memory.memMethods (frontLayout base C) (rearLayout base C) w C o) := by
+        simp only [StateTransitionSpec.clientState, StateTransitionSpec.runClient_bind]
+        rfl
+      rw [htag]
+      change _ = (memoryState (register 11) y)
+      change memoryState (register 11) y = (Memory.spec w).clientState
+        (memoryState (register 11) x) ((Queue.Memory.memRefinement (layouts_valid hf).1
+          (layouts_valid hf).2.1 (layouts_valid hf).2.2).methods o) at hm
+      rw [Queue.Memory.memRefinement_methods] at hm
+      exact hm.symm
+    rw [hs] at hp
+    exact hp
+
+private theorem implementation_data (w base C : ℕ) (hf : Fits w (base + space C)) :
+    (implementation w base C hf).space = space C ∧
+    (implementation w base C hf).initTime = 13 ∧
+    (implementation w base C hf).initPotential = 0 ∧
+    (∀ q o, (implementation w base C hf).charge q o =
+      153 * MemoryQueueMethod.realizes_method.factor) ∧
+    (∀ x, (implementation w base C hf).potential x =
+      48 * MemoryQueueMethod.realizes_method.factor * x.mem (base + 1 + C)) ∧
+    (∀ v regs, (implementation w base C hf).decode (.enqueue v) regs = some ()) ∧
+    (∀ regs, (implementation w base C hf).decode .dequeue regs =
+      some (if regs (outputRegister 2) = 0 then none else some (regs (outputRegister 3)))) :=
+  ⟨rfl, rfl, rfl, fun _ _ => rfl, fun _ => rfl, fun _ _ => rfl, fun _ => rfl⟩
+
+@[simp] theorem implementation_space (w base C : ℕ) (hf : Fits w (base + space C)) :
+    (implementation w base C hf).space = space C := (implementation_data w base C hf).1
+
+@[simp] theorem implementation_initTime (w base C : ℕ) (hf : Fits w (base + space C)) :
+    (implementation w base C hf).initTime = 13 := (implementation_data w base C hf).2.1
+
+@[simp] theorem implementation_initPotential (w base C : ℕ) (hf : Fits w (base + space C)) :
+    (implementation w base C hf).initPotential = 0 := (implementation_data w base C hf).2.2.1
+
+@[simp] theorem implementation_charge (w base C : ℕ) (hf : Fits w (base + space C))
+    (q : List ℕ) (o : Queue.QueueOp ℕ) :
+    (implementation w base C hf).charge q o = 153 * MemoryQueueMethod.realizes_method.factor :=
+  (implementation_data w base C hf).2.2.2.1 q o
+
+@[simp] theorem implementation_potential (w base C : ℕ) (hf : Fits w (base + space C))
+    (x : Data registers) :
+    (implementation w base C hf).potential x =
+      48 * MemoryQueueMethod.realizes_method.factor * x.mem (base + 1 + C) :=
+  (implementation_data w base C hf).2.2.2.2.1 x
+
+/-- The local native representation is the original semantic queue representation plus bounded
+native data and the persistent layout ABI. It does not equate globally different memories. -/
+theorem implementation_rep_iff (w base C : ℕ) (hf : Fits w (base + space C))
+    (q : List ℕ) (x : Data registers) :
+    (implementation w base C hf).rep q x ↔
+      x.Bounded w ∧
+        (∀ i : Fin 8, x.regs (register (Fin.castLE (by decide) i)) =
+          MemoryQueue.layoutWords (frontLayout base C, rearLayout base C) i) ∧
+        (Queue.Memory.memRefinement (layouts_valid hf).1 (layouts_valid hf).2.1
+          (layouts_valid hf).2.2).toModule.rep q (memoryState (register 11) x) := Iff.rfl
+
+@[simp] theorem implementation_decode_enqueue (w base C : ℕ) (hf : Fits w (base + space C))
+    (v : ℕ) (regs : Fin registers → ℕ) :
+    (implementation w base C hf).decode (.enqueue v) regs = some () :=
+  (implementation_data w base C hf).2.2.2.2.2.1 v regs
+
+@[simp] theorem implementation_decode_dequeue (w base C : ℕ) (hf : Fits w (base + space C))
+    (regs : Fin registers → ℕ) :
+    (implementation w base C hf).decode .dequeue regs =
+      some (if regs (outputRegister 2) = 0 then none else some (regs (outputRegister 3))) :=
+  (implementation_data w base C hf).2.2.2.2.2.2 regs
+
+end Cslib.WordRAM.Realization.MemoryQueueAdapter
diff --git a/ComplexityTests/WordRAMRealizationQueueAdapter.lean b/ComplexityTests/WordRAMRealizationQueueAdapter.lean
new file mode 100644
index 0000000000..d1168eb180
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationQueueAdapter.lean
@@ -0,0 +1,186 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueAdapter
+
+/-!
+The framed queue is initialized after a nonempty five-cell prefix. Its actual flat programs
+execute two enqueues and a transfer-triggering dequeue, including each operation's trailing
+halt. Register argument delivery follows the existing `prepareRegs` ABI and is outside this
+clock. The fresh owned block is zero; the separate literal M1a allocation path may keep dirty
+unused item cells and is not replaced by this initializer.
+-/
+
+namespace ComplexityTests.WordRAMRealizationQueueAdapter
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+open Cslib.WordRAM.Realization.MemoryQueueAdapter
+
+private abbrev spec := Queue.WordRAM.spec 4 2
+private def ops : List spec.Op := [.enqueue 7, .enqueue 15, .dequeue]
+private def expected : spec.Transcript :=
+  [⟨.enqueue 7, (), [7]⟩, ⟨.enqueue 15, (), [7, 15]⟩, ⟨.dequeue, some 7, [15]⟩]
+
+private noncomputable def fresh (C : ℕ) : Data registers where
+  regs i := if i = register 3 then C else if i = register 11 then 5 else 0
+  mem a := if a < 5 then 7 else if a < 11 then 0 else 9
+
+private theorem valid : spec.ValidOpSeq [] ops := by
+  apply (spec.validOpSeq_iff_validHistory [] ops).mpr
+  change (0 < 2 ∧ Fits 4 7) ∧ (1 < 2 ∧ Fits 4 15) ∧ True ∧ True
+  norm_num [Fits]
+
+private theorem runsOps_modifies {capacity : ℕ}
+    {C : DataStructure.WordRAM.StateTransitionImpl program (Queue.WordRAM.spec 4 capacity)
+      4 5 (fun _ => capacity) []}
+    {q q' : (Queue.WordRAM.spec 4 capacity).State} {x y : Data registers} {os tr t}
+    (h : C.RunsOps C.prepareRegs q x os tr q' y t) :
+    Modifies (Block.mk 5 C.space).footprint x.mem y.mem := by
+  induction h with
+  | nil => exact Modifies.refl _ _
+  | cons _ _ _ _ hm _ ih => exact fun a ha => (ih a ha).trans (hm a ha)
+
+-- The concrete framed target is inhabited and its flat native FIFO trace has the right answer.
+example :
+    let I := implementation 4 5 2 (by norm_num [space, Fits])
+    ∃ pc x₀ t_init z t_ops,
+      Runs 4 program.initFreshProg ⟨0, fresh 2⟩ ⟨pc, x₀⟩ t_init ∧
+      (∃ out, step 4 program.initFreshProg ⟨pc, x₀⟩ = .halt out) ∧
+      I.RunsOps I.prepareRegs [] x₀ ops expected [15] z t_ops ∧
+      I.rep [15] z ∧ z.mem 100 = 9 ∧ z.mem 0 = 7 ∧ t_init ≤ 13 ∧
+      t_ops ≤ 3 * (153 * MemoryQueueMethod.realizes_method.factor + 1) := by
+  let I := implementation 4 5 2 (by norm_num [space, Fits])
+  have hb : (fresh 2).Bounded 4 := by
+    constructor
+    · intro i
+      change Fits 4 (if i = register 3 then 2 else if i = register 11 then 5 else 0)
+      split_ifs <;> norm_num [Fits]
+    · intro a
+      change Fits 4 (if a < 5 then 7 else if a < 11 then 0 else 9)
+      split_ifs <;> norm_num [Fits]
+  have hfr : (fresh 2).regs program.frontierReg = 5 := by simp [fresh, program, register]
+  have hpar : ∀ j, (fresh 2).regs (program.initParams j) = (2 : ℕ) := by
+    intro j
+    simp [fresh, program]
+  have hspace : I.space = space 2 := implementation_space 4 5 2 _
+  have hz : ∀ a ∈ (Block.mk 5 I.space).footprint, (fresh 2).mem a = 0 := by
+    intro a ha
+    rw [hspace] at ha
+    simp only [Block.mem_footprint, Block.Owns, space] at ha
+    simp [fresh, show ¬a < 5 by omega, show a < 11 by omega]
+  obtain ⟨pc, x₀, ti, tr, q, z, nativeSteps, hri, hhalt, hm, hro, hops, htr, hr, hti, hto⟩ :=
+    I.run_ops_exact_fresh hb hfr hpar hz ops valid
+  have hcanonical := (spec.validTranscript_iff_run [] tr q).mp htr
+  rw [hops] at hcanonical
+  have hq : q = [15] := hcanonical.2.1
+  have ht : tr = expected := hcanonical.2.2
+  subst q
+  subst tr
+  have hOutside : 100 ∉ (Block.mk 5 I.space).footprint := by
+    rw [hspace]
+    norm_num [Block.mem_footprint, Block.Owns, space]
+  have hmem := (runsOps_modifies (capacity := 2) hro) 100 hOutside
+  have hinitmem := hm 100 hOutside
+  have hfinal : z.mem 100 = 9 := hmem.trans (hinitmem.trans (by rfl))
+  have hPrefixOutside : 0 ∉ (Block.mk 5 I.space).footprint := by
+    simp [Block.mem_footprint, Block.Owns]
+  have hprefix : z.mem 0 = 7 := ((runsOps_modifies (capacity := 2) hro) 0 hPrefixOutside).trans
+    ((hm 0 hPrefixOutside).trans (by rfl))
+  have htime : nativeSteps ≤ 3 * (153 * MemoryQueueMethod.realizes_method.factor + 1) := by
+    have hbound := hto
+    have hc : ∀ q o, I.charge q o = 153 * MemoryQueueMethod.realizes_method.factor :=
+      fun q o => implementation_charge 4 5 2 _ q o
+    have hp : I.initPotential = 0 := implementation_initPotential 4 5 2 _
+    simp only [hc, hp, StateTransitionSpec.totalCostTranscript_const] at hbound
+    change nativeSteps + _ ≤ 3 * (153 * MemoryQueueMethod.realizes_method.factor + 1) + 0 at hbound
+    omega
+  have hiTime : I.initTime = 13 := implementation_initTime 4 5 2 _
+  rw [hiTime] at hti
+  exact ⟨pc, x₀, ti, z, nativeSteps, hri, hhalt, hro, hr, hfinal, hprefix, hti, htime⟩
+
+-- Capacity zero uses the SAME program and initializes a valid empty queue at a nonzero base.
+-- An empty dequeue returns none through an actual flat call, with no transfer iterations.
+example :
+    let I := implementation 4 5 0 (by norm_num [space, Fits])
+    ∃ pc x₀ ti z t,
+      Runs 4 program.initFreshProg ⟨0, fresh 0⟩ ⟨pc, x₀⟩ ti ∧
+      I.RunsOps I.prepareRegs [] x₀ [.dequeue] [⟨.dequeue, none, []⟩] [] z t ∧
+      I.rep [] z ∧ z.mem 100 = 9 ∧ ti ≤ 13 ∧
+      t ≤ 153 * MemoryQueueMethod.realizes_method.factor + 1 := by
+  let I := implementation 4 5 0 (by norm_num [space, Fits])
+  have hb : (fresh 0).Bounded 4 := by
+    constructor
+    · intro i
+      change Fits 4 (if i = register 3 then 0 else if i = register 11 then 5 else 0)
+      split_ifs <;> norm_num [Fits]
+    · intro a
+      change Fits 4 (if a < 5 then 7 else if a < 11 then 0 else 9)
+      split_ifs <;> norm_num [Fits]
+  have hfr : (fresh 0).regs program.frontierReg = 5 := by simp [fresh, program, register]
+  have hpar : ∀ j, (fresh 0).regs (program.initParams j) = (0 : ℕ) := by
+    intro j
+    simp [fresh, program]
+  have hspace : I.space = space 0 := implementation_space 4 5 0 _
+  have hz : ∀ a ∈ (Block.mk 5 I.space).footprint, (fresh 0).mem a = 0 := by
+    intro a ha
+    rw [hspace] at ha
+    simp only [Block.mem_footprint, Block.Owns, space] at ha
+    simp [fresh, show ¬a < 5 by omega, show a < 11 by omega]
+  have hv : (Queue.WordRAM.spec 4 0).ValidOpSeq [] [.dequeue] := by
+    apply ((Queue.WordRAM.spec 4 0).validOpSeq_iff_validHistory [] [.dequeue]).mpr
+    exact ⟨trivial, trivial⟩
+  obtain ⟨pc, x₀, ti, tr, q, z, t, hri, _, hm, hro, hops, htr, hr, hti, hto⟩ :=
+    I.run_ops_exact_fresh hb hfr hpar hz [.dequeue] hv
+  have hcanonical := ((Queue.WordRAM.spec 4 0).validTranscript_iff_run [] tr q).mp htr
+  rw [hops] at hcanonical
+  have hq : q = [] := hcanonical.2.1
+  have ht : tr = [⟨.dequeue, none, []⟩] := hcanonical.2.2
+  subst q
+  subst tr
+  have hOutside : 100 ∉ (Block.mk 5 I.space).footprint := by
+    rw [hspace]
+    norm_num [Block.mem_footprint, Block.Owns, space]
+  have hfinal : z.mem 100 = 9 := ((runsOps_modifies (capacity := 0) hro) 100 hOutside).trans
+    ((hm 100 hOutside).trans (by rfl))
+  have htime : t ≤ 153 * MemoryQueueMethod.realizes_method.factor + 1 := by
+    have hc : ∀ q o, I.charge q o = 153 * MemoryQueueMethod.realizes_method.factor :=
+      fun q o => implementation_charge 4 5 0 _ q o
+    have hp : I.initPotential = 0 := implementation_initPotential 4 5 0 _
+    simp only [hc, hp, StateTransitionSpec.totalCostTranscript_const] at hto
+    change t + _ ≤ 1 * (153 * MemoryQueueMethod.realizes_method.factor + 1) + 0 at hto
+    omega
+  have hiTime : I.initTime = 13 := implementation_initTime 4 5 0 _
+  rw [hiTime] at hti
+  exact ⟨pc, x₀, ti, z, t, hri, hro, hr, hfinal, hti, htime⟩
+
+-- The existing dirty-clear API has a LINEAR initialization allowance. It inhabits the local
+-- framed target and preserves unowned memory; it is separate from literal source allocLayout.
+example :
+    let I := implementation 4 5 2 (by norm_num [space, Fits])
+    ∃ y, ExecWithin 4 program.initClear (⟨(fresh 2).regs, fun _ => 7⟩ : Data registers) y 43 ∧
+      I.rep [] y ∧ y.mem 100 = 7 := by
+  let I := implementation 4 5 2 (by norm_num [space, Fits])
+  let x : Data registers := ⟨(fresh 2).regs, fun _ => 7⟩
+  have hb : x.Bounded 4 := by
+    constructor
+    · intro i
+      change Fits 4 (if i = register 3 then 2 else if i = register 11 then 5 else 0)
+      split_ifs <;> norm_num [Fits]
+    · exact fun _ => by norm_num [Fits]
+  have hfr : x.regs program.frontierReg = 5 := by simp [x, fresh, program, register]
+  have hpar : ∀ j, x.regs (program.initParams j) = (2 : ℕ) := by
+    intro j
+    simp [x, fresh, program]
+  obtain ⟨y, he, _, hr, _, hm⟩ := I.initClear_exec hb hfr hpar
+  have hs : I.space = space 2 := implementation_space 4 5 2 _
+  have ht : I.initTime = 13 := implementation_initTime 4 5 2 _
+  rw [hs, ht] at he
+  have hout : 100 ∉ (Block.mk 5 I.space).footprint := by
+    rw [hs]
+    norm_num [space, Block.mem_footprint, Block.Owns]
+  exact ⟨y, he, hr, hm 100 hout⟩
+
+end ComplexityTests.WordRAMRealizationQueueAdapter
diff --git a/ROADMAP.md b/ROADMAP.md
index b1fd6b8378..28b510c423 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -646,8 +646,10 @@ reusing graph and matroid foundations and the shared data-structure interfaces.
   queue transfer and dequeue dispatch also have native certificates; bounded transfer charges
   inactive iterations after early stop, and valid transfer fuel has memory cost 6*n and local
   work 40*n+1. One typed method emitter handles both operations before runtime layouts and
-  widths; register setup and footprint lemmas support the local-ADT boundary. Remaining: the
-  complete framed queue and faithful allocation/native-client path.
+  widths; register setup and footprint lemmas support the local-ADT boundary. The complete
+  framed queue certificate has explicit runtime-base/capacity fit, finite locality, fresh
+  initialization and an amortized native-body charge. Its linear dirty clear is separate from
+  faithful source allocation. Remaining: the faithful allocation/native-client path.
   The full C2/M1b objective remains open; arbitrary host continuations do not acquire runtime bounds.
 - **Stateful algorithms and data structures:** Word-RAM controllers for larger adaptive and
   iterative clients, including the two-stack queue and timeline-editing controllers; reusable
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 0db2fd5000..43a776549c 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -536,8 +536,14 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   the span and install layouts at an arbitrary runtime base without changing memory. Queue-method
   footprint and representation-congruence lemmas reuse the existing memory methods and `Modifies`.
   These support the framed boundary; they do not replace storage initialization or faithful source
-  allocation. The full framed queue/faithful allocation client remains separate. No abstract
-  headline is added.
+  allocation. The complete framed queue instantiates the existing local certificate, with one
+  program before runtime base/capacity/width and space `2*(C+1)`. Its actual work envelope
+  `G <= 7*M+80` scales the original memory potential to `48*factor*rearCount` and amortized
+  native-body charge `153*factor`; each flat call's halt is separate. Fresh initialization costs
+  13 body instructions under the zero-block premise; dirty clearing costs `4*space+19` and can
+  change unused item cells. Delivered arguments follow the existing calling convention. Faithful
+  source allocation and a complete allocated-client clock remain separate. No abstract headline
+  or legacy size/space/step improvement is claimed.
   `DataStructure/OrderedSet` and `DataStructure/OrderedSet/*` provide neutral
   optional-minimum contracts, a typed finite-set interface including deletion, and adaptive
   minimum extraction, with no tree or cost dependency. Bounded-key implementations may specialize

From 31e0718a92528725a0fb419363e8e7b7e8746b85 Mon Sep 17 00:00:00 2001
From: Samuel Giuseppe Schlesinger <sgschlesinger@gmail.com>
Date: Sun, 1 Nov 2026 20:46:38 -0500
Subject: [PATCH 2/2] refactor(WordRAM): reuse source queue layout helpers

Use definitionally equal frontier specializations of existing M1a layouts and remove redundant simp arguments. All statements and native code are preserved. Delegated Codex authoring by mathlib_cache_retry_1730; integration/self-review by roadmap_algorithms. Integrated strict focused native tests and hygiene pass. Original full six at addb04 is retained; corrected frozen head receives full validation before publication. No selected abstract impact.
---
 .../Client/MemoryQueueAdapter.lean            | 23 ++++++++++---------
 1 file changed, 12 insertions(+), 11 deletions(-)

diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
index 6bcfac178b..dc4f7d795b 100644
--- a/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAdapter.lean
@@ -66,12 +66,13 @@ namespace Cslib.WordRAM.Realization.MemoryQueueAdapter
 
 open Cslib.DataStructure
 
-/-- The front count cell and item array, relative to the queue's runtime base. -/
-def frontLayout (base C : ℕ) : Stack.Memory.Layout := ⟨⟨base, 1⟩, ⟨base + 1, C⟩⟩
+/-- The existing front layout specialized to a runtime base. Only its frontier argument is read. -/
+abbrev frontLayout (base C : ℕ) : Stack.Memory.Layout :=
+  Queue.Memory.frontLayout (⟨fun _ => 0, base⟩ : Memory.State) C
 
-/-- The rear follows the complete front layout. -/
-def rearLayout (base C : ℕ) : Stack.Memory.Layout :=
-  ⟨⟨base + 1 + C, 1⟩, ⟨base + 1 + C + 1, C⟩⟩
+/-- The existing rear layout specialized to the same runtime base. -/
+abbrev rearLayout (base C : ℕ) : Stack.Memory.Layout :=
+  Queue.Memory.rearLayout (⟨fun _ => 0, base⟩ : Memory.State) C
 
 /-- The two count cells and two capacity-sized arrays. -/
 def space (C : ℕ) : ℕ := 2 * (C + 1)
@@ -82,11 +83,11 @@ theorem layouts_valid {w base C : ℕ} (hf : Fits w (base + space C)) :
       Disjoint (frontLayout base C).footprint (rearLayout base C).footprint := by
   have hC : Fits w C := hf.of_le (by unfold space; omega)
   refine ⟨⟨rfl, ?_, rfl, hC⟩, ⟨rfl, ?_, rfl, hC⟩, ?_⟩
-  · simp [frontLayout, Block.Owns]
-  · simp [rearLayout, Block.Owns]
+  · simp [Block.Owns]
+  · simp [Block.Owns]
   · rw [Finset.disjoint_left]
     intro a ha hb
-    simp only [Stack.Memory.Layout.footprint, frontLayout, rearLayout, Finset.mem_union,
+    simp only [Stack.Memory.Layout.footprint, Finset.mem_union,
       Block.mem_footprint, Block.Owns] at ha hb
     omega
 
@@ -95,7 +96,7 @@ theorem layouts_footprint (base C : ℕ) :
     (frontLayout base C).footprint ∪ (rearLayout base C).footprint =
       (Block.mk base (space C)).footprint := by
   ext a
-  simp only [Stack.Memory.Layout.footprint, frontLayout, rearLayout, Finset.mem_union,
+  simp only [Stack.Memory.Layout.footprint, Finset.mem_union,
     Block.mem_footprint, Block.Owns, space]
   omega
 
@@ -139,9 +140,9 @@ theorem empty_rep {w base C : ℕ} (hf : Fits w (base + space C)) (e : Memory.St
       rw [h₁]
       exact Nat.zero_le C
   have ha₀ : Stack.Memory.abs (frontLayout base C) e = [] := by
-    simp only [Stack.Memory.abs, frontLayout, h₀, Block.entries_zero, List.reverse_nil]
+    simp only [Stack.Memory.abs, h₀, Block.entries_zero, List.reverse_nil]
   have ha₁ : Stack.Memory.abs (rearLayout base C) e = [] := by
-    simp only [Stack.Memory.abs, rearLayout, h₁, Block.entries_zero, List.reverse_nil]
+    simp only [Stack.Memory.abs, h₁, Block.entries_zero, List.reverse_nil]
   change ((Stack.Memory.Inv (frontLayout base C) e ∧
     Stack.Memory.Inv (rearLayout base C) e) ∧
     Queue.Memory.Inv w C (Queue.WordRAM.contents