diff --git a/deps/k_release b/deps/k_release index 5b7f57a99..1204e754d 100644 --- a/deps/k_release +++ b/deps/k_release @@ -1 +1 @@ -7.1.180 +7.1.184 diff --git a/deps/kevm_release b/deps/kevm_release index 1bbb95300..d00461b9d 100644 --- a/deps/kevm_release +++ b/deps/kevm_release @@ -1 +1 @@ -1.0.757 +1.0.759 diff --git a/flake.lock b/flake.lock index 4e373b2ba..ef700a43a 100644 --- a/flake.lock +++ b/flake.lock @@ -209,11 +209,11 @@ ] }, "locked": { - "lastModified": 1730625090, - "narHash": "sha256-lWfkkj+GEUM0UqYLD2Rx3zzILTL3xdmGJKGR4fwONpA=", + "lastModified": 1733217107, + "narHash": "sha256-T5rE+F85pRWkG7efabISw7ZNLgCBhnAg6egu5uGT4Bg=", "owner": "shazow", "repo": "foundry.nix", - "rev": "1c6a742bcbfd55a80de0e1f967a60174716a1560", + "rev": "b0534fca03a058756b4a405aacd5f5059a879673", "type": "github" }, "original": { @@ -275,16 +275,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" } @@ -390,16 +390,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" } @@ -435,16 +435,16 @@ ] }, "locked": { - "lastModified": 1732872362, - "narHash": "sha256-BWFSJXrs1ZE+hQj+Y3nWU08XA6XaUw2aaXeB7Bm13Gs=", + "lastModified": 1733417850, + "narHash": "sha256-Tkip8UkE9ccESQo8V57donxTCTtkj96A3GgTRhX6DKA=", "owner": "runtimeverification", "repo": "evm-semantics", - "rev": "03b0358b7d74846fcd2c9e186d54886c3ca30a2b", + "rev": "b608c9f69f31fcfc9992ff903586c7d057098337", "type": "github" }, "original": { "owner": "runtimeverification", - "ref": "v1.0.757", + "ref": "v1.0.759", "repo": "evm-semantics", "type": "github" } diff --git a/flake.nix b/flake.nix index 5c7a5fbbc..22e860eca 100644 --- a/flake.nix +++ b/flake.nix @@ -2,7 +2,7 @@ description = "Kontrol"; inputs = { - kevm.url = "github:runtimeverification/evm-semantics/v1.0.757"; + kevm.url = "github:runtimeverification/evm-semantics/v1.0.759"; nixpkgs.follows = "kevm/nixpkgs"; k-framework.follows = "kevm/k-framework"; flake-utils.follows = "kevm/flake-utils"; diff --git a/poetry.lock b/poetry.lock index bc587ccf1..c82431a6f 100644 --- a/poetry.lock +++ b/poetry.lock @@ -612,13 +612,13 @@ pyreadline3 = {version = "*", markers = "sys_platform == \"win32\" and python_ve [[package]] name = "hypothesis" -version = "6.121.2" +version = "6.122.1" description = "A library for property-based testing" optional = false python-versions = ">=3.9" files = [ - {file = "hypothesis-6.121.2-py3-none-any.whl", hash = "sha256:43edc07f9f4758807fc6cf10309dd6a376f3d6d886a5ef345ca49fe80ca3d394"}, - {file = "hypothesis-6.121.2.tar.gz", hash = "sha256:4c95ed50ef76cd073a43efab2d4c2297f0b3c85aafb6c1134aac0719dab56428"}, + {file = "hypothesis-6.122.1-py3-none-any.whl", hash = "sha256:59e52da0f2529b40f0b7bd0c3c61d8b3fe3337102800bf3534c53d4a8bdf8a6d"}, + {file = "hypothesis-6.122.1.tar.gz", hash = "sha256:23280e802eef88316b02cb32205d74b5bf2e3de4a378e2579a8974117c512b83"}, ] [package.dependencies] @@ -693,7 +693,7 @@ colors = ["colorama (>=0.4.6)"] [[package]] name = "kevm-pyk" -version = "1.0.757" +version = "1.0.759" description = "" optional = false python-versions = "^3.10" @@ -701,26 +701,26 @@ files = [] develop = false [package.dependencies] -kframework = "7.1.180" +kframework = "7.1.184" pathos = "*" tomlkit = "^0.11.6" [package.source] type = "git" url = "https://github.com/runtimeverification/evm-semantics.git" -reference = "v1.0.757" -resolved_reference = "03b0358b7d74846fcd2c9e186d54886c3ca30a2b" +reference = "v1.0.759" +resolved_reference = "b608c9f69f31fcfc9992ff903586c7d057098337" subdirectory = "kevm-pyk" [[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] @@ -1503,4 +1503,4 @@ type = ["pytest-mypy"] [metadata] lock-version = "2.0" python-versions = "^3.10" -content-hash = "1fd61b5067bdd3289b17686faf73c59f081693e3c88013aa6fe39ab06e2640b3" +content-hash = "70634a6e078393bedd5510d6ff723f0e2f8baaf78719536c7ed7a5a0aeb9723f" diff --git a/pyproject.toml b/pyproject.toml index 760cbd29b..659bc3af9 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.757", subdirectory = "kevm-pyk" } +kevm-pyk = { git = "https://github.com/runtimeverification/evm-semantics.git", tag = "v1.0.759", subdirectory = "kevm-pyk" } eth-utils = "^4.1.1" pycryptodome = "^3.20.0" pyevmasm = "^0.2.3" diff --git a/src/kontrol/kompile.py b/src/kontrol/kompile.py index 10864945c..51f4e48d6 100644 --- a/src/kontrol/kompile.py +++ b/src/kontrol/kompile.py @@ -15,7 +15,6 @@ from pyk.utils import ensure_dir_path, hash_str from . import VERSION -from .foundry import Foundry from .kdist.utils import KSRC_DIR from .solc_to_k import Contract, contract_to_main_module, contract_to_verification_module from .utils import _read_digest_file, _rv_blue, console, kontrol_up_to_date @@ -24,8 +23,7 @@ from collections.abc import Iterable from typing import Final - from pyk.kast.inner import KInner - + from .foundry import Foundry from .options import BuildOptions _LOGGER: Final = logging.getLogger(__name__) @@ -108,10 +106,7 @@ def foundry_kompile( copied_requires = [] copied_requires += [f'requires/{name}' for name in list(requires_paths.keys())] - kevm = KEVM(kdist.get('kontrol.foundry')) - empty_config = kevm.definition.empty_config(Foundry.Sorts.FOUNDRY_CELL) bin_runtime_definition = _foundry_to_contract_def( - empty_config=empty_config, contracts=foundry.contracts.values(), requires=['foundry.md'], enums=foundry.enums, @@ -119,7 +114,6 @@ def foundry_kompile( contract_main_definition = _foundry_to_main_def( main_module=main_module, - empty_config=empty_config, contracts=foundry.contracts.values(), requires=(['contracts.k'] + copied_requires), imports=_imports, @@ -193,14 +187,11 @@ def should_rekompile() -> bool: def _foundry_to_contract_def( - empty_config: KInner, contracts: Iterable[Contract], requires: Iterable[str], enums: dict[str, int], ) -> KDefinition: - modules = [ - contract_to_main_module(contract, empty_config, imports=['FOUNDRY'], enums=enums) for contract in contracts - ] + modules = [contract_to_main_module(contract, imports=['FOUNDRY'], enums=enums) for contract in contracts] # First module is chosen as main module arbitrarily, since the contract definition is just a set of # contract modules. main_module = Contract.contract_to_module_name(list(contracts)[0].name_with_path) @@ -215,15 +206,13 @@ def _foundry_to_contract_def( def _foundry_to_main_def( main_module: str, contracts: Iterable[Contract], - empty_config: KInner, requires: Iterable[str], imports: dict[str, list[str]], keccak_lemmas: bool, auxiliary_lemmas: bool, ) -> KDefinition: modules = [ - contract_to_verification_module(contract, empty_config, imports=imports[contract.name_with_path]) - for contract in contracts + contract_to_verification_module(contract, imports=imports[contract.name_with_path]) for contract in contracts ] _main_module = KFlatModule( main_module, diff --git a/src/kontrol/solc_to_k.py b/src/kontrol/solc_to_k.py index 02d0c8cf4..e16598ca9 100644 --- a/src/kontrol/solc_to_k.py +++ b/src/kontrol/solc_to_k.py @@ -35,8 +35,6 @@ def solc_to_k(options: SolcToKOptions) -> str: definition_dir = kdist.get('evm-semantics.haskell') - kevm = KEVM(definition_dir) - empty_config = kevm.definition.empty_config(KEVM.Sorts.KEVM_CELL) solc_json = solc_compile(options.contract_file) contract_json = solc_json['contracts'][options.contract_file.name][options.contract_name] @@ -49,7 +47,7 @@ def solc_to_k(options: SolcToKOptions) -> str: imports = list(options.imports) requires = list(options.requires) - contract_module = contract_to_main_module(contract, empty_config, enums={}, imports=['EDSL'] + imports) + contract_module = contract_to_main_module(contract, enums={}, imports=['EDSL'] + imports) _main_module = KFlatModule( options.main_module if options.main_module else 'MAIN', [], @@ -1175,14 +1173,12 @@ def solc_compile(contract_file: Path) -> dict[str, Any]: return result -def contract_to_main_module( - contract: Contract, empty_config: KInner, enums: dict[str, int], imports: Iterable[str] = () -) -> KFlatModule: +def contract_to_main_module(contract: Contract, enums: dict[str, int], imports: Iterable[str] = ()) -> KFlatModule: module_name = Contract.contract_to_module_name(contract.name_with_path) return KFlatModule(module_name, contract.sentences(enums), [KImport(i) for i in list(imports)]) -def contract_to_verification_module(contract: Contract, empty_config: KInner, imports: Iterable[str]) -> KFlatModule: +def contract_to_verification_module(contract: Contract, imports: Iterable[str]) -> KFlatModule: main_module_name = Contract.contract_to_module_name(contract.name_with_path) verification_module_name = Contract.contract_to_verification_module_name(contract.name_with_path) return KFlatModule(verification_module_name, [], [KImport(main_module_name)] + [KImport(i) for i in list(imports)])