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

packages/testing/src/consensus_testing/test_types/block_spec.py

@@ -11,16 +11,16 @@
 from lean_spec.base import CamelModel
 from lean_spec.spec.crypto.merkleization import hash_tree_root
 from lean_spec.spec.crypto.xmss.containers import PublicKey, Signature
-from lean_spec.spec.forks import AggregationBits, Interval, Slot, ValidatorIndex
+from lean_spec.spec.forks import AggregationBits, Slot, ValidatorIndex
 from lean_spec.spec.forks.lstar.containers import (
     AggregatedAttestation,
     AggregatedAttestations,
     Attestation,
     AttestationData,
+    AttestationSignatureEntry,
     Block,
     BlockBody,
     MultiMessageAggregate,
-    SignedAttestation,
     SignedBlock,
     SingleMessageAggregate,
     State,
@@ -418,35 +418,27 @@ def build_signed_block_with_store(
             parent_state, block_registry, key_manager
         )
 
-        # In-body attestations carry the block's slot.
-        # The store's time check rejects votes whose slot has not yet started locally,
-        # so advance the local clock first.
-        block_slot_interval = Interval.from_slot(self.slot)
-        if store.time < block_slot_interval:
-            store, _ = spec.on_tick(
-                store, block_slot_interval, has_proposal=True, is_aggregator=True
-            )
-
-        # Gossip valid signatures so they run through the spec's verification path.
+        # The real block-import path does not gossip-validate block-carried attestations.
+        # So seed the signature pool directly instead of routing through the gossip admission guard.
+        # That guard would wrongly reject a legitimately-includable vote whose head is now stale.
+        grouped_signatures: dict[AttestationData, set[AttestationSignatureEntry]] = {
+            existing_data: set(existing_signatures)
+            for existing_data, existing_signatures in store.attestation_signatures.items()
+        }
         for attestation in valid_attestations:
             signatures_for_data = attestation_signatures.get(attestation.data)
             if (
                 signatures_for_data is None
                 or (signature := signatures_for_data.get(attestation.validator_index)) is None
             ):
                 continue
-            store = spec.on_gossip_attestation(
-                store,
-                SignedAttestation(
-                    validator_index=attestation.validator_index,
-                    data=attestation.data,
-                    signature=signature,
-                ),
-                is_aggregator=True,
+            grouped_signatures.setdefault(attestation.data, set()).add(
+                AttestationSignatureEntry(attestation.validator_index, signature)
             )
+        store = store.model_copy(update={"attestation_signatures": grouped_signatures})
 
-        # Aggregate gossip signatures into known payloads on the local clone.
-        # Gossip pools mutate here, but the caller's gossip view must not be consumed.
+        # Aggregate the pooled signatures into known payloads on the local clone.
+        # The pools mutate here, but the caller's signature pool must not be consumed.
         # Only the freshly aggregated payloads propagate back.
         aggregation_store, _ = spec.aggregate(store)
         merged_store = spec.accept_new_attestations(aggregation_store)

src/lean_spec/spec/forks/lstar/containers/checkpoint.py

@@ -26,6 +26,10 @@ def advance_to(self, candidate: "Checkpoint") -> "Checkpoint":
 
         The candidate replaces this checkpoint only when its slot is strictly higher.
         This enforces forward-only progression for justified and finalized checkpoints.
+
+        Selection is by slot only.
+        It does not verify that the candidate's block descends from this one.
+        For justified and finalized checkpoints that ancestry is a separate store invariant.
         """
         return candidate if candidate.slot > self.slot else self
 

src/lean_spec/spec/forks/lstar/containers/store.py

@@ -40,14 +40,14 @@ class Store[StateT: Container, BlockT: Container](StrictBaseModel):
     """Root of the block a validator is safe to attest to."""
 
     latest_justified: Checkpoint
-    """Highest-slot justified checkpoint observed so far."""
+    """Highest-slot justified checkpoint observed so far; the head walk starts here."""
 
     latest_finalized: Checkpoint
     """
     Finalization as seen from the canonical head, not irreversible economic finality.
 
-    This tracks the head chain's view and is reorg-mutable.
-    A reorg onto a fork that finalized a lower slot lowers this value.
+    Re-derived from the head each update, so it is reorg-mutable and can lower on a reorg.
+    Always an ancestor of the head, never monotone, never a safety guarantee.
     """
 
     blocks: dict[Bytes32, BlockT] = Field(default_factory=dict)

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

@@ -74,6 +74,9 @@ class RejectionReason(StrEnum):
     TARGET_NOT_ANCESTOR_OF_HEAD = "TARGET_NOT_ANCESTOR_OF_HEAD"
     """The attestation target checkpoint is not an ancestor of its head."""
 
+    HEAD_NOT_DESCENDANT_OF_FINALIZED = "HEAD_NOT_DESCENDANT_OF_FINALIZED"
+    """The attestation head checkpoint does not descend from the finalized block."""
+
     ATTESTATION_TOO_FAR_IN_FUTURE = "ATTESTATION_TOO_FAR_IN_FUTURE"
     """The attestation slot is beyond the store's acceptance horizon."""
 

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

@@ -142,6 +142,8 @@ def prune_stale_attestation_data(self, store: LstarStore) -> LstarStore:
         Drop attestation data whose head can no longer influence fork choice.
 
         Fork choice only ever descends from the latest finalized block.
+        This is sound only because the finalized checkpoint is re-derived from the head each update.
+        Pruning against a finalized checkpoint that drifted off the head chain would be unsound.
         A vote carries no fork-choice weight, and is dropped, when either holds:
 
         - Its head sits at or below the finalized slot.
@@ -197,9 +199,13 @@ def validate_attestation(self, store: LstarStore, attestation_data: AttestationD
         Validate incoming attestation before processing.
 
         Ensures the vote respects the basic laws of time and topology.
+        The head must also descend from the finalized block.
+        Fork choice only descends from the finalized block, so an orphaned head carries no weight.
+        Rejecting it here stops a stale vote from re-entering after pruning drops it.
 
         Raises:
             SpecRejectionError: If the attestation fails any of the validation checks above.
+            SpecRejectionError: HEAD_NOT_DESCENDANT_OF_FINALIZED when the head is off finalized.
         """
         source_checkpoint = attestation_data.source
         target_checkpoint = attestation_data.target
@@ -270,6 +276,13 @@ def validate_attestation(self, store: LstarStore, attestation_data: AttestationD
                 "Target checkpoint must be ancestor of head",
             )
 
+        # Fork choice only ever descends from the finalized block.
+        if not self._checkpoint_is_ancestor(store, store.latest_finalized, head_checkpoint):
+            raise SpecRejectionError(
+                RejectionReason.HEAD_NOT_DESCENDANT_OF_FINALIZED,
+                "Head checkpoint must descend from the finalized block",
+            )
+
         # Head Consistency Check
         #
         # A vote cannot have observed its head before that head existed.

tests/consensus/lstar/fork_choice/test_prune_finalized_orphaned_branch.py

@@ -6,12 +6,13 @@
     AggregatedAttestationSpec,
     BlockSpec,
     BlockStep,
+    ExpectedRejection,
     ForkChoiceTestFiller,
     GossipAggregatedAttestationStep,
     StoreChecks,
     build_genesis_state,
 )
-from lean_spec.spec.forks import Slot, ValidatorIndex
+from lean_spec.spec.forks import RejectionReason, Slot, ValidatorIndex
 
 pytestmark = pytest.mark.valid_until("Lstar")
 
@@ -164,3 +165,169 @@ def test_finalization_prunes_vote_on_orphaned_branch(
             ),
         ],
     )
+
+
+def test_re_gossip_of_pruned_orphaned_vote_is_rejected(
+    fork_choice_test: ForkChoiceTestFiller,
+) -> None:
+    """
+    Re-gossiping a vote pruned onto a finalized-orphaned branch is rejected, not re-admitted.
+
+    Given
+    -----
+    - 8 validators; a slot needs 6 votes (2/3) to be justified.
+    - the chain:
+        genesis(0) -> block_1(1)
+        - block_2(2) -> block_3(3) -> block_4(4)
+        - orph_2(2) -> orph_3(3) -> orph_4(4)
+    - an aggregate from V6 targets orph_4 at slot 4, admitted while finalized is slot 1.
+    - block_4 finalizes slot 2 on block_2.
+    - orph_4 is not a descendant of block_2, so finalization pruning drops that vote.
+    - the pending pool now holds no target slots.
+    - the counted pool holds only the canonical target slot 3.
+
+    When
+    ----
+    - V6 re-gossips the same aggregate targeting orph_4 at slot 4.
+
+    Then
+    ----
+    - validation fails because the head no longer descends from the finalized block.
+    - the rejection reason is head not descendant of finalized.
+    - the pending pool still holds no target slots.
+    - the counted pool still holds only the canonical target slot 3.
+    """
+    fork_choice_test(
+        anchor_state=build_genesis_state(num_validators=8),
+        steps=[
+            BlockStep(
+                block=BlockSpec(slot=Slot(1), parent_label="genesis", 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(
+                    head_slot=Slot(2),
+                    head_root_label="block_2",
+                    latest_justified_slot=Slot(1),
+                    latest_finalized_slot=Slot(0),
+                ),
+            ),
+            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(
+                    head_slot=Slot(3),
+                    head_root_label="block_3",
+                    latest_justified_slot=Slot(2),
+                    latest_finalized_slot=Slot(1),
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(2), parent_label="block_1", label="orph_2"),
+                checks=StoreChecks(head_slot=Slot(3), head_root_label="block_3"),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(3), parent_label="orph_2", label="orph_3"),
+                checks=StoreChecks(head_slot=Slot(3), head_root_label="block_3"),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(4), parent_label="orph_3", label="orph_4"),
+                checks=StoreChecks(
+                    head_slot=Slot(3),
+                    head_root_label="block_3",
+                    latest_justified_slot=Slot(2),
+                    latest_finalized_slot=Slot(1),
+                ),
+            ),
+            GossipAggregatedAttestationStep(
+                attestation=AggregatedAttestationSpec(
+                    validator_indices=[ValidatorIndex(6)],
+                    slot=Slot(4),
+                    target_slot=Slot(4),
+                    target_root_label="orph_4",
+                    head_root_label="orph_4",
+                    head_slot=Slot(4),
+                    source_slot=Slot(0),
+                    source_root_label="genesis",
+                ),
+                checks=StoreChecks(
+                    head_slot=Slot(3),
+                    head_root_label="block_3",
+                    latest_new_aggregated_target_slots=[Slot(4)],
+                ),
+            ),
+            BlockStep(
+                block=BlockSpec(
+                    slot=Slot(4),
+                    parent_label="block_3",
+                    label="block_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(
+                    head_slot=Slot(4),
+                    head_root_label="block_4",
+                    latest_justified_slot=Slot(3),
+                    latest_finalized_slot=Slot(2),
+                    latest_finalized_root_label="block_2",
+                    latest_known_aggregated_target_slots=[Slot(3)],
+                    latest_new_aggregated_target_slots=[],
+                ),
+            ),
+            GossipAggregatedAttestationStep(
+                attestation=AggregatedAttestationSpec(
+                    validator_indices=[ValidatorIndex(6)],
+                    slot=Slot(4),
+                    target_slot=Slot(4),
+                    target_root_label="orph_4",
+                    head_root_label="orph_4",
+                    head_slot=Slot(4),
+                    source_slot=Slot(0),
+                    source_root_label="genesis",
+                ),
+                valid=False,
+                expected_rejection=ExpectedRejection(
+                    reason=RejectionReason.HEAD_NOT_DESCENDANT_OF_FINALIZED,
+                    exact_message="Head checkpoint must descend from the finalized block",
+                ),
+                checks=StoreChecks(
+                    latest_new_aggregated_target_slots=[],
+                    latest_known_aggregated_target_slots=[Slot(3)],
+                ),
+            ),
+        ],
+    )