diff --git a/package/version b/package/version index 44516207b..868227d78 100644 --- a/package/version +++ b/package/version @@ -1 +1 @@ -0.1.448 +0.1.449 diff --git a/pyproject.toml b/pyproject.toml index 412c91ea1..a9928acb2 100644 --- a/pyproject.toml +++ b/pyproject.toml @@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api" [tool.poetry] name = "pyk" -version = "0.1.448" +version = "0.1.449" description = "" authors = [ "Runtime Verification, Inc. ", diff --git a/src/pyk/kcfg/kcfg.py b/src/pyk/kcfg/kcfg.py index a6b4bae32..aa5426656 100644 --- a/src/pyk/kcfg/kcfg.py +++ b/src/pyk/kcfg/kcfg.py @@ -351,7 +351,7 @@ def from_dict(dct: Mapping[str, Any]) -> KCFG: max_id = max(max_id, node_id) cterm = CTerm.from_dict(node_dict['cterm']) node = KCFG.Node(node_id, cterm) - cfg.add_node(node) + cfg._add_node(node) cfg._node_id = dct.get('next', max_id + 1) @@ -449,7 +449,7 @@ def get_node(self, node_id: NodeIdLike) -> Node | None: def contains_node(self, node: Node) -> bool: return bool(self.get_node(node.id)) - def add_node(self, node: Node) -> None: + def _add_node(self, node: Node) -> None: if node.id in self._nodes: raise ValueError(f'Node with id already exists: {node.id}') self._nodes[node.id] = node @@ -982,7 +982,7 @@ def read_cfg_data(cfg_dir: Path, id: str) -> KCFG: node_dict = json.loads(node_json.read_text()) cterm = CTerm.from_dict(node_dict['cterm']) node = KCFG.Node(node_id, cterm) - cfg.add_node(node) + cfg._add_node(node) cfg._node_id = dct.get('next', max_id + 1) diff --git a/src/pyk/proof/proof.py b/src/pyk/proof/proof.py index f4d0558c5..0aa3fbde4 100644 --- a/src/pyk/proof/proof.py +++ b/src/pyk/proof/proof.py @@ -33,9 +33,19 @@ class Proof(ABC): id: str proof_dir: Path | None - _subproofs: dict[str, Proof] + _subproofs: dict[str, Proof | None] admitted: bool + def get_subproof(self, proof_id: str) -> Proof: + if proof_id not in self._subproofs: + raise ValueError(f'subproof: {proof_id} not found in subproofs of {self.id}') + proof = self._subproofs[proof_id] + if proof is None: + proof = self.fetch_subproof_data(proof_id) + + assert isinstance(proof, Proof) + return proof + @property def proof_subdir(self) -> Path | None: if self.proof_dir is None: @@ -57,7 +67,7 @@ def __init__( raise ValueError(f'Cannot read subproofs {subproof_ids} of proof {self.id} with no proof_dir') if len(list(subproof_ids)) > 0: for proof_id in subproof_ids: - self.fetch_subproof_data(proof_id, force_reread=True) + self._subproofs[proof_id] = None if proof_dir is not None: ensure_dir_path(proof_dir) if self.proof_dir is not None: @@ -68,7 +78,7 @@ def admit(self) -> None: @property def subproof_ids(self) -> list[str]: - return [sp.id for sp in self._subproofs.values()] + return list(self._subproofs.keys()) def write_proof(self, subproofs: bool = False) -> None: if not self.proof_dir: @@ -136,29 +146,43 @@ def fetch_subproof( ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self._subproofs[proof_id].up_to_date): + assert self.proof_dir is not None + + subproof = self._subproofs[proof_id] + + if force_reread or subproof is None or subproof.up_to_date: updated_subproof = Proof.read_proof(proof_id, self.proof_dir) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self._subproofs[proof_id] + return subproof def fetch_subproof_data( self, proof_id: str, force_reread: bool = False, uptodate_check_method: str = 'timestamp' ) -> Proof: """Get a subproof, re-reading from disk if it's not up-to-date""" - if self.proof_dir is not None and (force_reread or not self._subproofs[proof_id].up_to_date): + assert self.proof_dir is not None + + subproof = self._subproofs[proof_id] if proof_id in self._subproofs else None + + if force_reread or subproof is None or subproof.up_to_date: updated_subproof = Proof.read_proof_data(self.proof_dir, proof_id) self._subproofs[proof_id] = updated_subproof return updated_subproof else: - return self._subproofs[proof_id] + return subproof @property def subproofs(self) -> Iterable[Proof]: """Return the subproofs, re-reading from disk the ones that changed""" - return self._subproofs.values() + for subproof_id in self._subproofs.keys(): + self.fetch_subproof_data(subproof_id) + subproofs_all_loaded: list[Proof] = [] + for subproof in self._subproofs.values(): + assert subproof is not None + subproofs_all_loaded.append(subproof) + return subproofs_all_loaded @property def subproofs_status(self) -> ProofStatus: @@ -182,6 +206,10 @@ def failed(self) -> bool: def passed(self) -> bool: return self.status == ProofStatus.PASSED + @property + def is_proof_pending(self) -> bool: + return self.status == ProofStatus.PENDING + @property def dict(self) -> dict[str, Any]: return { diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py index d3542944f..652de52a0 100644 --- a/src/pyk/proof/reachability.py +++ b/src/pyk/proof/reachability.py @@ -19,7 +19,7 @@ from .proof import CompositeSummary, Proof, ProofStatus if TYPE_CHECKING: - from collections.abc import Iterable, Mapping + from collections.abc import Callable, Iterable, Mapping from pathlib import Path from typing import Any, Final, TypeVar @@ -43,10 +43,12 @@ class APRProof(Proof, KCFGExploration): """ node_refutations: dict[int, RefutationProof] # TODO _node_refutatations + subproof_nodes: set[int] init: int target: int logs: dict[int, tuple[LogEntry, ...]] circularity: bool + generate_subproof_name: Callable[[APRProof, int], str] | None failure_info: APRFailureInfo | None def __init__( @@ -58,10 +60,12 @@ def __init__( target: NodeIdLike, logs: dict[int, tuple[LogEntry, ...]], proof_dir: Path | None = None, + subproof_nodes: Iterable[int] | None = None, node_refutations: dict[int, str] | None = None, subproof_ids: Iterable[str] = (), circularity: bool = False, admitted: bool = False, + generate_subproof_name: Callable[[APRProof, int], str] | None = None, ): Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted) KCFGExploration.__init__(self, kcfg, terminal) @@ -73,11 +77,14 @@ def __init__( self.circularity = circularity self.node_refutations = {} self.kcfg.cfg_dir = self.proof_subdir / 'kcfg' if self.proof_subdir else None + self.generate_subproof_name = generate_subproof_name if self.proof_dir is not None and self.proof_subdir is not None: ensure_dir_path(self.proof_dir) ensure_dir_path(self.proof_subdir) + self.subproof_nodes = set(subproof_nodes) if subproof_nodes is not None else set() + if node_refutations is not None: refutations_not_in_subprroofs = set(node_refutations.values()).difference( set(subproof_ids if subproof_ids else []) @@ -103,11 +110,19 @@ def is_refuted(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) in self.node_refutations.keys() def is_pending(self, node_id: NodeIdLike) -> bool: - return self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id) + return ( + self.is_explorable(node_id) + and not self.is_target(node_id) + and not self.is_refuted(node_id) + and not self.is_subproof_node(node_id) + ) def is_init(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.init) + def is_subproof_node(self, node_id: NodeIdLike) -> bool: + return self.kcfg._resolve(node_id) in self.subproof_nodes + def is_target(self, node_id: NodeIdLike) -> bool: return self.kcfg._resolve(node_id) == self.kcfg._resolve(self.target) @@ -117,9 +132,13 @@ def is_failing(self, node_id: NodeIdLike) -> bool: and not self.is_explorable(node_id) and not self.is_target(node_id) and not self.is_refuted(node_id) + and not self.is_subproof_node(node_id) and not self.kcfg.is_vacuous(node_id) ) + def add_subproof_node(self, node_id: int) -> None: + self.subproof_nodes.add(node_id) + def shortest_path_to(self, node_id: NodeIdLike) -> tuple[KCFG.Successor, ...]: spb = self.kcfg.shortest_path_between(self.init, node_id) assert spb is not None @@ -158,6 +177,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non id = dct['id'] circularity = dct.get('circularity', False) admitted = dct.get('admitted', False) + subproof_nodes = dct['subproof_nodes'] if 'subproof_nodes' in dct else [] subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else [] node_refutations: dict[int, str] = {} if 'node_refutation' in dct: @@ -177,6 +197,7 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non circularity=circularity, admitted=admitted, proof_dir=proof_dir, + subproof_nodes=subproof_nodes, subproof_ids=subproof_ids, node_refutations=node_refutations, ) @@ -231,6 +252,7 @@ def dict(self) -> dict[str, Any]: dct['terminal'] = sorted(self._terminal) dct['init'] = self.init dct['target'] = self.target + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['node_refutations'] = {node_id: proof.id for (node_id, proof) in self.node_refutations.items()} dct['circularity'] = self.circularity logs = {int(k): [l.to_dict() for l in ls] for k, ls in self.logs.items()} @@ -253,6 +275,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.stuck), len(self._terminal), len(self.node_refutations), + len(self.subproof_nodes), len(self.subproof_ids), ), *subproofs_summaries, @@ -271,6 +294,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof: kcfg = KCFG.read_cfg_data(cfg_dir, id) init = int(proof_dict['init']) target = int(proof_dict['target']) + subproof_nodes = proof_dict['subproof_nodes'] circularity = bool(proof_dict['circularity']) admitted = bool(proof_dict['admitted']) terminal = proof_dict['terminal'] @@ -284,6 +308,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof: terminal=terminal, init=init, target=target, + subproof_nodes=subproof_nodes, logs=logs, circularity=circularity, admitted=admitted, @@ -307,6 +332,7 @@ def write_proof_data(self) -> None: dct['type'] = 'APRProof' dct['init'] = self.kcfg._resolve(self.init) dct['target'] = self.kcfg._resolve(self.target) + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['terminal'] = sorted(self._terminal) dct['node_refutations'] = { self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items() @@ -337,10 +363,12 @@ def __init__( bmc_depth: int, bounded: Iterable[int] | None = None, proof_dir: Path | None = None, + subproof_nodes: Iterable[int] | None = None, subproof_ids: Iterable[str] = (), node_refutations: dict[int, str] | None = None, circularity: bool = False, admitted: bool = False, + generate_subproof_name: Callable[[APRProof, int], str] | None = None, ): super().__init__( id, @@ -350,10 +378,12 @@ def __init__( target, logs, proof_dir=proof_dir, + subproof_nodes=subproof_nodes, subproof_ids=subproof_ids, node_refutations=node_refutations, circularity=circularity, admitted=admitted, + generate_subproof_name=generate_subproof_name, ) self.bmc_depth = bmc_depth self._bounded = set(bounded) if bounded is not None else set() @@ -367,6 +397,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof: kcfg = KCFG.read_cfg_data(cfg_dir, id) init = int(proof_dict['init']) target = int(proof_dict['target']) + subproof_nodes = proof_dict['subproof_nodes'] circularity = bool(proof_dict['circularity']) terminal = proof_dict['terminal'] admitted = bool(proof_dict['admitted']) @@ -382,6 +413,7 @@ def read_proof_data(proof_dir: Path, id: str) -> APRBMCProof: terminal=terminal, init=init, target=target, + subproof_nodes=subproof_nodes, logs=logs, circularity=circularity, admitted=admitted, @@ -407,6 +439,7 @@ def write_proof_data(self) -> None: dct['type'] = 'APRBMCProof' dct['init'] = self.kcfg._resolve(self.init) dct['target'] = self.kcfg._resolve(self.target) + dct['subproof_nodes'] = sorted(self.subproof_nodes) dct['node_refutations'] = { self.kcfg._resolve(node_id): proof.id for (node_id, proof) in self.node_refutations.items() } @@ -522,6 +555,7 @@ def summary(self) -> CompositeSummary: len(self.kcfg.stuck), len(self._terminal), len(self.node_refutations), + len(self.subproof_nodes), len(self._bounded), len(self.subproof_ids), ), @@ -635,6 +669,7 @@ def advance_proof( cut_point_rules: Iterable[str] = (), terminal_rules: Iterable[str] = (), fail_fast: bool = False, + max_branches: int | None = None, ) -> None: iterations = 0 @@ -642,6 +677,15 @@ def advance_proof( while self.proof.pending: self.proof.write_proof_data() + + if max_branches is not None and len(self.proof.pending) > max_branches: + _LOGGER.info( + f'Reached max_branches={max_branches} bound on number of pending nodes. Nodes {self.proof.pending} will be turned into subproofs.' + ) + for pending_node in self.proof.pending: + self.delegate_to_subproof(pending_node) + break + if fail_fast and self.proof.failed: _LOGGER.warning( f'Terminating proof early because fail_fast is set {self.proof.id}, failing nodes: {[nd.id for nd in self.proof.failing]}' @@ -672,6 +716,38 @@ def advance_proof( self.proof.write_proof_data() + def delegate_to_subproof(self, node: KCFG.Node) -> None: + _LOGGER.info(f'Delegating node {node.id} to a new proof.') + subproof = self.construct_node_subproof(node) + self.proof.add_subproof(subproof) + self.proof.add_subproof_node(node.id) + + def construct_node_subproof(self, node: KCFG.Node) -> APRProof: + kcfg = KCFG(self.proof.proof_dir) + target_node = self.proof.kcfg.node(self.proof.target) + + node_cterm, _ = self.kcfg_explore.cterm_simplify(node.cterm) + ( + target_node_cterm, + _, + ) = self.kcfg_explore.cterm_simplify(target_node.cterm) + + new_init = kcfg.create_node(node_cterm) + new_target = kcfg.create_node(target_node_cterm) + + assert self.proof.generate_subproof_name is not None + + return APRProof( + id=self.proof.generate_subproof_name(self.proof, node.id), + kcfg=kcfg, + terminal=[], + init=new_init.id, + target=new_target.id, + logs={}, + proof_dir=self.proof.proof_dir, + generate_subproof_name=self.proof.generate_subproof_name, + ) + def refute_node(self, node: KCFG.Node) -> RefutationProof | None: _LOGGER.info(f'Attempting to refute node {node.id}') refutation = self.construct_node_refutation(node) @@ -757,6 +833,7 @@ class APRSummary(ProofSummary): stuck: int terminal: int refuted: int + subproof_nodes: int subproofs: int @property @@ -772,6 +849,7 @@ def lines(self) -> list[str]: f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', + f' subproof_nodes: {self.subproof_nodes}', f'Subproofs: {self.subproofs}', ] @@ -935,6 +1013,7 @@ class APRBMCSummary(ProofSummary): stuck: int terminal: int refuted: int + subproof_nodes: int bounded: int subproofs: int @@ -950,6 +1029,7 @@ def lines(self) -> list[str]: f' stuck: {self.stuck}', f' terminal: {self.terminal}', f' refuted: {self.refuted}', + f' subproof_nodes: {self.subproof_nodes}', f' bounded: {self.bounded}', f'Subproofs: {self.subproofs}', ] diff --git a/src/pyk/proof/show.py b/src/pyk/proof/show.py index 20747610e..55ac591db 100644 --- a/src/pyk/proof/show.py +++ b/src/pyk/proof/show.py @@ -36,6 +36,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]: attrs.append('target') if self.proof.is_pending(node.id): attrs.append('pending') + if self.proof.is_subproof_node(node.id): + attrs.append('subproof') if self.proof.is_terminal(node.id): attrs.append('terminal') if 'stuck' in attrs: diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py index dc3940cac..27c10df98 100644 --- a/src/tests/integration/kcfg/test_imp.py +++ b/src/tests/integration/kcfg/test_imp.py @@ -1242,6 +1242,41 @@ def test_anti_unify_forget_values( assert anti_unifier.kast == expected_anti_unifier.kast + def test_delegate_to_subproof( + self, + kcfg_explore: KCFGExplore, + proof_dir: Path, + kprove: KProve, + ) -> None: + claim = single( + kprove.get_claims( + K_FILES / 'imp-simple-spec.k', + spec_module_name='IMP-SIMPLE-SPEC', + claim_labels=['IMP-SIMPLE-SPEC.failing-if'], + ) + ) + + proof = APRProof.from_claim( + kprove.definition, + claim, + logs={}, + proof_dir=proof_dir, + generate_subproof_name=(lambda proof, node_id: str(node_id)), + ) + + prover = APRProver( + proof, + kcfg_explore=kcfg_explore, + ) + + assert len(list(proof.subproofs)) == 0 + assert len(proof.pending) == 1 + + prover.advance_proof(max_branches=1) + + assert len(list(proof.subproofs)) == 2 + assert len(proof.pending) == 0 + def test_anti_unify_keep_values( self, kcfg_explore: KCFGExplore, diff --git a/src/tests/unit/test_kcfg.py b/src/tests/unit/test_kcfg.py index 7e4c10f6e..b5703c8f9 100644 --- a/src/tests/unit/test_kcfg.py +++ b/src/tests/unit/test_kcfg.py @@ -435,9 +435,9 @@ def delete_node_data(node_id: int) -> None: monkeypatch.setattr(kcfg, '_write_node_data', write_node_data) monkeypatch.setattr(kcfg, '_delete_node_data', delete_node_data) - kcfg.add_node(node(1)) - kcfg.add_node(node(2)) - kcfg.add_node(node(3)) + kcfg._add_node(node(1)) + kcfg._add_node(node(2)) + kcfg._add_node(node(3)) assert written_nodes == set() assert deleted_nodes == set() @@ -449,11 +449,11 @@ def delete_node_data(node_id: int) -> None: written_nodes.clear() - kcfg.add_node(node(4)) + kcfg._add_node(node(4)) kcfg.remove_node(1) kcfg.remove_node(2) kcfg.replace_node(3, node(3).cterm) - kcfg.add_node(node(2)) + kcfg._add_node(node(2)) assert written_nodes == set() assert deleted_nodes == set() diff --git a/src/tests/unit/test_proof.py b/src/tests/unit/test_proof.py index c604ebf24..0a919f8d1 100644 --- a/src/tests/unit/test_proof.py +++ b/src/tests/unit/test_proof.py @@ -342,6 +342,7 @@ def test_apr_proof_summary(proof_dir: Path) -> None: vacuous=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=0, ) @@ -365,6 +366,7 @@ def test_aprbmc_proof_summary(proof_dir: Path) -> None: vacuous=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=0, bounded=0, @@ -402,6 +404,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: vacuous=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=1, ) @@ -418,6 +421,7 @@ def test_apr_proof_summary_subproofs(proof_dir: Path) -> None: vacuous=0, stuck=0, terminal=0, + subproof_nodes=0, refuted=0, subproofs=1, ),