From 93ecbebfaee7c7d9993ab1405cafdca1453c4140 Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Wed, 17 Jan 2024 11:12:03 +0000 Subject: [PATCH 01/14] refactoring new account generation to ensure definedness preservation --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 28 ++++++++++--------- 1 file changed, 15 insertions(+), 13 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 3b52d51e75..8180041cdf 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -748,10 +748,23 @@ These are just used by the other operators for shuffling local execution state a ```k syntax InternalOp ::= "#newAccount" Int | "#newExistingAccount" Int - | "#newFreshAccount" Int // -------------------------------------------- rule #newAccount ACCT => #newExistingAccount ACCT ... ACCT ... - rule #newAccount ACCT => #newFreshAccount ACCT ... [owise] + rule #newAccount ACCT => . ... + + ( .Bag + => + + ACCT + 0 + .Bytes:AccountCode + .Map + .Map + 0 + + ) + ... + [owise, preserves-definedness] rule #newExistingAccount ACCT => #end EVMC_ACCOUNT_ALREADY_EXISTS ... @@ -772,17 +785,6 @@ These are just used by the other operators for shuffling local execution state a ... requires lengthBytes(CODE) ==Int 0 - - rule #newFreshAccount ACCT => . ... - - ( .Bag - => - ACCT - ... - - ) - ... - ``` - `#transferFunds` moves money from one account into another, creating the destination account if it doesn't exist. From 87fcb45e8254586c819a7b0d39f6d4bd09b19ebb Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 17 Jan 2024 11:14:56 +0000 Subject: [PATCH 02/14] Set Version: 1.0.420 --- 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 d5616de63f..21af7e9585 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.418" +version = "1.0.420" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 4a35436369..7e14f4eba4 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.418' +VERSION: Final = '1.0.420' diff --git a/package/version b/package/version index 5d99d1d587..7bf92eee6c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.418 +1.0.420 From dda3a83471f5f2b50227cbb59f4a44708c5d3c14 Mon Sep 17 00:00:00 2001 From: devops Date: Wed, 17 Jan 2024 11:23:33 +0000 Subject: [PATCH 03/14] Set Version: 1.0.420 --- 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 5ec53a718a..21af7e9585 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.419" +version = "1.0.420" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 0e581f48cf..7e14f4eba4 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.419' +VERSION: Final = '1.0.420' diff --git a/package/version b/package/version index ae19aa4110..7bf92eee6c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.419 +1.0.420 From b687d231a8e706620025d7c10214754c31614c3c Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 18 Jan 2024 23:32:12 +0000 Subject: [PATCH 04/14] Set Version: 1.0.421 --- 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 21af7e9585..b3e013d8b8 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.420" +version = "1.0.421" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 7e14f4eba4..6b9cc3bc73 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.420' +VERSION: Final = '1.0.421' diff --git a/package/version b/package/version index 7bf92eee6c..8bbd18b2c0 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.420 +1.0.421 From c00dd37b73bfcef65c2395245b85ed539597fa0c Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 25 Jan 2024 13:36:02 +0000 Subject: [PATCH 05/14] Set Version: 1.0.432 --- 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 d5da3824cd..3c55a49ce1 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.431" +version = "1.0.432" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index b9eedbc0a3..29758917ac 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.431' +VERSION: Final = '1.0.432' diff --git a/package/version b/package/version index 5414b84116..49f963031e 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.431 +1.0.432 From 65d729d7ffe352055a404018ee4a39748f2c9b8f Mon Sep 17 00:00:00 2001 From: devops Date: Tue, 30 Jan 2024 09:03:20 +0000 Subject: [PATCH 06/14] Set Version: 1.0.433 --- 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 3c55a49ce1..7bdb5e09a6 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.432" +version = "1.0.433" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 29758917ac..8e4ccb24f9 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.432' +VERSION: Final = '1.0.433' diff --git a/package/version b/package/version index 49f963031e..b2844ba7de 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.432 +1.0.433 From a80e62e5215ef478106f73111b2fa9eda4b11bcf Mon Sep 17 00:00:00 2001 From: devops Date: Mon, 5 Feb 2024 10:34:56 +0000 Subject: [PATCH 07/14] Set Version: 1.0.443 --- 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 1879e53f59..ded2755694 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.442" +version = "1.0.443" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index 19f978de4b..6e349f8a11 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.442' +VERSION: Final = '1.0.443' diff --git a/package/version b/package/version index 3a55179cd7..95bf08962a 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.442 +1.0.443 From 04da00e1f551c9c67a8f19c84421e4fdad3dc751 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 15 Feb 2024 06:22:20 +0000 Subject: [PATCH 08/14] Set Version: 1.0.457 --- 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 05a0fd0bcc..04e0488fa6 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.456" +version = "1.0.457" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index dab4a9082e..b6859c17f1 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.456' +VERSION: Final = '1.0.457' diff --git a/package/version b/package/version index 4916ca9848..ea0c147dcf 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.456 +1.0.457 From 253c6fa574250e60a408de8262d88e0f19d9dd97 Mon Sep 17 00:00:00 2001 From: devops Date: Sat, 24 Feb 2024 14:41:58 +0000 Subject: [PATCH 09/14] Set Version: 1.0.465 --- 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 42836d815c..41621facb5 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.464" +version = "1.0.465" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/kevm-pyk/src/kevm_pyk/__init__.py b/kevm-pyk/src/kevm_pyk/__init__.py index e84c42b0f0..1f16de7190 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.464' +VERSION: Final = '1.0.465' diff --git a/package/version b/package/version index 42d08cf19a..569c1a0b0c 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -1.0.464 +1.0.465 From 2e7a7702a5ecc60f9daa309c6e99610608dbdaab Mon Sep 17 00:00:00 2001 From: Petar Maksimovic Date: Sun, 25 Feb 2024 10:48:38 +0000 Subject: [PATCH 10/14] further annotations --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 2 ++ 1 file changed, 2 insertions(+) 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 fe622baa5b..8105513129 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -814,6 +814,7 @@ These are just used by the other operators for shuffling local execution state a ... requires ACCTFROM =/=K ACCTTO andBool VALUE <=Int ORIGFROM + [preserves-definedness] rule #transferFunds ACCTFROM _ACCTTO VALUE => #end EVMC_BALANCE_UNDERFLOW ... @@ -1367,6 +1368,7 @@ The various `CALL*` (and other inter-contract control flow) operations will be d ... ACCT |-> (TS:Set => TS |Set SetItem(INDEX)) ... SCHED requires Ghasaccesslist << SCHED >> + [preserves-definedness] rule #accessStorage ACCT INDEX => .K ... TS => TS[ACCT <- SetItem(INDEX)] From 36f8e92059c4eb5894c631f8cd7ccf568a035af6 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 26 Feb 2024 17:30:07 +0800 Subject: [PATCH 11/14] Bump SMT timeout to 500 in `test_pyk_prove` --- kevm-pyk/src/tests/integration/test_prove.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index fc10d65ba6..9e828c3110 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -227,7 +227,7 @@ def test_pyk_prove( definition_dir=definition_dir, includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], save_directory=use_directory, - smt_timeout=300, + smt_timeout=500, smt_retry_limit=10, md_selector='foo', # TODO Ignored flag, this is to avoid KeyError use_booster=use_booster, From be5f59e21309f60cf73fb84765527e8b3f748018 Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 26 Feb 2024 20:11:24 +0800 Subject: [PATCH 12/14] Increased the SMT timeout to 1800 in `test_pyk_prove` to make `kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k` pass --- kevm-pyk/src/tests/integration/test_prove.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 9e828c3110..b709a74229 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -227,7 +227,7 @@ def test_pyk_prove( definition_dir=definition_dir, includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], save_directory=use_directory, - smt_timeout=500, + smt_timeout=1800, smt_retry_limit=10, md_selector='foo', # TODO Ignored flag, this is to avoid KeyError use_booster=use_booster, From b25d52865243ed75396c7aa2dc842679b83a84fc Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Mon, 26 Feb 2024 22:02:16 +0800 Subject: [PATCH 13/14] Change SMT timeout in `test_pyk_prove` to 1600 --- kevm-pyk/src/tests/integration/test_prove.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index b709a74229..ce004cedb0 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -227,7 +227,7 @@ def test_pyk_prove( definition_dir=definition_dir, includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], save_directory=use_directory, - smt_timeout=1800, + smt_timeout=1600, smt_retry_limit=10, md_selector='foo', # TODO Ignored flag, this is to avoid KeyError use_booster=use_booster, From 5784c19668b9cca54a16fc320be061a929e9a2db Mon Sep 17 00:00:00 2001 From: palinatolmach Date: Tue, 27 Feb 2024 22:31:02 +0800 Subject: [PATCH 14/14] Revert SMT timeout to 300 in tests, skip `test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec` in Booster --- kevm-pyk/src/tests/integration/test_prove.py | 2 +- tests/failing-symbolic.haskell-booster | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index ce004cedb0..fc10d65ba6 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -227,7 +227,7 @@ def test_pyk_prove( definition_dir=definition_dir, includes=[str(include_dir) for include_dir in config.INCLUDE_DIRS], save_directory=use_directory, - smt_timeout=1600, + smt_timeout=300, smt_retry_limit=10, md_selector='foo', # TODO Ignored flag, this is to avoid KeyError use_booster=use_booster, diff --git a/tests/failing-symbolic.haskell-booster b/tests/failing-symbolic.haskell-booster index 6cc20db2ad..190f2e99ec 100644 --- a/tests/failing-symbolic.haskell-booster +++ b/tests/failing-symbolic.haskell-booster @@ -15,6 +15,7 @@ tests/specs/functional/lemmas-no-smt-spec.k tests/specs/functional/lemmas-spec.k tests/specs/functional/merkle-spec.k tests/specs/functional/storageRoot-spec.k +tests/specs/kontrol/test-arithmetictest-test_wmul_wdiv_inverse_underflow-uint256-uint256-0-spec.k tests/specs/mcd/dstoken-burn-self-fail-rough-spec.k tests/specs/mcd/dstoken-transferfrom-fail-rough-spec.k tests/specs/mcd/end-cash-pass-rough-spec.k