Trait FinalizationQuorumForms 

pub trait FinalizationQuorumForms:
    ValidationQuorumForms
    + ConfirmationOnlyInCurrentRound
    + ConfirmationNeedsValidatedCertificate
    + CommittedBlock
    + CorrectValidatorsFormQuorum { }

Lemma (The finalization quorum forms). Given a valid ValidatedBlockCertificate for block B in round r, and every correct validator in round r after GST, the driver obtains a valid ConfirmedBlockCertificate for B within 2Δ plus local processing — so B becomes a CommittedBlock.

Proof. Client::finalize_block sends CommunicateAction::FinalizeBlock to every validator. A correct recipient runs ChainWorkerState::process_validated_block, which verifies the certificate, checks ChainManager::check_validated_block — whose guards are new_round ≥ validated_vote.round, satisfied since no correct validator voted above r, and new_round > locking_block.round(), satisfied since no lock in round r existed before this certificate — and calls ChainManager::create_final_vote. That signs, because by ConfirmationOnlyInCurrentRound it requires the current round to equal r, which holds by hypothesis and is re-established by its own update_locking/update_current_round prelude.

All confirmation votes again share one payload: the value is ConfirmedBlock::new(B), the round is r, and the first_round flag and justification commitment are derived from r and the certificate, identically at every validator. So they aggregate; CorrectValidatorsFormQuorum gives the threshold. Client::finalize_block then attaches the justification chain the quorum committed to and returns the certificate, which is a CommittedBlock by definition. ∎

Implementors