Add --fail-fast and --maintainence-rate pyk flags (#900)

- `--fail-fast` will terminate a proof if any branch fails (instead of
continuing on other branches);
- `--maintainence-rate <RATE>` where `RATE` is an integer and `1 <=
RATE` and `RATE` is how many steps between writing to proof state to
disc. Writing to disc is slow, so this increases performance at the cost
of an interrupted proof needing to redo work that was not written to
disc.

Author: dkcumming

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,

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
 
 

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