From 43488bcd6164fd862fbba9269744066b27b60baa Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Tue, 10 Sep 2024 13:23:03 +0200
Subject: [PATCH] Stabilising `chop` lemmas (#2613)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* removing some unneeded lemmas

* first attempt at stabilising chop lemmas

* removing unused claim

* correction

* formatting

* corrections

* further corrections

* correction

* adding tests

---------

Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com>
---
 .../lemmas/evm-int-simplification.k           | 36 +++++++++++++++----
 tests/specs/functional/lemmas-spec.k          | 19 ++++++++++
 2 files changed, 49 insertions(+), 6 deletions(-)

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 6c2e39931c..a4c168fbb2 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
@@ -91,12 +91,36 @@ module EVM-INT-SIMPLIFICATION-COMMON
     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
+    rule [chop-add-left]:  chop ( chop ( X:Int ) +Int Y:Int ) => chop ( X +Int Y ) [simplification]
+    rule [chop-add-right]: chop ( X:Int +Int chop ( Y:Int ) ) => chop ( X +Int Y ) [simplification]
+    rule [chop-mul-left]:  chop ( chop ( X:Int ) *Int Y:Int ) => chop ( X *Int Y ) [simplification]
+    rule [chop-mul-right]: chop ( X:Int *Int chop ( Y:Int ) ) => chop ( X *Int Y ) [simplification]
+
+    rule [chop-add-r-pos]:
+      chop ( X:Int +Int Y:Int ) ==Int 0 => X ==Int chop ( pow256 -Int chop ( Y ) )
+      requires #rangeUInt(256, X) andBool 0 <=Int Y
+      [simplification, concrete(Y), comm]
+
+    rule [chop-add-r-neg]:
+      chop ( X:Int +Int Y:Int ) ==Int 0 => X ==Int (-1) *Int Y
+      requires #rangeUInt(256, X) andBool #rangeUInt(256, (-1) *Int Y)
+      [simplification, concrete(Y), comm]
+
+    rule [chop-zero-sub]:
+      chop ( 0 -Int X:Int ) ==Int Y:Int => X ==Int chop ( pow256 -Int Y )
       requires #rangeUInt(256, X) andBool #rangeUInt(256, Y)
-      [simplification]
+      [simplification, concrete(Y), comm]
+
+    rule [chop-no-overflow-add-le-l]: X:Int <=Int chop ( X +Int Y:Int )        => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
+    rule [chop-no-overflow-add-le-r]: X:Int <=Int chop ( Y:Int +Int X )        => X +Int Y <Int pow256 requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) [simplification]
+    rule [chop-no-overflow-mul-le-l]: X:Int <=Int chop ( X *Int Y:Int ) /Int Y => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y           [simplification, preserves-definedness]
+    rule [chop-no-overflow-mul-le-r]: X:Int <=Int chop ( Y:Int *Int X ) /Int Y => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y           [simplification, preserves-definedness]
+    rule [chop-no-overflow-mul-eq-l]: X:Int ==Int chop ( X *Int Y:Int ) /Int Y => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y           [simplification, preserves-definedness, comm]
+    rule [chop-no-overflow-mul-eq-r]: X:Int ==Int chop ( Y:Int *Int X ) /Int Y => X *Int Y <Int pow256 requires #rangeUInt(256, X) andBool 0 <Int Y           [simplification, preserves-definedness, comm]
+
+    rule [chop-no-overflow-mul-eq-ml-ll]: { X #Equals chop ( X *Int Y ) /Int Y } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]
+    rule [chop-no-overflow-mul-eq-ml-rl]: { X #Equals chop ( Y *Int X ) /Int Y } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]
+    rule [chop-no-overflow-mul-eq-ml-lr]: { chop ( X *Int Y ) /Int Y #Equals X } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]
+    rule [chop-no-overflow-mul-eq-ml-rr]: { chop ( Y *Int X ) /Int Y #Equals X } => { true #Equals X *Int Y <Int pow256 } requires #rangeUInt(256, X) andBool 0 <Int Y [simplification, preserves-definedness]
 
 endmodule
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index 63a130b656..0f9cd2517a 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -404,6 +404,25 @@ module LEMMAS-SPEC
           ) => doneLemma ( false ) ... </k>
     requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) andBool #rangeUInt(256, C)
 
+    claim [chop-sub-01]: <k> runLemma ( chop ( X -Int Y ) ) => doneLemma ( X -Int Y ) ... </k>
+      requires #rangeUInt(256, X) andBool #rangeUInt(256, Y) andBool Y <=Int X
+
+    claim [chop-mul-01]: <k> runLemma ( chop ( X *Int Y ) ) => doneLemma ( X *Int Y ) ... </k>
+      requires 0 <=Int X andBool X <Int 2 ^Int 96
+       andBool 0 <=Int Y andBool Y <Int 2 ^Int ( 256 -Int 96 )
+
+    claim [chop-add-sub-conc]: <k> runLemma ( chop ( 0 -Int chop ( X +Int (-16)) ) ==Int 0 ) => doneLemma ( false ) ... </k>
+      requires 0 <=Int X andBool X <Int 10
+
+    claim [chop-overflow-01]: <k> runLemma ( X:Int <=Int chop ( X +Int Y:Int ) ) => doneLemma ( true ) ... </k>
+      requires #rangeUInt(128, X) andBool #rangeUInt(128, Y)
+
+    claim [chop-overflow-02]: <k> runLemma ( X:Int <=Int chop ( X *Int Y:Int ) /Int Y ) => doneLemma ( true ) ... </k>
+      requires #rangeUInt(128, X) andBool #rangeUInt(128, Y)
+
+    claim [chop-overflow-03]: <k> runLemma ( X:Int ==Int chop ( X *Int Y:Int ) /Int Y ) => doneLemma ( false ) ... </k>
+      requires pow128 <=Int X andBool X <Int pow256 andBool pow256 <=Int Y
+
  // #padToWidth simplification
  // --------------------------