diff --git a/deps/k_release b/deps/k_release index 1dd611da1e..d349d55683 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.111 +7.1.112 diff --git a/flake.lock b/flake.lock index 547341660e..63c586736e 100644 --- a/flake.lock +++ b/flake.lock @@ -370,16 +370,16 @@ ] }, "locked": { - "lastModified": 1723826727, - "narHash": "sha256-Z5P9Ki+Qw4dcg9c5XvYSKPgLuWIDlOyrJTok+xaFA+U=", + "lastModified": 1724075892, + "narHash": "sha256-/xlvUynh4jO1Tq24mYQj3++tman37uXSAWECUIZD6pA=", "owner": "runtimeverification", "repo": "k", - "rev": "3692aa781186422363be7a49f6a157714caf84d7", + "rev": "d8abc6b62823435eae5a2a8df2ae1e8256ae2c43", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.111", + "ref": "v7.1.112", "repo": "k", "type": "github" } @@ -711,17 +711,17 @@ }, "locked": { "dir": "pyk", - "lastModified": 1723826727, - "narHash": "sha256-Z5P9Ki+Qw4dcg9c5XvYSKPgLuWIDlOyrJTok+xaFA+U=", + "lastModified": 1724075892, + "narHash": "sha256-/xlvUynh4jO1Tq24mYQj3++tman37uXSAWECUIZD6pA=", "owner": "runtimeverification", "repo": "k", - "rev": "3692aa781186422363be7a49f6a157714caf84d7", + "rev": "d8abc6b62823435eae5a2a8df2ae1e8256ae2c43", "type": "github" }, "original": { "dir": "pyk", "owner": "runtimeverification", - "ref": "v7.1.111", + "ref": "v7.1.112", "repo": "k", "type": "github" } diff --git a/flake.nix b/flake.nix index d4d8b9eb16..5f32cac189 100644 --- a/flake.nix +++ b/flake.nix @@ -2,11 +2,11 @@ description = "A flake for the KEVM Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v7.1.111"; + k-framework.url = "github:runtimeverification/k/v7.1.112"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; - pyk.url = "github:runtimeverification/k/v7.1.111?dir=pyk"; + pyk.url = "github:runtimeverification/k/v7.1.112?dir=pyk"; nixpkgs-pyk.follows = "pyk/nixpkgs"; poetry2nix.follows = "pyk/poetry2nix"; blockchain-k-plugin = { diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 103054419e..ac6720e39c 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -319,13 +319,13 @@ pyflakes = ">=3.2.0,<3.3.0" [[package]] name = "flake8-bugbear" -version = "24.4.26" +version = "24.8.19" description = "A plugin for flake8 finding likely bugs and design problems in your program. Contains warnings that don't belong in pyflakes and pycodestyle." optional = false python-versions = ">=3.8.1" files = [ - {file = "flake8_bugbear-24.4.26-py3-none-any.whl", hash = "sha256:cb430dd86bc821d79ccc0b030789a9c87a47a369667f12ba06e80f11305e8258"}, - {file = "flake8_bugbear-24.4.26.tar.gz", hash = "sha256:ff8d4ba5719019ebf98e754624c30c05cef0dadcf18a65d91c7567300e52a130"}, + {file = "flake8_bugbear-24.8.19-py3-none-any.whl", hash = "sha256:25bc3867f7338ee3b3e0916bf8b8a0b743f53a9a5175782ddc4325ed4f386b89"}, + {file = "flake8_bugbear-24.8.19.tar.gz", hash = "sha256:9b77627eceda28c51c27af94560a72b5b2c97c016651bdce45d8f56c180d2d32"}, ] [package.dependencies] @@ -443,13 +443,13 @@ zoneinfo = ["backports.zoneinfo (>=0.2.1)", "tzdata (>=2024.1)"] [[package]] name = "importlib-metadata" -version = "8.2.0" +version = "8.3.0" description = "Read metadata from Python packages" optional = false python-versions = ">=3.8" files = [ - {file = "importlib_metadata-8.2.0-py3-none-any.whl", hash = "sha256:11901fa0c2f97919b288679932bb64febaeacf289d18ac84dd68cb2e74213369"}, - {file = "importlib_metadata-8.2.0.tar.gz", hash = "sha256:72e8d4399996132204f9a16dcc751af254a48f8d1b20b9ff0f98d4a8f901e73d"}, + {file = "importlib_metadata-8.3.0-py3-none-any.whl", hash = "sha256:42817a4a0be5845d22c6e212db66a94ad261e2318d80b3e0d363894a79df2b67"}, + {file = "importlib_metadata-8.3.0.tar.gz", hash = "sha256:9c8fa6e8ea0f9516ad5c8db9246a731c948193c7754d3babb0114a05b27dd364"}, ] [package.dependencies] @@ -501,13 +501,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.111" +version = "7.1.112" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.111-py3-none-any.whl", hash = "sha256:456ef27c7fcb830947c34f5286c9ecdab4bedd6475a33c95bc39793d9dee1ad1"}, - {file = "kframework-7.1.111.tar.gz", hash = "sha256:e9651b8df38fbf975e6eb82e7d0097d0c3461d442b4a9f38d587029a47143663"}, + {file = "kframework-7.1.112-py3-none-any.whl", hash = "sha256:bf0eae34aa35b67d831c91f314bd94a80c5a88a59cda77fc7399bafb0c2c8fe5"}, + {file = "kframework-7.1.112.tar.gz", hash = "sha256:d171197791d794e58a0e5b813e8ccde010bcc8d022e247cb1d2c71b8326ed15a"}, ] [package.dependencies] @@ -1035,19 +1035,19 @@ jupyter = ["ipywidgets (>=7.5.1,<9)"] [[package]] name = "setuptools" -version = "72.2.0" +version = "73.0.0" description = "Easily download, build, install, upgrade, and uninstall Python packages" optional = false python-versions = ">=3.8" files = [ - {file = "setuptools-72.2.0-py3-none-any.whl", hash = "sha256:f11dd94b7bae3a156a95ec151f24e4637fb4fa19c878e4d191bfb8b2d82728c4"}, - {file = "setuptools-72.2.0.tar.gz", hash = "sha256:80aacbf633704e9c8bfa1d99fa5dd4dc59573efcf9e4042c13d3bcef91ac2ef9"}, + {file = "setuptools-73.0.0-py3-none-any.whl", hash = "sha256:f2bfcce7ae1784d90b04c57c2802e8649e1976530bb25dc72c2b078d3ecf4864"}, + {file = "setuptools-73.0.0.tar.gz", hash = "sha256:3c08705fadfc8c7c445cf4d98078f0fafb9225775b2b4e8447e40348f82597c0"}, ] [package.extras] -core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.text (>=3.7)", "more-itertools (>=8.8)", "ordered-set (>=3.1.1)", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] +core = ["importlib-metadata (>=6)", "importlib-resources (>=5.10.2)", "jaraco.text (>=3.7)", "more-itertools (>=8.8)", "packaging (>=24)", "platformdirs (>=2.6.2)", "tomli (>=2.0.1)", "wheel (>=0.43.0)"] doc = ["furo", "jaraco.packaging (>=9.3)", "jaraco.tidelift (>=1.4)", "pygments-github-lexers (==0.0.5)", "pyproject-hooks (!=1.1)", "rst.linker (>=1.9)", "sphinx (>=3.5)", "sphinx-favicon", "sphinx-inline-tabs", "sphinx-lint", "sphinx-notfound-page (>=1,<2)", "sphinx-reredirects", "sphinxcontrib-towncrier", "towncrier (<24.7)"] -test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test", "mypy (==1.11.*)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (<0.4)", "pytest-ruff (>=0.2.1)", "pytest-ruff (>=0.3.2)", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel"] +test = ["build[virtualenv] (>=1.0.3)", "filelock (>=3.4.0)", "importlib-metadata", "ini2toml[lite] (>=0.14)", "jaraco.develop (>=7.21)", "jaraco.envs (>=2.2)", "jaraco.path (>=3.2.0)", "jaraco.test", "mypy (==1.11.*)", "packaging (>=23.2)", "pip (>=19.1)", "pyproject-hooks (!=1.1)", "pytest (>=6,!=8.1.*)", "pytest-checkdocs (>=2.4)", "pytest-cov", "pytest-enabler (>=2.2)", "pytest-home (>=0.5)", "pytest-mypy", "pytest-perf", "pytest-ruff (<0.4)", "pytest-ruff (>=0.2.1)", "pytest-ruff (>=0.3.2)", "pytest-subprocess", "pytest-timeout", "pytest-xdist (>=3)", "tomli", "tomli-w (>=1.0.0)", "virtualenv (>=13.0.0)", "wheel (>=0.44.0)"] [[package]] name = "sortedcontainers" @@ -1178,4 +1178,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "864ae8fe639baee8fbeaa7b42c7767a688d2c0883a623a65021d0673e3f2e674" +content-hash = "47dee8e19191e2121815e2ab8786768dfe3f17ad39533ba4ba9dccf5a68325f7" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 3487a8795e..5959475382 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -kframework = "7.1.111" +kframework = "7.1.112" tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/__main__.py b/kevm-pyk/src/kevm_pyk/__main__.py index aee82a3185..30c02a0783 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -357,7 +357,6 @@ def create_kcfg_explore() -> KCFGExplore: ), terminal_rules=KEVMSemantics.terminal_rules(options.break_every_step), fail_fast=options.fail_fast, - always_check_subsumption=options.always_check_subsumption, fast_check_subsumption=options.fast_check_subsumption, direct_subproof_rules=options.direct_subproof_rules, max_frontier_parallel=options.max_frontier_parallel, diff --git a/kevm-pyk/src/kevm_pyk/cli.py b/kevm-pyk/src/kevm_pyk/cli.py index 08da2d1593..89473a4d6d 100644 --- a/kevm-pyk/src/kevm_pyk/cli.py +++ b/kevm-pyk/src/kevm_pyk/cli.py @@ -375,7 +375,6 @@ def from_option_string() -> dict[str, str]: class KProveOptions(Options): debug_equations: list[str] - always_check_subsumption: bool fast_check_subsumption: bool direct_subproof_rules: bool maintenance_rate: int @@ -385,7 +384,6 @@ class KProveOptions(Options): def default() -> dict[str, Any]: return { 'debug_equations': [], - 'always_check_subsumption': True, 'fast_check_subsumption': False, 'direct_subproof_rules': False, 'maintenance_rate': 1, @@ -823,20 +821,6 @@ def kprove_args(self) -> ArgumentParser: type=list_of(str, delim=','), help='Comma-separated list of equations to debug.', ) - args.add_argument( - '--always-check-subsumption', - dest='always_check_subsumption', - default=None, - action='store_true', - help='Check subsumption even on non-terminal nodes (default, experimental).', - ) - args.add_argument( - '--no-always-check-subsumption', - dest='always_check_subsumption', - default=None, - action='store_false', - help='Do not check subsumption on non-terminal nodes (experimental).', - ) args.add_argument( '--fast-check-subsumption', dest='fast_check_subsumption', diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 38ceccba6c..d502841d3d 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -38,7 +38,7 @@ from pathlib import Path from typing import Final - from pyk.kast.inner import KAst + from pyk.kast.inner import KAst, Subst from pyk.kast.outer import KFlatModule from pyk.kcfg import KCFG from pyk.kcfg.semantics import KCFGExtendResult @@ -53,10 +53,12 @@ class KEVMSemantics(KCFGSemantics): auto_abstract_gas: bool allow_symbolic_program: bool + _cached_subst: Subst | None def __init__(self, auto_abstract_gas: bool = False, allow_symbolic_program: bool = False) -> None: self.auto_abstract_gas = auto_abstract_gas self.allow_symbolic_program = allow_symbolic_program + self._cached_subst = None @staticmethod def is_functional(term: KInner) -> bool: @@ -155,13 +157,11 @@ def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None: """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL. :param cterm: CTerm of a proof node. - :type cterm: CTerm :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned. - :rtype: KCFGExtendResult | None """ - load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')]) - subst = load_pattern.match(cterm.cell('K_CELL')) - if subst is not None: + if self.can_make_custom_step(cterm): + subst = self._cached_subst + assert subst is not None bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE']) jumpdests_set = compute_jumpdests(bytecode_sections) new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set)) @@ -213,6 +213,18 @@ def terminal_rules(break_every_step: bool) -> list[str]: terminal_rules.append('EVM.step') return terminal_rules + def can_make_custom_step(self, cterm: CTerm) -> bool: + """Given a CTerm, check if the rule 'EVM.program.load' is at the top of the K_CELL. + + This method checks if the `EVM.program.load` rule is at the top of the `K_CELL` in the given `cterm`. + If the rule matches, the resulting substitution is cached in `_cached_subst` for later use in `custom_step` + :param cterm: The CTerm representing the current state of the proof node. + :return: `True` if the pattern matches and a custom step can be made; `False` otherwise. + """ + load_pattern = KSequence([KApply('loadProgram', KVariable('###BYTECODE')), KVariable('###CONTINUATION')]) + self._cached_subst = load_pattern.match(cterm.cell('K_CELL')) + return self._cached_subst is not None + class KEVM(KProve, KRun): _use_hex: bool diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index b69a6340c8..4aeebc356a 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -106,7 +106,6 @@ def run_prover( terminal_rules: Iterable[str] = (), fail_fast: bool = False, counterexample_info: bool = False, - always_check_subsumption: bool = False, fast_check_subsumption: bool = False, direct_subproof_rules: bool = False, max_frontier_parallel: int = 1, @@ -127,7 +126,6 @@ def create_prover() -> APRProver: terminal_rules=terminal_rules, cut_point_rules=cut_point_rules, counterexample_info=counterexample_info, - always_check_subsumption=always_check_subsumption, fast_check_subsumption=fast_check_subsumption, direct_subproof_rules=direct_subproof_rules, assume_defined=assume_defined, diff --git a/kevm-pyk/src/tests/integration/test_prove.py b/kevm-pyk/src/tests/integration/test_prove.py index 35605a4260..f4814770b9 100644 --- a/kevm-pyk/src/tests/integration/test_prove.py +++ b/kevm-pyk/src/tests/integration/test_prove.py @@ -427,7 +427,6 @@ def _get_optimization_proofs() -> list[APRProof]: terminal_rules=[], cut_point_rules=['EVM.pc.inc', 'EVM.end-basic-block'], counterexample_info=False, - always_check_subsumption=True, fast_check_subsumption=True, ) for proof in _get_optimization_proofs():