Add bytes concatenation simplification rules (#155)

Add simp rule 4 zkevm project's `SSTORE`

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: automergerpr-permission-manager[bot] <190534181+automergerpr-permission-manager[bot]@users.noreply.github.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.114
+0.1.115

pyproject.toml

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

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

@@ -43,6 +43,13 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     rule [bytes-concat-right-assoc-symb-l]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B1), simplification(40)]
     rule [bytes-concat-right-assoc-symb-r]: (B1:Bytes +Bytes B2:Bytes) +Bytes B3:Bytes => B1 +Bytes (B2 +Bytes B3) [symbolic(B2), simplification(40)]
     rule [bytes-concat-left-assoc-conc]:    B1:Bytes +Bytes (B2:Bytes +Bytes B3:Bytes) => (B1 +Bytes B2) +Bytes B3 [concrete(B1, B2), symbolic(B3), simplification(40)]
+
+    rule [bytes-concat-substr]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) => substrBytes(A, I0, J1)
+      requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A)
+      [simplification, preserves-definedness]
+    rule [bytes-concat-substr-cxt]: substrBytes(A, I0, J0) +Bytes substrBytes(A, I1, J1) +Bytes B => substrBytes(A, I0, J1) +Bytes B
+      requires I0 <=Int J0 andBool I1 <=Int J1 andBool J0 ==Int I1 andBool J1 <=Int lengthBytes(A)
+      [simplification, preserves-definedness]
 ```
 
 ## Bytes Update Lemmas

src/tests/integration/test-data/specs/bytes-concat-consecutive.k

@@ -0,0 +1,14 @@
+module BYTES-CONCAT-CONSECUTIVE
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <pc> 0 </pc>
+    <mem>
+      #bytes(b"\x00\x00\x00\x00" +Bytes substrBytes(reverseBytes(VALUE), 0, 4) +Bytes substrBytes(reverseBytes(VALUE), 4, 8) +Bytes substrBytes(reverseBytes(VALUE), 8, 12) +Bytes substrBytes(reverseBytes(VALUE), 12, 16) +Bytes substrBytes(reverseBytes(VALUE), 16, 20) +Bytes substrBytes(reverseBytes(VALUE), 20, 24) +Bytes substrBytes(reverseBytes(VALUE), 24, 28) +Bytes substrBytes(reverseBytes(VALUE), 28, 32) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes 
+    =>
+    #bytes(b"\x00\x00\x00\x00" +Bytes reverseBytes(VALUE) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes
+    </mem>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires lengthBytes(VALUE) ==Int 32
+endmodule