Check if pre-branch node is subsumed in AGProver, add CTerm.cell (#340)

Currently, if we have a proof that reaches a branch-point, and the pre-branch state is subsumed into the target state, it will still compute the branches, and then check each post-branch state individually for subsumption into the target state. The branches are still subsumed into the target, but it makes the KCFG more complicated because it has the uneeded branch there. This PR: - Adds a test where subsumption happens at a branch point, and fails because we set it to only do one iteration of extending the prover (passes after these changes). - Factors out the final subsumption check into its own routine, and calls it on new frontier nodes as well as on new pre-branch nodes. - Adds a helper getter `CTerm.cell(...)` as a shortcut to `get_cell(CTerm.config, ...)` - Removes the unused parameter `simplify_init` to `AGProver.advance_proof(...)`. It has been tested on [this proof](https://github.com/runtimeverification/evm-semantics/blob/master/tests/specs/mcd/vat-addui-pass-spec.k), which is subsumed right at the branch point, and does indeed produce a smaller KCFG. This proof was introduced by @dkcumming in order to work on proof-reuse in the larger still-failing proofs in KEVM test-suite. With this change, we reduce the branching factor of the proof from 6 to 3. The overall runtime goes from ~4min to ~3min40s (not much change), and the number of queries to the RPC server goes from 26 to 25 (not much change). Overall this will increase the number of implication checks we make, but still not nearly as many as the original prover made. The test added fails before the change because with `--max-iterations=1` set, it never makes it to checking subsumption into the target state once it hits the branch point on the `if(...) ...` statement. But with this change, it checks subsumption into the target state as soon as it's made the first basic block, and the proof is discharged. --------- Co-authored-by: devops <devops@runtimeverification.com>
runtimeverification · Apr 11, 2023 · fb5f409 · fb5f409
1 parent 4874526
commit fb5f409
Show file tree

Hide file tree

Showing 9 changed files with 58 additions and 30 deletions.
diff --git a/k-files/imp-simple-spec.k b/k-files/imp-simple-spec.k
@@ -9,8 +9,11 @@ module IMP-SIMPLE-SPEC
 
     claim [addition-var]: <k> 3 + N => 7 ... </k> requires N ==Int 4
 
+    claim [pre-branch-proved]: <k> $n = 7 ; if (B:Bool) { $n = 6 ; } else { $n = 5 ; } ~> #FINISH => if (B:Bool) { $n = 6 ; } else { $n = 5 ; } ~> #FINISH </k>
+                               <state> $n |-> (0 => 7) </state>
+
     claim [sum-10]: <k> int $s, $n, .Ids ; $n = 10 ; while (0 <= $n) { $s = $s + $n ; $n = $n + -1 ; } ~> #FINISH => . ... </k>
-                     <state> .Map => $s |-> 55 $n |-> -1 </state>
+                    <state> .Map => $s |-> 55 $n |-> -1 </state>
 
     claim [sum-100]: <k> int $s, $n, .Ids ; $n = 100 ; while (0 <= $n) { $s = $s + $n ; $n = $n + -1 ; } ~> #FINISH => . ... </k>
                      <state> .Map => $s |-> 5050 $n |-> -1 </state>

diff --git a/package/version b/package/version
@@ -1 +1 @@
-0.1.225
+0.1.226
diff --git a/pyproject.toml b/pyproject.toml
@@ -4,7 +4,7 @@ build-backend = "poetry.core.masonry.api"
 
 [tool.poetry]
 name = "pyk"
-version = "0.1.225"
+version = "0.1.226"
 description = ""
 authors = [
     "Runtime Verification, Inc. <contact@runtimeverification.com>",

diff --git a/src/pyk/cterm.py b/src/pyk/cterm.py
@@ -17,6 +17,7 @@
     remove_generated_cells,
     simplify_bool,
     split_config_and_constraints,
+    split_config_from,
 )
 from .kast.outer import KClaim, KRule
 from .prelude.k import GENERATED_TOP_CELL
@@ -94,6 +95,14 @@ def kast(self) -> KInner:
     def hash(self) -> str:
         return self.kast.hash
 
+    @cached_property
+    def cells(self) -> Subst:
+        _, subst = split_config_from(self.config)
+        return Subst(subst)
+
+    def cell(self, cell: str) -> KInner:
+        return self.cells[cell]
+
     def match(self, cterm: CTerm) -> Subst | None:
         csubst = self.match_with_constraint(cterm)
 

diff --git a/src/pyk/proof/reachability.py b/src/pyk/proof/reachability.py
@@ -70,6 +70,27 @@ class AGProver:
     def __init__(self, proof: AGProof) -> None:
         self.proof = proof
 
+    def _check_subsumption(
+        self,
+        kcfg_explore: KCFGExplore,
+        curr_node: KCFG.Node,
+        is_terminal: Callable[[CTerm], bool] | None = None,
+        implication_every_block: bool = True,
+    ) -> bool:
+        if implication_every_block or (is_terminal is not None and is_terminal(curr_node.cterm)):
+            target_node = self.proof.kcfg.get_unique_target()
+            _LOGGER.info(
+                f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
+            )
+            csubst = kcfg_explore.cterm_implies(curr_node.cterm, target_node.cterm)
+            if csubst is not None:
+                self.proof.kcfg.create_cover(curr_node.id, target_node.id, csubst=csubst)
+                _LOGGER.info(
+                    f'Subsumed into target node {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
+                )
+                return True
+        return False
+
     def advance_proof(
         self,
         kcfg_explore: KCFGExplore,
@@ -79,10 +100,8 @@ def advance_proof(
         execute_depth: int | None = None,
         cut_point_rules: Iterable[str] = (),
         terminal_rules: Iterable[str] = (),
-        simplify_init: bool = True,
         implication_every_block: bool = True,
     ) -> KCFG:
-        target_node = self.proof.kcfg.get_unique_target()
         iterations = 0
 
         while self.proof.kcfg.frontier:
@@ -94,17 +113,10 @@ def advance_proof(
             iterations += 1
             curr_node = self.proof.kcfg.frontier[0]
 
-            if implication_every_block or (is_terminal is not None and is_terminal(curr_node.cterm)):
-                _LOGGER.info(
-                    f'Checking subsumption into target state {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
-                )
-                csubst = kcfg_explore.cterm_implies(curr_node.cterm, target_node.cterm)
-                if csubst is not None:
-                    self.proof.kcfg.create_cover(curr_node.id, target_node.id, csubst=csubst)
-                    _LOGGER.info(
-                        f'Subsumed into target node {self.proof.id}: {shorten_hashes((curr_node.id, target_node.id))}'
-                    )
-                    continue
+            if self._check_subsumption(
+                kcfg_explore, curr_node, is_terminal=is_terminal, implication_every_block=implication_every_block
+            ):
+                continue
 
             if is_terminal is not None:
                 _LOGGER.info(f'Checking terminal {self.proof.id}: {shorten_hashes(curr_node.id)}')
@@ -132,6 +144,11 @@ def advance_proof(
                 )
                 curr_node = next_node
 
+                if self._check_subsumption(
+                    kcfg_explore, curr_node, is_terminal=is_terminal, implication_every_block=implication_every_block
+                ):
+                    continue
+
             if len(next_cterms) == 0:
                 _LOGGER.info(f'Found stuck node {self.proof.id}: {shorten_hashes(curr_node.id)}')
 

diff --git a/src/tests/integration/kcfg/test_cell_map.py b/src/tests/integration/kcfg/test_cell_map.py
@@ -7,7 +7,6 @@
 
 from pyk.cterm import CTerm
 from pyk.kast.inner import KApply, KSequence, KToken, KVariable, build_assoc
-from pyk.kast.manip import get_cell
 from pyk.kcfg import KCFG
 from pyk.proof import AGProof, AGProver
 
@@ -103,7 +102,7 @@ def test_execute(
         actual_depth, actual_post_term, _ = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, k, aacounts, accounts), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
 
         # Then
         assert actual_depth == expected_depth

diff --git a/src/tests/integration/kcfg/test_imp.py b/src/tests/integration/kcfg/test_imp.py
@@ -7,7 +7,6 @@
 
 from pyk.cterm import CSubst, CTerm
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, KVariable, Subst
-from pyk.kast.manip import get_cell
 from pyk.kcfg import KCFG
 from pyk.prelude.kint import intToken
 from pyk.prelude.ml import mlAnd, mlBottom, mlEqualsFalse, mlEqualsTrue
@@ -111,6 +110,7 @@
     ('imp-simple-addition-1', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-1', 2, 1, []),
     ('imp-simple-addition-2', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-2', 2, 7, []),
     ('imp-simple-addition-var', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'addition-var', 2, 1, []),
+    ('pre-branch-proved', 'k-files/imp-simple-spec.k', 'IMP-SIMPLE-SPEC', 'pre-branch-proved', 1, 100, []),
     (
         'imp-simple-sum-10',
         'k-files/imp-simple-spec.k',
@@ -193,13 +193,13 @@ def test_execute(
         actual_depth, actual_post_term, actual_next_terms = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, k, state), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
-        actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'STATE_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
+        actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL'))
 
         actual_next_states = [
             (
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'K_CELL')),
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'STATE_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('K_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')),
             )
             for s in actual_next_terms
         ]

diff --git a/src/tests/integration/kcfg/test_simple.py b/src/tests/integration/kcfg/test_simple.py
@@ -81,12 +81,12 @@ def test_execute(
         actual_depth, actual_post_term, actual_next_terms = kcfg_explore.cterm_execute(
             self.config(kcfg_explore.kprint, *pre), depth=depth
         )
-        actual_k = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'K_CELL'))
-        actual_state = kcfg_explore.kprint.pretty_print(get_cell(actual_post_term.kast, 'STATE_CELL'))
+        actual_k = kcfg_explore.kprint.pretty_print(actual_post_term.cell('K_CELL'))
+        actual_state = kcfg_explore.kprint.pretty_print(actual_post_term.cell('STATE_CELL'))
         actual_next_states = [
             (
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'K_CELL')),
-                kcfg_explore.kprint.pretty_print(get_cell(s.kast, 'STATE_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('K_CELL')),
+                kcfg_explore.kprint.pretty_print(s.cell('STATE_CELL')),
             )
             for s in actual_next_terms
         ]

diff --git a/src/tests/integration/test_krun.py b/src/tests/integration/test_krun.py
@@ -5,7 +5,7 @@
 import pytest
 
 from pyk.kast.inner import KApply, KSequence, KSort, KToken, Subst
-from pyk.kast.manip import flatten_label, get_cell
+from pyk.kast.manip import flatten_label
 from pyk.kore.prelude import int_dv
 from pyk.kore.syntax import App
 from pyk.prelude.kint import intToken
@@ -34,8 +34,8 @@ def test_run(self, krun: KRun) -> None:
         ]
 
         # When
-        actual_k = get_cell(final_cterm.config, 'K_CELL')
-        actual_map_items = flatten_label('_Map_', get_cell(final_cterm.config, 'STATE_CELL'))
+        actual_k = final_cterm.cell('K_CELL')
+        actual_map_items = flatten_label('_Map_', final_cterm.cell('STATE_CELL'))
 
         assert actual_k == expected_k
         assert set(actual_map_items) == set(expected_map_items)