pub trait FastRetryPreservesBlock:
UnlockingRequiresHigherCertificate
+ DeterministicExecution
+ ConflictingBlocks { }Expand description
Lemma (A fast retry cannot change the block). Let a block A be confirmed in
Round::Fast, and let a correct validator later cast a validation vote for a block B on a
proposal whose OriginalProposal::Fast retries A’s proposal. Then B = A.
Proof. By UnlockingRequiresHigherCertificate, the fast-retry arm of
ChainManager::check_proposed_block accepts only if the validator’s stored confirmation
vote is in the fast round and its value satisfies matches_proposed_block(new_block). That
predicate compares the ProposedBlock components only — chain, epoch, transactions,
height, timestamp, authenticated owner, parent hash — so it leaves open that A and B
share a proposal but differ in BlockExecutionOutcome, which by ConflictingBlocks
would make them conflicting blocks.
That gap is closed by DeterministicExecution. The retry re-executes the proposal
(try_handle_block_proposal takes the else branch of if let Some(outcome) = outcome,
since a fast retry carries no outcome), at the same height with the same parent, so the only
input that differs from the original fast execution is the round argument
Round::multi_leader. A block accepted in the fast round recorded no oracle responses —
try_handle_block_proposal rejects one that did with WorkerError::FastBlockUsingOracles —
and the round is observable only as OracleResponse::Round. An execution that never
queried the round therefore cannot branch on it, so by determinism the two executions agree
and B = A. ∎
Residual obligation. The no-oracle check is applied when the proposal’s round is fast,
not when a fast block is retried, so this step relies on determinism of the execution engine
rather than on a runtime check at the retry. An execution engine that made an outcome depend
on the round without recording an OracleResponse::Round would break it. This is the one
place in the safety argument that reaches outside consensus into execution.