Filter GST discarded keys in the Python harness (#2679)

* filter discarded keys in the Python harness

* remove unused import

* update kevm-pyk run command

* use frozenset instead of list

kevm-pyk/src/kevm_pyk/__main__.py

@@ -34,7 +34,7 @@
 
 from . import VERSION, config
 from .cli import _create_argument_parser, generate_options, get_argument_type_setter, get_option_string_destination
-from .gst_to_kore import SORT_ETHEREUM_SIMULATION, gst_to_kore, kore_pgm_to_kore
+from .gst_to_kore import SORT_ETHEREUM_SIMULATION, filter_gst_keys, gst_to_kore, kore_pgm_to_kore
 from .kevm import KEVM, KEVMSemantics, kevm_node_printer
 from .kompile import KompileTarget, kevm_kompile
 from .utils import (
@@ -591,7 +591,8 @@ def exec_run(options: RunOptions) -> None:
 
     try:
         json_read = json.loads(options.input_file.read_text())
-        kore_pattern = gst_to_kore(json_read, options.schedule, options.mode, options.chainid, options.usegas)
+        gst_data = filter_gst_keys(json_read)
+        kore_pattern = gst_to_kore(gst_data, options.schedule, options.mode, options.chainid, options.usegas)
     except json.JSONDecodeError:
         pgm_token = KToken(options.input_file.read_text(), KSort('EthereumSimulation'))
         kast_pgm = kevm.parse_token(pgm_token)

kevm-pyk/src/kevm_pyk/gst_to_kore.py

@@ -28,6 +28,67 @@
 SORT_MODE: Final = SortApp('SortMode')
 SORT_ETHEREUM_SIMULATION: Final = SortApp('SortEthereumSimulation')
 
+_GST_DISCARD_KEYS: Final = frozenset(
+    [
+        '//',
+        '_info',
+        'callcreates',
+        'sealEngine',
+        'transactionSequence',
+        'chainname',
+        'expectException',
+        'lastblockhash',
+    ]
+)
+_GST_LOAD_KEYS: Final = frozenset(
+    [
+        'env',
+        'pre',
+        'rlp',
+        'network',
+        'genesisRLP',
+    ]
+)
+_GST_EXEC_KEYS: Final = frozenset(
+    [
+        'exec',
+        'blocks',
+    ]
+)
+_GST_POST_KEYS: Final = frozenset(
+    [
+        'post',
+        'postState',
+        'postStateHash',
+    ]
+)
+_GST_ALL_POST_KEYS: Final = _GST_POST_KEYS.union(['expect', 'export'])
+_GST_CHECK_KEYS: Final = _GST_ALL_POST_KEYS.union(
+    [
+        'logs',
+        'out',
+        'gas',
+        'blockHeader',
+        'transactions',
+        'uncleHeaders',
+        'genesisBlockHeader',
+        'withdrawals',
+        'blocknumber',
+    ]
+)
+
+
+def filter_gst_keys(gst_data: dict) -> dict:
+    """Filters the discarded keys out of a single GeneralStateTest.
+
+    :param gst_data: A single test from a GST file structured as {"test_name": {test_fields}, ... }.
+    :returns: The gst_data object after filtering out _GST_DISCARD_KEYS.
+    """
+    return {
+        test_name: {k: v for k, v in test_data.items() if k not in _GST_DISCARD_KEYS}
+        for test_name, test_data in gst_data.items()
+    }
+
 
 def gst_to_kore(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> App:
     return kore_pgm_to_kore(json_to_kore(gst_data), SORT_JSON, schedule, mode, chainid, usegas)

kevm-pyk/src/kevm_pyk/interpreter.py

@@ -6,7 +6,7 @@
 from pyk.kore.parser import KoreParser
 from pyk.utils import run_process_2
 
-from .gst_to_kore import gst_to_kore
+from .gst_to_kore import filter_gst_keys, gst_to_kore
 
 if TYPE_CHECKING:
     from subprocess import CompletedProcess
@@ -26,7 +26,8 @@ def interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: boo
 
 
 def _interpret(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> CompletedProcess:
+    gst_data_filtered = filter_gst_keys(gst_data)
     interpreter = kdist.get('evm-semantics.llvm') / 'interpreter'
-    init_kore = gst_to_kore(gst_data, schedule, mode, chainid, usegas)
+    init_kore = gst_to_kore(gst_data_filtered, schedule, mode, chainid, usegas)
     proc_res = run_process_2([str(interpreter), '/dev/stdin', '-1', '/dev/stdout'], input=init_kore.text, check=False)
     return proc_res

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

@@ -254,7 +254,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
  // -------------------------------------
     rule <k> run { .JSONs } => .K ... </k>
     rule <k> run { TESTID : { TEST:JSONs } , TESTS }
-          => run ( TESTID : { qsortJSONs(TEST) } )
+          => run ( TESTID : { TEST } )
           ~> #if #hasPost?( { TEST } ) #then .K #else exception #fi
           ~> clear
           ~> run { TESTS }
@@ -298,7 +298,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
 
     rule <k> process  TESTID : { KEY : VAL , REST } => load KEY : VAL ~> process TESTID : { REST }             ... </k> requires KEY in #loadKeys
     rule <k> process  TESTID : { KEY : VAL , REST } => process TESTID : { REST } ~> check TESTID : {KEY : VAL} ... </k> requires KEY in #checkKeys
-    rule <k> process _TESTID : { KEY : _   , REST   => REST }                                                  ... </k> requires KEY in #discardKeys
     rule <k> process _TESTID : { .JSONs }           => #startBlock ~> startTx ... </k>
 
     rule <k> run _TESTID : { "exec" : (EXEC:JSON) } => loadCallState EXEC ~> start ~> flush ... </k>
@@ -339,16 +338,6 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
     rule <k> run TESTID : { KEY : (VAL:JSON) , REST } => run TESTID : { REST } ~> check TESTID : { KEY    : VAL } ... </k> requires KEY in #checkKeys andBool notBool KEY in #allPostKeys
 ```
 
--   `#discardKeys` are all the JSON nodes in the tests which should just be ignored.
-
-```k
-    syntax Set ::= "#discardKeys" [function]
- // ----------------------------------------
-    rule #discardKeys => ( SetItem("//") SetItem("_info") SetItem("callcreates") SetItem("sealEngine") SetItem("transactionSequence") SetItem("chainname") SetItem("expectException") SetItem("lastblockhash"))
-
-    rule <k> run TESTID : { KEY : _ , REST } => run TESTID : { REST } ... </k> requires KEY in #discardKeys
-```
-
 -   `driver.md` specific handling of state-utils commands
 
 ```k

kevm-pyk/src/tests/integration/test_conformance.py

@@ -24,8 +24,6 @@
 
 
 _LOGGER: Final = logging.getLogger(__name__)
-_LOG_FORMAT: Final = '%(levelname)s %(asctime)s %(name)s - %(message)s'
-
 
 sys.setrecursionlimit(10**8)