RangeInteger abstraction for more compact representation#1061
Draft
RangeInteger abstraction for more compact representation#1061
Conversation
ehildenb
changed the title
…ray representing packed integers
… simplification and test
…rget ProveRawOpts.__init__ did not initialize haskell_target or llvm_lib_target, which _kmir_prove_raw accesses unconditionally. This caused an AttributeError when test_prove[functional-spec] ran. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…r projection rules and decode fix Add the full set of RangeInteger projection rules to data.md so that unsigned-integer arrays stored as packed Bytes can be traversed and mutated just like Range(List) arrays: - projectionElemIndex(local(LOCAL)): read element at runtime index - projectionElemConstantIndex: read element at compile-time index (from front or from end) - projectionElemSubslice (from-front and from-end): produce a sub-range - PointerOffset: advance the start of the range - derefTruncate(staticSize) and derefTruncate(dynamicSize): truncate to N elements (fix for the previous rule that computed LEN-SIZE instead of SIZE) - Write-back contexts (CtxRangeIntegerIndex, CtxRangeIntSubslice, CtxRangeIntPointerOffset) and a #buildUpdate rule for element mutation - isRange(RangeInteger) = true, so the noMetadataSize pass-through works - #normalizeValue: converts Range([Integer(v,W,false)...]) → RangeInteger for uniform comparison (used by raw_eq in intrinsics.md) - #projectionsFor rules for all new contexts Fix #decodeArrayAllocation in decoding.md: split the single rule into three to avoid calling the partial function #intTypeOf on non-integer types, which caused the K Haskell symbolic backend to branch on #Ceil(#intTypeOf(ELEMTYPEINFO)) and emit spurious side-conditions. Also add #decodeSliceAllocation for unsigned-integer element types so that slices over packed byte arrays decode to RangeInteger. Add [preserves-definedness] to operandConstant and #decodeConstant rules to suppress spurious #Ceil conditions in symbolic mode. Add kmir-lemmas simplifications: #Ceil(substrBytes) = #Top when indices are in-range, and substrBytes(B, 0, lengthBytes(B)) = B. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…E: add raw K spec prove test Rename test_prove → test_prove_rs to distinguish from a new test_prove that runs raw K spec files from integration/data/proving/. Add functional-spec.k as the first such spec, exercising the bytes simplification lemma added to kmir-lemmas.md. Fix ImpliesProver to use assume_defined=True so functional equality proofs don't get stuck on definedness side-conditions. Update kast.py _ArgGenerator to wrap staticSize in Metadata(staticSize(N), 0, staticSize(N)) to match the current K semantics Metadata constructor. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
- decode-value: array-u8 tests now show RangeInteger instead of Range - exec-smir/allocs/array_nest_compare: updated for RangeInteger repr - exec-smir/newtype-pubkey: now terminates with #EndProgram (was stuck at projectionElemIndex on RangeInteger(0, ...) due to the buggy staticSize rule that set LEN = LEN - SIZE instead of SIZE) - run-smir-random/complex-types: init states show RangeInteger; final states reflect updated Metadata wrapping for staticSize in kast.py Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Remove commented-out EqualityProof import, isinstance assertion, and _LOGGER warnings left over from development; remove unused logging import and Final. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
ehildenb
force-pushed
the
range-abstraction
branch
from
4054518 to
5deb9c9
Compare
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 seeks to reduce the size of KMIR configurations by packing ranges of integers into a single byte-array instead. Currently, if we ahve a list of
Integer(...)of the same unsigned width each, we store it as aList(...)of all the integer instead of packing it into a single Byte array. This leads to way more AST nodes for each term than is needed, and exploded output for the same bytearray.So this change:
RangeofInteger, and instead builds aRangeIntegerconstruct with the bytes packed. It only does this when the integers are byte-aligned, so that the byte-level access we get on bytes are sufficient.RangeIntegerconstruct.kprove ...style tests that we can execute for testing lemmas.