Support for multimasks in slot updates (#2657)

* support for multimasks * syntax correction * test correction
runtimeverification · Dec 16, 2024 · 6cf2f54 · 6cf2f54
1 parent 3921a7a
commit 6cf2f54
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 2 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/slot-updates.k
@@ -25,10 +25,12 @@ module SLOT-UPDATES [symbolic]
     // SHIFT appropriate, and in the latter case, the slot will appear on the LHS of the |Int.
 
     // 1. Slot masking using &Int
-    rule [mask-b-and]:
+    rule [multimask-b-and]:
       MASK:Int &Int SLOT:Int =>
+        ( MASK |Int ( 2 ^Int ( 8 *Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) ) -Int 1 ) )
+          &Int
         #asWord ( #buf ( 32, SLOT ) [ 32 -Int ( #getMaskShiftBytes(MASK) +Int #getMaskWidthBytes(MASK) ) := #buf ( #getMaskWidthBytes(MASK), 0 ) ] )
-        requires #isMask(MASK) andBool #rangeUInt(256, SLOT)
+        requires 0 <=Int #getMaskShiftBytes(MASK) andBool 0 <=Int #getMaskWidthBytes(MASK) andBool #rangeUInt(256, SLOT)
         [simplification, concrete(MASK), preserves-definedness]
 
     // 2a. |Int and +Bytes, update to be done in left

diff --git a/tests/specs/functional/slot-updates-spec.k b/tests/specs/functional/slot-updates-spec.k
@@ -191,4 +191,17 @@ module SLOT-UPDATES-SPEC
       andBool notBool #asWord ( #range(BA, lengthBytes(BA) -Int (log2Int(X +Int 1) /Int 8), log2Int(X +Int 1) /Int 8) ) <=Int Y
       andBool X ==Int 2 ^Int ( 8 *Int 5 ) -Int 1 // 5 can be replaced by any number between 0 and 32
 
+    claim [slot-update-14]:
+      <k> runLemma (
+            #asWord ( #range (
+                        #buf ( 32 ,
+                               80750600743933639278906278912030932992000 |Int
+                               ( 664984632478924800 |Int
+                               ( 115792089237316195423570985008687885552524791327314281033844573408277819293695 &Int
+                               #asWord ( #range ( #buf ( 32 , #lookup ( STORAGE1:Map , 0 ) ) , 0 , 14 ) +Bytes
+                                         b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes
+                                         #range ( #buf ( 32 , #lookup ( STORAGE1:Map , 0 ) ) , 27 , 4 ) +Bytes b"\x02" ) ) ) ) ,
+                        31 , 1 ) ) <=Int 2 )
+          => doneLemma ( true ) ... </k>
+
 endmodule