Skip to content

Commit 03e946a

Browse files
tcoratgerclaude
andauthored
refactor(lstar): trim state-transition docs and use itertools.batched (leanEthereum#1116)
* refactor(lstar): trim state-transition docs and use itertools.batched Cut the comment volume in the lstar state transition and replace the flat-vote-list index arithmetic with a stdlib idiom. No behavior change: the 3SF-mini justification and finalization logic is untouched, and the state-transition vectors are byte-identical (verified with fill, including the determinism check across hash seeds). - Unpack the flat justification vote list with itertools.batched zipped against the tracked roots, replacing the i*N:(i+1)*N slicing. The zip is strict so the length invariant is enforced, and each batch is listed because the per-root tallies are mutated downstream. - Hoist the validator count, which was recomputed four times. - Trim over-explained comment blocks to the load-bearing reasoning and one sentence per line: the vote-map round trip, the justifiable-slot filter (now deferring to the documented rule rather than re-deriving it), the finalization no-gap rule, and the finalized-relative flag encoding. - Glue front-loaded comments to the line they justify, rather than stacking them at the top of a block. - Correct the genesis-anchor comment: genesis is justified and finalized by definition as the anchor, not because it "cannot receive votes" (genesis self-votes exist; they are dropped by the already-justified filter). Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * refactor(anchor): inline the single-use head slot lookup Drop the head_slot local and read store.blocks[store.head].slot directly in the checkpoint, matching the inline-single-use convention. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> * refactor(lstar): inline the single-use genesis-parent check Fold the parent-slot-zero test directly into the if, dropping the single-use intermediate boolean. Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
1 parent 456e046 commit 03e946a

2 files changed

Lines changed: 68 additions & 235 deletions

File tree

src/lean_spec/node/anchor.py

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -128,13 +128,12 @@ async def from_checkpoint(
128128

129129
# The protocol return type is structural, but only one concrete store ships.
130130
store = cast(Store, fork.create_store(state, anchor_block, validator_index))
131-
head_slot = store.blocks[store.head].slot
132131

133132
return cls(
134133
validators=state.validators,
135134
store=store,
136135
initial_status=Status(
137136
finalized=store.latest_finalized,
138-
head=Checkpoint(root=store.head, slot=head_slot),
137+
head=Checkpoint(root=store.head, slot=store.blocks[store.head].slot),
139138
),
140139
)

0 commit comments

Comments
 (0)