From cb7fb937a02f17fc3adbdad1e3b783e8662a1401 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 15 May 2024 17:56:08 -0500 Subject: [PATCH 1/5] Add MultiProof --- pyk/src/pyk/proof/proof.py | 45 +++++++++ .../integration/proof/test_multi_proof.py | 94 +++++++++++++++++++ 2 files changed, 139 insertions(+) create mode 100644 pyk/src/tests/integration/proof/test_multi_proof.py diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index f8600ed09ec..2cb0d89ba57 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -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 @@ -287,6 +289,49 @@ 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 True + + def commit(self, result: SR) -> None: + """Apply the step result of type `SR` to `self`, modifying `self`.""" + ... + + @classmethod + def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> Proof: + _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) + + def get_steps(self) -> Iterable[PS]: + """Return all currently available steps associated with this Proof. Should not modify `self`.""" + return [] + + @property + def own_status(self) -> ProofStatus: + return ProofStatus.PASSED + + 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..bb89b6a3ca0 --- /dev/null +++ b/pyk/src/tests/integration/proof/test_multi_proof.py @@ -0,0 +1,94 @@ +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_pass( + 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 From 7c428642e264712f47a794cbb5241a8d04d0a6d0 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 15 May 2024 17:58:39 -0500 Subject: [PATCH 2/5] Remove typevars from MultiProof definition --- pyk/src/pyk/proof/proof.py | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 2cb0d89ba57..414e72ebfd2 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -300,9 +300,7 @@ class MultiProof(Proof[None, None]): def can_progress(self) -> bool: return True - def commit(self, result: SR) -> None: - """Apply the step result of type `SR` to `self`, modifying `self`.""" - ... + def commit(self, result: None) -> None: ... @classmethod def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> Proof: @@ -311,7 +309,7 @@ def from_dict(cls: type[Proof], dct: Mapping[str, Any], proof_dir: Path | None = _admitted = dct['admitted'] return MultiProof(id=_id, subproof_ids=_subproof_ids, proof_dir=proof_dir, admitted=_admitted) - def get_steps(self) -> Iterable[PS]: + def get_steps(self) -> Iterable[None]: """Return all currently available steps associated with this Proof. Should not modify `self`.""" return [] From 66c49c12a01e2c5b03478beea4c6b69a11534bae Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Wed, 15 May 2024 18:23:45 -0500 Subject: [PATCH 3/5] Add disk read/write test and fix --- pyk/src/pyk/proof/proof.py | 20 ++++++++- .../integration/proof/test_multi_proof.py | 41 ++++++++++++++++++- 2 files changed, 57 insertions(+), 4 deletions(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 414e72ebfd2..8a1c9e6d89e 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 @@ -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: diff --git a/pyk/src/tests/integration/proof/test_multi_proof.py b/pyk/src/tests/integration/proof/test_multi_proof.py index bb89b6a3ca0..681f02872cf 100644 --- a/pyk/src/tests/integration/proof/test_multi_proof.py +++ b/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 From 71892762c1bd136754118a41ffb6b0c2e33945c9 Mon Sep 17 00:00:00 2001 From: Noah Watson Date: Thu, 16 May 2024 13:30:49 -0500 Subject: [PATCH 4/5] Fix bug in RefutationProof antecedent building --- pyk/src/pyk/proof/implies.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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, From da55d8d0320286d73fcd1604cba5cf112bf779c1 Mon Sep 17 00:00:00 2001 From: Noah Watson <107630091+nwatson22@users.noreply.github.com> Date: Thu, 16 May 2024 13:55:39 -0500 Subject: [PATCH 5/5] Update pyk/src/pyk/proof/proof.py --- pyk/src/pyk/proof/proof.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/pyk/src/pyk/proof/proof.py b/pyk/src/pyk/proof/proof.py index 8a1c9e6d89e..df247db29df 100644 --- a/pyk/src/pyk/proof/proof.py +++ b/pyk/src/pyk/proof/proof.py @@ -299,7 +299,7 @@ class MultiProof(Proof[None, None]): @property def can_progress(self) -> bool: - return True + return False def commit(self, result: None) -> None: ...