Dynamic concurrent processes

This file introduces the semantic center of the concurrent Interaction layer.

The structural syntax in Concurrent.Spec is a useful source language, but it is not the only natural presentation of concurrency. Many systems are better viewed as a residual process which, at any moment, exposes one finite sequential interaction episode; completing that episode yields the next residual process.

That is the viewpoint formalized here.

The file is organized in two levels:

• StepOver Γ P and ProcessOver Γ are the generic forms, parameterized by a realized node context Γ;
• Step Party P and Process Party are the closed-world specializations whose node metadata is exactly NodeSemantics Party.

So the intended reading is:

• a step is one finite local protocol episode,
• a process is an unbounded sequence of such steps obtained by continuation,
• and controller / observation metadata lives in a node context rather than being built into the process infrastructure itself.

This design stays continuation-first, but is more general than the structural tree frontend: cyclic or unbounded behavior is represented by the residual state type, while each individual step remains a finite Interaction.Spec.

structure Interaction.Concurrent.NodeSemantics (Party : Type u) (X : Type w) : Type (max u (w + 1))

NodeSemantics Party X records the local semantic data attached to one sequential interaction node whose move space is X.

It packages two orthogonal pieces of information:

• controllers x is the controller-path contribution associated to choosing the move x : X;
• views assigns to each party its local view of the chosen move x : X.

The controller-path contribution and the local views are intentionally stored separately. Many natural systems align them so that the first controller in controllers x has local view active, but this file does not force that relationship definitionally. Any desired coherence law can be imposed later as a separate well-formedness predicate.

• controllers : X → List Party
• views : Party → Multiparty.LocalView X

@[reducible, inline]

abbrev Interaction.Concurrent.StepContext (Party : Type u) (X : Type u_1) : Type (max u (u_1 + 1))

The closed-world node context used by the current concurrent semantics.

At a node with move space X, the context value is exactly the NodeSemantics Party X describing:

• which parties are recorded as controllers of the chosen move, and
• what each party locally observes of that move.

This is the context whose specialization recovers the existing closed-world Step / Process APIs.

structure Interaction.Concurrent.StepOver (Γ : Spec.Node.Context) (P : Type v) : Type (max (max v (w + 1)) w₂)

StepOver Γ P is one finite sequential interaction episode whose nodes are decorated by realized context Γ, and whose completion produces the next residual process state P.

Fields:

• spec is the shape of the sequential interaction episode;
• semantics decorates that sequential tree by node-local context Γ;
• next maps a complete transcript of that episode to the next residual process state.

The important point is that a StepOver is not restricted to a single atomic event. One concurrent step may itself be a short sequential protocol: for example, a scheduler choice followed by a payload choice, or a small request/response exchange treated as one logical concurrent transition.

So StepOver is the right object when the concurrency layer should expose finite sequential structure inside each global step, rather than flattening everything into atomic transitions.

• spec : Spec
• semantics : Spec.Decoration Γ self.spec
• next : self.spec.Transcript → P

def Interaction.Concurrent.StepOver.mapContext {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {P : Type v} (f : Spec.Node.ContextHom Γ Δ) (step : StepOver Γ P) : StepOver Δ P

Map the node-local context carried by a step along a realized context morphism.

This changes only the metadata decorating the step protocol. The underlying sequential interaction tree and the continuation next are left unchanged.

@[implicit_reducible]

instance Interaction.Concurrent.instFunctorStepOver {Γ : Spec.Node.Context} : Functor (StepOver Γ)

StepOver Γ is functorial in the continuation type: map f post-composes f after the next continuation, preserving the interaction protocol and its decoration.

instance Interaction.Concurrent.instLawfulFunctorStepOver {Γ : Spec.Node.Context} : LawfulFunctor (StepOver Γ)

structure Interaction.Concurrent.ProcessOver (Γ : Spec.Node.Context) : Type (max (max (v + 1) (w + 1)) w₂)

ProcessOver Γ is a continuation-based concurrent process whose current step episodes are decorated by realized context Γ.

From any residual process state p : Proc, the process exposes exactly one step protocol step p : StepOver Γ Proc. Running that step to completion produces the next residual state.

So ProcessOver should be read as:

a system whose behavior unfolds as a sequence of finite step protocols.

This is the generic semantic center for the concurrent layer. Structural trees, flat machines, and future frontends can all compile into ProcessOver by choosing an appropriate node-local context Γ.

• Proc : Type v
• step : self.Proc → StepOver Γ self.Proc

def Interaction.Concurrent.ProcessOver.mapContext {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} (f : Spec.Node.ContextHom Γ Δ) (process : ProcessOver Γ) : ProcessOver Δ

Map the node-local context carried by a process along a realized context morphism.

This changes only the metadata exposed at each step. The residual state space and transition structure are preserved.

@[implicit_reducible]

instance Interaction.Concurrent.ProcessOver.instCoalgStepOverProc {Γ : Spec.Node.Context} (p : ProcessOver Γ) : Coalg (StepOver Γ) p.Proc

Every ProcessOver Γ is an F-coalgebra for the StepOver Γ endofunctor.

def Interaction.Concurrent.ProcessOver.interleave {Γ₁ Γ₂ Δ : Spec.Node.Context} (p₁ : ProcessOver Γ₁) (p₂ : ProcessOver Γ₂) (f₁ : Spec.Node.ContextHom Γ₁ Δ) (f₂ : Spec.Node.ContextHom Γ₂ Δ) (schedulerCtx : Δ (ULift Bool)) : ProcessOver Δ

Binary-choice interleaving of two processes with different node contexts.

Given processes p₁ over Γ₁ and p₂ over Γ₂, context morphisms mapping each into a common target context Δ, and a scheduler decoration in Δ for the ULift Bool choice node, produce a single ProcessOver Δ whose state space is p₁.Proc × p₂.Proc.

At each step, a scheduler node chooses left (true) or right (false), then the selected subprocess's step protocol runs with its decoration mapped into Δ. Only the selected component of the product state advances.

theorem Interaction.Concurrent.ProcessOver.mapContext_interleave {Γ₁ Γ₂ Δ Δ' : Spec.Node.Context} (p₁ : ProcessOver Γ₁) (p₂ : ProcessOver Γ₂) (f₁ : Spec.Node.ContextHom Γ₁ Δ) (f₂ : Spec.Node.ContextHom Γ₂ Δ) (sched : Δ (ULift Bool)) (g : Spec.Node.ContextHom Δ Δ') : mapContext g (p₁.interleave p₂ f₁ f₂ sched) = p₁.interleave p₂ (g.comp f₁) (g.comp f₂) (g (ULift Bool) sched)

Post-composing mapContext g distributes over interleave: the result is the same interleaving with each injection pre-composed by g.

theorem Interaction.Concurrent.ProcessOver.interleave_mapContext {Γ₁ Γ₁' Γ₂ Γ₂' Δ : Spec.Node.Context} (p₁ : ProcessOver Γ₁) (p₂ : ProcessOver Γ₂) (g₁ : Spec.Node.ContextHom Γ₁ Γ₁') (g₂ : Spec.Node.ContextHom Γ₂ Γ₂') (f₁ : Spec.Node.ContextHom Γ₁' Δ) (f₂ : Spec.Node.ContextHom Γ₂' Δ) (sched : Δ (ULift Bool)) : (mapContext g₁ p₁).interleave (mapContext g₂ p₂) f₁ f₂ sched = p₁.interleave p₂ (f₁.comp g₁) (f₂.comp g₂) sched

Pre-composing both operands with mapContext distributes into the interleave injections via ContextHom.comp.

theorem Interaction.Concurrent.ProcessOver.interleave_mapContext_left {Γ₁ Γ₁' Γ₂ Δ : Spec.Node.Context} (p₁ : ProcessOver Γ₁) (p₂ : ProcessOver Γ₂) (g₁ : Spec.Node.ContextHom Γ₁ Γ₁') (f₁ : Spec.Node.ContextHom Γ₁' Δ) (f₂ : Spec.Node.ContextHom Γ₂ Δ) (sched : Δ (ULift Bool)) : (mapContext g₁ p₁).interleave p₂ f₁ f₂ sched = p₁.interleave p₂ (f₁.comp g₁) f₂ sched

Specialization of interleave_mapContext when only the left operand is pre-composed with mapContext.

theorem Interaction.Concurrent.ProcessOver.interleave_mapContext_right {Γ₁ Γ₂ Γ₂' Δ : Spec.Node.Context} (p₁ : ProcessOver Γ₁) (p₂ : ProcessOver Γ₂) (g₂ : Spec.Node.ContextHom Γ₂ Γ₂') (f₁ : Spec.Node.ContextHom Γ₁ Δ) (f₂ : Spec.Node.ContextHom Γ₂' Δ) (sched : Δ (ULift Bool)) : p₁.interleave (mapContext g₂ p₂) f₁ f₂ sched = p₁.interleave p₂ f₁ (f₂.comp g₂) sched

Specialization of interleave_mapContext when only the right operand is pre-composed with mapContext.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.EventMap {Γ : Spec.Node.Context} (process : ProcessOver Γ) (Event : Type w₃) : Type (max (max w₃ v) w)

A stable external label for each complete step transcript of a process.

The point of an EventMap is to attach one comparison-friendly label to a whole step, independently of how much internal sequential structure that step contains.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.Tickets {Γ : Spec.Node.Context} (process : ProcessOver Γ) (Ticket : Type w₃) : Type (max (max w₃ v) w)

A stable ticket for each complete step transcript of a process.

Tickets are the intended handles for fairness and liveness: instead of talking about unstable frontier events whose types change from state to state, later semantic layers can talk about these stable identifiers.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.TranscriptRel {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} (left : ProcessOver Γ) (right : ProcessOver Δ) : Type (max (max u_1 u_2) w)

TranscriptRel left right is a relation between one complete step transcript of left and one complete step transcript of right.

This is the generic step-matching interface consumed by refinement and bisimulation. No controller or observation structure is assumed here; those become special cases once the surrounding contexts are projected into StepContext.

def Interaction.Concurrent.ProcessOver.TranscriptRel.top {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} : left.TranscriptRel right

The permissive step relation that accepts every pair of complete step transcripts.

def Interaction.Concurrent.ProcessOver.TranscriptRel.reverse {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (rel : left.TranscriptRel right) : right.TranscriptRel left

Reverse a step-matching relation by flipping its two transcript arguments.

def Interaction.Concurrent.ProcessOver.TranscriptRel.inter {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver Γ} {right : ProcessOver Δ} (first second : left.TranscriptRel right) : left.TranscriptRel right

Conjunction of step-matching relations.

structure Interaction.Concurrent.ProcessOver.Labeled (Γ : Spec.Node.Context) : Type (max (max (max (v + 1) (w + 1)) w₂) (w₃ + 1))

ProcessOver.Labeled is a process equipped with a stable external event label for each complete step transcript.

• toProcess : ProcessOver Γ
• Event : Type w₃
• event : self.toProcess.EventMap self.Event

structure Interaction.Concurrent.ProcessOver.Ticketed (Γ : Spec.Node.Context) : Type (max (max (max (v + 1) (w + 1)) w₂) (w₃ + 1))

ProcessOver.Ticketed is a process equipped with a stable ticket for each complete step transcript.

These tickets are the obligation identifiers used by the fairness and liveness layers.

• toProcess : ProcessOver Γ
• Ticket : Type w₃
• ticket : self.toProcess.Tickets self.Ticket

structure Interaction.Concurrent.ProcessOver.System (Γ : Spec.Node.Context) extends Interaction.Concurrent.ProcessOver Γ : Type (max (max (u_1 + 1) (w + 1)) w₂)

ProcessOver.System Γ augments a process over context Γ by the standard verification predicates used throughout VCVio.

• Proc : Type u_1
• step : self.Proc → StepOver Γ self.Proc
• init : self.Proc → Prop
• assumptions : self.Proc → Prop
• safe : self.Proc → Prop
• inv : self.Proc → Prop

@[reducible, inline]

abbrev Interaction.Concurrent.Step (Party : Type u) (P : Type v) : Type (max (max v (u_1 + 1)) (u_1 + 1) u)

The closed-world specialization of StepOver.

Here the node context is fixed to StepContext Party, so every node carries the usual controller-path and local-view data for that party universe.

def Interaction.Concurrent.Step.controllerPath {Party : Type u} {P : Type v} (step : Step Party P) : step.spec.Transcript → List Party

controllerPath step tr is the controller sequence exposed by the concrete step transcript tr.

Every visited node contributes the controller list recorded for the chosen move at that node. These per-node contributions are concatenated along the whole step transcript.

So if a step internally consists of, say, "the scheduler chooses a branch, then Alice chooses a payload", the controller path records both pieces in order.

def Interaction.Concurrent.Step.controllerPath.go {Party : Type u} {spec : Spec} : Spec.Decoration (StepContext Party) spec → spec.Transcript → List Party

def Interaction.Concurrent.Step.currentController? {Party : Type u} {P : Type v} (step : Step Party P) (tr : step.spec.Transcript) : Option Party

currentController? step tr is the head of the controller path exposed by the concrete transcript tr, if such a controller exists.

This is the most immediate "who controlled this step?" projection. It is only the first controller because one step may internally contain several controlled subchoices.

@[reducible, inline]

abbrev Interaction.Concurrent.StepOver.controllerPath {Party : Type u} {P : Type v} (step : StepOver (StepContext Party) P) : step.spec.Transcript → List Party

Closed-world controller-path projection for a StepOver specialized to StepContext Party.

This bridge keeps the old dot-notation ergonomics after the StepOver cutover: downstream closed-world code can still write (process.step p).controllerPath tr.

@[reducible, inline]

abbrev Interaction.Concurrent.StepOver.currentController? {Party : Type u} {P : Type v} (step : StepOver (StepContext Party) P) (tr : step.spec.Transcript) : Option Party

Closed-world current-controller projection for a StepOver specialized to StepContext Party.

@[reducible, inline]

abbrev Interaction.Concurrent.Process (Party : Type u) : Type (max (max (u_1 + 1) (u_2 + 1)) (u_2 + 1) u)

The closed-world specialization of ProcessOver.

This is the process type consumed by the current execution, run, observation, refinement, fairness, and liveness layers.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.EventMap {Party : Type u} (process : Process Party) (Event : Type w₂) : Type (max (max w₂ u_1) u_2)

A stable external label for each complete closed-world process step.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Tickets {Party : Type u} (process : Process Party) (Ticket : Type w₂) : Type (max (max w₂ u_1) u_2)

A stable ticket for each complete closed-world process step.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.TranscriptRel {Party : Type u} (left : Process Party) (right : Process Party) : Type (max (max u_1 u_3) u_2)

The closed-world specialization of ProcessOver.TranscriptRel.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Labeled (Party : Type u) : Type (max (max (max (u_1 + 1) (u_2 + 1)) (u_2 + 1) u) (u_3 + 1))

Process.Labeled is a closed-world process together with a stable event label for each complete step transcript.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Ticketed (Party : Type u) : Type (max (max (max (u_1 + 1) (u_2 + 1)) (u_2 + 1) u) (u_3 + 1))

Process.Ticketed is a closed-world process together with a stable ticket for each complete step transcript.

These tickets are the obligation identifiers used later by the fairness and liveness layers.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.System (Party : Type u) : Type (max (max (u_1 + 1) (u_2 + 1)) (u_2 + 1) u)

Process.System augments a closed-world process by the standard verification predicates used throughout VCVio and in transition-system-style frameworks.

Its parent field toProcess is the dynamic semantics; the remaining fields are verification metadata on top of that semantics:

• init marks initial residual states;
• assumptions records ambient assumptions on runs;
• safe is the intended state safety predicate;
• inv is the intended inductive invariant.

This keeps the semantic object and the proof obligations separate while still bundling them in one place for refinement and liveness statements.