Trait SingleLeaderRoundsNeedTimeout 

pub trait SingleLeaderRoundsNeedTimeout: RoundFloor + CertificateCarriesCorrectVote { }

Lemma (Which rounds can be skipped without a timeout). For a correct validator:

• a SingleLeader round above SingleLeader(0), and any Validator round, is left only via a TimeoutCertificate or a locking block in a higher round;
• Round::Fast and MultiLeader rounds are additionally left by any authenticated proposal in a higher round.

Proof. By RoundFloor the round can rise only from a timeout certificate, the lock, or proposed / signed_proposal. For the proposal inputs:

• ChainManager::update_signed_proposal returns false immediately for proposal.content.round > Round::SingleLeader(0), so signed_proposal never carries a higher round;
• proposed is written only by the private update_proposed, called from ChainManager::create_vote, which by ProposalGate runs only after ChainManager::check_proposed_block returned Accept; and that method requires new_round == current_round on the Round::SingleLeader(_) | Round::Validator(_) arm, so it cannot raise the round either. On the MultiLeader(_) | SingleLeader(0) arm it requires only new_round >= current_round, which can raise it.

The lock case is not an exception to the intent: a LockingBlock::Regular in round r is a ValidatedBlockCertificate, hence by CertificateCarriesCorrectVote evidence that a quorum — including a correct validator — was already in round r. So the validator is following the round the chain has demonstrably reached, not being pushed past a leader’s turn. ∎

Implementors