Mailbox Actors

1.1. Parametric Context🔗

The formalization is parameterised by the typeclass MailboxActors.EngineSpec, which bundles:

  • A finite type of engine type indices (𝕀), with decidable equality and a Fintype instance.

  • Indexed families MsgType, CfgData, and LocalState assigning message, configuration, and state types to each index.

  • Operations mailboxContains, mailboxRemove, and unwrap that connect mailbox state to message delivery.

An MailboxActors.Address identifies an engine as a (nodeId, engineId) pair.