runtimeverification · mariaKt · Mar 4, 2026 · Mar 4, 2026 · Mar 4, 2026 · Mar 4, 2026
diff --git 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/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]: <k> #setUpCalleeData(
@@ -581,16 +583,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/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/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
@@ -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
@@ -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/...on/data/prove-rs/and_then_closure-fail.rs → ...gration/data/prove-rs/and_then_closure.rs b/...on/data/prove-rs/and_then_closure-fail.rs → ...gration/data/prove-rs/and_then_closure.rs
diff --git a/...ta/prove-rs/closure_access_struct-fail.rs → ...on/data/prove-rs/closure_access_struct.rs b/...ta/prove-rs/closure_access_struct-fail.rs → ...on/data/prove-rs/closure_access_struct.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
@@ -0,0 +1,8 @@
+fn apply<F: FnOnce(u8, u8) -> 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
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
diff --git a/...on/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected b/...on/data/prove-rs/show/transmute-u8-to-enum-changed-discriminant-signed-fail.main.expected
diff --git a/...-enum-changed-discriminant-signed-fail.rs → ...u8-to-enum-changed-discriminant-signed.rs b/...-enum-changed-discriminant-signed-fail.rs → ...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
@@ -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',
@@ -63,8 +62,6 @@
     'test_offset_from-fail',
     'ref-ptr-cast-elem-fail',
     'ref-ptr-cast-elem-offset-fail',
-    'and_then_closure-fail',
-    'closure_access_struct-fail',
 ]