Add a new chop simplification lemma. (#2527)

* Add a new `chop` simplification lemma. This lemma is required to make `vow-fess-fail-rough` pass once the backend uses the SMT solver to evaluate and simplify expressions. What happens with the SMT solver is that some calls to `chop` are simplified away, but others aren't. This leads to a spurious branch because a `JUMPI` condition cannot be evaluated to `false` any more. The SMT solver loses information when applying `chop-idempotent`. For more context see [the slack discussion here](https://runtimeverification.slack.com/archives/CC360GUTG/p1721069197632439) and [here](https://runtimeverification.slack.com/archives/CC360GUTG/p1721062195080599?thread_ts=1721041777.289639&cid=CC360GUTG). * Set Version: 1.0.644 * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/evm-int-simplification.k Co-authored-by: Petar Maksimović <[email protected]> * rename chop-idempotent to chop-resolve --------- Co-authored-by: devops <[email protected]> Co-authored-by: Petar Maksimović <[email protected]>
runtimeverification · Jul 16, 2024 · d6d151b · d6d151b
1 parent aba19fb
commit d6d151b
Show file tree

Hide file tree

Showing 4 changed files with 9 additions and 4 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.643"
+version = "1.0.644"
 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
@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '1.0.643'
+VERSION: Final = '1.0.644'
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
@@ -87,11 +87,16 @@ module EVM-INT-SIMPLIFICATION-COMMON
   // chop
   // ###########################################################################
 
-    rule [chop-idempotent]:  chop(I) => I requires #rangeUInt( 256 , I ) [simplification]
+    rule [chop-resolve]:     chop(I) => I requires #rangeUInt( 256 , I ) [simplification]
     rule [chop-upper-bound]: 0 <=Int chop(_V)             => true        [simplification, smt-lemma]
     rule [chop-lower-bound]:         chop(_V) <Int pow256 => true        [simplification, smt-lemma]
 
     rule [chop-sum-left]:  chop ( chop ( X:Int ) +Int Y:Int ) => chop ( X +Int Y ) [simplification]
     rule [chop-sum-right]: chop ( X:Int +Int chop ( Y:Int ) ) => chop ( X +Int Y ) [simplification]
 
+    rule [chop-no-overflow-add]:
+      X:Int <=Int chop ( X +Int Y:Int ) => X +Int Y <Int pow256
+      requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
+      [simplification]
+
 endmodule
diff --git a/package/version b/package/version
@@ -1 +1 @@
-1.0.643
+1.0.644