Module locking 

Locking invariants: what a correct validator’s committed-to state can look like.

These are protocol invariants: each is proved by induction over the transitions of one consensus instance (ConsensusInstance), and each proof discharges the induction by enumerating every method that writes the relevant field. The enumerations are the load-bearing part — a new writer invalidates them — so each invariant names its writers explicitly.

The writer sets, for reference:

field	writers
locking_block	private update_locking (from create_vote ×3 and create_final_vote); ManagerSafetySnapshot::restore; reset
confirmed_vote	create_vote (fast branch); create_final_vote; ManagerSafetySnapshot::restore; reset
validated_vote	create_vote (both branches); create_final_vote; ManagerSafetySnapshot::restore; reset
timeout_vote	create_timeout_vote; ManagerSafetySnapshot::restore; reset
fallback_vote	vote_fallback; ManagerSafetySnapshot::restore; reset
timeout	handle_timeout_certificate; reset
proposed	private update_proposed (from create_vote); reset
signed_proposal	update_signed_proposal; private update_proposed (clears it); reset

Traits

CastValidationRoundFloor

Invariant (Cast validation rounds leave a floor). If a correct validator has ever cast a validation vote in round s during an instance, then from that moment on

ConfirmedVoteRoundMonotone

Invariant (The confirmed-vote round never decreases). Within one consensus instance, if confirmed_vote is Some with round p, it never later holds a vote with round < p.

Lock

Definition (Lock). The lock of an instance is ChainManager::locking_block, and its lock round is LockingBlock::round of that value, or ⊥ when the field is None, with ⊥ below every round.

LockRoundMonotone

Invariant (The lock round never decreases). Within one consensus instance, the lock round is non-decreasing.

NoValidatedBlockInFastRound

Lemma (No validated block certificate in the fast round). No valid ValidatedBlockCertificate is certified in Round::Fast.

OneConfirmationVotePerRound

Lemma (One confirmation vote per round). A correct validator casts at most one confirmation vote per round of an instance.

OneValidationVotePerRound

Lemma (One validation vote per round). A correct validator casts at most one validation vote per round of an instance.

SafetyStateRecovery

Lemma (Safety state survives a local reset). After ChainWorkerState::reset_and_reexecute_chain, the manager’s lock and cast votes are at least what they were before the reset, and no invariant of this module is broken.

SimultaneousVotes

Remark (Votes a correct validator may hold simultaneously). Nothing above forbids a correct validator from holding a confirmed_vote and a validated_vote at once — it does, whenever it validates in a round above its last confirmation. What the invariants forbid is two of the same kind in the same round. The reporting projection ChainManagerInfo::pending picks whichever is higher, which is why a client observing a validator sees a single “pending” vote even though two are stored.

UniqueValidatedBlockPerRound

Lemma (At most one validated block per round). For a given chain and height, all valid ValidatedBlockCertificates certified in the same round certify the same block.