Proof container proof type

pyk/src/pyk/proof/implies.py

@@ -308,7 +308,7 @@ def __init__(
         subproof_ids: Iterable[str] = (),
         admitted: bool = False,
     ):
-        antecedent = mlAnd(mlEqualsTrue(c) for c in pre_constraints)
+        antecedent = mlAnd((c if is_top(c) else mlEqualsTrue(c)) for c in pre_constraints)
         consequent = mlEqualsFalse(last_constraint)
         super().__init__(
             id,

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
@@ -175,6 +175,8 @@ def fetch_subproof_data(
     @property
     def subproofs(self) -> Iterable[Proof]:
         """Return the subproofs, re-reading from disk the ones that changed"""
+        for subproof_id in self._subproofs.keys():
+            self.fetch_subproof_data(subproof_id)
         return self._subproofs.values()
 
     @property
@@ -245,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'
@@ -287,6 +290,62 @@ def get_steps(self) -> Iterable[PS]:
         ...
 
 
+class MultiProof(Proof[None, None]):
+    """Thin concrete Proof class that has no execution logic of its own, but holds subproofs. The intended use
+    case for this is when we run kontrol proofs with setUp functions, to separate the proof into several
+    subproof APRProofs: one for the setUp function and one for the test function for each final configuration
+    of the setUp function.
+    """
+
+    @property
+    def can_progress(self) -> bool:
+        return False
+
+    def commit(self, result: None) -> None: ...
+
+    @classmethod
+    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 []
+
+    @property
+    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:
+            return
+        ensure_dir_path(self.proof_dir)
+        ensure_dir_path(self.proof_dir / self.id)
+        proof_path = self.proof_dir / self.id / 'proof.json'
+        if not self.up_to_date:
+            proof_json = json.dumps(self.dict)
+            proof_path.write_text(proof_json)
+            _LOGGER.info(f'Updated proof file {self.id}: {proof_path}')
+
+
 class ProofSummary(ABC):
     id: str
     status: ProofStatus

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

@@ -0,0 +1,131 @@
+from __future__ import annotations
+
+import logging
+from pathlib import Path
+from typing import TYPE_CHECKING
+
+import pytest
+
+from pyk.proof import EqualityProof, ImpliesProver, ProofStatus
+from pyk.proof.proof import MultiProof
+from pyk.testing import KCFGExploreTest, KProveTest
+from pyk.utils import single
+
+from ..utils import K_FILES
+
+if TYPE_CHECKING:
+    from typing import Final
+
+    from pytest import TempPathFactory
+
+    from pyk.kcfg import KCFGExplore
+    from pyk.ktool.kprint import SymbolTable
+    from pyk.ktool.kprove import KProve
+
+
+_LOGGER: Final = logging.getLogger(__name__)
+
+
+@pytest.fixture(scope='function')
+def proof_dir(tmp_path_factory: TempPathFactory) -> Path:
+    return tmp_path_factory.mktemp('proofs')
+
+
+class TestImpMultiProof(KCFGExploreTest, KProveTest):
+    KOMPILE_MAIN_FILE = K_FILES / 'imp-verification.k'
+
+    @staticmethod
+    def _update_symbol_table(symbol_table: SymbolTable) -> None:
+        symbol_table['.List{"_,_"}_Ids'] = lambda: '.Ids'
+
+    MULTIPROOF_TEST_DATA = (
+        ('multiproof-passing', 'concrete-addition', 'concrete-identity', ProofStatus.PASSED),
+        ('multiproof-failing', 'concrete-addition-fail', 'concrete-identity', ProofStatus.FAILED),
+    )
+
+    @pytest.mark.parametrize(
+        'test_id,claim_id_1,claim_id_2,proof_status',
+        MULTIPROOF_TEST_DATA,
+        ids=[test_id for test_id, *_ in MULTIPROOF_TEST_DATA],
+    )
+    def test_multiproof_status(
+        self,
+        kprove: KProve,
+        kcfg_explore: KCFGExplore,
+        proof_dir: Path,
+        test_id: str,
+        claim_id_1: str,
+        claim_id_2: str,
+        proof_status: ProofStatus,
+    ) -> None:
+        spec_file = K_FILES / 'imp-simple-spec.k'
+        spec_module = 'IMP-FUNCTIONAL-SPEC'
+
+        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
+        )
+
+        assert mproof.status == ProofStatus.PENDING
+
+        equality_prover = ImpliesProver(equality_proof_1, kcfg_explore)
+        equality_prover.advance_proof(equality_proof_1)
+
+        equality_prover = ImpliesProver(equality_proof_2, kcfg_explore)
+        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