Specify the broadcast semantics of mini-protocol programs

[jeltsch]

We shall specify a semantics that translates mini-protocol programs into Þ-calculus processes, using broadcast communication for communication between parties. This semantics is only intended for programs that conform to some possibilities, which excludes programs that use pipelining.

Concretely, the broadcast semantics shall have the following characteristics:

1. Communication is handled using a single medium for ordered transmission as described in Add support for ordered transmission thorn-calculus#128.
2. Each party maintains a single cursor, which is its receiving position within the ordered-transmission medium.
3. Each party fetches all messages, also those that it has sent itself.
4. The parties use their cursors also for sending.

Item 4 doesn’t cause problems, because of item 3: when a party has agency, it has received all messages, and consequently its receiving position coincides with the position that it should use for sending.

The broadcast semantics shall be subject to some additional constraints, which it shares with the multicast semantics described in #96:

• Cursors for sending and receiving messages between parties are introduced locally.
• Whenever a program receives a message that it cannot handle, it uses the to get an unspecified follow-up program instead of making the behavior unspecified in a different way. This is because the documentation of the ↓-construct says the following:

  ↓ M. 𝔒 M receives a message M from a peer and continues like the (𝔒 M).