feat: support roundtrip pointer <> int cast

Author: Stevengre

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

@@ -10,6 +10,7 @@ requires "./types.md"
 requires "./value.md"
 requires "./numbers.md"
 requires "./decoding.md"
+requires "./pointer-int.md"
 
 module RT-DATA
   imports INT
@@ -27,6 +28,7 @@ module RT-DATA
   imports RT-NUMBERS
   imports RT-DECODING
   imports RT-TYPES
+  imports RT-POINTER-INT
   imports KMIR-CONFIGURATION
 
 ```
@@ -316,7 +318,6 @@ These helpers mark down, as we traverse the projection, what `Place` we are curr
                    | 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)
 
-  syntax ProjectionElem ::= PointerOffset( Int, Int ) // Same as subslice but coming from BinopOffset injected by us
 
   syntax Contexts ::= List{Context, ""}
 
@@ -1456,28 +1457,6 @@ What can be supported without additional layout consideration is trivial casts b
       requires lookupTy(TY_SOURCE) ==K lookupTy(TY_TARGET)
 ```
 
-Transmuting a pointer to an integer discards provenance and reinterprets the pointer’s offset as a value of the target integer type.
-
-```k
-  // `prove-rs/interior-mut3.rs` needs this
-  // TODO: check its correctness, I assume the pointer offset is the address here and we can use it to recover the PtrLocal
-  rule <k> #cast(
-              PtrLocal(_, _, _, metadata(_, PTR_OFFSET, _)),
-              castKindTransmute,
-              _TY_SOURCE,
-              TY_TARGET
-            )
-          =>
-            #intAsType(
-              PTR_OFFSET,
-              #bitWidth(#numTypeOf(lookupTy(TY_TARGET))),
-              #numTypeOf(lookupTy(TY_TARGET))
-            )
-          ...
-        </k>
-      requires #isIntType(lookupTy(TY_TARGET))
-```
-
 Other `Transmute` casts that can be resolved are round-trip casts from type A to type B and then directly back from B to A.
 The first cast is reified as a `thunk`, the second one resolves it and eliminates the `thunk`:
 
@@ -1582,17 +1561,57 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
   rule #staticArrayLenBits(_OTHER) => 0 [owise]
 ```
 
-A transmutation from an integer to an enum is wellformed if:
-- The bit width of the incoming integer is the same as the discriminant type of the enum
-    (e.g. `u8 -> i8` fine, `u8 -> u16` not fine) - this is guaranteed by the compiler;
-- The incoming integer has a bit pattern that matches a discriminant of the enum
-    (e.g. `255_u8` and `-1_i8` fine iff `0b1111_1111` is a discriminant of the enum);
-
-Note that discriminants are stored as `u128` in the type data even if they are signed
-or unsigned at the source level. This means that our approach to soundly transmute an
-integer into a enum is to treat the incoming integer as unsigned (converting if signed),
-and check if the value is in the discriminants. If yes, find the corresponding variant
-index; if not, return `#UBErrorInvalidDiscriminantsInEnumCast`.
+Transmuting a pointer to an integer uses the helpers defined in `RT-POINTER-INT` to encode the entire pointer (stack depth, place, mutability, and metadata) into a single natural number; decoding applies the inverse helpers. The encoding must fit into the target integer bit-width, otherwise the transmute is stuck.
+
+```k
+  syntax Value ::= #ptrWithOffset ( Value , Int , TypeInfo ) [function, total]
+  rule #ptrWithOffset(PtrLocal(STACK, PLACE, MUT, metadata(SIZE, _, ORIGIN)), OFFSET, TYINFO)
+    => PtrLocal(STACK, PLACE, MUT, #convertMetadata(metadata(SIZE, OFFSET, ORIGIN), TYINFO))
+  rule #ptrWithOffset(VAL:Value, _, _) => VAL [owise]
+
+  rule <k> #cast(
+              PtrLocal(_, _, _, _) #as PTR,
+              castKindTransmute,
+              TY_SOURCE,
+              TY_TARGET
+            )
+          =>
+            #intAsType(
+              #encodePtrInt(PTR, pointeeTy(lookupTy(TY_SOURCE))),
+              #bitWidth(#numTypeOf(lookupTy(TY_TARGET))),
+              #numTypeOf(lookupTy(TY_TARGET))
+            )
+          ...
+        </k>
+      requires #isIntType(lookupTy(TY_TARGET))
+       andBool #fitsInWidth(
+                 #encodePtrInt(PTR, pointeeTy(lookupTy(TY_SOURCE))),
+                 #bitWidth(#numTypeOf(lookupTy(TY_TARGET)))
+               )
+
+  rule <k> #cast(
+              Integer(VAL, WIDTH, SIGNED) #as _INT,
+              castKindTransmute,
+              TY_SOURCE,
+              TY_TARGET
+            )
+          =>
+            #ptrWithOffset(
+              #decodePtrBase(#cantorUnpairLeft(#unsignedFromIntValue(VAL, WIDTH, SIGNED))),
+              #bytesToPtrOffset(
+                #cantorUnpairRight(#unsignedFromIntValue(VAL, WIDTH, SIGNED)),
+                pointeeTy(lookupTy(TY_TARGET))
+              ),
+              lookupTy(TY_TARGET)
+            )
+          ...
+        </k>
+      requires #isIntType(lookupTy(TY_SOURCE))
+```
+
+Another specialisation is getting the discriminant of `enum`s without fields after converting some integer data to it
+(see `#discriminant` and `rvalueDiscriminant`).
+If none of the `enum` variants has any fields, the `Transmute` of a number to the `enum` data is necessarily just the discriminant itself., and can be returned as the integer value afgter adjusting to the byte length of the discriminant:
 
 ```k
   syntax Bool ::= #isEnumWithoutFields ( TypeInfo ) [function, total]