From 2f4336b66c03fccee1af65d2576a4c4801d50101 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Mon, 16 Dec 2024 19:23:15 +0000
Subject: [PATCH] Support for multimasks in slot updates (#2657)

* support for multimasks

* syntax correction

* test correction
---
 .../kproj/evm-semantics/lemmas/slot-updates.k       |  6 ++++--
 tests/specs/functional/slot-updates-spec.k          | 13 +++++++++++++
 2 files changed, 17 insertions(+), 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
index 4167371782..4ba193b550 100644
--- 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
index 5aa76302ef..6ea887822d 100644
--- 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