From a928ea0e9fa65282b77d8b4f2a46212f9f870c20 Mon Sep 17 00:00:00 2001
From: Petar Maksimovic <petar.maksimovic@runtimeverification.com>
Date: Thu, 26 Dec 2024 14:50:22 +0100
Subject: [PATCH] removing ecrec smt lemmas

---
 .../evm-semantics/lemmas/bytes-simplification.k      |  7 ++-----
 tests/specs/benchmarks/verification.k                | 12 ++++++------
 tests/specs/functional/lemmas-spec.k                 |  4 ++--
 3 files changed, 10 insertions(+), 13 deletions(-)

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 00ad215864..c8d111beec 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
@@ -279,10 +279,7 @@ module BYTES-SIMPLIFICATION [symbolic]
 
     // #ecrec
 
-    rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int 32 => true
-        [simplification, smt-lemma]
-
-    rule #asWord ( #ecrec ( _ , _ , _ , _ ) ) <Int pow160 => true
-        [simplification, smt-lemma]
+    rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int X:Int => true requires     32 <=Int X [simplification]
+    rule     #asWord ( #ecrec ( _ , _ , _ , _ ) )  <Int X:Int => true requires pow160 <=Int X [simplification]
 
 endmodule
diff --git a/tests/specs/benchmarks/verification.k b/tests/specs/benchmarks/verification.k
index dff254eb89..5968966aef 100644
--- a/tests/specs/benchmarks/verification.k
+++ b/tests/specs/benchmarks/verification.k
@@ -9,7 +9,7 @@ module VERIFICATION-COMMON
   // Ecrecover
   // ########################
 
-    //Symbolic predicate representing whether output of #ecrec is empty. No implementation.
+    // Symbolic predicate representing whether output of #ecrec is empty. No implementation.
     syntax Bool ::= #ecrecEmpty( Bytes , Bytes , Bytes , Bytes ) [function, no-evaluators, smtlib(ecrecEmpty)]
  // ----------------------------------------------------------------------------------------------------------
     rule lengthBytes(#ecrec(HASH, SIGV, SIGR, SIGS)) => 32 requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
@@ -18,11 +18,8 @@ module VERIFICATION-COMMON
     rule         #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => 0    requires         #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
     rule 0  <Int #asWord(#ecrec(HASH, SIGV, SIGR, SIGS))             => true requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
 
-    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
-     requires #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
-
-    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top
-     requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
+    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top requires notBool #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
+    rule #Ceil( #ecrec(HASH, SIGV, SIGR, SIGS) ) => #Top requires         #ecrecEmpty(HASH, SIGV, SIGR, SIGS) [simplification]
 
 endmodule
 
@@ -142,6 +139,9 @@ module VERIFICATION-HASKELL [symbolic]
 
     rule maxUInt160 &Int Y => Y requires 0 <=Int Y andBool Y <=Int maxUInt160 [simplification]
 
+    rule lengthBytes ( #ecrec ( _ , _ , _ , _ ) ) <=Int     32 => true [simplification, smt-lemma]
+    rule     #asWord ( #ecrec ( _ , _ , _ , _ ) )  <Int pow160 => true [simplification, smt-lemma]
+
     rule ( lengthBytes(#ecrec( HASH, SIGV, SIGR, SIGS )) ==Int 0  ) =>           #ecrecEmpty ( HASH, SIGV, SIGR, SIGS )  [simplification]
     rule ( lengthBytes(#ecrec( HASH, SIGV, SIGR, SIGS )) ==Int 32 ) => notBool ( #ecrecEmpty ( HASH, SIGV, SIGR, SIGS )) [simplification]
 
diff --git a/tests/specs/functional/lemmas-spec.k b/tests/specs/functional/lemmas-spec.k
index 58f2fb0983..5a16925e7c 100644
--- a/tests/specs/functional/lemmas-spec.k
+++ b/tests/specs/functional/lemmas-spec.k
@@ -811,8 +811,8 @@ module LEMMAS-SPEC
     claim [ecrec-range]: <k> runLemma  ( #rangeUInt ( 160 , #asWord ( #ecrec ( _ , _ , _ , _ ) ) ) )
                           => doneLemma ( true ) ... </k>
 
-    // claim [ecrec-mask]: <k> runLemma  ( #asWord ( #ecrec ( HASH , SIGV , SIGR , SIGS ) ) &Int maxUInt160 )
-    //                      => doneLemma ( #asWord ( #ecrec ( HASH , SIGV , SIGR , SIGS ) ) ) ... </k>
+    claim [ecrec-mask]: <k> runLemma  ( maxUInt160 &Int #asWord ( #ecrec ( HASH , SIGV , SIGR , SIGS ) ) )
+                         => doneLemma ( #asWord ( #ecrec ( HASH , SIGV , SIGR , SIGS ) ) ) ... </k>
 
  // Address computation
  // -------------------