Module model 

System model and the assumptions the safety argument rests on.

The definitions here fix what a consensus instance is and what it means for two blocks to conflict; the assumptions are the things the implementation does not prove and that a deployment must supply. Everything in this module is a leaf of the dependency graph.

The assumptions needed only for progress — synchrony, availability, leader fairness, an active driver — are stated separately in linera_core::proof::assumptions, because their evidence lives in that crate. Safety depends on none of them.

Traits

ConflictingBlocks

Definition (Conflicting blocks). Two Blocks conflict when they have the same chain_id and height but different hashes. Certificates certify ConfirmedBlock and ValidatedBlock values, each of which wraps a Block and hashes to that block’s hash, so “certificates for conflicting blocks” is well defined.

ConsensusInstance

Definition (Consensus instance). The protocol decides one block at a time, per chain. A consensus instance is a pair (chain, height), and its state is one ChainManager, reachable as ChainStateView::manager, whose height is ChainTipState::next_block_height.

CorrectValidator

Definition (Correct validator). A validator is correct in an execution if every signature it produces was produced by an unmodified build of this code, driven through the public entry points of linera_core::worker::WorkerState, with a private key no other party holds. A validator that is not correct is faulty, and may sign anything at any time, including contradictory statements.

DeterministicExecution

Assumption (Deterministic execution). For a fixed chain state at a height, a fixed ProposedBlock, a fixed set of published blobs and a fixed multi-leader round argument, block execution returns a unique BlockExecutionOutcome.

DurablePersistence

Assumption (Durable persistence). A correct validator persists its ChainManager state before releasing a vote to the network, and that state survives a crash.

EpochAgreement

Assumption (Epoch agreement). All correct validators evaluate a given consensus instance against the same Committee.

MaxByzantineWeight

Assumption (Maximum Byzantine weight, per epoch). For every epoch whose committee has not been revoked, the total Committee::weight of faulty validators in that committee is strictly less than its Committee::validity_threshold — at most f⁺ − 1 where f⁺ = ⌈N/3⌉, equivalently strictly below one third of that committee’s total weight.

RoundOrder

Definition (Round order). Rounds are Round values, totally ordered by the derived Ord on the enum, which orders first by variant and then by the contained u32:

SequentialChainState

Assumption (Sequential instance state). The transitions of one consensus instance are mutually exclusive and each runs to completion: no two of them interleave their reads and writes of the same ChainManager.

StorageAtomicity

Assumption (Atomic persistence). A single WritableKeyValueStore::write_batch — one batch against one root key — is applied atomically, within whatever key-count and size limits the backend imposes.

UnforgeableSignatures

Assumption (Cryptographic soundness). ValidatorSignature is existentially unforgeable: no party without a validator’s secret key produces a signature that ValidatorSignature::check accepts for that validator’s public key. CryptoHash is collision resistant, so distinct values — in particular distinct Blocks and distinct VoteValues — have distinct hashes.