Add a few simplifications and definedness preservation attributes (#855)

* declares that `#intAsType` and `littleEndianFromBytes` equations
preserve definedness (booster should apply them)
* removes round-trips from (symbolic) `discriminant` to `variantIdx` and
back
* simplifies repeated bit shifts and asserts magnitude limit for
byte-sliced values

Author: jberthold

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

@@ -74,6 +74,24 @@ Definedness of the list and list elements is also guaranteed.
     [simplification]
 ```
 
+## Simplifications for `enum` Discriminants and Variant Indexes
+
+For symbolic enum values, the variant index remains unevaluated but the original (symbolic) discriminant can be restored:
+
+```k
+  rule #lookupDiscriminant(typeInfoEnumType(_, _, _, _, _), #findVariantIdxAux(DISCR, DISCRS, _IDX)) => DISCR
+    requires isOneOf(DISCR, DISCRS)
+    [simplification, preserves-definedness, symbolic(DISCR)]
+
+  syntax Bool ::= isOneOf ( Int , Discriminants ) [function, total]
+  // --------------------------------------------------------------
+  rule isOneOf( _,                       .Discriminants                      ) => false
+  rule isOneOf( I, discriminant(D)                     .Discriminants        ) => I ==Int D
+  rule isOneOf( I, discriminant(mirInt(D))             .Discriminants        ) => I ==Int D
+  rule isOneOf( I, discriminant(D)         ((discriminant(_) _MORE) #as REST)) => I ==Int D orBool isOneOf(I, REST)
+  rule isOneOf( I, discriminant(mirInt(D)) ((discriminant(_) _MORE) #as REST)) => I ==Int D orBool isOneOf(I, REST)
+```
+
 ## Simplifications for Int
 
 These are trivial simplifications driven by syntactic equality, which should be present upstream.
@@ -130,6 +148,14 @@ 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]
 ```
 
+Repeated bit-masking can be simplified in an even more general way:
+
+```k
+     rule (X &Int MASK &Int MASK) => X &Int MASK
+       requires 0 <Int MASK
+       [simplification, 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.
 
@@ -165,6 +191,24 @@ To support simplifying round-trip conversion, the following simplifications are
     [simplification, preserves-definedness, symbolic(VAL)]
 ```
 
+More generally, a value which is composed of sliced bytes can generally be assumed to be in range of a suitable bitmask for the byte length.
+This avoids building up large expressions related to overflow checks and vacuous branches leading to overflow errors.
+
+```k
+  rule ((( _X0 )                                                                     &Int 255) +Int 256 *Int (
+         (( _X1 >>Int 8)                                                              &Int 255) +Int 256 *Int (
+           (( _X2 >>Int 8 >>Int 8)                                                    &Int 255) +Int 256 *Int (
+              (( _X3 >>Int 8 >>Int 8 >>Int 8)                                         &Int 255) +Int 256 *Int (
+                (( _X4 >>Int 8 >>Int 8 >>Int 8 >>Int 8)                               &Int 255) +Int 256 *Int (
+                  (( _X5 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)                     &Int 255) +Int 256 *Int (
+                    (( _X6 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8)           &Int 255) +Int 256 *Int (
+                      (( _X7 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8 >>Int 8) &Int 255)))))))))
+          <=Int bitmask64
+        => true
+    [simplification, preserves-definedness, symbolic]
+```
+
+
 For the case where the (symbolic) byte values are first converted to a number, the round-trip simplification requires different matching.
 First, the bit-masking with `&Int 255` eliminates `Bytes2Int(Int2Bytes(1, ..) +Bytes ..)` enclosing a byte-valued variable:
 

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

@@ -1506,6 +1506,7 @@ Casting a byte array/slice to an integer reinterprets the bytes in little-endian
   rule #littleEndianFromBytes(.List) => 0
   rule #littleEndianFromBytes(ListItem(Integer(BYTE, 8, false)) REST)
     => BYTE +Int 256 *Int #littleEndianFromBytes(REST)
+    [preserves-definedness]
 ```
 
 Casting an integer to a `[u8; N]` array materialises its little-endian bytes.

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

@@ -127,12 +127,14 @@ This truncation function is instrumental in the implementation of Integer arithm
           true
         )
     requires #bitWidth(INTTYPE) <=Int WIDTH
+    [preserves-definedness]
 
   // widening: nothing to do: VAL does not change (enough bits to represent, no sign change possible)
   rule #intAsType(VAL, WIDTH, INTTYPE:IntTy)
       =>
         Integer(VAL, #bitWidth(INTTYPE), true)
     requires WIDTH <Int #bitWidth(INTTYPE)
+    [preserves-definedness]
 
   // converting to unsigned int types (simple bitmask)
   rule #intAsType(VAL, _, UINTTYPE:UintTy)
@@ -142,6 +144,7 @@ This truncation function is instrumental in the implementation of Integer arithm
           #bitWidth(UINTTYPE),
           false
         )
+    [preserves-definedness]
 ```
 
 ## Alignment of Primitives