From 697e68a491475741ab72e0496a82c5e9f09d6d58 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Wed, 4 Mar 2026 15:18:36 +0800 Subject: [PATCH 1/3] fix(rt): handle fun-type closure env refs in callee setup (#956) - Extend closure callee setup (`setupCalleeClosure2`) to accept closure-env references whose pointee resolves to `typeInfoFunType` (in addition to `typeInfoVoidType`). - Add `isFunType(TypeInfo)` helper predicate used by that guard. - In the fix commit, refresh `closure_access_struct-fail.main.expected` to show the behavior change from stuck frontier to terminal `#EndProgram`. - Cleanup after fix: - rename `closure_access_struct-fail.rs` -> `closure_access_struct.rs` - remove `show/closure_access_struct-fail.main.expected` - remove this case from `PROVE_RS_SHOW_SPECS` --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 8 +++++++- ...ss_struct-fail.rs => closure_access_struct.rs} | 0 .../show/closure_access_struct-fail.main.expected | 15 --------------- kmir/src/tests/integration/test_integration.py | 1 - 4 files changed, 7 insertions(+), 17 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{closure_access_struct-fail.rs => closure_access_struct.rs} (100%) delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index ece4c9a3f..05df79d37 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -581,16 +581,22 @@ Therefore a heuristics is used here: // or the closure ref type pointee is missing from the type table andBool isRefType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) andBool isTy(pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))) - andBool lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + andBool ( + lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty) ==K typeInfoVoidType + orBool isFunType(lookupTy({pointeeTy(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)))}:>Ty)) + ) [priority(45), preserves-definedness] syntax Bool ::= isTupleType ( TypeInfo ) [function, total] | isRefType ( TypeInfo ) [function, total] + | isFunType ( TypeInfo ) [function, total] // ------------------------------------------------------- rule isTupleType(typeInfoTupleType(_, _)) => true rule isTupleType( _ ) => false [owise] rule isRefType(typeInfoRefType(_)) => true rule isRefType( _ ) => false [owise] + rule isFunType(typeInfoFunType(_)) => true + rule isFunType( _ ) => false [owise] syntax KItem ::= #setTupleArgs ( Int , Value ) | #setTupleArgs ( Int , List ) diff --git a/kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs b/kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/closure_access_struct-fail.rs rename to kmir/src/tests/integration/data/prove-rs/closure_access_struct.rs diff --git a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected deleted file mode 100644 index 8a1aff14b..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/closure_access_struct-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (196 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( - span: 125 - - -┌─ 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 8b1def7f8..a5f470208 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -64,7 +64,6 @@ 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', 'and_then_closure-fail', - 'closure_access_struct-fail', ] From 431a484b27fba81f5bdbedb414ce4c1544a67443 Mon Sep 17 00:00:00 2001 From: JianHong Zhao Date: Wed, 4 Mar 2026 17:10:11 +0800 Subject: [PATCH 2/3] fix(decode): accept signed enum tag scalars in _extract_tag (#954) ## Summary - Relax `_extract_tag` to accept both signed and unsigned `PrimitiveInt` tag metadata (`signed=_`). - Keep discriminant decoding based on raw tag bits (`int.from_bytes(..., signed=False)`), which is what variant dispatch needs. - Add a decode fixture for signed-tag metadata (`enum-3-variants-0-fields-signed-tag`). - Update the prove-rs case to a passing case and refresh its `show` snapshot. ## Problem (concrete case) This PR is motivated by: `kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs` ```rust #[repr(i8)] enum AccountState { Uninitialized = 0, Initialized = 1, Frozen = -1, } // main checks both byte-level and signed views of the same discriminant bits: // 255 maps to Frozen in the u8 path // -1 maps to Frozen in the i8 path ``` For this enum layout, the tag scalar metadata can be `signed=true` (I8), even though the stored discriminant bytes are still valid raw bytes for dispatch. ## Red (before this fix) `_extract_tag` only matched `PrimitiveInt(..., signed=False)`. When metadata was signed, decode failed with: ```text ValueError: Unsupported tag: Initialized(value=PrimitiveInt(length=I8, signed=True), ...) ``` That blocked the signed-discriminant path in proving. ## Green (after this fix) - `_extract_tag` now accepts either signedness metadata. - The same bytes are decoded as unsigned raw bits for dispatch. - The concrete program above now proves in integration tests: - input case is now `transmute-u8-to-enum-changed-discriminant-signed.rs` - expected proof snapshot is `show/transmute-u8-to-enum-changed-discriminant-signed.main.expected` - terminal `#EndProgram` is reached for `main` ## Why this is the right scope This change fixes tag extraction compatibility for signed discriminant metadata without changing enum dispatch semantics beyond that path. It is covered by both: - decode-value fixture (`enum-3-variants-0-fields-signed-tag`) and - end-to-end prove-rs integration snapshot for the concrete Rust program above. --------- Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com> --- kmir/src/kmir/decoding.py | 4 +- ...um-3-variants-0-fields-signed-tag.expected | 1 + .../enum-3-variants-0-fields-signed-tag.json | 138 ++++++++++++++++++ ...ged-discriminant-signed-fail.main.expected | 15 -- ...u8-to-enum-changed-discriminant-signed.rs} | 0 .../src/tests/integration/test_integration.py | 1 - 6 files changed, 142 insertions(+), 17 deletions(-) create mode 100644 kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected create mode 100644 kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected rename kmir/src/tests/integration/data/prove-rs/{transmute-u8-to-enum-changed-discriminant-signed-fail.rs => transmute-u8-to-enum-changed-discriminant-signed.rs} (100%) diff --git a/kmir/src/kmir/decoding.py b/kmir/src/kmir/decoding.py index 4d0dc95fb..27a2dc019 100644 --- a/kmir/src/kmir/decoding.py +++ b/kmir/src/kmir/decoding.py @@ -445,10 +445,12 @@ def _extract_tag(*, data: bytes, tag_offset: MachineSize, tag: Scalar) -> tuple[ case Initialized( value=PrimitiveInt( length=length, - signed=False, + signed=_, ), valid_range=_, ): + # Stable MIR enum discriminants are represented against the raw tag bits. + # Use unsigned decoding even when the scalar metadata marks the tag as signed. tag_data = data[tag_offset.in_bytes : tag_offset.in_bytes + length.value] tag_value = int.from_bytes(tag_data, byteorder='little', signed=False) return tag_value, length diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected new file mode 100644 index 000000000..8916e2b4d --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.expected @@ -0,0 +1 @@ +Aggregate ( variantIdx ( 1 ) , .List ) diff --git a/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json new file mode 100644 index 000000000..3696e0d04 --- /dev/null +++ b/kmir/src/tests/integration/data/decode-value/enum-3-variants-0-fields-signed-tag.json @@ -0,0 +1,138 @@ +{ + "bytes": [ + 0 + ], + "types": [], + "typeInfo": { + "EnumType": { + "name": "OrderingLike", + "adt_def": 72, + "discriminants": [ + 255, + 0, + 1 + ], + "fields": [ + [], + [], + [] + ], + "layout": { + "fields": { + "Arbitrary": { + "offsets": [ + { + "num_bits": 0 + } + ] + } + }, + "variants": { + "Multiple": { + "tag": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + }, + "tag_encoding": "Direct", + "tag_field": 0, + "variants": [ + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 0 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 1 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + }, + { + "fields": { + "Arbitrary": { + "offsets": [] + } + }, + "variants": { + "Single": { + "index": 2 + } + }, + "abi": { + "Aggregate": { + "sized": true + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + ] + } + }, + "abi": { + "Scalar": { + "Initialized": { + "value": { + "Int": { + "length": "I8", + "signed": true + } + }, + "valid_range": { + "start": 255, + "end": 1 + } + } + } + }, + "abi_align": 1, + "size": { + "num_bits": 8 + } + } + } + } +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected deleted file mode 100644 index ce7aaeddb..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (102 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , thunk ( #decodeConstant ( constantKindAllo - span: 153 - - -┌─ 2 (root, leaf, target, terminal) -│ #EndProgram ~> .K - - diff --git a/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs b/kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed-fail.rs rename to kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum-changed-discriminant-signed.rs diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py index a5f470208..0de9ce097 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -54,7 +54,6 @@ 'assume-cheatcode-conflict-fail', 'raw-ptr-cast-fail', 'transmute-u8-to-enum-fail', - 'transmute-u8-to-enum-changed-discriminant-signed-fail', 'assert-inhabited-fail', 'iterator-simple', 'unions-fail', From 7258cfb4f2d29cbdcb739edb94ce201a95319570 Mon Sep 17 00:00:00 2001 From: Daniel Cumming <124537596+dkcumming@users.noreply.github.com> Date: Wed, 4 Mar 2026 23:58:46 +1000 Subject: [PATCH 3/3] Added check for `FunType` in `setupCalleeClosure` (#969) #956 added handles `FunType` for closures instead of `VoidType` for that come from [stable mir json 129](https://github.com/runtimeverification/stable-mir-json/pull/129) for `setupCalleeClosure2`. This PR adds the same thing to `setupCalleeClosure`. (Fixes regressed proofs for P-Token) - Added explicit `FnOnce` test `closure_fnonce_tuple_arg.rs` - Fixed `and_then_closure.rs` --- kmir/src/kmir/kdist/mir-semantics/kmir.md | 6 ++++-- .../two-crate-bin/crate2::main.expected | 2 +- ...d_then_closure-fail.rs => and_then_closure.rs} | 0 .../data/prove-rs/closure_fnonce_tuple_arg.rs | 8 ++++++++ .../show/and_then_closure-fail.main.expected | 15 --------------- kmir/src/tests/integration/test_integration.py | 1 - 6 files changed, 13 insertions(+), 19 deletions(-) rename kmir/src/tests/integration/data/prove-rs/{and_then_closure-fail.rs => and_then_closure.rs} (100%) create mode 100644 kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs delete mode 100644 kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md index 05df79d37..5a2b48c65 100644 --- a/kmir/src/kmir/kdist/mir-semantics/kmir.md +++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md @@ -548,8 +548,10 @@ Therefore a heuristics is used here: andBool isTypedValue(LOCALS[TUPLE]) andBool isTupleType(lookupTy(tyOfLocal({LOCALS[TUPLE]}:>TypedLocal))) andBool isTypedLocal(LOCALS[CLOSURE]) - andBool typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) - // either the closure ref type is missing from type table + andBool ( + typeInfoVoidType ==K lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal)) + orBool isFunType(lookupTy(tyOfLocal({LOCALS[CLOSURE]}:>TypedLocal))) + ) [priority(40), preserves-definedness] rule [setupCalleeClosure2]: #setUpCalleeData( diff --git a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected index 60dbf8403..544958705 100644 --- a/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected +++ b/kmir/src/tests/integration/data/crate-tests/two-crate-bin/crate2::main.expected @@ -2,7 +2,7 @@ ┌─ 1 (root, init) │ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC │ -│ (740 steps) +│ (737 steps) ├─ 3 (terminal) │ #EndProgram ~> .K │ diff --git a/kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs b/kmir/src/tests/integration/data/prove-rs/and_then_closure.rs similarity index 100% rename from kmir/src/tests/integration/data/prove-rs/and_then_closure-fail.rs rename to kmir/src/tests/integration/data/prove-rs/and_then_closure.rs diff --git a/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs new file mode 100644 index 000000000..18cfb9c22 --- /dev/null +++ b/kmir/src/tests/integration/data/prove-rs/closure_fnonce_tuple_arg.rs @@ -0,0 +1,8 @@ +fn apply u8>(f: F, a: u8, b: u8) -> u8 { + f(a, b) +} + +fn main() { + let result = apply(|x, y| x + y, 10, 32); + assert_eq!(result, 42); +} diff --git a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected deleted file mode 100644 index a6b62b249..000000000 --- a/kmir/src/tests/integration/data/prove-rs/show/and_then_closure-fail.main.expected +++ /dev/null @@ -1,15 +0,0 @@ - -┌─ 1 (root, init) -│ #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC -│ span: 0 -│ -│ (142 steps) -└─ 3 (stuck, leaf) - #traverseProjection ( toLocal ( 2 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( - span: 157 - - -┌─ 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 0de9ce097..5f36b155d 100644 --- a/kmir/src/tests/integration/test_integration.py +++ b/kmir/src/tests/integration/test_integration.py @@ -62,7 +62,6 @@ 'test_offset_from-fail', 'ref-ptr-cast-elem-fail', 'ref-ptr-cast-elem-offset-fail', - 'and_then_closure-fail', ]