diff --git a/kmir/src/kmir/kdist/mir-semantics/kmir.md b/kmir/src/kmir/kdist/mir-semantics/kmir.md
index 305bf7718..c80f91a76 100644
--- a/kmir/src/kmir/kdist/mir-semantics/kmir.md
+++ b/kmir/src/kmir/kdist/mir-semantics/kmir.md
@@ -565,7 +565,8 @@ Therefore a heuristics is used here:
                 _SPAN
               )
          =>
-           #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
+           #setLocalValue(place(local(1), .ProjectionElems), #incrementRef(getValue(LOCALS, CLOSURE)))
+        ~> #setTupleArgs(2, getValue(LOCALS, TUPLE)) ~> #execBlock(FIRST)
           // arguments are tuple components, stored as _2 .. _n
          ...
        </k>
@@ -609,6 +610,11 @@ Therefore a heuristics is used here:
   // unpack tuple and set arguments individually
   rule <k> #setTupleArgs(IDX, Aggregate(variantIdx(0), ARGS)) => #setTupleArgs(IDX, ARGS) ... </k>
 
+  rule <k> #setTupleArgs(IDX, VAL:Value)
+        => #setTupleArgs(IDX, ListItem(VAL))
+        ...
+       </k> [owise]
+
   rule <k> #setTupleArgs(_, .List ) => .K ... </k>
 
   rule <k> #setTupleArgs(IDX, ListItem(VAL) REST:List)
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index 840ae6095..f76620160 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -1051,6 +1051,12 @@ Literal arrays are also built using this RValue.
         ...
        </k>
 
+  rule <k> ARGS:List ~> #mkAggregate(aggregateKindClosure(_DEF, _TY_ARGS))
+        =>
+            Aggregate(variantIdx(0), ARGS)
+        ...
+       </k>
+
 
   // #readOperands accumulates a list of `TypedLocal` values from operands
   syntax KItem ::= #readOperands ( Operands )
@@ -1434,6 +1440,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>(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 <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
+          => PtrLocal(OFFSET, PLACE, MUT, META)
+          ...
+        </k>
+      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 <k> #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
           =>
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
index 0ac8cff08..98b522012 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/decoding.md
@@ -297,27 +297,26 @@ If there are no fields, the enum can be decoded by using their data as the discr
    requires TAG =/=Int DISCRIMINANT
 ```
 
-#### Enums with two variants
+#### Enums with direct tag encoding and fields
 
-Having two variants with possibly zero or one field each is a very common case,
-it includes a number of standard library types such as `Option` and `Result`.
-
-The following rules are specialised to the case of encoding an `Option`.
-An important distinction here is whether or not the tag is niche-encoded.
-If the option holds data that has all-zero as a possible value, a separate tag is used, usually as the first field.
-In both cases we expect the tag to be in the single shared field, and the discriminant to be just 0 and 1.
+Decodes any enum with `tagEncodingDirect` and a `primitiveInt` tag,
+with arbitrary variant counts, discriminant values, and field counts per variant.
+The tag is read as an unsigned little-endian integer, matched against the discriminant
+list to find the variant index, and then the variant's fields are decoded using the
+per-variant layout offsets.
 
 ```k
+  // General entry rule: direct-tag enum with at least one field somewhere.
   rule #decodeValue(
          BYTES
        , typeInfoEnumType(...
            name: _
          , adtDef: _
-         , discriminants: discriminant(0) discriminant(1) .Discriminants
-         , fields: (.Tys : (FIELD_TYPE .Tys) : .Tyss)
+         , discriminants: DISCRIMINANTS
+         , fields: FIELD_TYPESS
          , layout:
             someLayoutShape(layoutShape(...
-                fields: fieldsShapeArbitrary(mk(... offsets: machineSize(0) .MachineSizes))
+                fields: _FIELDS
               , variants:
                   variantsShapeMultiple(
                     mk(...
@@ -329,7 +328,7 @@ In both cases we expect the tag to be in the single shared field, and the discri
                         )
                       , tagEncoding: tagEncodingDirect
                       , tagField: 0
-                      , variants: _VARIANTS
+                      , variants: VARIANT_LAYOUTS
                       )
                     )
               , abi: _ABI
@@ -338,22 +337,59 @@ In both cases we expect the tag to be in the single shared field, and the discri
             ))
          ) #as ENUM_TYPE
        )
-    => #decodeOptionTag01(BYTES, TAG_WIDTH, FIELD_TYPE, ENUM_TYPE)
-
-  syntax Evaluation ::= #decodeOptionTag01 ( Bytes , IntegerLength , Ty , TypeInfo ) [function, total]
-  // --------------------------------------------------------------------------------------
-  rule #decodeOptionTag01(BYTES, _LEN, _TY, _ENUM_TYPE)
-    => Aggregate(variantIdx(0), .List)
-    requires 0 ==Int BYTES[0] // expect only 0 or 1 as tags, so higher bytes do not matter
-    [preserves-definedness]
-  rule #decodeOptionTag01(BYTES,  LEN,  TY, _ENUM_TYPE)
-    => Aggregate(variantIdx(1), ListItem(#decodeValue(substrBytes(BYTES, #byteLength(LEN), lengthBytes(BYTES)), lookupTy(TY))))
-    requires 1 ==Int BYTES[0] // expect only 0 or 1 as tags, so higher bytes do not matter
+    => #decodeEnumDirectFields(
+         BYTES,
+         #findVariantIdx(#decodeEnumDirectTag(BYTES, TAG_WIDTH), DISCRIMINANTS),
+         FIELD_TYPESS,
+         VARIANT_LAYOUTS,
+         ENUM_TYPE
+       )
+    requires notBool #noFields(FIELD_TYPESS)
+
+  // ---------------------------------------------------------------------------
+  // #decodeEnumDirectFields: given the variant index, decode its fields
+  // ---------------------------------------------------------------------------
+  syntax Evaluation ::= #decodeEnumDirectFields ( Bytes , VariantIdx , Tyss , LayoutShapes , TypeInfo ) [function, total]
+  // --------------------------------------------------------------------------------------------------------------------------
+  rule #decodeEnumDirectFields(BYTES, variantIdx(IDX), FIELD_TYPESS, VARIANT_LAYOUTS, _ENUM_TYPE)
+    => Aggregate(
+         variantIdx(IDX),
+         #decodeFieldsWithOffsets(BYTES, #nthTys(FIELD_TYPESS, IDX), #nthVariantOffsets(VARIANT_LAYOUTS, IDX))
+       )
+    requires 0 <=Int IDX
     [preserves-definedness]
-  rule #decodeOptionTag01(BYTES, _LEN, _TY,  ENUM_TYPE)
+
+  // Error cases: variant not found or other failure
+  rule #decodeEnumDirectFields(BYTES, _, _FIELD_TYPESS, _VARIANT_LAYOUTS, ENUM_TYPE)
     => UnableToDecode(BYTES, ENUM_TYPE)
     [owise]
 
+  // ---------------------------------------------------------------------------
+  // #decodeEnumDirectTag: read the tag bytes as an unsigned little-endian int
+  // ---------------------------------------------------------------------------
+  syntax Int ::= #decodeEnumDirectTag ( Bytes , IntegerLength ) [function, total]
+  rule #decodeEnumDirectTag(BYTES, TAG_WIDTH)
+    => Bytes2Int(substrBytes(BYTES, 0, #byteLength(TAG_WIDTH)), LE, Unsigned)
+    requires lengthBytes(BYTES) >=Int #byteLength(TAG_WIDTH)
+    [preserves-definedness]
+  rule #decodeEnumDirectTag(_, _) => -1 [owise]
+
+  // ---------------------------------------------------------------------------
+  // List-indexing helpers
+  // ---------------------------------------------------------------------------
+
+  // Index into a Tyss (list of per-variant field type lists)
+  syntax Tys ::= #nthTys ( Tyss , Int ) [function, total]
+  rule #nthTys(TYS : _REST, 0) => TYS
+  rule #nthTys(_TYS : REST, N) => #nthTys(REST, N -Int 1) requires N >Int 0
+  rule #nthTys(_, _) => .Tys [owise]
+
+  // Index into variant layouts and extract field offsets in one step (total)
+  syntax MachineSizes ::= #nthVariantOffsets ( LayoutShapes , Int ) [function, total]
+  rule #nthVariantOffsets(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _) _REST, 0) => OFFSETS
+  rule #nthVariantOffsets(_L REST, N) => #nthVariantOffsets(REST, N -Int 1) requires N >Int 0
+  rule #nthVariantOffsets(_, _) => .MachineSizes [owise]
+
   syntax Int ::= #byteLength ( IntegerLength ) [function, total]
   // -----------------------------------------------------------
   rule #byteLength(integerLengthI8  ) => 1
diff --git a/kmir/src/kmir/kompile.py b/kmir/src/kmir/kompile.py
index 67878e05e..c48fef906 100644
--- a/kmir/src/kmir/kompile.py
+++ b/kmir/src/kmir/kompile.py
@@ -521,13 +521,25 @@ def _functions(kmir: KMIR, smir_info: SMIRInfo) -> dict[int, KInner]:
         for ty in smir_info.function_symbols_reverse[item_name]:
             functions[ty] = parsed_item_kinner.args[1]
 
-    # Add intrinsic functions
+    # Add intrinsic functions and linked normal symbols that have no local body in `items`.
+    # Normal symbols must still map to `monoItemFn(..., noBody)` instead of falling back to UNKNOWN FUNCTION.
     for ty, sym in smir_info.function_symbols.items():
-        if 'IntrinsicSym' in sym and ty not in functions:
+        if ty in functions:
+            continue
+        if 'IntrinsicSym' in sym:
             functions[ty] = KApply(
                 'IntrinsicFunction',
                 [KApply('symbol(_)_LIB_Symbol_String', [stringToken(sym['IntrinsicSym'])])],
             )
+        elif isinstance(sym.get('NormalSym'), str):
+            functions[ty] = KApply(
+                'MonoItemKind::MonoItemFn',
+                (
+                    KApply('symbol(_)_LIB_Symbol_String', (stringToken(sym['NormalSym']),)),
+                    KApply('defId(_)_BODY_DefId_Int', (intToken(ty),)),
+                    KApply('noBody_BODY_MaybeBody', ()),
+                ),
+            )
 
     return functions
 
diff --git a/kmir/src/kmir/testing/fixtures.py b/kmir/src/kmir/testing/fixtures.py
index 4ade1e06d..d42bf606d 100644
--- a/kmir/src/kmir/testing/fixtures.py
+++ b/kmir/src/kmir/testing/fixtures.py
@@ -1,5 +1,7 @@
 from __future__ import annotations
 
+import re
+import sys
 from difflib import unified_diff
 from typing import TYPE_CHECKING
 
@@ -13,24 +15,36 @@
 
     from pytest import FixtureRequest, Parser
 
-import sys
-
 
 def pytest_configure(config) -> None:
     sys.setrecursionlimit(1000000)
 
 
+def _normalize_symbol_hashes(text: str) -> str:
+    """Normalize rustc symbol hash suffixes that drift across builds/environments."""
+    # Normalize mangled symbol hashes, including generic names with `$` and `.`.
+    # Keep trailing `E` when present; truncated variants may omit it.
+    text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+E', r'\1<hash>E', text)
+    text = re.sub(r'(_ZN[0-9A-Za-z_$.]+17h)[0-9a-fA-F]+', r'\1<hash>', text)
+    # Normalize demangled hash suffixes (`...::h<hex>`).
+    text = re.sub(r'(::h)[0-9a-fA-F]{8,}', r'\1<hash>', text)
+    return text
+
+
 def assert_or_update_show_output(
     actual_text: str, expected_file: Path, *, update: bool, path_replacements: dict[str, str] | None = None
 ) -> None:
     if path_replacements:
         for old, new in path_replacements.items():
             actual_text = actual_text.replace(old, new)
+    # Normalize rustc symbol hash suffixes that can drift across builds/environments.
+    actual_text = _normalize_symbol_hashes(actual_text)
     if update:
         expected_file.write_text(actual_text)
     else:
         assert expected_file.is_file()
         expected_text = expected_file.read_text()
+        expected_text = _normalize_symbol_hashes(expected_text)
         if actual_text != expected_text:
             diff = '\n'.join(
                 unified_diff(
diff --git a/kmir/src/kmir/utils.py b/kmir/src/kmir/utils.py
index 935d37656..8feb00ca5 100644
--- a/kmir/src/kmir/utils.py
+++ b/kmir/src/kmir/utils.py
@@ -288,8 +288,8 @@ def _extract_alloc_id(operands: KInner) -> int | None:
             return None
 
 
-def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
-    """If the k cell is `#setUpCalleeData` for `** UNKNOWN FUNCTION **`, return annotation lines with decoded info."""
+def _annotate_nobody_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]:
+    """If the k cell is `#setUpCalleeData` for a `noBody` callee, return annotation lines with decoded info."""
 
     from .alloc import Allocation, AllocId, AllocInfo, Memory
     from .linker import _demangle
@@ -307,16 +307,14 @@ def _annotate_unknown_function(k_cell: KInner, smir_info: SMIRInfo) -> list[str]
                     KApply(
                         label=KLabel(name='MonoItemKind::MonoItemFn'),
                         args=[
-                            KApply(args=[KToken(token=symbol_name)]),
+                            KApply(args=[KToken()]),
                             KApply(label=KLabel(name='defId(_)_BODY_DefId_Int'), args=[KToken(token=def_id_str)]),
                             _,
                         ],
                     ),
                     operands,
                     KApply(label=KLabel(name='span'), args=[KToken(token=span_str)]),
-                ] if (
-                    symbol_name == '\"** UNKNOWN FUNCTION **\"'
-                ):
+                ]:
                     def_id = int(def_id_str)
                     span = int(span_str)
                 case _:
@@ -379,7 +377,7 @@ def render_leaf_k_cells(proof: APRProof, cterm_show: CTermShow, smir_info: SMIRI
             lines.extend(f'  {k_line}' for k_line in k_lines)
 
         if smir_info is not None and k_cell is not None:
-            annotations = _annotate_unknown_function(k_cell, smir_info)
+            annotations = _annotate_nobody_function(k_cell, smir_info)
             lines.extend(annotations)
 
         if idx != len(leaves) - 1:
diff --git a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected
index 36e7fa6a7..3cb67eec2 100644
--- a/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected
+++ b/kmir/src/tests/integration/data/crate-tests/single-lib/small_test_lib::testing::test_add_in_range.expected
@@ -16,7 +16,7 @@
 ┃  │
 ┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
-┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN3std7process4exit17h<hash>
 ┃
 ┗━━┓ subst: .Subst
    ┃ constraint:
diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json
index 88db28bbd..3058a6679 100644
--- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json
+++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols.expected.json
@@ -1,69 +1,69 @@
 {
   "-6": {
-    "NormalSym": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hb524060ed0e83bbbE"
+    "NormalSym": "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h<hash>E"
   },
   "-5": {
-    "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E"
+    "NormalSym": "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17h<hash>E"
   },
   "-4": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h<hash>E"
   },
   "-3": {
-    "NormalSym": "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h3a8781eea2f9ddb7E"
+    "NormalSym": "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h<hash>E"
   },
   "-2": {
-    "NormalSym": "_ZN3std2rt10lang_start17h17250425291430deE"
+    "NormalSym": "_ZN3std2rt10lang_start17h<hash>E"
   },
   "-1": {
-    "NormalSym": "_ZN8blackbox4main17h56268fefa1135d9eE"
+    "NormalSym": "_ZN8blackbox4main17h<hash>E"
   },
   "0": {
-    "NormalSym": "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E"
+    "NormalSym": "_ZN3std2rt19lang_start_internal17h<hash>E"
   },
   "13": {
-    "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE"
+    "NormalSym": "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h<hash>E"
   },
   "14": {
-    "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h8eaae5c69aab66e9E"
+    "NormalSym": "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h<hash>E"
   },
   "19": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h<hash>E"
   },
   "20": {
     "IntrinsicSym": "black_box"
   },
   "21": {
-    "NormalSym": "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h99c61f0bde9a2afdE"
+    "NormalSym": "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "27": {
-    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E"
+    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "28": {
-    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE"
+    "NormalSym": "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "29": {
-    "NormalSym": "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E"
+    "NormalSym": "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17h<hash>E"
   },
   "30": {
-    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E"
+    "NormalSym": "_ZN4core3ops8function6FnOnce9call_once17h<hash>E"
   },
   "32": {
-    "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E"
+    "NormalSym": "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h<hash>E"
   },
   "35": {
     "IntrinsicSym": "black_box"
   },
   "36": {
-    "NormalSym": "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E"
+    "NormalSym": "_ZN4core9panicking19assert_failed_inner17h<hash>E"
   },
   "43": {
-    "NormalSym": "_ZN8blackbox7add_one17h19d5f3b41fdf13daE"
+    "NormalSym": "_ZN8blackbox7add_one17h<hash>E"
   },
   "44": {
-    "NormalSym": "_ZN4core4hint9black_box17h0bfc654765aa2ddfE"
+    "NormalSym": "_ZN4core4hint9black_box17h<hash>E"
   },
   "45": {
-    "NormalSym": "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE"
+    "NormalSym": "_ZN4core9panicking13assert_failed17h<hash>E"
   },
   "48": {
     "NoOpSym": ""
diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json
index 4fcfd0647..05755f54f 100644
--- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json
+++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_function_symbols_reverse.expected.json
@@ -1,62 +1,62 @@
 {
-  "_ZN3std2rt10lang_start17h17250425291430deE": [
+  "_ZN3std2rt10lang_start17h<hash>E": [
     -2
   ],
-  "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h5c121846c1652782E": [
+  "_ZN3std2rt10lang_start28_$u7b$$u7b$closure$u7d$$u7d$17h<hash>E": [
     32
   ],
-  "_ZN3std2rt19lang_start_internal17h018b8394ba015d86E": [
+  "_ZN3std2rt19lang_start_internal17h<hash>E": [
     0
   ],
-  "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h3ac302c9481e885fE": [
+  "_ZN3std3sys9backtrace28__rust_begin_short_backtrace17h<hash>E": [
     13
   ],
-  "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h3a8781eea2f9ddb7E": [
+  "_ZN42_$LT$$RF$T$u20$as$u20$core..fmt..Debug$GT$3fmt17h<hash>E": [
     -3
   ],
-  "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17hec74c53b91325b16E": [
+  "_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     29
   ],
-  "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h99c61f0bde9a2afdE": [
+  "_ZN4core3fmt3num50_$LT$impl$u20$core..fmt..Debug$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     21
   ],
-  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E": [
+  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     27
   ],
-  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h7baa47f3e5cbe44cE": [
+  "_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h<hash>E": [
     28
   ],
-  "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h526a5c5d4d9d3202E": [
+  "_ZN4core3ops8function6FnOnce40call_once$u7b$$u7b$vtable.shim$u7d$$u7d$17h<hash>E": [
     -4
   ],
-  "_ZN4core3ops8function6FnOnce9call_once17h2d8e0aae13049ae8E": [
+  "_ZN4core3ops8function6FnOnce9call_once17h<hash>E": [
     30
   ],
-  "_ZN4core3ops8function6FnOnce9call_once17haae505bd39892fd2E": [
+  "_ZN4core3ops8function6FnOnce9call_once17h<hash>E": [
     19
   ],
-  "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17hb92e31f0aaa3d322E": [
+  "_ZN4core3ptr28drop_in_place$LT$$RF$u32$GT$17h<hash>E": [
     -5
   ],
-  "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17hb524060ed0e83bbbE": [
+  "_ZN4core3ptr85drop_in_place$LT$std..rt..lang_start$LT$$LP$$RP$$GT$..$u7b$$u7b$closure$u7d$$u7d$$GT$17h<hash>E": [
     -6
   ],
-  "_ZN4core4hint9black_box17h0bfc654765aa2ddfE": [
+  "_ZN4core4hint9black_box17h<hash>E": [
     44
   ],
-  "_ZN4core9panicking13assert_failed17h9acd0d94a91ca0eaE": [
+  "_ZN4core9panicking13assert_failed17h<hash>E": [
     45
   ],
-  "_ZN4core9panicking19assert_failed_inner17h1d286061ca0adfe7E": [
+  "_ZN4core9panicking19assert_failed_inner17h<hash>E": [
     36
   ],
-  "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h8eaae5c69aab66e9E": [
+  "_ZN54_$LT$$LP$$RP$$u20$as$u20$std..process..Termination$GT$6report17h<hash>E": [
     14
   ],
-  "_ZN8blackbox4main17h56268fefa1135d9eE": [
+  "_ZN8blackbox4main17h<hash>E": [
     -1
   ],
-  "_ZN8blackbox7add_one17h19d5f3b41fdf13daE": [
+  "_ZN8blackbox7add_one17h<hash>E": [
     43
   ],
   "black_box": [
diff --git a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json
index 8c767e34e..029619a88 100644
--- a/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json
+++ b/kmir/src/tests/integration/data/exec-smir/intrinsic/blackbox_functions.expected.json
@@ -13569,6 +13569,69 @@
     "node": "KApply",
     "variable": false
   },
+  "0": {
+    "args": [
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "String",
+              "node": "KSort"
+            },
+            "token": "\"_ZN3std2rt19lang_start_internal17h<hash>E\""
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "symbol(_)_LIB_Symbol_String",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "Int",
+              "node": "KSort"
+            },
+            "token": "0"
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "defId(_)_BODY_DefId_Int",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [],
+        "arity": 0,
+        "label": {
+          "name": "noBody_BODY_MaybeBody",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      }
+    ],
+    "arity": 3,
+    "label": {
+      "name": "MonoItemKind::MonoItemFn",
+      "node": "KLabel",
+      "params": []
+    },
+    "node": "KApply",
+    "variable": false
+  },
   "13": {
     "args": [
       {
@@ -22521,6 +22584,195 @@
     "node": "KApply",
     "variable": false
   },
+  "27": {
+    "args": [
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "String",
+              "node": "KSort"
+            },
+            "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E\""
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "symbol(_)_LIB_Symbol_String",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "Int",
+              "node": "KSort"
+            },
+            "token": "27"
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "defId(_)_BODY_DefId_Int",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [],
+        "arity": 0,
+        "label": {
+          "name": "noBody_BODY_MaybeBody",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      }
+    ],
+    "arity": 3,
+    "label": {
+      "name": "MonoItemKind::MonoItemFn",
+      "node": "KLabel",
+      "params": []
+    },
+    "node": "KApply",
+    "variable": false
+  },
+  "28": {
+    "args": [
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "String",
+              "node": "KSort"
+            },
+            "token": "\"_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..UpperHex$u20$for$u20$u32$GT$3fmt17h<hash>E\""
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "symbol(_)_LIB_Symbol_String",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "Int",
+              "node": "KSort"
+            },
+            "token": "28"
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "defId(_)_BODY_DefId_Int",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [],
+        "arity": 0,
+        "label": {
+          "name": "noBody_BODY_MaybeBody",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      }
+    ],
+    "arity": 3,
+    "label": {
+      "name": "MonoItemKind::MonoItemFn",
+      "node": "KLabel",
+      "params": []
+    },
+    "node": "KApply",
+    "variable": false
+  },
+  "29": {
+    "args": [
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "String",
+              "node": "KSort"
+            },
+            "token": "\"_ZN4core3fmt3num3imp52_$LT$impl$u20$core..fmt..Display$u20$for$u20$u32$GT$3fmt17h<hash>E\""
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "symbol(_)_LIB_Symbol_String",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "Int",
+              "node": "KSort"
+            },
+            "token": "29"
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "defId(_)_BODY_DefId_Int",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [],
+        "arity": 0,
+        "label": {
+          "name": "noBody_BODY_MaybeBody",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      }
+    ],
+    "arity": 3,
+    "label": {
+      "name": "MonoItemKind::MonoItemFn",
+      "node": "KLabel",
+      "params": []
+    },
+    "node": "KApply",
+    "variable": false
+  },
   "30": {
     "args": [
       {
@@ -27986,6 +28238,69 @@
     "node": "KApply",
     "variable": false
   },
+  "36": {
+    "args": [
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "String",
+              "node": "KSort"
+            },
+            "token": "\"_ZN4core9panicking19assert_failed_inner17h<hash>E\""
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "symbol(_)_LIB_Symbol_String",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [
+          {
+            "node": "KToken",
+            "sort": {
+              "name": "Int",
+              "node": "KSort"
+            },
+            "token": "36"
+          }
+        ],
+        "arity": 1,
+        "label": {
+          "name": "defId(_)_BODY_DefId_Int",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      },
+      {
+        "args": [],
+        "arity": 0,
+        "label": {
+          "name": "noBody_BODY_MaybeBody",
+          "node": "KLabel",
+          "params": []
+        },
+        "node": "KApply",
+        "variable": false
+      }
+    ],
+    "arity": 3,
+    "label": {
+      "name": "MonoItemKind::MonoItemFn",
+      "node": "KLabel",
+      "params": []
+    },
+    "node": "KApply",
+    "variable": false
+  },
   "43": {
     "args": [
       {
diff --git a/kmir/src/tests/integration/data/prove-rs/closure-staged.rs b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs
new file mode 100644
index 000000000..98e256256
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/closure-staged.rs
@@ -0,0 +1,11 @@
+fn apply<F: FnOnce(u8) -> u8>(f: F, v: u8) -> u8 {
+    f(v)
+}
+
+fn main() {
+    let delta: u8 = 1u8;
+    let _captured = |x: u8| x + delta;
+
+    let f = |x: u8| x + 1u8;
+    assert_eq!(apply(f, 41u8), 42u8);
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs b/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs
new file mode 100644
index 000000000..30eef03d1
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/enum-direct-tag-decode.rs
@@ -0,0 +1,72 @@
+/// Comprehensive test for direct-tag enum decoding.
+///
+/// Covers:
+///   - `#[repr(u8)]` with discriminants 0/1 (baseline, like Option)
+///   - `#[repr(u8)]` with discriminants 2/5 (non-zero start)
+///   - `#[repr(u16)]` with discriminants 0/256 (wide tag exceeding u8 range)
+///   - `#[repr(u8)]` with 3 variants (beyond two-variant restriction)
+
+// --- Baseline: repr(u8), disc 0 / 1 -------------------------------------------
+
+#[repr(u8)]
+enum TwoU8 {
+    A(bool) = 0,
+    B(bool) = 1,
+}
+
+const TWO_U8_A: TwoU8 = TwoU8::A(true);
+const TWO_U8_B: TwoU8 = TwoU8::B(false);
+
+// --- Non-zero discriminants: repr(u8), disc 2 / 5 -----------------------------
+
+#[repr(u8)]
+enum NonZero {
+    X(bool) = 2,
+    Y(bool) = 5,
+}
+
+const NZ_X: NonZero = NonZero::X(false);
+const NZ_Y: NonZero = NonZero::Y(true);
+
+// --- Wide tag: repr(u16), disc 0 / 256 ----------------------------------------
+
+#[repr(u16)]
+enum WideTag {
+    Lo(bool) = 0,
+    Hi(bool) = 256,
+}
+
+const WIDE_LO: WideTag = WideTag::Lo(true);
+const WIDE_HI: WideTag = WideTag::Hi(false);
+
+// --- Three variants: repr(u8), disc 0 / 1 / 2 ---------------------------------
+
+#[repr(u8)]
+enum Three {
+    First(bool)  = 0,
+    Second(bool) = 1,
+    Third(bool)  = 2,
+}
+
+const THREE_A: Three = Three::First(true);
+const THREE_B: Three = Three::Second(false);
+const THREE_C: Three = Three::Third(true);
+
+fn main() {
+    // Baseline
+    assert!(matches!(TWO_U8_A, TwoU8::A(true)));
+    assert!(matches!(TWO_U8_B, TwoU8::B(false)));
+
+    // Non-zero discriminants
+    assert!(matches!(NZ_X, NonZero::X(false)));
+    assert!(matches!(NZ_Y, NonZero::Y(true)));
+
+    // Wide tag
+    assert!(matches!(WIDE_LO, WideTag::Lo(true)));
+    assert!(matches!(WIDE_HI, WideTag::Hi(false)));
+
+    // Three variants
+    assert!(matches!(THREE_A, Three::First(true)));
+    assert!(matches!(THREE_B, Three::Second(false)));
+    assert!(matches!(THREE_C, Three::Third(true)));
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate.rs b/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate.rs
new file mode 100644
index 000000000..75e7c1b9e
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter-eq-copied-take-dereftruncate.rs
@@ -0,0 +1,32 @@
+fn main() {
+    let _keep: fn() -> bool = repro;
+}
+
+#[inline(never)]
+#[no_mangle]
+pub fn repro() -> bool {
+    let k0 = Pubkey([1; 32]);
+    let k1 = Pubkey([2; 32]);
+    let k2 = Pubkey([3; 32]);
+    let n = 2usize;
+
+    let accounts = [
+        AccountInfo { key: &k0 },
+        AccountInfo { key: &k1 },
+        AccountInfo { key: &k2 },
+    ];
+    let signers = [k1, k2, k0];
+
+    accounts[1..]
+        .iter()
+        .map(|signer| *signer.key)
+        .eq(signers.iter().take(n).copied())
+}
+
+#[derive(Clone)]
+struct AccountInfo<'a> {
+    key: &'a Pubkey,
+}
+
+#[derive(Clone, Copy, Debug, PartialEq, Eq)]
+struct Pubkey([u8; 32]);
diff --git a/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs b/kmir/src/tests/integration/data/prove-rs/iter_next_3.rs
new file mode 100644
index 000000000..260b11cae
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/iter_next_3.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/assume-cheatcode-conflict-fail.check_assume_conflict.expected b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected
index 700446f6e..470f41c25 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/assume-cheatcode-conflict-fail.check_assume_conflict.expected
@@ -5,7 +5,7 @@
 │
 │  (61 steps)
 └─ 3 (stuck, leaf)
-    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
     span: 32
 
 
diff --git a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
index 44581b4f2..4c165cf72 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/interior-mut-fail.main.expected
@@ -5,7 +5,7 @@
 │
 │  (877 steps)
 └─ 3 (stuck, leaf)
-    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core4cell22panic_already
     span: 32
 
 
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/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
index 1a3c758c5..9198552ba 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/pointer-cast-length-test-fail.array_cast_test.expected
@@ -17,7 +17,7 @@
 ┃  │
 ┃  │  (6 steps)
 ┃  └─ 6 (stuck, leaf)
-┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
 ┃      span: 32
 ┃
 ┗━━┓ subst: .Subst
diff --git a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected
index 378034e6e..645835cf8 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/spl-multisig-iter-eq-copied-next-fail.repro.expected
@@ -3,10 +3,10 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (1077 steps)
+│  (1837 steps)
 └─ 3 (stuck, leaf)
-    ListItem ( thunk ( #decodeConstant ( constantKindZeroSized , ty ( 89 ) , typeInf
-    span: 274
+    #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandM
+    span: 149
 
 
 ┌─ 2 (root, leaf, target, terminal)
diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected
index 84737597a..e4e10b74c 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.cli-stats-leaves.expected
@@ -5,7 +5,7 @@
 │
 │  (566 steps)
 └─ 3 (stuck, leaf)
-    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
     span: no-location:0
 
 
@@ -32,7 +32,7 @@ Leaf paths from init:
 LEAF <k> CELLS
 ---------------
 Node 3:
-  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands , span ( 117 ) ) ~> .K
-  >> function: core::panicking::panic::h941160ead03e2d54
+  #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>E" ) , id: defId ( 38 ) , body: noBody ) , operandConstant ( constOperand ( ... span: span ( 32 ) , userTy: noUserTypeAnnotationIndex , const: mirConst ( ... kind: constantKindAllocated ( allocation ( ... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00\x17\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap ( ... ptrs: provenanceMapEntry ( ... offset: 0 , allocId: allocId ( 1 ) )  .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 39 ) , id: mirConstId ( 25 ) ) ) )  .Operands , span ( 117 ) ) ~> .K
+  >> function: core::panicking::panic::h<hash>
   >> call span: <REPO>/kmir/src/tests/integration/data/prove-rs/symbolic-args-fail.rs:53:5
   >> message: 'assertion failed: false'
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected
index ef7740af7..e5b630195 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-args-fail.main.expected
@@ -5,7 +5,7 @@
 │
 │  (566 steps)
 └─ 3 (stuck, leaf)
-    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+    #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
     span: 32
 
 
diff --git a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected
index a3abc238d..673eb0193 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/symbolic-structs-fail.eats_struct_args.expected
@@ -29,7 +29,7 @@
 ┃  ┃  │
 ┃  ┃  │  (6 steps)
 ┃  ┃  └─ 10 (stuck, leaf)
-┃  ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+┃  ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
 ┃  ┃      span: 32
 ┃  ┃
 ┃  ┗━━┓ subst: .Subst
diff --git a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected
index a0ac24cae..8fd816dd8 100644
--- a/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected
+++ b/kmir/src/tests/integration/data/prove-rs/show/test_offset_from-fail.testing.expected
@@ -114,7 +114,7 @@
             ┃  │
             ┃  │  (70 steps)
             ┃  └─ 22 (stuck, leaf)
-            ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "** UNKNOWN FUNCTION **" ) ,
+            ┃      #setUpCalleeData ( monoItemFn ( ... name: symbol ( "_ZN4core9panicking5panic17h<hash>
             ┃      span: 32
             ┃
             ┗━━┓ subst: .Subst
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index 101f9141e..d9ddc37ae 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -38,6 +38,7 @@
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
     'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
     'test_offset_from-fail': ['testing'],
+    'iter-eq-copied-take-dereftruncate': ['repro'],
     'spl-multisig-iter-eq-copied-next-fail': ['repro'],
     'spl-multisig-signer-index': ['repro'],
 }
@@ -45,6 +46,7 @@
     'local-raw-fail',
     'interior-mut-fail',
     'interior-mut3-fail',
+    'iter_next_3',
     'assert_eq_exp',
     'bitwise-not-shift',
     'symbolic-args-fail',
diff --git a/kmir/src/tests/unit/test_fixtures.py b/kmir/src/tests/unit/test_fixtures.py
new file mode 100644
index 000000000..b9a3de5b5
--- /dev/null
+++ b/kmir/src/tests/unit/test_fixtures.py
@@ -0,0 +1,27 @@
+from __future__ import annotations
+
+import pytest
+
+from kmir.testing.fixtures import _normalize_symbol_hashes
+
+
+@pytest.mark.parametrize(
+    ('raw', 'expected'),
+    [
+        (
+            '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8E',
+            '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>E',
+        ),
+        (
+            '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17hb987357f13dc6cc8',
+            '_ZN4core3fmt3num53_$LT$impl$u20$core..fmt..LowerHex$u20$for$u20$u32$GT$3fmt17h<hash>',
+        ),
+        (
+            'core::panicking::panic::h941160ead03e2d54',
+            'core::panicking::panic::h<hash>',
+        ),
+    ],
+    ids=['generic-mangled-full', 'generic-mangled-truncated', 'demangled'],
+)
+def test_normalize_symbol_hashes(raw: str, expected: str) -> None:
+    assert _normalize_symbol_hashes(raw) == expected