Write symbolic value at symbolic index

package/version

@@ -1 +1 @@
-0.1.112
+0.1.113

pyproject.toml

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

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

@@ -30,6 +30,51 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _`
     requires I >=Int lengthBytes(B)                     [simplification(45), preserves-definedness]
 ```
 
+## writeBytes
+
+If the write index is concrete, we can directly call `writeBytesBF` or `writeBytesEF`.
+
+```k
+  rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification(45), concrete(I)]
+  rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification(45), concrete(I)]
+```
+
+If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike `writeBytes`, `#WB` contains a boolean value to determine whether the write operation has been completed. `true` means completed, `false` means not completed.
+
+```k
+  syntax SparseBytes ::= #WB(Bool, Int, Int, Int, SparseBytes) [function, total]
+  rule #WB(_, I, V, NUM, B:SparseBytes) => writeBytes(I, V, NUM, B)     [concrete]
+  rule writeBytes(I, V, NUM, B:SparseBytes) => #WB(false, I, V, NUM, B) [simplification]
+```
+
+**Termination Control**: The boolean flag ensures that symbolic write operations eventually terminate by transitioning from `false` to `true` state, at which point concrete write functions can be applied when the index becomes concrete.
+
+```k
+  rule #WB(false, I, V, NUM, BF:SparseBytesBF) => #WB(true, I, V, NUM, BF)    [simplification]
+  rule #WB(false, I, V, NUM, EF:SparseBytesEF) => #WB(true, I, V, NUM, EF)    [simplification]
+  rule #WB(true,  I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [simplification, concrete(I)]
+  rule #WB(true,  I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [simplification, concrete(I)]
+```
+
+**Reordering for Optimization**: When multiple `#WB` operations are nested, the rules bring incomplete `#WB` operations (with `false` flag) to the terminal position, allowing them to traverse and find all possible merge opportunities. 
+
+```k
+  rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I1, V1, NUM1, #WB(false, I0, V0, NUM0, B)) 
+    requires I0 +Int NUM0 <=Int I1 orBool I1 +Int NUM1 <=Int I0 [simplification]
+```
+
+The rule below handles a termination edge case: it immediately marks the operation as complete with reduced priority to avoid infinite rewriting cycles.
+
+```k
+  rule #WB(false, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B:SparseBytes)) => #WB(true, I0, V0, NUM0, #WB(true, I1, V1, NUM1, B)) [simplification(60)]
+```
+
+**Write Consolidation**: When multiple write operations target the same symbolic index with equal byte counts (`NUM0 == NUM1`), the rules merge them by eliminating the older write operation. When the new write has fewer bytes than the existing one (`NUM1 < NUM0`), the smaller write is also eliminated to maintain simplicity.
+
+```k
+  rule #WB(false, I0, V0, NUM0, #WB(_, I1, _, NUM1, B:SparseBytes)) => #WB(false, I0, V0, NUM0, B)
+    requires I0 <=Int I1 andBool I1 +Int NUM1 <=Int I0 +Int NUM0  [simplification(45)]  
+```
 
 ## writeByteBF
 

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

@@ -87,8 +87,8 @@ We provide helpers to prepend either data or an empty region to an existing `Spa
     | writeBytesEF(Int, Int, Int, SparseBytesEF) [function, total]
     | writeBytesBF(Int, Int, Int, SparseBytesBF) [function, total]
 
-  rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF)
-  rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF)
+  rule writeBytes(I, V, NUM, BF:SparseBytesBF) => writeBytesBF(I, V, NUM, BF) [concrete]
+  rule writeBytes(I, V, NUM, EF:SparseBytesEF) => writeBytesEF(I, V, NUM, EF) [concrete]
 
   rule writeBytesEF(I, _, _  , _           ) => .SparseBytes    requires I <Int 0 // error case for totality
   rule writeBytesEF(I, V, NUM, .SparseBytes) => prependEmpty(I, #bytes(Int2Bytes(NUM, V, LE)) .SparseBytes)    requires I >=Int 0

src/tests/integration/test-data/specs/store-symbolic-index-overlap-counter.k

@@ -0,0 +1,21 @@
+module STORE-SYMBOLIC-INDEX-OVERLAP-COUNTER
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+        .Map
+    </regs>
+    <pc> 0 </pc>
+    <mem>
+    // Perfect overlapping writes - I0's write completely covers I1's write
+    storeBytes(I0, V1, 2,
+    storeBytes(I1, V0, 1, #bytes ( b"\x00\x00" ) .SparseBytes))
+    => 
+    // Only I0's write remains since it completely covers I1's write
+    #WB(true, I0, V1, 2, #bytes ( b"\x00\x00" ) .SparseBytes)
+    </mem>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires // Perfect overlapping case: I1 is completely within I0's write range
+        I0 <=Int I1 andBool I1 +Int 1 <=Int I0 +Int 2 // I1's write [I1, I1+1) is within I0's write [I0, I0+2)
+endmodule 

src/tests/integration/test-data/specs/store-symbolic-index-partial-overlap.k

@@ -0,0 +1,22 @@
+module STORE-SYMBOLIC-INDEX-PARTIAL-OVERLAP
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+        .Map
+    </regs>
+    <pc> 0 </pc>
+    <mem>
+    // Partial overlapping writes - only part of the writes overlap
+    storeBytes(I0, V1, 2,
+    storeBytes(I1, V0, 2, #bytes ( b"\x00\x00\x00\x00" ) .SparseBytes))
+    => 
+    // Ordering is preserved
+    #WB(true, I0, V1, 2, 
+    #WB(true, I1, V0, 2, #bytes ( b"\x00\x00\x00\x00" ) .SparseBytes))
+    </mem>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires // Partial overlapping case: I0 starts 1 byte after I1, so they overlap by 1 byte
+        I0 ==Int I1 +Int 1 // I1 writes [I1, I1+2), I0 writes [I1+1, I1+3), overlap at [I1+1, I1+2)
+endmodule 

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

@@ -0,0 +1,33 @@
+module STORE-SYMBOLIC-INDEX-VALUE
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+        .Map
+    </regs>
+    <pc> 0 </pc>
+    <mem>
+    storeBytes(0 , V6, 4,
+    storeBytes(I2, V5, 4,
+    storeBytes(I1, V4, 2,
+    storeBytes(I0, V3, 4,
+    storeBytes(I2, V2, 2,
+    storeBytes(I1, V1, 4,
+    storeBytes(I0, V0, 4, #bytes ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) .SparseBytes)))))))
+    => // No way to simplify this without any information about the index. Just eliminate the writes on the same index.
+    #WB(true, I1, V4, 2,
+    #WB(true, I1, V1, 4,
+    #WB(true, I0, V3, 4,
+    #WB(true, I2, V5, 4, 
+    #bytes (Int2Bytes(4, V6, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes))))
+    </mem>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires // Ensure truly non-overlapping writes
+        // I0 writes 4 bytes [I0, I0+4), must not overlap with [0, 4)
+        4 <=Int I0 andBool
+        // I1 writes 4 bytes [I1, I1+4), must not overlap with I0 [I0, I0+4)
+        I0 +Int 4 <=Int I1 andBool
+        // I2 writes 4 bytes [I2, I2+4), must not overlap with I1 [I1, I1+4)
+        I1 +Int 4 <=Int I2
+endmodule