pacta/protocol/relations

Deciding duality, equivalence and subtyping between projected protocols.

pacta/session/duality proves two protocols fit together by building a value out of combinators. That works, and it is checked by the compiler, which is why it is the right tool for a protocol written as a nested type. It also has a hard limit: a finite value cannot witness an infinite unfolding, so the moment a protocol repeats there is no proof to build.

This module is the answer for those. Once a protocol is a state graph rather than a type, the questions stop being about syntax and start being about behaviour, and behavioural questions are answered coinductively: instead of building a proof upward from the leaves, assume the pair of states you care about is related, and look for a contradiction. If none turns up before you run out of pairs, there was never going to be one.

Keizer, Basold and Pérez set this out in Session Coalgebras: A Coalgebraic View on Session Types and Communication Protocols (2020) part that makes it practical is their Theorem 1: for a coalgebra with finitely many reachable states, all three relations are decidable. A projected graph always has finitely many states, so all three are decidable here, and the procedure is small enough to read.

The procedure

Start with the pair of initial states. Repeatedly take a pair, check the two states carry compatible labels, and add whatever pairs their matching transitions lead to. Stop when a check fails, or when every pair has been visited. Termination is free: there are at most left * right pairs and none is ever visited twice.

What comes back on success is the relation itself, because that is the certificate. A bisimulation is not evidence for equivalence, it is what equivalence means.

The three relations

Duality asks whether two participants fit together: every send meets a receive of the same thing, every choice meets an offer of the same arms, and both finish together. This is the recursive counterpart of session/duality.

Equivalence asks whether two protocols are the same protocol. Useful for checking that an edit to a specification changed nothing, and for telling a genuine redesign from a renaming.

Subtyping asks whether one protocol may stand in for another, and is capability the nested encoding has none of. subtype(new, old) succeeding means a participant written against old keeps working against new, so it is the check to run before shipping a protocol change. The rule is the usual one: a subtype may offer more than it was asked to, because being ready for a message nobody sends costs nothing, and may select fewer, because declining to use an option strands nobody. Widening in the other direction breaks callers, and gets rejected here rather than in production.

Limits

Payload types are compared by name, because a specification holds names rather than types. Two payloads spelled differently are treated as different even when one is an alias for the other, which errs toward rejecting a change that is in fact safe.

A send is never related to a choice, even a choice with one arm, and the projector cannot produce a one-armed choice anyway. Nothing is lost, but it does mean these relations are slightly finer than the ones in the paper.

pub type Mismatch {
  Mismatch(left: String, right: String, reason: Reason)
}

pub type Reason {
  Incompatible(left: String, right: String)
  DifferentLabels(left: String, right: String)
  DifferentPayloads(label: String, left: String, right: String)
  DifferentPeers(left: String, right: String)
  UnmatchedBranch(label: String)
  UnknownState(name: String)
}

pub type Witness {
  Witness(pairs: List(#(String, String)))
}

pub fn dual(
  left: graph.Graph,
  right: graph.Graph,
) -> Result(Witness, Mismatch)

let assert Ok([customer, teller]) = graph.compile(atm())
let assert Ok(_) = relations.dual(customer, teller)

pub fn equivalent(
  left: graph.Graph,
  right: graph.Graph,
) -> Result(Witness, Mismatch)

// Did tidying the specification change the protocol?
let assert Ok(_) = relations.equivalent(before, after)

pub fn explain(mismatch: Mismatch) -> String

pub fn render(witness: Witness) -> String

pub fn subtype(
  sub: graph.Graph,
  sup: graph.Graph,
) -> Result(Witness, Mismatch)

let assert Ok([_, new_teller]) = graph.compile(atm_with_transfers())
let assert Ok([_, old_teller]) = graph.compile(atm())

// Handling a new request is safe. Requiring one would not be.
let assert Ok(_) = relations.subtype(new_teller, old_teller)