Module liveness 

The liveness theorems, and a precise account of what they exclude.

Everything here is conditional on the assumptions in super::assumptions, all of which can fail without endangering CommitAgreement. Read LivenessScope alongside UnboundedProgress: several natural readings of “the protocol makes progress” are not implied, and the differences are design choices rather than oversights.

Traits

HeightProgress

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.

LivenessScope

Remark (What liveness does not claim). Five exclusions, each of which a reader may reasonably expect UnboundedProgress to cover.

RoundProgress

Theorem (Round progress). Consider a chain with at least one regular owner, at a height whose consensus instance has not yet committed. Under ActiveCorrectDriver and the other assumptions of super::assumptions, there is a round r beginning after GST such that the height commits during r.

UnboundedProgress

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.