fix(types): make #pointeeProjection confluent with source-first unwrapping strategy

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

@@ -76,29 +76,18 @@ It also implements cancellation of inverse projections (such as casting from one
 
 The `#pointeeProjection` function computes, for compatible pointee types, how to project from one pointee to the other.
 
+It uses a **source-first strategy**: always unwrap the source type (struct wrapper or array) before
+attempting to unwrap the target type. This eliminates non-deterministic overlap between source-side
+and target-side rules, because a type cannot be both a struct and an array simultaneously.
+When the source cannot be unwrapped further, target-side unwrapping is handled by `#pointeeProjectionTarget`.
+
 ```k
   syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total]
 ```
 
 A short-cut rule for identical types takes preference.
-As a default, no projection elements are returned for incompatible types.
 ```k
   rule #pointeeProjection(T , T) => .ProjectionElems  [priority(40)]
-  rule #pointeeProjection(_ , _) => NoProjectionElems [owise]
-```
-
-Pointers to arrays/slices are compatible with pointers to the element type
-```k
-  rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
-    => maybeConcatProj(
-          projectionElemConstantIndex(0, 0, false),
-          #pointeeProjection(lookupTy(TY1), TY2)
-        )
-  rule #pointeeProjection(TY1, typeInfoArrayType(TY2, _))
-    => maybeConcatProj(
-          projectionElemSingletonArray,
-          #pointeeProjection(TY1, lookupTy(TY2))
-        )
 ```
 
 Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST.
@@ -112,22 +101,33 @@ Pointers to zero-sized types can be converted from and to. No recursion beyond t
     [priority(45)]
 ```
 
-Pointers to structs with a single zero-offset field are compatible with pointers to that field's type
-```k
+Source-side: unwrap structs and arrays from the source type first.
 
+When source is an array and target is a transparent wrapper whose inner type equals the source,
+the source should be wrapped rather than unwrapped (e.g., `*const [u8;2] → *const Wrapper([u8;2])`).
+```k
   rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
     => maybeConcatProj(
           projectionElemField(fieldIdx(0), FIELD),
           #pointeeProjection(lookupTy(FIELD), OTHER)
         )
     requires #zeroFieldOffset(LAYOUT)
 
-  rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+  rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT))
     => maybeConcatProj(
           projectionElemWrapStruct,
-          #pointeeProjection(OTHER, lookupTy(FIELD))
+          #pointeeProjection(SRC, lookupTy(FIELD))
+        )
+    requires #isArrayType(SRC)
+    andBool #zeroFieldOffset(LAYOUT)
+    andBool lookupTy(FIELD) ==K SRC
+    [priority(42)]
+
+  rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
+    => maybeConcatProj(
+          projectionElemConstantIndex(0, 0, false),
+          #pointeeProjection(lookupTy(TY1), TY2)
         )
-    requires #zeroFieldOffset(LAYOUT)
 ```
 
 Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
@@ -148,6 +148,34 @@ which is a singleton struct (see above).
      andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO
 ```
 
+Fallback: source is not unwrappable, delegate to target-side.
+```k
+  rule #pointeeProjection(SRC, TGT) => #pointeeProjectionTarget(SRC, TGT) [owise]
+```
+
+Target-side fallback: only reached when source cannot be unwrapped further.
+After one step of target unwrapping, recurse back to `#pointeeProjection` to maintain
+the source-first strategy.
+
+```k
+  syntax MaybeProjectionElems ::= #pointeeProjectionTarget ( TypeInfo , TypeInfo ) [function, total]
+
+  rule #pointeeProjectionTarget(TY1, typeInfoArrayType(TY2, _))
+    => maybeConcatProj(
+          projectionElemSingletonArray,
+          #pointeeProjection(TY1, lookupTy(TY2))
+        )
+
+  rule #pointeeProjectionTarget(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+    => maybeConcatProj(
+          projectionElemWrapStruct,
+          #pointeeProjection(OTHER, lookupTy(FIELD))
+        )
+    requires #zeroFieldOffset(LAYOUT)
+
+  rule #pointeeProjectionTarget(_, _) => NoProjectionElems [owise]
+```
+
 ```k
   syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
   // --------------------------------------------------------------------

kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs

@@ -0,0 +1,12 @@
+// [T; N] -> W2(W1([T; N])) - nested struct wrapping on target
+#[derive(Clone, Copy, PartialEq, Debug)]
+struct Inner([u8; 2]);
+
+#[derive(Clone, Copy, PartialEq, Debug)]
+struct Outer(Inner);
+
+fn main() {
+    let arr: [u8; 2] = [11, 22];
+    let o: Outer = unsafe { *((&arr) as *const [u8; 2] as *const Outer) };
+    assert_eq!(o.0 .0, [11, 22]);
+}

kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs

@@ -0,0 +1,9 @@
+// [T; N] -> W([[T; N]; 1]) - singleton-array wrapping array (in-wrapper) on target
+#[derive(Clone, Copy, PartialEq, Debug)]
+struct Wrapper([[u8; 2]; 1]);
+
+fn main() {
+    let arr: [u8; 2] = [11, 22];
+    let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) };
+    assert_eq!(w.0, [[11, 22]]);
+}

kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs

@@ -0,0 +1,8 @@
+#[derive(Clone, Copy, PartialEq, Debug)]
+struct Wrapper([u8; 2]);
+
+fn main() {
+    let arr: [u8; 2] = [11, 22];
+    let w: Wrapper = unsafe { *((&arr) as *const [u8; 2] as *const Wrapper) };
+    assert_eq!(w.0, [11, 22]);
+}

kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs

@@ -0,0 +1,9 @@
+// W2(W1([T; N])) -> [T; N] - nested struct wrapping on source
+struct Inner([u8; 2]);
+struct Outer(Inner);
+
+fn main() {
+    let o = Outer(Inner([11, 22]));
+    let arr: [u8; 2] = unsafe { *((&o) as *const Outer as *const [u8; 2]) };
+    assert_eq!(arr, [11, 22]);
+}

kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs

@@ -0,0 +1,8 @@
+// W([[T; N]; 1]) -> [T; N] - singleton-array wrapping array (in-wrapper) on source
+struct Wrapper([[u8; 2]; 1]);
+
+fn main() {
+    let w = Wrapper([[11, 22]]);
+    let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
+    assert_eq!(arr, [11, 22]);
+}

kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs

@@ -0,0 +1,7 @@
+struct Wrapper([u8; 2]);
+
+fn main() {
+    let w = Wrapper([11, 22]);
+    let arr: [u8; 2] = unsafe { *((&w) as *const Wrapper as *const [u8; 2]) };
+    assert_eq!(arr, [11, 22]);
+}

kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected

@@ -0,0 +1,39 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (128 steps)
+├─ 3
+│   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+│   function: main
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+┃  │   function: main
+┃  │
+┃  │  (1 step)
+┃  └─ 6 (stuck, leaf)
+┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+┃      function: main
+┃
+┗━━┓
+   │
+   ├─ 5
+   │   #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
+   │   function: main
+   │
+   │  (11 steps)
+   └─ 7 (stuck, leaf)
+       #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+       function: main
+       span: 282
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected

@@ -0,0 +1,39 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (128 steps)
+├─ 3
+│   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+│   function: main
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+┃  │   function: main
+┃  │
+┃  │  (1 step)
+┃  └─ 6 (stuck, leaf)
+┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+┃      function: main
+┃
+┗━━┓
+   │
+   ├─ 5
+   │   #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
+   │   function: main
+   │
+   │  (10 steps)
+   └─ 7 (stuck, leaf)
+       #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+       function: main
+       span: 282
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+

kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected

@@ -0,0 +1,40 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (128 steps)
+├─ 3
+│   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+│   function: main
+┃
+┃ (1 step)
+┣━━┓
+┃  │
+┃  ├─ 4
+┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+┃  │   function: main
+┃  │
+┃  │  (1 step)
+┃  └─ 6 (stuck, leaf)
+┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+┃      function: main
+┃
+┗━━┓
+   │
+   ├─ 5
+   │   #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
+   │   function: main
+   │
+   │  (154 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │   function: main
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+

kmir/src/tests/integration/test_integration.py

@@ -68,6 +68,9 @@
     'volatile_store_static-fail',
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
+    'ptr-cast-array-to-wrapper-fail',
+    'ptr-cast-array-to-nested-wrapper-fail',
+    'ptr-cast-array-to-singleton-wrapped-array-fail',
 ]