fix: skip finalization advance for stale finalized sources (#405)

## Summary

Ports [leanSpec #802](leanEthereum/leanSpec#802)
to ethlambda.

A supermajority attestation whose source checkpoint sits **at or behind
the finalized boundary** is a valid justification anchor
(`is_slot_justified` treats slots `<= finalized.slot` as already
justified), so it may justify a newer target. But once it crosses the
supermajority threshold, the finalization logic scanned `source.slot + 1
.. target.slot` and could try to advance (rewind/re-finalize) below the
finalized boundary.

The fix gates finalization advancement on `source.slot >
finalized_slot`. Stale or boundary sources may still justify newer
targets; they no longer try to rewind or scan below the finalized
boundary.

## Relationship to #402

This supersedes
[#402](#402) (`fix(stf):
reject blocks justifying a target whose source is below finalized`),
which was the pre-#802 attempt that fixed the issue by *rejecting* such
blocks. The spec instead **accepts** the justification and only skips
the finalization advance, so this PR follows the merged spec approach.
#402 can be closed in favor of this.

## Changes

Two mirrored spots get the `source.slot > finalized_slot` guard:

| Location | Role |
|----------|------|
| `try_finalize` (state transition) | The actual finalization advance |
| `score_entry` (block builder) | Projects/scores finalization while
packing blocks |

## Tests

- `state_transition`:
`stale_finalized_source_justifies_without_rewinding_finalization` —
supermajority from a stale source justifies the target while
finalization stays pinned.
- `block_builder`: `score_entry_does_not_finalize_source_at_boundary` —
a boundary source is scored `Justify`, not `Finalize`.

```
cargo test -p ethlambda-state-transition --lib   # 2 passed
cargo test -p ethlambda-blockchain --lib block_builder   # 8 passed
```

fmt + clippy (`-D warnings`) clean on both crates.

Co-authored-by: Pablo Deymonnaz <pdeymon@fi.uba.ar>

Author: MegaRedHand

crates/blockchain/src/block_builder.rs

@@ -364,10 +364,14 @@ fn score_entry(
     let total = prior_count + new_voters.len();
     let crosses_2_3 = 3 * total >= 2 * validator_count;
 
-    // 3SF-mini finalization requires no slot strictly between source.slot
-    // and target.slot to still be justifiable (so source and target are
-    // consecutive justified checkpoints in the projected post-state).
+    // 3SF-mini finalization requires the source to lie past the finalized
+    // boundary (a source at or behind it is already final and must not
+    // re-finalize) and no slot strictly between source.slot and target.slot to
+    // still be justifiable (so source and target are consecutive justified
+    // checkpoints in the projected post-state). Mirrors `try_finalize` in the
+    // state transition.
     let finalizes = crosses_2_3
+        && att_data.source.slot > projected_finalized_slot
         && (att_data.source.slot + 1..att_data.target.slot)
             .all(|s| !slot_is_justifiable_after(s, projected_finalized_slot));
 
@@ -688,6 +692,52 @@ mod tests {
         bits
     }
 
+    /// Regression (leanSpec #802): a supermajority entry whose source sits at
+    /// the finalized boundary must be scored `Justify`, not `Finalize`. Such a
+    /// source is already final, so it advances nothing; the empty scan range
+    /// `(source.slot + 1..target.slot)` would otherwise make `.all(...)`
+    /// vacuously true and mis-tier the entry as a finalizer.
+    #[test]
+    fn score_entry_does_not_finalize_source_at_boundary() {
+        const NUM_VALIDATORS: usize = 4;
+        const FINALIZED_SLOT: u64 = 4;
+
+        // Source at the finalized boundary, target one slot ahead (empty scan).
+        let att_data = AttestationData {
+            slot: 7,
+            head: Checkpoint {
+                slot: 5,
+                root: H256([5u8; 32]),
+            },
+            target: Checkpoint {
+                slot: 5,
+                root: H256([5u8; 32]),
+            },
+            source: Checkpoint {
+                slot: FINALIZED_SLOT,
+                root: H256([4u8; 32]),
+            },
+        };
+
+        // Supermajority (3 of 4) so the entry crosses 2/3.
+        let proofs = vec![AggregatedSignatureProof::empty(make_bits(&[0, 1, 2]))];
+
+        let (score, _) = score_entry(
+            &att_data,
+            &proofs,
+            &HashMap::new(),
+            FINALIZED_SLOT,
+            NUM_VALIDATORS,
+        )
+        .expect("entry contributes new voters");
+
+        assert_eq!(
+            score.tier,
+            Tier::Justify,
+            "source at the finalized boundary must justify, not finalize"
+        );
+    }
+
     /// Regression test for https://github.com/lambdaclass/ethlambda/issues/259
     ///
     /// Simulates a stall scenario by populating the payload pool with 50

crates/blockchain/state_transition/src/lib.rs

@@ -387,16 +387,25 @@ fn is_valid_vote(state: &State, data: &AttestationData) -> bool {
 
 /// Attempt to advance finalization from source to target.
 ///
-/// Finalization succeeds when there are no justifiable slots between
-/// source.slot and target.slot (exclusive). When finalization advances,
-/// shifts the justified_slots window and prunes stale justifications.
+/// Finalization advances only when the source lies past the old finalized point
+/// and there are no justifiable slots between source.slot and target.slot
+/// (exclusive). A source at or behind the finalized boundary is already final:
+/// it may justify a newer target, but it must not re-finalize or scan below the
+/// finalized boundary. When finalization advances, shifts the justified_slots
+/// window and prunes stale justifications.
 fn try_finalize(
     state: &mut State,
     source: Checkpoint,
     target: Checkpoint,
     justifications: &mut HashMap<H256, Vec<bool>>,
     root_to_slot: &HashMap<H256, u64>,
 ) {
+    // A stale or boundary source is already finalized; advancing from it would
+    // rewind the finalized checkpoint and scan slots below the boundary.
+    if source.slot <= state.latest_finalized.slot {
+        return;
+    }
+
     // Consider whether finalization can advance.
     if ((source.slot + 1)..target.slot)
         .any(|slot| slot_is_justifiable_after(slot, state.latest_finalized.slot))
@@ -683,4 +692,72 @@ mod tests {
         );
         assert_eq!(state.latest_justified.root, r9);
     }
+
+    /// Regression (leanSpec #802): a supermajority attestation whose source sits
+    /// at or behind the finalized boundary may justify a newer target, but must
+    /// never advance (rewind) finalization below that boundary.
+    ///
+    /// Setup: finalized = justified = slot 4. A supermajority votes from a stale
+    /// source at slot 1 to a fresh target at slot 6 (Δ=2 is pronic, so the target
+    /// is justifiable). The target should become justified while the finalized
+    /// checkpoint stays pinned at slot 4.
+    #[test]
+    fn stale_finalized_source_justifies_without_rewinding_finalization() {
+        const NUM_VALIDATORS: usize = 4;
+        let r1 = H256([1u8; 32]);
+        let r4 = H256([4u8; 32]);
+        let r6 = H256([6u8; 32]);
+
+        let mut hashes: Vec<H256> = vec![H256::ZERO; 7];
+        hashes[1] = r1;
+        hashes[4] = r4;
+        hashes[6] = r6;
+
+        let validators = make_validators(NUM_VALIDATORS);
+        // Window is relative to finalized=4; cover up to slot 6 (slots 5 and 6).
+        let mut justified_slots = JustifiedSlots::new();
+        justified_slots_ops::extend_to_slot(&mut justified_slots, 4, 6);
+
+        let mut state = State {
+            config: ChainConfig { genesis_time: 0 },
+            slot: 7,
+            latest_block_header: BlockHeader {
+                slot: 6,
+                proposer_index: 0,
+                parent_root: H256::ZERO,
+                state_root: H256::ZERO,
+                body_root: BlockBody::default().hash_tree_root(),
+            },
+            latest_justified: Checkpoint { slot: 4, root: r4 },
+            latest_finalized: Checkpoint { slot: 4, root: r4 },
+            historical_block_hashes: SszList::try_from(hashes).unwrap(),
+            justified_slots,
+            validators: SszList::try_from(validators).unwrap(),
+            justifications_roots: Default::default(),
+            justifications_validators: JustificationValidators::new(),
+        };
+
+        // Supermajority (3 of 4) attesting from the stale source (slot 1) to the
+        // fresh target (slot 6). Source slot 1 <= finalized 4, so it is implicitly
+        // justified and passes is_valid_vote.
+        let atts: Vec<AggregatedAttestation> = vec![make_attestation(
+            7,
+            (1, r1),
+            (6, r6),
+            (6, r6),
+            &[0, 1, 2],
+            NUM_VALIDATORS,
+        )];
+        let atts: AggregatedAttestations = atts.try_into().unwrap();
+
+        process_attestations(&mut state, &atts).expect("process_attestations should succeed");
+
+        // The target is justified.
+        assert_eq!(state.latest_justified.slot, 6);
+        assert_eq!(state.latest_justified.root, r6);
+        // Finalization stays pinned at the boundary: the stale source must not
+        // rewind or re-finalize.
+        assert_eq!(state.latest_finalized.slot, 4);
+        assert_eq!(state.latest_finalized.root, r4);
+    }
 }