From aa073fd05c8b609a0cacfa9d57a860d8fb44c056 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Sep 2024 15:10:17 +0200 Subject: [PATCH 1/3] generalising circularity --- tests/specs/examples/sum-to-n-foundry-spec.k | 7 +------ 1 file changed, 1 insertion(+), 6 deletions(-) diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k index 3a789b7d74..1dc2386cdd 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]: ... - requires 0 =Int N *Int 178 [circularity] - endmodule From 882e2ffe814c72549095cc91b0ce11e737296e8b Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 11 Sep 2024 15:15:17 +0200 Subject: [PATCH 2/3] removing unnecessary comm attribute --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 4 ++-- 1 file changed, 2 insertions(+), 2 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 (B andBool C Date: Wed, 11 Sep 2024 15:28:47 +0200 Subject: [PATCH 3/3] further streamlining --- tests/specs/examples/sum-to-n-foundry-spec.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/specs/examples/sum-to-n-foundry-spec.k b/tests/specs/examples/sum-to-n-foundry-spec.k index 1dc2386cdd..7a31d89d32 100644 --- a/tests/specs/examples/sum-to-n-foundry-spec.k +++ b/tests/specs/examples/sum-to-n-foundry-spec.k @@ -64,7 +64,7 @@ claim [foundry-sum-to-n-loop-invariant]: requires 0 <=Int N andBool 0 <=Int S - andBool #rangeUInt(256, S +Int ((N *Int (N +Int 1)) divInt 2)) + andBool S +Int ((N *Int (N +Int 1)) divInt 2) =Int N *Int 178 [circularity]