From 986f47b1338f16e98be295bce93e81e269e62b65 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 19 Nov 2024 13:13:57 +0000
Subject: [PATCH 1/3] support for multimasks

---
 .../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..5158dc535f 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 )
+
 endmodule

From 7b8757b439c528017ac575612c4810f1663022c1 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Tue, 19 Nov 2024 14:55:11 +0000
Subject: [PATCH 2/3] syntax correction

---
 tests/specs/functional/slot-updates-spec.k | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/tests/specs/functional/slot-updates-spec.k b/tests/specs/functional/slot-updates-spec.k
index 5158dc535f..18bda5d94c 100644
--- a/tests/specs/functional/slot-updates-spec.k
+++ b/tests/specs/functional/slot-updates-spec.k
@@ -202,6 +202,6 @@ module SLOT-UPDATES-SPEC
                                          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 )
+          => doneLemma ( true ) ... </k>
 
 endmodule

From b76a49e430f090c3743de2e9055be47709a3d22a Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Mon, 16 Dec 2024 16:15:03 +0000
Subject: [PATCH 3/3] test correction

---
 tests/specs/functional/slot-updates-spec.k | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/tests/specs/functional/slot-updates-spec.k b/tests/specs/functional/slot-updates-spec.k
index 18bda5d94c..6ea887822d 100644
--- a/tests/specs/functional/slot-updates-spec.k
+++ b/tests/specs/functional/slot-updates-spec.k
@@ -199,8 +199,8 @@ module SLOT-UPDATES-SPEC
                                ( 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" ) ) ) ) ,
+                                         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>