Add --schedule to kontrol prove

runtimeverification · Aug 29, 2024 · e8c507f · e8c507f
1 parent 75b7e0e
commit e8c507f
Show file tree

Hide file tree

Showing 3 changed files with 24 additions and 2 deletions.
diff --git a/src/kontrol/cli.py b/src/kontrol/cli.py
@@ -577,6 +577,17 @@ 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
@@ -369,6 +369,7 @@ 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)
@@ -397,6 +398,7 @@ def default() -> dict[str, Any]:
             'hide_status_bar': False,
             'remove_old_proofs': False,
             'optimize_performance': None,
+            'schedule': 'Shanghai',
         }
 
     @staticmethod

diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
@@ -411,6 +411,7 @@ def create_kcfg_explore() -> KCFGExplore:
                     active_symbolik=options.with_non_general_state,
                     hevm=options.hevm,
                     config_type=options.config_type,
+                    schedule=options.schedule,
                     trace_options=TraceOptions(
                         {
                             'active_tracing': options.active_tracing,
@@ -552,6 +553,7 @@ def method_to_apr_proof(
     foundry: Foundry,
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
+    schedule: str,
     bmc_depth: int | None = None,
     run_constructor: bool = False,
     use_gas: bool = False,
@@ -585,6 +587,7 @@ def method_to_apr_proof(
         hevm=hevm,
         trace_options=trace_options,
         config_type=config_type,
+        schedule=schedule,
     )
 
     apr_proof = APRProof(
@@ -621,6 +624,7 @@ def _method_to_initialized_cfg(
     test: FoundryTest,
     kcfg_explore: KCFGExplore,
     config_type: ConfigType,
+    schedule: str,
     *,
     setup_proof: APRProof | None = None,
     graft_setup_proof: bool = False,
@@ -644,6 +648,7 @@ def _method_to_initialized_cfg(
         recorded_state_entries,
         active_symbolik,
         config_type=config_type,
+        schedule=schedule,
         hevm=hevm,
         trace_options=trace_options,
     )
@@ -680,6 +685,7 @@ def _method_to_cfg(
     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]:
@@ -711,6 +717,7 @@ def _method_to_cfg(
         active_symbolik=active_symbolik,
         trace_options=trace_options,
         config_type=config_type,
+        schedule=schedule,
     )
     new_node_ids = []
 
@@ -950,14 +957,16 @@ def _init_cterm(
     method: Contract.Method | Contract.Constructor,
     use_gas: bool,
     config_type: ConfigType,
+    schedule: str,
     active_symbolik: bool,
     *,
     calldata: KInner | None = None,
     callvalue: KInner | None = None,
     recorded_state_entries: Iterable[StateDiffEntry] | Iterable[StateDumpEntry] | None = None,
     trace_options: TraceOptions | None = None,
 ) -> CTerm:
-    schedule = KApply('SHANGHAI_EVM')
+    schedule = '_'.join(schedule.split()).upper() + '_EVM'
+    schedule_name = KApply(schedule)
     contract_name = contract_name.upper()
 
     if not trace_options:
@@ -967,7 +976,7 @@ def _init_cterm(
     init_subst = {
         'MODE_CELL': KApply('NORMAL'),
         'USEGAS_CELL': TRUE if use_gas else FALSE,
-        'SCHEDULE_CELL': schedule,
+        'SCHEDULE_CELL': schedule_name,
         'STATUSCODE_CELL': KVariable('STATUSCODE'),
         'PROGRAM_CELL': bytesToken(program),
         'JUMPDESTS_CELL': jumpdests,