From a6e45eb3e9e04c270f3e699d0fbc0300007f22ce Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Thu, 9 Jul 2026 14:09:25 +0700 Subject: [PATCH 1/3] fix(testing): make equivocation head assertions scheme-independent The equivocation tiebreak vectors hardcoded the winning fork of #1181's largest-attestation-data-root rule. That root embeds validator XMSS pubkeys, so the winner flips between test and prod schemes; the vectors passed PR CI (test scheme) and failed prod-vectors on main (prod scheme). Same class as #916. Add a scheme-independent canonical_equivocation_head_among check that reads each fork's attestation root from the store and asserts the head is the largest-root fork, mirroring lexicographic_head_among. Rewrite the 3 vectors to use it, note the scheme-dependence on the spec tiebreak, add a CLAUDE.md rule, and gate fork-choice vectors under --scheme=prod in PR CI. --- .github/workflows/ci.yml | 35 ++++++ CLAUDE.md | 18 ++++ .../test_types/store_checks.py | 102 ++++++++++++++++++ src/lean_spec/spec/forks/lstar/fork_choice.py | 8 ++ .../lstar/fork_choice/test_equivocation.py | 51 ++++----- 5 files changed, 184 insertions(+), 30 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 9b6784c6a..26606fbd6 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -159,6 +159,41 @@ jobs: - name: Fill test fixtures run: just fill-ci + # Scheme-fragility guard. A root-based fork-choice tiebreak embeds the validator XMSS public + # keys, so a vector that hardcodes the winning fork can pass under the default `test` scheme + # and fail under `prod`. This reruns the fork-choice vectors under the prod scheme to catch + # that pre-merge. See CLAUDE.md, "FORK-CHOICE HEAD ASSERTIONS MUST BE SCHEME-INDEPENDENT". + # Determinism is already gated by fill-tests; this job disables it to stay a fast smoke check. + fill-tests-prod-scheme: + name: Fill fork-choice fixtures under the prod scheme - Python 3.14 + runs-on: macos-latest + timeout-minutes: 20 + steps: + - name: Checkout leanSpec + uses: actions/checkout@v4 + + - name: Set up Python 3.14 + uses: actions/setup-python@v5 + with: + python-version: "3.14" + + - name: Install uv + uses: astral-sh/setup-uv@v4 + with: + enable-cache: true + cache-dependency-glob: "pyproject.toml" + + - name: Install just + uses: taiki-e/install-action@v2 + with: + tool: just + + - name: Download prod scheme keys + run: uv run keys --download --scheme prod + + - name: Fill fork-choice fixtures under the prod scheme + run: just fill-ci --scheme=prod --no-check-determinism tests/consensus/lstar/fork_choice + interop-tests: name: Interop tests - Multi-node consensus runs-on: macos-latest diff --git a/CLAUDE.md b/CLAUDE.md index 4ddda2145..b4425d14d 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -128,3 +128,21 @@ 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**: This is a STRICT + requirement. A fork-choice head assertion (`head_slot`, `head_root_label`, or any check that + pins which block is head) must NOT depend on the signature scheme. Block and attestation-data + roots embed the genesis state root, which embeds the validator XMSS public keys, so a + root-based tiebreak winner can flip between the `test` and `prod` schemes. A vector that + hardcodes the winning fork passes under one scheme and fails under the other; this has shipped + twice (PR #916, PR #1181). + - Never pin the winner of a weight tie or an equal-slot equivocation tie to a hardcoded fork + label or slot. Assert the scheme-independent facts instead. + - For a weight tie between equal-weight forks, use `lexicographic_head_among` (head = highest + block root, computed from the store). + - For an equal-slot equivocation tie, use `canonical_equivocation_head_among` (head = fork + whose attestation carries the largest attestation-data root, computed from the store). + - When a tie is incidental to the scenario, prefer asserting the genuine behavior at a later + step where a single child or unambiguous weight removes the tie, rather than asserting the + head at the tie step. + - The identity of the winning fork may legitimately differ across schemes; what must hold is + that all nodes with identical store contents pick the identical head. 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..fbbe48fb7 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,18 @@ 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 at least one attestation in the store's accepted + aggregated pool. The fork whose attestation carries the largest canonical hash_tree_root + absorbs each equivocator's single counted vote, so the head must sit at that fork. + + The roots are read from the store, so the assertion holds under any signature scheme; + it never pins which fork wins. The winner is a pure function of store contents, exactly as + the fork-choice latest-vote extraction computes it. + """ + reorg_depth: int | None = None """Expected count of blocks from the old head back to its common ancestor with the new head.""" @@ -437,6 +449,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 +601,81 @@ 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. + + Each listed fork must be targeted by at least one attestation in the store's accepted + aggregated pool. The fork whose attestation carries the largest canonical + ``hash_tree_root`` absorbs each equivocator's single counted vote, so the head must sit + at that fork. The comparison key is identical to the one the fork-choice latest-vote + extraction sorts on, so the winner derived here is the fork that wins in the spec. + + The roots are read from the store rather than hardcoded, which keeps the assertion + independent of the signature scheme: a block root embeds the genesis state root, which + embeds the validator XMSS public keys, so the identity of the winning fork can flip + between schemes. What is invariant is that the head tracks the largest root present. + """ + 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]) + + # For each fork, take the largest canonical attestation-data root among the attestations + # targeting it. This is the same key the latest-vote extraction sorts on, so the fork with + # the maximum value here is the one each equivocator's weight lands 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..b3eaad41a 100644 --- a/src/lean_spec/spec/forks/lstar/fork_choice.py +++ b/src/lean_spec/spec/forks/lstar/fork_choice.py @@ -682,6 +682,14 @@ 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. + What is guaranteed is agreement: any two nodes with identical store contents map every + validator to the identical vote, and so select the identical head. The identity of the + winning fork is not stable across configurations: an attestation-data root embeds its + target block root, which embeds the genesis state root, which embeds the validator XMSS + public keys, so the larger root (and thus the equivocator's landing fork) can flip between + signature schemes. Tests must assert the head against the largest root present in the + store, never against a hardcoded fork label. + 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), ), ], ), From d63f96a51fcf9a35e6a69527ce447e4b7c37d665 Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Thu, 9 Jul 2026 21:25:46 +0700 Subject: [PATCH 2/3] ci: drop prod-scheme fork-choice smoke job The fill-tests-prod-scheme job was cancelled at its 20-minute timeout on the macOS runner (the fork-choice tree under --scheme=prod takes >20 min in CI). Remove it; the scheme-independence rule in CLAUDE.md and the canonical_equivocation_head_among check remain. --- .github/workflows/ci.yml | 35 ----------------------------------- 1 file changed, 35 deletions(-) diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 26606fbd6..9b6784c6a 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -159,41 +159,6 @@ jobs: - name: Fill test fixtures run: just fill-ci - # Scheme-fragility guard. A root-based fork-choice tiebreak embeds the validator XMSS public - # keys, so a vector that hardcodes the winning fork can pass under the default `test` scheme - # and fail under `prod`. This reruns the fork-choice vectors under the prod scheme to catch - # that pre-merge. See CLAUDE.md, "FORK-CHOICE HEAD ASSERTIONS MUST BE SCHEME-INDEPENDENT". - # Determinism is already gated by fill-tests; this job disables it to stay a fast smoke check. - fill-tests-prod-scheme: - name: Fill fork-choice fixtures under the prod scheme - Python 3.14 - runs-on: macos-latest - timeout-minutes: 20 - steps: - - name: Checkout leanSpec - uses: actions/checkout@v4 - - - name: Set up Python 3.14 - uses: actions/setup-python@v5 - with: - python-version: "3.14" - - - name: Install uv - uses: astral-sh/setup-uv@v4 - with: - enable-cache: true - cache-dependency-glob: "pyproject.toml" - - - name: Install just - uses: taiki-e/install-action@v2 - with: - tool: just - - - name: Download prod scheme keys - run: uv run keys --download --scheme prod - - - name: Fill fork-choice fixtures under the prod scheme - run: just fill-ci --scheme=prod --no-check-determinism tests/consensus/lstar/fork_choice - interop-tests: name: Interop tests - Multi-node consensus runs-on: macos-latest From 17ae8dd282b5265bf544e4bcb2e9fd3ebb5e5ff0 Mon Sep 17 00:00:00 2001 From: Leo Lara Date: Sat, 11 Jul 2026 19:13:07 +0700 Subject: [PATCH 3/3] docs: trim equivocation scheme-independence notes Cut the root-to-pubkey derivations and test guidance an experienced reader already knows. The CLAUDE.md rule keeps the actionable bullets, the check's field docstring matches lexicographic_head_among's brevity, and the spec docstring states only the behavioral property (no test instructions). --- CLAUDE.md | 26 +++++------------ .../test_types/store_checks.py | 29 ++++--------------- src/lean_spec/spec/forks/lstar/fork_choice.py | 10 ++----- 3 files changed, 16 insertions(+), 49 deletions(-) diff --git a/CLAUDE.md b/CLAUDE.md index b4425d14d..c827f8b64 100644 --- a/CLAUDE.md +++ b/CLAUDE.md @@ -128,21 +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**: This is a STRICT - requirement. A fork-choice head assertion (`head_slot`, `head_root_label`, or any check that - pins which block is head) must NOT depend on the signature scheme. Block and attestation-data - roots embed the genesis state root, which embeds the validator XMSS public keys, so a - root-based tiebreak winner can flip between the `test` and `prod` schemes. A vector that - hardcodes the winning fork passes under one scheme and fails under the other; this has shipped - twice (PR #916, PR #1181). - - Never pin the winner of a weight tie or an equal-slot equivocation tie to a hardcoded fork - label or slot. Assert the scheme-independent facts instead. - - For a weight tie between equal-weight forks, use `lexicographic_head_among` (head = highest - block root, computed from the store). - - For an equal-slot equivocation tie, use `canonical_equivocation_head_among` (head = fork - whose attestation carries the largest attestation-data root, computed from the store). - - When a tie is incidental to the scenario, prefer asserting the genuine behavior at a later - step where a single child or unambiguous weight removes the tie, rather than asserting the - head at the tie step. - - The identity of the winning fork may legitimately differ across schemes; what must hold is - that all nodes with identical store contents pick the identical head. +- **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 fbbe48fb7..71851d2b6 100644 --- a/packages/testing/src/consensus_testing/test_types/store_checks.py +++ b/packages/testing/src/consensus_testing/test_types/store_checks.py @@ -217,13 +217,9 @@ class StoreChecks(SelectiveCheck): 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 at least one attestation in the store's accepted - aggregated pool. The fork whose attestation carries the largest canonical hash_tree_root - absorbs each equivocator's single counted vote, so the head must sit at that fork. - - The roots are read from the store, so the assertion holds under any signature scheme; - it never pins which fork wins. The winner is a pure function of store contents, exactly as - the fork-choice latest-vote extraction computes it. + 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 @@ -609,20 +605,7 @@ def _validate_canonical_equivocation_head( block_registry: dict[str, Block], step_index: int, ) -> None: - """ - Validate the equal-slot equivocation tiebreak. - - Each listed fork must be targeted by at least one attestation in the store's accepted - aggregated pool. The fork whose attestation carries the largest canonical - ``hash_tree_root`` absorbs each equivocator's single counted vote, so the head must sit - at that fork. The comparison key is identical to the one the fork-choice latest-vote - extraction sorts on, so the winner derived here is the fork that wins in the spec. - - The roots are read from the store rather than hardcoded, which keeps the assertion - independent of the signature scheme: a block root embeds the genesis state root, which - embeds the validator XMSS public keys, so the identity of the winning fork can flip - between schemes. What is invariant is that the head tracks the largest root present. - """ + """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 " @@ -639,9 +622,7 @@ def _validate_canonical_equivocation_head( ) fork_roots[label] = hash_tree_root(block_registry[label]) - # For each fork, take the largest canonical attestation-data root among the attestations - # targeting it. This is the same key the latest-vote extraction sorts on, so the fork with - # the maximum value here is the one each equivocator's weight lands on. + # 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 = [ diff --git a/src/lean_spec/spec/forks/lstar/fork_choice.py b/src/lean_spec/spec/forks/lstar/fork_choice.py index b3eaad41a..f2c983ae5 100644 --- a/src/lean_spec/spec/forks/lstar/fork_choice.py +++ b/src/lean_spec/spec/forks/lstar/fork_choice.py @@ -682,13 +682,9 @@ 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. - What is guaranteed is agreement: any two nodes with identical store contents map every - validator to the identical vote, and so select the identical head. The identity of the - winning fork is not stable across configurations: an attestation-data root embeds its - target block root, which embeds the genesis state root, which embeds the validator XMSS - public keys, so the larger root (and thus the equivocator's landing fork) can flip between - signature schemes. Tests must assert the head against the largest root present in the - store, never against a hardcoded fork label. + 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.