Merge branch 'master' into fix-deduplicate-productions

Author: virgil-serbanuta

src/pyk/proof/proof.py

@@ -4,6 +4,7 @@
 import logging
 from abc import ABC, abstractmethod
 from enum import Enum
+from itertools import chain
 from typing import TYPE_CHECKING
 
 from ..utils import hash_file, hash_str
@@ -29,20 +30,33 @@ class Proof(ABC):
 
     id: str
     proof_dir: Path | None
+    _subproofs: dict[str, Proof]
 
-    def __init__(self, id: str, proof_dir: Path | None = None) -> None:
+    def __init__(self, id: str, proof_dir: Path | None = None, subproof_ids: Iterable[str] = ()) -> None:
         self.id = id
         self.proof_dir = proof_dir
+        self._subproofs = {}
+        if self.proof_dir is None and len(list(subproof_ids)) > 0:
+            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(proof_id, force_reread=True)
 
-    def write_proof(self) -> None:
+    @property
+    def subproof_ids(self) -> list[str]:
+        return [sp.id for sp in self._subproofs.values()]
+
+    def write_proof(self, subproofs: bool = False) -> None:
         if not self.proof_dir:
             return
         proof_path = self.proof_dir / f'{hash_str(self.id)}.json'
-        if not self.up_to_date():
+        if not self.up_to_date:
             proof_json = json.dumps(self.dict)
             proof_path.write_text(proof_json)
-            self._last_modified = proof_path.stat().st_mtime_ns
             _LOGGER.info(f'Updated proof file {self.id}: {proof_path}')
+        if subproofs:
+            for sp in self.subproofs:
+                sp.write_proof(subproofs=subproofs)
 
     @staticmethod
     def proof_exists(id: str, proof_dir: Path) -> bool:
@@ -53,32 +67,69 @@ def proof_exists(id: str, proof_dir: Path) -> bool:
     def digest(self) -> str:
         return hash_str(json.dumps(self.dict))
 
-    def up_to_date(self, check_method: str = 'checksum') -> bool:
+    @property
+    def up_to_date(self) -> bool:
         """
         Check that the proof's representation on disk is up-to-date.
-        By default, compares the file timestamp to self._last_modified. Use check_method = 'checksum' to compare hashes instead.
         """
         if self.proof_dir is None:
             raise ValueError(f'Cannot check if proof {self.id} with no proof_dir is up-to-date')
         proof_path = self.proof_dir / f'{hash_str(id)}.json'
         if proof_path.exists() and proof_path.is_file():
-            match check_method:
-                case 'checksum':
-                    return self.digest == hash_file(proof_path)
-                case _:  # timestamp
-                    return self._last_modified == proof_path.stat().st_mtime_ns
+            return self.digest == hash_file(proof_path)
         else:
             return False
 
+    def add_subproof(self, proof_id: str) -> None:
+        if self.proof_dir is None:
+            raise ValueError(f'Cannot add subproof to the proof {self.id} with no proof_dir')
+        assert self.proof_dir
+        if not Proof.proof_exists(proof_id, self.proof_dir):
+            raise ValueError(f"Cannot find subproof {proof_id} in parent proof's {self.id} proof_dir {self.proof_dir}")
+        self._subproofs[proof_id] = self.fetch_subproof(proof_id, force_reread=True)
+
+    def remove_subproof(self, proof_id: str) -> None:
+        del self._subproofs[proof_id]
+
+    def fetch_subproof(
+        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):
+            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]
+
+    @property
+    def subproofs(self) -> Iterable[Proof]:
+        """Return the subproofs, re-reading from disk the ones that changed"""
+        return self._subproofs.values()
+
+    @property
+    def subproofs_status(self) -> ProofStatus:
+        any_subproof_failed = any([p.status == ProofStatus.FAILED for p in self.subproofs])
+        any_subproof_pending = any([p.status == ProofStatus.PENDING for p in self.subproofs])
+        if any_subproof_failed:
+            return ProofStatus.FAILED
+        elif any_subproof_pending:
+            return ProofStatus.PENDING
+        else:
+            return ProofStatus.PASSED
+
     @property
     @abstractmethod
     def status(self) -> ProofStatus:
         ...
 
     @property
-    @abstractmethod
     def dict(self) -> dict[str, Any]:
-        ...
+        return {
+            'id': self.id,
+            'subproof_ids': self.subproof_ids,
+        }
 
     @classmethod
     @abstractmethod
@@ -107,7 +158,5 @@ def json(self) -> str:
 
     @property
     def summary(self) -> Iterable[str]:
-        return [
-            f'Proof: {self.id}',
-            f'    status: {self.status}',
-        ]
+        subproofs_summaries = [subproof.summary for subproof in self.subproofs]
+        return chain([f'Proof: {self.id}', f'    status: {self.status}'], *subproofs_summaries)

src/pyk/proof/reachability.py

@@ -2,6 +2,7 @@
 
 import json
 import logging
+from itertools import chain
 from typing import TYPE_CHECKING
 
 from pyk.kore.rpc import LogEntry
@@ -51,8 +52,9 @@ def __init__(
         logs: dict[int, tuple[LogEntry, ...]],
         terminal_nodes: Iterable[NodeIdLike] | None = None,
         proof_dir: Path | None = None,
+        subproof_ids: Iterable[str] = (),
     ):
-        super().__init__(id, proof_dir=proof_dir)
+        super().__init__(id, proof_dir=proof_dir, subproof_ids=subproof_ids)
         self.kcfg = kcfg
         self.init = init
         self.target = target
@@ -90,24 +92,36 @@ def read_proof(id: str, proof_dir: Path) -> APRProof:
     def status(self) -> ProofStatus:
         if len(self.terminal) > 0:
             return ProofStatus.FAILED
-        elif len(self.pending) > 0:
+        elif len(self.pending) > 0 or self.subproofs_status == ProofStatus.PENDING:
             return ProofStatus.PENDING
         else:
-            return ProofStatus.PASSED
+            if self.subproofs_status == ProofStatus.PASSED:
+                return ProofStatus.PASSED
+            else:
+                return ProofStatus.FAILED
 
     @classmethod
     def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> APRProof:
         cfg = KCFG.from_dict(dct['cfg'])
-        terminal_nodes = dct['terminal_nodes']
         init_node = dct['init']
+        terminal_nodes = dct['terminal_nodes']
         target_node = dct['target']
         id = dct['id']
+        subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else []
         if 'logs' in dct:
             logs = {k: tuple(LogEntry.from_dict(l) for l in ls) for k, ls in dct['logs'].items()}
         else:
             logs = {}
-
-        return APRProof(id, cfg, init_node, target_node, logs, terminal_nodes=terminal_nodes, proof_dir=proof_dir)
+        return APRProof(
+            id,
+            cfg,
+            init_node,
+            target_node,
+            logs,
+            terminal_nodes=terminal_nodes,
+            proof_dir=proof_dir,
+            subproof_ids=subproof_ids,
+        )
 
     @staticmethod
     def from_claim(defn: KDefinition, claim: KClaim, *args: Any, **kwargs: Any) -> APRProof:
@@ -130,29 +144,34 @@ def path_constraints(self, final_node_id: NodeIdLike) -> KInner:
 
     @property
     def dict(self) -> dict[str, Any]:
+        dct = super().dict
+        dct['type'] = 'APRProof'
+        dct['cfg'] = self.kcfg.to_dict()
+        dct['init'] = self.init
+        dct['target'] = self.target
+        dct['terminal_nodes'] = self._terminal_nodes
         logs = {k: [l.to_dict() for l in ls] for k, ls in self.logs.items()}
-        return {
-            'type': 'APRProof',
-            'id': self.id,
-            'cfg': self.kcfg.to_dict(),
-            'init': self.init,
-            'target': self.target,
-            'terminal_nodes': self._terminal_nodes,
-            'logs': logs,
-        }
+        dct['logs'] = logs
+        return dct
 
     def add_terminal(self, nid: NodeIdLike) -> None:
         self._terminal_nodes.append(self.kcfg._resolve(nid))
 
     @property
     def summary(self) -> Iterable[str]:
-        return [
+        subproofs_summaries = chain(subproof.summary for subproof in self.subproofs)
+        yield from [
             f'APRProof: {self.id}',
             f'    status: {self.status}',
             f'    nodes: {len(self.kcfg.nodes)}',
+            f'    frontier: {len(self.kcfg.frontier)}',
+            f'    stuck: {len(self.kcfg.stuck)}',
+            'Subproofs:' if len(self.subproof_ids) else '',
             f'    pending: {len(self.pending)}',
             f'    terminal: {len(self.terminal)}',
         ]
+        for summary in subproofs_summaries:
+            yield from summary
 
 
 class APRBMCProof(APRProof):
@@ -171,8 +190,9 @@ def __init__(
         bmc_depth: int,
         bounded_nodes: Iterable[int] | None = None,
         proof_dir: Path | None = None,
+        subproof_ids: Iterable[str] = (),
     ):
-        super().__init__(id, kcfg, init, target, logs, proof_dir=proof_dir)
+        super().__init__(id, kcfg, init, target, logs, proof_dir=proof_dir, subproof_ids=subproof_ids)
         self.bmc_depth = bmc_depth
         self._bounded_nodes = list(bounded_nodes) if bounded_nodes is not None else []
 
@@ -202,26 +222,40 @@ def is_bounded(self, node_id: NodeIdLike) -> bool:
 
     @property
     def status(self) -> ProofStatus:
-        if len(self.terminal) > 0:
+        if (
+            any(nd.id not in self._bounded_nodes for nd in self.kcfg.stuck)
+            or self.subproofs_status == ProofStatus.FAILED
+        ):
             return ProofStatus.FAILED
-        elif len(self.pending) > 0:
+        elif len(self.pending) > 0 or self.subproofs_status == ProofStatus.PENDING:
             return ProofStatus.PENDING
         else:
             return ProofStatus.PASSED
 
     @classmethod
     def from_dict(cls: type[APRBMCProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> APRBMCProof:
         cfg = KCFG.from_dict(dct['cfg'])
-        id = dct['id']
         init = dct['init']
         target = dct['target']
         bounded_nodes = dct['bounded_nodes']
         bmc_depth = dct['bmc_depth']
+        id = dct['id']
+        subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else []
         if 'logs' in dct:
             logs = {k: tuple(LogEntry.from_dict(l) for l in ls) for k, ls in dct['logs'].items()}
         else:
             logs = {}
-        return APRBMCProof(id, cfg, init, target, logs, bmc_depth, bounded_nodes=bounded_nodes, proof_dir=proof_dir)
+        return APRBMCProof(
+            id,
+            cfg,
+            init,
+            target,
+            logs,
+            bmc_depth,
+            bounded_nodes=bounded_nodes,
+            proof_dir=proof_dir,
+            subproof_ids=subproof_ids,
+        )
 
     @staticmethod
     def from_claim_with_bmc_depth(defn: KDefinition, claim: KClaim, bmc_depth: int) -> APRBMCProof:
@@ -243,14 +277,21 @@ def add_bounded(self, nid: NodeIdLike) -> None:
 
     @property
     def summary(self) -> Iterable[str]:
-        return [
+        subproofs_summaries = chain(subproof.summary for subproof in self.subproofs)
+        yield from [
             f'APRBMCProof(depth={self.bmc_depth}): {self.id}',
             f'    status: {self.status}',
             f'    nodes: {len(self.kcfg.nodes)}',
+            f'    frontier: {len(self.kcfg.frontier)}',
+            f'    stuck: {len([nd for nd in self.kcfg.stuck if nd.id not in self._bounded_nodes])}',
+            f'    bmc-depth-bounded: {len(self._bounded_nodes)}',
+            'Subproofs' if len(self.subproof_ids) else '',
             f'    pending: {len(self.pending)}',
             f'    terminal: {len(self.terminal)}',
             f'    bounded: {len(self.bounded)}',
         ]
+        for summary in subproofs_summaries:
+            yield from summary
 
 
 class APRProver: