4.5. Eventual Delivery (Proposition 5)🔗

@MailboxActors.eventualDelivery : ∀ [inst : MailboxActors.EngineSpec] (trace : MailboxActors.Trace)
  (m : MailboxActors.Message) (n : ℕ),
  MailboxActors.IsExecution trace →
    MailboxActors.StronglyFair trace →
      MailboxActors.WellTypedState (trace n) →
        MailboxActors.MailboxIsolation (trace n) →
          MailboxActors.UniqueInTransit trace m n →
            MailboxActors.EventuallyAccepts trace m n → m ∈ (trace n).messages → ∃ k ≥ n, m ∉ (trace k).messages#check @MailboxActors.eventualDelivery

Under strong fairness, every in-transit message is eventually consumed.

The proof is structured around infinite execution traces (MailboxActors.Trace). The key definitions are:

MailboxActors.IsExecution — consecutive states are related by SysStep.
MailboxActors.StronglyFair — every infinitely-often-enabled transition is eventually taken (TLA⁺-style).
MailboxActors.UniqueInTransit — the message appears at most once in the transit pool.
MailboxActors.EventuallyAccepts — the target mailbox is eventually ready and willing to accept the message.

The safety lemma MailboxActors.invariants_trace establishes that well-typedness and mailbox isolation are jointly preserved along any execution trace. The main theorem then shows that under the fairness and acceptance hypotheses, there exists a future step k where the message is no longer in transit.