diff --git a/Complexity.lean b/Complexity.lean
index 899bc48751..69357311d9 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2655,6 +2655,8 @@ public import Complexity.Computability.WordRAM.Realization.Module
 public import Complexity.Computability.WordRAM.Realization.Primitive
 public import Complexity.Computability.WordRAM.Realization.Program
 public import Complexity.Computability.WordRAM.Realization.Program.Standard
+public import Complexity.Computability.WordRAM.Realization.Random
+public import Complexity.Computability.WordRAM.Realization.RandomLoop
 public import Complexity.Computability.WordRAM.Realization.Reindex
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.While
diff --git a/Complexity/Computability/WordRAM/Randomized/Law.lean b/Complexity/Computability/WordRAM/Randomized/Law.lean
index 140259bc45..7dc2a2f5bb 100644
--- a/Complexity/Computability/WordRAM/Randomized/Law.lean
+++ b/Complexity/Computability/WordRAM/Randomized/Law.lean
@@ -44,6 +44,9 @@ with `f` (`Cslib.WordRAM.ExecRandLaw.program`).
   `Cslib.WordRAM.ExecRandLaw.loop_iter`: composition rules.
 * `Cslib.WordRAM.ExecRandLaw.rename`: renaming registers.
 * `Cslib.WordRAM.ExecRandLaw.execRandWithin`: forgetting the law.
+* `Cslib.WordRAM.ExecRandLaw.map`, `Cslib.WordRAM.ExecRandLaw.withBounded`,
+  `Cslib.WordRAM.ExecRandLaw.withSupport`: mapping the observation, and the boundedness and the
+  support of every final observation.
 * `Cslib.WordRAM.ExecRandLaw.program`: the compiled program halts within the bound, respects the
   call budget and the postcondition, and has the law `μ`.
 -/
@@ -83,6 +86,28 @@ theorem congr_law {μ' : PMF α} (h : ExecRandLaw w c x P T R f μ) (hμ : μ =
     ExecRandLaw w c x P T R f μ' :=
   hμ ▸ h
 
+/-- Post-composing the observation with `g` maps the law by `g`. -/
+theorem map (h : ExecRandLaw w c x P T R f μ) (g : α → β) :
+    ExecRandLaw w c x P T R (fun y => g (f y)) (μ.map g) := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  refine ⟨m, hm, hq, hsup, ?_⟩
+  rw [← hlaw, ProbComp.eval_map, ProbComp.eval_map, PMF.map_comp]
+  rfl
+
+/-- Strengthening the postcondition with word-boundedness, from bounded initial data. -/
+theorem withBounded (h : ExecRandLaw w c x P T R f μ) (hx : x.Bounded w) :
+    ExecRandLaw w c x (fun y => P y ∧ y.Bounded w) T R f μ := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  exact ⟨m, hm, hq, fun z hz => ⟨⟨(hsup z hz).1, hm.bounded hx hz⟩, (hsup z hz).2⟩, hlaw⟩
+
+/-- Strengthening the postcondition: every final observation lies in the support of the law. -/
+theorem withSupport (h : ExecRandLaw w c x P T R f μ) :
+    ExecRandLaw w c x (fun y => P y ∧ f y ∈ μ.support) T R f μ := by
+  obtain ⟨m, hm, hq, hsup, hlaw⟩ := h
+  refine ⟨m, hm, hq, fun z hz => ⟨⟨(hsup z hz).1, ?_⟩, (hsup z hz).2⟩, hlaw⟩
+  rw [← hlaw, ProbComp.eval_map, PMF.support_map, ProbComp.support_eval]
+  exact ⟨z, hz, rfl⟩
+
 /-- Strengthening the postcondition with a register that `c` never writes. -/
 theorem withPreserves {i : Fin r} (h : ExecRandLaw w c x P T R f μ) (hi : c.Preserves i) :
     ExecRandLaw w c x (fun y => P y ∧ y.regs i = x.regs i) T R f μ := by
diff --git a/Complexity/Computability/WordRAM/Realization/Bind.lean b/Complexity/Computability/WordRAM/Realization/Bind.lean
index 9858fb81ce..eaa40a802c 100644
--- a/Complexity/Computability/WordRAM/Realization/Bind.lean
+++ b/Complexity/Computability/WordRAM/Realization/Bind.lean
@@ -18,6 +18,10 @@ Its source registers append the first computation's answer slots to the original
 Two disjoint static scratch banks preserve that environment without client-written intermediate
 assertions. The continuation's bank already contains the final output slots, so no copy is needed.
 
+## Main definitions
+
+* `bindLeft`, `bindRight`: the two scratch banks inside a sequential composition's bank.
+
 ## Main results
 
 * `Realizes.bind`: sequential realization with additive memory and local-work charges.
@@ -29,10 +33,14 @@ namespace Cslib.WordRAM.Realization
 
 open Cslib.DataStructure
 
-private def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) :
+/-- The continuation's scratch bank inside a sequential composition's bank: its first slots, so
+its result slots are the composition's. -/
+def bindLeft {m n₂ l n₁ : ℕ} (i : Fin (m + n₂ + 1)) :
     Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨i.val, by omega⟩
 
-private def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) :
+/-- The first computation's scratch bank inside a sequential composition's bank, after the
+continuation's. -/
+def bindRight {m n₂ l n₁ : ℕ} (i : Fin (l + n₁ + 1)) :
     Fin (m + (n₂ + l + n₁ + 1) + 1) := ⟨m + n₂ + 1 + i.val, by omega⟩
 
 namespace Realizes
diff --git a/Complexity/Computability/WordRAM/Realization/Branch.lean b/Complexity/Computability/WordRAM/Realization/Branch.lean
index 3d55738f1e..7ead84d964 100644
--- a/Complexity/Computability/WordRAM/Realization/Branch.lean
+++ b/Complexity/Computability/WordRAM/Realization/Branch.lean
@@ -22,6 +22,7 @@ The two-instruction allowance includes the jump on the negative path.
 
 ## Main results
 
+* `test_rename`: a renamed native condition tests the words in its source registers.
 * `Realizes.branch`: compose two realizations using an actual native conditional.
 -/
 
@@ -40,7 +41,9 @@ instance (c : Cond k) (v : Fin k → ℕ) : Decidable (test c v) := by
   unfold test
   infer_instance
 
-private theorem test_rename {r : ℕ} (c : Cond k) (src : Fin k → Fin r)
+/-- A renamed condition holds of native data exactly when it holds of the words in its source
+registers. -/
+theorem test_rename {r : ℕ} (c : Cond k) (src : Fin k → Fin r)
     (x : Data r) (v : Fin k → ℕ) (h : x.regs ∘ src = v) :
     (c.rename src).Holds x ↔ test c v := by
   cases c <;> simp only [Cond.rename, Cond.Holds, test] <;>
diff --git a/Complexity/Computability/WordRAM/Realization/Loop.lean b/Complexity/Computability/WordRAM/Realization/Loop.lean
index 893fbe6260..9b66bdda09 100644
--- a/Complexity/Computability/WordRAM/Realization/Loop.lean
+++ b/Complexity/Computability/WordRAM/Realization/Loop.lean
@@ -20,6 +20,8 @@ uses one fixed body emitter and static registers for the mutable state and count
 
 * `iterate`: bounded iteration in the existing memory-client monad.
 * `iterationWork`, `iterationSafe`: local work and domains along the actual semantic states.
+* `loopEmit`, `loopBody`: the native loop with a fixed body emitter, and one native iteration,
+  over the register bank `stateSlot`, `counterSlot`, `zeroSlot`, `oneSlot`, `bodySlot`.
 
 ## Main results
 
@@ -192,17 +194,24 @@ theorem iterationSum_eq (body : δ × σ → Memory.Prog σ)
     dsimp only [iterationStep] at *
     omega
 
-private def stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1) :=
+/-- The loop's state words, which are also its result slots. -/
+def stateSlot {l n : ℕ} (i : Fin l) : Fin (l + (l + n + 3) + 1) :=
   ⟨i.val, by omega⟩
 
-private def counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l, by omega⟩
-private def zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 1, by omega⟩
-private def oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 2, by omega⟩
+/-- The loop's countdown register. -/
+def counterSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l, by omega⟩
+/-- A register holding zero, for the loop test. -/
+def zeroSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 1, by omega⟩
+/-- A register holding one, for the countdown. -/
+def oneSlot (l n : ℕ) : Fin (l + (l + n + 3) + 1) := ⟨l + 2, by omega⟩
 
-private def bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1) :=
+/-- The body's scratch bank inside the loop's bank. -/
+def bodySlot {l n : ℕ} (i : Fin (l + n + 1)) : Fin (l + (l + n + 3) + 1) :=
   ⟨l + 3 + i.val, by omega⟩
 
-private def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
+/-- One native iteration: run the body on the environment and state words, copy its result into
+the state words and count down. -/
+def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
     (Fin (l + n + 1) → Fin r) → Code .exact r)
     (frontier : Fin r) (src : Fin (k + l + 1) → Fin r)
     (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r :=
@@ -214,7 +223,9 @@ private def loopBody {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) →
         (.op (.exactBin .sub (tmp (counterSlot l n))
           (tmp (counterSlot l n)) (tmp (oneSlot l n))))
 
-private def loopEmit {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
+/-- The native loop: install the state words and the counter, then iterate `loopBody` while the
+counter is positive. -/
+def loopEmit {n : ℕ} (emit : ∀ {r : ℕ}, Fin r → (Fin (k + l) → Fin r) →
     (Fin (l + n + 1) → Fin r) → Code .exact r)
     (frontier : Fin r) (src : Fin (k + l + 1) → Fin r)
     (tmp : Fin (l + (l + n + 3) + 1) → Fin r) : Code .exact r :=
diff --git a/Complexity/Computability/WordRAM/Realization/Random.lean b/Complexity/Computability/WordRAM/Realization/Random.lean
new file mode 100644
index 0000000000..1f7d2b2f1c
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/Random.lean
@@ -0,0 +1,398 @@
+/-
+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.Program
+public import Complexity.Computability.WordRAM.Randomized.Law
+public import Complexity.DataStructure.StateTransition.Randomized
+
+/-!
+# Realizing memory clients with private coins
+
+A memory client with private coins is a `ProbOracleComp Memory.Op.Result` program: it calls the
+memory oracle and draws uniform coins. It runs against `(Memory.spec w).toRandomized.withCoins`,
+the memory oracle beside uniform sampling. Linking a client of a randomized specification
+through a memory refinement with its coins passed through (`RandomizedRefinement.withCoins`)
+produces exactly such a program. `RealizesRand` certifies one uniform native emitter for a family
+of them, as `Realizes` does for deterministic clients, with the same emitter, scratch bank,
+frontier and register frame. The certificate gives the exact law instead of a single run. At
+word size `w`, from native data whose memory abstraction is `s`, the emitted code's result words
+and memory state have the law of `(Memory.spec w).toRandomized.withCoins.run (p d) s`, read
+through the result encoding (`ExecRandLaw`). Every path runs within `C * (time d s + 1)`
+instructions and makes at most `calls d s` `rand` calls. Both are worst-case bounds that hold on
+every path, not expected ones.
+
+Deterministic parts are certified by `Realizes`, including every certificate `realize` builds,
+and enter unchanged (`Realizes.toRand`). A coin is one `rand` instruction (`RealizesRand.coin`).
+Sequencing (`RealizesRand.bind`) needs the continuation's domain and budgets at every supported
+intermediate state; these obligations become part of the visible domain. Branching on the live
+words is `RealizesRand.branch`. A flat program from the native list-input convention halts within
+its bound on every path, respects the `rand` budget and has the law of the client
+(`RealizesRand.exists_init_program`). Runtime-bounded loops are in
+`Complexity.Computability.WordRAM.Realization.RandomLoop`.
+
+## Main definitions
+
+* `RealizesRand`: uniform native realization of a memory client with private coins, with its
+  law, a worst-case instruction bound and a worst-case `rand` budget.
+
+## Main results
+
+* `Realizes.toRand`: deterministic certificates are randomized ones with no `rand` call.
+* `RealizesRand.coin`: a uniform draw from `[0, n]`, for a live word `n`.
+* `RealizesRand.bind`, `RealizesRand.branch`: sequencing and branching.
+* `RealizesRand.consequence`, `RealizesRand.congr`: weakening and transport along equal clients.
+* `RealizesRand.exists_init_program`: a flat program with `RandHaltsWithin`, `RandCallsBounded` and
+  the law of its halting configurations.
+
+The randomized certificate is original infrastructure over the existing realization kernel, the
+structured randomized semantics `ExecRandLaw` and the randomized specifications of
+`DataStructure.StateTransition.Randomized`; no execution semantics or client language is added.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+variable {B : Basis} {δ α β : Type} {k l m : ℕ}
+
+/-- Uniform native realization of a family of memory clients with private coins. The emitter,
+scratch size and exchange constant precede every runtime argument, word width and initial
+memory, and the register conventions are those of `Realizes`. From admissible entry data, the
+emitted code terminates on every path within `C * (time d s + 1)` instructions and `calls d s`
+`rand` calls, keeps every register outside the scratch bank and the frontier, and the result words
+together with the memory state have the law of the client's run, read through `output`. -/
+def RealizesRand (B : Basis) (p : δ → ProbOracleComp Memory.Op.Result α)
+    (input : δ ↪ (Fin k → ℕ)) (output : α ↪ (Fin l → ℕ))
+    (safe : ℕ → δ → Memory.State → Prop) (time calls : δ → Memory.State → ℕ) : Prop :=
+  ∃ n C : ℕ,
+    ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) →
+        (Fin (l + n + 1) → Fin r) → Code B r,
+      ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r)
+        (tmp : Fin (l + n + 1) → Fin r),
+        Function.Injective tmp → (∀ i j, src i ≠ tmp j) →
+        (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) →
+        ¬(emit frontier src tmp).ReadsWidth ∧
+        ∀ (w : ℕ) (d : δ) (x : Data r), x.Bounded w → x.regs ∘ src = input d →
+          safe w d (memoryState frontier x) →
+          (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid (memoryState frontier x)
+            (p d) →
+          ExecRandLaw w (emit frontier src tmp) x
+            (fun y => ∀ i, i ≠ frontier → (∀ j, tmp j ≠ i) → y.regs i = x.regs i)
+            (C * (time d (memoryState frontier x) + 1)) (calls d (memoryState frontier x))
+            (fun y => (fun i : Fin l => y.regs (tmp (Fin.castAdd (n + 1) i)),
+              memoryState frontier y))
+            (((Memory.spec w).toRandomized.withCoins.run (p d) (memoryState frontier x)).map
+              fun (a, s) => (output a, s))
+
+namespace Realizes
+
+variable {p : δ → Memory.Prog α} {input : δ ↪ (Fin k → ℕ)} {output : α ↪ (Fin l → ℕ)}
+  {safe : ℕ → δ → Memory.State → Prop} {work : δ → Memory.State → ℕ}
+
+/-- **Deterministic parts.** A deterministic certificate, for instance one built by `realize`,
+realizes the same client with coins available and unused: its law is the point mass at the
+deterministic run, its time is the memory charge plus local work, and it makes no `rand` call. -/
+theorem toRand (h : Realizes B p input output safe work) :
+    RealizesRand B (fun d => OracleComp.liftRight (p d)) input output safe
+      (fun d s => memoryCost (p d) s + work d s) (fun _ _ => 0) := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨n, C, emit, fun frontier src tmp hi hd hf hs => ?_⟩
+  obtain ⟨hnw, hrun⟩ := he frontier src tmp hi hd hf hs
+  refine ⟨hnw, fun w d x hx hin hsafe hv => ?_⟩
+  have hv' := ((Memory.spec w).demonicValid_iff_validHistory_runClient _ (p d)).mp
+    (StateTransitionSpec.toRandomized_demonicValid_iff.mp
+      (RandomizedSpec.demonicValid_liftRight_iff.mp hv))
+  obtain ⟨y, hy, hm, hout, hframe⟩ := hrun w d x hx hin hsafe hv'
+  refine (ExecRandLaw.of_execWithin hy hframe).congr_law ?_
+  rw [RandomizedSpec.withCoins_run_liftRight, StateTransitionSpec.run_toRandomized, PMF.pure_map]
+  exact congrArg PMF.pure (Prod.ext (funext hout) hm)
+
+end Realizes
+
+namespace RealizesRand
+
+variable {p : δ → ProbOracleComp Memory.Op.Result α} {input : δ ↪ (Fin k → ℕ)}
+  {output : α ↪ (Fin l → ℕ)} {safe : ℕ → δ → Memory.State → Prop}
+  {time calls : δ → Memory.State → ℕ}
+
+/-- Strengthen the visible domain, and enlarge the time and `rand` budgets on it. The entry word
+and memory bounds may be used. -/
+theorem consequence {safe' : ℕ → δ → Memory.State → Prop} {time' calls' : δ → Memory.State → ℕ}
+    (h : RealizesRand B p input output safe time calls)
+    (hsafe : ∀ w d s, (∀ i, Fits w (input d i)) → Memory.WellFormed w s → safe' w d s →
+      safe w d s ∧ time d s ≤ time' d s ∧ calls d s ≤ calls' d s) :
+    RealizesRand B p input output safe' time' calls' := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨n, C, emit, fun frontier src tmp hi hd hf hs => ?_⟩
+  obtain ⟨hnw, hrun⟩ := he frontier src tmp hi hd hf hs
+  refine ⟨hnw, fun w d x hx hin hsafe' hv => ?_⟩
+  have hwords (i : Fin k) : Fits w (input d i) := congrFun hin i ▸ hx.1 (src i)
+  obtain ⟨hsafe, htime, hcalls⟩ := hsafe w d _ hwords (wellFormed_memoryState hx) hsafe'
+  exact (hrun w d x hx hin hsafe hv).mono (fun _ h => h)
+    (Nat.mul_le_mul_left C (Nat.add_le_add_right htime 1)) hcalls
+
+/-- Pointwise equal clients have the same certificates. -/
+theorem congr {p' : δ → ProbOracleComp Memory.Op.Result α}
+    (h : RealizesRand B p input output safe time calls) (hp : ∀ d, p d = p' d) :
+    RealizesRand B p' input output safe time calls :=
+  funext hp ▸ h
+
+/-- **A coin.** Drawing uniformly from `[0, n]`, for a live word `n`, is one `rand` instruction
+into the result slot. -/
+theorem coin (input : δ ↪ (Fin k → ℕ)) (i : Fin k) :
+    RealizesRand B (fun d => Fin.val <$> ProbOracleComp.sample (ProbComp.unifFin (input d i)))
+      input (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding (fun _ _ _ => True)
+      (fun _ _ => 1) (fun _ _ => 1) := by
+  refine ⟨0, 1, fun _ src tmp => .rand (tmp 0) (src i), fun frontier src tmp _ _ hf _ => ?_⟩
+  refine ⟨fun h => h, fun w d x hx hin _ _ => ?_⟩
+  have h := ExecRandLaw.rand (B := B) (w := w) (x := x) (dst := tmp 0) (src := src i)
+    (P := fun y => ∀ j, j ≠ frontier → (∀ t, tmp t ≠ j) → y.regs j = x.regs j)
+    (f := fun y => (fun j : Fin 1 => y.regs (tmp (Fin.castAdd (0 + 1) j)),
+      memoryState frontier y))
+    (hx.1 (src i)) fun c j _ hj => Function.update_of_ne (hj 0).symm _ _
+  refine (h.mono (fun _ h => h) (by omega) le_rfl).congr_law ?_
+  have hsrc : x.regs (src i) = input d i := congrFun hin i
+  rw [RandomizedSpec.run_map, RandomizedSpec.withCoins_run_sample, ProbComp.eval_unifFin,
+    PMF.map_comp, PMF.map_comp, ← hsrc]
+  congr 1
+  funext c
+  refine Prod.ext (funext fun j => ?_) ?_
+  · rw [Fin.fin_one_eq_zero j]
+    simp [Data.set]
+  · exact Memory.State.ext rfl (Function.update_of_ne (hf 0).symm _ _)
+
+section Bind
+
+variable {q : δ × α → ProbOracleComp Memory.Op.Result β} {answer : α ↪ (Fin l → ℕ)}
+  {output : β ↪ (Fin m → ℕ)}
+  {safeP : ℕ → δ → Memory.State → Prop} {safeQ : ℕ → δ × α → Memory.State → Prop}
+  {timeP callsP : δ → Memory.State → ℕ} {timeQ callsQ : δ × α → Memory.State → ℕ}
+
+/-- **Sequencing.** One uniform continuation emitter consumes the original environment and the
+first computation's answer. Its domain and budgets must hold at every supported intermediate
+answer and state, within the uniform budgets `T` and `R`; these obligations join the visible
+domain. The laws compose by `PMF.bind`, the times and `rand` budgets add. -/
+theorem bind (hP : RealizesRand B p input answer safeP timeP callsP)
+    (hQ : RealizesRand B q (appendWords input answer) output safeQ timeQ callsQ)
+    (T R : δ → Memory.State → ℕ) :
+    RealizesRand B (fun d => p d >>= fun a => q (d, a)) input output
+      (fun w d s => safeP w d s ∧ ∀ a s',
+        (a, s') ∈ ((Memory.spec w).toRandomized.withCoins.run (p d) s).support →
+          safeQ w (d, a) s' ∧ timeQ (d, a) s' ≤ T d s ∧ callsQ (d, a) s' ≤ R d s)
+      (fun d s => timeP d s + T d s + 1) (fun d s => callsP d s + R d s) := by
+  obtain ⟨n₁, C₁, emitP, heP⟩ := hP
+  obtain ⟨n₂, C₂, emitQ, heQ⟩ := hQ
+  let N := n₂ + l + n₁ + 1
+  let left : Fin (m + n₂ + 1) → Fin (m + N + 1) := bindLeft
+  let right : Fin (l + n₁ + 1) → Fin (m + N + 1) := bindRight
+  refine ⟨N, max C₁ C₂, fun frontier src tmp => .seq (emitP frontier src (tmp ∘ right))
+    (emitQ frontier (Fin.append src (fun i => tmp (right (Fin.castAdd (n₁ + 1) i))))
+      (tmp ∘ left)), ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  have hleft : Function.Injective (tmp ∘ left) := by
+    intro a b hab
+    apply Fin.ext
+    have h := congrArg Fin.val (hi hab)
+    exact h
+  have hright : Function.Injective (tmp ∘ right) := by
+    intro a b hab
+    apply Fin.ext
+    have := congrArg Fin.val (hi hab)
+    change m + n₂ + 1 + a.val = m + n₂ + 1 + b.val at this
+    omega
+  have hdisjoint (a : Fin (l + n₁ + 1)) (b : Fin (m + n₂ + 1)) :
+      tmp (right a) ≠ tmp (left b) := by
+    intro hab
+    have := congrArg Fin.val (hi hab)
+    change m + n₂ + 1 + a.val = b.val at this
+    omega
+  let nextSrc : Fin (k + l) → Fin r :=
+    Fin.append src (fun i => tmp (right (Fin.castAdd (n₁ + 1) i)))
+  have hnextDisjoint (i : Fin (k + l)) (j : Fin (m + n₂ + 1)) :
+      nextSrc i ≠ (tmp ∘ left) j := by
+    refine Fin.addCases (fun a => ?_) (fun b => ?_) i
+    · simpa only [nextSrc, Fin.append_left, Function.comp_apply] using hd a (left j)
+    · simpa only [nextSrc, Fin.append_right, Function.comp_apply] using
+        hdisjoint (Fin.castAdd (n₁ + 1) b) j
+  have hnextFrontier (i : Fin (k + l)) : nextSrc i ≠ frontier := by
+    refine Fin.addCases (fun a => ?_) (fun b => ?_) i
+    · simpa only [nextSrc, Fin.append_left] using hs a
+    · simpa only [nextSrc, Fin.append_right] using hf (right (Fin.castAdd (n₁ + 1) b))
+  obtain ⟨hnwP, hrunP⟩ := heP frontier src (tmp ∘ right) hright
+    (fun i j => hd i (right j)) (fun j => hf (right j)) hs
+  obtain ⟨hnwQ, hrunQ⟩ := heQ frontier nextSrc (tmp ∘ left) hleft hnextDisjoint
+    (fun j => hf (left j)) hnextFrontier
+  refine ⟨fun h => h.elim hnwP hnwQ, fun w d x hx hin hsafe hv => ?_⟩
+  let s := memoryState frontier x
+  let D := (Memory.spec w).toRandomized.withCoins
+  have hv' : D.toSpec.DemonicValid s ((p d).bind fun a => q (d, a)) := hv
+  obtain ⟨hvP, hvQ⟩ := StateTransitionSpec.DemonicValid.of_bind hv'
+  obtain ⟨⟨a₀, -⟩, -⟩ := (D.run (p d) s).support_nonempty
+  have : Nonempty α := ⟨a₀⟩
+  have hdecode : ∀ a, Function.invFun answer (answer a) = a :=
+    Function.leftInverse_invFun answer.injective
+  let κ : (Fin l → ℕ) × Memory.State → PMF ((Fin m → ℕ) × Memory.State) := fun (v, s') =>
+    (D.run (q (d, Function.invFun answer v)) s').map fun (b, s'') => (output b, s'')
+  have h₁ := ((hrunP w d x hx hin hsafe.1 hvP).withBounded hx).withSupport
+  have h := ExecRandLaw.seq (κ := κ)
+    (Q := fun y => ∀ i, i ≠ frontier → (∀ j, tmp j ≠ i) → y.regs i = x.regs i)
+    (T₂ := C₂ * (T d s + 1)) (R₂ := R d s)
+    (f := fun y => (fun i : Fin m => y.regs (tmp (Fin.castAdd (N + 1) i)),
+      memoryState frontier y)) h₁ fun z ⟨⟨hframe, hzb⟩, hzsup⟩ => by
+    obtain ⟨⟨a, s'⟩, hmem, hz⟩ := (PMF.mem_support_map_iff _ _ _).mp hzsup
+    have hzout : (fun i : Fin l => z.regs ((tmp ∘ right) (Fin.castAdd (n₁ + 1) i))) = answer a :=
+      (congrArg Prod.fst hz).symm
+    have hzs : memoryState frontier z = s' := (congrArg Prod.snd hz).symm
+    have hinQ : z.regs ∘ nextSrc = (appendWords input answer) (d, a) := by
+      funext i
+      refine Fin.addCases (fun j => ?_) (fun j => ?_) i
+      · change z.regs (nextSrc (Fin.castAdd l j)) =
+          Fin.append (input d) (answer a) (Fin.castAdd l j)
+        simp only [nextSrc, Fin.append_left]
+        exact (hframe (src j) (hs j) (fun t => (hd j (right t)).symm)).trans (congrFun hin j)
+      · change z.regs (nextSrc (Fin.natAdd k j)) =
+          Fin.append (input d) (answer a) (Fin.natAdd k j)
+        simp only [nextSrc, Fin.append_right]
+        exact congrFun hzout j
+    obtain ⟨hsafeQ, htime, hcalls⟩ := hsafe.2 a s' hmem
+    obtain ⟨tr, hrun⟩ := D.exists_clientRun_of_mem_support hvP hmem
+    have hQ := hrunQ w (d, a) z hzb hinQ (hzs ▸ hsafeQ) (hzs ▸ hvQ a s' tr hrun)
+    rw [hzs] at hQ
+    have hκ : κ (answer a, s') = (D.run (q (d, a)) s').map fun (b, s'') => (output b, s'') := by
+      simp only [κ, hdecode]
+    change ExecRandLaw w _ z _ _ _ _
+      (κ ((fun i : Fin l => z.regs ((tmp ∘ right) (Fin.castAdd (n₁ + 1) i))),
+        memoryState frontier z))
+    rw [hzout, hzs, hκ]
+    exact hQ.mono (fun y hy i hif htmp => (hy i hif fun j => htmp (left j)).trans
+      (hframe i hif fun j => htmp (right j)))
+      (Nat.mul_le_mul_left C₂ (Nat.add_le_add_right htime 1)) hcalls
+  refine (h.mono (fun _ h => h) ?_ le_rfl).congr_law ?_
+  · change C₁ * (timeP d s + 1) + C₂ * (T d s + 1) ≤ max C₁ C₂ * (timeP d s + T d s + 1 + 1)
+    calc
+      _ ≤ max C₁ C₂ * (timeP d s + 1) + max C₁ C₂ * (T d s + 1) :=
+        Nat.add_le_add (Nat.mul_le_mul_right _ (Nat.le_max_left _ _))
+          (Nat.mul_le_mul_right _ (Nat.le_max_right _ _))
+      _ = _ := by ring
+  · change ((D.run (p d) s).map fun (a, s') => (answer a, s')).bind κ =
+      (D.run (p d >>= fun a => q (d, a)) s).map fun (b, s'') => (output b, s'')
+    rw [PMF.bind_map, RandomizedSpec.run_bind, PMF.map_bind]
+    congr 1
+    funext ⟨a, s'⟩
+    simp only [Function.comp_apply, κ, hdecode]
+
+end Bind
+
+section Branch
+
+variable {pos neg : δ → ProbOracleComp Memory.Op.Result α}
+  {safePos safeNeg : ℕ → δ → Memory.State → Prop}
+  {timePos timeNeg callsPos callsNeg : δ → Memory.State → ℕ}
+
+/-- **Branching** on a test of the live words. Only the selected alternative's domain and
+budgets are required; the test and the jump are absorbed by the exchange constant. -/
+theorem branch (c : Cond k) (hp : RealizesRand B pos input output safePos timePos callsPos)
+    (hn : RealizesRand B neg input output safeNeg timeNeg callsNeg) :
+    RealizesRand B (fun d => if test c (input d) then pos d else neg d) input output
+      (fun w d s => if test c (input d) then safePos w d s else safeNeg w d s)
+      (fun d s => if test c (input d) then timePos d s else timeNeg d s)
+      (fun d s => if test c (input d) then callsPos d s else callsNeg d s) := by
+  obtain ⟨np, Cp, ep, hep⟩ := hp
+  obtain ⟨nn, Cn, en, hen⟩ := hn
+  let ip : Fin (l + np + 1) → Fin (l + (np + nn) + 1) := Fin.castLE (by omega)
+  let ineg : Fin (l + nn + 1) → Fin (l + (np + nn) + 1) := Fin.castLE (by omega)
+  refine ⟨np + nn, max Cp Cn + 2, fun frontier src tmp =>
+    .branch (c.rename src) (ep frontier src (tmp ∘ ip)) (en frontier src (tmp ∘ ineg)), ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  have hip : Function.Injective (tmp ∘ ip) := fun a b hab =>
+    Fin.ext (congrArg (fun z : Fin (l + (np + nn) + 1) => z.val) (hi hab))
+  have hin : Function.Injective (tmp ∘ ineg) := fun a b hab =>
+    Fin.ext (congrArg (fun z : Fin (l + (np + nn) + 1) => z.val) (hi hab))
+  obtain ⟨hnp, hrp⟩ := hep frontier src (tmp ∘ ip) hip
+    (fun i j => hd i (ip j)) (fun j => hf (ip j)) hs
+  obtain ⟨hnn, hrn⟩ := hen frontier src (tmp ∘ ineg) hin
+    (fun i j => hd i (ineg j)) (fun j => hf (ineg j)) hs
+  refine ⟨fun h => h.elim hnp hnn, fun w d x hx hinput hsafe hv => ?_⟩
+  have hc := test_rename c src x (input d) hinput
+  have hle (C t : ℕ) (hC : C ≤ max Cp Cn) (e : ℕ) (he : e ≤ 2) :
+      C * (t + 1) + e ≤ (max Cp Cn + 2) * (t + 1) := by
+    have := Nat.mul_le_mul_right (t + 1) hC
+    nlinarith
+  by_cases ht : test c (input d)
+  · simp only [ite_eq_left ht] at hsafe hv ⊢
+    exact ((hrp w d x hx hinput hsafe hv).branch_pos (hc.mpr ht)).mono
+      (fun y hy i hif htmp => hy i hif fun j => htmp (ip j))
+      (hle Cp _ (Nat.le_max_left _ _) 1 (by omega)) le_rfl
+  · simp only [ite_eq_right ht] at hsafe hv ⊢
+    exact ((hrn w d x hx hinput hsafe hv).branch_neg (fun h => ht (hc.mp h))).mono
+      (fun y hy i hif htmp => hy i hif fun j => htmp (ineg j))
+      (hle Cn _ (Nat.le_max_right _ _) 2 le_rfl) le_rfl
+
+end Branch
+
+/-- **Flat programs.** Each static coordinate of the result has one flat exact-basis program from
+the native list-input convention. On an input list whose first `k` words encode the environment,
+it halts on every path within its bound, makes at most the budgeted `rand` calls, and the halting
+output word together with the memory state has the law of the client's run from the whole input
+memory, read at that coordinate. The rest of the input list is arbitrary memory content, such as
+a graph the client reads. The argument installation is absorbed into the exchange constant; the
+bound includes the trailing halt. -/
+theorem exists_init_program (h : RealizesRand .exact p input output safe time calls) :
+    ∃ n C : ℕ,
+      ∃ emit : ∀ {r : ℕ}, (frontier : Fin r) → (Fin k → Fin r) →
+          (Fin (l + n + 1) → Fin r) → Code .exact r,
+        ∀ {r : ℕ} (frontier : Fin r) (src : Fin k → Fin r)
+          (tmp : Fin (l + n + 1) → Fin r),
+          Function.Injective src → Function.Injective tmp → (∀ i j, src i ≠ tmp j) →
+          (∀ j, tmp j ≠ frontier) → (∀ i, src i ≠ frontier) →
+          ∀ (i : Fin l) (w : ℕ) (d : δ) (xs : List ℕ), (∀ j : Fin k, xs.getD j.val 0 = input d j) →
+          k ≤ xs.length → Fits w (xs.length + 1) → InputFits w xs → safe w d (inputState xs) →
+          (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid (inputState xs) (p d) →
+          ∀ F : RandCfg r → ℕ × Memory.State,
+          (∀ v y, F (.halted v y) = (v, memoryState frontier y)) →
+          RandHaltsWithin w ((Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src)
+              (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) i)))
+            (State.init xs) (C * (time d (inputState xs) + 1) + 1) ∧
+          RandCallsBounded w ((Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src)
+              (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) i)))
+            (State.init xs) (C * (time d (inputState xs) + 1) + 1) (calls d (inputState xs)) ∧
+          (evalRand w ((Code.seq (inputPrefix frontier (tmp (Fin.last (l + n))) src)
+              (emit frontier src tmp)).program (tmp (Fin.castAdd (n + 1) i)))
+            (C * (time d (inputState xs) + 1) + 1) (State.init xs)).map F =
+            ((Memory.spec w).toRandomized.withCoins.run (p d) (inputState xs)).map
+              fun (a, s) => (output a i, s) := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨n, C + (2 * k + 5), emit, ?_⟩
+  intro r frontier src tmp hsrc htmp hd hf hs i w d xs hlayout hk hw hin hsafe hv F hF
+  obtain ⟨x, ex, hx, hm, hwords, -⟩ :=
+    inputPrefix_exec frontier (tmp (Fin.last (l + n))) src xs hsrc
+      (hf _) (fun j => hd j _) hs hk hw hin
+  have harg : x.regs ∘ src = input d := funext fun j => (hwords j).trans (hlayout j)
+  have h₁ := (he frontier src tmp htmp hd hf hs).2 w d x hx harg (hm.symm ▸ hsafe)
+    (hm.symm ▸ hv)
+  rw [hm] at h₁
+  have h₂ := ExecRandLaw.seq_det ex (h₁.map fun (v, s) => (v i, s))
+  have hT : 2 * k + 5 + C * (time d (inputState xs) + 1) + 1 ≤
+      (C + (2 * k + 5)) * (time d (inputState xs) + 1) + 1 := by
+    rw [Nat.add_mul]
+    have := Nat.mul_le_mul_left (2 * k + 5) (Nat.le_add_left 1 (time d (inputState xs)))
+    omega
+  obtain ⟨hhalt, hcalls, -, hlaw⟩ := h₂.program (tmp (Fin.castAdd (n + 1) i)) hT F
+    fun y _ => hF _ y
+  refine ⟨hhalt, hcalls, hlaw.trans ?_⟩
+  rw [PMF.map_comp]
+  rfl
+
+end RealizesRand
+
+end Cslib.WordRAM.Realization
diff --git a/Complexity/Computability/WordRAM/Realization/RandomLoop.lean b/Complexity/Computability/WordRAM/Realization/RandomLoop.lean
new file mode 100644
index 0000000000..bb7dbf43f9
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/RandomLoop.lean
@@ -0,0 +1,334 @@
+/-
+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.Loop
+public import Complexity.Computability.WordRAM.Realization.Random
+
+/-!
+# Runtime-bounded loops with private coins
+
+`RealizesRand.iterate` realizes a runtime-bounded loop whose body is a memory client with private
+coins. The loop is any family `loop d n a` satisfying the iteration equations
+`loop d 0 a = pure a` and `loop d (n + 1) a = body (d, a) >>= loop d n`. The client need not be
+rewritten into a canonical form: a recursive client such as `link methods (contractTimes n)`
+satisfies these equations directly. The native code is the loop of `Realizes.iterateRuntime`
+(`loopEmit`) around the body's emitter.
+
+Every body run must satisfy the body's domain, and the body's time and `rand` budgets must stay
+within the uniform per-iteration budgets `T` and `R`, at every state that the loop reaches with
+positive probability. With `n` iterations the loop then takes `n * (T + 1)` units of time and at
+most `n * R` `rand` calls on every path. Its law is the law of the loop's run.
+
+## Main results
+
+* `RealizesRand.iterate`: one uniform body certificate realizes a runtime-bounded loop.
+
+The rule is original infrastructure over the existing native loop and `ExecRandLaw`.
+-/
+
+@[expose] public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+variable {δ σ : Type} {k l : ℕ}
+
+namespace RealizesRand
+
+/-- **Loops.** One uniform body certificate realizes a runtime-bounded loop, given by its
+iteration equations. The visible domain asks for the body's domain and per-iteration budgets at
+every supported state reached after fewer than `fuel` iterations. -/
+theorem iterate (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l → ℕ))
+    {body : δ × σ → ProbOracleComp Memory.Op.Result σ}
+    {loop : δ → ℕ → σ → ProbOracleComp Memory.Op.Result σ}
+    (hzero : ∀ d a, loop d 0 a = pure a)
+    (hsucc : ∀ d n a, loop d (n + 1) a = body (d, a) >>= loop d n)
+    {safe : ℕ → δ × σ → Memory.State → Prop} {time calls : δ × σ → Memory.State → ℕ}
+    (T R : (δ × σ) × ℕ → Memory.State → ℕ)
+    (h : RealizesRand .exact body (appendWords input output) output safe time calls) :
+    RealizesRand .exact (fun ((d, a), fuel) => loop d fuel a)
+      (((appendWords input output).prodMap (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding).trans
+        (Fin.appendEquiv (k + l) 1).toEmbedding) output
+      (fun w ((d, a), fuel) s => ∀ j < fuel, ∀ b s',
+        (b, s') ∈ ((Memory.spec w).toRandomized.withCoins.run (loop d j a) s).support →
+          safe w (d, b) s' ∧ time (d, b) s' ≤ T ((d, a), fuel) s ∧
+            calls (d, b) s' ≤ R ((d, a), fuel) s)
+      (fun ((d, a), fuel) s => fuel * (T ((d, a), fuel) s + 1))
+      (fun ((d, a), fuel) s => fuel * R ((d, a), fuel) s) := by
+  obtain ⟨n, C, emit, he⟩ := h
+  refine ⟨l + n + 3, C + l + 5, loopEmit emit, ?_⟩
+  intro r frontier src tmp hi hd hf hs
+  let st : Fin l → Fin r := fun i => tmp (stateSlot i)
+  let ctr := tmp (counterSlot l n)
+  let zero := tmp (zeroSlot l n)
+  let one := tmp (oneSlot l n)
+  let bt : Fin (l + n + 1) → Fin r := fun i => tmp (bodySlot i)
+  let env : Fin k → Fin r := fun i => src ⟨i.val, by omega⟩
+  let bs := Fin.append env st
+  have hval {a b : Fin (l + (l + n + 3) + 1)} (h : tmp a = tmp b) : a.val = b.val :=
+    congrArg Fin.val (hi h)
+  have hst : Function.Injective st := fun i j h => Fin.ext (hval h)
+  have hbt : Function.Injective bt := fun i j h => by
+    have := hval h
+    dsimp only [bodySlot] at this
+    exact Fin.ext (by omega)
+  have hbdis : ∀ i j, bs i ≠ bt j := by
+    intro i j
+    refine Fin.addCases (fun i => ?_) (fun i => ?_) i
+    · simpa only [bs, Fin.append_left] using hd (⟨i.val, by omega⟩ : Fin (k + l + 1)) (bodySlot j)
+    · simp only [bs, Fin.append_right]
+      intro h
+      have := hval h
+      dsimp only [stateSlot, bodySlot] at this
+      omega
+  have hbs : ∀ i, bs i ≠ frontier := by
+    intro i
+    refine Fin.addCases (fun i => ?_) (fun i => ?_) i
+    · simpa only [bs, Fin.append_left] using hs (⟨i.val, by omega⟩ : Fin (k + l + 1))
+    · simpa only [bs, Fin.append_right] using hf (stateSlot i)
+  obtain ⟨hnw, hrun⟩ := he frontier bs bt hbt hbdis (fun j => hf _) hbs
+  have houtdis : ∀ i j : Fin l, bt (Fin.castAdd (n + 1) i) ≠ st j := fun i j h => by
+    have := hval h
+    dsimp only [bodySlot, stateSlot] at this
+    omega
+  have hct : ctr ≠ zero := fun h => by have := hval h; simp [counterSlot, zeroSlot] at this
+  have hco : ctr ≠ one := fun h => by have := hval h; simp [counterSlot, oneSlot] at this
+  have hzo : zero ≠ one := fun h => by have := hval h; simp [zeroSlot, oneSlot] at this
+  have hregbt (a : Fin (l + (l + n + 3) + 1)) (ha : a.val < l + 3) : ∀ j, bt j ≠ tmp a :=
+    fun j h => by
+      have := hval h
+      dsimp only [bodySlot] at this
+      omega
+  have hregst (a : Fin (l + (l + n + 3) + 1)) (ha : l ≤ a.val) : ∀ i, st i ≠ tmp a :=
+    fun i h => by
+      have := hval h
+      dsimp only [stateSlot] at this
+      omega
+  refine ⟨?_, ?_⟩
+  · change ¬(loopEmit emit frontier src tmp).ReadsWidth
+    simpa [loopEmit, loopBody, Code.ReadsWidth, Op.ReadsWidth, Op.exactBin,
+      copyBank_not_readsWidth] using hnw
+  intro w ⟨⟨d₀, a₀⟩, fuel⟩ x hx hin hsafe hv
+  let s₀ := memoryState frontier x
+  let D := (Memory.spec w).toRandomized.withCoins
+  let T₀ := T ((d₀, a₀), fuel) s₀
+  let R₀ := R ((d₀, a₀), fuel) s₀
+  let K := C * (T₀ + 1) + l + 5
+  let Q : Data r → Prop := fun y => ∀ i, i ≠ frontier → (∀ j, tmp j ≠ i) → y.regs i = x.regs i
+  let obs : Data r → (Fin l → ℕ) × Memory.State :=
+    fun y => (fun i => y.regs (st i), memoryState frontier y)
+  let F : σ × Memory.State → (Fin l → ℕ) × Memory.State := fun (b, s) => (output b, s)
+  let Good : ℕ → σ → Memory.State → Prop := fun j a s => ∀ i < j, ∀ b s',
+    (b, s') ∈ (D.run (loop d₀ i a) s).support →
+      safe w (d₀, b) s' ∧ time (d₀, b) s' ≤ T₀ ∧ calls (d₀, b) s' ≤ R₀
+  let I : ℕ → σ → Memory.State → Data r → Prop := fun j a s y =>
+    y.Bounded w ∧ memoryState frontier y = s ∧ (∀ i, y.regs (env i) = input d₀ i) ∧
+      (∀ i, y.regs (st i) = output a i) ∧ y.regs ctr = j ∧ y.regs zero = 0 ∧ Good j a s ∧
+      (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid s (loop d₀ j a) ∧ Q y
+  have key : ∀ j a s y, I j a s y →
+      ExecRandLaw w (.loop (.lt zero ctr) (loopBody emit frontier src tmp)) y Q (j * K + 2)
+        (j * R₀) obs ((D.run (loop d₀ j a) s).map F) := by
+    intro j
+    induction j with
+    | zero =>
+      rintro a s y ⟨-, hym, -, hys, hyc, hyz, -, -, hyQ⟩
+      have hexit : ¬(Cond.lt zero ctr).Holds y := by
+        change ¬y.regs zero < y.regs ctr
+        rw [hyc, hyz]
+        exact Nat.lt_irrefl 0
+      refine ((ExecRandLaw.loop_exit (body := loopBody emit frontier src tmp) (P := Q) (f := obs)
+        hexit hyQ).mono (fun _ h => h) (by simp) (Nat.zero_le _)).congr_law ?_
+      rw [hzero, RandomizedSpec.run_pure, PMF.pure_map]
+      exact congrArg PMF.pure (Prod.ext (funext hys) hym)
+    | succ j ih =>
+      rintro a s y ⟨hyb, hym, hye, hys, hyc, hyz, hgood, hyv, hyQ⟩
+      have hself : (a, s) ∈ (D.run (loop d₀ 0 a) s).support := by
+        rw [hzero, RandomizedSpec.run_pure, PMF.support_pure]
+        rfl
+      obtain ⟨hsafe₀, htime₀, hcalls₀⟩ := hgood 0 (Nat.succ_pos j) a s hself
+      rw [hsucc] at hyv
+      have hyv' : D.toSpec.DemonicValid s ((body (d₀, a)).bind (loop d₀ j)) := hyv
+      obtain ⟨hvB, hvL⟩ := StateTransitionSpec.DemonicValid.of_bind hyv'
+      have hinbody : y.regs ∘ bs = (appendWords input output) (d₀, a) := by
+        funext i
+        refine Fin.addCases (fun i => ?_) (fun i => ?_) i
+        · simpa [bs, appendWords, Fin.appendEquiv] using hye i
+        · simpa [bs, appendWords, Fin.appendEquiv] using hys i
+      let ν := (D.run (body (d₀, a)) s).map F
+      have hB := ((hrun w (d₀, a) y hyb hinbody (hym ▸ hsafe₀) (hym ▸ hvB)).withBounded
+        hyb).withSupport
+      rw [hym] at hB
+      -- The deterministic tail of an iteration: copy the result into the state words and count
+      -- down.
+      let P' : Data r → Prop := fun y' => y'.Bounded w ∧ (∀ i, y'.regs (env i) = input d₀ i) ∧
+        y'.regs ctr = j ∧ y'.regs zero = 0 ∧ Q y' ∧ obs y' ∈ ν.support
+      have hbody : ExecRandLaw w (loopBody emit frontier src tmp) y P'
+          (C * (time (d₀, a) s + 1) + (l + 1 + (1 + 1))) (calls (d₀, a) s + 0) obs
+          (ν.bind PMF.pure) := by
+        refine ExecRandLaw.seq hB fun u ⟨⟨huf, hub⟩, husup⟩ => ?_
+        obtain ⟨v, hv', hvm, hvs, hvf⟩ := copyBank_exec
+          (fun i : Fin l => bt (Fin.castAdd (n + 1) i)) st zero hst houtdis w u
+        have hvctr : v.regs ctr = j + 1 := by
+          rw [hvf _ (hregst _ (by simp [counterSlot])),
+            huf _ (hf _) (hregbt _ (by simp [counterSlot]))]
+          exact hyc
+        have hvzero : v.regs zero = 0 := by
+          rw [hvf _ (hregst _ (by simp [zeroSlot])), huf _ (hf _) (hregbt _ (by simp [zeroSlot]))]
+          exact hyz
+        have h1 : Fits w 1 := (hyb.1 ctr).of_le (by omega)
+        have hjfit : Fits w j := (hyb.1 ctr).of_le (by omega)
+        let t := v.set one 1
+        let y' := t.set ctr j
+        have ht : ExecWithin (B := .exact) w (.op (.const one 1)) v t 1 := ExecWithin.const h1
+        have htc : t.regs ctr = j + 1 := by
+          rw [show t.regs ctr = v.regs ctr from Function.update_of_ne hco _ _]
+          exact hvctr
+        have htone : t.regs one = 1 := by simp [t, Data.set]
+        have hdec : ExecWithin w (.op (.exactBin .sub ctr ctr one)) t y' 1 := by
+          apply ExecWithin.op
+          rw [Op.eval_exactBin, htc, htone]
+          simp only [BinOp.evalExact, Nat.le_add_left, ↓reduceIte, Nat.add_sub_cancel,
+            Option.bind_some]
+          exact Data.put_of_fits hjfit
+        have hobs : obs y' =
+            ((fun i : Fin l => u.regs (bt (Fin.castAdd (n + 1) i))), memoryState frontier u) := by
+          refine Prod.ext (funext fun i => ?_) (Memory.State.ext hvm ?_)
+          · change (t.set ctr j).regs (st i) = _
+            simp only [t, Data.set]
+            rw [Function.update_of_ne (hregst _ (by simp [counterSlot]) i),
+              Function.update_of_ne (hregst _ (by simp [oneSlot]) i), hvs]
+          · change (t.set ctr j).regs frontier = u.regs frontier
+            rw [show (t.set ctr j).regs frontier = t.regs frontier from
+              Function.update_of_ne (hf (counterSlot l n)).symm _ _,
+              show t.regs frontier = v.regs frontier from
+                Function.update_of_ne (hf (oneSlot l n)).symm _ _,
+              hvf frontier (fun i => hf _)]
+        rw [← hobs]
+        refine ExecRandLaw.of_execWithin (hv'.seq (ht.seq hdec)) ⟨?_, ?_, ?_, ?_, ?_, ?_⟩
+        · exact (hv'.seq (ht.seq hdec)).bounded hub
+        · intro i
+          simp only [y', t, Data.set]
+          rw [Function.update_of_ne (hd _ _), Function.update_of_ne (hd _ _),
+            hvf _ (fun _ => (hd _ _).symm), huf _ (hs _) (fun _ => (hd _ _).symm)]
+          exact hye i
+        · simp [y', Data.set]
+        · simp [y', t, Data.set, hct.symm, hzo, hvzero]
+        · intro i hif htmp
+          simp only [y', t, Data.set]
+          rw [Function.update_of_ne (htmp _).symm, Function.update_of_ne (htmp _).symm,
+            hvf _ (fun _ => htmp _), huf _ hif (fun _ => htmp _)]
+          exact hyQ i hif htmp
+        · rw [hobs]
+          exact husup
+      rw [PMF.bind_pure] at hbody
+      have : Nonempty σ := ⟨a⟩
+      let κ : (Fin l → ℕ) × Memory.State → PMF ((Fin l → ℕ) × Memory.State) := fun (v, s') =>
+        (D.run (loop d₀ j (Function.invFun output v)) s').map F
+      have hdecode : ∀ b, Function.invFun output (output b) = b :=
+        Function.leftInverse_invFun output.injective
+      have hcond : (Cond.lt zero ctr).Holds y := by
+        change y.regs zero < y.regs ctr
+        rw [hyc, hyz]
+        exact Nat.succ_pos j
+      refine ((ExecRandLaw.loop_iter (κ := κ) (Q := Q) (f := obs) (T₂ := j * K + 2)
+        (R₂ := j * R₀) hcond hbody
+        fun y' ⟨hy'b, hy'e, hy'c, hy'z, hy'Q, hy'sup⟩ => ?_).mono (fun _ h => h) ?_ ?_).congr_law
+        ?_
+      · obtain ⟨⟨b, s'⟩, hmem, hb⟩ := (PMF.mem_support_map_iff _ _ _).mp hy'sup
+        obtain ⟨hbout, hbs⟩ := Prod.mk.inj hb
+        obtain ⟨tr, hrunB⟩ := D.exists_clientRun_of_mem_support hvB hmem
+        have hκ : κ (obs y') = (D.run (loop d₀ j b) s').map F := by
+          change (D.run (loop d₀ j (Function.invFun output (fun i => y'.regs (st i))))
+            (memoryState frontier y')).map F = _
+          rw [← hbout, hdecode, ← hbs]
+        rw [hκ]
+        refine ih b s' y' ⟨hy'b, hbs.symm, hy'e, fun i => (congrFun hbout i).symm, hy'c, hy'z,
+          fun i hi b' s'' hmem' => hgood (i + 1) (by omega) b' s'' ?_, hvL b s' tr hrunB, hy'Q⟩
+        rw [hsucc, RandomizedSpec.run_bind, PMF.mem_support_bind_iff]
+        exact ⟨(b, s'), hmem, hmem'⟩
+      · have := Nat.mul_le_mul_left C (Nat.add_le_add_right htime₀ 1)
+        change C * (time (d₀, a) s + 1) + (l + 1 + (1 + 1)) +
+          (j * (C * (T₀ + 1) + l + 5) + 2) + 2 ≤ (j + 1) * (C * (T₀ + 1) + l + 5) + 2
+        rw [Nat.succ_mul]
+        omega
+      · rw [Nat.add_zero, Nat.succ_mul]
+        omega
+      · change ((D.run (body (d₀, a)) s).map F).bind κ = (D.run (loop d₀ (j + 1) a) s).map F
+        rw [PMF.bind_map, hsucc, RandomizedSpec.run_bind, PMF.map_bind]
+        congr 1
+        funext ⟨b, s'⟩
+        simp only [Function.comp_apply, κ, F, hdecode]
+  have henv (i : Fin k) : x.regs (env i) = input d₀ i := by
+    have hh : x.regs (src (Fin.castAdd 1 (Fin.castAdd l i))) = input d₀ i := by
+      simpa [appendWords, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.castAdd l i))
+    exact hh
+  have hstate (i : Fin l) : x.regs (src ⟨k + i.val, by omega⟩) = output a₀ i := by
+    have hh : x.regs (src (Fin.castAdd 1 (Fin.natAdd k i))) = output a₀ i := by
+      simpa [appendWords, Fin.appendEquiv] using congrFun hin (Fin.castAdd 1 (Fin.natAdd k i))
+    exact hh
+  have hfuel : x.regs (src ⟨k + l, by omega⟩) = fuel := by
+    have hh : x.regs (src (Fin.natAdd (k + l) 0)) = fuel := by
+      simpa [Fin.appendEquiv] using congrFun hin (Fin.natAdd (k + l) 0)
+    exact hh
+  obtain ⟨a, ha, ham, has, haf⟩ := copyBank_exec
+    (fun i : Fin l => src ⟨k + i.val, by omega⟩) st zero hst (fun _ _ => hd _ _) w x
+  let b := a.set ctr fuel
+  let z := b.set zero 0
+  have hafuel : a.regs (src ⟨k + l, by omega⟩) = fuel := by
+    rw [haf _ (fun _ => (hd _ _).symm)]
+    exact hfuel
+  have hc : ExecWithin (B := .exact) w (.op (.copy ctr (src ⟨k + l, by omega⟩))) a b 1 := by
+    simpa only [hafuel] using
+      (ExecWithin.copy (B := .exact) (w := w) (d := ctr) (s := src ⟨k + l, by omega⟩) (x := a))
+  have hz : ExecWithin (B := .exact) w (.op (.const zero 0)) b z 1 :=
+    ExecWithin.const (fits_zero w)
+  have hIz : I fuel a₀ s₀ z := by
+    refine ⟨(ha.seq (hc.seq hz)).bounded hx, ?_, ?_, ?_, ?_, ?_, hsafe, hv, ?_⟩
+    · apply Memory.State.ext
+      · exact ham
+      · change (b.set zero 0).regs frontier = x.regs frontier
+        rw [show (b.set zero 0).regs frontier = b.regs frontier from
+          Function.update_of_ne (hf (zeroSlot l n)).symm _ _,
+          show b.regs frontier = a.regs frontier from
+            Function.update_of_ne (hf (counterSlot l n)).symm _ _,
+          haf frontier (fun i => hf _)]
+    · intro i
+      simp only [z, b, Data.set]
+      rw [Function.update_of_ne (hd _ _), Function.update_of_ne (hd _ _),
+        haf _ (fun _ => (hd _ _).symm)]
+      exact henv i
+    · intro i
+      simp only [z, b, Data.set]
+      rw [Function.update_of_ne (hregst _ (by simp [zeroSlot]) i),
+        Function.update_of_ne (hregst _ (by simp [counterSlot]) i), has]
+      exact hstate i
+    · simp [z, b, Data.set, hct]
+    · simp [z, Data.set]
+    · intro i hif htmp
+      simp only [z, b, Data.set]
+      rw [Function.update_of_ne (htmp _).symm,
+        Function.update_of_ne (htmp _).symm, haf _ (fun _ => htmp _)]
+  have hloop := ExecRandLaw.seq_det ha (ExecRandLaw.seq_det hc (ExecRandLaw.seq_det hz
+    (key fuel a₀ s₀ z hIz)))
+  refine hloop.mono (fun _ h => h) ?_ le_rfl
+  change l + 1 + (1 + (1 + (fuel * (C * (T₀ + 1) + l + 5) + 2))) ≤
+    (C + l + 5) * (fuel * (T₀ + 1) + 1)
+  have h₁ : fuel * (l + 5) ≤ (l + 5) * (fuel * (T₀ + 1)) := by
+    rw [Nat.mul_comm fuel]
+    exact Nat.mul_le_mul_left _ (Nat.le_mul_of_pos_right _ (Nat.succ_pos _))
+  have h₂ : fuel * (C * (T₀ + 1) + l + 5) = C * (fuel * (T₀ + 1)) + fuel * (l + 5) := by ring
+  have h₃ : (C + l + 5) * (fuel * (T₀ + 1) + 1) =
+      C * (fuel * (T₀ + 1)) + (l + 5) * (fuel * (T₀ + 1)) + (C + l + 5) := by ring
+  rw [h₂, h₃]
+  omega
+
+end RealizesRand
+
+end Cslib.WordRAM.Realization
diff --git a/Complexity/DataStructure/StateTransition.lean b/Complexity/DataStructure/StateTransition.lean
index 032f4dac9f..35e0341482 100644
--- a/Complexity/DataStructure/StateTransition.lean
+++ b/Complexity/DataStructure/StateTransition.lean
@@ -64,7 +64,8 @@ The relational semantics is **demonic** for callers and **angelic** for implemen
   `StateTransitionSpec.DemonicValid.exists_clientRun`: existence of valid runs under
   `[StateTransitionSpec.Total]`.
 * `StateTransitionSpec.ClientRun.bind`, `StateTransitionSpec.clientRun_bind_iff`,
-  `StateTransitionSpec.DemonicValid.bind`: sequential composition for relational adaptive clients.
+  `StateTransitionSpec.DemonicValid.bind`, `StateTransitionSpec.DemonicValid.of_bind`: sequential
+  composition and decomposition for relational adaptive clients.
 * `StateTransitionSpec.validOpSeq_iff_validHistory`, `StateTransitionSpec.validTranscript_iff_run`,
   `StateTransitionSpec.demonicValid_iff_validHistory_runClient`,
   `StateTransitionSpec.clientRun_iff_runClient`: equivalence of relational and functional semantics
@@ -558,6 +559,23 @@ theorem DemonicValid.bind {D : StateTransitionSpec.{u, v, w}} {s : D.State} {p :
     exact ih s₁ r hstep fun a s₂ tr hrun => hk a s₂ (⟨o, r, s₁⟩ :: tr)
       (.liftBind o cont r hv_o hstep hrun)
 
+/-- Demonic admissibility of `p.bind k` splits: `p` is demonically admissible, and so is the
+continuation after every valid run of `p`. This is the converse of `DemonicValid.bind`. -/
+theorem DemonicValid.of_bind {D : StateTransitionSpec.{u, v, w}} {s : D.State} {p : D.Client α}
+    {k : α → D.Client β} (h : D.DemonicValid s (p.bind k)) :
+    D.DemonicValid s p ∧ ∀ a s' tr, D.ClientRun s p a s' tr → D.DemonicValid s' (k a) := by
+  induction p generalizing s with
+  | pure a =>
+    refine ⟨.pure s a, fun b s' tr hrun => ?_⟩
+    obtain ⟨rfl, rfl, -⟩ := (clientRun_pure_iff s a b s' tr).mp hrun
+    exact h
+  | liftBind o cont ih =>
+    obtain ⟨hv, hk⟩ := (demonicValid_liftBind_iff s o fun r => (cont r).bind k).mp h
+    refine ⟨.liftBind o cont hv fun s₁ r hstep => (ih r (hk s₁ r hstep)).1,
+      fun b s₂ tr hrun => ?_⟩
+    obtain ⟨-, r, s₁, tr', hstep, hrest, -⟩ := (clientRun_liftBind_iff s o cont b s₂ tr).mp hrun
+    exact (ih r (hk s₁ r hstep)).2 b s₂ tr' hrest
+
 /-! ## Deterministic specifications (`StateTransitionSpec.ofFn`, `StateTransitionSpec.HasStepFn`)
 and functional helpers -/
 
diff --git a/Complexity/DataStructure/StateTransition/Randomized.lean b/Complexity/DataStructure/StateTransition/Randomized.lean
index de38badc36..1a6d1b7993 100644
--- a/Complexity/DataStructure/StateTransition/Randomized.lean
+++ b/Complexity/DataStructure/StateTransition/Randomized.lean
@@ -78,10 +78,12 @@ with coins (`RandomizedRefinement.compCoins`), and expected potentials stack acr
 
 * `RandomizedSpec.mem_support_run_of_clientRun`, `RandomizedSpec.exists_clientRun_of_mem_support`:
   the support of a run consists of the relational runs.
-* `StateTransitionSpec.run_toRandomized`, `StateTransitionSpec.toRandomized_step_iff`: a
-  deterministic run is a point mass, and the support of a deterministic specification is itself.
-* `RandomizedSpec.demonicValid_liftRight`, `RandomizedSpec.demonicValid_sample_bind`: coin calls
-  are admissible, and programs over `E` keep their admissibility.
+* `StateTransitionSpec.run_toRandomized`, `StateTransitionSpec.toRandomized_step_iff`,
+  `StateTransitionSpec.toRandomized_demonicValid_iff`: a deterministic run is a point mass, and the
+  support of a deterministic specification is itself, with the same admissible clients.
+* `RandomizedSpec.demonicValid_liftRight`, `RandomizedSpec.demonicValid_liftRight_iff`,
+  `RandomizedSpec.demonicValid_sample_bind`: coin calls are admissible, and programs over `E`
+  keep their admissibility.
 * `RandomizedSpec.expectedCost_bind`, `RandomizedSpec.expectedCost_le_of_isCostBounded`,
   `RandomizedSpec.isCostBounded_obliviousClient`: expected charges of sequenced programs, and
   query budgets.
@@ -301,6 +303,18 @@ theorem demonicValid_liftRight {p : D.toSpec.Client α} {s : D.toSpec.State}
     exact StateTransitionSpec.DemonicValid.liftBind (D := D.withCoins.toSpec) (Sum.inr o)
       (fun a => OracleComp.liftRight (k a)) hv fun s' a hstep => ih s' a hstep
 
+/-- A program over `E` is admissible over `E.withCoins` exactly when it is admissible over `E`. -/
+theorem demonicValid_liftRight_iff {p : D.toSpec.Client α} {s : D.toSpec.State} :
+    D.withCoins.toSpec.DemonicValid s (OracleComp.liftRight p) ↔ D.toSpec.DemonicValid s p := by
+  refine ⟨fun h => ?_, demonicValid_liftRight⟩
+  induction p generalizing s with
+  | pure a => exact .pure s a
+  | liftBind o k ih =>
+    obtain ⟨hv, hk⟩ := (StateTransitionSpec.demonicValid_liftBind_iff (D := D.withCoins.toSpec) s
+      (Sum.inr o) fun a => OracleComp.liftRight (k a)).mp h
+    exact StateTransitionSpec.DemonicValid.liftBind (D := D.toSpec) o k hv
+      fun s' a hstep => ih a (hk s' a hstep)
+
 /-- Coin calls are admissible, and leave the state unchanged. -/
 theorem demonicValid_sample_bind {q : ProbComp β} {k : β → OracleComp D.withCoins.Result α}
     {s : D.State} (h : ∀ b, D.withCoins.toSpec.DemonicValid s (k b)) :
@@ -420,6 +434,18 @@ theorem toRandomized_demonicValid {p : D.Client α} {s : D.State} (h : D.Demonic
     exact StateTransitionSpec.DemonicValid.liftBind (D := D.toRandomized.toSpec) o k hv
       fun s' a hstep => ih s' a ((toRandomized_step_iff _ _ _ _).mp hstep)
 
+/-- Admissibility on the support of a deterministic specification is admissibility on it. -/
+theorem toRandomized_demonicValid_iff {p : D.Client α} {s : D.State} :
+    D.toRandomized.toSpec.DemonicValid s p ↔ D.DemonicValid s p := by
+  refine ⟨fun h => ?_, toRandomized_demonicValid⟩
+  induction p generalizing s with
+  | pure a => exact .pure s a
+  | liftBind o k ih =>
+    obtain ⟨hv, hk⟩ := (StateTransitionSpec.demonicValid_liftBind_iff
+      (D := D.toRandomized.toSpec) s o k).mp h
+    exact StateTransitionSpec.DemonicValid.liftBind (D := D) o k hv fun s' a hstep =>
+      ih a (hk s' a ((toRandomized_step_iff _ _ _ _).mpr hstep))
+
 /-- Admissibility of a deterministic history is admissibility on the support. -/
 theorem toRandomized_demonicValid_of_validHistory {p : D.Client α} {s : D.State}
     (h : D.ValidHistory s (D.clientHistory s p)) : D.toRandomized.toSpec.DemonicValid s p :=
diff --git a/ComplexityTests/WordRAMRealizationRandom.lean b/ComplexityTests/WordRAMRealizationRandom.lean
new file mode 100644
index 0000000000..bdee5d574a
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizationRandom.lean
@@ -0,0 +1,281 @@
+/-
+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.RandomLoop
+import Complexity.Tactic.Realize
+
+/-! `RealizesRand` end to end: sample a uniformly random input word.
+
+The client `sample` reads the input length, draws a uniform index below it, and reads that input
+word. Its two memory reads are certified by `realize` and enter through `Realizes.toRand`; the
+draw is `RealizesRand.coin`. On every path the flat program from the list input halts within a
+fixed bound and makes at most one `rand` call. It chooses an input position uniformly, retaining
+repeated values (`sample_program`). Repeated in a loop (`RealizesRand.iterate`), every path takes
+`6` units of time and at most one `rand` call per iteration. -/
+
+namespace ComplexityTests.WordRAMRealizationRandom
+
+open Cslib Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization
+
+/-- One word. -/
+abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+/-- No words. -/
+abbrev unitWords : Unit ↪ (Fin 0 → ℕ) := (Equiv.ofUnique Unit (Fin 0 → ℕ)).toEmbedding
+
+/-- The largest input index: the input length, less one. -/
+def lastIndex : Memory.Prog ℕ := do
+  let n ← Memory.read 0
+  pure (n - 1)
+
+/-- A uniform index `c ≤ n`. -/
+noncomputable abbrev index (n : ℕ) : ProbOracleComp Memory.Op.Result ℕ :=
+  Fin.val <$> ProbOracleComp.sample (ProbComp.unifFin n)
+
+/-- **Sample an input word**: draw a uniform index below the input length, and read that word. -/
+noncomputable def sample : ProbOracleComp Memory.Op.Result ℕ := do
+  let n ← OracleComp.liftRight lastIndex
+  let c ← index n
+  OracleComp.liftRight (Memory.read (c + 1))
+
+/-! ## The law -/
+
+/-- The law of `sample` from any memory: a uniform index `c` below the length cell, the cell
+`c + 1`, and the memory unchanged. -/
+theorem run_sample (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).toRandomized.withCoins.run sample s =
+      (Probability.PMF.uniformOfFintype (Fin (s.mem 0 - 1 + 1))).map
+        fun c => (s.mem (c.val + 1), s) := by
+  rw [sample, RandomizedSpec.run_bind, RandomizedSpec.withCoins_run_liftRight,
+    StateTransitionSpec.run_toRandomized, PMF.pure_bind]
+  change (Memory.spec w).toRandomized.withCoins.run
+    (index (s.mem 0 - 1) >>= fun c => OracleComp.liftRight (Memory.read (c + 1))) s = _
+  rw [RandomizedSpec.run_bind, RandomizedSpec.run_map, RandomizedSpec.withCoins_run_sample,
+    ProbComp.eval_unifFin, PMF.map_comp, PMF.bind_map, ← PMF.bind_pure_comp]
+  congr 1
+  funext c
+  simp only [Function.comp_apply]
+  rw [RandomizedSpec.withCoins_run_liftRight, StateTransitionSpec.run_toRandomized]
+  rfl
+
+/-- On the list input, `sample` chooses a position uniformly, retaining repeated values. -/
+theorem run_sample_inputState (w : ℕ) (xs : List ℕ) :
+    ((Memory.spec w).toRandomized.withCoins.run sample (inputState xs)).map Prod.fst =
+      (Probability.PMF.uniformOfFintype (Fin (xs.length - 1 + 1))).map
+        fun c => xs.getD c.val 0 := by
+  rw [run_sample, PMF.map_comp]
+  rfl
+
+/-- `sample` leaves the memory unchanged on every path. -/
+theorem eq_of_mem_support_sample {w : ℕ} {s s' : Memory.State} {v : ℕ}
+    (h : (v, s') ∈ ((Memory.spec w).toRandomized.withCoins.run sample s).support) : s' = s := by
+  rw [run_sample, PMF.mem_support_map_iff] at h
+  obtain ⟨c, -, hc⟩ := h
+  exact (congrArg Prod.snd hc).symm
+
+/-- Every call of `sample` is admissible when the length cell is positive and allocated. -/
+theorem demonicValid_sample {w : ℕ} {s : Memory.State} (h0 : 1 ≤ s.mem 0)
+    (hf : s.mem 0 < s.frontier) :
+    (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid s sample := by
+  refine StateTransitionSpec.DemonicValid.bind (D := (Memory.spec w).toRandomized.withCoins.toSpec)
+    (p := OracleComp.liftRight lastIndex)
+    (RandomizedSpec.demonicValid_liftRight
+      (StateTransitionSpec.toRandomized_demonicValid_of_validHistory (D := Memory.spec w)
+        (p := lastIndex) (s := s) (And.intro (show 0 < s.frontier by omega) trivial)))
+    fun n s' tr hrun => ?_
+  have hmem := RandomizedSpec.mem_support_run_of_clientRun _ hrun
+  rw [RandomizedSpec.withCoins_run_liftRight, StateTransitionSpec.run_toRandomized,
+    PMF.mem_support_pure_iff] at hmem
+  obtain ⟨hn, hs'⟩ := Prod.mk.inj hmem
+  subst n s'
+  change (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid s
+    (index (s.mem 0 - 1) >>= fun c => OracleComp.liftRight (Memory.read (c + 1)))
+  rw [bind_map_left]
+  refine RandomizedSpec.demonicValid_sample_bind fun c => ?_
+  have hc := c.isLt
+  exact RandomizedSpec.demonicValid_liftRight
+    (StateTransitionSpec.toRandomized_demonicValid_of_validHistory (D := Memory.spec w)
+      (p := Memory.read (c.val + 1)) (s := s)
+      (And.intro (show c.val + 1 < s.frontier by omega) trivial))
+
+/-! ## The certificate -/
+
+/-- The appended word of an environment. -/
+theorem appendWords_last {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ)) (d : δ) (a : ℕ) :
+    (appendWords input word) (d, a) (Fin.natAdd k 0) = a := by
+  simp [appendWords, Fin.appendEquiv]
+
+/-- `sample` in any environment of word encodings, from certificates of its two reads. -/
+theorem realizesRand_sample {δ : Type} {k : ℕ} (input : δ ↪ (Fin k → ℕ))
+    (hlast : Realizes .exact (fun _ : δ => lastIndex) input word
+      (fun _ _ s => 1 ≤ s.mem 0) (fun _ _ => 0))
+    (hread : Realizes .exact (fun e : (δ × ℕ) × ℕ => Memory.read (e.2 + 1))
+      (appendWords (appendWords input word) word) word (fun w e _ => Fits w (e.2 + 1))
+      (fun _ _ => 0)) :
+    RealizesRand .exact (fun _ => sample) input word (fun _ _ s => 1 ≤ s.mem 0)
+      (fun _ _ => 5) (fun _ _ => 1) := by
+  have hinner := (RealizesRand.coin (B := .exact) (appendWords input word) (Fin.natAdd k 0)).bind
+    hread.toRand (fun _ _ => 1) (fun _ _ => 0)
+  refine ((hlast.toRand.bind hinner (fun _ _ => 3) (fun _ _ => 1)).congr fun d => ?_).consequence
+    ?_
+  · unfold sample
+    congr 1
+    funext a
+    rw [appendWords_last]
+  · intro w d s _ hs h0
+    refine ⟨⟨h0, fun n s' hmem => ?_⟩, le_rfl, le_rfl⟩
+    rw [RandomizedSpec.withCoins_run_liftRight, StateTransitionSpec.run_toRandomized,
+      PMF.mem_support_pure_iff] at hmem
+    obtain ⟨hn, hs'⟩ := Prod.mk.inj hmem
+    subst n s'
+    refine ⟨⟨trivial, fun c s'' hc => ⟨?_, le_rfl, le_rfl⟩⟩, le_rfl, le_rfl⟩
+    rw [RandomizedSpec.run_map, RandomizedSpec.withCoins_run_sample, ProbComp.eval_unifFin,
+      PMF.map_comp, PMF.mem_support_map_iff] at hc
+    obtain ⟨c', -, hc'⟩ := hc
+    have hcv : c = c'.val := (congrArg Prod.fst hc').symm
+    have hbound : (appendWords input word) (d, (Memory.spec w).clientResult s lastIndex)
+        (Fin.natAdd k 0) + 1 = s.mem 0 - 1 + 1 := by
+      rw [appendWords_last]
+      rfl
+    have hlt : c'.val < s.mem 0 - 1 + 1 := c'.isLt.trans_eq hbound
+    exact (hs.mem_fits 0).of_le (by omega)
+
+/-- `sample` with no environment: both reads by `realize`. -/
+theorem realizesRand_sample_unit :
+    RealizesRand .exact (fun _ : Unit => sample) unitWords word (fun _ _ s => 1 ≤ s.mem 0)
+      (fun _ _ => 5) (fun _ _ => 1) :=
+  realizesRand_sample unitWords (by realize; exact h) (by realize; exact h)
+
+/-! ## The flat program -/
+
+/-- The output word and the memory of a halting configuration. -/
+def observe {r : ℕ} (frontier : Fin r) : RandCfg r → ℕ × Memory.State
+  | .halted v y => (v, memoryState frontier y)
+  | _ => (0, ⟨fun _ => 0, 0⟩)
+
+/-- **End to end.** One flat word-RAM program samples a uniform input position: from every
+nonempty input that fits, it halts within `T` steps on every path, makes at most one `rand`
+call, and returns the word at the chosen position. Repeated values retain their multiplicity. -/
+theorem sample_program : ∃ (r : ℕ) (prog : Program .exact r) (T : ℕ),
+    ∀ (w : ℕ) (xs : List ℕ), xs ≠ [] → Fits w (xs.length + 1) → InputFits w xs →
+      RandHaltsWithin w prog (State.init xs) T ∧ RandCallsBounded w prog (State.init xs) T 1 ∧
+      ∃ out : RandCfg r → ℕ, (evalRand w prog T (State.init xs)).map out =
+        (Probability.PMF.uniformOfFintype (Fin (xs.length - 1 + 1))).map
+        fun c => xs.getD c.val 0 := by
+  obtain ⟨n, C, emit, he⟩ := realizesRand_sample_unit.exists_init_program
+  let frontier : Fin (1 + n + 1 + 1) := Fin.last _
+  let tmp : Fin (1 + n + 1) → Fin (1 + n + 1 + 1) := Fin.castSucc
+  have hrun := he frontier Fin.elim0 tmp (fun i => i.elim0) (Fin.castSucc_injective _)
+    (fun i => i.elim0) (fun j => Fin.castSucc_ne_last j) (fun i => i.elim0)
+  refine ⟨1 + n + 1 + 1, (Code.seq (inputPrefix frontier (tmp (Fin.last (1 + n))) Fin.elim0)
+    (emit frontier Fin.elim0 tmp)).program (tmp (Fin.castAdd (n + 1) 0)), C * (5 + 1) + 1,
+    fun w xs hxs hw hin => ?_⟩
+  have hlen : 1 ≤ xs.length := List.length_pos_iff.mpr hxs
+  obtain ⟨hhalt, hcalls, hlaw⟩ := hrun 0 w () xs (fun j => j.elim0) (Nat.zero_le _) hw hin hlen
+    (demonicValid_sample hlen (by simp [inputState])) (observe frontier)
+    fun _ _ => rfl
+  refine ⟨hhalt, hcalls, fun cfg => (observe frontier cfg).1, ?_⟩
+  rw [show (fun cfg => (observe frontier cfg).1) = Prod.fst ∘ observe frontier from rfl,
+    ← PMF.map_comp, hlaw, PMF.map_comp, ← run_sample_inputState w xs]
+  rfl
+
+/-! ## A loop -/
+
+/-- Sample `n` input words, keeping the last. -/
+noncomputable def sampleTimes : ℕ → ℕ → ProbOracleComp Memory.Op.Result ℕ
+  | 0, a => pure a
+  | n + 1, _ => sample >>= sampleTimes n
+
+/-- Every iteration samples once, so every path of `n` iterations takes `6 n` units of time and at
+most `n` `rand` calls. -/
+example : RealizesRand .exact (fun ((_, a), fuel) => sampleTimes fuel a)
+    (((appendWords unitWords word).prodMap word).trans (Fin.appendEquiv (0 + 1) 1).toEmbedding)
+    word (fun _ _ s => 1 ≤ s.mem 0) (fun ((_, _), fuel) _ => fuel * 6)
+    (fun ((_, _), fuel) _ => fuel) := by
+  have hbody := realizesRand_sample (appendWords unitWords word) (by realize; exact h)
+    (by realize; exact h)
+  refine (RealizesRand.iterate unitWords word (loop := fun _ n a => sampleTimes n a)
+    (fun _ _ => rfl) (fun _ _ _ => rfl) (fun _ _ => 5) (fun _ _ => 1) hbody).consequence ?_
+  rintro w ⟨⟨_, a⟩, fuel⟩ s - - h0
+  refine ⟨fun j _ b s' hmem => ⟨?_, le_rfl, le_rfl⟩, le_rfl, by simp⟩
+  suffices ∀ j a b s', (b, s') ∈ ((Memory.spec w).toRandomized.withCoins.run
+      (sampleTimes j a) s).support → s' = s by
+    rw [this j a b s' hmem]
+    exact h0
+  intro j
+  induction j with
+  | zero =>
+    intro a b s' h
+    rw [sampleTimes, RandomizedSpec.run_pure, PMF.mem_support_pure_iff] at h
+    exact (congrArg Prod.snd h)
+  | succ j ih =>
+    intro a b s' h
+    rw [sampleTimes, RandomizedSpec.run_bind, PMF.mem_support_bind_iff] at h
+    obtain ⟨⟨v, s₁⟩, h₁, h₂⟩ := h
+    obtain rfl := eq_of_mem_support_sample h₁
+    exact ih v b s' h₂
+
+/-! ## An adaptive write retains the joint result/memory law -/
+
+/-- Sample an input word, then store the sampled value in the length cell. -/
+noncomputable def storeSample : ProbOracleComp Memory.Op.Result ℕ := do
+  let v ← sample
+  OracleComp.liftRight (do
+    Memory.write 0 v
+    pure v)
+
+/-- The returned value and the updated cell are correlated, while every other cell and the
+frontier are unchanged. Separate result and memory marginals would not express this law. -/
+theorem run_storeSample (w : ℕ) (s : Memory.State) :
+    (Memory.spec w).toRandomized.withCoins.run storeSample s =
+      (Probability.PMF.uniformOfFintype (Fin (s.mem 0 - 1 + 1))).map fun c =>
+        (s.mem (c.val + 1),
+          (⟨Function.update s.mem 0 (s.mem (c.val + 1)), s.frontier⟩ : Memory.State)) := by
+  rw [storeSample, RandomizedSpec.run_bind, run_sample, PMF.bind_map, ← PMF.bind_pure_comp]
+  congr 1
+  funext c
+  simp only [Function.comp_apply]
+  rw [RandomizedSpec.withCoins_run_liftRight, StateTransitionSpec.run_toRandomized]
+  rfl
+
+/-- Every supported joint outcome records the returned value in cell zero. -/
+theorem storeSample_result_eq_cell {w : ℕ} {s s' : Memory.State} {v : ℕ}
+    (h : (v, s') ∈ ((Memory.spec w).toRandomized.withCoins.run storeSample s).support) :
+    s'.mem 0 = v := by
+  rw [run_storeSample, PMF.mem_support_map_iff] at h
+  obtain ⟨c, -, hc⟩ := h
+  obtain ⟨rfl, rfl⟩ := Prod.mk.inj hc
+  simp only [Function.update_self]
+
+/-- The adaptive write is admissible on the same nonempty allocated input as `sample`, when
+the memory words fit. The stored value is a word read from that memory. -/
+theorem demonicValid_storeSample {w : ℕ} {s : Memory.State} (hs : Memory.WellFormed w s)
+    (h0 : 1 ≤ s.mem 0) (hf : s.mem 0 < s.frontier) :
+    (Memory.spec w).toRandomized.withCoins.toSpec.DemonicValid s storeSample := by
+  refine StateTransitionSpec.DemonicValid.bind (demonicValid_sample h0 hf) fun v s' tr hrun => ?_
+  have hmem := RandomizedSpec.mem_support_run_of_clientRun _ hrun
+  rw [run_sample, PMF.mem_support_map_iff] at hmem
+  obtain ⟨c, -, hc⟩ := hmem
+  obtain ⟨rfl, rfl⟩ := Prod.mk.inj hc
+  apply RandomizedSpec.demonicValid_liftRight
+  apply StateTransitionSpec.toRandomized_demonicValid_of_validHistory
+  exact ⟨⟨by omega, hs.mem_fits _⟩, trivial⟩
+
+/-- The adaptive store uses the same deterministic entry point and preserves a pathwise
+single-call budget; its concrete memory write is included in the instruction currency. -/
+theorem realizesRand_storeSample :
+    RealizesRand .exact (fun _ : Unit => storeSample) unitWords word
+      (fun _ _ s => 1 ≤ s.mem 0) (fun _ _ => 7) (fun _ _ => 1) := by
+  have hwrite : Realizes .exact (fun e : Unit × ℕ => do
+      Memory.write 0 e.2
+      pure e.2) (appendWords unitWords word) word (fun _ _ _ => True) (fun _ _ => 0) := by
+    realize
+  refine ((realizesRand_sample_unit.bind hwrite.toRand (fun _ _ => 1) (fun _ _ => 0)).congr
+    fun _ => rfl).consequence ?_
+  intro w d s _ _ h
+  exact ⟨⟨h, fun _ _ _ => ⟨trivial, le_rfl, le_rfl⟩⟩, le_rfl, le_rfl⟩
+
+end ComplexityTests.WordRAMRealizationRandom
diff --git a/manual/algorithms-and-memory/wordram-and-bridges.md b/manual/algorithms-and-memory/wordram-and-bridges.md
index eabcb5a73a..082653f7d9 100644
--- a/manual/algorithms-and-memory/wordram-and-bridges.md
+++ b/manual/algorithms-and-memory/wordram-and-bridges.md
@@ -62,6 +62,51 @@ The extension records worst-case successful halting, fault-freedom, random-call
 
 [Complexity/Computability/WordRAM/Randomized/Structured.lean](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Randomized/Structured.lean) uses `ExecRand` to certify a finite fault-free structured execution tree with the distribution of final data and exact instruction count. Compilation and random/cost bounds preserve its law.
 
+### Realize memory clients with private coins
+
+Import `Complexity.Computability.WordRAM.Realization.Random` for
+[`RealizesRand`](../../Complexity/Computability/WordRAM/Realization/Random.lean), and
+`Complexity.Computability.WordRAM.Realization.RandomLoop` for runtime-bounded iteration.
+Start with a memory client with private coins, faithful input/output word encodings, a safe
+entry domain, and separate time and random-call budgets. The realization chooses its emitter,
+scratch size and exchange constant before runtime arguments, word widths and initial memories.
+It requires bounded initial data, the encoded argument in its source registers, disjoint
+scratch/frontier placement, the safe-domain premise and demonic admissibility of the client.
+
+[`ExecRandLaw`](../../Complexity/Computability/WordRAM/Randomized/Law.lean) relates the emitted
+code to the **joint** law of encoded result words and the entire memory function and frontier.
+A result-only marginal cannot preserve a later memory-dependent call. The code keeps registers
+outside its scratch bank and frontier, and every path terminates within `C*(time+1)` native
+instructions and the separate random-call budget. Deterministic components enter through an
+existing `Realizes` certificate and `Realizes.toRand`; their time is memory charge plus local
+work and their random-call budget is zero.
+
+`RealizesRand.bind` requires the continuation's domain and uniform time/call bounds for every
+supported intermediate answer and memory. `RealizesRand.iterate` requires the corresponding
+bounds at every supported loop prefix, using one body emitter. Supply those obligations at
+reached memories; a bound only at the initial state, or only in expectation, is insufficient.
+The native rules account for register copies, loop counters, headers and exits.
+
+`RealizesRand.exists_init_program` compiles a selected result coordinate to the existing flat
+program semantics, retaining its joint law with full memory/frontier and exporting both
+`RandHaltsWithin` and `RandCallsBounded`. Keep the raw-input prefix equality, length/fit,
+safe-domain and demonic-admissibility premises. `Data.init` raw-memory placement is an
+**uncharged calling convention**; the charged `2*k+5` native prefix installs the frontier and
+first `k` argument registers, not the whole graph. Its allowance `C*(time+1)+1` includes that
+prefix, the body and trailing halt. The random budget counts primitive inclusive-range calls,
+even `rand(0)`; it does not prove a bounded-cost exact fair-bit sampler.
+
+Open the complete checked
+[WordRAMRealizationRandom clients](../../ComplexityTests/WordRAMRealizationRandom.lean),
+including their imports and encodings. `sample_program` samples an input position, retaining
+repeated values' multiplicity; its input is nonempty and must fit. The runtime-repeat client
+bounds every iteration. `storeSample_result_eq_cell` and `realizesRand_storeSample` retain the
+correlation between the returned sample and the written cell, while preserving other memory
+and the frontier. These are realization clients, not a completed native Karger implementation:
+K2 still needs its method/setup and exact-resource deletion train, and K3 needs recursive
+frame-stack realization. No expected-cost or uniform-word claim becomes a strict fair-coin
+runtime claim through this interface.
+
 ## Expected time and unbounded termination
 
 [expectedTime](https://github.com/cslib-community/complexitylib/blob/13e6a31951bf1c89a1a6258c44f9444aecbbefd8/Complexity/Computability/WordRAM/Randomized/Expected.lean#L165) sums, over horizons `t`, the probability that execution is still running. It is valued in extended nonnegative reals. Since both halt and fault are absorbing, this is time until either; concluding almost-sure **successful** halting also requires fault-freedom. `Executes.expectedTime_eq` recovers deterministic instruction counts, and worst-case halting reduces the sum to a finite horizon.