Automating implication-every-block reasoning (#580)

This PR removes the need for the `implication-every-block` parameter in
APR-related provers. The reasoning is as follows:
- if the `target` node is a `terminal` node, then subsumption into
target should be checked only for `terminal` nodes (equivalent to
previously setting `implication-every-block` to `false`)
- otherwise (and this is possible, for example, for internal functions),
subsumption into target is checked on every block ((equivalent to
previously setting `implication-every-block` to `true`).

I am assuming that this change requires changes to KEVM so that the
`implication-every-block` parameter is removed.

---------

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

Author: PetarMax

package/version

@@ -1 +1 @@
-0.1.402
+0.1.403

pyproject.toml

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

src/pyk/proof/reachability.py

@@ -557,6 +557,8 @@ class APRProver(Prover):
     dependencies_module_name: str
     circularities_module_name: str
 
+    _target_is_terminal: bool
+
     def __init__(
         self,
         proof: APRProof,
@@ -591,6 +593,10 @@ def __init__(
             priority=1,
         )
 
+        self._target_is_terminal = kcfg_explore.kcfg_semantics.is_terminal(
+            self.proof.kcfg.node(self.proof.target).cterm
+        )
+
     def nonzero_depth(self, node: KCFG.Node) -> bool:
         return not self.proof.kcfg.zero_depth_between(self.proof.init, node.id)
 
@@ -620,13 +626,12 @@ def advance_pending_node(
         execute_depth: int | None = None,
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
-        implication_every_block: bool = True,
     ) -> None:
         if self._check_terminal(node):
             _ = self._check_subsume(node)
             return
 
-        if implication_every_block:
+        if not self._target_is_terminal:
             if self._check_subsume(node):
                 return
 
@@ -647,7 +652,6 @@ def advance_proof(
         execute_depth: int | None = None,
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
-        implication_every_block: bool = True,
         fail_fast: bool = False,
     ) -> KCFG:
         iterations = 0
@@ -671,7 +675,6 @@ def advance_proof(
                 execute_depth=execute_depth,
                 cut_point_rules=cut_point_rules,
                 terminal_rules=terminal_rules,
-                implication_every_block=implication_every_block,
             )
 
         self.proof.write_proof_data()
@@ -855,7 +858,6 @@ def advance_pending_node(
         execute_depth: int | None = None,
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
-        implication_every_block: bool = True,
     ) -> None:
         if node.id not in self._checked_nodes:
             _LOGGER.info(f'Checking bmc depth for node {self.proof.id}: {node.id}')
@@ -881,7 +883,6 @@ def advance_pending_node(
             execute_depth=execute_depth,
             cut_point_rules=cut_point_rules,
             terminal_rules=terminal_rules,
-            implication_every_block=implication_every_block,
         )