linera_chain/manager/proof/mod.rs
1// Copyright (c) Zefchain Labs, Inc.
2// SPDX-License-Identifier: Apache-2.0
3
4//! The consensus correctness argument for the chain manager, from the system model to the
5//! safety theorem.
6//!
7//! This is the chain-crate half of the specification; the progress and liveness half lives in
8//! `linera_core::proof`, which cites into here, and accountability lives in
9//! [`crate::justification::proof`]. The `linera-spec` crate gives the reading order across all
10//! of them and explains the conventions.
11//!
12//! # Layout
13//!
14//! | module | contents |
15//! |---|---|
16//! | [`model`] | system model, and the assumptions safety rests on |
17//! | [`voting`] | voting rules: what a correct validator's state must be for it to sign |
18//! | [`rounds`] | the round register: what it means, and why it only grows |
19//! | [`locking`] | locking invariants, proved by induction over an instance's transitions |
20//! | [`commit`] | the commit rule, and what a node does when a block commits |
21//! | [`safety`] | the safety theorem: at most one block per chain and height |
22//! | [`timeouts`] | how a height leaves a round it cannot finish in, for the progress argument |
23//!
24//! The single most important statement is [`safety::CommitAgreement`]; the single most
25//! substantial proof is [`safety::LockPreservation`].
26//!
27//! # What is proved, in one paragraph
28//!
29//! A correct validator will not cast a validation vote for a block it has not been shown a
30//! justification for, and will not confirm a block that a quorum has not validated in the very
31//! round it confirms in ([`voting`]). Its lock and its cast-vote rounds only ever move up
32//! ([`rounds`], [`locking`]), so it votes at most once per round and per kind. Any two quorums
33//! share a correct validator ([`crate::data_types::proof::quorum`]), so those per-validator
34//! limits become per-round limits on the certificates that can exist. Finally, a validator
35//! abandons a block it confirmed only in exchange for a certificate strictly above its own
36//! confirmation round, which lets an induction over rounds show that once a block is committed,
37//! no later round validates anything else ([`safety::LockPreservation`]) — hence at most one
38//! block per height is ever committed ([`safety::CommitAgreement`]).
39
40pub mod commit;
41pub mod locking;
42pub mod model;
43pub mod rounds;
44pub mod safety;
45pub mod timeouts;
46pub mod voting;