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.
• OpenNodeSemantics Party Δ X extends the existing NodeSemantics Party X by one BoundaryAction field.
• OpenStepContext 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 openStepContextForget, which drops the boundary action and retains only the NodeSemantics. 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.

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 maps each chosen move to the list of outbound packets it contributes on Δ.Out.

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 : X → List Δ.Out.Packet

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 : X → List Δ.Out.Packet) : 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 packets are translated forward along φ.onOut.

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

Emitted packets are injected into the left summand of the combined output interface. 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.

Emitted packets are injected into the right summand of the combined output interface. 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).

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

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.

@[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.OpenNodeSemantics (Party : Type u) (Δ : PortBoundary) (X : Type w) extends Interaction.Concurrent.NodeSemantics Party X : Type (max u (w + 1))

OpenNodeSemantics Party Δ X extends NodeSemantics 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.LocalView X
• boundary : BoundaryAction Δ X

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

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

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

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

@[simp]

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

@[simp]

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

@[reducible, inline]

abbrev Interaction.UC.OpenStepContext (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 OpenNodeSemantics Party Δ X: the usual controller-path and local-view data, plus a BoundaryAction describing the node's external traffic.

def Interaction.UC.OpenStepContext.forget (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (OpenStepContext 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 NodeSemantics (controllers and local views).

def Interaction.UC.OpenStepContext.embed (Party : Type u) (Δ : PortBoundary) : Spec.Node.ContextHom (Concurrent.StepContext Party) (OpenStepContext 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.OpenStepContext.map (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) : Spec.Node.ContextHom (OpenStepContext Party Δ₁) (OpenStepContext 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.OpenStepContext.map_id (Party : Type u) (Δ : PortBoundary) : map Party (PortBoundary.Hom.id Δ) = Spec.Node.ContextHom.id (OpenStepContext Party Δ)

theorem Interaction.UC.OpenStepContext.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.OpenStepContext.inlTensor (Party : Type u) (Δ₁ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenStepContext Party Δ₁) (OpenStepContext 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.OpenStepContext.inrTensor (Party : Type u) (Δ₁ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenStepContext Party Δ₂) (OpenStepContext 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.OpenStepContext.wireLeft (Party : Type u) (Δ₁ Γ Δ₂ : PortBoundary) : Spec.Node.ContextHom (OpenStepContext Party (Δ₁.tensor Γ)) (OpenStepContext Party (Δ₁.tensor Δ₂))

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

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

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

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

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

theorem Interaction.UC.OpenStepContext.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.OpenStepContext.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.OpenStepContext.close_comp_map (Party : Type u) {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) : (close Party Δ₂).comp (map Party φ) = close Party Δ₁

theorem Interaction.UC.OpenStepContext.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.OpenStepContext.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₂))

@[reducible, inline]

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

The open-world specialization of StepOver.

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

@[reducible, inline]

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

The open-world specialization of ProcessOver.

An OpenProcess Party Δ is a continuation-based process whose steps are decorated by OpenNodeSemantics Party Δ. It exposes the directed boundary Δ to an external context.

The closed-world Process Party is recovered by ProcessOver.mapContext (OpenStepContext.forget Party Δ).

def Interaction.UC.OpenProcess.toClosed {Party : Type u} {Δ : PortBoundary} (op : OpenProcess 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.

def Interaction.UC.OpenProcess.ofClosed {Party : Type u} {Δ : PortBoundary} (p : Concurrent.Process Party) : OpenProcess Party Δ

Embed a closed-world process as an open process with no boundary traffic.

Every node is marked as purely internal: isActivated = false and emit produces no packets.

def Interaction.UC.OpenProcess.mapBoundary {Party : Type u} {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) (op : OpenProcess Party Δ₁) : OpenProcess 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 and closed-world node semantics unchanged.

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

def Interaction.UC.IsSilentDecoration {Party : Type u} {Δ : PortBoundary} {spec : Spec} : Spec.Decoration (OpenStepContext 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 {Party : Type u} {Δ : PortBoundary} (p : OpenProcess 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 (OpenStepContext Party Δ₁) (OpenStepContext Party Δ₂)) (hAct : ∀ (X : Type w) (ons : OpenStepContext Party Δ₁ X), (f X ons).boundary.isActivated = ons.boundary.isActivated) {spec : Spec} (d : Spec.Decoration (OpenStepContext 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 {Party : Type u} {Δ₁ Δ₂ : PortBoundary} (φ : Δ₁.Hom Δ₂) (p : OpenProcess 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.

def Interaction.UC.OpenProcessIso {Party : Type u} {Δ : PortBoundary} (p₁ p₂ : OpenProcess 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 {Party : Type u} {Δ : PortBoundary} (p : OpenProcess Party Δ) : OpenProcessIso p p

Every open process is weakly bisimilar to itself.

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

Weak bisimilarity is symmetric.

theorem Interaction.UC.OpenProcessIso.trans {Party : Type u} {Δ : PortBoundary} {p₁ p₂ p₃ : OpenProcess 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.