Simp rule 4 int2bytes o bytes2int (#147)

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.109
+0.1.110

pyproject.toml

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

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

@@ -162,6 +162,18 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     [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 [simplification, preserves-definedness]
+  
+  rule [substr-reverse-bytes]:
+    substrBytes(reverseBytes(B), START, END)
+    => substrBytes(B, lengthBytes(B) -Int END, lengthBytes(B) -Int START)
+    requires 0 <=Int START andBool START +Int 1 ==Int END andBool END <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
+  
+  rule [int2bytes-bytes2int-pad-zeros]:
+    Int2Bytes(LEN, Bytes2Int(B, LE, Unsigned), LE)
+    => B +Bytes Int2Bytes(LEN -Int lengthBytes(B), 0, LE)
+    requires lengthBytes(B) <=Int LEN
+    [simplification]
 ```
 
 ```k

src/tests/integration/test-data/specs/int2bytes-bytes2int.k

@@ -0,0 +1,14 @@
+module INT2BYTES-BYTES2INT
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <mem>
+      #bytes (  Int2Bytes ( 4 , Bytes2Int ( substrBytes ( reverseBytes ( VALUE:Bytes ) , 20 , 21 ) , LE , Unsigned ) , LE ) ) .SparseBytes
+      => 
+      #bytes ( substrBytes ( VALUE:Bytes , 11 , 12 ) +Bytes b"\x00\x00\x00" ) .SparseBytes
+    </mem>
+    <pc> 0 </pc>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires lengthBytes(VALUE) ==Int 32
+endmodule