Concurrent interaction examples

This file gives small definitional examples for the current concurrent layer.

The examples are intentionally focused on:

• binary structural parallelism;
• frontier events and residuals;
• per-party observation profiles over concurrently live components.
• scheduler ownership versus atomic payload ownership;
• the combined current local view of the next frontier event.
• process executions, controller paths, and observed local traces.
• interleaving equivalence under commuting independent steps.
• executable scheduler and controller policies over finite traces.

They are meant to exercise the current expressivity surface before later layers such as fairness or richer execution semantics are added.

inductive Interaction.Concurrent.Examples.Party : Type

Three parties for the toy concurrent examples: two honest parties and a network adversary.

• alice : Party
• bob : Party
• adv : Party

@[implicit_reducible]

instance Interaction.Concurrent.Examples.instDecidableEqParty : DecidableEq Party

def Interaction.Concurrent.Examples.delivery : Spec

One atomic message-delivery step whose payload is a pair of a public header and a private payload bit.

def Interaction.Concurrent.Examples.deliveryProfile : Profile Party delivery

A profile where Alice originates the payload, Bob sees the whole message, and the adversary sees only the public header.

def Interaction.Concurrent.Examples.ack : Spec

A second atomic node that only Bob fully observes, while the adversary learns nothing.

def Interaction.Concurrent.Examples.ackProfile : Profile Party ack

Local observations for the acknowledgement node.

def Interaction.Concurrent.Examples.inFlight : Spec

A concurrent system where delivery and acknowledgement are both live.

def Interaction.Concurrent.Examples.inFlightProfile : Profile Party inFlight

The corresponding concurrent observation profile.

def Interaction.Concurrent.Examples.deliveryControl : Control Party delivery

Control ownership for the delivery step: Alice chooses the payload.

def Interaction.Concurrent.Examples.ackControl : Control Party ack

Control ownership for the acknowledgement step: Bob chooses the bit.

def Interaction.Concurrent.Examples.inFlightControl : Control Party inFlight

The adversary controls scheduling between the two concurrently live subsystems, while Alice and Bob still control their respective atomic nodes.

def Interaction.Concurrent.Examples.afterDelivery : Control Party (Spec.done.par ack)

def Interaction.Concurrent.Examples.afterDeliveryProfile : Profile Party (Spec.done.par ack)

def Interaction.Concurrent.Examples.deliveryThenAck : Trace inFlight

A concrete structural trace where the adversary schedules delivery first and the remaining acknowledgement second.

def Interaction.Concurrent.Examples.inFlightProcess : Process Party

The dynamic process compiled from the structural tree frontend.

def Interaction.Concurrent.Examples.inFlightState : Tree.State Party

The packaged initial structural state of the in-flight system.

def Interaction.Concurrent.Examples.deliveryThenAckExec : inFlightProcess.Trace inFlightState

The process execution induced by deliveryThenAck.

def Interaction.Concurrent.Examples.afterDeliveryState : Tree.State Party

def Interaction.Concurrent.Examples.ackThenDelivery : Trace inFlight

A concrete structural trace where the adversary schedules the acknowledgement before the delivery event.

def Interaction.Concurrent.Examples.afterAck : Control Party (delivery.par Spec.done)

def Interaction.Concurrent.Examples.afterAckProfile : Profile Party (delivery.par Spec.done)

def Interaction.Concurrent.Examples.ackThenDeliveryExec : inFlightProcess.Trace inFlightState

The process execution induced by ackThenDelivery.

def Interaction.Concurrent.Examples.afterAckState : Tree.State Party

def Interaction.Concurrent.Examples.deliveryEvent : Front inFlight

def Interaction.Concurrent.Examples.ackEvent : Front inFlight

def Interaction.Concurrent.Examples.leftThenRight : Trace inFlight

def Interaction.Concurrent.Examples.rightThenLeft : Trace inFlight

def Interaction.Concurrent.Examples.preferLeft : inFlightProcess.StepPolicy

When both sides of a live par are available, prefer the left branch.

def Interaction.Concurrent.Examples.preferRight : inFlightProcess.StepPolicy

When both sides of a live par are available, prefer the right branch.

def Interaction.Concurrent.Examples.threeWay : Spec

A three-way concurrent system used to illustrate recursive independence inside one branch of a larger parallel spec.

def Interaction.Concurrent.Examples.loopNode : NodeSemantics Party Bool

Node semantics for a tiny looping process: the adversary actively chooses the boolean step, Bob observes it, and Alice is hidden from it.

def Interaction.Concurrent.Examples.loopProcess : Process Party

A tiny one-state looping process used to exercise runs, tickets, fairness, and refinement.

def Interaction.Concurrent.Examples.loopTicketed : Process.Ticketed Party

A ticketed view of loopProcess using the chosen boolean as the stable ticket.

def Interaction.Concurrent.Examples.trueRun : loopProcess.Run

A simple always-true infinite run of loopProcess.

def Interaction.Concurrent.Examples.loopSystem : Process.System Party

A trivial system wrapper around loopProcess.

def Interaction.Concurrent.Examples.loopSim : Refinement.ForwardSimulation loopSystem loopSystem fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byTicket loopTicketed.ticket loopTicketed.ticket

The identity simulation on loopSystem, preserving the boolean ticket.

noncomputable def Interaction.Concurrent.Examples.loopMappedRun : Process.Run loopSystem.toProcess

The specification-side run obtained by matching trueRun through loopSim.

def Interaction.Concurrent.Examples.loopObsSimBob : Refinement.ForwardSimulation loopSystem loopSystem fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byObservation Party.bob

The identity simulation on loopSystem, preserving Bob's local observations.

noncomputable def Interaction.Concurrent.Examples.loopObsMappedRunBob : Process.Run loopSystem.toProcess

The specification-side run obtained by matching trueRun through loopObsSimBob.

def Interaction.Concurrent.Examples.loopTicketBisim : Refinement.Bisimulation loopSystem loopSystem (fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byTicket loopTicketed.ticket loopTicketed.ticket) fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byTicket loopTicketed.ticket loopTicketed.ticket

The identity ticket bisimulation on loopSystem.

def Interaction.Concurrent.Examples.loopObsBisimBob : Refinement.Bisimulation loopSystem loopSystem (fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byObservation Party.bob) fun {pL pR : loopSystem.Proc} => Observation.Process.TranscriptRel.byObservation Party.bob

The identity observational bisimulation on loopSystem for Bob.