Merge remote-tracking branch 'origin/master' into release

.gitignore

@@ -20,3 +20,4 @@
 /tests/vm/*.out
 .DS_Store
 .idea/
+.vscode/

deps/k_release

@@ -1 +1 @@
-7.1.145
+7.1.149

flake.nix

@@ -2,7 +2,7 @@
  description = "A flake for the KEVM Semantics";
 
  inputs = {
- k-framework.url = "github:runtimeverification/k/v7.1.145";
+ k-framework.url = "github:runtimeverification/k/v7.1.149";
  nixpkgs.follows = "k-framework/nixpkgs";
  flake-utils.follows = "k-framework/flake-utils";
  rv-utils.follows = "k-framework/rv-utils";

kevm-pyk/pyproject.toml

@@ -13,7 +13,7 @@ authors = [
 [tool.poetry.dependencies]
 python = "^3.10"
 pathos = "*"
-kframework = "7.1.145"
+kframework = "7.1.149"
 tomlkit = "^0.11.6"
 
 [tool.poetry.group.dev.dependencies]

kevm-pyk/src/kevm_pyk/kevm.py

@@ -225,6 +225,29 @@ 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 is_mergeable(self, ct1: CTerm, ct2: CTerm) -> bool:
+ """Given two CTerms of Edges' targets, check if they are mergeable.
+
+ Two CTerms are mergeable if their `STATUSCODE_CELL` and `PROGRAM_CELL` are the same.
+ If mergeable, the two corresponding Edges are merged into one.
+
+ :param ct1: CTerm of one Edge's target.
+ :param ct2: CTerm of another Edge's target.
+ :return: `True` if the two CTerms are mergeable; `False` otherwise.
+ """
+ status_code_1 = ct1.cell('STATUSCODE_CELL')
+ status_code_2 = ct2.cell('STATUSCODE_CELL')
+ program_1 = ct1.cell('PROGRAM_CELL')
+ program_2 = ct2.cell('PROGRAM_CELL')
+ if (
+ type(status_code_1) is KApply
+ and type(status_code_2) is KApply
+ and type(program_1) is KToken
+ and type(program_2) is KToken
+ ):
+ return status_code_1 == status_code_2 and program_1 == program_2
+ raise ValueError(f'Attempted to merge nodes with non-concrete <statusCode> or <program>: {(ct1, ct2)}')
+
 
 class KEVM(KProve, KRun):
  _use_hex: bool

kevm-pyk/src/tests/unit/test_kevm.py

@@ -8,10 +8,11 @@
  from typing import Final
  from pyk.kast.inner import KInner
 
+from pyk.cterm.cterm import CTerm
 from pyk.kast.inner import KApply, KToken, KVariable
 from pyk.prelude.utils import token
 
-from kevm_pyk.kevm import KEVM, compute_jumpdests
+from kevm_pyk.kevm import KEVM, KEVMSemantics, compute_jumpdests
 
 TEST_DATA: Final = [
  ('single-ktoken', token(0), KToken('0x0', 'Int')),
@@ -108,3 +109,109 @@ def test_process_jumpdests(test_id: str, input: list[KInner], expected: KInner)
 
  # Then
  assert result == expected
+
+
+IS_MERGEABLE_DATA: Final = [
+ (
+ 'mergeable_total_same',
+ [
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_SUCCESS')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_SUCCESS')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ ],
+ True,
+ False,
+ ),
+ (
+ 'mergeable_not_care_others',
+ [
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_SUCCESS')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ KApply('<callStack>', token(b'\x00')),
+ )
+ ),
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_SUCCESS')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ KApply('<callStack>', token(b'\x01')),
+ )
+ ),
+ ],
+ True,
+ False,
+ ),
+ (
+ 'not_mergeable',
+ [
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_SUCCESS')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KApply('EVMC_REVERT')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ ],
+ False,
+ True,
+ ),
+ (
+ 'raise_error',
+ [
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KToken('EVMC_SUCCESS', 'StatusCode')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ CTerm(
+ KApply(
+ '<generatedTop>',
+ KApply('<statusCode>', KToken('EVMC_SUCCESS', 'StatusCode')),
+ KApply('<program>', token(b'\xcc\xff\xff\xfac\x60\xf5')),
+ )
+ ),
+ ],
+ False,
+ True,
+ ),
+]
+
+
+@pytest.mark.parametrize(
+ 'test_id,input,expected,raise_error',
+ IS_MERGEABLE_DATA,
+ ids=[test_id for test_id, *_ in IS_MERGEABLE_DATA],
+)
+def test_is_mergeable(test_id: str, input: list[CTerm], expected: KInner, raise_error: bool) -> None:
+ # When
+ try:
+ result = KEVMSemantics().is_mergeable(input[0], input[1])
+ except ValueError:
+ assert raise_error
+ return
+ # Then
+ assert result == expected