From e9fafdbf3580ab6f5cb2a3e2cd57647981ea8c24 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Wed, 4 Mar 2026 12:24:45 -0600 Subject: [PATCH 1/3] Added failing test (minimized from solana-token's inner_test_validate_owner.rs) --- .../data/prove-rs/iter_next_3-fail.rs | 19 +++++++++++++++++++ .../show/iter_next_3-fail.main.expected | 15 +++++++++++++++ .../src/tests/integration/test_integration.py | 1 + 3 files changed, 35 insertions(+) create mode 100644 kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.rs create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.rs new file mode 100644 index 000000000..260b11cae --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.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); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected new file mode 100644 index 000000000..67eacf7b1 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected @@ -0,0 +1,15 @@ + +┌─ 1 (root, init) +│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC +│ span: 0 +│ +│ (2164 steps) +└─ 3 (stuck, leaf) + #traverseProjection ( toStack ( 2 , local ( 1 ) ) , Range ( ListItem ( Range ( L + span: 126 + + +┌─ 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 5f36b155d..cbe716029 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -43,6 +43,7 @@ 'local-raw-fail', 'interior-mut-fail', 'interior-mut3-fail', + 'iter_next_3-fail', 'assert_eq_exp', 'bitwise-not-shift', 'symbolic-args-fail', From 99048aae7ef7117452131081065e4eb24cca1653 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Wed, 4 Mar 2026 16:34:29 -0600 Subject: [PATCH 2/3] Cast for mutability only preserves source pointer's metadata. --- kmir/src/kmir/kdist/mir-semantics/rt/data.md | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md index 840ae6095..41209fbb2 100644 --- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md +++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md @@ -1434,6 +1434,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)`) 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 #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET) + => PtrLocal(OFFSET, PLACE, MUT, META) + ... + + 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 #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET) => From 68a9792ad79b4d65c3f3d4f47b59d36cff4c7d32 Mon Sep 17 00:00:00 2001 From: mariaKt Date: Wed, 4 Mar 2026 16:38:22 -0600 Subject: [PATCH 3/3] Test iter_next_3-fail.rs -> iter_next_3.rs. --- .../{iter_next_3-fail.rs => iter_next_3.rs} | 0 .../show/iter_next_3-fail.main.expected | 15 --------------- .../prove-rs/show/iter_next_3.main.expected | 17 +++++++++++++++++ kmir/src/tests/integration/test_integration.py | 2 +- 4 files changed, 18 insertions(+), 16 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{iter_next_3-fail.rs => iter_next_3.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected create mode 100644 kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/iter_next_3-fail.rs rename to kmir/src/tests/integration/data/prove-rs/iter_next_3.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected deleted file mode 100644 index 67eacf7b1..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (2164 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toStack ( 2 , local ( 1 ) ) , Range ( ListItem ( Range ( L - span: 126 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iter_next_3.main.expected new file mode 100644 index 000000000..a4c5bdc3d --- /dev/null +++ b/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 + + + diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index cbe716029..3014e4b04 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -43,7 +43,7 @@ 'local-raw-fail', 'interior-mut-fail', 'interior-mut3-fail', - 'iter_next_3-fail', + 'iter_next_3', 'assert_eq_exp', 'bitwise-not-shift', 'symbolic-args-fail',