From 7eac740d1dfb4b059092b248e6d3d888c678c15b Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Thu, 6 Nov 2025 20:34:33 +0800
Subject: [PATCH 1/3] fix(rt): Apply adjustRef when updating stack locals

---
 kmir/src/kmir/kdist/mir-semantics/rt/data.md | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 7adc8dd0f..b6170942f 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -269,7 +269,11 @@ A `Deref` projection in the projections list changes the target of the write ope
        </k>
        <stack> STACK
             => STACK[(FRAME -Int 1) <-
-                      #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(NEW, CONTEXTS))
+                      #updateStackLocal(
+                        {STACK[FRAME -Int 1]}:>StackFrame,
+                        I,
+                        #adjustRef(#buildUpdate(NEW, CONTEXTS), 0 -Int FRAME)
+                      )
                     ]
        </stack>
     requires 0 <Int FRAME andBool FRAME <=Int size(STACK)
@@ -283,7 +287,11 @@ A `Deref` projection in the projections list changes the target of the write ope
        </k>
        <stack> STACK
             => STACK[(FRAME -Int 1) <-
-                      #updateStackLocal({STACK[FRAME -Int 1]}:>StackFrame, I, #buildUpdate(Moved, CONTEXTS)) // TODO retain Ty and Mutability from _ORIGINAL
+                      #updateStackLocal(
+                        {STACK[FRAME -Int 1]}:>StackFrame,
+                        I,
+                        #adjustRef(#buildUpdate(Moved, CONTEXTS), 0 -Int FRAME)
+                      ) // TODO retain Ty and Mutability from _ORIGINAL
                     ]
        </stack>
     requires 0 <Int FRAME andBool FRAME <=Int size(STACK)

From f3e5c4db73230d55e4a30dba7fb94786d18035de Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 7 Nov 2025 09:21:08 +0800
Subject: [PATCH 2/3] test(prove-rs): Add stack assign integration test

---
 .../tests/integration/data/prove-rs/stack_assign.rs | 13 +++++++++++++
 1 file changed, 13 insertions(+)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/stack_assign.rs

diff --git a/kmir/src/tests/integration/data/prove-rs/stack_assign.rs b/kmir/src/tests/integration/data/prove-rs/stack_assign.rs
new file mode 100644
index 000000000..c0773f656
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/stack_assign.rs
@@ -0,0 +1,13 @@
+fn assign<'a>(dst: &mut &'a i32, src: &&'a i32) {
+    *dst = *src;
+}
+
+fn main() {
+    let x = 1;
+    let mut dst = &x;
+    let src = dst;
+
+    assign(&mut dst, &src);
+
+    assert_eq!(*dst, 1);
+}

From 1c3f2fabcacd9096be6a7ff0d81813e74f48809a Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 7 Nov 2025 03:57:35 +0000
Subject: [PATCH 3/3] test: udpate expected output

---
 .../pointer-cast-length-test-fail.array_cast_test.expected    | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
index ff6808691..2688fd0d2 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
@@ -41,7 +41,7 @@
    ┃  │
    ┃  │  (6 steps)
    ┃  ├─ 10
-   ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range (
+   ┃  │   #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff
    ┃  │   span: 87
    ┃  ┃
    ┃  ┃ (1 step)
@@ -59,7 +59,7 @@
    ┃  ┗━━┓
    ┃     │
    ┃     └─ 12 (stuck, leaf)
-   ┃         #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( range (
+   ┃         #traverseProjection ( toStack ( 1 , local ( 2 ) ) , Range ( #mapOffset ( #mapOff
    ┃         span: 87
    ┃
    ┗━━┓