runtimeverification / runtimeverification/mir-semantics

Unify #traverseProjection value representation to eliminate singleton Range round-trips

Open
#1,011 1 comment 0 reactions 0 assignees View on GitHub

Nobody has claimed this yet.

area:semantics kind:refactor priority:p1 status:triage type:task
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(...) and Union(...)
  • Range(...) values, including synthetic singleton ranges like Range(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:

  1. lift a non-Range value VAL to Range(ListItem(VAL)) so PointerOffset can reuse range-based logic
  2. unwrap Range(ListItem(Union(...))) back to Union(...) so the existing Field rules 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

  1. Define a single documented representation invariant for #traverseProjection
  2. Prefer the "first approach": projection steps should operate on one consistent representation instead of switching between bare values and singleton Range wrappers
  3. Refactor #traverseProjection toward a function-style structure so normalization and traversal decisions are centralized rather than spread across ad hoc bridge rules
  4. Rework PointerOffset so it does not enter the main traversal loop by manufacturing Range(ListItem(...))
  5. Audit closure of Field / Union / Index / Subslice / PointerOffset combinations under the new invariant
  6. Delete the two bridge rules added in PR #999 once the new structure subsumes them

Target direction:

  • Range should represent real sequence/slice semantics, not temporary singleton wrappers for unrelated projection steps
  • Field and Union projections should operate directly on the canonical representation rather than depending on follow-up unwrapping
  • #traverseProjection should become more function-like and locally normalized, so representation changes do not leak into unrelated rules

Acceptance Criteria

  • #traverseProjection has a clear, documented representation invariant
  • the traversal is refactored toward a function-style structure with centralized normalization decisions
  • PointerOffset no longer depends on the round-trip path VAL -> Range(ListItem(VAL)) -> bare value
  • Field / Union / PointerOffset / Index / Subslice combinations are closed under the chosen invariant
  • the two bridge rules added in PR #999 are deleted
  • iterator-simple still passes
  • run-smir-random complex-types remains 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

  1. Read the whole issue, then the project's contributing guide.
  2. Comment on the issue to say you are picking it up — it saves two people doing the same work.
  3. Fork the repository and make your change on a branch.
  4. 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

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.