Executable step policies for dynamic concurrent processes

This file adds a lightweight policy layer on top of finite executions of Concurrent.ProcessOver.

The point of a policy here is operational rather than semantic in the liveness sense: it describes which concrete step transcripts are allowed to occur in a finite execution. So this layer is useful for expressing scheduler rules, authorization filters, event allowlists, or ticket filters that can be checked step by step.

The closed-world Process API is recovered as a specialization of these generic definitions.

@[reducible, inline]

abbrev Interaction.Concurrent.ProcessOver.StepPolicy {Γ : Spec.Node.Context} (process : ProcessOver Γ) : Type (max u_1 w)

StepPolicy process is an executable constraint on one complete process step.

A policy sees:

• the current residual process state p;
• the concrete sequential transcript tr chosen for the current step protocol process.step p.

It returns true when that step is allowed and false when it is forbidden.

def Interaction.Concurrent.ProcessOver.StepPolicy.top {Γ : Spec.Node.Context} {process : ProcessOver Γ} : process.StepPolicy

The permissive policy that allows every step transcript.

def Interaction.Concurrent.ProcessOver.StepPolicy.inter {Γ : Spec.Node.Context} {process : ProcessOver Γ} (left right : process.StepPolicy) : process.StepPolicy

Conjunction of two step policies. A step is allowed exactly when both component policies allow it.

def Interaction.Concurrent.ProcessOver.StepPolicy.byController {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (allow : Party → Bool) : process.StepPolicy

byController resolve allow constrains only the current controlling party of the concrete step transcript, after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.StepPolicy.byPath {Γ : Spec.Node.Context} {Party : Type u} {process : ProcessOver Γ} (resolve : Spec.Node.ContextHom Γ (StepContext Party)) (allow : List Party → Bool) : process.StepPolicy

byPath resolve allow constrains the full controller path of the concrete step transcript, after projecting the generic context into StepContext.

def Interaction.Concurrent.ProcessOver.StepPolicy.byEvent {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Event : Type w₃} (eventMap : process.EventMap Event) (allow : Event → Bool) : process.StepPolicy

byEvent eventMap allow constrains the stable event label induced by the transcript-level event map eventMap.

def Interaction.Concurrent.ProcessOver.StepPolicy.byTicket {Γ : Spec.Node.Context} {process : ProcessOver Γ} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (allow : Ticket → Bool) : process.StepPolicy

byTicket ticketMap allow constrains the stable ticket attached to each step transcript by ticketMap.

def Interaction.Concurrent.ProcessOver.Trace.respects {Γ : Spec.Node.Context} {process : ProcessOver Γ} (policy : process.StepPolicy) {p : process.Proc} : process.Trace p → Bool

respects policy trace checks whether every step of the finite process execution trace satisfies the executable step policy policy.

@[simp]

theorem Interaction.Concurrent.ProcessOver.Trace.respects_top {Γ : Spec.Node.Context} {process : ProcessOver Γ} {p : process.Proc} (trace : process.Trace p) : respects (fun {p : process.Proc} => StepPolicy.top) trace = true

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy {Party : Type u} (process : Process Party) : Type (max u_1 u_2)

The closed-world specialization of ProcessOver.StepPolicy.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.top {Party : Type u} {process : Process Party} : process.StepPolicy

The permissive closed-world step policy.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.inter {Party : Type u} {process : Process Party} (left right : process.StepPolicy) : process.StepPolicy

Conjunction of closed-world step policies.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.byController {Party : Type u} {process : Process Party} (allow : Party → Bool) : process.StepPolicy

byController allow constrains only the current controlling party of the concrete closed-world step transcript.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.byPath {Party : Type u} {process : Process Party} (allow : List Party → Bool) : process.StepPolicy

byPath allow constrains the full controller path of the concrete closed-world step transcript.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.byEvent {Party : Type u} {process : Process Party} {Event : Type w₃} (eventMap : process.EventMap Event) (allow : Event → Bool) : process.StepPolicy

byEvent eventMap allow constrains the stable event label induced by the transcript-level event map eventMap.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.StepPolicy.byTicket {Party : Type u} {process : Process Party} {Ticket : Type w₃} (ticketMap : process.Tickets Ticket) (allow : Ticket → Bool) : process.StepPolicy

byTicket ticketMap allow constrains the stable ticket attached to each closed-world step transcript by ticketMap.

@[reducible, inline]

abbrev Interaction.Concurrent.Process.Trace.respects {Party : Type u} {process : Process Party} (policy : process.StepPolicy) {p : process.Proc} : process.Trace p → Bool

respects policy trace checks whether every step of the finite closed-world process execution trace satisfies the executable step policy policy.

@[simp]

theorem Interaction.Concurrent.Process.Trace.respects_top {Party : Type u} {process : Process Party} {p : process.Proc} (trace : process.Trace p) : respects (fun {p : process.Proc} => StepPolicy.top) trace = true