EIP-4895: Beacon chain push withdrawals as operations

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

@@ -403,14 +403,14 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
  // ---------------------------------------
     rule <k> #halt ~> check J:JSON => check J ~> #halt ... </k>
 
-    rule <k> check DATA : { .JSONs } => .K ... </k> requires DATA =/=String "transactions"
-    rule <k> check DATA : [ .JSONs ] => .K ... </k> requires DATA =/=String "ommerHeaders"
+    rule <k> check DATA : { .JSONs } => .K ... </k> requires notBool DATA in (SetItem("transactions") SetItem("withdrawals"))
+    rule <k> check DATA : [ .JSONs ] => .K ... </k> requires notBool DATA in (SetItem("ommerHeaders") SetItem( "transactions") SetItem("withdrawals"))
 
     rule <k> check DATA : { (KEY:String) : VALUE , REST } => check DATA : { KEY : VALUE } ~> check DATA : { REST } ... </k>
-      requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions"))
+      requires REST =/=K .JSONs andBool notBool DATA in (SetItem("callcreates") SetItem("transactions") SetItem("withdrawals"))
 
     rule <k> check DATA : [ { TEST } , REST ] => check DATA : { TEST } ~> check DATA : [ REST ] ... </k>
-      requires DATA =/=String "transactions"
+      requires notBool DATA in (SetItem("transactions") SetItem("withdrawals"))
 
     rule <k> check (KEY:String) : { JS:JSONs => qsortJSONs(JS) } ... </k>
       requires KEY in (SetItem("callcreates")) andBool notBool sortedJSONs(JS)
@@ -628,6 +628,20 @@ TODO: case with nonzero ommers.
 ```k
     rule <k> check TESTID : {"withdrawals" : WITHDRAWALS } => check "withdrawals" : WITHDRAWALS ~> failure TESTID ... </k>
  // ----------------------------------------------------------------------------------------------------------------------
+    rule <k> check "withdrawals" : [ .JSONs ] => .K ... </k> <withdrawalsOrder> .List                    </withdrawalsOrder>
+    rule <k> check "withdrawals" : { .JSONs } => .K ... </k> <withdrawalsOrder> ListItem(_) => .List ... </withdrawalsOrder>
+
+    rule <k> check "withdrawals" : [ WITHDRAWAL , REST ]  => check "withdrawals" : WITHDRAWAL    ~> check "withdrawals" : [ REST ] ... </k>
+    rule <k> check "withdrawals" : { KEY : VALUE , REST } => check "withdrawals" : (KEY : VALUE) ~> check "withdrawals" : { REST } ... </k>
+
+    rule <k> check "withdrawals" : (_KEY      : (VALUE:String => #parseByteStack(VALUE))) ... </k>
+    rule <k> check "withdrawals" : ("address" : (VALUE:Bytes  => #asAccount(VALUE)))      ... </k>
+    rule <k> check "withdrawals" : ( KEY      : (VALUE:Bytes  => #asWord(VALUE)))         ... </k> requires KEY =/=String "address"
+
+    rule <k> check "withdrawals" : ("address"        : VALUE ) => .K ... </k> <withdrawalsOrder> ListItem(WID) ... </withdrawalsOrder> <withdrawal> <withdrawalID> WID </withdrawalID> <address>        VALUE </address>        ... </withdrawal>
+    rule <k> check "withdrawals" : ("amount"         : VALUE ) => .K ... </k> <withdrawalsOrder> ListItem(WID) ... </withdrawalsOrder> <withdrawal> <withdrawalID> WID </withdrawalID> <amount>         VALUE </amount>         ... </withdrawal>
+    rule <k> check "withdrawals" : ("validatorIndex" : VALUE ) => .K ... </k> <withdrawalsOrder> ListItem(WID) ... </withdrawalsOrder> <withdrawal> <withdrawalID> WID </withdrawalID> <validatorIndex> VALUE </validatorIndex> ... </withdrawal>
+    rule <k> check "withdrawals" : ("index"          : VALUE ) => .K ... </k> <withdrawalsOrder> ListItem(WID) ... </withdrawalsOrder> <withdrawal> <withdrawalID> WID </withdrawalID> <index>          VALUE </index>          ... </withdrawal>
 ```
 
 ```k

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

@@ -170,6 +170,22 @@ In the comments next to each cell, we've marked which component of the YellowPap
               </message>
             </messages>
 
+            // Withdrawals Record
+            // ------------------
+
+            <withdrawalsPending> .List </withdrawalsPending>
+            <withdrawalsOrder>   .List </withdrawalsOrder>
+
+            <withdrawals>
+              <withdrawal multiplicity="*" type="Map">
+                <withdrawalID>   0        </withdrawalID>
+                <index>          0        </index>
+                <validatorIndex> 0        </validatorIndex>
+                <address>        .Account </address>
+                <amount>         0        </amount>
+              </withdrawal>
+            </withdrawals>
+
           </network>
 
         </ethereum>
@@ -359,7 +375,7 @@ The `#next [_]` operator initiates execution by:
 ```k
     syntax Bool ::= #stackUnderflow ( WordStack , OpCode ) [symbol(#stackUnderflow), macro]
                   | #stackOverflow  ( WordStack , OpCode ) [symbol(#stackOverflow), macro]
- // ---------------------------------------------------------------------------------------
+ // --------------------------------------------------------------------------------------
     rule #stackUnderflow(WS, OP:OpCode) => #sizeWordStack(WS) <Int #stackNeeded(OP)
     rule #stackOverflow (WS, OP) => #sizeWordStack(WS) +Int #stackDelta(OP) >Int 1024
 
@@ -533,8 +549,36 @@ After executing a transaction, it's necessary to have the effect of the substate
 -   `#finalizeStorage` updates the origStorage cell with the new values of storage.
 -   `#finalizeTx` makes the substate log actually have an effect on the state.
 -   `#deleteAccounts` deletes the accounts specified by the self destruct list.
-
+-   `#finalizeWithdrawals` increases the balance of the `address` specified by the `amount` given, for each withdrawal.
 ```k
+
+    syntax InternalOp ::= "#finalizeWithdrawals" [symbol(#finalizeWithdrawals)]
+ // ---------------------------------------------------------------------------
+    rule <k> #finalizeWithdrawals => .K ... </k>
+         <withdrawalsPending> .List </withdrawalsPending>
+
+    rule <k> #finalizeWithdrawals ... </k>
+         <withdrawalsPending> ListItem(WDID) LS => LS </withdrawalsPending>
+         <withdrawal>
+           <withdrawalID> WDID </withdrawalID>
+           <address> ACCT </address>
+           <amount> VALUE </amount>
+           ...
+         </withdrawal>
+         <account>
+           <acctID> ACCT </acctID>
+           <balance> B => B +Int (VALUE *Int 10 ^Int 9) </balance>
+           ...
+         </account>
+
+    rule <k> (.K => #newAccount ACCT) ~> #finalizeWithdrawals ... </k>
+         <withdrawalsPending> ListItem(WDID) _ </withdrawalsPending>
+         <withdrawal>
+           <withdrawalID> WDID </withdrawalID>
+           <address> ACCT </address>
+           ...
+         </withdrawal> [owise]
+
     syntax InternalOp ::= #finalizeStorage ( List ) [symbol(#finalizeStorage)]
  // --------------------------------------------------------------------------
     rule <k> #finalizeStorage(ListItem(ACCT) REST => REST) ... </k>
@@ -667,7 +711,7 @@ After executing a transaction, it's necessary to have the effect of the substate
     syntax EthereumCommand ::= "#finalizeBlock"
                              | #rewardOmmers ( JSONs ) [symbol(#rewardOmmers)]
  // --------------------------------------------------------------------------
-    rule <k> #finalizeBlock => #rewardOmmers(OMMERS) ... </k>
+    rule <k> #finalizeBlock => #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi ~> #rewardOmmers(OMMERS) ... </k>
          <schedule> SCHED </schedule>
          <ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
          <coinbase> MINER </coinbase>

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

@@ -28,9 +28,9 @@ module SCHEDULE
                           | "Ghasdirtysstore"         | "Ghascreate2"      | "Ghasextcodehash"     | "Ghasselfbalance"
                           | "Ghassstorestipend"       | "Ghaschainid"      | "Ghasaccesslist"      | "Ghasbasefee"
                           | "Ghasrejectedfirstbyte"   | "Ghasprevrandao"   | "Ghasmaxinitcodesize" | "Ghaspushzero"
-                          | "Ghaswarmcoinbase"        | "Ghastransient"    | "Ghasmcopy"           | "Ghasbeaconroot"
-                          | "Ghaseip6780"
- // -------------------------------------
+                          | "Ghaswarmcoinbase"        | "Ghaswithdrawals"  | "Ghastransient"       | "Ghasmcopy"
+                          | "Ghasbeaconroot"          | "Ghaseip6780"
+ // -----------------------------------------------------------------
 ```
 
 ### Schedule Constants
@@ -147,6 +147,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghasmaxinitcodesize     << DEFAULT >> => false
     rule Ghaspushzero            << DEFAULT >> => false
     rule Ghaswarmcoinbase        << DEFAULT >> => false
+    rule Ghaswithdrawals         << DEFAULT >> => false
     rule Ghastransient           << DEFAULT >> => false
     rule Ghasmcopy               << DEFAULT >> => false
     rule Ghasbeaconroot          << DEFAULT >> => false
@@ -373,10 +374,12 @@ A `ScheduleConst` is a constant determined by the fee schedule.
     rule Ghasmaxinitcodesize << SHANGHAI >> => true
     rule Ghaspushzero        << SHANGHAI >> => true
     rule Ghaswarmcoinbase    << SHANGHAI >> => true
+    rule Ghaswithdrawals     << SHANGHAI >> => true
     rule SCHEDFLAG           << SHANGHAI >> => SCHEDFLAG << MERGE >>
       requires notBool ( SCHEDFLAG ==K Ghasmaxinitcodesize
                   orBool SCHEDFLAG ==K Ghaspushzero
                   orBool SCHEDFLAG ==K Ghaswarmcoinbase
+                  orBool SCHEDFLAG ==K Ghaswithdrawals
                        )
 ```
 

kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md

@@ -83,6 +83,7 @@ module STATE-UTILS
          <statusCode>     _ => .StatusCode </statusCode>
          <accounts>       _ => .Bag        </accounts>
          <messages>       _ => .Bag        </messages>
+         <withdrawals>    _ => .Bag        </withdrawals>
          <schedule>       _ => DEFAULT     </schedule>
 
 ```
@@ -249,6 +250,45 @@ The `"rlp"` key loads the block information.
     rule <k> load "genesisRLP": [ [ HP, HO, HC, HR, HT, HE:Bytes, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, .JSONs ], _, _, .JSONs ] => .K ... </k>
          <blockhashes> .List => ListItem(#blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF)) ListItem(#asWord(HP)) ... </blockhashes>
 
+    syntax Int ::= "#newWithdrawalID" "(" List ")" [function]
+ // ---------------------------------------------------------
+    rule #newWithdrawalID (.List) => 0
+    rule #newWithdrawalID (_ ListItem(I)) => I +Int 1
+
+    syntax EthereumCommand ::= "mkWD" Int
+ // -------------------------------------
+    rule <k> mkWD (WDID => WDID +Int 1) ... </k>
+         <withdrawal> <withdrawalID> WDID </withdrawalID> ... </withdrawal>
+
+    rule <k> mkWD WDID => .K ... </k>
+         <withdrawalsOrder>   ... (.List => ListItem(WDID)) </withdrawalsOrder>
+         <withdrawalsPending> ... (.List => ListItem(WDID)) </withdrawalsPending>
+         <withdrawals>
+            ( .Bag
+           => <withdrawal>
+                <withdrawalID> WDID </withdrawalID>
+                ...
+              </withdrawal>
+            )
+            ...
+          </withdrawals> [owise]
+
+    syntax EthereumCommand ::= "loadWithdraw" JSON
+ // ----------------------------------------------
+    rule <k> loadWithdraw [ INDEX , VALIDATOR , ACCT , VALUE , .JSONs ] => .K ... </k>
+         <withdrawalsOrder> ... ListItem(WID) </withdrawalsOrder>
+         <withdrawal>
+              <withdrawalID>   WID                     </withdrawalID>
+              <index>          _ => #asWord(INDEX)     </index>
+              <validatorIndex> _ => #asWord(VALIDATOR) </validatorIndex>
+              <address>        _ => #asAccount(ACCT)   </address>
+              <amount>         _ => #asWord(VALUE)     </amount>
+         </withdrawal>
+
+    rule <k> load "withdraw" : [ .JSONs ]          => .K ... </k>
+    rule <k> load "withdraw" : [ WITHDRAW , REST ] => mkWD #newWithdrawalID(WIDS) ~> loadWithdraw WITHDRAW ~> load "withdraw" : [ REST ] ... </k>
+         <withdrawalsOrder> WIDS </withdrawalsOrder>
+
     syntax EthereumCommand ::= "mkTX" Int
  // -------------------------------------
     rule <k> mkTX TXID => .K ... </k>

tests/failing.llvm

@@ -10,10 +10,7 @@ BlockchainTests/GeneralStateTests/Cancun/stEIP4844-blobtransactions/opcodeBlobhB
 BlockchainTests/GeneralStateTests/Cancun/stEIP4844-blobtransactions/wrongBlobhashVersion.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tstore_clear_after_deployment_tx.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip1153_tstore/tstore_clear_after_tx.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_contract_deploy.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/beacon_root_transition.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/multi_block_beacon_root_timestamp_calls.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/no_beacon_root_contract_at_transition.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/tx_to_beacon_root_contract.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4788_beacon_root/test_beacon_root_contract.py::test_tx_to_beacon_root_contract[fork_Cancun-tx_type_3-blockchain_test-call_beacon_root_contract_True-auto_access_list_False]
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4788_beacon_root/tx_to_beacon_root_contract.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4788_beacon_root/test_beacon_root_contract.py::test_tx_to_beacon_root_contract[fork_Cancun-tx_type_3-blockchain_test-call_beacon_root_contract_True-auto_access_list_True]
 BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_gas_subtraction_tx.json,*
@@ -134,17 +131,9 @@ 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,*
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/multiple_withdrawals_same_address.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/newly_created_contract.json,*
 BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/no_evm_execution.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/self_destructing_account.json,*
-BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/use_value_in_contract.json,*
-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/Pyspecs/shanghai/eip4895_withdrawals/withdrawing_to_precompiles.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_0x000000000000000000000000000000000000000a-blockchain_test-amount_0]
+BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/withdrawing_to_precompiles.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_0x000000000000000000000000000000000000000a-blockchain_test-amount_1]
 BlockchainTests/GeneralStateTests/Shanghai/stEIP3860-limitmeterinitcode/creationTxInitCodeSizeLimit.json,creationTxInitCodeSizeLimit_d1g0v0_Cancun
 BlockchainTests/GeneralStateTests/stBadOpcode/opc49DiffPlaces.json,*
 BlockchainTests/GeneralStateTests/stBadOpcode/opc4ADiffPlaces.json,*

tests/failing/ContractCreationSpam_d0g0v0.json.expected

@@ -321,6 +321,15 @@
           </txType>
         </message>
       </messages>
+      <withdrawalsPending>
+        .List
+      </withdrawalsPending>
+      <withdrawalsOrder>
+        .List
+      </withdrawalsOrder>
+      <withdrawals>
+        .WithdrawalCellMap
+      </withdrawals>
     </network>
   </ethereum>
 </kevm>

tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

@@ -367,6 +367,15 @@
           </txType>
         </message>
       </messages>
+      <withdrawalsPending>
+        .List
+      </withdrawalsPending>
+      <withdrawalsOrder>
+        .List
+      </withdrawalsOrder>
+      <withdrawals>
+        .WithdrawalCellMap
+      </withdrawals>
     </network>
   </ethereum>
 </kevm>

tests/specs/benchmarks/address00-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/bytes00-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/dynamicarray00-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecover00-siginvalid-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecover00-sigvalid-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop00-sig0-invalid-spec.k

@@ -123,6 +123,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop00-sig1-invalid-spec.k

@@ -123,6 +123,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop00-sigs-valid-spec.k

@@ -123,6 +123,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop02-sig0-invalid-spec.k

@@ -124,6 +124,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop02-sig1-invalid-spec.k

@@ -124,6 +124,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/ecrecoverloop02-sigs-valid-spec.k

@@ -124,6 +124,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/encode-keccak00-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/encodepacked-keccak01-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/keccak00-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/overflow00-nooverflow-spec.k

@@ -119,6 +119,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)

tests/specs/benchmarks/overflow00-overflow-spec.k

@@ -120,6 +120,7 @@ _
         <txOrder> _ </txOrder>
         <txPending> _ </txPending>
         <messages> _ </messages>
+        ...
       </network>
     </ethereum>
     requires #rangeAddress(CONTRACT_ID)