remove or fix lemmas that are now dead

runtimeverification · Mar 25, 2024 · 7662f4b · 7662f4b
1 parent 9ce02c7
commit 7662f4b
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 5 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k
@@ -39,7 +39,7 @@ module LEMMAS [symbolic]
   // Word Reasoning
   // ########################
 
-    rule 0 <=Int #sizeWordStack ( _ , N ) => true requires 0 <=Int N [simplification, smt-lemma]
+    rule 0 <=Int size( _:List ) => true [simplification, smt-lemma]
 
     // bool2Word range & simplification
     rule 0 <=Int bool2Word(_B)             => true   [simplification]

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/optimizations.md
@@ -10,10 +10,8 @@ requires "lemmas/int-simplification.k"
 module EVM-OPTIMIZATIONS-LEMMAS
   imports EVM
 
-    rule #sizeWordStack(WS           , N) => #sizeWordStack(WS, 0) +Int N requires N =/=Int 0                [simplification]
-    rule #sizeWordStack(WS [ I := _ ], N) => #sizeWordStack(WS, N)        requires I <Int #sizeWordStack(WS) [simplification]
-    rule 0 <=Int #sizeWordStack(_ , 0)    => true                                                            [simplification]
-    rule #sizeWordStack(_ , 0) <Int N     => false                        requires N <=Int 0                 [simplification]
+    rule 0 <=Int size(_:List)    => true                                                            [simplification]
+    rule size(_:List) <Int N     => false                        requires N <=Int 0                 [simplification]
 
 endmodule