From df56618b5755d4088972c8ffea8cc5ee01881fac Mon Sep 17 00:00:00 2001
From: Noah Watson <107630091+nwatson22@users.noreply.github.com>
Date: Wed, 14 Aug 2024 14:02:27 -0500
Subject: [PATCH] APRProof get_steps optimizations (#4585)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- Calling `nonzero_depth` is (relatively) expensive, when it's done for
each pending nodes and we have 50+ pending nodes. This is because it
traverses the KCFG to find all paths between the init node and the
current node.
- We were calling `nonzero_depth` twice unnecessarily. Caches the result
in a variable instead.
- In most cases, depth will be immediately obvious to be nonzero just
from looking at the first edge on the path. In this case, skips the
traversal. Also skips the traversal if the nodes we are checking the if
the depth between is 0 for if they are the same node.
- Tested on
`test%kontrol%VetoSignallingTest.testVetoSignallingInvariantsArePreserved4(uint256,uint256,uint256)`
from the lido tests. Around 400 nodes in, the sync time is 0.3-0.4
seconds without the optimization. With the optimization it is around
0.015 to 0.04 seconds (although this also depends on the number of
pending nodes at any given time). This seems to eliminates the bulk of
the sync time when there are a large number of pending nodes (~30+).

---------

Co-authored-by: Petar Maksimović <PetarMax@users.noreply.github.com>
---
 pyk/src/pyk/kcfg/kcfg.py          | 14 +++++++++++++-
 pyk/src/pyk/proof/reachability.py |  5 +++--
 2 files changed, 16 insertions(+), 3 deletions(-)

diff --git a/pyk/src/pyk/kcfg/kcfg.py b/pyk/src/pyk/kcfg/kcfg.py
index d3f9247e49f..835aea290c5 100644
--- a/pyk/src/pyk/kcfg/kcfg.py
+++ b/pyk/src/pyk/kcfg/kcfg.py
@@ -1188,7 +1188,19 @@ def shortest_distance_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike
         return distance
 
     def zero_depth_between(self, node_1_id: NodeIdLike, node_2_id: NodeIdLike) -> bool:
-        shortest_distance = self.shortest_distance_between(node_1_id, node_2_id)
+        _node_1_id = self._resolve(node_1_id)
+        _node_2_id = self._resolve(node_2_id)
+        if _node_1_id == _node_2_id:
+            return True
+        # Short-circuit and don't run pathing algorithm if there is no 0 length path on the first step.
+        path_lengths = [
+            self.path_length([successor]) for successor in self.successors(_node_1_id) + self.successors(_node_2_id)
+        ]
+        if 0 not in path_lengths:
+            return False
+
+        shortest_distance = self.shortest_distance_between(_node_1_id, _node_2_id)
+
         return shortest_distance is not None and shortest_distance == 0
 
     def paths_between(self, source_id: NodeIdLike, target_id: NodeIdLike) -> list[tuple[Successor, ...]]:
diff --git a/pyk/src/pyk/proof/reachability.py b/pyk/src/pyk/proof/reachability.py
index 2a62fe37f5b..58c9bb24df0 100644
--- a/pyk/src/pyk/proof/reachability.py
+++ b/pyk/src/pyk/proof/reachability.py
@@ -167,7 +167,8 @@ def get_steps(self) -> list[APRProofStep]:
                     else:
                         shortest_path.append(succ.source)
 
-            module_name = self.circularities_module_name if self.nonzero_depth(node) else self.dependencies_module_name
+            nonzero_depth = self.nonzero_depth(node)
+            module_name = self.circularities_module_name if nonzero_depth else self.dependencies_module_name
 
             steps.append(
                 APRProofStep(
@@ -179,7 +180,7 @@ def get_steps(self) -> list[APRProofStep]:
                     shortest_path_to_node=tuple(shortest_path),
                     prior_loops_cache=FrozenDict(self.prior_loops_cache),
                     circularity=self.circularity,
-                    nonzero_depth=self.nonzero_depth(node),
+                    nonzero_depth=nonzero_depth,
                     circularity_rule_id=f'{self.rule_id}-{self.init}-TO-{self.target}',
                 )
             )