minor update to slot updates to align with tutorial (#2647)

runtimeverification · Oct 17, 2024 · 84d4c63 · 84d4c63
1 parent 4a2692c
commit 84d4c63
Showing 1 changed file with 14 additions and 14 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
@@ -36,43 +36,43 @@ module SLOT-UPDATES [symbolic]
       A |Int #asWord ( B1 +Bytes B2 ) =>
         #asWord ( #buf ( 32 -Int lengthBytes(B2), (A /Int (2 ^Int (8 *Int lengthBytes(B2)))) |Int #asWord ( B1 ) ) +Bytes B2 )
         requires #rangeUInt(256, A) andBool A modInt (2 ^Int (8 *Int lengthBytes(B2))) ==Int 0 andBool lengthBytes(B1 +Bytes B2) <=Int 32
-        [simplification, preserves-definedness]
+        [simplification(40), comm, preserves-definedness]
 
     // 2b. |Int of +Bytes, update to be done in right
     rule [bor-update-to-right]:
       A |Int #asWord ( B1 +Bytes B2 ) =>
         #asWord ( B1 +Bytes #buf ( lengthBytes(B2), A |Int #asWord ( B2 ) ) )
         requires 0 <=Int A andBool A <Int 2 ^Int (8 *Int lengthBytes(B2)) andBool lengthBytes(B2) <=Int 32
-        [simplification, preserves-definedness]
+        [simplification(40), comm, preserves-definedness]
 
     // 3a. Update with explicit shift and symbolic slot
     rule [bor-update-with-shift]:
       ( SHIFT *Int X ) |Int Y => #asWord ( #buf( 32 -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, Y ) )
       requires #isByteShift(SHIFT)
        andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (32 -Int ( log2Int(SHIFT) /Int 8 )))
        andBool 0 <=Int Y andBool Y <Int SHIFT
-       [simplification, concrete(SHIFT), comm, preserves-definedness]
+       [simplification(42), concrete(SHIFT), comm, preserves-definedness]
 
-    // 3b. Buffer cropping
+    // 3b. Update with implicit shift and symbolic slot
+    rule [bor-update-without-shift]:
+      X |Int Y => #asWord ( #buf ( 32 -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) ) ) ) +Bytes
+                            #buf ( #getFirstOneBit(X) /Int 8, Y ) )
+      requires #rangeUInt(256, X) andBool 0 <=Int #getFirstOneBit(X)
+       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) )
+       [simplification(42), concrete(X), preserves-definedness]
+
+    // 4. Buffer cropping
     rule [buf-asWord-crop]:
       #buf (W:Int , #asWord(B:Bytes)) => #range(B, lengthBytes(B) -Int W, W)
       requires 0 <=Int W andBool W <=Int 32 andBool W <Int lengthBytes(B)
        andBool #asWord ( #range(B, 0, lengthBytes(B) -Int W) ) ==Int 0
       [simplification, concrete(W), preserves-definedness]
 
-    // 3c. Splitting the updated buffer into the updated value and the trailing zeros, explicit shift
-    rule [buf-split-l]:
+    // 5. Splitting the updated buffer into the updated value and the trailing zeros
+    rule [buf-split-on-shift]:
       #buf ( W, SHIFT *Int X ) => #buf( W -Int ( log2Int(SHIFT) /Int 8 ), X ) +Bytes #buf( log2Int(SHIFT) /Int 8, 0)
       requires 0 <=Int W andBool W <=Int 32 andBool #isByteShift(SHIFT)
        andBool 0 <=Int X andBool X <Int 2 ^Int (8 *Int (W -Int ( log2Int(SHIFT) /Int 8)))
        [simplification, concrete(W, SHIFT), preserves-definedness]
 
-    // 3d. Splitting the updated buffer into the updated value and the trailing zeros, implicit shift
-    rule [bor-split]:
-      X |Int Y => #asWord ( #buf ( 32 -Int #getFirstOneBit(X) /Int 8, X /Int ( 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) ) ) ) +Bytes
-                            #buf ( #getFirstOneBit(X) /Int 8, Y ) )
-      requires #rangeUInt(256, X) andBool 0 <=Int #getFirstOneBit(X)
-       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 8 *Int ( #getFirstOneBit(X) /Int 8 ) )
-       [simplification, concrete(X), preserves-definedness]
-
 endmodule