diff --git a/VCVio.lean b/VCVio.lean
index e6bf199fc..110db075c 100644
--- a/VCVio.lean
+++ b/VCVio.lean
@@ -99,6 +99,9 @@ import VCVio.Interaction.UC.StdDoBridge
 import VCVio.OracleComp.Coercions.Add
 import VCVio.OracleComp.Coercions.SubSpec
 import VCVio.OracleComp.Coinductive.Bridge
+import VCVio.OracleComp.Coinductive.Composition
+import VCVio.OracleComp.Coinductive.DynSystem
+import VCVio.OracleComp.Coinductive.Machine
 import VCVio.OracleComp.Constructions.BitVec
 import VCVio.OracleComp.Constructions.GenerateSeed
 import VCVio.OracleComp.Constructions.Replicate
diff --git a/VCVio/Interaction/UC/AsyncRuntime.lean b/VCVio/Interaction/UC/AsyncRuntime.lean
index 85a452983..0a24a56f0 100644
--- a/VCVio/Interaction/UC/AsyncRuntime.lean
+++ b/VCVio/Interaction/UC/AsyncRuntime.lean
@@ -209,8 +209,8 @@ process sampler type is unchanged from the synchronous runtime: the
 noncomputable def runStepsAsync
     {m : Type → Type} [Monad m]
     {Γ : Spec.Node.Context}
-    {State : Type} {Event : Type}
-    (process : ProcessOver Γ)
+    {State : Type} {Event : Type} {P : Type}
+    (process : ProcessOver P Γ)
     (envAction : Interaction.UC.EnvAction m Event State)
     (procScheduler :
       Interaction.UC.ProcessScheduler m process.Proc State
@@ -249,8 +249,8 @@ trace bookkeeping pass, and is reused by
 -/
 theorem runStepsAsync_empty_trivial_eq
     {m : Type → Type} [Monad m] [LawfulMonad m]
-    {Γ : Spec.Node.Context}
-    (process : ProcessOver Γ)
+    {Γ : Spec.Node.Context} {P : Type}
+    (process : ProcessOver P Γ)
     (sampler : (s : process.Proc) → Spec.Sampler m (process.step s).spec)
     (fuel : ℕ) (s : process.Proc) :
     runStepsAsync (m := m) process (Interaction.UC.EnvAction.empty Unit)
diff --git a/VCVio/Interaction/UC/AsyncSecurity.lean b/VCVio/Interaction/UC/AsyncSecurity.lean
index 969bda061..078492227 100644
--- a/VCVio/Interaction/UC/AsyncSecurity.lean
+++ b/VCVio/Interaction/UC/AsyncSecurity.lean
@@ -106,8 +106,8 @@ runtime distribution, exactly as
 `ProcessOver.Run`.
 -/
 structure AsyncRun
-    {Γ : Spec.Node.Context} {m : Type → Type} [Pure m] {State Event : Type}
-    (process : Concurrent.ProcessOver Γ)
+    {Γ : Spec.Node.Context} {m : Type → Type} [Pure m] {State Event P : Type}
+    (process : Concurrent.ProcessOver P Γ)
     (envAction : EnvAction m Event State) where
   /-- The joint runtime state at each step. -/
   state : ℕ → AsyncRuntimeState process.Proc State
@@ -134,8 +134,8 @@ namespace AsyncRun
 
 variable {Γ : Spec.Node.Context}
 variable {m : Type → Type} [Pure m]
-variable {State Event : Type}
-variable {process : Concurrent.ProcessOver Γ}
+variable {State Event P : Type}
+variable {process : Concurrent.ProcessOver P Γ}
 variable {envAction : EnvAction m Event State}
 
 /-- The initial joint runtime state of an async run. -/
diff --git a/VCVio/Interaction/UC/Runtime.lean b/VCVio/Interaction/UC/Runtime.lean
index d4a6c752e..d5d5d39b8 100644
--- a/VCVio/Interaction/UC/Runtime.lean
+++ b/VCVio/Interaction/UC/Runtime.lean
@@ -149,8 +149,8 @@ Run `fuel` steps of a process, starting from state `s`, using a
 state-dependent sampler at each step.
 -/
 noncomputable def ProcessOver.runSteps {m : Type → Type} [Monad m]
-    {Γ : Spec.Node.Context}
-    (process : ProcessOver Γ)
+    {Γ : Spec.Node.Context} {P : Type}
+    (process : ProcessOver P Γ)
     (sampler : (p : process.Proc) → Spec.Sampler m (process.step p).spec) :
     ℕ → process.Proc → m process.Proc
   | 0, s => pure s
@@ -188,7 +188,8 @@ noncomputable def processSemantics (Party : Type u) {m : Type → Type} [Monad m
   instMonad := inferInstance
   sem := sem
   run process :=
-    process.toProcess.runSteps process.stepSampler fuel (init process) >>= observe process
+    ProcessOver.runSteps process.toProcess process.stepSampler fuel (init process) >>=
+      observe process
 
 /--
 `processSemanticsProbComp` is the specialization of `processSemantics`
diff --git a/VCVio/Interaction/UC/StdDoBridge.lean b/VCVio/Interaction/UC/StdDoBridge.lean
index 38855983d..8812391a8 100644
--- a/VCVio/Interaction/UC/StdDoBridge.lean
+++ b/VCVio/Interaction/UC/StdDoBridge.lean
@@ -101,12 +101,12 @@ variable {m : Type → Type} [Monad m]
 variable {Γ : Interaction.Spec.Node.Context.{0, 0}}
 
 @[simp]
-theorem ProcessOver.runSteps_zero (process : ProcessOver Γ)
+theorem ProcessOver.runSteps_zero {P : Type} (process : ProcessOver P Γ)
     (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec) (s : process.Proc) :
     process.runSteps sampler 0 s = pure s := rfl
 
 @[simp]
-theorem ProcessOver.runSteps_succ (process : ProcessOver Γ)
+theorem ProcessOver.runSteps_succ {P : Type} (process : ProcessOver P Γ)
     (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec) (n : ℕ)
     (s : process.Proc) :
     process.runSteps sampler (n + 1) s =
@@ -133,7 +133,7 @@ This is the process-runtime analogue of
 `OracleComp.ProgramLogic.StdDo.simulateQ_triple_preserves_invariant`:
 a generic invariant lemma that factors out the fuel induction so
 downstream proofs stay inside the `Std.Do` world. -/
-theorem runSteps_triple_preserves_invariant (process : ProcessOver Γ)
+theorem runSteps_triple_preserves_invariant {P : Type} (process : ProcessOver P Γ)
     (sampler : ∀ p : process.Proc, Spec.Sampler m (process.step p).spec)
     (I : process.Proc → Prop) (hstep : ∀ p : process.Proc,
       Std.Do.Triple ((process.step p).sample (sampler p))
@@ -174,9 +174,8 @@ private abbrev trivCtx : Interaction.Spec.Node.Context.{0, 0} := fun _ => PUnit
 
 /-- Always-increment process: each step has no moves and bumps the
 counter by one. -/
-private def incrementProcess : ProcessOver trivCtx where
-  Proc := ℕ
-  step p :=
+private def incrementProcess : ProcessOver ℕ trivCtx :=
+  ProcessOver.ofStep ℕ fun p =>
     { spec := .done
       semantics := PUnit.unit
       next := fun _ => p + 1 }
diff --git a/VCVio/OracleComp/Coinductive/Composition.lean b/VCVio/OracleComp/Coinductive/Composition.lean
new file mode 100644
index 000000000..0851ffbbc
--- /dev/null
+++ b/VCVio/OracleComp/Coinductive/Composition.lean
@@ -0,0 +1,42 @@
+/-
+Copyright (c) 2026 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+import VCVio.OracleComp.Coinductive.Machine
+
+/-!
+# Composition of Implementing Oracle Machines
+
+This file specializes PolyFun's fuel-exact sequential composition of pointed machines to
+`OracleComp`. Machines implementing two program stages compose into a machine implementing their
+monadic bind, with the two query budgets added.
+-/
+
+universe u
+
+open OracleSpec PFunctor
+
+variable {ι : Type u} {spec : OracleSpec.{u, u} ι} {α mid β : Type u}
+
+namespace OracleMachine
+
+/-- Sequential composition of implementing machines implements the bind of their programs. -/
+theorem Implements.seqComp {M₁ : OracleMachine spec α mid} {M₂ : OracleMachine spec mid β}
+    {oa : α → OracleComp spec mid} {ob : mid → OracleComp spec β} {k₁ k₂ : ℕ}
+    (h₁ : M₁ ⊨[k₁] oa) (h₂ : M₂ ⊨[k₂] ob) :
+    M₁ ⨟ M₂ ⊨[k₁ + k₂] fun x => oa x >>= ob := by
+  apply Implements.of_runK_eq
+  intro m _ _ H x
+  rw [show OracleMachine.runK (M₁ ⨟ M₂) H (k₁ + k₂) ((M₁ ⨟ M₂).init x) =
+      (M₁ ⨟ M₂).runWith H (k₁ + k₂) ((M₁ ⨟ M₂).init x) from rfl,
+    PointedMachine.runWith_seqComp_init M₁ M₂ H k₂ x
+      (PFunctor.PointedMachine.Implements.resolvesIn h₁ x)
+      (fun y => PFunctor.PointedMachine.Implements.resolvesIn h₂ y),
+    show M₁.runWith H k₁ (M₁.init x) = M₁.runK H k₁ (M₁.init x) from rfl,
+    h₁.runK_eq H x, simulateQ_bind, map_eq_bind_pure_comp, bind_assoc, map_bind]
+  refine bind_congr fun a => ?_
+  rw [Function.comp_apply, pure_bind]
+  exact h₂.runK_eq H a
+
+end OracleMachine
diff --git a/VCVio/OracleComp/Coinductive/DynSystem.lean b/VCVio/OracleComp/Coinductive/DynSystem.lean
new file mode 100644
index 000000000..5529ebb81
--- /dev/null
+++ b/VCVio/OracleComp/Coinductive/DynSystem.lean
@@ -0,0 +1,668 @@
+/-
+Copyright (c) 2026 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+import VCVio.OracleComp.EvalDist
+import VCVio.OracleComp.SimSemantics.SimulateQ
+import VCVio.OracleComp.Coercions.SubSpec
+import VCVio.OracleComp.QueryTracking.LoggingOracle
+import PolyFun.PFunctor.Dynamical.Behavior
+import PolyFun.PFunctor.Dynamical.Run
+import PolyFun.PFunctor.Free.Path
+
+/-!
+# Oracle strategies: the coalgebra dual of `OracleComp`
+
+`OracleComp spec` is the *inductive* free monad on `spec.toPFunctor`: a program that **asks**
+queries and halts. This file develops the *coalgebraic* dual, following Niu–Spivak
+(*Polynomial Functors*, Ch. 4): a stateful, adaptive querier is a **`spec.toPFunctor`-dynamical
+system**, and a deterministic oracle is a **section** of the same polynomial functor.
+
+```
+OracleComp  (algebra / answer side, inductive)  ⟷  OracleStrategy  (coalgebra / ask side, stateful)
+                          glued by a handler  (=  Section spec.toPFunctor  =  QueryImpl spec Id)
+```
+
+* `OracleStrategy S spec := PFunctor.DynSystem S spec.toPFunctor` — states `S` with
+  `expose : S → ι` (the next query to ask) and `update : S → spec.Range _ → S`
+  (digest the answer, advance) — literally a lens `selfMonomial S ⟹ spec.toPFunctor`.
+  This is exactly an adaptive querying strategy / adversary.
+* `OracleHandler spec := PFunctor.Section spec.toPFunctor` — a deterministic oracle as a section
+  (a lens `spec.toPFunctor ⟹ X`); build with `ofFn`, apply via `DFunLike` (`h t`), and coerce to the
+  underlying `QueryImpl spec Id` with `toQueryImpl`.
+* `OracleStrategy.runAgainst h A : PFunctor.Closed S` — close the strategy off with a handler
+  (PolyFun's `close`); its `Closed.iterate` is the state trajectory and `transcript` the run log.
+* `OracleStrategy.reduce` / `pair` / `juxtapose` — install a strategy along a reduction
+  (`⊂ₒ` lens), against a product oracle (`*`), or in parallel (`⊗`).
+
+The probabilistic Kleisli lift, the headline `iterate = simulateQ` correspondence, and the bridge
+to `OracleComp.withQueryLog` live further down this file. The inductive-to-coinductive embedding
+`toITree` is in `VCVio.OracleComp.Coinductive.Bridge`.
+-/
+
+universe u v w
+
+open OracleSpec
+open scoped PFunctor
+
+variable {ι : Type u} {spec : OracleSpec.{u, v} ι}
+
+/-- A stateful, adaptive querier against `spec` with states `S` (an adversary / environment): a
+PolyFun dynamical system whose interface is the oracle's polynomial functor `spec.toPFunctor` —
+literally a lens `selfMonomial S ⟹ spec.toPFunctor`. Its `expose` chooses the next query from the
+current state; `update` digests an oracle answer into the next state. The whole
+`PFunctor.DynSystem` / `PFunctor.Lens` combinator library applies directly. -/
+abbrev OracleStrategy (S : Type w) (spec : OracleSpec ι) : Type _ :=
+  PFunctor.DynSystem S spec.toPFunctor
+
+/-- A deterministic, total oracle for `spec`, as a PolyFun **section** — a lens
+`spec.toPFunctor ⟹ X` choosing a direction (answer) at every position (query). Build one from an
+answer function with `OracleHandler.ofFn`, apply it as a function through the `DFunLike` coercion
+(`h t : spec.Range t`), and recover the underlying `QueryImpl spec Id` with
+`OracleHandler.toQueryImpl`. Being a lens, it is exactly what `PFunctor.DynSystem.wrap` closes a
+strategy with (`OracleStrategy.runAgainst`), and the whole `PFunctor.Lens` algebra applies. -/
+abbrev OracleHandler (spec : OracleSpec.{u, v} ι) : Type _ :=
+  PFunctor.Section spec.toPFunctor
+
+namespace OracleHandler
+
+/-- Build a handler from a dependent answer function `(t : spec.Domain) → spec.Range t`. -/
+def ofFn (f : (t : spec.Domain) → spec.Range t) : OracleHandler spec :=
+  PFunctor.sectionLens f
+
+/-- The answer function underlying a handler. -/
+def toFn (h : OracleHandler spec) (t : spec.Domain) : spec.Range t :=
+  h.toFunB t PUnit.unit
+
+instance instDFunLike : DFunLike (OracleHandler spec) spec.Domain (fun t => spec.Range t) where
+  coe := toFn
+  coe_injective _ _ heq := by
+    apply PFunctor.Lens.ext _ _ (fun a => Subsingleton.elim _ _)
+    intro a
+    refine funext fun u => ?_
+    rw [Subsingleton.elim u PUnit.unit]
+    exact congrFun heq a
+
+@[simp] theorem coe_ofFn (f : (t : spec.Domain) → spec.Range t) : ⇑(ofFn f) = f := rfl
+
+@[simp] theorem ofFn_apply (f : (t : spec.Domain) → spec.Range t) (t : spec.Domain) :
+    ofFn f t = f t := rfl
+
+/-- A handler is a deterministic `QueryImpl spec Id` — its answer function. -/
+def toQueryImpl (h : OracleHandler spec) : QueryImpl spec Id := ⇑h
+
+@[simp] theorem toQueryImpl_apply (h : OracleHandler spec) (t : spec.Domain) :
+    h.toQueryImpl t = h t := rfl
+
+instance : Coe (OracleHandler spec) (QueryImpl spec Id) := ⟨toQueryImpl⟩
+
+end OracleHandler
+
+/-- A **randomized** oracle for `spec`: a `QueryImpl` valued in `SPMF = OptionT PMF`, i.e. each
+query answered by a sub-probability distribution. This is the Kleisli-category section that closes
+a strategy into a Markov chain on its states (`OracleStrategy.kleisliStep`). Single-universe because
+`SPMF : Type u → Type u`. -/
+abbrev ProbHandler {ι : Type u} (spec : OracleSpec.{u, u} ι) : Type u := QueryImpl spec SPMF
+
+namespace OracleSpec
+
+/-- The canonical randomized oracle of a probability spec: answer each query by its
+`IsProbabilitySpec` distribution, lifted to `SPMF`. Specializes to a fair coin on
+`coinSpec` and to uniform selection on `unifSpec`. -/
+noncomputable def probHandler {ι : Type} (spec : OracleSpec.{0, 0} ι)
+    [IsProbabilitySpec spec] : ProbHandler spec :=
+  fun t => (IsProbabilitySpec.toPMF t : SPMF (spec.Range t))
+
+open OracleComp in
+/-- Running a program against the canonical probabilistic handler computes its
+distributional semantics: machine-level game values against `probHandler` are `Pr[…]`
+statements about the program. -/
+theorem simulateQ_probHandler {ι : Type} {spec : OracleSpec.{0, 0} ι}
+    [IsProbabilitySpec spec] {α : Type} (oa : OracleComp spec α) :
+    simulateQ spec.probHandler oa = 𝒟[oa] := by
+  induction oa using OracleComp.inductionOn with
+  | pure x => simp
+  | query_bind t k ih =>
+    rw [simulateQ_query_bind]
+    simp only [ih, evalDist_bind, evalDist_liftM_toPMF]
+    simp [OracleSpec.probHandler, ← PMF.monad_map_eq_map]
+
+end OracleSpec
+
+namespace OracleStrategy
+
+variable {S : Type w}
+
+/-! ## Deterministic run and transcript -/
+
+/-- Closing a strategy with a deterministic handler gives an autonomous (`Closed`) system whose
+pure state transition is "ask the exposed query, feed the handler's answer back". Since the handler
+*is* the section lens `spec.toPFunctor ⟹ X`, this is just `wrap` along it. -/
+def runAgainst (h : OracleHandler spec) (A : OracleStrategy S spec) : PFunctor.Closed S :=
+  PFunctor.DynSystem.wrap h A
+
+/-- One step of the closed-loop run: ask `A.expose s`, answer with `h`, advance. Definitionally
+equal to `(runAgainst h A).step s`. -/
+def advanceOnce (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) : S :=
+  A.update s (h (A.expose s))
+
+@[simp] theorem runAgainst_step (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
+    (runAgainst h A).step s = advanceOnce h A s := rfl
+
+/-- The strategy's state after `n` handler-answered steps from `s`. Definitionally the closed
+system's `Closed.iterate`. -/
+def stateAfter (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) : S :=
+  (advanceOnce h A)^[n] s
+
+theorem stateAfter_eq_iterate (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S)
+    (n : ℕ) : stateAfter h A s n = (runAgainst h A).iterate s n := rfl
+
+@[simp] theorem stateAfter_zero (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
+    stateAfter h A s 0 = s := rfl
+
+theorem stateAfter_succ (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
+    stateAfter h A s (n + 1) = stateAfter h A (advanceOnce h A s) n :=
+  Function.iterate_succ_apply (advanceOnce h A) n s
+
+/-- The query asked at step `n` of the run. -/
+def queryStream (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
+    spec.Domain := A.expose (stateAfter h A s n)
+
+/-- The answer received at step `n` of the run. -/
+def answerStream (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) (n : ℕ) :
+    spec.Range (queryStream h A s n) := h (queryStream h A s n)
+
+/-- The length-`n` transcript of the run from state `s`: the recorded sequence of
+`⟨query, answer⟩` pairs, valued in `QueryLog spec`. This associates a concrete run log to the
+abstract state machine. -/
+def transcript (h : OracleHandler spec) (A : OracleStrategy S spec) :
+    S → ℕ → QueryLog spec
+  | _, 0 => []
+  | s, n + 1 => ⟨A.expose s, h (A.expose s)⟩ :: transcript h A (advanceOnce h A s) n
+
+@[simp] theorem transcript_zero (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S) :
+    transcript h A s 0 = [] := rfl
+
+@[simp] theorem transcript_succ (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S)
+    (n : ℕ) : transcript h A s (n + 1) =
+      ⟨A.expose s, h (A.expose s)⟩ :: transcript h A (advanceOnce h A s) n := rfl
+
+@[simp] theorem transcript_length (h : OracleHandler spec) (A : OracleStrategy S spec) (s : S)
+    (n : ℕ) : (transcript h A s n).length = n := by
+  induction n generalizing s with
+  | zero => rfl
+  | succ n ih => simp [ih]
+
+/-! ## The cofree behaviour trajectory
+
+`PFunctor.DynSystem.trajectory` gives the cofree-`p` behaviour tree of the strategy; for the closed
+run its spine is the state `iterate` (`PFunctor.DynSystem.next_iterate_trajectory`). -/
+
+/-- The behaviour trajectory of the closed-loop run: the cofree tree whose spine is the state
+sequence. The `n`-fold `CofreeC.next` walks it to the state after `n` steps. -/
+theorem next_iterate_trajectory_runAgainst (h : OracleHandler spec) (A : OracleStrategy S spec)
+    (s : S) (n : ℕ) :
+    (PFunctor.CofreeC.next)^[n] (PFunctor.DynSystem.trajectory (runAgainst h A) s) =
+      PFunctor.DynSystem.trajectory (runAgainst h A) (stateAfter h A s n) :=
+  PFunctor.DynSystem.next_iterate_trajectory (runAgainst h A) s n
+
+/-! ## Combinators: reductions, products, and parallel composition
+
+These reuse PolyFun's `wrap` / `pairing` / `tensor`, made meaningful on the oracle side. The key
+identification is **a reduction is a lens**: a sub-spec coercion `⊂ₒ` is a `PFunctor.Lens`
+(`SubSpec.toLens`), and applying it to a strategy is `wrap`, with composition for free. -/
+
+/-- Install a strategy into a larger oracle along a sub-spec inclusion `spec ⊂ₒ superSpec`. This is
+`wrap` along the reduction lens `SubSpec.toLens`; it rewrites each query forward and each answer
+backward, exactly a reduction of adversaries. -/
+def reduce {τ : Type u} {superSpec : OracleSpec.{u, v} τ} (h : spec ⊂ₒ superSpec)
+    (A : OracleStrategy S spec) : OracleStrategy S superSpec :=
+  PFunctor.DynSystem.wrap (SubSpec.toLens h) A
+
+/-- Reductions compose: reducing along `h₁` then `h₂` is reducing along `h₁.trans h₂`. Free from
+`PFunctor.DynSystem.wrap_comp` and `SubSpec.trans_toLens`. -/
+theorem reduce_trans {τ : Type u} {superSpec : OracleSpec.{u, v} τ}
+    {ρ : Type u} {superSpec' : OracleSpec.{u, v} ρ}
+    (h₁ : spec ⊂ₒ superSpec) (h₂ : superSpec ⊂ₒ superSpec') (A : OracleStrategy S spec) :
+    reduce h₂ (reduce h₁ A) = reduce (h₁.trans h₂) A := rfl
+
+/-- A shared-state strategy against the product oracle `spec₁ * spec₂`, built from two interface
+lenses out of one self-monomial state. This is PolyFun's categorical product `pairing`, landing in
+`PFunctor.prod = *` definitionally (directions are a `Sum`, matching `OracleSpec` `*`). -/
+def pair {ι₁ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {ι₂ : Type u} {spec₂ : OracleSpec.{u, v} ι₂}
+    {S : Type u} (l₁ : OracleStrategy S spec₁) (l₂ : OracleStrategy S spec₂) :
+    OracleStrategy S (spec₁ * spec₂) :=
+  PFunctor.DynSystem.pairing l₁ l₂
+
+/-- Parallel product of two independent-state strategies. This lands in the Dirichlet tensor
+`spec₁.toPFunctor ⊗ spec₂.toPFunctor`, a *synchronous joint oracle* (answers both at once) whose
+directions are a `Prod`. Note `⊗ ≠ *`: this interface has no standard `OracleSpec` preimage, unlike
+`pair`. Kept for modeling genuinely parallel adversaries. -/
+def juxtapose {ι₁ : Type u} {spec₁ : OracleSpec.{u, v} ι₁} {ι₂ : Type u}
+    {spec₂ : OracleSpec.{u, v} ι₂} {S₁ S₂ : Type w} (A : OracleStrategy S₁ spec₁)
+    (B : OracleStrategy S₂ spec₂) :
+    PFunctor.DynSystem (S₁ × S₂) (spec₁.toPFunctor ⊗ spec₂.toPFunctor) :=
+  A.tensor B
+
+/-! ## Probabilistic Kleisli run
+
+When the handler is randomized (`ProbHandler spec`), closing a strategy no longer gives a pure state
+endofunction but a **Markov chain on states**: `kleisliStep` samples an answer and advances, and its
+Kleisli iterate is the distribution over states (equivalently transcripts) after `n` adaptive
+queries. The deterministic run embeds as the Dirac special case (`ofHandler`). -/
+
+section Probabilistic
+
+variable {spec : OracleSpec.{u, u} ι} {S : Type u}
+
+/-- One probabilistic step: sample an answer to the exposed query from the handler, then advance the
+state. The result is a sub-distribution over next states. -/
+noncomputable def kleisliStep (H : ProbHandler spec) (A : OracleStrategy S spec) (s : S) :
+    SPMF S :=
+  (fun r => A.update s r) <$> H (A.expose s)
+
+/-- The `n`-fold Kleisli iterate of `kleisliStep`: the sub-distribution over states reached after
+`n` adaptive queries, starting from `s`. -/
+noncomputable def kleisliIterate (H : ProbHandler spec) (A : OracleStrategy S spec) :
+    ℕ → S → SPMF S
+  | 0, s => pure s
+  | n + 1, s => kleisliStep H A s >>= kleisliIterate H A n
+
+/-- The joint sub-distribution over the length-`n` transcript and the final state. -/
+noncomputable def kleisliTranscript (H : ProbHandler spec) (A : OracleStrategy S spec) :
+    S → ℕ → SPMF (QueryLog spec × S)
+  | s, 0 => pure ([], s)
+  | s, n + 1 => do
+      let r ← H (A.expose s)
+      let p ← kleisliTranscript H A (A.update s r) n
+      pure (⟨A.expose s, r⟩ :: p.1, p.2)
+
+/-- The sub-distribution over length-`n` transcripts of the randomized run from `s`. -/
+noncomputable def transcriptDist (H : ProbHandler spec) (A : OracleStrategy S spec) (s : S)
+    (n : ℕ) : SPMF (QueryLog spec) :=
+  Prod.fst <$> kleisliTranscript H A s n
+
+/-- A deterministic handler as a Dirac `ProbHandler`. -/
+noncomputable def _root_.ProbHandler.ofHandler (h : OracleHandler spec) : ProbHandler spec :=
+  fun t => (pure (h t) : SPMF (spec.Range t))
+
+@[simp] theorem kleisliStep_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
+    (s : S) : kleisliStep (ProbHandler.ofHandler h) A s = pure (advanceOnce h A s) := by
+  simp [kleisliStep, ProbHandler.ofHandler, advanceOnce]
+
+@[simp] theorem kleisliIterate_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
+    (n : ℕ) (s : S) :
+    kleisliIterate (ProbHandler.ofHandler h) A n s = pure (stateAfter h A s n) := by
+  induction n generalizing s with
+  | zero => rfl
+  | succ n ih => rw [kleisliIterate, kleisliStep_ofHandler, pure_bind, ih, stateAfter_succ]
+
+@[simp] theorem kleisliTranscript_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
+    (n : ℕ) (s : S) : kleisliTranscript (ProbHandler.ofHandler h) A s n =
+      pure (transcript h A s n, stateAfter h A s n) := by
+  induction n generalizing s with
+  | zero => rfl
+  | succ n ih =>
+      rw [kleisliTranscript, ProbHandler.ofHandler]
+      simp only [pure_bind, ih, transcript_succ, advanceOnce, stateAfter_succ]
+
+/-- **Dirac bridge.** The randomized transcript distribution of a deterministic handler is the Dirac
+mass on the deterministic transcript: parts 1 and 3 agree. -/
+@[simp] theorem transcriptDist_ofHandler (h : OracleHandler spec) (A : OracleStrategy S spec)
+    (s : S) (n : ℕ) :
+    transcriptDist (ProbHandler.ofHandler h) A s n = pure (transcript h A s n) := by
+  rw [transcriptDist, kleisliTranscript_ofHandler, map_pure]
+
+end Probabilistic
+
+end OracleStrategy
+
+/-! ## Headline: a program *is* a state machine whose run computes `simulateQ`
+
+`OracleComp spec` is the inductive querier; here we read it back as a coalgebra. A program becomes a
+closed dynamical system on the state set `OracleComp spec α` (the remaining computation), and
+iterating that system under a deterministic handler `h` for `stepsToHalt` steps lands at `pure` of
+`simulateQ (ofFn h)`. The randomized version exhibits `simulateQ` as one coalgebraic Kleisli step
+followed by the rest. -/
+
+namespace OracleComp
+
+variable {α : Type v}
+
+/-- One handler-driven reduction step of a program viewed as its own state: answer the head query
+with `h` and continue, or stay put at a `pure`. -/
+def advance (h : OracleHandler spec) (oa : OracleComp spec α) : OracleComp spec α :=
+  oa.casesOn (fun x => pure x) (fun t k => k (h t))
+
+@[simp] theorem advance_pure (h : OracleHandler spec) (x : α) :
+    advance h (pure x : OracleComp spec α) = pure x := rfl
+
+@[simp] theorem advance_queryBind (h : OracleHandler spec) (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec α) : advance h (queryBind t k) = k (h t) := rfl
+
+/-- The number of handler-answered query steps until the program halts. -/
+def stepsToHalt (h : OracleHandler spec) (oa : OracleComp spec α) : ℕ :=
+  OracleComp.construct (C := fun _ => ℕ) (fun _ => 0) (fun t _ ih => ih (h t) + 1) oa
+
+@[simp] theorem stepsToHalt_pure (h : OracleHandler spec) (x : α) :
+    stepsToHalt h (pure x : OracleComp spec α) = 0 := rfl
+
+@[simp] theorem stepsToHalt_queryBind (h : OracleHandler spec) (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec α) :
+    stepsToHalt h (queryBind t k) = stepsToHalt h (k (h t)) + 1 := rfl
+
+@[simp] theorem evalWithAnswerFn_queryBind (f : QueryImpl spec Id) (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec α) :
+    evalWithAnswerFn f (queryBind t k) = evalWithAnswerFn f (k (f t)) := by
+  change simulateQ f (queryBind t k) = simulateQ f (k (f t))
+  rw [show queryBind t k = liftM (spec.query t) >>= k from rfl, simulateQ_query_bind]
+  rfl
+
+/-- **Headline correspondence.** Answering a program's head query with a deterministic handler `h`,
+iterated for exactly `stepsToHalt` steps, lands at `pure` of the simulated value: the coalgebraic
+state iterate *computes* `simulateQ`/`evalWithAnswerFn`. -/
+theorem iterate_advance_eq_simulate (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (advance h)^[stepsToHalt h oa] oa = pure (evalWithAnswerFn (QueryImpl.ofFn h) oa) := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih =>
+      rw [stepsToHalt_queryBind, Function.iterate_succ_apply, advance_queryBind, ih,
+        evalWithAnswerFn_queryBind, QueryImpl.ofFn_apply]
+
+/-- The program as a closed dynamical system: the state is the remaining computation, the interface
+is the unit `X`, and one step answers the head query via `h`. The system reaches a fixed point
+exactly at `pure`; iterating it is `iterate_advance_eq_simulate`. -/
+def evalSystem (h : OracleHandler spec) (α : Type v) :
+    PFunctor.Closed.{max u v, u, v} (OracleComp spec α) :=
+  PFunctor.DynSystem.mk' (fun _ => PUnit.unit) (fun oa _ => advance h oa)
+
+@[simp] theorem evalSystem_step (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (evalSystem h α).step oa = advance h oa := rfl
+
+@[simp] theorem evalSystem_iterate (h : OracleHandler spec) (oa : OracleComp spec α) (n : ℕ) :
+    (evalSystem h α).iterate oa n = (advance h)^[n] oa := rfl
+
+/-- The `Closed`-system form of the headline: `Closed.iterate` of the program-system computes
+`simulateQ`. -/
+theorem iterate_evalSystem_eq_simulate (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (evalSystem h α).iterate oa (stepsToHalt h oa) =
+      pure (evalWithAnswerFn (QueryImpl.ofFn h) oa) :=
+  iterate_advance_eq_simulate h oa
+
+/-- Wrapper view: the deterministic run of a program against a handler. -/
+def runProgram (h : OracleHandler spec) (oa : OracleComp spec α) : OracleComp spec α :=
+  (evalSystem h α).iterate oa (stepsToHalt h oa)
+
+theorem runProgram_eq (h : OracleHandler spec) (oa : OracleComp spec α) :
+    runProgram h oa = pure (evalWithAnswerFn (QueryImpl.ofFn h) oa) :=
+  iterate_advance_eq_simulate h oa
+
+/-- Cofree corollary: the behaviour trajectory of the program-system, walked `stepsToHalt` steps,
+stabilizes at the trajectory of `pure (simulated value)`. The literal `trajectory ↔ simulateQ`
+shadow of the correspondence. -/
+theorem trajectory_evalSystem_stabilizes (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (PFunctor.CofreeC.next)^[stepsToHalt h oa]
+        (PFunctor.DynSystem.trajectory (evalSystem h α) oa) =
+      PFunctor.DynSystem.trajectory (evalSystem h α)
+        (pure (evalWithAnswerFn (QueryImpl.ofFn h) oa)) := by
+  rw [PFunctor.DynSystem.next_iterate_trajectory]
+  exact congrArg _ (iterate_evalSystem_eq_simulate h oa)
+
+end OracleComp
+
+/-! ## Probabilistic headline: `simulateQ` as a coalgebraic Kleisli step -/
+
+namespace OracleComp
+
+section Probabilistic
+
+variable {spec : OracleSpec.{u, u} ι} {α : Type u}
+
+/-- One randomized coalgebra step on programs: sample the head query's answer from `H`, exposing the
+continuation; a `pure` is already the answer. -/
+noncomputable def advanceK (H : ProbHandler spec) (oa : OracleComp spec α) :
+    SPMF (OracleComp spec α) :=
+  oa.casesOn (fun x => pure (pure x)) (fun t k => k <$> H t)
+
+@[simp] theorem advanceK_pure (H : ProbHandler spec) (x : α) :
+    advanceK H (pure x : OracleComp spec α) = pure (pure x) := rfl
+
+@[simp] theorem advanceK_queryBind (H : ProbHandler spec) (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec α) : advanceK H (queryBind t k) = k <$> H t := rfl
+
+/-- **Probabilistic headline.** The `SPMF` semantics of a program is one randomized coalgebra step
+followed by the semantics of the continuation — `simulateQ` unfolds coalgebraically. With the Dirac
+bridge (`transcriptDist_ofHandler`) this specializes to the deterministic correspondence. -/
+theorem simulateQ_eq_advanceK_bind (H : ProbHandler spec) (oa : OracleComp spec α) :
+    simulateQ H oa = advanceK H oa >>= simulateQ H := by
+  cases oa with
+  | pure x =>
+      change simulateQ H (pure x) = advanceK H (pure x) >>= simulateQ H
+      simp [advanceK_pure]
+  | queryBind t k =>
+      rw [advanceK_queryBind]
+      change simulateQ H (liftM (spec.query t) >>= k) = (k <$> H t) >>= simulateQ H
+      rw [simulateQ_query_bind]
+      simp [map_eq_bind_pure_comp]
+
+end Probabilistic
+
+/-! ## Subsumption: the program transcript *is* the logging-oracle output
+
+The coalgebraic transcript is not a new notion: running a program against a deterministic handler
+with the existing `QueryImpl.withLogging` instrumentation produces exactly `(simulated value,
+transcript)`. So the new layer reuses — rather than duplicates — VCVio's `QueryLog` machinery. -/
+
+variable {α : Type v}
+
+/-- The transcript of running a program `oa` against a deterministic handler `h`: the `⟨query,
+answer⟩` pairs in execution order. The program-side analogue of `OracleStrategy.transcript`. -/
+def transcript (h : OracleHandler spec) (oa : OracleComp spec α) : QueryLog spec :=
+  oa.construct (fun _ => ([] : QueryLog spec)) (fun t _k ih => ⟨t, h t⟩ :: ih (h t))
+
+@[simp] theorem transcript_pure (h : OracleHandler spec) (x : α) :
+    transcript h (pure x : OracleComp spec α) = [] := rfl
+
+@[simp] theorem transcript_queryBind (h : OracleHandler spec) (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec α) :
+    transcript h (queryBind t k) = ⟨t, h t⟩ :: transcript h (k (h t)) := rfl
+
+/-! ### Denotational query bounds
+
+Because `transcript` lands in `QueryLog spec`, its length is the number of handler-answered steps
+(`stepsToHalt`), and the existing `IsTotalQueryBound` becomes a *denotational* bound on the run:
+a program that makes at most `n` queries has a transcript of length at most `n`. -/
+
+/-- The transcript length is exactly the number of handler-answered query steps. -/
+@[simp] theorem transcript_length (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (transcript h oa).length = stepsToHalt h oa := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih => simp [ih]
+
+@[simp] theorem transcript_countQ_pure (h : OracleHandler spec) (p : ι → Prop) [DecidablePred p]
+    (x : α) : (transcript h (pure x : OracleComp spec α)).countQ p = 0 := rfl
+
+/-- `countQ` recurrence on the transcript: a query to `t` contributes one iff `p t`. -/
+theorem transcript_countQ_queryBind (h : OracleHandler spec) (p : ι → Prop) [DecidablePred p]
+    (t : spec.Domain) (k : spec.Range t → OracleComp spec α) :
+    (transcript h (queryBind t k)).countQ p =
+      (if p t then 1 else 0) + (transcript h (k (h t))).countQ p := by
+  simp only [transcript_queryBind, QueryLog.countQ, QueryLog.getQ_cons]
+  by_cases hpt : p t <;> simp [hpt, Nat.add_comm]
+
+/-! ### Typed transcripts via `PFunctor.FreeM.Path`
+
+`OracleComp spec` *is* `PFunctor.FreeM spec.toPFunctor`, and a `PFunctor.FreeM.Path` is a typed
+root-to-leaf branch choice — i.e. a sequence of typed oracle answers. A deterministic handler picks
+the canonical such path (`handlerPath`): its leaf is the simulated value (`output_handlerPath`) and
+its erasure is the flat `QueryLog` transcript (`logOfPath_handlerPath`). So the flat transcript is
+the answer-erasure of the program's typed interaction path. -/
+
+/-- The typed root-to-leaf path through a program induced by a deterministic handler: at each query
+node, choose the handler's answer. This is the program's *typed* transcript. -/
+def handlerPath (h : OracleHandler spec) : (oa : OracleComp spec α) → PFunctor.FreeM.Path oa
+  | .pure _ => ⟨⟩
+  | .roll a rest => ⟨h a, handlerPath h (rest (h a))⟩
+
+/-- The leaf selected by the handler's typed path is exactly the simulated value. -/
+theorem output_handlerPath (h : OracleHandler spec) (oa : OracleComp spec α) :
+    PFunctor.FreeM.output oa (handlerPath h oa) = evalWithAnswerFn (QueryImpl.ofFn h) oa := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih =>
+      have h1 : PFunctor.FreeM.output (queryBind t k) (handlerPath h (queryBind t k))
+          = PFunctor.FreeM.output (k (h t)) (handlerPath h (k (h t))) := rfl
+      rw [h1, ih, evalWithAnswerFn_queryBind, QueryImpl.ofFn_apply]
+
+/-- Erase a typed path to a flat `QueryLog`: pair each tree node's query with the answer the path
+selected there. -/
+def logOfPath : (oa : OracleComp spec α) → PFunctor.FreeM.Path oa → QueryLog spec
+  | .pure _, _ => []
+  | .roll a rest, ⟨b, path⟩ => ⟨a, b⟩ :: logOfPath (rest b) path
+
+/-- The flat transcript is the answer-erasure of the handler's typed path. -/
+theorem logOfPath_handlerPath (h : OracleHandler spec) (oa : OracleComp spec α) :
+    logOfPath oa (handlerPath h oa) = transcript h oa := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih =>
+      have h1 : logOfPath (queryBind t k) (handlerPath h (queryBind t k))
+          = ⟨t, h t⟩ :: logOfPath (k (h t)) (handlerPath h (k (h t))) := rfl
+      rw [h1, ih, transcript_queryBind]
+
+/-! ### Running along a reduction lens
+
+`reduce` rewrites a strategy *forward* along a `⊂ₒ` lens; dually, a program can be *run* along that
+lens, its queries answered by a super-spec handler. The runtime path it traces
+(`PFunctor.FreeM.PathAlong`) has the same leaf as running directly with the pulled-back handler —
+the denotational content of "a reduction is a lens". -/
+
+section Reduction
+
+variable {τ : Type u} {superSpec : OracleSpec.{u, v} τ}
+
+/-- A super-spec handler pulled back along a sub-spec inclusion: translate a `spec`-query forward,
+ask the super-handler, translate the answer back. -/
+def _root_.OracleHandler.pullback (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec) :
+    OracleHandler spec :=
+  OracleHandler.ofFn fun a => (SubSpec.toLens hs).toFunB a (H ((SubSpec.toLens hs).toFunA a))
+
+/-- The runtime path through a `spec`-program executed along the reduction lens, answered by a
+super-spec handler `H`. -/
+def runAlong (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec) :
+    (oa : OracleComp spec α) → PFunctor.FreeM.PathAlong (SubSpec.toLens hs) oa
+  | .pure _ => ⟨⟩
+  | .roll a rest => ⟨H ((SubSpec.toLens hs).toFunA a),
+      runAlong hs H (rest (OracleHandler.pullback hs H a))⟩
+
+/-- Running a program along the reduction lens with a super-spec handler computes the same value as
+running it directly with the pulled-back handler (`output_handlerPath`'s lens-relative form). -/
+theorem outputAlong_runAlong (hs : spec ⊂ₒ superSpec) (H : OracleHandler superSpec)
+    (oa : OracleComp spec α) :
+    PFunctor.FreeM.outputAlong (SubSpec.toLens hs) oa (runAlong hs H oa) =
+      evalWithAnswerFn (QueryImpl.ofFn (OracleHandler.pullback hs H)) oa := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih =>
+      have h1 : PFunctor.FreeM.outputAlong (SubSpec.toLens hs) (queryBind t k)
+            (runAlong hs H (queryBind t k))
+          = PFunctor.FreeM.outputAlong (SubSpec.toLens hs) (k (OracleHandler.pullback hs H t))
+              (runAlong hs H (k (OracleHandler.pullback hs H t))) := rfl
+      rw [h1, ih, evalWithAnswerFn_queryBind, QueryImpl.ofFn_apply]
+
+end Reduction
+
+section QueryBound
+
+variable {spec : OracleSpec.{u, u} ι} {α : Type u}
+
+/-- A total query bound bounds the number of handler-answered steps: if `oa` makes at most `n`
+queries, the run halts within `n` steps. The operational `IsTotalQueryBound` made denotational. -/
+theorem stepsToHalt_le_of_isTotalQueryBound (h : OracleHandler spec) :
+    ∀ {oa : OracleComp spec α} {n : ℕ}, IsTotalQueryBound oa n → stepsToHalt h oa ≤ n := by
+  intro oa
+  induction oa with
+  | pure x => intro n _; exact Nat.zero_le n
+  | queryBind t k ih =>
+      intro n hb
+      obtain ⟨hpos, hrest⟩ := hb
+      have hle := ih (h t) (hrest (h t))
+      simp only [] at hpos hle
+      rw [stepsToHalt_queryBind]; omega
+
+/-- **Denotational query bound.** A total query bound on a program bounds the length of every
+handler-answered transcript: if `oa` makes at most `n` queries, `(transcript h oa).length ≤ n`. -/
+theorem transcript_length_le_of_isTotalQueryBound (h : OracleHandler spec)
+    {oa : OracleComp spec α} {n : ℕ} (hb : IsTotalQueryBound oa n) :
+    (transcript h oa).length ≤ n := by
+  rw [transcript_length]; exact stepsToHalt_le_of_isTotalQueryBound h hb
+
+/-- **Predicate query bound.** If `oa` makes at most `n` queries matching `p`, the transcript
+contains at most `n` `p`-matching entries (`QueryLog.countQ`). -/
+theorem transcript_countQ_le_of_isQueryBoundP (h : OracleHandler spec) (p : ι → Prop)
+    [DecidablePred p] :
+    ∀ {oa : OracleComp spec α} {n : ℕ}, IsQueryBoundP oa p n →
+      (transcript h oa).countQ p ≤ n := by
+  intro oa
+  induction oa with
+  | pure x => intro n _; exact Nat.zero_le n
+  | queryBind t k ih =>
+      intro n hb
+      obtain ⟨hp, hrest⟩ := hb
+      have hle := ih (h t) (hrest (h t))
+      simp only [] at hle
+      rw [transcript_countQ_queryBind]
+      by_cases hpt : p t
+      · have hn : 0 < n := hp.resolve_left (not_not_intro hpt)
+        simp only [hpt, if_true] at hle ⊢
+        omega
+      · simp only [hpt, if_false] at hle ⊢
+        omega
+
+/-- **Per-index query bound.** If `oa` respects a per-index budget `qb`, then for every oracle index
+`t` the transcript contains at most `qb t` queries to `t`. -/
+theorem transcript_countQ_le_of_isPerIndexQueryBound (h : OracleHandler spec) [DecidableEq ι]
+    (t : ι) :
+    ∀ {oa : OracleComp spec α} {qb : ι → ℕ}, IsPerIndexQueryBound oa qb →
+      (transcript h oa).countQ (· = t) ≤ qb t := by
+  intro oa
+  induction oa with
+  | pure x => intro qb _; exact Nat.zero_le (qb t)
+  | queryBind t' k ih =>
+      intro qb hb
+      obtain ⟨hpos, hrest⟩ := hb
+      have hle := ih (h t') (hrest (h t'))
+      simp only [] at hpos hle
+      rw [transcript_countQ_queryBind]
+      rcases eq_or_ne t' t with rfl | htt
+      · rw [Function.update_self] at hle
+        split_ifs <;> omega
+      · rw [Function.update_of_ne htt.symm] at hle
+        simp only [if_neg htt]; omega
+
+end QueryBound
+
+section Subsumption
+
+variable {spec : OracleSpec.{u, u} ι} {α : Type u}
+
+/-- **Subsumption bridge.** Running a program against the deterministic handler `ofFn h` through the
+existing `QueryImpl.withLogging` instrumentation yields exactly the simulated value paired with the
+coalgebraic `transcript`. The new transcript is the established logging-oracle output. -/
+theorem run_simulateQ_ofFn_withLogging (h : OracleHandler spec) (oa : OracleComp spec α) :
+    (simulateQ ((QueryImpl.ofFn h).withLogging) oa).run =
+      (evalWithAnswerFn (QueryImpl.ofFn h) oa, transcript h oa) := by
+  induction oa with
+  | pure x => rfl
+  | queryBind t k ih =>
+      rw [transcript_queryBind, evalWithAnswerFn_queryBind, QueryImpl.ofFn_apply,
+        show queryBind t k = liftM (spec.query t) >>= k from rfl, simulateQ_query_bind]
+      simp only [QueryImpl.withLogging_apply, QueryImpl.ofFn_apply, OracleQuery.input_query,
+        WriterT.run_bind', monadLift_self, ih]
+      rfl
+
+end Subsumption
+
+end OracleComp
diff --git a/VCVio/OracleComp/Coinductive/Machine.lean b/VCVio/OracleComp/Coinductive/Machine.lean
new file mode 100644
index 000000000..b8aa6ff51
--- /dev/null
+++ b/VCVio/OracleComp/Coinductive/Machine.lean
@@ -0,0 +1,504 @@
+/-
+Copyright (c) 2026 Devon Tuma. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Devon Tuma
+-/
+import PolyFun.PFunctor.Dynamical.PointedMachine
+import VCVio.OracleComp.Coinductive.DynSystem
+import VCVio.OracleComp.QueryTracking.QueryBound
+
+/-!
+# Oracle Machines: Strategies with Initialization and Readout
+
+An `OracleMachine spec α β` is PolyFun's `PFunctor.PointedMachine` at the spec's polynomial:
+an `OracleStrategy` together with an initial-state map `init : α → State` and a Moore-style
+partial readout `output : State → Option β`. `output s = some b` means the machine has
+halted with result `b`, while `none` means it queries on. This is the machine-shaped
+presentation of an adversary `α → OracleComp spec β`.
+
+The run/unrolling theory is inherited from PolyFun rather than duplicated:
+
+* `OracleMachine.toComp` is `PFunctor.PointedMachine.toComp` — the fuelled unrolling into
+  `OracleComp spec (Option β)` (which *is* `FreeM spec.toPFunctor (Option β)`). Fuel counts
+  queries exactly: the readout is free, so the `k`-step unrolling makes at most `k` queries
+  and resolves precisely when the machine is steady within `k` queries.
+* `OracleMachine.runK`: the monad-parametric fuelled run — `PointedMachine.runWith` fed a
+  `QueryImpl spec m` (which *is* a `PFunctor.Handler m spec.toPFunctor`). The probabilistic
+  run of an adversary is the `m := SPMF` instance; the early-stopping behaviour (halted
+  states are absorbing) is what keeps sub-probability mass against lossy handlers.
+* `OracleMachine.runD`: the deterministic run, the `m := Id` instance of `runK`.
+* `simulateQ H (M.toComp k s) = M.runK H k s` is *definitional* (`simulateQ` is
+  `FreeM.mapM`, and `runWith` is `FreeM.mapM ∘ toComp`).
+
+Key definitions:
+
+* `OracleMachine.Implements M oa k` (scoped notation `M ⊨[k] oa`): the run of `M` at fuel
+  `k` agrees with `simulateQ` of
+  `oa` against every query implementation in every lawful monad. The single-monad SPMF
+  form (agreement against every `ProbHandler`) already pins down distribution semantics,
+  but the monad-parametric form is what stateful challengers consume (`m := StateT σ SPMF`
+  runs a machine against an oracle with hidden state) and it makes the deterministic form
+  `ImplementsDet` the trivial `m := Id` instance rather than a Dirac-bridge argument.
+* `OracleMachine.IsSimulation`: a step-synchronized simulation relation between machine
+  states and program residues; `implements_of_isSimulation` is the practical method for
+  establishing `Implements`, with the fuel supplied by a total query bound. One fuel
+  induction gives agreement in *every* lawful monad at once.
+-/
+
+universe u v w
+
+open OracleSpec PFunctor
+
+variable {ι : Type u} {spec : OracleSpec.{u, u} ι} {α β : Type u}
+
+/-! ## Oracle machines -/
+
+/-- An oracle machine: PolyFun's `PointedMachine` over the spec's polynomial. An adaptive
+querying strategy (`OracleStrategy`, the `toDynSystem` parent) together with an
+initialization of its state from an input and a Moore-style partial readout of its result.
+`output s = some b` means the machine has halted with result `b`; `output s = none` means
+it queries on. -/
+abbrev OracleMachine (spec : OracleSpec.{u, u} ι) (α β : Type u) :=
+  PFunctor.PointedMachine.{u, u, u, u, u} spec.toPFunctor α β
+
+/-- A query implementation *is* a PolyFun handler for the spec's polynomial — the
+identification `runK = PointedMachine.runWith` rests on. Recorded as a regression
+guard: it must remain definitional. -/
+example {m : Type u → Type u} : QueryImpl spec m = PFunctor.Handler m spec.toPFunctor := rfl
+
+namespace OracleMachine
+
+variable (M : OracleMachine spec α β)
+
+/-! ## Stability and steadiness -/
+
+/-- Output stability: once the readout is `some b`, every further update preserves it. -/
+def StableOutput : Prop :=
+  ∀ ⦃s : M.State⦄ ⦃b : β⦄, M.output s = some b →
+    ∀ r : spec.Range (M.expose s), M.output (M.update s r) = some b
+
+/-- A stable readout persists along every handler-answered run. -/
+theorem StableOutput.output_stateAfter {M : OracleMachine spec α β} (hst : M.StableOutput)
+    (h : OracleHandler spec) {s : M.State} {b : β} (hb : M.output s = some b) (k : ℕ) :
+    M.output (OracleStrategy.stateAfter h M.toDynSystem s k) = some b := by
+  induction k generalizing s with
+  | zero => exact hb
+  | succ k ih => exact OracleStrategy.stateAfter_succ h M.toDynSystem s k ▸ ih (hst hb _)
+
+/-- Steadiness against a handler: after `k` answered steps from `s`, the readout has
+resolved. -/
+def SteadyBy (h : OracleHandler spec) (s : M.State) (k : ℕ) : Prop :=
+  (M.output (OracleStrategy.stateAfter h M.toDynSystem s k)).isSome
+
+/-! ## Fuelled monad-parametric runs
+
+`runK` is `PointedMachine.runWith`: a `QueryImpl spec m` is definitionally a
+`PFunctor.Handler m spec.toPFunctor`, so the machine run against a randomized oracle
+(`m := SPMF`), a stateful oracle (`m := StateT σ SPMF`), or a deterministic handler
+(`m := Id`, packaged as `runD`) are all instances of one PolyFun run. -/
+
+section runK
+
+variable {m : Type u → Type u} [Monad m]
+
+/-- The fuelled run of a machine against a query implementation in an arbitrary monad,
+stopping early at the first `some` readout. At `m := SPMF` this is the sub-distribution
+over readouts after at most `k` adaptive queries, with halted states absorbing; early
+stopping is essential there, since continuing to sample after halting would multiply by
+the remaining handler mass against lossy handlers. -/
+def runK (H : QueryImpl spec m) : ℕ → M.State → m (Option β) :=
+  M.runWith H
+
+@[simp] theorem runK_zero (H : QueryImpl spec m) (s : M.State) :
+    M.runK H 0 s = pure (M.output s) := rfl
+
+theorem runK_succ_of_output_eq_none (H : QueryImpl spec m) {s : M.State}
+    (hb : M.output s = none) (k : ℕ) :
+    M.runK H (k + 1) s = H (M.expose s) >>= fun r => M.runK H k (M.update s r) := by
+  rw [runK, PointedMachine.runWith_succ, hb]
+  rfl
+
+/-- A halted machine's run is `pure` on its readout, at any fuel. -/
+theorem runK_of_output_eq_some (H : QueryImpl spec m) {s : M.State} {b : β}
+    (hb : M.output s = some b) (k : ℕ) : M.runK H k s = pure (some b) :=
+  PointedMachine.runWith_of_output_eq_some M H k hb
+
+theorem runK_succ_of_output_eq_some (H : QueryImpl spec m) {s : M.State} {b : β}
+    (hb : M.output s = some b) (k : ℕ) : M.runK H (k + 1) s = pure (some b) :=
+  M.runK_of_output_eq_some H hb (k + 1)
+
+/-- The probabilistic run unfolds through `kleisliStep`: sample an answer, advance, and
+recurse. The generic unfolding is `runK_succ_of_output_eq_none`. -/
+theorem runK_succ_of_output_eq_none' (H : ProbHandler spec) {s : M.State}
+    (hb : M.output s = none) (k : ℕ) :
+    M.runK H (k + 1) s = OracleStrategy.kleisliStep H M.toDynSystem s >>= M.runK H k := by
+  rw [M.runK_succ_of_output_eq_none H hb, OracleStrategy.kleisliStep, bind_map_left]
+  rfl
+
+end runK
+
+/-! ## The deterministic run -/
+
+/-- The fuelled deterministic run of a machine against a handler: the `m := Id` instance
+of `runK`, stopping early at the first `some` readout. For stable machines the plain
+readout after `k` steps agrees (`runD_eq_output_stateAfter`). -/
+def runD (h : OracleHandler spec) (k : ℕ) (s : M.State) : Option β :=
+  M.runK (m := Id) h.toQueryImpl k s
+
+@[simp] theorem runD_zero (h : OracleHandler spec) (s : M.State) :
+    M.runD h 0 s = M.output s := rfl
+
+theorem runD_succ_of_output_eq_some (h : OracleHandler spec) {s : M.State} {b : β}
+    (hb : M.output s = some b) (k : ℕ) : M.runD h (k + 1) s = some b :=
+  M.runK_succ_of_output_eq_some h.toQueryImpl hb k
+
+theorem runD_succ_of_output_eq_none (h : OracleHandler spec) {s : M.State}
+    (hb : M.output s = none) (k : ℕ) :
+    M.runD h (k + 1) s = M.runD h k (OracleStrategy.advanceOnce h M.toDynSystem s) :=
+  M.runK_succ_of_output_eq_none (m := Id) h.toQueryImpl hb k
+
+/-- A halted machine's run is its readout, at any fuel. -/
+theorem runD_of_output_eq_some (h : OracleHandler spec) {s : M.State} {b : β}
+    (hb : M.output s = some b) (k : ℕ) : M.runD h k s = some b :=
+  M.runK_of_output_eq_some h.toQueryImpl hb k
+
+/-- For a stable machine, the early-stopping run is the plain readout after `k` steps. -/
+theorem runD_eq_output_stateAfter {M : OracleMachine spec α β} (hst : M.StableOutput)
+    (h : OracleHandler spec) (k : ℕ) (s : M.State) :
+    M.runD h k s = M.output (OracleStrategy.stateAfter h M.toDynSystem s k) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih =>
+    cases hb : M.output s with
+    | none =>
+      rw [M.runD_succ_of_output_eq_none h hb, ih, OracleStrategy.stateAfter_succ]
+    | some b =>
+      rw [M.runD_succ_of_output_eq_some h hb, (hst.output_stateAfter h hb (k + 1)).symm]
+
+/-- For a stable machine, steadiness is exactly the early-stopping run resolving. -/
+theorem steadyBy_iff_isSome_runD {M : OracleMachine spec α β} (hst : M.StableOutput)
+    (h : OracleHandler spec) (s : M.State) (k : ℕ) :
+    M.SteadyBy h s k ↔ (M.runD h k s).isSome := by
+  rw [SteadyBy, runD_eq_output_stateAfter hst]
+
+/-- **Dirac bridge**: the probabilistic run against a deterministic handler is the Dirac
+mass on the deterministic run. -/
+@[simp] theorem runK_ofHandler (h : OracleHandler spec) (k : ℕ) (s : M.State) :
+    M.runK (ProbHandler.ofHandler h) k s = pure (M.runD h k s) := by
+  induction k generalizing s with
+  | zero => rfl
+  | succ k ih =>
+    cases hb : M.output s with
+    | some b =>
+      rw [M.runK_succ_of_output_eq_some _ hb, M.runD_succ_of_output_eq_some h hb]
+    | none =>
+      rw [M.runK_succ_of_output_eq_none' _ hb, OracleStrategy.kleisliStep_ofHandler,
+        pure_bind, ih, M.runD_succ_of_output_eq_none h hb]
+
+end OracleMachine
+
+namespace OracleComp
+
+/-! ## Simulation by a deterministic handler is deterministic -/
+
+/-- `simulateQ` on the `queryBind` constructor: answer the head query with the
+implementation, then simulate the continuation. -/
+theorem simulateQ_queryBind {r : Type u → Type w} [Monad r] [LawfulMonad r]
+    (impl : QueryImpl spec r) (t : spec.Domain) (k : spec.Range t → OracleComp spec β) :
+    simulateQ impl (queryBind t k) = impl t >>= fun u => simulateQ impl (k u) := by
+  rw [show queryBind t k = liftM (spec.query t) >>= k from rfl, simulateQ_bind,
+    simulateQ_spec_query]
+
+/-- `simulateQ` under the Dirac lift of a deterministic handler is the Dirac mass on the
+deterministic evaluation `evalWithAnswerFn`. -/
+theorem simulateQ_ofHandler (h : OracleHandler spec) (ob : OracleComp spec β) :
+    simulateQ (ProbHandler.ofHandler h) ob =
+      (pure (evalWithAnswerFn (QueryImpl.ofFn h) ob) : SPMF β) := by
+  induction ob with
+  | pure x => rfl
+  | queryBind t k ih =>
+    rw [simulateQ_queryBind]
+    simp only [ProbHandler.ofHandler, pure_bind]
+    rw [ih (h t), evalWithAnswerFn_queryBind, QueryImpl.ofFn_apply]
+
+end OracleComp
+
+namespace OracleMachine
+
+/-! ## The implements relation -/
+
+variable (M : OracleMachine spec α β)
+
+/-- A machine implements a program at fuel `k`: **PolyFun's native
+`PointedMachine.Implements`**, the free-handler equation `M.toComp k (M.init x) = some <$> oa x`
+(`OracleComp spec` is `FreeM spec.toPFunctor`). Stated at the free/initial handler, it pins
+the machine's observable behaviour once and universally; the run against *any* lawful-monad
+handler is the derived reading `Implements.runK_eq` (the `m := SPMF` instance pins the full
+distribution; `m := Id` gives the deterministic form). -/
+def Implements (oa : α → OracleComp spec β) (k : ℕ) : Prop :=
+  PFunctor.PointedMachine.Implements M oa k
+
+@[inherit_doc Implements]
+scoped notation:50 M " ⊨[" k "] " oa => OracleMachine.Implements M oa k
+
+/-- **The handler reading of `Implements`.** Running an implementing machine through any
+lawful-monad handler `H` agrees with `simulateQ H` of the program — a one-line corollary of
+`PointedMachine.Implements.runWith_eq` via `FreeM.mapM` naturality, using `runK = runWith`
+and `simulateQ = FreeM.mapMHom` definitionally. This is the monad-parametric form the
+stateful game transfer consumes (`m := StateT σ SPMF`), the distribution semantics
+(`m := SPMF`), and the deterministic form (`m := Id`), all at once. -/
+theorem Implements.runK_eq {M : OracleMachine spec α β} {oa : α → OracleComp spec β} {k : ℕ}
+    (h : M ⊨[k] oa) ⦃m : Type u → Type u⦄ [Monad m] [LawfulMonad m]
+    (H : QueryImpl spec m) (x : α) :
+    M.runK H k (M.init x) = some <$> simulateQ H (oa x) :=
+  PFunctor.PointedMachine.Implements.runWith_eq M H h x
+
+/-- Converse of `Implements.runK_eq`: agreement of the fuelled run with `simulateQ` against
+every lawful-monad handler already gives `Implements` — it suffices to check the free/initial
+handler (`m := OracleComp spec`, `QueryImpl.id'`), where `runK` is `toComp` and `simulateQ` is
+the identity. Lets run-level arguments (e.g. `runK_setInit`) discharge `Implements`. -/
+theorem Implements.of_runK_eq {M : OracleMachine spec α β} {oa : α → OracleComp spec β} {k : ℕ}
+    (h : ∀ ⦃m : Type u → Type u⦄ [Monad m] [LawfulMonad m] (H : QueryImpl spec m) (x : α),
+      M.runK H k (M.init x) = some <$> simulateQ H (oa x)) : M ⊨[k] oa := by
+  intro x
+  have key := h (m := OracleComp spec) (QueryImpl.id' spec) x
+  rwa [show M.runK (QueryImpl.id' spec) k (M.init x) = M.toComp k (M.init x) from
+    simulateQ_id' _, simulateQ_id'] at key
+
+/-- The deterministic form of the implements relation: the early-stopping run against
+every deterministic handler computes `evalWithAnswerFn`. Weaker than `Implements`; see
+`Implements.implementsDet`. -/
+def ImplementsDet (oa : α → OracleComp spec β) (k : ℕ) : Prop :=
+  ∀ (h : OracleHandler spec) (x : α),
+    M.runD h k (M.init x) = some (evalWithAnswerFn (QueryImpl.ofFn h) (oa x))
+
+/-- Monad-parametric agreement specializes to deterministic agreement at `m := Id`. -/
+theorem Implements.implementsDet {M : OracleMachine spec α β}
+    {oa : α → OracleComp spec β} {k : ℕ} (h : M ⊨[k] oa) :
+    M.ImplementsDet oa k := by
+  intro hd x
+  have key := h.runK_eq (m := Id) hd.toQueryImpl x
+  rw [runD, key]
+  rfl
+
+/-- For a stable machine, implementing a program at fuel `k` forces deterministic
+steadiness at `k`. -/
+theorem Implements.steadyBy {M : OracleMachine spec α β} {oa : α → OracleComp spec β}
+    {k : ℕ} (hst : M.StableOutput) (h : M ⊨[k] oa) (hd : OracleHandler spec)
+    (x : α) : M.SteadyBy hd (M.init x) k := by
+  rw [steadyBy_iff_isSome_runD hst, h.implementsDet hd x]
+  rfl
+
+/-- An implementing machine resolves along every randomized run: the early-stopping
+probabilistic run puts no mass on an unresolved readout. Probabilistic steadiness is
+thus a consequence of `Implements`, not an extra assumption. -/
+theorem Implements.runK_none_eq_zero {M : OracleMachine spec α β}
+    {oa : α → OracleComp spec β} {k : ℕ} (h : M ⊨[k] oa)
+    (H : ProbHandler spec) (x : α) : M.runK H k (M.init x) none = 0 := by
+  rw [h.runK_eq H x, map_eq_bind_pure_comp, SPMF.bind_apply_eq_tsum]
+  refine ENNReal.tsum_eq_zero.mpr fun b => ?_
+  rw [Function.comp_apply, (SPMF.pure_apply_eq_zero_iff _ _).mpr (by simp)]
+  exact mul_zero _
+
+/-! ## Simulation relations: the practical proof method for `Implements` -/
+
+/-- A step-synchronized simulation between machine states and program residues. This is
+PolyFun's interface-generic simulation relation specialized to the oracle polynomial. -/
+abbrev IsSimulation (R : M.State → OracleComp spec β → Prop) : Prop :=
+  PFunctor.PointedMachine.IsSimulation M R
+
+/-- **Main proof method.** A machine implements a program at any fuel that totally
+bounds the program's queries, given a simulation relation matching the initial states.
+The bound supplies the fuel; the simulation supplies the step-by-step agreement, in
+every lawful monad at once. -/
+theorem implements_of_isSimulation {M : OracleMachine spec α β}
+    {oa : α → OracleComp spec β} {k : ℕ} {R : M.State → OracleComp spec β → Prop}
+    (hsim : M.IsSimulation R) (hinit : ∀ x, R (M.init x) (oa x))
+    (hqb : ∀ x, OracleComp.IsTotalQueryBound (oa x) k) : M ⊨[k] oa :=
+  PFunctor.PointedMachine.implements_of_isSimulation hsim hinit hqb
+
+end OracleMachine
+
+/-! ## Bridging between programs and machines
+
+Query bounds on the inductive side and steadiness on the coinductive side are two
+presentations of the same finiteness. A program family with a total query bound `k` is
+a machine — its own residual program is the state — that is steady within `k` rounds
+against every handler and implements the family (`OracleComp.toMachine`). Conversely a
+machine unrolled for `k` rounds is a program with total query bound `k` — the PolyFun
+unrolling `PointedMachine.toComp`, whose `simulateQ` semantics is *definitionally* the
+machine's run (`simulateQ_toComp`). -/
+
+namespace OracleComp
+
+section ToMachine
+
+/-- The readout of a program: its value at `pure`, nothing at a query. -/
+def pureOutput (ob : OracleComp spec β) : Option β :=
+  ob.casesOn some fun _ _ => none
+
+@[simp] theorem pureOutput_pure (x : β) :
+    pureOutput (pure x : OracleComp spec β) = some x := rfl
+
+@[simp] theorem pureOutput_queryBind (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec β) : pureOutput (queryBind t k) = none := rfl
+
+variable [Inhabited ι]
+
+/-- The head query of a program; a default query at `pure`. -/
+def headQuery (ob : OracleComp spec β) : ι :=
+  ob.casesOn (fun _ => default) fun t _ => t
+
+@[simp] theorem headQuery_pure (x : β) :
+    headQuery (pure x : OracleComp spec β) = default := rfl
+
+@[simp] theorem headQuery_queryBind (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec β) : headQuery (queryBind t k) = t := rfl
+
+/-- Feed one answer to the head query of a program; a `pure` stays put. -/
+def headUpdate : (ob : OracleComp spec β) → spec.Range (headQuery ob) → OracleComp spec β :=
+  fun ob => ob.casesOn (motive := fun ob => spec.Range (headQuery ob) → OracleComp spec β)
+    (fun x _ => pure x) fun _ k r => k r
+
+@[simp] theorem headUpdate_pure (x : β)
+    (r : spec.Range (headQuery (pure x : OracleComp spec β))) :
+    headUpdate (pure x) r = pure x := rfl
+
+@[simp] theorem headUpdate_queryBind (t : spec.Domain)
+    (k : spec.Range t → OracleComp spec β) (r : spec.Range t) :
+    headUpdate (queryBind t k) r = k r := rfl
+
+/-- The readout survives one head update: it is only ever `some` at a `pure`, which
+head updates fix. -/
+theorem pureOutput_headUpdate_of_eq_some {ob : OracleComp spec β} {b : β}
+    (hb : pureOutput ob = some b) (r : spec.Range (headQuery ob)) :
+    pureOutput (headUpdate ob r) = some b := by
+  cases ob with
+  | pure x => exact hb
+  | queryBind t k => simp at hb
+
+/-- A program family as an oracle machine: the state is the residual program, one round
+answers the head query. Steadiness of this machine is exactly a total query bound on
+the family (`toMachine_steadyBy`), and it implements the family at any such bound
+(`toMachine_implements`). -/
+def toMachine (oa : α → OracleComp spec β) : OracleMachine spec α β where
+  State := OracleComp spec β
+  expose := headQuery
+  update := headUpdate
+  init := oa
+  output := pureOutput
+
+/-- One closed-loop step of the program-as-machine is `advance`. -/
+theorem toMachine_advanceOnce (h : OracleHandler spec) (oa : α → OracleComp spec β) :
+    OracleStrategy.advanceOnce h (toMachine oa).toDynSystem = advance h := by
+  refine funext fun ob : OracleComp spec β => ?_
+  cases ob with
+  | pure x => rfl
+  | queryBind t k => rfl
+
+theorem toMachine_stableOutput (oa : α → OracleComp spec β) :
+    OracleMachine.StableOutput (toMachine oa) :=
+  fun _ _ hb r => pureOutput_headUpdate_of_eq_some hb r
+
+/-- The program-as-machine is in step-synchronized simulation with the programs
+themselves, via equality of states and residual programs. -/
+theorem toMachine_isSimulation (oa : α → OracleComp spec β) :
+    OracleMachine.IsSimulation (toMachine oa) Eq where
+  output_pure := by rintro s b rfl; rfl
+  output_roll := by rintro s t k rfl; rfl
+  expose_eq := by rintro s t k rfl; rfl
+  update_rel := by rintro s t k rfl r; rfl
+
+open scoped OracleMachine in
+/-- **Program-to-machine bridge (semantics).** A query-bounded program family is
+implemented by its program-as-machine at the bound. -/
+theorem toMachine_implements {oa : α → OracleComp spec β} {k : ℕ}
+    (hqb : ∀ x, IsTotalQueryBound (oa x) k) : toMachine oa ⊨[k] oa :=
+  OracleMachine.implements_of_isSimulation (toMachine_isSimulation oa) (fun _ => rfl) hqb
+
+omit [Inhabited ι] in
+/-- Iterating `advance` at or beyond `stepsToHalt` lands at the simulated value: `pure`
+states are fixed points, so the run stabilizes. -/
+theorem iterate_advance_eq_of_le (h : OracleHandler spec) {ob : OracleComp spec β}
+    {n : ℕ} (hn : stepsToHalt h ob ≤ n) :
+    (advance h)^[n] ob = pure (evalWithAnswerFn (QueryImpl.ofFn h) ob) := by
+  obtain ⟨d, rfl⟩ := Nat.exists_eq_add_of_le hn
+  rw [Nat.add_comm, Function.iterate_add_apply, iterate_advance_eq_simulate,
+    Function.iterate_fixed (advance_pure h _)]
+
+/-- **Program-to-machine bridge (steadiness).** A total query bound on the program
+makes the program-as-machine steady within that bound, against every handler. -/
+theorem toMachine_steadyBy {oa : α → OracleComp spec β} (h : OracleHandler spec)
+    (x : α) {k : ℕ} (hqb : IsTotalQueryBound (oa x) k) :
+    OracleMachine.SteadyBy (toMachine oa) h ((toMachine oa).init x) k := by
+  have key : OracleStrategy.stateAfter h (toMachine oa).toDynSystem (oa x) k =
+      pure (evalWithAnswerFn (QueryImpl.ofFn h) (oa x)) := by
+    change (OracleStrategy.advanceOnce h (toMachine oa).toDynSystem)^[k] (oa x) = _
+    rw [toMachine_advanceOnce]
+    exact iterate_advance_eq_of_le h (stepsToHalt_le_of_isTotalQueryBound h hqb)
+  change (pureOutput (OracleStrategy.stateAfter h (toMachine oa).toDynSystem (oa x) k)).isSome
+  exact key ▸ rfl
+
+end ToMachine
+
+end OracleComp
+
+namespace OracleMachine
+
+/-! ## The unrolling bridge, inherited from PolyFun
+
+`M.toComp` is `PFunctor.PointedMachine.toComp`, which lands in
+`FreeM spec.toPFunctor (Option β) = OracleComp spec (Option β)` on the nose. The `Option`
+accounts for fuel exhaustion; under steadiness at `k` the result is always `some`. -/
+
+section ToComp
+
+variable (M : OracleMachine spec α β)
+
+theorem toComp_succ_of_output_eq_some {s : M.State} {b : β} (hb : M.output s = some b)
+    (k : ℕ) : M.toComp (k + 1) s = pure (some b) := by
+  rw [PointedMachine.toComp_succ, hb]
+  rfl
+
+theorem toComp_succ_of_output_eq_none {s : M.State} (hb : M.output s = none) (k : ℕ) :
+    M.toComp (k + 1) s =
+      OracleComp.queryBind (M.expose s) fun r => M.toComp k (M.update s r) := by
+  rw [PointedMachine.toComp_succ, hb]
+  rfl
+
+/-- A halted machine unrolls to its readout, at any fuel. -/
+theorem toComp_of_output_eq_some {s : M.State} {b : β} (hb : M.output s = some b)
+    (k : ℕ) : M.toComp k s = pure (some b) :=
+  PointedMachine.toComp_of_output_eq_some M k hb
+
+/-- **Machine-to-program bridge (query bounds).** The `k`-round unrolling makes at most
+`k` queries: steadiness fuel is a total query bound. -/
+theorem isTotalQueryBound_toComp (k : ℕ) (s : M.State) :
+    OracleComp.IsTotalQueryBound (M.toComp k s) k := by
+  induction k generalizing s with
+  | zero => cases hb : M.output s <;> · rw [show M.toComp 0 s = pure (M.output s) from rfl]; trivial
+  | succ k ih =>
+    cases hb : M.output s with
+    | some b => rw [M.toComp_succ_of_output_eq_some hb]; trivial
+    | none =>
+      rw [M.toComp_succ_of_output_eq_none hb]
+      exact OracleComp.isTotalQueryBound_query_bind_iff.mpr
+        ⟨Nat.succ_pos k, fun u => ih (M.update s u)⟩
+
+/-- **Machine-to-program bridge (semantics).** Simulating the unrolled program is the
+machine's run — *definitionally*: `simulateQ` is `FreeM.mapM` and `runK` is
+`PointedMachine.runWith = FreeM.mapM ∘ toComp`. -/
+theorem simulateQ_toComp {m : Type u → Type u} [Monad m] (H : QueryImpl spec m)
+    (k : ℕ) (s : M.State) : simulateQ H (M.toComp k s) = M.runK H k s := rfl
+
+/-- Deterministic form of `simulateQ_toComp`. -/
+theorem evalWithAnswerFn_toComp (h : OracleHandler spec) (k : ℕ) (s : M.State) :
+    evalWithAnswerFn (QueryImpl.ofFn h) (M.toComp k s) = M.runD h k s := by
+  have key := M.simulateQ_toComp (ProbHandler.ofHandler h) k s
+  rw [M.runK_ofHandler, OracleComp.simulateQ_ofHandler] at key
+  refine Set.singleton_injective (α := Option β) ?_
+  rw [← SPMF.support_pure, ← SPMF.support_pure, key]
+
+end ToComp
+
+end OracleMachine
diff --git a/lake-manifest.json b/lake-manifest.json
index 73330daaf..5b95bfd57 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -5,10 +5,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "04a12b67fa2048c9412fdd26ed9e446f25919d37",
+   "rev": "5c3a070362f68c5f9edb60b730985b2107eeaaf4",
    "name": "PolyFun",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "04a12b67fa2048c9412fdd26ed9e446f25919d37",
+   "inputRev": "5c3a070362f68c5f9edb60b730985b2107eeaaf4",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4",
diff --git a/lakefile.lean b/lakefile.lean
index c9ca83f59..dc7be0d3d 100644
--- a/lakefile.lean
+++ b/lakefile.lean
@@ -60,7 +60,7 @@ require "leanprover-community" / "mathlib" @ git "v4.31.0"
 
 require PolyFun from git
   "https://github.com/Verified-zkEVM/PolyFun.git" @
-  "04a12b67fa2048c9412fdd26ed9e446f25919d37"
+  "5c3a070362f68c5f9edb60b730985b2107eeaaf4"
 
 /-- Main library. -/
 @[default_target] lean_lib VCVio