From fbacafc3cc20dc9308cbbeaa8eeda24a38aaa8de Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Tue, 20 Feb 2024 12:45:27 +0000
Subject: [PATCH] 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 <devops@runtimeverification.com>
Co-authored-by: Palina Tolmach <polina.tolmach@gmail.com>
---
 kevm-pyk/pyproject.toml                             |  2 +-
 kevm-pyk/src/kevm_pyk/__init__.py                   |  2 +-
 .../evm-semantics/lemmas/bytes-simplification.k     |  5 +++--
 .../evm-semantics/lemmas/evm-int-simplification.k   |  3 +++
 .../kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k    |  3 ---
 package/version                                     |  2 +-
 tests/specs/functional/lemmas-spec.k                | 13 ++++++++++++-
 7 files changed, 21 insertions(+), 9 deletions(-)

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 04e0488fa6..2574b0a6bb 100644
--- 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. <contact@runtimeverification.com>",
diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py
index b6859c17f1..4e3e7884da 100644
--- 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
index 8a78afec06..20ffbfb5f6 100644
--- 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
index cf0ac74d80..cd4fd27078 100644
--- 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
index f92eb59c8e..e9abc747bb 100644
--- 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
index ea0c147dcf..ada8dd4208 100644
--- 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
index a1e0c931ea..53285744ce 100644
--- 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
  // ---------