From 3884714651448e76e0e9c9fd6d2efad8f8f01d90 Mon Sep 17 00:00:00 2001
From: dkcumming <daniel.cumming@runtimeverification.com>
Date: Wed, 17 Dec 2025 20:44:05 +1000
Subject: [PATCH] Added `--fail-fast` and `--maintainence-rate` pyk flags to
 `kmir prove`

---
 kmir/src/kmir/__main__.py | 16 ++++++++++++++++
 kmir/src/kmir/kmir.py     |  7 ++++++-
 kmir/src/kmir/options.py  | 10 ++++++++++
 3 files changed, 32 insertions(+), 1 deletion(-)

diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
index 846cf91ef..8de67ff4f 100644
--- a/kmir/src/kmir/__main__.py
+++ b/kmir/src/kmir/__main__.py
@@ -245,6 +245,20 @@ def _arg_parser() -> ArgumentParser:
         '--max-iterations', metavar='ITERATIONS', type=int, help='max number of proof iterations to take'
     )
     prove_args.add_argument('--reload', action='store_true', help='Force restarting proof')
+    prove_args.add_argument(
+        '--fail-fast',
+        dest='fail_fast',
+        action='store_true',
+        help='Halt execution early if the proof is failing',
+    )
+    prove_args.add_argument(
+        '--maintenance-rate',
+        dest='maintenance_rate',
+        type=int,
+        default=1,
+        metavar='RATE',
+        help='Number of iterations between proof maintenance (writing to disk). Default: 1',
+    )
     prove_args.add_argument(
         '--break-on-calls', dest='break_on_calls', action='store_true', help='Break on all function and intrinsic calls'
     )
@@ -496,6 +510,8 @@ def _parse_args(ns: Namespace) -> KMirOpts:
                 max_depth=ns.max_depth,
                 max_iterations=ns.max_iterations,
                 reload=ns.reload,
+                fail_fast=ns.fail_fast,
+                maintenance_rate=ns.maintenance_rate,
                 save_smir=ns.save_smir,
                 smir=ns.smir,
                 start_symbol=ns.start_symbol,
diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
index 4c63c93bd..7453c1325 100644
--- a/kmir/src/kmir/kmir.py
+++ b/kmir/src/kmir/kmir.py
@@ -268,7 +268,12 @@ def prove_rs(opts: ProveRSOpts) -> APRProof:
 
             with kmir.kcfg_explore(label, terminate_on_thunk=opts.terminate_on_thunk) as kcfg_explore:
                 prover = APRProver(kcfg_explore, execute_depth=opts.max_depth, cut_point_rules=cut_point_rules)
-                prover.advance_proof(apr_proof, max_iterations=opts.max_iterations)
+                prover.advance_proof(
+                    apr_proof,
+                    max_iterations=opts.max_iterations,
+                    fail_fast=opts.fail_fast,
+                    maintenance_rate=opts.maintenance_rate,
+                )
                 return apr_proof
 
 
diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py
index ff6371fdd..b50af33e5 100644
--- a/kmir/src/kmir/options.py
+++ b/kmir/src/kmir/options.py
@@ -41,6 +41,8 @@ class ProveOpts(KMirOpts):
     max_depth: int | None
     max_iterations: int | None
     reload: bool
+    fail_fast: bool
+    maintenance_rate: int
     break_on_calls: bool
     break_on_function_calls: bool
     break_on_intrinsic_calls: bool
@@ -64,6 +66,8 @@ def __init__(
         max_depth: int | None = None,
         max_iterations: int | None = None,
         reload: bool = False,
+        fail_fast: bool = False,
+        maintenance_rate: int = 1,
         break_on_calls: bool = False,
         break_on_function_calls: bool = False,
         break_on_intrinsic_calls: bool = False,
@@ -85,6 +89,8 @@ def __init__(
         self.max_depth = max_depth
         self.max_iterations = max_iterations
         self.reload = reload
+        self.fail_fast = fail_fast
+        self.maintenance_rate = maintenance_rate
         self.break_on_calls = break_on_calls
         self.break_on_function_calls = break_on_function_calls
         self.break_on_intrinsic_calls = break_on_intrinsic_calls
@@ -117,6 +123,8 @@ def __init__(
         max_depth: int | None = None,
         max_iterations: int | None = None,
         reload: bool = False,
+        fail_fast: bool = False,
+        maintenance_rate: int = 1,
         save_smir: bool = False,
         smir: bool = False,
         start_symbol: str = 'main',
@@ -142,6 +150,8 @@ def __init__(
         self.max_depth = max_depth
         self.max_iterations = max_iterations
         self.reload = reload
+        self.fail_fast = fail_fast
+        self.maintenance_rate = maintenance_rate
         self.save_smir = save_smir
         self.smir = smir
         self.start_symbol = start_symbol