fix(data): resolve alignment check stuck state for pointer dereferences

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

@@ -1624,20 +1624,36 @@ What can be supported without additional layout consideration is trivial casts b
       requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
 ```
 
-Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A.
-The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`:
+Transmuting a pointer to `usize` occurs in compiler-generated alignment checks.
+Since KMIR uses an abstract pointer model without real memory addresses, all pointers are
+properly aligned by construction. We return `Integer(0, 64, false)` as a maximally-aligned
+abstract address, which ensures the alignment check evaluates concretely (rather than remaining
+stuck as a `thunk`) and passes as expected.
 
 ```k
-  rule <k> #cast(
-              thunk(#cast(DATA, castKindTransmute, TY_SRC_INNER, TY_DEST_INNER)),
-              castKindTransmute,
-              TY_SRC_OUTER,
-              TY_DEST_OUTER
-            ) => DATA
+  rule <k> #cast(PtrLocal(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+          =>
+            Integer(0, 64, false)
           ...
-       </k>
-    requires lookupTy(TY_SRC_INNER) ==K lookupTy(TY_DEST_OUTER) // cast is a round-trip
-     andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant)
+        </k>
+      requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+    [priority(45)]
+
+  rule <k> #cast(Reference(_, _, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+          =>
+            Integer(0, 64, false)
+          ...
+        </k>
+      requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+    [priority(45)]
+
+  rule <k> #cast(AllocRef(_, _, _), castKindTransmute, _TY_SOURCE, TY_TARGET)
+          =>
+            Integer(0, 64, false)
+          ...
+        </k>
+      requires lookupTy(TY_TARGET) ==K typeInfoPrimitiveType(primTypeUint(uintTyUsize))
+    [priority(45)]
 ```
 
 Transmuting a value `T` into a single-field wrapper struct `G<T>` (or vice versa) is sound when the struct

kmir/src/tests/integration/data/prove-rs/alignment-check.rs

@@ -0,0 +1,14 @@
+// Test for issue #638: alignment check in raw pointer dereference.
+// The compiler inserts an alignment check that transmutes a pointer to usize.
+// Verifies that the transmute cast evaluates concretely.
+
+struct Thing { payload: i16 }
+
+fn main() {
+    let a = [Thing { payload: 1 }, Thing { payload: 2 }, Thing { payload: 3 }];
+    let p = &a as *const Thing;
+    let p1 = unsafe { p.add(1) };
+
+    let two = unsafe { (*p1).payload };
+    assert!(two == 2);
+}

kmir/src/tests/integration/data/prove-rs/raw-ptr-cast-fail.rs → kmir/src/tests/integration/data/prove-rs/raw-ptr-cast.rs

@@ -5,6 +5,6 @@ fn main() {
     let ptr_mut = &mut data as *mut i32;
     unsafe {
         (*ptr_mut) = 44;
-        assert_eq!(44, *ptr); // FIXME: fails due to thunks on casts
+        assert_eq!(44, *ptr);
     }
 }

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

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

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

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

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

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

kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper.main.expected

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