Fix bugs in node refutation functionality (#877)

This PR fixes bugs in the implementation of node refutation, in advance
of implementing a `kontrol refute-node` command as part of
runtimeverification/evm-semantics#1752. The following changes are
introduced:
1. Fix the way node refutations are read from a JSON file:
1. When iterating over the `node_refutations` dictionary, the `.items()`
method was missing, meaning that only the keys were being iterated over,
rather than both keys and values.
2. In the same line, the node id needed to be converted back to an int
before being passed to `_resolve`, since the JSON file stores the key as
a string.
2. Prevent refuting a node that has successors (otherwise execution of
the refuted branch, which should have been paused, will continue from
the successor nodes).
3. Add `refuted` to the list of attributes for a node when displaying
the KCFG.

---------

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

Author: 3 people

docs/conf.py

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

package/version

@@ -1 +1 @@
-0.1.622
+0.1.623

pyproject.toml

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

src/pyk/proof/reachability.py

@@ -198,7 +198,9 @@ def from_dict(cls: type[APRProof], dct: Mapping[str, Any], proof_dir: Path | Non
         subproof_ids = dct['subproof_ids'] if 'subproof_ids' in dct else []
         node_refutations: dict[int, str] = {}
         if 'node_refutation' in dct:
-            node_refutations = {kcfg._resolve(node_id): proof_id for (node_id, proof_id) in dct['node_refutations']}
+            node_refutations = {
+                kcfg._resolve(int(node_id)): proof_id for node_id, proof_id in dct['node_refutations'].items()
+            }
         if 'logs' in dct:
             logs = {int(k): tuple(LogEntry.from_dict(l) for l in ls) for k, ls in dct['logs'].items()}
         else:
@@ -404,7 +406,9 @@ def read_proof_data(proof_dir: Path, id: str) -> APRProof:
         terminal = proof_dict['terminal']
         logs = {int(k): tuple(LogEntry.from_dict(l) for l in ls) for k, ls in proof_dict['logs'].items()}
         subproof_ids = proof_dict['subproof_ids']
-        node_refutations = {kcfg._resolve(node_id): proof_id for (node_id, proof_id) in proof_dict['node_refutations']}
+        node_refutations = {
+            kcfg._resolve(int(node_id)): proof_id for node_id, proof_id in proof_dict['node_refutations'].items()
+        }
 
         return APRProof(
             id=id,
@@ -474,6 +478,10 @@ def unrefute_node(self, node: KCFG.Node) -> None:
         _LOGGER.info(f'Disabled refutation of node {node.id}.')
 
     def construct_node_refutation(self, node: KCFG.Node) -> RefutationProof | None:  # TODO put into prover class
+        if len(self.kcfg.successors(node.id)) > 0:
+            _LOGGER.error(f'Cannot refute node {node.id} that already has successors')
+            return None
+
         path = single(self.kcfg.paths_between(source_id=self.init, target_id=node.id))
         branches_on_path = list(filter(lambda x: type(x) is KCFG.Split or type(x) is KCFG.NDBranch, reversed(path)))
         if len(branches_on_path) == 0:

src/pyk/proof/show.py

@@ -36,6 +36,8 @@ def node_attrs(self, kcfg: KCFG, node: KCFG.Node) -> list[str]:
             attrs.append('target')
         if self.proof.is_pending(node.id):
             attrs.append('pending')
+        if self.proof.is_refuted(node.id):
+            attrs.append('refuted')
         if self.proof.is_terminal(node.id):
             attrs.append('terminal')
             if 'stuck' in attrs: