pub trait ChainTilesRounds { }Expand description
Lemma (A sound chain tiles every round below the confirmation). Let a valid
ConfirmedBlockCertificate in round s carry a non-empty chain with link rounds
ρ₀ < ρ₁ < … < ρₖ. Then ρₖ = s, link i was cast under unlocking round ρᵢ₋₁ (and link 0
under None), and the half-open windows
[⊥, ρ₀), [ρ₀, ρ₁), …, [ρₖ₋₁, ρₖ)partition the rounds strictly below s. In particular every round r < s lies in exactly one
link’s window.
Proof. JustificationChain::verify rejects unless the rounds strictly increase, and
LiteCertificate::check on a Confirmed certificate with a non-empty chain requires
top == self.round, i.e. ρₖ = s. JustificationChain::commitment folds the chain from the
bottom, setting each link’s unlocking_round to the round of the link below and None for the
first — so the reconstructed payload of link i carries unlocking round ρᵢ₋₁, which is the
window’s lower bound; the upper bound ρᵢ is where the link’s own votes were cast. Consecutive
windows abut and the first is unbounded below, so their union is [⊥, ρₖ) = [⊥, s). ∎
This is what makes the chain walk in extract_equivocations exhaustive rather than
best-effort: a lower confirmation cannot slip between two links.