Module assumptions 

The assumptions that progress needs and safety does not.

Safety rests only on the assumptions in linera_chain::manager::proof::model, all of which remain in force here. This module adds the ones that mention time, responsiveness, or the existence of somebody willing to drive the protocol. Every one of them can fail without endangering CommitAgreement; each failure costs progress only.

Traits

ActiveCorrectDriver

Assumption (An active correct driver). Some correct owner of the chain runs a ChainClient that, from some point on, repeatedly and without giving up calls ChainClient::process_pending_block (or an operation that does, such as ChainClient::execute_operations) with a block to propose, and holds the signing key for the owner it proposes as.

BlobRetention

Assumption (Blob retention). A correct validator that has processed a certified block keeps the blobs that block requires, for as long as any node may still need to execute it.

BoundedRecovery

Assumption (Bounded recovery). After GST, a correct validator that crashes restarts and is again answering requests within Δ.

ClockAccuracy

Assumption (Clock accuracy). Correct validators’ clocks (linera_storage::Clock::current_time) advance in real time and agree within a bound small compared to the round timeout.

CorrectValidatorAvailability

Assumption (Correct validator availability). After GST, every correct validator accepts requests and answers them within Δ, and its linera_core::worker::WorkerState completes each request in bounded local time.

EventualSynchrony

Assumption (Eventual synchrony). There is a time GST and a bound Δ, both unknown to the protocol, such that every message sent between correct participants after GST is delivered within Δ, and every message sent before GST is delivered by GST + Δ.

FullReachability

Assumption (Full reachability during synchronization). After GST, a correct driver’s ChainClient::synchronize_chain_state reaches every correct validator, not merely a quorum of them.

LeaderFairness

Assumption (Leader fairness). The leader schedule selects the correct owner of ActiveCorrectDriver in infinitely many SingleLeader rounds.

RoundTimeoutGrowth

Assumption (Round timeouts eventually exceed the round trip). The round timeout grows without bound over successive rounds, so that eventually a round lasts longer than the time a correct leader needs to complete it after GST.