fix(forkchoice): derive finalized from canonical head, not an independent max (leanEthereum#1001)

* fix(forkchoice): derive finalized from canonical head, not an independent max

The store advanced latest_finalized by an independent monotonic max over every
imported block's post-state, decoupling it from the head. A fork that finalized
a higher slot but then lost head selection left its finalized checkpoint latched
in the store. get_attestation_target derives the attestation target against
store.latest_finalized, while the state transition validates targets against the
canonical state's latest_finalized; once the two finalized slots diverged,
is_justifiable_after disagreed and every advancing target was rejected, so
finalization froze.

Derive the finalized checkpoint from the canonical head's chain instead, in
update_head, so it is recomputed on every head change -- block import, acceptance
ticks, and proposals: take the finalized slot named by the head state and recover
its root as the head's own ancestor at that slot. The checkpoint then always lies
on the head chain, store.latest_finalized.slot matches the slot the state
transition validates against, and a checkpoint-sync anchor survives because the
head descends from it (its state cannot name its own block, so the root is
recovered as the head's ancestor). This restores the 3sf-mini reference, where a
staker reads latest_finalized from post_states[head], not a max over states.

Block production carried a second copy of the same independent max: it advanced
store.latest_finalized from the produced block's own state and pruned against it,
stranding -- and over-pruning -- when the proposal lost head selection. Remove
that write; update_head, which get_proposal_head runs just before each proposal,
owns the finalized checkpoint.

The fork choice is not clamped to finalized descendants: leanSpec finalization is
order dependent, so a fork that finalizes a higher slot can still lose head
selection, and clamping would latch the head onto that losing fork. The
attestation source keeps using store.latest_justified (the LMD anchor), matching
3sf-mini's get_latest_justified_hash and the deliberate choice in leanEthereum#595.

* Update src/lean_spec/spec/forks/lstar/fork_choice.py

Co-authored-by: Thomas Coratger <60488569+tcoratger@users.noreply.github.com>

* Update src/lean_spec/spec/forks/lstar/fork_choice.py

Co-authored-by: Thomas Coratger <60488569+tcoratger@users.noreply.github.com>

* refactor(forkchoice): address review -- inline finalized helper, tidy comments

Inline the single-use _finalized_on_head_chain into update_head, folding the head
and finalized updates into one model_copy; trim the verbose comments in
update_head and produce_block. No behavior change.

* fix(forkchoice): guard the finalized walk against a checkpoint-sync boot

The ancestor walk in head recomputation assumed every parent was already in the
store. On a fresh checkpoint-synced node the store holds only the anchor block,
whose state's finalized slot sits below the anchor block slot, so the first head
recompute stepped to a parent root absent from the store and raised KeyError.
The vectors missed it because the test anchor rebases its finalized up to the
anchor slot, so the loop never iterated.

Guard the walk as the other ancestor walks in this file do, stop when the parent
is absent, and keep the trusted anchor when no block sits exactly at the
finalized slot (which also covers a skipped finalized slot).

Add a regression vector: a mid-chain anchor whose finalized stays at genesis,
below the anchor slot, no longer crashes head recomputation.

* test(forkchoice): cover the proposer path not pinning a higher finalized

Build genesis -> block_1 -> block_2 justifying slot 1, then produce block_3 whose
own state finalizes slot 1. Block production does not advance its own head, so
block_3 stays off the head while the head remains block_2, finalized at the
genesis boundary. Assert the store's finalized tracks the head state, not
block_3's higher finalized, and the counted pool is left untouched.

Fails on the pre-fix advance-and-prune in block production, passes on the fix.

---------

Co-authored-by: Thomas Coratger <60488569+tcoratger@users.noreply.github.com>

Author: GrapeBaBa

src/lean_spec/spec/forks/lstar/fork_choice.py

@@ -596,15 +596,14 @@ def on_block(
             # Run the state transition from the parent state to this block's post-state.
             post_state = self.state_transition(parent_state, block)
 
-            # Advance the justified and finalized checkpoints from the post-state.
+            # Advance the justified checkpoint from the post-state.
             #
             # A candidate wins only when its slot is strictly higher than the store's.
             # On a slot tie the store keeps its checkpoint, avoiding a silent root swap:
             #
             #     store slot 5, candidate slot 7  ->  take candidate
             #     store slot 5, candidate slot 5  ->  keep store
             latest_justified = store.latest_justified.advance_to(post_state.latest_justified)
-            latest_finalized = store.latest_finalized.advance_to(post_state.latest_finalized)
 
             # Seed each block-carried vote into the known pool with an empty proof set.
             #
@@ -625,7 +624,6 @@ def on_block(
                     "blocks": store.blocks | {block_root: block},
                     "states": store.states | {block_root: post_state},
                     "latest_justified": latest_justified,
-                    "latest_finalized": latest_finalized,
                     "latest_known_aggregated_payloads": new_known_aggregated_payloads,
                 }
             )
@@ -830,7 +828,24 @@ def update_head(self, store: LstarStore) -> LstarStore:
             start_root=store.latest_justified.root,
             attestations=latest_votes,
         )
-        return store.model_copy(update={"head": new_head})
+        # Invariant: the finalized checkpoint stays on the head's chain.
+        # Climb from the head to its ancestor at the finalized slot.
+        finalized_slot = store.states[new_head].latest_finalized.slot
+        finalized_root = new_head
+        while finalized_root in store.blocks and store.blocks[finalized_root].slot > finalized_slot:
+            parent_root = store.blocks[finalized_root].parent_root
+            if parent_root not in store.blocks:
+                break
+            finalized_root = parent_root
+
+        # A fresh checkpoint-sync anchor stores no block at that slot.
+        # Keep the trusted anchor there rather than emit an unresolved root.
+        if store.blocks[finalized_root].slot == finalized_slot:
+            latest_finalized = Checkpoint(root=finalized_root, slot=finalized_slot)
+        else:
+            latest_finalized = store.latest_finalized
+
+        return store.model_copy(update={"head": new_head, "latest_finalized": latest_finalized})
 
     def accept_new_attestations(self, store: LstarStore) -> LstarStore:
         """

src/lean_spec/spec/forks/lstar/validator_duties.py

@@ -199,29 +199,17 @@ def produce_block_with_signatures(
         # Compute block hash for storage.
         block_hash = hash_tree_root(final_block)
 
-        # Update checkpoints from post-state.
-        #
-        # Locally produced blocks bypass normal block processing.
-        # Checkpoint advances must be propagated manually here.
-        #
-        # Tie semantics mirror the block-import path.
-        # A candidate needs a strictly higher slot to replace the store's view.
+        # A locally produced block skips the import path.
+        # Advance the justified checkpoint manually here.
+        # Leave the finalized checkpoint to head recomputation.
+        # Pinning it from this block's own state would strand it on a later reorg.
         latest_justified = store.latest_justified.advance_to(final_post_state.latest_justified)
-        latest_finalized = store.latest_finalized.advance_to(final_post_state.latest_finalized)
-
-        # Persist block and state.
-        previous_finalized_slot = store.latest_finalized.slot
         store = store.model_copy(
             update={
                 "blocks": store.blocks | {block_hash: final_block},
                 "states": store.states | {block_hash: final_post_state},
                 "latest_justified": latest_justified,
-                "latest_finalized": latest_finalized,
             }
         )
 
-        # Prune stale attestation data when finalization advances
-        if store.latest_finalized.slot > previous_finalized_slot:
-            store = self.prune_stale_attestation_data(store)
-
         return store, final_block, signatures

tests/consensus/lstar/fork_choice/test_checkpoint_sync.py

@@ -82,6 +82,55 @@ def test_store_init_from_non_genesis_anchor(
     )
 
 
+def test_head_recompute_on_anchor_below_its_finalized_slot(
+    fork_choice_test: ForkChoiceTestFiller,
+) -> None:
+    """
+    Appending a block above a mid-chain anchor whose finalized sits below it does not crash.
+
+    Given
+    -----
+    - 4 validators.
+    - a mid-chain anchor at slot 10 built without rebasing its checkpoints.
+    - the anchor state's finalized stays at the genesis boundary, slot 0.
+    - slot 0 sits below the anchor block slot.
+    - the store holds only the anchor block.
+
+    When
+    ----
+    - one block is appended above the anchor, recomputing the head over the anchor chain.
+
+    Then
+    ----
+    - head advances to the appended block at slot 11.
+    - finalized stays at the trusted anchor at slot 10.
+    - the parent walk stops at the anchor, so head recomputation does not raise.
+    """
+    anchor_state, anchor_block = build_anchor(
+        synced=False, num_validators=NUM_VALIDATORS, anchor_slot=ANCHOR_SLOT
+    )
+
+    fork_choice_test(
+        anchor_state=anchor_state,
+        anchor_block=anchor_block,
+        steps=[
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(11),
+                    parent_label="genesis",
+                    label="block_11",
+                ),
+                checks=StoreChecks(
+                    head_slot=Slot(11),
+                    head_root_label="block_11",
+                    latest_finalized_slot=ANCHOR_SLOT,
+                    latest_finalized_root_label="genesis",
+                ),
+            ),
+        ],
+    )
+
+
 def test_extend_chain_from_non_genesis_anchor(
     fork_choice_test: ForkChoiceTestFiller,
 ) -> None:

tests/consensus/lstar/fork_choice/test_finalized_safety.py

@@ -387,3 +387,192 @@ def test_fork_above_finalized_wins_at_or_below_loses(
             ),
         ],
     )
+
+
+def test_losing_fork_higher_finalized_does_not_latch(
+    fork_choice_test: ForkChoiceTestFiller,
+) -> None:
+    """
+    A fork that finalizes a higher slot but loses head selection must not leave its
+    finalized checkpoint latched in the store.
+
+    Given
+    -----
+    - 8 validators; a slot needs 6 votes (2/3) to be justified.
+    - the chain:
+        genesis
+        - block_1(1) -> block_2(2) -> block_3(3)
+          - dead_4(4) -> dead_5(5) -> dead_6(6)
+          - heavy_7(7) -> heavy_8(8)
+    - block_2 includes V0..V5's votes for block_1.
+    - block_3 includes V0..V5's votes for block_2.
+    - the chain through block_3 justifies slot 2 and finalizes slot 1.
+    - the dead fork branches off block_3:
+        - dead_4 includes V0..V5's votes for block_3, finalizing slot 2.
+        - dead_5 includes V0..V5's votes for dead_4, finalizing slot 3.
+        - dead_6 includes V0..V5's votes for dead_5, finalizing slot 4.
+      so the dead fork reaches justified slot 5 and finalized slot 4 on dead_4.
+    - the heavy fork branches off block_3:
+        - heavy_8 includes V0..V5's votes for heavy_7, source block_2.
+        - those 6 votes justify heavy_7 at slot 7.
+        - slots 3, 4, 5, 6 between source block_2 and target heavy_7 are justifiable,
+          so the heavy fork finalizes nothing beyond slot 1.
+
+    When
+    ----
+    - the dead fork is built to justified slot 5 and finalized slot 4, then the
+      heavy fork justifies slot 7, the highest justified checkpoint in the store.
+
+    Then
+    ----
+    - the justified checkpoint moves to heavy_7 at slot 7, on the heavy fork.
+    - head moves onto the heavy fork at heavy_8.
+    - the finalized checkpoint tracks the canonical head heavy_8's state: slot 1 on
+      block_1. It must not stay at the dead fork's higher finalized slot 4 on dead_4,
+      which is not an ancestor of the head.
+
+    Reachability
+    ------------
+    - head selection starts from the justified root at heavy_7.
+    - the dead fork branches off block_3, below the justified root, so the forward
+      walk never reaches it and its finalized checkpoint cannot stay canonical.
+    """
+    fork_choice_test(
+        anchor_state=generate_pre_state(num_validators=8),
+        steps=[
+            BlockStep(
+                block=BlockSpec(slot=Slot(1), label="block_1"),
+                checks=StoreChecks(head_slot=Slot(1)),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(2),
+                    parent_label="block_1",
+                    label="block_2",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(2),
+                            target_slot=Slot(1),
+                            target_root_label="block_1",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(latest_justified_slot=Slot(1)),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(3),
+                    parent_label="block_2",
+                    label="block_3",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(3),
+                            target_slot=Slot(2),
+                            target_root_label="block_2",
+                            source_slot=Slot(1),
+                            source_root_label="block_1",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(
+                    latest_justified_slot=Slot(2),
+                    latest_finalized_slot=Slot(1),
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(4),
+                    parent_label="block_3",
+                    label="dead_4",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(4),
+                            target_slot=Slot(3),
+                            target_root_label="block_3",
+                            source_slot=Slot(2),
+                            source_root_label="block_2",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(
+                    latest_justified_slot=Slot(3),
+                    latest_finalized_slot=Slot(2),
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(5),
+                    parent_label="dead_4",
+                    label="dead_5",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(5),
+                            target_slot=Slot(4),
+                            target_root_label="dead_4",
+                            source_slot=Slot(3),
+                            source_root_label="block_3",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(
+                    latest_justified_slot=Slot(4),
+                    latest_finalized_slot=Slot(3),
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(6),
+                    parent_label="dead_5",
+                    label="dead_6",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(6),
+                            target_slot=Slot(5),
+                            target_root_label="dead_5",
+                            source_slot=Slot(4),
+                            source_root_label="dead_4",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(
+                    head_root_label="dead_6",
+                    latest_justified_slot=Slot(5),
+                    latest_finalized_slot=Slot(4),
+                    latest_finalized_root_label="dead_4",
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(7), parent_label="block_3", label="heavy_7"),
+                checks=StoreChecks(head_root_label="dead_6"),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(8),
+                    parent_label="heavy_7",
+                    label="heavy_8",
+                    attestations=[
+                        AggregatedAttestationSpec(
+                            validator_indices=[ValidatorIndex(i) for i in range(6)],
+                            slot=Slot(8),
+                            target_slot=Slot(7),
+                            target_root_label="heavy_7",
+                            source_slot=Slot(2),
+                            source_root_label="block_2",
+                        ),
+                    ],
+                ),
+                checks=StoreChecks(
+                    head_root_label="heavy_8",
+                    latest_justified_slot=Slot(7),
+                    latest_justified_root_label="heavy_7",
+                    latest_finalized_slot=Slot(1),
+                    latest_finalized_root_label="block_1",
+                ),
+            ),
+        ],
+    )