Add Byte simplification rules from evm semantics (#83)

Co-authored-by: Tamás Tóth <tothtamas28@users.noreply.github.com>
Co-authored-by: devops <devops@runtimeverification.com>

Author: 3 people

package/version

@@ -1 +1 @@
-0.1.62
+0.1.63

pyproject.toml

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

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

@@ -0,0 +1,48 @@
+# Bytes Simplifications
+
+## Preliminaries
+
+```k
+module BYTES-SIMPLIFICATIONS
+  imports BYTES
+  imports INT
+  imports K-EQUAL
+  imports BOOL
+```
+
+## Bytes Equality Lemmas
+
+```k
+  rule [bytes-not-equal-length]:
+    BA1:Bytes ==K BA2:Bytes => false
+    requires lengthBytes(BA1) =/=Int lengthBytes(BA2)
+    [simplification]
+    
+```
+
+## Bytes Concatenation Lemmas
+
+```k
+    rule [bytes-equal-concat-split-k]:
+      A:Bytes +Bytes B:Bytes ==K C:Bytes +Bytes D:Bytes => A ==K C andBool B ==K D
+      requires lengthBytes(A) ==Int lengthBytes(C)
+        orBool lengthBytes(B) ==Int lengthBytes(D)
+      [simplification]
+
+    rule [bytes-equal-concat-split-ml]:
+      { A:Bytes +Bytes B:Bytes #Equals C:Bytes +Bytes D:Bytes } => { A #Equals C } #And { B #Equals D }
+      requires lengthBytes(A) ==Int lengthBytes(C)
+        orBool lengthBytes(B) ==Int lengthBytes(D)
+      [simplification]
+
+    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-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)]
+```
+
+```k
+endmodule
+```

src/kriscv/kdist/riscv-semantics/lemmas/lemmas.k

@@ -1,5 +1,7 @@
-requires "sparse-bytes-simplificaitons.md"
+requires "sparse-bytes-simplifications.md"
+requires "bytes-simplifications.md"
 
 module LEMMAS
   imports SPARSE-BYTES-SIMPLIFICATIONS
+  imports BYTES-SIMPLIFICATIONS
 endmodule

…s/lemmas/sparse-bytes-simplificaitons.md …s/lemmas/sparse-bytes-simplifications.mdsrc/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplificaitons.md renamed to src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplificaitons.md renamed to src/kriscv/kdist/riscv-semantics/lemmas/sparse-bytes-simplifications.md

@@ -15,7 +15,7 @@ module SW-SPEC
     <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"\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>