fix(rt): Apply adjustRef when updating stack locals (#805)

Author: Stevengre

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)

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
    ┃
    ┗━━┓

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);
+}