fix(rt): align transparent pointer casts

Author: Stevengre

kmir/src/kmir/kdist/mir-semantics/rt/data.md

@@ -1262,15 +1262,78 @@ the `Value` sort.
 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 (for example newtypes that just forward field `0`), 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.
+
 ```k
   rule <k> #cast(PtrLocal(OFFSET, PLACE, MUT, META), castKindPtrToPtr, TY_SOURCE, TY_TARGET)
           =>
-            PtrLocal(OFFSET, PLACE, MUT, #convertMetadata(META, lookupTy(TY_TARGET)))
+            PtrLocal(
+              OFFSET,
+              #alignTransparentPlace(
+                PLACE,
+                #lookupMaybeTy(pointeeTy(lookupTy(TY_SOURCE))),
+                #lookupMaybeTy(pointeeTy(lookupTy(TY_TARGET)))
+              ),
+              MUT,
+              #convertMetadata(META, lookupTy(TY_TARGET))
+            )
           ...
         </k>
       requires #typesCompatible(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]
+
   syntax Metadata ::= #convertMetadata ( Metadata , TypeInfo ) [function, total]
   // -------------------------------------------------------------------------------------
 ```

kmir/src/kmir/kdist/mir-semantics/rt/types.md

@@ -61,6 +61,32 @@ Pointers to arrays/slices are compatible with pointers to the element type
   rule #isArrayOf(      _                 , _ ) => false [owise]
 ```
 
+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)
+    requires #zeroFieldOffset(LAYOUT)
+
+  rule #typesCompatible(OTHER, typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+    => #typesCompatible(OTHER, lookupTy(FIELD))
+    requires #zeroFieldOffset(LAYOUT)
+
+  syntax Bool ::= #zeroFieldOffset ( MaybeLayoutShape ) [function, total]
+
+  rule #zeroFieldOffset(LAYOUT)
+    =>      #structOffsets(LAYOUT) ==K .MachineSizes
+     orBool #structOffsets(LAYOUT) ==K machineSize(mirInt(0)) .MachineSizes
+     orBool #structOffsets(LAYOUT) ==K machineSize(0) .MachineSizes
+
+  syntax MachineSizes ::= #structOffsets ( MaybeLayoutShape ) [function, total]
+
+  rule #structOffsets(someLayoutShape(layoutShape(fieldsShapeArbitrary(mk(OFFSETS)), _, _, _, _))) => OFFSETS
+  rule #structOffsets(_) => .MachineSizes [owise]
+```
+
 ## Determining types of places with projection
 
 A helper function `getTyOf` traverses type metadata (using the type metadata map `Ty -> TypeInfo`) along the applied projections to determine the `Ty` of the projected place.
@@ -70,6 +96,24 @@ To make this function total, an optional `MaybeTy` is used.
   syntax MaybeTy ::= Ty
                    | "TyUnknown"
 
+  syntax MaybeTy ::= #transparentFieldTy ( TypeInfo ) [function, total]
+
+  rule #transparentFieldTy(typeInfoStructType(_, _, FIELD .Tys, LAYOUT)) => FIELD
+    requires #zeroFieldOffset(LAYOUT)
+  rule #transparentFieldTy(_) => TyUnknown [owise]
+
+  syntax Int ::= #transparentDepth ( TypeInfo ) [function, total]
+
+  rule #transparentDepth(typeInfoStructType(_, _, FIELD .Tys, LAYOUT))
+    => 1 +Int #transparentDepth(lookupTy(FIELD))
+    requires #zeroFieldOffset(LAYOUT)
+  rule #transparentDepth(_) => 0 [owise]
+
+  syntax TypeInfo ::= #lookupMaybeTy ( MaybeTy ) [function, total]
+
+  rule #lookupMaybeTy(TY:Ty) => lookupTy(TY)
+  rule #lookupMaybeTy(TyUnknown) => typeInfoVoidType
+
   syntax MaybeTy ::= getTyOf( MaybeTy , ProjectionElems ) [function, total]
   // -----------------------------------------------------------
   rule getTyOf(TyUnknown,             _                      ) => TyUnknown