feat(fc): prove FC-2 the head descends from latest justified - #45
Merged
Conversation
AncestorOrEqual states the catalog's isAncestorOrEqual relationally: a = d or ProperAncestor st a d. The GHOST descent never leaves the subtree of its start (ghostWalk_ancestorOrEqual): each step lands on a childrenOf element, which under nodup keys is a stored block whose parent link is the current head (childrenOf_parent, getBlock?_eq_some_of_mem), and ProperAncestor.trans composes the steps. computeLmdGhostHead_descends lifts this through the anchor match, and head_descends_from_justified instantiates it at update_head's justified anchor under Store.WellFormed. ghostWalk loses its private marker so the descent lemmas can state per-step facts about it.
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
Third FC proposition, completing the head-selection safety trio (FC-1 determinism → FC-4 acyclicity → FC-2 descent), on the
Storemodel of #43 and theProperAncestorrelation of #44.Theorems (
Store/Ancestry.lean)AncestorOrEqual st a d := a = d ∨ ProperAncestor st a d— the catalog'sisAncestorOrEqual, stated relationallyProperAncestor.trans— proper ancestry composesmem_unique_of_keys_nodup/getBlock?_eq_some_of_mem— under Python-dict key uniqueness (WellFormed.blocksKeysNodup) the lookup returns exactly the stored entrychildrenOf_parent— an eligible child is stored with its parent link at the walk's current headghostWalk_ancestorOrEqual— the GHOST descent never leaves the subtree of its startcomputeLmdGhostHead_descends— for any vote set and threshold, the selected head sits in the anchor's subtreehead_descends_from_justified(FC-2) — underStore.WellFormed,update_headselects the justified root or a strict descendantghostWalkloses itsprivatemarker so the descent lemmas can state per-step facts about it (noted in its docstring).Catalog: FC-2 checked, progress table 19/11/1 — FC now 3 proved / 2 open (remaining: FC-3
validate_attestation, FC-5 production-loop termination).lake buildpasses with nosorry.