Add disk read/write test and fix

pyk/src/pyk/proof/proof.py

@@ -40,7 +40,7 @@ class Proof(Generic[PS, SR]):
     :param SR: Step result: data produced by executing a PS with `Prover.step_proof` used to update the `Proof`
     """
 
-    _PROOF_TYPES: Final = {'APRProof', 'EqualityProof', 'RefutationProof'}
+    _PROOF_TYPES: Final = {'APRProof', 'EqualityProof', 'RefutationProof', 'MultiProof'}
 
     id: str
     proof_dir: Path | None
@@ -247,6 +247,7 @@ def read_proof(cls: type[Proof], id: str, proof_dir: Path) -> Proof:
     def read_proof_data(proof_dir: Path, id: str) -> Proof:
         # these local imports allow us to call .to_dict() based on the proof type we read from JSON
         from .implies import EqualityProof, RefutationProof  # noqa
+        from .proof import MultiProof  # noqa
         from .reachability import APRProof  # noqa
 
         proof_path = proof_dir / id / 'proof.json'
@@ -303,12 +304,18 @@ def can_progress(self) -> bool:
     def commit(self, result: None) -> None: ...
 
     @classmethod
-    def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> Proof:
+    def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> MultiProof:
         _id = dct['id']
         _subproof_ids = dct['subproof_ids']
         _admitted = dct['admitted']
         return MultiProof(id=_id, subproof_ids=_subproof_ids, proof_dir=proof_dir, admitted=_admitted)
 
+    @property
+    def dict(self) -> dict[str, Any]:
+        dct = super().dict
+        dct['type'] = 'MultiProof'
+        return dct
+
     def get_steps(self) -> Iterable[None]:
         """Return all currently available steps associated with this Proof. Should not modify `self`."""
         return []
@@ -317,6 +324,15 @@ def get_steps(self) -> Iterable[None]:
     def own_status(self) -> ProofStatus:
         return ProofStatus.PASSED
 
+    @staticmethod
+    def read_proof_data(proof_dir: Path, id: str) -> MultiProof:
+        proof_path = proof_dir / id / 'proof.json'
+        if Proof.proof_data_exists(id, proof_dir):
+            proof_dict = json.loads(proof_path.read_text())
+            return MultiProof.from_dict(proof_dict, proof_dir)
+
+        raise ValueError(f'Could not load Proof from file {id}: {proof_path}')
+
     def write_proof_data(self) -> None:
         super().write_proof_data()
         if not self.proof_dir:

pyk/src/tests/integration/proof/test_multi_proof.py

@@ -48,7 +48,7 @@ def _update_symbol_table(symbol_table: SymbolTable) -> None:
         MULTIPROOF_TEST_DATA,
         ids=[test_id for test_id, *_ in MULTIPROOF_TEST_DATA],
     )
-    def test_multiproof_pass(
+    def test_multiproof_status(
         self,
         kprove: KProve,
         kcfg_explore: KCFGExplore,
@@ -58,7 +58,6 @@ def test_multiproof_pass(
         claim_id_2: str,
         proof_status: ProofStatus,
     ) -> None:
-
         spec_file = K_FILES / 'imp-simple-spec.k'
         spec_module = 'IMP-FUNCTIONAL-SPEC'
 
@@ -92,3 +91,41 @@ def test_multiproof_pass(
         equality_prover.advance_proof(equality_proof_2)
 
         assert mproof.status == proof_status
+
+    def test_multiproof_write(
+        self,
+        kprove: KProve,
+        kcfg_explore: KCFGExplore,
+        proof_dir: Path,
+    ) -> None:
+        spec_file = K_FILES / 'imp-simple-spec.k'
+        spec_module = 'IMP-FUNCTIONAL-SPEC'
+
+        claim_id_1 = 'concrete-addition'
+        claim_id_2 = 'concrete-identity'
+
+        claim_1 = single(
+            kprove.get_claims(
+                Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id_1}']
+            )
+        )
+        claim_2 = single(
+            kprove.get_claims(
+                Path(spec_file), spec_module_name=spec_module, claim_labels=[f'{spec_module}.{claim_id_2}']
+            )
+        )
+
+        equality_proof_1 = EqualityProof.from_claim(claim_1, kprove.definition, proof_dir=proof_dir)
+        equality_proof_2 = EqualityProof.from_claim(claim_2, kprove.definition, proof_dir=proof_dir)
+
+        equality_proof_1.write_proof_data()
+        equality_proof_2.write_proof_data()
+
+        mproof = MultiProof(
+            id='multiproof1', subproof_ids=[equality_proof_1.id, equality_proof_2.id], proof_dir=proof_dir
+        )
+
+        mproof.write_proof_data()
+
+        disk_mproof = MultiProof.read_proof_data(proof_dir=proof_dir, id='multiproof1')
+        assert disk_mproof.dict == mproof.dict