Certified Implementability of Global Multiparty Protocols

In [34], the authors introduce an additional model for finitely representing potentially infinite GCLTS, called symbolic protocols. Symbolic protocol states store a set of registers, and transitions are labeled with dependent predicates that can refer to communication variables and register variables, and can thus describe register updates (see e.g. Figure 1). The semantics and implementability of a symbolic protocol is defined in terms of the concrete GCLTS it represents.

For illustration purposes, the GCLTS and symbolic protocol representations of a simple addition protocol between three participants $𝚙$, $𝚚$ and $𝚛$ are depicted in Figure 3 and Figure 3. In the protocol, participants $𝚙$ and $𝚚$ send two natural number values $x$ and $y$ to participant $𝚛$, who replies to participant $𝚙$ with the sum $z=x+y$, after which the protocol terminates.

[34] thus extends the Coherence Conditions to a set of Symbolic Coherence Conditions for algorithmically checking implementability of symbolic protocols, as well as investigating complexity of various decidable symbolic protocol fragments.

Thanks to Rocq’s type universe, we unify the two disparate definitions under a single formal definition in our mechanization, which represents protocols simply as an LTS parametric in a state and alphabet type, containing a transition relation, an initial state, and a final state relation.

We define LTS semantics using an inductive relation to represent reachability, lists to represent finite traces, and streams to represent infinite traces. Despite the apparent inconvenience imposed by the type-level distinction between finite and infinite words, we will see in §3.4 that we can greatly delay the acknowledgement of this distinction in key proofs, and moreover, that doing so simplifies the existing pen-and-paper proofs.

In this section, we examine asynchronous protocol semantics for infinite words. As mentioned in §2, the protocol semantics of $𝒮$ is defined in steps: we begin with the LTS semantics of $𝒮$, then apply a homomorphism split to obtain a set of asynchronous words that remain “synchronously ordered”, i.e. matching send and receive events are adjacent to each other. In an asynchronous network with peer-to-peer, FIFO channels, certain events can be reordered, and are thus considered independent. For example, the synchronous trace $𝚙\to 𝚚:m\cdot 𝚛\to 𝚜:m$ yields the asynchronous trace $u_1=𝚙⊳𝚚!m\cdot 𝚛⊳𝚜!m\cdot 𝚜⊲𝚛\mathrm{?}m\cdot 𝚚⊲𝚙\mathrm{?}m$, as well as $u_2=𝚛⊳𝚜!m\cdot 𝚙⊳𝚚!m\cdot 𝚜⊲𝚛\mathrm{?}m\cdot 𝚚⊲𝚙\mathrm{?}m$, in which the independent sends by $𝚙$ and $𝚛$ are reordered.

We call two words $w,w^{\prime }\in {\mathrm{\Sigma }}_{\mathrm{𝑎𝑠𝑦𝑛𝑐}}^{\omega }$ indistinguishable when any asynchronous implementation recognizing one word necessarily recognizes the other. Note that indistinguishability is specific to the assumed communication architecture: two words that are indistinguishable in a peer-to-peer FIFO setting may not be in a mailbox setting.

Allowing the semantics of global protocols to selectively exclude indistinguishable behaviors, e.g. by including $u_1$ but excluding $u_2$, would render protocols spuriously non-implementable. Thus, we desire for our protocol semantics to be closed under this notion of indistinguishability. For finite words, the indistinguishability relation is intuitive to formalize. Prior works that give language-theoretic semantics to session types, such as [36], define indistinguishability in terms of a binary relation on asynchronous events capturing when they can be reordered ¹¹1We identify a minor erratum in the original formulation of the indistinguishability relation [36] used in later works [45, 32, 31]: cases (3) and (4) are not symmetric, and thus the relation is not an equivalence relation as claimed., and a notion of channel compliance that captures valid traces with respect to peer-to-peer, FIFO semantics. In the message sequence chart literature, linearizations are required to satisfy the union of per-participant total orders and the send-before-receive partial order on events, coinciding with the definition from [36]. A key observation is that in pairs of indistinguishable finite words, the sequence of events for each participant is identical. Thus, given an asynchronous implementation that recognizes $w\in {\mathrm{\Sigma }}_{\mathrm{𝑎𝑠𝑦𝑛𝑐}}^{\omega }$, to show that the same asynchronous implementation recognizes $w^{\prime }$ indistinguishable from $w$, we do not need to know more about each participant’s local implementation beyond the fact that it accepts $w{\Downarrow }_{{\mathrm{\Sigma }}_{𝚙}}$, which is given from the fact that the implementation as a whole recognizes $w$.

For infinite words, however, indistinguishability can no longer be defined purely alphabetically. Consider the pair of infinite words $v_1=𝚙⊳𝚚!m^{\omega }$ and $v_2=𝚛⊳𝚜!m\cdot 𝚙⊳𝚚!m^{\omega }$. Are $v_1$ and $v_2$ indistinguishable? On our previous notion of indistinguishability, the answer is unfortunately, no. The fact that $v_1$ is a trace of an arbitrary asynchronous implementation gives us no information about the local implementation of participant $𝚛$, yet to show that $v_2$ is also a trace of said implementation, we need to additionally know that $𝚛$’s local implementation admits the trace $𝚛⊳𝚜!m$. This discrepancy arises from the fact that infinite traces in an asynchronous implementation can infinitely reorder independent events, in this case every occurrence of $𝚙⊳𝚚!m$ with $𝚛⊳𝚜!m$, achieving the effect of indefinitely postponing $𝚛⊳𝚜!m$.

Equipped with an understanding of the importance of indistinguishability-closed global semantics, we revisit the definition of infinite protocol semantics in [34]:

We show via counterexample that ${𝒞}^{\sim }{(𝒮)}^{\omega }$ is not indistinguishability-closed. Consider the simple protocol depicted in Figure 5, involving four participants $𝚙$, $𝚚$, $𝚛$, $𝚜$ and two message values $m,m^{\prime }$. As per [34], ${𝒞}^{\sim }({𝒮}_{\mathrm{𝑖𝑛𝑓}})$ does not include the infinite word $𝚛⊳𝚜!m^{\prime }\cdot 𝚙⊳𝚚!m^{\omega }$. In contrast, ${𝒞}^{\sim }({𝒮}_{\mathrm{𝑖𝑛𝑓}}^{\prime })$, whose protocol is obtained by a simple state renaming of Figure 5 and is depicted in Figure 5, does include $𝚛⊳𝚜!m^{\prime }\cdot 𝚙⊳𝚚!m^{\omega }$.

Before proposing a revised infinite word semantics that resolves this discrepancy, we discuss the implications of this counterexample on the results from [34]. It is easy to verify that ${𝒮}_{\mathrm{𝑖𝑛𝑓}}$ is a GCLTS and satisfies CC. However, ${𝒮}_{\mathrm{𝑖𝑛𝑓}}$ is not implementable: there exists no CLTS that recognizes the finite word $𝚙⊳𝚚!m^n\cdot 𝚙⊳𝚚!m^{\prime }\cdot 𝚛⊳𝚜!m^{\prime }$ for all values of $n\in \mathbb{N}$ yet does not recognize the infinite word $𝚛⊳𝚜!m\cdot 𝚙⊳𝚚!m^{\omega }$. This contradicts the soundness of the Coherence Conditions as stated in [34]. The error lies in the case for infinite words in the proof of [34, Lemma 4.9], which concludes from the fact that every prefix of an infinite word $w$ in the canonical implementation has a non-empty intersection run set $I(w)$, that $w\in {𝒞}^{\sim }{(𝒮)}^{\omega }$. To show that $w\in {𝒞}^{\sim }{(𝒮)}^{\omega }$, one needs to find a witness infinite run $\rho$ in $𝒮$, such that for every prefix $v^{\prime }\le w$, there exists an extension $u^{\prime }$ and a prefix of rho ${\rho }_v^{\prime }$ such that for all participants, the events prescribed by ${\rho }_v^{\prime }$ and $v^{\prime }\cdot u^{\prime }$ are identical. To show the existence of such a run, the authors appeal to König’s Lemma, and argue that in a finitely-branching infinite tree containing possible run prefixes for every prefix of $w^{\prime }$, there exists a ray representing an infinite run. This argument appears inherited from earlier works that deal with finite, multiparty session types [36, 32]. We discover that not only is König’s Lemma not applicable in the infinite setting of [34] where GCLTS states can have infinitely many transitions, the existence of a ray is insufficient to prove membership of $w$ in ${𝒞}^{\sim }{(𝒮)}^{\omega }$. The latter implies that the proof using König’s Lemma in both prior works [36, 32] is flawed: indeed, ${𝒮}_{\mathrm{𝑖𝑛𝑓}}^{\prime }$ is expressible in the multiparty session type fragments defined in these works that assume finitely many participants, states and transitions. The gap in the reasoning lies in showing that the infinite run obtained from König’s Lemma is indeed a suitable existential witness required by the infinite protocol semantics. In the infinite tree constructed for ${𝒮}_{\mathrm{𝑖𝑛𝑓}}$ and word $𝚛⊳𝚜!m^{\prime }\cdot 𝚙⊳𝚚!m^{\omega }$, the prefix $𝚛⊳𝚜!m^{\prime }$ contributes a vertex labeled with the run prefix $𝚙\to 𝚚:m\cdot 𝚙\to 𝚚:m^{\prime }\cdot 𝚛\to 𝚜:m^{\prime }$. Subsequent prefixes of the form $𝚛⊳𝚜!m^{\prime }\cdot 𝚙⊳𝚚!m^n$ contribute vertices labeled with run prefixes $𝚙\to 𝚚:m^n\cdot 𝚙\to 𝚚:m^{\prime }\cdot 𝚛\to 𝚜:m^{\prime }$. A ray exists in this finite-degree, infinite tree representing the run $𝚙\to 𝚚:m^{\omega }$. This is clearly an infinite run in ${𝒮}_{\mathrm{𝑖𝑛𝑓}}$, but unfortunately does not satisfy the conditions required to show membership of $w^{\prime }$ in ${𝒞}^{\sim }({𝒮}_{\mathrm{𝑖𝑛𝑓}})$: for prefix $𝚛⊳𝚜!m^{\prime }$ of $w$, there exists no prefix of $𝚙\to 𝚚:m^{\omega }$ that matches $𝚛$’s events.

Fortunately, the flawed infinite word semantics from [34] can easily be amended to accurately reflect the desired, indistinguishability-closed semantics. Our revised infinite word semantics is as follows:

${𝒞}_{\mathrm{𝑎𝑙𝑡}}^{\sim }{(𝒮)}^{\omega }$ swaps the first two quantifiers in the original definition, and weakens the requirement that $w$ come from an infinite run to the requirement that $w$ come from a finite run prefix (that could be part of a finite or infinite maximal run in $𝒮$). We hypothesize that this revised condition faithfully represents what prior works intended to capture with their infinite protocol semantics. It also more closely matches simulation-based notions of trace equivalence, for example in [50]. This is further evidenced by the fact that the requisite changes to the overall proof were minimal: the flawed König’s Lemma argument could simply be omitted in favor of appealing directly to the intersection set non-emptiness inductive invariant, and the completeness proof remained largely unchanged. The latter is due to the fact that for any infinite word $w$, $w\in {𝒞}^{\sim }{(𝒮)}^{\omega }⟹w\in {𝒞}_{\mathrm{𝑎𝑙𝑡}}^{\sim }{(𝒮)}^{\omega }$.

Showing that a global protocol is implementable amounts to finding a witness CLTS that implements it. The soundness proof of CC in [34] chooses a particular CLTS as witness, referred to as the canonical implementation. The canonicity of an implementation is defined as follows:²²2Note that in [34], the notation $ℒ(𝒮)$ is overloaded to denote ${𝒞}^{\sim }(𝒮)$.

In [34], the existence of a canonical implementation for any protocol is assumed. Formally proving the existence of canonical implementations in our mechanization requires constructing an explicit, albeit non-constructive, witness CLTS. The construction is conceptually straightforward; nonetheless, we illustrate key steps here as it is novel to our mechanization.

We begin by observing that because canonicity is defined on a per-participant basis, and with respect to an LTS that is deadlock-free, the definition can be weakened to use the LTS semantics of $𝒮$ rather than its protocol semantics. The weaker definition avoids reasoning about asynchronous reorderings and channel compliance, and is formalized in Rocq as follows.

In the Rocq definitions below, S is a protocol of type LTS SyncAlphabet State, and p is a participant. We choose State -> Prop for the state type of local implementations, so S_p is an LTS of type LTS AsyncAlphabet (State -> Prop).

The four conjuncts correspond to four inclusions that altogether define the two equalities in Section 3.3, and need to be stated separately due to the type mismatch between finite and infinite words.

Our construction for each participant’s local implementation can be expressed simply as a composition of two purely automata-theoretic operations: applying the homomorphism ${\Downarrow }_{{\mathrm{\Sigma }}_{𝚙}}$ for each participant, followed by determinization. This coincides with the subset construction automaton as defined in [32], whose name we borrow in our definitions. Formally, for each participant $𝚙\in 𝒫$, the result of the second step is an LTS over ${\mathrm{\Sigma }}_{𝚙}\cup \{ϵ\}$. To avoid introducing this compounded alphabet and reasoning about identity elements, we define both operations declaratively in one shot, to obtain a local LTS over the alphabet AsyncAlphabet, whose states are of type State -> Prop, representing subsets of $Q$.

The initial state is defined relationally as the set of all states reachable on $ϵ$ from $s_0$ in $𝒮$. States in the subset construction are the set of non-empty subsets of states in $𝒮$. Final states are defined relationally as sets of states containing at least one final state from $𝒮$.

The transition relation describes triples (ls, a, ls’) where ls is a pre-state in the subset construction, a is an asynchronous alphabet symbol in p’s restricted alphabet, and ls’ is a post-state. The relation states that ls’ contains all states from $𝒮$ that are either an immediate post-state of some state $s$ in ls, or is $ϵ$-reachable from an immediate post-state.

The former two conjuncts are implied by the latter two conjuncts together with the definition of final states in the subset construction. The latter two conjuncts state that every asynchronous trace in a participant’s canonical local implementation corresponds to a synchronous trace in $𝒮$, and every synchronous trace in $𝒮$ corresponds to an asynchronous trace in the participant’s canonical local implementation.

Unfortunately, these two properties are not themselves inductive: in both cases, the induction hypothesis is not strong enough to show that the respective traces can be extended. We state and prove two inductive invariants that explicitly quantify over states of $𝒮$ in a participant’s canonical local implementation S_p, and weaken them to obtain the third and fourth conjuncts. The strengthened inductive properties respectively state that for every reachable state ls on some asynchronous word w in S_p, for every global state s in ls, one can find a corresponding synchronous word w’ such that w’ and w agree on participant p’s events, and $𝒮$ reaches s on w’; conversely, for every reachable global state s on some synchronous word w in $𝒮$, one can find a corresponding local state ls’ and asynchronous word w’ such that w’ and w agree on participant p’s events, and S_p reaches ls’ on w’.

Finally, we define the canonical CLTS by mapping each participant to their subset construction. To show that the map thus defined is indeed a CLTS, we additionally need to prove that each local implementation is deterministic, and moreover operates on its own restricted alphabet. Both proofs are straightforward by definition of the subset construction; our proof of determinism uses the axioms of functional and propositional extensionality from Rocq’s Logic library to establish the equality of local states of type State -> Prop. We conclude with the existence lemma:

The core argument for soundness in [34] relies on proving the following inductive invariant:

Let $𝒮$ be a protocol satisfying CC, and let ${\{\{T_{𝚙}\}\}}_{𝚙\in 𝒫}$ be a canonical CLTS for $𝒮$. Let $w$ be a trace of ${\{\{T_{𝚙}\}\}}_{𝚙\in 𝒫}$. Then, $I(w)\ne \mathrm{\varnothing }$.

The set $I(w)$ contains finite or infinite maximal runs in $𝒮$ that are possible with respect to the trace $w$. Formally, $\rho \in I(w)$ means that for every participant $𝚙\in 𝒫$, $w{\Downarrow }_{{\mathrm{\Sigma }}_{𝚙}}\le \text{split}(\rho ){\Downarrow }_{{\mathrm{\Sigma }}_{𝚙}}$, i.e. each participant’s local events in $w$ agree with what $\rho$ prescribes. The proof proceeds by induction on the length of $w$, with case analysis in the inductive step on whether the next event is a send or receive event.

The non-emptiness of $I(w)$ amounts to an existential quantification over a disjunction. In our mechanization, however, due to the type-level distinction between finite and infinite runs, this property takes the form of a disjunction over existentials:

Although the soundness arguments from [34] are mechanizable using this definition of intersection set non-emptiness, doing so would involve repetitive reasoning to deal with finite and infinite runs separately that does not shed additional insight on the problem. We instead prove that every canonical CLTS trace has a possible run prefix. Our new inductive invariant factors out the distinction between finite and infinite runs, and is additionally more expressive than its pen-and-paper counterpart: it makes explicit the construction of a possible run prefix for $wx$ from one for $w$. When $x$ is a receive event, our lemma states that the exact same run prefix can be reused. When $x$ is a send event, a run prefix can be constructed incrementally by processing $w$ in increasing length order, and appealing to CC to incrementally extend a prefix of the possible run prefix for $wx$.

We focus the exposition below on our simplified proof for the inductive step when $x$ is a send event. Lemma 4.16 in [34] is stated as follows:

The unique splitting of a run for a participant with respect to a trace is the largest prefix of the run that matches the participant’s actions in the trace, formalized as follows:

For example, the unique splitting of run $\rho =𝚙\to 𝚚:m\cdot 𝚛\to 𝚜:m\cdot 𝚛\to 𝚚:m\cdot 𝚚\to 𝚙:m$ for participant $𝚙$ with respect to trace $u=𝚙⊳𝚚!m\cdot 𝚛⊳𝚜!m\cdot 𝚛⊳𝚚!m$ is $𝚙\to 𝚚:m\cdot 𝚛\to 𝚜:m\cdot 𝚛\to 𝚚:m$, because $𝚙$ has only completed the first event prescribed by $\rho$ in $u$, namely sending $m$ to $𝚛$, but has not completed the second event, namely receiving $m$ from $𝚚$. Because the two synchronous events in between these two events in $\rho$ do not concern $𝚙$, they are included in the largest prefix. If a run disagrees with a trace on some participant’s actions, the unique splitting is $ϵ$, for example $\rho$’s unique splitting for participant $𝚛$ with respect to trace $𝚛⊳𝚜!m^{\prime }$.

Our adapted formalization of Lemma 5 is thus stated as follows:

The proof of Lemma 4.16 in [34] relies on a nested induction argument. We illustrate the key steps in order to elucidate the structure of the nested induction and explain our simplified proof. From the induction hypothesis, we are granted a canonical CLTS trace w and a possible run prefix for w. Let the send extention to w be x = Snd p q m. We can then define the largest prefix of rho matching w for participant p, and because the premise grants that alpha <> rho, there must exist a next action prescribed by rho for p, which we denote l. As a reminder, since rho is a run of the global protocol, which is an LTS over the synchronous alphabet, l is a synchronous alphabet symbol. By the induction hypothesis, rho is compliant with all participants:

forall (p: participant), prefix (wproj w p) (wproj (split rho) p)

The induction step asks to construct an existential witness for a new possible run prefix, rho’, that is compliant with wx. In the case that l = Event p q m, we can directly reuse rho as our witness, and the three conjuncts required of rho’ are trivially satisfied when rho’ = rho. When this is not the case, we must construct a different witness. We first appeal to Send Coherence Condition to show that we can find a different continuation from alpha that agrees with x, in other words, l’ = [Event p q m] and alpha ++ l’ is a run in the global protocol.

With this extension and removal of the original suffix from rho, however, we are left only with a guarantee about p’s compliance:

prefix (wproj (w ++ [x]) p) (wproj (split (alpha ++ [Event p q m])) p)

In the case that all of the actions in w were already contained in alpha, we can use alpha ++ [l’] directly as our witness for rho’. However, in the case that some of w’s actions were contained in the now removed suffix, it is no longer true that all participants are compliant with alpha ++ [l’]. Therefore, the next step of the proof involves restoring a suffix that is “long enough” to contain all of the actions that were originally in w.

The argument for suffix restoration in [34] is algorithmic in nature, and is captured by the pseudocode in Algorithm 1. The algorithm initializes the candidate run ${\rho }_c$ as $\alpha \cdot \text{l’}$ appended to an arbitrary run suffix $\beta$ to form a maximal run. The outer while loop then “fixes” disagreements between $w$ and the current candidate run ${\rho }_c$ one symbol at a time, updating ${\rho }_c$ after each fix. Termination is guaranteed by the fact that $w$ has finite length and that each event in $w$ is fixed at most once. The outer while loop invariant relates ${\rho }_c^{\prime }$ with ${\rho }_c$, and guarantees that the largest common prefix shared by ${\rho }_c^{\prime }$ and ${\rho }_c$ between each loop iteration is strictly increasing. Because the initial candidate run is picked such that it includes $\alpha \cdot \text{l’}$ as a prefix, and the common prefix between runs can only get longer, it holds by transitivity that when the while loop terminates, the final candidate run must have $\alpha \cdot \text{l’}$ as a prefix, and furthermore is compliant with all events in $w$.

Formalizing the above algorithm in addition to its loop invariants would require a custom inductive predicate that relates the candidate run with disagreeing events in $w$. The fact that the loop invariant depends on both the current and previous candidate run introduces significant additional complexity.

We find a weaker inductive invariant that eliminates this dependency: it suffices to show that $\alpha \cdot \text{l’}\le {\rho }_c$ remains a prefix of the candidate run. This holds trivially upon entry to the while loop, and is preserved by each iteration from the fact that $\alpha$ comes from the original $\rho$ that is compliant with $w$, and thus no events in $w$ can disagree with events in $\alpha$.

In our new inductive invariant, $\alpha \cdot \text{l’}$ can now be treated as a constant. We convert the algorithmic reasoning in [34] to the following inner induction hypothesis:

We prove H_inner directly by induction on prefixes of w using rev_ind from the standard List library. Figure 7 visualizes the simplified inductive argument: the red symbols in w depict disagreeing events in w as a result of removing the suffix from rho.

To prove send_preserves_run_prefixes_finite, we needed to consider cases glossed over in the pen-and-paper proof from [34], and in some case develop arguments from scratch. For example, in the special case when alpha is a possible run prefix for participant p for trace w, but prescribes exactly as many events as are in w, we needed to show that either w is a maximal CLTS trace, or a different alpha can be found which prescribes more events, by appealing to the sink-finality of $𝒮$.