pub trait LockRoundMonotone: Lock + ConsensusInstance { }Expand description
Invariant (The lock round never decreases). Within one consensus instance, the lock round is non-decreasing.
Proof. By the writer table in the module documentation, locking_block is
written only by the private update_locking, by ManagerSafetySnapshot::restore, and by
reset (which by ConsensusInstance ends the instance).
update_locking begins with
if let Some(old_locked) = self.locking_block.get() {
if old_locked.round() >= locking.round() { return Ok(()); }
}so it writes only a strictly higher round. All four call sites go through it: the two
update_locking calls in the Regular and Fast arms of create_vote’s match, the one
in the None arm, and the one in create_final_vote.
ManagerSafetySnapshot::restore is handled by SafetyStateRecovery. ∎