Add feature: prove a single claim in kmir prove (#325)

* add command option `--claim` for `kmir prove` * Set Version: 0.2.26 * fix claim not found issue * add `--claim-list` option * Set Version: 0.2.27 * Set Version: 0.2.27 * Set Version: 0.2.28 --------- Co-authored-by: yanliu18 <[email protected]> Co-authored-by: devops <[email protected]>
runtimeverification · Feb 26, 2024 · d0092c0 · d0092c0
1 parent 7598a55
commit d0092c0
Show file tree

Hide file tree

Showing 7 changed files with 57 additions and 15 deletions.
diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "kmir"
-version = "0.2.27"
+version = "0.2.28"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py
@@ -5,4 +5,4 @@
 from .prove import prove, show_proof, view_proof
 from .run import run
 
-VERSION: Final = '0.2.27'
+VERSION: Final = '0.2.28'
diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py
@@ -11,7 +11,7 @@
 from .cli import create_argument_parser
 from .kmir import KMIR
 from .parse import parse
-from .prove import prove, show_proof, view_proof
+from .prove import get_claim_labels, prove, show_proof, view_proof
 from .run import run
 from .utils import NodeIdLike
 
@@ -91,6 +91,8 @@ def exec_prove(
     spec_file: Path,
     smt_timeout: int,
     smt_retry_limit: int,
+    claim_list: bool = False,
+    claim: Optional[str] = None,
     definition_dir: Optional[Path] = None,
     haskell_dir: Optional[Path] = None,
     use_booster: bool = True,
@@ -129,9 +131,15 @@ def exec_prove(
     # We provide configuration of which backend to use in a KMIR object.
     # `use_booster` is by default True, where Booster Backend is always used unless turned off
 
+    if claim_list:
+        claim_labels = get_claim_labels(kmir, spec_file)
+        print(*claim_labels, sep='\n')
+        sys.exit(0)
+
     (passed, failed) = prove(
         kmir,
         spec_file,
+        claim_label=claim,
         save_directory=save_directory,
         reinit=reinit,
         depth=depth,

diff --git a/kmir/src/kmir/cli.py b/kmir/src/kmir/cli.py
@@ -83,7 +83,9 @@ def create_argument_parser() -> ArgumentParser:
 
     # Prove
     prove_subparser = command_parser.add_parser(
-        'prove', parents=[logging_args], help='Prove a MIR specification WARN: EXPERIMENTAL AND WORK IN PROGRESS'
+        'prove',
+        parents=[logging_args],
+        help='Prove a MIR specification, by default, it proves all the claims. Use `--claim` option to prove a selected claim.',
     )
     prove_subparser.add_argument(
         'spec_file',
@@ -102,6 +104,18 @@ def create_argument_parser() -> ArgumentParser:
         type=dir_path,
         help='Path to Haskell definition to use.',
     )
+    prove_subparser.add_argument(
+        '--claim-list',
+        default=False,
+        action='store_true',
+        help='Print a list of claims in the specificatoin file',
+    )
+    prove_subparser.add_argument(
+        '--claim',
+        default=None,
+        type=str,
+        help='Provide the claim label for proving a single claim',
+    )
     prove_subparser.add_argument(
         '--bug-report',
         action='store_true',

diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py
@@ -110,8 +110,13 @@ def rpc_session(self, server: KoreServer, claim_id: str, trace_rewrites: bool =
                 )
 
     # A wrapper on KProve's get_claims
-    def get_all_claims(self, spec_file: Path) -> list[KClaim]:
-        return self.mir_prove.get_claims(spec_file)
+    def get_all_claims(self, spec_file: Path, claim_label: Optional[str]) -> list[KClaim]:
+        if claim_label:
+            claim_list = []
+            claim_list.append(claim_label)
+            return self.mir_prove.get_claims(spec_file, claim_labels=claim_list)
+        else:
+            return self.mir_prove.get_claims(spec_file)
 
     def initialise_a_proof(
         self,

diff --git a/kmir/src/kmir/prove.py b/kmir/src/kmir/prove.py
@@ -1,8 +1,8 @@
 import logging
 from pathlib import Path
-from typing import Any, Final, Iterable
+from typing import Any, Final, Iterable, Optional
 
-from pyk.proof import APRProof  # , EqualityProof, APRBMCProof
+from pyk.proof import APRProof
 from pyk.proof.proof import Proof
 from pyk.proof.reachability import APRFailureInfo
 from pyk.proof.show import APRProofShow
@@ -15,17 +15,32 @@
 _LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
 
 
+def get_claim_labels(kmir: KMIR, spec_file: Path) -> list[str]:
+    _LOGGER.info(f'Extracting claim labels from spec file {spec_file}')
+
+    if kmir.prover:
+        kmir_prover = kmir.prover
+    else:
+        raise ValueError('The prover object in kmir is not initialised.')
+
+    flat_module_list = kmir_prover.mir_prove.get_claim_modules(spec_file=spec_file)
+
+    all_claims = {c.label: c for m in flat_module_list.modules for c in m.claims}
+
+    return list(all_claims.keys())
+
+
 def prove(
     kmir: KMIR,
     spec_file: Path,
     *,
-    save_directory: Path | None = None,
+    claim_label: Optional[str] = None,
+    save_directory: Optional[Path] = None,
     reinit: bool = False,
-    depth: int | None = None,
-    smt_timeout: int | None = None,
-    smt_retry_limit: int | None = None,
+    depth: Optional[int] = None,
+    smt_timeout: Optional[int] = None,
+    smt_retry_limit: Optional[int] = None,
     trace_rewrites: bool = False,
-    # kore_rpc_command: str | Iterable[str] | None = None,
 ) -> tuple[list[Proof], list[Proof]]:
     _LOGGER.info('Extracting claims from file')
 
@@ -34,7 +49,7 @@ def prove(
     else:
         raise ValueError('The prover object in kmir is not initialised.')
 
-    claims = kmir_prover.get_all_claims(spec_file)
+    claims = kmir_prover.get_all_claims(spec_file, claim_label)
     assert claims, ValueError(f'No claims found in file {spec_file}')
 
     passing: list[Proof] = []

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.2.27
+0.2.28