feat(coinductive): let oracle machines implement OracleComp programs

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

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)

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. -/

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`

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 }

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