Trait CertifiedBlockWasExecuted 

pub trait CertifiedBlockWasExecuted:
    CertificateCarriesCorrectVote
    + ProposalGate
    + MaxByzantineWeight
    + CommitRestsOnValidation { }

Lemma (Every certified block was executed by a correct validator). If a valid ValidatedBlockCertificate for a block B exists, then some correct validator executed B’s ProposedBlock itself and obtained B’s BlockExecutionOutcome. The same follows for a ConfirmedBlockCertificate outside the fast round, by CommitRestsOnValidation; inside the fast round it holds directly, a fast proposal carrying no outcome.

This is what stands between the protocol and a committed block whose outcome is fabricated. It is not accountability: a validator that votes for a mis-executed block leaves no extractable proof (see AccountabilityScope). And unlike the results in crate::justification::proof, it needs MaxByzantineWeight — so validity, unlike agreement, degrades above the fault bound with no forensic residue.

Proof. Induction on the certificate’s round, well founded because rounds are totally ordered. By CertificateCarriesCorrectVote some correct validator v cast a validation vote for B in that round, so by ProposalGate it ran ChainWorkerState::try_handle_block_proposal to acceptance on a proposal for B. That function computes the block as

let block = if let Some(outcome) = outcome { outcome.clone().with(proposal.content.block.clone()) }
            else { self.execute_block(…).await? };

and BlockProposal::check_invariants admits a carried outcome only together with an OriginalProposal::Regular certificate. So:

• a fresh proposal and a fast retry both carry outcome: None and are therefore executed by v itself — the base case;
• a regular retry is not re-executed, but check_invariants requires its certificate to satisfy certificate.check_value(&ValidatedBlock::new(outcome.with(block))), i.e. to certify exactly this B, and content.round > certificate.round; the caller verified it with certificate.check(&committee). The induction hypothesis at that strictly lower round supplies the correct validator that executed B. ∎

All eight outputs, not just the state. BlockHeader commits to each component of the outcome separately — state_hash, messages_hash, events_hash, blobs_hash, oracle_responses_hash, operation_results_hash, previous_message_blocks_hash and previous_event_blocks_hash — and this lemma covers all of them, since the correct validator computed the whole BlockExecutionOutcome. That matters because the components differ sharply in reach: state_hash is local to the chain, whereas messages and events leave it and are consumed by other chains, and blobs are content-addressed (BlobId is a hash of the content) and so are the only component that is self-verifying without any execution at all.

What this does not give. The correct validator executed the proposal, but the execution replays whatever oracle answers it recorded; a later re-execution of the confirmed block feeds outcome.oracle_responses back in rather than re-deriving them. So the lemma certifies that the outcome follows from the proposal and those oracle answers, not that the answers were truthful. Oracle results are attested by quorum, which is inherent — they are not reproducible functions of the chain state.

Implementors