pyk: add node_id to custom_step (#4907)

This PR adds a new parameter that is passed to custom steps in pyk.
Specifically, the `node_id` is passed so that it can be used in
downstream custom steps.

This is required for a downstream PR in kontrol
(runtimeverification/kontrol#1131) that adds the
node id to console log cheatcode logging, which is implemented by means
of a custom step.

This PR will require adjustments in some downstream dependencies as well
such as kevm. However, not all downstream dependencies make use of
custom steps such as, e.g., wasm-semantics and komet.

Author: juliankuners

pyk/src/pyk/kcfg/explore.py

@@ -220,7 +220,7 @@ def extend_cterm(
         module_name: str | None = None,
     ) -> list[KCFGExtendResult]:
 
-        custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic)
+        custom_step_result = self.kcfg_semantics.custom_step(_cterm, self.cterm_symbolic, node_id)
         if custom_step_result is not None:
             return [custom_step_result]
 

pyk/src/pyk/kcfg/semantics.py

@@ -35,9 +35,18 @@ def can_make_custom_step(self, c: CTerm) -> bool: ...
     """Check whether or not the semantics can make a custom step from a given ``CTerm``."""
 
     @abstractmethod
-    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None: ...
-
-    """Implement a custom semantic step."""
+    def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: ...
+
+    """Implement a custom semantic step.
+    
+    Args:
+        c: Current constrained term representing the state.
+        cs: ``CTermSymbolic`` for computing the custom step result.
+        node_id: Current node id.
+    
+    Returns:
+        The ``KCFGExtendResult`` produced by this custom step if this custom step can produce one, ``None`` otherwise.
+    """
 
     @abstractmethod
     def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ...
@@ -61,7 +70,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
     def can_make_custom_step(self, c: CTerm) -> bool:
         return False
 
-    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None:
         return None
 
     def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool:

pyk/src/tests/integration/proof/test_custom_step.py

@@ -70,7 +70,7 @@ def can_make_custom_step(self, c: CTerm) -> bool:
             and k_cell[0].label.name == 'c_CUSTOM-STEP-SYNTAX_Step'
         )
 
-    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None:
         if self.can_make_custom_step(c):
             new_cterm = CTerm.from_kast(set_cell(c.kast, 'K_CELL', KSequence(KApply('d_CUSTOM-STEP-SYNTAX_Step'))))
             return Step(new_cterm, 1, (), ['CUSTOM-STEP.c.d'], cut=True)
@@ -153,7 +153,7 @@ def test_custom_step_exec(
 
         # When
         kcfg_semantics = CustomStepSemanticsWithStep()
-        actual = kcfg_semantics.custom_step(cterm, cterm_symbolic)
+        actual = kcfg_semantics.custom_step(cterm, cterm_symbolic, node_id=0)
         # Then
         assert expected == actual
 

pyk/src/tests/integration/proof/test_prove_rpc.py

@@ -71,7 +71,7 @@ def same_loop(self, c1: CTerm, c2: CTerm) -> bool:
     def can_make_custom_step(self, c: CTerm) -> bool:
         return False
 
-    def custom_step(self, c: CTerm, cs: CTermSymbolic) -> KCFGExtendResult | None:
+    def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None:
         return None