Add new simp rules for integer operations and Bool2Word (#153)

These rules are used for zkevm-harness project's `MSTORE` termination
proof.

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.116
+0.1.117

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.116"
+version = "0.1.117"
 description = "K tooling for the RISC-V architecture"
 readme = "README.md"
 requires-python = "~=3.10"

src/kriscv/kdist/riscv-semantics/lemmas/bytes-simplifications.md

@@ -183,6 +183,13 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     [simplification]
 ```
 
+## Additional Bytes Simplifications
+
+```k
+  rule [bytes2int-pad-trailing-zeros]: Bytes2Int (B:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) => Bytes2Int (B, LE, Unsigned) 
+    [simplification(45)]
+```
+
 ```k
 endmodule
 ```

src/kriscv/kdist/riscv-semantics/lemmas/int-simplifications.md

@@ -54,13 +54,26 @@ module INT-SIMPLIFICATIONS [symbolic]
 
 ```k
   rule [int-and-ineq]: 0 <=Int A &Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
+  rule [int-and-ineq-4294967295]: 0 <=Int _ &Int 4294967295 => true [simplification(45)]
+  rule [int-and-ineq-65535]: 0 <=Int _ &Int 65535 => true [simplification(45)]
+  rule [int-and-ineq-255]: 0 <=Int _ &Int 255 => true [simplification(45)]
+  rule [int-or-gt]: 0 <Int A |Int B => true requires 0 <Int A orBool 0 <Int B [simplification]
   rule [int-rhs-ineq]: 0 <=Int A >>Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
   rule [int-add-ineq]: A <=Int A +Int B => true requires 0 <=Int B [simplification]
   rule [int-add-ineq-0]: 0 <=Int A +Int B => true requires 0 <=Int A andBool 0 <=Int B [simplification]
   rule [int-add-ineq-4294967295]: X &Int 4294967295 <Int A => 4294967295 <Int X
     requires 0 <=Int A andBool A <=Int X [simplification]
 ```
 
+## Additional Int Simplifications
+
+```k
+  rule [int-add-ineq-pos-1]: 0 <Int A +Int B => true 
+    requires 0 <=Int A andBool 0 <Int B [simplification(45)]
+  rule [int-add-ineq-pos-2]: 0 <Int A +Int B => true 
+    requires 0 <Int A andBool 0 <=Int B [simplification]
+```
+
 ## Int Expression Simplifications for Bytes
 
 ### Shift Left for Bytes

src/kriscv/kdist/riscv-semantics/lemmas/word-simplifications.md

@@ -19,6 +19,12 @@ module WORD-SIMPLIFICATIONS
 
 ```k
   rule [bool2word-non-neg]: 0 <=Int Bool2Word(_) => true [simplification]
+  rule [bool2word-eq-0]: Bool2Word(B) ==Int 0 => notBool B [simplification]
+  rule [bool2word-eq-1]: Bool2Word(B) ==Int 1 => B [simplification]
+
+
+  rule [int-bool2word-or-ineq]: 0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295 => true 
+    requires 0 <Int X [simplification(45)]
 ```
 
 ```k

src/tests/integration/test-data/specs/byte-offset-bounds-check.k

@@ -0,0 +1,21 @@
+module BYTE-OFFSET-BOUNDS-CHECK
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <regs>
+     1  |-> (Bool2Word(0 <Int (0 -Int Bool2Word(4294967295 <Int X)) &Int 4294967295 |Int X &Int 4294967295) => 1)
+     2  |-> (Bool2Word(0 <=Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned )) => 1)
+     3  |-> (Bool2Word(0 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 1)
+     4  |-> (Bool2Word(0 <Int 0 -Int Bool2Word ( 4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 ) &Int 4294967295 |Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32 &Int 4294967295) => 1)
+     // 5  |-> (Bool2Word(4294967295 <Int Bytes2Int ( OFFSET:Bytes +Bytes b"\x00\x00\x00" , LE , Unsigned ) +Int 32) => 0)
+     6  |-> (Bool2Word(Y <=Int Z) => 0)
+     7  |-> (Bool2Word(Z <=Int 4294967295) => 1)
+    </regs>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires 0 <Int X 
+     andBool lengthBytes(OFFSET) ==Int 1
+     andBool notBool (Y <=Int Z)
+     andBool notBool (Bool2Word(Z <=Int 4294967295) ==Int 0)
+endmodule