Common concurrent equivalence notions

This file packages the bisimulation-based equivalence notions that are most useful in practice.

The underlying Refinement.Bisimulation API is intentionally general: it can talk about any step relation whatsoever. For actual protocol work, however, one usually wants a smaller family of standard questions:

• do the two systems expose the same controller at each step?
• do they expose the same full controller path?
• do they produce the same external event trace?
• do they preserve the same fairness tickets?
• does a chosen party observe the same thing in both systems?

This file packages exactly those questions as named equivalence notions and records the immediate preservation lemmas for finite run prefixes.

@[reducible, inline]

abbrev Interaction.Concurrent.Equivalence.Controller {Party : Type u} (left : Process.System Party) (right : Process.System Party) : Type (max u_1 u_3)

Controller left right means that left and right are bisimilar while preserving the current controlling party chosen at each executed step.

@[reducible, inline]

abbrev Interaction.Concurrent.Equivalence.ControllerPath {Party : Type u} (left : Process.System Party) (right : Process.System Party) : Type (max u_1 u_3)

ControllerPath left right means that left and right are bisimilar while preserving the full controller path of each executed step.

@[reducible, inline]

abbrev Interaction.Concurrent.Equivalence.Trace {Party : Type u} {Event : Type w} (left : Process.System Party) (right : Process.System Party) (eventLeft : left.EventMap Event) (eventRight : right.EventMap Event) : Type (max u_1 u_3)

Trace left right eventLeft eventRight means that left and right are bisimilar while preserving the stable external event label attached to each complete step transcript.

@[reducible, inline]

abbrev Interaction.Concurrent.Equivalence.Ticket {Party : Type u} {TicketTy : Type w} (left : Process.System Party) (right : Process.System Party) (ticketLeft : left.Tickets TicketTy) (ticketRight : right.Tickets TicketTy) : Type (max u_1 u_3)

Ticket left right ticketLeft ticketRight means that left and right are bisimilar while preserving the stable tickets attached to complete step transcripts.

@[reducible, inline]

abbrev Interaction.Concurrent.Equivalence.Observation {Party : Type u} [DecidableEq Party] (me : Party) (left : Process.System Party) (right : Process.System Party) : Type (max u_1 u_3)

Observation me left right means that left and right are bisimilar while preserving the packed local observations exposed to the fixed party me at every executed step.

theorem Interaction.Concurrent.Equivalence.Controller.currentControllersUpTo_eq {Party : Type u} {left : Process.System Party} {right : Process.System Party} (equiv : Controller left right) (run : Process.Run left.toProcess) {pRight : right.Proc} (hrel : equiv.forth.stateRel run.initial pRight) (n : ℕ) : run.currentControllersUpTo n = Process.Run.currentControllersUpTo (equiv.forth.mapRun run hrel) n

Along the forward direction of a controller equivalence, the current controller sequence of every finite run prefix is preserved.

theorem Interaction.Concurrent.Equivalence.ControllerPath.controllerPathsUpTo_eq {Party : Type u} {left : Process.System Party} {right : Process.System Party} (equiv : ControllerPath left right) (run : Process.Run left.toProcess) {pRight : right.Proc} (hrel : equiv.forth.stateRel run.initial pRight) (n : ℕ) : run.controllerPathsUpTo n = Process.Run.controllerPathsUpTo (equiv.forth.mapRun run hrel) n

Along the forward direction of a controller-path equivalence, the full controller-path sequence of every finite run prefix is preserved.

theorem Interaction.Concurrent.Equivalence.Trace.eventsUpTo_eq {Party : Type u} {Event : Type w} {left : Process.System Party} {right : Process.System Party} {eventLeft : left.EventMap Event} {eventRight : right.EventMap Event} (equiv : Trace left right eventLeft eventRight) (run : Process.Run left.toProcess) {pRight : right.Proc} (hrel : equiv.forth.stateRel run.initial pRight) (n : ℕ) : Process.Run.eventsUpTo eventLeft run n = Process.Run.eventsUpTo eventRight (equiv.forth.mapRun run hrel) n

Along the forward direction of a trace equivalence, the stable event trace of every finite run prefix is preserved.

theorem Interaction.Concurrent.Equivalence.Ticket.ticketsUpTo_eq {Party : Type u} {TicketTy : Type w} {left : Process.System Party} {right : Process.System Party} {ticketLeft : left.Tickets TicketTy} {ticketRight : right.Tickets TicketTy} (equiv : Ticket left right ticketLeft ticketRight) (run : Process.Run left.toProcess) {pRight : right.Proc} (hrel : equiv.forth.stateRel run.initial pRight) (n : ℕ) : Process.Run.ticketsUpTo ticketLeft run n = Process.Run.ticketsUpTo ticketRight (equiv.forth.mapRun run hrel) n

Along the forward direction of a ticket equivalence, the stable ticket sequence of every finite run prefix is preserved.

theorem Interaction.Concurrent.Equivalence.Observation.observationsUpTo_eq {Party : Type u} [DecidableEq Party] (me : Party) {left : Process.System Party} {right : Process.System Party} (equiv : Observation me left right) (run : Process.Run left.toProcess) {pRight : right.Proc} (hrel : equiv.forth.stateRel run.initial pRight) (n : ℕ) : Observation.Process.Run.observationsUpTo me run n = Observation.Process.Run.observationsUpTo me (equiv.forth.mapRun run hrel) n

Along the forward direction of an observational equivalence, the packed local observations of the chosen party are preserved on every finite run prefix.