Add simplification rule for storing symbolic bytes (#85)

Co-authored-by: devops <devops@runtimeverification.com>

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.66
+0.1.67

pyproject.toml

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

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

@@ -37,12 +37,33 @@ module BYTES-SIMPLIFICATIONS
 
     rule [bytes-concat-empty-right]: B:Bytes +Bytes .Bytes  => B [simplification]
     rule [bytes-concat-empty-left]:   .Bytes +Bytes B:Bytes => B [simplification]
+    rule [bytes-concat-concrete-empty-right]: B:Bytes +Bytes b"" => B [simplification]
+    rule [bytes-concat-concrete-empty-left]:   b"" +Bytes B:Bytes => B [simplification]
 
     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)]
 ```
 
+## Bytes Update Lemmas
+
+```k
+  rule [bytes-update-symbolic-value]:
+    B:Bytes [I <- V] => substrBytes(B, 0, I) +Bytes Int2Bytes(1, V, LE) +Bytes substrBytes(B, I +Int 1, lengthBytes(B) -Int I -Int 1)
+    requires I <Int lengthBytes(B)
+    [simplification, concrete(B, I), symbolic(V), preserves-definedness]
+```
+
+
+## Int2Bytes Lemmas
+
+```k
+  rule [int2bytes-length]:
+    lengthBytes(Int2Bytes(N, _:Int, _:Endianness)) => N
+    [simplification]
+
+```
+    
 ```k
 endmodule
 ```

src/tests/integration/test-data/specs/store-symbolic-bytes.k

@@ -0,0 +1,25 @@
+requires "riscv-semantics/riscv.md"
+
+module STORE-SYMBOLIC-BYTES
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+        .Map
+    </regs>
+    <pc> W ( 0 ) </pc>
+    <mem>
+    storeBytes(
+        #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes, 
+        W(0), 
+        X:Int,
+        4
+    ) =>
+    #bytes ( Int2Bytes ( 1 , X:Int &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 >>Int 8 &Int 255 , LE ) +Bytes Int2Bytes ( 1 , X:Int >>Int 8 >>Int 8 >>Int 8 , LE ) +Bytes b"\x00\x00\x00\x00" ) .SparseBytes
+    </mem>
+    <test>
+      <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>
+    </test>
+requires lengthBytes(W0) ==Int 4
+endmodule