Update loadTx rules in driver.md (#2692)

* throw EVMC_OUT_OF_GAS when src account is not in accounts * fix loadTx for invalid init code * add hasBigInt as discardKey
runtimeverification · Jan 23, 2025 · f7435ba · f7435ba
1 parent 903e131
commit f7435ba
Show file tree

Hide file tree

Showing 3 changed files with 8 additions and 10 deletions.
diff --git a/kevm-pyk/src/kevm_pyk/gst_to_kore.py b/kevm-pyk/src/kevm_pyk/gst_to_kore.py
@@ -37,6 +37,7 @@
         'transactionSequence',
         'chainname',
         'lastblockhash',
+        'hasBigInt',
     ]
 )
 _GST_LOAD_KEYS: Final = frozenset(

diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
@@ -83,9 +83,10 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
 
     syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)]
  // --------------------------------------------------------------
-    rule <k> loadTx(_) => #end EVMC_OUT_OF_GAS ... </k>
+    rule <k> loadTx(_) => startTx ... </k>
+         <statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
+         <txPending> ListItem(TXID:Int) REST => REST </txPending>
          <schedule> SCHED </schedule>
-         <txPending> ListItem(TXID:Int) ... </txPending>
          <message>
            <msgID>      TXID     </msgID>
            <to>         .Account </to>
@@ -176,6 +177,10 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
          </account>
       requires notBool ACCTCODE ==K .Bytes
 
+    rule <k> loadTx(_) => startTx ... </k>
+         <statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
+         <txPending> ListItem(_TXID:Int) REST => REST </txPending> [owise]
+
     syntax EthereumCommand ::= "#finishTx"
  // --------------------------------------
     rule <statusCode> _:ExceptionalStatusCode </statusCode> <k> #halt ~> #finishTx => #popCallStack ~> #popWorldState                   ... </k>

diff --git a/tests/failing.llvm b/tests/failing.llvm
@@ -132,8 +132,6 @@ BlockchainTests/GeneralStateTests/Pyspecs/constantinople/eip1014_create2/recreat
 BlockchainTests/GeneralStateTests/Pyspecs/frontier/opcodes/all_opcodes.json,src/GeneralStateTestsFiller/Pyspecs/frontier/opcodes/test_all_opcodes.py::test_all_opcodes[fork_Cancun-blockchain_test]
 BlockchainTests/GeneralStateTests/Pyspecs/frontier/opcodes/double_kill.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/paris/security/tx_selfdestruct_balance_bug.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip3860_initcode/contract_creating_tx.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Cancun-blockchain_test-over_limit_ones]
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip3860_initcode/contract_creating_tx.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Cancun-blockchain_test-over_limit_zeros]
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/balance_within_block.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/large_amount.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/many_withdrawals.json,*
@@ -145,7 +143,6 @@ BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/use_value
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/use_value_in_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/withdrawing_to_precompiles.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/zero_amount.json,*
-BlockchainTests/GeneralStateTests/Shanghai/stEIP3860-limitmeterinitcode/creationTxInitCodeSizeLimit.json,creationTxInitCodeSizeLimit_d1g0v0_Cancun
 BlockchainTests/GeneralStateTests/stBadOpcode/opc49DiffPlaces.json,*
 BlockchainTests/GeneralStateTests/stBadOpcode/opc4ADiffPlaces.json,*
 BlockchainTests/GeneralStateTests/stBadOpcode/undefinedOpcodeFirstByte.json,*
@@ -183,8 +180,3 @@ BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.j
 BlockchainTests/GeneralStateTests/stRevertTest/RevertInCreateInInit_Paris.json,*
 BlockchainTests/GeneralStateTests/stSpecialTest/failed_tx_xcf416c53_Paris.json,*
 BlockchainTests/GeneralStateTests/stSStoreTest/InitCollisionParis.json,*
-BlockchainTests/GeneralStateTests/stTransactionTest/NoSrcAccount1559.json,*
-BlockchainTests/GeneralStateTests/stTransactionTest/NoSrcAccountCreate1559.json,*
-BlockchainTests/GeneralStateTests/stTransactionTest/NoSrcAccountCreate.json,*
-BlockchainTests/GeneralStateTests/stTransactionTest/NoSrcAccount.json,*
-BlockchainTests/GeneralStateTests/stTransactionTest/ValueOverflowParis.json,*