pub trait TimeoutCertificateAdvancesRound: RoundFloor + CurrentRoundMonotone { }Expand description
Lemma (A timeout certificate advances the round). After a correct validator processes a
valid TimeoutCertificate for round r at its pending height, its
ChainManager::current_round is at least ChainOwnership::next_round(r), or
Round::Validator(u32::MAX) if that is None.
Code correspondence.
| transition | ChainManager::handle_timeout_certificate |
| reads | timeout |
| writes | timeout, and via update_current_round: current_round, round_timeout |
| precondition | certificate.check(committee), epoch equality and pending-height equality, all checked by ChainWorkerState::process_timeout |
Proof. ChainManager::handle_timeout_certificate returns early when the stored
timeout is already in a round ≥ r; otherwise it stores the certificate and calls
update_current_round. In the first case the stored certificate’s round r' ≥ r, and a
previous application of this lemma already raised the round to next_round(r') ≥ next_round(r)
by monotonicity of ChainOwnership::next_round together with CurrentRoundMonotone. In
the second, RoundFloor includes next_round(timeout.round) in the maximum. ∎