Trait ConfirmedVoteRoundMonotone 

pub trait ConfirmedVoteRoundMonotone:
    ConfirmationOnlyInCurrentRound
    + FastConfirmationNeedsEmptyLock
    + VoteRoundBelowCurrentRound
    + CurrentRoundMonotone { }

Invariant (The confirmed-vote round never decreases). Within one consensus instance, if confirmed_vote is Some with round p, it never later holds a vote with round < p.

Proof. By the writer table in the module documentation the field has three in-instance writers.

create_final_vote at round r. By ConfirmationOnlyInCurrentRound it writes only when current_round == r. If a previous confirmation vote had round p, then by VoteRoundBelowCurrentRound the current round was ≥ p at that time, and by CurrentRoundMonotone it still is. Hence r = current_round ≥ p.

create_vote, fast branch. Writes a vote in Round::Fast, the minimum round — but by FastConfirmationNeedsEmptyLock this branch is reachable only when confirmed_vote was None, so there is no earlier round to undercut.

ManagerSafetySnapshot::restore. See SafetyStateRecovery. ∎

Implementors