Read symbolic value at symbolic address

package/version

@@ -1 +1 @@
-0.1.117
+0.1.118

pyproject.toml

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

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

@@ -26,6 +26,7 @@ module INT-SIMPLIFICATIONS [symbolic]
 
 ```k
   rule [chop-32bits]: X &Int 4294967295 => X requires 0 <=Int X andBool X <Int 4294967296 [simplification]
+  rule [chop-16bits]: X &Int 65535 => X requires 0 <=Int X andBool X <Int 65536 [simplification]
   rule [int-and-assoc]: (X &Int Y) &Int Z => X &Int (Y &Int Z) [simplification, symbolic(X), concrete(Y,Z)]
   rule [int-and-add-assoc-8]: ((X &Int 255) +Int Y) &Int 255 => (X +Int Y) &Int 255
     [simplification]

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

@@ -30,6 +30,41 @@ For symbolic execution, we need to tackle the patterns of `#bytes(B +Bytes _) _`
     requires I >=Int lengthBytes(B)                     [simplification(45), preserves-definedness]
 ```
 
+Simplification rules for pickFront and dropFront operations on symbolic write blocks (#WB)
+- Default case: For most symbolic write operations, we can bypass the #WB wrapper and apply pickFront directly to the underlying byte structure
+```k
+  rule pickFront(PICK, #WB(_, I, _, _, B:SparseBytes)) => pickFront(PICK, B) 
+    requires PICK <=Int I
+    [simplification(45)]
+```
+- Special case for zero-indexed writes: When a write starts at position 0, we must combine bytes from both the written value and the remaining underlying structure
+```k
+  rule pickFront(PICK, #WB(_, I, V, NUM, B:SparseBytes)) => Int2Bytes(minInt(PICK, NUM), V, LE) +Bytes pickFront(maxInt(0, PICK -Int NUM), B >>SparseBytes NUM)
+    requires 0 ==Int I [simplification(40)]
+```
+- Front-dropping with symbolic writes: Adjust both the write offset and apply dropFront to the underlying structure to maintain correct relative positioning
+```k
+  rule dropFront(DROP, #WB(FLAG, I, V, NUM, B:SparseBytes)) => #WB(FLAG, I -Int DROP, V, NUM, dropFront(DROP, B)) 
+    [simplification(45)]
+```
+
+## Right Shift Operations
+
+The `>>SparseBytes` operator performs a right shift operation on SparseBytes, effectively dropping the first N bytes from the sparse byte structure while maintaining the integer value semantics of the remaining bytes. Unlike `dropFront`, which simply removes N bytes from the beginning, `>>SparseBytes` performs a byte-level right shift that preserves the underlying integer representation of the data.
+
+This is primarily used in `pickFront` operations when we need to extract bytes from a specific offset within the sparse byte structure.
+
+```k
+  syntax SparseBytes ::= SparseBytes ">>SparseBytes" Int  [function, total]
+
+  // For concrete sparse bytes, we can directly use dropFront to simplify the operation
+  rule SBS >>SparseBytes SHIFT => dropFront(SHIFT, SBS) [concrete]
+
+  // Symbolic write case: Adjust the written value by right-shifting and recursively apply to underlying structure
+  rule #WB(FLAG, I, V, NUM, B:SparseBytes) >>SparseBytes SHIFT => #WB(FLAG, maxInt(0, I -Int SHIFT), V >>Int (SHIFT *Int 8), NUM, B >>SparseBytes SHIFT)
+    requires SHIFT >=Int 0 [simplification(45), preserves-definedness]
+```
+
 ## writeBytes
 
 If the write index is concrete, we can directly call `writeBytesBF` or `writeBytesEF`.
@@ -50,10 +85,11 @@ If the write index is symbolic, we use `#WB` to wrap the write operation. Unlike
 **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)]
+  rule #WB(_, I, _, NUM, B:SparseBytes) => B requires I <Int 0 orBool NUM <=Int 0 [simplification(40)]
+  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. 
@@ -76,7 +112,7 @@ The rule below handles a termination edge case: it immediately marks the operati
     requires I0 <=Int I1 andBool I1 +Int NUM1 <=Int I0 +Int NUM0  [simplification(45)]  
 ```
 
-## writeByteBF
+## writeBytesBF
 
 To write a byte to a symbolic sparse byte region, we need to:
 

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

@@ -0,0 +1,59 @@
+module READ-SYMBOLIC-INDEX-VALUE
+  imports RISCV
+
+  claim [id]:
+    <instrs> #CHECK_HALT => #HALT </instrs>
+    <regs>
+    // read from #bytes
+        1 |-> (readBytes(4, 4, 
+          #WB(true, I1, V0, 2,
+          #WB(true, I1, V1, 4,
+          #WB(true, I0, V2, 4,
+          #WB(true, I2, V3, 4, 
+          #bytes (b"\x00\x00\x00\x00" +Bytes Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))))
+          => V4)
+    // read I2 with same number of bytes
+        2 |-> (readBytes(I2, 4,
+          #WB(true, I1, V0, 2,
+          #WB(true, I1, V1, 4,
+          #WB(true, I0, V2, 4,
+          #WB(true, I2, V3, 4, 
+          #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))))
+          => V3)
+    // read I2 with smaller number of bytes
+        3 |-> (readBytes(I2, 2,
+          #WB(true, I1, V0, 2,
+          #WB(true, I1, V1, 4,
+          #WB(true, I0, V2, 4,
+          #WB(true, I2, V3, 4, 
+          #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))))
+          => V3 &Int 65535)
+    // DISALLOWED: read with more number of bytes (8 bytes, but only 4 stored) 
+    // read I1 with 2 bytes
+        4 |-> (readBytes(I1, 2,
+          #WB(true, I1, V0, 2,
+          #WB(true, I1, V1, 4,
+          #WB(true, I0, V2, 4,
+          #WB(true, I2, V3, 4, 
+          #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))))
+          => V0)
+    // read I1 with 4 bytes
+        5 |-> (readBytes(I1, 4,
+          #WB(true, I1, V0, 2,
+          #WB(true, I1, V1, 4,
+          #WB(true, I0, V2, 4,
+          #WB(true, I2, V3, 4, 
+          #bytes (Int2Bytes(4, V4, LE) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00") .SparseBytes)))))
+          => Bytes2Int(Int2Bytes(2, V0, LE) +Bytes Int2Bytes(2, V1 >>Int 16, LE), LE, Unsigned))
+    </regs>
+    <pc> 0 </pc>
+    <haltCond> ADDRESS ( 0 ) </haltCond>
+    requires 8 <Int I0 andBool I0 +Int 4 <Int I1 andBool I1 +Int 4 <Int I2
+    // values are within range
+    andBool  0 <=Int V0 andBool V0 <=Int 65535
+    andBool  0 <=Int V1 andBool V1 <=Int 4294967295
+    andBool  0 <=Int V2 andBool V2 <=Int 4294967295
+    andBool  0 <=Int V3 andBool V3 <=Int 4294967295
+    andBool  0 <=Int V4 andBool V4 <=Int 4294967295
+endmodule
+