Trait LockViolationSoundness 

pub trait LockViolationSoundness:
    UnforgeableSignatures
    + UnlockingRequiresHigherCertificate
    + ConfirmedVoteRoundMonotone
    + ConfirmationOnlyInCurrentRound
    + FastConfirmationNeedsEmptyLock
    + OneConfirmationVotePerRound
    + VoteRoundBelowCurrentRound
    + CurrentRoundMonotone
    + DeterministicExecution { }

Lemma (Lock violations are never honest). No correct validator is named by an accepted LockViolation proof — subject to the residual obligation below.

Proof. An accepted proof exhibits v’s confirmation vote for X at round r and v’s validation vote for Y at round s, with hash(X) ≠ hash(Y), the same chain and height, r < s, and a signed unlocking round u with u ≤ r (or u = None). Suppose v correct.

The confirmation came first. Otherwise, after the validation at s, VoteRoundBelowCurrentRound and CurrentRoundMonotone pin v’s current round at ≥ s. A later confirmation at r < s is then impossible: via ChainManager::create_final_vote it would need current_round == r (ConfirmationOnlyInCurrentRound); via the fast branch it would need r = Round::Fast and, by FastConfirmationNeedsEmptyLock, an empty lock and no validation vote — contradicting the floor ≥ s that the validation at s established.

So let (X', p) be v’s stored confirmation vote just before the validation at s. It is present, and by ConfirmedVoteRoundMonotone, p ≥ r. Apply UnlockingRequiresHigherCertificate to the validation vote, by the shape of its proposal:

• Fresh proposal. Rejected outright — v would not have voted.
• Regular retry with certificate c, and X' not matching Y’s proposal. The guard is p < c.round, and c.round is exactly the signed u. With u ≤ r ≤ p this gives p < u ≤ p. Contradiction.
• Regular retry with X' matching Y’s proposal. The guard is p ≤ u, so p ≤ u ≤ r ≤ p forces p = u = r.
• Fast retry. The signed u is None, and the guard forces p = Round::Fast and X' matching Y’s proposal; with Round::Fast minimal and p ≥ r, again p = r.

The last two cases coincide: v confirmed X at round r and its stored confirmation at the same round r = p is X', so OneConfirmationVotePerRound gives X = X'. Hence X matches Y’s ProposedBlock while hash(X) ≠ hash(Y) — the two blocks share a proposal and differ only in BlockExecutionOutcome. Sharing a proposal means sharing a previous_block_hash, so by UnforgeableSignatures (collision resistance) they have the same parent and hence the same ancestry and the same pre-state, and DeterministicExecution makes the outcome a function of that pre-state and the proposal. So X = Y, contradicting hash(X) ≠ hash(Y). ∎

Residual obligation. Only the first two cases are unconditional; the last two are closed by DeterministicExecution, the same hinge as FastRetryPreservesBlock. The ancestry argument avoids circularity — it follows previous_block_hash down rather than appealing to UniqueChain — but an execution engine whose outcome depends on the round without recording an OracleResponse::Round would make a correct validator convictable here.

Implementors