1.6. Guards and Guarded Actions🔗

A MailboxActors.GuardInput is the triple (msg, config, env) that guards and actions receive.

A MailboxActors.GuardedAction pairs a guard with an action. The action is dependently typed: it may only be invoked when guard inp = some w, so the type system enforces the invariant "action fires only when the guard holds." The witness w carries any data extracted by the guard (pattern-match results, decoded fields, etc.).

The convenience function MailboxActors.GuardedAction.apply evaluates a guarded action on a given input: if the guard matches it fires the action (forwarding the proof), otherwise it produces noop.