feat(fc): model on_block and prove FC-7 invariant preservation - #62
Merged
Conversation
FC-6 proved update_head preserves Store.WellFormed under two side conditions maintained elsewhere. This models the elsewhere: on_block, the mutator that establishes them, closing the composition on_block -> update_head over the full invariant. - Store.onBlock mirrors the upstream gate sequence: known-block skip, parent-state gate (UNKNOWN_PARENT_BLOCK), the #1182 gap/horizon guards, duplicate-attestation rejection (DUPLICATE_ATTESTATION_DATA, new STError variant), the state transition, the import writes (block + post-state insertion, advance_to on latest_justified, vote seeding), update_head, and conditional pruning. Divergences documented in the module docstring: blockRoot as a parameter (hash_tree_root is Arklib-side), signature verification omitted (rejects only more blocks), pruning as a field-preserving parameter. - Store.Aligned packages the FC-6 side conditions plus the two state-alignment clauses their preservation runs on (states sit at their block's slot; states satisfy ST-4). - Store.applyBlock_invariants: the import writes preserve WellFormed and Aligned. Key steps: fresh-root nodup/alignment, parent-slot ordering from transition_slot_lt through the state-slot alignment, advance_to case analysis, and walk stability under a grown block map (ancestorWalk_extend + ancestorWalk_fuel_mono + checkpointIsAncestor_applyBlock). - Store.onBlock_wellFormed composes that with FC-6's updateHead_wellFormed and the congruence transfers (wellFormed_congr / aligned_congr). - State.transition_state_slot: a successful transition lands the state exactly on the block's slot (new STF lemma). - Residual hypotheses (the historical-chain alignment layer, documented in the catalog): the incoming root is not a stored parent link, and an STF-advanced justified checkpoint names an imported block at its own slot and descends from finalized. Catalog: FC-7 entry added; progress table now 33 proved / 1 axiom.
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
FC-6 (#61) proved
update_headpreservesStore.WellFormedunder two side conditions maintained elsewhere. This PR models the elsewhere:on_block, the mutator that establishes them — closing the compositionon_block → update_headover the full invariant (Store.onBlock_wellFormed).Model (
Store.onBlock)Mirrors the upstream gate sequence post-#1182: known-block skip → parent-state gate (
UNKNOWN_PARENT_BLOCK) → gap/horizon guards (BLOCK_SLOT_GAP_TOO_LARGE/BLOCK_TOO_FAR_IN_FUTURE) → duplicate-attestation rejection (DUPLICATE_ATTESTATION_DATA, newSTErrorvariant) → STF → import writes (block + post-state insertion,advance_toonlatest_justified, vote seeding) →update_head→ conditional pruning. Documented divergences:blockRootas a parameter (hash_tree_rootis Arklib-side), signature verification omitted (it only rejects more blocks), pruning as a field-preserving parameter.Proof structure
Store.Alignedpackages the FC-6 side conditions plus the two state-alignment clauses their preservation runs on (stored states sit at their block's slot — via the new STF lemmaState.transition_state_slot— and satisfy ST-4).Store.applyBlock_invariants: the import writes preserveWellFormed ∧ Aligned. Highlights: parent-slot ordering of the new link fromtransition_slot_ltthrough the state-slot alignment;advance_tocase analysis (kept checkpoint transfers across the grown block map viaancestorWalk_extend+ancestorWalk_fuel_mono; advanced checkpoint covered by the alignment hypothesis).Store.onBlock_wellFormedcomposes with FC-6'supdateHead_wellFormedand the congruence transferswellFormed_congr/aligned_congr.Residual hypotheses (the next milestone)
Documented in the theorem docstring and catalog: (1) no stored block already names the incoming root as its parent (STOR-1 + hash acyclicity upstream); (2) an STF-advanced justified checkpoint names an imported block at its own slot and descends from finalized — the historical-chain alignment layer (
historical_block_hashesmirroring the block map), which is the natural FC-8 candidate.Catalog
FC-7 entry added; progress table now 33 proved / 1 axiom / 34 total.
Verification
lake buildsucceeds (37 jobs);#print axiomsforonBlock_wellFormed/applyBlock_invariants→ standard axioms only; nosorry.