diff --git a/Complexity.lean b/Complexity.lean
index b988a1c9a7..7012a36253 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2626,10 +2626,12 @@ public import Complexity.Computability.WordRAM.Randomized.LoopSegment
 public import Complexity.Computability.WordRAM.Randomized.Structured
 public import Complexity.Computability.WordRAM.Randomized.UniformLoopExit
 public import Complexity.Computability.WordRAM.Realization.Absorb
+public import Complexity.Computability.WordRAM.Realization.Backend
 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.Function
 public import Complexity.Computability.WordRAM.Realization.Glue
 public import Complexity.Computability.WordRAM.Realization.GlueVector
 public import Complexity.Computability.WordRAM.Realization.Grade
diff --git a/Complexity/Computability/WordRAM/Realization/Backend.lean b/Complexity/Computability/WordRAM/Realization/Backend.lean
new file mode 100644
index 0000000000..881155547c
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Backend.lean
@@ -0,0 +1,456 @@
+/-
+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.Witness
+public import Complexity.DataStructure.StateTransition.Refinement
+public import Complexity.DataStructure.StateTransition.Resource
+
+/-!
+# Native implementations of refinements, one realized body per operation constructor
+
+`MemoryBackend` runs each memory operation as the static body of a primitive realization, chosen
+by the operation's constructor. `Backend` does the same for any specification `D` refined to the
+memory oracle by a `Refinement D (Memory.spec w)`. One `Realizes` certificate per constructor tag
+supplies the body; the refinement supplies correctness and memory charges.
+
+A `Certificate` bundles one realization with its program, encodings, domain and local work. A
+family `C : ι → Certificate B` over a finite type of tags fixes one register file, one body per
+tag and one exchange factor (`Backend.registers`, `Backend.code`, `Backend.factor`), before every
+width, refinement, runtime layout and argument. A `Backend D C` says which tag each operation of
+`D` selects (`tag`), which arguments the tag's program receives (`arg`, which may include the
+structure's runtime layout), and how the program's result gives the specified answer (`answer`).
+The result encoding belongs to the tag, so an operation's arguments are never encoded in its
+result; the native code never dispatches on the operation.
+
+`Backend.Implements` connects a backend to a refinement: each method runs the selected program
+and maps its result by `answer`, and from an admissible state the arguments are words and the
+program's domain holds. Then `Backend.implementation` is a `StateTransitionImpl D` with a
+functional representation: the memory satisfies the refinement's invariant and abstracts to the
+state, and every register and cell holds a word. Instruction counts follow from the refinement's
+amortized memory charges (`Backend.amortized`), and are constant per operation when those charges
+are constant and need no potential (`Backend.bound`). Backends of two specifications run their
+product side by side (`Backend.sum`), with tags in a sum type: the operation's `Sum` constructor
+selects the family, and no native code dispatches on it.
+
+As in `MemoryBackend`, the selected tag's arguments are installed in registers before its body
+runs, uncharged, as a calling convention; decoding the answer executes no instruction. Bounds
+count the body's instructions only.
+
+Memory charges do not depend on the word width (`totalCost_width`, `memoryCost_eq_totalCost`),
+so `memoryCost`, which is taken at width zero, is the charge that refinements state at width `w`.
+
+## Main definitions
+
+* `Certificate`: a realization certificate with its program, encodings, domain and work.
+* `Backend.registers`, `Backend.frontier`, `Backend.code`, `Backend.factor`: the register file,
+  the body of each tag and one exchange factor.
+* `Backend.data`: the native data holding a memory state.
+* `Backend`: the tag, arguments and answer of each operation.
+* `Backend.Implements`: a backend runs the methods of a refinement.
+* `Backend.sum`: two backends side by side, for a product specification.
+* `Backend.exec`, `Backend.implementation`: native execution, and the native implementation.
+
+## Main results
+
+* `totalCost_width`, `clientHistory_width`, `memoryCost_eq_totalCost`: memory charges do not
+  depend on the word width.
+* `fits_appendWords`: appended argument words fit when both parts do.
+* `Backend.Implements.prod`: side-by-side backends run a product of refinements.
+* `Backend.exec_iff`, `Backend.rep_iff`: the execution relation and representation, unfolded.
+* `Backend.rep_data`: the data holding an invariant state represents its abstraction.
+* `Backend.exec_memoryState`: an operation leaves its method's final memory.
+* `Backend.amortized`, `Backend.bound`: amortized and worst-case instruction bounds.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+/-! ## Memory charges and the word width -/
+
+/-- Memory charges along a history do not depend on the word width. -/
+theorem totalCost_width (w : ℕ) (s : Memory.State) (os : List Memory.Op) :
+    (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 => exact congrArg (Memory.charge s o + ·) (ih _)
+
+/-- The memory history of a client does not depend on the word width. -/
+theorem clientHistory_width {α : Type} (w : ℕ) (p : Memory.Prog α) (s : Memory.State) :
+    (Memory.spec w).clientHistory s p = (Memory.spec 0).clientHistory s p :=
+  congrArg (fun t => t.2.2) (runClient_width w p s)
+
+/-- `memoryCost` is the memory charge of the client's history at every word width. -/
+theorem memoryCost_eq_totalCost {α : Type} (w : ℕ) (p : Memory.Prog α) (s : Memory.State) :
+    memoryCost p s =
+      (Memory.spec w).totalCost Memory.charge s ((Memory.spec w).clientHistory s p) := by
+  rw [totalCost_width, clientHistory_width]
+  rfl
+
+/-- Appended argument words fit when both parts do. -/
+theorem fits_appendWords {δ α : Type} {k l w : ℕ} (input : δ ↪ (Fin k → ℕ))
+    (output : α ↪ (Fin l → ℕ)) {d : δ} {a : α} (h₁ : ∀ i, Fits w (input d i))
+    (h₂ : ∀ i, Fits w (output a i)) : ∀ i, Fits w (appendWords input output (d, a) i) :=
+  Fin.addCases (fun i => by simpa [appendWords, Fin.appendEquiv] using h₁ i)
+    (fun i => by simpa [appendWords, Fin.appendEquiv] using h₂ i)
+
+/-! ## Certificates and backends -/
+
+/-- A uniform realization certificate, bundled with the program it realizes, its argument and
+result encodings, its entry domain and its local work. -/
+structure Certificate (B : Basis) where
+  /-- The argument type. -/
+  {Arg : Type}
+  /-- The result type. -/
+  {Res : Type}
+  /-- The number of argument words. -/
+  {k : ℕ}
+  /-- The number of result words. -/
+  {l : ℕ}
+  /-- The realized memory program. -/
+  {prog : Arg → Memory.Prog Res}
+  /-- The faithful argument encoding. -/
+  {input : Arg ↪ (Fin k → ℕ)}
+  /-- The faithful result encoding. -/
+  {output : Res ↪ (Fin l → ℕ)}
+  /-- The entry domain. -/
+  {safe : ℕ → Arg → Memory.State → Prop}
+  /-- The certified local work. -/
+  {work : Arg → Memory.State → ℕ}
+  /-- The realization. -/
+  realizes : Realizes B prog input output safe work
+
+variable {B : Basis} {ι : Type}
+
+/-- How the operations of `D` run on the bodies of `C`: each operation selects a tag, passes
+arguments to the tag's program and reads its answer from that program's result. Only the tag
+selects code. -/
+structure Backend (D : StateTransitionSpec.{0, 0, 0}) (C : ι → Certificate B) where
+  /-- The tag of each operation, typically its constructor. -/
+  tag : D.Op → ι
+  /-- The arguments of the selected program, including any runtime layout. -/
+  arg : ∀ o, (C (tag o)).Arg
+  /-- The specified answer, read off the selected program's result. -/
+  answer : ∀ o, (C (tag o)).Res → D.Result o
+
+namespace Backend
+
+section Registers
+
+variable [Fintype ι] (C : ι → Certificate B)
+
+/-- Registers for the longest argument vector. -/
+noncomputable def argWords : ℕ := Finset.univ.sup fun i => (C i).k
+
+/-- Registers for the largest result and scratch bank. -/
+noncomputable def scratchWords : ℕ :=
+  Finset.univ.sup fun i => (C i).l + (C i).realizes.scratchSize + 1
+
+/-- One register count, chosen before every width, refinement, layout and argument. -/
+noncomputable def registers : ℕ := argWords C + scratchWords C + 1
+
+/-- Register zero holds the allocation frontier. -/
+def frontier : Fin (registers C) := ⟨0, by unfold registers; omega⟩
+
+/-- The argument registers of tag `i`, from register one. -/
+def src (i : ι) (j : Fin (C i).k) : Fin (registers C) :=
+  ⟨j.val + 1, by
+    have := Finset.le_sup (f := fun i => (C i).k) (Finset.mem_univ i)
+    have := j.isLt
+    unfold registers argWords at *
+    omega⟩
+
+/-- The result and scratch registers of tag `i`, after all argument registers. -/
+noncomputable def tmp (i : ι) (j : Fin ((C i).l + (C i).realizes.scratchSize + 1)) :
+    Fin (registers C) :=
+  ⟨argWords C + 1 + j.val, by
+    have := Finset.le_sup (f := fun i => (C i).l + (C i).realizes.scratchSize + 1)
+      (Finset.mem_univ i)
+    have := j.isLt
+    unfold registers scratchWords at *
+    omega⟩
+
+/-- The static body of tag `i`. -/
+noncomputable def code (i : ι) : Code B (registers C) :=
+  (C i).realizes.code (frontier C) (src C i) (tmp C i)
+
+/-- One exchange factor for every tag. -/
+noncomputable def factor : ℕ := Finset.univ.sup fun i => (C i).realizes.factor
+
+/-- Each tag's exchange factor is at most the common one. -/
+theorem factor_le (i : ι) : (C i).realizes.factor ≤ factor C :=
+  Finset.le_sup (f := fun i => (C i).realizes.factor) (Finset.mem_univ i)
+
+/-- The native data holding the memory state `s`: its cells, the frontier in its register, and
+zero in every other register. A calling-convention state, not an allocation. -/
+noncomputable def data (s : Memory.State) : Data (registers C) where
+  regs i := if i = frontier C then s.frontier else 0
+  mem := s.mem
+
+/-- The data holding `s` abstracts to `s`. -/
+@[simp] theorem memoryState_data (s : Memory.State) : memoryState (frontier C) (data C s) = s :=
+  Memory.State.ext rfl (by simp [memoryState, data])
+
+/-- The data holding a well-formed memory state is word-bounded. -/
+theorem bounded_data {w : ℕ} {s : Memory.State} (hs : Memory.WellFormed w s) :
+    (data C s).Bounded w := by
+  refine ⟨fun i => ?_, hs.mem_fits⟩
+  simp only [data]
+  split
+  · exact hs.frontier_fits
+  · exact fits_zero w
+
+private theorem layout (i : ι) :
+    Function.Injective (tmp C i) ∧ (∀ a b, src C i a ≠ tmp C i b) ∧
+      (∀ b, tmp C i b ≠ frontier C) ∧ ∀ a, src C i a ≠ frontier C := by
+  have hk := Finset.le_sup (f := fun i => (C i).k) (Finset.mem_univ i)
+  refine ⟨fun a b h => Fin.ext ?_, fun a b h => ?_, fun b h => ?_, fun a h => ?_⟩ <;>
+    have := congrArg Fin.val h <;> simp only [src, tmp, frontier, argWords] at * <;> omega
+
+end Registers
+
+variable {C : ι → Certificate B} {D : StateTransitionSpec.{0, 0, 0}} (S : Backend D C)
+
+/-- A backend runs the methods of `R`: each method is the selected program with its result
+mapped by `answer`, and from an admissible state the arguments are words and the program's
+domain holds. -/
+structure Implements {w : ℕ} (R : Refinement D (Memory.spec w)) : Prop where
+  /-- Each method runs the selected program and answers through `answer`. -/
+  run : ∀ o s, (Memory.spec w).runClient s (R.methods o) =
+    Prod.map (S.answer o) id ((Memory.spec w).runClient s ((C (S.tag o)).prog (S.arg o)))
+  /-- From an admissible state, the arguments fit words and the program's domain holds. -/
+  entry : ∀ {e} o, Memory.WellFormed w e → R.inv e → D.valid (R.abs e) o →
+    (∀ j, Fits w ((C (S.tag o)).input (S.arg o) j)) ∧ (C (S.tag o)).safe w (S.arg o) e
+
+/-! ### Products -/
+
+section Sum
+
+variable {ι' : Type} {C' : ι' → Certificate B} {D' : StateTransitionSpec.{0, 0, 0}}
+
+/-- Two backends side by side run the product specification: a left operation selects a left
+tag and a right operation a right tag. -/
+def sum (S' : Backend D' C') : Backend (product D D') (Sum.elim C C') where
+  tag := Sum.map S.tag S'.tag
+  arg
+    | .inl o => S.arg o
+    | .inr o => S'.arg o
+  answer
+    | .inl o => S.answer o
+    | .inr o => S'.answer o
+
+/-- Side-by-side backends run the product of two non-interfering refinements, whatever their
+joint invariant `J`. -/
+theorem Implements.prod {w : ℕ} {S : Backend D C} {S' : Backend D' C'}
+    {R : Refinement D (Memory.spec w)} {R' : Refinement D' (Memory.spec w)}
+    {J : Memory.State → Prop}
+    {frame₁ : ∀ {e} o {a e' tr}, R.inv e → R'.inv e → J e → D.valid (R.abs e) o →
+      (Memory.spec w).ClientRun e (R.methods o) a e' tr → R'.abs e' = R'.abs e ∧ R'.inv e' ∧ J e'}
+    {frame₂ : ∀ {e} o {a e' tr}, R.inv e → R'.inv e → J e → D'.valid (R'.abs e) o →
+      (Memory.spec w).ClientRun e (R'.methods o) a e' tr → R.abs e' = R.abs e ∧ R.inv e' ∧ J e'}
+    (hS : S.Implements R) (hS' : S'.Implements R') :
+    (S.sum S').Implements (R.prod R' J frame₁ frame₂) where
+  run
+    | .inl o, s => hS.run o s
+    | .inr o, s => hS'.run o s
+  entry
+    | .inl o, hw, hi, hv => hS.entry o hw hi.1 hv
+    | .inr o, hw, hi, hv => hS'.entry o hw hi.2.1 hv
+
+end Sum
+
+/-! ### Native execution -/
+
+variable [Fintype ι]
+
+/-- Install the selected program's arguments in its argument registers. Installation is
+uncharged and leaves memory and the frontier unchanged. -/
+def prepare (o : D.Op) (x : Data (registers C)) : Data (registers C) where
+  regs j := if h : 0 < j.val ∧ j.val ≤ (C (S.tag o)).k then
+      (C (S.tag o)).input (S.arg o) ⟨j.val - 1, by omega⟩
+    else x.regs j
+  mem := x.mem
+
+/-- An operation runs the body of its tag from the prepared data, in the counted number of
+instructions, and its answer is read off the encoded result. -/
+def exec (w : ℕ) : Execution D (Data (registers C)) ℕ :=
+  fun x o a y n => Exec w (code C (S.tag o)) (S.prepare o x) y n ∧
+    ∃ b, a = S.answer o b ∧ ∀ j, y.regs (tmp C (S.tag o)
+      (Fin.castAdd ((C (S.tag o)).realizes.scratchSize + 1) j)) = (C (S.tag o)).output b j
+
+/-- The execution relation, unfolded. -/
+theorem exec_iff (w : ℕ) (x y : Data (registers C)) (o : D.Op) (a : D.Result o) (n : ℕ) :
+    S.exec w x o a y n ↔ Exec w (code C (S.tag o)) (S.prepare o x) y n ∧
+      ∃ b, a = S.answer o b ∧ ∀ j, y.regs (tmp C (S.tag o)
+        (Fin.castAdd ((C (S.tag o)).realizes.scratchSize + 1) j)) =
+          (C (S.tag o)).output b j := Iff.rfl
+
+variable {S} {w : ℕ} {R : Refinement D (Memory.spec w)}
+
+private theorem prepare_memoryState (o : D.Op) (x : Data (registers C)) :
+    memoryState (frontier C) (S.prepare o x) = memoryState (frontier C) x := by
+  apply Memory.State.ext rfl
+  simp [memoryState, prepare, frontier]
+
+private theorem prepare_src (o : D.Op) (x : Data (registers C)) :
+    (S.prepare o x).regs ∘ src C (S.tag o) = (C (S.tag o)).input (S.arg o) := by
+  funext j
+  simp [prepare, src]
+
+private theorem prepare_bounded {o : D.Op} {x : Data (registers C)} (hx : x.Bounded w)
+    (hin : ∀ j, Fits w ((C (S.tag o)).input (S.arg o) j)) : (S.prepare o x).Bounded w := by
+  refine ⟨fun j => ?_, hx.2⟩
+  simp only [prepare]
+  split
+  · exact hin _
+  · exact hx.1 j
+
+/-- One operation from represented data: its body's execution, instruction count, memory,
+encoded result and answer. -/
+private theorem exists_body (hS : S.Implements R) (o : D.Op) {x : Data (registers C)}
+    (hi : R.inv (memoryState (frontier C) x)) (hx : x.Bounded w)
+    (hv : D.valid (R.abs (memoryState (frontier C) x)) o) :
+    ∃ y n, Exec w (code C (S.tag o)) (S.prepare o x) y n ∧
+      n ≤ factor C * ((Memory.spec w).totalCost Memory.charge (memoryState (frontier C) x)
+          ((Memory.spec w).clientHistory (memoryState (frontier C) x) (R.methods o)) +
+        (C (S.tag o)).work (S.arg o) (memoryState (frontier C) x) + 1) ∧
+      memoryState (frontier C) y =
+        (Memory.spec w).clientState (memoryState (frontier C) x) (R.methods o) ∧
+      (∀ j, y.regs (tmp C (S.tag o) (Fin.castAdd ((C (S.tag o)).realizes.scratchSize + 1) j)) =
+        (C (S.tag o)).output
+          ((Memory.spec w).clientResult (memoryState (frontier C) x)
+            ((C (S.tag o)).prog (S.arg o))) j) ∧
+      S.answer o ((Memory.spec w).clientResult (memoryState (frontier C) x)
+          ((C (S.tag o)).prog (S.arg o))) =
+        (Memory.spec w).clientResult (memoryState (frontier C) x) (R.methods o) ∧
+      y.Bounded w ∧
+      (Memory.spec w).ValidHistory (memoryState (frontier C) x)
+        ((Memory.spec w).clientHistory (memoryState (frontier C) x) (R.methods o)) := by
+  have hrun := hS.run o (memoryState (frontier C) x)
+  have hvalid := ((Memory.spec w).demonicValid_iff_validHistory_runClient _ _).mp
+    (R.valid o hi hv)
+  obtain ⟨hin, hsafe⟩ := hS.entry o (wellFormed_memoryState hx) hi hv
+  have hb := prepare_bounded hx hin
+  have hp := prepare_memoryState (S := S) o x
+  obtain ⟨hi', hd, hf, hs⟩ := layout C (S.tag o)
+  have hhist : (Memory.spec w).clientHistory (memoryState (frontier C) x) (R.methods o) =
+      (Memory.spec w).clientHistory (memoryState (frontier C) x)
+        ((C (S.tag o)).prog (S.arg o)) := congrArg (fun t => t.2.2) hrun
+  obtain ⟨y, ⟨n, hn, he⟩, hm, hout, -⟩ :=
+    ((C (S.tag o)).realizes.code_spec (frontier C) (src C _) (tmp C _) hi' hd hf hs).2 w
+      (S.arg o) _ hb (prepare_src o x) (hp ▸ hsafe) (hp ▸ hhist ▸ hvalid)
+  rw [hp] at hn hm hout
+  refine ⟨y, n, he, hn.trans ?_, hm.trans (congrArg (fun t => t.2.1) hrun).symm, hout,
+    (congrArg Prod.fst hrun).symm, he.bounded hb, hvalid⟩
+  rw [memoryCost_eq_totalCost w, ← hhist]
+  exact Nat.mul_le_mul_right _ (factor_le C _)
+
+/-- The answer of an execution is the method's result. -/
+private theorem answer_eq (hS : S.Implements R) {o : D.Op} {x y : Data (registers C)}
+    {a : D.Result o} {n : ℕ} (he : S.exec w x o a y n)
+    (hout : ∀ j, y.regs (tmp C (S.tag o) (Fin.castAdd ((C (S.tag o)).realizes.scratchSize + 1) j)) =
+      (C (S.tag o)).output
+        ((Memory.spec w).clientResult (memoryState (frontier C) x)
+          ((C (S.tag o)).prog (S.arg o))) j) :
+    a = (Memory.spec w).clientResult (memoryState (frontier C) x) (R.methods o) := by
+  obtain ⟨-, b, rfl, hb⟩ := he
+  rw [(C (S.tag o)).output.injective (funext fun j => (hb j).symm.trans (hout j))]
+  exact (congrArg Prod.fst (hS.run o _)).symm
+
+/-- The native implementation: represented data holds a memory that satisfies the refinement's
+invariant and abstracts to the state, and every register and cell holds a word. -/
+noncomputable def implementation (hS : S.Implements R) : StateTransitionImpl D (S.exec w) where
+  rep s x := R.inv (memoryState (frontier C) x) ∧ R.abs (memoryState (frontier C) x) = s ∧
+    x.Bounded w
+  total o hr hv := by
+    obtain ⟨hi, rfl, hx⟩ := hr
+    obtain ⟨y, n, he, -, -, hout, -⟩ := exists_body hS o hi hx hv
+    exact ⟨_, y, n, he, _, rfl, hout⟩
+  correct {s x o a y n} hr hv he := by
+    obtain ⟨hi, rfl, hx⟩ := hr
+    obtain ⟨y', n', he', -, hm, hout, -, hb, hvalid⟩ := exists_body hS o hi hx hv
+    obtain ⟨rfl, rfl⟩ := he.1.unique he'
+    have ha := answer_eq hS he hout
+    obtain ⟨hstep, hi'⟩ := R.correct o hi hv ((Memory.spec w).clientRun_canonical _ _ hvalid)
+    exact ⟨_, ha ▸ hstep, hm ▸ hi', by rw [hm], hb⟩
+
+/-- The representation, unfolded. -/
+theorem rep_iff (hS : S.Implements R) (s : D.State) (x : Data (registers C)) :
+    (implementation hS).rep s x ↔ R.inv (memoryState (frontier C) x) ∧
+      R.abs (memoryState (frontier C) x) = s ∧ x.Bounded w := Iff.rfl
+
+/-- The data holding a well-formed memory state that satisfies the invariant represents its
+abstraction. -/
+theorem rep_data (hS : S.Implements R) {e : Memory.State} {s : D.State}
+    (hw : Memory.WellFormed w e) (hi : R.inv e) (ha : R.abs e = s) :
+    (implementation hS).rep s (data C e) := by
+  refine (rep_iff hS s _).mpr ⟨?_, ?_, bounded_data C hw⟩ <;> rw [memoryState_data] <;> assumption
+
+/-- An operation leaves the memory and frontier of its method. -/
+theorem exec_memoryState (hS : S.Implements R) {s : D.State} {x y : Data (registers C)}
+    {o : D.Op} {a : D.Result o} {n : ℕ} (hr : (implementation hS).rep s x) (hv : D.valid s o)
+    (he : S.exec w x o a y n) :
+    memoryState (frontier C) y =
+      (Memory.spec w).clientState (memoryState (frontier C) x) (R.methods o) := by
+  obtain ⟨hi, rfl, hx⟩ := hr
+  obtain ⟨y', n', he', -, hm, -⟩ := exists_body hS o hi hx hv
+  obtain ⟨rfl, -⟩ := he.1.unique he'
+  exact hm
+
+/-- **Amortized instructions.** Memory charges with a potential, plus local work at most `c`,
+give native instruction counts with the potential scaled by the exchange factor. -/
+theorem amortized (hS : S.Implements R) {upper : D.State → D.Op → ℕ}
+    {Φ : Memory.State → ℕ} (A : R.Amortized Memory.charge upper Φ) (c : ℕ)
+    (hwork : ∀ {e} o, R.inv e → D.valid (R.abs e) o → (C (S.tag o)).work (S.arg o) e ≤ c) :
+    DataStructure.Amortized (implementation hS) id
+      (fun _ x => factor C * Φ (memoryState (frontier C) x))
+      (fun s o => factor C * (upper s o + c + 1)) where
+  step {s x o a y n} hr hv he := by
+    obtain ⟨hi, rfl, hx⟩ := hr
+    obtain ⟨y', n', he', hn, hm, hout, -, hb, hvalid⟩ := exists_body hS o hi hx hv
+    obtain ⟨rfl, rfl⟩ := he.1.unique he'
+    have ha := answer_eq hS he hout
+    have hrun := (Memory.spec w).clientRun_canonical _ _ hvalid
+    obtain ⟨hstep, hi'⟩ := R.correct o hi hv hrun
+    have hA := A.step o hi hv hrun
+    rw [StateTransitionSpec.totalCostTranscript_canonicalTranscript, ← hm] at hA
+    have hw := hwork o hi hv
+    refine ⟨_, ha ▸ hstep, ⟨hm ▸ hi', by rw [hm], hb⟩, ?_⟩
+    change n + _ ≤ _
+    calc n + factor C * Φ (memoryState (frontier C) y)
+        ≤ factor C * ((Memory.spec w).totalCost Memory.charge (memoryState (frontier C) x)
+            ((Memory.spec w).clientHistory (memoryState (frontier C) x) (R.methods o)) +
+          (C (S.tag o)).work (S.arg o) (memoryState (frontier C) x) + 1) +
+          factor C * Φ (memoryState (frontier C) y) := Nat.add_le_add_right hn _
+      _ = factor C * ((Memory.spec w).totalCost Memory.charge (memoryState (frontier C) x)
+            ((Memory.spec w).clientHistory (memoryState (frontier C) x) (R.methods o)) +
+          Φ (memoryState (frontier C) y) +
+          (C (S.tag o)).work (S.arg o) (memoryState (frontier C) x) + 1) := by ring
+      _ ≤ factor C * (upper (R.abs (memoryState (frontier C) x)) o +
+          Φ (memoryState (frontier C) x) + c + 1) := Nat.mul_le_mul_left _ (by omega)
+      _ = factor C * (upper (R.abs (memoryState (frontier C) x)) o + c + 1) +
+          factor C * Φ (memoryState (frontier C) x) := by ring
+
+/-- **Worst-case instructions.** Memory charges at most `upper` without a potential, plus local
+work at most `c`, bound every operation's instructions by `factor C * (upper + c + 1)`. With a
+constant `upper` this is one constant for every width and refinement. -/
+theorem bound (hS : S.Implements R) {upper : D.State → D.Op → ℕ}
+    (A : R.Amortized Memory.charge upper fun _ => 0) (c : ℕ)
+    (hwork : ∀ {e} o, R.inv e → D.valid (R.abs e) o → (C (S.tag o)).work (S.arg o) e ≤ c) :
+    Bound (implementation hS) id fun s o => factor C * (upper s o + c + 1) := by
+  intro s x o a y n hr hv he
+  obtain ⟨-, -, -, hcost⟩ := (amortized hS A c hwork).step hr hv he
+  simpa only [id, Nat.mul_zero, Nat.add_zero] using hcost
+
+end Backend
+
+end Cslib.WordRAM.Realization
diff --git a/Complexity/Computability/WordRAM/Realization/Function.lean b/Complexity/Computability/WordRAM/Realization/Function.lean
new file mode 100644
index 0000000000..2e583cc370
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Function.lean
@@ -0,0 +1,87 @@
+/-
+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.Function
+public import Complexity.Computability.WordRAM.MapOp
+public import Complexity.Computability.WordRAM.Realization.Program
+public import Complexity.Computability.WordRAM.Realization.Witness
+
+/-!
+# Functions computed by realized memory clients
+
+`Realizes.uniformComputableInPolyTime` turns one realization certificate into
+`UniformComputableInPolyTime`. The flat program is the certificate's emitted body, preceded by
+the charged argument-installation prefix `inputPrefix` and followed by a halt on one result
+coordinate; it is chosen before every width and input. The client supplies the input layout and
+an entry width and, at every admitted width, the program's domain, its admissible history, its
+answer and a polynomial bound on its memory charge plus local work. A basis simulation carries
+the exact-basis code to the target basis.
+
+## Main results
+
+* `Realizes.uniformComputableInPolyTime`: uniform polynomial time from a realization.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization.Realizes
+
+open Cslib.DataStructure
+
+variable {δ α : Type} {k l : ℕ} {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)}
+  {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop}
+  {work : δ → Memory.State → ℕ}
+
+/-- **Uniform polynomial time from a realization.** If the first `k` input words encode the
+argument, and at every width admitted by `logWidth c` the input fits, the program's domain and
+admissible history hold, result coordinate `i` is the function's value, and the memory charge
+plus local work is at most `T (size d)` for a polynomially bounded `T`, then one flat program
+computes the function in polynomial time. Argument installation and the halt are charged. -/
+theorem uniformComputableInPolyTime {B : Basis} (φ : Basis.exact.Simulates B)
+    (h : Realizes .exact p input output safe work) (i : Fin l)
+    {f : δ → ℕ} {encode : ℕ → δ → List ℕ} {size : δ → ℕ} {T : ℕ → ℕ}
+    (hT : PolynomiallyBounded T) (c : ℕ) (hc : 0 < c)
+    (hlayout : ∀ w d (j : Fin k), (encode w d).getD j.val 0 = input d j)
+    (hspec : ∀ d w, logWidth c (size d) ≤ w → InputFits w (encode w d) →
+      k ≤ (encode w d).length ∧ Fits w ((encode w d).length + 1) ∧
+        safe w d (inputState (encode w d)) ∧
+        (Memory.spec w).ValidHistory (inputState (encode w d))
+          ((Memory.spec w).clientHistory (inputState (encode w d)) (p d)) ∧
+        output ((Memory.spec w).clientResult (inputState (encode w d)) (p d)) i = f d ∧
+        memoryCost (p d) (inputState (encode w d)) + work d (inputState (encode w d)) ≤
+          T (size d)) :
+    UniformComputableInPolyTime B f encode size := by
+  let r := k + (l + h.scratchSize + 1) + 1
+  let fr : Fin r := ⟨0, by omega⟩
+  let src : Fin k → Fin r := fun j => ⟨j.val + 1, by omega⟩
+  let tmp : Fin (l + h.scratchSize + 1) → Fin r := fun j => ⟨k + 1 + j.val, by omega⟩
+  have hsrc : Function.Injective src := fun a b hab =>
+    Fin.ext (by have := congrArg Fin.val hab; simp only [src] at this; omega)
+  have htmp : Function.Injective tmp := fun a b hab =>
+    Fin.ext (by have := congrArg Fin.val hab; simp only [tmp] at this; omega)
+  have hd : ∀ a b, src a ≠ tmp b := fun a b hab => by
+    have := congrArg Fin.val hab; simp only [src, tmp] at this; omega
+  have hf : ∀ b, tmp b ≠ fr := fun b hb => by
+    have := congrArg Fin.val hb; simp only [tmp, fr] at this; omega
+  have hs : ∀ a, src a ≠ fr := fun a ha => by
+    have := congrArg Fin.val ha; simp only [src, fr] at this; omega
+  refine UniformComputableInPolyTime.of_code
+    ((Code.seq (inputPrefix fr (tmp (Fin.last _)) src) (h.code fr src tmp)).mapSimulates φ)
+    (tmp (Fin.castAdd (h.scratchSize + 1) i)) (T := fun n => 2 * k + 5 + h.factor * (T n + 1))
+    (by fun_prop) c hc fun d w hw hin => ?_
+  obtain ⟨hk, hfit, hsafe, hvalid, hout, hcost⟩ := hspec d w hw hin
+  obtain ⟨x, ex, hx, hm, hwords, -⟩ := inputPrefix_exec fr (tmp (Fin.last _)) src (encode w d)
+    hsrc (hf _) (fun j => hd j _) hs hk hfit hin
+  obtain ⟨y, ey, -, hy, -⟩ := (h.code_spec fr src tmp htmp hd hf hs).2 w d x hx
+    (funext fun j => (hwords j).trans (hlayout w d j)) (hm ▸ hsafe) (hm ▸ hvalid)
+  rw [hm] at ey hy
+  exact ⟨y, ((ex.seq ey).mapSimulates φ).mono
+    (Nat.add_le_add_left (Nat.mul_le_mul_left _ (by omega)) _), (hy i).trans hout⟩
+
+end Cslib.WordRAM.Realization.Realizes
diff --git a/ComplexityTests/WordRAMRealizationBackend.lean b/ComplexityTests/WordRAMRealizationBackend.lean
new file mode 100644
index 0000000000..e9870c8ff2
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationBackend.lean
@@ -0,0 +1,147 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+-- upstream: candidate
+
+import Complexity.Computability.WordRAM.Realization.Backend
+import Complexity.Computability.WordRAM.Realization.Client.MemoryStack
+import Complexity.Computability.WordRAM.Realization.Function
+
+/-! The per-constructor backend on the array stack. Three tags select the bodies of
+`MemoryStack.realizes_push`, `realizes_pop` and `realizes_size`. The push carries a value and
+answers `()`; its result encoding has no words, so the value is not echoed. The layout is a
+runtime argument of every tag. Correctness and a constant instruction bound come from
+`Stack.Memory.refinement` and `Stack.Memory.amortized`. -/
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+  Cslib.WordRAM.Realization.MemoryStack Cslib.DataStructure.Queue
+
+namespace ComplexityTests.WordRAMRealizationBackend
+
+/-- The stack's operation constructors. -/
+inductive Tag
+  | push
+  | pop
+  | size
+  deriving DecidableEq
+
+instance : Fintype Tag := Fintype.ofList [.push, .pop, .size] fun t => by cases t <;> simp
+
+/-- One realization per constructor. -/
+noncomputable def certificates : Tag → Certificate .exact
+  | .push => ⟨realizes_push⟩
+  | .pop => ⟨realizes_pop⟩
+  | .size => ⟨realizes_size⟩
+
+/-- The stack on layout `L`: the push value and the layout are the only arguments. -/
+noncomputable def backend (w C : ℕ) (L : Stack.Memory.Layout) :
+    Backend (Stack.WordRAM.spec w C) certificates where
+  tag
+    | .push _ => .push
+    | .pop => .pop
+    | .size => .size
+  arg
+    | .push v => (L, v)
+    | .pop => L
+    | .size => L
+  answer
+    | .push _ => id
+    | .pop => id
+    | .size => id
+
+theorem layoutWords_fits {w : ℕ} {L : Stack.Memory.Layout} {e : Memory.State}
+    (hw : Memory.WellFormed w e) (hi : Stack.Memory.Inv L e) (j : Fin 4) :
+    Fits w (layoutWords L j) := by
+  have h₁ : L.count.base + L.count.length ≤ e.frontier := hi.count_allocated
+  have h₂ : L.items.base + L.items.length ≤ e.frontier := hi.items_allocated
+  refine hw.frontier_fits.of_le ?_
+  fin_cases j <;> simp [layoutWords] <;> omega
+
+theorem implements {w C : ℕ} {L : Stack.Memory.Layout} (hL : L.Valid w C) :
+    (backend w C L).Implements (Stack.Memory.refinement hL) where
+  run o s := by cases o <;> rfl
+  entry {e} o hw hi hv := by
+    have hC := hL.items_length
+    cases o with
+    | push v =>
+      obtain ⟨hlen, hv⟩ := hv
+      change (Stack.Memory.abs L e).length < C at hlen
+      rw [Stack.Memory.length_abs] at hlen
+      exact ⟨fits_appendWords (d := L) (a := v) layoutWords
+        (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (layoutWords_fits hw hi) fun _ => hv,
+        hC ▸ hL, hi, (by omega : e.mem L.count.base < L.items.length)⟩
+    | pop => exact ⟨layoutWords_fits hw hi, hC ▸ hL, hi⟩
+    | size => exact ⟨layoutWords_fits hw hi, trivial⟩
+
+/-- The native stack on layout `L`. -/
+noncomputable def implementation {w C : ℕ} {L : Stack.Memory.Layout} (hL : L.Valid w C) :
+    StateTransitionImpl (Stack.WordRAM.spec w C) ((backend w C L).exec w) :=
+  Backend.implementation (implements hL)
+
+/-- One constant bounds every operation, before every width, capacity and layout. -/
+theorem instruction_bound : ∃ K, ∀ {w C : ℕ} {L : Stack.Memory.Layout} (hL : L.Valid w C),
+    Bound (implementation hL) id fun _ _ => K :=
+  ⟨Backend.factor certificates * 23, fun hL =>
+    Backend.bound (implements hL) (Stack.Memory.amortized hL) 19 fun o _ _ => by
+      cases o <;> exact Nat.le_of_ble_eq_true rfl⟩
+
+/-- Adaptive clients run one operation at a time, within `K` instructions per operation. -/
+theorem run_client : ∃ K, ∀ {w C : ℕ} {L : Stack.Memory.Layout} (hL : L.Valid w C) {α : Type}
+    (p : (Stack.WordRAM.spec w C).Client α) {vs : List ℕ}
+    {x : Data (Backend.registers certificates)},
+    (implementation hL).rep vs x →
+    (Stack.WordRAM.spec w C).ValidHistory vs ((Stack.WordRAM.spec w C).clientHistory vs p) →
+    ∃ y traces, Executes ((backend w C L).exec w) p x
+        ((Stack.WordRAM.spec w C).clientResult vs p) y traces ∧
+      (implementation hL).rep ((Stack.WordRAM.spec w C).clientState vs p) y ∧
+      total id traces ≤ ((Stack.WordRAM.spec w C).clientHistory vs p).length * K := by
+  obtain ⟨K, hK⟩ := instruction_bound
+  exact ⟨K, fun hL _ p _ _ hr hv => Bound.exists_executes_const (hK hL) p hr hv⟩
+
+-- The push value never selects code: every push runs the body of the `push` tag.
+example (w C : ℕ) (L : Stack.Memory.Layout) :
+    Backend.code certificates ((backend w C L).tag (.push 3)) =
+      Backend.code certificates ((backend w C L).tag (.push 4)) := rfl
+
+-- A push answers `()` through an empty result encoding; its value is not echoed.
+example : (certificates .push).l = 0 := rfl
+
+-- Every native execution from a represented stack takes the specified step, and its memory is
+-- the method's final memory.
+example {w C : ℕ} {L : Stack.Memory.Layout} (hL : L.Valid w C) {vs : List ℕ}
+    {x y : Data (Backend.registers certificates)} {o : StackOp ℕ}
+    {a : (Stack.WordRAM.spec w C).Result o} {n : ℕ} (hr : (implementation hL).rep vs x)
+    (hv : (Stack.WordRAM.spec w C).valid vs o) (he : (backend w C L).exec w x o a y n) :
+    a = ((Stack.WordRAM.spec w C).stepFn vs o).2 ∧
+      memoryState (Backend.frontier certificates) y = (Memory.spec w).clientState
+        (memoryState (Backend.frontier certificates) x) (Stack.Memory.methods L w C o) :=
+  ⟨((implementation hL).correct_ofFn hr hv he).1,
+    Backend.exec_memoryState (implements hL) hr hv he⟩
+
+-- An empty stack of capacity two at address three, held in zero memory with the frontier at six,
+-- is represented by the native data holding that memory state.
+example : (implementation (Stack.Memory.valid_allocLayout (w := 4) (f := 3) (C := 2)
+    (by decide))).rep [] (Backend.data certificates ⟨fun _ => 0, 6⟩) :=
+  Backend.rep_data _ ⟨by decide, fun _ => fits_zero 4⟩ ⟨le_of_lt (by decide), le_rfl, by simp⟩
+    (by simp [Stack.Memory.refinement, Stack.Memory.abs])
+
+-- Two stacks with disjoint layouts: product operations select tags of `Tag ⊕ Tag`.
+example {w C : ℕ} {L₁ L₂ : Stack.Memory.Layout} (h₁ : L₁.Valid w C) (h₂ : L₂.Valid w C) :
+    ((backend w C L₁).sum (backend w C L₂)).Implements
+      ((Stack.Memory.framed h₁).prod (Stack.Memory.framed h₂)).toRefinement :=
+  (implements h₁).prod (frame₁ := Memory.Framed.prod_frame_left _ _)
+    (frame₂ := Memory.Framed.prod_frame_right _ _) (implements h₂)
+
+-- Doubling at every width of at least `2 * (log₂ n + 1)` bits, as one flat program.
+example : UniformComputableInPolyTime .standard (fun n => n + n) (fun _ n => [n]) id :=
+  (Realizes.addWords (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding 0 0).uniformComputableInPolyTime
+    .exactStandard 0 (.const 3) 2 (by decide) (fun _ _ j => by fin_cases j; rfl)
+    fun n w hw _ => by
+      have h2 : Fits w 2 := (show Fits 2 2 by decide).mono (le_trans (by simp [logWidth]) hw)
+      have hn : Fits w (n + n) := (fits_of_lt_pow (k := 2) (n := n) (by nlinarith)).mono hw
+      exact ⟨le_rfl, h2, hn, trivial, rfl, le_rfl⟩
+
+end ComplexityTests.WordRAMRealizationBackend