From f8b6de0c74fce1bb62bac9e6fe9ea0e5dede8e79 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 17:34:43 +0800
Subject: [PATCH 1/7] test(prove-rs): add ptr-cast-wrapper-to-array-fail
 reproducer

Demonstrates stuck #traverseProjection caused by incorrect projection
chain SingletonArray+Field(0)+ConstantIndex(0) from #pointeeProjection
when casting *const Wrapper to *const [u8; 2].

Minimal reproducer from @dkcumming's review comment on PR #988.
---
 .../prove-rs/ptr-cast-wrapper-to-array-fail.rs   |  7 +++++++
 .../ptr-cast-wrapper-to-array-fail.main.expected | 16 ++++++++++++++++
 kmir/src/tests/integration/test_integration.py   |  1 +
 3 files changed, 24 insertions(+)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected

diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.rs
new file mode 100644
index 000000000..dbc4625ac
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.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]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected
new file mode 100644
index 000000000..21d56fc68
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected
@@ -0,0 +1,16 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (70 steps)
+└─ 3 (stuck, leaf)
+    #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+    function: main
+    span: 278
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index c67f6275f..4b425c376 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -68,6 +68,7 @@
     'volatile_store_static-fail',
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
+    'ptr-cast-wrapper-to-array-fail',
 ]
 
 

From d455d674bfd720bd08c15a9dca312345b9f015b7 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 17:38:22 +0800
Subject: [PATCH 2/7] fix(types): add priority(45) to struct rules in
 #pointeeProjection
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

This fixes ptr-cast-wrapper-to-array by ensuring struct unwrapping
takes precedence over array unwrapping. However, it REGRESSES
iter_next_2 (renamed to iter_next_2-fail) because that test needs
the opposite priority (array first for [Thing;3] → Thing).

This commit demonstrates why priority alone cannot fix the
non-deterministic overlap — the two cases need conflicting priorities.
---
 kmir/src/kmir/kdist/mir-semantics/rt/types.md   |  2 ++
 .../{iter_next_2.rs => iter_next_2-fail.rs}     |  0
 ...ray-fail.rs => ptr-cast-wrapper-to-array.rs} |  0
 ....expected => iter_next_2-fail.main.expected} |  7 +++----
 .../ptr-cast-wrapper-to-array.main.expected     | 17 +++++++++++++++++
 kmir/src/tests/integration/test_integration.py  |  3 ++-
 6 files changed, 24 insertions(+), 5 deletions(-)
 rename kmir/src/tests/integration/data/prove-rs/{iter_next_2.rs => iter_next_2-fail.rs} (100%)
 rename kmir/src/tests/integration/data/prove-rs/{ptr-cast-wrapper-to-array-fail.rs => ptr-cast-wrapper-to-array.rs} (100%)
 rename kmir/src/tests/integration/data/prove-rs/show/{ptr-cast-wrapper-to-array-fail.main.expected => iter_next_2-fail.main.expected} (62%)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
index 3998cb3eb..ea174b6bc 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
@@ -121,6 +121,7 @@ Pointers to structs with a single zero-offset field are compatible with pointers
           #pointeeProjection(lookupTy(FIELD), OTHER)
         )
     requires #zeroFieldOffset(LAYOUT)
+    [priority(45)]
 
   rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
     => maybeConcatProj(
@@ -128,6 +129,7 @@ Pointers to structs with a single zero-offset field are compatible with pointers
           #pointeeProjection(OTHER, lookupTy(FIELD))
         )
     requires #zeroFieldOffset(LAYOUT)
+    [priority(45)]
 ```
 
 Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_2.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/iter_next_2.rs
rename to kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/ptr-cast-wrapper-to-array.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
similarity index 62%
rename from kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected
rename to kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
index 21d56fc68..d1be7c58c 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
@@ -3,11 +3,10 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (70 steps)
+│  (629 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
-    function: main
-    span: 278
+    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Aggregate ( variantIdx ( 0 )
+    span: 146
 
 
 ┌─ 2 (root, leaf, target, terminal)
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected
new file mode 100644
index 000000000..639ce03bf
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (214 steps)
+├─ 3 (terminal)
+│   #EndProgram ~> .K
+│   function: main
+│
+┊  constraint: true
+┊  subst: ...
+└─ 2 (leaf, target, terminal)
+    #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 4b425c376..d1b27ddef 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -68,7 +68,8 @@
     'volatile_store_static-fail',
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
-    'ptr-cast-wrapper-to-array-fail',
+    'ptr-cast-wrapper-to-array',
+    'iter_next_2-fail',
 ]
 
 

From aeefea2a3b59386aa942b94103bee8047703d423 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 17:42:31 +0800
Subject: [PATCH 3/7] fix(types): make #pointeeProjection confluent with
 source-first strategy

Revert the priority approach (which regressed iter_next_2) and instead
refactor #pointeeProjection to always unwrap the source type first.
Target-side unwrapping is deferred to #pointeeProjectionTarget, only
reached when source cannot be unwrapped further.

This eliminates the non-deterministic overlap because a type cannot be
both a struct and an array simultaneously. Both ptr-cast-wrapper-to-array
and iter_next_2 now pass.
---
 kmir/src/kmir/kdist/mir-semantics/rt/types.md | 61 +++++++++++--------
 .../{iter_next_2-fail.rs => iter_next_2.rs}   |  0
 .../show/iter_next_2-fail.main.expected       | 15 -----
 .../src/tests/integration/test_integration.py |  1 -
 4 files changed, 37 insertions(+), 40 deletions(-)
 rename kmir/src/tests/integration/data/prove-rs/{iter_next_2-fail.rs => iter_next_2.rs} (100%)
 delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
index ea174b6bc..932013f6a 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md
+++ b/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,24 +101,20 @@ 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
+Source-side: unwrap structs and arrays from the source type first.
 ```k
-
   rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
     => maybeConcatProj(
           projectionElemField(fieldIdx(0), FIELD),
           #pointeeProjection(lookupTy(FIELD), OTHER)
         )
     requires #zeroFieldOffset(LAYOUT)
-    [priority(45)]
 
-  rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+  rule #pointeeProjection(typeInfoArrayType(TY1, _), TY2)
     => maybeConcatProj(
-          projectionElemWrapStruct,
-          #pointeeProjection(OTHER, lookupTy(FIELD))
+          projectionElemConstantIndex(0, 0, false),
+          #pointeeProjection(lookupTy(TY1), TY2)
         )
-    requires #zeroFieldOffset(LAYOUT)
-    [priority(45)]
 ```
 
 Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
@@ -150,6 +135,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]
   // --------------------------------------------------------------------
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_2.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/iter_next_2-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/iter_next_2.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
deleted file mode 100644
index d1be7c58c..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/iter_next_2-fail.main.expected
+++ /dev/null
@@ -1,15 +0,0 @@
-
-┌─ 1 (root, init)
-│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│   span: 0
-│
-│  (629 steps)
-└─ 3 (stuck, leaf)
-    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Aggregate ( variantIdx ( 0 )
-    span: 146
-
-
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K
-
-
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index d1b27ddef..9435b93f2 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -69,7 +69,6 @@
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
     'ptr-cast-wrapper-to-array',
-    'iter_next_2-fail',
 ]
 
 

From 0877ae179146d0b4021168fd20398a9cd8fd6f6c Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 18:14:22 +0800
Subject: [PATCH 4/7] test: remove ptr-cast-wrapper-to-array from
 PROVE_SHOW_SPECS

The proof now passes with just #EndProgram, no interesting show output.
---
 .../ptr-cast-wrapper-to-array.main.expected     | 17 -----------------
 kmir/src/tests/integration/test_integration.py  |  1 -
 2 files changed, 18 deletions(-)
 delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected

diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected
deleted file mode 100644
index 639ce03bf..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-wrapper-to-array.main.expected
+++ /dev/null
@@ -1,17 +0,0 @@
-
-┌─ 1 (root, init)
-│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│   span: 0
-│
-│  (214 steps)
-├─ 3 (terminal)
-│   #EndProgram ~> .K
-│   function: main
-│
-┊  constraint: true
-┊  subst: ...
-└─ 2 (leaf, target, terminal)
-    #EndProgram ~> .K
-
-
-
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 9435b93f2..c67f6275f 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -68,7 +68,6 @@
     'volatile_store_static-fail',
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
-    'ptr-cast-wrapper-to-array',
 ]
 
 

From 0c9184d607e92d4ea103412d63204e4d32b32086 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 18:43:34 +0800
Subject: [PATCH 5/7] test(prove-rs): add ptr-cast-array-to-wrapper-fail
 (pre-existing bug)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The reverse cast *const [u8; 2] → *const Wrapper([u8; 2]) gets stuck
on both master and with the source-first strategy. This is a
pre-existing limitation of #pointeeProjection: source-first unwraps
the array before considering the target struct, producing an
uncancelable SingletonArray in the projection chain.
---
 .../ptr-cast-array-to-wrapper-fail.rs         |  8 ++++
 ...r-cast-array-to-wrapper-fail.main.expected | 39 +++++++++++++++++++
 .../src/tests/integration/test_integration.py |  1 +
 3 files changed, 48 insertions(+)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected

diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-wrapper-fail.rs
new file mode 100644
index 000000000..ae40e8d8b
--- /dev/null
+++ b/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]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected
new file mode 100644
index 000000000..a7bbe1146
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-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
+   │
+   │  (10 steps)
+   └─ 7 (stuck, leaf)
+       #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
+       function: main
+       span: 282
+
+
+┌─ 2 (root, leaf, target, terminal)
+│   #EndProgram ~> .K
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index c67f6275f..8f26f03aa 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -68,6 +68,7 @@
     'volatile_store_static-fail',
     'volatile_load_static-fail',
     'box_heap_alloc-fail',
+    'ptr-cast-array-to-wrapper-fail',
 ]
 
 

From c22c881c74e90f28fec0a5a9aade7e18756a1141 Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Fri, 20 Mar 2026 19:09:29 +0800
Subject: [PATCH 6/7] fix(types): handle array-to-wrapper cast in
 #pointeeProjection
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

When source is an array and target is a transparent struct wrapping
that same array type (e.g., *const [u8;2] → *const Wrapper([u8;2])),
the source-first strategy incorrectly unwraps the array first,
producing an uncancelable SingletonArray in the projection chain.

Add a prioritized rule that detects this case (lookupTy(FIELD) ==K SRC)
and directly produces WrapStruct, deferring to target-side wrapping.

The expected output for ptr-cast-array-to-wrapper-fail now shows
node 7 reaching #EndProgram (was previously stuck on
#traverseProjection). The test still fails overall due to an
unrelated alignment assertion on the other proof branch.
---
 kmir/src/kmir/kdist/mir-semantics/rt/types.md   | 13 +++++++++++++
 ...ptr-cast-array-to-wrapper-fail.main.expected | 17 +++++++++--------
 2 files changed, 22 insertions(+), 8 deletions(-)

diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
index 932013f6a..31ad4f915 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
@@ -102,6 +102,9 @@ Pointers to zero-sized types can be converted from and to. No recursion beyond t
 ```
 
 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(
@@ -110,6 +113,16 @@ Source-side: unwrap structs and arrays from the source type first.
         )
     requires #zeroFieldOffset(LAYOUT)
 
+  rule #pointeeProjection(SRC:TypeInfo, typeInfoStructType(_NAME, _ADTDEF, FIELD .Tys, LAYOUT))
+    => maybeConcatProj(
+          projectionElemWrapStruct,
+          #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),
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected
index a7bbe1146..2a3653a3e 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-wrapper-fail.main.expected
@@ -26,14 +26,15 @@
    │   #execBlockIdx ( basicBlockIdx ( 4 ) ) ~> .K
    │   function: main
    │
-   │  (10 steps)
-   └─ 7 (stuck, leaf)
-       #traverseProjection ( toLocal ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem (
-       function: main
-       span: 282
-
+   │  (154 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │   function: main
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
 
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K
 
 

From 898c0e81f0d0cfb9c943423cff53d8cdd467bf1f Mon Sep 17 00:00:00 2001
From: Stevengre <zhaojianhong96@gmail.com>
Date: Wed, 25 Mar 2026 00:18:32 +0000
Subject: [PATCH 7/7] test(prove-rs): add reproducers for
 nested/singleton-array pointer cast cases

Add failing tests for target-side nested struct and singleton-array wrapping:
- ptr-cast-array-to-nested-wrapper-fail: [T; N] -> W2(W1([T; N]))
- ptr-cast-array-to-singleton-wrapped-array-fail: [T; N] -> W([[T; N]; 1])

Add passing tests for source-side unwrapping (already handled):
- ptr-cast-nested-wrapper-to-array: W2(W1([T; N])) -> [T; N]
- ptr-cast-singleton-wrapped-array-to-array: W([[T; N]; 1]) -> [T; N]

Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
---
 .../ptr-cast-array-to-nested-wrapper-fail.rs  | 12 ++++++
 ...t-array-to-singleton-wrapped-array-fail.rs |  9 +++++
 .../ptr-cast-nested-wrapper-to-array.rs       |  9 +++++
 ...r-cast-singleton-wrapped-array-to-array.rs |  8 ++++
 ...array-to-nested-wrapper-fail.main.expected | 39 +++++++++++++++++++
 ...singleton-wrapped-array-fail.main.expected | 39 +++++++++++++++++++
 .../src/tests/integration/test_integration.py |  2 +
 7 files changed, 118 insertions(+)
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected
 create mode 100644 kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected

diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-nested-wrapper-fail.rs
new file mode 100644
index 000000000..9df7ec0f8
--- /dev/null
+++ b/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]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-array-to-singleton-wrapped-array-fail.rs
new file mode 100644
index 000000000..1e40d8de2
--- /dev/null
+++ b/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]]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-nested-wrapper-to-array.rs
new file mode 100644
index 000000000..ca931f6cc
--- /dev/null
+++ b/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]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs b/kmir/src/tests/integration/data/prove-rs/ptr-cast-singleton-wrapped-array-to-array.rs
new file mode 100644
index 000000000..58aa5f74c
--- /dev/null
+++ b/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]);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-nested-wrapper-fail.main.expected
new file mode 100644
index 000000000..7ea5e8b1e
--- /dev/null
+++ b/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
+
+
diff --git a/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-cast-array-to-singleton-wrapped-array-fail.main.expected
new file mode 100644
index 000000000..a7bbe1146
--- /dev/null
+++ b/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
+
+
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 5e23aa6fb..ba7faccec 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -69,6 +69,8 @@
     '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',
 ]