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 NodeProfile Party, the bundled NodeAuthority + NodeView view of node-local semantic data.

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.NodeAuthority (Party : Type u) (X : Type w) : Type (max u w)

NodeAuthority Party X records the controller-attribution part of node-local semantic data: which parties are credited as controllers of each move x : X.

This is one of the two orthogonal layers of NodeProfile. It is stored separately so that downstream reasoning that depends only on controller attribution (corruption policies, scheduler accountability, party-side responsibility arguments) can take a NodeAuthority parameter without committing to any particular observation structure.

• controllers : X → List Party

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

NodeView Party X records the view-attribution part of node-local semantic data: what each party me : Party locally observes of the chosen move x : X, expressed as a Multiparty.ViewMode X.

This is the second of the two orthogonal layers of NodeProfile. It is stored separately so that downstream reasoning that depends only on local views (information-flow arguments, projection / trace semantics, view-equivalence proofs) can take a NodeView parameter without committing to any particular controller attribution.

The name avoids confusion with Multiparty.Observation X, which is the unrelated per-move information-lattice kernel living in Multiparty/Observation.lean. NodeView is the per-party operational view assignment at one node; Observation is one quotient morphism X → Obs packaged with its codomain.

• views : Party → Multiparty.ViewMode X

structure Interaction.Concurrent.NodeProfile (Party : Type u) (X : Type w) extends Interaction.Concurrent.NodeAuthority Party X, Interaction.Concurrent.NodeView Party X : Type (max u (w + 1))

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

It bundles two orthogonal layers:

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

The two layers are intentionally stored as separate factor structures. 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.

Because NodeProfile extends both factors, the dot-notation accessors node.controllers, node.views and the structure-literal constructor { controllers := ..., views := ... } work exactly as if the fields were declared inline. The factor projections node.toNodeAuthority, node.toNodeView are auto-generated and let downstream code restrict attention to a single layer.

• controllers : X → List Party
• views : Party → Multiparty.ViewMode 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 NodeProfile 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.

Polynomial reading

StepOver Γ P is the application to P of the polynomial functor StepOver.toPFunctor Γ whose positions are Γ-decorated specs and whose directions over a position are transcripts of its underlying spec. The Equiv StepOver.equivObj exhibits this on the nose by regrouping the (spec, semantics, next) fields. The position type is itself equivalent to Interaction.Spec.DecoratedSpec Γ via Interaction.Spec.decoratedSpecEquiv, identifying StepOver as a polynomial substrate built directly on top of Γ.toPFunctor. The structure form is preserved as the working API because its named fields support clean { spec := ..., semantics := ..., next := ... } construction at every call site, and projections such as (mapContext f s).spec are definitionally equal to s.spec.

• 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 Γ)

Polynomial bridge

StepOver Γ P is the application to P of the polynomial functor StepOver.toPFunctor Γ whose positions are Γ-decorated specs and whose direction family at each position is the type of complete transcripts of the underlying spec. The Equiv StepOver.equivObj regroups the (spec, semantics, next) fields into the polynomial form (position, continuation); both roundtrips are definitionally rfl.

The position type Σ spec, Decoration Γ spec is itself equivalent to Interaction.Spec.DecoratedSpec Γ via Interaction.Spec.decoratedSpecEquiv, which is the free monad on Γ.toPFunctor at the unit payload. This bridge identifies StepOver as a polynomial substrate sitting directly on top of Γ.toPFunctor while preserving the structure form's ergonomic call sites and definitional projection equalities.

@[reducible]

def Interaction.Concurrent.StepOver.toPFunctor (Γ : Spec.Node.Context) : PFunctor.{max (w + 1) w₂, w}

The polynomial functor whose application to P is StepOver Γ P.

A position is a Γ-decorated spec — a pair of an interaction shape spec : Spec and a Decoration Γ spec of per-node Γ-metadata on it. A direction over such a position is a complete transcript of spec.

Up to Interaction.Spec.decoratedSpecEquiv, positions are exactly Interaction.Spec.DecoratedSpec Γ, the free term of Γ.toPFunctor at the unit payload.

def Interaction.Concurrent.StepOver.equivObj {Γ : Spec.Node.Context} {P : Type v} : StepOver Γ P ≃ ↑(toPFunctor Γ) P

StepOver Γ P is exactly (StepOver.toPFunctor Γ).Obj P, exhibiting the step-over structure as a polynomial application.

The forward direction regroups the (spec, semantics, next) fields into the polynomial form (position, continuation), and the inverse unpacks them again. Both roundtrips are definitionally rfl.

@[simp]

theorem Interaction.Concurrent.StepOver.equivObj_symm_apply {Γ : Spec.Node.Context} {P : Type v} (x✝ : ↑(toPFunctor Γ) P) : equivObj.symm x✝ = match x✝ with | ⟨⟨spec, semantics⟩, next⟩ => { spec := spec, semantics := semantics, next := next }

@[simp]

theorem Interaction.Concurrent.StepOver.equivObj_apply_snd {Γ : Spec.Node.Context} {P : Type v} (s : StepOver Γ P) (a✝ : s.spec.Transcript) : (equivObj s).snd a✝ = s.next a✝

@[simp]

theorem Interaction.Concurrent.StepOver.equivObj_apply_fst_snd {Γ : Spec.Node.Context} {P : Type v} (s : StepOver Γ P) : (equivObj s).fst.snd = s.semantics

@[simp]

theorem Interaction.Concurrent.StepOver.equivObj_apply_fst_fst {Γ : Spec.Node.Context} {P : Type v} (s : StepOver Γ P) : (equivObj s).fst.fst = s.spec

def Interaction.Concurrent.StepOver.equivPositions (Γ : Spec.Node.Context) : (toPFunctor Γ).A ≃ Spec.DecoratedSpec Γ

The position type of StepOver.toPFunctor Γ is the same data as a Γ-decorated spec, via Interaction.Spec.decoratedSpecEquiv. This is the bridge that identifies the StepOver polynomial as a substrate built on top of Γ.toPFunctor.

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.{w, 0} 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.{w, 0} Bool)) (g : Spec.Node.ContextHom Δ Δ') : mapContext g (p₁.interleave p₂ f₁ f₂ sched) = p₁.interleave p₂ (g.comp f₁) (g.comp f₂) (g (ULift.{w, 0} 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.{w, 0} 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.{w, 0} 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.{w, 0} 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

Polynomial-coalgebra behavior

StepOver.toPFunctor Γ (from S3) exhibits one episode of Γ-decorated interaction as a polynomial functor. Its terminal coalgebra is the M-type PFunctor.M (StepOver.toPFunctor Γ): the type of all possibly-infinite trees of step protocols.

Every ProcessOver Γ is canonically a coalgebra for this polynomial functor (process.step composed with the polynomial bridge equivObj), so the universal property of M-types gives a unique coalgebra homomorphism behavior : process.Proc → M (StepOver.toPFunctor Γ). This function records, at each residual state, the observable infinite tree of step protocols obtained by repeatedly running process.step.

The universal property is concretely the "bisimulation by uniqueness" principle: any candidate behavior function that respects the coalgebra structure must equal the canonical one. Equality of behavior trees is therefore the canonical observational equivalence on residual states, agreeing on the nose with any relational bisimulation witness one might construct via Concurrent.Refinement.Bisimulation.

@[reducible, inline]

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

The terminal coalgebra of StepOver.toPFunctor Γ: the type of possibly-infinite trees of Γ-decorated step protocols. Each such tree records one complete observable behavior of a ProcessOver Γ from a chosen seed state.

def Interaction.Concurrent.ProcessOver.behavior {Γ : Spec.Node.Context} (process : ProcessOver Γ) : process.Proc → Behavior Γ

The unique coalgebra homomorphism from process into the terminal StepOver.toPFunctor Γ-coalgebra. Each residual state is mapped to its observable behavior tree.

@[simp]

theorem Interaction.Concurrent.ProcessOver.dest_behavior {Γ : Spec.Node.Context} (process : ProcessOver Γ) (p : process.Proc) : PFunctor.M.dest (process.behavior p) = (StepOver.toPFunctor Γ).map process.behavior (StepOver.equivObj (process.step p))

The defining equation of behavior: destructing the behavior tree at a state recovers one step protocol from process.step, with each subtree obtained by applying behavior to the corresponding continuation.

theorem Interaction.Concurrent.ProcessOver.behavior_unique {Γ : Spec.Node.Context} (process : ProcessOver Γ) (f : process.Proc → Behavior Γ) (hf : ∀ (p : process.Proc), PFunctor.M.dest (f p) = (StepOver.toPFunctor Γ).map f (StepOver.equivObj (process.step p))) : f = process.behavior

Bisimulation by uniqueness. Any function f : process.Proc → Behavior Γ that commutes with the coalgebra structure (i.e., that satisfies the coalgebra-homomorphism diagram for the M-type) agrees with process.behavior on the nose. This is the universal property of M (StepOver.toPFunctor Γ) as the terminal StepOver.toPFunctor Γ-coalgebra.

def Interaction.Concurrent.ProcessOver.ObsEq {Γ : Spec.Node.Context} (process₁ process₂ : ProcessOver Γ) (p₁ : process₁.Proc) (p₂ : process₂.Proc) : Prop

Two residual states (possibly in different processes over the same context) are observationally equivalent when their behavior trees are equal. By behavior_unique, this is the strongest equivalence preserved by every StepOver Γ-coalgebra homomorphism.

theorem Interaction.Concurrent.ProcessOver.ObsEq.refl {Γ : Spec.Node.Context} (process : ProcessOver Γ) (p : process.Proc) : process.ObsEq process p p

Observational equivalence is reflexive (within a fixed process).

theorem Interaction.Concurrent.ProcessOver.ObsEq.symm {Γ : Spec.Node.Context} {process₁ process₂ : ProcessOver Γ} {p₁ : process₁.Proc} {p₂ : process₂.Proc} (h : process₁.ObsEq process₂ p₁ p₂) : process₂.ObsEq process₁ p₂ p₁

Observational equivalence is symmetric.

theorem Interaction.Concurrent.ProcessOver.ObsEq.trans {Γ : Spec.Node.Context} {process₁ process₂ process₃ : ProcessOver Γ} {p₁ : process₁.Proc} {p₂ : process₂.Proc} {p₃ : process₃.Proc} (h₁₂ : process₁.ObsEq process₂ p₁ p₂) (h₂₃ : process₂.ObsEq process₃ p₂ p₃) : process₁.ObsEq process₃ p₁ p₃

Observational equivalence is transitive.

@[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.