Update dependency: deps/k_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