adding lemmas

runtimeverification · Sep 26, 2024 · 6466343 · 6466343
1 parent 8e98c87
commit 6466343
Showing 1 changed file with 2 additions and 1 deletion.
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
@@ -46,7 +46,8 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // Word Reasoning
   // ########################
 
-    rule 0 <=Int #sizeWordStack(_) => true [simplification]
+    rule 0 <=Int #sizeWordStack(_) => true                     [simplification, smt-lemma]
+    rule #sizeWordStack(_) <Int N  => false requires N <=Int 0 [simplification, smt-lemma]
 
     // #newAddr range
     rule 0 <=Int #newAddr(_,_)             => true   [simplification]