diff --git a/deps/k_release b/deps/k_release index 92d74b933f..49672789e7 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.0.114 +7.0.119 diff --git a/flake.lock b/flake.lock index 8cf8f8a4f1..6775461bb7 100644 --- a/flake.lock +++ b/flake.lock @@ -208,16 +208,16 @@ "rv-utils": "rv-utils_3" }, "locked": { - "lastModified": 1717603356, - "narHash": "sha256-+XD9c8XcKI5x3XZCVXpFQbtBHn2Kiply1wZ7NHWENUs=", + "lastModified": 1717694753, + "narHash": "sha256-CCLIlYVNu09HtAxNPBVLe4JkdV6azkPyqaGL6g1UVo8=", "owner": "runtimeverification", "repo": "k", - "rev": "9629a8dfd046db68e27efc7b1c9accd783000004", + "rev": "f512f333f79e6066d1eb6a66db76acd554e92c55", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v7.0.114", + "ref": "v7.0.119", "repo": "k", "type": "github" } @@ -259,16 +259,16 @@ ] }, "locked": { - "lastModified": 1717532732, - "narHash": "sha256-0VTqGrolstZlxtd6DRmoWnJsYO+BB8i+PniGKenB34I=", + "lastModified": 1717613611, + "narHash": "sha256-5rDBlXOfvxYNei+mL949pV6TIE5oAfY6LKxV/AcU3Mo=", "owner": "runtimeverification", "repo": "llvm-backend", - "rev": "caca83fbec616482760697fbf7620c45e9b560b7", + "rev": "744a6150c4e616edcd60faf9786cc27780c364ad", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v0.1.42", + "ref": "v0.1.44", "repo": "llvm-backend", "type": "github" } @@ -413,17 +413,17 @@ }, "locked": { "dir": "pyk", - "lastModified": 1717603356, - "narHash": "sha256-+XD9c8XcKI5x3XZCVXpFQbtBHn2Kiply1wZ7NHWENUs=", + "lastModified": 1717694753, + "narHash": "sha256-CCLIlYVNu09HtAxNPBVLe4JkdV6azkPyqaGL6g1UVo8=", "owner": "runtimeverification", "repo": "k", - "rev": "9629a8dfd046db68e27efc7b1c9accd783000004", + "rev": "f512f333f79e6066d1eb6a66db76acd554e92c55", "type": "github" }, "original": { "dir": "pyk", "owner": "runtimeverification", - "ref": "v7.0.114", + "ref": "v7.0.119", "repo": "k", "type": "github" } diff --git a/flake.nix b/flake.nix index 350a5bc0e3..d5350b2066 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.0.114"; + k-framework.url = "github:runtimeverification/k/v7.0.119"; 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.0.114?dir=pyk"; + pyk.url = "github:runtimeverification/k/v7.0.119?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 b75df1f06e..fdeb8e3e29 100644 --- a/kevm-pyk/poetry.lock +++ b/kevm-pyk/poetry.lock @@ -814,7 +814,7 @@ windows-terminal = ["colorama (>=0.4.6)"] [[package]] name = "pyk" -version = "7.0.114" +version = "7.0.119" description = "" optional = false python-versions = "^3.10" @@ -835,8 +835,8 @@ xdg-base-dirs = "^6.0.1" [package.source] type = "git" url = "https://github.com/runtimeverification/k.git" -reference = "v7.0.114" -resolved_reference = "9629a8dfd046db68e27efc7b1c9accd783000004" +reference = "v7.0.119" +resolved_reference = "f512f333f79e6066d1eb6a66db76acd554e92c55" subdirectory = "pyk" [[package]] @@ -1116,4 +1116,4 @@ test = ["big-O", "importlib-resources", "jaraco.functools", "jaraco.itertools", [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "2ad0313020cff78b809d5e32b09839482ae10979baad535ce9d79ca0d21d38d6" +content-hash = "3c47463cd7a88cc3197be9d65d65d47382767a873d78e13f0a78771eb0653190" diff --git a/kevm-pyk/pyproject.toml b/kevm-pyk/pyproject.toml index 60efeb2750..3073acd506 100644 --- a/kevm-pyk/pyproject.toml +++ b/kevm-pyk/pyproject.toml @@ -13,7 +13,7 @@ authors = [ [tool.poetry.dependencies] python = "^3.10" pathos = "*" -pyk = { git = "https://github.com/runtimeverification/k.git", tag="v7.0.114", subdirectory = "pyk" } +pyk = { git = "https://github.com/runtimeverification/k.git", tag="v7.0.119", subdirectory = "pyk" } 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 a7693f147a..567368a6e4 100644 --- a/kevm-pyk/src/kevm_pyk/__main__.py +++ b/kevm-pyk/src/kevm_pyk/__main__.py @@ -340,9 +340,7 @@ def create_kcfg_explore() -> KCFGExplore: bug_report_id=claim.label, dispatch=dispatch, ) - cterm_symbolic = CTermSymbolic( - client, kevm.definition, kevm.kompiled_kore, trace_rewrites=options.trace_rewrites - ) + cterm_symbolic = CTermSymbolic(client, kevm.definition, trace_rewrites=options.trace_rewrites) return KCFGExplore( cterm_symbolic, kcfg_semantics=KEVMSemantics(auto_abstract_gas=options.auto_abstract_gas), diff --git a/kevm-pyk/src/kevm_pyk/utils.py b/kevm-pyk/src/kevm_pyk/utils.py index 7e0956ccaf..27e61ee0aa 100644 --- a/kevm-pyk/src/kevm_pyk/utils.py +++ b/kevm-pyk/src/kevm_pyk/utils.py @@ -438,9 +438,7 @@ def legacy_explore( no_post_exec_simplify=no_post_exec_simplify, ) as server: with KoreClient('localhost', server.port, bug_report=bug_report, bug_report_id=id) as client: - cterm_symbolic = CTermSymbolic( - client, kprint.definition, kprint.kompiled_kore, trace_rewrites=trace_rewrites - ) + cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites) yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id) else: if port is None: @@ -457,7 +455,5 @@ def legacy_explore( ], } with KoreClient('localhost', port, bug_report=bug_report, bug_report_id=id, dispatch=dispatch) as client: - cterm_symbolic = CTermSymbolic( - client, kprint.definition, kprint.kompiled_kore, trace_rewrites=trace_rewrites - ) + cterm_symbolic = CTermSymbolic(client, kprint.definition, trace_rewrites=trace_rewrites) yield KCFGExplore(cterm_symbolic, kcfg_semantics=kcfg_semantics, id=id)