fix(rt): bug fix for castKindPtrToPtr

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1440,6 +1440,20 @@ which have the same representation `Value::Range`.
 Also, casts to and from _transparent wrappers_ (newtypes that just forward field `0`, i.e. `struct Wrapper<T>(T)`)
 are allowed, and supported by a special projection `WrapStruct`.
 
+When the source and target types are pointer types with the same pointee type (i.e., differing only in mutability),
+the cast preserves the source pointer and its metadata unchanged.
+
+```k
+  rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
+          => PtrLocal(OFFSET, PLACE, MUT, META)
+          ...
+        </k>
+      requires pointeeTy(lookupTy(TY_SOURCE)) ==K pointeeTy(lookupTy(TY_TARGET))
+      [priority(45), preserves-definedness] // valid map lookups checked
+```
+
+Otherwise, compute the type projection and convert metadata accordingly.
+
 ```k
   rule <k> #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
           =>

kmir/src/tests/integration/data/prove-rs/iter_next_3.rs

@@ -0,0 +1,19 @@
+struct Wrapper {
+    tag: u8,
+    a: [[u8; 32]; 3],
+}
+
+fn foo(c: &Wrapper) {
+    for elem in c.a.iter() {
+        assert!(elem[0] != 0);
+    }
+}
+
+fn main() {
+    let c = Wrapper {
+        tag: 42,
+        a: [[1u8; 32], [2u8; 32], [3u8; 32]],
+    };
+
+    foo(&c);
+}

kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected

@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (2028 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/test_integration.py

@@ -43,6 +43,7 @@
     'local-raw-fail',
     'interior-mut-fail',
     'interior-mut3-fail',
+    'iter_next_3',
     'assert_eq_exp',
     'bitwise-not-shift',
     'symbolic-args-fail',