Trait ValidationRoundStrictlyIncreases 

pub trait ValidationRoundStrictlyIncreases: ProposalGate { }

Lemma (Validation rounds strictly increase). If a correct validator’s validated_vote holds a vote in round s, it casts no further validation vote in any round ≤ s while that field still holds that vote.

Code correspondence.

transition	ChainManager::check_proposed_block
reads	proposed, validated_vote, locking_block, confirmed_vote, current_round, ownership
writes	nothing
precondition	none
establishes	this lemma, UnlockingRequiresHigherCertificate

Proof. By ProposalGate a validation vote in round r requires ChainManager::check_proposed_block to have returned Accept for a proposal in round r. That method contains

if let Some(vote) = self.validated_vote() {
    ensure!(new_round > vote.round, ChainError::InsufficientRoundStrict(vote.round));
}

so Accept with validated_vote == Some(_, s) requires r > s. ∎

Note the qualifier “while that field still holds that vote”: ChainManager::create_final_vote clears validated_vote, so this lemma alone does not give a per-round bound over the whole life of an instance. CastValidationRoundFloor supplies what is missing.

Implementors