Asynchronous runtime semantics for env-open processes

This file defines the asynchronous-execution layer of the UC framework. The runtime alternates between process steps (processTick) and environment-driven events (envTick e) according to a pair of schedulers; the alphabet of env events is supplied by an EnvAction Event State (see EnvAction.lean).

The shape of every definition mirrors the synchronous processSemantics in Runtime.lean: the bundled SPMFSemantics m is threaded uniformly, so the same constructor serves coin-flip-only protocols, shared-oracle protocols, and observation-style semantics that introduce failure mass. The synchronous runtime is the special case in which the env scheduler always returns processTick and the env alphabet is empty; processSemantics_eq_processSemanticsAsync_trivial records that equivalence by name, with processSemanticsProbComp_eq_processSemanticsAsyncProbComp_trivial giving the ProbComp-specialized form most coin-flip-only protocol developments will reach for.

Main definitions

• RuntimeEvent Event / RuntimeTrace Event — the observable trace alphabet, a sum of processTick and envTick e.
• AsyncRuntimeState Proc State — the joint state threaded through async execution: the residual process state plus the env-action bookkeeping state.
• ProcessScheduler / EnvScheduler — the two sibling samplers driving the async runtime. The process scheduler reuses the existing Spec.Sampler m from Runtime.lean; the env scheduler is a separate monadic choice over RuntimeEvent.
• Concurrent.runStepsAsync — the recursive engine. Mirrors Concurrent.ProcessOver.runSteps from Runtime.lean, with explicit env-event interleaving.
• UC.processSemanticsAsync — the headline Semantics constructor.
• UC.processSemanticsAsyncProbComp — the coin-flip-only specialization, companion to processSemanticsProbComp.
• trivialEnvScheduler — the env scheduler that always returns processTick.

Universe constraints

The runtime layer requires move types, state types, and the env-event alphabet to live at universe 0, so that ProbComp and the runtime monad m : Type → Type fit. This is strictly stronger than the data layer in EnvAction.lean (which is generic in Event : Type uE) because the runtime needs m (RuntimeEvent Event) to typecheck, and m : Type → Type forces RuntimeEvent Event : Type and hence Event : Type. Concrete env-event alphabets such as MomentaryCorruption.Alphabet Sid Pid (with Sid Pid : Type) live at universe 0, so this is not a restriction in practice. The same universe-0 constraint applies to processSemantics.

Runtime trace alphabet

inductive Interaction.UC.RuntimeEvent (Event : Type) : Type

One tick of the async runtime: either a process step (no payload, the actual move is sampled inside the Spec-driven procScheduler) or an environment event carrying its alphabet symbol.

The sum is non-symmetric on purpose: processTick carries no payload because the move space at a process step is determined by the process's Spec, not by the runtime trace; envTick carries the alphabet symbol because the EnvAction.react reaction is keyed by the symbol.

• processTick {Event : Type} : RuntimeEvent Event
• envTick {Event : Type} (e : Event) : RuntimeEvent Event

def Interaction.UC.instDecidableEqRuntimeEvent.decEq {Event✝ : Type} [DecidableEq Event✝] (x✝ x✝¹ : RuntimeEvent Event✝) : Decidable (x✝ = x✝¹)

@[implicit_reducible]

instance Interaction.UC.instDecidableEqRuntimeEvent {Event✝ : Type} [DecidableEq Event✝] : DecidableEq (RuntimeEvent Event✝)

@[simp]

theorem Interaction.UC.RuntimeEvent.processTick_ne_envTick {Event : Type} (e : Event) : processTick ≠ envTick e

@[simp]

theorem Interaction.UC.RuntimeEvent.envTick_ne_processTick {Event : Type} (e : Event) : envTick e ≠ processTick

@[reducible, inline]

abbrev Interaction.UC.RuntimeTrace (Event : Type) : Type

The complete observable trace of one async run.

Async-runtime distributional reasoning compares distributions over RuntimeTrace × Result, so this is the type forwarding and healing lemmas work over.

Joint runtime state

structure Interaction.UC.AsyncRuntimeState (Proc State : Type) : Type

Joint state threaded through async execution: the residual process state plus the env-action's bookkeeping state.

The runtime treats this structure opaquely through the ProcessScheduler and EnvScheduler signatures, so a future reactive variant that adds per-port pending packet queues (and possibly a queue of pending env events) can extend this structure without invalidating the scheduler APIs.

• proc : Proc

  The residual process state.

• envState : State

  The env-action bookkeeping state.

theorem Interaction.UC.AsyncRuntimeState.ext {Proc State : Type} {x y : AsyncRuntimeState Proc State} (proc : x.proc = y.proc) (envState : x.envState = y.envState) : x = y

theorem Interaction.UC.AsyncRuntimeState.ext_iff {Proc State : Type} {x y : AsyncRuntimeState Proc State} : x = y ↔ x.proc = y.proc ∧ x.envState = y.envState

@[simp]

theorem Interaction.UC.AsyncRuntimeState.mk_eta {Proc State : Type} (st : AsyncRuntimeState Proc State) : { proc := st.proc, envState := st.envState } = st

Schedulers

@[reducible, inline]

abbrev Interaction.UC.ProcessScheduler (m : Type → Type) (Proc State : Type) (specOf : AsyncRuntimeState Proc State → Spec) : Type

A process scheduler picks a process-side Spec.Sampler at each step, parameterized by the joint async-runtime state.

The sampler-side type Spec.Sampler m (specOf st) is the existing one from Runtime.lean, unchanged. The extra AsyncRuntimeState-dependent argument lets a scheduler refuse to schedule, e.g., a corrupted machine's tick.

@[reducible, inline]

abbrev Interaction.UC.EnvScheduler (m : Type → Type) (Proc State Event : Type) : Type

An env scheduler chooses the next runtime event in the monad m.

Returning processTick yields control back to the process layer; returning envTick e fires e against the env-action. This is the sibling channel to ProcessScheduler: security definitions over the async runtime quantify over both schedulers, so that the typed split between adversary-controlled process scheduling and environment-controlled env scheduling is preserved.

def Interaction.UC.trivialEnvScheduler {m : Type → Type} [Pure m] {Proc : Type} (State Event : Type) : EnvScheduler m Proc State Event

The trivial env scheduler that always returns processTick.

Instantiating processSemanticsAsync at this scheduler with the empty env alphabet recovers the synchronous processSemantics; see processSemantics_eq_processSemanticsAsync_trivial.

@[simp]

theorem Interaction.UC.trivialEnvScheduler_apply {m : Type → Type} [Pure m] {Proc State Event : Type} (st : AsyncRuntimeState Proc State) : trivialEnvScheduler State Event st = pure RuntimeEvent.processTick

Async core engine

noncomputable def Interaction.Concurrent.runStepsAsync {m : Type → Type} [Monad m] [MonadLiftT ProbComp m] {Γ : Spec.Node.Context} {State Event : Type} (process : ProcessOver Γ) (envAction : UC.EnvAction Event State) (procScheduler : UC.ProcessScheduler m process.Proc State fun (st : UC.AsyncRuntimeState process.Proc State) => (process.step st.proc).spec) (envScheduler : UC.EnvScheduler m process.Proc State Event) : ℕ → UC.AsyncRuntimeState process.Proc State → m (UC.AsyncRuntimeState process.Proc State × UC.RuntimeTrace Event)

Async core engine. Iterates fuel ticks, alternating between process samples and env reactions according to envScheduler. Returns the final joint state and the observable runtime trace.

Mirrors the recursion shape of Concurrent.ProcessOver.runSteps with explicit env-event interleaving. The env reaction lives in ProbComp (EnvAction.react : Event → State → ProbComp State) and is lifted into the runtime monad m via MonadLiftT ProbComp m. The process sampler type is unchanged from the synchronous runtime: the ProcessScheduler carries the existing Spec.Sampler m from Runtime.lean.

theorem Interaction.Concurrent.runStepsAsync_empty_trivial_eq {m : Type → Type} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] {Γ : Spec.Node.Context} (process : ProcessOver Γ) (sampler : (s : process.Proc) → Spec.Sampler m (process.step s).spec) (fuel : ℕ) (s : process.Proc) : runStepsAsync process (UC.EnvAction.empty Unit) (fun (st : UC.AsyncRuntimeState process.Proc Unit) => sampler st.proc) (UC.trivialEnvScheduler Unit Empty) fuel { proc := s, envState := () } = do let s' ← process.runSteps sampler fuel s pure ({ proc := s', envState := () }, List.replicate fuel UC.RuntimeEvent.processTick)

Under the empty env alphabet (EnvAction.empty Unit) and the trivial env scheduler (always processTick), runStepsAsync reduces to ProcessOver.runSteps with the env state pinned to () and a constant processTick trace.

This is the operational core of the sync-recovery story: it factors the async engine into the synchronous ProcessOver.runSteps plus a trivial trace bookkeeping pass, and is reused by UC.processSemantics_eq_processSemanticsAsync_trivial.

noncomputable def Interaction.UC.processSemanticsAsync (Party : Type u) {m : Type → Type} [Monad m] [MonadLiftT ProbComp m] (schedulerSampler : m (ULift.{0, 0} Bool)) (sem : SPMFSemantics m) {Event State : Type} (envAction : EnvAction Event State) (initEnvState : State) (init : (p : Interaction.UC.Closed✝ Party m schedulerSampler) → p.Proc) (envScheduler : (p : Interaction.UC.Closed✝¹ Party m schedulerSampler) → EnvScheduler m p.Proc State Event) (fuel : ℕ) (observe : (p : Interaction.UC.Closed✝² Party m schedulerSampler) → p.Proc → State → RuntimeTrace Event → m Unit) : Semantics (openTheory Party m schedulerSampler)

Construct an async Semantics for the open-process theory.

Threads an env-action channel and an env scheduler. The per-step process sampler is obtained directly from the closed process's stepSampler (keyed by the underlying process state, ignoring any async env state). The bundled SPMFSemantics m plays the same role as in processSemantics and supports the same instantiations: coin-flip-only protocols via processSemanticsAsyncProbComp, shared-oracle protocols via an OracleComp-monad SPMFSemantics built with simulateQ', and observation-style semantics over OptionT ProbComp.

The init and envScheduler arguments are quantified over the closed process p : Closed Party, matching the shape of the synchronous processSemantics.

noncomputable def Interaction.UC.processSemanticsAsyncProbComp (Party : Type u) (schedulerSampler : ProbComp (ULift.{0, 0} Bool)) {Event State : Type} (envAction : EnvAction Event State) (initEnvState : State) (init : (p : Interaction.UC.Closed✝ Party ProbComp schedulerSampler) → p.Proc) (envScheduler : (p : Interaction.UC.Closed✝¹ Party ProbComp schedulerSampler) → EnvScheduler ProbComp p.Proc State Event) (fuel : ℕ) (observe : (p : Interaction.UC.Closed✝² Party ProbComp schedulerSampler) → p.Proc → State → RuntimeTrace Event → ProbComp Unit) : Semantics (openTheory Party ProbComp schedulerSampler)

Coin-flip-only specialization of processSemanticsAsync (m = ProbComp, sem := SPMFSemantics.ofHasEvalSPMF ProbComp). Companion of processSemanticsProbComp.

Sync recovery

theorem Interaction.UC.processSemantics_eq_processSemanticsAsync_trivial (Party : Type u) {m : Type → Type} [Monad m] [LawfulMonad m] [MonadLiftT ProbComp m] (schedulerSampler : m (ULift.{0, 0} Bool)) (sem : SPMFSemantics m) (init : (p : Interaction.UC.Closed✝ Party m schedulerSampler) → p.Proc) (fuel : ℕ) (observe : (p : Interaction.UC.Closed✝¹ Party m schedulerSampler) → p.Proc → m Unit) : processSemantics Party schedulerSampler sem init fuel observe = processSemanticsAsync Party schedulerSampler sem (EnvAction.empty Unit) () init (fun (p : Interaction.UC.Closed✝² Party m schedulerSampler) => trivialEnvScheduler Unit Empty) fuel fun (p : Interaction.UC.Closed✝³ Party m schedulerSampler) (s : p.Proc) (x : Unit) (x_1 : RuntimeTrace Empty) => observe p s

The synchronous processSemantics is the special case of processSemanticsAsync instantiated at:

• the empty env alphabet (EnvAction.empty Unit, with state Unit);
• the trivial env scheduler (always returns processTick);
• an observe that ignores the env state and the trace.

The proof factors through Concurrent.runStepsAsync_empty_trivial_eq, which collapses the async engine to ProcessOver.runSteps together with a constant processTick trace; the observe-side argument then drops the trace and the unit env state.

theorem Interaction.UC.processSemanticsProbComp_eq_processSemanticsAsyncProbComp_trivial (Party : Type u) (schedulerSampler : ProbComp (ULift.{0, 0} Bool)) (init : (p : Interaction.UC.Closed✝ Party ProbComp schedulerSampler) → p.Proc) (fuel : ℕ) (observe : (p : Interaction.UC.Closed✝¹ Party ProbComp schedulerSampler) → p.Proc → ProbComp Unit) : processSemanticsProbComp Party schedulerSampler init fuel observe = processSemanticsAsyncProbComp Party schedulerSampler (EnvAction.empty Unit) () init (fun (p : Interaction.UC.Closed✝² Party ProbComp schedulerSampler) => trivialEnvScheduler Unit Empty) fuel fun (p : Interaction.UC.Closed✝³ Party ProbComp schedulerSampler) (s : p.Proc) (x : Unit) (x_1 : RuntimeTrace Empty) => observe p s

The ProbComp specialization of processSemantics_eq_processSemanticsAsync_trivial: the synchronous processSemanticsProbComp equals the trivial async lift built from processSemanticsAsyncProbComp with the empty env alphabet, the trivial env scheduler, and an observe that ignores the env state and the trace.

This is the form most coin-flip-only protocol developments will reach for: it discharges the m/close/MonadLiftT choices the general theorem leaves abstract, leaving only the protocol-specific data (init, sampler, fuel, observe) on each side of the equation.