Trait HeightProgress 

pub trait HeightProgress:
    RoundProgress
    + TipAdvancesOnlyOnValidCertificate
    + CommitAgreement { }

Theorem (Height progress). Under the same assumptions, once the driver has a block to propose at height h, a block at height h is committed within finite time after GST, and every correct validator’s ChainTipState::next_block_height reaches h + 1 — provided it is reachable and receives the certificate.

Proof. Commitment at h is RoundProgress. For the observable half: the driver’s ChainClient::process_pending_block ends by calling Client::update_validators with the new ConfirmedBlockCertificate, which delivers it to every validator; a correct recipient runs ChainWorkerState::process_confirmed_block, which verifies it and — since the block is contiguous with the recipient’s tip, h being the pending height — executes it and advances ChainTipState::next_block_height to h + 1 (TipAdvancesOnlyOnValidCertificate). By CommitAgreement the block it records is the same at all of them. ∎

The proviso is not removable and is not a defect: a validator that is partitioned away, or that has been down since before GST, simply has not received the certificate yet. It catches up through the ordinary certificate-download path, since the certificate is by then durable at a quorum.

Implementors