diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 0644d09a9..32ce98757 100644 --- 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. ", diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index e1faa70ff..9aab1d164 100644 --- 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 index 921d0c26b..84e00193a 100644 --- 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 index 56e5fba12..bbc54cc34 100644 --- 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 index 7fb9523d8..8ac9a4d87 100644 --- 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 index 4a4c8f711..475aa80d1 100644 --- 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 index b32698427..8bc53d520 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.2.27 +0.2.28