Trait BundleConsumedAtMostOnce 

pub trait BundleConsumedAtMostOnce:
    InboxHoldsOnlySentBundles
    + EffectsSurviveRestart
    + IncomingBundlesMatchTheLocalInbox { }

Lemma (A bundle is consumed at most once). No two blocks of a chain consume the same MessageBundle from the same origin, even though delivery is at-least-once.

Together with EffectsSurviveRestart’s at-least-once delivery this is the exactly-once property for consumption. It is not exactly-once delivery: the same bundle may arrive any number of times, and nothing here says it arrives at all.

Proof. Four filters, one per way a repeat can present itself:

• Redelivery. select_message_bundles drops bundles below the inbox’s next_block_height_to_receive, which has advanced past every height already received.
• Order. Should one slip through, Inbox::add_bundle requires the Cursor to be at least next_cursor_to_add — set to the previous cursor plus one on every successful add — and fails with InboxError::IncorrectOrder otherwise.
• Anticipation. A bundle consumed before it arrived sits in removed_bundles; on arrival it is matched by cursor, checked for equality and deleted rather than queued, so it is never offered for consumption a second time.
• Checkpoint restore. A bundle below restored_cursor is dropped, its effects being already part of the restored state.

Consumption itself removes the bundle: remove_bundles_from_inboxes pops it from added_bundles, and by IncomingBundlesMatchTheLocalInbox a correct validator does not vote for a block consuming a bundle that is not there. ∎

Scoped to one validator. Every clause above is about one validator’s own inboxes. That all correct validators consume the same bundles in the same blocks follows from agreement on the block sequence (UniqueChain), not from anything here.

Implementors