Skip to main content

TimeoutCertificateProvesRoundReached

Trait TimeoutCertificateProvesRoundReached 

Source
pub trait TimeoutCertificateProvesRoundReached: TimeoutVoteConditions + CertificateCarriesCorrectVote { }
Expand description

Lemma (A timeout certificate proves a correct validator’s round expired). If a valid TimeoutCertificate is certified in round r for a chain and height, then some correct validator was in round r at that height, with a configured round timeout that had elapsed.

Proof. By CertificateCarriesCorrectVote a correct validator cast a timeout vote with the certificate’s payload, whose round is r. By TimeoutVoteConditions its ChainManager::current_round was r and its round_timeout had elapsed. ∎

This is what makes a timeout certificate meaningful rather than merely well-formed: it cannot be manufactured by faulty validators ahead of time, because a quorum contains a correct validator whose own clock had to have passed the deadline.

Implementors§