#asWord simplifications (#2604)

* #asWord simplifications * undoing changes to slot updates * undoing changes to slot updates * correction * correction * redesigning unification lemmas * correction * correction * revisiting choices * minor corrections due to slot updates * re-adding tests * stabilising CI * alignment * alignment * alignment * alignment * alignment * correction * Update test-pr.yml * priority of bitwise normalizations * further tests * one more test * restrictions on lower priority simplifications * kevm-pyk/plugin: correct submodule * simplifying lemmas --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Everett Hildenbrandt <everett.hildenbrandt@gmail.com>
runtimeverification · Sep 17, 2024 · 9bfb537 · 9bfb537
1 parent 94bd37a
commit 9bfb537
Show file tree

Hide file tree

Showing 7 changed files with 189 additions and 116 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k
@@ -13,7 +13,7 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule A |Int 0 => A [simplification]
     rule A |Int A => A [simplification]
 
-    rule A |Int B => B |Int A [simplification(40), concrete(B), symbolic(A)]
+    rule A |Int B => B |Int A [simplification(30), symbolic(A), concrete(B)]
 
     rule  X |Int _  ==Int 0          => false requires 0 <Int X [simplification, concrete(X)]
     rule (A |Int B) ==Int (B |Int A) => true  [simplification, smt-lemma]
@@ -22,7 +22,7 @@ module BITWISE-SIMPLIFICATION [symbolic]
   // bit-and
   // ###########################################################################
 
-    rule A &Int B => B &Int A [symbolic(A), concrete(B), simplification]
+    rule A &Int B => B &Int A [simplification(30), symbolic(A), concrete(B)]
 
     rule 0 &Int _ => 0 [simplification]
     rule _ &Int 0 => 0 [simplification]
@@ -34,24 +34,26 @@ module BITWISE-SIMPLIFICATION [symbolic]
     rule [bitwise-or-lt-zero]:  (X |Int Y) <Int Z => false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification]
     rule [bitwise-and-lt-zero]: (X &Int Y) <Int Z => false requires 0 <=Int X andBool 0 <=Int Y andBool Z <=Int 0 [concrete(Z), simplification]
 
-    rule [bitwise-and-lt]:       (X &Int Y) <Int Z      => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z)          [simplification]
-    rule [bitwise-or-lt-pow256]: (X |Int Y) <Int pow256 => true requires 0 <=Int X andBool 0 <=Int Y andBool X <Int pow256 andBool Y <Int pow256 [simplification]
+    rule [bitwise-and-lt]: (X &Int Y) <Int Z => true requires 0 <=Int X andBool 0 <=Int Y andBool (X <Int Z orBool Y <Int Z) [simplification]
+
+    rule [bitwise-or-lt]:
+      (X |Int Y) <Int Z => true
+      requires 0 <=Int X andBool 0 <=Int Y andBool X <Int Z andBool Y <Int Z
+       andBool Z ==Int 2 ^Int ( log2Int( Z ) ) [simplification, concrete(Z)]
 
     // Generalization of: maxUIntXXX &Int Y => Y requires #rangeUInt(XXX, Y)
     rule [bitwise-and-maxUInt-identity]:
       X &Int Y => Y
-      requires 0 <=Int X
-       andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
+      requires 0 <=Int X andBool X +Int 1 ==Int 2 ^Int log2Int(X +Int 1)
        andBool 0 <=Int Y andBool Y <Int X +Int 1
-       [concrete(X), simplification, comm, preserves-definedness]
+       [simplification(40), concrete(X), preserves-definedness]
 
-    // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(XXX, Y)
+    // Generalization of: notMaxUIntXXX &Int Y => 0 requires #rangeUInt(256 -Int XXX, Y)
     rule [bitwise-and-notMaxUInt-zero]:
       X &Int Y => 0
-      requires #rangeUInt(256, X)
-       andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
+      requires #rangeUInt(256, X) andBool pow256 -Int X ==Int 2 ^Int ( log2Int ( pow256 -Int X ) )
        andBool 0 <=Int Y andBool Y <Int pow256 -Int X
-      [simplification, concrete(X), preserves-definedness]
+      [simplification(40), concrete(X), preserves-definedness]
 
     rule [notMaxUInt5-bit-and-nested]:
       notMaxUInt5 &Int ( ( notMaxUInt5 &Int X ) +Int Y ) => chop ( ( notMaxUInt5 &Int X ) +Int ( notMaxUInt5 &Int Y ) )

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
@@ -72,30 +72,6 @@ module BYTES-SIMPLIFICATION [symbolic]
        andBool #asWord(B) <Int 2 ^Int (8 *Int W)
       [simplification, concrete(W), preserves-definedness]
 
-    rule [buf-asWord-invert-rl]:
-      #asWord ( #buf ( WB:Int, X:Int ) ) => X
-      requires 0 <=Int WB andBool 0 <=Int X andBool
-               ( ( WB <=Int 32 andBool X <Int 2 ^Int (8 *Int WB) ) orBool
-                 ( WB  >Int 32 andBool X <Int pow256 ) )
-      [simplification, concrete(WB), preserves-definedness]
-
-    rule [buf-asWord-invert-rl-range]:
-      #asWord ( #range ( #buf ( WB:Int, X:Int ), S:Int, WR:Int ) ) => X
-      requires 0 <=Int WB andBool 0 <=Int X andBool 0 <=Int S andBool 0 <=Int WR
-       andBool S +Int WR ==Int WB
-       andBool X <Int 2 ^Int (8 *Int WR)
-      [simplification, concrete(WB, S, WR), preserves-definedness]
-
-    rule [asWord-trim-leading-zeros-concat]:
-      #asWord ( BZ +Bytes B ) => #asWord ( B )
-      requires #asInteger ( BZ ) ==Int 0
-      [simplification, concrete(BZ)]
-
-    rule [asWord-trim-overflowing-zeros]:
-      #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
-      requires 32 <Int lengthBytes(B)
-      [simplification]
-
     rule [buf-zero-concat-base]:
       #buf(W1:Int, 0) +Bytes #buf(W2:Int, 0) => #buf(W1 +Int W2, 0)
       requires 0 <=Int W1 andBool 0 <=Int W2
@@ -244,24 +220,6 @@ module BYTES-SIMPLIFICATION [symbolic]
       #range(#padRightToWidth(_, BUF), 0, WIDTH) => BUF
       requires lengthBytes(BUF) ==Int WIDTH [simplification]
 
-    rule [range-eq-check]:
-      BZ +Bytes #range ( B, S, W ) ==K B => true
-      requires 0 <=Int S andBool 0 <=Int W
-      andBool lengthBytes( B ) ==Int S +Int W
-      andBool #asInteger( BZ ) ==Int 0
-      andBool lengthBytes( BZ ) ==Int S
-      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
-
-    rule [range-eq-check-ml]:
-      { BZ +Bytes #range ( B, S, W ) #Equals B } => #Top
-      requires 0 <=Int S andBool 0 <=Int W
-      andBool lengthBytes( B ) ==Int S +Int W
-      andBool #asInteger( BZ ) ==Int 0
-      andBool lengthBytes( BZ ) ==Int S
-      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-      [simplification, concrete(BZ, S, W), comm, preserves-definedness]
-
     // Memory update
 
     rule [memUpdate-is-empty]:
@@ -301,15 +259,7 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule [lengthBytes-leq-zero]: lengthBytes(B:Bytes) <=Int 0 => B ==K .Bytes [simplification]
 
-    // #asWord
-
-    rule #asWord(WS) >>Int M => #asWord(#range(WS, 0, lengthBytes(WS) -Int (M /Int 8) ))
-      requires 0 <=Int M andBool M modInt 8 ==Int 0
-      [simplification, preserves-definedness]
-
-    // This simplification needs to be generalised properly
-    rule notMaxUInt224 &Int #asWord(#padRightToWidth(32, BUF)) => #asWord(#padRightToWidth(32, BUF))
-      requires lengthBytes(BUF) <=Int 4 [simplification]
+    // #padToWidth
 
     rule #padToWidth(32, #asByteStack(V)) => #buf(32, V)  requires #rangeUInt(256, V) [simplification]
 

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k
@@ -1,17 +1,10 @@
 requires "evm-types.md"
 
 module EVM-INT-SIMPLIFICATION
-    imports EVM-INT-SIMPLIFICATION-HASKELL
-endmodule
-
-module EVM-INT-SIMPLIFICATION-HASKELL [symbolic]
-    imports EVM-INT-SIMPLIFICATION-COMMON
-endmodule
-
-module EVM-INT-SIMPLIFICATION-COMMON
-    imports INT
     imports BOOL
+    imports BUF
     imports EVM-TYPES
+    imports INT
     imports WORD
 
   // ###########################################################################
@@ -57,31 +50,91 @@ module EVM-INT-SIMPLIFICATION-COMMON
   // #asWord
   // ###########################################################################
 
-  rule [asWord-lb]: 0 <=Int #asWord(_WS)     => true [simplification, smt-lemma]
-  rule [asWord-ub]: #asWord(_WS) <Int pow256 => true [simplification, smt-lemma]
-
-  rule [asWord-lt]:
-    #asWord ( BA ) <Int X => true
-    requires 2 ^Int ( 8 *Int lengthBytes(BA) ) <=Int X
-    [concrete(X), simplification]
-
-  rule [asWord-lt-concat]:
-    #asWord ( BA1 +Bytes BA2 ) <Int X => #asWord ( BA1 ) <Int ( X -Int #asWord ( BA2 ) ) /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
-    requires ( X -Int #asWord ( BA2 ) ) modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) ) ==Int 0
-    [concrete(BA2, X), simplification, preserves-definedness]
-
-  rule [asWord-lt-range]:
-    #asWord ( #range ( _:Bytes, S, W ) ) <Int X => true
-    requires 0 <=Int S andBool 0 <=Int W
-     andBool 2 ^Int ( 8 *Int W ) <=Int X
-    [simplification, concrete(S, W, X), preserves-definedness]
-
-  rule [lt-asWord-range]:
-    X <Int #asWord ( #range ( B:Bytes, S, W ) ) => X <Int #asWord ( B )
+  // Unification: two `#asWord`s
+  rule [asWord-eq-asWord]:
+    #asWord ( B1 ) ==Int #asWord ( B2 ) => #buf ( 32 -Int lengthBytes(B1), 0 ) +Bytes B1 ==K #buf ( 32 -Int lengthBytes(B2), 0 ) +Bytes B2
+    requires lengthBytes(B1) <=Int 32 andBool lengthBytes(B2) <=Int 32
+    [simplification, preserves-definedness]
+
+  // Unification: two `#asWord`s
+  rule [asWord-eq-asWord-ml]:
+    { #asWord ( B1 ) #Equals #asWord ( B2 ) } => { true #Equals #asWord ( B1 ) ==Int #asWord ( B2 ) }
+    [simplification, preserves-definedness]
+
+  // Unification: `#asWord` and concrete number
+  rule [asWord-eq-num]:
+    #asWord ( B:Bytes ) ==Int X:Int =>
+      0 <=Int X andBool X <Int 2 ^Int (8 *Int lengthBytes(B))
+                andBool B ==K #buf ( lengthBytes(B), X )
+    requires lengthBytes(B) <=Int 32
+    [simplification, concrete(X), comm, preserves-definedness]
+
+  // Unification: `#asWord` and concrete number
+  rule [asWord-eq-num-ml-l]: { #asWord ( B:Bytes ) #Equals X:Int } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness]
+  rule [asWord-eq-num-ml-r]: { X:Int #Equals #asWord ( B:Bytes ) } => { true #Equals #asWord ( B:Bytes ) ==K X:Int } [simplification, concrete(X), preserves-definedness]
+
+  // Reduction: we can always remove leading zeros
+  rule [asWord-trim-leading-zeros]:
+    #asWord ( BZ +Bytes B ) => #asWord ( B )
+    requires #asInteger ( BZ ) ==Int 0
+    [simplification(40), concrete(BZ), preserves-definedness]
+
+  // Reduction: we can always ignore content beyond 32 bytes
+  rule [asWord-trim-overflowing]:
+    #asWord ( B ) => #asWord ( #range(B, lengthBytes(B) -Int 32, 32) )
+    requires 32 <Int lengthBytes(B)
+    [simplification(40), preserves-definedness]
+
+  // Reduction: `#range` can be ignored under certain conditions
+  rule [asWord-range]:
+    #asWord ( #range ( B:Bytes, S, W ) ) => #asWord ( B )
     requires 0 <=Int S andBool 0 <=Int W
+     andBool lengthBytes(B) <=Int 32
      andBool lengthBytes(B) ==Int S +Int W
      andBool #asWord ( B ) <Int 2 ^Int ( 8 *Int W )
-    [simplification, concrete(X, S, W), preserves-definedness]
+    [simplification, concrete(S, W), preserves-definedness]
+
+  // Reduction: `#asWord` inverts `#buf` under certain conditions
+  rule [asWord-buf-inversion]:
+    #asWord ( #buf ( WB:Int, X:Int ) ) => X
+    requires 0 <=Int WB andBool 0 <=Int X andBool X <Int minInt ( 2 ^Int (8 *Int WB), pow256 )
+    [simplification, concrete(WB), preserves-definedness]
+
+  // Reduction: bitwise right shift in terms of `#range`
+  rule [asWord-shr]:
+    #asWord( BA ) >>Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( N /Int 8 ) ) )
+    requires 0 <=Int N andBool N modInt 8 ==Int 0
+    [simplification, concrete(N), preserves-definedness]
+
+  // Reduction: division in terms of `#range`
+  rule [asWord-div]:
+    #asWord( BA ) /Int N => #asWord ( #range ( BA, 0, lengthBytes( BA ) -Int ( log2Int( N ) /Int 8 ) ) )
+    requires 0 <Int N andBool N ==Int 2 ^Int log2Int ( N ) andBool log2Int( N ) modInt 8 ==Int 0
+     andBool lengthBytes ( BA ) <=Int 32
+    [simplification, preserves-definedness]
+
+  // Comparison: `#asWord` is always in the range `[0, pow256)`
+  rule [asWord-lb]: 0 <=Int #asWord( _ )     => true [simplification, smt-lemma]
+  rule [asWord-ub]: #asWord( _ ) <Int pow256 => true [simplification, smt-lemma]
+
+  // Comparison: `#asWord(B)` is certainly less than something that does not fit into `lengthBytes(B)` bytes
+  rule [asWord-lt]:  #asWord ( B )  <Int X:Int => true  requires   2 ^Int (8 *Int minInt(32, lengthBytes(B)))          <=Int X [simplification, preserves-definedness]
+  // Comparison: `#asWord(B)` is certainly less than or equal to something that is not less than the max number fitting into `lengthBytes(B)` bytes
+  rule [asWord-le]:  #asWord ( B ) <=Int X:Int => true  requires ( 2 ^Int (8 *Int minInt(32, lengthBytes(B))) -Int 1 ) <=Int X [simplification, preserves-definedness]
+
+  // Comparison: `#asWord` of `+Bytes` when lower bytes match, with `<Int`
+  rule [asWord-concat-lt]:
+    #asWord ( BA1 +Bytes BA2 ) <Int X:Int => #asWord ( BA1 ) <Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+    requires #asWord ( BA2 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+     andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32
+    [simplification, concrete(BA2, X), preserves-definedness]
+
+  // Comparison: `#asWord` of `+Bytes` when lower bytes match, with `<=Int`
+  rule [asWord-concat-le]:
+    #asWord ( BA1 +Bytes BA2 ) <=Int X:Int => #asWord ( BA1 ) <=Int X /Int ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+    requires #asWord ( BA2 ) ==Int X modInt ( 2 ^Int ( 8 *Int lengthBytes ( BA2 ) ) )
+     andBool lengthBytes ( BA1 +Bytes BA2 ) <=Int 32
+    [simplification, concrete(BA2, X), preserves-definedness]
 
   // ###########################################################################
   // chop

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -194,14 +194,6 @@ module LEMMAS-HASKELL [symbolic]
     imports EVM
     imports BUF
 
-  // ########################
-  // Word Reasoning
-  // ########################
-
-    rule #asWord(BUF) /Int D => #asWord(#range(BUF, 0, lengthBytes(BUF) -Int log256Int(D)))
-       requires 0 <Int D andBool D <Int pow256 andBool D ==Int 256 ^Int log256Int(D)
-        andBool log256Int(D) <=Int lengthBytes(BUF) [simplification, preserves-definedness]
-
   // ########################
   // Arithmetic
   // ########################

diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k
@@ -17,8 +17,6 @@ module VERIFICATION-COMMON
 
     rule         #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => 0    requires         #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
     rule 0  <Int #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
-    rule 0 <=Int #asWord(#ecrec(_   , _   , _   , _   ))             => true                                                      [simplification]
-    rule         #asWord(#ecrec(_   , _   , _   , _   )) <Int pow160 => true                                                      [simplification]
 
     rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
      requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]

diff --git a/tests/specs/examples/storage-spec.md b/tests/specs/examples/storage-spec.md
@@ -26,7 +26,7 @@ requires "storage-bin-runtime.k"
 
 module VERIFICATION
     imports EDSL
-    imports LEMMAS
+    imports LEMMAS-WITHOUT-SLOT-UPDATES
     imports EVM-OPTIMIZATIONS
     imports STORAGE-VERIFICATION