diff --git a/Complexity.lean b/Complexity.lean
index b988a1c9a7..d9bc3c49b7 100644
--- a/Complexity.lean
+++ b/Complexity.lean
@@ -2640,6 +2640,7 @@ public import Complexity.Computability.WordRAM.Realization.Primitive
 public import Complexity.Computability.WordRAM.Realization.Program
 public import Complexity.Computability.WordRAM.Realization.Result
 public import Complexity.Computability.WordRAM.Realization.While
+public import Complexity.Computability.WordRAM.Realization.WhileAbsorb
 public import Complexity.Computability.WordRAM.Realization.Witness
 public import Complexity.Computability.WordRAM.RegisterFrame
 public import Complexity.Computability.WordRAM.Sequence
diff --git a/Complexity/Computability/WordRAM/Realization/Absorb.lean b/Complexity/Computability/WordRAM/Realization/Absorb.lean
index 32a30eaf6c..000f25274a 100644
--- a/Complexity/Computability/WordRAM/Realization/Absorb.lean
+++ b/Complexity/Computability/WordRAM/Realization/Absorb.lean
@@ -38,6 +38,7 @@ absorption applied. They are the target shapes of the `realize` tactic. Glue tak
 * `Realizes.mono_mul`: absorb local work dominated by a constant multiple of the memory charge
   plus another grading.
 * `Realizes.congr`: transport a certificate along pointwise equal programs.
+* `Realizes.consequence_valid`: strengthen the domain under the client's valid history.
 * `Realizes.bind₀`, `Realizes.branch₀`: sequencing and branching with absorbed control work.
   `Realizes.bind₀_of_run` states the continuation's domain at a closed form of the first
   client's reply and next memory.
@@ -121,6 +122,19 @@ theorem congr {p' : δ → Memory.Prog α} (h : Realizes B p input output safe w
     (hp : ∀ d, p d = p' d) : Realizes B p' input output safe work :=
   funext hp ▸ h
 
+/-- Strengthen the visible domain using, besides the input fits and memory well-formedness, the
+validity of the client's own history from the entry memory, which every execution supplies. -/
+theorem consequence_valid {safe' : ℕ → δ → Memory.State → Prop}
+    (h : Realizes B p input output safe work)
+    (hsafe : ∀ w d s, (∀ i, Fits w (input d i)) → Memory.WellFormed w s →
+      (Memory.spec w).ValidHistory s ((Memory.spec w).clientHistory s (p d)) →
+      safe' w d s → safe w d s) : Realizes B p input output safe' work := 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 => hrun w d x hx hin ?_ hv⟩
+  exact hsafe w d _ (fun i => congrFun hin i ▸ hx.1 (src i)) (wellFormed_memoryState hx) hv hsafe'
+
 variable {q : δ × α → Memory.Prog β} {answer : α ↪ (Fin l → ℕ)} {output' : β ↪ (Fin m → ℕ)}
   {safeP : ℕ → δ → Memory.State → Prop} {safeQ : ℕ → δ × α → Memory.State → Prop}
 
diff --git a/Complexity/Computability/WordRAM/Realization/WhileAbsorb.lean b/Complexity/Computability/WordRAM/Realization/WhileAbsorb.lean
new file mode 100644
index 0000000000..a71ec2b3c1
--- /dev/null
+++ b/Complexity/Computability/WordRAM/Realization/WhileAbsorb.lean
@@ -0,0 +1,181 @@
+/-
+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.Absorb
+public import Complexity.Computability.WordRAM.Realization.While
+
+/-!
+# While loops with semantic guards and absorbed work
+
+`boundedWhile` accepts any decidable guard, so a source states its guard in its own terms:
+`0 < r`, `a ≠ 0`, `i < n`. `Realizes.whileBounded` certifies the loop whose guard is a native
+comparison of the encoded words. The congruence lemmas below move a loop, its domain and its
+charge between pointwise equivalent guards and between environments at which the loop's
+guard and body agree, so a certificate for the native guard transfers to the source's guard.
+The `realize` tactic does this transfer itself.
+
+`whileWork_le` bounds the local work of a loop whose body costs at most `K` by
+`cutoff * (K + 1)`; with a logarithmic cutoff this gives a sift its logarithmic local work through
+`Realizes.consequence`. When every body begins with a memory query, that query pays the
+iteration's control unit (`whileWork_zero_le`), and `Realizes.while₀` is the while rule with local
+work `0`, the shape `realize` composes.
+
+## Main results
+
+* `boundedWhile_congr`, `whileSafe_imp`, `whileSafe_congr`, `whileWork_congr`: congruence in
+  the guard, the body and the environment.
+* `whileWork_le`: the local work is at most `cutoff * (K + 1)`.
+* `whileWork_zero_le`: a loop whose body begins with a query pays its control from memory.
+* `Realizes.while₀`: the native while rule with absorbed local work.
+-/
+
+public section
+
+namespace Cslib.WordRAM.Realization
+
+open Cslib.DataStructure
+
+variable {δ δ' σ : Type}
+
+/-! ### Congruence -/
+
+section Congr
+
+variable (guard : δ → σ → Prop) [∀ d a, Decidable (guard d a)]
+  (guard' : δ' → σ → Prop) [∀ d a, Decidable (guard' d a)]
+  {body : δ × σ → Memory.Prog σ} {body' : δ' × σ → Memory.Prog σ} {d : δ} {d' : δ'}
+
+/-- Loops whose guards and bodies agree at their environments are equal, whatever the guards'
+decidability instances. -/
+theorem boundedWhile_congr (hguard : ∀ a, guard d a ↔ guard' d' a)
+    (hbody : ∀ a, body (d, a) = body' (d', a)) (n : ℕ) (a : σ) :
+    boundedWhile guard body d n a = boundedWhile guard' body' d' n a := by
+  induction n generalizing a with
+  | zero => rfl
+  | succ n ih =>
+    by_cases hg : guard d a
+    · simp only [boundedWhile, hg, (hguard a).mp hg, ↓reduceIte, hbody, ih]
+    · simp only [boundedWhile, hg, mt (hguard a).mpr hg, ↓reduceIte]
+
+/-- The reached-state domain transfers along agreeing guards and bodies and a weaker body
+domain. The body domains are compared only where the guard holds, as only there is a body run. -/
+theorem whileSafe_imp {safe : ℕ → δ × σ → Memory.State → Prop}
+    {safe' : ℕ → δ' × σ → Memory.State → Prop} {w : ℕ}
+    (hguard : ∀ a, guard d a ↔ guard' d' a) (hbody : ∀ a, body (d, a) = body' (d', a))
+    (hsafe : ∀ a s, guard d a → safe w (d, a) s → safe' w (d', a) s) {n : ℕ} {a : σ}
+    {s : Memory.State} (h : whileSafe guard body safe w d n a s) :
+    whileSafe guard' body' safe' w d' n a s := by
+  induction n generalizing a s with
+  | zero => exact fun hg => h ((hguard a).mpr hg)
+  | succ n ih =>
+    by_cases hg : guard d a
+    · simp only [whileSafe, hg, ↓reduceIte] at h
+      simp only [whileSafe, (hguard a).mp hg, ↓reduceIte, ← hbody]
+      exact ⟨hsafe a s hg h.1, ih h.2⟩
+    · simp only [whileSafe, mt (hguard a).mpr hg, ↓reduceIte]
+
+/-- The reached-state domain is invariant under agreeing guards, bodies and body domains. -/
+theorem whileSafe_congr {safe : ℕ → δ × σ → Memory.State → Prop}
+    {safe' : ℕ → δ' × σ → Memory.State → Prop} {w : ℕ}
+    (hguard : ∀ a, guard d a ↔ guard' d' a) (hbody : ∀ a, body (d, a) = body' (d', a))
+    (hsafe : ∀ a s, guard d a → (safe w (d, a) s ↔ safe' w (d', a) s)) (n : ℕ) (a : σ)
+    (s : Memory.State) :
+    whileSafe guard body safe w d n a s ↔ whileSafe guard' body' safe' w d' n a s :=
+  ⟨whileSafe_imp guard guard' hguard hbody fun a s hg => (hsafe a s hg).mp,
+    whileSafe_imp guard' guard (fun a => (hguard a).symm) (fun a => (hbody a).symm)
+      fun a s hg => (hsafe a s ((hguard a).mpr hg)).mpr⟩
+
+/-- The local work is invariant under agreeing guards, bodies and body charges. -/
+theorem whileWork_congr {work : δ × σ → Memory.State → ℕ} {work' : δ' × σ → Memory.State → ℕ}
+    (hguard : ∀ a, guard d a ↔ guard' d' a) (hbody : ∀ a, body (d, a) = body' (d', a))
+    (hwork : ∀ a s, work (d, a) s = work' (d', a) s) (n : ℕ) (a : σ) (s : Memory.State) :
+    whileWork guard body work d n a s = whileWork guard' body' work' d' n a s := by
+  induction n generalizing a s with
+  | zero => rfl
+  | succ n ih =>
+    by_cases hg : guard d a
+    · simp only [whileWork, hg, (hguard a).mp hg, ↓reduceIte, hwork, ← hbody, ih]
+    · simp only [whileWork, hg, mt (hguard a).mpr hg, ↓reduceIte]
+
+end Congr
+
+/-! ### Work envelopes -/
+
+section Work
+
+variable (guard : δ → σ → Prop) [∀ d a, Decidable (guard d a)] (body : δ × σ → Memory.Prog σ)
+
+/-- With body work at most `K`, a loop with cutoff `n` has local work at most `n * (K + 1)`. -/
+theorem whileWork_le {work : δ × σ → Memory.State → ℕ} {K : ℕ} (hK : ∀ x s, work x s ≤ K)
+    (d : δ) (n : ℕ) (a : σ) (s : Memory.State) :
+    whileWork guard body work d n a s ≤ n * (K + 1) := by
+  induction n generalizing a s with
+  | zero => exact Nat.zero_le _
+  | succ n ih =>
+    by_cases hg : guard d a
+    · have h₁ := hK (d, a) s
+      have h₂ := ih ((Memory.spec 0).clientResult s (body (d, a)))
+        ((Memory.spec 0).clientState s (body (d, a)))
+      simp only [whileWork, hg, ↓reduceIte, Nat.succ_mul]
+      omega
+    · simp only [whileWork, hg, ↓reduceIte]
+      exact Nat.zero_le _
+
+/-- When every body issues a query, the loop's control work is at most its memory charge. -/
+theorem whileWork_zero_le (hquery : ∀ x s, 1 ≤ memoryCost (body x) s) (d : δ) (n : ℕ) (a : σ)
+    (s : Memory.State) :
+    whileWork guard body (fun _ _ => 0) d n a s ≤ memoryCost (boundedWhile guard body d n a) s := by
+  induction n generalizing a s with
+  | zero => exact Nat.zero_le _
+  | succ n ih =>
+    by_cases hg : guard d a
+    · have h := while_charge_succ guard body (fun _ _ => 0) d n a s hg
+      have h₁ := hquery (d, a) s
+      have h₂ := ih ((Memory.spec 0).clientResult s (body (d, a)))
+        ((Memory.spec 0).clientState s (body (d, a)))
+      have h₃ : whileWork guard body (fun _ _ => 0) d (n + 1) a s =
+          whileWork guard body (fun _ _ => 0) d n ((Memory.spec 0).clientResult s (body (d, a)))
+            ((Memory.spec 0).clientState s (body (d, a))) + 1 := by
+        simp only [whileWork, hg, ↓reduceIte, Nat.zero_add]
+      omega
+    · simp only [whileWork, hg, ↓reduceIte]
+      exact Nat.zero_le _
+
+end Work
+
+/-! ### The absorbed rule -/
+
+namespace Realizes
+
+variable {B : Basis} {k l : ℕ}
+
+/-- A while loop whose body begins with a query has local work `0`: each executed iteration's
+control unit is paid by that query's memory charge. The guard is the native comparison `cond`
+of the encoded environment and state; the cutoff is a ghost bound, never computed. -/
+theorem while₀ (input : δ ↪ (Fin k → ℕ)) (output : σ ↪ (Fin l → ℕ)) (cond : Cond (k + l))
+    (cutoff : δ × σ → ℕ) {body : δ × σ → Memory.Prog σ}
+    {safe : ℕ → (δ × σ) → Memory.State → Prop}
+    (h : Realizes B body (appendWords input output) output safe (fun _ _ => 0))
+    (hquery : ∀ x s, 1 ≤ memoryCost (body x) s) :
+    Realizes B (fun (d, a) => boundedWhile
+      (fun d a => test cond ((appendWords input output) (d, a))) body d (cutoff (d, a)) a)
+      (appendWords input output) output
+      (fun w (d, a) s => whileSafe
+        (fun d a => test cond ((appendWords input output) (d, a))) body safe w d
+        (cutoff (d, a)) a s)
+      (fun _ _ => 0) :=
+  (whileBounded input output cond cutoff h).mono_mul 1 fun (d, a) s => by
+    have := whileWork_zero_le (fun d a => test cond ((appendWords input output) (d, a))) body
+      hquery d (cutoff (d, a)) a s
+    dsimp only
+    omega
+
+end Realizes
+
+end Cslib.WordRAM.Realization
diff --git a/Complexity/Tactic/Realize.lean b/Complexity/Tactic/Realize.lean
index 0ec652571c..11f41a3bbf 100644
--- a/Complexity/Tactic/Realize.lean
+++ b/Complexity/Tactic/Realize.lean
@@ -7,7 +7,7 @@ Authors: Samuel Schlesinger
 module
 -- upstream: candidate
 
-public import Complexity.Computability.WordRAM.Realization.Absorb
+public import Complexity.Computability.WordRAM.Realization.WhileAbsorb
 
 /-!
 # The `realize` tactic
@@ -26,6 +26,13 @@ the client syntax, unfolding definitions, with one rule per form:
   (`Realizes.congr`, proved by cases).
 * `iterate step D n a` whose step begins with a query: `Realizes.iterate₀`, after
   `iterate_comap` moves `D` into the step.
+* `boundedWhile G step D n a` whose step begins with a query: `Realizes.while₀`. The guard
+  `G D r` may be `a = b`, `a < b`, `a > b` or `a ≠ 0` (tested as `0 < a`), with any decidability
+  instance, over the live words and the state's words; an operand independent of the state, such
+  as a constant, is computed before the loop. The cutoff `n` is a ghost bound and is not computed.
+  The certificate is transported to the client's guard, step and `D` (`boundedWhile_congr`,
+  `whileSafe_imp`), so the loop's domain is `whileSafe G step …` in the client's terms, under
+  the loop's valid history (`Realizes.consequence_valid`), ready for `whileSafe_of_measure`.
 
 Operands are located among the live words by definitional equality. An operand that is not a
 live word is first computed by an inserted `pure`, which leaves the program unchanged up to
@@ -41,7 +48,7 @@ Local work is absorbed (`Realizes.mono_mul`): every certificate built by `realiz
 `0`, so any local-work grading in the goal is accepted. Intermediate domains are stated in the
 client's own terms, with the replies of earlier queries written as `s.mem a`, `s.frontier`,
 updated memories, or the interpreter's result of a called method; a loop contributes its
-`iterationSafe` domain.
+`iterationSafe` or `whileSafe` domain.
 
 After the composition, `realize` introduces `w d s hwords hmem h`: the word width, the
 environment, the memory, the fit of the input words, memory well-formedness, and the goal's
@@ -605,17 +612,38 @@ private def checkOutput (proof : Expr) (output? : Option Expr) : MetaM Expr := d
         but the goal requires{indentExpr o}"
   return out
 
-/-- The comparison of a branch condition: equality or `<`, with its operands. -/
-private def parseCond (c : Expr) : MetaM (Name × Expr × Expr) := do
+/-- The native comparison of a word condition, equality or `<`, with its operands. -/
+private def cond? (c : Expr) : MetaM (Option (Name × Expr × Expr)) := do
   if let some (ty, a, b) := c.eq? then
-    if (← whnfR ty).isConstOf ``Nat then return (``Cond.eq, a, b)
+    if (← whnfR ty).isConstOf ``Nat then return some (``Cond.eq, a, b)
   if c.isAppOfArity ``LT.lt 4 && (c.getArg! 0).isConstOf ``Nat then
-    return (``Cond.lt, c.getArg! 2, c.getArg! 3)
+    return some (``Cond.lt, c.getArg! 2, c.getArg! 3)
   if c.isAppOfArity ``GT.gt 4 && (c.getArg! 0).isConstOf ``Nat then
-    return (``Cond.lt, c.getArg! 3, c.getArg! 2)
+    return some (``Cond.lt, c.getArg! 3, c.getArg! 2)
+  return none
+
+/-- The comparison of a branch condition: equality or `<`, with its operands. -/
+private def parseCond (c : Expr) : MetaM (Name × Expr × Expr) := do
+  if let some r ← cond? c then return r
   throwError "realize: a branch condition must be `a = b`, `a < b` or `a > b` on words, \
     got{indentExpr c}"
 
+/-- The comparison of a loop guard, after unfolding definitions. `a = b`, `a < b` and `a > b`
+are tested as written. `a ≠ 0` is tested as `0 < a`; the flag records this rewriting. -/
+private partial def parseGuard (g : Expr) (orig : Expr := g.headBeta) (fuel : Nat := 64) :
+    MetaM (Name × Expr × Expr × Bool) := do
+  let g := g.headBeta
+  if let some (kind, a, b) ← cond? g then return (kind, a, b, false)
+  if let some (ty, a, z) := g.ne?.orElse fun _ => g.not?.bind Expr.eq? then
+    if (← whnfR ty).isConstOf ``Nat && (← withNewMCtxDepth (isDefEq z (mkNatLit 0))) then
+      return (``Cond.lt, z, a, true)
+  if fuel != 0 then
+    let g' ← whnfR g
+    if g' != g then return ← parseGuard g' orig (fuel - 1)
+    if let some g' ← unfoldDefinition? g then return ← parseGuard g' orig (fuel - 1)
+  throwError "realize: a loop guard must be `a = b`, `a < b`, `a > b` or `a ≠ 0` on words, \
+    got{indentExpr orig}"
+
 /-- Rebuild a branch condition with new operands. -/
 private def rebuildCond (c a b : Expr) : MetaM Expr := do
   if c.isEq then mkEq a b
@@ -627,7 +655,7 @@ private def isClientForm (e : Expr) : Bool :=
   e.isAppOfArity ``Bind.bind 6 || e.isAppOfArity ``PFunctor.FreeM.bind 5 ||
   e.isAppOfArity ``Pure.pure 4 || e.isAppOfArity ``PFunctor.FreeM.pure 3 ||
   e.isAppOfArity ``PFunctor.FreeM.lift 2 || e.isAppOfArity ``PFunctor.FreeM.liftBind 4 ||
-  e.isAppOfArity ``ite 5
+  e.isAppOfArity ``ite 5 || e.isAppOfArity ``boundedWhile 8
 
 /-- Unfold definitions until a client form appears. -/
 private partial def normBody (e : Expr) (fuel : Nat := 64) : MetaM Expr := do
@@ -785,6 +813,9 @@ private partial def realizeBody (ctx : Ctx) (env : Env) (d : Expr) (atoms : Arra
         mkLambdaFVars #[w, d, s] (mkApp5 (mkConst ``ite [Level.one]) (mkSort Level.zero) c inst
           (hp.safe.beta #[w, d, s]) (hn.safe.beta #[w, d, s]))
     return { proof, output := out, safe }
+  -- a guarded loop
+  if body.isAppOfArity ``boundedWhile 8 then
+    return ← realizeWhile ctx env d atoms body output?
   -- a runtime-bounded loop
   if body.isAppOfArity ``iterate 6 then
     return ← realizeIterate ctx env d atoms (body.getArg! 1) (body.getArg! 2) (body.getArg! 3)
@@ -795,8 +826,8 @@ private partial def realizeBody (ctx : Ctx) (env : Env) (d : Expr) (atoms : Arra
     return ← realizeOptionSplit ctx env d atoms body r output?
   throwError "realize: unsupported client form{indentExpr body}\n\
     Expected `bind`, `pure`, a memory query, `if` on a word comparison,\n\
-    or a `match` on an optional answer. Recursion on a runtime value is a loop\n\
-    and needs a loop rule."
+    a `match` on an optional answer, `iterate` or `boundedWhile`.\n\
+    Write recursion on a runtime value as one of these loops."
 
 /-- Certify a client that matches on the optional answer `r`: it equals the branch on `r`'s
 presence tag, with `r` replaced by `none` and by `some` of its payload. -/
@@ -872,6 +903,151 @@ private partial def realizeIterate (ctx : Ctx) (env : Env) (d : Expr) (atoms : A
   let eq ← mkLambdaFVars #[d] (← mkEqSymm (← mkAppM ``iterate_comap #[g, step, d, n, a]))
   return { proof := ← mkAppM ``Realizes.congr #[proof, eq], output := out, safe }
 
+/-- Certify `boundedWhile G step D n a` for the environment variable `d`.
+
+The guard becomes a native comparison of the live words and the state's words. An operand that
+does not depend on the state, such as the `0` of `0 < r`, is computed first into one more live
+word. The body runs over the environment and the state, and must begin with a query
+(`Realizes.while₀`). The cutoff `n` is a ghost bound: it is never computed. The certificate is
+transported to the client's own guard, step and loop environment `D` (`boundedWhile_congr`,
+`whileSafe_imp`), and the loop's domain may assume the loop's valid history
+(`Realizes.consequence_valid`), which `whileSafe_of_measure` uses. -/
+private partial def realizeWhile (ctx : Ctx) (env : Env) (d : Expr) (atoms : Array Expr)
+    (body : Expr) (output? : Option Expr) : TermElabM Out := do
+  let args := body.getAppArgs
+  let (Δ, σ, G, inst, step, D, n, a) :=
+    (args[0]!, args[1]!, args[2]!, args[3]!, args[4]!, args[5]!, args[6]!, args[7]!)
+  let out ← match output? with
+    | some o => pure o
+    | none => encodingOf σ
+  let l ← encodingWidth out
+  let k := env.k
+  let nat := mkConst ``Nat
+  let state := mkConst ``Memory.State
+  -- the comparison, its operands among the live words and the state's words (`none` for a
+  -- computed operand), the computed operand, and the operand of a guard `x ≠ 0`
+  let (kind, posA, posB, pre?, neFn?) ← withLocalDeclD `a σ fun x => do
+    let (kind, oa, ob, ne) ← parseGuard (mkApp2 G D x)
+    let words := atoms ++ (← encodingAtoms out x l)
+    let locate (o : Expr) : MetaM (Option Nat) := do
+      if let some i ← findAtom words o then return some i
+      if o.containsFVar x.fvarId! then
+        throwError "realize: a loop guard compares words; the operand{indentExpr o}\n\
+          depends on the loop state but is not one of its words"
+      return none
+    let (ia, ib) := (← locate oa, ← locate ob)
+    let pre? ← match ia, ib with
+      | none, none => throwError "realize: the loop guard{indentExpr (mkApp2 G D x)}\n\
+          does not depend on the loop state"
+      | none, _ => pure (some oa)
+      | _, none => pure (some ob)
+      | _, _ => pure none
+    let neFn? ← if ne then pure (some (← mkLambdaFVars #[x] ob)) else pure none
+    return (kind, ia, ib, pre?, neFn?)
+  let word ← encodingOf nat
+  let envP ← if pre?.isSome then extend env nat word 1 else pure env
+  let cmp := envP.k + l
+  let pos (i? : Option Nat) : MetaM Expr := finLit cmp <| match i? with
+    | none => k
+    | some i => if i < k || pre?.isNone then i else i + 1
+  let cond ← mkAppM kind #[← pos posA, ← pos posB]
+  -- `X` at the loop environment `e`, whose first component is `d` when an operand is computed
+  let atEnv (X e : Expr) : MetaM Expr := do
+    return X.replaceFVar d (← if pre?.isSome then mkAppM ``Prod.fst #[e] else pure e)
+  -- the body over the loop environment and the state, and the ghost cutoff
+  let envB ← extend envP σ out l
+  let (bodyN, cutoff) ← withLocalDeclD `y envB.ty fun y => do
+    let e ← mkAppM ``Prod.fst #[y]
+    let x ← mkAppM ``Prod.mk #[← atEnv D e, ← mkAppM ``Prod.snd #[y]]
+    return (← mkLambdaFVars #[y] (mkApp (← atEnv step e) x), ← mkLambdaFVars #[y] (← atEnv n e))
+  let hB ← realizeProg ctx envB bodyN (some out)
+  let hLoop ← mkAppM ``Realizes.while₀
+    #[envP.input, out, cond, cutoff, hB.proof, ← proveQuery bodyN envB.ty]
+  -- the initial state, then the loop
+  let (hA, h) ← withLocalDeclD `e envP.ty fun e => do
+    let ae ← atEnv a e
+    let hA ← realizePure ctx envP e (envP.atoms.map (·.beta #[e])) ae out
+    let (reply, next) ← withLocalDeclD `s state fun s => do
+      return (← mkLambdaFVars #[e, s] ae, ← mkLambdaFVars #[e, s] s)
+    return (hA, ← bindRun hA.proof hLoop reply next)
+  -- the computed operand, then the initial state and the loop
+  let (hC?, h, e₀) ← match pre? with
+    | none => pure (none, h, d)
+    | some c => do
+      let hC ← realizePure ctx env d atoms c word
+      let (reply, next) ← withLocalDeclD `s state fun s => do
+        return (← mkLambdaFVars #[d, s] c, ← mkLambdaFVars #[d, s] s)
+      pure (some hC, ← bindRun hC.proof h reply next, ← mkAppM ``Prod.mk #[d, c])
+  -- the native guard at the loop environment, and its agreement with the client's
+  let (gN, iN) ← withLocalDeclD `e envP.ty fun e => withLocalDeclD `a σ fun x => do
+    let words ← mkAppM ``DFunLike.coe
+      #[← mkAppM ``appendWords #[envP.input, out], ← mkAppM ``Prod.mk #[e, x]]
+    let t ← mkAppM ``test #[cond, words]
+    return (← mkLambdaFVars #[e, x] t,
+      ← mkLambdaFVars #[e, x] (← synthInstance (← mkAppM ``Decidable #[t])))
+  let (hgU, hgN, hbU, hbN) ← withLocalDeclD `a σ fun x => do
+    let gU := mkApp2 G D x
+    let gn := mkApp2 gN e₀ x
+    let iff ← match neFn? with
+      | some f => mkAppM ``Iff.symm #[← mkAppOptM ``Nat.pos_iff_ne_zero #[f.beta #[x]]]
+      | none => mkAppM ``Iff.refl #[gU]
+    let hgU ← mkExpectedTypeHint iff (mkApp2 (mkConst ``Iff) gU gn)
+    let bU := mkApp step (← mkAppM ``Prod.mk #[D, x])
+    let bN := mkApp bodyN (← mkAppM ``Prod.mk #[e₀, x])
+    let hbU ← mkExpectedTypeHint (← mkEqRefl bU) (← mkEq bU bN)
+    return (← mkLambdaFVars #[x] hgU, ← mkLambdaFVars #[x] (← mkAppM ``Iff.symm #[hgU]),
+      ← mkLambdaFVars #[x] hbU, ← mkLambdaFVars #[x] (← mkEqSymm hbU))
+  -- the client's loop
+  let prog := (← instantiateMVars (← inferType h)).getArg! 5
+  let eq ← mkLambdaFVars #[d] (← mkExpectedTypeHint
+    (← mkAppOptM ``boundedWhile_congr #[envP.ty, Δ, σ, gN, iN, G, inst, bodyN, step, e₀, D,
+      hgN, hbN, n, a])
+    (← mkEq (mkApp prog d) body))
+  let h ← mkAppM ``Realizes.congr #[h, eq]
+  -- the domain in the client's terms: the body's domain at the client's loop environment
+  let pairTy ← mkAppM ``Prod #[Δ, σ]
+  let safeB ← withLocalDeclD `w nat fun w => withLocalDeclD `x pairTy fun x =>
+    withLocalDeclD `s state fun s => do
+      let y ← mkAppM ``Prod.mk #[e₀, ← mkAppM ``Prod.snd #[x]]
+      mkLambdaFVars #[w, x, s] (← reducePairs (hB.safe.beta #[w, y, s]))
+  let safe ← withLocalDeclD `w nat fun w => withLocalDeclD `s state fun s => do
+    let spec ← mkAppM ``Memory.spec #[w]
+    let valid ← mkAppM ``StateTransitionSpec.ValidHistory
+      #[spec, s, ← mkAppM ``StateTransitionSpec.clientHistory #[spec, s, body]]
+    let loop ← mkArrow valid
+      (← mkAppOptM ``whileSafe #[Δ, σ, G, inst, step, safeB, w, D, n, a, s])
+    let dom := mkAnd (← reducePairs (hA.safe.beta #[w, e₀, s])) loop
+    mkLambdaFVars #[w, d, s] <| match hC? with
+      | some hC => mkAnd (hC.safe.beta #[w, d, s]) dom
+      | none => dom
+  -- the client's domain implies the native one under the loop's valid history
+  let cv ← mkAppOptM ``Realizes.consequence_valid
+    #[none, none, none, none, none, none, none, none, none, none, safe, h]
+  let hsafeTy := (← whnf (← inferType cv)).bindingDomain!
+  let hsafe ← withLocalDeclD `w nat fun w => withLocalDeclD `s state fun s => do
+    forallBoundedTelescope (← instantiateForall hsafeTy #[w, d, s]) (some 4) fun hs goal => do
+      let #[_, _, hv, hd] := hs | throwError "realize: internal error in the loop domain"
+      let part (h : Expr) : MetaM (Expr × Expr) := do
+        return (← mkAppM ``And.left #[h], ← mkAppM ``And.right #[h])
+      let (hcs, rest) ← match hC? with
+        | some _ => do let (p, q) ← part hd; pure (some p, q)
+        | none => pure (none, hd)
+      let (has, hloop) ← part rest
+      let hsU ← withLocalDeclD `a σ fun x => withLocalDeclD `s state fun s' =>
+        withLocalDeclD `hg (mkApp2 G D x) fun hg => do
+          let hs := mkApp3 safeB w (← mkAppM ``Prod.mk #[D, x]) s'
+          withLocalDeclD `h hs fun hh => do
+            let hN := mkApp3 hB.safe w (← mkAppM ``Prod.mk #[e₀, x]) s'
+            mkLambdaFVars #[x, s', hg, hh] (← mkExpectedTypeHint hh hN)
+      let ws ← mkAppOptM ``whileSafe_imp #[Δ, envP.ty, σ, G, inst, gN, iN, step, bodyN, D, e₀,
+        safeB, hB.safe, w, hgU, hbU, hsU, none, none, none, mkApp hloop hv]
+      let dom ← mkAppM ``And.intro #[has, ws]
+      let pf ← match hcs with
+        | some p => mkAppM ``And.intro #[p, dom]
+        | none => pure dom
+      mkLambdaFVars (#[w, d, s] ++ hs) (← mkExpectedTypeHint pf goal)
+  return { proof := mkApp cv hsafe, output := out, safe }
+
 /-- Certify `bind m f`: the first client, then the continuation over the extended environment. -/
 private partial def realizeBind (ctx : Ctx) (env : Env) (d m f : Expr) (output? : Option Expr) :
     TermElabM Out := do
diff --git a/ComplexityTests/WordRAMRealize.lean b/ComplexityTests/WordRAMRealize.lean
index 3c2259fc3b..23910a456d 100644
--- a/ComplexityTests/WordRAMRealize.lean
+++ b/ComplexityTests/WordRAMRealize.lean
@@ -321,8 +321,8 @@ def readMany : ℕ → Memory.Prog Unit
 error: realize: unsupported client form
   readMany d
 Expected `bind`, `pure`, a memory query, `if` on a word comparison,
-or a `match` on an optional answer. Recursion on a runtime value is a loop
-and needs a loop rule.
+a `match` on an optional answer, `iterate` or `boundedWhile`.
+Write recursion on a runtime value as one of these loops.
 -/
 #guard_msgs in
 example : Realizes .exact readMany (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
diff --git a/ComplexityTests/WordRAMRealizeWhile.lean b/ComplexityTests/WordRAMRealizeWhile.lean
new file mode 100644
index 0000000000..7c8e733814
--- /dev/null
+++ b/ComplexityTests/WordRAMRealizeWhile.lean
@@ -0,0 +1,220 @@
+/-
+Copyright (c) 2026 Samuel Schlesinger. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Samuel Schlesinger
+-/
+
+import Complexity.Computability.WordRAM.Realization.Client.MemoryStack
+import Complexity.Tactic.Realize
+
+/-! `realize` on guarded loops (`boundedWhile`).
+
+Three loop shapes the migrations need, each closed by `realize` and a short discharge of the loop
+domain it leaves: a countdown whose body reads memory, the queue's transfer between two array
+stacks counted down by the items left, and a sift-shaped descent `i ↦ 2i + 1` with logarithmic
+rank. Guards are written in the client's terms (`0 < r`, `r ≠ 0`, `i < n`), with any
+decidability instance; `realize` tests them natively and computes the `0` of `0 < r` before the
+loop. The cutoff is a ghost bound, never computed. The controls pin the unsupported forms and
+show that a truncating cutoff leaves an unsatisfiable domain. -/
+
+namespace ComplexityTests.WordRAMRealizeWhile
+
+open Cslib.DataStructure Cslib.WordRAM Cslib.WordRAM.Realization MemoryStack
+
+/-- One word. -/
+abbrev word : ℕ ↪ (Fin 1 → ℕ) := (Equiv.funUnique (Fin 1) ℕ).symm.toEmbedding
+
+/-- Two words. -/
+abbrev pairWords : ℕ × ℕ ↪ (Fin 2 → ℕ) :=
+  (word.prodMap word).trans (Fin.appendEquiv 1 1).toEmbedding
+
+/-! ## A countdown whose body reads memory -/
+
+/-- Load the count at `b`, then count it down, reading the cell after `b` on every step. -/
+def countdown (b : ℕ) : Memory.Prog ℕ := do
+  let n ← Memory.read b
+  boundedWhile (fun _ r => 0 < r) (fun (c, r) => do
+    let _ ← Memory.read c
+    pure (r - 1)) (b + 1) n n
+
+/-- The remaining count is the rank, and the loaded count the cutoff. -/
+example : Realizes .exact countdown word word (fun w b _ => Fits w (b + 1)) (fun _ _ => 0) := by
+  realize
+  intro hv
+  refine whileSafe_of_measure _ _ _ w _ (fun _ _ => True) (fun r _ => r)
+    (fun r _ _ hr hg => by omega) (fun r t _ hg _ => ⟨⟨h, hg⟩, trivial, ?_⟩) trivial le_rfl hv
+  change r - 1 < r
+  omega
+
+/-- The same countdown with the guard `r ≠ 0` under a classical decidability instance. -/
+noncomputable def countdownNe (b : ℕ) : Memory.Prog ℕ := do
+  let n ← Memory.read b
+  @boundedWhile _ _ (fun _ r => r ≠ 0) (fun _ _ => Classical.propDecidable _) (fun (c, r) => do
+    let _ ← Memory.read c
+    pure (r - 1)) (b + 1) n n
+
+/-- `r ≠ 0` is tested as `0 < r`, whatever its decidability instance. -/
+example : Realizes .exact countdownNe word word (fun w b _ => Fits w (b + 1)) (fun _ _ => 0) := by
+  realize
+  intro hv
+  refine @whileSafe_of_measure _ _ _ (fun _ _ => Classical.propDecidable _) _ _ w _
+    (fun _ _ => True) (fun r _ => r) (fun r _ _ hr hg => hg hr)
+    (fun r t _ hg _ => ⟨⟨h, by omega⟩, trivial, ?_⟩) _ _ _ trivial le_rfl hv
+  change r - 1 < r
+  omega
+
+/-- Count up to `b`, reading `b` on every step: the guard and the step capture the environment,
+and the loop's own environment is `()`. -/
+def countUp (b : ℕ) : Memory.Prog ℕ :=
+  boundedWhile (fun _ r => r < b) (fun ((_ : Unit), r) => do
+    let _ ← Memory.read b
+    pure (r + 1)) () b 0
+
+/-- The distance to `b` is the rank. -/
+example : Realizes .exact countUp word word (fun w b _ => Fits w (b + 1)) (fun _ _ => 0) := by
+  realize
+  intro hv
+  refine whileSafe_of_measure _ _ _ w _ (fun r _ => r ≤ d) (fun r _ => d - r)
+    (fun r _ _ hr hg => by omega) (fun r t hi hg _ => ⟨h.of_le (by omega), ?_, ?_⟩)
+    (Nat.zero_le _) (by omega) hv
+  · change r + 1 ≤ d
+    omega
+  · change d - (r + 1) < d - r
+    omega
+
+/-! ## The queue's transfer, counted down by the items left -/
+
+/-- Front and rear stack layouts. -/
+def queueWords : Stack.Memory.Layout × Stack.Memory.Layout ↪ (Fin 8 → ℕ) :=
+  (layoutWords.prodMap layoutWords).trans (Fin.appendEquiv 4 4).toEmbedding
+
+/-- One transfer step: pop the rear; push a popped item on the front and count down, and stop on
+an empty rear. -/
+def transferStep (F R : Stack.Memory.Layout) (r : ℕ) : Memory.Prog ℕ := do
+  match ← Stack.Memory.pop R with
+  | none => pure 0
+  | some v => do
+    Stack.Memory.push F v
+    pure (r - 1)
+
+/-- Read the rear's size, then move that many items while some remain. -/
+def transfer : Stack.Memory.Layout × Stack.Memory.Layout → Memory.Prog ℕ
+  | (F, R) => do
+    let n ← Stack.Memory.size R
+    boundedWhile (fun _ r => 0 < r) (fun ((F, R), r) => transferStep F R r) (F, R) n n
+
+/-- What one step needs at a reached memory: a nonempty rear's top item and the front's next
+slot are addressable, and the front's count can grow. -/
+def StepReady (w : ℕ) (F R : Stack.Memory.Layout) (s : Memory.State) : Prop :=
+  s.mem R.count.base ≠ 0 → Fits w (R.items.base + (s.mem R.count.base - 1)) ∧
+    Fits w (F.items.base + s.mem F.count.base) ∧ Fits w (s.mem F.count.base + 1)
+
+set_option maxHeartbeats 40000 in
+-- Performance guard: about 3k heartbeats are needed, side conditions included.
+/-- `realize` certifies the size query and the loop, with the pop's `match` and the push in the
+body. Each step's domain follows from `StepReady` at the reached memory. What remains,
+`whileSafe … StepReady …`, is what a queue migration discharges with its transfer invariant
+(`whileSafe_of_measure`, rank `r`). -/
+example : Realizes .exact transfer queueWords word
+    (fun w (F, R) s => F.count.base ≠ R.count.base ∧
+      whileSafe (fun _ r => 0 < r) (fun ((F, R), r) => transferStep F R r)
+        (fun w ((F, R), _) s => StepReady w F R s) w (F, R) (s.mem R.count.base)
+        (s.mem R.count.base) s)
+    (fun _ _ => 0) := by
+  realize
+  intro _
+  refine whileSafe_imp _ _ (fun _ => Iff.rfl) (fun _ => rfl) (fun r t hg hr => ?_) h.2
+  by_cases hc : t.mem d.2.count.base = 0
+  · simp [hc, Stack.Memory.runClient_pop_of_eq_zero _ t hc, StateTransitionSpec.clientResult]
+  · obtain ⟨h₁, h₂, h₃⟩ := hr hc
+    simp only [hc, ↓reduceIte, StateTransitionSpec.clientResult, StateTransitionSpec.clientState,
+      Stack.Memory.runClient_pop_of_pos _ t hc, optionWords_some, Matrix.cons_val_zero,
+      Nat.one_ne_zero, Function.update_of_ne h.1]
+    exact ⟨⟨⟨by omega, h₁⟩, by omega, h₃.of_le (by omega)⟩, ⟨h₂, h₃⟩, hg⟩
+
+/-! ## A sift-shaped descent with logarithmic rank -/
+
+/-- Descend from the root of a heap of size `n` at `b` through left children `i ↦ 2i + 1`,
+reading each visited item. -/
+def descend : ℕ × ℕ → Memory.Prog ℕ
+  | (b, n) => boundedWhile (fun (_, n) i => i < n)
+      (fun ((b, _), i) => do
+        let _ ← Memory.read (b + i)
+        pure (i + i + 1)) (b, n) (Nat.log 2 n + 1) 0
+
+/-- The levels left below index `i` in a heap of size `n`. -/
+def levels (n i : ℕ) : ℕ := Nat.log 2 n + 1 - Nat.log 2 (i + 1)
+
+/-- A left child within the heap has one level fewer left. -/
+theorem levels_child {n i : ℕ} (h : i < n) : levels n (i + i + 1) < levels n i := by
+  have hle : Nat.log 2 (i + 1) ≤ Nat.log 2 n := Nat.log_mono_right (by omega)
+  have hlog : Nat.log 2 (i + i + 1 + 1) = Nat.log 2 (i + 1) + 1 := by
+    rw [show i + i + 1 + 1 = (i + 1) * 2 by ring, Nat.log_mul_base (by norm_num) (by omega)]
+  unfold levels
+  omega
+
+/-- The rank is the levels left; the cutoff `log₂ n + 1` is a ghost bound. -/
+example : Realizes .exact descend pairWords word
+    (fun w (b, n) _ => Fits w (b + n) ∧ Fits w (n + n)) (fun _ _ => 0) := by
+  realize
+  intro hv
+  refine whileSafe_of_measure _ _ _ w _ (fun _ _ => True) (fun i _ => levels d.2 i)
+    (fun i _ _ hr hg => ?_) (fun i t _ hg _ => ⟨?_, trivial, ?_⟩) trivial (Nat.sub_le _ _) hv
+  · have := levels_child (n := d.2) hg
+    omega
+  · exact ⟨h.1.of_le (by dsimp only at hg ⊢; omega), h.2.of_le (by dsimp only at hg ⊢; omega)⟩
+  · exact levels_child hg
+
+/-! ## Controls -/
+
+/-- A truncating cutoff leaves an unsatisfiable domain: at cutoff `0` the guard must be false. -/
+example (w : ℕ) (s : Memory.State) :
+    ¬whileSafe (fun _ r => 0 < r) (fun ((_ : ℕ), r) => pure (r - 1)) (fun _ _ _ => True)
+      w 0 0 1 s :=
+  fun h => h Nat.one_pos
+
+/-- A query-free loop keeps a graded charge, which `whileWork_le` bounds by the cutoff. -/
+example (n i : ℕ) (s : Memory.State) :
+    whileWork (fun n i => i < n) (fun ((_ : ℕ), i) => pure (i + i + 1)) (fun _ _ => 5) n
+      (Nat.log 2 n + 1) i s ≤ (Nat.log 2 n + 1) * 6 :=
+  whileWork_le _ _ (fun _ _ => le_rfl) n _ i s
+
+/-- A query-free body has no memory charge to pay for its iterations. -/
+def halve (a : ℕ) : Memory.Prog ℕ :=
+  boundedWhile (fun _ a => 0 < a) (fun ((_ : ℕ), a) => pure (a >>> 1)) a (a + 1) a
+
+/--
+error: realize: a loop body must begin with a memory query, which pays for the iteration;
+the body begins with
+  PFunctor.FreeM.pure (x.2 >>> 1)
+-/
+#guard_msgs in
+example : Realizes .exact halve word word (fun _ _ _ => True) (fun _ _ => 0) := by
+  realize
+
+/-- A non-strict comparison is not a native test. -/
+def upTo (n : ℕ) : Memory.Prog ℕ :=
+  boundedWhile (fun n i => i ≤ n) (fun (_, i) => do let _ ← Memory.read i; pure (i + 1)) n (n + 1) 0
+
+/--
+error: realize: a loop guard must be `a = b`, `a < b`, `a > b` or `a ≠ 0` on words, got
+  a ≤ d
+-/
+#guard_msgs in
+example : Realizes .exact upTo word word (fun _ _ _ => True) (fun _ _ => 0) := by
+  realize
+
+/-- The guard compares live words; a computed function of the state is not one. -/
+def doubling (n : ℕ) : Memory.Prog ℕ :=
+  boundedWhile (fun n i => i + i < n) (fun (_, i) => do let _ ← Memory.read i; pure (i + 1)) n n 0
+
+/--
+error: realize: a loop guard compares words; the operand
+  a + a
+depends on the loop state but is not one of its words
+-/
+#guard_msgs in
+example : Realizes .exact doubling word word (fun _ _ _ => True) (fun _ _ => 0) := by
+  realize
+
+end ComplexityTests.WordRAMRealizeWhile