diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/data.md b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
index a25d7a2c2..7f69eef37 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/data.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/data.md
@@ -327,6 +327,7 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
                    | CtxIndex( List , Int ) // array index constant or has been read before
                    | CtxSubslice( List , Int , Int ) // start and end always counted from beginning
                    | CtxPointerOffset( List, Int, Int ) // pointer offset for accessing elements with an offset (Offset, Origin Length)
+                   | "CtxWrapStruct" // special context adding a singleton Aggregate(0, _) around a value
 
   syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us
 
@@ -361,6 +362,11 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
     requires size(INNER) ==Int END -Int START // ensures updateList is defined
      [preserves-definedness] // START,END indexes checked before, length check for update here
 
+  // removing a struct wrapper added by a WrapStruct projection
+  rule #buildUpdate(Aggregate(variantIdx(0), ListItem(VALUE) .List), CtxWrapStruct CTXS)
+    => #buildUpdate(VALUE, CTXS)
+
+
   syntax StackFrame ::= #updateStackLocal ( StackFrame, Int, Value ) [function]
 
   rule #updateStackLocal(StackFrame(CALLER, DEST, TARGET, UNWIND, LOCALS), I, VAL)
@@ -371,8 +377,25 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
     [preserves-definedness] // valid list indexing and sort checked
 
   syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total]
+  syntax ProjectionElems ::= appendP ( ProjectionElems , ProjectionElems ) [function, total]
+                           | consP ( ProjectionElem , ProjectionElems ) [function, total]
+  // ----------------------------------------------------------------------------------------
   rule appendP(.ProjectionElems, TAIL) => TAIL
-  rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => X appendP(REST, TAIL)
+  rule appendP(X:ProjectionElem REST:ProjectionElems, TAIL) => consP(X, appendP(REST, TAIL))
+  // default
+  rule consP(      PROJ      ,           .ProjectionElems           ) => PROJ .ProjectionElems
+  rule consP(      PROJ      ,   P:ProjectionElem PS:ProjectionElems) => PROJ (P PS)
+  // high-priority rules to cancel out projection pairs at the head
+  rule consP(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) PS:ProjectionElems) => PS [priority(40)]
+  rule consP(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray PS:ProjectionElems) => PS [priority(40)]
+  rule consP(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) PS:ProjectionElems) => PS [priority(40)]
+  // this rule is not valid if the original pointee has more than one field
+  // rule consP(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct PS:ProjectionElems) => PS [priority(40)]
+  // HACK: special rule which munges together constant-indexing and offset projections 
+  rule consP( projectionElemConstantIndex(I, 0, false), PointerOffset(OFF, _SIZE) PS) => projectionElemConstantIndex(I +Int OFF, 0, false) PS [priority(40)]
+    // requires I +Int OFF < _SIZE // _SIZE is metadataSize, needs a < operation for this to work
+  rule consP(projectionElemToZST, projectionElemFromZST PS:ProjectionElems) => PS [priority(40)]
+  rule consP(projectionElemFromZST, projectionElemToZST PS:ProjectionElems) => PS [priority(40)]
 
   syntax Value ::= #localFromFrame ( StackFrame, Local, Int ) [function]
 
@@ -462,21 +485,19 @@ This is done without consideration of the validity of the Downcast[^downcast].
 ```
 
 In context with pointer casts, the semantics handles the special case of a _transparent wrapper struct_:
-A pointer to a struct containing a single element can be cast to a pointer to the single element itself.
-While the pointer cast tries to insert and remove field projections to the singleton field,
-it is still possible that a field projection occurs on a value which is not an Aggregate (nor a union).
-This necessitates a special rule which allows the semantics to perform a field projection to field 0 as a Noop.
-The situation typically arises when the stored value is a pointer (`NonNull`), therefore the rule is restricted to this case.
-The context is populated with the correct field access data, so that write-backs will correct the stored value to an Aggregate.
+A pointer to a struct containing a single element can be cast to a pointer to the single element itself, and back.
+The special projection used to enable this is `projectionElemWrapStruct`, inserted by the pointer `#cast` operation.
+
+The situation typically arises when the stored value is a pointer (`NonNull`) but the rule is not restricted to this.
 
 ```k
   rule <k> #traverseProjection(
              DEST,
-             PtrLocal(_, _, _, _) #as VALUE,
-             projectionElemField(fieldIdx(0), TY) PROJS,
+             VALUE,
+             projectionElemWrapStruct PROJS,
              CTXTS
            )
-        => #traverseProjection(DEST, VALUE, PROJS, CtxField(variantIdx(0), ListItem(VALUE), 0, TY) CTXTS) ... </k>
+        => #traverseProjection(DEST, Aggregate(variantIdx(0), ListItem(VALUE)), PROJS, CtxWrapStruct CTXTS) ... </k>
     [preserves-definedness, priority(100)]
 ```
 
@@ -1083,16 +1104,41 @@ for _fat_ pointers it is a `usize` value indicating the data length.
 
 [^rawPtrAgg]: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_middle/mir/enum.AggregateKind.html#variant.RawPtr
 
+The data pointer is assumed to point to a single element of an array that was originally present, 
+and an array of the indeicated size gets reconstructed if the provided metadata is a `usize` value
+(potentially removing an indexing operation to get the element).
+
 ```k
-  rule <k> ListItem(PtrLocal(OFFSET, PLACE, _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Integer(LENGTH, 64, false)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
-        => PtrLocal(OFFSET, PLACE, MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE))
+  rule <k> ListItem(PtrLocal(OFFSET, place(LOCAL, PROJS), _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) 
+           ListItem(Integer(LENGTH, 64, false))
+           ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
+        => PtrLocal(OFFSET, place(LOCAL, removeIndexTail(PROJS)), MUT, metadata(dynamicSize(LENGTH), PTR_OFFSET, ORIGIN_SIZE))
         ...
        </k>
+    // requires LENGTH +Int PTR_OFFSET <=Int ORIGIN_SIZE // refuse to create an invalid fat pointer
+    //  andBool dynamicSize(1) ==K #metadataSize(lookupTy(_TY)) // expect a slice type
+    //  andBool hasIndexTail(PROJS) ???
 
   rule <k> ListItem(PtrLocal(OFFSET, PLACE, _, metadata(_SIZE, PTR_OFFSET, ORIGIN_SIZE))) ListItem(Aggregate(_, .List)) ~> #mkAggregate(aggregateKindRawPtr(_TY, MUT))
         => PtrLocal(OFFSET, PLACE, MUT, metadata(noMetadataSize, PTR_OFFSET, ORIGIN_SIZE))
         ...
        </k>
+
+  syntax Bool ::= hasIndexTail ( ProjectionElems ) [function, total]
+  // ---------------------------------------------------------------
+  rule hasIndexTail(           .ProjectionElems                          ) => false
+  rule hasIndexTail(projectionElemConstantIndex(0, _, _) .ProjectionElems) => true
+  rule hasIndexTail(     _OTHER:ProjectionElem           .ProjectionElems) => false [owise]
+  rule hasIndexTail(_:ProjectionElem ((_:ProjectionElem _:ProjectionElems) #as MORE)) => hasIndexTail(MORE)
+
+  // remove ConstantIndex(0, _, _) at the end if present, otherwise identity
+  syntax ProjectionElems ::= removeIndexTail ( ProjectionElems ) [function, total]
+  // ---------------------------------------------------------------
+  rule removeIndexTail(           .ProjectionElems                          ) => .ProjectionElems
+  rule removeIndexTail(projectionElemConstantIndex(0, _, _) .ProjectionElems) => .ProjectionElems
+  rule removeIndexTail(      OTHER:ProjectionElem           .ProjectionElems) => OTHER .ProjectionElems [owise]
+  rule removeIndexTail(FIRST:ProjectionElem ((_:ProjectionElem _:ProjectionElems) #as MORE)) => FIRST removeIndexTail(MORE)
+
 ```
 
 The `Aggregate` type carries a `VariantIdx` to distinguish the different variants for an `enum`.
@@ -1180,6 +1226,7 @@ This eliminates any `Deref` projections from the place, and also resolves `Index
   // rule #projectionsFor(CtxPointerOffset(OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemSubslice(OFFSET, ORIGIN_LENGTH, false) PROJS)
   rule #projectionsFor(CtxPointerOffset( _, OFFSET, ORIGIN_LENGTH) CTXS, PROJS) => #projectionsFor(CTXS, PointerOffset(OFFSET, ORIGIN_LENGTH) PROJS)
   rule #projectionsFor(CtxFieldUnion(F_IDX, _, TY) CTXS, PROJS) => #projectionsFor(CTXS, projectionElemField(F_IDX, TY) PROJS)
+  rule #projectionsFor(  CtxWrapStruct       CTXS, PROJS) => #projectionsFor(CTXS,                 projectionElemWrapStruct PROJS)
 
   // Borrowing a zero-sized local that is still `NewLocal`: initialise it, then reuse the regular rule.
   rule <k> rvalueRef(REGION, KIND, place(local(I), PROJS))
@@ -1376,86 +1423,34 @@ Casts involving `Float` values are currently not implemented.
 | PtrToPtr | Convert between references when representations compatible |
 
 Pointers can be converted from one type to another (`PtrToPtr`) when the representations are compatible.
-The compatibility of types (defined in `rt/types.md`) considers their representations (recursively) in
-the `Value` sort.
+For compatible types, an additional projection is added to the pointer's place projections,
+which transforms the previous pointee type to the new one (computation defined in `rt/types.md`).
+If types are not compatible, no such projection exists and the cast is invalid.
 
 Conversion is especially possible for the case of _Slices_ (of dynamic length) and _Arrays_ (of static length),
 which have the same representation `Value::Range`.
-
-When the cast crosses transparent wrappers (newtypes that just forward field `0` e.g. `struct Wrapper<T>(T)`), the pointer's
-`Place` must be realigned. `#alignTransparentPlace` rewrites the projection list until the source and target
-expose the same inner value:
-- if the source unwraps more than the target, append an explicit `field(0)` so the target still sees that field;
-- if the target unwraps more, strip any redundant tail projections with `#popTransparentTailTo`, leaving the
-  canonical prefix shared by both sides.
+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`.
 
 ```k
-  rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
+  rule <k> #cast(PtrLocal(OFFSET, place(LOCAL, PROJS), MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
           =>
             PtrLocal(
               OFFSET,
-              #alignTransparentPlace(
-                PLACE,
-                #lookupMaybeTy(pointeeTy(lookupTy(TY_SOURCE))),
-                #lookupMaybeTy(pointeeTy(lookupTy(TY_TARGET)))
-              ),
+              place(LOCAL, appendP(PROJS, {#typeProjection(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))}:>ProjectionElems)),
               MUT,
               #convertMetadata(META, lookupTy(TY_TARGET))
             )
           ...
         </k>
-      requires #typesCompatible(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))
+      requires NoProjectionElems =/=K #typeProjection(lookupTy(TY_SOURCE), lookupTy(TY_TARGET))
       [preserves-definedness] // valid map lookups checked
+```
 
-  syntax Place ::= #alignTransparentPlace ( Place , TypeInfo , TypeInfo ) [function, total]
-  syntax ProjectionElems ::= #popTransparentTailTo ( ProjectionElems , TypeInfo ) [function, total]
-
-  rule #alignTransparentPlace(place(LOCAL, PROJS), typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as SOURCE, TARGET)
-    => #alignTransparentPlace(
-         place(
-           LOCAL,
-           appendP(PROJS, projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems)
-         ),
-         lookupTy(FIELD_TY),
-         TARGET
-       )
-    requires #transparentDepth(SOURCE) >Int #transparentDepth(TARGET)
-     andBool #zeroFieldOffset(LAYOUT)
-
-  rule #alignTransparentPlace(
-         place(LOCAL, PROJS),
-         SOURCE,
-         typeInfoStructType(_, _, FIELD_TY .Tys, LAYOUT) #as TARGET
-       )
-    => #alignTransparentPlace(
-         place(LOCAL, #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))),
-         SOURCE,
-         lookupTy(FIELD_TY)
-       )
-    requires #transparentDepth(SOURCE) <Int #transparentDepth(TARGET)
-     andBool #zeroFieldOffset(LAYOUT)
-     andBool PROJS =/=K #popTransparentTailTo(PROJS, lookupTy(FIELD_TY))
-
-  rule #alignTransparentPlace(PLACE, _, _) => PLACE [owise]
-
-  rule #popTransparentTailTo(
-         projectionElemField(fieldIdx(0), FIELD_TY) .ProjectionElems,
-         TARGET
-       )
-    => .ProjectionElems
-    requires lookupTy(FIELD_TY) ==K TARGET
-
-  rule #popTransparentTailTo(
-         X:ProjectionElem REST:ProjectionElems,
-         TARGET
-       )
-    => X #popTransparentTailTo(REST, TARGET)
-    requires REST =/=K .ProjectionElems
-
-  rule #popTransparentTailTo(PROJS, _) => PROJS [owise]
+The pointer's metadata needs to be adapted to the new type.
 
+```k
   syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total]
-  // -------------------------------------------------------------------------------------
 ```
 
 Pointers to slices can be converted to pointers to single elements, _losing_ their metadata.
@@ -1535,17 +1530,17 @@ Specifically, pointers to arrays of statically-known length are cast to pointers
 The original metadata is therefore already stored as `staticSize` to avoid having to look it up here.
 
 ```k
+  rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, metadata(staticSize(SIZE), PTR_OFFSET, ORIGIN_SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET)
+          =>
+            PtrLocal(OFFSET, PLACE, MUT, metadata(dynamicSize(SIZE), PTR_OFFSET, ORIGIN_SIZE))
+          ...
+        </k>
+
   rule <k> #cast(Reference(OFFSET, PLACE, MUT, metadata(staticSize(SIZE), PTR_OFFSET, ORIGIN_SIZE)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET)
           =>
             Reference(OFFSET, PLACE, MUT, metadata(dynamicSize(SIZE), PTR_OFFSET, ORIGIN_SIZE))
           ...
         </k>
-      //   <types> TYPEMAP </types>
-      // could look up the static size here instead of caching it:
-      // requires TY_SOURCE in_keys(TYPEMAP)
-      //  andBool isTypeInfo(TYPEMAP[TY_SOURCE])
-      // andBool notBool hasMetadata(_TY_TARGET, TYPEMAP)
-      // [preserves-definedness] // valid type map indexing and sort coercion
 
   rule <k> #cast(AllocRef(ID, PROJS, metadata(staticSize(SIZE), OFF, ORIG)), castKindPointerCoercion(pointerCoercionUnsize), _TY_SOURCE, _TY_TARGET)
           =>
@@ -2365,7 +2360,7 @@ A trivial case where `binOpOffset` applies an offset of `0` is added with higher
   rule #applyBinOp(
           binOpOffset,
           PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET, dynamicSize(ORIGIN_SIZE)) ),
-          Integer(OFFSET_VAL, _WIDTH, false), // unsigned offset
+          Integer(OFFSET_VAL, _WIDTH, _SIGN), // offset: signed (for stable offset) or unsigned (for get_unchecked)
           _CHECKED)
     =>
           PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, dynamicSize(ORIGIN_SIZE)) )
@@ -2377,7 +2372,7 @@ A trivial case where `binOpOffset` applies an offset of `0` is added with higher
   rule #applyBinOp(
           binOpOffset,
           PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET, staticSize(ORIGIN_SIZE)) ),
-          Integer(OFFSET_VAL, _WIDTH, false), // unsigned offset
+          Integer(OFFSET_VAL, _WIDTH, _SIGN), // offset: signed (for stable offset) or unsigned (for get_unchecked)
           _CHECKED)
     =>
           PtrLocal( STACK_DEPTH , PLACE , MUT, metadata(CURRENT_SIZE, CURRENT_OFFSET +Int OFFSET_VAL, staticSize(ORIGIN_SIZE)) )
diff --git a/kmir/src/kmir/kdist/mir-semantics/rt/types.md b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
index 7374115d1..3998cb3eb 100644
--- a/kmir/src/kmir/kdist/mir-semantics/rt/types.md
+++ b/kmir/src/kmir/kdist/mir-semantics/rt/types.md
@@ -23,71 +23,148 @@ This module contains helper functions to operate on this type information.
 
 ## Compatibility of types (high-level representation)
 
-When two types use the same representation for their values, these
-values, and pointers to them, can be converted from one type to the other.
-The `#typesCompatible` function determines this compatibility, and is by default `false`.
+When two types use the same (low-level) representation for their values, pointers to them can be converted from one type to the other.
+
+For compatible pointer types, the `#typeProjection` function computes a projection that can be appended to the pointer's projection
+to return the correct type when the pointer is cast to a different pointee type.
+Most notably, casting between arrays and single elements as well as casting to and from transparent wrappers.
+This projection computation happens _recursively_, for instance casting from `*const [[T]]` to `*const T`.
+
+The interface function is meant for pointer casts to compute pointee projections and returns nothing for other types.
 
 ```k
-  syntax Bool ::= #typesCompatible ( TypeInfo , TypeInfo ) [function, total]
+  syntax MaybeProjectionElems ::= ProjectionElems
+                                | "NoProjectionElems"
 
-  // by default, only identical types are compatible
-  rule #typesCompatible (             T            ,           T              ) => true  [priority(60)] 
-  rule #typesCompatible (             _            ,           _              ) => false [owise] 
+  syntax MaybeProjectionElems ::= #typeProjection ( TypeInfo , TypeInfo )    [function, total]
+  // ---------------------------------------------------------------------------------------
+  rule #typeProjection ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => #pointeeProjection(lookupTy(TY1), lookupTy(TY2))
+  rule #typeProjection ( _, _ ) => NoProjectionElems [owise]
 ```
 
-Arrays and slices are compatible if their element type is (ignoring length)
+Note that certain projections can cancel each other, such as casting from one transparent wrapper to another.
+In case of casting an element pointer to an array pointer, we rely on this cancellation to recover the array length
+(NB ultimately there needs to be an underlying array if there is more than one element in the original allocation).
+
+This can be done in an extended `append` function for projections, and already in the special cons function here. **TODO**
+
+The `#maybeConsProj` function is a "cons" for projection lists with a short-cut case for when the second argument is not a projection list.
+It also implements cancellation of inverse projections (such as casting from one transparent wrapper to another, or between arrays).
+
 ```k
-  rule #typesCompatible ( typeInfoArrayType(TY1, _), typeInfoArrayType(TY2, _)) => #typesCompatible(lookupTy(TY1), lookupTy(TY2))
+  syntax ProjectionElem ::= "projectionElemSingletonArray" // elem -> array. Incomplete information! (relies on cancellation, or caller must consider metadata)
+                          | "projectionElemWrapStruct"     // transparent wrapper (singleton struct)
+                          | "projectionElemToZST"          // cast to ZST (immaterial data)
+                          | "projectionElemFromZST"        // ...and back from ZST to something material (the two cancel out in sequence)
+
+  syntax MaybeProjectionElems ::= maybeConcatProj ( ProjectionElem, MaybeProjectionElems ) [function, total]
+
+  rule maybeConcatProj(PROJ, REST:ProjectionElems) => PROJ REST
+  rule maybeConcatProj(  _ , NoProjectionElems   ) => NoProjectionElems
+
+  // special cancellation rules with higher priority
+  rule maybeConcatProj(projectionElemSingletonArray, projectionElemConstantIndex(0, 0, false) REST:ProjectionElems) => REST [priority(40)]
+  rule maybeConcatProj(projectionElemConstantIndex(0, 0, false), projectionElemSingletonArray REST:ProjectionElems) => REST [priority(40)]
+
+  rule maybeConcatProj(projectionElemWrapStruct, projectionElemField(fieldIdx(0), _) REST:ProjectionElems) => REST [priority(40)]
+  // this rule would not be valid if the original pointee had more than one field. In the calling context, this won't occur, though.
+  rule maybeConcatProj(projectionElemField(fieldIdx(0), _), projectionElemWrapStruct REST:ProjectionElems) => REST [priority(40)]
+
+  rule maybeConcatProj(projectionElemToZST, projectionElemFromZST REST:ProjectionElems) => REST [priority(40)]
+  rule maybeConcatProj(projectionElemFromZST, projectionElemToZST REST:ProjectionElems) => REST [priority(40)]
 ```
 
-Pointers are compatible if their pointee types are
+The `#pointeeProjection` function computes, for compatible pointee types, how to project from one pointee to the other.
+
 ```k
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #typesCompatible(lookupTy(TY1), lookupTy(TY2))
-     [priority(59)]
+  syntax MaybeProjectionElems ::= #pointeeProjection ( TypeInfo , TypeInfo ) [function, total]
 ```
 
-Pointers to arrays/slices are compatible with pointers to the element type
+A short-cut rule for identical types takes preference.
+As a default, no projection elements are returned for incompatible types.
 ```k
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #isArrayOf(lookupTy(TY1), TY2)
-
-  rule #typesCompatible ( typeInfoPtrType(TY1)     , typeInfoPtrType(TY2)     ) => true
-    requires #isArrayOf(lookupTy(TY2), TY1)
+  rule #pointeeProjection(T , T) => .ProjectionElems  [priority(40)]
+  rule #pointeeProjection(_ , _) => NoProjectionElems [owise]
+```
 
-  syntax Bool ::= #isArrayOf ( TypeInfo , Ty ) [function, total]
+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))
+        )
+```
 
-  rule #isArrayOf(typeInfoArrayType(TY, _), TY) => true
-  rule #isArrayOf(      _                 , _ ) => false [owise]
+Pointers to zero-sized types can be converted from and to. No recursion beyond the ZST.
+**TODO** Problem: our ZSTs have different representation: compare empty arrays and empty structs/unit tuples.
+```k
+  rule #pointeeProjection(SRC, OTHER) => projectionElemToZST   .ProjectionElems
+    requires #zeroSizedType(OTHER) andBool notBool #zeroSizedType(SRC)
+    [priority(45)]
+  rule #pointeeProjection(SRC, OTHER) => projectionElemFromZST .ProjectionElems
+    requires #zeroSizedType(SRC) andBool notBool #zeroSizedType(OTHER)
+    [priority(45)]
 ```
 
 Pointers to structs with a single zero-offset field are compatible with pointers to that field's type
 ```k
-  rule #typesCompatible(SRC, OTHER) => true
-    requires #zeroSizedType(SRC) orBool #zeroSizedType(OTHER)
 
-  rule #typesCompatible(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
-    => #typesCompatible(lookupTy(FIELD), OTHER)
+  rule #pointeeProjection(typeInfoStructType(_, _, FIELD .Tys, LAYOUT), OTHER)
+    => maybeConcatProj(
+          projectionElemField(fieldIdx(0), FIELD),
+          #pointeeProjection(lookupTy(FIELD), OTHER)
+        )
     requires #zeroFieldOffset(LAYOUT)
 
-  rule #typesCompatible(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
-    => #typesCompatible(OTHER, lookupTy(FIELD))
+  rule #pointeeProjection(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+    => maybeConcatProj(
+          projectionElemWrapStruct,
+          #pointeeProjection(OTHER, lookupTy(FIELD))
+        )
     requires #zeroFieldOffset(LAYOUT)
+```
 
-  syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
+Pointers to `MaybeUninit<X>` can be cast to pointers to `X`.
+This is actually a 2-step compatibility:
+The `MaybeUninit<X>` union contains a `ManuallyDrop<X>` (when filled),
+which is a singleton struct (see above).
 
+```k
+  rule #pointeeProjection(MAYBEUNINIT_TYINFO, ELEM_TYINFO)
+    => maybeConcatProj(
+          projectionElemField(fieldIdx(1), {getFieldTy(MAYBEUNINIT_TYINFO, 1)}:>Ty),
+          maybeConcatProj(
+            projectionElemField(fieldIdx(0), {getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)}:>Ty),
+           .ProjectionElems // TODO recursion?
+          )
+        )
+    requires #typeNameIs(MAYBEUNINIT_TYINFO, "std::mem::MaybeUninit<")
+     andBool #lookupMaybeTy(getFieldTy(#lookupMaybeTy(getFieldTy(MAYBEUNINIT_TYINFO, 1)), 0)) ==K ELEM_TYINFO
+```
+
+```k
+  syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
+  // --------------------------------------------------------------------
   rule #zeroFieldOffset(LAYOUT)
-    =>      #layoutOffsets(LAYOUT) ==K .MachineSizes
-     orBool #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
+    =>      #layoutOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
      orBool #layoutOffsets(LAYOUT) ==K machineSize(0) .MachineSizes
 
   // Extract field offsets from the struct layout when available (Arbitrary only).
   syntax MachineSizes ::= #layoutOffsets ( MaybeLayoutShape ) [function, total]
+  // --------------------------------------------------------------------------
   rule #layoutOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
   rule #layoutOffsets(noLayoutShape) => .MachineSizes
   rule #layoutOffsets(_) => .MachineSizes [owise]
 ```
 
+--------------------------------------------------
+
 Helper function to identify an `union` type, this is needed so `#setLocalValue`
 will not create an `Aggregate` instead of a `Union` `Value`.
 ```k
diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state b/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state
index 518b8bfe4..93cab02ec 100644
--- a/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state
+++ b/kmir/src/tests/integration/data/exec-smir/pointers/offset_get_unchecked.state
@@ -35,12 +35,12 @@
       ListItem ( typedValue ( Range ( ListItem ( Integer ( 11 , 32 , true ) )
       ListItem ( Integer ( 22 , 32 , true ) )
       ListItem ( Integer ( 33 , 32 , true ) ) ) , ty ( 38 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: PointerOffset ( 1 , 3 )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 1 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 39 ) , mutabilityMut ) )
       ListItem ( typedValue ( Integer ( 22 , 32 , true ) , ty ( 16 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 35 ) , mutabilityMut ) )
-      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: PointerOffset ( 2 , 3 )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 1 ) , projection: projectionElemConstantIndex (... offset: 2 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 26 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 27 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 39 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 16 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state
index 059a1ae70..691092911 100644
--- a/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state
+++ b/kmir/src/tests/integration/data/exec-smir/pointers/pointer-cast-zst.state
@@ -1,6 +1,6 @@
 <kmir>
   <k>
-    PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 29 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K
+    PtrLocal ( 1 , place (... local: local ( 1 ) , projection: projectionElemToZST  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , noMetadataSize ) ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindAssign (... place: place (... local: local ( 3 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 2 ) , projection: .ProjectionElems ) ) , ty ( 26 ) ) ) , span: span ( 52 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 4 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindPtrToPtr , operandCopy ( place (... local: local ( 3 ) , projection: .ProjectionElems ) ) , ty ( 25 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 5 ) , projection: .ProjectionElems ) , rvalue: rvalueCast ( castKindTransmute , operandCopy ( place (... local: local ( 4 ) , projection: .ProjectionElems ) ) , ty ( 27 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 6 ) , projection: .ProjectionElems ) , rvalue: rvalueNullaryOp ( nullOpAlignOf , ty ( 28 ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 7 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpSub , operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x01\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 9 ) ) ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 8 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpBitAnd , operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) , operandCopy ( place (... local: local ( 7 ) , projection: .ProjectionElems ) ) ) ) , span: span ( 50 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 9 ) , projection: .ProjectionElems ) , rvalue: rvalueBinaryOp ( binOpEq , operandCopy ( place (... local: local ( 8 ) , projection: .ProjectionElems ) ) , operandConstant ( constOperand (... span: span ( 50 ) , userTy: noUserTypeAnnotationIndex , const: mirConst (... kind: constantKindAllocated ( allocation (... bytes: b"\x00\x00\x00\x00\x00\x00\x00\x00" , provenance: provenanceMap (... ptrs: .ProvenanceMapEntries ) , align: align ( 8 ) , mutability: mutabilityMut ) ) , ty: ty ( 27 ) , id: mirConstId ( 10 ) ) ) ) ) ) , span: span ( 50 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: assert (... cond: operandCopy ( place (... local: local ( 9 ) , projection: .ProjectionElems ) ) , expected: true , msg: assertMessageMisalignedPointerDereference (... required: operandCopy ( place (... local: local ( 6 ) , projection: .ProjectionElems ) ) , found: operandCopy ( place (... local: local ( 5 ) , projection: .ProjectionElems ) ) ) , target: basicBlockIdx ( 1 ) , unwind: unwindActionUnreachable ) , span: span ( 50 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
diff --git a/kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs b/kmir/src/tests/integration/data/prove-rs/iterator-simple.rs
similarity index 100%
rename from kmir/src/tests/integration/data/prove-rs/iterator-simple-fail.rs
rename to kmir/src/tests/integration/data/prove-rs/iterator-simple.rs
diff --git a/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs b/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs
new file mode 100644
index 000000000..7d1f60541
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ptr-through-wrapper-fail.rs
@@ -0,0 +1,19 @@
+struct Wrapper<T>(T);
+
+fn main() {
+    let i = 32_i32;
+
+    unsafe {
+        let p_i = &i as *const i32;
+        assert!(32 == *p_i);
+
+        let p_w = p_i as *const Wrapper<i32>;
+        assert!(32 == (*p_w).0);
+
+        let p_ww = p_w as *const Wrapper<Wrapper<i32>>;
+        assert!(32 == (*p_ww).0.0);
+
+        let p_ii = p_ww as *const i32;
+        assert!(32 == *p_ii);
+    }
+}
\ No newline at end of file
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr-offset.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr-offset.rs
new file mode 100644
index 000000000..500424093
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr-offset.rs
@@ -0,0 +1,11 @@
+fn main() {
+    let arr: [i32; 2] = [42, 84];
+    let r_arr = &arr;
+    let p_arr_wide = r_arr as *const [i32; 2];
+    let p_arr_narrow = p_arr_wide as *const [i32; 1];
+    
+    unsafe {
+        let p_arr_narrow_offset = p_arr_narrow.offset(1);
+        assert!(*p_arr_narrow_offset == [84]);
+    }
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr.rs
new file mode 100644
index 000000000..74e559214
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-arr.rs
@@ -0,0 +1,9 @@
+fn main() {
+    let arr: [i32; 1] = [42];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const [i32; 1];
+    
+    unsafe {
+        assert!(*p_arr == [42]);
+    }
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs
new file mode 100644
index 000000000..4f6b94d03
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-fail.rs
@@ -0,0 +1,9 @@
+fn main() {
+    let arr: [i32; 1] = [42];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const i32;
+    
+    unsafe {
+        assert!(*p_arr == 42);
+    }
+}
diff --git a/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs
new file mode 100644
index 000000000..e1cd0c371
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/ref-ptr-cast-elem-offset-fail.rs
@@ -0,0 +1,11 @@
+// ptr-cast-elem-offset-fail.rs
+fn main() {
+    let arr: [i32; 2] = [42, 84];
+    let r_arr = &arr;
+    let p_arr = r_arr as *const i32;
+    
+    unsafe {
+        let p_arr_offset = p_arr.offset(1);
+        assert!(*p_arr_offset == 84);
+    }
+}
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
index 70f8119ac..62a1bb725 100644
--- 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
@@ -3,9 +3,9 @@
 │   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
 │   span: 0
 │
-│  (2000 steps)
+│  (2005 steps)
 └─ 3 (stuck, leaf)
-    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( .List ) , .Projectio
+    #traverseProjection ( toStack ( 1 , local ( 1 ) ) , Range ( ListItem ( Aggregate
     span: 146
 
 
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected
deleted file mode 100644
index f81ff04b5..000000000
--- a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple-fail.main.expected
+++ /dev/null
@@ -1,15 +0,0 @@
-
-┌─ 1 (root, init)
-│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
-│   span: 0
-│
-│  (496 steps)
-└─ 3 (stuck, leaf)
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place ( ..
-    span: 219
-
-
-┌─ 2 (root, leaf, target, terminal)
-│   #EndProgram ~> .K
-
-
diff --git a/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected
new file mode 100644
index 000000000..f1cd9a4d1
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/iterator-simple.main.expected
@@ -0,0 +1,17 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (798 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/ptr-through-wrapper-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected
new file mode 100644
index 000000000..6c000e5b0
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ptr-through-wrapper-fail.main.expected
@@ -0,0 +1,109 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (106 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 ( 12 ) ) ~> .K
+   │   function: main
+   │
+   │  (113 steps)
+   ├─ 7
+   │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+   │   function: main
+   ┃
+   ┃ (1 step)
+   ┣━━┓
+   ┃  │
+   ┃  ├─ 8
+   ┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+   ┃  │   function: main
+   ┃  │
+   ┃  │  (1 step)
+   ┃  └─ 10 (stuck, leaf)
+   ┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+   ┃      function: main
+   ┃
+   ┗━━┓
+      │
+      ├─ 9
+      │   #execBlockIdx ( basicBlockIdx ( 11 ) ) ~> .K
+      │   function: main
+      │
+      │  (115 steps)
+      ├─ 11
+      │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+      │   function: main
+      ┃
+      ┃ (1 step)
+      ┣━━┓
+      ┃  │
+      ┃  ├─ 12
+      ┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+      ┃  │   function: main
+      ┃  │
+      ┃  │  (1 step)
+      ┃  └─ 14 (stuck, leaf)
+      ┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+      ┃      function: main
+      ┃
+      ┗━━┓
+         │
+         ├─ 13
+         │   #execBlockIdx ( basicBlockIdx ( 10 ) ) ~> .K
+         │   function: main
+         │
+         │  (117 steps)
+         ├─ 15
+         │   #expect ( thunk ( #applyBinOp ( binOpEq , thunk ( #applyBinOp ( binOpBitAnd , th
+         │   function: main
+         ┃
+         ┃ (1 step)
+         ┣━━┓
+         ┃  │
+         ┃  ├─ 16
+         ┃  │   AssertError ( assertMessageMisalignedPointerDereference ( ... required: operandC
+         ┃  │   function: main
+         ┃  │
+         ┃  │  (1 step)
+         ┃  └─ 18 (stuck, leaf)
+         ┃      #ProgramError ( AssertError ( assertMessageMisalignedPointerDereference ( ... re
+         ┃      function: main
+         ┃
+         ┗━━┓
+            │
+            ├─ 17
+            │   #execBlockIdx ( basicBlockIdx ( 9 ) ) ~> .K
+            │   function: main
+            │
+            │  (25 steps)
+            ├─ 19 (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/ref-ptr-cast-elem-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected
new file mode 100644
index 000000000..e6f0eec24
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-fail.main.expected
@@ -0,0 +1,40 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (124 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 ( 3 ) ) ~> .K
+   │   function: main
+   │
+   │  (26 steps)
+   ├─ 7 (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/ref-ptr-cast-elem-offset-fail.main.expected b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected
new file mode 100644
index 000000000..2d1468486
--- /dev/null
+++ b/kmir/src/tests/integration/data/prove-rs/show/ref-ptr-cast-elem-offset-fail.main.expected
@@ -0,0 +1,40 @@
+
+┌─ 1 (root, init)
+│   #execTerminator ( terminator ( ... kind: terminatorKindCall ( ... func: operandC
+│   span: 0
+│
+│  (185 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
+   │
+   │  (26 steps)
+   ├─ 7 (terminal)
+   │   #EndProgram ~> .K
+   │   function: main
+   │
+   ┊  constraint: true
+   ┊  subst: ...
+   └─ 2 (leaf, target, terminal)
+       #EndProgram ~> .K
+
+
+
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
index c126e290c..f705c8ff0 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-0.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 207 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 244 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 183 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 111 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 144 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 244 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 183 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 111 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 144 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -100,7 +116,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 207 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
@@ -110,16 +126,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 144 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 71 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 207 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 207 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 207 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
index fdc646b58..d3b225d3b 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-1.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 32 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 130 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 60 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 253 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 230 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 241 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 107 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 130 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 60 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 253 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 230 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 241 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 107 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -98,7 +114,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 32 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 130 , 8 , false ) ) ) ) )
@@ -108,16 +124,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 241 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 107 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 32 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 32 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 32 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
index 7dfa4546e..c911a1108 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-2.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 46 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 184 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 86 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 157 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 128 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 108 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 184 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 86 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 157 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 128 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 108 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -98,7 +114,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 46 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
@@ -108,16 +124,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 128 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 108 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 46 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 46 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
index 0cfc09c47..624d04337 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-3.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 66 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 242 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 33 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 6 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 132 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 119 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 242 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 33 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 6 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 132 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 119 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -98,7 +114,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 66 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
@@ -108,16 +124,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 132 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 119 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 66 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 66 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 66 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
index 14875958d..3bf3a15cf 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-4.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 155 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 52 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 202 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 245 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 79 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 34 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 52 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 202 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 245 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 79 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 34 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -98,7 +114,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 155 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 52 , 8 , false ) ) ) ) )
@@ -108,16 +124,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 46 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 34 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 10 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 155 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 155 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 155 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
index 7e66ae902..646f5447f 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-5.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 238 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 127 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 26 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 80 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 57 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 190 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 127 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 26 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 80 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 57 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 190 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -101,7 +117,7 @@
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
     ListItem ( Moved ) ) , ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 238 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 127 , 8 , false ) ) ) ) )
@@ -111,16 +127,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 190 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 238 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 238 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 238 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
index 69928af3e..eda995444 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-6.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 18 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 0 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 74 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 191 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 163 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 139 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 0 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 74 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 240 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 191 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 163 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 139 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -101,7 +117,7 @@
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
     ListItem ( Moved ) ) , ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 18 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 0 , 8 , false ) ) ) ) )
@@ -111,16 +127,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 163 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 11 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 139 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 18 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 18 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 18 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
index c5b2a5756..a7096c2c3 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-8.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 189 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 192 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 64 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 98 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 22 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 70 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 192 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 64 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 98 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 22 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 70 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -98,7 +114,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 189 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 192 , 8 , false ) ) ) ) )
@@ -108,16 +124,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 43 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 70 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 126 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 189 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 189 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 189 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
index 8bd77c00a..c6eb4c360 100644
--- a/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
+++ b/kmir/src/tests/integration/data/run-smir-random/complex-types/final-9.expected
@@ -1,6 +1,22 @@
 <kmir>
   <k>
-    #traverseProjection ( toLocal ( 24 ) , thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , projectionElemDeref  .ProjectionElems , .Contexts ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
+    #traverseProjection ( toStack ( 1 , local ( 30 ) ) , Integer ( 95 , 8 , false ) , PointerOffset ( 1 , 0 )  .ProjectionElems , CtxField ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) , 0 , ty ( 23 ) )  CtxFieldUnion ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 74 ) )  CtxIndex ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 173 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 237 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 171 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 20 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) ) , 0 )  CtxField ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 173 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 237 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 41 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 171 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 20 , 8 , false ) ) ) ) )
+    ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) ) ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
+    ListItem ( Integer ( 8 , 64 , false ) ) ) ) , 0 , ty ( 11 ) )  .Contexts ) ~> #derefTruncate ( noMetadataSize , .ProjectionElems ) ~> #readProjection ( false ) ~> #freezer#setLocalValue(_,_)_RT-DATA_KItem_Place_Evaluation1_ ( place (... local: local ( 15 ) , projection: .ProjectionElems ) ~> .K ) ~> #execStmts ( statement (... kind: statementKindStorageDead ( local ( 24 ) ) , span: span ( 299 ) )  statement (... kind: statementKindStorageDead ( local ( 17 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 16 ) ) , span: span ( 277 ) )  statement (... kind: statementKindStorageDead ( local ( 25 ) ) , span: span ( 300 ) )  statement (... kind: statementKindAssign (... place: place (... local: local ( 0 ) , projection: .ProjectionElems ) , rvalue: rvalueAggregate ( aggregateKindAdt ( adtDef ( 15 ) , variantIdx ( 1 ) , genericArgKindType ( ty ( 23 ) )  .GenericArgs , noUserTypeAnnotationIndex , noFieldIdx ) , operandMove ( place (... local: local ( 15 ) , projection: .ProjectionElems ) )  .Operands ) ) , span: span ( 301 ) )  statement (... kind: statementKindStorageDead ( local ( 15 ) ) , span: span ( 295 ) )  .Statements ) ~> #execTerminator ( terminator (... kind: terminatorKindGoto (... target: basicBlockIdx ( 5 ) ) , span: span ( 295 ) ) ) ~> .K
   </k>
   <retVal>
     noReturn
@@ -47,17 +63,17 @@
       ListItem ( typedValue ( Moved , ty ( 3 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
+      ListItem ( typedValue ( Integer ( 1 , 64 , false ) , ty ( 3 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 50 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( dynamicSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 15 ) , mutabilityMut ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
       ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
-      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , ty ( 53 ) , mutabilityNot ) )
       ListItem ( newLocal ( ty ( 2 ) , mutabilityNot ) )
-      ListItem ( typedValue ( thunk ( #cast ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 0 , dynamicSize ( 8 ) ) ) , castKindPtrToPtr , ty ( 53 ) , ty ( 54 ) ) ) , ty ( 54 ) , mutabilityMut ) )
+      ListItem ( typedValue ( PtrLocal ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  projectionElemConstantIndex (... offset: 0 , minLength: 0 , fromEnd: false )  projectionElemField ( fieldIdx ( 1 ) , ty ( 74 ) )  projectionElemField ( fieldIdx ( 0 ) , ty ( 23 ) )  .ProjectionElems ) , mutabilityNot , metadata ( noMetadataSize , 1 , noMetadataSize ) ) , ty ( 54 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
       ListItem ( typedValue ( Reference ( 1 , place (... local: local ( 30 ) , projection: projectionElemField ( fieldIdx ( 0 ) , ty ( 11 ) )  .ProjectionElems ) , mutabilityNot , metadata ( staticSize ( 8 ) , 0 , noMetadataSize ) ) , ty ( 57 ) , mutabilityMut ) )
     </locals>
@@ -100,7 +116,7 @@
     ListItem ( newLocal ( ty ( 23 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 72 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
-    ListItem ( typedValue ( Integer ( 0 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 95 , 64 , false ) , ty ( 6 ) , mutabilityMut ) )
     ListItem ( typedValue ( Moved , ty ( 24 ) , mutabilityMut ) )
     ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Range ( ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 3 , 8 , false ) ) ) ) )
@@ -110,16 +126,17 @@
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 171 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 20 , 8 , false ) ) ) ) )
     ListItem ( Union ( fieldIdx ( 1 ) , Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 194 , 8 , false ) ) ) ) ) ) )
-    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 1 , 64 , false ) )
+    ListItem ( Aggregate ( variantIdx ( 0 ) , ListItem ( Integer ( 2 , 64 , false ) )
     ListItem ( Integer ( 8 , 64 , false ) ) ) ) ) , ty ( 24 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 55 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 1 ) , ListItem ( Integer ( 95 , 8 , false ) ) ) , ty ( 55 ) , mutabilityMut ) )
     ListItem ( typedValue ( Reference ( 0 , place (... local: local ( 30 ) , projection: .ProjectionElems ) , mutabilityMut , metadata ( noMetadataSize , 0 , noMetadataSize ) ) , ty ( 10 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 69 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 23 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityNot ) )
-    ListItem ( newLocal ( ty ( 7 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 4 ) , mutabilityMut ) )
-    ListItem ( newLocal ( ty ( 6 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 69 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Integer ( 95 , 8 , false ) , ty ( 23 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Integer ( 95 , 64 , false ) , ty ( 6 ) , mutabilityNot ) )
+    ListItem ( typedValue ( Aggregate ( variantIdx ( 0 ) , ListItem ( Moved )
+    ListItem ( Moved ) ) , ty ( 7 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 4 ) , mutabilityMut ) )
+    ListItem ( typedValue ( Moved , ty ( 6 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 5 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 28 ) , mutabilityMut ) )
     ListItem ( newLocal ( ty ( 31 ) , mutabilityMut ) )
diff --git a/kmir/src/tests/integration/test_integration.py b/kmir/src/tests/integration/test_integration.py
index f3e172edd..6cff124fb 100644
--- a/kmir/src/tests/integration/test_integration.py
+++ b/kmir/src/tests/integration/test_integration.py
@@ -56,11 +56,14 @@
     'transmute-u8-to-enum-fail',
     'transmute-u8-to-enum-changed-discriminant-signed-fail',
     'assert-inhabited-fail',
-    'iterator-simple-fail',
+    'iterator-simple',
     'unions-fail',
     'transmute-maybe-uninit-fail',
+    'ptr-through-wrapper-fail',
     'iter_next_2-fail',
     'test_offset_from-fail',
+    'ref-ptr-cast-elem-fail',
+    'ref-ptr-cast-elem-offset-fail',
 ]