Add simp rules for replaceAtBytes (#112)

Co-authored-by: devops <[email protected]>
Co-authored-by: Tamás Tóth <[email protected]>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.81
+0.1.82

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kriscv"
-version = "0.1.81"
+version = "0.1.82"
 description = "K tooling for the RISC-V architecture"
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

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

@@ -51,36 +51,40 @@ module BYTES-SIMPLIFICATIONS
   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]
+    [simplification, preserves-definedness]
   
   rule [multiple-bytes-update-symbolic-value]:
     replaceAtBytes(B, I, V) => substrBytes(B, 0, I) +Bytes V +Bytes substrBytes(B, I +Int lengthBytes(V), lengthBytes(B))
-    requires I +Int lengthBytes(V) <Int lengthBytes(B)
-    [simplification, concrete(B, I), symbolic(V), preserves-definedness]
+    requires I +Int lengthBytes(V) <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
 ```
 
 
-## Int2Bytes Lemmas
+## Length Bytes Lemmas
 
 ```k
-  rule [int2bytes-length]:
-    lengthBytes(Int2Bytes(N, _:Int, _:Endianness)) => N
+  rule [length-bytes-int2bytes]: lengthBytes(Int2Bytes(N, _:Int, _:Endianness)) => N 
+    [simplification]   
+  rule [length-bytes-substr]: lengthBytes(substrBytes(B, I, J)) => J -Int I
+    requires 0 <=Int I andBool I <=Int J andBool J <=Int lengthBytes(B)
+    [simplification, preserves-definedness]
+  rule [length-bytes-concat]: lengthBytes(A +Bytes B) => lengthBytes(A) +Int lengthBytes(B) 
     [simplification]
-
 ```
 
 ## substrBytes Lemmas
 
 ```k
-  rule [substr-bytes-length]: lengthBytes(substrBytes(B, I, J)) => J -Int I 
-    requires 0 <=Int I
-     andBool I <=Int J
-     andBool J <=Int lengthBytes(B)
-  [simplification, preserves-definedness]
   rule [substr-substr]: substrBytes(substrBytes(B, I, J), I0, J0) => substrBytes(B, I +Int I0, I +Int J0) 
     requires 0 <=Int I  andBool I  <=Int J  andBool J  <=Int lengthBytes(B)
      andBool 0 <=Int I0 andBool I0 <=Int J0 andBool J0 <=Int J -Int I
   [simplification, preserves-definedness]
+  rule [substr-bytes-eq-ij]: substrBytes(B, I, I) => b""
+    requires 0 <=Int I andBool I <=Int lengthBytes(B)
+  [simplification, preserves-definedness]
+  rule [substr-bytes-self]: substrBytes(B, 0, J) => B
+    requires J ==Int lengthBytes(B)
+    [simplification, preserves-definedness]
   rule [substr-concat-0]: substrBytes(A +Bytes _, I, J) => substrBytes(A, I, J)
     requires J <=Int lengthBytes(A)
     [simplification, preserves-definedness]

src/tests/integration/test-data/specs/bytes-int.k

@@ -7,16 +7,22 @@ module BYTES-INT
     <instrs> #CHECK_HALT => #HALT </instrs>
     <pc> W ( 0 ) </pc>
     <regs>
-     1 |-> (W(Bytes2Int (b"\x12\x34\x56\x78", LE, Unsigned) &Int 65280) => W(13312))
-     2 |-> (W(b"\x12\x34\x56\x78" [ 1 ] <<Int 8) => W(13312))
-     3 |-> (W(Bytes2Int (substrBytes(W0, 0, 4), LE, Unsigned ) &Int 65280) => W(W0 [ 1 ] <<Int 8))
-     4 |-> (W(Bytes2Int(substrBytes(b"\x01\x02", 0, 1), LE, Unsigned) &Int 65280) => W(0))
-     5 |-> (W(Bytes2Int(substrBytes(W0, 0, 1), LE, Unsigned) &Int 65280) => W(0))
-     6 |-> (W(Bytes2Int(substrBytes( W0 +Bytes b"\x12\x34\x56\x78", 0, 4), LE, Unsigned)) => W(Bytes2Int(substrBytes( W0, 0, 4), LE, Unsigned)))
-     7 |-> (W(Bytes2Int(substrBytes( W0 +Bytes b"\x01\x00\x00\x00", 32, 36), LE, Unsigned)) => W(1))
+     1  |-> (W(Bytes2Int (b"\x12\x34\x56\x78", LE, Unsigned) &Int 65280) => W(13312))
+     2  |-> (W(b"\x12\x34\x56\x78" [ 1 ] <<Int 8) => W(13312))
+     3  |-> (W(Bytes2Int (substrBytes(W0, 0, 4), LE, Unsigned ) &Int 65280) => W(W0 [ 1 ] <<Int 8))
+     4  |-> (W(Bytes2Int(substrBytes(b"\x01\x02", 0, 1), LE, Unsigned) &Int 65280) => W(0))
+     5  |-> (W(Bytes2Int(substrBytes(W0, 0, 1), LE, Unsigned) &Int 65280) => W(0))
+     6  |-> (W(Bytes2Int(substrBytes( W0 +Bytes b"\x12\x34\x56\x78", 0, 4), LE, Unsigned)) => W(Bytes2Int(substrBytes( W0, 0, 4), LE, Unsigned)))
+     7  |-> (W(Bytes2Int(substrBytes( W0 +Bytes b"\x01\x00\x00\x00", 32, 36), LE, Unsigned)) => W(1))
+     8  |-> (W(Bytes2Int(replaceAtBytes (W0 +Bytes W3 +Bytes b"\x00\x00\x00\x00" , 64 , b"\x02" ), LE, Unsigned)) => W(Bytes2Int ( W0:Bytes +Bytes W3:Bytes +Bytes b"\x02\x00\x00\x00" , LE , Unsigned )))
+     9  |-> (W(Bytes2Int(replaceAtBytes (b"\x00\x00", 0, b"\x01\x02"), LE, Unsigned)) => W(513))
+     10 |-> (W(Bytes2Int(replaceAtBytes (W1, 2, b"\x01\x02"), LE, Unsigned)) => W(Bytes2Int(substrBytes ( W1:Bytes , 0 , 2 ) +Bytes b"\x01\x02", LE, Unsigned)))
+     11 |-> (W(Bytes2Int(substrBytes(b"\x00", 1, 1), LE, Unsigned)) => W(0))
     </regs>
     <test>
       <haltCond> ADDRESS ( W ( 0 ) ) </haltCond>
     </test>
 requires lengthBytes(W0) ==Int 32
+ andBool lengthBytes(W1) ==Int 4
+ andBool lengthBytes(W3) ==Int 32
 endmodule