Trait CastValidationRoundFloor 

pub trait CastValidationRoundFloor:
    LockRoundMonotone
    + ProposalGate
    + ConfirmationOnlyInCurrentRound
    + VoteRoundBelowCurrentRound
    + CurrentRoundMonotone
    + RoundFloor { }

Invariant (Cast validation rounds leave a floor). If a correct validator has ever cast a validation vote in round s during an instance, then from that moment on

max(validated_vote.round, lock round) ≥ s

where an absent field contributes ⊥.

This is the invariant that survives create_final_vote clearing validated_vote, and it is what makes OneValidationVotePerRound hold over a whole instance rather than only between confirmations.

Proof. Induction over the transitions of the instance.

Base. Immediately after the vote, validated_vote is Some(_, s) — the non-fast branch of create_vote ends with self.validated_vote.get_mut().insert(vote).

Step. Only two transitions can lower either side of the maximum. The lock round is non-decreasing by LockRoundMonotone, so only validated_vote can fall, and by the writer table it is set to None in exactly two places:

• create_vote, fast branch (self.validated_vote.set(None)). Unreachable here: that branch requires ChainManager::check_proposed_block to have accepted a proposal in Round::Fast (ProposalGate), whose validated_vote guard ensure!(new_round > vote.round) is unsatisfiable for the minimum round unless validated_vote is already None; and if it is None, the induction hypothesis is carried by the lock, which this branch does not lower.
• create_final_vote at some round r. It clears the field only after update_locking(LockingBlock::Regular(validated), blobs) and only on the branch where a vote is cast, which by ConfirmationOnlyInCurrentRound requires current_round == r. By VoteRoundBelowCurrentRound and CurrentRoundMonotone, current_round ≥ s, so r ≥ s. By RoundFloor and LockRoundMonotone, after update_locking the lock round is ≥ r ≥ s. So the maximum is preserved by the lock. ∎

Implementors