Trait SafetyStateRecovery 

pub trait SafetyStateRecovery:
    ConsensusInstance
    + LockRoundMonotone
    + RoundFloor
    + ConfirmationOnlyInCurrentRound { }

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.

This is the one transition that writes locking_block, confirmed_vote and validated_vote without going through the voting path, so LockRoundMonotone, ConfirmedVoteRoundMonotone and CastValidationRoundFloor each owe it an argument.

Proof. The procedure captures ManagerSafetySnapshot::capture before wiping storage, replays the chain’s confirmed blocks from storage, and then calls ManagerSafetySnapshot::restore — but only under the explicit guard new_tip_height == tip_height, so the restored fields belong to the same pending height and hence the same consensus instance in the sense of ConsensusInstance.

Replay only feeds ConfirmedBlockCertificates to process_confirmed_block, which casts no vote and calls reset once per replayed height; so at the moment of restore the five snapshot fields are exactly what the final reset left them — None. The restore therefore re-installs the pre-reset values rather than overwriting newer ones, and each field returns to a value it genuinely held. The three invariants above are stated over the values a correct validator has committed to, so restoring them re-establishes rather than violates them.

The subtle point is current_round, which the snapshot does not capture or restore: it is left at ChainOwnership::first_round by the last reset, potentially far below the restored lock. That cannot be exploited, because every path that could act on the lower round re-derives the round from the lock first:

• create_final_vote calls update_locking then update_current_round before comparing against round, so by RoundFloor the comparison sees a round ≥ the restored lock round — this is exactly ConfirmationOnlyInCurrentRound;
• ChainManager::check_proposed_block rejects any proposal not strictly above the lock round, regardless of current_round.

So the restored lock, not the round register, is what binds. ∎

Residual obligation. ManagerSafetySnapshot records no height of its own; the correspondence between snapshot and instance rests entirely on the caller’s new_tip_height == tip_height guard. A future caller of ManagerSafetySnapshot::restore must reproduce it.

Implementors