diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py index 4aa4b1c15..deaf98fd3 100644 --- a/src/kontrol/cli.py +++ b/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', diff --git a/src/kontrol/options.py b/src/kontrol/options.py index a73f26dbd..cf0bbe1aa 100644 --- a/src/kontrol/options.py +++ b/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, diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index 8a98791c0..8d2fc102a 100644 --- a/src/kontrol/prove.py +++ b/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,18 +956,16 @@ 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: @@ -974,9 +973,10 @@ def _init_cterm( 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) diff --git a/src/tests/integration/test_foundry_prove.py b/src/tests/integration/test_foundry_prove.py index 1778a8828..43aeb39c1 100644 --- a/src/tests/integration/test_foundry_prove.py +++ b/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, } diff --git a/src/tests/integration/test_kontrol.py b/src/tests/integration/test_kontrol.py index c0102b1c4..a9e81669e 100644 --- a/src/tests/integration/test_kontrol.py +++ b/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, }