Refine simp rule for Bytes2Int o Int2Byes (#139)

Solve the problem in #137.

---------

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

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.105
+0.1.106

pyproject.toml

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

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

@@ -161,7 +161,7 @@ module BYTES-SIMPLIFICATIONS [symbolic]
      andBool LEN <=Int lengthBytes(B)
     [simplification, preserves-definedness]
   rule [bytes2int-int2bytes]: Bytes2Int(Int2Bytes(LEN, V, LE), LE, Unsigned) => V &Int (2 ^Int (LEN *Int 8) -Int 1)
-    requires 0 <=Int LEN andBool 0 <=Int V [simplification, preserves-definedness]
+    requires 0 <=Int LEN [simplification, preserves-definedness]
 ```
 
 ```k

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

@@ -29,6 +29,7 @@ module BYTES-INT
      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))
+     25 |-> (Bytes2Int(Int2Bytes(1, (Bytes2Int(substrBytes(reverseBytes(W3), 8, 12), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 8, 12), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 4, 8), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 4, 8), LE, Unsigned) +Int Bool2Word(4294967295 <Int Bytes2Int(substrBytes(reverseBytes(W3), 0, 4), LE, Unsigned) +Int Bytes2Int(substrBytes(reverseBytes(W0), 0, 4), LE, Unsigned))) &Int 4294967295) >>Int 8, LE), LE, Unsigned) => ( Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 8 , 12 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 8 , 12 ) , LE , Unsigned ) +Int Bool2Word ( 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 4 , 8 ) , LE , Unsigned ) +Int Bool2Word ( 4294967295 <Int Bytes2Int ( substrBytes ( reverseBytes ( W3:Bytes ) , 0 , 4 ) , LE , Unsigned ) +Int Bytes2Int ( substrBytes ( reverseBytes ( W0:Bytes ) , 0 , 4 ) , LE , Unsigned ) ) ) &Int 4294967295 ) >>Int 8 &Int 255)
     </regs>
     <haltCond> ADDRESS ( 0 ) </haltCond>
 requires lengthBytes(W0) ==Int 32