Removing #rangeBool reasoning (#2616)

* removing rangeBool reasoning * equality simplifications * reducing required lemmas * sum-to-n-foundry-spec
runtimeverification · Sep 10, 2024 · 3ea7ed5 · 3ea7ed5
1 parent 43488bc
commit 3ea7ed5
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 9 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
@@ -55,15 +55,6 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
 
     rule #isPrecompiledAccount(#newAddr(_, _), _) => false [simplification]
 
-  // ########################
-  // #rangeBool reasoning
-  // ########################
-
-    rule [rangeBool-not-zero-l]: notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
-    rule [rangeBool-not-zero-r]: notBool (0 ==Int X) => X ==Int 1 requires #rangeBool(X) [simplification]
-    rule [rangeBool-not-one-l]:  notBool (X ==Int 1) => X ==Int 0 requires #rangeBool(X) [simplification]
-    rule [rangeBool-not-one-r]:  notBool (1 ==Int X) => X ==Int 0 requires #rangeBool(X) [simplification]
-
   // ########################
   // bool2Word reasoning
   // ########################
@@ -99,6 +90,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
     rule [b2w-bxor-one]:            1  xorInt bool2Word(Y) => bool2Word(notBool Y)                                             [simplification, comm]
     rule [b2w-bxor]:      bool2Word(X) xorInt bool2Word(Y) => bool2Word ( (X andBool notBool Y) orBool (notBool X andBool Y) ) [simplification]
 
+    // Relationship with `#rangeBool`
+    rule [b2w-rangeBool-eq-not-zero-l]: bool2Word (notBool (X ==Int 0)) => X requires #rangeBool(X) [simplification, comm]
+    rule [b2w-rangeBool-eq-not-zero-r]: bool2Word (notBool (0 ==Int X)) => X requires #rangeBool(X) [simplification, comm]
+
     // As part of multiplication
     rule [b2w-mul-lt-l]: bool2Word(B) *Int C  <Int A => (B andBool C  <Int A) orBool (notBool B andBool 0  <Int A) [simplification]
     rule [b2w-mul-le-l]: bool2Word(B) *Int C <=Int A => (B andBool C <=Int A) orBool (notBool B andBool 0 <=Int A) [simplification]

diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k
@@ -6,6 +6,8 @@ module VERIFICATION
     imports INFINITE-GAS
     imports EVM
 
+    rule [rangeBool-not-zero-l]: notBool (X ==Int 0) => X ==Int 1 requires #rangeBool(X) [simplification]
+
     rule N xorInt maxUInt256 => maxUInt256 -Int N
     requires #rangeUInt(256, N)
     [simplification]