From b8c68febfc96232a8d0bcaac7f08ddb20bd53239 Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 12 Dec 2023 16:22:29 +0200 Subject: [PATCH 01/14] add suport for kevm nogas --- deps/kevm_release | 2 +- src/kontrol/__main__.py | 5 +++++ src/kontrol/options.py | 3 +++ src/kontrol/prove.py | 11 ++++++++++- 4 files changed, 19 insertions(+), 2 deletions(-) diff --git a/deps/kevm_release b/deps/kevm_release index 566c03b53..c559926ee 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.392 +nogas diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index 285f8e851..a3f67366f 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -209,6 +209,7 @@ def exec_prove( fail_fast: bool = False, port: int | None = None, maude_port: int | None = None, + use_gas: bool = True, **kwargs: Any, ) -> None: _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}') @@ -238,6 +239,7 @@ def exec_prove( max_iterations=max_iterations, run_constructor=run_constructor, fail_fast=fail_fast, + use_gas=use_gas, ) rpc_options = RPCOptions( @@ -673,6 +675,9 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: action='store_true', help='Include the contract constructor in the test execution.', ) + prove_args.add_argument( + '--no-gas', dest='use_gas', default=True, action='store_false', help='Disables gas computation.' + ) show_args = command_parser.add_parser( 'show', diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 7f472078a..11d810ac8 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -24,6 +24,7 @@ class ProveOptions: run_constructor: bool fail_fast: bool reinit: bool + use_gas: bool def __init__( self, @@ -41,6 +42,7 @@ def __init__( run_constructor: bool = False, fail_fast: bool = True, reinit: bool = False, + use_gas: bool = True, ) -> None: object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas) object.__setattr__(self, 'bug_report', bug_report) @@ -55,6 +57,7 @@ def __init__( object.__setattr__(self, 'run_constructor', run_constructor) object.__setattr__(self, 'fail_fast', fail_fast) object.__setattr__(self, 'reinit', reinit) + object.__setattr__(self, 'use_gas', use_gas) @dataclass(frozen=True) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 04b7492e5..6fb4fa370 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -12,7 +12,7 @@ from pyk.kast.manip import flatten_label, set_cell from pyk.kcfg import KCFG from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kbool import FALSE, notBool +from pyk.prelude.kbool import FALSE, TRUE, notBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlEqualsTrue from pyk.proof.proof import Proof @@ -204,6 +204,7 @@ def init_and_run_proof(test: FoundryTest) -> Proof: kcfg_explore=kcfg_explore, bmc_depth=prove_options.bmc_depth, run_constructor=prove_options.run_constructor, + use_gas=prove_options.use_gas, ) run_prover( @@ -237,6 +238,7 @@ def method_to_apr_proof( kcfg_explore: KCFGExplore, bmc_depth: int | None = None, run_constructor: bool = False, + use_gas: bool = True, ) -> APRProof | APRBMCProof: if Proof.proof_data_exists(test.id, foundry.proofs_dir): apr_proof = foundry.get_apr_proof(test.id) @@ -258,6 +260,7 @@ def method_to_apr_proof( test=test, kcfg_explore=kcfg_explore, setup_proof=setup_proof, + use_gas=use_gas, ) if bmc_depth is not None: @@ -298,6 +301,7 @@ def _method_to_initialized_cfg( kcfg_explore: KCFGExplore, *, setup_proof: APRProof | None = None, + use_gas: bool = True, ) -> tuple[KCFG, int, int]: _LOGGER.info(f'Initializing KCFG for test: {test.id}') @@ -307,6 +311,7 @@ def _method_to_initialized_cfg( test.contract, test.method, setup_proof, + use_gas, ) for node_id in new_node_ids: @@ -335,6 +340,7 @@ def _method_to_cfg( contract: Contract, method: Contract.Method | Contract.Constructor, setup_proof: APRProof | None, + use_gas: bool, ) -> tuple[KCFG, list[int], int, int]: calldata = None callvalue = None @@ -355,6 +361,7 @@ def _method_to_cfg( program=program, calldata=calldata, callvalue=callvalue, + use_gas=use_gas, ) new_node_ids = [] @@ -414,6 +421,7 @@ def _init_cterm( empty_config: KInner, contract_name: str, program: KInner, + use_gas: bool, *, setup_cterm: CTerm | None = None, calldata: KInner | None = None, @@ -429,6 +437,7 @@ def _init_cterm( ) init_subst = { 'MODE_CELL': KApply('NORMAL'), + 'USEGAS_CELL': TRUE if use_gas else FALSE, 'SCHEDULE_CELL': KApply('SHANGHAI_EVM'), 'STATUSCODE_CELL': KVariable('STATUSCODE'), 'CALLSTACK_CELL': KApply('.List'), From 0ba7b826b982434d91ca2e6e7fdd3b93c848202c Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 12 Dec 2023 16:32:48 +0200 Subject: [PATCH 02/14] hardcode use-gas for profiling --- src/kontrol/prove.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 6fb4fa370..7d9d867c9 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -12,7 +12,7 @@ from pyk.kast.manip import flatten_label, set_cell from pyk.kcfg import KCFG from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kbool import FALSE, TRUE, notBool +from pyk.prelude.kbool import FALSE, notBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlEqualsTrue from pyk.proof.proof import Proof @@ -437,7 +437,7 @@ def _init_cterm( ) init_subst = { 'MODE_CELL': KApply('NORMAL'), - 'USEGAS_CELL': TRUE if use_gas else FALSE, + 'USEGAS_CELL': FALSE, 'SCHEDULE_CELL': KApply('SHANGHAI_EVM'), 'STATUSCODE_CELL': KVariable('STATUSCODE'), 'CALLSTACK_CELL': KApply('.List'), From edae5e66f58cf4c15b30f6a005ab87fab6c39f8f Mon Sep 17 00:00:00 2001 From: Andrei Date: Tue, 12 Dec 2023 22:22:42 +0200 Subject: [PATCH 03/14] test --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index 65293540d..61779b48a 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.392", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "nogas", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" From 377ba45dce550dd37fc8c8497206da65089a4f62 Mon Sep 17 00:00:00 2001 From: devops Date: Fri, 15 Dec 2023 18:24:16 +0000 Subject: [PATCH 04/14] Set Version: 0.1.100 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 5c5330a6e..71fb8a1ce 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.99 +0.1.100 diff --git a/pyproject.toml b/pyproject.toml index 455f1c664..1428269fa 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.99" +version = "0.1.100" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 0be7b5a7b..8cbd7ec8d 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.99' +VERSION: Final = '0.1.100' From 40d31ddd06df20f52b9d3da9322cce5f199c228b Mon Sep 17 00:00:00 2001 From: devops Date: Sun, 17 Dec 2023 18:10:15 +0000 Subject: [PATCH 05/14] Set Version: 0.1.101 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 71fb8a1ce..3234805de 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.100 +0.1.101 diff --git a/pyproject.toml b/pyproject.toml index 1428269fa..4ccdbee9e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.100" +version = "0.1.101" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 8cbd7ec8d..5ffc4e07c 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.100' +VERSION: Final = '0.1.101' From 89b651885519b84e4decbb33a791e53d78b0f12b Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 20 Dec 2023 11:27:09 +0200 Subject: [PATCH 06/14] set kevm version tag --- deps/kevm_release | 2 +- pyproject.toml | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/deps/kevm_release b/deps/kevm_release index c559926ee..302d5deb2 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -nogas +1.0.397 diff --git a/pyproject.toml b/pyproject.toml index 4ccdbee9e..d6fa14cb9 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", branch = "nogas", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.397", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" From 921041735ce1849dae1dd6f03c14dd89ab3bfb76 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 20 Dec 2023 11:27:42 +0200 Subject: [PATCH 07/14] remove space --- pyproject.toml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyproject.toml b/pyproject.toml index d6fa14cb9..951c8e876 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.397", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.397", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" From 4214f09c38d3130f71ffab2601895cfa05b4c82d Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 20 Dec 2023 11:31:45 +0200 Subject: [PATCH 08/14] set use_gas to false by default --- src/kontrol/__main__.py | 6 +++--- src/kontrol/options.py | 6 +++--- src/kontrol/prove.py | 16 ++++++++-------- 3 files changed, 14 insertions(+), 14 deletions(-) diff --git a/src/kontrol/__main__.py b/src/kontrol/__main__.py index ca5c76b7c..b74e551d4 100644 --- a/src/kontrol/__main__.py +++ b/src/kontrol/__main__.py @@ -229,7 +229,7 @@ def exec_prove( fail_fast: bool = False, port: int | None = None, maude_port: int | None = None, - usegas: bool = True, + use_gas: bool = False, **kwargs: Any, ) -> None: _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}') @@ -259,7 +259,7 @@ def exec_prove( max_iterations=max_iterations, run_constructor=run_constructor, fail_fast=fail_fast, - usegas=usegas, + use_gas=use_gas, ) rpc_options = RPCOptions( @@ -727,7 +727,7 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]: help='Include the contract constructor in the test execution.', ) prove_args.add_argument( - '--no-gas', dest='usegas', default=True, action='store_false', help='Disables gas computation.' + '--use-gas', dest='use_gas', default=False, action='store_true', help='Enables gas computation in KEVM.' ) show_args = command_parser.add_parser( diff --git a/src/kontrol/options.py b/src/kontrol/options.py index 51034cc5a..1762be1f6 100644 --- a/src/kontrol/options.py +++ b/src/kontrol/options.py @@ -24,7 +24,7 @@ class ProveOptions: run_constructor: bool fail_fast: bool reinit: bool - usegas: bool + use_gas: bool def __init__( self, @@ -42,7 +42,7 @@ def __init__( run_constructor: bool = False, fail_fast: bool = True, reinit: bool = False, - usegas: bool = True, + use_gas: bool = False, ) -> None: object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas) object.__setattr__(self, 'bug_report', bug_report) @@ -57,7 +57,7 @@ def __init__( object.__setattr__(self, 'run_constructor', run_constructor) object.__setattr__(self, 'fail_fast', fail_fast) object.__setattr__(self, 'reinit', reinit) - object.__setattr__(self, 'usegas', usegas) + object.__setattr__(self, 'use_gas', use_gas) @dataclass(frozen=True) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index b7f9b0493..c18d7d015 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -204,7 +204,7 @@ def init_and_run_proof(test: FoundryTest) -> Proof: kcfg_explore=kcfg_explore, bmc_depth=prove_options.bmc_depth, run_constructor=prove_options.run_constructor, - usegas=prove_options.usegas, + use_gas=prove_options.use_gas, ) run_prover( @@ -239,7 +239,7 @@ def method_to_apr_proof( kcfg_explore: KCFGExplore, bmc_depth: int | None = None, run_constructor: bool = False, - usegas: bool = True, + use_gas: bool = False, ) -> APRProof | APRBMCProof: if Proof.proof_data_exists(test.id, foundry.proofs_dir): apr_proof = foundry.get_apr_proof(test.id) @@ -261,7 +261,7 @@ def method_to_apr_proof( test=test, kcfg_explore=kcfg_explore, setup_proof=setup_proof, - usegas=usegas, + use_gas=use_gas, ) if bmc_depth is not None: @@ -302,7 +302,7 @@ def _method_to_initialized_cfg( kcfg_explore: KCFGExplore, *, setup_proof: APRProof | None = None, - usegas: bool = True, + use_gas: bool = False, ) -> tuple[KCFG, int, int]: _LOGGER.info(f'Initializing KCFG for test: {test.id}') @@ -312,7 +312,7 @@ def _method_to_initialized_cfg( test.contract, test.method, setup_proof, - usegas, + use_gas, ) for node_id in new_node_ids: @@ -341,7 +341,7 @@ def _method_to_cfg( contract: Contract, method: Contract.Method | Contract.Constructor, setup_proof: APRProof | None, - usegas: bool, + use_gas: bool, ) -> tuple[KCFG, list[int], int, int]: calldata = None callvalue = None @@ -362,7 +362,7 @@ def _method_to_cfg( program=program, calldata=calldata, callvalue=callvalue, - usegas=usegas, + use_gas=use_gas, ) new_node_ids = [] @@ -422,7 +422,7 @@ def _init_cterm( empty_config: KInner, contract_name: str, program: KInner, - usegas: bool, + use_gas: bool, *, setup_cterm: CTerm | None = None, calldata: KInner | None = None, From 06f1f790356a02d00179f9bcd9eb6e890e2d9969 Mon Sep 17 00:00:00 2001 From: Andrei Date: Wed, 20 Dec 2023 11:35:49 +0200 Subject: [PATCH 09/14] Revert "hardcode use-gas for profiling" This reverts commit 0ba7b826b982434d91ca2e6e7fdd3b93c848202c. --- src/kontrol/prove.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index c18d7d015..250fc1dd7 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -12,7 +12,7 @@ from pyk.kast.manip import flatten_label, set_cell from pyk.kcfg import KCFG from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kbool import FALSE, notBool +from pyk.prelude.kbool import FALSE, TRUE, notBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlEqualsTrue from pyk.proof.proof import Proof @@ -438,7 +438,7 @@ def _init_cterm( ) init_subst = { 'MODE_CELL': KApply('NORMAL'), - 'USEGAS_CELL': FALSE, + 'USEGAS_CELL': TRUE if use_gas else FALSE, 'SCHEDULE_CELL': KApply('SHANGHAI_EVM'), 'STATUSCODE_CELL': KVariable('STATUSCODE'), 'CALLSTACK_CELL': KApply('.List'), From c9a80ce37b405c70fcc0255f18165f772243a7b2 Mon Sep 17 00:00:00 2001 From: rv-jenkins Date: Thu, 21 Dec 2023 11:02:56 -0700 Subject: [PATCH 10/14] Update dependency: deps/kevm_release (#253) * deps/kevm_release: Set Version 1.0.398 * Set Version: 0.1.101 * Sync Poetry files: kevm-pyk version 1.0.398 * deps/k_release: sync release file version 6.1.67 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.399 * Sync Poetry files: kevm-pyk version 1.0.399 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.400 * Sync Poetry files: kevm-pyk version 1.0.400 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.401 * Sync Poetry files: kevm-pyk version 1.0.401 * deps/k_release: sync release file version 6.1.69 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.402 * Sync Poetry files: kevm-pyk version 1.0.402 * deps/k_release: sync release file version 6.1.71 * flake.{nix,lock}: update Nix derivations * Set Version: 0.1.102 * deps/kevm_release: Set Version 1.0.403 * Sync Poetry files: kevm-pyk version 1.0.403 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.404 * Sync Poetry files: kevm-pyk version 1.0.404 * flake.{nix,lock}: update Nix derivations * deps/kevm_release: Set Version 1.0.405 * Sync Poetry files: kevm-pyk version 1.0.405 * flake.{nix,lock}: update Nix derivations * set USEGAS in init_term * update expected output * Sync Poetry files: kevm-pyk version 1.0.405 --------- Co-authored-by: devops Co-authored-by: Andrei --- deps/k_release | 2 +- deps/kevm_release | 2 +- flake.lock | 46 ++--- flake.nix | 2 +- package/version | 2 +- poetry.lock | 178 +++++++++--------- pyproject.toml | 4 +- src/kontrol/__init__.py | 2 +- src/kontrol/prove.py | 3 +- .../test-data/gas-abstraction.expected | 12 ++ ...ssertTest.testFail_assert_false().expected | 21 +++ ...AssertTest.testFail_assert_true().expected | 24 +++ ...sertTest.testFail_expect_revert().expected | 48 +++++ .../AssertTest.test_assert_false().expected | 24 +++ .../AssertTest.test_assert_true().expected | 21 +++ ...Test.test_failing_branch(uint256).expected | 36 ++++ ...st_revert_branch(uint256,uint256).expected | 36 ++++ ...ail_assume_false(uint256,uint256).expected | 18 ++ ...est_assume_false(uint256,uint256).expected | 30 +++ 19 files changed, 391 insertions(+), 120 deletions(-) diff --git a/deps/k_release b/deps/k_release index 65f6d2bc1..773066585 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -6.1.60 +6.1.71 diff --git a/deps/kevm_release b/deps/kevm_release index 302d5deb2..a0b345325 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.397 +1.0.405 diff --git a/flake.lock b/flake.lock index 16675c477..0a918aba7 100644 --- a/flake.lock +++ b/flake.lock @@ -72,17 +72,17 @@ ] }, "locked": { - "lastModified": 1702465848, - "narHash": "sha256-pikJMY8bJqbO+kTKGZiPRzspHcGJ6lFk/JytCUrm1yk=", + "lastModified": 1703078812, + "narHash": "sha256-Un3MXYKEm2tlOMbk8LSI98lQQIzp+LJFvXv8pyypcGU=", "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6e29375d4cbcfdeddf99e98f2ba7577db0cbf963", + "rev": "c6edfad1aa4c085e2cc2978c6d7cdc885157b0fb", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "hs-backend-booster", - "rev": "6e29375d4cbcfdeddf99e98f2ba7577db0cbf963", + "rev": "c6edfad1aa4c085e2cc2978c6d7cdc885157b0fb", "type": "github" } }, @@ -238,17 +238,17 @@ "z3": "z3" }, "locked": { - "lastModified": 1701950567, - "narHash": "sha256-e4A4dTW8GYQ0KPHcAb1PVaLXqGpKUJuQNJLlM7HO74Y=", + "lastModified": 1703063258, + "narHash": "sha256-wL5kFsbs6RS+bsrf+SDq85DDKce/sZZ7VQDtJZA5JS0=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "a5847301404583e16d55cd4d051b8e605d704fbc", + "rev": "ca05f14b7957fec9f2a5ab3444cae01c5a76f12f", "type": "github" }, "original": { "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "a5847301404583e16d55cd4d051b8e605d704fbc", + "rev": "ca05f14b7957fec9f2a5ab3444cae01c5a76f12f", "type": "github" } }, @@ -284,16 +284,16 @@ "rv-utils": "rv-utils" }, "locked": { - "lastModified": 1702579377, - "narHash": "sha256-SM7WOVRO15OabLdeYZjVf4feRv1LK6Hm/nhCUuJc48Q=", + "lastModified": 1703095402, + "narHash": "sha256-3Szh7B8Ui8/kGXMWywrbaARFJ5okvdE8vBJix3nsW6s=", "owner": "runtimeverification", "repo": "k", - "rev": "0b4353c62f018a46736dc6b512414b77ab81523d", + "rev": "3f547d5459b244c5e258231362c467d3ef50beb6", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v6.1.60", + "ref": "v6.1.71", "repo": "k", "type": "github" } @@ -337,16 +337,16 @@ ] }, "locked": { - "lastModified": 1702661104, - "narHash": "sha256-tiTfnsicKHPvJdp9pKPbAuN4OrgWQQeD6evCdF7n054=", + "lastModified": 1703166093, + "narHash": "sha256-bqfoBC/4IddlaDl8HnrtDR4ueOAQ4YrbRaXqXEJlKvY=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "1349ef9203534b80bd52577637060ceb5d4e0d24", + "rev": "2382ef6ad179f72691283d8d3c048d30829eadcc", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.397", + "ref": "v1.0.405", "repo": "evm-semantics", "type": "github" } @@ -388,11 +388,11 @@ ] }, "locked": { - "lastModified": 1702393410, - "narHash": "sha256-YbfXAIj/qax/o9G5dhGAiJOvvOQrtMPoi3KDCfOPOms=", + "lastModified": 1703090628, + "narHash": "sha256-uYF53yhj4XlelzSEpjVu4nElkyx6CWndfGUjcBt0yfs=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "14c372e93bf6133b2c780868dcda8bb2abbe6d8b", + "rev": "136dc466528f3cd9e157351cb85909716c3ed9b2", "type": "github" }, "original": { @@ -543,16 +543,16 @@ "poetry2nix": "poetry2nix" }, "locked": { - "lastModified": 1702643479, - "narHash": "sha256-umKe3kkRGP3CB/Meujbc51hu6+aM/xDgEk8dRhezrH8=", + "lastModified": 1703157822, + "narHash": "sha256-VJDAnQ3RjutL0Wils8b62fFB++wMZnZJKUiWZdKbR/8=", "owner": "runtimeverification", "repo": "pyk", - "rev": "c397bba169e7e3f46ea403452a5f44c4cfa9eab0", + "rev": "3a91f68cfe2145562eae3c57187338b06317bfaa", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.549", + "ref": "v0.1.563", "repo": "pyk", "type": "github" } diff --git a/flake.nix b/flake.nix index 4e46451b9..c760c369e 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.397"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.405"; nixpkgs.follows = "kevm/nixpkgs"; nixpkgs-pyk.follows = "kevm/nixpkgs-pyk"; k-framework.follows = "kevm/k-framework"; diff --git a/package/version b/package/version index 3234805de..91c96fdf8 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.101 +0.1.102 diff --git a/poetry.lock b/poetry.lock index d58ff6d8b..275c18b79 100644 --- a/poetry.lock +++ b/poetry.lock @@ -156,63 +156,63 @@ cron = ["capturer (>=2.4)"] [[package]] name = "coverage" -version = "7.3.3" +version = "7.3.4" description = "Code coverage measurement for Python" optional = false python-versions = ">=3.8" files = [ - {file = "coverage-7.3.3-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:d874434e0cb7b90f7af2b6e3309b0733cde8ec1476eb47db148ed7deeb2a9494"}, - {file = "coverage-7.3.3-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:ee6621dccce8af666b8c4651f9f43467bfbf409607c604b840b78f4ff3619aeb"}, - {file = "coverage-7.3.3-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:1367aa411afb4431ab58fd7ee102adb2665894d047c490649e86219327183134"}, - {file = "coverage-7.3.3-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:1f0f8f0c497eb9c9f18f21de0750c8d8b4b9c7000b43996a094290b59d0e7523"}, - {file = "coverage-7.3.3-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:db0338c4b0951d93d547e0ff8d8ea340fecf5885f5b00b23be5aa99549e14cfd"}, - {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:d31650d313bd90d027f4be7663dfa2241079edd780b56ac416b56eebe0a21aab"}, - {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:9437a4074b43c177c92c96d051957592afd85ba00d3e92002c8ef45ee75df438"}, - {file = "coverage-7.3.3-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:9e17d9cb06c13b4f2ef570355fa45797d10f19ca71395910b249e3f77942a837"}, - {file = "coverage-7.3.3-cp310-cp310-win32.whl", hash = "sha256:eee5e741b43ea1b49d98ab6e40f7e299e97715af2488d1c77a90de4a663a86e2"}, - {file = "coverage-7.3.3-cp310-cp310-win_amd64.whl", hash = "sha256:593efa42160c15c59ee9b66c5f27a453ed3968718e6e58431cdfb2d50d5ad284"}, - {file = "coverage-7.3.3-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:8c944cf1775235c0857829c275c777a2c3e33032e544bcef614036f337ac37bb"}, - {file = "coverage-7.3.3-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:eda7f6e92358ac9e1717ce1f0377ed2b9320cea070906ece4e5c11d172a45a39"}, - {file = "coverage-7.3.3-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:3c854c1d2c7d3e47f7120b560d1a30c1ca221e207439608d27bc4d08fd4aeae8"}, - {file = "coverage-7.3.3-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:222b038f08a7ebed1e4e78ccf3c09a1ca4ac3da16de983e66520973443b546bc"}, - {file = "coverage-7.3.3-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:ff4800783d85bff132f2cc7d007426ec698cdce08c3062c8d501ad3f4ea3d16c"}, - {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:fc200cec654311ca2c3f5ab3ce2220521b3d4732f68e1b1e79bef8fcfc1f2b97"}, - {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:307aecb65bb77cbfebf2eb6e12009e9034d050c6c69d8a5f3f737b329f4f15fb"}, - {file = "coverage-7.3.3-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:ffb0eacbadb705c0a6969b0adf468f126b064f3362411df95f6d4f31c40d31c1"}, - {file = "coverage-7.3.3-cp311-cp311-win32.whl", hash = "sha256:79c32f875fd7c0ed8d642b221cf81feba98183d2ff14d1f37a1bbce6b0347d9f"}, - {file = "coverage-7.3.3-cp311-cp311-win_amd64.whl", hash = "sha256:243576944f7c1a1205e5cd658533a50eba662c74f9be4c050d51c69bd4532936"}, - {file = "coverage-7.3.3-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:a2ac4245f18057dfec3b0074c4eb366953bca6787f1ec397c004c78176a23d56"}, - {file = "coverage-7.3.3-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f9191be7af41f0b54324ded600e8ddbcabea23e1e8ba419d9a53b241dece821d"}, - {file = "coverage-7.3.3-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:31c0b1b8b5a4aebf8fcd227237fc4263aa7fa0ddcd4d288d42f50eff18b0bac4"}, - {file = "coverage-7.3.3-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:ee453085279df1bac0996bc97004771a4a052b1f1e23f6101213e3796ff3cb85"}, - {file = "coverage-7.3.3-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:1191270b06ecd68b1d00897b2daddb98e1719f63750969614ceb3438228c088e"}, - {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:007a7e49831cfe387473e92e9ff07377f6121120669ddc39674e7244350a6a29"}, - {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:af75cf83c2d57717a8493ed2246d34b1f3398cb8a92b10fd7a1858cad8e78f59"}, - {file = "coverage-7.3.3-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:811ca7373da32f1ccee2927dc27dc523462fd30674a80102f86c6753d6681bc6"}, - {file = "coverage-7.3.3-cp312-cp312-win32.whl", hash = "sha256:733537a182b5d62184f2a72796eb6901299898231a8e4f84c858c68684b25a70"}, - {file = "coverage-7.3.3-cp312-cp312-win_amd64.whl", hash = "sha256:e995efb191f04b01ced307dbd7407ebf6e6dc209b528d75583277b10fd1800ee"}, - {file = "coverage-7.3.3-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:fbd8a5fe6c893de21a3c6835071ec116d79334fbdf641743332e442a3466f7ea"}, - {file = "coverage-7.3.3-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:50c472c1916540f8b2deef10cdc736cd2b3d1464d3945e4da0333862270dcb15"}, - {file = "coverage-7.3.3-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:2e9223a18f51d00d3ce239c39fc41410489ec7a248a84fab443fbb39c943616c"}, - {file = "coverage-7.3.3-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:f501e36ac428c1b334c41e196ff6bd550c0353c7314716e80055b1f0a32ba394"}, - {file = "coverage-7.3.3-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:475de8213ed95a6b6283056d180b2442eee38d5948d735cd3d3b52b86dd65b92"}, - {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:afdcc10c01d0db217fc0a64f58c7edd635b8f27787fea0a3054b856a6dff8717"}, - {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:fff0b2f249ac642fd735f009b8363c2b46cf406d3caec00e4deeb79b5ff39b40"}, - {file = "coverage-7.3.3-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:a1f76cfc122c9e0f62dbe0460ec9cc7696fc9a0293931a33b8870f78cf83a327"}, - {file = "coverage-7.3.3-cp38-cp38-win32.whl", hash = "sha256:757453848c18d7ab5d5b5f1827293d580f156f1c2c8cef45bfc21f37d8681069"}, - {file = "coverage-7.3.3-cp38-cp38-win_amd64.whl", hash = "sha256:ad2453b852a1316c8a103c9c970db8fbc262f4f6b930aa6c606df9b2766eee06"}, - {file = "coverage-7.3.3-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:3b15e03b8ee6a908db48eccf4e4e42397f146ab1e91c6324da44197a45cb9132"}, - {file = "coverage-7.3.3-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:89400aa1752e09f666cc48708eaa171eef0ebe3d5f74044b614729231763ae69"}, - {file = "coverage-7.3.3-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:c59a3e59fb95e6d72e71dc915e6d7fa568863fad0a80b33bc7b82d6e9f844973"}, - {file = "coverage-7.3.3-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:9ede881c7618f9cf93e2df0421ee127afdfd267d1b5d0c59bcea771cf160ea4a"}, - {file = "coverage-7.3.3-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f3bfd2c2f0e5384276e12b14882bf2c7621f97c35320c3e7132c156ce18436a1"}, - {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:7f3bad1a9313401ff2964e411ab7d57fb700a2d5478b727e13f156c8f89774a0"}, - {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:65d716b736f16e250435473c5ca01285d73c29f20097decdbb12571d5dfb2c94"}, - {file = "coverage-7.3.3-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:a702e66483b1fe602717020a0e90506e759c84a71dbc1616dd55d29d86a9b91f"}, - {file = "coverage-7.3.3-cp39-cp39-win32.whl", hash = "sha256:7fbf3f5756e7955174a31fb579307d69ffca91ad163467ed123858ce0f3fd4aa"}, - {file = "coverage-7.3.3-cp39-cp39-win_amd64.whl", hash = "sha256:cad9afc1644b979211989ec3ff7d82110b2ed52995c2f7263e7841c846a75348"}, - {file = "coverage-7.3.3-pp38.pp39.pp310-none-any.whl", hash = "sha256:d299d379b676812e142fb57662a8d0d810b859421412b4d7af996154c00c31bb"}, - {file = "coverage-7.3.3.tar.gz", hash = "sha256:df04c64e58df96b4427db8d0559e95e2df3138c9916c96f9f6a4dd220db2fdb7"}, + {file = "coverage-7.3.4-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:aff2bd3d585969cc4486bfc69655e862028b689404563e6b549e6a8244f226df"}, + {file = "coverage-7.3.4-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:e4353923f38d752ecfbd3f1f20bf7a3546993ae5ecd7c07fd2f25d40b4e54571"}, + {file = "coverage-7.3.4-cp310-cp310-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:ea473c37872f0159294f7073f3fa72f68b03a129799f3533b2bb44d5e9fa4f82"}, + {file = "coverage-7.3.4-cp310-cp310-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:5214362abf26e254d749fc0c18af4c57b532a4bfde1a057565616dd3b8d7cc94"}, + {file = "coverage-7.3.4-cp310-cp310-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:f99b7d3f7a7adfa3d11e3a48d1a91bb65739555dd6a0d3fa68aa5852d962e5b1"}, + {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_aarch64.whl", hash = "sha256:74397a1263275bea9d736572d4cf338efaade2de9ff759f9c26bcdceb383bb49"}, + {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_i686.whl", hash = "sha256:f154bd866318185ef5865ace5be3ac047b6d1cc0aeecf53bf83fe846f4384d5d"}, + {file = "coverage-7.3.4-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:e0d84099ea7cba9ff467f9c6f747e3fc3906e2aadac1ce7b41add72e8d0a3712"}, + {file = "coverage-7.3.4-cp310-cp310-win32.whl", hash = "sha256:3f477fb8a56e0c603587b8278d9dbd32e54bcc2922d62405f65574bd76eba78a"}, + {file = "coverage-7.3.4-cp310-cp310-win_amd64.whl", hash = "sha256:c75738ce13d257efbb6633a049fb2ed8e87e2e6c2e906c52d1093a4d08d67c6b"}, + {file = "coverage-7.3.4-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:997aa14b3e014339d8101b9886063c5d06238848905d9ad6c6eabe533440a9a7"}, + {file = "coverage-7.3.4-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:8a9c5bc5db3eb4cd55ecb8397d8e9b70247904f8eca718cc53c12dcc98e59fc8"}, + {file = "coverage-7.3.4-cp311-cp311-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:27ee94f088397d1feea3cb524e4313ff0410ead7d968029ecc4bc5a7e1d34fbf"}, + {file = "coverage-7.3.4-cp311-cp311-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:8ce03e25e18dd9bf44723e83bc202114817f3367789052dc9e5b5c79f40cf59d"}, + {file = "coverage-7.3.4-cp311-cp311-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:85072e99474d894e5df582faec04abe137b28972d5e466999bc64fc37f564a03"}, + {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_aarch64.whl", hash = "sha256:a877810ef918d0d345b783fc569608804f3ed2507bf32f14f652e4eaf5d8f8d0"}, + {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_i686.whl", hash = "sha256:9ac17b94ab4ca66cf803f2b22d47e392f0977f9da838bf71d1f0db6c32893cb9"}, + {file = "coverage-7.3.4-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:36d75ef2acab74dc948d0b537ef021306796da551e8ac8b467810911000af66a"}, + {file = "coverage-7.3.4-cp311-cp311-win32.whl", hash = "sha256:47ee56c2cd445ea35a8cc3ad5c8134cb9bece3a5cb50bb8265514208d0a65928"}, + {file = "coverage-7.3.4-cp311-cp311-win_amd64.whl", hash = "sha256:11ab62d0ce5d9324915726f611f511a761efcca970bd49d876cf831b4de65be5"}, + {file = "coverage-7.3.4-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:33e63c578f4acce1b6cd292a66bc30164495010f1091d4b7529d014845cd9bee"}, + {file = "coverage-7.3.4-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:782693b817218169bfeb9b9ba7f4a9f242764e180ac9589b45112571f32a0ba6"}, + {file = "coverage-7.3.4-cp312-cp312-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:7c4277ddaad9293454da19121c59f2d850f16bcb27f71f89a5c4836906eb35ef"}, + {file = "coverage-7.3.4-cp312-cp312-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:3d892a19ae24b9801771a5a989fb3e850bd1ad2e2b6e83e949c65e8f37bc67a1"}, + {file = "coverage-7.3.4-cp312-cp312-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:3024ec1b3a221bd10b5d87337d0373c2bcaf7afd86d42081afe39b3e1820323b"}, + {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_aarch64.whl", hash = "sha256:a1c3e9d2bbd6f3f79cfecd6f20854f4dc0c6e0ec317df2b265266d0dc06535f1"}, + {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_i686.whl", hash = "sha256:e91029d7f151d8bf5ab7d8bfe2c3dbefd239759d642b211a677bc0709c9fdb96"}, + {file = "coverage-7.3.4-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:6879fe41c60080aa4bb59703a526c54e0412b77e649a0d06a61782ecf0853ee1"}, + {file = "coverage-7.3.4-cp312-cp312-win32.whl", hash = "sha256:fd2f8a641f8f193968afdc8fd1697e602e199931012b574194052d132a79be13"}, + {file = "coverage-7.3.4-cp312-cp312-win_amd64.whl", hash = "sha256:d1d0ce6c6947a3a4aa5479bebceff2c807b9f3b529b637e2b33dea4468d75fc7"}, + {file = "coverage-7.3.4-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:36797b3625d1da885b369bdaaa3b0d9fb8865caed3c2b8230afaa6005434aa2f"}, + {file = "coverage-7.3.4-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:bfed0ec4b419fbc807dec417c401499ea869436910e1ca524cfb4f81cf3f60e7"}, + {file = "coverage-7.3.4-cp38-cp38-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:f97ff5a9fc2ca47f3383482858dd2cb8ddbf7514427eecf5aa5f7992d0571429"}, + {file = "coverage-7.3.4-cp38-cp38-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:607b6c6b35aa49defaebf4526729bd5238bc36fe3ef1a417d9839e1d96ee1e4c"}, + {file = "coverage-7.3.4-cp38-cp38-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:a8e258dcc335055ab59fe79f1dec217d9fb0cdace103d6b5c6df6b75915e7959"}, + {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_aarch64.whl", hash = "sha256:a02ac7c51819702b384fea5ee033a7c202f732a2a2f1fe6c41e3d4019828c8d3"}, + {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_i686.whl", hash = "sha256:b710869a15b8caf02e31d16487a931dbe78335462a122c8603bb9bd401ff6fb2"}, + {file = "coverage-7.3.4-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:c6a23ae9348a7a92e7f750f9b7e828448e428e99c24616dec93a0720342f241d"}, + {file = "coverage-7.3.4-cp38-cp38-win32.whl", hash = "sha256:758ebaf74578b73f727acc4e8ab4b16ab6f22a5ffd7dd254e5946aba42a4ce76"}, + {file = "coverage-7.3.4-cp38-cp38-win_amd64.whl", hash = "sha256:309ed6a559bc942b7cc721f2976326efbfe81fc2b8f601c722bff927328507dc"}, + {file = "coverage-7.3.4-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:aefbb29dc56317a4fcb2f3857d5bce9b881038ed7e5aa5d3bcab25bd23f57328"}, + {file = "coverage-7.3.4-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:183c16173a70caf92e2dfcfe7c7a576de6fa9edc4119b8e13f91db7ca33a7923"}, + {file = "coverage-7.3.4-cp39-cp39-manylinux_2_17_aarch64.manylinux2014_aarch64.whl", hash = "sha256:4a4184dcbe4f98d86470273e758f1d24191ca095412e4335ff27b417291f5964"}, + {file = "coverage-7.3.4-cp39-cp39-manylinux_2_5_i686.manylinux1_i686.manylinux_2_17_i686.manylinux2014_i686.whl", hash = "sha256:93698ac0995516ccdca55342599a1463ed2e2d8942316da31686d4d614597ef9"}, + {file = "coverage-7.3.4-cp39-cp39-manylinux_2_5_x86_64.manylinux1_x86_64.manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:fb220b3596358a86361139edce40d97da7458412d412e1e10c8e1970ee8c09ab"}, + {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_aarch64.whl", hash = "sha256:d5b14abde6f8d969e6b9dd8c7a013d9a2b52af1235fe7bebef25ad5c8f47fa18"}, + {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_i686.whl", hash = "sha256:610afaf929dc0e09a5eef6981edb6a57a46b7eceff151947b836d869d6d567c1"}, + {file = "coverage-7.3.4-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:d6ed790728fb71e6b8247bd28e77e99d0c276dff952389b5388169b8ca7b1c28"}, + {file = "coverage-7.3.4-cp39-cp39-win32.whl", hash = "sha256:c15fdfb141fcf6a900e68bfa35689e1256a670db32b96e7a931cab4a0e1600e5"}, + {file = "coverage-7.3.4-cp39-cp39-win_amd64.whl", hash = "sha256:38d0b307c4d99a7aca4e00cad4311b7c51b7ac38fb7dea2abe0d182dd4008e05"}, + {file = "coverage-7.3.4-pp38.pp39.pp310-none-any.whl", hash = "sha256:b1e0f25ae99cf247abfb3f0fac7ae25739e4cd96bf1afa3537827c576b4847e5"}, + {file = "coverage-7.3.4.tar.gz", hash = "sha256:020d56d2da5bc22a0e00a5b0d54597ee91ad72446fa4cf1b97c35022f6b6dbf0"}, ] [package.dependencies] @@ -431,7 +431,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.397" +version = "1.0.405" description = "" optional = false python-versions = "^3.10" @@ -440,14 +440,14 @@ develop = false [package.dependencies] pathos = "*" -pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.549"} +pyk = {git = "https://github.com/runtimeverification/pyk.git", tag = "v0.1.563"} tomlkit = "^0.11.6" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.397" -resolved_reference = "1349ef9203534b80bd52577637060ceb5d4e0d24" +reference = "v1.0.405" +resolved_reference = "2382ef6ad179f72691283d8d3c048d30829eadcc" subdirectory = "kevm-pyk" [[package]] @@ -567,38 +567,38 @@ dill = ">=0.3.7" [[package]] name = "mypy" -version = "1.7.1" +version = "1.8.0" description = "Optional static typing for Python" optional = false python-versions = ">=3.8" files = [ - {file = "mypy-1.7.1-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:12cce78e329838d70a204293e7b29af9faa3ab14899aec397798a4b41be7f340"}, - {file = "mypy-1.7.1-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:1484b8fa2c10adf4474f016e09d7a159602f3239075c7bf9f1627f5acf40ad49"}, - {file = "mypy-1.7.1-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:31902408f4bf54108bbfb2e35369877c01c95adc6192958684473658c322c8a5"}, - {file = "mypy-1.7.1-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:f2c2521a8e4d6d769e3234350ba7b65ff5d527137cdcde13ff4d99114b0c8e7d"}, - {file = "mypy-1.7.1-cp310-cp310-win_amd64.whl", hash = "sha256:fcd2572dd4519e8a6642b733cd3a8cfc1ef94bafd0c1ceed9c94fe736cb65b6a"}, - {file = "mypy-1.7.1-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:4b901927f16224d0d143b925ce9a4e6b3a758010673eeded9b748f250cf4e8f7"}, - {file = "mypy-1.7.1-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:2f7f6985d05a4e3ce8255396df363046c28bea790e40617654e91ed580ca7c51"}, - {file = "mypy-1.7.1-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:944bdc21ebd620eafefc090cdf83158393ec2b1391578359776c00de00e8907a"}, - {file = "mypy-1.7.1-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9c7ac372232c928fff0645d85f273a726970c014749b924ce5710d7d89763a28"}, - {file = "mypy-1.7.1-cp311-cp311-win_amd64.whl", hash = "sha256:f6efc9bd72258f89a3816e3a98c09d36f079c223aa345c659622f056b760ab42"}, - {file = "mypy-1.7.1-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:6dbdec441c60699288adf051f51a5d512b0d818526d1dcfff5a41f8cd8b4aaf1"}, - {file = "mypy-1.7.1-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:4fc3d14ee80cd22367caaaf6e014494415bf440980a3045bf5045b525680ac33"}, - {file = "mypy-1.7.1-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2c6e4464ed5f01dc44dc9821caf67b60a4e5c3b04278286a85c067010653a0eb"}, - {file = "mypy-1.7.1-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:d9b338c19fa2412f76e17525c1b4f2c687a55b156320acb588df79f2e6fa9fea"}, - {file = "mypy-1.7.1-cp312-cp312-win_amd64.whl", hash = "sha256:204e0d6de5fd2317394a4eff62065614c4892d5a4d1a7ee55b765d7a3d9e3f82"}, - {file = "mypy-1.7.1-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:84860e06ba363d9c0eeabd45ac0fde4b903ad7aa4f93cd8b648385a888e23200"}, - {file = "mypy-1.7.1-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:8c5091ebd294f7628eb25ea554852a52058ac81472c921150e3a61cdd68f75a7"}, - {file = "mypy-1.7.1-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:40716d1f821b89838589e5b3106ebbc23636ffdef5abc31f7cd0266db936067e"}, - {file = "mypy-1.7.1-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:5cf3f0c5ac72139797953bd50bc6c95ac13075e62dbfcc923571180bebb662e9"}, - {file = "mypy-1.7.1-cp38-cp38-win_amd64.whl", hash = "sha256:78e25b2fd6cbb55ddfb8058417df193f0129cad5f4ee75d1502248e588d9e0d7"}, - {file = "mypy-1.7.1-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:75c4d2a6effd015786c87774e04331b6da863fc3fc4e8adfc3b40aa55ab516fe"}, - {file = "mypy-1.7.1-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:2643d145af5292ee956aa0a83c2ce1038a3bdb26e033dadeb2f7066fb0c9abce"}, - {file = "mypy-1.7.1-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:75aa828610b67462ffe3057d4d8a4112105ed211596b750b53cbfe182f44777a"}, - {file = "mypy-1.7.1-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ee5d62d28b854eb61889cde4e1dbc10fbaa5560cb39780c3995f6737f7e82120"}, - {file = "mypy-1.7.1-cp39-cp39-win_amd64.whl", hash = "sha256:72cf32ce7dd3562373f78bd751f73c96cfb441de147cc2448a92c1a308bd0ca6"}, - {file = "mypy-1.7.1-py3-none-any.whl", hash = "sha256:f7c5d642db47376a0cc130f0de6d055056e010debdaf0707cd2b0fc7e7ef30ea"}, - {file = "mypy-1.7.1.tar.gz", hash = "sha256:fcb6d9afb1b6208b4c712af0dafdc650f518836065df0d4fb1d800f5d6773db2"}, + {file = "mypy-1.8.0-cp310-cp310-macosx_10_9_x86_64.whl", hash = "sha256:485a8942f671120f76afffff70f259e1cd0f0cfe08f81c05d8816d958d4577d3"}, + {file = "mypy-1.8.0-cp310-cp310-macosx_11_0_arm64.whl", hash = "sha256:df9824ac11deaf007443e7ed2a4a26bebff98d2bc43c6da21b2b64185da011c4"}, + {file = "mypy-1.8.0-cp310-cp310-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:2afecd6354bbfb6e0160f4e4ad9ba6e4e003b767dd80d85516e71f2e955ab50d"}, + {file = "mypy-1.8.0-cp310-cp310-musllinux_1_1_x86_64.whl", hash = "sha256:8963b83d53ee733a6e4196954502b33567ad07dfd74851f32be18eb932fb1cb9"}, + {file = "mypy-1.8.0-cp310-cp310-win_amd64.whl", hash = "sha256:e46f44b54ebddbeedbd3d5b289a893219065ef805d95094d16a0af6630f5d410"}, + {file = "mypy-1.8.0-cp311-cp311-macosx_10_9_x86_64.whl", hash = "sha256:855fe27b80375e5c5878492f0729540db47b186509c98dae341254c8f45f42ae"}, + {file = "mypy-1.8.0-cp311-cp311-macosx_11_0_arm64.whl", hash = "sha256:4c886c6cce2d070bd7df4ec4a05a13ee20c0aa60cb587e8d1265b6c03cf91da3"}, + {file = "mypy-1.8.0-cp311-cp311-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:d19c413b3c07cbecf1f991e2221746b0d2a9410b59cb3f4fb9557f0365a1a817"}, + {file = "mypy-1.8.0-cp311-cp311-musllinux_1_1_x86_64.whl", hash = "sha256:9261ed810972061388918c83c3f5cd46079d875026ba97380f3e3978a72f503d"}, + {file = "mypy-1.8.0-cp311-cp311-win_amd64.whl", hash = "sha256:51720c776d148bad2372ca21ca29256ed483aa9a4cdefefcef49006dff2a6835"}, + {file = "mypy-1.8.0-cp312-cp312-macosx_10_9_x86_64.whl", hash = "sha256:52825b01f5c4c1c4eb0db253ec09c7aa17e1a7304d247c48b6f3599ef40db8bd"}, + {file = "mypy-1.8.0-cp312-cp312-macosx_11_0_arm64.whl", hash = "sha256:f5ac9a4eeb1ec0f1ccdc6f326bcdb464de5f80eb07fb38b5ddd7b0de6bc61e55"}, + {file = "mypy-1.8.0-cp312-cp312-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:afe3fe972c645b4632c563d3f3eff1cdca2fa058f730df2b93a35e3b0c538218"}, + {file = "mypy-1.8.0-cp312-cp312-musllinux_1_1_x86_64.whl", hash = "sha256:42c6680d256ab35637ef88891c6bd02514ccb7e1122133ac96055ff458f93fc3"}, + {file = "mypy-1.8.0-cp312-cp312-win_amd64.whl", hash = "sha256:720a5ca70e136b675af3af63db533c1c8c9181314d207568bbe79051f122669e"}, + {file = "mypy-1.8.0-cp38-cp38-macosx_10_9_x86_64.whl", hash = "sha256:028cf9f2cae89e202d7b6593cd98db6759379f17a319b5faf4f9978d7084cdc6"}, + {file = "mypy-1.8.0-cp38-cp38-macosx_11_0_arm64.whl", hash = "sha256:4e6d97288757e1ddba10dd9549ac27982e3e74a49d8d0179fc14d4365c7add66"}, + {file = "mypy-1.8.0-cp38-cp38-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7f1478736fcebb90f97e40aff11a5f253af890c845ee0c850fe80aa060a267c6"}, + {file = "mypy-1.8.0-cp38-cp38-musllinux_1_1_x86_64.whl", hash = "sha256:42419861b43e6962a649068a61f4a4839205a3ef525b858377a960b9e2de6e0d"}, + {file = "mypy-1.8.0-cp38-cp38-win_amd64.whl", hash = "sha256:2b5b6c721bd4aabaadead3a5e6fa85c11c6c795e0c81a7215776ef8afc66de02"}, + {file = "mypy-1.8.0-cp39-cp39-macosx_10_9_x86_64.whl", hash = "sha256:5c1538c38584029352878a0466f03a8ee7547d7bd9f641f57a0f3017a7c905b8"}, + {file = "mypy-1.8.0-cp39-cp39-macosx_11_0_arm64.whl", hash = "sha256:4ef4be7baf08a203170f29e89d79064463b7fc7a0908b9d0d5114e8009c3a259"}, + {file = "mypy-1.8.0-cp39-cp39-manylinux_2_17_x86_64.manylinux2014_x86_64.whl", hash = "sha256:7178def594014aa6c35a8ff411cf37d682f428b3b5617ca79029d8ae72f5402b"}, + {file = "mypy-1.8.0-cp39-cp39-musllinux_1_1_x86_64.whl", hash = "sha256:ab3c84fa13c04aeeeabb2a7f67a25ef5d77ac9d6486ff33ded762ef353aa5592"}, + {file = "mypy-1.8.0-cp39-cp39-win_amd64.whl", hash = "sha256:99b00bc72855812a60d253420d8a2eae839b0afa4938f09f4d2aa9bb4654263a"}, + {file = "mypy-1.8.0-py3-none-any.whl", hash = "sha256:538fd81bb5e430cc1381a443971c0475582ff9f434c16cd46d2c66763ce85d9d"}, + {file = "mypy-1.8.0.tar.gz", hash = "sha256:6ff8b244d7085a0b425b56d327b480c3b29cafbd2eff27316a004f9a7391ae07"}, ] [package.dependencies] @@ -810,7 +810,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "0.1.549" +version = "0.1.563" description = "" optional = false python-versions = "^3.10" @@ -831,8 +831,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/pyk.git" -reference = "v0.1.549" -resolved_reference = "c397bba169e7e3f46ea403452a5f44c4cfa9eab0" +reference = "v0.1.563" +resolved_reference = "3a91f68cfe2145562eae3c57187338b06317bfaa" [[package]] name = "pyperclip" @@ -1082,4 +1082,4 @@ testing = ["big-O", "jaraco.functools", "jaraco.itertools", "more-itertools", "p [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "2c6a4cf888cf5961dc58a2969d1fd69cf532bdc3003683d8673cef1533f4c161" +content-hash = "4d4bc05145fd87e870e86485d16e0514c66c716181c24ce8bbf2eea6a0846c6e" diff --git a/pyproject.toml b/pyproject.toml index 951c8e876..5599d4d0f 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.101" +version = "0.1.102" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", @@ -12,7 +12,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" -kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.397", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.405", subdirectory = "kevm-pyk" } [tool.poetry.group.dev.dependencies] autoflake = "*" diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index 5ffc4e07c..f6b5570fd 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.101' +VERSION: Final = '0.1.102' diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index dfb1cf0f1..6b8186d6e 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -12,7 +12,7 @@ from pyk.kast.manip import flatten_label, set_cell from pyk.kcfg import KCFG from pyk.prelude.k import GENERATED_TOP_CELL -from pyk.prelude.kbool import FALSE, notBool +from pyk.prelude.kbool import FALSE, TRUE, notBool from pyk.prelude.kint import intToken from pyk.prelude.ml import mlEqualsTrue from pyk.proof.proof import Proof @@ -433,6 +433,7 @@ def _init_cterm( init_subst = { 'MODE_CELL': KApply('NORMAL'), 'SCHEDULE_CELL': KApply('SHANGHAI_EVM'), + 'USEGAS_CELL': TRUE, 'STATUSCODE_CELL': KVariable('STATUSCODE'), 'CALLSTACK_CELL': KApply('.List'), 'CALLDEPTH_CELL': intToken(0), diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected index 51cea1ec7..cfa779311 100644 --- a/src/tests/integration/test-data/gas-abstraction.expected +++ b/src/tests/integration/test-data/gas-abstraction.expected @@ -103,6 +103,9 @@ Node 6: SHANGHAI + + true + @@ -408,6 +411,9 @@ Node 6: SHANGHAI + + true + @@ -614,6 +620,9 @@ Node 6: SHANGHAI + + true + @@ -823,6 +832,9 @@ Node 6: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected index 4fb341571..dd9e8b298 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected @@ -81,6 +81,9 @@ SHANGHAI + + true + @@ -286,6 +289,9 @@ SHANGHAI + + true + @@ -494,6 +500,9 @@ SHANGHAI + + true + @@ -700,6 +709,9 @@ SHANGHAI + + true + @@ -908,6 +920,9 @@ SHANGHAI + + true + @@ -1094,6 +1109,9 @@ SHANGHAI + + true + @@ -1283,6 +1301,9 @@ SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index 4967d3c24..daa82690c 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -77,6 +77,9 @@ Node 10: SHANGHAI + + true + @@ -267,6 +270,9 @@ Node 10: SHANGHAI + + true + @@ -472,6 +478,9 @@ Node 10: SHANGHAI + + true + @@ -680,6 +689,9 @@ Node 10: SHANGHAI + + true + @@ -886,6 +898,9 @@ Node 10: SHANGHAI + + true + @@ -1094,6 +1109,9 @@ Node 10: SHANGHAI + + true + @@ -1280,6 +1298,9 @@ Node 10: SHANGHAI + + true + @@ -1469,6 +1490,9 @@ Node 10: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index 786e4e74a..85337ae5a 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -133,6 +133,9 @@ Node 18: SHANGHAI + + true + @@ -334,6 +337,9 @@ Node 18: SHANGHAI + + true + @@ -539,6 +545,9 @@ Node 18: SHANGHAI + + true + @@ -747,6 +756,9 @@ Node 18: SHANGHAI + + true + @@ -953,6 +965,9 @@ Node 18: SHANGHAI + + true + @@ -1161,6 +1176,9 @@ Node 18: SHANGHAI + + true + @@ -1349,6 +1367,9 @@ Node 18: SHANGHAI + + true + @@ -1540,6 +1561,9 @@ Node 18: SHANGHAI + + true + @@ -1738,6 +1762,9 @@ Node 18: SHANGHAI + + true + @@ -1938,6 +1965,9 @@ Node 18: SHANGHAI + + true + @@ -2212,6 +2242,9 @@ Node 18: SHANGHAI + + true + @@ -2487,6 +2520,9 @@ Node 18: SHANGHAI + + true + @@ -2765,6 +2801,9 @@ Node 18: SHANGHAI + + true + @@ -3043,6 +3082,9 @@ Node 18: SHANGHAI + + true + @@ -3315,6 +3357,9 @@ Node 18: SHANGHAI + + true + @@ -3515,6 +3560,9 @@ Node 18: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index 3dc16681d..9c39a301f 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -77,6 +77,9 @@ Node 10: SHANGHAI + + true + @@ -267,6 +270,9 @@ Node 10: SHANGHAI + + true + @@ -472,6 +478,9 @@ Node 10: SHANGHAI + + true + @@ -680,6 +689,9 @@ Node 10: SHANGHAI + + true + @@ -886,6 +898,9 @@ Node 10: SHANGHAI + + true + @@ -1094,6 +1109,9 @@ Node 10: SHANGHAI + + true + @@ -1280,6 +1298,9 @@ Node 10: SHANGHAI + + true + @@ -1469,6 +1490,9 @@ Node 10: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index 9dda7ff30..1ce54d21e 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -81,6 +81,9 @@ SHANGHAI + + true + @@ -286,6 +289,9 @@ SHANGHAI + + true + @@ -494,6 +500,9 @@ SHANGHAI + + true + @@ -700,6 +709,9 @@ SHANGHAI + + true + @@ -908,6 +920,9 @@ SHANGHAI + + true + @@ -1094,6 +1109,9 @@ SHANGHAI + + true + @@ -1283,6 +1301,9 @@ SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 98e4e2c88..4600e957b 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -124,6 +124,9 @@ Node 16: SHANGHAI + + true + @@ -317,6 +320,9 @@ Node 16: SHANGHAI + + true + @@ -522,6 +528,9 @@ Node 16: SHANGHAI + + true + @@ -730,6 +739,9 @@ Node 16: SHANGHAI + + true + @@ -936,6 +948,9 @@ Node 16: SHANGHAI + + true + @@ -1147,6 +1162,9 @@ Node 16: SHANGHAI + + true + @@ -1334,6 +1352,9 @@ Node 16: SHANGHAI + + true + @@ -1525,6 +1546,9 @@ Node 16: SHANGHAI + + true + @@ -1716,6 +1740,9 @@ Node 16: SHANGHAI + + true + @@ -1909,6 +1936,9 @@ Node 16: SHANGHAI + + true + @@ -2102,6 +2132,9 @@ Node 16: SHANGHAI + + true + @@ -2295,6 +2328,9 @@ Node 16: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index e1dab288e..d5c522946 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -124,6 +124,9 @@ Node 15: SHANGHAI + + true + @@ -319,6 +322,9 @@ Node 15: SHANGHAI + + true + @@ -524,6 +530,9 @@ Node 15: SHANGHAI + + true + @@ -732,6 +741,9 @@ Node 15: SHANGHAI + + true + @@ -938,6 +950,9 @@ Node 15: SHANGHAI + + true + @@ -1151,6 +1166,9 @@ Node 15: SHANGHAI + + true + @@ -1340,6 +1358,9 @@ Node 15: SHANGHAI + + true + @@ -1533,6 +1554,9 @@ Node 15: SHANGHAI + + true + @@ -1726,6 +1750,9 @@ Node 15: SHANGHAI + + true + @@ -1921,6 +1948,9 @@ Node 15: SHANGHAI + + true + @@ -2116,6 +2146,9 @@ Node 15: SHANGHAI + + true + @@ -2311,6 +2344,9 @@ Node 15: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index 8efd6d73d..d0748ba49 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -63,6 +63,9 @@ Node 7: SHANGHAI + + true + @@ -277,6 +280,9 @@ Node 7: SHANGHAI + + true + @@ -487,6 +493,9 @@ Node 7: SHANGHAI + + true + @@ -698,6 +707,9 @@ Node 7: SHANGHAI + + true + @@ -910,6 +922,9 @@ Node 7: SHANGHAI + + true + @@ -1123,6 +1138,9 @@ Node 7: SHANGHAI + + true + diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index af163d093..eb9ee44c4 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -91,6 +91,9 @@ Node 11: SHANGHAI + + true + @@ -308,6 +311,9 @@ Node 11: SHANGHAI + + true + @@ -518,6 +524,9 @@ Node 11: SHANGHAI + + true + @@ -730,6 +739,9 @@ Node 11: SHANGHAI + + true + @@ -945,6 +957,9 @@ Node 11: SHANGHAI + + true + @@ -1158,6 +1173,9 @@ Node 11: SHANGHAI + + true + @@ -1373,6 +1391,9 @@ Node 11: SHANGHAI + + true + @@ -1589,6 +1610,9 @@ Node 11: SHANGHAI + + true + @@ -1802,6 +1826,9 @@ Node 11: SHANGHAI + + true + @@ -2018,6 +2045,9 @@ Node 11: SHANGHAI + + true + From 37572299d2b2a829837438de44d938987cbd2533 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 21 Dec 2023 18:09:48 +0000 Subject: [PATCH 11/14] Set Version: 0.1.103 --- package/version | 2 +- pyproject.toml | 2 +- src/kontrol/__init__.py | 2 +- 3 files changed, 3 insertions(+), 3 deletions(-) diff --git a/package/version b/package/version index 91c96fdf8..5950146bb 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.102 +0.1.103 diff --git a/pyproject.toml b/pyproject.toml index 5599d4d0f..02da1492e 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "kontrol" -version = "0.1.102" +version = "0.1.103" description = "Foundry integration for KEVM" authors = [ "Runtime Verification, Inc. ", diff --git a/src/kontrol/__init__.py b/src/kontrol/__init__.py index f6b5570fd..b76a15e04 100644 --- a/src/kontrol/__init__.py +++ b/src/kontrol/__init__.py @@ -5,4 +5,4 @@ if TYPE_CHECKING: from typing import Final -VERSION: Final = '0.1.102' +VERSION: Final = '0.1.103' From 92909c11989a907066f7b40c2fa56fb9894e15fc Mon Sep 17 00:00:00 2001 From: Andrei Date: Thu, 21 Dec 2023 20:59:47 +0200 Subject: [PATCH 12/14] remove duplicated substitution --- src/kontrol/prove.py | 1 - 1 file changed, 1 deletion(-) diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index c8e94ea1f..b316cf2f9 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -442,7 +442,6 @@ def _init_cterm( 'MODE_CELL': KApply('NORMAL'), 'USEGAS_CELL': TRUE if use_gas else FALSE, 'SCHEDULE_CELL': KApply('SHANGHAI_EVM'), - 'USEGAS_CELL': TRUE, 'STATUSCODE_CELL': KVariable('STATUSCODE'), 'CALLSTACK_CELL': KApply('.List'), 'CALLDEPTH_CELL': intToken(0), From 9712d1bfe9c9c21ad37472731d3a5ce8f11eba61 Mon Sep 17 00:00:00 2001 From: Andrei Date: Thu, 21 Dec 2023 21:33:57 +0200 Subject: [PATCH 13/14] update expected output --- ...ssertTest.testFail_assert_false().expected | 32 +- ...AssertTest.testFail_assert_true().expected | 36 +- ...sertTest.testFail_expect_revert().expected | 177 ++++---- .../AssertTest.test_assert_false().expected | 36 +- .../AssertTest.test_assert_true().expected | 32 +- ...Test.test_failing_branch(uint256).expected | 56 +-- ...st_revert_branch(uint256,uint256).expected | 56 +-- ...ail_assume_false(uint256,uint256).expected | 69 ++-- ...est_assume_false(uint256,uint256).expected | 381 ++++-------------- src/tests/integration/test_foundry_prove.py | 1 + 10 files changed, 301 insertions(+), 575 deletions(-) diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected index dd9e8b298..99dcdd49e 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_false().expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (376 steps) +│ (244 steps) ├─ 8 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 2984 @@ -82,7 +82,7 @@ SHANGHAI - true + false @@ -119,7 +119,7 @@ ... ... - ( 0 => 3 ) + 0 false @@ -290,7 +290,7 @@ SHANGHAI - true + false @@ -330,7 +330,7 @@ ... ... - 3 + 0 false @@ -501,7 +501,7 @@ SHANGHAI - true + false @@ -541,7 +541,7 @@ ... ... - 3 + 0 false @@ -710,7 +710,7 @@ SHANGHAI - true + false @@ -750,7 +750,7 @@ ... ... - ( 3 => 0 ) + 0 false @@ -921,7 +921,7 @@ SHANGHAI - true + false @@ -955,7 +955,7 @@ ... ... - ( 0 => 3 ) + 0 false @@ -1110,7 +1110,7 @@ SHANGHAI - true + false @@ -1147,7 +1147,7 @@ ... ... - 3 + 0 false @@ -1302,7 +1302,7 @@ SHANGHAI - true + false @@ -1339,7 +1339,7 @@ ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index daa82690c..93b9b49bd 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (303 steps) +│ (200 steps) ├─ 8 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -78,7 +78,7 @@ Node 10: SHANGHAI - true + false @@ -111,7 +111,7 @@ Node 10: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" - 3 + 0 false @@ -271,7 +271,7 @@ Node 10: SHANGHAI - true + false @@ -308,7 +308,7 @@ Node 10: ... ... - ( 0 => 3 ) + 0 false @@ -479,7 +479,7 @@ Node 10: SHANGHAI - true + false @@ -519,7 +519,7 @@ Node 10: ... ... - 3 + 0 false @@ -690,7 +690,7 @@ Node 10: SHANGHAI - true + false @@ -730,7 +730,7 @@ Node 10: ... ... - 3 + 0 false @@ -899,7 +899,7 @@ Node 10: SHANGHAI - true + false @@ -939,7 +939,7 @@ Node 10: ... ... - ( 3 => 0 ) + 0 false @@ -1110,7 +1110,7 @@ Node 10: SHANGHAI - true + false @@ -1144,7 +1144,7 @@ Node 10: ... ... - ( 0 => 3 ) + 0 false @@ -1299,7 +1299,7 @@ Node 10: SHANGHAI - true + false @@ -1336,7 +1336,7 @@ Node 10: ... ... - 3 + 0 false @@ -1491,7 +1491,7 @@ Node 10: SHANGHAI - true + false @@ -1528,7 +1528,7 @@ Node 10: ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index 85337ae5a..9003b03d8 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,9 +33,9 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (641 steps) +│ (416 steps) ├─ 8 -│ k: CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 ... +│ k: CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~> ... │ pc: 800 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -47,9 +47,9 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (365 steps) +│ (228 steps) ├─ 10 -│ k: STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306 ... +│ k: STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0 ... │ pc: 881 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -61,7 +61,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (505 steps) +│ (338 steps) ├─ 12 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> #return 128 0 ~> #pc [ STATICC ... │ pc: 2984 @@ -84,12 +84,12 @@ │ │ (1 step) ├─ 15 -│ k: #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund #gas ( ( Cgascap ( SHAN ... +│ k: #popCallStack ~> #popWorldState ~> 0 ~> #push ~> #refund #gas ( VGAS:Int ) ~> #s ... │ pc: 2984 │ callDepth: 1 │ statusCode: EVMC_REVERT │ -│ (150 steps) +│ (95 steps) ├─ 16 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -134,7 +134,7 @@ Node 18: SHANGHAI - true + false @@ -170,11 +170,8 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) - false @@ -188,7 +185,7 @@ Node 18: .List - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map @@ -338,7 +335,7 @@ Node 18: SHANGHAI - true + false @@ -375,7 +372,7 @@ Node 18: ... ... - ( 0 => 3 ) + 0 false @@ -546,7 +543,7 @@ Node 18: SHANGHAI - true + false @@ -586,7 +583,7 @@ Node 18: ... ... - 3 + 0 false @@ -757,7 +754,7 @@ Node 18: SHANGHAI - true + false @@ -797,7 +794,7 @@ Node 18: ... ... - 3 + 0 false @@ -966,7 +963,7 @@ Node 18: SHANGHAI - true + false @@ -1006,7 +1003,7 @@ Node 18: ... ... - ( 3 => 0 ) + 0 false @@ -1165,7 +1162,7 @@ Node 18: rule [BASIC-BLOCK-6-TO-8]: - ( .K => CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0 + ( .K => CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0 ~> #pc [ CALL ] ) ~> #execute ~> _CONTINUATION @@ -1177,7 +1174,7 @@ Node 18: SHANGHAI - true + false @@ -1208,11 +1205,8 @@ Node 18: ... ... - ( 0 => 5 ) + 0 - - ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) ) - false @@ -1226,7 +1220,7 @@ Node 18: .List - ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + .Set .Map @@ -1354,7 +1348,7 @@ Node 18: rule [BASIC-BLOCK-8-TO-9]: - ( CALL ( VGAS:Int +Int -2951 ) 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xf4\x84H\x14" false ~> #return 128 0 ) ~> #pc [ CALL ] @@ -1368,7 +1362,7 @@ Node 18: SHANGHAI - true + false @@ -1399,11 +1393,8 @@ Node 18: ... ... - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -2951 ) , ( VGAS:Int +Int -2951 ) , 100 ) ) - false @@ -1417,7 +1408,7 @@ Node 18: .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1548,7 +1539,7 @@ Node 18: ( #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"\xf4\x84H\x14" false ~> #return 128 0 - ~> #pc [ CALL ] => STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306518 128 4 128 0 + ~> #pc [ CALL ] => STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0 ~> #pc [ STATICCALL ] ~> #checkRevert ~> #updateRevertOutput 128 0 ) @@ -1562,7 +1553,7 @@ Node 18: SHANGHAI - true + false @@ -1596,11 +1587,8 @@ Node 18: ... ... - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -2951 => -5792 ) ) , ( VGAS:Int +Int ( -2951 => -5792 ) ) , 100 ) ) - false @@ -1614,7 +1602,7 @@ Node 18: .List - ( SetItem ( 645326474426547203313410069153905908525362434349 ) => ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) ) + .Set .Map @@ -1747,7 +1735,7 @@ Node 18: rule [BASIC-BLOCK-10-TO-11]: - ( STATICCALL ( VGAS:Int +Int -5792 ) 728815563385977040452943777879061427756277306518 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL VGAS:Int 728815563385977040452943777879061427756277306518 128 4 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 728815563385977040452943777879061427756277306518 728815563385977040452943777879061427756277306518 0 0 b"\xf3\xad0#" true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -1763,7 +1751,7 @@ Node 18: SHANGHAI - true + false @@ -1797,11 +1785,8 @@ Node 18: ... ... - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) - false @@ -1815,7 +1800,7 @@ Node 18: .List - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map @@ -1966,7 +1951,7 @@ Node 18: SHANGHAI - true + false @@ -1987,9 +1972,9 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ... ... - 5 + 0 - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) + CALLGAS_CELL:Gas false @@ -2039,7 +2024,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map -fragment } ) ) @@ -2071,10 +2056,10 @@ Node 18: ... ... - ( 5 => 3 ) + 0 - ( #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) => 0 ) + CALLGAS_CELL:Gas ( false => true ) @@ -2094,7 +2079,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + ( .Set => SetItem ( 728815563385977040452943777879061427756277306518 ) ) .Map @@ -2243,7 +2228,7 @@ Node 18: SHANGHAI - true + false @@ -2265,9 +2250,9 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ... ... - 5 + 0 - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) + CALLGAS_CELL:Gas false @@ -2317,7 +2302,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map -fragment } ) @@ -2349,10 +2334,10 @@ Node 18: ... ... - 3 + 0 - 0 + CALLGAS_CELL:Gas true @@ -2372,7 +2357,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + SetItem ( 728815563385977040452943777879061427756277306518 ) .Map @@ -2521,7 +2506,7 @@ Node 18: SHANGHAI - true + false @@ -2543,9 +2528,9 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ... ... - 5 + 0 - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) + CALLGAS_CELL:Gas false @@ -2595,7 +2580,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map -fragment } ) @@ -2627,10 +2612,10 @@ Node 18: ... ... - 3 + 0 - 0 + CALLGAS_CELL:Gas true @@ -2650,7 +2635,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + SetItem ( 728815563385977040452943777879061427756277306518 ) .Map @@ -2787,7 +2772,7 @@ Node 18: ~> #popWorldState ~> 0 ~> #push - ~> #refund #gas ( ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) +Int -290 ) ) + ~> #refund #gas ( VGAS:Int ) ~> #setLocalMem 128 0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) ~> #pc [ STATICCALL ] ~> #checkRevert @@ -2802,7 +2787,7 @@ Node 18: SHANGHAI - true + false @@ -2824,9 +2809,9 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ... ... - 5 + 0 - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) + CALLGAS_CELL:Gas false @@ -2876,7 +2861,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map -fragment } ) @@ -2908,10 +2893,10 @@ Node 18: ... ... - 3 + 0 - 0 + CALLGAS_CELL:Gas true @@ -2931,7 +2916,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + SetItem ( 728815563385977040452943777879061427756277306518 ) .Map @@ -3067,7 +3052,7 @@ Node 18: ~> #popWorldState ~> 0 ~> #push - ~> #refund #gas ( ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) +Int -290 ) ) + ~> #refund #gas ( VGAS:Int ) ~> #setLocalMem 128 0 b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ~> #pc [ STATICCALL ] ~> #checkRevert @@ -3083,7 +3068,7 @@ Node 18: SHANGHAI - true + false @@ -3107,9 +3092,9 @@ Node 18: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xf3\xad0#\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ... ... - 5 + 0 - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) + CALLGAS_CELL:Gas false @@ -3159,7 +3144,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map -fragment } ) => .List ) @@ -3191,10 +3176,10 @@ Node 18: ... ... - ( 3 => 5 ) + 0 - ( 0 => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) ) + CALLGAS_CELL:Gas ( true => false ) @@ -3214,7 +3199,7 @@ Node 18: REFUND_CELL:Int - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + ( SetItem ( 728815563385977040452943777879061427756277306518 ) => .Set ) .Map @@ -3358,7 +3343,7 @@ Node 18: SHANGHAI - true + false @@ -3398,11 +3383,8 @@ Node 18: ... ... - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) - false @@ -3416,7 +3398,7 @@ Node 18: .List - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map @@ -3561,7 +3543,7 @@ Node 18: SHANGHAI - true + false @@ -3601,11 +3583,8 @@ Node 18: ... ... - 5 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -5792 ) , ( VGAS:Int +Int -5792 ) , 100 ) ) - false @@ -3619,7 +3598,7 @@ Node 18: .List - ( SetItem ( 645326474426547203313410069153905908525362434349 ) SetItem ( 728815563385977040452943777879061427756277306518 ) ) + .Set .Map diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index 9c39a301f..972f95ae5 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (469 steps) +│ (307 steps) ├─ 8 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 2984 @@ -78,7 +78,7 @@ Node 10: SHANGHAI - true + false @@ -111,7 +111,7 @@ Node 10: b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" - 3 + 0 false @@ -271,7 +271,7 @@ Node 10: SHANGHAI - true + false @@ -308,7 +308,7 @@ Node 10: ... ... - ( 0 => 3 ) + 0 false @@ -479,7 +479,7 @@ Node 10: SHANGHAI - true + false @@ -519,7 +519,7 @@ Node 10: ... ... - 3 + 0 false @@ -690,7 +690,7 @@ Node 10: SHANGHAI - true + false @@ -730,7 +730,7 @@ Node 10: ... ... - 3 + 0 false @@ -899,7 +899,7 @@ Node 10: SHANGHAI - true + false @@ -939,7 +939,7 @@ Node 10: ... ... - ( 3 => 0 ) + 0 false @@ -1110,7 +1110,7 @@ Node 10: SHANGHAI - true + false @@ -1144,7 +1144,7 @@ Node 10: ... ... - ( 0 => 3 ) + 0 false @@ -1299,7 +1299,7 @@ Node 10: SHANGHAI - true + false @@ -1336,7 +1336,7 @@ Node 10: ... ... - 3 + 0 false @@ -1491,7 +1491,7 @@ Node 10: SHANGHAI - true + false @@ -1528,7 +1528,7 @@ Node 10: ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index 1ce54d21e..25d7ea272 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (396 steps) +│ (263 steps) ├─ 8 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -82,7 +82,7 @@ SHANGHAI - true + false @@ -119,7 +119,7 @@ ... ... - ( 0 => 3 ) + 0 false @@ -290,7 +290,7 @@ SHANGHAI - true + false @@ -330,7 +330,7 @@ ... ... - 3 + 0 false @@ -501,7 +501,7 @@ SHANGHAI - true + false @@ -541,7 +541,7 @@ ... ... - 3 + 0 false @@ -710,7 +710,7 @@ SHANGHAI - true + false @@ -750,7 +750,7 @@ ... ... - ( 3 => 0 ) + 0 false @@ -921,7 +921,7 @@ SHANGHAI - true + false @@ -955,7 +955,7 @@ ... ... - ( 0 => 3 ) + 0 false @@ -1110,7 +1110,7 @@ SHANGHAI - true + false @@ -1147,7 +1147,7 @@ ... ... - 3 + 0 false @@ -1302,7 +1302,7 @@ SHANGHAI - true + false @@ -1339,7 +1339,7 @@ ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 4600e957b..316b4222e 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (543 steps) +│ (360 steps) ├─ 8 (split) │ k: JUMPI 1113 bool2Word ( 100 <=Int VV0_x_114b9705:Int ) ~> #pc [ JUMPI ] ~> #execu ... │ pc: 1105 @@ -49,7 +49,7 @@ ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ -┃ │ (64 steps) +┃ │ (39 steps) ┃ ├─ 11 ┃ │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K ┃ │ pc: 317 @@ -86,7 +86,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ - │ (102 steps) + │ (63 steps) ├─ 12 │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K │ pc: 2984 @@ -125,7 +125,7 @@ Node 16: SHANGHAI - true + false @@ -158,7 +158,7 @@ Node 16: b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" - 3 + 0 false @@ -321,7 +321,7 @@ Node 16: SHANGHAI - true + false @@ -358,7 +358,7 @@ Node 16: ... ... - ( 0 => 3 ) + 0 false @@ -529,7 +529,7 @@ Node 16: SHANGHAI - true + false @@ -569,7 +569,7 @@ Node 16: ... ... - 3 + 0 false @@ -740,7 +740,7 @@ Node 16: SHANGHAI - true + false @@ -780,7 +780,7 @@ Node 16: ... ... - 3 + 0 false @@ -949,7 +949,7 @@ Node 16: SHANGHAI - true + false @@ -989,7 +989,7 @@ Node 16: ... ... - ( 3 => 0 ) + 0 false @@ -1163,7 +1163,7 @@ Node 16: SHANGHAI - true + false @@ -1194,7 +1194,7 @@ Node 16: ... ... - ( 0 => 3 ) + 0 false @@ -1353,7 +1353,7 @@ Node 16: SHANGHAI - true + false @@ -1387,7 +1387,7 @@ Node 16: ... ... - 3 + 0 false @@ -1547,7 +1547,7 @@ Node 16: SHANGHAI - true + false @@ -1581,7 +1581,7 @@ Node 16: ... ... - 3 + 0 false @@ -1741,7 +1741,7 @@ Node 16: SHANGHAI - true + false @@ -1778,7 +1778,7 @@ Node 16: ... ... - 3 + 0 false @@ -1937,7 +1937,7 @@ Node 16: SHANGHAI - true + false @@ -1974,7 +1974,7 @@ Node 16: ... ... - 3 + 0 false @@ -2133,7 +2133,7 @@ Node 16: SHANGHAI - true + false @@ -2170,7 +2170,7 @@ Node 16: ... ... - 3 + 0 false @@ -2329,7 +2329,7 @@ Node 16: SHANGHAI - true + false @@ -2366,7 +2366,7 @@ Node 16: ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index d5c522946..bd27726f3 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -5,7 +5,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (272 steps) +│ (179 steps) ├─ 3 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -33,7 +33,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (580 steps) +│ (387 steps) ├─ 8 (split) │ k: JUMPI 1583 bool2Word ( VV1_y_114b9705:Int <=Int VV0_x_114b9705:Int ) ~> #pc [ JU ... │ pc: 1579 @@ -49,7 +49,7 @@ ┃ │ callDepth: 0 ┃ │ statusCode: STATUSCODE:StatusCode ┃ │ -┃ │ (116 steps) +┃ │ (72 steps) ┃ ├─ 11 ┃ │ k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K ┃ │ pc: 2984 @@ -78,7 +78,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ - │ (62 steps) + │ (37 steps) ├─ 12 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 317 @@ -125,7 +125,7 @@ Node 15: SHANGHAI - true + false @@ -158,7 +158,7 @@ Node 15: b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" - 3 + 0 false @@ -323,7 +323,7 @@ Node 15: SHANGHAI - true + false @@ -360,7 +360,7 @@ Node 15: ... ... - ( 0 => 3 ) + 0 false @@ -531,7 +531,7 @@ Node 15: SHANGHAI - true + false @@ -571,7 +571,7 @@ Node 15: ... ... - 3 + 0 false @@ -742,7 +742,7 @@ Node 15: SHANGHAI - true + false @@ -782,7 +782,7 @@ Node 15: ... ... - 3 + 0 false @@ -951,7 +951,7 @@ Node 15: SHANGHAI - true + false @@ -991,7 +991,7 @@ Node 15: ... ... - ( 3 => 0 ) + 0 false @@ -1167,7 +1167,7 @@ Node 15: SHANGHAI - true + false @@ -1198,7 +1198,7 @@ Node 15: ... ... - ( 0 => 3 ) + 0 false @@ -1359,7 +1359,7 @@ Node 15: SHANGHAI - true + false @@ -1393,7 +1393,7 @@ Node 15: ... ... - 3 + 0 false @@ -1555,7 +1555,7 @@ Node 15: SHANGHAI - true + false @@ -1589,7 +1589,7 @@ Node 15: ... ... - 3 + 0 false @@ -1751,7 +1751,7 @@ Node 15: SHANGHAI - true + false @@ -1788,7 +1788,7 @@ Node 15: ... ... - 3 + 0 false @@ -1949,7 +1949,7 @@ Node 15: SHANGHAI - true + false @@ -1986,7 +1986,7 @@ Node 15: ... ... - 3 + 0 false @@ -2147,7 +2147,7 @@ Node 15: SHANGHAI - true + false @@ -2184,7 +2184,7 @@ Node 15: ... ... - 3 + 0 false @@ -2345,7 +2345,7 @@ Node 15: SHANGHAI - true + false @@ -2382,7 +2382,7 @@ Node 15: ... ... - 3 + 0 false diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index d0748ba49..f0cc0c4c4 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -5,9 +5,9 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (875 steps) +│ (560 steps) ├─ 3 -│ k: STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434 ... +│ k: STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 ... │ pc: 563 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -19,7 +19,7 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (299 steps) +│ (189 steps) ├─ 5 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 281 @@ -64,7 +64,7 @@ Node 7: SHANGHAI - true + false @@ -100,11 +100,8 @@ Node 7: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) - false @@ -118,7 +115,7 @@ Node 7: .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -269,7 +266,7 @@ Node 7: rule [BASIC-BLOCK-1-TO-3]: - ( .K => STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0 + ( .K => STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute ~> _CONTINUATION @@ -281,7 +278,7 @@ Node 7: SHANGHAI - true + false @@ -315,24 +312,22 @@ Node 7: ... ... - ( 0 => 6 ) + 0 - - ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) ) - false 0 + ... .List - ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + .Set .Map @@ -480,7 +475,7 @@ Node 7: rule [BASIC-BLOCK-3-TO-4]: - ( STATICCALL ( VGAS:Int +Int -3048 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -494,7 +489,7 @@ Node 7: SHANGHAI - true + false @@ -528,24 +523,22 @@ Node 7: ... ... - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -708,7 +701,7 @@ Node 7: SHANGHAI - true + false @@ -745,24 +738,22 @@ Node 7: ... ... - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -923,7 +914,7 @@ Node 7: SHANGHAI - true + false @@ -963,24 +954,22 @@ Node 7: ... ... - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1139,7 +1128,7 @@ Node 7: SHANGHAI - true + false @@ -1179,24 +1168,22 @@ Node 7: ... ... - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3048 ) , ( VGAS:Int +Int -3048 ) , 100 ) ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index eb9ee44c4..91e37f62c 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -5,9 +5,9 @@ │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (890 steps) +│ (570 steps) ├─ 3 -│ k: STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434 ... +│ k: STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 ... │ pc: 563 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode @@ -21,48 +21,41 @@ │ │ (1000 steps) ├─ 5 -│ k: #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745 ... -│ pc: 3667 +│ k: #gas [ ISZERO , ISZERO 1 ] ~> ISZERO 1 ~> #pc [ ISZERO ] ~> #execute ~> CONTINUA ... +│ pc: 4206 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (1000 steps) +│ (825 steps) ├─ 6 -│ k: #next [ DUP ( 2 ) ] ~> #execute ~> CONTINUATION:K -│ pc: 4451 -│ callDepth: 0 -│ statusCode: STATUSCODE:StatusCode -│ -│ (797 steps) -├─ 7 -│ k: CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 ... +│ k: CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0 ~ ... │ pc: 3785 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) -├─ 8 +├─ 7 │ k: #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563 ... │ pc: 3785 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ -│ (387 steps) -├─ 9 +│ (241 steps) +├─ 8 │ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 281 │ callDepth: 0 │ statusCode: STATUSCODE:StatusCode │ │ (1 step) -├─ 10 +├─ 9 │ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K │ pc: 281 │ callDepth: 0 │ statusCode: EVMC_SUCCESS │ │ (2 steps) -└─ 11 (leaf, terminal) +└─ 10 (leaf, terminal) k: #halt ~> CONTINUATION:K pc: 281 callDepth: 0 @@ -76,7 +69,7 @@ │ statusCode: STATUSCODE_FINAL:StatusCode -Node 11: +Node 10: ( @@ -92,7 +85,7 @@ Node 11: SHANGHAI - true + false @@ -128,11 +121,8 @@ Node 11: b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" - 17 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) - false @@ -149,7 +139,7 @@ Node 11: SetItem ( 645326474426547203313410069153905908525362434349 ) - ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) + .Map ... @@ -300,7 +290,7 @@ Node 11: rule [BASIC-BLOCK-1-TO-3]: - ( .K => STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0 + ( .K => STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 ~> #pc [ STATICCALL ] ) ~> #execute ~> _CONTINUATION @@ -312,7 +302,7 @@ Node 11: SHANGHAI - true + false @@ -346,24 +336,22 @@ Node 11: ... ... - ( 0 => 6 ) + 0 - - ( _CALLGAS_CELL => #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) ) - false 0 + ... .List - ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) + .Set .Map @@ -511,7 +499,7 @@ Node 11: rule [BASIC-BLOCK-3-TO-4]: - ( STATICCALL ( VGAS:Int +Int -3061 ) 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( STATICCALL VGAS:Int 645326474426547203313410069153905908525362434349 128 36 128 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true ~> #return 128 0 ) ~> #pc [ STATICCALL ] @@ -525,7 +513,7 @@ Node 11: SHANGHAI - true + false @@ -559,24 +547,22 @@ Node 11: ... ... - 6 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) - false 0 + ... .List - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -727,9 +713,9 @@ Node 11: ( #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) true ~> #return 128 0 - ~> #pc [ STATICCALL ] => #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ] - ~> MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 - ~> #pc [ MSTORE ] ) + ~> #pc [ STATICCALL ] => #gas [ ISZERO , ISZERO 1 ] + ~> ISZERO 1 + ~> #pc [ ISZERO ] ) ~> #execute ~> _CONTINUATION @@ -740,7 +726,7 @@ Node 11: SHANGHAI - true + false @@ -769,32 +755,30 @@ Node 11: 0 - ( ( 164 => 128 ) : ( ( selector ( "assume(bool)" ) => 645326474426547203313410069153905908525362434349 ) : ( ( 645326474426547203313410069153905908525362434349 => 594 ) : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( ( 280 => 594 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) + ( ( 164 => 64 ) : ( ( selector ( "assume(bool)" ) => 160 ) : ( ( 645326474426547203313410069153905908525362434349 => 292 ) : ( ( VV1_b_114b9705:Int => 96 ) : ( ( VV0_a_114b9705:Int => 4586 ) : ( ( 280 => 96 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => 0 ) : ( .WordStack => ( 288 : ( 128 : ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 : ( 3745 : ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) - ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00Lc\xe5b" +Bytes #buf ( 32 , bool2Word ( ( notBool VV0_a_114b9705:Int ==Int VV1_b_114b9705:Int ) ) ) => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) ... ... - ( 6 => 8 ) + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) - false 0 + ... ( .List => ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ) - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -945,9 +929,10 @@ Node 11: rule [BASIC-BLOCK-5-TO-6]: - ( #gas [ MSTORE , MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 ] - ~> MSTORE 192 46308022326495007027972728677917914892729792999299745830475596687180801507328 - ~> #pc [ MSTORE ] => #next [ DUP ( 2 ) ] ) + ( #gas [ ISZERO , ISZERO 1 ] + ~> ISZERO 1 + ~> #pc [ ISZERO ] => CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0 + ~> #pc [ CALL ] ) ~> #execute ~> _CONTINUATION @@ -958,7 +943,7 @@ Node 11: SHANGHAI - true + false @@ -987,32 +972,30 @@ Node 11: 0 - ( ( 128 => 4461 ) : ( ( 645326474426547203313410069153905908525362434349 => 100 ) : ( ( 594 => 0 ) : ( ( VV1_b_114b9705:Int => 388 ) : ( ( VV0_a_114b9705:Int => 256 ) : ( ( 594 => 3771 ) : ( ( VV1_b_114b9705:Int => 645326474426547203313410069153905908525362434349 ) : ( ( VV0_a_114b9705:Int => 0 ) : ( ( 280 => 594 ) : ( ( selector ( "test_assume_false(uint256,uint256)" ) => VV1_b_114b9705:Int ) : ( .WordStack => ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) + ( ( 64 => 488 ) : ( ( 160 => 645326474426547203313410069153905908525362434349 ) : ( ( 292 => 0 ) : ( ( 96 => 594 ) : ( ( 4586 => VV1_b_114b9705:Int ) : ( ( 96 => VV0_a_114b9705:Int ) : ( ( 0 => 594 ) : ( ( 288 => VV1_b_114b9705:Int ) : ( ( 128 => VV0_a_114b9705:Int ) : ( ( 51016057639858100040180367130768047423658391221723556551037572491782395555780 => 280 ) : ( ( 3745 => selector ( "test_assume_false(uint256,uint256)" ) ) : ( ( 645326474426547203313410069153905908525362434349 : ( 0 : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) ) - ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" ) + ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) ... ... - ( 8 => 13 ) + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -3061 ) , ( VGAS:Int +Int -3061 ) , 100 ) ) - false 0 + ... ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1162,223 +1145,7 @@ Node 11: rule [BASIC-BLOCK-6-TO-7]: - ( #next [ DUP ( 2 ) ] => CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 - ~> #pc [ CALL ] ) - ~> #execute - ~> _CONTINUATION - - - NORMAL - - - SHANGHAI - - - true - - - - - b"" - - - .List - - - .List - - - ... - ... - - 728815563385977040452943777879061427756277306518 - - - CALLER_ID:Int - - - b"\xe4\x1b\xef\xb4" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes #buf ( 32 , VV1_b_114b9705:Int ) - - - 0 - - - ( ( 4461 => 488 ) : ( ( 100 => 645326474426547203313410069153905908525362434349 ) : ( 0 : ( ( 388 => 594 ) : ( ( 256 => VV1_b_114b9705:Int ) : ( ( 3771 => VV0_a_114b9705:Int ) : ( ( 645326474426547203313410069153905908525362434349 => 594 ) : ( ( 0 => VV1_b_114b9705:Int ) : ( ( 594 => VV0_a_114b9705:Int ) : ( ( VV1_b_114b9705:Int => 280 ) : ( ( VV0_a_114b9705:Int => selector ( "test_assume_false(uint256,uint256)" ) ) : ( ( 594 : ( VV1_b_114b9705:Int : ( VV0_a_114b9705:Int : ( 280 : ( selector ( "test_assume_false(uint256,uint256)" ) : .WordStack ) ) ) ) ) => .WordStack ) ) ) ) ) ) ) ) ) ) ) ) - - - ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x84\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00`\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00dp\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" ) - - ... - ... - - ( 13 => 17 ) - - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int ( -3061 => -10173 ) ) , ( VGAS:Int +Int ( -3061 => -10173 ) ) , 100 ) ) - - - false - - - 0 - - - - - ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) - - - SetItem ( 645326474426547203313410069153905908525362434349 ) - - - .Map - - ... - - - ORIGIN_ID:Int - - - - NUMBER_CELL:Int - - ... - - ... - - - - ( - - 645326474426547203313410069153905908525362434349 - - - 0 - - ... - - .Map - - - .Map - - - 0 - - - - - 728815563385977040452943777879061427756277306518 - - - 0 - - ... - - .Map - - - .Map - - - 1 - - ) - - ... - - - ... - - - - - .Account - - - .Account - - - .Account - - - .Account - - - false - - - false - - ... - - - - false - - ... - - - - false - - - .Account - - - 0 - - - b"" - - - .OpcodeType - - - - - false - - - false - - ... - - - - false - - - false - - - .Set - - - .Set - - - - - requires ( 0 <=Int CALLER_ID:Int - andBool ( 0 <=Int ORIGIN_ID:Int - andBool ( VV0_a_114b9705:Int =/=K VV1_b_114b9705:Int - andBool ( 0 <=Int NUMBER_CELL:Int - andBool ( 0 <=Int VV0_a_114b9705:Int - andBool ( 0 <=Int VV1_b_114b9705:Int - andBool ( CALLER_ID:Int - - - ( CALL ( VGAS:Int +Int -10173 ) 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 + ( CALL VGAS:Int 645326474426547203313410069153905908525362434349 0 388 100 388 0 => #checkCall 728815563385977040452943777879061427756277306518 0 ~> #call 728815563385977040452943777879061427756277306518 645326474426547203313410069153905908525362434349 645326474426547203313410069153905908525362434349 0 0 b"p\xca\x10\xbb\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00q\tp\x9e\xcf\xa9\x1a\x80bo\xf3\x98\x9dh\xf6\x7f[\x1d\xd1-failed\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" false ~> #return 388 0 ) ~> #pc [ CALL ] @@ -1392,7 +1159,7 @@ Node 11: SHANGHAI - true + false @@ -1429,24 +1196,22 @@ Node 11: ... ... - 17 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) - false 0 + ... ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) - SetItem ( 645326474426547203313410069153905908525362434349 ) + .Set .Map @@ -1591,9 +1356,9 @@ Node 11: andBool ( VV1_b_114b9705:Int + rule [BASIC-BLOCK-7-TO-8]: ( #checkCall 728815563385977040452943777879061427756277306518 0 @@ -1611,7 +1376,7 @@ Node 11: SHANGHAI - true + false @@ -1648,27 +1413,25 @@ Node 11: ... ... - 17 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) - false 0 + ... ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 29485693714967335757563038618841744472215891622979272243827124658718922284880 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00 \x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\"Error: a == b not satisfied [uint]\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV0_a_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Left\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) ListItem ( { 728815563385977040452943777879061427756277306518 | ListItem ( 80904256614161075919025625882663817043659112028191499838463115877652359487912 ) | b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00@" +Bytes #buf ( 32 , VV1_b_114b9705:Int ) +Bytes b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\n Right\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" } ) - SetItem ( 645326474426547203313410069153905908525362434349 ) + ( .Set => SetItem ( 645326474426547203313410069153905908525362434349 ) ) - ( .Map => ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) ) + .Map ... @@ -1810,9 +1573,9 @@ Node 11: andBool ( VV1_b_114b9705:Int + rule [BASIC-BLOCK-8-TO-9]: ( #end EVMC_SUCCESS => #halt ) @@ -1827,7 +1590,7 @@ Node 11: SHANGHAI - true + false @@ -1867,17 +1630,15 @@ Node 11: ... ... - 17 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) - false 0 + ... @@ -1887,7 +1648,7 @@ Node 11: SetItem ( 645326474426547203313410069153905908525362434349 ) - ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) + .Map ... @@ -2029,9 +1790,9 @@ Node 11: andBool ( VV1_b_114b9705:Int + rule [BASIC-BLOCK-9-TO-10]: #halt @@ -2046,7 +1807,7 @@ Node 11: SHANGHAI - true + false @@ -2086,17 +1847,15 @@ Node 11: ... ... - 17 + 0 - - #gas ( Cgascap ( SHANGHAI , ( VGAS:Int +Int -10173 ) , ( VGAS:Int +Int -10173 ) , 100 ) ) - false 0 + ... @@ -2106,7 +1865,7 @@ Node 11: SetItem ( 645326474426547203313410069153905908525362434349 ) - ( 728815563385977040452943777879061427756277306518 |-> SetItem ( 7 ) ) + .Map ... @@ -2248,14 +2007,14 @@ Node 11: andBool ( VV1_b_114b9705:Int Date: Fri, 22 Dec 2023 09:32:09 +0200 Subject: [PATCH 14/14] use gas for GasTests --- src/tests/integration/test-data/foundry-prove-with-gas | 8 ++++++++ src/tests/integration/test_foundry_prove.py | 8 ++++---- 2 files changed, 12 insertions(+), 4 deletions(-) create mode 100644 src/tests/integration/test-data/foundry-prove-with-gas diff --git a/src/tests/integration/test-data/foundry-prove-with-gas b/src/tests/integration/test-data/foundry-prove-with-gas new file mode 100644 index 000000000..e65ddea40 --- /dev/null +++ b/src/tests/integration/test-data/foundry-prove-with-gas @@ -0,0 +1,8 @@ +GasTest.testInfiniteGas() +GasTest.testSetGas() +StoreTest.testGasLoadColdVM() +StoreTest.testGasLoadWarmUp() +StoreTest.testGasLoadWarmVM() +StoreTest.testGasStoreColdVM() +StoreTest.testGasStoreWarmUp() +StoreTest.testGasStoreWarmVM() \ No newline at end of file diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 328df4ba5..eb88d799a 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/src/tests/integration/test_foundry_prove.py @@ -121,6 +121,7 @@ def assert_or_update_k_output(k_file: Path, expected_file: Path, *, update: bool ALL_PROVE_TESTS: Final = tuple((TEST_DATA_DIR / 'foundry-prove-all').read_text().splitlines()) SKIPPED_PROVE_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-skip').read_text().splitlines()) SKIPPED_LEGACY_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-skip-legacy').read_text().splitlines()) +GAS_TESTS: Final = set((TEST_DATA_DIR / 'foundry-prove-with-gas').read_text().splitlines()) SHOW_TESTS = set((TEST_DATA_DIR / 'foundry-show').read_text().splitlines()) @@ -141,14 +142,13 @@ def test_foundry_prove( ): pytest.skip() + prove_options = ProveOptions(counterexample_info=True, bug_report=bug_report, use_gas=test_id in GAS_TESTS) + # When prove_res = foundry_prove( foundry, tests=[(test_id, None)], - prove_options=ProveOptions( - counterexample_info=True, - bug_report=bug_report, - ), + prove_options=prove_options, rpc_options=RPCOptions( port=server.port, ),