linera_chain/manager/proof/
rounds.rs

1// Copyright (c) Zefchain Labs, Inc.
2// SPDX-License-Identifier: Apache-2.0
3
4//! The round register: what [`current_round`] means, and why it only ever grows.
5//!
6//! These are the first genuinely inductive results: they quantify over all reachable states of
7//! one consensus instance ([`ConsensusInstance`]). They are used by both the locking invariants
8//! and round advancement, so they are stated once, here.
9//!
10//! [`current_round`]: field@crate::manager::ChainManager::current_round
11//! [`ConsensusInstance`]: crate::manager::proof::model::ConsensusInstance
12
13use crate::manager::proof::{
14    model::ConsensusInstance,
15    voting::{ProposalGate, VoteConstructionSites},
16};
17
18/// **Definition (Current round).** The *current round* of an instance is
19/// [`ChainManager::current_round`], the lowest round in which the validator is still willing to
20/// vote. It is the round to which [`round_timeout`] applies.
21///
22/// It is a *derived* quantity: the register caches the maximum of the evidence the validator has
23/// seen that the chain has entered a round — a timeout certificate for the previous round, a
24/// locking block, or an authenticated proposal — floored at
25/// [`ChainOwnership::first_round`]. `RoundFloor` states exactly that.
26///
27/// [`ChainManager::current_round`]: method@crate::manager::ChainManager::current_round
28/// [`round_timeout`]: crate::manager::ChainManager::round_timeout
29/// [`ChainOwnership::first_round`]: linera_base::ownership::ChainOwnership::first_round
30pub trait CurrentRound {}
31
32/// **Lemma (Round floor).** Let `M` denote
33///
34/// ```text
35/// M = max( { ownership.first_round() }
36///        ∪ { ownership.next_round(timeout.round)  (or Round::Validator(u32::MAX) if none) }
37///        ∪ { locking_block.round() }
38///        ∪ { proposed.content.round }
39///        ∪ { signed_proposal.content.round } )
40/// ```
41///
42/// over whichever of the four optional fields are `Some`. Then the private
43/// `ChainManager::update_current_round` sets [`current_round`] to `max(current_round, M)`, and
44/// resets [`round_timeout`] from [`ChainOwnership::round_timeout`] exactly when that raises the
45/// value.
46///
47/// *Proof.* Direct reading of the method: it builds an iterator over the four optional fields,
48/// mapping the timeout certificate through `ownership.next_round(..).unwrap_or(Round::Validator(
49/// u32::MAX))`, takes `.max()`, applies `.unwrap_or_default()` — and `Round::default()` is
50/// [`Round::Fast`], the minimum ([`RoundOrder`]), so this adds nothing — and then
51/// `.max(self.ownership.get().first_round())`. That is `M`. It then returns early on
52/// `current_round <= self.current_round()`, and otherwise sets both
53/// [`round_timeout`] and [`current_round`]. ∎
54///
55/// [`current_round`]: field@crate::manager::ChainManager::current_round
56/// [`round_timeout`]: crate::manager::ChainManager::round_timeout
57/// [`ChainOwnership::round_timeout`]: linera_base::ownership::ChainOwnership::round_timeout
58/// [`Round::Fast`]: linera_base::data_types::Round::Fast
59/// [`RoundOrder`]: crate::manager::proof::model::RoundOrder
60pub trait RoundFloor {}
61
62/// **Invariant (The current round never decreases).** Within one consensus instance,
63/// [`current_round`] is non-decreasing over time.
64///
65/// *Proof.* The register has exactly two writers in the crate:
66///
67/// * `ChainManager::update_current_round`, which by [`RoundFloor`] assigns
68///   `max(current_round, M) ≥ current_round`;
69/// * [`ChainManager::reset`], which by [`ConsensusInstance`] ends the instance and begins the
70///   next one, so it is outside the scope of this invariant.
71///
72/// Every other mutation of the manager reaches the register only through
73/// `update_current_round`: it is called from [`ChainManager::create_vote`],
74/// [`ChainManager::create_final_vote`], [`ChainManager::handle_timeout_certificate`],
75/// [`ChainManager::update_signed_proposal`], and nowhere else. Note in particular that
76/// [`ManagerSafetySnapshot::restore`] does **not** write it — see [`SafetyStateRecovery`] for
77/// why that is nonetheless safe. ∎
78///
79/// [`current_round`]: field@crate::manager::ChainManager::current_round
80/// [`ChainManager::reset`]: crate::manager::ChainManager::reset
81/// [`ChainManager::create_vote`]: crate::manager::ChainManager::create_vote
82/// [`ChainManager::create_final_vote`]: crate::manager::ChainManager::create_final_vote
83/// [`ChainManager::handle_timeout_certificate`]: crate::manager::ChainManager::handle_timeout_certificate
84/// [`ChainManager::update_signed_proposal`]: crate::manager::ChainManager::update_signed_proposal
85/// [`ManagerSafetySnapshot::restore`]: crate::manager::ManagerSafetySnapshot::restore
86/// [`SafetyStateRecovery`]: crate::manager::proof::locking::SafetyStateRecovery
87pub trait CurrentRoundMonotone: RoundFloor + ConsensusInstance {}
88
89/// **Invariant (A cast vote never exceeds the current round).** Immediately after a correct
90/// validator casts a validation or confirmation vote in round `r`, its [`current_round`] is at
91/// least `r`; and by [`CurrentRoundMonotone`] it stays at least `r` for the rest of the
92/// instance.
93///
94/// *Proof.* By [`VoteConstructionSites`] there are three cases.
95///
96/// *Validation vote in round `r` (non-fast branch of [`ChainManager::create_vote`]).* Before
97/// signing, the method calls `update_proposed(proposal.clone(), blobs)` and then
98/// `update_current_round(local_time)`. After `update_proposed`, [`proposed`] is `Some` with a
99/// round `≥ r`: either it was `None` or held a lower round, and the proposal was stored with
100/// round `r`; or it already held a round `≥ r` and the write was skipped. By [`RoundFloor`],
101/// `update_current_round` then raises [`current_round`] to at least `proposed.content.round ≥ r`.
102///
103/// *Confirmation vote in [`Round::Fast`] (fast branch of [`ChainManager::create_vote`]).* Same
104/// call sequence; and [`Round::Fast`] is the minimum round ([`RoundOrder`]), so the claim is
105/// immediate.
106///
107/// *Confirmation vote in round `r` ([`ChainManager::create_final_vote`]).* Immediate from
108/// [`ConfirmationOnlyInCurrentRound`], which gives `current_round == r`. ∎
109///
110/// [`current_round`]: field@crate::manager::ChainManager::current_round
111/// [`proposed`]: crate::manager::ChainManager::proposed
112/// [`ChainManager::create_vote`]: crate::manager::ChainManager::create_vote
113/// [`ChainManager::create_final_vote`]: crate::manager::ChainManager::create_final_vote
114/// [`Round::Fast`]: linera_base::data_types::Round::Fast
115/// [`RoundOrder`]: crate::manager::proof::model::RoundOrder
116/// [`ConfirmationOnlyInCurrentRound`]: crate::manager::proof::voting::ConfirmationOnlyInCurrentRound
117pub trait VoteRoundBelowCurrentRound:
118    VoteConstructionSites
119    + ProposalGate
120    + RoundFloor
121    + CurrentRoundMonotone
122    + crate::manager::proof::voting::ConfirmationOnlyInCurrentRound
123{
124}
linera_chain/manager/proof/rounds.rs

linera_chain/manager/proof/
rounds.rs
