From 1a865c09caecd085006837b1df6cdb3798c7471a Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sat, 23 Dec 2023 00:53:55 +0000 Subject: [PATCH 1/8] kproj/evm: avoid generating cell fragments --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 83a4c833b3..1b30969ff0 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -203,13 +203,13 @@ The `callStack` cell stores a list of previous VM execution states. syntax InternalOp ::= "#pushCallStack" // -------------------------------------- rule #pushCallStack => . ... - STACK => ListItem(CALLSTATE) STACK + STACK => ListItem( CALLSTATE ) STACK CALLSTATE syntax InternalOp ::= "#popCallStack" // ------------------------------------- rule #popCallStack => . ... - ListItem(CALLSTATE) REST => REST + ListItem( CALLSTATE ) REST => REST _ => CALLSTATE syntax InternalOp ::= "#dropCallStack" @@ -227,22 +227,22 @@ The `interimStates` cell stores a list of previous world states. - `#dropWorldState` removes the top element of the `interimStates`. ```k - syntax Accounts ::= "{" AccountsCellFragment "|" SubstateCellFragment "}" - // ------------------------------------------------------------------------- + syntax Accounts ::= "{" AccountsCell "|" SubstateCell "}" + // --------------------------------------------------------- syntax InternalOp ::= "#pushWorldState" // --------------------------------------- rule #pushWorldState => .K ... - STATES => ListItem({ ACCTDATA | SUBSTATE }) STATES - ACCTDATA - SUBSTATE + STATES => ListItem({ ACCTDATA | SUBSTATE }) STATES + ACCTDATA + SUBSTATE syntax InternalOp ::= "#popWorldState" // -------------------------------------- rule #popWorldState => .K ... - ListItem({ ACCTDATA | SUBSTATE }) REST => REST - _ => ACCTDATA - _ => SUBSTATE + ListItem({ ACCTDATA | SUBSTATE }) REST => REST + _ => ACCTDATA + _ => SUBSTATE syntax InternalOp ::= "#dropWorldState" // --------------------------------------- From 42ef32d24a78c877e904964b5ddc37652237e1c0 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 Dec 2023 15:41:37 +0000 Subject: [PATCH 2/8] lemmas/bitwise-simplification, specs/int-simplifications-spec: add simplification for simple bitwise xor --- .../kproj/evm-semantics/lemmas/bitwise-simplification.k | 6 ++++++ tests/specs/functional/int-simplifications-spec.k | 4 ++++ 2 files changed, 10 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k index c857bb8da8..4dc151e1ce 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k @@ -87,6 +87,12 @@ module BITWISE-SIMPLIFICATION [symbolic] lengthBytes(X) +Int 32 >Int notMaxUInt5 &Int ( lengthBytes(X) +Int 31 ) => true [simplification, smt-lemma] + // ########################################################################### + // bit-xor + // ########################################################################### + + rule X xorInt Y false requires 0 <=Int X andBool 0 <=Int Y [simplification] + // ########################################################################### // shift // ########################################################################### diff --git a/tests/specs/functional/int-simplifications-spec.k b/tests/specs/functional/int-simplifications-spec.k index 2726b09f1f..7443b7e0d1 100644 --- a/tests/specs/functional/int-simplifications-spec.k +++ b/tests/specs/functional/int-simplifications-spec.k @@ -36,4 +36,8 @@ module INT-SIMPLIFICATIONS-SPEC runLemma ( minInt(_A +Int E, B +Int E) <=Int maxInt(_C +Int F, D +Int F) ) => doneLemma ( true ) ... requires B <=Int D andBool E <=Int F + claim [xor-maxuint256]: + runLemma ( notBool ( 0 -Int V0 <=Int V0 xorInt maxUInt256 ) ) => doneLemma ( false ) ... + requires #rangeUInt(96, V0) + endmodule From eaaac0c84bc712d0bf644697f6c1e26b9bafccd2 Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Sun, 24 Dec 2023 16:52:35 +0000 Subject: [PATCH 3/8] lemmas/int-simplification, specs/lemmas-spec: add simplifications for a bool2Word clause --- .../kproj/evm-semantics/lemmas/int-simplification.k | 7 +++++++ tests/specs/functional/lemmas-spec.k | 3 +++ 2 files changed, 10 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k index 18bae09b65..6b08c94d37 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/int-simplification.k @@ -243,4 +243,11 @@ module INT-SIMPLIFICATION-COMMON requires 0 true requires 0 <=Int X andBool X <=Int 0 [simplification, comm] + rule X ==Int 0 => false requires 0 runLemma ( bool2Word((UINT8 ==K 0) ==K false) ) => doneLemma ( UINT8 ) ... requires #rangeBool(UINT8) + claim [bool2Word-0]: runLemma ( bool2Word(X ==Int 0) ) => doneLemma ( 1 ) ... requires 0 <=Int X andBool X <=Int 0 + claim [bool2Word-1]: runLemma ( bool2Word(X ==Int 0) ) => doneLemma ( 0 ) ... requires 0 <=Int X andBool 0 Date: Tue, 9 Jan 2024 03:32:02 +0000 Subject: [PATCH 4/8] Set Version: 1.0.408 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 013e5fdad8..415790f84d 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.407" +version = "1.0.408" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 656dfe6f49..95c47455ac 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.407' +VERSION: Final = '1.0.408' diff --git a/package/version b/package/version index 481e49eb47..35734c07a6 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.407 +1.0.408 From 9d1328aea05da46f5148222d5bc033fb2aaf580f Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 9 Jan 2024 17:44:19 +0000 Subject: [PATCH 5/8] Set Version: 1.0.409 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 415790f84d..f19258e4c8 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.408" +version = "1.0.409" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 95c47455ac..d8c138911d 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.408' +VERSION: Final = '1.0.409' diff --git a/package/version b/package/version index 35734c07a6..302fcc8674 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.408 +1.0.409 From a668e48aa7721a28187d63cd03185c68799f35a5 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 10 Jan 2024 21:43:14 +0000 Subject: [PATCH 6/8] Set Version: 1.0.411 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 8e587cdf79..8790ae96a4 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.410" +version = "1.0.411" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 73880f470d..ad71417dc7 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.410' +VERSION: Final = '1.0.411' diff --git a/package/version b/package/version index 82d479aaf0..144afd4a20 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.410 +1.0.411 From 980998f012c9b637c5fa69ee677394c8d222185d Mon Sep 17 00:00:00 2001 From: Everett Hildenbrandt Date: Wed, 10 Jan 2024 22:42:54 +0000 Subject: [PATCH 7/8] lemmas/bitwise-simplification: generalize lemma --- .../kproj/evm-semantics/lemmas/bitwise-simplification.k | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k index 4dc151e1ce..3df2172acc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/bitwise-simplification.k @@ -91,7 +91,7 @@ module BITWISE-SIMPLIFICATION [symbolic] // bit-xor // ########################################################################### - rule X xorInt Y false requires 0 <=Int X andBool 0 <=Int Y [simplification] + rule X xorInt Y false requires 0 <=Int X andBool 0 <=Int Y andBool 0 <=Int Z [simplification] // ########################################################################### // shift From 00aedfb484c50d0c091a5da63833fd73fd2269eb Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 11 Jan 2024 08:19:52 +0000 Subject: [PATCH 8/8] Set Version: 1.0.413 --- kevm-pyk/pyproject.toml | 2 +- kevm-pyk/src/kevm_pyk/__init__.py | 2 +- package/version | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 7abd7970c9..94b8e1a206 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kevm-pyk" -version = "1.0.412" +version = "1.0.413" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index cc29c3b0e4..4be637f809 100644 --- a/kevm-pyk/src/kevm_pyk/__init__.py +++ b/kevm-pyk/src/kevm_pyk/__init__.py @@ -6,4 +6,4 @@ from typing import Final -VERSION: Final = '1.0.412' +VERSION: Final = '1.0.413' diff --git a/package/version b/package/version index 2b9c98c876..a72006d007 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.412 +1.0.413