module arch.node.types.messages;

import prelude open public;
import arch.node.types.basics open;
import arch.node.types.crypto open;
import arch.node.types.identities open;

Messages and mailboxes¶

Types¶

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.

EngineMsg¶

An engine message is a message between engines. It consists of a sender, a target, an optional mailbox identifier, and the message itself.

type EngineMsg M :=
  mkEngineMsg@{
    sender : EngineID;
    target : EngineID;
    mailbox : Option MailboxID;
    msg : M;
  };

EngineMsgID¶

An engine message identifier. The cryptographic hash of the corresponding EngineMsg.

syntax alias EngineMsgID := Digest;

Mailbox S¶

A mailbox is a container for engine 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.

type Mailbox S M :=
  mkMailbox@{
    messages : List (EngineMsg M);
    mailboxState : Option S;
  };

MailboxID¶

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

syntax alias MailboxID := Nat;

Timer H¶

type Timer H :=
  mkTimer@{
    time : Time;
    handle : H;
  };

Trigger H¶

type Trigger H M :=
  | MessageArrived@{msg : EngineMsg M}
  | Elapsed@{timers : List (Timer H)};

• Extract the EngineMsg from a trigger in case it has one:

  getEngineMsgFromTrigger {H M} (tr : Trigger H M) : Option (EngineMsg M) :=
    case tr of
      | MessageArrived@{msg} := some msg
      | Elapsed@{} := none;

• Extract the Msg from a trigger in case it has one:

  getMsgFromTrigger {H M} (tr : Trigger H M) : Option M :=
    case tr of
      | MessageArrived@{msg} := some (EngineMsg.msg msg)
      | Elapsed@{} := none;

• Get the message sender from a trigger:

  getSenderFromTrigger {H M} (tr : Trigger H M) : Option EngineID :=
    case tr of
      | MessageArrived@{msg} := some (EngineMsg.sender msg)
      | Elapsed@{} := none;

• Get the target destination from a trigger:

  getTargetFromTrigger {H M} (tr : Trigger H M) : Option EngineID :=
    case tr of
      | MessageArrived@{msg} := some (EngineMsg.target msg)
      | Elapsed@{} := none;

TimestampedTrigger H¶

type TimestampedTrigger H M :=
  mkTimestampedTrigger@{
    time : Time;
    trigger : Trigger H M;
  };

• Get the EngineMsg from a TimestampedTrigger:

  getEngineMsgFromTimestampedTrigger
    {H M} (tr : TimestampedTrigger H M) : Option (EngineMsg M) :=
    getEngineMsgFromTrigger (TimestampedTrigger.trigger tr);

• Get the Msg from a TimestampedTrigger:

  getMsgFromTimestampedTrigger {H M} (tr : TimestampedTrigger H M) : Option M :=
    getMsgFromTrigger (TimestampedTrigger.trigger tr);

• Get the sender from a TimestampedTrigger:

  getSenderFromTimestampedTrigger
    {H M} (tr : TimestampedTrigger H M) : Option EngineID :=
    getSenderFromTrigger (TimestampedTrigger.trigger tr);

• Get the target from a TimestampedTrigger:

  getTargetFromTimestampedTrigger
    {H M} (tr : TimestampedTrigger H M) : Option EngineID :=
    getTargetFromTrigger (TimestampedTrigger.trigger tr);