From d8871962ec8ecf53550926a617b29ad78813c5da Mon Sep 17 00:00:00 2001 From: dkcumming Date: Wed, 30 Apr 2025 21:37:15 -0400 Subject: [PATCH 1/3] prove-rs now saves proofs and can resume them --- kmir/src/kmir/__main__.py | 6 ++++-- kmir/src/kmir/kmir.py | 17 ++++++++++++++--- kmir/src/kmir/options.py | 12 ++++++++++-- 3 files changed, 28 insertions(+), 7 deletions(-) diff --git a/kmir/src/kmir/__main__.py b/kmir/src/kmir/__main__.py index f87f5847d..0e7e56e90 100644 --- a/kmir/src/kmir/__main__.py +++ b/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() diff --git a/kmir/src/kmir/kmir.py b/kmir/src/kmir/kmir.py index 3b30bcbf7..a96c3ce50 100644 --- a/kmir/src/kmir/kmir.py +++ b/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) diff --git a/kmir/src/kmir/options.py b/kmir/src/kmir/options.py index 548f1c879..3570ba98d 100644 --- a/kmir/src/kmir/options.py +++ b/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, From f518d3ed160682508223c10a6e73f75a05d21c89 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 1 May 2025 01:44:19 +0000 Subject: [PATCH 2/3] Set Version: 0.3.135 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index 7de9bb80b..c6d79ec31 100644 --- a/kmir/pyproject.toml +++ b/kmir/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "hatchling.build" [project] name = "kmir" -version = "0.3.134" +version = "0.3.135" description = "" requires-python = "~=3.10" dependencies = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 217b0a44a..06c348435 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.134' +VERSION: Final = '0.3.135' diff --git a/kmir/uv.lock b/kmir/uv.lock index 9d71d30aa..ef0258283 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.134" +version = "0.3.135" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index d6f2cdd3f..4212f2702 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.134 +0.3.135 From c7fe2183c961894232bdca7b7a955308998d6767 Mon Sep 17 00:00:00 2001 From: devops Date: Thu, 1 May 2025 02:10:38 +0000 Subject: [PATCH 3/3] Set Version: 0.3.136 --- kmir/pyproject.toml | 2 +- kmir/src/kmir/__init__.py | 2 +- kmir/uv.lock | 2 +- package/version | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/kmir/pyproject.toml b/kmir/pyproject.toml index c6d79ec31..6105584fd 100644 --- a/kmir/pyproject.toml +++ b/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 = [ diff --git a/kmir/src/kmir/__init__.py b/kmir/src/kmir/__init__.py index 06c348435..a6a487a64 100644 --- a/kmir/src/kmir/__init__.py +++ b/kmir/src/kmir/__init__.py @@ -1,3 +1,3 @@ from typing import Final -VERSION: Final = '0.3.135' +VERSION: Final = '0.3.136' diff --git a/kmir/uv.lock b/kmir/uv.lock index ef0258283..30c3dd27a 100644 --- a/kmir/uv.lock +++ b/kmir/uv.lock @@ -488,7 +488,7 @@ wheels = [ [[package]] name = "kmir" -version = "0.3.135" +version = "0.3.136" source = { editable = "." } dependencies = [ { name = "kframework" }, diff --git a/package/version b/package/version index 4212f2702..2c0588971 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.3.135 +0.3.136