pacta/protocol/weave

Weaving two protocols into one, guided by their contact points.

Sequencing puts one protocol after another, which is type application and needs nothing from this module. Weaving is the other thing: two protocols that have to advance in step, each constraining the other in both directions. A banking service and the authentication it depends on are the standard example. The login has to precede the menu, and each payment needs its own second factor, so neither protocol can simply be appended to the other.

This is an attempt to implement some ideas from Bocchi, Orchard and Voinea’s A Theory of Composing Protocols (2023) Their prefix actions are a parameter of the theory, so instantiating them with spec.Message is within what the paper covers, and the output is one ordinary spec.Spec that projects and checks like any other.

Composition is a relation, not a function

Two protocols may have no valid interleaving, one, or many. That is not a deficiency to be smoothed over by picking a winner: which weaving is wanted is a question about the domain, and nothing here can answer it. So compose returns candidates, ranked, and the way to narrow them is to add contact points rather than to guess.

The paper’s own figures are worth knowing before running this on something large. Their suite mostly yields one or two candidates, but an example with nested recursion reaches fourteen. Options.limit bounds the search, and Composition.truncated says when it bit.

Contact points

Assert introduces a guarantee, Require demands one and leaves it, and Consume demands one and spends it. They are what turn an intractable set of interleavings into a useful one.

// Payment first, then dispatch. Not the other way round.
let paying = spec.Message("Buyer", "Shop", "pay", "Money", spec.Assert("paid", spec.End))
let sending = spec.Consume("paid", spec.Message("Shop", "Buyer", "item", "Link", spec.End))

let assert weave.Composition(candidates: [only], ..) =
  weave.compose(paying, sending, weave.defaults())

Without the annotations there are two interleavings and no reason to prefer either. With them there is exactly one, and it is the right one.

Branching

How a choice composes is the one knob worth understanding, because the strict reading returns nothing surprisingly often.

• Strong composes the other protocol into every arm. Correct, and frequently empty: an authentication protocol that grants access in one arm and refuses in the other cannot compose the service into the refusing arm, because the guarantee it needs was never asserted there.
• Weak lets an arm go uncomposed when it genuinely cannot compose, which is exactly the authentication case. At least one arm still has to compose, so neither protocol can be dropped altogether.
• Correlating pairs each arm of one protocol with the arms of the other it can compose with, rather than distributing into all of them. This is what you want when two choices are meant to line up, such as a service choice and a matching payment method.
• All permits both relaxations.

Each relaxation widens the result set rather than narrowing it, so a candidate derivable strongly is still derivable under All. Every candidate records which relaxations its derivation needed, and that is what the ranking is built on: candidates needing none come first.

What this does not do

Composition drops the cosmetic state names spec.At carries, because a woven protocol’s states do not correspond to either input’s.

Nothing here checks that the result is projectable. Weaving can easily produce a protocol some participant cannot follow, and graph.compile is what says so. Run it on the candidate you pick.

pub type Branching {
  Strong
  Weak
  Correlating
  All
}

pub type Candidate {
  Candidate(protocol: spec.Spec, relaxations: List(Relaxation))
}

pub type Composition {
  Composition(candidates: List(Candidate), truncated: Bool)
}

pub type Options {
  Options(branching: Branching, given: List(String), limit: Int)
}

pub type Relaxation {
  WeakBranch(label: String)
  CorrelatedBranch(left: String, right: String)
}

let error = weave.UnexpectedCandidateCount(2)

pub type SelectionError {
  SearchTruncated
  UnexpectedCandidateCount(found: Int)
}

pub fn compose(
  left: spec.Spec,
  right: spec.Spec,
  options: Options,
) -> Composition

let options = weave.Options(..weave.defaults(), branching: weave.Weak)
let weave.Composition(candidates:, truncated: _) =
  weave.compose(banking, authentication, options)

case candidates {
  [] -> io.println("no valid interleaving; try adding contact points")
  [best, ..] -> chosen(best.protocol)
}

pub fn defaults() -> Options

pub fn describe(relaxation: Relaxation) -> String

pub fn interleave(
  left: spec.Protocol,
  right: spec.Protocol,
  options: Options,
) -> List(spec.Protocol)

let assert [best, ..] = weave.interleave(banking, authentication, options)
let assert Ok(graphs) = graph.compile(best)

pub fn select_unique(
  composition: Composition,
) -> Result(Candidate, SelectionError)

case weave.select_unique(composition) {
  Ok(candidate) -> generate(candidate.protocol)
  Error(weave.SearchTruncated) -> increase_the_search_limit()
  Error(weave.UnexpectedCandidateCount(_)) -> refine_the_contact_points()
}

pub fn summarise(candidate: Candidate) -> String