fix: skip finalization advance for stale finalized sources

[MegaRedHand]

Summary

Ports 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 (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.

[github-actions]

🤖 Kimi Code Review

Overall Assessment: Correct and critical safety fix for 3SF-mini finalization. The PR prevents a supermajority from rewinding finalization by voting with a stale source at or behind the finalized boundary.

Code Correctness & Security

1. Boundary Check Consistency (block_builder.rs:370, state_transition/src/lib.rs:405)

   • The fix correctly implements the 3SF-mini invariant: a source checkpoint at or behind latest_finalized is already finalized and must not trigger new finalization.
   • The use of strict inequality source.slot > finalized_slot (block builder) and early return on source.slot <= state.latest_finalized.slot (state transition) are logically equivalent and correct.

2. Vacuous Truth Protection (block_builder.rs:371-373)

   • Without the boundary check, an empty range (source.slot + 1..target.slot) (when target.slot == source.slot + 1) would make .all(...) vacuously true, incorrectly scoring the entry as Finalize when the source is already final. The fix correctly guards against this.

Performance

3. Fail-Fast Optimization (state_transition/src/lib.rs:405-408)
   • The early return occurs before the potentially expensive slot range scan ((source.slot + 1)..target.slot).any(...). This is the correct ordering—cheap checks first.

Testing

4. Regression Test Coverage
   • score_entry_does_not_finalize_source_at_boundary (block_builder.rs:695): Correctly tests the exact boundary condition (source slot == finalized slot).
   • stale_finalized_source_justifies_without_rewinding_finalization (state_transition:695): Tests the "behind boundary" case (source slot < finalized slot) and verifies monotonicity of finalization.
   • Both tests validate that justification still works while finalization remains pinned.

Nitpicks

5. Comment Clarity (block_builder.rs:367-369)
   • The comment mentions "source to lie past the finalized boundary" but could explicitly state "strictly greater than" to match the code logic, though the current phrasing is acceptable.

Verdict: Ship it. This is a precise, minimal fix for a consensus safety bug with excellent test coverage.

---

Automated review by Kimi (Moonshot AI) · kimi-k2.5 · custom prompt

[github-actions]

🤖 Claude Code Review

Here is the review:

---

PR #405 — fix: skip finalization advance for stale finalized sources

Overview: This ports leanSpec #802 — the correct fix for spurious re-finalization from stale/boundary sources. Rather than rejecting such attestations (the approach in #402), the spec now accepts the justification and only guards the finalization advancement. Two symmetric guards are added: one in try_finalize (state transition) and one in score_entry (block builder).

---

Correctness

The root bug (boundary case, source.slot == finalized_slot):

In try_finalize, the pre-fix logic was:

if ((source.slot + 1)..target.slot).any(|slot| justifiable(slot, finalized)) {
    return; // gaps remain — don't finalize
}
// else: advance finalization

With source.slot == finalized_slot and target.slot == finalized_slot + 1, the range is (finalized+1..finalized+1) — empty. .any(...) on an empty range is false, so the guard is skipped and finalization "advances" to the same boundary. The new if source.slot <= state.latest_finalized.slot { return; } guard correctly short-circuits before this.

The same vacuous-truth hazard appeared in score_entry with .all(...) on an empty range returning true, mis-tiering the entry as Finalize. The new att_data.source.slot > projected_finalized_slot guard fixes this symmetrically.

Both guards use strict > — this correctly excludes the boundary (==) case in addition to truly stale sources.

The stale case (source.slot < finalized_slot):
Per the PR description, the finalized post-state was already correct here (underflow in slot_is_justifiable_after returns false, and the finalized slot falls in the scan range, short-circuiting). The guard's effect is removing the spurious inc_finalizations("error") side-effect, which is a worthwhile cleanup.

Symmetry: The two guards mirror each other precisely, and the comment in block_builder.rs explicitly cross-references try_finalize. Good.

---

Tests

score_entry_does_not_finalize_source_at_boundary — covers the genuine behavioral bug (empty-range vacuous-truth case) in the block builder. Clear and well-targeted.

stale_finalized_source_justifies_without_rewinding_finalization — verifies that a stale source (slot 1 < finalized 4) still justifies a new target without moving finalization. This is valuable, but it tests the already-correct code path (where the pre-fix logic happened to be safe). The actual behavioral regression — the boundary case source.slot == finalized_slot in the state transition — has no dedicated test in state_transition/src/lib.rs.

Suggestion: Add a companion test in state_transition for source.slot == finalized_slot, analogous to score_entry_does_not_finalize_source_at_boundary. Something like:

// source = finalized = slot 4, target = slot 5
// Empty scan range would spuriously re-finalize without the guard.
// After fix: justified advances to 5, finalized stays at 4.
fn boundary_source_justifies_without_re_finalizing() { ... }

This directly exercises the code path described as "the genuine behavioral fix" in the PR body.

---

Minor Points

• The test AttestationData in score_entry_does_not_finalize_source_at_boundary sets head == target (both slot 5, root [5u8;32]). This is fine and consistent with how other tests in the file construct AttestationData.
• The updated doc comments in both files accurately reflect the new semantics. They're on the longer side relative to the CLAUDE.md guidance, but for a consensus-critical invariant change this level of explanation is justified.

---

Summary

The fix is correct, minimal, and well-reasoned. The only gap is the missing boundary-case test in state_transition. Everything else — the symmetric guards, updated comments, and existing tests — is solid.

---

Automated review by Claude (Anthropic) · sonnet · custom prompt

[github-actions]

🤖 Codex Code Review

No blocking findings in the reviewed diff.

The core fix looks correct: lib.rs now rejects finalization attempts when source.slot <= latest_finalized.slot, which closes the rewind path without preventing the newer target from becoming justified, and block_builder.rs mirrors the same constraint so block-building stays aligned with STF behavior. The added regressions exercise both sides of that invariant.

Residual risk: this was a static review only. I could not run the new tests in this sandbox because Cargo needs to fetch/write external dependencies (lean-multisig via git), which is blocked here.

---

Automated review by OpenAI Codex · gpt-5.4 · custom prompt

[greptile-apps]

Greptile Summary

Ports leanSpec #802: gates finalization advancement on source.slot > finalized_slot, preventing a stale or boundary source checkpoint from rewinding or spuriously re-finalizing an already-final boundary.

• try_finalize (state transition): adds an early-return guard if source.slot <= state.latest_finalized.slot before the scan. Stale sources already hit the error metric due to finalized_slot being justifiable inside the scan range; the boundary case (source.slot == finalized_slot, empty scan) vacuously passed .any(...) and spuriously re-finalized. Both are now silently skipped.
• score_entry (block builder): mirrors the guard in the finalizes predicate so a boundary-source entry is scored Tier::Justify rather than Tier::Finalize.
• Two regression tests added — one per crate — directly targeting the boundary-case vacuous-truth bug.

Confidence Score: 5/5

Safe to merge — the change is a targeted spec-alignment fix with no regressions in the surrounding logic.

Both changed sites (state transition and block builder) receive the identical guard, the boundary-case vacuous-truth bug is directly reproduced and fixed by the new tests, and the pre-existing stale-source path now exits cleanly instead of incrementing a misleading error metric. The fix is additive (an early-return and a short-circuit &&), leaving all downstream finalization logic untouched.

No files require special attention.

Important Files Changed

Filename	Overview
crates/blockchain/state_transition/src/lib.rs	Adds a 6-line early-return guard to try_finalize plus a well-constructed regression test; guard logic is correct and matches the spec change.
crates/blockchain/src/block_builder.rs	Adds source.slot > projected_finalized_slot to the finalizes conjunction and a regression test for the boundary mis-tier; mirrors the state-transition guard correctly.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A[Supermajority attestation crosses 2/3 threshold] --> B{source.slot <= finalized_slot?}
    B -- Yes: stale or boundary source --> C[Return early / score as Justify\nNo finalization advance]
    B -- No: source is past finalized boundary --> D{Any slot in source+1..target\nis justifiable?}
    D -- Yes: gap exists --> E[Block finalization\ninc_finalizations error]
    D -- No: source and target are consecutive --> F[Advance finalized to source\ninc_finalizations success\nShift justified_slots window\nPrune stale justifications]

Loading

_{Reviews (1): Last reviewed commit: "fix: skip finalization advance for stale..." | Re-trigger Greptile}