Trait CurrentRoundMonotone 

pub trait CurrentRoundMonotone: RoundFloor + ConsensusInstance { }

Invariant (The current round never decreases). Within one consensus instance, current_round is non-decreasing over time.

Proof. The register has exactly two writers in the crate:

• ChainManager::update_current_round, which by RoundFloor assigns max(current_round, M) ≥ current_round;
• ChainManager::reset, which by ConsensusInstance ends the instance and begins the next one, so it is outside the scope of this invariant.

Every other mutation of the manager reaches the register only through update_current_round: it is called from ChainManager::create_vote, ChainManager::create_final_vote, ChainManager::handle_timeout_certificate, ChainManager::update_signed_proposal, and nowhere else. Note in particular that ManagerSafetySnapshot::restore does not write it — see SafetyStateRecovery for why that is nonetheless safe. ∎

Implementors