4.4. Mailbox Isolation (Proposition 4)🔗

@MailboxActors.mailboxIsolation : ∀ [inst : MailboxActors.EngineSpec] (κ κ' : MailboxActors.SystemState)
  (op : MailboxActors.OpLabel),
  MailboxActors.WellTypedState κ →
    MailboxActors.MailboxIsolation κ → MailboxActors.OpStep κ op κ' → MailboxActors.MailboxIsolation κ'#check @MailboxActors.mailboxIsolation

All messages in transit target mailbox engines, never processing engines directly. This invariant is preserved by every system step.

The key insight is that M-Send is the only rule that creates messages, and it always routes them to the target's mailbox address.

Two companion theorems formalize Remark 4.4 of the paper:

MailboxActors.mailboxPersistence — when S-Clean removes a terminated processing engine, its paired mailbox engine survives.
MailboxActors.mailboxSurvivesClean — the surviving mailbox retains its type index and mail mode.