Simp rule 4 (A +Int B) &Int 4294967295 <Int A (#130)

Also fix a bug for `bytes2int-upperbound`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.102
+0.1.103

pyproject.toml

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

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

@@ -137,8 +137,8 @@ module BYTES-SIMPLIFICATIONS [symbolic]
   rule [bytes2int-substr-ff00-1]: Bytes2Int (substrBytes(B, I, J), LE, Unsigned) &Int 65280 => B[I +Int 1] <<Int 8
     requires 0 <=Int I andBool I +Int 1 <Int J andBool J <=Int lengthBytes(B)
     [simplification, preserves-definedness]
-  rule [bytes2int-upperbound]: Bytes2Int(B, _, _) <Int X => true
-    requires 2 ^Int lengthBytes(B) <=Int X
+  rule [bytes2int-upperbound]: Bytes2Int(B, _, Unsigned) <Int X => true
+    requires 2 ^Int (lengthBytes(B) *Int 8) <=Int X
     [simplification]
   rule [bytes2int-lowerbound]: 0 <=Int Bytes2Int(_, _, Unsigned) => true [simplification]
 ```

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

@@ -42,6 +42,9 @@ 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-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-4294967295]: X &Int 4294967295 <Int A => 4294967295 <Int X
+    requires 0 <=Int A andBool A <=Int X [simplification]
 ```
 
 ## Int Expression Simplifications for Bytes

src/tests/integration/test-data/specs/bytes-int.k

@@ -26,6 +26,8 @@ module BYTES-INT
      19 |-> (Bytes2Int(substrBytes(W0, 2, 3) +Bytes substrBytes(W0, 1, 2) +Bytes substrBytes(W0, 0, 1), LE, Unsigned) => Bytes2Int(reverseBytes(substrBytes(W0, 0, 3)), LE, Unsigned))
      20 |-> (Bytes2Int(reverseBytes(substrBytes(W0, 10, 12)) +Bytes substrBytes(W0, 9, 10) +Bytes substrBytes(W0, 8, 12), LE, Unsigned) => Bytes2Int(reverseBytes(substrBytes(W0, 9, 12)) +Bytes substrBytes(W0, 8, 12), LE, Unsigned))
      21 |-> (Bytes2Int(reverseBytes(substrBytes(W0, 8, 13)) +Bytes reverseBytes(substrBytes(W0, 5, 8)) +Bytes reverseBytes(substrBytes(W0, 0, 5)) +Bytes reverseBytes(substrBytes(W3, 29, 32)) +Bytes reverseBytes(substrBytes(W3, 24, 29)) +Bytes reverseBytes(substrBytes(W3, 21, 24)) +Bytes reverseBytes(substrBytes(W3, 16, 21)) +Bytes reverseBytes(substrBytes(W3, 13, 16)) +Bytes reverseBytes(substrBytes(W3, 8, 13)) +Bytes reverseBytes(substrBytes(W3, 5, 8)) +Bytes reverseBytes(substrBytes(W3, 0, 5)), LE, Unsigned) => Bytes2Int(reverseBytes(substrBytes(W0, 0, 13)) +Bytes reverseBytes(W3), LE, Unsigned))
+     22 |-> (Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned) &Int 4294967295 => Bytes2Int(substrBytes(reverseBytes(W0), 16, 20), LE, Unsigned))
+     23 |-> (Bool2Word(Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned) &Int 4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned)) => Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned)))
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32

src/tests/integration/test-data/specs/int-spec.k

@@ -12,7 +12,7 @@ module INT-SPEC
      5  |-> ((W2 <<Int 16 &Int 4294967295) => W2 <<Int 16)
      6  |-> ((b"\x12"[0] <<Int 16 &Int 4294967295) => 1179648)
      7  |-> ((Bytes2Int(b"\x00\x00\x12", LE, Unsigned)) => 1179648)
-     8  |-> ((Bytes2Int(W3, LE, Unsigned) &Int 4294967295) => Bytes2Int(W3, LE, Unsigned))
+     8  |-> ((Bytes2Int(substrBytes(W3, 0, 4), LE, Unsigned) &Int 4294967295) => Bytes2Int(substrBytes(W3, 0, 4), LE, Unsigned))
      9  |-> ((W3[0] <<Int 16 &Int 4294967295) => Bytes2Int(b"\x00\x00" +Bytes substrBytes(W3, 0, 1 ), LE, Unsigned))
      10 |-> ((Bytes2Int(b"\x12\x34\x56\x78", LE, Unsigned) >>Int 8) => 7886388)
      11 |-> ((Bytes2Int(b"\x34\x56\x78", LE, Unsigned)) => 7886388)