Merge branch 'master' into abstraction-cheatcodes

deps/k_release

@@ -1 +1 @@
-7.1.180
+7.1.184

deps/kevm_release

@@ -1 +1 @@
-1.0.757
+1.0.759

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";

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"

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,18 +106,14 @@ 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,
         )
 
         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,

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)])