Trait RoundFloor 

pub trait RoundFloor { }

Lemma (Round floor). Let M denote

M = max( { ownership.first_round() }
       ∪ { ownership.next_round(timeout.round)  (or Round::Validator(u32::MAX) if none) }
       ∪ { locking_block.round() }
       ∪ { proposed.content.round }
       ∪ { signed_proposal.content.round } )

over whichever of the four optional fields are Some. Then the private ChainManager::update_current_round sets current_round to max(current_round, M), and resets round_timeout from ChainOwnership::round_timeout exactly when that raises the value.

Proof. Direct reading of the method: it builds an iterator over the four optional fields, mapping the timeout certificate through ownership.next_round(..).unwrap_or(Round::Validator( u32::MAX)), takes .max(), applies .unwrap_or_default() — and Round::default() is Round::Fast, the minimum (RoundOrder), so this adds nothing — and then .max(self.ownership.get().first_round()). That is M. It then returns early on current_round <= self.current_round(), and otherwise sets both round_timeout and current_round. ∎

Implementors