Hotfix byte number conversion optimisations (#824)

* avoids using `/Int` and `%Int` in the byte-to-number conversions
* modifies the tests to exhibit a bit more complicated expressions
* Adds targeted simplifications to make the modified tests pass

Author: jberthold

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

@@ -118,18 +118,39 @@ 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]
 ```
 
+Support for `transmute` between byte arrays and numbers (and vice-versa) uses computations involving bit masks with 255 and 8-bit shifts.
+To support simplifying round-trip conversion, the following simplifications are essential.
+
 ```k
-  rule (VAL +Int 256 *Int REST) %Int 256 => VAL
+  rule (VAL +Int 256 *Int REST) &Int 255 => 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
+  rule (VAL +Int 256 *Int REST) >>Int 8 => REST
   requires 0 <=Int VAL
     andBool VAL <=Int 255
     andBool 0 <=Int REST
   [simplification, preserves-definedness]
+
+  rule (_ &Int 255) <=Int 255 => true
+    [simplification, preserves-definedness]
+  rule 0 <=Int (_ &Int 255) => true
+    [simplification, preserves-definedness]
+
+  rule [simplify-u64-bytes-u64]:
+      (VAL                                                                         &Int 255) +Int (256 *Int (
+        ((VAL >>Int 8)                                                             &Int 255) +Int (256 *Int (
+          ((VAL >>Int 8 >>Int 8)                                                   &Int 255) +Int (256 *Int (
+            ((VAL >>Int 8 >>Int 8 >>Int 8)                                         &Int 255) +Int (256 *Int (
+              ((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8)                               &Int 255) +Int (256 *Int (
+                ((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)                     &Int 255) +Int (256 *Int (
+                  ((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)           &Int 255) +Int (256 *Int (
+                    ((VAL >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255)))))))))))))))
+      => VAL
+    requires 0 <=Int VAL andBool VAL <=Int bitmask64
+    [simplification, preserves-definedness, symbolic(VAL)]
 ```
 
 

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

@@ -1459,16 +1459,16 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
           ...
         </k>
       requires #isStaticU8Array(lookupTy(TY_TARGET))
-       andBool WIDTH >=Int 0
-       andBool WIDTH %Int 8 ==Int 0
        andBool WIDTH ==Int #staticArrayLenBits(lookupTy(TY_TARGET))
+      //  andBool WIDTH >=Int 0  ensured by the above
+      //  andBool WIDTH % 8 == 0 ensured by the above
       [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
+    => #littleEndianBytes(truncate(VAL, WIDTH, Unsigned), WIDTH >>Int 3)
+    requires WIDTH &Int 7 ==Int 0 // WIDTH % 8 == 0
      andBool WIDTH >=Int 0
     [preserves-definedness]
 
@@ -1479,7 +1479,7 @@ Casting an integer to a `[u8; N]` array materialises its little-endian bytes.
     requires COUNT <=Int 0
 
   rule #littleEndianBytes(VAL, COUNT)
-    => ListItem(Integer(VAL %Int 256, 8, false)) #littleEndianBytes(VAL /Int 256, COUNT -Int 1)
+    => ListItem(Integer(VAL &Int 255, 8, false)) #littleEndianBytes(VAL >>Int 8, COUNT -Int 1)
     requires COUNT >Int 0
     [preserves-definedness]
 

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

@@ -5,13 +5,19 @@ 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) };
+    // prevent round-trip-transmute rule from simplifying this
+    let enlarged = value as u128;
+    let original = enlarged as u64;
+    let roundtrip = unsafe { transmute::<u64, [u8; 8]>(original) };
     assert_eq!(roundtrip, bytes);
     value
 }
 
 fn u64_to_bytes(value: u64) -> [u8; 8] {
-    let bytes = unsafe { transmute::<u64, [u8; 8]>(value) };
+    let mut bytes = unsafe { transmute::<u64, [u8; 8]>(value) };
+    let first = bytes[0];
+    bytes[0] = 255u8;
+    bytes[0] = first;
     let roundtrip = unsafe { transmute::<[u8; 8], u64>(bytes) };
     assert_eq!(roundtrip, value);
     bytes