Fork choice: store.latest_finalized can latch a losing fork's higher finalized, freezing finalization

[GrapeBaBa]

Summary

on_block advances store.latest_finalized by an independent monotonic max over every imported block's post-state, decoupled from store.latest_justified and the head:

# src/lean_spec/spec/forks/lstar/fork_choice.py  (on_block)
latest_finalized = store.latest_finalized.advance_to(post_state.latest_finalized)

A fork that finalizes a higher slot but then loses head selection leaves its finalized checkpoint latched in the store. store.latest_finalized can then sit on a dead branch that is not an ancestor of the head, while store.latest_justified and head are on a different branch whose state finalized is lower.

Impact — finalization freeze (liveness)

get_attestation_target decides target justifiability against store.latest_finalized (is_justifiable_after(store.latest_finalized.slot, ...)). But the canonical state transition (process_attestations) validates each attestation's target against the state's latest_finalized (the head chain's, which is lower). When the two disagree the justifiable-slot lattice is offset, so every advancing target the validators vote is rejected (target not justifiable) and justification/finalization freezes permanently — even with full (2/3+) attestation coverage and a live, advancing head.

This was first observed as a network-wide finalization freeze in a long-running multi-subnet devnet (a client mirroring this store update): head and justification kept advancing while finalized stayed pinned. Root cause: store.latest_finalized (higher, from a block that had been reorged out) ≠ the canonical head state's latest_finalized (lower).

Root cause / when it was introduced

The original forkchoice store (#53) and the 3sf-mini reference derive the finalized checkpoint from the chosen (head / max-justified) state, so justified and finalized always come from one consistent state:

• 3sf-mini: get_latest_justified_hash(post_states) picks the max-justified state; there is no separate finalized max.
• leanSpec subspecs: add forkchoice subspec with tests #53 update_head: latest_finalized = self.states[new_head].latest_finalized (the head's state).

#194 (a1ae0916, "forkchoice: simplify store's latest_justified and latest_finalized updates") moved the finalized update out of update_head and into on_block, changing it to an independent max over post-states — which is what allows the desync. #727 later renamed that max to advance_to; #817 relocated it to fork_choice.py.

Reproduction

Added as a regression test test_losing_fork_higher_finalized_does_not_latch (see PR): a dead fork finalizes slot 4, then a heavier fork justifies slot 7 (winning the head) but finalizes only slot 1. On the current code store.latest_finalized latches dead_4 (slot 4, not an ancestor of the head); it should track the head's state (slot 1 on block_1).

Fix

Derive store.latest_finalized from the canonical head's state after head selection — restoring #53 / 3sf-mini semantics (the finalized checkpoint travels with the chosen state). PR linked below.