Trait ProposalGate 

pub trait ProposalGate: SequentialChainState { }

Lemma (Proposal gate). A correct validator reaches ChainManager::create_vote for a proposal p only after ChainManager::check_proposed_block returned Outcome::Accept for p against the same manager state.

Similarly, it reaches ChainManager::create_final_vote for a certificate c only after ChainManager::check_validated_block returned Outcome::Accept for c, and after c.check(committee) succeeded.

Proof. Both methods have exactly one caller in the workspace outside tests, in linera_core::chain_worker::state:

• create_vote is called at the end of ChainWorkerState::try_handle_block_proposal, which earlier matches on chain.manager.check_proposed_block(&proposal) and returns without voting on both non-Accept arms — Ok(Outcome::Skip) returns the unchanged chain info, and Err(_) returns the error (after, at most, recording the proposal via ChainManager::update_signed_proposal, which casts no vote).
• create_final_vote is called at the end of ChainWorkerState::process_validated_block, which earlier evaluates certificate.check(&committee)? and then should_skip_validated_block()?, a closure wrapping chain.manager.check_validated_block(&certificate). A Skip outcome returns early; an Err propagates via ?. Only Ok(Accept) falls through.

By SequentialChainState no other transition on this instance interleaves, so the state the guard inspected is the state create_vote / create_final_vote then mutates. ∎

Where this is fragile. The guards are at the call sites, not inside the signing methods: create_final_vote in particular re-checks only ChainManager::current_round, and would happily sign a second confirmation in the same round if invoked directly. A new caller must replicate the guards. This is the single largest gap between “the module is correct” and “the module cannot be misused”.

Implementors