linera_core/proof/mod.rs
1// Copyright (c) Zefchain Labs, Inc.
2// SPDX-License-Identifier: Apache-2.0
3
4//! The progress and liveness half of the microchain consensus correctness specification.
5//!
6//! The safety half is in [`linera_chain::manager::proof`] and does not depend on anything here.
7//! This half does the reverse: it cites the chain crate's voting, locking and timeout results
8//! throughout, and adds the assumptions that mention time and availability.
9//!
10//! | module | contents |
11//! |---|---|
12//! | [`assumptions`] | synchrony, availability, leader fairness, timeout growth, reachability |
13//! | [`availability`] | what a certified block guarantees to everyone else, and what a crash costs |
14//! | [`progress`] | the individual steps a correct driver can force after GST |
15//! | [`liveness`] | the liveness theorems, and what they exclude |
16//! | [`notifications`] | what a notification tells a client, and why no proof relies on one |
17//! | [`storage`] | what may be assumed about anything read back from storage |
18//!
19//! The `linera-spec` crate gives the reading order across both crates.
20//!
21//! # Why liveness lives in this crate
22//!
23//! A Linera validator does not propose blocks and does not advance rounds on its own. Both are
24//! done by a [`ChainClient`](crate::client::ChainClient) run by a chain owner — which is why
25//! [`assumptions::ActiveCorrectDriver`] is an assumption rather than a lemma, and why the
26//! progress lemmas cite `linera_core::client` rather than `linera_chain::manager`. Placing them
27//! here keeps every statement next to the code that discharges it.
28
29pub mod assumptions;
30pub mod availability;
31pub mod liveness;
32pub mod notifications;
33pub mod progress;
34pub mod storage;