From e20da98a12923dc57515eac6f988fdd18024b871 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Petar=20Maksimovi=C4=87?=
 <PetarMax@users.noreply.github.com>
Date: Wed, 11 Sep 2024 16:42:12 +0200
Subject: [PATCH] Correcting the `sum-to-n-foundry-spec.k` circularity test
 (#2618)

* generalising circularity

* removing unnecessary comm attribute

* further streamlining
---
 .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k     | 4 ++--
 tests/specs/examples/sum-to-n-foundry-spec.k             | 9 ++-------
 2 files changed, 4 insertions(+), 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
index d2bf28faae..0969d2574a 100644
--- 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
index 3a789b7d74..7a31d89d32 100644
--- 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