linera_chain/proof/
epochs.rs

1// Copyright (c) Zefchain Labs, Inc.
2// SPDX-License-Identifier: Apache-2.0
3
4//! Committees, epochs, and how a node comes to trust one.
5//!
6//! A committee is identified by an [`Epoch`], and epochs are managed on the admin chain: created by
7//! [`AdminOperation::CreateCommittee`], retired by [`AdminOperation::RemoveCommittee`]. Every
8//! certificate is judged by the committee for the epoch its block declares, so before anything can
9//! be verified a node must know which committee that is.
10//!
11//! This module is about where that knowledge comes from. The results here are what let the rest of
12//! the specification induct on epochs at all.
13//!
14//! [`Epoch`]: linera_base::data_types::Epoch
15//! [`AdminOperation::CreateCommittee`]: linera_execution::system::AdminOperation::CreateCommittee
16//! [`AdminOperation::RemoveCommittee`]: linera_execution::system::AdminOperation::RemoveCommittee
17
18use crate::manager::proof::model::CorrectValidator;
19
20/// **Theorem (No committee certifies its own introduction).** For every epoch, a node can learn
21/// that epoch's committee only from evidence certified under a *strictly earlier* epoch, or — for
22/// epoch zero alone — from network configuration that is not a certificate at all. The relation
23/// "the committee for `e` was learned from a certificate in epoch `e'`" is therefore well founded,
24/// with `e' < e`.
25///
26/// This is what makes induction on the epoch legitimate, and it is the property a reconfiguration
27/// scheme is easiest to get wrong. Were a committee able to authenticate the evidence that
28/// introduces it — a per-chain genesis configuration naming a committee would do it — an attacker
29/// who could produce such a configuration could mint a committee out of nothing and have it vouch
30/// for itself. Nothing here would detect that, because every signature would check out.
31///
32/// *Code correspondence.*
33///
34/// | | |
35/// |---|---|
36/// | transition | `ExecutionRuntimeContext::get_committee_hashes`, reached from `ChainWorkerState::committee_for_epoch` before `certificate.check` |
37/// | reads | for epoch `0`, `NetworkDescription::genesis_committee_blob_hash`; otherwise the admin chain's [`EPOCH_STREAM_NAME`] event at index `epoch` |
38/// | writes | nothing |
39/// | failure | `ExecutionError::EventsNotFound` when the epoch's event is absent, so the certificate is not verified rather than verified optimistically |
40///
41/// *Proof.* By descent on the epoch.
42///
43/// *The base is not a certificate.* Epoch `0` resolves to
44/// `NetworkDescription::genesis_committee_blob_hash`. A [`NetworkDescription`] is configuration a
45/// node is given, network-wide and identical for every chain. No chain can introduce one, and in
46/// particular creating a chain cannot introduce a committee — the failure mode this theorem exists
47/// to exclude.
48///
49/// *Every step descends.* For `epoch > 0` the committee hash is read from the event at index
50/// `epoch` of the admin chain's epoch stream, written by [`AdminOperation::CreateCommittee`]. To
51/// hold that event a node must have processed the admin-chain block containing it, which by
52/// [`TipAdvancesOnlyOnValidCertificate`] required a valid certificate for that block, judged
53/// against the committee for the epoch that block *declares*. A block declares the epoch its chain
54/// was in before executing, and a block advances the epoch at most once
55/// ([`ChainError::MultipleEpochAdvances`]), so the block introducing epoch `e` declares at most
56/// `e - 1`.
57///
58/// *There is no other route.* `committee_for_epoch` is the sole path from an epoch to a committee
59/// on the verification path, and it consults exactly these two sources. When the event is missing
60/// it fails with `EventsNotFound`; nothing falls back to a committee carried by the certificate
61/// being checked, or by the block, or by the chain being created. ∎
62///
63/// **A missing epoch is recoverable, which is why the strictness costs nothing.** Refusing to
64/// verify a certificate whose epoch a node has not yet learned would be an availability problem if
65/// there were no way to catch up. There is: `EventsNotFound` on the admin chain's stream is a class
66/// in `linera_core::proof::availability::MissingDependenciesAreRecoverable`, and
67/// `send_confirmed_certificate` answers it by pushing the admin chain to that validator before
68/// retrying. So the node learns the epoch and then verifies, in that order — which is the whole
69/// point.
70///
71/// [`EPOCH_STREAM_NAME`]: linera_execution::system::EPOCH_STREAM_NAME
72/// [`NetworkDescription`]: linera_base::data_types::NetworkDescription
73/// [`AdminOperation::CreateCommittee`]: linera_execution::system::AdminOperation::CreateCommittee
74/// [`TipAdvancesOnlyOnValidCertificate`]: crate::manager::proof::commit::TipAdvancesOnlyOnValidCertificate
75/// [`ChainError::MultipleEpochAdvances`]: crate::ChainError::MultipleEpochAdvances
76pub trait CommitteeKnowledgeIsWellFounded: CorrectValidator {}
linera_chain/proof/epochs.rs

linera_chain/proof/
epochs.rs
