HOTFIX: avoid bitRangeInt function for branching (#switchInt) (#732)

The [`bitRangeInt` equation in
`domains.md`](https://github.com/runtimeverification/k/blob/c376de7d91e5f14cff13b7e32e1c997983a2859b/k-distribution/include/kframework/builtin/domains.md?plain=1#L1438)
uses partial bit-shift symbols and is therefore not applied by booster.
A better alternative is to use the `truncate` function locally defined
in `mir-semantics`. Expressions are equivalent:

```
bitRangeInt(VAL, 0, WIDTH)
      (def)      == (VAL >>Int 0) modInt (1 <<Int WIDTH)
      (>> 0)     == VAL modInt (1 <<Int WIDTH)
  (mod via mask) == VAL &Int ((1<<Int WIDTH) -Int 1) == truncate(VAL, WIDTH, Unsigned)
```

Also marking some relevant simplifications as smt-lemmas.

Altogether, this avoids a number of observed fall-backs in p-token
execution.

Author: jberthold

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

@@ -324,7 +324,7 @@ will be `129`.
 
   rule #switchMatch(0, BoolVal(B)           ) => notBool B
   rule #switchMatch(1, BoolVal(B)           ) => B
-  rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int bitRangeInt(I2, 0, WIDTH)
+  rule #switchMatch(I, Integer(I2, WIDTH, _)) => I ==Int truncate(I2, WIDTH, Unsigned)
 ```
 
 `Return` simply returns from a function call, using the information

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

@@ -81,14 +81,16 @@ Therefore, its value range should be simplified for symbolic input asserted to b
 
 ```k
   rule truncate(VAL, WIDTH, Unsigned) => VAL
-    requires VAL <Int (1 <<Int WIDTH)
+    requires 0 <Int WIDTH
+     andBool VAL <Int (1 <<Int WIDTH)
      andBool 0 <=Int VAL
-     [simplification]
+     [simplification, preserves-definedness] // , smt-lemma], but `Unsigned` needs to be smtlib
 
   rule truncate(VAL, WIDTH, Signed) => VAL
-    requires VAL <Int (1 <<Int (WIDTH -Int 1))
+    requires 0 <Int WIDTH
+     andBool VAL <Int (1 <<Int (WIDTH -Int 1))
      andBool 0 -Int (1 <<Int (WIDTH -Int 1)) <=Int VAL
-     [simplification]
+     [simplification, preserves-definedness] // , smt-lemma], but `Signed` needs to be smtlib
 ```
 
 However, `truncate` gets evaluated and is therefore not present any more for this simplification.
@@ -97,17 +99,6 @@ The following simplification rules operate on the expression created by evaluati
 power of two but the semantics will always operate with these particular ones.
 
 ```k
-  rule VAL &Int MASK => VAL 
-    requires 0   <=Int VAL 
-     andBool VAL <=Int MASK
-     andBool ( MASK ==Int bitmask8
-        orBool MASK ==Int bitmask16
-        orBool MASK ==Int bitmask32
-        orBool MASK ==Int bitmask64
-        orBool MASK ==Int bitmask128
-     )
-    [simplification, preserves-definedness]
-
   syntax Int ::= "bitmask8"    [macro]
                | "bitmask16"   [macro]
                | "bitmask32"   [macro]
@@ -120,6 +111,11 @@ power of two but the semantics will always operate with these particular ones.
   rule bitmask64  => ( 1 <<Int 64 ) -Int 1
   rule bitmask128 => ( 1 <<Int 128) -Int 1
 
+  rule VAL &Int bitmask8   => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask8   [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int bitmask16  => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask16  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int bitmask32  => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask32  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int bitmask64  => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask64  [simplification, preserves-definedness, smt-lemma]
+  rule VAL &Int bitmask128 => VAL requires 0 <=Int VAL andBool VAL <=Int bitmask128 [simplification, preserves-definedness, smt-lemma]
 ```
 
 

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

@@ -68,7 +68,7 @@ This truncation function is instrumental in the implementation of Integer arithm
 
 ```k
   // helper function to truncate int values
-  syntax Int ::= truncate(Int, Int, Signedness) [function, total]
+  syntax Int ::= truncate(Int, Int, Signedness) [function, total, smtlib(smt_truncate)]
   // -------------------------------------------------------------
   rule truncate(_, WIDTH, _) => 0
     requires WIDTH <=Int 0