diff --git a/Complexity.lean b/Complexity.lean
index fb6d2fc56d..05c33006ea 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2628,7 +2628,9 @@ public import Complexity.Computability.WordRAM.Randomized.UniformLoopExit
 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.MemoryStack
 public import Complexity.Computability.WordRAM.Realization.Glue
+public import Complexity.Computability.WordRAM.Realization.GlueVector
 public import Complexity.Computability.WordRAM.Realization.Grade
 public import Complexity.Computability.WordRAM.Realization.Loop
 public import Complexity.Computability.WordRAM.Realization.MemoryBackend
diff --git a/Complexity/Computability/WordRAM/Realization/Client/MemoryStack.lean b/Complexity/Computability/WordRAM/Realization/Client/MemoryStack.lean
new file mode 100644
index 0000000000..de5d905ce3
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Client/MemoryStack.lean
@@ -0,0 +1,180 @@
+/-
+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.Bind
+public import Complexity.Computability.WordRAM.Realization.Branch
+public import Complexity.Computability.WordRAM.Realization.Glue
+public import Complexity.Computability.WordRAM.Realization.GlueVector
+public import Complexity.Computability.WordRAM.Realization.Primitive
+public import Complexity.DataStructure.Stack.Memory
+
+/-!
+# Native realizations of the memory-oracle stack
+
+The certificates consume the existing `Stack.Memory` methods unchanged. Every field of the
+runtime layout has a faithful word encoding, so the emitter is chosen before the layout's
+allocation addresses and all operation arguments. Arithmetic, copies, binds and branches have
+explicit local-work charges in addition to the actual memory history.
+
+## Main definitions
+
+* `layoutWords`, `pushWords`: faithful encodings of the complete layout and push arguments.
+
+## Main results
+
+* `realizes_size`, `realizes_push`, `realizes_pop`: uniform native realizations of the existing
+  stack methods.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization.MemoryStack
+
+open Cslib.DataStructure
+
+private abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+private abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+/-- All four layout fields are retained: count base/length, then items base/length. -/
+def layoutWords : Stack.Memory.Layout ↪ (Fin 4 → ℕ) where
+  toFun L := ![L.count.base, L.count.length, L.items.base, L.items.length]
+  inj' := by
+    rintro ⟨⟨a, b⟩, ⟨c, d⟩⟩ ⟨⟨a', b'⟩, ⟨c', d'⟩⟩ h
+    have ha := congrFun h 0
+    have hb := congrFun h 1
+    have hc := congrFun h 2
+    have hd := congrFun h 3
+    change a = a' at ha
+    change b = b' at hb
+    change c = c' at hc
+    change d = d' at hd
+    cases ha; cases hb; cases hc; cases hd
+    rfl
+
+/-- Push arguments append the unshifted value to the complete runtime layout. -/
+def pushWords : Stack.Memory.Layout × ℕ ↪ (Fin 5 → ℕ) :=
+  appendWords layoutWords (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+/-- Size uses the existing count query with no additional local computation. -/
+theorem realizes_size :
+    Realizes .exact Stack.Memory.size layoutWords
+      (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+      (fun _ _ _ => True) (fun _ _ => 0) := Realizes.read layoutWords 0
+
+/-- Push works uniformly for every runtime layout and value. The visible invariant and spare
+capacity discharge the address and increment fit obligations. The two additions cost six local
+instructions; four bind rules contribute four units of local control work. -/
+theorem realizes_push :
+    Realizes .exact (fun d : Stack.Memory.Layout × ℕ => Stack.Memory.push d.1 d.2)
+      pushWords (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+      (fun w d s => d.1.Valid w d.1.items.length ∧ Stack.Memory.Inv d.1 s ∧
+        s.mem d.1.count.base < d.1.items.length) (fun _ _ => 10) := by
+  let e₁ := appendWords pushWords word
+  let e₂ := appendWords e₁ word
+  let e₃ := appendWords e₂ word
+  let e₄ := appendWords e₃ unitWords
+  apply ((Realizes.read pushWords 0).bind
+    ((Realizes.addWords e₁ 2 5).bind ((Realizes.increment e₂ 5).bind
+      ((Realizes.write e₃ 6 4).bind (Realizes.write e₄ 0 7))))).consequence
+    (hwork := fun _ _ => le_rfl)
+  intro w d s _ hw ⟨hL, hInv, hcap⟩
+  change True ∧ Fits w (d.1.items.base + s.mem d.1.count.base) ∧
+    Fits w (s.mem d.1.count.base + 1) ∧ True ∧ True
+  exact ⟨trivial, hw.fits_of_lt_frontier (hInv.item_lt hcap),
+    hL.capacity_fits.of_le (by omega), trivial, trivial⟩
+
+/-- Pop returns a presence tag and unshifted payload. Its positive branch uses defined exact
+subtraction and performs the existing memory reads/write. All copies and branch/bind overhead
+are charged; the local-work allowance is 19 for either path, including the shorter empty path. -/
+theorem realizes_pop :
+    Realizes .exact Stack.Memory.pop layoutWords optionWords
+      (fun w L s => L.Valid w L.items.length ∧ Stack.Memory.Inv L s) (fun _ _ => 19) := by
+  let e₁ := appendWords layoutWords word
+  let e₂ := appendWords e₁ word
+  let e₃ := appendWords e₂ word
+  let e₄ := appendWords e₃ word
+  let e₅ := appendWords e₄ word
+  let e₆ := appendWords e₅ unitWords
+  have hread : Realizes .exact (fun L : Stack.Memory.Layout => Memory.read L.count.base)
+      layoutWords word (fun _ _ _ => True) (fun _ _ => 0) := Realizes.read layoutWords 0
+  have hzero : Realizes .exact (fun _ : Stack.Memory.Layout × ℕ => pure 0) e₁ word
+      (fun _ _ _ => True) (fun _ _ => 1) := by
+    have h := Realizes.glue e₁
+      (GlueComputes.const (B := .exact) (P := fun _ => True) (bound := fun _ => 0)
+        0 (fun _ _ => le_rfl))
+    exact h.consequence (fun w _ _ _ _ _ => ⟨trivial, fits_zero w⟩) (fun _ _ => le_rfl)
+  have hsub : Realizes .exact
+      (fun d : (Stack.Memory.Layout × ℕ) × ℕ => pure (d.1.2 - 1)) e₂ word
+      (fun w d _ => 1 ≤ d.1.2 ∧ Fits w d.1.2) (fun _ _ => 3) := Realizes.decrement e₂ 4
+  have haddr : Realizes .exact
+      (fun d : ((Stack.Memory.Layout × ℕ) × ℕ) × ℕ => pure (d.1.1.1.items.base + d.2))
+      e₃ word (fun w d _ => Fits w (d.1.1.1.items.base + d.2)) (fun _ _ => 3) :=
+    Realizes.addWords e₃ 2 6
+  have hitem : Realizes .exact
+      (fun d : (((Stack.Memory.Layout × ℕ) × ℕ) × ℕ) × ℕ => Memory.read d.2)
+      e₄ word (fun _ _ _ => True) (fun _ _ => 0) := Realizes.read e₄ 7
+  have hwrite : Realizes .exact
+      (fun d : ((((Stack.Memory.Layout × ℕ) × ℕ) × ℕ) × ℕ) × ℕ =>
+        Memory.write d.1.1.1.1.1.count.base d.1.1.2)
+      e₅ unitWords (fun _ _ _ => True) (fun _ _ => 0) := Realizes.write e₅ 0 6
+  have hsome : Realizes .exact
+      (fun d : (((((Stack.Memory.Layout × ℕ) × ℕ) × ℕ) × ℕ) × ℕ) × Unit =>
+        pure (some d.1.2)) e₆ optionWords
+      (fun w d _ => Fits w 1 ∧ Fits w d.1.2) (fun _ _ => 4) := Realizes.returnSome e₆ 8
+  have hpos := (Realizes.bind hsub (Realizes.bind haddr
+    (Realizes.bind hitem (Realizes.bind hwrite hsome)))).consequence
+    (safe' := fun w d s => 1 ≤ d.1.2 ∧ Fits w d.1.2 ∧
+      Fits w (d.1.1.items.base + (d.1.2 - 1)) ∧ Fits w 1 ∧
+      Fits w (s.mem (d.1.1.items.base + (d.1.2 - 1))))
+    (work' := fun _ _ => 14)
+    (by
+      intro w d s _ _ ⟨hpos, hn, ha, h1, hv⟩
+      change (1 ≤ d.1.2 ∧ Fits w d.1.2) ∧
+        Fits w (d.1.1.items.base + (d.1.2 - 1)) ∧ True ∧ True ∧
+        Fits w 1 ∧ Fits w (s.mem (d.1.1.items.base + (d.1.2 - 1)))
+      exact ⟨⟨hpos, hn⟩, ha, trivial, trivial, h1, hv⟩)
+    (fun _ _ => le_rfl)
+  have hbranch := Realizes.branch (.eq 4 5) (Realizes.returnNone e₂) hpos
+  apply (Realizes.bind hread (Realizes.bind hzero hbranch)).consequence
+  · intro w L s hwords hw ⟨hL, hInv⟩
+    have hn : Fits w (s.mem L.count.base) := hw.mem_fits _
+    have h1 : Fits w 1 := hL.count_length ▸ hwords 1
+    change True ∧ True ∧ (if s.mem L.count.base = 0 then True else
+      1 ≤ s.mem L.count.base ∧ Fits w (s.mem L.count.base) ∧
+      Fits w (L.items.base + (s.mem L.count.base - 1)) ∧ Fits w 1 ∧
+      Fits w (s.mem (L.items.base + (s.mem L.count.base - 1))))
+    refine ⟨trivial, trivial, ?_⟩
+    split
+    · trivial
+    · have hle := hInv.count_le
+      exact ⟨by omega, hn, hw.fits_of_lt_frontier (hInv.item_lt (by omega)), h1,
+        hw.mem_fits _⟩
+  · intro L s
+    change 0 + (1 + ((if test (.eq 4 5) (e₂ ((L,
+      (Memory.spec 0).clientResult s (Memory.read L.count.base)), 0)) then 4 else 14) + 2) + 1) +
+      1 ≤ 19
+    split <;> omega
+
+/-- The push's explicit local work is dominated by its actual three-query memory charge. -/
+theorem push_work_bound (L : Stack.Memory.Layout) (v : ℕ) (s : Memory.State) :
+    10 ≤ 4 * memoryCost (Stack.Memory.push L v) s := by
+  change 10 ≤ 4 * 3
+  decide
+
+/-- Even the empty pop has a memory query. This domination uses the actual method history,
+after separately certifying all 19 units of local work, and is not a general query-only rule. -/
+theorem pop_work_bound (L : Stack.Memory.Layout) (s : Memory.State) :
+    19 ≤ 19 * memoryCost (Stack.Memory.pop L) s := by
+  by_cases h : s.mem L.count.base = 0
+  · simp [memoryCost, StateTransitionSpec.clientHistory, Stack.Memory.runClient_pop_of_eq_zero,
+      h, StateTransitionSpec.totalCost, Memory.charge]
+  · simp [memoryCost, StateTransitionSpec.clientHistory, Stack.Memory.runClient_pop_of_pos,
+      h, StateTransitionSpec.totalCost, Memory.charge]
+
+end Cslib.WordRAM.Realization.MemoryStack
diff --git a/Complexity/Computability/WordRAM/Realization/GlueVector.lean b/Complexity/Computability/WordRAM/Realization/GlueVector.lean
new file mode 100644
index 0000000000..1f5e8ebfc0
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/GlueVector.lean
@@ -0,0 +1,280 @@
+/-
+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.Glue
+
+/-!
+# Certified finite-result word glue
+
+A finite family of scalar `GlueComputes` certificates realizes one faithfully encoded result.
+The scalar witnesses are selected before every runtime input and word width. All coordinates
+reuse a static auxiliary bank disjoint from the output slots, and each computed coordinate is
+copied into its final slot. Both those copies and the empty-vector case are charged.
+
+`optionWords` supplies the shared two-word result convention needed by memory-stack and queue
+clients: `none` is `(0,0)` and `some v` is `(1,v)`. The payload is not incremented, so the largest
+fitting word remains representable. `boolWords` retains a zero slot for active-loop tests; a
+true tag still requires the visible word-fit condition for `1`.
+
+## Main definitions
+
+* `optionWords`: a faithful tag/payload encoding of optional natural words.
+* `boolWords`: a Boolean tag with a retained zero slot for native comparisons.
+
+## Main results
+
+* `Realizes.glueVector`: realize a finite result using certified scalar coordinate computations.
+* `Realizes.addWords`, `Realizes.increment`, `Realizes.decrement`: charged scalar word arithmetic.
+* `Realizes.returnNone`, `Realizes.returnSome`: charged optional-word results.
+
+This is a realization rule over the existing memory client and structured native code, not an
+additional program syntax or execution judgment.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+variable {B : Basis} {δ α : Type} {k l r : ℕ}
+
+/-- A presence tag and unshifted payload distinguish `none` from every `some v`. -/
+def optionWords : Option ℕ ↪ (Fin 2 → ℕ) where
+  toFun
+    | none => ![0, 0]
+    | some v => ![1, v]
+  inj' := by
+    intro a b h
+    cases a with
+    | none =>
+      cases b with
+      | none => rfl
+      | some v => have hh := congrFun h 0; simp at hh
+    | some u =>
+      cases b with
+      | none => have hh := congrFun h 0; simp at hh
+      | some v => exact congrArg some (congrFun h 1)
+
+@[simp] theorem optionWords_none : optionWords none = ![0, 0] := rfl
+@[simp] theorem optionWords_some (v : ℕ) : optionWords (some v) = ![1, v] := rfl
+
+/-- A Boolean tag with a retained zero slot supports native comparisons without immediates. -/
+def boolWords : Bool ↪ (Fin 2 → ℕ) where
+  toFun b := ![b.toNat, 0]
+  inj' := by
+    intro a b h
+    have hh := congrFun h 0
+    cases a <;> cases b <;> simp_all
+
+@[simp] theorem boolWords_false : boolWords false = ![0, 0] := rfl
+@[simp] theorem boolWords_true : boolWords true = ![1, 0] := rfl
+
+private def coordinateSeq (code : Fin l → Code B r) (idle : Fin r) : List (Fin l) → Code B r
+  | [] => .op (.copy idle idle)
+  | i :: is => .seq (code i) (coordinateSeq code idle is)
+
+private theorem coordinateSeq_glue (code : Fin l → Code B r) (idle : Fin r)
+    (h : ∀ i, (code i).IsGlue) (is : List (Fin l)) : (coordinateSeq code idle is).IsGlue := by
+  induction is with
+  | nil => trivial
+  | cons i is ih => exact ⟨h i, ih⟩
+
+namespace Realizes
+
+/-- Compute every output coordinate using actual certified scalar code. The common domain and
+all coordinate envelopes remain visible, while code, exchange constant and scratch are uniform.
+A final neutral copy pays for the empty result without materializing a non-fitting constant. -/
+theorem glueVector (input : δ ↪ (Fin k → ℕ)) (output : α ↪ (Fin l → ℕ))
+    (f : δ → α) (g bound : Fin l → (Fin k → ℕ) → ℕ) (time : Fin l → ℕ)
+    {P : (Fin k → ℕ) → Prop}
+    (hresult : ∀ d i, output (f d) i = g i (input d))
+    (hcoord : ∀ i, GlueComputes B P (g i) (bound i) (time i)) :
+    Realizes B (fun d => pure (f d)) input output
+      (fun w d _ => P (input d) ∧ ∀ i, Fits w (bound i (input d)))
+      (fun _ _ => (∑ i, time i) + l) := by
+  classical
+  choose n emit he using fun i => (hcoord i).2
+  let N := ∑ i, n i
+  have hn (i : Fin l) : n i ≤ N :=
+    Finset.single_le_sum (fun j _ => Nat.zero_le (n j)) (Finset.mem_univ i)
+  refine ⟨N, 1, fun _ src tmp =>
+    coordinateSeq (fun i => .seq
+      (emit i src (fun j => tmp ⟨l + j.val, by have := hn i; omega⟩))
+      (.op (.copy (tmp (Fin.castAdd (N + 1) i)) (tmp ⟨l, by omega⟩))))
+      (tmp ⟨l, by omega⟩) (List.finRange l), ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  let dst : Fin l → Fin r := fun i => tmp (Fin.castAdd (N + 1) i)
+  let aux : ∀ i : Fin l, Fin (n i + 1) → Fin r :=
+    fun i j => tmp ⟨l + j.val, by have := hn i; omega⟩
+  let scratch : Fin (N + 1) → Fin r := fun j => tmp ⟨l + j.val, by omega⟩
+  let coord : Fin l → Code B r := fun i =>
+    .seq (emit i src (aux i)) (.op (.copy (dst i) (scratch 0)))
+  have hdsti : Function.Injective dst := by
+    intro i j hij
+    apply Fin.ext
+    exact congrArg (fun a : Fin (l + N + 1) => a.val) (hi hij)
+  have hauxi (i : Fin l) : Function.Injective (aux i) := by
+    intro a b hab
+    apply Fin.ext
+    have h := congrArg (fun a : Fin (l + N + 1) => a.val) (hi hab)
+    dsimp only [aux] at h
+    omega
+  have had (i : Fin l) (j : Fin k) (a : Fin (n i + 1)) : src j ≠ aux i a := hd _ _
+  have hauxDst (i : Fin l) (j : Fin l) : ∀ a, aux i a ≠ dst j := by
+    intro a h
+    have hh := congrArg (fun a : Fin (l + N + 1) => a.val) (hi h)
+    dsimp only [aux, dst] at hh
+    simp only [Fin.val_castAdd] at hh
+    omega
+  have hcglue (i : Fin l) : (coord i).IsGlue :=
+    ⟨(he i src (aux i) (hauxi i) (had i)).1, trivial⟩
+  refine ⟨(coordinateSeq_glue coord (scratch 0) hcglue _).not_readsWidth, ?_⟩
+  intro w d x hx hin hsafe hv
+  have hruni (i : Fin l) (a : Data r) (ha : a.regs ∘ src = input d) :
+      ∃ b, ExecWithin w (coord i) a b (time i + 1) ∧ b.mem = a.mem ∧
+        b.regs ∘ src = input d ∧ b.regs (dst i) = output (f d) i ∧
+        ∀ j, (∀ z, scratch z ≠ j) → dst i ≠ j → b.regs j = a.regs j := by
+    obtain ⟨b, hb, hbo, hbm, hbf⟩ :=
+      (he i src (aux i) (hauxi i) (had i)).2 w a (ha.symm ▸ hsafe.1)
+        (ha.symm ▸ hsafe.2 i)
+    let c := b.set (dst i) (g i (input d))
+    have ho : b.regs (scratch 0) = g i (input d) := by
+      have hz : aux i 0 = scratch 0 := by
+        apply congrArg tmp
+        apply Fin.ext
+        rfl
+      rw [← hz]
+      simpa only [ha] using hbo
+    have hc : ExecWithin (B := B) w (.op (.copy (dst i) (scratch 0))) b c 1 := by
+      simpa only [ho] using
+        (ExecWithin.copy (B := B) (w := w) (d := dst i) (s := scratch 0) (x := b))
+    refine ⟨c, hb.seq hc, hbm, ?_, ?_, ?_⟩
+    · funext j
+      change c.regs (src j) = input d j
+      rw [show c.regs (src j) = b.regs (src j) from Function.update_of_ne (hd _ _) _ _,
+        hbf _ (fun a => (had i j a).symm)]
+      exact congrFun ha j
+    · change (b.set (dst i) _).regs (dst i) = _
+      simp [Data.set, hresult]
+    · intro j hsj hdj
+      rw [show c.regs j = b.regs j from Function.update_of_ne hdj.symm _ _,
+        hbf j (fun z => ?_)]
+      exact hsj ⟨z.val, by have := hn i; omega⟩
+  have hseq (is : List (Fin l)) (hnodup : is.Nodup) (a : Data r)
+      (ha : a.regs ∘ src = input d) :
+      ∃ b, ExecWithin w (coordinateSeq coord (scratch 0) is) a b
+          ((is.map fun i => time i + 1).sum + 1) ∧
+        b.mem = a.mem ∧ b.regs ∘ src = input d ∧
+        (∀ i ∈ is, b.regs (dst i) = output (f d) i) ∧
+        ∀ j, (∀ z, scratch z ≠ j) → (∀ i ∈ is, dst i ≠ j) → b.regs j = a.regs j := by
+    induction is generalizing a with
+    | nil =>
+      have hself : ExecWithin (B := B) w (.op (.copy (scratch 0) (scratch 0))) a a 1 := by
+        convert (ExecWithin.copy (B := B) (w := w) (d := scratch 0) (s := scratch 0)
+          (x := a)) using 1
+        apply Data.ext <;> simp [Data.set]
+      exact ⟨a, hself, rfl, ha, by simp, fun _ _ _ => rfl⟩
+    | cons i is ih =>
+      obtain ⟨b, hb, hbm, hbs, hbo, hbf⟩ := hruni i a ha
+      obtain ⟨c, hc, hcm, hcs, hco, hcf⟩ := ih hnodup.of_cons b hbs
+      refine ⟨c, (hb.seq hc).mono (by simp; omega), hcm.trans hbm, hcs, ?_, ?_⟩
+      · intro j hj
+        rcases List.mem_cons.mp hj with rfl | hj
+        · rw [hcf _ (fun z => ?_) (fun j hj h => ?_)]
+          · exact hbo
+          · intro hh
+            have hval := congrArg (fun a : Fin (l + N + 1) => a.val) (hi hh)
+            dsimp only [scratch, dst] at hval
+            simp only [Fin.val_castAdd] at hval
+            omega
+          · exact (List.nodup_cons.mp hnodup).1 (hdsti h ▸ hj)
+        · exact hco j hj
+      · intro j hsj hdj
+        rw [hcf j hsj (fun i hi => hdj i (by simp [hi]))]
+        exact hbf j hsj (hdj i (by simp))
+  obtain ⟨y, hy, hym, _, hyo, hyf⟩ := hseq (List.finRange l) (List.nodup_finRange l) x hin
+  refine ⟨y, hy.mono ?_, ?_, fun i => hyo i (by simp), ?_⟩
+  · change ((List.finRange l).map fun i => time i + 1).sum + 1 ≤
+      1 * (0 + ((∑ i, time i) + l) + 1)
+    rw [← List.sum_toFinset (fun i => time i + 1) (List.nodup_finRange l)]
+    simp [Finset.sum_add_distrib]
+  · apply Memory.State.ext
+    · exact hym
+    · exact hyf frontier (fun _ => hf _) (fun _ _ => hf _)
+  · intro i hif htmp
+    exact hyf i (fun _ => htmp _) (fun _ _ => htmp _)
+
+/-- Add two input words when their sum fits; both projections and the addition are charged. -/
+theorem addWords {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (i j : Fin k) :
+    Realizes .exact (fun d => pure (input d i + input d j)) input
+      (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+      (fun w d _ => Fits w (input d i + input d j)) (fun _ _ => 3) := by
+  have ha : GlueComputes .exact (fun _ : Fin k → ℕ => True) (fun v => v i)
+      (fun v => v i + v j) 1 := GlueComputes.proj i (fun _ _ => Nat.le_add_right _ _)
+  have hb : GlueComputes .exact (fun _ : Fin k → ℕ => True) (fun v => v j)
+      (fun v => v i + v j) 1 := GlueComputes.proj j (fun _ _ => Nat.le_add_left _ _)
+  have h := Realizes.glue input (ha.bin_exact hb .add (fun _ _ => rfl) (fun _ _ => le_rfl))
+  exact h.consequence (fun _ _ _ _ _ hf => ⟨trivial, hf⟩) (fun _ _ => le_rfl)
+
+/-- Increment an input word with an explicit successor-fit condition and three local units. -/
+theorem increment {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (i : Fin k) :
+    Realizes .exact (fun d => pure (input d i + 1)) input
+      (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+      (fun w d _ => Fits w (input d i + 1)) (fun _ _ => 3) := by
+  have ha : GlueComputes .exact (fun _ : Fin k → ℕ => True) (fun v => v i)
+      (fun v => v i + 1) 1 := GlueComputes.proj i (fun _ _ => Nat.le_add_right _ _)
+  have hb : GlueComputes .exact (fun _ : Fin k → ℕ => True) (fun _ => 1)
+      (fun v => v i + 1) 1 := GlueComputes.const 1 (fun _ _ => by omega)
+  have h := Realizes.glue input (ha.bin_exact hb .add (fun _ _ => rfl) (fun _ _ => le_rfl))
+  exact h.consequence (fun _ _ _ _ _ hf => ⟨trivial, hf⟩) (fun _ _ => le_rfl)
+
+/-- Defined subtraction of one keeps positivity and the input-word envelope explicit. -/
+theorem decrement {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (i : Fin k) :
+    Realizes .exact (fun d => pure (input d i - 1)) input
+      (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+      (fun w d _ => 1 ≤ input d i ∧ Fits w (input d i)) (fun _ _ => 3) := by
+  have ha : GlueComputes .exact (fun v : Fin k → ℕ => 1 ≤ v i) (fun v => v i)
+      (fun v => v i) 1 := GlueComputes.proj i (fun _ _ => le_rfl)
+  have hb : GlueComputes .exact (fun v : Fin k → ℕ => 1 ≤ v i) (fun _ => 1)
+      (fun v => v i) 1 := GlueComputes.const 1 (fun _ h => h)
+  exact Realizes.glue input (ha.bin_exact hb .sub
+    (fun v h => by simp [h]) (fun _ _ => Nat.sub_le _ _))
+
+/-- Return the two zero words encoding `none`, charging both constants and output copies. -/
+theorem returnNone {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) :
+    Realizes .exact (fun _ => pure none) input optionWords
+      (fun _ _ _ => True) (fun _ _ => 4) := by
+  have h := Realizes.glueVector (B := .exact) input optionWords (fun _ => none)
+    (fun _ _ => 0) (fun _ _ => 0) (fun _ => 1)
+    (fun _ i => by fin_cases i <;> rfl)
+    (P := fun _ => True) (fun _ => GlueComputes.const 0 (fun _ _ => le_rfl))
+  exact h.consequence (fun w _ _ _ _ _ => ⟨trivial, fun _ => fits_zero w⟩)
+    (fun _ _ => by simp)
+
+/-- Return a presence tag and unshifted input payload, with both word fits explicit. -/
+theorem returnSome {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (j : Fin k) :
+    Realizes .exact (fun d => pure (some (input d j))) input optionWords
+      (fun w d _ => Fits w 1 ∧ Fits w (input d j)) (fun _ _ => 4) := by
+  let g : Fin 2 → (Fin k → ℕ) → ℕ := fun i v => if i = 0 then 1 else v j
+  have hc (i : Fin 2) : GlueComputes .exact (fun _ : Fin k → ℕ => True) (g i) (g i) 1 := by
+    fin_cases i
+    · exact GlueComputes.const 1 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj j (fun _ _ => le_rfl)
+  have h := Realizes.glueVector input optionWords (fun d => some (input d j)) g g
+    (fun _ => 1) (fun _ i => by fin_cases i <;> rfl) hc
+  apply h.consequence (hwork := fun _ _ => by simp)
+  intro w d s _ _ ⟨h1, hv⟩
+  refine ⟨trivial, fun i => ?_⟩
+  fin_cases i
+  · exact h1
+  · exact hv
+
+end Realizes
+end Cslib.WordRAM.Realization
diff --git a/ComplexityTests/WordRAMMemoryStack.lean b/ComplexityTests/WordRAMMemoryStack.lean
new file mode 100644
index 0000000000..b65055e4c1
--- /dev/null
+++ b/ComplexityTests/WordRAMMemoryStack.lean
@@ -0,0 +1,172 @@
+/-
+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.MemoryStack
+
+/-! Concrete native instances of the unchanged stack methods. The pop uses the largest four-bit
+payload, so a successor-based option encoding could not satisfy this instance. Both methods retain
+the literal inaccessible memory. These instruction bounds include certified local work. -/
+
+namespace ComplexityTests.WordRAMMemoryStack
+
+open Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+open MemoryStack
+
+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 layout (k 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
+    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 L : Stack.Memory.Layout := ⟨⟨2, 1⟩, ⟨3, 2⟩⟩
+private def empty : Memory.State := ⟨fun a => if a = 2 then 0 else 7, 8⟩
+private def singleton : Memory.State :=
+  ⟨fun a => if a = 2 then 1 else if a = 3 then 15 else 7, 8⟩
+
+private theorem valid_layout : L.Valid 4 2 := by
+  refine ⟨rfl, ?_, rfl, by decide⟩
+  change ¬(3 ≤ 2 ∧ 2 < 3 + 2)
+  omega
+
+private theorem empty_inv : Stack.Memory.Inv L empty := by
+  constructor
+  · change 2 + 1 ≤ 8; decide
+  · change 3 + 2 ≤ 8; decide
+  · change 0 ≤ 2; decide
+
+private theorem singleton_inv : Stack.Memory.Inv L singleton := by
+  constructor
+  · change 2 + 1 ≤ 8; decide
+  · change 3 + 2 ≤ 8; decide
+  · change 1 ≤ 2; decide
+
+private theorem empty_wf : Memory.WellFormed 4 empty := by
+  refine ⟨by decide, fun a => ?_⟩
+  change Fits 4 (if a = 2 then 0 else 7)
+  split <;> decide
+
+private theorem singleton_wf : Memory.WellFormed 4 singleton := by
+  refine ⟨by decide, fun a => ?_⟩
+  change Fits 4 (if a = 2 then 1 else if a = 3 then 15 else 7)
+  split
+  · decide
+  · split <;> decide
+
+-- A maximum-word push executes the generic certificate on a complete runtime layout.
+example : ∃ r C, ∃ (code : Code .exact r) (x y : Data r),
+    ExecWithin 4 code x y (C * 14) ∧ y.mem 3 = 15 ∧ y.mem 10 = 7 := by
+  obtain ⟨n, C, emit, he⟩ := realizes_push
+  let x := packed (t := 0 + n + 1) (pushWords (L, 15)) empty
+  obtain ⟨hi, hd, hf, hs⟩ := layout 5 (0 + n + 1)
+  have hx : x.Bounded 4 := packed_bounded (by intro i; fin_cases i <;> decide) empty_wf
+  have hin := packed_input (t := 0 + n + 1) (pushWords (L, 15)) empty
+  have hm := packed_state (t := 0 + n + 1) (pushWords (L, 15)) empty
+  have hsafe : L.Valid 4 L.items.length ∧ Stack.Memory.Inv L (memoryState front x) ∧
+      (memoryState front x).mem L.count.base < L.items.length := by
+    rw [hm]
+    exact ⟨valid_layout, empty_inv, by decide⟩
+  have hv : (Memory.spec 4).ValidHistory (memoryState front x)
+      ((Memory.spec 4).clientHistory (memoryState front x) (Stack.Memory.push L 15)) := by
+    rw [hm]
+    decide
+  obtain ⟨y, hy, hmem, _, _⟩ := (he front src tmp hi hd hf hs).2 4 (L, 15) x hx hin hsafe hv
+  rw [hm] at hy hmem
+  refine ⟨_, C, emit front src tmp, x, y, hy, ?_, ?_⟩
+  · exact congrArg (fun s : Memory.State => s.mem 3) hmem
+  · exact congrArg (fun s : Memory.State => s.mem 10) hmem
+
+-- One native pop body handles both actual branches. The positive branch returns the maximum
+-- word as (tag=1,payload=15), while the empty branch returns (0,0).
+example : ∃ r C, ∃ (code : Code .exact r) (x y x₀ y₀ : Data r) (tag payload : Fin r),
+    ExecWithin 4 code x y (C * 23) ∧ y.regs tag = 1 ∧ y.regs payload = 15 ∧
+      y.mem 2 = 0 ∧ y.mem 10 = 7 ∧ ExecWithin 4 code x₀ y₀ (C * 21) ∧
+      y₀.regs tag = 0 ∧ y₀.regs payload = 0 ∧ y₀.mem 10 = 7 := by
+  obtain ⟨n, C, emit, he⟩ := realizes_pop
+  let x := packed (t := 2 + n + 1) (layoutWords L) singleton
+  obtain ⟨hi, hd, hf, hs⟩ := layout 4 (2 + n + 1)
+  have hx : x.Bounded 4 := packed_bounded (by intro i; fin_cases i <;> decide) singleton_wf
+  have hin := packed_input (t := 2 + n + 1) (layoutWords L) singleton
+  have hm := packed_state (t := 2 + n + 1) (layoutWords L) singleton
+  have hsafe : L.Valid 4 L.items.length ∧ Stack.Memory.Inv L (memoryState front x) := by
+    rw [hm]
+    exact ⟨valid_layout, singleton_inv⟩
+  have hv : (Memory.spec 4).ValidHistory (memoryState front x)
+      ((Memory.spec 4).clientHistory (memoryState front x) (Stack.Memory.pop L)) := by
+    rw [hm]
+    decide
+  obtain ⟨y, hy, hmem, hout, _⟩ := (he front src tmp hi hd hf hs).2 4 L x hx hin hsafe hv
+  rw [hm] at hy hmem hout
+  let x₀ := packed (t := 2 + n + 1) (layoutWords L) empty
+  have hx₀ : x₀.Bounded 4 := packed_bounded (by intro i; fin_cases i <;> decide) empty_wf
+  have hin₀ := packed_input (t := 2 + n + 1) (layoutWords L) empty
+  have hm₀ := packed_state (t := 2 + n + 1) (layoutWords L) empty
+  have hsafe₀ : L.Valid 4 L.items.length ∧ Stack.Memory.Inv L (memoryState front x₀) := by
+    rw [hm₀]
+    exact ⟨valid_layout, empty_inv⟩
+  have hv₀ : (Memory.spec 4).ValidHistory (memoryState front x₀)
+      ((Memory.spec 4).clientHistory (memoryState front x₀) (Stack.Memory.pop L)) := by
+    rw [hm₀]
+    decide
+  obtain ⟨y₀, hy₀, hmem₀, hout₀, _⟩ :=
+    (he front src tmp hi hd hf hs).2 4 L x₀ hx₀ hin₀ hsafe₀ hv₀
+  rw [hm₀] at hy₀ hmem₀ hout₀
+  refine ⟨_, C, emit front src tmp, x, y, x₀, y₀, tmp (Fin.castAdd (n + 1) 0),
+    tmp (Fin.castAdd (n + 1) 1), hy, hout 0, hout 1, ?_, ?_, hy₀, hout₀ 0, hout₀ 1, ?_⟩
+  · exact congrArg (fun s : Memory.State => s.mem 2) hmem
+  · exact congrArg (fun s : Memory.State => s.mem 10) hmem
+  · exact congrArg (fun s : Memory.State => s.mem 10) hmem₀
+
+-- The empty path is semantically none and uses a valid, non-vacuous layout and memory state.
+example : (Memory.spec 4).clientResult empty (Stack.Memory.pop L) = none := by decide
+
+example : optionWords (some 15) = ![1, 15] ∧ Fits 4 15 ∧ ¬Fits 4 (15 + 1) := by decide
+
+end ComplexityTests.WordRAMMemoryStack
diff --git a/ComplexityTests/WordRAMRealizationGlueVector.lean b/ComplexityTests/WordRAMRealizationGlueVector.lean
new file mode 100644
index 0000000000..2ac5f49c02
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationGlueVector.lean
@@ -0,0 +1,154 @@
+/-
+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: local-only (regression clients for finite-result glue realization)
+
+public import Complexity.Computability.WordRAM.Realization.GlueVector
+
+/-!
+# Optional-word vector glue regressions
+
+Every coordinate is computed by an actual scalar certificate. `none` uses two zero constants
+and remains valid at word width zero; `some v` uses a presence constant and an unshifted word
+projection, including the maximal word. Empty results retain the charged neutral-copy case.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Tests
+
+open Cslib.DataStructure
+
+private def unitWords : Unit ↪ (Fin 0 → ℕ) :=
+  (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+private def wordInput : ℕ ↪ (Fin 1 → ℕ) :=
+  (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+private theorem none_realizes :
+    Realizes .exact (fun _ : Unit => pure (none : Option ℕ)) unitWords optionWords
+      (fun w _ _ => True ∧ ∀ _ : Fin 2, Fits w 0) (fun _ _ => 4) := by
+  have hcoord (i : Fin 2) : GlueComputes .exact (fun _ : Fin 0 → ℕ => True)
+      (fun _ => 0) (fun _ => 0) 1 := GlueComputes.const 0 (fun _ _ => le_rfl)
+  have hresult (d : Unit) (i : Fin 2) : optionWords none i = 0 := by
+    fin_cases i <;> rfl
+  simpa using Realizes.glueVector unitWords optionWords (fun _ => none)
+    (fun _ _ => 0) (fun _ _ => 0) (fun _ => 1) hresult hcoord
+
+private def someCoordinate : Fin 2 → (Fin 1 → ℕ) → ℕ := ![fun _ => 1, fun v => v 0]
+
+private theorem some_realizes :
+    Realizes .exact (fun v : ℕ => pure (some v)) wordInput optionWords
+      (fun w v _ => True ∧ Fits w 1 ∧ Fits w v) (fun _ _ => 4) := by
+  have hcoord (i : Fin 2) : GlueComputes .exact (fun _ : Fin 1 → ℕ => True)
+      (someCoordinate i) (someCoordinate i) 1 := by
+    fin_cases i
+    · exact GlueComputes.const 1 (fun _ _ => le_rfl)
+    · exact GlueComputes.proj 0 (fun _ _ => le_rfl)
+  have hresult (v : ℕ) (i : Fin 2) : optionWords (some v) i =
+      someCoordinate i (wordInput v) := by
+    fin_cases i <;> rfl
+  simpa [someCoordinate, wordInput, Fin.forall_fin_succ] using
+    Realizes.glueVector wordInput optionWords some someCoordinate someCoordinate
+      (fun _ => 1) hresult hcoord
+
+private theorem unit_realizes :
+    Realizes .exact (fun _ : Unit => pure ()) unitWords unitWords
+      (fun _ _ _ => True ∧ True) (fun _ _ => 0) := by
+  have hcoord (i : Fin 0) : GlueComputes .exact (fun _ : Fin 0 → ℕ => True)
+      (Fin.elim0 i) (Fin.elim0 i) (Fin.elim0 i) := Fin.elim0 i
+  have hresult (d : Unit) (i : Fin 0) :
+      unitWords () i = (Fin.elim0 i : (Fin 0 → ℕ) → ℕ) (unitWords d) :=
+    Fin.elim0 i
+  simpa using Realizes.glueVector unitWords unitWords (fun _ => ())
+    Fin.elim0 Fin.elim0 Fin.elim0 hresult hcoord
+
+/-- The optional payload is not shifted, so the maximal two-bit word is retained. -/
+theorem optionWords_some_max : optionWords (some 3) = ![1, 3] := rfl
+
+example : optionWords none ≠ optionWords (some 0) := by decide
+example : ¬Fits 0 (optionWords (some 0) 0) := by decide
+example : Fits 2 (optionWords (some 3) 0) ∧ Fits 2 (optionWords (some 3) 1) := by decide
+
+/-- The certified two-coordinate `none` emitter actually executes at width zero. -/
+example : ∃ r, ∃ p : Program .exact r, ∃ steps,
+    Executes 0 p ⟨0, ⟨fun _ => 0, fun _ => 0⟩⟩ 0 steps := by
+  obtain ⟨n, C, emit, he⟩ := none_realizes
+  let r := (2 + n + 1) + 1
+  let frontier : Fin r := ⟨r - 1, by omega⟩
+  let src : Fin 0 → Fin r := Fin.elim0
+  let tmp : Fin (2 + n + 1) → Fin r := fun i => ⟨i.val, by omega⟩
+  have hi : Function.Injective tmp := by
+    intro i j h
+    apply Fin.ext
+    exact congrArg (fun i : Fin r => i.val) h
+  have hf (j : Fin (2 + n + 1)) : tmp j ≠ frontier := by
+    intro h
+    have hh := congrArg (fun i : Fin r => i.val) h
+    dsimp only [tmp, frontier, r] at hh
+    omega
+  let x : Data r := ⟨fun _ => 0, fun _ => 0⟩
+  have hx : x.Bounded 0 := ⟨fun _ => fits_zero 0, fun _ => fits_zero 0⟩
+  have hin : x.regs ∘ src = unitWords () := Subsingleton.elim _ _
+  obtain ⟨y, ⟨steps, _, hy⟩, _, hout, _⟩ :=
+    (he frontier src tmp hi (fun i => Fin.elim0 i) hf (fun i => Fin.elim0 i)).2
+      0 () x hx hin ⟨trivial, fun _ => fits_zero 0⟩ trivial
+  have ho : y.regs (tmp 0) = 0 := hout 0
+  refine ⟨r, (emit frontier src tmp).program (tmp 0), steps + 1, ?_⟩
+  simpa only [ho] using hy.executes (tmp 0)
+
+example : boolWords false = ![0, 0] := rfl
+example : Fits 0 (boolWords false 0) ∧ Fits 0 (boolWords false 1) := by decide
+example : ¬Fits 0 (boolWords true 0) := by decide
+
+/-- The certified payload emitter returns the maximal two-bit word without incrementing it. -/
+example : ∃ r, ∃ p : Program .exact r, ∃ x : Data r, ∃ steps,
+    x.Bounded 2 ∧ Executes 2 p ⟨0, x⟩ 3 steps := by
+  obtain ⟨n, C, emit, he⟩ := some_realizes
+  let r := 1 + (2 + n + 1) + 1
+  let frontier : Fin r := ⟨r - 1, by omega⟩
+  let src : Fin 1 → Fin r := fun i => ⟨i.val, by omega⟩
+  let tmp : Fin (2 + n + 1) → Fin r := fun i => ⟨1 + i.val, by omega⟩
+  have hi : Function.Injective tmp := by
+    intro i j h
+    apply Fin.ext
+    have hh := congrArg (fun i : Fin r => i.val) h
+    dsimp only [tmp] at hh
+    omega
+  have hd (i : Fin 1) (j : Fin (2 + n + 1)) : src i ≠ tmp j := by
+    intro h
+    have hh := congrArg (fun i : Fin r => i.val) h
+    dsimp only [src, tmp] at hh
+    omega
+  have hf (j : Fin (2 + n + 1)) : tmp j ≠ frontier := by
+    intro h
+    have hh := congrArg (fun i : Fin r => i.val) h
+    dsimp only [tmp, frontier, r] at hh
+    omega
+  have hs (i : Fin 1) : src i ≠ frontier := by
+    intro h
+    have hh := congrArg (fun i : Fin r => i.val) h
+    dsimp only [src, frontier, r] at hh
+    omega
+  let x : Data r := ⟨fun i => if i = src 0 then 3 else 0, fun _ => 0⟩
+  have hx : x.Bounded 2 := by
+    refine ⟨fun i => ?_, fun _ => fits_zero 2⟩
+    change Fits 2 (if i = src 0 then 3 else 0)
+    split_ifs <;> decide
+  have hin : x.regs ∘ src = wordInput 3 := by
+    funext i
+    have hi : i = 0 := Fin.eq_zero i
+    subst i
+    simp [x, wordInput]
+  obtain ⟨y, ⟨steps, _, hy⟩, _, hout, _⟩ :=
+    (he frontier src tmp hi hd hf hs).2 2 3 x hx hin ⟨trivial, by decide, by decide⟩ trivial
+  let out := tmp (Fin.castAdd (n + 1) (1 : Fin 2))
+  have ho : y.regs out = 3 := hout 1
+  refine ⟨r, (emit frontier src tmp).program out, x, steps + 1, hx, ?_⟩
+  simpa only [ho] using hy.executes out
+
+end Cslib.WordRAM.Realization.Tests
diff --git a/ROADMAP.md b/ROADMAP.md
index 5d3937849b..bc3680623c 100644
--- a/ROADMAP.md
+++ b/ROADMAP.md
@@ -646,7 +646,9 @@ reusing graph and matroid foundations and the shared data-structure interfaces.
   with explicit input layout, fits and safe-domain hypotheses. A separate operation-level
   memory implementation exposes body-only costs under delivered arguments. Existing framed
   Word-RAM certificates can be derived from semantic modules after discharging their local
-  initialization, footprint and ABI conditions; a one-cell ADT checks that boundary. Remaining:
+  initialization, footprint and ABI conditions; a one-cell ADT checks that boundary. Multiword
+  glue preserves full-word Option payloads, and the actual memory-stack size/push/pop methods
+  have uniform native certificates over runtime layouts, with local work 0/10/19. Remaining:
   the representative framed queue and its faithful whole-memory 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
diff --git a/UPSTREAM.md b/UPSTREAM.md
index 40197480d9..b71c6e87c8 100644
--- a/UPSTREAM.md
+++ b/UPSTREAM.md
@@ -550,6 +550,10 @@ Do not add a ledger row for an ordinary candidate or repeat its source marker he
   initialization/locality bundle and semantic module; its argument map instantiates one global
   emitter rather than selecting code after runtime layouts. Combined cost takes the program and
   an explicit work grading, with a separately proved envelope before dropping local work.
+  Certified coordinate-wise glue stages multiword results with every copy charged; Option
+  values use a tag and unshifted payload, including maximal fitting words. The actual
+  `Stack.Memory` size/push/pop clients reuse those rules over faithfully encoded runtime layouts,
+  with visible layout/representation/spare-capacity conditions and local work 0/10/19.
   The full framed queue/faithful allocation client remains separate. No abstract headline is added.
   `DataStructure/OrderedSet` and `DataStructure/OrderedSet/*` provide neutral
   optional-minimum contracts, a typed finite-set interface including deletion, and adaptive