APRProof get_steps optimizations (#4585)

- 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ć <[email protected]>

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, ...]]:

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}',
                 )
             )