Add new simplification rule for concatenating byte substrings in BYTES-SIMPLIFICATIONS and update ZKEVM-SSTORE test specification to include padding bytes.

Author: Stevengre

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

@@ -47,6 +47,9 @@ module BYTES-SIMPLIFICATIONS [symbolic]
     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/zkevm-sstore.k

@@ -5,9 +5,9 @@ module ZKEVM-SSTORE
     <instrs> #CHECK_HALT => #HALT </instrs>
     <pc> 0 </pc>
     <mem>
-      #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)) .SparseBytes 
+      #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(reverseBytes(VALUE)) .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