Add writeByteBF simplification rules (#82)

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

Author: Stevengre

package/version

@@ -1 +1 @@
-0.1.60
+0.1.61

pyproject.toml

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

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

@@ -21,6 +21,18 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _`
     requires I >=Int lengthBytes(B) [simplification(45)]
 ```
 
+
+## writeByteBF
+
+To write a byte to a symbolic sparse byte region, we need to:
+
+```k
+  rule writeByteBF(#bytes(B +Bytes BS) EF, I, V) => #bytes(B[ I <- V ] +Bytes BS) EF 
+    requires I >=Int 0 andBool I <Int lengthBytes(B) [simplification(45)]
+  rule writeByteBF(#bytes(B +Bytes BS) EF, I, V) => prepend(B, writeByteBF(#bytes(BS) EF, I -Int lengthBytes(B), V))
+    requires I >=Int lengthBytes(B) [simplification(45)]
+```
+
 ```k
 endmodule
 ```

src/tests/integration/test-data/specs/sw-spec.k

@@ -0,0 +1,26 @@
+requires "riscv-semantics/riscv.md"
+
+module SW-SPEC
+  imports RISCV
+
+  claim [id]:
+    <instrs> (.K => #HALT) ~> #EXECUTE ... </instrs>
+    <regs>
+      1 |-> W(12)
+      2 |-> W(24)
+      3 |-> W(28)
+      4 |-> W(4)
+    </regs>
+    <pc> W ( 0 => 8 ) </pc>
+    <mem>
+      #bytes ( b"\x23\xa0\x40\x00\x23\x20\x41\x00" )  // sw x4, 0(x1) ; sw x4, 0(x3)
+      #empty ( 4 )
+      (#bytes ( b"\x00\x00\x00\x00" +Bytes X +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00") =>
+       #bytes ( b"\x04\x00\x00\x00" +Bytes X +Bytes b"\x00\x00\x00\x00\x04\x00\x00\x00\x00\x00\x00\x00"))
+      .SparseBytes
+    </mem>
+    <test>
+      <haltCond> ADDRESS ( W ( 8 ) ) </haltCond>
+    </test>
+    requires lengthBytes(X) ==Int 4
+endmodule