KEVMSemantics: refactor custom_step and can_make_custom_step (#2662)

runtimeverification · Dec 5, 2024 · b40fd7b · b40fd7b
1 parent 622dc98
commit b40fd7b
Showing 1 changed file with 23 additions and 16 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/kevm.py b/kevm-pyk/src/kevm_pyk/kevm.py
@@ -146,21 +146,10 @@ def _replace(term: KInner) -> KInner:
         return CTerm(config=bottom_up(_replace, cterm.config), constraints=cterm.constraints)
 
     def custom_step(self, cterm: CTerm, _cterm_symbolic: CTermSymbolic) -> KCFGExtendResult | None:
-        """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL.
-
-        :param cterm: CTerm of a proof node.
-        :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied. Otherwise, None is returned.
-        """
-        if self.can_make_custom_step(cterm):
-            subst = self._cached_subst
-            assert subst is not None
-            bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
-            jumpdests_set = compute_jumpdests(bytecode_sections)
-            new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set))
-            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'PROGRAM_CELL', subst['###BYTECODE']))
-            new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
-            return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
-        return None
+        if self._check_load_pattern(cterm):
+            return self._exec_load_custom_step(cterm)
+        else:
+            return None
 
     @staticmethod
     def cut_point_rules(
@@ -208,7 +197,7 @@ def terminal_rules(break_every_step: bool) -> list[str]:
             terminal_rules.append('EVM.step')
         return terminal_rules
 
-    def can_make_custom_step(self, cterm: CTerm) -> bool:
+    def _check_load_pattern(self, cterm: CTerm) -> bool:
         """Given a CTerm, check if the rule 'EVM.program.load' is at the top of the K_CELL.
 
         This method checks if the `EVM.program.load` rule is at the top of the `K_CELL` in the given `cterm`.
@@ -220,6 +209,24 @@ def can_make_custom_step(self, cterm: CTerm) -> bool:
         self._cached_subst = load_pattern.match(cterm.cell('K_CELL'))
         return self._cached_subst is not None
 
+    def _exec_load_custom_step(self, cterm: CTerm) -> KCFGExtendResult:
+        """Given a CTerm, update the JUMPDESTS_CELL and PROGRAM_CELL if the rule 'EVM.program.load' is at the top of the K_CELL.
+
+        :param cterm: CTerm of a proof node.
+        :return: If the K_CELL matches the load_pattern, a Step with depth 1 is returned together with the new configuration, also registering that the `EVM.program.load` rule has been applied.
+        """
+        subst = self._cached_subst
+        assert subst is not None
+        bytecode_sections = flatten_label('_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes', subst['###BYTECODE'])
+        jumpdests_set = compute_jumpdests(bytecode_sections)
+        new_cterm = CTerm.from_kast(set_cell(cterm.kast, 'JUMPDESTS_CELL', jumpdests_set))
+        new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'PROGRAM_CELL', subst['###BYTECODE']))
+        new_cterm = CTerm.from_kast(set_cell(new_cterm.kast, 'K_CELL', KSequence(subst['###CONTINUATION'])))
+        return Step(new_cterm, 1, (), ['EVM.program.load'], cut=True)
+
+    def can_make_custom_step(self, cterm: CTerm) -> bool:
+        return self._check_load_pattern(cterm)
+
     def is_mergeable(self, ct1: CTerm, ct2: CTerm) -> bool:
         """Given two CTerms of Edges' targets, check if they are mergeable.