State-indexed concurrent machines

This file provides the flat, transition-system presentation of the concurrent interaction framework.

The semantic center of the library is Concurrent.Process: a residual process state exposes one sequential interaction step, and completing that step yields the next residual state. That continuation-based view is convenient when the shape of the current interaction matters.

Many protocol designers, however, start from a more operational picture:

• there is an explicit global state σ,
• a family Enabled σ of events that may happen next, and
• a function describing the successor state after such an event.

Machine packages exactly that presentation. It is intentionally small, and then layered enrichments add stable event labels, fairness tickets, and system predicates. The key bridge is Machine.toProcess, which interprets each enabled event set as a one-node sequential step and thereby embeds machine semantics into the general Concurrent.Process core.

This is the natural frontend for transition-system style models, including state-heavy distributed and cryptographic protocol semantics.

structure Interaction.Concurrent.Machine : Type (max (u + 1) (v + 1))

Machine is the minimal state-indexed presentation of a concurrent system.

At any residual state σ, the type Enabled σ describes the events that may occur next, and step σ e records the successor state produced by choosing the enabled event e.

This record intentionally contains only dynamics. Event labels, fairness tickets, controller ownership, local views, and verification predicates are all added in separate layers so that the core transition semantics stays small and reusable.

• State : Type v
• Enabled : self.State → Type u
• step (σ : self.State) : self.Enabled σ → self.State

def Interaction.Concurrent.Machine.StepFun : Type v → Type (max (u + 1) v)

The step functor for Machine: at a state, the machine exposes an event type E together with a successor-state function E → S.

@[implicit_reducible]

instance Interaction.Concurrent.Machine.instFunctorStepFun : Functor StepFun

instance Interaction.Concurrent.Machine.instLawfulFunctorStepFun : LawfulFunctor StepFun

@[implicit_reducible]

instance Interaction.Concurrent.Machine.instCoalgStepFunState (m : Machine) : Coalg StepFun m.State

Every Machine is an F-coalgebra for Machine.StepFun.

@[reducible, inline]

abbrev Interaction.Concurrent.Machine.EventMap (machine : Machine) (Event : Type u) : Type (max (max u u_2) u_1)

EventMap assigns a stable external label to each enabled machine event.

These labels are the observable step descriptions that one typically wants to preserve under refinement, compare across runs, or expose in user-facing trace statements.

@[reducible, inline]

abbrev Interaction.Concurrent.Machine.Tickets (machine : Machine) (Ticket : Type u) : Type (max (max u u_2) u_1)

Tickets assigns a stable obligation identifier to each enabled machine event.

Unlike the raw event itself, a ticket is meant to persist across different representations of the same scheduling obligation, so later fairness and liveness layers quantify over tickets rather than over the concrete event type of one particular state.

structure Interaction.Concurrent.Machine.Labeled : Type (u + 1)

Machine.Labeled packages a machine together with its chosen event-label map.

This is the smallest bundle that supports statements about observable event traces without committing to fairness or safety metadata.

• toMachine : Machine
• Event : Type u
• event : self.toMachine.EventMap self.Event

structure Interaction.Concurrent.Machine.Ticketed : Type (u + 1)

Machine.Ticketed packages a machine together with stable tickets for its enabled events.

This is the machine-side entry point for fairness and liveness statements.

• toMachine : Machine
• Ticket : Type u
• ticket : self.toMachine.Tickets self.Ticket

structure Interaction.Concurrent.Machine.Systemextends Interaction.Concurrent.Machine : Type (max (u_1 + 1) (u_2 + 1))

Machine.System augments a machine by the standard verification predicates used throughout VCVio: initial states, ambient assumptions, safety, and invariants.

These predicates are orthogonal to the step relation itself, so they are kept out of Machine and bundled only when one wants verification-oriented statements about the machine.

• State : Type u_1
• Enabled : self.State → Type u_2
• step (σ : self.State) : self.Enabled σ → self.State
• init : self.State → Prop
• assumptions : self.State → Prop
• safe : self.State → Prop
• inv : self.State → Prop

def Interaction.Concurrent.Machine.toProcess {Party : Type u} (machine : Machine) (semantics : (σ : machine.State) → NodeSemantics Party (machine.Enabled σ)) : Process Party

Compile a flat state-indexed machine into the continuation-based Concurrent.Process core.

At each machine state σ, the current enabled event type Enabled σ is turned into a one-node sequential interaction step. The supplied semantics equips that node with controller and local-view information, so the result is not just an operational embedding of the state transition relation, but a full process step inside the richer interaction semantics.

Machine.toProcess is therefore the canonical bridge from transition-system models to the more general process-centered concurrent layer.

def Interaction.Concurrent.Machine.System.toProcess {Party : Type u} (system : System) (semantics : (σ : system.State) → NodeSemantics Party (system.Enabled σ)) : Process.System Party

Lift Machine.toProcess from bare dynamics to the verification-oriented Process.System layer by reusing the same initial, assumption, safety, and invariant predicates.