Mailbox Actors

2.3. Well-Typedness🔗

A MailboxActors.WellTypedState bundles five structural invariants:

  1. Messages typed — every in-transit message has a payload whose engine type index matches the target engine's type.

  2. Mailbox exists — every processing engine has a paired mailbox engine whose type index matches and whose mode is mail.

  3. Fresh IDs — the nextId counter exceeds every existing engineId, guaranteeing address freshness.

  4. Message targets valid — all messages in transit target addresses created before the current nextId.

  5. Nodes exist — for every engine, the corresponding node is present.

The companion predicate MailboxActors.MailboxIsolation states that all messages in transit target mailbox engines (not processing engines). This is a separate invariant because it is preserved by the semantics and required by type preservation, but it is not part of the well-typedness definition itself.

The theorem MailboxActors.spawnPairing restates the mailbox_exists field as a standalone result for clarity: every processing engine has a paired mailbox engine with matching type index in mail mode.