From ec8bc2812592cb18c1e7a378e5abb56ae11ed79a Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Fri, 11 Apr 2025 17:57:30 +0700
Subject: [PATCH 1/9] GlobalAllocs are added to memory map

---
 kmir/src/kmir/kdist/mir-semantics/kmir.md            | 12 +++++++++++-
 .../src/kmir/kdist/mir-semantics/rt/configuration.md |  5 ++---
 2 files changed, 13 insertions(+), 4 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index 63beaa787..cc6642088 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -45,11 +45,12 @@ function map and the initial memory have to be set up.
 
 ```k
   // #init step, assuming a singleton in the K cell
-  rule <k> #init(_NAME:Symbol _ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings)
+  rule <k> #init(_NAME:Symbol ALLOCS:GlobalAllocs FUNCTIONS:FunctionNames ITEMS:MonoItems TYPES:TypeMappings)
          =>
            #execFunction(#findItem(ITEMS, FUNCNAME), FUNCTIONS)
        </k>
        <functions> _ => #mkFunctionMap(FUNCTIONS, ITEMS) </functions>
+       <memory> _ => #mkMemoryMap(ALLOCS) </memory>
        <start-symbol> FUNCNAME </start-symbol>
        <types> _ => #mkTypeMap(.Map, TYPES) </types>
        <adt-to-ty> _ => #mkAdtMap(.Map, TYPES) </adt-to-ty>
@@ -108,7 +109,16 @@ they are callee in a `Call` terminator within an `Item`).
 The function _names_ and _ids_ are not relevant for calls and therefore dropped.
 
 ```k
+  syntax Address ::= "Address" "(" Int ")"
+
+  rule #mkMemoryMap(Globals) => #accumMemory(.Map, Address(1), Globals)
+
+  rule #accumMemory(Acc, _, .GlobalAllocs) => Acc
+  rule #accumMemory(Acc, Address(INDEX), Global REST) => #accumMemory(Acc (Address(INDEX) |-> Global), Address(INDEX +Int 1), REST)
+
   syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ]
+               | #mkMemoryMap ( GlobalAllocs )               [ function, total ]
+               | #accumMemory ( Map, Address, GlobalAllocs ) [ function, total ]
                | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
                | #accumItems ( Map, MonoItems )              [ function, total ]
 
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
index 80d39e906..5e9b05ad4 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
@@ -48,9 +48,8 @@ module KMIR-CONFIGURATION
                   <stack> .List </stack>
                   // function store, Ty -> MonoItemFn
                   <functions> .Map </functions>
-                  // heap
-                  <memory> .Map </memory> // FIXME unclear how to model
-                  // FIXME where do we put the "GlobalAllocs"? in the heap, presumably?
+                  // heap, Address(Int) -> ( GlobalAlloc | Data? ) 
+                  <memory> .Map </memory>
                   <start-symbol> symbol($STARTSYM:String) </start-symbol>
                   // static information about the base type interning in the MIR
                   <types> .Map </types>

From e604728f3d4fa5848bda18d42d0fff742151b01b Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Thu, 24 Apr 2025 05:22:59 +0000
Subject: [PATCH 2/9] Set Version: 0.3.122

---
 kmir/pyproject.toml       | 2 +-
 kmir/src/kmir/__init__.py | 2 +-
 package/version           | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index bf71df0eb..d43c4bc8e 100644
--- a/kmir/pyproject.toml
+++ b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.3.121"
+version = "0.3.122"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index 171936af8..1345b2f7a 100644
--- a/kmir/src/kmir/__init__.py
+++ b/kmir/src/kmir/__init__.py
@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.121'
+VERSION: Final = '0.3.122'
diff --git a/package/version b/package/version
index b96616520..165ea630e 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.121
+0.3.122

From c13170b571632d05d3e4c3674bfda22e5c766a24 Mon Sep 17 00:00:00 2001
From: devops <devops@runtimeverification.com>
Date: Thu, 15 May 2025 20:27:37 +0000
Subject: [PATCH 3/9] Set Version: 0.3.163

---
 kmir/pyproject.toml       | 2 +-
 kmir/src/kmir/__init__.py | 2 +-
 kmir/uv.lock              | 2 +-
 package/version           | 2 +-
 4 files changed, 4 insertions(+), 4 deletions(-)

diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
index d338eeff7..6601457ea 100644
--- a/kmir/pyproject.toml
+++ b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.162"
+version = "0.3.163"
 description = ""
 requires-python = "~=3.10"
 dependencies = [
diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
index 679240233..6fff8bfbd 100644
--- a/kmir/src/kmir/__init__.py
+++ b/kmir/src/kmir/__init__.py
@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.162'
+VERSION: Final = '0.3.163'
diff --git a/kmir/uv.lock b/kmir/uv.lock
index 16c6ad2dc..df2fb5022 100644
--- a/kmir/uv.lock
+++ b/kmir/uv.lock
@@ -491,7 +491,7 @@ wheels = [
 
 [[package]]
 name = "kmir"
-version = "0.3.162"
+version = "0.3.163"
 source = { editable = "." }
 dependencies = [
     { name = "kframework" },
diff --git a/package/version b/package/version
index e41771856..ee7ed8106 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-0.3.162
+0.3.163

From e2cca64340b706a202e67450c49a0e051cdd17f5 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Thu, 15 May 2025 18:32:40 -0400
Subject: [PATCH 4/9] Fixed duplicate memory typox

---
 kmir/src/kmir/kdist/mir-semantics/rt/configuration.md | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
index 5a5a99ac1..5c1af3a0a 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
@@ -46,12 +46,11 @@ module KMIR-CONFIGURATION
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>
+                  // heap, Address(Int) -> ( GlobalAlloc | Data? ) 
                   <memory> .Map </memory>
                   // ============ static information ============
                   // function store, Ty -> MonoItemFn
                   <functions> .Map </functions>
-                  // heap, Address(Int) -> ( GlobalAlloc | Data? ) 
-                  <memory> .Map </memory>
                   <start-symbol> symbol($STARTSYM:String) </start-symbol>
                   // static information about the base type interning in the MIR
                   <types> .Map </types>

From a80d051f6f158f93aa919ba309b52e7db09ac5a9 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Thu, 15 May 2025 21:30:15 -0400
Subject: [PATCH 5/9] Map is now from AllocId -> GlobalAllocKind

---
 kmir/src/kmir/kdist/mir-semantics/kmir.md             | 10 ++++------
 kmir/src/kmir/kdist/mir-semantics/rt/configuration.md |  2 +-
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index 549ed1a0d..df359c7cb 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -109,16 +109,14 @@ they are callee in a `Call` terminator within an `Item`).
 The function _names_ and _ids_ are not relevant for calls and therefore dropped.
 
 ```k
-  syntax Address ::= "Address" "(" Int ")"
+  rule #mkMemoryMap(Globals) => #accumMemory(.Map, Globals)
 
-  rule #mkMemoryMap(Globals) => #accumMemory(.Map, Address(1), Globals)
-
-  rule #accumMemory(Acc, _, .GlobalAllocs) => Acc
-  rule #accumMemory(Acc, Address(INDEX), Global REST) => #accumMemory(Acc (Address(INDEX) |-> Global), Address(INDEX +Int 1), REST)
+  rule #accumMemory(Acc, .GlobalAllocs) => Acc
+  rule #accumMemory(Acc, globalAllocEntry(ID, ALLOC) REST) => #accumMemory(Acc (ID |-> ALLOC), REST)
 
   syntax Map ::= #mkFunctionMap ( FunctionNames, MonoItems ) [ function, total ]
                | #mkMemoryMap ( GlobalAllocs )               [ function, total ]
-               | #accumMemory ( Map, Address, GlobalAllocs ) [ function, total ]
+               | #accumMemory ( Map, GlobalAllocs )          [ function, total ]
                | #accumFunctions ( Map, Map, FunctionNames ) [ function, total ]
                | #accumItems ( Map, MonoItems )              [ function, total ]
 
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
index 5c1af3a0a..1c863f684 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/configuration.md
@@ -46,7 +46,7 @@ module KMIR-CONFIGURATION
                   </currentFrame>
                   // remaining call stack (without top frame)
                   <stack> .List </stack>
-                  // heap, Address(Int) -> ( GlobalAlloc | Data? ) 
+                  // heap, Address(Int) -> ( GlobalAlloc | Data? )
                   <memory> .Map </memory>
                   // ============ static information ============
                   // function store, Ty -> MonoItemFn

From 4348cb1ca82cb882f200acba57fed2293412f594 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Fri, 16 May 2025 14:46:12 -0400
Subject: [PATCH 6/9] Reference now RefStack and RefAlloc

---
 kmir/src/kmir/kdist/mir-semantics/rt/data.md  | 14 +++++++-------
 kmir/src/kmir/kdist/mir-semantics/rt/value.md |  5 ++++-
 2 files changed, 11 insertions(+), 8 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 55291746e..6d38587de 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -232,7 +232,7 @@ In the simplest case, the reference refers to a local in the same stack frame (h
 
 ```k
   rule <k> #readProjection(
-              typedValue(Reference(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _),
+              typedValue(RefStack(0, place(local(I:Int), PLACEPROJS:ProjectionElems), _), _, _),
               projectionElemDeref PROJS:ProjectionElems
             )
          =>
@@ -259,7 +259,7 @@ An important prerequisite of this rule is that when passing references to a call
 
 ```k
   rule <k> #readProjection(
-              typedValue(Reference(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _),
+              typedValue(RefStack(FRAME, place(LOCAL:Local, PLACEPROJS), _), _, _),
               projectionElemDeref PROJS
             )
          =>
@@ -290,8 +290,8 @@ An important prerequisite of this rule is that when passing references to a call
                       | #decrementRef ( TypedLocal )  [function, total]
                       | #adjustRef (TypedLocal, Int ) [function, total]
 
-  rule #adjustRef(typedValue(Reference(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
-    => typedValue(Reference(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
+  rule #adjustRef(typedValue(RefStack(HEIGHT, PLACE, REFMUT), TY, MUT), OFFSET)
+    => typedValue(RefStack(HEIGHT +Int OFFSET, PLACE, REFMUT), TY, MUT)
   rule #adjustRef(TL, _) => TL [owise]
 
   rule #incrementRef(TL) => #adjustRef(TL, 1)
@@ -523,7 +523,7 @@ The solution is to use rewrite operations in a downward pass through the project
 
   rule <k> #projectedUpdate(
             _DEST,
-            typedValue(Reference(OFFSET, place(LOCAL, PLACEPROJ), _MUT), _, _),
+            typedValue(RefStack(OFFSET, place(LOCAL, PLACEPROJ), _MUT), _, _),
             projectionElemDeref PROJS,
             UPDATE,
             _CTXTS,
@@ -548,7 +548,7 @@ The solution is to use rewrite operations in a downward pass through the project
 
   rule <k> #projectedUpdate(
             _DEST,
-            typedValue(Reference(OFFSET, place(local(I), PLACEPROJ), _MUT), _, _),
+            typedValue(RefStack(OFFSET, place(local(I), PLACEPROJ), _MUT), _, _),
             projectionElemDeref PROJS,
             UPDATE,
             _CTXTS,
@@ -799,7 +799,7 @@ The `BorrowKind` indicates mutability of the value through the reference, but al
 ```k
   rule <k> rvalueRef(_REGION, KIND, PLACE)
          =>
-           typedValue(Reference(0, PLACE, #mutabilityOf(KIND)), TyUnknown, #mutabilityOf(KIND))
+           typedValue(RefStack(0, PLACE, #mutabilityOf(KIND)), TyUnknown, #mutabilityOf(KIND))
        ...
        </k>
 
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/value.md b/kmir/src/kmir/kdist/mir-semantics/rt/value.md
index 937faa980..7fd6ec799 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/value.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/value.md
@@ -30,7 +30,7 @@ High-level values can be
                    // heterogenous value list        for tuples and structs (standard, tuple, or anonymous)
                  | Float( Float, Int )
                    // value, bit-width               for f16-f128
-                 | Reference( Int , Place , Mutability )
+                 | Reference
                    // stack depth (initially 0), place, borrow kind
                  | Range( List )
                    // homogenous values              for array/slice
@@ -38,6 +38,9 @@ High-level values can be
                    // address, metadata              for ref/ptr
                  | "Any"
                    // arbitrary value                for transmute/invalid ptr lookup
+
+  syntax Reference ::= RefStack( Int , Place , Mutability )
+                     | RefAlloc( Int )
 ```
 
 ## Local variables

From 8d140186e0fd5a94fbccec3e40f00af150b899e8 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Fri, 16 May 2025 15:17:05 -0400
Subject: [PATCH 7/9] Decoding Constant with Prov

---
 kmir/src/kmir/kdist/mir-semantics/rt/data.md | 22 +++++++++++++-------
 1 file changed, 15 insertions(+), 7 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 6d38587de..fc20a0212 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -74,10 +74,11 @@ Constant operands are simply decoded according to their type.
 ```k
   rule <k> operandConstant(constOperand(_, _, mirConst(KIND, TY, _)))
         =>
-           typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo), TY, mutabilityNot)
+           typedValue(#decodeConstant(KIND, {TYPEMAP[TY]}:>TypeInfo, MEM), TY, mutabilityNot)
         ...
       </k>
       <types> TYPEMAP </types>
+      <memory> MEM </memory>
     requires TY in_keys(TYPEMAP)
      andBool isTypeInfo(TYPEMAP[TY])
     [preserves-definedness] // valid Map lookup checked
@@ -851,19 +852,19 @@ bit width, signedness, and possibly truncating or 2s-complementing the value.
 The `Value` sort above operates at a higher level than the bytes representation found in the MIR syntax for constant values. The bytes have to be interpreted according to the given `TypeInfo` to produce the higher-level value. This is currently only defined for `PrimitiveType`s (primitive types in MIR).
 
 ```k
-  syntax Value ::= #decodeConstant ( ConstantKind, TypeInfo ) [function]
+  syntax Value ::= #decodeConstant ( ConstantKind, TypeInfo, Map ) [function]
 
   //////////////////////////////////////////////////////////////////////////////////////
   // decoding the correct amount of bytes depending on base type size
 
   // Boolean: should be one byte with value one or zero
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(false)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool), _MEM) => BoolVal(false)
     requires 0 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool)) => BoolVal(true)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeBool), _MEM) => BoolVal(true)
     requires 1 ==Int Bytes2Int(BYTES, LE, Unsigned) andBool lengthBytes(BYTES) ==Int 1
 
   // Integer: handled in separate module for numeric operations
-  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO)
+  rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), TYPEINFO, _MEM)
       =>
         #decodeInteger(BYTES, #intTypeOf(TYPEINFO))
     requires #isIntType(TYPEINFO)
@@ -872,16 +873,23 @@ The `Value` sort above operates at a higher level than the bytes representation
 
   ////////////////////////////////////////////////////////////////////////////////////////////////
   // FIXME Char type
-  // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _)), typeInfoPrimitiveType(primTypeChar))
+  // rule #decodeConstant(constantKindAllocated(allocation(BYTES, _, _, _), _MEM), typeInfoPrimitiveType(primTypeChar))
   //     =>
   //      Str(...)
   /////////////////////////////////////////////////////////////////////////////////////////////////
 
+  rule #decodeConstant(constantKindAllocated(allocation(_BYTES, provenanceMap(
+          provenanceMapEntry(_SIZE, allocId(ID:Int)) .ProvenanceMapEntries
+        ), _ALIGN, _MUT)), typeInfoRefType(_TY), MEMORY)
+     =>
+       RefAlloc(ID)
+     requires ID in_keys(MEMORY)
+     [preserves-definedness] // AllocId in Memory is checked, TY in Types checked previously
 
   /////////////////////////////////////////////////////////////////////////////////////////////////
   // TODO Float decoding: not supported natively in K
 
-  rule #decodeConstant(_, _) => Any [owise]
+  rule #decodeConstant(_, _, _) => Any [owise]
 ```
 
 ## Primitive operations on numeric data

From 05e9a3b66047b54dc1c95aea423df996037f397e Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Fri, 16 May 2025 15:19:19 -0400
Subject: [PATCH 8/9] Added tests with GlobalAlloc / promoted

---
 .../data/prove-rs/ptr-metadata-array-fail.rs    |  6 ++++++
 .../data/prove-rs/ptr-metadata-slice-fail.rs    |  4 ++++
 .../show/ptr-metadata-array-fail.expected       | 17 +++++++++++++++++
 .../show/ptr-metadata-slice-fail.expected       | 16 ++++++++++++++++
 kmir/src/tests/integration/test_integration.py  |  2 ++
 5 files changed, 45 insertions(+)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-metadata-array-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-metadata-slice-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-array-fail.expected
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-slice-fail.expected

diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-metadata-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-metadata-array-fail.rs
new file mode 100644
index 000000000..a06ffc2d8
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ptr-metadata-array-fail.rs
@@ -0,0 +1,6 @@
+fn main() {
+    let len = [1; 2].len();
+    let len2 = [4; 3].len();
+    assert!(len == 2);
+    assert!(len2 == 3);
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-metadata-slice-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-metadata-slice-fail.rs
new file mode 100644
index 000000000..4e441f695
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ptr-metadata-slice-fail.rs
@@ -0,0 +1,4 @@
+fn main() {
+    let t = [1; 2];
+    assert!(&t[..] == t);
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-array-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-array-fail.expected
new file mode 100644
index 000000000..f9d5bf1fb
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-array-fail.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "ptr_metadata_array_fail" ) globalAllocEntry ( 0 , Memory ( all
+│   function: main
+│   span: 51
+│
+│  (27 steps)
+└─ 3 (stuck, leaf)
+    #applyUnOp ( unOpPtrMetadata , typedValue ( thunk ( #cast ( typedValue ( RefAllo
+    function: main
+    span: 53
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-slice-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-slice-fail.expected
new file mode 100644
index 000000000..40e235a6c
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-metadata-slice-fail.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #init ( symbol ( "ptr_metadata_slice_fail" ) globalAllocEntry ( 1 , Memory ( all
+│   function: main
+│   span: 127
+│
+│  (156 steps)
+└─ 3 (stuck, leaf)
+    #applyUnOp ( unOpPtrMetadata , typedValue ( thunk ( #cast ( typedValue ( RefStac
+    span: 58
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 89b8cab6d..abc2b75cd 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -435,6 +435,8 @@ def test_prove(spec: Path, tmp_path: Path, kmir: KMIR) -> None:
     'interior-mut3-fail',
     'assert_eq_exp-fail',
     'bitwise-not-shift-fail',
+    'ptr-metadata-array-fail',
+    'ptr-metadata-slice-fail',
 ]
 
 

From 1005aa0c4ab8c5b0702c4a4a206b26979a329095 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Fri, 16 May 2025 15:54:07 -0400
Subject: [PATCH 9/9] Updated output of tests

---
 .../arithmetic-unchecked-runs.state           |  3 +-
 .../exec-smir/arrays/array_indexing.state     |  2 +-
 .../data/exec-smir/arrays/array_write.state   |  4 +--
 .../data/exec-smir/references/doubleRef.state | 13 ++++----
 .../exec-smir/references/mutableRef.state     |  7 +++--
 .../data/exec-smir/references/refAsArg.state  |  4 +--
 .../data/exec-smir/references/refAsArg2.state |  4 +--
 .../exec-smir/references/refReturned.state    |  6 ++--
 .../data/exec-smir/references/simple.state    |  4 +--
 .../data/exec-smir/references/weirdRefs.state | 30 +++++++++++--------
 .../prove-rs/show/assert_eq_exp-fail.expected |  2 +-
 .../show/bitwise-not-shift-fail.expected      |  2 +-
 12 files changed, 44 insertions(+), 37 deletions(-)

diff --git a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
index 53eeafebc..2b77e91a2 100644
--- a/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
+++ b/kmir/src/tests/integration/data/exec-smir/arithmetic/arithmetic-unchecked-runs.state
@@ -55,7 +55,8 @@
     .List
   </stack>
   <memory>
-    .Map
+    2 |-> Memory ( allocation (... bytes: b"unsafe precondition(s) violated: u8::unchecked_add cannot overflow" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    3 |-> Memory ( allocation (... bytes: b"unsafe precondition(s) violated: i8::unchecked_sub cannot overflow" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
index 00e97802c..0162c2d25 100644
--- a/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
+++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_indexing.state
@@ -50,7 +50,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: b == c" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
index 0f43ea603..3ce67125c 100644
--- a/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
+++ b/kmir/src/tests/integration/data/exec-smir/arrays/array_write.state
@@ -39,7 +39,7 @@
       ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 25 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 25 ) , mutabilityMut ) )
       ListItem ( Moved )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemIndex ( local ( 6 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: projectionElemIndex ( local ( 6 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 25 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 4 , 64 , false ) , ty ( 25 ) , mutabilityMut ) )
       ListItem ( Moved )
@@ -59,7 +59,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: a[0] == a[1]" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
index a1b59c1a6..6525a9527 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/doubleRef.state
@@ -32,25 +32,26 @@
     <locals>
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 25 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 2 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 25 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) )
       ListItem ( Moved )
       ListItem ( Moved )
       ListItem ( Moved )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 11 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 25 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 11 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 25 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 34 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 22 ) , mutabilityMut ) )
     </locals>
   </currentFrame>
   <stack>
     .List
   </stack>
   <memory>
-    .Map
+    2 |-> Memory ( allocation (... bytes: b"assertion failed: **z == x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    3 |-> Memory ( allocation (... bytes: b"assertion failed: z == &&x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
index 4e94dcbac..3f4ead477 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/mutableRef.state
@@ -33,10 +33,10 @@
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 22 , 8 , true ) , ty ( 2 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 1 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 28 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 28 ) , mutabilityMut ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 28 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 28 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
     </locals>
@@ -45,7 +45,8 @@
     .List
   </stack>
   <memory>
-    .Map
+    2 |-> Memory ( allocation (... bytes: b"assertion failed: x == 32" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    3 |-> Memory ( allocation (... bytes: b"assertion failed: x == 22" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
index f7644429c..b7d70e4ff 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg.state
@@ -31,7 +31,7 @@
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) )
     </locals>
@@ -40,7 +40,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: z == x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
index 794203331..c97fc9834 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refAsArg2.state
@@ -31,7 +31,7 @@
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) )
     </locals>
@@ -40,7 +40,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: z == x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
index 51a91f2bc..1b38ddc4a 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/refReturned.state
@@ -30,8 +30,8 @@
     <locals>
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 28 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 30 ) , mutabilityMut ) )
@@ -41,7 +41,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: z == x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/simple.state b/kmir/src/tests/integration/data/exec-smir/references/simple.state
index 87f5b17ef..9f62ed9cb 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/simple.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/simple.state
@@ -29,7 +29,7 @@
     <locals>
       ListItem ( newLocal ( ty ( 1 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 27 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityNot ) , ty ( 27 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 42 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 29 ) , mutabilityMut ) )
@@ -39,7 +39,7 @@
     .List
   </stack>
   <memory>
-    .Map
+    1 |-> Memory ( allocation (... bytes: b"assertion failed: z == x" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
index 76b6b45ca..c9b5aea89 100644
--- a/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
+++ b/kmir/src/tests/integration/data/exec-smir/references/weirdRefs.state
@@ -39,36 +39,40 @@
       ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( typedValue ( Integer ( 43 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( BoolVal ( true ) , ty ( 25 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 43 , 64 , false ) , ty ( 26 ) , mutabilityMut ) ) ) , ty ( 30 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 33 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 5 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 33 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) ) ) , ty ( 34 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 35 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) ) ) , ty ( 34 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 9 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 35 ) , mutabilityNot ) )
       ListItem ( typedValue ( Integer ( 43 , 8 , true ) , ty ( 2 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 23 ) , projection: projectionElemDeref  projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 36 ) , mutabilityNot ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 23 ) , projection: projectionElemDeref  projectionElemField ( fieldIdx ( 2 ) , ty ( 26 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 36 ) , mutabilityNot ) )
       ListItem ( Moved )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
       ListItem ( Moved )
       ListItem ( newLocal ( ty ( 32 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 2 ) )  .ProjectionElems ) , mutabilityMut ) , ty ( 31 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
+      ListItem ( typedValue ( RefStack ( 0 , place (... local: local ( 1 ) , projection: .ProjectionElems ) , mutabilityMut ) , ty ( 29 ) , mutabilityMut ) )
     </locals>
   </currentFrame>
   <stack>
     .List
   </stack>
   <memory>
-    .Map
+    5 |-> Memory ( allocation (... bytes: b"assertion failed: a.a_value == 42" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    6 |-> Memory ( allocation (... bytes: b"assertion failed: a.a_value == 43" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    7 |-> Memory ( allocation (... bytes: b"assertion failed: vv == 43" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    8 |-> Memory ( allocation (... bytes: b"assertion failed: a.another" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
+    9 |-> Memory ( allocation (... bytes: b"assertion failed: a.a_third == 43" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 1 ) , mutability: mutabilityNot ) )
   </memory>
   <functions>
     ty ( 13 ) |-> monoItemFn (... name: symbol ( "std::sys::backtrace::__rust_begin_short_backtrace::<fn(), ()>" ) , id: defId ( 2 ) , body: someBody ( body (... blocks: basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 31 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 19 ) , id: mirConstId ( 3 ) ) ) ) , args: operandMove ( place (... local: local ( 1 ) , projection: .ProjectionElems ) )  operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 0 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 1 ) ) , unwind: unwindActionContinue ) , span: span ( 33 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindCall (... func: operandConstant ( constOperand (... span: span ( 34 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 20 ) , id: mirConstId ( 5 ) ) ) ) , args: operandConstant ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) )  .Operands , destination: place (... local: local ( 2 ) , projection: .ProjectionElems ) , target: someBasicBlockIdx ( basicBlockIdx ( 2 ) ) , unwind: unwindActionUnreachable ) , span: span ( 35 ) ) )  basicBlock (... statements: .Statements , terminator: terminator (... kind: terminatorKindReturn , span: span ( 36 ) ) )  .BasicBlocks , locals: localDecl (... ty: ty ( 1 ) , span: span ( 37 ) , mut: mutabilityMut )  localDecl (... ty: ty ( 7 ) , span: span ( 38 ) , mut: mutabilityNot )  localDecl (... ty: ty ( 1 ) , span: span ( 39 ) , mut: mutabilityNot )  .LocalDecls , argCount: 1 , varDebugInfo: varDebugInfo (... name: symbol ( "f" ) , sourceInfo: sourceInfo (... span: span ( 38 ) , scope: sourceScope ( 0 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 1 ) , projection: .ProjectionElems ) ) , argumentIndex: someInt ( 1 ) )  varDebugInfo (... name: symbol ( "result" ) , sourceInfo: sourceInfo (... span: span ( 40 ) , scope: sourceScope ( 1 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsPlace ( place (... local: local ( 0 ) , projection: .ProjectionElems ) ) , argumentIndex: noInt )  varDebugInfo (... name: symbol ( "dummy" ) , sourceInfo: sourceInfo (... span: span ( 41 ) , scope: sourceScope ( 2 ) ) , composite: noVarDebugInfoFragment , value: varDebugInfoContentsConst ( constOperand (... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindZeroSized , ty: ty ( 1 ) , id: mirConstId ( 4 ) ) ) ) , argumentIndex: someInt ( 1 ) )  .VarDebugInfos , spreadArg: noLocal , span: span ( 42 ) ) ) )
diff --git a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected
index 7ecce8811..e54da3382 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/assert_eq_exp-fail.expected
@@ -6,7 +6,7 @@
 │
 │  (88 steps)
 └─ 3 (stuck, leaf)
-    #readProjection ( typedValue ( Any , ty ( 25 ) , mutabilityNot ) , projectionEle
+    #readProjection ( typedValue ( RefAlloc ( 0 ) , ty ( 25 ) , mutabilityNot ) , pr
     function: main
     span: 101
 
diff --git a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift-fail.expected b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift-fail.expected
index 6086a86ae..63265c2bf 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift-fail.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/bitwise-not-shift-fail.expected
@@ -6,7 +6,7 @@
 │
 │  (254 steps)
 └─ 3 (stuck, leaf)
-    #readProjection ( typedValue ( Any , ty ( 25 ) , mutabilityNot ) , projectionEle
+    #readProjection ( typedValue ( RefAlloc ( 8 ) , ty ( 25 ) , mutabilityNot ) , pr
     span: 63