pub trait VoteConstructionSites: CorrectValidator { }Expand description
Lemma (Vote construction sites). A correct validator signs a block-related vote only in
ChainManager::create_vote and ChainManager::create_final_vote, and a timeout vote only
in ChainManager::create_timeout_vote and ChainManager::vote_fallback. Specifically:
| vote kind | round of the vote | sole producer |
|---|---|---|
Validated | proposal.content.round, never Round::Fast | ChainManager::create_vote, else branch |
Confirmed | Round::Fast | ChainManager::create_vote, if round.is_fast() branch |
Confirmed | validated.round | ChainManager::create_final_vote |
Timeout | ChainManager::current_round | ChainManager::create_timeout_vote |
Timeout | Round::SingleLeader(u32::MAX) | ChainManager::vote_fallback |
Proof. By ValidatorVote, a vote exists only if one of Vote::new,
Vote::new_with_unlocking_round or Vote::new_with_first_round was called with the
validator’s key. Outside test-only code there are exactly five such calls in the workspace,
all in linera_chain::manager, and they are the five rows above: Vote::new in
create_timeout_vote and in vote_fallback; Vote::new_with_first_round in the
fast-round branch of create_vote and in create_final_vote;
Vote::new_with_unlocking_round in the non-fast branch of create_vote. In each case the
round passed is the one tabulated: create_vote passes proposal.content.round, guarded
by round.is_fast() into one branch or the other; create_final_vote passes
validated.round; create_timeout_vote passes its round argument, which it has just
checked to equal ChainManager::current_round; vote_fallback passes the constant
Round::SingleLeader(u32::MAX). By CorrectValidator no other code path of a correct
validator holds its key. ∎
Where this is fragile. The claim is an exhaustive-search argument over call sites, so it
is invalidated by adding a sixth call. A new signing site must either be shown to preserve
OneValidationVotePerRound and OneConfirmationVotePerRound, or be added to this table.