pub trait CommitRestsOnValidation: CertificateCarriesCorrectVote + ConfirmationNeedsValidatedCertificate { }Expand description
Lemma (A commit outside the fast round rests on a validated block certificate). If a
ConfirmedBlockCertificate for B is certified in a round r other than
Round::Fast, then a valid
ValidatedBlockCertificate for B in the same round r exists.
Proof. By CertificateCarriesCorrectVote some correct validator cast a confirmation vote
for B in round r. By ConfirmationNeedsValidatedCertificate, since r is not the fast
round, a valid ValidatedBlockCertificate for B in round r existed when it did so. ∎
This is what lets the safety argument reason exclusively about validated certificates: every commit above the fast round is backed by one, in its own round.