Module rounds 

The round register: what current_round means, and why it only ever grows.

These are the first genuinely inductive results: they quantify over all reachable states of one consensus instance (ConsensusInstance). They are used by both the locking invariants and round advancement, so they are stated once, here.

Traits

CurrentRound

Definition (Current round). The current round of an instance is ChainManager::current_round, the lowest round in which the validator is still willing to vote. It is the round to which round_timeout applies.

CurrentRoundMonotone

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

RoundFloor

Lemma (Round floor). Let M denote

VoteRoundBelowCurrentRound

Invariant (A cast vote never exceeds the current round). Immediately after a correct validator casts a validation or confirmation vote in round r, its current_round is at least r; and by CurrentRoundMonotone it stays at least r for the rest of the instance.