Implementing saving and resuming proofs with prove-rs command (#551)

This PR updates the `prove-rs` command. In particular:
- `prove-rs` takes optional arg `--proof-dir <DIR>` that it will save
proof objects in to disc
- `prove-rs` will resume a proof from disc if it exists, unless optional
arg `--reload` is added

Now it is possible to use `prove view` and `prove prune` after using
`prove-rs`.

Since `ProveRunOpts` and `ProveRSOpts` now have `--proof-dir` and
`--reload` in common I refactored the logic into `ProveOpts`.

---------

Co-authored-by: devops <devops@runtimeverification.com>

Author: dkcumming

kmir/pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "hatchling.build"
 
 [project]
 name = "kmir"
-version = "0.3.135"
+version = "0.3.136"
 description = ""
 requires-python = "~=3.10"
 dependencies = [

kmir/src/kmir/__init__.py

@@ -1,3 +1,3 @@
 from typing import Final
 
-VERSION: Final = '0.3.135'
+VERSION: Final = '0.3.136'

kmir/src/kmir/__main__.py

@@ -172,11 +172,13 @@ def _arg_parser() -> ArgumentParser:
     )
 
     prove_args = ArgumentParser(add_help=False)
+    prove_args.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
     prove_args.add_argument('--bug-report', metavar='PATH', help='path to optional bug report')
     prove_args.add_argument('--max-depth', metavar='DEPTH', type=int, help='max steps to take between nodes in kcfg')
     prove_args.add_argument(
         '--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_parser = command_parser.add_parser(
         'prove', help='Utilities for working with proofs over SMIR', parents=[kcli_args.logging_args]
@@ -185,14 +187,12 @@ def _arg_parser() -> ArgumentParser:
 
     prove_run_parser = prove_command_parser.add_parser('run', help='Run the prover on a spec', parents=[prove_args])
     prove_run_parser.add_argument('input_file', metavar='FILE', help='K File with the spec module')
-    prove_run_parser.add_argument('--proof-dir', metavar='DIR', help='Proof directory')
     prove_run_parser.add_argument(
         '--include-labels', metavar='LABELS', help='Comma separated list of claim labels to include'
     )
     prove_run_parser.add_argument(
         '--exclude-labels', metavar='LABELS', help='Comma separated list of claim labels to exclude'
     )
-    prove_run_parser.add_argument('--reload', action='store_true', help='Force restarting proof')
 
     prove_view_parser = prove_command_parser.add_parser('view', help='View a saved proof')
     prove_view_parser.add_argument('id', metavar='PROOF_ID', help='The id of the proof to view')
@@ -253,9 +253,11 @@ def _parse_args(ns: Namespace) -> KMirOpts:
         case 'prove-rs':
             return ProveRSOpts(
                 rs_file=Path(ns.rs_file).resolve(),
+                proof_dir=ns.proof_dir,
                 bug_report=ns.bug_report,
                 max_depth=ns.max_depth,
                 max_iterations=ns.max_iterations,
+                reload=ns.reload,
             )
         case _:
             raise AssertionError()

kmir/src/kmir/kmir.py

@@ -1,5 +1,6 @@
 from __future__ import annotations
 
+import logging
 from contextlib import contextmanager
 from typing import TYPE_CHECKING
 
@@ -29,6 +30,8 @@
 
     from .options import ProveRSOpts
 
+_LOGGER: Final = logging.getLogger(__name__)
+
 
 class KMIR(KProve, KRun):
     llvm_library_dir: Path | None
@@ -56,7 +59,9 @@ def kcfg_explore(self, label: str | None = None) -> Iterator[KCFGExplore]:
         ) as cts:
             yield KCFGExplore(cts, kcfg_semantics=KMIRSemantics())
 
-    def apr_proof_from_kast(self, id: str, kmir_kast: KInner, sort: str = 'GeneratedTopCell') -> APRProof:
+    def apr_proof_from_kast(
+        self, id: str, kmir_kast: KInner, sort: str = 'GeneratedTopCell', proof_dir: Path | None = None
+    ) -> APRProof:
         tools = Tools(self.definition_dir)
         config = tools.make_init_config(kmir_kast, 'main', sort=sort)
         config_with_cell_vars, _ = split_config_from(config)
@@ -68,7 +73,7 @@ def apr_proof_from_kast(self, id: str, kmir_kast: KInner, sort: str = 'Generated
         kcfg = KCFG()
         init_node = kcfg.create_node(lhs)
         target_node = kcfg.create_node(rhs)
-        return APRProof(id, kcfg, [], init_node.id, target_node.id, {})
+        return APRProof(id, kcfg, [], init_node.id, target_node.id, {}, proof_dir=proof_dir)
 
     def prove_rs(self, opts: ProveRSOpts) -> APRProof:
         if not opts.rs_file.is_file():
@@ -81,7 +86,13 @@ def prove_rs(self, opts: ProveRSOpts) -> APRProof:
         kmir_kast, _ = parse_result
         assert isinstance(kmir_kast, KInner)
 
-        apr_proof = self.apr_proof_from_kast(str(opts.rs_file.stem), kmir_kast)
+        label = str(opts.rs_file.stem)
+        if not opts.reload and opts.proof_dir is not None and APRProof.proof_data_exists(label, opts.proof_dir):
+            _LOGGER.info(f'Reading proof from disc: {opts.proof_dir}, {label}')
+            apr_proof = APRProof.read_proof_data(opts.proof_dir, label)
+        else:
+            _LOGGER.info(f'Initialising proof: {label}')
+            apr_proof = self.apr_proof_from_kast(label, kmir_kast, proof_dir=opts.proof_dir)
         with self.kcfg_explore('PROOF-TEST') as kcfg_explore:
             prover = APRProver(kcfg_explore, execute_depth=opts.max_depth)
             prover.advance_proof(apr_proof, max_iterations=opts.max_iterations)

kmir/src/kmir/options.py

@@ -29,19 +29,25 @@ class RunOpts(KMirOpts):
 
 @dataclass
 class ProveOpts(KMirOpts):
+    proof_dir: Path | None
     bug_report: Path | None
     max_depth: int | None
     max_iterations: int | None
+    reload: bool
 
     def __init__(
         self,
+        proof_dir: Path | str | None,
         bug_report: Path | None = None,
         max_depth: int | None = None,
         max_iterations: int | None = None,
+        reload: bool = False,
     ) -> None:
+        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
         self.bug_report = bug_report
         self.max_depth = max_depth
         self.max_iterations = max_iterations
+        self.reload = reload
 
 
 @dataclass
@@ -66,23 +72,25 @@ class ProveRSOpts(ProveOpts):
     def __init__(
         self,
         rs_file: Path,
+        proof_dir: Path | str | None = None,
         bug_report: Path | None = None,
         max_depth: int | None = None,
         max_iterations: int | None = None,
+        reload: bool = False,
     ) -> None:
         self.rs_file = rs_file
+        self.proof_dir = Path(proof_dir).resolve() if proof_dir is not None else None
         self.bug_report = bug_report
         self.max_depth = max_depth
         self.max_iterations = max_iterations
+        self.reload = reload
 
 
 @dataclass
 class ProveRunOpts(ProveOpts):
     spec_file: Path
-    proof_dir: Path | None
     include_labels: tuple[str, ...] | None
     exclude_labels: tuple[str, ...] | None
-    reload: bool
 
     def __init__(
         self,

kmir/uv.lock

@@ -1 +1 @@
-0.3.135
+0.3.136