From 0c0e59d12c218e1ccc850eaaa1e4ac44f04e4128 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 10 Sep 2024 10:14:41 +0200 Subject: [PATCH 1/4] removing rangeBool reasoning --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 9 --------- 1 file changed, 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..b4799b5f26 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 // ######################## From 47aef48841a128fd77be90084891fb0ade24db84 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 10 Sep 2024 11:10:18 +0200 Subject: [PATCH 2/4] equality simplifications --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 10 ++++++++++ 1 file changed, 10 insertions(+) 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 b4799b5f26..23efbad911 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 @@ -90,6 +90,16 @@ 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-zero-l]: X ==Int bool2Word (X ==Int 0) => false requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-zero-r]: X ==Int bool2Word (0 ==Int X) => false requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-one-l]: X ==Int bool2Word (X ==Int 1) => true requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-one-r]: X ==Int bool2Word (1 ==Int X) => true requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-not-zero-l]: X ==Int bool2Word (notBool (X ==Int 0)) => true requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-not-zero-r]: X ==Int bool2Word (notBool (0 ==Int X)) => true requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-not-one-l]: X ==Int bool2Word (notBool (X ==Int 1)) => false requires #rangeBool(X) [simplification, comm] + rule [b2w-rangeBool-eq-not-one-r]: X ==Int bool2Word (notBool (1 ==Int X)) => false 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] From 0f5f3194f4ca9b251be473507622b600b77558c5 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Tue, 10 Sep 2024 15:24:14 +0200 Subject: [PATCH 3/4] reducing required lemmas --- .../src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 10 ++-------- 1 file changed, 2 insertions(+), 8 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 23efbad911..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 @@ -91,14 +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-zero-l]: X ==Int bool2Word (X ==Int 0) => false requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-zero-r]: X ==Int bool2Word (0 ==Int X) => false requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-one-l]: X ==Int bool2Word (X ==Int 1) => true requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-one-r]: X ==Int bool2Word (1 ==Int X) => true requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-not-zero-l]: X ==Int bool2Word (notBool (X ==Int 0)) => true requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-not-zero-r]: X ==Int bool2Word (notBool (0 ==Int X)) => true requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-not-one-l]: X ==Int bool2Word (notBool (X ==Int 1)) => false requires #rangeBool(X) [simplification, comm] - rule [b2w-rangeBool-eq-not-one-r]: X ==Int bool2Word (notBool (1 ==Int X)) => false requires #rangeBool(X) [simplification, comm] + 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 Date: Tue, 10 Sep 2024 17:59:02 +0200 Subject: [PATCH 4/4] sum-to-n-foundry-spec --- tests/specs/examples/sum-to-n-foundry-spec.k | 2 ++ 1 file changed, 2 insertions(+) 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]