feat(stor): track upstream #1182 block-horizon guards in insertBlock - #57
Merged
Conversation
Mirror the pending leanEthereum/leanSpec#1182 (head 5e1b7b51, fixing issue #1171): on_block bounds a block's slot right after the parent lookup, before the state transition's empty-slot loop can run - at most HISTORICAL_ROOTS_LIMIT beyond the parent state (BLOCK_SLOT_GAP_TOO_LARGE) and at most one slot past the store clock (BLOCK_TOO_FAR_IN_FUTURE). STError gains both reasons and Config gains HISTORICAL_ROOTS_LIMIT. insertBlock now reads the parent *state*, exactly as on_block does; parentsPresent_insertBlock therefore takes the #1176 M-4 blocks-states alignment as a hypothesis to carry presence over to the block map. insertBlock_slot_gap_bounded and insertBlock_within_horizon extract the two bounds from a successful insertion - the formal content of issue #1171's fix. Hold this PR until upstream #1182 merges; re-verify the mirrored guards against the merged diff then.
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.
This PR mirrors the pending leanEthereum/leanSpec#1182 (head
5e1b7b51, fixing issue #1171 — adust09's future-slot-horizon finding). CI is green and the model is ready; merge after #1182 lands upstream, re-verifying the mirrored guards against the merged diff (they are unchanged since filing, but the upstream PR could still be revised).What it mirrors
on_blockbounds a block's slot right after the parent lookup, before the state transition's empty-slot loop can run:BLOCK_SLOT_GAP_TOO_LARGE— the slot may run at mostHISTORICAL_ROOTS_LIMIT(2^18) beyond the parent stateBLOCK_TOO_FAR_IN_FUTURE— at most one slot past the store clock (store.time // INTERVALS_PER_SLOT + 1)Changes
STErrorgains both reasons (docstring notes they come from the pending #1182);Config.leangainsHISTORICAL_ROOTS_LIMITinsertBlocknow reads the parent state, exactly ason_blockdoes — soparentsPresent_insertBlocktakes the #1176 M-4 blocks-states alignment (WellFormed.blocksStatesAligned's shape) as a hypothesis to carry presence over to the block mapinsertBlock_slot_gap_bounded(an accepted block names a stored parent state and sits within the gap bound — the empty-slot loop is bounded) andinsertBlock_within_horizon(an accepted block sits within the clock horizon)lake buildpasses with nosorry.