Trait VoteRoundBelowCurrentRound 

pub trait VoteRoundBelowCurrentRound:
    VoteConstructionSites
    + ProposalGate
    + RoundFloor
    + CurrentRoundMonotone
    + ConfirmationOnlyInCurrentRound { }

Invariant (A cast vote never exceeds the current round). Immediately after a correct validator casts a validation or confirmation vote in round r, its current_round is at least r; and by CurrentRoundMonotone it stays at least r for the rest of the instance.

Proof. By VoteConstructionSites there are three cases.

Validation vote in round r (non-fast branch of ChainManager::create_vote). Before signing, the method calls update_proposed(proposal.clone(), blobs) and then update_current_round(local_time). After update_proposed, proposed is Some with a round ≥ r: either it was None or held a lower round, and the proposal was stored with round r; or it already held a round ≥ r and the write was skipped. By RoundFloor, update_current_round then raises current_round to at least proposed.content.round ≥ r.

Confirmation vote in Round::Fast (fast branch of ChainManager::create_vote). Same call sequence; and Round::Fast is the minimum round (RoundOrder), so the claim is immediate.

Confirmation vote in round r (ChainManager::create_final_vote). Immediate from ConfirmationOnlyInCurrentRound, which gives current_round == r. ∎

Implementors