fix(fork-choice): state store invariants; reject attestations off the finalized subtree

[tcoratger]

What

Addresses the four unstated fork-choice store invariants in #1176. After a four-specialist analysis (fork-choice safety, API design, tests, docs), the conclusion is that none of the four is an exploitable bug today — three hold by construction and are now documented; one is closed with a typed rejection. This is primarily an invariant-stating PR plus one robustness hardening.

Item	Verdict	Change
M-1 justified ⊒ finalized	Holds by construction	Documentation
M-2 admit/prune asymmetry	Not a safety bug; DoS + idempotence gap	Code + vector
M-3 prune vs reorg-mutable finalized	Document-only (monotonicity is unsafe — see below)	Documentation + open question
M-4 blocks.keys() == states.keys()	Holds by construction	Documentation

M-1 — justified descends from finalized

Documented as an invariant on the justified checkpoint and on the slot-only advance_to. It holds by construction: every post-state finalizes an ancestor of what it justifies, and update_head anchors the LMD walk at the justified root, so the head (and the head-derived finalized) stay on one chain with justified. No code change.

M-2 — attestation admission now mirrors the prune predicate

validate_attestation previously never checked that a vote's head descends from latest_finalized, while prune_stale_attestation_data drops exactly those heads. So a re-gossiped stale aggregate re-entered the pool after pruning removed it. Such a vote carries zero fork-choice weight (an off-finalized head never sits under the justified anchor the LMD walk descends from), so this is not a safety fix — it closes a pool-inflation / signature-verification DoS amplifier and restores prune idempotence.

• New RejectionReason.HEAD_NOT_DESCENDANT_OF_FINALIZED.
• The guard uses the ancestry form (_checkpoint_is_ancestor(store, latest_finalized, head)), so a head equal to the finalized checkpoint is admitted — genesis votes are not wrongly rejected.
• Only stale / orphaned-branch votes are rejected; a live honest vote always descends from finalized.

Test-harness fix included

The regression gate surfaced that the block-builder harness (build_signed_block_with_store) was synthesizing a block's aggregate by replaying signatures through the gossip path (on_gossip_attestation → validate_attestation). The real on_block never gossip-validates block-carried attestations — it verifies proofs and runs the state transition. The harness now seeds the signature pool directly, so it no longer re-validates block attestations against the current finalized checkpoint. The pruning test is reworked to seed stale entries via still-valid gossip that a later finalization strands, and a new proving vector locks the guard (prune → re-gossip → rejected, asserting the full message).

M-3 — pruning against a reorg-mutable finalized (documented, not changed)

We deliberately do not make latest_finalized monotone, and this is the one item worth maintainer attention.

The tempting fix — take the slot-wise max of the old and head-derived finalized in update_head, matching the monotone finalized_checkpoint in consensus-specs — is unsafe here. leanSpec anchors fork choice at the justified root, not finalized, and has no filter_block_tree forcing the head to descend from finalized. update_head keeps latest_finalized on the canonical chain only by re-deriving it from the head each call. Pinning it monotonically lets it drift onto an orphaned branch, where it (a) is no longer an ancestor of the head and (b) inflates the LMD staleness cutoff, silently dropping live votes for the canonical branch. It buys nothing under honest majority (the two values coincide whenever accountable safety holds) and is strictly worse under a ≥1/3 safety fault. The existing prune gate (prune only fires when finalized advances to an on-chain value) prevents the catastrophic mass-prune, but the invariant break and cutoff distortion are real.

A genuinely monotone, economically-final latest_finalized would require adopting the consensus-specs machinery wholesale: guard the justified advance so justified only moves to descendants of finalized, filter the block tree to descendants of finalized, and re-anchor LMD-GHOST at finalized. That is a fork-choice redesign, not a localized fix.

Open question for maintainers: do we want to migrate leanSpec's fork choice to be finalized-anchored (filter_block_tree style) so that a monotone finalized becomes well-defined? If yes, that belongs in its own design proposal. This PR documents the invariant update_head actually maintains (finalized is always an ancestor of the head, reorg-mutable, not a safety guarantee).

M-4 — blocks/states share one key set

Documented as an invariant on the store; the dependent asserts are relabelled as provably-unreachable internal checks. Blocks and states are only ever written as a matched pair, so the invariant holds by construction. A Pydantic model_validator would be the wrong tool here — it is bypassed by model_copy and would swallow the domain error — so the honest remedy is documentation plus the existing asserts.

Credit

Found via the Lean 4 formalization of this spec (NyxFoundation/formal-leanSpec): each item is a clause a Store.WellFormed predicate had to assume because the spec did not guarantee it.

Testing

New and reworked consensus vectors fill green and deterministically; just check passes.

Refs #1176

🤖 Generated with Claude Code