Move the exception handling logic from K to kevm-pyk

kevm-pyk/src/kevm_pyk/gst_to_kore.py

@@ -37,6 +37,7 @@
         'transactionSequence',
         'chainname',
         'lastblockhash',
+        'expectException',
         'hasBigInt',
         'config',
     ]

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md

@@ -366,20 +366,11 @@ Processing SetCode Transaction Authority Entries
     syntax Mode ::= "SUCCESS"
  // -------------------------
 
-    syntax EthereumCommand ::= "exception" | "status" StatusCode
- // ------------------------------------------------------------
+    syntax EthereumCommand ::= "exception"
+ // --------------------------------------
     rule <statusCode> _:ExceptionalStatusCode </statusCode>
          <k> #halt ~> exception => .K ... </k>
 
-    rule <statusCode> _:ExceptionalStatusCode </statusCode>
-         <k> exception ~> check _ => exception ... </k>
-
-    rule <statusCode> _:ExceptionalStatusCode </statusCode>
-         <k> exception ~> run TEST => run TEST ~> exception ... </k>
-
-    rule <statusCode> _:ExceptionalStatusCode </statusCode>
-         <k> exception ~> clear => clear ... </k>
-
     syntax EthereumCommand ::= "failure" String | "success"
  // -------------------------------------------------------
     rule <k> success => .K ... </k>
@@ -440,15 +431,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
 
     syntax EthereumCommand ::= "process" JSON
  // -----------------------------------------
-    rule <k> process  TESTID : { "expectException" : _ , REST } => exception ~> process  TESTID : { REST } ... </k>
-
-    rule <k> exception ~> process _TESTID : { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
-    rule <k> exception ~> process _TESTID : { "rlp_decoded" : { .JSONs } , REST   => REST}                                    ... </k>
-
-    rule <k> exception ~> process  TESTID : { KEY : VAL , REST } => load KEY : VAL ~> exception ~> process TESTID : { REST }             ... </k> requires KEY in #loadKeys
-    rule <k> exception ~> process  TESTID : { KEY : VAL , REST } => exception ~> process TESTID : { REST } ~> check TESTID : {KEY : VAL} ... </k> requires KEY in #checkKeys
-    rule <k> exception ~> process _TESTID : { .JSONs }           => #startBlock ~> startTx ~> exception ... </k>
-
     rule <k> process _TESTID : { "rlp_decoded" : { KEY : VAL , REST1 => REST1 }, (REST2 => KEY : VAL , REST2 ) } ... </k>
     rule <k> process _TESTID : { "rlp_decoded" : { .JSONs } , REST => REST}                                      ... </k>
 
@@ -484,7 +466,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     syntax Set ::= "#postKeys" [function] | "#allPostKeys" [function] | "#checkKeys" [function]
  // -------------------------------------------------------------------------------------------
     rule #postKeys    => ( SetItem("post") SetItem("postState") SetItem("postStateHash") )
-    rule #allPostKeys => ( #postKeys SetItem("expect") SetItem("export") SetItem("expet") )
+    rule #allPostKeys => ( #postKeys SetItem("expect") SetItem("export") )
     rule #checkKeys   => ( #allPostKeys SetItem("logs") SetItem("out") SetItem("gas")
                            SetItem("blockHeader") SetItem("transactions") SetItem("uncleHeaders")
                            SetItem("genesisBlockHeader") SetItem("withdrawals") SetItem("blocknumber")

kevm-pyk/src/tests/utils.py

@@ -7,9 +7,9 @@
 from typing import TYPE_CHECKING
 
 import pytest
-from pyk.kdist import kdist
+from pyk.kdist._kdist import kdist
 from pyk.kore.prelude import int_dv
-from pyk.kore.syntax import App
+from pyk.kore.syntax import App, SortApp, SymbolId
 from pyk.kore.tools import PrintOutput, kore_print
 
 from kevm_pyk.interpreter import interpret
@@ -27,8 +27,11 @@
 REPO_ROOT: Final = Path(__file__).parents[3].resolve(strict=True)
 GOLDEN: Final = (REPO_ROOT / 'tests/templates/output-success-llvm.json').read_text().rstrip()
 
+DOT_STATUS_CODE: Final = App(SymbolId("Lbl'Stop'StatusCode'Unds'NETWORK'Unds'StatusCode"))
+SORT_EXCEPTIONAL_STATUS_CODE: Final = SortApp('SortExceptionalStatusCode')
 
-def _assert_exit_code_zero(pattern: Pattern) -> None:
+
+def _assert_exit_code_zero(pattern: Pattern, exception_expected: bool = False) -> None:
     assert type(pattern) is App
     kevm_cell = pattern.args[0]
     assert type(kevm_cell) is App
@@ -38,11 +41,34 @@ def _assert_exit_code_zero(pattern: Pattern) -> None:
     exit_code = exit_code_cell.args[0]
     if exit_code == int_dv(0):
         return
-
+    elif exception_expected:
+        _assert_exit_code_exception(kevm_cell)
+        return
     pretty = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY)
     assert pretty == GOLDEN
 
 
+def _assert_exit_code_exception(kevm_cell: App) -> None:
+    """Assert that the status code in a kevm_cell has the ExceptionalStatusCode sort."""
+    status_code = _fetch_status_code(kevm_cell)
+    # Some tests that are expected to fail might get stuck somewhere not related to the exception.
+    # This assert should catch any false negatives
+    assert status_code != DOT_STATUS_CODE
+    status_code_sort = status_code.sorts[0]
+    assert status_code_sort == SORT_EXCEPTIONAL_STATUS_CODE
+
+
+def _fetch_status_code(kevm_cell: App) -> App:
+    """Return the value of the "<statusCode>" cell in a kevm_cell:App."""
+    # <statusCode> is nested under <kevm><ethereum><evm>
+    ethereum_cell = kevm_cell.args[5]  # type: ignore[attr-defined]
+    evm_cell = ethereum_cell.args[0]  # type: ignore[attr-defined]
+    status_code_cell = evm_cell.args[1]  # type: ignore[attr-defined]
+    status_code = status_code_cell.args[0]  # type: ignore[attr-defined]
+    assert type(status_code) is App
+    return status_code
+
+
 def _skipped_tests(test_dir: Path, slow_tests_file: Path, failing_tests_file: Path) -> dict[Path, list[str]]:
     try:
         slow_tests = read_csv_file(slow_tests_file)
@@ -63,6 +89,19 @@ def read_csv_file(csv_file: Path) -> tuple[tuple[Path, str], ...]:
         return tuple((Path(row[0]), row[1]) for row in reader)
 
 
+def has_exception(gst_data: dict) -> tuple[bool, bool]:
+    """Parse the "blocks" field of a General State Test and check if the "expectException"
+    and "hasBigInt" fields are inside."""
+    exception_expected = False
+    has_big_int = False
+    for block in gst_data.get('blocks', []):
+        exception_expected = exception_expected or 'expectException' in block
+        has_big_int = has_big_int or 'hasBigInt' in block
+        if exception_expected and has_big_int:
+            break
+    return (exception_expected, has_big_int)
+
+
 def _test(
     gst_file: Path,
     *,
@@ -79,34 +118,45 @@ def _test(
     if '*' in skipped_gst_tests:
         pytest.skip()
 
-    failing_tests: list[str] = []
     gst_file_relative_path: Final[str] = str(gst_file.relative_to(test_dir))
 
+    chain_id = compute_chain_id(gst_file_relative_path)
+
     with gst_file.open() as f:
         gst_data = json.load(f)
 
-    for test_name, test in gst_data.items():
+    tests_to_run = {k: v for k, v in gst_data.items() if k not in skipped_gst_tests}
+    failing_tests: list[str] = []
+
+    for test_name, test in tests_to_run.items():
         _LOGGER.info(f'Running test: {gst_file} - {test_name}')
-        if test_name in skipped_gst_tests:
+
+        (exception_expected, has_big_int) = has_exception(test)
+        try:
+            res = interpret({test_name: test}, schedule, mode, chain_id, usegas, check=False)
+        except RuntimeError:
+            if not has_big_int:
+                if not save_failing:
+                    raise
+                failing_tests.append(test_name)
             continue
-        chain_id = compute_chain_id(gst_file_relative_path)
-        res = interpret({test_name: test}, schedule, mode, chain_id, usegas, check=False)
 
         try:
-            _assert_exit_code_zero(res)
+            _assert_exit_code_zero(res, exception_expected)
         except AssertionError:
             if not save_failing:
                 raise
             failing_tests.append(test_name)
 
     if not failing_tests:
         return
-    if save_failing:
-        with failing_tests_file.open('a', newline='') as ff:
-            writer = csv.writer(ff)
-            if len(failing_tests) == len(gst_data):
-                writer.writerow([gst_file_relative_path, '*'])
-            else:
-                for test_name in sorted(failing_tests):
-                    writer.writerow([gst_file_relative_path, test_name])
+
+    with failing_tests_file.open('a', newline='') as ff:
+        writer = csv.writer(ff)
+        if len(failing_tests) == len(gst_data):
+            writer.writerow([gst_file_relative_path, '*'])
+        else:
+            for test_name in sorted(failing_tests):
+                writer.writerow([gst_file_relative_path, test_name])
+
     raise AssertionError(f'Found failing tests in GST file {gst_file_relative_path}: {failing_tests}')

tests/execution-spec-tests/failing.llvm

@@ -322,6 +322,7 @@ blockchain_tests/prague/eip7251_consolidations/consolidations_during_fork/consol
 blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requests.json,tests/prague/eip7251_consolidations/test_consolidations.py::test_consolidation_requests[fork_Prague-blockchain_test-multiple_block_fee_increments]
 blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requests.json,tests/prague/eip7251_consolidations/test_consolidations.py::test_consolidation_requests[fork_Prague-blockchain_test-single_block_multiple_consolidation_request_last_oog]
 blockchain_tests/prague/eip7251_consolidations/contract_deployment/system_contract_deployment.json,*
+blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,*
 blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_from_account_with_non_delegating_code.json,*
 blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/valid_tx_invalid_auth_signature.json,*
 state_tests/berlin/eip2930_access_list/acl/access_list.json,*

tests/failing.llvm

@@ -9,9 +9,9 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/precompile_during
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/reject_valid_full_blob_in_block_rlp.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/create_selfdestruct_same_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/recreate_self_destructed_contract_different_txs.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_created_same_block_different_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/self_destructing_initcode_create_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/self_destructing_initcode.json,*
+BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_created_same_block_different_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/selfdestruct_pre_existing.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip7516_blobgasfee/blobbasefee_before_fork.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip7516_blobgasfee/blobbasefee_during_fork.json,*