Encapsulate program-level options

package/version

@@ -1 +1 @@
-0.1.32
+0.1.33

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kontrol"
-version = "0.1.32"
+version = "0.1.33"
 description = "Foundry integration for KEVM"
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/kontrol/__init__.py

@@ -5,4 +5,4 @@
 if TYPE_CHECKING:
     from typing import Final
 
-VERSION: Final = '0.1.32'
+VERSION: Final = '0.1.33'

src/kontrol/__main__.py

@@ -28,6 +28,7 @@
     foundry_to_dot,
 )
 from .kompile import foundry_kompile
+from .options import ProveOptions
 from .prove import foundry_prove
 from .solc_to_k import solc_compile, solc_to_k
 
@@ -160,6 +161,7 @@ def exec_prove(
     trace_rewrites: bool = False,
     auto_abstract_gas: bool = False,
     run_constructor: bool = False,
+    fail_fast: bool = False,
     **kwargs: Any,
 ) -> None:
     _ignore_arg(kwargs, 'main_module', f'--main-module: {kwargs["main_module"]}')
@@ -175,26 +177,30 @@ def exec_prove(
     if isinstance(kore_rpc_command, str):
         kore_rpc_command = kore_rpc_command.split()
 
-    results = foundry_prove(
-        foundry_root=foundry_root,
-        max_depth=max_depth,
-        max_iterations=max_iterations,
+    options = ProveOptions(
+        auto_abstract_gas=auto_abstract_gas,
         reinit=reinit,
-        tests=tests,
-        workers=workers,
-        break_every_step=break_every_step,
-        break_on_jumpi=break_on_jumpi,
-        break_on_calls=break_on_calls,
-        bmc_depth=bmc_depth,
         bug_report=bug_report,
         kore_rpc_command=kore_rpc_command,
-        use_booster=use_booster,
-        counterexample_info=counterexample_info,
         smt_timeout=smt_timeout,
         smt_retry_limit=smt_retry_limit,
         trace_rewrites=trace_rewrites,
-        auto_abstract_gas=auto_abstract_gas,
+        bmc_depth=bmc_depth,
+        max_depth=max_depth,
+        break_every_step=break_every_step,
+        break_on_jumpi=break_on_jumpi,
+        break_on_calls=break_on_calls,
+        workers=workers,
+        counterexample_info=counterexample_info,
+        max_iterations=max_iterations,
         run_constructor=run_constructor,
+        fail_fast=fail_fast,
+    )
+
+    results = foundry_prove(
+        foundry_root=foundry_root,
+        options=options,
+        tests=tests,
     )
     failed = 0
     for pid, r in results.items():
@@ -526,6 +532,13 @@ def _parse_test_version_tuple(value: str) -> tuple[str, int | None]:
         action='store_true',
         help='Include the contract constructor in the test execution.',
     )
+    prove_args.add_argument(
+        '--fail-fast',
+        dest='fail_fast',
+        default=False,
+        action='store_true',
+        help='Stop execution on other branches if a failing node is detected.',
+    )
 
     show_args = command_parser.add_parser(
         'show',

src/kontrol/options.py

@@ -0,0 +1,77 @@
+from __future__ import annotations
+
+from dataclasses import dataclass
+from typing import TYPE_CHECKING
+
+if TYPE_CHECKING:
+    from collections.abc import Iterable
+
+    from pyk.utils import BugReport
+
+
+@dataclass(frozen=True)
+class ProveOptions:
+    auto_abstract_gas: bool
+    bug_report: BugReport | None
+    use_booster: bool
+    kore_rpc_command: str | Iterable[str] | None
+    smt_timeout: int | None
+    smt_retry_limit: int | None
+    trace_rewrites: bool
+    simplify_init: bool
+    bmc_depth: int | None
+    max_depth: int
+    break_every_step: bool
+    break_on_jumpi: bool
+    break_on_calls: bool
+    workers: int
+    counterexample_info: bool
+    max_iterations: int | None
+    run_constructor: bool
+    fail_fast: bool
+    reinit: bool
+    port: int | None
+
+    def __init__(
+        self,
+        auto_abstract_gas: bool = False,
+        bug_report: BugReport | None = None,
+        use_booster: bool = True,
+        kore_rpc_command: str | Iterable[str] | None = None,
+        smt_timeout: int | None = None,
+        smt_retry_limit: int | None = None,
+        trace_rewrites: bool = False,
+        bmc_depth: int | None = None,
+        max_depth: int = 1000,
+        break_every_step: bool = False,
+        break_on_jumpi: bool = False,
+        break_on_calls: bool = True,
+        workers: int = 1,
+        counterexample_info: bool = False,
+        max_iterations: int | None = None,
+        run_constructor: bool = False,
+        fail_fast: bool = True,
+        reinit: bool = False,
+        port: int | None = None,
+    ) -> None:
+        if kore_rpc_command is None:
+            kore_rpc_command = ('kore-rpc-booster',) if use_booster else ('kore-rpc',)
+        object.__setattr__(self, 'auto_abstract_gas', auto_abstract_gas)
+        object.__setattr__(self, 'bug_report', bug_report)
+        object.__setattr__(self, 'use_booster', use_booster)
+        object.__setattr__(self, 'kore_rpc_command', kore_rpc_command)
+        object.__setattr__(self, 'smt_timeout', smt_timeout)
+        object.__setattr__(self, 'smt_retry_limit', smt_retry_limit)
+        object.__setattr__(self, 'trace_rewrites', trace_rewrites)
+        object.__setattr__(self, 'bmc_depth', bmc_depth)
+        object.__setattr__(self, 'max_depth', max_depth)
+        object.__setattr__(self, 'break_every_step', break_every_step)
+        object.__setattr__(self, 'break_on_jumpi', break_on_jumpi)
+        object.__setattr__(self, 'break_on_calls', break_on_calls)
+        object.__setattr__(self, 'workers', workers)
+        object.__setattr__(self, 'counterexample_info', counterexample_info)
+        object.__setattr__(self, 'max_iterations', max_iterations)
+        object.__setattr__(self, 'run_constructor', run_constructor)
+        object.__setattr__(self, 'fail_fast', fail_fast)
+        object.__setattr__(self, 'reinit', reinit)
+        object.__setattr__(self, 'port', port)