runtimeverification / runtimeverification/mir-semantics
Unify #traverseProjection value representation to eliminate singleton Range round-trips
Nobody has claimed this yet.
- Dominant language
- Python
- Stars
- 52
- Forks
- 5
- PR merge metrics
- No merged PRs in 30d
Description
Problem / Goal
#traverseProjection currently mixes two different intermediate representations:
- bare values such as
Aggregate(...)andUnion(...) Range(...)values, including synthetic singleton ranges likeRange(ListItem(VAL))
That means the projection engine has no stable representation invariant. Some rules expect a bare value, while others expect a Range. Along PointerOffset + Field + Union paths, the engine can surface bridge shapes such as Range(ListItem(Union(...))), which then require extra rules just to unwrap the value and continue.
PR #999 added two bridge rules to fix the iterator-simple regression on the newly exercised drop-glue path:
- lift a non-
RangevalueVALtoRange(ListItem(VAL))soPointerOffsetcan reuse range-based logic - unwrap
Range(ListItem(Union(...)))back toUnion(...)so the existingFieldrules can match
Those rules are acceptable as a narrow regression fix, but they also show the deeper design problem: the internal representation used by #traverseProjection is not closed under common projection combinations.
This issue tracks a dedicated refactor PR that adopts the first-class solution: define and enforce a single representation invariant for #traverseProjection, and reshape the traversal so these round-trip bridge rules are no longer needed.
Proposed Approach
- Define a single documented representation invariant for
#traverseProjection - Prefer the "first approach": projection steps should operate on one consistent representation instead of switching between bare values and singleton
Rangewrappers - Refactor
#traverseProjectiontoward a function-style structure so normalization and traversal decisions are centralized rather than spread across ad hoc bridge rules - Rework
PointerOffsetso it does not enter the main traversal loop by manufacturingRange(ListItem(...)) - Audit closure of
Field/Union/Index/Subslice/PointerOffsetcombinations under the new invariant - Delete the two bridge rules added in PR #999 once the new structure subsumes them
Target direction:
Rangeshould represent real sequence/slice semantics, not temporary singleton wrappers for unrelated projection stepsFieldandUnionprojections should operate directly on the canonical representation rather than depending on follow-up unwrapping#traverseProjectionshould become more function-like and locally normalized, so representation changes do not leak into unrelated rules
Acceptance Criteria
-
#traverseProjectionhas a clear, documented representation invariant - the traversal is refactored toward a function-style structure with centralized normalization decisions
-
PointerOffsetno longer depends on the round-trip pathVAL -> Range(ListItem(VAL)) -> bare value -
Field/Union/PointerOffset/Index/Subslicecombinations are closed under the chosen invariant - the two bridge rules added in PR #999 are deleted
-
iterator-simplestill passes -
run-smir-randomcomplex-typesremains stable - relevant pointer/slice/wrapper regression tests do not introduce new stuck states or snapshot drift
Suggested Validation
uv run pytest src/tests/integration/test_integration.py -v --timeout=600 -k 'iterator-simple or iter-eq-copied-take-dereftruncate or maybe-uninit'uv run pytest src/tests/integration/test_run_smir_random.py -v -k 'complex-types'uv run pytest src/tests/integration --maxfail=1 --verbose --durations=0 --numprocesses=6 --dist=worksteal -k "not llvm and not test_run_smir_random and not test_exec_smir and not test_prove_termination and not test_prove"
Assumptions
- [guess] this should land in a dedicated PR because it is a traversal-engine refactor, not just a targeted regression fix
- [guess] enforcing a single invariant will remove the need for future bridge rules of the same shape
- [guess] the first stage does not need to redesign the entire pointer model, only the internal representation discipline inside
#traverseProjection
Contributor guide
No contributing guide indexed for this repository
First steps
- Read the whole issue, then the project's contributing guide.
- Comment on the issue to say you are picking it up — it saves two people doing the same work.
- Fork the repository and make your change on a branch.
- Open a pull request that references the issue number.
Research direction
Start at #traverseProjection and inspect the PointerOffset, Field, Union, Index, and Subslice paths, along with the bridge rules added in PR #999. Run the listed iterator-simple, complex-types, and integration regression tests before changing the traversal. Done means one documented representation invariant, no singleton Range round-trip, deleted bridge rules, and stable validation results.
Written by the indexing model from the issue text.
Assessment
- Tech stack
- python
- Domain
- compilers
- Issue type
- Refactor
- Difficulty
- 5/5
- Estimated time
- Over a week
- Activity status
- Quiet
- Clarity
- Mostly clear
- Newbie friendliness
- 35/100