refactor: move runtime local access to slot-backed frames

[Stevengre]

Context

This PR refactors KMIR runtime locals from per-frame value lists into slot-backed storage. The <locals> cell still represents the current frame's MIR local index order, but it now stores runtime slot ids. The actual TypedLocal data lives in the global <slotStore>, and <nextSlot> allocates fresh slots for new frames.

The motivation is not just renaming storage:

• reduce the complexity caused by stack-depth / OFFSET-style reference and pointer bookkeeping by giving runtime locals stable slot identities
• model MIR stack locals more accurately as addressable runtime storage, separate from MIR's relative local(i) indexes
• leave a cleaner target for future address support
• make generated function-summary rules easier to express against stable slot-store entries instead of frame-local value-list positions

Summary

• Adds slot-backed runtime local storage with <slotStore>, <nextSlot>, SlotPlace, and #frameSlotId.
• Reworks local reads, moves, writes, references, pointers, projections, returns, and frame unwind/restore paths to resolve MIR local(i) through the current frame's slot list before reading or updating <slotStore>.
• Refactors function-call setup so non-intrinsic calls materialize operands while the caller frame is still current, normalize the resulting values for rust-call / closure calls, then reserve and initialize the callee's slots from that value list.
• Keeps intrinsic dispatch separate from body-backed call setup and updates intrinsic local/type handling, including raw_eq, to work with slot-backed locals.
• Updates Python-side config/value construction so concrete, symbolic, and random test inputs initialize <locals> as slot ids plus <slotStore> entries.
• Adds slotstore-symbolic-branch proof coverage and updates affected exec/prove/show snapshots for the new runtime configuration shape.

[Stevengre]

Some ideas for better performance:

1. transform the locals into slots when call a function to reduce the term size
2. investigate why it makes proof slower and optimize the haskell backend. Maybe map access functions should be optimized in the haskell backend.
3. We may remove the newlocal value, because if the map item is not exist, it should be newlocal.

[ehildenb]

Are these lists always just counting up from 0? THen do we need the list at all?

[ehildenb]

I see here that we have an example where there are multiple call frames, and so it now starts at 22 and goes to 38. But it still just counts by 1. So I tihnk we really only need to store, for each frame, the start index (here 22), and the width (here 16), just two integers instead of a list of integers. Then we can use basic arithmetic to figure out the slot index. Would that work?

[ehildenb]

I think in general, doing map accesses for both CSE and symbolic execution may not perform as well as doing list access. So I'm not sure this will actually do better for our proof performance than how the semantics is currently arranged. What about this change makes you think CSE will work better?

[Stevengre]

@ehildenb After discussing with Daniel and Maria, we found an easy way to specify the references and pointers in arguments. This is to implement existing traverse-projection as a function so that we can write something like

ARG: Referece(OFFSET, LOCAL_ID, ...)
requires traverseprojection(ARG, LOCAL_CELL, FRAME_CELL) == Value

Another solution for this using List maybe

<local> Start Index in the slotStore </local>
<slot> List of locals from caller to callee <slot>

For the specification:

ARG: Referece(SlotIDX, ...)
requires STORE[ID] == Reference (slotid) & traverseProjection(SLOT_CELL, ID) = Value

okay, we always need this traverseProjection function...

BTW, this structure may also cause performance issue, because I remember that the haskell backend access the List through a front -> end way.

---

I think we still need to provide better support for map, especially the map with concrete key or int/string/id key (this should cover most of cases). Otherwise, it's hard to reason programs like C and Java directly. Additionally, it may introduce more complexity to the semantics and make the semantics harder to understand. And I think the change should be relatively small.

For this reason, even though map may not be the best way to model, I'd like to keep this PR as a performance test for the haskell backend.