From d6d151b8351921e6048843d590fc0e9649ed4a3a Mon Sep 17 00:00:00 2001
From: Jost Berthold <jost.berthold@gmail.com>
Date: Tue, 16 Jul 2024 21:15:10 +1000
Subject: [PATCH] Add a new `chop` simplification lemma. (#2527)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* 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ć <PetarMax@users.noreply.github.com>

* rename chop-idempotent to chop-resolve

---------

Co-authored-by: devops <devops@runtimeverification.com>
Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
---
 kevm-pyk/pyproject.toml                                    | 2 +-
 kevm-pyk/src/kevm_pyk/__init__.py                          | 2 +-
 .../kproj/evm-semantics/lemmas/evm-int-simplification.k    | 7 ++++++-
 package/version                                            | 2 +-
 4 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml
index 9074a6af41..9e2444ceab 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.643"
+version = "1.0.644"
 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 caaad3e3ed..e46253fd7d 100644
--- 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
index b8793ee89f..d528af8986 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
@@ -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
index b9f0f10a3e..fd0e1c0467 100644
--- a/package/version
+++ b/package/version
@@ -1 +1 @@
-1.0.643
+1.0.644