Mailbox Actors

4.2. Progress (Proposition 2)🔗

@MailboxActors.progress : ∀ [inst : MailboxActors.EngineSpec] (κ : MailboxActors.SystemState), MailboxActors.WellTypedState κ → MailboxActors.MailboxIsolation κ → MailboxActors.hasProductiveWork κ → ∃ op, op ≠ MailboxActors.OpLabel.node ∧ ∃ κ', MailboxActors.OpStep κ op κ'#check @MailboxActors.progress

A well-typed system with productive work can always take a non-trivial step (excluding S-Node, which is always available).

The predicate MailboxActors.hasProductiveWork holds when at least one of the following is true:

  1. An engine is busy — guaranteed to proceed via S-Process.

  2. A processing engine is terminated — guaranteed to be cleaned via S-Clean.

  3. A message is in transit to a ready mailbox that accepts it — guaranteed to proceed via M-Enqueue.

The proof relies on two helper results:

  • MailboxActors.evalStep_total — behaviour evaluation is total for well-formed behaviours.

  • MailboxActors.effectEvalStep_total — effect execution always produces a valid successor state.