removing ecrec smt lemmas

runtimeverification · Dec 26, 2024 · a928ea0 · a928ea0
1 parent ed164b4
commit a928ea0
Show file tree

Hide file tree

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