fix: bound attestation slot against head and store clock (leanEthereum#1020)

* fix: bound attestation slot against head and store clock

The gossip attestation validator fed the unbounded wire field
attestation_data.slot straight into the interval conversion, which
multiplies it by the intervals-per-slot count and wraps the product in a
range-checked unsigned 64-bit constructor. A crafted gossip attestation
with a near-2**64 slot raised a pydantic validation error that escaped
the gossip handler's rejection-only catch and crashed the node, a
one-message remote denial of service.

The root cause is that the slot was never tied to the head it claims.
This change adds two checks after the topology checks:

- The vote's slot must not precede the slot of the head block it claims
  to have seen, surfaced as a new ATTESTATION_SLOT_BEFORE_HEAD rejection.
  This anchors the wire slot from below by a known block and enforces the
  3SF attestation semantics where the slot records when the head was seen.
- The future-time gate now compares in slot units with plain-int
  arithmetic before constructing any interval, so a near-ceiling slot is
  rejected cleanly instead of overflowing. The integer comparison is
  equivalent to the previous interval comparison.

Adds two negative consensus vectors: one for a slot at the unsigned
64-bit ceiling rejected without overflow, and one for a slot preceding
its head. All 115 fork-choice vectors still fill green.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs: align attestation slot-bound comments with doc rules

Split multi-clause sentences onto their own lines and replace
code-identifier-style names (intervals_per_slot, horizon) in the
head-consistency and time-check comments with plain English, per
the documentation rules. No behavior change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

* docs: simplify attestation slot-bound comments

Cut the head-consistency and time-check comments to their essential
reason (two lines each) and shorten the new rejection-reason docstring.
No behavior change.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

---------

Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: tcoratger

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

@@ -77,6 +77,9 @@ class RejectionReason(StrEnum):
     ATTESTATION_TOO_FAR_IN_FUTURE = "ATTESTATION_TOO_FAR_IN_FUTURE"
     """The attestation slot is beyond the store's acceptance horizon."""
 
+    ATTESTATION_SLOT_BEFORE_HEAD = "ATTESTATION_SLOT_BEFORE_HEAD"
+    """The attestation slot precedes its head block's slot."""
+
     VALIDATOR_NOT_IN_STATE = "VALIDATOR_NOT_IN_STATE"
     """The referenced validator does not exist in the state registry."""
 

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

@@ -9,6 +9,7 @@
 from lean_spec.spec.forks.lstar._base import LstarSpecBase, LstarStore
 from lean_spec.spec.forks.lstar.config import (
     GOSSIP_DISPARITY_INTERVALS,
+    INTERVALS_PER_SLOT,
     MAX_ATTESTATIONS_DATA,
 )
 from lean_spec.spec.forks.lstar.containers import (
@@ -185,7 +186,8 @@ def validate_attestation(self, store: LstarStore, attestation_data: AttestationD
             3. The head must be at least as recent as source and target.
             4. Checkpoint slots must match the actual block slots.
             5. Source, target, and head must lie on one parent chain.
-            6. The vote's slot must have started locally (a small disparity margin is allowed).
+            6. The vote's slot cannot precede the slot of the head it claims to have seen.
+            7. The vote's slot must have started locally (a small disparity margin is allowed).
 
         Raises:
             SpecRejectionError: If the attestation fails any of the validation checks above.
@@ -259,6 +261,16 @@ def validate_attestation(self, store: LstarStore, attestation_data: AttestationD
                 "Target checkpoint must be ancestor of head",
             )
 
+        # Head Consistency Check
+        #
+        # A vote cannot have observed its head before that head existed.
+        # This lower bound also keeps the wire slot clear of the 2**64 overflow edge.
+        if attestation_data.slot < head_checkpoint.slot:
+            raise SpecRejectionError(
+                RejectionReason.ATTESTATION_SLOT_BEFORE_HEAD,
+                "Attestation slot precedes head",
+            )
+
         # Time Check
         #
         # Reject votes whose slot has not started, with a small clock-skew margin.
@@ -270,8 +282,12 @@ def validate_attestation(self, store: LstarStore, attestation_data: AttestationD
         #     interval 45  ->  admitted only by a whole-slot margin, a full slot early
         #
         # The early window lets an adversary pre-publish next-slot aggregates.
-        attestation_start_interval = Interval.from_slot(attestation_data.slot)
-        if attestation_start_interval > store.time + Interval(GOSSIP_DISPARITY_INTERVALS):
+        #
+        # Work in slot units, not intervals.
+        # Multiplying a near-2**64 wire slot into intervals would overflow and crash first.
+        admission_horizon_interval = int(store.time) + int(GOSSIP_DISPARITY_INTERVALS)
+        max_admissible_slot = admission_horizon_interval // int(INTERVALS_PER_SLOT)
+        if int(attestation_data.slot) > max_admissible_slot:
             raise SpecRejectionError(
                 RejectionReason.ATTESTATION_TOO_FAR_IN_FUTURE, "Attestation too far in future"
             )
@@ -322,6 +338,7 @@ def on_gossip_attestation(
             # - their slots are ordered source <= target <= head,
             # - each checkpoint slot matches its block's actual slot from the store,
             # - source, target, and head lie on one parent chain,
+            # - the vote's slot is not before the head block's slot,
             # - the vote's slot has already started locally with a small margin.
             self.validate_attestation(store, attestation_data)
 
@@ -428,6 +445,7 @@ def on_gossip_aggregated_attestation(
         # - their slots are ordered source <= target <= head,
         # - each checkpoint slot matches its block's actual slot from the store,
         # - source, target, and head lie on one parent chain,
+        # - the vote's slot is not before the head block's slot,
         # - the vote's slot has already started locally with a small margin.
         self.validate_attestation(store, attestation_data)
 

tests/consensus/lstar/fork_choice/test_gossip_attestation_validation.py

@@ -1001,6 +1001,118 @@ def test_attestation_head_on_sibling_fork_rejected(
     )
 
 
+def test_attestation_slot_near_uint64_max_rejected(
+    fork_choice_test: ForkChoiceTestFiller,
+) -> None:
+    """
+    A vote with a slot near the unsigned 64-bit ceiling is rejected without overflow.
+
+    Given
+    -----
+    - 4 validators.
+    - the chain:
+        block_1(1) -> block_2(2)
+    - local time is at slot 2.
+
+    When
+    ----
+    - V1 gossips a vote naming target block_2 at slot 2.
+    - the vote's own slot is the largest unsigned 64-bit value.
+
+    Then
+    ----
+    - validation fails with attestation too far in future.
+
+    Regression
+    ----------
+    - an earlier rule multiplied the wire slot into intervals before the bound check.
+    - a near-ceiling slot overflowed the interval constructor and crashed the node.
+    """
+    fork_choice_test(
+        steps=[
+            BlockStep(
+                block=BlockSpec(slot=Slot(1), label="block_1"),
+                checks=StoreChecks(head_slot=Slot(1)),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(2), label="block_2"),
+                checks=StoreChecks(head_slot=Slot(2)),
+            ),
+            AttestationStep(
+                attestation=GossipAttestationSpec(
+                    validator_index=ValidatorIndex(1),
+                    slot=Slot(2**64 - 1),
+                    target_slot=Slot(2),
+                    target_root_label="block_2",
+                    head_slot=Slot(2),
+                    head_root_label="block_2",
+                    valid_signature=False,
+                ),
+                valid=False,
+                expected_rejection=ExpectedRejection(
+                    reason=RejectionReason.ATTESTATION_TOO_FAR_IN_FUTURE,
+                    message_substring="Attestation too far in future",
+                ),
+            ),
+        ],
+    )
+
+
+def test_attestation_slot_before_head_rejected(
+    fork_choice_test: ForkChoiceTestFiller,
+) -> None:
+    """
+    A vote whose slot precedes the slot of its head block is rejected.
+
+    Given
+    -----
+    - 4 validators.
+    - the chain:
+        block_1(1) -> block_2(2) -> block_3(3)
+
+    When
+    ----
+    - V1 gossips a vote with target block_2 at slot 2 and head block_3 at slot 3.
+    - the vote's own slot is 2, before the head block's slot 3.
+
+    Then
+    ----
+    - validation fails because the vote slot precedes the head it claims to have seen.
+    """
+    fork_choice_test(
+        steps=[
+            BlockStep(
+                block=BlockSpec(slot=Slot(1), label="block_1"),
+                checks=StoreChecks(head_slot=Slot(1)),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(2), label="block_2"),
+                checks=StoreChecks(head_slot=Slot(2)),
+            ),
+            BlockStep(
+                block=BlockSpec(slot=Slot(3), label="block_3"),
+                checks=StoreChecks(head_slot=Slot(3)),
+            ),
+            AttestationStep(
+                attestation=GossipAttestationSpec(
+                    validator_index=ValidatorIndex(1),
+                    slot=Slot(2),
+                    target_slot=Slot(2),
+                    target_root_label="block_2",
+                    head_slot=Slot(3),
+                    head_root_label="block_3",
+                    valid_signature=False,
+                ),
+                valid=False,
+                expected_rejection=ExpectedRejection(
+                    reason=RejectionReason.ATTESTATION_SLOT_BEFORE_HEAD,
+                    message_substring="Attestation slot precedes head",
+                ),
+            ),
+        ],
+    )
+
+
 def test_attestation_source_on_sibling_fork_rejected(
     fork_choice_test: ForkChoiceTestFiller,
 ) -> None: