Use original finalized slot for justifiability and finalization gap checks#212
Use original finalized slot for justifiability and finalization gap checks#212pablodeymo wants to merge 1 commit intomainfrom
Conversation
…hecks The spec uses self.latest_finalized.slot (immutable) for the justifiability check (Rule 6) and the finalization gap check, while using a separate local mutable finalized_slot for is_slot_justified (Rules 1-2) and window shifts. The code was using state.latest_finalized.slot (mutable) for all of these, which diverges from the spec when finalization advances mid-processing: the first attestation group can trigger finalization, changing latest_finalized.slot and altering the justifiability check for subsequent attestations. Capture original_finalized_slot before the attestation loop and pass it to is_valid_vote (Rule 6) and try_finalize (gap check) to match the spec.
🤖 Kimi Code ReviewReview SummaryThe PR correctly implements the consensus spec requirement to use the original finalized slot (before attestation processing) for justifiability checks. This prevents a critical consensus bug where finalization could incorrectly advance based on attestations processed within the same state transition. Issues Found1. Critical Bug in
|
🤖 Codex Code ReviewNo blocking findings in this diff.
Validation note: I could not run tests in this environment due sandbox/toolchain constraints ( Automated review by OpenAI Codex · custom prompt |
🤖 Claude Code ReviewHere is the review: Review: Use original finalized slot for justifiability and finalization gap checksSummary: Consensus-critical bug fix. The change is correct, minimal, and well-aligned with the leanSpec reference implementation. CorrectnessThe core fix is sound. The spec (
The Rust code now correctly maps these:
Specifically:
The invariant also holds for multiple finalization events within a single call to Pre-existing concern (not introduced by this PR)
justifications.retain(|root, _| {
let slot = root_to_slot[root];
slot > state.latest_finalized.slot
});The index operator Testing gapThe PR description correctly notes the divergence requires a block with multiple attestation groups where the first triggers finalization — a rare but constructible scenario. No regression test is added. A targeted spec test exercising this exact path (two attestation groups, first causes finalization, second group's validity changes based on which finalized slot is used) would close this coverage gap and prevent accidental reintroduction. Minor notes
OverallThe fix is correct, the implementation is clean, and the comments are accurate. The exploitability analysis is on point — a block builder controlling attestation ordering could trigger a consensus split across clients. Approve pending the suggestion to add a targeted regression test. Automated review by Claude (Anthropic) · custom prompt |
Greptile SummaryThis PR restores a frozen
Confidence Score: 2/5
|
| Filename | Overview |
|---|---|
| crates/blockchain/state_transition/src/lib.rs | Re-introduces original_finalized_slot snapshot for Rule 6 and finalization gap checks — directly conflicts with the behavior added by commit 9c7f5f6 (PR #203, merged one day prior) which explicitly followed leanSpec PR #443 to use the live state.latest_finalized.slot; spec authority needs resolution before merging. |
Flowchart
%%{init: {'theme': 'neutral'}}%%
flowchart TD
A[process_attestations starts] --> B["Snapshot: original_finalized_slot = state.latest_finalized.slot"]
B --> C[For each attestation in block]
C --> D["is_valid_vote(state, source, target, original_finalized_slot)"]
D --> E["Rules 1-2: is_slot_justified\nuses state.latest_finalized.slot\n(live / mutable)"]
D --> F["Rule 6: slot_is_justifiable_after\nuses original_finalized_slot\n(frozen snapshot)"]
E --> G{Vote valid?}
F --> G
G -- No --> C
G -- Yes --> H[Record vote, check supermajority]
H --> I{Supermajority reached?}
I -- No --> C
I -- Yes --> J["set_justified (uses live state.latest_finalized.slot)"]
J --> K["try_finalize(state, source, target, original_finalized_slot, ...)"]
K --> L["Gap check: slot_is_justifiable_after\nuses original_finalized_slot\n(frozen snapshot)"]
L --> M{Any justifiable slot\nin gap?}
M -- Yes --> N[Abort finalization]
N --> C
M -- No --> O["state.latest_finalized = source\n(live state UPDATED here)"]
O --> P[Shift justified_slots window]
P --> Q[Prune stale justifications]
Q --> C
C --> R[serialize_justifications]
style B fill:#f9c74f,stroke:#f3722c
style F fill:#f9c74f,stroke:#f3722c
style L fill:#f9c74f,stroke:#f3722c
style E fill:#90be6d,stroke:#43aa8b
style J fill:#90be6d,stroke:#43aa8b
style O fill:#e63946,stroke:#c1121f,color:#fff
Comments Outside Diff (1)
-
crates/blockchain/state_transition/src/lib.rs, line 249-256 (link)No regression test for the triggering scenario
The PR description itself notes: "A targeted spec test exercising this path would further strengthen coverage." The specific scenario — a block with multiple attestation groups where the first group triggers finalization — is the only observable way to distinguish the old behavior from the new. Without a test fixture, the existing 108 tests cannot verify the fix is correct nor catch a future accidental regression.
Consider adding a test fixture to
leanSpec/fixtures/consensus/state_transition/(or a Rust unit test) that:- Sets
latest_finalized.slot = 0. - Includes a block with two attestation groups: group 1 triggers finalization (advancing to slot 5), group 2 has a target at slot 11.
- Asserts the expected post-state differs from the pre-fix behavior.
Prompt To Fix With AI
This is a comment left during a code review. Path: crates/blockchain/state_transition/src/lib.rs Line: 249-256 Comment: **No regression test for the triggering scenario** The PR description itself notes: *"A targeted spec test exercising this path would further strengthen coverage."* The specific scenario — a block with multiple attestation groups where the first group triggers finalization — is the only observable way to distinguish the old behavior from the new. Without a test fixture, the existing 108 tests cannot verify the fix is correct nor catch a future accidental regression. Consider adding a test fixture to `leanSpec/fixtures/consensus/state_transition/` (or a Rust unit test) that: 1. Sets `latest_finalized.slot = 0`. 2. Includes a block with two attestation groups: group 1 triggers finalization (advancing to slot 5), group 2 has a target at slot 11. 3. Asserts the expected post-state differs from the pre-fix behavior. How can I resolve this? If you propose a fix, please make it concise.
- Sets
Prompt To Fix All With AI
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 215-219
Comment:
**Directly conflicts with the recently-merged commit #203 (`9c7f5f6`)**
This PR re-introduces `original_finalized_slot` and uses it for Rule 6 and the finalization gap check — but commit `9c7f5f6` (merged yesterday, March 12) *explicitly removed this snapshot* to align with [leanSpec PR #443](https://github.com/leanEthereum/leanSpec/pull/443). That commit's message states:
> "The above PR in leanSpec removed the use of the `original_finalized_slot` snapshot and changed it to using the updated `latest_finalized.slot` from state."
The two PRs are directly contradictory about what the canonical spec requires:
| Commit #203 / leanSpec PR #443 | This PR #212 |
|---|---|
| Use live `state.latest_finalized.slot` for Rule 6 & gap check | Use frozen `original_finalized_slot` for Rule 6 & gap check |
If leanSpec PR #443 is still merged and canonical, then this PR reintroduces the divergence that #203 was rushed in (pre-devnet) to fix, and will cause state root mismatches against other clients that follow that spec update.
Before merging, the PR needs to explicitly address one of:
1. leanSpec PR #443 has been **reverted** or superseded — link to the current leanSpec commit that confirms the original-snapshot semantics.
2. The spec is being updated back to original-snapshot semantics — the PR should reference the leanSpec PR that makes this change.
3. Other client implementations have been audited and agree with this reading of the spec.
Without resolving this, merging risks a consensus split in the opposite direction from the one described in the PR description.
How can I resolve this? If you propose a fix, please make it concise.
---
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 387-391
Comment:
**Gap check uses frozen slot across multiple `try_finalize` calls**
`try_finalize` can be invoked more than once within a single `process_attestations` call (once per attestation that crosses the supermajority threshold). After the first successful call, `state.latest_finalized.slot` is advanced, but subsequent calls still use the same `original_finalized_slot`.
Consider a block with three attestation groups:
- Group 1 justifies slot 5 → `try_finalize` is called, `state.latest_finalized.slot` advances from 0 → 5.
- Group 2 justifies slot 12 → `try_finalize` is called with `original_finalized_slot = 0`. The gap `(5+1)..12 = [6,7,8,9,10,11]` is checked against `original_finalized_slot=0`. `delta=6` is pronic → justifiable → finalization blocked.
- If instead we used the *updated* `state.latest_finalized.slot=5`, delta for slot 6 would be 1 ≤ 5 → justifiable → same result, but for slot 7 delta=2 (pronic: no; square: no; ≤5: no… wait 2 ≤ 5 → yes). Different justifiability windows could yield different finalization decisions.
The PR description carefully explains the two-reference distinction in the Python spec, but it's worth explicitly verifying that the Python `self.latest_finalized` is **never mutated** mid-loop (i.e., the spec writes the final result back to `self.latest_finalized` only after the full loop completes, keeping `self.latest_finalized.slot` constant at L516 and L570). If Python does update `self.latest_finalized` within the loop, then subsequent iterations would see the new slot — the same behavior that `state.latest_finalized.slot` exhibits in the Rust code — and `original_finalized_slot` would be wrong here too.
How can I resolve this? If you propose a fix, please make it concise.
---
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 249-256
Comment:
**No regression test for the triggering scenario**
The PR description itself notes: *"A targeted spec test exercising this path would further strengthen coverage."* The specific scenario — a block with multiple attestation groups where the first group triggers finalization — is the only observable way to distinguish the old behavior from the new. Without a test fixture, the existing 108 tests cannot verify the fix is correct nor catch a future accidental regression.
Consider adding a test fixture to `leanSpec/fixtures/consensus/state_transition/` (or a Rust unit test) that:
1. Sets `latest_finalized.slot = 0`.
2. Includes a block with two attestation groups: group 1 triggers finalization (advancing to slot 5), group 2 has a target at slot 11.
3. Asserts the expected post-state differs from the pre-fix behavior.
How can I resolve this? If you propose a fix, please make it concise.Last reviewed commit: f58af17
![greptile-apps[bot]](https://avatars.githubusercontent.com/in/867647?s=60&v=4){kind=small}
| // Capture the original finalized slot before attestation processing. | ||
| // The spec uses self.latest_finalized.slot (immutable) for justifiability | ||
| // checks (Rule 6) and finalization gap checks, while using a local mutable | ||
| // finalized_slot for is_slot_justified (Rules 1-2) and window shifts. | ||
| let original_finalized_slot = state.latest_finalized.slot; |
There was a problem hiding this comment.
Directly conflicts with the recently-merged commit #203 (9c7f5f6)
This PR re-introduces original_finalized_slot and uses it for Rule 6 and the finalization gap check — but commit 9c7f5f6 (merged yesterday, March 12) explicitly removed this snapshot to align with leanSpec PR #443. That commit's message states:
"The above PR in leanSpec removed the use of the
original_finalized_slotsnapshot and changed it to using the updatedlatest_finalized.slotfrom state."
The two PRs are directly contradictory about what the canonical spec requires:
| Commit #203 / leanSpec PR #443 | This PR #212 |
|---|---|
Use live state.latest_finalized.slot for Rule 6 & gap check |
Use frozen original_finalized_slot for Rule 6 & gap check |
If leanSpec PR #443 is still merged and canonical, then this PR reintroduces the divergence that #203 was rushed in (pre-devnet) to fix, and will cause state root mismatches against other clients that follow that spec update.
Before merging, the PR needs to explicitly address one of:
- leanSpec PR #443 has been reverted or superseded — link to the current leanSpec commit that confirms the original-snapshot semantics.
- The spec is being updated back to original-snapshot semantics — the PR should reference the leanSpec PR that makes this change.
- Other client implementations have been audited and agree with this reading of the spec.
Without resolving this, merging risks a consensus split in the opposite direction from the one described in the PR description.
Prompt To Fix With AI
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 215-219
Comment:
**Directly conflicts with the recently-merged commit #203 (`9c7f5f6`)**
This PR re-introduces `original_finalized_slot` and uses it for Rule 6 and the finalization gap check — but commit `9c7f5f6` (merged yesterday, March 12) *explicitly removed this snapshot* to align with [leanSpec PR #443](https://github.com/leanEthereum/leanSpec/pull/443). That commit's message states:
> "The above PR in leanSpec removed the use of the `original_finalized_slot` snapshot and changed it to using the updated `latest_finalized.slot` from state."
The two PRs are directly contradictory about what the canonical spec requires:
| Commit #203 / leanSpec PR #443 | This PR #212 |
|---|---|
| Use live `state.latest_finalized.slot` for Rule 6 & gap check | Use frozen `original_finalized_slot` for Rule 6 & gap check |
If leanSpec PR #443 is still merged and canonical, then this PR reintroduces the divergence that #203 was rushed in (pre-devnet) to fix, and will cause state root mismatches against other clients that follow that spec update.
Before merging, the PR needs to explicitly address one of:
1. leanSpec PR #443 has been **reverted** or superseded — link to the current leanSpec commit that confirms the original-snapshot semantics.
2. The spec is being updated back to original-snapshot semantics — the PR should reference the leanSpec PR that makes this change.
3. Other client implementations have been audited and agree with this reading of the spec.
Without resolving this, merging risks a consensus split in the opposite direction from the one described in the PR description.
How can I resolve this? If you propose a fix, please make it concise.| if ((source.slot + 1)..target.slot) | ||
| .any(|slot| slot_is_justifiable_after(slot, state.latest_finalized.slot)) | ||
| .any(|slot| slot_is_justifiable_after(slot, original_finalized_slot)) | ||
| { | ||
| metrics::inc_finalizations("error"); | ||
| return; |
There was a problem hiding this comment.
Gap check uses frozen slot across multiple try_finalize calls
try_finalize can be invoked more than once within a single process_attestations call (once per attestation that crosses the supermajority threshold). After the first successful call, state.latest_finalized.slot is advanced, but subsequent calls still use the same original_finalized_slot.
Consider a block with three attestation groups:
- Group 1 justifies slot 5 →
try_finalizeis called,state.latest_finalized.slotadvances from 0 → 5. - Group 2 justifies slot 12 →
try_finalizeis called withoriginal_finalized_slot = 0. The gap(5+1)..12 = [6,7,8,9,10,11]is checked againstoriginal_finalized_slot=0.delta=6is pronic → justifiable → finalization blocked. - If instead we used the updated
state.latest_finalized.slot=5, delta for slot 6 would be 1 ≤ 5 → justifiable → same result, but for slot 7 delta=2 (pronic: no; square: no; ≤5: no… wait 2 ≤ 5 → yes). Different justifiability windows could yield different finalization decisions.
The PR description carefully explains the two-reference distinction in the Python spec, but it's worth explicitly verifying that the Python self.latest_finalized is never mutated mid-loop (i.e., the spec writes the final result back to self.latest_finalized only after the full loop completes, keeping self.latest_finalized.slot constant at L516 and L570). If Python does update self.latest_finalized within the loop, then subsequent iterations would see the new slot — the same behavior that state.latest_finalized.slot exhibits in the Rust code — and original_finalized_slot would be wrong here too.
Prompt To Fix With AI
This is a comment left during a code review.
Path: crates/blockchain/state_transition/src/lib.rs
Line: 387-391
Comment:
**Gap check uses frozen slot across multiple `try_finalize` calls**
`try_finalize` can be invoked more than once within a single `process_attestations` call (once per attestation that crosses the supermajority threshold). After the first successful call, `state.latest_finalized.slot` is advanced, but subsequent calls still use the same `original_finalized_slot`.
Consider a block with three attestation groups:
- Group 1 justifies slot 5 → `try_finalize` is called, `state.latest_finalized.slot` advances from 0 → 5.
- Group 2 justifies slot 12 → `try_finalize` is called with `original_finalized_slot = 0`. The gap `(5+1)..12 = [6,7,8,9,10,11]` is checked against `original_finalized_slot=0`. `delta=6` is pronic → justifiable → finalization blocked.
- If instead we used the *updated* `state.latest_finalized.slot=5`, delta for slot 6 would be 1 ≤ 5 → justifiable → same result, but for slot 7 delta=2 (pronic: no; square: no; ≤5: no… wait 2 ≤ 5 → yes). Different justifiability windows could yield different finalization decisions.
The PR description carefully explains the two-reference distinction in the Python spec, but it's worth explicitly verifying that the Python `self.latest_finalized` is **never mutated** mid-loop (i.e., the spec writes the final result back to `self.latest_finalized` only after the full loop completes, keeping `self.latest_finalized.slot` constant at L516 and L570). If Python does update `self.latest_finalized` within the loop, then subsequent iterations would see the new slot — the same behavior that `state.latest_finalized.slot` exhibits in the Rust code — and `original_finalized_slot` would be wrong here too.
How can I resolve this? If you propose a fix, please make it concise.
MegaRedHand
deleted the
fix/use-original-finalized-slot-in-attestation-processing
branch
2 participants
Motivation
A spec-to-code compliance audit identified a consensus-critical divergence between ethlambda and the leanSpec Python reference implementation in how
process_attestationsreferences the finalized slot.The leanSpec (
state.py) uses two distinct references to the finalized slot during attestation processing:self.latest_finalized.slotprocess_attestations)state.pyL516), Finalization gap check (state.pyL570)finalized_slot(local variable)is_slot_justified— Rules 1-2 (state.pyL459, L466),set_justified(L550), window shift (L584)The Rust code was using
state.latest_finalized.slotfor all of these. Becausestateis&mut State, this value changes when finalization advances mid-processing (at the formerlib.rsL373), making it behave like the spec's local mutablefinalized_sloteverywhere — including the two places where the spec deliberately uses the original immutable value.The divergence
When a block contains multiple attestation groups and the first group triggers finalization (advancing
latest_finalized.slot), subsequent attestations are checked against the new finalized slot instead of the original. This affects:Vote validation Rule 6 (
slot_is_justifiable_after): A target slot's justifiability depends on its delta from the finalized slot. Changing the finalized slot changes the delta, which can flip the justifiability result (e.g., delta=11 is not justifiable, but delta=6 is — it's a pronic number).Finalization gap check: Whether finalization can advance depends on there being no justifiable slots in the gap between source and target. Using the wrong finalized slot reference changes which slots are considered justifiable in that gap.
Concrete example
Consider
finalized_slot=0, and a block with two attestation groups:latest_finalized.slotfrom 0 to 5For Rule 6 on Group 2:
delta = 11 - 0 = 11→ NOT justifiable (not ≤5, not a perfect square, not pronic) → vote rejecteddelta = 11 - 5 = 6→ IS justifiable (6 = 2×3, pronic) → vote acceptedThis produces different post-states (different
justified_slots,latest_justified,latest_finalized), leading to different state roots and a consensus split between implementations.Exploitability
A block builder who includes attestations in a specific order can trigger this divergence. The attacker constructs a block where one attestation group causes finalization, and a subsequent group's validity changes based on which finalized slot reference is used.
Description
The fix captures the original finalized slot before the attestation loop and passes it explicitly to the two functions that need it:
process_attestations: Captureslet original_finalized_slot = state.latest_finalized.slot;before the loopis_valid_vote: Acceptsoriginal_finalized_slotas a parameter, uses it for Rule 6 (slot_is_justifiable_after). Rules 1-2 (is_slot_justified) continue usingstate.latest_finalized.slot(mutable), correctly matching the spec's localfinalized_slottry_finalize: Acceptsoriginal_finalized_slotas a parameter, uses it for the finalization gap checkSpec references
leanSpec/src/lean_spec/subspecs/containers/state/state.pylatest_finalized = self.latest_finalized/finalized_slot = latest_finalized.slot(local mutable copy)justified_slots.is_slot_justified(finalized_slot, ...)(local mutable — Rules 1-2)target.slot.is_justifiable_after(self.latest_finalized.slot)(original immutable — Rule 6)Slot(slot).is_justifiable_after(self.latest_finalized.slot)(original immutable — gap check)finalized_slot = latest_finalized.slot(local mutable updated after finalization)How to Test
cargo test --workspace --release— all 108 tests pass (5 ignored: slow crypto tests)cargo clippy --workspace -- -D warnings— cleancargo fmt --all -- --check— clean