Add parameter to advance_proof to split into subproofs after enough branches have been created

package/version

@@ -1 +1 @@
-0.1.448
+0.1.449

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. <[email protected]>",

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)
 

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 {