pub trait DeliveryAndConsumptionAreOrdered: InboxHoldsOnlySentBundles { }Expand description
Lemma (Bundles are delivered and consumed in order). For a given (sender, recipient) pair,
bundles enter an inbox in strictly increasing Cursor order and are consumed in strictly
increasing cursor order. A bundle may be passed over only if every message in it is skippable.
Proof. Three guards, one per way order could break.
Within a batch. ChainWorkerState::select_message_bundles walks the incoming bundles and
rejects the request with WorkerError::InvalidCrossChainRequest unless their heights are
non-decreasing, so a batch is already ordered when it reaches the inbox.
Across batches, on delivery. Inbox::add_bundle requires cursor >= next_cursor_to_add and
fails with InboxError::IncorrectOrder otherwise, then sets next_cursor_to_add to
cursor + 1. Delivery positions are therefore strictly increasing.
On consumption. Inbox::remove_bundle requires cursor >= next_cursor_to_remove on the same
terms. Before consuming, it drains queued bundles below that cursor — and each one must satisfy
is_skippable(), or the block is rejected with InboxError::UnskippableBundle. ∎
What “skippable” excludes is the point. PostedMessage::is_skippable is false for
MessageKind::Protected and MessageKind::Tracked unconditionally, and false for Simple or
Bouncing messages carrying a non-zero grant. So a recipient may leave ordinary zero-grant
messages unconsumed, and may not silently drop a protected or tracked one, or one carrying funds:
consuming a later bundle forces it to account for those first. Ordering here is a safety
property — it constrains which blocks are valid — not a delivery guarantee.