fix(fork-choice): make the equal-slot equivocation tie deterministic#1181
Merged
tcoratger merged 1 commit intoJul 4, 2026
Merged
Conversation
When a validator equivocates by signing two distinct votes for the same slot, fork choice kept whichever vote arrived first. Both votes are admitted and aggregated, and the latest-vote extraction resolved the equal-slot tie by dict iteration, which is arrival order. Two honest nodes holding the same blocks and votes but receiving them in different orders could pick different heads permanently. The block-level tiebreak sits one layer too late: the equivocator's weight has already landed on different branches, so the branch weights are unequal and it never fires. Resolve the equal-slot tie by the largest canonical attestation-data root, the same rule the block tiebreak applies to block roots. The latest-vote extraction now sorts the pool by slot then data root and keeps the first vote per validator, so the head is a pure function of store contents, independent of arrival or insertion order. An equivocator is counted once, on one branch every node agrees on. This needs no slashing or equivocation-tracking construct, which this fork lacks. Block production gains the same secondary sort key, so a proposer builds the same block regardless of arrival order. The testing fixture's own vote checker mirrored the old first-seen rule and is brought into lockstep with the spec. An existing vector that asserted the arrival-order winner is corrected to the deterministic winner, and two new vectors deliver the same equivocating votes in opposite orders and assert an identical head. Refs leanEthereum#1172 Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
adust09
added a commit
to NyxFoundation/formal-leanSpec
that referenced
this pull request
Jul 5, 2026
Store/BlockProduction.lean mirrors build_block's fixed-point selection (block_production.py, post leanEthereum/leanSpec#1181): candidates ordered once by (target.slot, hash_tree_root), the per-candidate filter chain, the MAX_ATTESTATIONS_DATA budget, the trial state transition, and re-anchoring on a moved justified/finalized checkpoint. selectionLoop is defined by well-founded recursion on the unprocessed candidate count with no fuel: selectionPass_rest_lt shows a pass that accepted something strictly shrinks the remainder, which is exactly upstream's termination argument (the chosen set only grows, and is bounded). Lean accepts the definition only because the iteration provably terminates - that is FC-5. The explicit bound is build_block_selection_terminates: at most payloads.length + 1 passes. The coverage picker (select_proofs_for_coverage) is a parameter: its choices never steer the loop's control flow and its tie-break needs encode_bytes of XMSS aggregates (Arklib side), so FC-5 holds for every picker. The post-loop collapse is packaging outside the fixed point and is not modeled.
2 tasks
MegaRedHand
added a commit
to lambdaclass/ethlambda
that referenced
this pull request
Jul 6, 2026
…(leanSpec #1181) (#503) ## What Ports leanSpec [#1181](leanEthereum/leanSpec#1181): make the equal-slot equivocation tie in fork choice deterministic. ## Why An equivocating validator can sign two distinct votes `A` and `B` for the same slot. Nothing rejects the second (the pool is keyed by attestation data, and the two data differ), so both are admitted. `extract_latest_attestations` then resolved the equal-slot tie with a strict `existing.slot < entry.data.slot` while iterating in **insertion (arrival) order**, so the winner was simply whichever was seen first. Two honest nodes with the same blocks and votes but different arrival order could land the equivocator's weight on different branches and pick **different heads permanently** — a determinism/safety bug that unit tests miss because it only appears across nodes. ## Changes `crates/storage/src/store.rs` — both `extract_latest_attestations` implementations (the aggregated `PayloadBuffer` and the raw `GossipSignatureBuffer`): - Process votes newest-first, breaking the equal-slot tie toward the **larger canonical attestation-data root** — the same rule the block-level fork-choice tiebreak applies to block roots. The extracted head becomes a pure function of pool contents, independent of arrival/insertion order. An equivocator is counted once, on one branch every node agrees on. - The pool key is already `hash_tree_root(data)`, so the tie needs no extra hashing. Block production is **not** changed: ethlambda's block builder already uses `data_root` as its deterministic final tiebreak (`EntryScore::ordering_key`, from leanSpec #1149), so it is already order-independent. The `drain` doc comment is updated (vote-extraction determinism no longer depends on drain order), and the unit test that asserted first-seen-wins is rewritten to assert order-independence (larger canonical root wins in both arrival orders). ## Tests - `extract_latest_attestations_canonical_root_wins_on_slot_tie` (rewritten from `..._first_inserted_wins_on_slot_tie`) `cargo fmt`, `clippy -D warnings`, and the storage lib tests (44) pass. > Since #1181 is merged in leanSpec, the released fork-choice fixtures encode the new expected head for the equivocation vectors; this change aligns ethlambda with them. Recommend a `forkchoice_spectests` run against fresh fixtures to confirm.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Fixes #1172: an equivocation tie-break in fork choice was insertion-order dependent, so two honest nodes with the same blocks and votes but different arrival order could pick different heads permanently. This is a genuine consensus-safety / determinism bug — all unit tests passed; the split only appeared between nodes on a live network.
The bug
An equivocating validator can sign two distinct votes
AandBfor the same slot. Nothing rejects the second (the pool is keyed by attestation data, and the two data differ), so both are admitted and aggregated. The latest-vote extraction then resolved the equal-slot tie with a strict<on slot:On the tie the second vote never overwrites the first, so the winner is simply whichever was iterated first — i.e. dict insertion = arrival order. The block-level tiebreak
max(children, key=(weights[r], r))is one layer too late: the equivocator's weight has already landed on different branches on the two nodes, so the branch weights are unequal and the tiebreak never fires. The heads diverge and stay diverged.The fix
Resolve the equal-slot tie deterministically by the largest canonical attestation-data root, the same rule the block-level tiebreak applies to block roots. The extraction now sorts the pool by
(slot, hash_tree_root(data))descending and keeps the first vote per validator:hash_tree_root(attestation_data)is computed once per distinct vote (in the sort key), never per validator.This is chosen over the consensus-specs approach of dropping equivocators via an
equivocating_indicesset: that requires slashing / equivocation-detection infrastructure this fork does not have, whereas a canonical tiebreak needs none.Block production gains the same
(target.slot, hash_tree_root)secondary sort key, so a proposer builds the same block regardless of arrival order (a related determinism gap where distinct data at one target slot previously fell back to arrival order under truncation).Determinism note (supersedes an earlier choice)
An earlier change (PR #892) made the tie keep the first-seen vote via an insertion-order-preserving pool merge. That only guaranteed intra-run reproducibility (identical output across
PYTHONHASHSEEDfor a single scripted fill); it did not give inter-node agreement, which is what this issue is about. The canonical-root tiebreak is a strict superset: it keeps the hash-seed reproducibility PR #892 wanted and adds inter-node determinism. Verified by filling the equivocation vectors underPYTHONHASHSEED=0and7— byte-identical.Tests
Consensus vectors only (fork tests are vector-driven):
attestation_checksmatch the fixed store.fork_a, first-gossiped); it is corrected to the deterministic winner (fork_b, larger data root), with its Given/When/Then docstring rewritten to describe the canonical rule.Full
tests/consensus/lstar/fork_choice/re-fill passes (119 vectors), no other vector relied on arrival order;just checkis clean.Credit
Found via the Lean 4 formalization of this spec (NyxFoundation/formal-leanSpec): modeling the store as an unordered map made "the head is a function of store contents" unprovable, because the result depended on an insertion order a map does not carry.
Refs #1172
🤖 Generated with Claude Code