From 985f1a0e53cfc5ba65b7607bd6b733aa7b2a79b9 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Wed, 8 Apr 2026 10:40:35 +0200 Subject: [PATCH 1/4] pyk: add `node_id` to `custom_step` --- pyk/src/pyk/kcfg/explore.py | 2 +- pyk/src/pyk/kcfg/semantics.py | 4 ++-- pyk/src/tests/integration/proof/test_custom_step.py | 4 ++-- pyk/src/tests/integration/proof/test_prove_rpc.py | 2 +- 4 files changed, 6 insertions(+), 6 deletions(-) diff --git a/pyk/src/pyk/kcfg/explore.py b/pyk/src/pyk/kcfg/explore.py index f1d06cc3eab..5562132e3e2 100644 --- a/pyk/src/pyk/kcfg/explore.py +++ b/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] diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index 89569e300e7..d658ed13071 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -35,7 +35,7 @@ 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: ... + def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: ... """Implement a custom semantic step.""" @@ -61,7 +61,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: diff --git a/pyk/src/tests/integration/proof/test_custom_step.py b/pyk/src/tests/integration/proof/test_custom_step.py index 141f95b3a1a..4330c21ae50 100644 --- a/pyk/src/tests/integration/proof/test_custom_step.py +++ b/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 diff --git a/pyk/src/tests/integration/proof/test_prove_rpc.py b/pyk/src/tests/integration/proof/test_prove_rpc.py index 5ffbfc449ea..bdb90314bea 100644 --- a/pyk/src/tests/integration/proof/test_prove_rpc.py +++ b/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 From 67cd7216b93196157189bb788b0b1558377350ad Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Wed, 8 Apr 2026 13:45:59 +0200 Subject: [PATCH 2/4] empty commit From d0cb81b9ea208b461c41305710ed8169f045ff28 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Thu, 9 Apr 2026 10:18:21 +0200 Subject: [PATCH 3/4] add docstring to `custom_step` --- pyk/src/pyk/kcfg/semantics.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index d658ed13071..c1d037ba718 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -37,7 +37,16 @@ def can_make_custom_step(self, c: CTerm) -> bool: ... @abstractmethod def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendResult | None: ... - """Implement a custom semantic step.""" + """Implement a custom semantic step. + + Args: + c: Current configuration term representing the EVM state. + cs: Symbolic configuration term. + node_id: Current node id. + + Returns: + The KCFGExtendResult produced by this custom step if this custom step can produce one, otherwise returns None, + """ @abstractmethod def is_mergeable(self, c1: CTerm, c2: CTerm) -> bool: ... From 9e7cae7b06b3e670e5c70da15ea6dab8a98075b2 Mon Sep 17 00:00:00 2001 From: Julian Kuners Date: Thu, 9 Apr 2026 10:41:26 +0200 Subject: [PATCH 4/4] address requested docstring changes --- pyk/src/pyk/kcfg/semantics.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/pyk/src/pyk/kcfg/semantics.py b/pyk/src/pyk/kcfg/semantics.py index c1d037ba718..4f356565710 100644 --- a/pyk/src/pyk/kcfg/semantics.py +++ b/pyk/src/pyk/kcfg/semantics.py @@ -40,12 +40,12 @@ def custom_step(self, c: CTerm, cs: CTermSymbolic, node_id: int) -> KCFGExtendRe """Implement a custom semantic step. Args: - c: Current configuration term representing the EVM state. - cs: Symbolic configuration term. + 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, otherwise returns None, + The ``KCFGExtendResult`` produced by this custom step if this custom step can produce one, ``None`` otherwise. """ @abstractmethod