Self-contained proof steps for EqualityProver and APRProver

docs/conf.py

@@ -9,8 +9,8 @@
 project = 'pyk'
 author = 'Runtime Verification, Inc'
 copyright = '2024, Runtime Verification, Inc'
-version = '0.1.631'
-release = '0.1.631'
+version = '0.1.632'
+release = '0.1.632'
 
 # -- General configuration ---------------------------------------------------
 # https://www.sphinx-doc.org/en/master/usage/configuration.html#general-configuration

package/version

@@ -1 +1 @@
-0.1.631
+0.1.632

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.631"
+version = "0.1.632"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

src/pyk/proof/implies.py

@@ -12,7 +12,7 @@
 from ..prelude.kbool import BOOL, TRUE
 from ..prelude.ml import is_bottom, is_top, mlAnd, mlEquals, mlEqualsFalse, mlEqualsTrue
 from ..utils import ensure_dir_path
-from .proof import Proof, ProofStatus, ProofSummary, Prover
+from .proof import Proof, ProofStatus, ProofStep, ProofSummary, Prover, StepResult
 
 if TYPE_CHECKING:
     from collections.abc import Iterable, Mapping
@@ -66,6 +66,32 @@ def status(self) -> ProofStatus:
         else:
             return ProofStatus.PASSED
 
+    def get_steps(self) -> Iterable[ProofStep]:
+        proof_type = type(self).__name__
+        _LOGGER.info(f'Attempting {proof_type} {self.id}')
+
+        if self.status is not ProofStatus.PENDING:
+            _LOGGER.info(f'{proof_type} finished {self.id}: {self.status}')
+            return []
+        return [
+            ImpliesProofStep(
+                antecedent=self.antecedent,
+                consequent=self.consequent,
+                proof_id=self.id,
+                bind_universally=self.bind_universally,
+            )
+        ]
+
+    def commit(self, result: StepResult) -> None:
+        proof_type = type(self).__name__
+        if isinstance(result, ImpliesProofResult):
+            self.csubst = result.csubst
+            self.simplified_antecedent = result.simplified_antecedent
+            self.simplified_consequent = result.simplified_consequent
+            _LOGGER.info(f'{proof_type} finished {self.id}: {self.status}')
+        else:
+            raise ValueError('Incorrect result type')
+
     @property
     def can_progress(self) -> bool:
         return self.simplified_antecedent is None or self.simplified_consequent is None
@@ -372,47 +398,58 @@ def lines(self) -> list[str]:
         ]
 
 
+@dataclass
+class ImpliesProofResult(StepResult):
+    csubst: CSubst | None
+    simplified_antecedent: KInner | None
+    simplified_consequent: KInner | None
+
+
+@dataclass
+class ImpliesProofStep(ProofStep):
+    antecedent: KInner
+    consequent: KInner
+    bind_universally: bool
+    proof_id: str
+
+
 class ImpliesProver(Prover):
     proof: ImpliesProof
 
     def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore):
         super().__init__(kcfg_explore)
         self.proof = proof
 
-    def step_proof(self) -> None:
-        proof_type = type(self.proof).__name__
-        _LOGGER.info(f'Attempting {proof_type} {self.proof.id}')
-
-        if self.proof.status is not ProofStatus.PENDING:
-            _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}')
-            return
+    def step_proof(self, step: ProofStep) -> StepResult:
+        assert isinstance(step, ImpliesProofStep)
 
         # to prove the equality, we check the implication of the form `constraints #Implies LHS #Equals RHS`, i.e.
         # "LHS equals RHS under these constraints"
-        antecedent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof.antecedent)
-        consequent_simplified_kast, _ = self.kcfg_explore.kast_simplify(self.proof.consequent)
-        self.proof.simplified_antecedent = antecedent_simplified_kast
-        self.proof.simplified_consequent = consequent_simplified_kast
-        _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(antecedent_simplified_kast)}')
-        _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(consequent_simplified_kast)}')
+        simplified_antecedent, _ = self.kcfg_explore.kast_simplify(step.antecedent)
+        simplified_consequent, _ = self.kcfg_explore.kast_simplify(step.consequent)
+        _LOGGER.info(f'Simplified antecedent: {self.kcfg_explore.kprint.pretty_print(simplified_antecedent)}')
+        _LOGGER.info(f'Simplified consequent: {self.kcfg_explore.kprint.pretty_print(simplified_consequent)}')
 
-        if is_bottom(antecedent_simplified_kast):
-            _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {self.proof.id}')
-            self.proof.csubst = CSubst(Subst({}), ())
+        csubst: CSubst | None = None
 
-        elif is_top(consequent_simplified_kast):
-            _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {self.proof.id}')
-            self.proof.csubst = CSubst(Subst({}), ())
+        if is_bottom(simplified_antecedent):
+            _LOGGER.warning(f'Antecedent of implication (proof constraints) simplifies to #Bottom {step.proof_id}')
+            csubst = CSubst(Subst({}), ())
+
+        elif is_top(simplified_consequent):
+            _LOGGER.warning(f'Consequent of implication (proof equality) simplifies to #Top {step.proof_id}')
+            csubst = CSubst(Subst({}), ())
 
         else:
-            # TODO: we should not be forced to include the dummy configuration in the antecedent and consequent
             dummy_config = self.kcfg_explore.kprint.definition.empty_config(sort=GENERATED_TOP_CELL)
-            result = self.kcfg_explore.cterm_implies(
-                antecedent=CTerm(config=dummy_config, constraints=[self.proof.simplified_antecedent]),
-                consequent=CTerm(config=dummy_config, constraints=[self.proof.simplified_consequent]),
-                bind_universally=self.proof.bind_universally,
+            implies_result = self.kcfg_explore.cterm_implies(
+                antecedent=CTerm(config=dummy_config, constraints=[simplified_antecedent]),
+                consequent=CTerm(config=dummy_config, constraints=[simplified_consequent]),
+                bind_universally=step.bind_universally,
             )
-            if result is not None:
-                self.proof.csubst = result
+            if implies_result is not None:
+                csubst = implies_result
 
-        _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}')
+        return ImpliesProofResult(
+            csubst=csubst, simplified_antecedent=simplified_antecedent, simplified_consequent=simplified_consequent
+        )

src/pyk/proof/proof.py

@@ -36,6 +36,14 @@ class Proof(ABC):
     _subproofs: dict[str, Proof]
     admitted: bool
 
+    @abstractmethod
+    def get_steps(self) -> Iterable[ProofStep]:
+        ...
+
+    @abstractmethod
+    def commit(self, result: StepResult) -> None:
+        ...
+
     @property
     def proof_subdir(self) -> Path | None:
         if self.proof_dir is None:
@@ -286,25 +294,36 @@ def lines(self) -> list[str]:
         return [line for lines in (summary.lines for summary in self.summaries) for line in lines]
 
 
+class StepResult:
+    ...
+
+
+class ProofStep:
+    ...
+
+
 class Prover:
     kcfg_explore: KCFGExplore
     proof: Proof
 
-    def __init__(self, kcfg_explore: KCFGExplore):
-        self.kcfg_explore = kcfg_explore
-
     @abstractmethod
-    def step_proof(self) -> None:
+    def step_proof(self, step: ProofStep) -> StepResult:
         ...
 
+    def __init__(self, kcfg_explore: KCFGExplore):
+        self.kcfg_explore = kcfg_explore
+
     def advance_proof(self, max_iterations: int | None = None, fail_fast: bool = False) -> None:
         iterations = 0
         while self.proof.can_progress:
-            if fail_fast and self.proof.failed:
-                _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}')
-                return
-            if max_iterations is not None and max_iterations <= iterations:
-                return
-            iterations += 1
-            self.step_proof()
-            self.proof.write_proof_data()
+            steps = self.proof.get_steps()
+            for step in steps:
+                iterations += 1
+                result = self.step_proof(step)
+                self.proof.commit(result)
+                self.proof.write_proof_data()
+                if fail_fast and self.proof.failed:
+                    _LOGGER.warning(f'Terminating proof early because fail_fast is set: {self.proof.id}')
+                    return
+                if max_iterations is not None and max_iterations <= iterations:
+                    return