Update feature/ptoken with master (#849)

- #811
- #847 
- #846 
- #840
- #839

Author: jberthold

deps/k_release

@@ -1 +1 @@
-7.1.301
+7.1.304

deps/pyproject-build-systems

@@ -1 +1 @@
-dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5
+795a980d25301e5133eca37adae37283ec3c8e66

deps/uv2nix

@@ -1 +1 @@
-b6ed0901aec29583532abe65117b18d86a49b617
+c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c

deps/uv_release

@@ -1 +1 @@
-0.9.2
+0.9.9

flake.lock

@@ -12,13 +12,13 @@
       inputs.flake-utils.follows = "flake-utils";
     };
 
-    k-framework.url = "github:runtimeverification/k/v7.1.301";
+    k-framework.url = "github:runtimeverification/k/v7.1.304";
     k-framework = {
       inputs.flake-utils.follows = "flake-utils";
       inputs.nixpkgs.follows = "nixpkgs";
     };
 
-    uv2nix.url = "github:pyproject-nix/uv2nix/b6ed0901aec29583532abe65117b18d86a49b617";
+    uv2nix.url = "github:pyproject-nix/uv2nix/c8cf711802cb00b2e05d5c54d3486fce7bfc8f7c";
     # uv2nix requires a newer version of nixpkgs
     # therefore, we pin uv2nix specifically to a newer version of nixpkgs
     # until we replaced our stale version of nixpkgs with an upstream one as well
@@ -27,7 +27,7 @@
     nixpkgs-unstable.url = "github:NixOS/nixpkgs/nixos-unstable";
     uv2nix.inputs.nixpkgs.follows = "nixpkgs-unstable";
     # uv2nix.inputs.nixpkgs.follows = "nixpkgs";
-    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/dbfc0483b5952c6b86e36f8b3afeb9dde30ea4b5";
+    pyproject-build-systems.url = "github:pyproject-nix/build-system-pkgs/795a980d25301e5133eca37adae37283ec3c8e66";
     pyproject-build-systems = {
       inputs.nixpkgs.follows = "uv2nix/nixpkgs";
       inputs.uv2nix.follows = "uv2nix";

flake.nix

@@ -8,7 +8,7 @@ version = "0.3.181"
 description = ""
 requires-python = ">=3.10"
 dependencies = [
-    "kframework==v7.1.301",
+    "kframework==v7.1.304",
     "rust-demangler==1.0",
 ]
 

kmir/pyproject.toml

@@ -1265,15 +1265,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 (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.
+
 ```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]
   // -------------------------------------------------------------------------------------
 ```
@@ -1497,23 +1560,58 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
   rule #staticArrayLenBits(_OTHER) => 0 [owise]
 ```
 
-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:
+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);
 
-```k
-  rule <k> #discriminant(
-              thunk(#cast (Integer(DATA, _, false), castKindTransmute, _, TY)),
-              TY
-            ) => Integer(DATA, 0, false) // HACK: bit width 0 means "flexible"
-          ...
-        </k>
-    requires #isEnumWithoutFields(lookupTy(TY))
+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`.
 
+```k
   syntax Bool ::= #isEnumWithoutFields ( TypeInfo ) [function, total]
   // ----------------------------------------------------------------
   rule #isEnumWithoutFields(typeInfoEnumType(_, _, _, FIELDSS, _)) => #noFields(FIELDSS)
   rule #isEnumWithoutFields(_OTHER) => false [owise]
+
+  // TODO: Connect this with MirError
+  syntax Evaulation ::= "#UBErrorInvalidDiscriminantsInEnumCast"
+  rule <k>
+           #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO ) ~> _REST
+        =>
+           #UBErrorInvalidDiscriminantsInEnumCast
+      </k>
+      requires #isEnumWithoutFields(lookupTy(TY_TO))
+        andBool notBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO) )
+
+  rule <k>
+           #cast( Integer ( VAL , WIDTH , _SIGNED ) , castKindTransmute , _TY_FROM , TY_TO )
+        =>
+           Aggregate( #findVariantIdxFromTy( truncate(VAL, WIDTH, Unsigned), lookupTy(TY_TO) ) , .List )
+       ...
+      </k>
+      requires #isEnumWithoutFields(lookupTy(TY_TO))
+        andBool #validDiscriminant( truncate(VAL, WIDTH, Unsigned) , lookupTy(TY_TO))
+
+  syntax VariantIdx ::= #findVariantIdxFromTy ( Int , TypeInfo ) [function, total]
+  //------------------------------------------------------------------------------
+  rule #findVariantIdxFromTy( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => #findVariantIdx( VAL, DISCRIMINANTS)
+  rule #findVariantIdxFromTy( _ , _ ) => err("NotAnEnum") [owise]
+
+  syntax Bool ::= #validDiscriminant    ( Int , TypeInfo )      [function, total]
+  // ----------------------------------------------------------------------------
+  rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => #validDiscriminantAux( VAL , DISCRIMINANTS )
+  rule #validDiscriminant( _ , _ ) => false [owise]
+
+  syntax Bool ::= #validDiscriminantAux ( Int , Discriminants ) [function, total]
+  // ----------------------------------------------------------------------------
+  rule #validDiscriminantAux( VAL, discriminant(mirInt(DISCRIMINANT)) REST ) => VAL ==Int DISCRIMINANT orBool #validDiscriminantAux( VAL, REST )
+  rule #validDiscriminantAux( VAL, discriminant(    DISCRIMINANT    ) REST ) => VAL ==Int DISCRIMINANT orBool #validDiscriminantAux( VAL, REST )
+  rule #validDiscriminantAux( _VAL, .Discriminants ) => false
 ```
 
 

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

@@ -111,12 +111,6 @@ syntax Int ::= #msBytes ( MachineSize ) [function, total]
 rule #msBytes(machineSize(mirInt(NBITS))) => NBITS /Int 8 [preserves-definedness]
 rule #msBytes(machineSize(NBITS)) => NBITS /Int 8 [owise, preserves-definedness]
 
-// 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]
-
 // Minimum number of input bytes required to decode all fields by the chosen offsets.
 // Uses builtin maxInt to compute max(offset + size). The lists of types and
 // offsets must have the same length; if not, this function returns -1 to signal