Streamlining #asWord simplifications (#2301)

* streamlining #asWord simplifications * Set Version: 1.0.456 * alternative approach * Set Version: 1.0.457 * Added `buf-asWord-invert` test claim; fixed a typo * Set Version: 1.0.458 * more general claim --------- Co-authored-by: devops <[email protected]> Co-authored-by: Palina Tolmach <[email protected]>
runtimeverification · Feb 20, 2024 · fbacafc · fbacafc
1 parent 88c6735
commit fbacafc
Show file tree

Hide file tree

Showing 7 changed files with 21 additions and 9 deletions.
diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kevm-pyk"
-version = "1.0.457"
+version = "1.0.458"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
@@ -6,4 +6,4 @@
     from typing import Final
 
 
-VERSION: Final = '1.0.457'
+VERSION: Final = '1.0.458'
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
@@ -66,8 +66,9 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     rule [buf-asWord-invert-rl]:
       #asWord ( #buf ( WB:Int, X:Int ) ) => X
-      requires 0 <=Int WB andBool WB <=Int 32
-       andBool 0 <=Int X  andBool X <Int 2 ^Int (WB *Int 8)
+      requires 0 <=Int WB andBool 0 <=Int X andBool
+               ( ( WB <=Int 32 andBool X <Int 2 ^Int (WB *Int 8) ) orBool
+                 ( WB  >Int 32 andBool X <Int pow256 ) )
       [simplification, concrete(WB)]
 
     rule [buf-asWord-invert-rl-range]:

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
@@ -57,6 +57,9 @@ 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 ( lengthBytes(BA) *Int 8) <=Int X

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
@@ -61,9 +61,6 @@ module LEMMAS [symbolic]
 
     rule #isPrecompiledAccount(#newAddr(_, _), _) => false [simplification]
 
-    rule 0 <=Int #asWord(_WS)             => true [simplification]
-    rule         #asWord(_WS) <Int pow256 => true [simplification]
-
   // ########################
   // Keccak
   // ########################

diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.457
+1.0.458
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
@@ -391,7 +391,7 @@ module LEMMAS-SPEC
     claim <k> runLemma ( 160 ==Int #asWord ( #buf( 4, 160 ) +Bytes ( #range( #buf( 32 , _BUF ), 0, 28 ) ) ) >>Int 224 )
            => doneLemma( true ) ... </k>
 
- // buffer range sinplification
+ // buffer range simplification
  // ---------------------------
     claim <k> runLemma  ( #range((#buf(DATA_LEN, DATA) +Bytes _BUF), 0, DATA_LEN) )
            => doneLemma ( #range( #buf(DATA_LEN, DATA)             , 0, DATA_LEN) ) ... </k>
@@ -614,6 +614,17 @@ module LEMMAS-SPEC
           ) ... </k>
         requires #rangeUInt(32, VV0_x_114b9705)
 
+ // #asWord
+ // ----------------
+
+    claim [buf-asWord-invert]:
+      <k> runLemma(
+            #asWord ( #buf ( 63 , lengthBytes ( VV0_data_114b9705:Bytes ) ) ) <=Int maxUInt64
+          ) => doneLemma(
+            true
+          ) ... </k>
+        requires lengthBytes ( VV0_data_114b9705:Bytes ) <=Int 1073741824
+
  // ecrecover
  // ---------
Original file line number	Diff line number	Diff line change
Expand Up		@@ -6,4 +6,4 @@
		from typing import Final


		VERSION: Final = '1.0.457'
		VERSION: Final = '1.0.458'