pub trait UnboundedProgress: HeightProgress + UniqueChain { }Expand description
Theorem (Unbounded progress). If a correct driver (ActiveCorrectDriver) keeps
supplying blocks to propose — never exhausting its stream of operations — then under the
assumptions of super::assumptions every correct, reachable validator’s
ChainTipState::next_block_height grows without bound, and by UniqueChain the
validators’ committed prefixes remain identical throughout.
Proof. Induction on the height. Given that height h has committed and every correct
reachable validator has advanced to h + 1 (HeightProgress), each such validator’s
ChainStateView::reset_chain_manager has created the consensus instance for h + 1
(ConsensusInstance) with its round reset to
ChainOwnership::first_round. The hypotheses of RoundProgress then hold again at
h + 1: GST has passed, the driver has a block, and EventuallyCorrectLeader applies to
the fresh instance since the leader seed is the new height. So h + 1 commits, and the
induction continues. Uniqueness of what is committed at each height is UniqueChain. ∎
Note that the round numbering restarts at each height, so the round-timeout argument of
RoundProgress restarts too: each height may again spend a bounded number of rounds before
its timeout exceeds T. This costs latency, not liveness.