Add simp rules for Int2Bytes o Bytes2Int (#111)

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.84
+0.1.85

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.84"
+version = "0.1.85"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

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

@@ -118,6 +118,15 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     [simplification, preserves-definedness, concrete(L,V), symbolic(B)]
 ```
 
+## Bytes2Int Lemmas
+
+```k
+  rule [int2bytes-bytes2int]: Int2Bytes(LEN:Int, Bytes2Int(B:Bytes, LE, Unsigned), LE) => substrBytes(B, 0, LEN)
+    requires 0 <=Int LEN
+     andBool LEN <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
+```
+
 ```k
 endmodule
 ```

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

@@ -18,6 +18,8 @@ module BYTES-INT
      9  |-> (W(Bytes2Int(replaceAtBytes (b"\x00\x00", 0, b"\x01\x02"), LE, Unsigned)) => W(513))
      10 |-> (W(Bytes2Int(replaceAtBytes (W1, 2, b"\x01\x02"), LE, Unsigned)) => W(Bytes2Int(substrBytes ( W1:Bytes , 0 , 2 ) +Bytes b"\x01\x02", LE, Unsigned)))
      11 |-> (W(Bytes2Int(substrBytes(b"\x00", 1, 1), LE, Unsigned)) => W(0))
+     12 |-> (W(Bytes2Int(Int2Bytes ( 4 , Bytes2Int (W1, LE, Unsigned), LE ), LE, Unsigned)) => W(Bytes2Int(W1, LE, Unsigned)))
+     13 |-> (W(Bytes2Int(Int2Bytes ( 4 , Bytes2Int ( substrBytes ( W0:Bytes , 31 , 32 ) +Bytes substrBytes ( W0:Bytes , 30 , 31 ) +Bytes substrBytes ( W0:Bytes , 29 , 30 ) +Bytes substrBytes ( W0:Bytes , 28 , 32 ) , LE , Unsigned ) , LE ), LE, Unsigned)) => W(Bytes2Int(substrBytes ( W0:Bytes , 31 , 32 ) +Bytes substrBytes ( W0:Bytes , 30 , 31 ) +Bytes substrBytes ( W0:Bytes , 29 , 30 ) +Bytes substrBytes ( W0:Bytes , 28 , 29), LE, Unsigned)))
     </regs>
     <test>
       <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>