pub trait LivenessScope:
UnboundedProgress
+ RoundsWithoutTimeout
+ ActiveCorrectDriver
+ LockRecovery { }Expand description
Remark (What liveness does not claim). Five exclusions, each of which a reader may
reasonably expect UnboundedProgress to cover.
-
No progress without a client.
ActiveCorrectDriveris indispensable: a validator never proposes and never advances a round unprompted. A microchain whose owners have all gone away makes no progress and is not thereby faulty. This is the deepest structural difference from a validator-driven BFT protocol, and it is what makes a Linera validator’s per-chain cost proportional to use. -
The fast round can wedge a height permanently. By
RoundsWithoutTimeout, with the defaultTimeoutConfigthe fast round has no timeout at all, and while the current round is fast only a super owner may open a later one. A super owner that issues two conflicting fast proposals splits the correct validators — each locks onto the first it sees, byFastConfirmationNeedsEmptyLock— so neither reaches a quorum, and the height stops until that same super owner proposes again in a higher round.CommitAgreementis untouched; this is exactly the trade the fast path makes, and the reasonChainClient::process_pending_block_innerrefuses to replace a pending fast proposal whose signing key it no longer holds. -
Multi-leader rounds are not covered by
RoundProgress. The theorem is stated forSingleLeaderandValidatorrounds, where a unique leader is guaranteed byLeaderEligibility. In a multi-leader round several owners may propose simultaneously; correct validators then vote for whichever proposal they see first, quorums may not form, and byRoundsWithoutTimeouta non-final multi-leader round has no timeout — it is left only by a proposal in a higher round. This is by design (multi-leader rounds are the uncontended fast path) and costs nothing, because the round sequence passes through them into single-leader rounds where the theorem applies. -
No bound on the number of rounds, and no bound before GST.
RoundProgressasserts the existence of a successful round, not a bound on how many precede it. Faulty leaders and pre-GST delays each cost rounds. -
Nothing is claimed about the content of the committed blocks. A driver competing with other owners may find its own block superseded:
LockRecoveryobliges it to re-propose whatever is locked rather than its own pending block.process_pending_blockthen returns the committed certificate for the other block and keeps the driver’s proposal pending for a later height. Liveness of the chain does not imply liveness of any particular transaction.