Stabilising chop lemmas (#2613)

* 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>
runtimeverification · Sep 10, 2024 · 43488bc · 43488bc
1 parent 6dee165
commit 43488bc
Show file tree

Hide file tree

Showing 2 changed files with 49 additions and 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
@@ -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
@@ -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
  // --------------------------