From 3ea7ed50c059bfce2e3c76567477cff7070869df Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Petar=20Maksimovi=C4=87?= Date: Tue, 10 Sep 2024 19:23:01 +0200 Subject: [PATCH] Removing `#rangeBool` reasoning (#2616) * removing rangeBool reasoning * equality simplifications * reducing required lemmas * sum-to-n-foundry-spec --- .../kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 13 ++++--------- tests/specs/examples/sum-to-n-foundry-spec.k | 2 ++ 2 files changed, 6 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 24a07b8ffd..d2bf28faae 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 @@ -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 (B andBool C (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 50f0a1bc98..3a789b7d74 100644 --- 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]