feat(rt): support round-trip transmute bytes <> u64 casts (#804)

- close #697

---------

Co-authored-by: Jost Berthold <jost.berthold@gmail.com>
Co-authored-by: Daniel Cumming <124537596+dkcumming@users.noreply.github.com>

Author: 3 people

kmir/src/kmir/kdist/mir-semantics/lemmas/kmir-lemmas.md

@@ -118,6 +118,20 @@ power of two but the semantics will always operate with these particular ones.
   rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
 ```
 
+```k
+  rule (VAL +Int 256 *Int REST) %Int 256 => VAL
+  requires 0 <=Int VAL
+    andBool VAL <=Int 255
+    andBool 0 <=Int REST
+  [simplification, preserves-definedness]
+
+  rule (VAL +Int 256 *Int REST) /Int 256 => REST
+  requires 0 <=Int VAL
+    andBool VAL <=Int 255
+    andBool 0 <=Int REST
+  [simplification, preserves-definedness]
+```
+
 
 ```k
 endmodule

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

@@ -1433,6 +1433,94 @@ The first cast is reified as a `thunk`, the second one resolves it and eliminate
      andBool lookupTy(TY_DEST_INNER) ==K lookupTy(TY_SRC_OUTER) // and is well-formed (invariant)
 ```
 
+Casting a byte array/slice to an integer reinterprets the bytes in little-endian order.
+
+```k
+  rule <k> #cast(
+              Range(ELEMS),
+              castKindTransmute,
+              _TY_SOURCE,
+              TY_TARGET
+            )
+          =>
+            #intAsType(
+              #littleEndianFromBytes(ELEMS),
+              size(ELEMS) *Int 8,
+              #numTypeOf(lookupTy(TY_TARGET))
+            )
+          ...
+        </k>
+      requires #isIntType(lookupTy(TY_TARGET))
+       andBool size(ELEMS) *Int 8 ==Int #bitWidth(#numTypeOf(lookupTy(TY_TARGET)))
+       andBool #areLittleEndianBytes(ELEMS)
+      [preserves-definedness] // ensures #numTypeOf is defined
+
+  syntax Bool ::= #areLittleEndianBytes ( List ) [function, total]
+  // -------------------------------------------------------------
+  rule #areLittleEndianBytes(.List) => true
+  rule #areLittleEndianBytes(ListItem(Integer(_, 8, false)) REST)
+    => #areLittleEndianBytes(REST)
+  rule #areLittleEndianBytes(ListItem(_OTHER) _) => false [owise]
+
+  syntax Int ::= #littleEndianFromBytes ( List ) [function]
+  // -----------------------------------------------------
+  rule #littleEndianFromBytes(.List) => 0
+  rule #littleEndianFromBytes(ListItem(Integer(BYTE, 8, false)) REST)
+    => BYTE +Int 256 *Int #littleEndianFromBytes(REST)
+```
+
+Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
+
+```k
+  rule <k> #cast(
+              Integer(VAL, WIDTH, _SIGNEDNESS),
+              castKindTransmute,
+              _TY_SOURCE,
+              TY_TARGET
+            )
+          =>
+            Range(#littleEndianBytesFromInt(VAL, WIDTH))
+          ...
+        </k>
+      requires #isStaticU8Array(lookupTy(TY_TARGET))
+       andBool WIDTH >=Int 0
+       andBool WIDTH %Int 8 ==Int 0
+       andBool WIDTH ==Int #staticArrayLenBits(lookupTy(TY_TARGET))
+      [preserves-definedness] // ensures element type/length are well-formed
+
+  syntax List ::= #littleEndianBytesFromInt ( Int, Int ) [function]
+  // -------------------------------------------------------------
+  rule #littleEndianBytesFromInt(VAL, WIDTH)
+    => #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH /Int 8)
+    requires WIDTH %Int 8 ==Int 0
+     andBool WIDTH >=Int 0
+    [preserves-definedness]
+
+  syntax List ::= #littleEndianBytes ( Int, Int ) [function]
+  // -------------------------------------------------------------
+  rule #littleEndianBytes(_, COUNT)
+    => .List
+    requires COUNT <=Int 0
+
+  rule #littleEndianBytes(VAL, COUNT)
+    => ListItem(Integer(VAL %Int 256, 8, false)) #littleEndianBytes(VAL /Int 256, COUNT -Int 1)
+    requires COUNT >Int 0
+    [preserves-definedness]
+
+  syntax Bool ::= #isStaticU8Array ( TypeInfo ) [function, total]
+  // -------------------------------------------------------------
+  rule #isStaticU8Array(typeInfoArrayType(ELEM_TY, someTyConst(_)))
+    => lookupTy(ELEM_TY) ==K typeInfoPrimitiveType(primTypeUint(uintTyU8))
+  rule #isStaticU8Array(_OTHER) => false [owise]
+
+  syntax Int ::= #staticArrayLenBits ( TypeInfo ) [function, total]
+  // -------------------------------------------------------------
+  rule #staticArrayLenBits(typeInfoArrayType(_, someTyConst(tyConst(KIND, _))))
+    => readTyConstInt(KIND) *Int 8
+    [preserves-definedness]
+  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:

kmir/src/tests/integration/data/prove-rs/transmute-bytes.rs

@@ -0,0 +1,31 @@
+#![allow(clippy::transmute_bytes_to_bytes)]
+#![allow(clippy::unnecessary_transmute)]
+
+use std::mem::transmute;
+
+fn bytes_to_u64(bytes: [u8; 8]) -> u64 {
+    let value = unsafe { transmute::<[u8; 8], u64>(bytes) };
+    let roundtrip = unsafe { transmute::<u64, [u8; 8]>(value) };
+    assert_eq!(roundtrip, bytes);
+    value
+}
+
+fn u64_to_bytes(value: u64) -> [u8; 8] {
+    let bytes = unsafe { transmute::<u64, [u8; 8]>(value) };
+    let roundtrip = unsafe { transmute::<[u8; 8], u64>(bytes) };
+    assert_eq!(roundtrip, value);
+    bytes
+}
+
+fn main() {
+    let bytes = [0x01, 0x23, 0x45, 0x67, 0x89, 0xAB, 0xCD, 0xEF];
+    let int = bytes_to_u64(bytes);
+    assert_eq!(int, 0xEFCD_AB89_6745_2301);
+
+    let roundtrip = u64_to_bytes(int);
+    assert_eq!(roundtrip, bytes);
+
+    let value = 0x1020_3040_5060_7080_u64;
+    let value_roundtrip = bytes_to_u64(u64_to_bytes(value));
+    assert_eq!(value_roundtrip, value);
+}

kmir/src/tests/integration/test_integration.py

@@ -36,6 +36,7 @@
     'pointer-cast-length-test-fail': ['array_cast_test'],
     'assume-cheatcode': ['check_assume'],
     'assume-cheatcode-conflict-fail': ['check_assume_conflict'],
+    'transmute-bytes': ['bytes_to_u64', 'u64_to_bytes'],
 }
 PROVE_RS_SHOW_SPECS = [
     'local-raw-fail',