diff --git a/Complexity.lean b/Complexity.lean
index 91cb87a947..0b056bcb02 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2561,6 +2561,7 @@ 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.MemoryQueueAllocation
 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/MemoryQueueAllocation.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAllocation.lean
new file mode 100644
index 0000000000..18ecd9da44
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryQueueAllocation.lean
@@ -0,0 +1,375 @@
+/-
+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.MemoryQueueDispatch
+public import Complexity.Computability.WordRAM.Realization.Client.MemoryQueueAdapter
+public import Complexity.Computability.WordRAM.Realization.Program
+
+/-!
+# Faithful allocation for the memory-oracle queue
+
+The existing initializer zeroes each one-cell count and allocates each item array dirty. The
+certificates preserve this literal whole-memory behavior, without clearing the item arrays or
+replacing the initial memory. Code precedes the runtime capacity, frontier and allocation replies.
+
+## Main definitions
+
+* `allocPair`: exactly the two allocation calls that prefix `Queue.Memory.run`.
+* `roundTrip`: the supported concrete enqueue/dequeue client.
+
+## Main results
+
+* `realizes_allocLayout`, `realizes_allocPair`: certified initialization with constant local work.
+* `run_eq_allocPair_bind`: the prefix is the one used by the actual M1a queue run.
+* `realizes_roundTrip`, `roundTrip_correct_source`: uniform realization and the actual source
+  answer, with all fits and the physical word width explicit.
+
+The existing flat-program projections apply to these certificates. Their `Data.init` input
+prefix is charged separately and starts with zero future cells; it is distinct from the body
+ABI on arbitrary bounded old memory, which can retain dirty item words such as seven.
+
+## References
+
+This is original realization infrastructure for the existing `Stack.Memory` and `Queue.Memory`
+programs. Their source-algorithm citations and credit remain in those modules.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.MemoryQueueAllocation
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+private theorem copyResult {δ α : Type} {k l : ℕ} (input : δ ↪ (Fin k → ℕ))
+    (output : α ↪ (Fin l → ℕ)) (f : δ → α) (ix : Fin l → Fin k)
+    (hf : ∀ d i, output (f d) i = input d (ix i)) :
+    Realizes .exact (fun d => pure (f d)) input output
+      (fun _ _ _ => True) (fun _ _ => 2 * l) := by
+  have h := Realizes.glueVector (B := .exact) input output f
+    (fun i v => v (ix i)) (fun i v => v (ix i)) (fun _ => 1) hf
+    (P := fun _ => True) (fun i => GlueComputes.proj (ix i) (fun _ _ => le_rfl))
+  exact h.consequence (fun _ _ _ hwords _ _ => ⟨trivial, fun i => hwords (ix i)⟩)
+    (fun _ _ => by simp [two_mul])
+
+/-- Exactly the allocation prefix of the existing queue run: only the two one-cell count
+fields are cleared. Both item arrays retain their old contents. -/
+def allocPair (C : ℕ) : Memory.Prog (Stack.Memory.Layout × Stack.Memory.Layout) := do
+  let front ← Stack.Memory.allocLayout C
+  let rear ← Stack.Memory.allocLayout C
+  pure (front, rear)
+
+/-- The named prefix changes no source method or client. -/
+theorem run_eq_allocPair_bind (w C : ℕ) {α : Type}
+    (p : (Queue.WordRAM.spec w C).Client α) :
+    Queue.Memory.run w C p = (allocPair C).bind
+      (fun L => link (Queue.Memory.memMethods L.1 L.2 w C) p) := by
+  simp only [Queue.Memory.run, allocPair, PFunctor.FreeM.bind_eq_bind, bind_assoc, pure_bind]
+
+/-- The source prefix returns the actual allocation addresses and retains the full dirty memory. -/
+theorem runClient_allocPair (w C : ℕ) (s : Memory.State) :
+    (Memory.spec w).runClient s (allocPair C) =
+      ((Queue.Memory.frontLayout s C, Queue.Memory.rearLayout s C), Queue.Memory.allocated s C,
+        [.alloc 1, .allocDirty C, .alloc 1, .allocDirty C]) := rfl
+
+/-- The exact single-stack initializer has fixed code before capacity, frontier or replies.
+The staged one and all four returned layout coordinates are charged. -/
+theorem realizes_allocLayout :
+    Realizes .exact Stack.Memory.allocLayout (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+      MemoryStack.layoutWords (fun w C s => Fits w (s.frontier + 1 + C)) (fun _ _ => 12) := by
+  let e₁ := appendWords word word
+  let e₂ := appendWords e₁ word
+  let e₃ := appendWords e₂ word
+  have hone := Realizes.glue word
+    (GlueComputes.const (B := .exact) (P := fun _ => True) (bound := fun _ => 1)
+      1 (fun _ _ => le_rfl))
+  have hcount := Realizes.alloc e₁ 1
+  have hitems := Realizes.allocDirty e₂ 0
+  have hreturn := copyResult e₃ MemoryStack.layoutWords
+    (fun d : ((ℕ × ℕ) × ℕ) × ℕ =>
+      (⟨⟨d.1.2, d.1.1.2⟩, ⟨d.2, d.1.1.1⟩⟩ : Stack.Memory.Layout))
+    ![2, 1, 3, 0] (by intro d i; fin_cases i <;> rfl)
+  have h := hone.bind (hcount.bind (hitems.bind hreturn))
+  have hp : (fun C : ℕ => (pure 1 : Memory.Prog ℕ).bind (fun one =>
+      (Memory.alloc one).bind (fun count => (Memory.allocDirty C).bind (fun items =>
+        pure (⟨⟨count, one⟩, ⟨items, C⟩⟩ : Stack.Memory.Layout))))) = Stack.Memory.allocLayout := by
+    funext C
+    simp only [Stack.Memory.allocLayout, Memory.allocBlock, Memory.allocBlockDirty,
+      PFunctor.FreeM.bind_eq_bind, bind_assoc, pure_bind]
+  simp only [PFunctor.FreeM.bind_eq_bind, pure_bind] at hp h
+  change Realizes .exact (fun C : ℕ => (Memory.alloc 1).bind (fun count =>
+    (Memory.allocDirty C).bind (fun items =>
+      pure (⟨⟨count, 1⟩, ⟨items, C⟩⟩ : Stack.Memory.Layout)))) word MemoryStack.layoutWords _ _ at h
+  simp only [PFunctor.FreeM.bind_eq_bind] at h
+  rw [hp] at h
+  apply h.consequence (hwork := fun _ _ => le_rfl)
+  intro w C s _ _ hf
+  exact ⟨⟨trivial, hf.of_le (by omega)⟩, trivial, trivial, trivial⟩
+
+/-- The actual two-stack prefix has six memory units and 42 explicitly certified local units,
+independent of the item capacity. No item cell is cleared by this initialization. -/
+theorem realizes_allocPair :
+    Realizes .exact allocPair (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding MemoryQueue.layoutWords
+      (fun w C s => Fits w (s.frontier + 2 * (C + 1))) (fun _ _ => 42) := by
+  let e₁ := appendWords word MemoryStack.layoutWords
+  let e₂ := appendWords e₁ MemoryStack.layoutWords
+  have hsecond := realizes_allocLayout.reindex (fun d : ℕ × Stack.Memory.Layout => d.1)
+    e₁ ![0] (by intro d i; fin_cases i; rfl)
+  have hreturn := copyResult e₂ MemoryQueue.layoutWords
+    (fun d : (ℕ × Stack.Memory.Layout) × Stack.Memory.Layout => (d.1.2, d.2))
+    ![1, 2, 3, 4, 5, 6, 7, 8] (by intro d i; fin_cases i <;> rfl)
+  apply (realizes_allocLayout.bind (hsecond.bind hreturn)).consequence
+    (hwork := fun _ _ => le_rfl)
+  intro w C s _ _ hf
+  change Fits w (s.frontier + 1 + C) ∧
+    Fits w (s.frontier + 1 + C + 1 + C) ∧ True
+  refine ⟨hf.of_le (by omega), ?_, trivial⟩
+  convert hf using 1; omega
+
+/-- This initialization's actual memory charge is constant; it does not clear `C` item cells. -/
+theorem allocPair_memoryCost (C : ℕ) (s : Memory.State) : memoryCost (allocPair C) s = 6 := rfl
+
+/-- The end-fit condition makes every operation of the exact allocation prefix admissible. -/
+theorem valid_allocPair {w C : ℕ} {s : Memory.State}
+    (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (allocPair C)) := by
+  change Fits w (s.frontier + 1) ∧ Fits w (s.frontier + 1 + C) ∧
+    Fits w (s.frontier + 1 + C + 1) ∧ Fits w (s.frontier + 1 + C + 1 + C) ∧ True
+  exact ⟨hf.of_le (by omega), hf.of_le (by omega), hf.of_le (by omega),
+    hf.of_le (by omega), trivial⟩
+
+private theorem allocated_counts (C : ℕ) (s : Memory.State) :
+    (Queue.Memory.allocated s C).mem (Queue.Memory.frontLayout s C).count.base = 0 ∧
+    (Queue.Memory.allocated s C).mem (Queue.Memory.rearLayout s C).count.base = 0 := by
+  constructor
+  · change clear (clear s.mem s.frontier 1) (s.frontier + 1 + C) 1 s.frontier = 0
+    rw [clear_of_not_owns (by simp only [Block.Owns]; omega)]
+    apply clear_of_owns
+    change s.frontier ≤ s.frontier ∧ s.frontier < s.frontier + 1
+    omega
+  · apply clear_of_owns
+    change s.frontier + 1 + C ≤ s.frontier + 1 + C ∧
+      s.frontier + 1 + C < s.frontier + 1 + C + 1
+    omega
+
+private theorem allocated_invariants (C : ℕ) (s : Memory.State) :
+    Stack.Memory.Inv (Queue.Memory.frontLayout s C) (Queue.Memory.allocated s C) ∧
+      Stack.Memory.Inv (Queue.Memory.rearLayout s C) (Queue.Memory.allocated s C) := by
+  obtain ⟨hF, hR⟩ := allocated_counts C s
+  constructor
+  · refine ⟨?_, ?_, ?_⟩
+    · change s.frontier + 1 ≤ s.frontier + 1 + C + 1 + C; omega
+    · change s.frontier + 1 + C ≤ s.frontier + 1 + C + 1 + C; omega
+    · rw [hF]; exact Nat.zero_le _
+  · refine ⟨?_, ?_, ?_⟩
+    · change s.frontier + 1 + C + 1 ≤ s.frontier + 1 + C + 1 + C; omega
+    · exact le_rfl
+    · rw [hR]; exact Nat.zero_le _
+
+private theorem wellFormed_client {w : ℕ} {α : Type} {s : Memory.State}
+    (hw : Memory.WellFormed w s) (p : Memory.Prog α)
+    (hv : (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s p)) :
+    Memory.WellFormed w ((Memory.spec 0).clientState s p) := by
+  have h := hw.run hv
+  rw [StateTransitionSpec.run_runClient, clientState_width] at h
+  exact h
+
+private theorem allocated_wellFormed {w C : ℕ} {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    Memory.WellFormed w (Queue.Memory.allocated s C) := by
+  simpa only [StateTransitionSpec.clientState, runClient_allocPair] using
+    wellFormed_client hw (allocPair C) (valid_allocPair hf)
+
+/-- The concrete supported client; no certificate for an arbitrary opaque client is assumed. -/
+def roundTrip (w C v : ℕ) : (Queue.WordRAM.spec w C).Client (Option ℕ) := do
+  let _ ← PFunctor.FreeM.lift (P := (Queue.WordRAM.spec w C).signature) (Queue.QueueOp.enqueue v)
+  PFunctor.FreeM.lift (P := (Queue.WordRAM.spec w C).signature) Queue.QueueOp.dequeue
+
+/-- Both runtime argument words are faithfully retained. -/
+def roundTripWords : (ℕ × ℕ) ↪ (Fin 2 → ℕ) :=
+  ((Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding.prodMap
+    (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans (Fin.appendEquiv 1 1).toEmbedding
+
+private def enqueued (C v : ℕ) (s : Memory.State) : Memory.State :=
+  (Memory.spec 0).clientState (Queue.Memory.allocated s C)
+    (Stack.Memory.push (Queue.Memory.rearLayout s C) v)
+
+private theorem enqueued_counts (C v : ℕ) (s : Memory.State) :
+    (enqueued C v s).mem (Queue.Memory.frontLayout s C).count.base = 0 ∧
+      (enqueued C v s).mem (Queue.Memory.rearLayout s C).count.base = 1 := by
+  obtain ⟨hF, hR⟩ := allocated_counts C s
+  let m := clear (clear s.mem s.frontier 1) (s.frontier + 1 + C) 1
+  change m s.frontier = 0 at hF
+  change m (s.frontier + 1 + C) = 0 at hR
+  simp only [enqueued, StateTransitionSpec.clientState, Stack.Memory.runClient_push]
+  constructor
+  · change Function.update
+      (Function.update m (s.frontier + 1 + C + 1 + m (s.frontier + 1 + C)) v)
+      (s.frontier + 1 + C) (m (s.frontier + 1 + C) + 1) s.frontier = 0
+    rw [hR, Function.update_of_ne (by omega), Function.update_of_ne (by omega)]
+    exact hF
+  · change Function.update (_ : ℕ → ℕ) (s.frontier + 1 + C)
+      (m (s.frontier + 1 + C) + 1) (s.frontier + 1 + C) = 1
+    rw [Function.update_self, hR]
+
+private theorem enqueued_work (C v : ℕ) (s : Memory.State) :
+    MemoryQueueDispatch.dequeueWork (Queue.Memory.frontLayout s C, Queue.Memory.rearLayout s C)
+      (enqueued C v s) = 109 := by
+  obtain ⟨hF, hR⟩ := enqueued_counts C v s
+  have hp := Stack.Memory.runClient_pop_of_eq_zero (w := 0) (Queue.Memory.frontLayout s C)
+    (enqueued C v s) hF
+  simp only [MemoryQueueDispatch.dequeueWork, MemoryQueueDispatch.dequeueFuel,
+    StateTransitionSpec.clientResult, StateTransitionSpec.clientState, hp,
+    Stack.Memory.runClient_size, hR]
+
+private theorem enqueued_domain {w C v : ℕ} {s : Memory.State} (hw : Memory.WellFormed w s)
+    (hf : Fits w (s.frontier + 2 * (C + 1))) (hC : 1 ≤ C) (hv : Fits w v) :
+    MemoryQueueDispatch.dequeueSafe w
+      (Queue.Memory.frontLayout s C, Queue.Memory.rearLayout s C) (enqueued C v s) := by
+  have hLayouts := MemoryQueueAdapter.layouts_valid (base := s.frontier) hf
+  change (Queue.Memory.frontLayout s C).Valid w C ∧ (Queue.Memory.rearLayout s C).Valid w C ∧
+    Disjoint (Queue.Memory.frontLayout s C).footprint
+      (Queue.Memory.rearLayout s C).footprint at hLayouts
+  obtain ⟨hL₁, hL₂, hd⟩ := hLayouts
+  obtain ⟨hi₁, hi₂⟩ := allocated_invariants C s
+  obtain ⟨hc₁, hc₂⟩ := allocated_counts C s
+  have hwA := allocated_wellFormed hw hf
+  have hvPush : (Stack.WordRAM.spec w C).valid
+      (Stack.Memory.abs (Queue.Memory.rearLayout s C) (Queue.Memory.allocated s C))
+      (.push v) := by
+    refine ⟨?_, hv⟩
+    rw [Stack.Memory.length_abs, hc₂]
+    omega
+  let M := Stack.Memory.refinement hL₂
+  have hvalid := ((Memory.spec w).demonicValid_iff_validHistory_runClient _ _).mp
+    (M.valid (.push v) hi₂ hvPush)
+  have hcorrect := M.correct (.push v) hi₂ hvPush
+    ((Memory.spec w).clientRun_canonical (Queue.Memory.allocated s C) _ hvalid)
+  have hframe := Stack.Memory.frame hL₂ hL₁ hd.symm hi₁ (.push v) hvPush
+  have hi₁' : Stack.Memory.Inv (Queue.Memory.frontLayout s C) (enqueued C v s) := by
+    simpa only [enqueued, Stack.Memory.methods, StateTransitionSpec.clientState, runClient_width]
+      using hframe.2
+  have hi₂' : Stack.Memory.Inv (Queue.Memory.rearLayout s C) (enqueued C v s) := by
+    have hcorrect' := hcorrect.2
+    change Stack.Memory.Inv (Queue.Memory.rearLayout s C)
+      ((Memory.spec w).clientState (Queue.Memory.allocated s C)
+        (Stack.Memory.push (Queue.Memory.rearLayout s C) v)) at hcorrect'
+    simpa only [enqueued, StateTransitionSpec.clientState, runClient_width] using hcorrect'
+  have hvalid' : (Memory.spec w).ValidHistory (Queue.Memory.allocated s C)
+      ((Memory.spec w).clientHistory (Queue.Memory.allocated s C)
+        (Stack.Memory.push (Queue.Memory.rearLayout s C) v)) := hvalid
+  have hwE : Memory.WellFormed w (enqueued C v s) := wellFormed_client hwA _ hvalid'
+  apply MemoryQueueAdapter.dequeue_safe hL₁ hL₂ hd hwE hi₁' hi₂'
+  obtain ⟨hF, hR⟩ := enqueued_counts C v s
+  rw [hF, hR]
+  omega
+
+/-- The concrete allocated source client has a uniform native emitter before capacity, value,
+frontier, width or either allocated layout. Its explicit local work includes faithful allocation
+and the actual fallback transfer; the old dirty item cells are not initialized for free. -/
+theorem realizes_roundTrip (sourceWidth : ℕ) :
+    Realizes .exact (fun d : ℕ × ℕ =>
+      Queue.Memory.run sourceWidth d.1 (roundTrip sourceWidth d.1 d.2))
+      roundTripWords optionWords
+      (fun w d s => 1 ≤ d.1 ∧ Fits w (s.frontier + 2 * (d.1 + 1))) (fun _ _ => 163) := by
+  let e₁ := appendWords roundTripWords MemoryQueue.layoutWords
+  let e₂ := appendWords e₁ (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+  have halloc := realizes_allocPair.reindex (fun d : ℕ × ℕ => d.1) roundTripWords ![0]
+    (by intro d i; fin_cases i; rfl)
+  have henqueue := (MemoryQueueDispatch.realizes_enqueue 0 0).reindex
+    (fun d : (ℕ × ℕ) × (Stack.Memory.Layout × Stack.Memory.Layout) => (d.2, d.1.2))
+    e₁ ![2, 3, 4, 5, 6, 7, 8, 9, 1] (by intro d i; fin_cases i <;> rfl)
+  have hdequeue := (MemoryQueueDispatch.realizes_dequeue 0 0).reindex
+    (fun d : ((ℕ × ℕ) × (Stack.Memory.Layout × Stack.Memory.Layout)) × Unit => d.1.2)
+    e₂ ![2, 3, 4, 5, 6, 7, 8, 9] (by intro d i; fin_cases i <;> rfl)
+  have h := halloc.bind (henqueue.bind hdequeue)
+  have hp : (fun d : ℕ × ℕ => (allocPair d.1).bind (fun L =>
+      (Queue.Memory.memMethods L.1 L.2 0 0 (.enqueue d.2)).bind
+        (fun _ => Queue.Memory.memMethods L.1 L.2 0 0 .dequeue))) =
+      (fun d : ℕ × ℕ => Queue.Memory.run sourceWidth d.1
+        (roundTrip sourceWidth d.1 d.2)) := by
+    funext d
+    rw [run_eq_allocPair_bind]
+    congr 1
+    funext L
+    simp only [roundTrip, link, PFunctor.FreeM.liftM_bind]
+    rw [PFunctor.FreeM.liftM_lift, PFunctor.FreeM.liftM_lift]
+    simp only [PFunctor.FreeM.bind_eq_bind,
+      MemoryQueue.memMethods_enqueue, MemoryQueue.memMethods_dequeue]
+  simp only [PFunctor.FreeM.bind_eq_bind] at hp h
+  rw [hp] at h
+  apply h.consequence
+  · intro w d s hwords hw ⟨hC, hf⟩
+    obtain ⟨hi₁, hi₂⟩ := allocated_invariants d.1 s
+    obtain ⟨_, hc₂⟩ := allocated_counts d.1 s
+    have hL₂ : (Queue.Memory.rearLayout s d.1).Valid w d.1 :=
+      Stack.Memory.valid_allocLayout (hf.of_le (by omega))
+    change Fits w (s.frontier + 2 * (d.1 + 1)) ∧
+      ((Queue.Memory.rearLayout s d.1).Valid w d.1 ∧
+        Stack.Memory.Inv (Queue.Memory.rearLayout s d.1) (Queue.Memory.allocated s d.1) ∧
+        (Queue.Memory.allocated s d.1).mem (Queue.Memory.rearLayout s d.1).count.base < d.1) ∧
+      MemoryQueueDispatch.dequeueSafe w
+        (Queue.Memory.frontLayout s d.1, Queue.Memory.rearLayout s d.1)
+        ((Memory.spec 0).clientState (Queue.Memory.allocated s d.1)
+          (Queue.Memory.memMethods (Queue.Memory.frontLayout s d.1)
+            (Queue.Memory.rearLayout s d.1) 0 0 (.enqueue d.2)))
+    refine ⟨hf, ⟨hL₂, hi₂, ?_⟩, ?_⟩
+    · rw [hc₂]; omega
+    · rw [MemoryQueue.memMethods_enqueue]
+      exact enqueued_domain hw hf hC (hwords 1)
+  · intro d s
+    change 42 + (10 + MemoryQueueDispatch.dequeueWork
+      (Queue.Memory.frontLayout s d.1, Queue.Memory.rearLayout s d.1)
+      ((Memory.spec 0).clientState (Queue.Memory.allocated s d.1)
+        (Queue.Memory.memMethods (Queue.Memory.frontLayout s d.1)
+          (Queue.Memory.rearLayout s d.1) 0 0 (.enqueue d.2))) + 1) + 1 ≤ 163
+    rw [MemoryQueue.memMethods_enqueue]
+    change 42 + (10 + MemoryQueueDispatch.dequeueWork
+      (Queue.Memory.frontLayout s d.1, Queue.Memory.rearLayout s d.1)
+      (enqueued d.1 d.2 s) + 1) + 1 ≤ 163
+    rw [enqueued_work]
+
+/-- The actual allocated source client is admissible and returns `some v`. The capacity,
+value-word and final-frontier fits are explicit; no arbitrary-client native claim is used. -/
+theorem roundTrip_correct {w C v : ℕ} {s : Memory.State} (hC : 1 ≤ C) (hv : Fits w v)
+    (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s
+      (Queue.Memory.run w C (roundTrip w C v))) ∧
+      (Memory.spec w).clientResult s (Queue.Memory.run w C (roundTrip w C v)) = some v := by
+  apply Queue.Memory.run_correct (roundTrip w C v) hf
+  change (0 < C ∧ Fits w v) ∧ True ∧ True
+  exact ⟨⟨by omega, hv⟩, trivial, trivial⟩
+
+/-- The specification-width parameter does not select source code for this concrete client.
+Native word bounds and operation admissibility are still checked separately. -/
+theorem roundTrip_run_width (w C v : ℕ) :
+    Queue.Memory.run w C (roundTrip w C v) = Queue.Memory.run 0 C (roundTrip 0 C v) := by
+  rw [run_eq_allocPair_bind, run_eq_allocPair_bind]
+  congr 1
+  funext L
+  simp only [roundTrip, link, PFunctor.FreeM.liftM_bind]
+  rw [PFunctor.FreeM.liftM_lift, PFunctor.FreeM.liftM_lift,
+    PFunctor.FreeM.liftM_lift, PFunctor.FreeM.liftM_lift]
+  simp only [MemoryQueue.memMethods_enqueue, MemoryQueue.memMethods_dequeue]
+
+/-- Fix a source interface once, before the physical word width, while retaining the exact
+source answer and memory-history admissibility of the supported client. -/
+theorem roundTrip_correct_source (sourceWidth : ℕ) {w C v : ℕ} {s : Memory.State}
+    (hC : 1 ≤ C) (hv : Fits w v) (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s
+      (Queue.Memory.run sourceWidth C (roundTrip sourceWidth C v))) ∧
+      (Memory.spec w).clientResult s
+        (Queue.Memory.run sourceWidth C (roundTrip sourceWidth C v)) = some v := by
+  have h := roundTrip_correct hC hv hf
+  rw [roundTrip_run_width w C v] at h
+  rw [roundTrip_run_width sourceWidth C v]
+  exact h
+
+end Cslib.WordRAM.Realization.MemoryQueueAllocation
diff --git a/ComplexityTests/WordRAMMemoryQueueAllocation.lean b/ComplexityTests/WordRAMMemoryQueueAllocation.lean
new file mode 100644
index 0000000000..c9ebc37708
--- /dev/null
+++ b/ComplexityTests/WordRAMMemoryQueueAllocation.lean
@@ -0,0 +1,244 @@
+/-
+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.MemoryQueueAllocation
+import Complexity.Computability.WordRAM.Realization.Witness
+
+/-! The dirty-memory body ABI and the charged standard list-input ABI are checked separately.
+One allocation emitter is reused at independent frontiers, retaining old item words seven. The
+supported complete source client also compiles to a flat program. `Data.init` starts its future
+cells at zero and is not used as evidence for dirty-item preservation. -/
+
+namespace ComplexityTests.WordRAMMemoryQueueAllocation
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+open MemoryQueueAllocation
+
+private def front {k t : ℕ} : Fin (1 + (k + t)) := ⟨0, by omega⟩
+private def src {k t : ℕ} (i : Fin k) : Fin (1 + (k + t)) := Fin.natAdd 1 (Fin.castAdd t i)
+private def tmp {k t : ℕ} (i : Fin t) : Fin (1 + (k + t)) := Fin.natAdd 1 (Fin.natAdd k i)
+
+private theorem placement (k t : ℕ) :
+    Function.Injective (src (k := k) (t := t)) ∧
+    Function.Injective (tmp (k := k) (t := t)) ∧
+    (∀ i j, src (t := t) i ≠ tmp (k := k) j) ∧
+    (∀ j, tmp (k := k) (t := t) j ≠ front) ∧
+    (∀ i, src (k := k) (t := t) i ≠ front) := by
+  refine ⟨?_, ?_, ?_, ?_, ?_⟩
+  · intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    simpa only [src, Fin.val_natAdd, Fin.val_castAdd, Nat.add_left_cancel_iff] using this
+  · intro i j h
+    apply Fin.ext
+    have := congrArg Fin.val h
+    simp only [tmp, Fin.val_natAdd] at this
+    omega
+  · intro i j h
+    have := congrArg Fin.val h
+    simp only [src, tmp, Fin.val_natAdd, Fin.val_castAdd] at this
+    have := i.isLt
+    omega
+  · intro i h
+    have := congrArg Fin.val h
+    simp only [tmp, front, Fin.val_natAdd] at this
+    omega
+  · intro i h
+    have := congrArg Fin.val h
+    simp only [src, front, Fin.val_natAdd, Fin.val_castAdd] at this
+    omega
+
+private def packed {k t : ℕ} (v : Fin k → ℕ) (s : Memory.State) : Data (1 + (k + t)) :=
+  ⟨Fin.addCases (fun _ => s.frontier) (Fin.addCases v (fun _ => 0)), s.mem⟩
+
+private theorem packed_bounded {k t w : ℕ} {v : Fin k → ℕ} {s : Memory.State}
+    (hv : ∀ i, Fits w (v i)) (hs : Memory.WellFormed w s) :
+    (packed (t := t) v s).Bounded w := by
+  refine ⟨fun i => ?_, hs.mem_fits⟩
+  refine Fin.addCases (fun _ => by simpa [packed] using hs.frontier_fits) (fun j => ?_) i
+  exact Fin.addCases (fun i => by simpa [packed] using hv i) (fun _ => by simp [packed]) j
+
+private theorem packed_input {k t : ℕ} (v : Fin k → ℕ) (s : Memory.State) :
+    (packed (t := t) v s).regs ∘ src = v := by
+  funext i
+  simp [packed, src]
+
+private theorem packed_state {k t : ℕ} (v : Fin k → ℕ) (s : Memory.State) :
+    memoryState front (packed (t := t) v s) = s := by
+  cases s
+  rfl
+
+private def dirty (f : ℕ) : Memory.State := ⟨fun _ => 7, f⟩
+private theorem dirty_wf {f : ℕ} (hf : Fits 4 f) : Memory.WellFormed 4 (dirty f) :=
+  ⟨hf, fun _ => by change Fits 4 7; decide⟩
+
+private theorem allocation :
+    Realizes .exact allocPair (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding MemoryQueue.layoutWords
+      (fun w C s => Fits w (s.frontier + 2 * (C + 1))) (fun _ _ => 42) := realizes_allocPair
+private noncomputable def allocationCode := allocation.code
+  (front (k := 1) (t := 8 + allocation.scratchSize + 1)) src tmp
+private noncomputable def allocationData (C : ℕ) (s : Memory.State) :=
+  packed (t := 8 + allocation.scratchSize + 1) (fun _ : Fin 1 => C) s
+
+private theorem allocation_execution (w C : ℕ) (s : Memory.State) (hw : Memory.WellFormed w s)
+    (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    ∃ y, ExecWithin w allocationCode (allocationData C s) y (allocation.factor * 49) ∧
+      memoryState front y = Queue.Memory.allocated s C ∧
+      ∀ i : Fin 8, y.regs (tmp (Fin.castAdd (allocation.scratchSize + 1) i)) =
+        MemoryQueue.layoutWords (Queue.Memory.frontLayout s C, Queue.Memory.rearLayout s C) i := by
+  obtain ⟨_, hi, hd, hfr, hs⟩ := placement 1 (8 + allocation.scratchSize + 1)
+  have hx : (allocationData C s).Bounded w := packed_bounded (fun _ => hf.of_le (by omega)) hw
+  have hin := packed_input (t := 8 + allocation.scratchSize + 1) (fun _ : Fin 1 => C) s
+  have hm : memoryState front (allocationData C s) = s :=
+    packed_state (t := 8 + allocation.scratchSize + 1) (fun _ : Fin 1 => C) s
+  obtain ⟨y, he, hmem, hout, _⟩ := (allocation.code_spec front src tmp hi hd hfr hs).2
+    w C (allocationData C s) hx hin (hm ▸ hf) (hm ▸ valid_allocPair hf)
+  rw [hm] at he hmem hout
+  rw [allocPair_memoryCost] at he
+  exact ⟨y, he, hmem, hout⟩
+
+-- The SAME emitter is used at frontiers three and five. Items retain seven, so clearing the
+-- whole allocated block would not realize this source initializer.
+example (f : ℕ) (hf : f = 3 ∨ f = 5) :
+    ∃ y, ExecWithin 4 allocationCode (allocationData 2 (dirty f)) y (allocation.factor * 49) ∧
+      y.regs (tmp (Fin.castAdd (allocation.scratchSize + 1) 0)) = f ∧
+      y.mem f = 0 ∧ y.mem (f + 3) = 0 ∧ y.mem (f + 1) = 7 ∧
+      y.mem (f + 2) = 7 ∧ y.mem 100 = 7 ∧ y.regs front = f + 6 := by
+  have hf' : Fits 4 f := by rcases hf with rfl | rfl <;> decide
+  have hend : Fits 4 ((dirty f).frontier + 2 * (2 + 1)) := by
+    rcases hf with rfl | rfl <;> decide
+  obtain ⟨y, he, hm, hout⟩ := allocation_execution 4 2 (dirty f) (dirty_wf hf') hend
+  refine ⟨y, he, hout 0, ?_, ?_, ?_, ?_, ?_, congrArg Memory.State.frontier hm⟩
+  all_goals
+    rcases hf with rfl | rfl
+    all_goals first
+      | exact congrArg (fun s : Memory.State => s.mem 3) hm
+      | exact congrArg (fun s : Memory.State => s.mem 6) hm
+      | exact congrArg (fun s : Memory.State => s.mem 4) hm
+      | exact congrArg (fun s : Memory.State => s.mem 5) hm
+      | exact congrArg (fun s : Memory.State => s.mem 8) hm
+      | exact congrArg (fun s : Memory.State => s.mem 7) hm
+      | exact congrArg (fun s : Memory.State => s.mem 100) hm
+
+private theorem client :
+    Realizes .exact (fun d : ℕ × ℕ => Queue.Memory.run 0 d.1 (roundTrip 0 d.1 d.2))
+      roundTripWords optionWords
+      (fun w d s => 1 ≤ d.1 ∧ Fits w (s.frontier + 2 * (d.1 + 1)))
+      (fun _ _ => 163) := realizes_roundTrip 0
+private noncomputable def clientCode := client.code
+  (front (k := 2) (t := 2 + client.scratchSize + 1)) src tmp
+private noncomputable def clientData (C v : ℕ) (s : Memory.State) :=
+  packed (t := 2 + client.scratchSize + 1) (roundTripWords (C, v)) s
+
+private theorem client_execution (w C v : ℕ) (s : Memory.State) (hw : Memory.WellFormed w s)
+    (hC : 1 ≤ C) (hv : Fits w v) (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    ∃ y, ExecWithin w clientCode (clientData C v s) y
+        (client.factor * (memoryCost (Queue.Memory.run 0 C (roundTrip 0 C v)) s + 164)) ∧
+      memoryState front y = (Memory.spec w).clientState s
+        (Queue.Memory.run 0 C (roundTrip 0 C v)) ∧
+      y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 0)) = 1 ∧
+      y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 1)) = v := by
+  obtain ⟨_, hi, hd, hfr, hs⟩ := placement 2 (2 + client.scratchSize + 1)
+  have hwords (i : Fin 2) : Fits w (roundTripWords (C, v) i) := by
+    fin_cases i
+    · change Fits w C; exact hf.of_le (by omega)
+    · change Fits w v; exact hv
+  have hx : (clientData C v s).Bounded w := packed_bounded hwords hw
+  have hin := packed_input (t := 2 + client.scratchSize + 1) (roundTripWords (C, v)) s
+  have hm : memoryState front (clientData C v s) = s :=
+    packed_state (t := 2 + client.scratchSize + 1) (roundTripWords (C, v)) s
+  have hc := roundTrip_correct_source 0 hC hv hf
+  obtain ⟨y, he, hmem, hout, _⟩ := (client.code_spec front src tmp hi hd hfr hs).2
+    w (C, v) (clientData C v s) hx hin (hm ▸ And.intro hC hf) (hm ▸ hc.1)
+  rw [hm] at he hmem hout
+  rw [hc.2] at hout
+  exact ⟨y, he, hmem, hout 0, hout 1⟩
+
+private theorem client_program_execution (w C v : ℕ) (s : Memory.State)
+    (hw : Memory.WellFormed w s) (hC : 1 ≤ C) (hv : Fits w v)
+    (hf : Fits w (s.frontier + 2 * (C + 1))) :
+    ∃ y n, Runs w
+        (clientCode.program (tmp (Fin.castAdd (client.scratchSize + 1) 1)))
+        ⟨0, clientData C v s⟩ ⟨clientCode.size, y⟩ n ∧
+      step w (clientCode.program (tmp (Fin.castAdd (client.scratchSize + 1) 1)))
+        ⟨clientCode.size, y⟩ = .halt v ∧
+      n + 1 ≤ client.factor *
+        (memoryCost (Queue.Memory.run 0 C (roundTrip 0 C v)) s + 164) + 1 ∧
+      memoryState front y = (Memory.spec w).clientState s
+        (Queue.Memory.run 0 C (roundTrip 0 C v)) ∧
+      y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 0)) = 1 := by
+  obtain ⟨y, ⟨n, hn, he⟩, hm, ht, hv⟩ := client_execution w C v s hw hC hv hf
+  have hr := he.runs (pc := 0)
+    (p := clientCode.program (tmp (Fin.castAdd (client.scratchSize + 1) 1)))
+    (Program.Contains.self _).append_left
+  refine ⟨y, n, ?_, ?_, Nat.add_le_add_right hn 1, hm, ht⟩
+  · simpa only [Nat.zero_add] using hr
+  · rw [← hv]
+    exact step_halt (by simp [Code.program])
+
+-- Exact concrete grades: initialization is memory6/work42; the supported whole client is
+-- memory20/work163. Old inactive item cells and the inaccessible tail stay seven.
+example : memoryCost (allocPair 2) (dirty 3) = 6 := rfl
+example : memoryCost (Queue.Memory.run 0 2 (roundTrip 0 2 15)) (dirty 3) = 20 := by decide
+
+example : ∃ y, ExecWithin 4 clientCode (clientData 2 15 (dirty 3)) y (client.factor * 184) ∧
+    y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 0)) = 1 ∧
+    y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 1)) = 15 ∧
+    y.mem 3 = 0 ∧ y.mem 6 = 0 ∧ y.mem 5 = 7 ∧ y.mem 8 = 7 ∧ y.mem 100 = 7 ∧
+    y.regs front = 9 := by
+  obtain ⟨y, he, hm, ht, hv⟩ := client_execution 4 2 15 (dirty 3)
+    (dirty_wf (by decide)) (by decide) (by decide) (by decide)
+  refine ⟨y, he, ht, hv, ?_, ?_, ?_, ?_, ?_, congrArg Memory.State.frontier hm⟩
+  · exact congrArg (fun s : Memory.State => s.mem 3) hm
+  · exact congrArg (fun s : Memory.State => s.mem 6) hm
+  · exact congrArg (fun s : Memory.State => s.mem 5) hm
+  · exact congrArg (fun s : Memory.State => s.mem 8) hm
+  · exact congrArg (fun s : Memory.State => s.mem 100) hm
+
+-- Flat compilation retains that same final Data, then charges the trailing halt. Inputs here
+-- are already installed; this is the arbitrary dirty-memory ABI, not the Data.init ABI.
+example : ∃ y n, Runs 4
+      (clientCode.program (tmp (Fin.castAdd (client.scratchSize + 1) 1)))
+      ⟨0, clientData 2 15 (dirty 3)⟩ ⟨clientCode.size, y⟩ n ∧
+    step 4 (clientCode.program (tmp (Fin.castAdd (client.scratchSize + 1) 1)))
+      ⟨clientCode.size, y⟩ = .halt 15 ∧ n + 1 ≤ client.factor * 184 + 1 ∧
+    y.regs (tmp (Fin.castAdd (client.scratchSize + 1) 0)) = 1 ∧
+    y.mem 5 = 7 ∧ y.mem 100 = 7 ∧ y.regs front = 9 := by
+  obtain ⟨y, n, hr, hh, hn, hm, ht⟩ := client_program_execution 4 2 15 (dirty 3)
+    (dirty_wf (by decide)) (by decide) (by decide) (by decide)
+  refine ⟨y, n, hr, hh, hn, ht, ?_, ?_, congrArg Memory.State.frontier hm⟩
+  · exact congrArg (fun s : Memory.State => s.mem 5) hm
+  · exact congrArg (fun s : Memory.State => s.mem 100) hm
+
+-- The separate standard-input endpoint uses the existing charged prefix: one flat program
+-- precedes physical width, capacity and value. Future Data.init cells are initially zero.
+example : ∃ r K, ∃ p : Program .exact r, ∀ w C v, 1 ≤ C → Fits w v →
+    Fits w (3 + 2 * (C + 1)) → ∃ t, Executes w p (State.init [C, v]) v t ∧
+      t ≤ K * (memoryCost (Queue.Memory.run 0 C (roundTrip 0 C v))
+        (inputState [C, v]) + 164) + 1 := by
+  obtain ⟨n, K, emit, he⟩ := client.exists_init_program (fun d : ℕ × ℕ => [d.1, d.2])
+    (by intro d i; fin_cases i <;> rfl)
+  obtain ⟨hsrc, hi, hd, hfr, hs⟩ := placement 2 (2 + n + 1)
+  refine ⟨_, K, (Code.seq
+    (inputPrefix (front (k := 2) (t := 2 + n + 1)) (tmp (Fin.last (2 + n))) src)
+    (emit front src tmp)).program (tmp (Fin.castAdd (n + 1) 1)), ?_⟩
+  intro w C v hC hv hf
+  have hin : InputFits w [C, v] := by
+    refine ⟨?_, ?_⟩
+    · change Fits w 2
+      exact hf.of_le (by omega)
+    intro a ha
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at ha
+    rcases ha with rfl | rfl
+    · exact hf.of_le (by omega)
+    · exact hv
+  have hc := roundTrip_correct_source 0 (s := inputState [C, v]) hC hv hf
+  obtain ⟨t, ht, hbound⟩ := he front src tmp hsrc hi hd hfr hs 1 w (C, v)
+    (by change 2 ≤ 2; omega) (by change Fits w 3; exact hf.of_le (by omega)) hin ⟨hC, hf⟩ hc.1
+  rw [hc.2] at ht
+  exact ⟨t, ht, hbound⟩
+
+end ComplexityTests.WordRAMMemoryQueueAllocation
diff --git a/ROADMAP.md b/ROADMAP.md
index 28b510c423..1e62d5fb50 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -649,8 +649,11 @@ reusing graph and matroid foundations and the shared data-structure interfaces.
   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.
+  faithful source allocation. The exact source allocation prefix also has a constant-work native
+  certificate, preserving dirty item cells, followed by a supported allocated enqueue/dequeue
+  client. Its installed-argument dirty-memory and charged standard-input flat endpoints are
+  distinct. Broader M1 migration and comparison remain 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
   allocation and deallocation, shrinking, and live and peak space accounting; ownership and
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 43a776549c..7b5b094d18 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -542,8 +542,12 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   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.
+  source allocation remains distinct: its actual two count-cell and two dirty-array allocations
+  have memory charge 6 and certified local work 42, independent of capacity. A supported actual
+  allocated enqueue/dequeue client has local work 163. Its same native body preserves unused
+  dirty cells at different starting frontiers; a separate standard-input flat program charges
+  its real input prefix and halt. This does not time arbitrary opaque queue clients, close the
+  broader M1 comparison gate, or claim an abstract headline or legacy size/space/step improvement.
   `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