pub trait InboxHoldsOnlySentBundles: CorrectValidator + SequentialChainState { }Expand description
Lemma (An inbox holds only bundles its origin really sent). Every MessageBundle in a
correct validator’s inbox for an origin was produced by a block of that origin which the same
validator has processed.
Proof. Bundles enter an inbox at exactly one place, Inbox::add_bundle, reached only from
ChainWorkerState::process_cross_chain_update. That handler serves a
CrossChainRequest::UpdateRecipient, and cross-chain requests are internal to one validator:
linera_rpc routes each to the shard owning the target chain, so the request comes from
another worker of the same validator, which built it in build_network_actions from its own
persisted outbox for a block it had processed (EffectsSurviveRestart, sender half). No
other validator’s word enters, and by SequentialChainState no other process writes this
chain’s inboxes. select_message_bundles additionally drops bundles whose epoch has been
revoked, unless they were already anticipated. ∎
This is the premise IncomingBundlesMatchTheLocalInbox leaves open: that lemma proves a voter
matches consumed bundles against its own inbox, which is worth exactly as much as the inbox’s
own provenance.