diff --git a/deps/k_release b/deps/k_release index 5b7f57a995..1204e754d3 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.180 +7.1.184 diff --git a/flake.lock b/flake.lock index 062ef8253d..c439127dac 100644 --- a/flake.lock +++ b/flake.lock @@ -243,16 +243,16 @@ "z3": "z3_2" }, "locked": { - "lastModified": 1732696861, - "narHash": "sha256-gL/m08eSp07XvdTBG4+IniP3ciB4MPiyuNkl/4Cs1/U=", + "lastModified": 1733283993, + "narHash": "sha256-CK126KzmZQfPqqn0SFba1vg4DL/V/13dsjcFareE8Lo=", "owner": "runtimeverification", "repo": "haskell-backend", - "rev": "0a9f66963ea3e13bcec32f5d2c4f480bf0acf65e", + "rev": "1b6cacb3eab29c7e449b2d255321c3ed348f4229", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.101", + "ref": "v0.1.104", "repo": "haskell-backend", "type": "github" } @@ -352,16 +352,16 @@ ] }, "locked": { - "lastModified": 1732784580, - "narHash": "sha256-2e5gPnT2C1dImYSK9GMctKfYcFy1MaUh4HaXiID/cPU=", + "lastModified": 1733394552, + "narHash": "sha256-va6BP79v7ZrIBZR6WmVa8FNggvcHcfxcU4DOwz7lyEU=", "owner": "runtimeverification", "repo": "k", - "rev": "1095542f14bb9c963812926fd44c170f11297a7e", + "rev": "bb18443ebbe11d90674606828f3165bfe4fca1f9", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.1.180", + "ref": "v7.1.184", "repo": "k", "type": "github" } diff --git a/flake.nix b/flake.nix index cc34ed8228..768819f52e 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "A flake for the KEVM Semantics"; inputs = { - k-framework.url = "github:runtimeverification/k/v7.1.180"; + k-framework.url = "github:runtimeverification/k/v7.1.184"; nixpkgs.follows = "k-framework/nixpkgs"; flake-utils.follows = "k-framework/flake-utils"; rv-utils.follows = "k-framework/rv-utils"; diff --git a/kevm-pyk/poetry.lock b/kevm-pyk/poetry.lock index 2467d4c54c..4e31118959 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -441,13 +441,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.121.0" +version = "6.122.1" description = "A library for property-based testing" optional = false python-versions = ">=3.9" files = [ - {file = "hypothesis-6.121.0-py3-none-any.whl", hash = "sha256:7f62ec69a217e06adc6791eda4464fafd2f8d95b7bfe89a7120700cfac604adb"}, - {file = "hypothesis-6.121.0.tar.gz", hash = "sha256:99f6b38eacefbd7e10ddd3a716f242f4cfaabb3a332ff6b286f8314084d0be84"}, + {file = "hypothesis-6.122.1-py3-none-any.whl", hash = "sha256:59e52da0f2529b40f0b7bd0c3c61d8b3fe3337102800bf3534c53d4a8bdf8a6d"}, + {file = "hypothesis-6.122.1.tar.gz", hash = "sha256:23280e802eef88316b02cb32205d74b5bf2e3de4a378e2579a8974117c512b83"}, ] [package.dependencies] @@ -456,10 +456,10 @@ exceptiongroup = {version = ">=1.0.0", markers = "python_version < \"3.11\""} sortedcontainers = ">=2.1.0,<3.0.0" [package.extras] -all = ["black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.77)", "django (>=4.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.18)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.19.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"] +all = ["black (>=19.10b0)", "click (>=7.0)", "crosshair-tool (>=0.0.78)", "django (>=4.2)", "dpcontracts (>=0.4)", "hypothesis-crosshair (>=0.0.18)", "lark (>=0.10.1)", "libcst (>=0.3.16)", "numpy (>=1.19.3)", "pandas (>=1.1)", "pytest (>=4.6)", "python-dateutil (>=1.4)", "pytz (>=2014.1)", "redis (>=3.0.0)", "rich (>=9.0.0)", "tzdata (>=2024.2)"] cli = ["black (>=19.10b0)", "click (>=7.0)", "rich (>=9.0.0)"] codemods = ["libcst (>=0.3.16)"] -crosshair = ["crosshair-tool (>=0.0.77)", "hypothesis-crosshair (>=0.0.18)"] +crosshair = ["crosshair-tool (>=0.0.78)", "hypothesis-crosshair (>=0.0.18)"] dateutil = ["python-dateutil (>=1.4)"] django = ["django (>=4.2)"] dpcontracts = ["dpcontracts (>=0.4)"] @@ -536,13 +536,13 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kframework" -version = "7.1.180" +version = "7.1.184" description = "" optional = false python-versions = "<4.0,>=3.10" files = [ - {file = "kframework-7.1.180-py3-none-any.whl", hash = "sha256:9eaa81cc42c71efdee2edf5c6687410c732d489ebb5481f0a9c79484f0779ba0"}, - {file = "kframework-7.1.180.tar.gz", hash = "sha256:e6e55d057d89c26a2760ee68d6be8836607d99f81847e456ba1d72bc6e9744e2"}, + {file = "kframework-7.1.184-py3-none-any.whl", hash = "sha256:76739895f1947ed78ea9d59e54851daa705d5ca66edabde839cbf7dc1482ada9"}, + {file = "kframework-7.1.184.tar.gz", hash = "sha256:abaea1c279d3367871b11324236ceb0625b5259877bde3de53f31e8d3bec25a8"}, ] [package.dependencies] @@ -1267,4 +1267,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "3c3ab9ffd38b9bacc782ed5c14f94457ecb6505f83d1dd172ebfa82b00426f85" +content-hash = "b70dae0148741cc3fef5c2ef58a617630d29caad4a619952dfec7b9c4df46e8c" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index de34f8253e..ebad00d15d 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.180" +kframework = "7.1.184" tomlkit = "^0.11.6" [tool.poetry.group.dev.dependencies] diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py index 82f8c788d3..d27c971ed5 100644 --- a/kevm-pyk/src/kevm_pyk/kevm.py +++ b/kevm-pyk/src/kevm_pyk/kevm.py @@ -37,6 +37,7 @@ from pathlib import Path from typing import Final + from pyk.cterm import CTermSymbolic from pyk.kast.inner import KAst, Subst from pyk.kast.outer import KFlatModule from pyk.kcfg import KCFG @@ -144,7 +145,7 @@ def _replace(term: KInner) -> KInner: return CTerm(config=bottom_up(_replace, cterm.config), constraints=cterm.constraints) - def custom_step(self, cterm: CTerm) -> KCFGExtendResult | None: + def custom_step(self, cterm: CTerm, _cterm_symbolic: CTermSymbolic) -> 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.