Rewrite ingress, support bignum literals, fix FVar type inference#348
Open
arthurpaulino wants to merge 2 commits intomainfrom
Open
Rewrite ingress, support bignum literals, fix FVar type inference#348arthurpaulino wants to merge 2 commits intomainfrom
arthurpaulino wants to merge 2 commits intomainfrom
Conversation
Ingress: replace linear scan with position-map-based address resolution. Compute block layout in a separate pass, then build a parallel KGList mapping each loaded address to its kernel constant index. This removes the O(n²) find_*_position helpers and the U64-based ref_idxs/recur_idxs in favor of G-valued KGList lookups. Primitive type indices (Nat, String) are resolved by hardcoded blake3 address during ingress. Literals: Nat literals now use KLimbs (little-endian bignum list of U64 limbs) instead of a single U64, supporting arbitrarily large Nat values. String literals use raw ByteStream instead of U64. Blob ingress returns raw bytes; conversion decodes them into the appropriate literal type. Kernel: FVar now carries its domain type, fixing k_infer_val_type to return the actual type instead of the Sort 1 sentinel. Recursor iota uses rec_rule_try_find (returns KRecRuleMaybe) so missing rules produce an unreduced Const instead of a panic. Unit-like type equality and struct eta use kg_list_length for constructor counting. Also adds `lake exe kernel` executable for standalone typechecking.
Reuse kernelCheck from Kernel.lean instead of duplicating the IOBuffer setup logic. Replace individual kernelCheckNatAddComm and kernelCheckNatSubLeOfLeAdd with a single kernelChecks that maps over a list of constant names, adding String.Internal.append. Use string-based name construction to prevent instantiation errors with numerical limbs. Mark serde and kernel test cases as executionOnly.
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.
Ingress: replace linear scan with position-map-based address resolution. Compute block layout in a separate pass, then build a parallel KGList mapping each loaded address to its kernel constant index. This removes the O(n²) find_*_position helpers and the U64-based ref_idxs/recur_idxs in favor of G-valued KGList lookups. Primitive type indices (Nat, String) are resolved by hardcoded blake3 address during ingress.
Literals: Nat literals now use KLimbs (little-endian bignum list of U64 limbs) instead of a single U64, supporting arbitrarily large Nat values. String literals use raw ByteStream instead of U64. Blob ingress returns raw bytes; conversion decodes them into the appropriate literal type.
Kernel: FVar now carries its domain type, fixing k_infer_val_type to return the actual type instead of the Sort 1 sentinel. Recursor iota uses rec_rule_try_find (returns KRecRuleMaybe) so missing rules produce an unreduced Const instead of a panic. Unit-like type equality and struct eta use kg_list_length for constructor counting.
Also adds
lake exe kernelexecutable for standalone typechecking.