Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

KEVMSemantics: refactor custom_step and can_make_custom_step #2662

Merged
merged 2 commits into from
Dec 5, 2024
Merged
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
39 changes: 23 additions & 16 deletions kevm-pyk/src/kevm_pyk/kevm.py
Original file line number Diff line number Diff line change
Expand Up @@ -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(
Expand Down Expand Up @@ -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`.
Expand All @@ -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.

Expand Down
Loading