Open concurrent processes with boundary traffic

This file defines the semantic bridge between the closed-world concurrent process core (ProcessOver, StepOver) and the open-world layer needed for UC-style composition.

The key idea is simple: a closed concurrent step already records controller paths and local views at each node. An open concurrent step additionally records how each node may receive traffic from, or emit traffic to, an external boundary.

The design follows the layered approach from the UC design notes:

• BoundaryAction Δ X records, at one protocol node with move space X, whether the node is externally activated and what outbound packets the chosen move contributes.
• OpenNodeProfile Party Δ X extends the existing NodeProfile Party X by one BoundaryAction field.
• OpenNodeContext Party Δ is the resulting realized node context.
• OpenProcess Party Δ specializes ProcessOver to that open context.

The closed-world layer is recovered by the canonical forgetful projection OpenNodeContext.forget, which drops the boundary action and retains only the NodeProfile. This means every OpenProcess can be viewed as a plain closed Process by ProcessOver.mapContext.

Boundary actions are structurally mappable along PortBoundary.Hom via BoundaryAction.mapBoundary. The isActivated flag is invariant under boundary adaptation (only emit transforms), which ensures functoriality. The query-level decoding of how input messages determine node moves belongs in the runtime/execution layer, not the structural boundary action.

The emit field is presented as a PFunctor.Trace Δ.Out X (the free-monoid trace on Δ.Out-events indexed by the node's move space X). This makes the structural boundary operations land directly in the generic Trace API: mapBoundary is Trace.mapChart on the output chart, and wireLeft / wireRight are Trace.mapPartial on the appropriate sum projections. The empty-emission default is the trace-monoid unit 1, which is definitionally the constant-[] trace.

structure Interaction.UC.BoundaryAction (Δ : PortBoundary) (X : Type w) : Type w

BoundaryAction Δ X records the boundary traffic associated with one protocol node whose move space is X, against an open boundary Δ.

Fields:

• isActivated flags whether this node is driven by external boundary input (true) or by the internal protocol dynamics (false).
• emit is the PFunctor.Trace Δ.Out X recording, for each chosen move x : X, the finite ordered list of outbound packets contributed on Δ.Out. The default is the monoid unit 1, which is definitionally the constant-[] trace.

The activation flag is a structural marker. The query-level information about how an input message determines the node's move belongs in the runtime/execution layer: charts (used by PortBoundary.Hom) can map packets but cannot map queries, so the structural boundary action records only the fact of activation, not the decoding.

The emit field records only the protocol's own direct output. Runtime-level concerns (buffering, duplication, scheduling, delivery) belong in a separate Runtime layer and are not encoded here.

• isActivated : Bool
• emit : PFunctor.Trace Δ.Out X

def Interaction.UC.BoundaryAction.internal (Δ : PortBoundary) (X : Type w) : BoundaryAction Δ X

A purely internal node: not externally activated and no outbound packets.

def Interaction.UC.BoundaryAction.activated (Δ : PortBoundary) (X : Type w) : BoundaryAction Δ X

A boundary-activated node that emits no outbound packets.

def Interaction.UC.BoundaryAction.outputOnly {Δ : PortBoundary} {X : Type w} (e : PFunctor.Trace Δ.Out X) : BoundaryAction Δ X

An internally driven node that emits outbound packets.

def Interaction.UC.BoundaryAction.mapBoundary {Δ₁ Δ₂ : PortBoundary} {X : Type w} (φ : Δ₁.Hom Δ₂) (b : BoundaryAction Δ₁ X) : BoundaryAction Δ₂ X

Transform a boundary action along a boundary adaptation.

The activation flag is preserved (it does not depend on the boundary presentation). The emitted-trace is pushed forward along the output chart φ.onOut via PFunctor.Trace.mapChart.

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_id {Δ : PortBoundary} {X : Type w} (b : BoundaryAction Δ X) : mapBoundary (PortBoundary.Hom.id Δ) b = b

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_comp {Δ₁ Δ₂ Δ₃ : PortBoundary} {X : Type w} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (b : BoundaryAction Δ₁ X) : mapBoundary g (mapBoundary f b) = mapBoundary (g.comp f) b

def Interaction.UC.BoundaryAction.embedInlTensor {Δ₁ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w} (b : BoundaryAction Δ₁ X) : BoundaryAction (Δ₁.tensor Δ₂) X

Embed a boundary action on the left factor into the tensor boundary.

The trace is pushed forward along the left-injection chart Interface.Hom.inl Δ₁.Out Δ₂.Out via PFunctor.Trace.mapChart. The activation flag is preserved.

def Interaction.UC.BoundaryAction.embedInrTensor (Δ₁ : PortBoundary) {Δ₂ : PortBoundary} {X : Type w} (b : BoundaryAction Δ₂ X) : BoundaryAction (Δ₁.tensor Δ₂) X

Embed a boundary action on the right factor into the tensor boundary.

The trace is pushed forward along the right-injection chart Interface.Hom.inr Δ₁.Out Δ₂.Out via PFunctor.Trace.mapChart. The activation flag is preserved.

def Interaction.UC.BoundaryAction.wireLeft {Δ₁ Γ : PortBoundary} (Δ₂ : PortBoundary) {X : Type w} (b : BoundaryAction (Δ₁.tensor Γ) X) : BoundaryAction (Δ₁.tensor Δ₂) X

Transform a boundary action on tensor Δ₁ Γ into one on tensor Δ₁ Δ₂ by keeping only the left-summand (Δ₁) packets and re-injecting them into the left summand of the combined output. Right-summand (Γ) packets are dropped (they become internal traffic handled by the runtime).

Implemented as PFunctor.Trace.mapPartial on the appropriate index-level partial map.

def Interaction.UC.BoundaryAction.wireRight (Δ₁ : PortBoundary) {Γ Δ₂ : PortBoundary} {X : Type w} (b : BoundaryAction (Γ.swap.tensor Δ₂) X) : BoundaryAction (Δ₁.tensor Δ₂) X

Transform a boundary action on tensor (swap Γ) Δ₂ into one on tensor Δ₁ Δ₂ by keeping only the right-summand (Δ₂) packets and re-injecting them into the right summand of the combined output. Left-summand (swap Γ) packets are dropped (internal traffic).

Implemented as PFunctor.Trace.mapPartial on the appropriate index-level partial map.

def Interaction.UC.BoundaryAction.closed {Δ : PortBoundary} {X : Type w} (b : BoundaryAction Δ X) : BoundaryAction PortBoundary.empty X

Close a boundary action by dropping all external traffic.

The result lives on PortBoundary.empty and has no activation or emission. This is used by plug to internalize all boundary interactions. The emitted-trace is the monoid unit 1, which is definitionally the constant-[] trace.

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_embedInlTensor {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} {X : Type w} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (b : BoundaryAction Δ₁ X) : mapBoundary (f₁.tensor f₂) (embedInlTensor Δ₂ b) = embedInlTensor Δ₂' (mapBoundary f₁ b)

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_embedInrTensor {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} {X : Type w} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (b : BoundaryAction Δ₂ X) : mapBoundary (f₁.tensor f₂) (embedInrTensor Δ₁ b) = embedInrTensor Δ₁' (mapBoundary f₂ b)

@[simp]

theorem Interaction.UC.BoundaryAction.closed_mapBoundary {Δ₁ Δ₂ : PortBoundary} {X : Type w} (φ : Δ₁.Hom Δ₂) (b : BoundaryAction Δ₁ X) : (mapBoundary φ b).closed = b.closed

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_wireLeft {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} {X : Type w} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (b : BoundaryAction (Δ₁.tensor Γ) X) : mapBoundary (f₁.tensor f₂) (wireLeft Δ₂ b) = wireLeft Δ₂' (mapBoundary (f₁.tensor (PortBoundary.Hom.id Γ)) b)

@[simp]

theorem Interaction.UC.BoundaryAction.mapBoundary_wireRight {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} {X : Type w} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') (b : BoundaryAction (Γ.swap.tensor Δ₂) X) : mapBoundary (f₁.tensor f₂) (wireRight Δ₁ b) = wireRight Δ₁' (mapBoundary ((PortBoundary.Hom.id Γ.swap).tensor f₂) b)

structure Interaction.UC.OpenNodeProfile (Party : Type u) (Δ : PortBoundary) (X : Type w) extends Interaction.Concurrent.NodeProfile Party X : Type (max u (w + 1))

OpenNodeProfile Party Δ X extends NodeProfile Party X with one BoundaryAction Δ X recording the node's interaction with an external boundary.

This is the per-node data that distinguishes an open process from a closed one: the closed part (controllers, views) describes internal control and observation, while boundary describes the node's interface with the outside world.

• controllers : X → List Party
• views : Party → Multiparty.ViewMode X
• boundary : BoundaryAction Δ X

def Interaction.UC.OpenNodeProfile.ofClosed {Party : Type u} {Δ : PortBoundary} {X : Type w} (ns : Concurrent.NodeProfile Party X) : OpenNodeProfile Party Δ X

Build an OpenNodeProfile from a closed NodeProfile by marking the node as purely internal (no boundary traffic).

def Interaction.UC.OpenNodeProfile.mapBoundary {Party : Type u} {Δ₁ Δ₂ : PortBoundary} {X : Type w} (φ : Δ₁.Hom Δ₂) (ons : OpenNodeProfile Party Δ₁ X) : OpenNodeProfile Party Δ₂ X

Transform the boundary action of an open node profile along a boundary adaptation, preserving the closed-world node profile.

@[simp]

theorem Interaction.UC.OpenNodeProfile.mapBoundary_id {Party : Type u} {Δ : PortBoundary} {X : Type w} (ons : OpenNodeProfile Party Δ X) : mapBoundary (PortBoundary.Hom.id Δ) ons = ons

@[simp]

theorem Interaction.UC.OpenNodeProfile.mapBoundary_comp {Party : Type u} {Δ₁ Δ₂ Δ₃ : PortBoundary} {X : Type w} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) (ons : OpenNodeProfile Party Δ₁ X) : mapBoundary g (mapBoundary f ons) = mapBoundary (g.comp f) ons

@[reducible, inline]

abbrev Interaction.UC.OpenNodeContext (Party : Type u) (Δ : PortBoundary) (X : Type w) : Type (max u (w + 1))

The open-world node context for processes with boundary Δ.

At a node with move space X, the context value is OpenNodeProfile Party Δ X: the usual controller-path and local-view data, plus a BoundaryAction describing the node's external traffic.

Polynomial reading

OpenNodeContext Party Δ is, up to the named-field-vs-pair identification exhibited by OpenNodeContext.equivProductView, the non-dependent context product

Spec.Node.Context.prod (StepContext Party) (fun X => BoundaryAction Δ X)

That is, the open node context is the polynomial product of the closed StepContext Party and the boundary-action context fun X => BoundaryAction Δ X, with both factors carried independently at each move space X. The hand-rolled context-homs below (forget, embed, map, inlTensor, inrTensor, wireLeft, wireRight, close) are concrete instances of the universal projection / pairing maps for this product, specialized to the particular boundary-action transformations they perform. The structure form OpenNodeProfile extends NodeProfile is preserved as the working API because it gives clean { toNodeProfile := ..., boundary := ... } construction sites and definitional projections used pervasively below.

Polynomial-product bridge

Exhibit OpenNodeContext Party Δ as the non-dependent polynomial product of the closed StepContext Party and the boundary-action context, and prove that the bridge is a definitional isomorphism (round trips reduce to rfl by Prod.mk.eta and structure eta). The product view lets one phrase universal-property arguments without repeatedly pattern-matching on OpenNodeProfile literals; the structural API below is the working form.

@[reducible, inline]

abbrev Interaction.UC.OpenNodeContext.productView (Party : Type u) (Δ : PortBoundary) : Spec.Node.Context

The polynomial-product view of OpenNodeContext. Lives in the same universes as OpenNodeContext Party Δ itself: the first universe is the move-space universe w, and the second is whatever Lean infers for NodeProfile Party X × BoundaryAction Δ X.

def Interaction.UC.OpenNodeContext.toProductView (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party Δ) (productView Party Δ)

Forward direction of the polynomial-product bridge: read off the (NodeProfile, BoundaryAction) pair from an OpenNodeProfile.

def Interaction.UC.OpenNodeContext.ofProductView (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (productView Party Δ) (OpenNodeContext Party Δ)

Inverse direction of the polynomial-product bridge: reassemble an OpenNodeProfile from a (NodeProfile, BoundaryAction) pair.

@[simp]

theorem Interaction.UC.OpenNodeContext.toProductView_ofProductView (Party : Type u) (Δ : PortBoundary) : (toProductView Party Δ).comp (ofProductView Party Δ) = Spec.Node.ContextHom.id (productView Party Δ)

@[simp]

theorem Interaction.UC.OpenNodeContext.ofProductView_toProductView (Party : Type u) (Δ : PortBoundary) : (ofProductView Party Δ).comp (toProductView Party Δ) = Spec.Node.ContextHom.id (OpenNodeContext Party Δ)

def Interaction.UC.OpenNodeContext.forget (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party Δ) (Concurrent.StepContext Party)

The forgetful map from the open-world context to the closed-world context.

This drops the BoundaryAction and retains only the NodeProfile (controllers and local views).

def Interaction.UC.OpenNodeContext.embed (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (Concurrent.StepContext Party) (OpenNodeContext Party Δ)

The embedding from the closed-world context into the open-world context.

This marks every node as purely internal (no boundary traffic).

def Interaction.UC.OpenNodeContext.map (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) : Spec.Node.ContextHom (OpenNodeContext Party Δ₁) (OpenNodeContext Party Δ₂)

The context hom induced by a boundary adaptation.

This transforms every node's boundary action along φ while preserving the closed-world node semantics.

@[simp]

theorem Interaction.UC.OpenNodeContext.map_id (Party : Type u) (Δ : PortBoundary) : map Party (PortBoundary.Hom.id Δ) = Spec.Node.ContextHom.id (OpenNodeContext Party Δ)

theorem Interaction.UC.OpenNodeContext.map_comp (Party : Type u) {Δ₁ Δ₂ Δ₃ : PortBoundary} (g : Δ₂.Hom Δ₃) (f : Δ₁.Hom Δ₂) : (map Party g).comp (map Party f) = map Party (g.comp f)

def Interaction.UC.OpenNodeContext.inlTensor (Party : Type u) (Δ₁ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party Δ₁) (OpenNodeContext Party (Δ₁.tensor Δ₂))

Embed the left factor's open-world context into the tensor boundary context.

This injects emitted packets into the left summand of the combined output interface while preserving the closed-world node semantics.

def Interaction.UC.OpenNodeContext.inrTensor (Party : Type u) (Δ₁ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party Δ₂) (OpenNodeContext Party (Δ₁.tensor Δ₂))

Embed the right factor's open-world context into the tensor boundary context.

This injects emitted packets into the right summand of the combined output interface while preserving the closed-world node semantics.

def Interaction.UC.OpenNodeContext.wireLeft (Party : Type u) (Δ₁ Γ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party (Δ₁.tensor Γ)) (OpenNodeContext Party (Δ₁.tensor Δ₂))

Wire the left factor: transform OpenNodeContext Party (tensor Δ₁ Γ) into OpenNodeContext Party (tensor Δ₁ Δ₂) by filtering out internal (Γ) packets and keeping only external (Δ₁) packets.

def Interaction.UC.OpenNodeContext.wireRight (Party : Type u) (Δ₁ Γ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party (Γ.swap.tensor Δ₂)) (OpenNodeContext Party (Δ₁.tensor Δ₂))

Wire the right factor: transform OpenNodeContext Party (tensor (swap Γ) Δ₂) into OpenNodeContext Party (tensor Δ₁ Δ₂) by filtering out internal (swap Γ) packets and keeping only external (Δ₂) packets.

def Interaction.UC.OpenNodeContext.close (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (OpenNodeContext Party Δ) (OpenNodeContext Party PortBoundary.empty)

Close the boundary: transform OpenNodeContext Party Δ into OpenNodeContext Party empty by dropping all boundary traffic. Used by plug to internalize all external interactions.

theorem Interaction.UC.OpenNodeContext.map_tensor_comp_inlTensor (Party : Type u) {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') : (map Party (f₁.tensor f₂)).comp (inlTensor Party Δ₁ Δ₂) = (inlTensor Party Δ₁' Δ₂').comp (map Party f₁)

theorem Interaction.UC.OpenNodeContext.map_tensor_comp_inrTensor (Party : Type u) {Δ₁ Δ₁' Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') : (map Party (f₁.tensor f₂)).comp (inrTensor Party Δ₁ Δ₂) = (inrTensor Party Δ₁' Δ₂').comp (map Party f₂)

theorem Interaction.UC.OpenNodeContext.close_comp_map (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) : (close Party Δ₂).comp (map Party φ) = close Party Δ₁

theorem Interaction.UC.OpenNodeContext.map_tensor_comp_wireLeft (Party : Type u) {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') : (map Party (f₁.tensor f₂)).comp (wireLeft Party Δ₁ Γ Δ₂) = (wireLeft Party Δ₁' Γ Δ₂').comp (map Party (f₁.tensor (PortBoundary.Hom.id Γ)))

theorem Interaction.UC.OpenNodeContext.map_tensor_comp_wireRight (Party : Type u) {Δ₁ Δ₁' Γ Δ₂ Δ₂' : PortBoundary} (f₁ : Δ₁.Hom Δ₁') (f₂ : Δ₂.Hom Δ₂') : (map Party (f₁.tensor f₂)).comp (wireRight Party Δ₁ Γ Δ₂) = (wireRight Party Δ₁' Γ Δ₂').comp (map Party ((PortBoundary.Hom.id Γ.swap).tensor f₂))

Existing context-homs as polynomial-product operations

The following identities exhibit the hand-rolled OpenNodeContext context-homs above as concrete instances of the universal projections, pairing maps, and product maps for the polynomial product productView. They are documentation rather than a refactor: the named API forms remain the working surface, and the equalities below let one switch between the two presentations on demand.

theorem Interaction.UC.OpenNodeContext.forget_eq_prodFst_comp_toProductView (Party : Type u) (Δ : PortBoundary) : forget Party Δ = (Spec.Node.Context.prodFst (Concurrent.StepContext Party) fun (X : Type w) => BoundaryAction Δ X).comp (toProductView Party Δ)

forget is the first projection of the polynomial product, postcomposed with the bridge toProductView.

theorem Interaction.UC.OpenNodeContext.embed_eq_ofProductView_comp_prodPair (Party : Type u) (Δ : PortBoundary) : embed Party Δ = (ofProductView Party Δ).comp (Spec.Node.Context.prodPair (Spec.Node.ContextHom.id (Concurrent.StepContext Party)) fun (X : Type w) (x : Concurrent.StepContext Party X) => BoundaryAction.internal Δ X)

embed is the pairing of the identity on StepContext with the constant internal boundary action, transported back along the bridge.

theorem Interaction.UC.OpenNodeContext.map_eq_ofProductView_comp_prodMap_comp_toProductView (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) : map Party φ = ((ofProductView Party Δ₂).comp (Spec.Node.Context.prodMap (Spec.Node.ContextHom.id (Concurrent.StepContext Party)) fun (X : Type w) (b : BoundaryAction Δ₁ X) => BoundaryAction.mapBoundary φ b)).comp (toProductView Party Δ₁)

map φ factors as the polynomial-product map of the identity on StepContext and the boundary-action transport fun X => BoundaryAction.mapBoundary φ.

@[reducible, inline]

abbrev Interaction.UC.OpenStep (Party : Type u) (Δ : PortBoundary) (P : Type v) : Type (max (max v 1) 1 u)

The open-world specialization of StepOver.

Here the node context carries OpenNodeProfile Party Δ, so every node records both the usual controller/view data and its boundary traffic against Δ.

structure Interaction.UC.OpenProcess (m : Type w → Type w') (Party : Type u) (Δ : PortBoundary) : Type (max (max (max u (v + 1)) (w + 1)) w')

An m-parametric open concurrent process exposing boundary Δ.

OpenProcess m Party Δ bundles:

• Proc — the residual state space of the process;
• step — for each state, the protocol step observed by the open world (move-tree spec, node-local semantics, and continuation next);
• stepSampler — a per-state Spec.Sampler m (step s).spec resolving each move of the step protocol in the intermediate monad m.

Each state of an open process carries its own nodewise-monadic sampler as first-class data. openTheory m compositionally assembles the per-step samplers of composite processes through par, wire, and plug via Spec.Sampler.interleave, and the runtime layer (processSemantics, processSemanticsAsync) reads the sampler off the process rather than taking it as a separate argument.

Universe conventions

The spec / move-type universe is pinned at 0 because m : Type → Type only operates on Type and the Sampler m spec abbrev therefore requires spec : Spec.{0}. The Party universe u and the state universe v remain free.

Recovering the structural layer

op.toProcess : ProcessOver ... projects onto the underlying ProcessOver, feeding the structural lemmas in Concurrent/Process.lean and the bisimulation infrastructure below.

• Proc : Type v

  Residual state space of the process.

• step : self.Proc → Concurrent.StepOver (OpenNodeContext Party Δ) self.Proc

  Protocol step observed at state s.

• stepSampler (s : self.Proc) : Spec.Sampler m (self.step s).spec

  Per-state nodewise-monadic sampler that resolves each move of the step protocol in the intermediate monad m.

@[reducible]

def Interaction.UC.OpenProcess.toProcess {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (op : OpenProcess m Party Δ) : Concurrent.ProcessOver (OpenNodeContext Party Δ)

Structural projection onto the underlying ProcessOver, dropping the per-state sampler. The closed-world ProcessOver lemmas from Concurrent/Process.lean apply through this projection.

def Interaction.UC.OpenProcess.toClosed {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (op : OpenProcess m Party Δ) : Concurrent.Process Party

Forget the boundary layer and view an open process as a plain closed-world process.

This is the canonical projection: it drops all BoundaryAction data from every node while preserving the process structure, controller paths, and local views. The sampler is also discarded, so the result is a bare ProcessOver over the closed-world context.

def Interaction.UC.OpenProcess.ofClosed {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (p : Concurrent.Process Party) (sampler : (s : p.Proc) → Spec.Sampler m (p.step s).spec) : OpenProcess m Party Δ

Embed a closed-world process as an open process with no boundary traffic, using a user-supplied per-state sampler.

Every node is marked as purely internal: isActivated = false and emit produces no packets. The caller must supply the nodewise sampler because the closed-world process carries no monadic information.

def Interaction.UC.OpenProcess.mapBoundary {m : Type w → Type w'} {Party : Type u} {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) (op : OpenProcess m Party Δ₁) : OpenProcess m Party Δ₂

Adapt the exposed boundary of an open process along a structural boundary morphism.

This transforms every node's boundary action along φ (translating emitted packets, preserving activation flags) while leaving the process structure, closed-world node semantics, and per-step samplers unchanged. The sampler carries over verbatim because StepOver.mapContext preserves step.spec.

def Interaction.UC.OpenProcess.interleave {m : Type w → Type w'} {Party : Type u} {Δ₁ Δ₂ Δ : PortBoundary} (p₁ : OpenProcess m Party Δ₁) (p₂ : OpenProcess m Party Δ₂) (f₁ : Spec.Node.ContextHom (OpenNodeContext Party Δ₁) (OpenNodeContext Party Δ)) (f₂ : Spec.Node.ContextHom (OpenNodeContext Party Δ₂) (OpenNodeContext Party Δ)) (schedulerCtx : OpenNodeContext Party Δ (ULift.{w, 0} Bool)) (schedulerSampler : m (ULift.{w, 0} Bool)) : OpenProcess m Party Δ

Binary-choice interleaving of two open processes, targeting a common boundary Δ via structural injections f₁, f₂ and a scheduling node context schedulerCtx : OpenNodeContext Party Δ (ULift Bool).

Structure on Proc and step is delegated to the underlying Concurrent.ProcessOver.interleave; the per-state sampler is assembled by Spec.Sampler.interleave, which threads the scheduler sampler schedulerSampler : m (ULift Bool) above the per-branch samplers so that the resulting step carries a well-typed nodewise-monadic sampler.

This is the single ingredient shared by openTheory.par, openTheory.wire, and openTheory.plug: those operations differ only in which injection pair f₁, f₂ they supply.

@[reducible, inline]

abbrev Interaction.UC.OpenProcess.System (Party : Type u) (Δ : PortBoundary) : Type (max (max (u_1 + 1) (w + 1)) u (w + 1))

OpenProcess.System augments an open process by the standard verification predicates used throughout VCVio. The verification predicates are about the structural ProcessOver layer, so OpenProcess.System is monad- and sampler-agnostic and refers to the underlying ProcessOver.System.

Silent steps and weak bisimulation

def Interaction.UC.IsSilentDecoration {Party : Type u} {Δ : PortBoundary} {spec : Spec} : Spec.Decoration (OpenNodeContext Party Δ) spec → spec.Transcript → Prop

A transcript path through a decorated open-process spec is silent when every visited node is not externally activated (isActivated = false). Checking only isActivated (rather than also requiring emit x = []) ensures the predicate is invariant under all context morphisms, including wireLeft / wireRight which filter shared-boundary packets via List.filterMap.

def Interaction.UC.IsSilentStep {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (p : OpenProcess m Party Δ) (s : p.Proc) (tr : (p.step s).spec.Transcript) : Prop

A complete step of an open process is silent when every node along the chosen transcript path has boundary-internal semantics.

theorem Interaction.UC.isSilentDecoration_iff_map {Party : Type u} {Δ₁ Δ₂ : PortBoundary} (f : Spec.Node.ContextHom (OpenNodeContext Party Δ₁) (OpenNodeContext Party Δ₂)) (hAct : ∀ (X : Type w) (ons : OpenNodeContext Party Δ₁ X), (f X ons).boundary.isActivated = ons.boundary.isActivated) {spec : Spec} (d : Spec.Decoration (OpenNodeContext Party Δ₁) spec) (tr : spec.Transcript) : IsSilentDecoration (Spec.Decoration.map f spec d) tr ↔ IsSilentDecoration d tr

IsSilentDecoration is invariant under context morphisms that preserve isActivated. All morphisms in the open-process framework (including mapBoundary, embedInlTensor, embedInrTensor, wireLeft, wireRight, and closed) preserve isActivated.

theorem Interaction.UC.isSilentStep_mapBoundary_iff {m : Type w → Type w'} {Party : Type u} {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) (p : OpenProcess m Party Δ₁) (s : p.Proc) (tr : (p.step s).spec.Transcript) : IsSilentStep (OpenProcess.mapBoundary φ p) s tr ↔ IsSilentStep p s tr

IsSilentStep is invariant under OpenProcess.mapBoundary: remapping the boundary does not change which transcripts are silent, because all boundary maps preserve isActivated.

OpenProcessIso: weak bisimulation equivalence for open processes

def Interaction.UC.OpenProcessIso {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (p₁ p₂ : OpenProcess m Party Δ) : Prop

Two open processes with the same boundary are weakly bisimilar when there exists a relation on their state types satisfying:

1. Totality / surjectivity: every state on each side has a related partner.
2. Silent forward/backward: a silent step can either be matched by some step on the other side (maintaining the relation), or absorbed (the other side stays put and the relation is maintained with the successor).
3. Visible forward/backward: a visible (non-silent) step must be matched by a visible step on the other side that preserves the relation.

This is the appropriate equality notion for openTheory monoidal laws, where the internal scheduler structure differs (e.g., left-nested vs. right-nested interleaving) but the observable boundary traffic is the same. The scheduler nodes introduced by ProcessOver.interleave are always silent, so they can be absorbed by the weak bisimulation.

theorem Interaction.UC.OpenProcessIso.refl {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} (p : OpenProcess m Party Δ) : OpenProcessIso p p

Every open process is weakly bisimilar to itself.

theorem Interaction.UC.OpenProcessIso.symm {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} {p₁ p₂ : OpenProcess m Party Δ} (h : OpenProcessIso p₁ p₂) : OpenProcessIso p₂ p₁

Weak bisimilarity is symmetric.

theorem Interaction.UC.OpenProcessIso.trans {m : Type w → Type w'} {Party : Type u} {Δ : PortBoundary} {p₁ p₂ p₃ : OpenProcess m Party Δ} (h₁₂ : OpenProcessIso p₁ p₂) (h₂₃ : OpenProcessIso p₂ p₃) : OpenProcessIso p₁ p₃

Weak bisimilarity is transitive. The composite relation witnesses p₂ as an intermediate: ∃ s₂, r₁₂ s₁ s₂ ∧ r₂₃ s₂ s₃. For silent steps, the intermediate state can advance or stay, using Classical.em to case-split on whether the intermediate step is itself silent.