Bisimulation for dynamic concurrent processes

This file adds the symmetric refinement layer on top of Concurrent.Refinement.ForwardSimulation.

ForwardSimulation is intentionally one-way: it shows that every behavior of an implementation can be matched by some behavior of a specification. The purpose of this file is to package the corresponding two-way notion used when two systems should count as behaviorally equivalent rather than merely implementing one another.

The construction is deliberately simple:

• a backward simulation is just a forward simulation with the two systems swapped;
• a bisimulation packages one simulation in each direction; and
• once both directions are available, safety results can be transported either way, provided the chosen fairness assumptions also transfer.

This keeps the equivalence layer aligned with the existing process-centered refinement API rather than introducing a second semantic style.

def Interaction.Concurrent.Refinement.ForwardSimulation.refl {Γ : Spec.Node.Context} (system : ProcessOver.System Γ) (matchStep : system.TranscriptRel system.toProcess := fun {pL pR : system.Proc} => ProcessOver.TranscriptRel.top) (hmatch : ∀ {p : system.Proc} (tr : (system.step p).spec.Transcript), matchStep tr tr) : ForwardSimulation system system fun {pL pR : system.Proc} => matchStep

ForwardSimulation.refl system matchStep is the identity simulation on system, provided that matchStep relates each transcript to itself.

This is the canonical witness that every system refines itself.

@[reducible, inline]

abbrev Interaction.Concurrent.Refinement.BackwardSimulation {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} (impl : ProcessOver.System Γ) (spec : ProcessOver.System Δ) (matchStep : impl.TranscriptRel spec.toProcess := fun {pL : impl.Proc} {pR : spec.Proc} => ProcessOver.TranscriptRel.top) : Type (max u_2 u_1)

BackwardSimulation impl spec matchStep is just a forward simulation from spec to impl, with the transcript-matching relation reversed accordingly.

So "backward simulation" is only a change of viewpoint, not a second primitive notion.

structure Interaction.Concurrent.Refinement.Bisimulation {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} (left : ProcessOver.System Γ) (right : ProcessOver.System Δ) (matchForth : left.TranscriptRel right.toProcess := fun {pL : left.Proc} {pR : right.Proc} => ProcessOver.TranscriptRel.top) (matchBack : right.TranscriptRel left.toProcess := fun {pL : right.Proc} {pR : left.Proc} => ProcessOver.TranscriptRel.reverse fun {pL : left.Proc} {pR : right.Proc} => matchForth) : Type (max u_1 u_2)

Bisimulation left right matchForth matchBack packages one forward simulation in each direction between left and right.

By default, the backward transcript-matching relation is the reversal of the forward one.

This is the library's main process-level equivalence witness: each side can match the other's executions while preserving the chosen step relation.

• forth : ForwardSimulation left right fun {pL : left.Proc} {pR : right.Proc} => matchForth
• back : ForwardSimulation right left fun {pL : right.Proc} {pR : left.Proc} => matchBack

def Interaction.Concurrent.Refinement.Bisimulation.symm {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver.System Γ} {right : ProcessOver.System Δ} {matchForth : left.TranscriptRel right.toProcess} {matchBack : right.TranscriptRel left.toProcess} (bisim : Bisimulation left right (fun {pL : left.Proc} {pR : right.Proc} => matchForth) fun {pL : right.Proc} {pR : left.Proc} => matchBack) : Bisimulation right left (fun {pL : right.Proc} {pR : left.Proc} => matchBack) fun {pL : left.Proc} {pR : right.Proc} => matchForth

Swap the two sides of a bisimulation.

This is the symmetry principle for the packaged equivalence witness itself.

def Interaction.Concurrent.Refinement.Bisimulation.refl {Γ : Spec.Node.Context} (system : ProcessOver.System Γ) (matchForth : system.TranscriptRel system.toProcess := fun {pL pR : system.Proc} => ProcessOver.TranscriptRel.top) (matchBack : system.TranscriptRel system.toProcess := fun {pL pR : system.Proc} => ProcessOver.TranscriptRel.reverse fun {pL pR : system.Proc} => matchForth) (hForth : ∀ {p : system.Proc} (tr : (system.step p).spec.Transcript), matchForth tr tr) (hBack : ∀ {p : system.Proc} (tr : (system.step p).spec.Transcript), matchBack tr tr) : Bisimulation system system (fun {pL pR : system.Proc} => matchForth) fun {pL pR : system.Proc} => matchBack

The identity bisimulation on system, provided that both transcript relations relate every transcript to itself.

This is the reflexivity principle for the packaged equivalence witness.

theorem Interaction.Concurrent.Refinement.Bisimulation.left_safe_of_satisfies {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver.System Γ} {right : ProcessOver.System Δ} {matchForth : left.TranscriptRel right.toProcess} {matchBack : right.TranscriptRel left.toProcess} (bisim : Bisimulation left right (fun {pL : left.Proc} {pR : right.Proc} => matchForth) fun {pL : right.Proc} {pR : left.Proc} => matchBack) (fairLeft : ProcessOver.Run.Pred left.toProcess) (fairRight : ProcessOver.Run.Pred right.toProcess) (hfair : ∀ (run : left.Run) {pRight : right.Proc} (hrel : bisim.forth.stateRel run.initial pRight), fairLeft run → fairRight (bisim.forth.mapRun run hrel)) (hright : right.Satisfies fairRight right.Safe) : left.Satisfies fairLeft left.Safe

Transport safety from the right system to the left system under a bisimulation, assuming the chosen fairness predicates transfer along the forward direction.

This is the "use the right-hand system as the proof-oriented model" direction.

theorem Interaction.Concurrent.Refinement.Bisimulation.right_safe_of_satisfies {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver.System Γ} {right : ProcessOver.System Δ} {matchForth : left.TranscriptRel right.toProcess} {matchBack : right.TranscriptRel left.toProcess} (bisim : Bisimulation left right (fun {pL : left.Proc} {pR : right.Proc} => matchForth) fun {pL : right.Proc} {pR : left.Proc} => matchBack) (fairLeft : ProcessOver.Run.Pred left.toProcess) (fairRight : ProcessOver.Run.Pred right.toProcess) (hfair : ∀ (run : right.Run) {pLeft : left.Proc} (hrel : bisim.back.stateRel run.initial pLeft), fairRight run → fairLeft (bisim.back.mapRun run hrel)) (hleft : left.Satisfies fairLeft left.Safe) : right.Satisfies fairRight right.Safe

Transport safety from the left system to the right system under a bisimulation, assuming the chosen fairness predicates transfer along the backward direction.

This is the same transport principle in the opposite direction.

theorem Interaction.Concurrent.Refinement.Bisimulation.safe_iff_of_satisfies {Γ : Spec.Node.Context} {Δ : Spec.Node.Context} {left : ProcessOver.System Γ} {right : ProcessOver.System Δ} {matchForth : left.TranscriptRel right.toProcess} {matchBack : right.TranscriptRel left.toProcess} (bisim : Bisimulation left right (fun {pL : left.Proc} {pR : right.Proc} => matchForth) fun {pL : right.Proc} {pR : left.Proc} => matchBack) (fairLeft : ProcessOver.Run.Pred left.toProcess) (fairRight : ProcessOver.Run.Pred right.toProcess) (hfairLeft : ∀ (run : left.Run) {pRight : right.Proc} (hrel : bisim.forth.stateRel run.initial pRight), fairLeft run → fairRight (bisim.forth.mapRun run hrel)) (hfairRight : ∀ (run : right.Run) {pLeft : left.Proc} (hrel : bisim.back.stateRel run.initial pLeft), fairRight run → fairLeft (bisim.back.mapRun run hrel)) : left.Satisfies fairLeft left.Safe ↔ right.Satisfies fairRight right.Safe

Safety under fairness assumptions is equivalent across a bisimulation when the fairness assumptions themselves transfer in both directions.

So once fairness transport is established, either side of a bisimulation may be used as the proof-oriented presentation of the protocol.