Trait ValidationQuorumForms 

pub trait ValidationQuorumForms:
    ProposalAccepted
    + CorrectValidatorsFormQuorum
    + CorrectValidatorAvailability
    + EventualSynchrony { }

Lemma (The validation quorum forms). Under the hypotheses of ProposalAccepted, the driver obtains a valid ValidatedBlockCertificate for its block in round r within 2Δ plus local processing.

Proof. By ProposalAccepted every correct validator accepts the proposal, so ChainWorkerState::try_handle_block_proposal reaches ChainManager::create_vote, which — r not being the fast round — signs a validation vote for the block in round r. Every such vote carries the same signed payload: same block hash, same round, and the same unlocking_round/justification_commitment pair, which ChainManager::create_vote derives from the proposal’s own Regular certificate — identical across validators because the proposal is. So all correct votes fall into one group of communicate_with_quorum, which by CorrectValidatorsFormQuorum reaches the quorum threshold; by CorrectValidatorAvailability and EventualSynchrony they arrive within Δ. Client::submit_block_proposal assembles them into a certificate, whose justification chain is the retried certificate’s full_justification. ∎

Note the blob preconditions: a validator missing a blob the proposal requires answers WorkerError::BlobsNotFound instead of voting. That does not cost a round. The retry is per-validator, inside RemoteNodeUpdater::send_block_proposal‘s loop: the arm matching BlobsNotFound | InactiveChain sends the proposal’s published blobs with send_pending_blobs and re-submits to that validator alone, so the other validators’ votes are unaffected and the quorum round is not restarted. It terminates because the loop drains its blob_ids — the set is fixed by the proposal and each pass takes it with mem::take. So the 2Δ bound above absorbs it as a constant factor rather than an extra round of the protocol.

Implementors