Module voting 

Voting rules: what a correct validator’s state must look like for it to sign.

These are local implementation properties. Each one follows from a single method’s control flow together with the guards its call sites apply, with no induction over executions. They are what crate::manager::proof::locking inducts over, and what CertificateCarriesCorrectVote converts into constraints on the certificates that can exist at all.

Every statement below is accompanied by a code correspondence table naming the method that implements the transition, the fields it reads and writes, and the preconditions its callers establish.

Traits

ConfirmationNeedsValidatedCertificate

Lemma (A non-fast confirmation requires a validated certificate in the same round). If a correct validator casts a confirmation vote for block A in a round r other than Round::Fast, then a ValidatedBlockCertificate for A in round r, valid for the committee of its epoch, existed at that moment.

ConfirmationOnlyInCurrentRound

Lemma (A non-fast confirmation happens only in the current round). When ChainManager::create_final_vote casts a confirmation vote in round r, ChainManager::current_round equals r at that moment — and it had already been raised to at least r earlier in the same call.

FastConfirmationNeedsEmptyLock

Lemma (A fast confirmation requires an empty lock and no prior vote). If a correct validator casts a confirmation vote in Round::Fast, then immediately before that vote its locking_block, validated_vote and confirmed_vote were all None; and immediately after, locking_block holds a LockingBlock::Fast for the very block confirmed.

NoValidationInFastRound

Lemma (No validation vote in the fast round). A correct validator never casts a Validated vote in Round::Fast.

ProposalGate

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.

UnlockingRequiresHigherCertificate

Lemma (A validation vote past a lock needs a higher certificate). Suppose a correct validator casts a validation vote for block B in round r, and let (A, p) be the value of its confirmed_vote immediately before. Then p is defined only if the proposal carried an OriginalProposal, and:

ValidationRoundStrictlyIncreases

Lemma (Validation rounds strictly increase). If a correct validator’s validated_vote holds a vote in round s, it casts no further validation vote in any round ≤ s while that field still holds that vote.

VoteConstructionSites

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: