Juvix imports

module node_architecture.basics;

import prelude open public;
import prelude open using {Hash} public;
import node_architecture.types.anoma_message as Anoma;
import node_architecture.identity_types open;

Juvix Prelude of the Anoma Node Architecture¶

This document describes the basic types and functions used in the node architecture prelude. For a more general prelude, please refer to Juvix Base Prelude. (1)

If you are unfamiliar with Juvix, please refer to the Juvix documentation.

Types for messages and communication¶

A message is a piece of data dispatched from one engine, termed the sender, to another engine, referred to as the target. When a message is sent, it is enveloped with additional metadata such as the target address and potentially the sender address, in case the sender wants to be identified. Upon arrival at the target engine, the message is stored in the target engine's mailboxes. These mailboxes are indexed by an identifier that are only unique to their engine. If the target engine has only one mailbox, the mailbox identifier is redundant.

The following types are used to represent these messages and mailboxes.

MailboxID¶

A mailbox identifier is a natural number used to index mailboxes.

Where do mailbox identifiers come from?

The concept of mailbox identifier is taken from the paper ¹ (see also Mailbox Cluster and ²).

syntax alias MailboxID := Nat;

MessagePacket¶

A message packet consists of a target address, a mailbox identifier, and the message itself.

type MessagePacket : Type :=
  mkMessagePacket {
    target : Address;
    mailbox : Maybe Nat;
    message : Anoma.Msg
  };

EnvelopedMessage¶

An enveloped message consists of a possible sender address if the sender wishes to be identified, along with a message packet.

type EnvelopedMessage : Type :=
  mkEnvelopedMessage {
    sender : Maybe Address;
    packet : MessagePacket
  };

For convenience, here are some handy functions for enveloped messages:

getMessageType : EnvelopedMessage -> Anoma.Msg
  | mkEnvelopedMessage@{packet := mkMessagePacket@{message := mt}} := mt;

getMessageSender : EnvelopedMessage -> Maybe Address
  | mkEnvelopedMessage@{sender := s} := s;

getMessageTarget : EnvelopedMessage -> Address
  | mkEnvelopedMessage@{packet := mkMessagePacket@{target := t}} := t;

Mailbox S¶

A mailbox is a container for messages and optionally a mailbox state. The mailbox state could be used to store additional information about the mailbox, such as the priority of the messages in the mailbox.

Where does mailbox state come from?

The mailbox state is related to the capabilities of mailboxes of the paper ¹. In particular, at any given point in time, a mailbox will have a capability for receiving messages (in later versions of the specs). As mailbox state can be useful in general, we already have it now.

type Mailbox (MailboxStateType : Type) : Type :=
  mkMailbox {
    messages : List EnvelopedMessage;
    mailboxState : Maybe MailboxStateType
  };

Time¶

syntax alias Time := Nat;

Timer H¶

type Timer (HandleType : Type) : Type :=
  mkTimer {
    time : Time;
    handle : HandleType
  };

Trigger H¶

type Trigger (HandleType : Type) :=
  | MessageArrived {envelope : EnvelopedMessage}
  | Elapsed {timers : List (Timer HandleType)};

Extract the actual message from a trigger in case it has one:

getMessageFromTrigger : {H : Type} -> Trigger H -> Maybe Anoma.Msg
  | MessageArrived@{envelope := mkEnvelopedMessage@{packet := mkMessagePacket@{message := m}}} :=
    just m
  | _ := nothing;

Get the message sender from a trigger:

getMessageSenderFromTrigger : {H : Type} -> Trigger H -> Maybe Name
  | MessageArrived@{envelope := e} := EnvelopedMessage.sender e
  | _ := nothing;

Get the target destination from a trigger:

getMessageTargetFromTrigger : {H : Type} -> Trigger H -> Maybe Name
  | MessageArrived@{envelope := mkEnvelopedMessage@{packet := mkMessagePacket@{target := t}}} :=
    just t
  | _ := nothing;

TimestampedTrigger M H¶

type TimestampedTrigger (HandleType : Type) :=
  mkTimestampedTrigger {
    time : Time;
    trigger : Trigger HandleType
  };

Get the actual message from a TimestampedTrigger:

getMessageFromTimestampedTrigger
  {H} (tr : TimestampedTrigger H) : Maybe Anoma.Msg :=
  getMessageFromTrigger (TimestampedTrigger.trigger tr);

Get the sender from a TimestampedTrigger:

getMessageSenderFromTimestampedTrigger
  {H} (tr : TimestampedTrigger H) : Maybe Name :=
  getMessageSenderFromTrigger (TimestampedTrigger.trigger tr);

Get the target from

getMessageTargetFromTimestampedTrigger
  {H} (tr : TimestampedTrigger H) : Maybe Name :=
  getMessageTargetFromTrigger (TimestampedTrigger.trigger tr);

Simon Fowler, Duncan Paul Attard, Franciszek Sowul, Simon J. Gay, and Phil Trinder. Special delivery: programming with mailbox types. Proceedings of the ACM on Programming Languages, 7(ICFP):78–107, August 2023. URL: http://dx.doi.org/10.1145/3607832, doi:10.1145/3607832. ↩↩
Shams M. Imam and Vivek Sarkar. Selectors: actors with multiple guarded mailboxes. AGERE! '14: Proceedings of the 4th International Workshop on Programming based on Actors Agents and Decentralized Control, October 2014. URL: http://dx.doi.org/10.1145/2687357.2687360, doi:10.1145/2687357.2687360. ↩