diff --git a/pyk/src/pyk/proof/implies.py b/pyk/src/pyk/proof/implies.py index f6b59603608..e431d63eff5 100644 --- a/pyk/src/pyk/proof/implies.py +++ b/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, diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index f8600ed09ec..df247db29df 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/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 diff --git a/pyk/src/tests/integration/proof/test_multi_proof.py b/pyk/src/tests/integration/proof/test_multi_proof.py new file mode 100644 index 00000000000..681f02872cf --- /dev/null +++ b/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