diff --git a/CLAUDE.md b/CLAUDE.md index 4ddda2145..c827f8b64 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -128,3 +128,11 @@ subspecifications that the Lean Ethereum protocol relies on. one-to-one: if an assertion changes, the matching docstring line changes with it. - Do not weaken a docstring into vagueness to avoid updating it; describe the new behavior precisely, as the doc-writer rules require. +- **CRITICAL - FORK-CHOICE HEAD ASSERTIONS MUST BE SCHEME-INDEPENDENT**: A head assertion that + pins the winner of a root-based tiebreak (`head_slot`, `head_root_label`) is scheme-fragile — + roots embed validator keys, so the winner can flip between `test` and `prod` (shipped in #916, + #1181). Assert the invariant, not the winner. + - Equal-weight tie → `lexicographic_head_among` (highest block root, from the store). + - Equal-slot equivocation tie → `canonical_equivocation_head_among` (largest attestation-data + root, from the store). + - If the tie is incidental, assert the head at a later step where it is unambiguous. diff --git a/packages/testing/src/consensus_testing/test_types/store_checks.py b/packages/testing/src/consensus_testing/test_types/store_checks.py index 4ea414dbb..71851d2b6 100644 --- a/packages/testing/src/consensus_testing/test_types/store_checks.py +++ b/packages/testing/src/consensus_testing/test_types/store_checks.py @@ -214,6 +214,14 @@ class StoreChecks(SelectiveCheck): All listed forks must have equal attestation weight, and the head carries the highest root. """ + canonical_equivocation_head_among: list[str] | None = None + """Fork labels in an equal-slot equivocation tie, head on the largest attestation-data root. + + Each listed fork must be targeted by an attestation in the accepted pool; the head must be + the fork whose attestation carries the largest hash_tree_root. Scheme-independent (roots are + read from the store). + """ + reorg_depth: int | None = None """Expected count of blocks from the old head back to its common ancestor with the new head.""" @@ -437,6 +445,18 @@ def _canonical_precedence(vote: AttestationData) -> tuple[Slot, Bytes32]: self.lexicographic_head_among, store, block_registry, step_index ) + # Equal-slot equivocation tiebreak: head sits on the largest attestation-data root. + if "canonical_equivocation_head_among" in fields: + if block_registry is None: + raise ValueError( + f"Step {step_index}: canonical_equivocation_head_among specified " + f"but block_registry not provided" + ) + assert self.canonical_equivocation_head_among is not None + StoreChecks._validate_canonical_equivocation_head( + self.canonical_equivocation_head_among, store, block_registry, step_index + ) + # Reorg depth if "reorg_depth" in fields: if old_head is None: @@ -577,3 +597,66 @@ def _validate_lexicographic_head( f"When forks have equal weight, the fork with the lexicographically " f"highest root should be selected as head." ) + + @staticmethod + def _validate_canonical_equivocation_head( + fork_labels: list[str], + store: Store, + block_registry: dict[str, Block], + step_index: int, + ) -> None: + """Validate the equal-slot equivocation tiebreak.""" + if len(fork_labels) < 2: + raise ValueError( + f"Step {step_index}: canonical_equivocation_head_among requires at least 2 forks " + f"to test the equivocation tiebreak, got {len(fork_labels)}: {fork_labels}" + ) + + # Resolve each fork label to its block root. + fork_roots: dict[str, Bytes32] = {} + for label in fork_labels: + if label not in block_registry: + raise ValueError( + f"Step {step_index}: canonical_equivocation_head_among label '{label}' " + f"not found in block registry. Available: {list(block_registry.keys())}" + ) + fork_roots[label] = hash_tree_root(block_registry[label]) + + # Largest attestation-data root per fork — the key latest-vote extraction sorts on. + attestation_root_by_label: dict[str, Bytes32] = {} + for label, fork_root in fork_roots.items(): + targeting_data_roots = [ + hash_tree_root(attestation_data) + for attestation_data in store.latest_known_aggregated_payloads + if attestation_data.target.root == fork_root + ] + if not targeting_data_roots: + raise AssertionError( + f"Step {step_index}: canonical_equivocation_head_among fork '{label}' " + f"(block_root=0x{fork_root.hex()}) has no attestation targeting it in the " + f"accepted aggregated pool." + ) + attestation_root_by_label[label] = max(targeting_data_roots) + + winning_label = max( + attestation_root_by_label, key=lambda label: attestation_root_by_label[label] + ) + expected_head_root = fork_roots[winning_label] + + if store.head != expected_head_root: + actual_label = next( + (label for label, root in fork_roots.items() if root == store.head), + "unknown", + ) + fork_info = "\n".join( + f" {label}: block_root=0x{fork_roots[label].hex()} " + f"attestation_data_root=0x{attestation_root_by_label[label].hex()}" + for label in sorted(fork_roots) + ) + raise AssertionError( + f"Step {step_index}: canonical equivocation tiebreak failed.\n" + f"The head must be the fork with the largest attestation-data root.\n" + f"Expected head: '{winning_label}' (0x{expected_head_root.hex()})\n" + f"Actual head: '{actual_label}' (0x{store.head.hex()})\n" + f"Competing forks:\n{fork_info}\n" + ) diff --git a/src/lean_spec/spec/forks/lstar/fork_choice.py b/src/lean_spec/spec/forks/lstar/fork_choice.py index 7d9c54627..f2c983ae5 100644 --- a/src/lean_spec/spec/forks/lstar/fork_choice.py +++ b/src/lean_spec/spec/forks/lstar/fork_choice.py @@ -682,6 +682,10 @@ def _extract_attestations_from_aggregated_payloads( An equal-slot tie breaks toward the larger canonical attestation-data root. The result is therefore independent of arrival or insertion order. + Agreement is guaranteed — nodes with identical store contents select the identical head — + but the winning fork's identity is not stable across signature schemes (roots embed + validator keys). + A vote whose head sits at or below the finalized slot carries no fork-choice weight. Such stale votes are skipped here, so callers pass their pool without pre-filtering. diff --git a/tests/consensus/lstar/fork_choice/test_equivocation.py b/tests/consensus/lstar/fork_choice/test_equivocation.py index 68d16144e..b2dea4716 100644 --- a/tests/consensus/lstar/fork_choice/test_equivocation.py +++ b/tests/consensus/lstar/fork_choice/test_equivocation.py @@ -246,7 +246,7 @@ def test_same_slot_equivocating_attesters_count_once( fork_choice_test: ForkChoiceTestFiller, ) -> None: """ - An equivocating validator is counted once, on the canonical-root fork. + An equivocating validator is counted once, on the canonical attestation-data root fork. Given ----- @@ -259,7 +259,6 @@ def test_same_slot_equivocating_attesters_count_once( - one vote at slot 3 targets fork_b from V0, V1, V3, V4. - V0 and V1 equivocate by voting on both forks at the same slot. - the two votes tie on slot, so the larger attestation-data root wins. - - the fork_b vote carries the larger root. When ---- @@ -267,10 +266,11 @@ def test_same_slot_equivocating_attesters_count_once( Then ---- - - V0 and V1 count once, toward fork_b. - - fork_b has effective weight 4 from V0, V1, V3, V4. - - fork_a has effective weight 1 from V2. - - head is fork_b. + - V0 and V1 each have one canonical vote at slot 3 (counted once), not pinned to a fork + because the winner depends on roots read from the store, not on a hardcoded outcome. + - V2 targets fork_a; V3 and V4 target fork_b (the exclusive, non-equivocating supporters). + - the head is the fork whose vote carries the larger attestation-data root, derived from the + store, so the vector holds under either signature scheme. - no slot is justified by the below-threshold votes. """ fork_choice_test( @@ -317,8 +317,7 @@ def test_same_slot_equivocating_attesters_count_once( TickStep( time=16, checks=StoreChecks( - head_slot=Slot(3), - head_root_label="fork_b", + canonical_equivocation_head_among=["fork_a", "fork_b"], latest_justified_slot=Slot(0), latest_finalized_slot=Slot(0), latest_known_aggregated_target_slots=[Slot(2), Slot(3)], @@ -327,13 +326,11 @@ def test_same_slot_equivocating_attesters_count_once( validator=ValidatorIndex(0), location="known", attestation_slot=Slot(3), - target_slot=Slot(3), ), AttestationCheck( validator=ValidatorIndex(1), location="known", attestation_slot=Slot(3), - target_slot=Slot(3), ), AttestationCheck( validator=ValidatorIndex(2), @@ -364,7 +361,7 @@ def test_equivocation_head_independent_of_arrival_order_a_then_b( fork_choice_test: ForkChoiceTestFiller, ) -> None: """ - Head ignores arrival order: fork_a arriving first still picks the canonical-root fork. + Head ignores arrival order: the canonical-root fork wins regardless of vote order. Given ----- @@ -377,9 +374,8 @@ def test_equivocation_head_independent_of_arrival_order_a_then_b( - one vote at slot 3 targets fork_b from V0, V2. - V0 equivocates by voting on both forks at the same slot. - V1 backs fork_a alone; V2 backs fork_b alone. - - without V0 the two forks tie one-to-one, so V0's vote decides the head. + - without V0 the two forks tie one-to-one, so V0's single counted vote decides the head. - the two votes tie on slot, so the larger attestation-data root wins. - - the fork_a vote carries the larger root. When ---- @@ -387,10 +383,10 @@ def test_equivocation_head_independent_of_arrival_order_a_then_b( Then ---- - - V0 counts once, toward the larger-root fork. - - the larger-root fork has effective weight 2. - - the smaller-root fork has effective weight 1. - - head is fork_a. + - V0 counts once, toward whichever fork's vote carries the larger attestation-data root. + - that fork has effective weight 2; the other has weight 1. + - the head is that fork, derived from the store roots rather than pinned, so it matches the + opposite arrival order under either signature scheme. - no slot is justified by the below-threshold votes. """ fork_choice_test( @@ -428,8 +424,7 @@ def test_equivocation_head_independent_of_arrival_order_a_then_b( TickStep( time=16, checks=StoreChecks( - head_slot=Slot(2), - head_root_label="fork_a", + canonical_equivocation_head_among=["fork_a", "fork_b"], latest_justified_slot=Slot(0), latest_finalized_slot=Slot(0), attestation_checks=[ @@ -437,7 +432,6 @@ def test_equivocation_head_independent_of_arrival_order_a_then_b( validator=ValidatorIndex(0), location="known", attestation_slot=Slot(3), - target_slot=Slot(2), ), ], ), @@ -450,7 +444,7 @@ def test_equivocation_head_independent_of_arrival_order_b_then_a( fork_choice_test: ForkChoiceTestFiller, ) -> None: """ - Head ignores arrival order: fork_b arriving first still picks the canonical-root fork. + Head ignores arrival order: the canonical-root fork wins regardless of vote order. Given ----- @@ -463,9 +457,8 @@ def test_equivocation_head_independent_of_arrival_order_b_then_a( - one vote at slot 3 targets fork_b from V0, V2. - V0 equivocates by voting on both forks at the same slot. - V1 backs fork_a alone; V2 backs fork_b alone. - - without V0 the two forks tie one-to-one, so V0's vote decides the head. + - without V0 the two forks tie one-to-one, so V0's single counted vote decides the head. - the two votes tie on slot, so the larger attestation-data root wins. - - the fork_a vote carries the larger root. When ---- @@ -473,10 +466,10 @@ def test_equivocation_head_independent_of_arrival_order_b_then_a( Then ---- - - V0 counts once, toward the larger-root fork. - - the larger-root fork has effective weight 2. - - the smaller-root fork has effective weight 1. - - head is fork_a, matching the opposite arrival order. + - V0 counts once, toward whichever fork's vote carries the larger attestation-data root. + - that fork has effective weight 2; the other has weight 1. + - the head is that fork, derived from the store roots rather than pinned, so it matches the + opposite arrival order under either signature scheme. - no slot is justified by the below-threshold votes. """ fork_choice_test( @@ -514,8 +507,7 @@ def test_equivocation_head_independent_of_arrival_order_b_then_a( TickStep( time=16, checks=StoreChecks( - head_slot=Slot(2), - head_root_label="fork_a", + canonical_equivocation_head_among=["fork_a", "fork_b"], latest_justified_slot=Slot(0), latest_finalized_slot=Slot(0), attestation_checks=[ @@ -523,7 +515,6 @@ def test_equivocation_head_independent_of_arrival_order_b_then_a( validator=ValidatorIndex(0), location="known", attestation_slot=Slot(3), - target_slot=Slot(2), ), ], ),