Make advance proof functionality generic (#875)

~Blocked on: #878

In an attempt to make the prover interfaces simpler, we are making it so
that `advance_proof` is a generic method among all `*Prover` classes.
This will allow us to have a generic way to call subproofs and advance
them, then call superproofs and advance them, which will allow
simplifying some downstream logic a bit.

- Makes it so that `mlEqualsTrue` and `mlEqualsFalse` can take sort
arguments for their outer sort.
- Moves all the `APRProof` specific arguments of
`APRProof.advance_proof` to the constructor instead.
- Adds an `abstractmethod Proof.step_proof(...)` which should take one
step of executing a proof to completion.
- Adds an `abstractmethod Proof.can_progress` which lets you know if
it's possible to make progress on a given proof.
- Implements generic `Proof.advance_proof(...)` which handles calling
`step_proof` in a loop until either `max_iterations` is reached, the
proof can no longer progress, or if `fail_fast` trigger hits. It also
handles writing proof data each iteration.
- Adjusts all the tests to the new interface.

---------

Co-authored-by: devops <[email protected]>

Author: ehildenb

docs/conf.py

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

package/version

@@ -1 +1 @@
-0.1.626
+0.1.627

pyproject.toml

@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.626"
+version = "0.1.627"
 description = ""
 authors = [
     "Runtime Verification, Inc. <[email protected]>",

src/pyk/proof/equality.py

@@ -62,6 +62,10 @@ def status(self) -> ProofStatus:
         else:
             return ProofStatus.PASSED
 
+    @property
+    def can_progress(self) -> bool:
+        return self.simplified_antecedent is None or self.simplified_consequent is None
+
     def write_proof_data(self, subproofs: bool = False) -> None:
         super().write_proof_data()
         if not self.proof_dir:
@@ -352,7 +356,7 @@ def __init__(self, proof: ImpliesProof, kcfg_explore: KCFGExplore):
         super().__init__(kcfg_explore)
         self.proof = proof
 
-    def advance_proof(self) -> None:
+    def step_proof(self) -> None:
         proof_type = type(self.proof).__name__
         _LOGGER.info(f'Attempting {proof_type} {self.proof.id}')
 
@@ -388,4 +392,3 @@ def advance_proof(self) -> None:
                 self.proof.csubst = result
 
         _LOGGER.info(f'{proof_type} finished {self.proof.id}: {self.proof.status}')
-        self.proof.write_proof_data()

src/pyk/proof/proof.py

@@ -174,6 +174,11 @@ def subproofs_status(self) -> ProofStatus:
     def status(self) -> ProofStatus:
         ...
 
+    @property
+    @abstractmethod
+    def can_progress(self) -> bool:
+        ...
+
     @property
     def failed(self) -> bool:
         return self.status == ProofStatus.FAILED
@@ -283,6 +288,23 @@ def lines(self) -> list[str]:
 
 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 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()

src/pyk/proof/reachability.py

@@ -186,6 +186,10 @@ def status(self) -> ProofStatus:
         else:
             return ProofStatus.PASSED
 
+    @property
+    def can_progress(self) -> bool:
+        return len(self.pending) > 0
+
     @classmethod
     def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | None = None) -> APRProof:
         kcfg = KCFG.from_dict(dct['kcfg'])
@@ -533,6 +537,9 @@ class APRProver(Prover):
     main_module_name: str
     dependencies_module_name: str
     circularities_module_name: str
+    execute_depth: int | None
+    cut_point_rules: Iterable[str]
+    terminal_rules: Iterable[str]
     counterexample_info: bool
     always_check_subsumption: bool
     fast_check_subsumption: bool
@@ -545,6 +552,9 @@ def __init__(
         self,
         proof: APRProof,
         kcfg_explore: KCFGExplore,
+        execute_depth: int | None = None,
+        cut_point_rules: Iterable[str] = (),
+        terminal_rules: Iterable[str] = (),
         counterexample_info: bool = False,
         always_check_subsumption: bool = True,
         fast_check_subsumption: bool = False,
@@ -559,6 +569,9 @@ def _inject_module(module_name: str, import_name: str, sentences: list[KRuleLike
         super().__init__(kcfg_explore)
         self.proof = proof
         self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name
+        self.execute_depth = execute_depth
+        self.cut_point_rules = cut_point_rules
+        self.terminal_rules = terminal_rules
         self.counterexample_info = counterexample_info
         self.always_check_subsumption = always_check_subsumption
         self.fast_check_subsumption = fast_check_subsumption
@@ -672,57 +685,33 @@ def advance_pending_node(
             module_name=module_name,
         )
 
-    def advance_proof(
-        self,
-        max_iterations: int | None = None,
-        execute_depth: int | None = None,
-        cut_point_rules: Iterable[str] = (),
-        terminal_rules: Iterable[str] = (),
-        fail_fast: bool = False,
-    ) -> None:
-        iterations = 0
-
+    def step_proof(self) -> None:
         self._check_all_terminals()
 
-        while self.proof.pending:
-            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}, failing nodes: {[nd.id for nd in self.proof.failing]}'
-                )
-                break
-
-            if max_iterations is not None and max_iterations <= iterations:
-                _LOGGER.warning(f'Reached iteration bound {self.proof.id}: {max_iterations}')
-                break
-            iterations += 1
-            curr_node = self.proof.pending[0]
-
-            self.advance_pending_node(
-                node=curr_node,
-                execute_depth=execute_depth,
-                cut_point_rules=cut_point_rules,
-                terminal_rules=terminal_rules,
-            )
-
-            self._check_all_terminals()
+        if not self.proof.pending:
+            return
+        curr_node = self.proof.pending[0]
 
-            for node in self.proof.terminal:
-                if (
-                    not node.id in self._checked_for_subsumption
-                    and self.proof.kcfg.is_leaf(node.id)
-                    and not self.proof.is_target(node.id)
-                ):
-                    self._checked_for_subsumption.add(node.id)
-                    self._check_subsume(node)
+        self.advance_pending_node(
+            node=curr_node,
+            execute_depth=self.execute_depth,
+            cut_point_rules=self.cut_point_rules,
+            terminal_rules=self.terminal_rules,
+        )
 
-        if self.proof.failed:
-            self.save_failure_info()
+        self._check_all_terminals()
 
-        self.proof.write_proof_data()
+        for node in self.proof.terminal:
+            if (
+                not node.id in self._checked_for_subsumption
+                and self.proof.kcfg.is_leaf(node.id)
+                and not self.proof.is_target(node.id)
+            ):
+                self._checked_for_subsumption.add(node.id)
+                self._check_subsume(node)
 
-    def save_failure_info(self) -> None:
-        self.proof.failure_info = self.failure_info()
+        if self.proof.failed:
+            self.proof.failure_info = self.failure_info()
 
     def failure_info(self) -> APRFailureInfo:
         return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)

src/tests/integration/proof/test_cell_map.py

@@ -136,11 +136,8 @@ def test_all_path_reachability_prove(
         init = proof.kcfg.node(proof.init)
         new_init_term = kcfg_explore.cterm_assume_defined(init.cterm)
         proof.kcfg.replace_node(init.id, new_init_term)
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(
-            max_iterations=max_iterations,
-            execute_depth=max_depth,
-        )
+        prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth)
+        prover.advance_proof(max_iterations=max_iterations)
 
         kcfg_show = KCFGShow(
             kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True)

src/tests/integration/proof/test_goto.py

@@ -116,13 +116,14 @@ def test_all_path_bmc_reachability_prove(
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, bmc_depth=bmc_depth)
         kcfg_explore.simplify(proof.kcfg, {})
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(
-            max_iterations=max_iterations,
+        prover = APRProver(
+            proof,
+            kcfg_explore=kcfg_explore,
             execute_depth=max_depth,
             cut_point_rules=cut_rules,
             terminal_rules=terminal_rules,
         )
+        prover.advance_proof(max_iterations=max_iterations)
 
         kcfg_show = KCFGShow(
             kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True)

src/tests/integration/proof/test_imp.py

@@ -903,8 +903,8 @@ def test_all_path_reachability_prove(
                     subproof.admit()
                     subproof.write_proof_data()
 
-            prover = APRProver(proof, kcfg_explore=kcfg_explore)
-            prover.advance_proof(max_iterations=max_iterations, execute_depth=max_depth, cut_point_rules=cut_rules)
+            prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth, cut_point_rules=cut_rules)
+            prover.advance_proof(max_iterations=max_iterations)
 
             kcfg_show = KCFGShow(
                 kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True)
@@ -944,13 +944,14 @@ def _node_printer(cterm: CTerm) -> list[str]:
         )
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(
-            max_iterations=max_iterations,
+        prover = APRProver(
+            proof,
+            kcfg_explore=kcfg_explore,
             execute_depth=max_depth,
             terminal_rules=terminal_rules,
             cut_point_rules=cut_rules,
         )
+        prover.advance_proof(max_iterations=max_iterations)
 
         assert len(proof.failing) == 1
         path_constraint = proof.path_constraints(proof.failing[0].id)
@@ -984,13 +985,14 @@ def test_all_path_bmc_reachability_prove(
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, bmc_depth=bmc_depth)
         kcfg_explore.simplify(proof.kcfg, {})
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(
-            max_iterations=max_iterations,
+        prover = APRProver(
+            proof,
+            kcfg_explore=kcfg_explore,
             execute_depth=max_depth,
             terminal_rules=terminal_rules,
             cut_point_rules=cut_rules,
         )
+        prover.advance_proof(max_iterations=max_iterations)
 
         kcfg_show = KCFGShow(
             kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True)
@@ -1057,8 +1059,8 @@ def test_apr_prove_read_write_node_data(
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proofs_dir)
         kcfg_explore.simplify(proof.kcfg, {})
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(execute_depth=1)
+        prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=1)
+        prover.advance_proof()
 
         proof_from_disk = APRProof.read_proof_data(proof_dir=proofs_dir, id=proof.id)
 
@@ -1082,8 +1084,8 @@ def test_aprbmc_prove_read_write_node_data(
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proofs_dir, bmc_depth=3)
         kcfg_explore.simplify(proof.kcfg, {})
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(execute_depth=1)
+        prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=1)
+        prover.advance_proof()
 
         proof_from_disk = APRProof.read_proof_data(proof_dir=proofs_dir, id=proof.id)
 
@@ -1116,7 +1118,6 @@ def test_fail_fast(
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={}, proof_dir=proof_dir)
         prover = APRProver(proof, kcfg_explore=kcfg_explore)
-
         prover.advance_proof(fail_fast=True)
 
         # First branch will be reached first and terminate the proof, leaving the second long branch pending (fail_fast=True)

src/tests/integration/proof/test_mini_kevm.py

@@ -93,8 +93,10 @@ def test_all_path_reachability_prove(
             prover = APRProver(
                 proof,
                 kcfg_explore=kcfg_explore,
+                execute_depth=max_depth,
+                cut_point_rules=cut_rules,
             )
-            prover.advance_proof(max_iterations=max_iterations, execute_depth=max_depth, cut_point_rules=cut_rules)
+            prover.advance_proof(max_iterations=max_iterations)
 
             kcfg_show = KCFGShow(
                 kcfg_explore.kprint,

src/tests/integration/proof/test_non_det.py

@@ -54,11 +54,8 @@ def test_all_path_reachability_prove(
         )
 
         proof = APRProof.from_claim(kprove.definition, claim, logs={})
-        prover = APRProver(proof, kcfg_explore=kcfg_explore)
-        prover.advance_proof(
-            max_iterations=max_iterations,
-            execute_depth=max_depth,
-        )
+        prover = APRProver(proof, kcfg_explore=kcfg_explore, execute_depth=max_depth)
+        prover.advance_proof(max_iterations=max_iterations)
 
         kcfg_show = KCFGShow(
             kcfg_explore.kprint, node_printer=APRProofNodePrinter(proof, kcfg_explore.kprint, full_printer=True)