Use EVMChainOptions in Kontrol

src/kontrol/cli.py

@@ -419,6 +419,7 @@ def parse(s: str) -> list[T]:
             kontrol_cli_args.bug_report_args,
             kontrol_cli_args.explore_args,
             kontrol_cli_args.foundry_args,
+            kontrol_cli_args.evm_chain_args,
             config_args.config_args,
         ],
     )
@@ -466,7 +467,7 @@ def parse(s: str) -> list[T]:
         help='Include the contract constructor in the test execution.',
     )
     prove_args.add_argument(
-        '--use-gas', dest='use_gas', default=None, action='store_true', help='Enables gas computation in KEVM.'
+        '--use-gas', dest='usegas', default=None, action='store_true', help='Enables gas computation in KEVM.'
     )
     prove_args.add_argument(
         '--config-type', default=None, type=ConfigType, help='Config type', choices=list(ConfigType)
@@ -577,17 +578,6 @@ def parse(s: str) -> list[T]:
             "'maintenance-rate', 'smt-timeout', 'smt-retry-limit', 'max-depth', and 'max-iterations'."
         ),
     )
-    prove_args.add_argument(
-        '--schedule',
-        type=str,
-        default='Shanghai',
-        dest='schedule',
-        help=(
-            'Specify the name of the EVM hardfork to use during verification. '
-            'Available options: Cancun, Shanghai, Merge, London, Berlin, Istanbul, Petersburg, Constantinople, '
-            'Byzantium, Spurious Dragon, Tangerine Whistle, Homestead, Frontier, Default.'
-        ),
-    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/options.py

@@ -4,7 +4,16 @@
 from pathlib import Path
 from typing import TYPE_CHECKING, Any
 
-from kevm_pyk.cli import DisplayOptions, ExploreOptions, KCFGShowOptions, KOptions, KProveOptions, list_of, node_id_like
+from kevm_pyk.cli import (
+    DisplayOptions,
+    EVMChainOptions,
+    ExploreOptions,
+    KCFGShowOptions,
+    KOptions,
+    KProveOptions,
+    list_of,
+    node_id_like,
+)
 from kevm_pyk.kompile import KompileTarget
 from kevm_pyk.utils import arg_pair_of
 from pyk.cli.args import BugReportOptions, KompileOptions, LoggingOptions, Options, ParallelOptions, SMTOptions
@@ -348,12 +357,12 @@ class ProveOptions(
     ExploreOptions,
     FoundryOptions,
     TraceOptions,
+    EVMChainOptions,
 ):
     tests: list[tuple[str, int | None]]
     reinit: bool
     bmc_depth: int | None
     run_constructor: bool
-    use_gas: bool
     setup_version: int | None
     break_on_cheatcodes: bool
     recorded_diff_state_path: Path | None
@@ -369,7 +378,6 @@ class ProveOptions(
     hide_status_bar: bool
     remove_old_proofs: bool
     optimize_performance: int | None
-    schedule: str
 
     def __init__(self, args: dict[str, Any]) -> None:
         super().__init__(args)
@@ -382,7 +390,7 @@ def default() -> dict[str, Any]:
             'reinit': False,
             'bmc_depth': None,
             'run_constructor': False,
-            'use_gas': False,
+            'usegas': False,
             'break_on_cheatcodes': False,
             'recorded_diff_state_path': None,
             'recorded_dump_state_path': None,
@@ -398,7 +406,6 @@ def default() -> dict[str, Any]:
             'hide_status_bar': False,
             'remove_old_proofs': False,
             'optimize_performance': None,
-            'schedule': 'Shanghai',
         }
 
     @staticmethod
@@ -414,6 +421,7 @@ def from_option_string() -> dict[str, str]:
             | ExploreOptions.from_option_string()
             | FoundryOptions.from_option_string()
             | TraceOptions.from_option_string()
+            | EVMChainOptions.from_option_string()
             | {
                 'match-test': 'tests',
                 'init-node-from-diff': 'recorded_diff_state_path',
@@ -435,6 +443,7 @@ def get_argument_type() -> dict[str, Callable]:
             | ExploreOptions.get_argument_type()
             | FoundryOptions.get_argument_type()
             | TraceOptions.get_argument_type()
+            | EVMChainOptions.get_argument_type()
             | {
                 'match-test': list_of(parse_test_version_tuple),
                 'init-node-from': file_path,

src/kontrol/prove.py

@@ -9,6 +9,7 @@
 from subprocess import CalledProcessError
 from typing import TYPE_CHECKING, Any, ContextManager, NamedTuple
 
+from kevm_pyk.cli import EVMChainOptions
 from kevm_pyk.kevm import KEVM, KEVMSemantics, _process_jumpdests
 from kevm_pyk.utils import KDefinition__expand_macros, abstract_cell_vars, run_prover
 from multiprocess.pool import Pool  # type: ignore
@@ -405,13 +406,19 @@ def create_kcfg_explore() -> KCFGExplore:
                     kcfg_explore=create_kcfg_explore(),
                     bmc_depth=options.bmc_depth,
                     run_constructor=options.run_constructor,
-                    use_gas=options.use_gas,
                     recorded_state_entries=recorded_state_entries,
                     summary_ids=summary_ids,
                     active_symbolik=options.with_non_general_state,
                     hevm=options.hevm,
                     config_type=options.config_type,
-                    schedule=options.schedule,
+                    evm_chain_options=EVMChainOptions(
+                        {
+                            'schedule': options.schedule,
+                            'chainid': options.chainid,
+                            'mode': options.mode,
+                            'usegas': options.usegas,
+                        }
+                    ),
                     trace_options=TraceOptions(
                         {
                             'active_tracing': options.active_tracing,
@@ -553,10 +560,9 @@ def method_to_apr_proof(
     foundry: Foundry,
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
-    schedule: str,
+    evm_chain_options: EVMChainOptions,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
-    use_gas: bool = False,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None,
     summary_ids: Iterable[str] = (),
     active_symbolik: bool = False,
@@ -581,13 +587,12 @@ def method_to_apr_proof(
         kcfg_explore=kcfg_explore,
         setup_proof=setup_proof,
         graft_setup_proof=((setup_proof is not None) and not setup_proof_is_constructor),
-        use_gas=use_gas,
+        evm_chain_options=evm_chain_options,
         recorded_state_entries=recorded_state_entries,
         active_symbolik=active_symbolik,
         hevm=hevm,
         trace_options=trace_options,
         config_type=config_type,
-        schedule=schedule,
     )
 
     apr_proof = APRProof(
@@ -624,11 +629,10 @@ def _method_to_initialized_cfg(
     test: FoundryTest,
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
-    schedule: str,
+    evm_chain_options: EVMChainOptions,
     *,
     setup_proof: APRProof | None = None,
     graft_setup_proof: bool = False,
-    use_gas: bool = False,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None,
     active_symbolik: bool = False,
     hevm: bool = False,
@@ -644,11 +648,10 @@ def _method_to_initialized_cfg(
         test.method,
         setup_proof,
         graft_setup_proof,
-        use_gas,
+        evm_chain_options,
         recorded_state_entries,
         active_symbolik,
         config_type=config_type,
-        schedule=schedule,
         hevm=hevm,
         trace_options=trace_options,
     )
@@ -681,11 +684,10 @@ def _method_to_cfg(
     method: Contract.Method | Contract.Constructor,
     setup_proof: APRProof | None,
     graft_setup_proof: bool,
-    use_gas: bool,
+    evm_chain_options: EVMChainOptions,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None,
     active_symbolik: bool,
     config_type: ConfigType,
-    schedule: str,
     hevm: bool = False,
     trace_options: TraceOptions | None = None,
 ) -> tuple[KCFG, list[int], int, int]:
@@ -710,14 +712,13 @@ def _method_to_cfg(
         contract_code=bytesToken(contract_code),
         storage_fields=contract.fields,
         method=method,
-        use_gas=use_gas,
+        evm_chain_options=evm_chain_options,
         recorded_state_entries=recorded_state_entries,
         calldata=calldata,
         callvalue=callvalue,
         active_symbolik=active_symbolik,
         trace_options=trace_options,
         config_type=config_type,
-        schedule=schedule,
     )
     new_node_ids = []
 
@@ -955,28 +956,27 @@ def _init_cterm(
     contract_code: KInner,
     storage_fields: tuple[StorageField, ...],
     method: Contract.Method | Contract.Constructor,
-    use_gas: bool,
     config_type: ConfigType,
-    schedule: str,
     active_symbolik: bool,
+    evm_chain_options: EVMChainOptions,
     *,
     calldata: KInner | None = None,
     callvalue: KInner | None = None,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None,
     trace_options: TraceOptions | None = None,
 ) -> CTerm:
-    schedule = '_'.join(schedule.split()).upper() + '_EVM'
-    schedule_name = KApply(schedule)
+    schedule = KApply(evm_chain_options.schedule + '_EVM')
     contract_name = contract_name.upper()
 
     if not trace_options:
         trace_options = TraceOptions({})
 
     jumpdests = bytesToken(_process_jumpdests(bytecode=program))
     init_subst = {
-        'MODE_CELL': KApply('NORMAL'),
-        'USEGAS_CELL': TRUE if use_gas else FALSE,
-        'SCHEDULE_CELL': schedule_name,
+        'MODE_CELL': KApply(evm_chain_options.mode),
+        'USEGAS_CELL': TRUE if evm_chain_options.usegas else FALSE,
+        'SCHEDULE_CELL': schedule,
+        'CHAINID_CELL': intToken(evm_chain_options.chainid),
         'STATUSCODE_CELL': KVariable('STATUSCODE'),
         'PROGRAM_CELL': bytesToken(program),
         'JUMPDESTS_CELL': jumpdests,
@@ -1064,7 +1064,7 @@ def _init_cterm(
     if callvalue is not None:
         init_subst['CALLVALUE_CELL'] = callvalue
 
-    if not use_gas:
+    if not evm_chain_options.usegas:
         init_subst['GAS_CELL'] = intToken(0)
         init_subst['CALLGAS_CELL'] = intToken(0)
         init_subst['REFUND_CELL'] = intToken(0)

src/tests/integration/test_foundry_prove.py

@@ -117,7 +117,7 @@ def test_foundry_prove(
                 'tests': [(test_id, None)],
                 'bug_report': bug_report,
                 'break_on_calls': test_id in SHOW_TESTS,
-                'use_gas': test_id in GAS_TESTS,
+                'usegas': test_id in GAS_TESTS,
                 'port': server.port,
                 'force_sequential': force_sequential,
             }
@@ -589,7 +589,7 @@ def test_foundry_auto_abstraction(
                 'auto_abstract_gas': True,
                 'bug_report': bug_report,
                 'break_on_calls': True,
-                'use_gas': True,
+                'usegas': True,
                 'port': server.port,
                 'force_sequential': force_sequential,
             }

src/tests/integration/test_kontrol.py

@@ -109,7 +109,7 @@ def test_kontrol_end_to_end(
                 'tests': [(test_id, None)],
                 'bug_report': bug_report,
                 'break_on_calls': False,
-                'use_gas': False,
+                'usegas': False,
                 'port': server_end_to_end.port,
                 'force_sequential': force_sequential,
             }