While I have not understood the following (draft of a?) definition for *model,* stating that

the model is a lens through which messages are sent and received,

completely **yet**, I am jumping to the point that I find most important: the definition of *protocol.*

To get started, I would like to pick up the slogan that we are “moving from an imperative to a **declarative** paradigm”. In particular, I wonder what is the quickest way to “de-algorithmize” the above definition,^{[1]} i.e., the following:

In short, the plan is to avoid the jargon “ɴᴅᴛᴍ” and decouple the definition from any of the various entities that one may want to call an “agent”.

So, for starters, let us put aside the question of whether a protocol (instance) has to run `inside`

agents and defer the question of whether or not a first definition of protocol requires agents; I would think that all we need are primitive notions of receiving and sending of messages (w/o mention of who is sending or receiving) — very much in the spirit of the basics of service commitments (cc @Jamie @nzarin). But maybe not even that!

## Candidate for an abstract protocol definition

### Notation

- \wp powerset: \wp(A) ≔ \{ A' \mid A' \subseteq A\}
- \wp_f finite powerset: \wp_f(A) ≔ \{ A' \mid A' \subseteq A, A' \text{ is finite }\}
- A^B function space: A^B ≔ \{ f \mid f \colon B \to A\}

Also, suppose we have an arbitrary but fixed set of messages \mathbb M.

### Def. Protocol

A *protocol endpoint ^{[2]}* is a function e \colon \wp_f(\mathbb{M}) → \wp\bigl(\wp_f(\mathbb{M})\bigr) that takes a finite set of messages M —think

*received ones,*for the sake of intuition— as input and outputs a set of finite sets of messages e(M) —think

*all possible*options for message sets to be sent as

*correct*reaction, out of which one set

*must*be chosen. A

*protocol*is a pair (E, r), consisting of a finite set of protocol endpoints E and a function r \colon M \to \wp_f \left( \left(\wp\bigl(\wp_f(\mathbb M)\bigr)\right)^{\wp_f(\mathbb M)}\right), which maps each message to a finite set of protocol endpoints-- (think of it as the receivers).

## Exercise: describe protocol state as a pair of a set of messages in transit and sets of received messages at their endpoint (a map from endpoints to their received messages).

Best solution goes here!

## Exercise: describe protocol evolution as a transition system whose set of states are all possible protocol states.

The idea is that one message at a time gets delivered. See the WiP ART report (please dm me for details.)

### What about computable endpoints?

Once we have a definition of protocol in place, we sure want to have restrictions such that we can implement “sub-endpoints” of type \wp_f(\mathbb{M}) → \wp_f(\mathbb{M}), which is what Anoma’s engines do.^{[3]}

### What’s next: properties – but wait!

So, now, if we think about properties of protocols, likely we want to have this is sync with the current research on service commitments. Next up is the question of how to “upgrade” the above candidate definition with time, but one step at a time …

## TL;DR

I think, with little effort, we can find a way to polish our definition of protocol such that it is in line with Anoma’s philosophical underpinning, but independent of it *and* has clear links to published papers on the topic of protocol endpoints. In the end, engine instances should amount to implementations of protocol endpoints (cf. protocol instances in the above post).^{[4]}

## References

- Secure Synthesis of Distributed Cryptographic Applications
- Hybrid Multiparty Session Types - Full Version

Mainly, I want to put aside any ontological commitments, for the time being, being agnostic so to speak. Also, I think, some of the above text may already hint at some aspects of what I am after: the “boxing things up” and the occurrence of protocol

*instances*– as opposed to something else ↩︎The terminology

*protocol endpoint*is borrowed from two papers: the viaduct paper and Nobuko’s paper (see also ᴍᴘꜱᴛ)—without considering specifics of these papers. ↩︎I think, we can even encode the spawning of new endpoints in that we send messages to endpoints that are not yet present. However, No semantics given! ↩︎

In fact, the above idea of protocol could end up being extremely useful for setting the stage before we turn to the arduous definitions in the engine ART report (@jonathan @AHart). ↩︎