Correcting the sum-to-n-foundry-spec.k circularity test (#2618)

* generalising circularity * removing unnecessary comm attribute * further streamlining
runtimeverification · Sep 11, 2024 · e20da98 · e20da98
1 parent 3ea7ed5
commit e20da98
Show file tree

Hide file tree

Showing 2 changed files with 4 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
@@ -91,8 +91,8 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic]
     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]
+    rule [b2w-rangeBool-eq-not-zero-l]: bool2Word (notBool (X ==Int 0)) => X requires #rangeBool(X) [simplification]
+    rule [b2w-rangeBool-eq-not-zero-r]: bool2Word (notBool (0 ==Int X)) => X requires #rangeBool(X) [simplification]
 
     // 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]

diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k
@@ -6,8 +6,6 @@ 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]
@@ -65,12 +63,9 @@ claim [foundry-sum-to-n-loop-invariant]:
     ...
   </kevm>
 
-  requires 0 <Int N
-   andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) divInt 2))
-   andBool #rangeUInt(256, N)
-   andBool #rangeUInt(256, S)
+  requires 0 <=Int N andBool 0 <=Int S
+   andBool S +Int ((N *Int (N +Int 1)) divInt 2) <Int pow256
    andBool GAS_AMT >=Int N *Int 178
   [circularity]
 
-
 endmodule