Memory update simplifications (#2634)

* memory update simplifications from Kontrol * removing unneeded lemma * Revert "removing unneeded lemma" This reverts commit e1aa638.
runtimeverification · Oct 8, 2024 · ad5bce8 · ad5bce8
1 parent 22bd433
commit ad5bce8
Show file tree

Hide file tree

Showing 2 changed files with 28 additions and 15 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bytes-simplification.k
@@ -227,27 +227,35 @@ module BYTES-SIMPLIFICATION [symbolic]
       requires S <Int 0
       [simplification]
 
-    rule [memUpdate-as-concat-inside]:
-      B1:Bytes [ S:Int := B2:Bytes ] =>
-        #range(B1, 0, S) +Bytes B2 +Bytes #range (B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2)))
-      requires 0 <=Int S andBool S +Int lengthBytes(B2) <Int lengthBytes(B1)
-      [simplification(60)]
+    rule [memUpdate-concat-in-left]: (B1 +Bytes B2) [ S := B ] => (B1 [ S := B ]) +Bytes B2
+      requires 0 <=Int S andBool S +Int lengthBytes(B) <=Int lengthBytes(B1)
+      [simplification(40)]
 
-    rule [memUpdate-as-concat-outside-1]:
-      B1:Bytes [ S:Int := B2:Bytes ] => #range(B1, 0, S) +Bytes B2
-      requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2)
-      [simplification(60)]
+    rule [memUpdate-concat-in-right]: (B1 +Bytes B2) [ S := B ] => B1 +Bytes (B2 [ S -Int lengthBytes(B1) := B ])
+      requires lengthBytes(B1) <=Int S
+      [simplification(40)]
 
     rule [memUpdate-reorder]:
-      B:Bytes [ S1:Int := B1:Bytes] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ]
+      B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ] [ S1 := B1 ]
       requires 0 <=Int S2 andBool S2 <Int S1 andBool S2 +Int lengthBytes(B2) <=Int S1
       [simplification]
 
     rule [memUpdate-subsume]:
-      B:Bytes [ S1:Int := B1:Bytes] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ]
+      B:Bytes [ S1:Int := B1:Bytes ] [ S2:Int := B2:Bytes ] => B [ S2 := B2 ]
       requires 0 <=Int S2 andBool S2 <=Int S1 andBool S1 +Int lengthBytes(B1) <=Int S2 +Int lengthBytes(B2)
       [simplification]
 
+    rule [memUpdate-as-concat-inside]:
+      B1:Bytes [ S:Int := B2:Bytes ] =>
+        #range(B1, 0, S) +Bytes B2 +Bytes #range(B1 , S +Int lengthBytes(B2), lengthBytes(B1) -Int (S +Int lengthBytes(B2)))
+      requires 0 <=Int S andBool S +Int lengthBytes(B2) <Int lengthBytes(B1)
+      [simplification(60)]
+
+    rule [memUpdate-as-concat-outside]:
+      B1:Bytes [ S:Int := B2:Bytes ] => #range(B1, 0, S) +Bytes B2
+      requires 0 <=Int S andBool lengthBytes(B1) <=Int S +Int lengthBytes(B2)
+      [simplification(60)]
+
     // lengthBytes
 
     rule [lengthBytes-geq-zero]:   0 <=Int lengthBytes ( _ )                     => true                                     [simplification, smt-lemma]

diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
@@ -149,7 +149,7 @@ module LEMMAS-SPEC
       requires X =/=K Y
 
 
- // Buffer write simplifications
+ // Memory update simplifications
  // ----------------------------
 
     // claim <k> runLemma ( M [ L := .Bytes ] [ N := WS:Bytes ]                             ) => doneLemma ( M [ N := WS ]                        ) ... </k> requires L <=Int N
@@ -164,9 +164,14 @@ module LEMMAS-SPEC
     claim <k> runLemma( M:Bytes [ 32 := BA1 ] [ 32 := BA2 ]                                                                  ) => doneLemma(M [ 32 := BA2 ]                                                                ) ... </k> requires lengthBytes(BA1) <=Int lengthBytes(BA2)
     claim <k> runLemma( M:Bytes [ 32 := BA1 ] [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) => doneLemma(M [ 32 := #padToWidth(32, #asByteStack(#hashedLocation("Solidity", 2, OWNER))) ] ) ... </k> requires lengthBytes(BA1) ==Int 32 andBool #rangeUInt(256, OWNER)
 
-    // Memory write past the end of the buffer
-    claim [write-past-end]: <k> runLemma  ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] )
-                             => doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... </k>
+    claim [memUpdate-past-end]: <k> runLemma  ( #buf(160, A) [ 160 := #buf(32, B) ] [ 192 := #buf(32, C) ] [ 224 := #buf(32, D) ] [ 256 := #buf(32, E) ] )
+                                 => doneLemma ( #buf(160, A) +Bytes #buf(32, B) +Bytes #buf(32, C) +Bytes #buf(32, D) +Bytes #buf(32, E) ) ... </k>
+
+    claim [memUpdate-pinpoint]: <k> runLemma  ( ( B1 +Bytes B2 +Bytes B3 +Bytes B4 ) [ 70 := #buf(16, X:Int) ] )
+                                 => doneLemma ( ( B1 +Bytes B2 +Bytes ( B3 [ 10 := #buf(16, X:Int) ] ) +Bytes B4 ) ) ... </k>
+                                    requires lengthBytes(B1) ==Int 20
+                                     andBool lengthBytes(B2) ==Int 40
+                                     andBool lengthBytes(B3) ==Int 60
 
  // #lookup simplifications
  // -----------------------