Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Proof container proof type #4358

Open
wants to merge 8 commits into
base: develop
Choose a base branch
from
Open
Show file tree
Hide file tree
Changes from 7 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion pyk/src/pyk/proof/implies.py
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down
61 changes: 60 additions & 1 deletion pyk/src/pyk/proof/proof.py
Original file line number Diff line number Diff line change
Expand Up @@ -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'}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(forming a thread)

I would like to make the use case very precise. Imagine that we did have a branching setUp, with all of its final states, together with the proofs of the associated test for each of the branches. How are these connected in the MultiProof? How do I know which proof corresponds to which branch? Could you give an example - imagine setUp branches into 3 possibilities.

Also, from the test below, I see that subproof_ids are used, but I don't see a proof that's their superproof.

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I was thinking the constructor proof, setUp proof(s), and the main proof(s) could just go directly under one MultiProof.

To know which proof corresponds to each branch, we would probably set the proof ID of the test function subproofs to something which included the node ID of the setUp KCFG it copies its starting configuration from. So if the function is called my_test, and the setUp function branches into 3 and ends on nodes 10, 11, and 12, the subproof graph could look something like:

[MyContract.my_test (MultiProof)]-->(
    [MyContract.setUp (APRProof)], 
    [MyContract.my_test_setup_config_10 (APRProof)], 
    [MyContract.my_test_setup_config_11 (APRProof)], 
    [MyContract.my_test_setup_config_12 (APRProof)], 
)

And of course you can also inspect the initial configurations of the subproofs.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thoughts, @tothtamas28, @ehildenb?

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I guess the subproof abstraction cannot be used here because in kontrol these proof obligations are manually constructed from one another. i.e.

init -> constructor done
constructor done -> setup done
setup done -> target
------------------------------
init -> target

is done by hand (i.e. not by the prover backend).

I wonder, would it be possible to use subproofs if we changed the semantics? Because in a semantics where constructor and setup steps are handled internally, this sequential compositon can be handled by the backend.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Example to better highlight the difference between subproofs and MultiProof as I understand it. Suppose we want to prove a -> c.

Subproof approach:

claim: a -> c
sub-claim: a -> b

If the proof passes, we know a -> c. The sub-claim might make proving more efficient, or might even be necessary for a -> c to pass.

MultiProof approach:

sub-claim: b -> c
sub-claim: a -> b

If the MultiProof passes, we know a -> c, but just because we constructed it so. The composition or the original calim a -> c is never machine-checked.


id: str
proof_dir: Path | None
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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'
Expand Down Expand Up @@ -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.
Comment on lines +294 to +297
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

(Continuing the discussion here to form a thread.)

What feature of a Proof does this class rely on, what makes it different from, say, a list[Proof]?

Copy link
Member Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It would be the logic in Proof.status which tracks the status of the subproofs to tell when the whole proof has been discharged, and the ability to save/load from disk.

"""

@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
Expand Down
131 changes: 131 additions & 0 deletions pyk/src/tests/integration/proof/test_multi_proof.py
Original file line number Diff line number Diff line change
@@ -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
Loading