Add new lemmas for substrBytes and update pickFront rule (#94)

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.71
+0.1.72

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.71"
+version = "0.1.72"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

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

@@ -68,7 +68,21 @@ module BYTES-SIMPLIFICATIONS
     [simplification]
 
 ```
-    
+
+## substrBytes Lemmas
+
+```k
+  rule [substr-bytes-length]: lengthBytes(substrBytes(B, I, J)) => J -Int I 
+    requires 0 <=Int I
+     andBool I <=Int J
+     andBool J <=Int lengthBytes(B)
+  [simplification, preserves-definedness]
+  rule [substr-substr]: substrBytes(substrBytes(B, I, J), I0, J0) => substrBytes(B, I +Int I0, I +Int J0) 
+    requires 0 <=Int I  andBool I  <=Int J  andBool J  <=Int lengthBytes(B)
+     andBool 0 <=Int I0 andBool I0 <=Int J0 andBool J0 <=Int J -Int I
+  [simplification, preserves-definedness]
+```
+
 ```k
 endmodule
 ```

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

@@ -15,6 +15,10 @@ module SPARSE-BYTES-SIMPLIFICATIONS
 For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _` and `#bytes(B +Bytes BS) EF` to obtain as exact as possible values for `pickFront`.
 
 ```k
+  rule pickFront(#bytes(substrBytes(B, I, J) +Bytes _) _ , J0) => substrBytes(substrBytes(B, I, J), 0, J0)
+    requires 0 <=Int I andBool I <=Int J andBool J <=Int lengthBytes(B)
+     andBool J0 <=Int lengthBytes(substrBytes(B, I, J))
+  [simplification(44), preserves-definedness]
   rule pickFront(#bytes(B +Bytes _) _ , I) => substrBytes(B, 0, I)
     requires I >Int 0 andBool I <=Int lengthBytes(B)    [simplification(45)]
   rule pickFront(#bytes(B +Bytes BS) EF, I) => B +Bytes pickFront(#bytes(BS) EF, I -Int lengthBytes(B))

src/tests/integration/test-data/specs/pickfront0.k

@@ -0,0 +1,20 @@
+requires "riscv-semantics/riscv.md"
+
+module PICKFRONT0
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+        .Map
+    </regs>
+    <pc> W ( 0 ) </pc>
+    <mem>
+    #bytes(pickFront ( #bytes ( substrBytes ( W0:Bytes , 16 , 32 ) +Bytes W1:Bytes +Bytes b"\x00\x00\x00\x00\x00" ) .SparseBytes , 4 )) .SparseBytes
+    => #bytes ( substrBytes ( W0:Bytes , 16 , 20 ) ) .SparseBytes
+    </mem>
+    <test>
+      <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>
+    </test>
+requires lengthBytes(W0) ==Int 32 andBool lengthBytes(W1) ==Int 32
+endmodule