Add simplification rule for Bytes2Int &Int 4294967295 (#135)

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

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.104
+0.1.105

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kriscv"
-version = "0.1.104"
+version = "0.1.105"
 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,6 +137,9 @@ 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-ffffffff]: Bytes2Int(B, LE, Unsigned) &Int 4294967295 => Bytes2Int(substrBytes(B, 0, 4), LE, Unsigned)
+    requires 4 <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
   rule [bytes2int-upperbound]: Bytes2Int(B, _, Unsigned) <Int X => true
     requires 2 ^Int (lengthBytes(B) *Int 8) <=Int X
     [simplification]

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

@@ -28,6 +28,7 @@ module BYTES-INT
      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)))
+     24 |-> (Bytes2Int(b"\x00\x00\x00" +Bytes substrBytes(W0, 24, 28), LE, Unsigned) &Int 4294967295 => Bytes2Int ( b"\x00\x00\x00" +Bytes substrBytes(W0 ,24, 25), LE, Unsigned))
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32