feat(fc): prove FC-1 head selection is deterministic - #43
Merged
Conversation
Open the fork-choice domain: LeanSpec/Forks/Lstar/Store/Store.lean mirrors containers/store.py and the head-selection subset of fork_choice.py at upstream main 57d4339 (post #1179/#1181, so the vote tie-break is insertion-order independent and the store invariants are documented upstream). Model: Python dicts as association lists; XMSS material opaque; unbounded while-walks on blocks.length fuel (WellFormed.parentSlotLt is what bounds them upstream too); asserts as total fallbacks. FC-1 is update_head_deterministic (upstream renamed compute_head to update_head), with the substantive well-definedness proved as computeLmdGhostHead_in_store and updateHead_head_in_store: the selected head is the justified anchor or a stored block. Store.WellFormed states the invariants extracted in leanEthereum/leanSpec#1176 for the FC-2/FC-4 follow-ups. Supporting additions: SingleMessageAggregate and Interval containers, INTERVALS_PER_SLOT, and a LawfulBEq Bytes32 instance for association-list membership reasoning.
This was referenced Jul 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Opens the fork-choice domain (
LeanSpec/Forks/Lstar/Store/), modeling upstream atmain@57d4339— i.e. after the #1179/#1181 fixes, so the model starts from the hardened spec: the vote tie-break is insertion-order independent and the store invariants are documented.What is modeled
Store/Store.leanmirrorscontainers/store.pyand the head-selection subset offork_choice.py:Storecontainer (all fields; Pythondicts as association lists)_checkpoint_is_ancestor→checkpointIsAncestor_extract_attestations_from_aggregated_payloads→extractAttestationsFromAggregatedPayloads— newest-first, equal-slot ties toward the larger canonical root (the #1181 determinism rule), via theHasHashTreeRoottypeclass (SSZ-7)_accumulate_ancestor_weights/compute_block_weights_compute_lmd_ghost_head→computeLmdGhostHead(weight-then-lex-root child selection)update_head→updateHead(upstream successor of the catalog'scompute_head), including the finalized re-derivation climbModeling choices (documented in the module docstring): XMSS material opaque (Arklib side); unbounded
whilewalks onblocks.length + 1fuel —WellFormed.parentSlotLtis exactly what bounds them upstream too; Pythonasserts as total fallbacks.FC-1
Store.update_head_deterministic— the catalog meta-property (rfl; totality by fuel-bounded construction)Store.computeLmdGhostHead_in_storeandStore.updateHead_head_in_store— the selected head is the justified anchor or a block the store knows (the membership FC-2 will build on)Store.WellFormed
States the invariants extracted in leanEthereum/leanSpec#1176 (documented/enforced by #1179): dict-key uniqueness, blocks↔states alignment (M-4), parent-slot ordering (walk termination / FC-4 acyclicity source), justified anchor known, justified-descends-from-finalized (M-1). FC-2/FC-4 will consume these.
Supporting additions
Containers/Aggregation.lean(SingleMessageAggregate, proof bytes opaque),Containers/Interval.lean(Interval,fromSlot),INTERVALS_PER_SLOTinConfig.leanLawfulBEq Bytes32instance for association-list membership reasoningCatalog: FC-1 checked, progress table 17/13/1, FC intro cites
Store.WellFormed.lake buildpasses with nosorry.