Trait OneValidationVotePerRound 

pub trait OneValidationVotePerRound:
    ProposalGate
    + CastValidationRoundFloor
    + ValidationRoundStrictlyIncreases
    + DurablePersistence
    + SequentialChainState { }

Lemma (One validation vote per round). A correct validator casts at most one validation vote per round of an instance.

Proof. Suppose it casts validation votes for B₁ and then B₂ in the same round s. By ProposalGate the second was preceded by ChainManager::check_proposed_block returning Accept for a proposal in round s, so both of its round guards held at that moment:

• ensure!(new_round > vote.round) for validated_vote, and
• ensure!(locking_block.round() < new_round) for the lock.

Together these give max(validated_vote.round, lock round) < s, contradicting CastValidationRoundFloor, which the first vote established. (Where “the same vote” is re-submitted rather than a different block, ChainManager::check_proposed_block returns Outcome::Skip on its first branch and nothing is signed.)

The argument needs the two votes to be observed by the same manager state, which is DurablePersistence — a validator that lost its state across a crash could sign twice — and SequentialChainState, which rules out two concurrent handlers each seeing the pre-vote state. ∎

Implementors