further smt lemmas removed

runtimeverification · Dec 26, 2024 · 8513c80 · 8513c80
1 parent 77d490c
commit 8513c80
Show file tree

Hide file tree

Showing 2 changed files with 12 additions and 8 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
@@ -145,10 +145,10 @@ module EVM-INT-SIMPLIFICATION
 
     rule [chop-resolve]: chop(I) => I requires #rangeUInt( 256 , I ) [simplification]
 
-    rule [chop-ub-lt]: X:Int  <Int chop(_V)             => true requires          X  <Int 0 [simplification]
-    rule [chop-ub-le]: X:Int <=Int chop(_V)             => true requires          X <=Int 0 [simplification]
-    rule [chop-lb-lt]:             chop(_V)  <Int X:Int => true requires maxUInt256  <Int X [simplification]
-    rule [chop-lb-le]:             chop(_V) <=Int X:Int => true requires maxUInt256 <=Int X [simplification]
+    rule [chop-ub-lt]:    X:Int  <Int chop(_V) => true requires          X  <Int 0 [simplification]
+    rule [chop-ub-le]:    X:Int <=Int chop(_V) => true requires          X <=Int 0 [simplification]
+    rule [chop-lb-lt]: chop(_V)  <Int X:Int    => true requires maxUInt256  <Int X [simplification]
+    rule [chop-lb-le]: chop(_V) <=Int X:Int    => true requires maxUInt256 <=Int X [simplification]
 
     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]

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
@@ -60,8 +60,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // ########################
 
     // Range
-    rule [b2w-lb]: 0 <=Int bool2Word(_)         => true [simplification, smt-lemma]
-    rule [b2w-ub]:         bool2Word(_) <=Int 1 => true [simplification, smt-lemma]
+    rule [b2w-lb-lt]:        X:Int  <Int bool2Word(_) => true requires X  <Int 0 [simplification]
+    rule [b2w-lb-le]:        X:Int <=Int bool2Word(_) => true requires X <=Int 0 [simplification]
+    rule [b2w-ub-lt]: bool2Word(_)  <Int X:Int        => true requires 1  <Int X [simplification]
+    rule [b2w-ub-le]: bool2Word(_) <=Int X:Int        => true requires 1 <=Int X [simplification]
 
     // Relationship with equality
     rule [b2w-eq-zero]: bool2Word(B) ==Int 0 => notBool B [simplification(30), comm]
@@ -118,8 +120,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
   // Map Reasoning
   // ########################
 
-    rule 0 <=Int #lookup( _M:Map , _ )             => true [simplification, smt-lemma]
-    rule         #lookup( _M:Map , _ ) <Int pow256 => true [simplification, smt-lemma]
+    rule [lookup-lb-lt]:                 X:Int  <Int #lookup( _M:Map , _ ) => true requires          X  <Int 0 [simplification]
+    rule [lookup-lb-le]:                 X:Int <=Int #lookup( _M:Map , _ ) => true requires          X <=Int 0 [simplification]
+    rule [lookup-ub-lt]: #lookup( _M:Map , _ )  <Int X:Int                 => true requires maxUInt256  <Int X [simplification]
+    rule [lookup-ub-le]: #lookup( _M:Map , _ ) <=Int X:Int                 => true requires maxUInt256 <=Int X [simplification]
 
     rule #lookup ( _M:Map [ K1 <- V1 ] , K2 )    => #lookup ( K1 |-> V1 , K1 ) requires K1 ==Int  K2 [simplification]
     rule #lookup (  M:Map [ K1 <- _  ] , K2 )    => #lookup ( M         , K2 ) requires notBool ( K1 ==Int K2 ) [simplification]