remove unused empty_config arg (#901)

runtimeverification · Dec 4, 2024 · 1a953d9 · 1a953d9
1 parent 3311bbe
commit 1a953d9
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 21 deletions.
diff --git 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,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,

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