Store failure info in Proof (#654)

I'm trying to simplify the kontrol code that computes failure logs for
each of the failing proofs, and I thought maybe it would be simpler if
we could just pass around the Proof object and have any necessary info
be available from there. We already have functions of `Proof` that
pertain to the proof status. Currently in KEVM to get the failure log,
we have to call a function separately when we detect a proof has failed
that computes this log, which requires a `KCFGExplore`, and also takes a
nontrivial amount of time. We then have to pass this around as part of a
tuple. This makes the computing of the failure info automatically happen
when a failing proof is detected, and saves the `APRFailureInfo` object
as a field in the `APRProof`.

The potential drawback I see to this is it would hurt performance on
failing proofs if the user doesn't care about generating the
`APRFailureInfo` for the proof.

---------

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

package/version

@@ -1 +1 @@
-0.1.442
+0.1.443

pyproject.toml

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

src/pyk/proof/reachability.py

@@ -47,6 +47,7 @@ class APRProof(Proof, KCFGExploration):
     target: int
     logs: dict[int, tuple[LogEntry, ...]]
     circularity: bool
+    failure_info: APRFailureInfo | None
 
     def __init__(
         self,
@@ -65,6 +66,7 @@ def __init__(
         Proof.__init__(self, id, proof_dir=proof_dir, subproof_ids=subproof_ids, admitted=admitted)
         KCFGExploration.__init__(self, kcfg, terminal)
 
+        self.failure_info = None
         self.init = kcfg._resolve(init)
         self.target = kcfg._resolve(target)
         self.logs = logs
@@ -534,17 +536,20 @@ class APRProver(Prover):
     main_module_name: str
     dependencies_module_name: str
     circularities_module_name: str
+    counterexample_info: bool
 
     _checked_terminals: set[int]
 
     def __init__(
         self,
         proof: APRProof,
         kcfg_explore: KCFGExplore,
+        counterexample_info: bool = False,
     ) -> None:
         super().__init__(kcfg_explore)
         self.proof = proof
         self.main_module_name = self.kcfg_explore.kprint.definition.main_module_name
+        self.counterexample_info = counterexample_info
 
         subproofs: list[Proof] = (
             [Proof.read_proof_data(proof.proof_dir, i) for i in proof.subproof_ids]
@@ -662,6 +667,9 @@ def advance_proof(
                 if self.proof.kcfg.is_leaf(node.id) and not self.proof.is_target(node.id):
                     self._check_subsume(node)
 
+        if self.proof.failed:
+            self.save_failure_info()
+
         self.proof.write_proof_data()
 
     def refute_node(self, node: KCFG.Node) -> RefutationProof | None:
@@ -730,8 +738,11 @@ def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None:
         self.proof.add_subproof(refutation)
         return refutation
 
+    def save_failure_info(self) -> None:
+        self.proof.failure_info = self.failure_info()
+
     def failure_info(self) -> APRFailureInfo:
-        return APRFailureInfo.from_proof(self.proof, self.kcfg_explore)
+        return APRFailureInfo.from_proof(self.proof, self.kcfg_explore, counterexample_info=self.counterexample_info)
 
 
 @dataclass(frozen=True)
@@ -869,10 +880,12 @@ def __init__(
         self,
         proof: APRBMCProof,
         kcfg_explore: KCFGExplore,
+        counterexample_info: bool = False,
     ) -> None:
         super().__init__(
             proof,
             kcfg_explore=kcfg_explore,
+            counterexample_info=counterexample_info,
         )
         self._checked_nodes = []