Transmute integer to fieldless enum

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

@@ -1499,7 +1499,8 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
 
 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:
+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 after adjusting to the byte length of the discriminant:
+
 
 ```k
   rule <k> #discriminant(
@@ -1516,6 +1517,58 @@ If none of the `enum` variants has any fields, the `Transmute` of a number to th
   rule #isEnumWithoutFields(_OTHER) => false [owise]
 ```
 
+```k
+  rule <k>
+           #cast( Integer ( VAL , WIDTH , SIGNED ) , castKindTransmute , _TY_FROM , TY_TO )
+        =>
+           Aggregate( variantIdx(VAL) , .List )
+       ...
+      </k>
+      requires #isEnumWithoutFields(lookupTy(TY_TO))
+        andBool #tagCompatible(WIDTH, SIGNED, lookupTy(TY_TO))
+        andBool #validDiscriminant(VAL, lookupTy(TY_TO))
+
+  syntax Bool ::= #validDiscriminant    ( Int , TypeInfo )      [function, total]
+  // ----------------------------------------------------------------------------
+  rule #validDiscriminant( VAL , typeInfoEnumType(_, _, DISCRIMINANTS, _, _) ) => variantIdx(VAL) ==K #findVariantIdx(VAL, DISCRIMINANTS)
+  rule #validDiscriminant(_, _) => false [owise]
+
+  syntax Bool ::= #tagCompatible ( Int, Bool, TypeInfo )  [function, total]
+  // ----------------------------------------------------------------------
+  rule #tagCompatible(
+    WIDTH,
+    SIGNED,
+    typeInfoEnumType(...
+               name: _
+             , adtDef: _
+             , discriminants: _
+             , fields: _
+             , layout:
+                someLayoutShape(layoutShape(...
+                    fields: _
+                  , variants:
+                      variantsShapeMultiple(
+                        mk(...
+                            tag: scalarInitialized(
+                              mk(...
+                                  value: primitiveInt(mk(... length: TAG_WIDTH, signed: TAG_SIGNED))
+                                , validRange: _
+                              )
+                            )
+                          , tagEncoding: _
+                          , tagField: _
+                          , variants: _
+                          )
+                        )
+                  , abi: _
+                  , abiAlign: _
+                  , size: _
+                ))
+             )
+  ) => WIDTH ==Int #byteLength(TAG_WIDTH) andBool SIGNED ==Bool TAG_SIGNED
+  rule #tagCompatible( _ , _ , _ ) => false [owise]
+```
+
 
 ### Other casts involving pointers
 

kmir/src/tests/integration/data/prove-rs/transmute-u8-to-enum.rs

@@ -0,0 +1,15 @@
+#[repr(u8)]
+#[derive(Clone, Copy, Debug, PartialEq)]
+pub enum AccountState {
+    Uninitialized,
+    Initialized,
+    Frozen,
+}
+
+fn main() {
+    unsafe {
+        assert_eq!(core::mem::transmute::<u8, AccountState>(0), AccountState::Uninitialized);
+        assert_eq!(core::mem::transmute::<u8, AccountState>(1), AccountState::Initialized);
+        assert_eq!(core::mem::transmute::<u8, AccountState>(2), AccountState::Frozen);
+    }
+}