pub trait TipAdvancesOnlyOnValidCertificate { }Expand description
Lemma (The tip advances only on a verified certificate). A correct validator’s
ChainTipState::next_block_height passes from h to h + 1, and its
block_hashes records a hash at h, only for a block carried by a
ConfirmedBlockCertificate that has passed check against the committee of the block’s
epoch.
Proof. The tip register is advanced in one place in linera_chain::chain, at the end of
ChainStateView::apply_confirmed_block (tip.next_block_height.try_add_assign_one()).
That method has a single call site in the workspace outside tests, in
ChainWorkerState::execute_contiguous_block; execute_block_with_checkpoint_restore reaches
it by delegating there after installing the snapshot. Both are reached only through
ChainWorkerState::process_confirmed_block, whose every non-early-return path first
evaluates certificate.check(&committee)? with committee fetched for block.header.epoch.
The early returns — the tip.next_block_height > height skip and the Preprocess dispatch —
do not advance the tip. ∎
Where this is fragile. ChainStateView::apply_confirmed_block is pub, on a type this
crate re-exports, and it takes a ConfirmedBlock and no Committee — so it cannot verify
anything, and nothing about its signature confines it to verified callers. The enumeration
above holds by current usage, not by visibility. A new caller must perform the certificate
check itself.
Two paths deserve explicit mention because they weaken the precondition without weakening
this lemma. pre_checkpoint_block_trust lets a hash recorded by an earlier checkpoint
certificate bypass the already-processed skip; and a checkpoint block may install a state
snapshot rather than replay its ancestors. Neither bypasses certificate.check, so a block
entering the tip is always quorum-certified; what they bypass is the re-execution of
ancestors, which is a matter of state-transition correctness rather than of agreement.