Updates to the driver.md GST handler (#2682)

* sort failing.llvm

* skip intrinsincally invalid blocks

* regen failing.llvm

* driver.md updates

* preserve failing.llvm initial order

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

Co-authored-by: Everett Hildenbrandt <[email protected]>

* regen failing.llvm

---------

Co-authored-by: Everett Hildenbrandt <[email protected]>

Author: anvacaru

kevm-pyk/src/kevm_pyk/gst_to_kore.py

@@ -36,7 +36,6 @@
         'sealEngine',
         'transactionSequence',
         'chainname',
-        'expectException',
         'lastblockhash',
     ]
 )
@@ -79,15 +78,21 @@
 
 
 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()
-    }
+    Filters the discarded keys out of a single GeneralStateTest,
+    recursively removing them from nested dicts/lists as well.
+    """
+
+    def _remove_discard_keys(obj: Any) -> Any:
+        if type(obj) is dict:
+            return {k: _remove_discard_keys(v) for k, v in obj.items() if k not in _GST_DISCARD_KEYS}
+        elif type(obj) is list:
+            return [_remove_discard_keys(item) for item in obj]
+        else:
+            # If it's neither dict nor list, just return as-is
+            return obj
+
+    return _remove_discard_keys(gst_data)
 
 
 def gst_to_kore(gst_data: Any, schedule: str, mode: str, chainid: int, usegas: bool) -> App:

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

@@ -97,6 +97,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
           ~> #loadAccessList(TA)
+          ~> #checkCreate ACCTFROM VALUE
           ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
           ~> #finishTx ~> #finalizeTx(false) ~> startTx
          ...
@@ -121,15 +122,18 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <acctID> ACCTFROM </acctID>
            <balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
            <nonce> NONCE </nonce>
+           <code> ACCTCODE </code>
            ...
          </account>
          <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires #hasValidInitCode(lengthBytes(CODE), SCHED)
+        andBool ACCTCODE ==K .Bytes
 
     rule <k> loadTx(ACCTFROM)
           => #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
           ~> #loadAccessList(TA)
+          ~> #checkCall ACCTFROM VALUE
           ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
           ~> #finishTx ~> #finalizeTx(false) ~> startTx
          ...
@@ -154,11 +158,23 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
            <acctID> ACCTFROM </acctID>
            <balance> BAL => BAL -Int (GLIMIT *Int #effectiveGasPrice(TXID)) </balance>
            <nonce> NONCE => NONCE +Int 1 </nonce>
+           <code> ACCTCODE </code>
            ...
          </account>
          <accessedAccounts> _ => #if Ghaswarmcoinbase << SCHED >> #then SetItem(MINER) #else .Set #fi </accessedAccounts>
          <touchedAccounts> _ => SetItem(MINER) </touchedAccounts>
       requires ACCTTO =/=K .Account
+        andBool ACCTCODE ==K .Bytes
+
+    rule <k> loadTx(ACCTFROM) => startTx ... </k>
+         <statusCode> _ => EVMC_FAILURE </statusCode>
+         <txPending> ListItem(_TXID:Int) REST => REST </txPending>
+         <account>
+           <acctID> ACCTFROM </acctID>
+           <code> ACCTCODE </code>
+           ...
+         </account>
+      requires notBool ACCTCODE ==K .Bytes
 
     syntax EthereumCommand ::= "#finishTx"
  // --------------------------------------
@@ -231,7 +247,14 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
     rule <statusCode> _:ExceptionalStatusCode </statusCode>
          <k> #halt ~> exception => .K ... </k>
 
-    rule <k> status SC => .K ... </k> <statusCode> SC </statusCode>
+    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"
  // -------------------------------------------------------
@@ -293,6 +316,15 @@ 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>