From 001dc2e7dc15754d49cf9a8fe85d5ef18e217b1a Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 2 May 2025 13:30:10 +0300 Subject: [PATCH 1/8] define SetCode transaction --- .../src/kevm_pyk/kproj/evm-semantics/evm-types.md | 13 ++++++++----- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 1 + .../kevm_pyk/kproj/evm-semantics/serialization.md | 6 +++++- 3 files changed, 14 insertions(+), 6 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index b401b2f2a4..c1bd8d7d49 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -449,7 +449,8 @@ Productions related to transactions | "AccessList" | "DynamicFee" | "Blob" - // ------------------------ + | "SetCode" + // --------------------------- syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function] // ------------------------------------------------------------------------- @@ -457,6 +458,7 @@ Productions related to transactions rule #dasmTxPrefix (AccessList) => 1 rule #dasmTxPrefix (DynamicFee) => 2 rule #dasmTxPrefix (Blob) => 3 + rule #dasmTxPrefix (SetCode) => 4 syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function] // ----------------------------------------------------------------------- @@ -464,16 +466,17 @@ Productions related to transactions rule #asmTxPrefix (1) => AccessList rule #asmTxPrefix (2) => DynamicFee rule #asmTxPrefix (3) => Blob + rule #asmTxPrefix (4) => SetCode - syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx - // ----------------------------------------------------------------- + syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx | SetCodeTx + // ----------------------------------------------------------------------------- syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)] | LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)] syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: List ) [symbol(BlobTxData)] - // --------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- - + syntax SetCodeTx ::= SetCodeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, authorizationList: JSONs) [symbol(SetCodeTxData)] + // ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ endmodule ``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index b2fd55a98f..2a3fc95d3c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -171,6 +171,7 @@ In the comments next to each cell, we've marked which component of the YellowPap .TxType // T_x 0 .List + .List diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 2884d5e99d..7c2e18d735 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -194,7 +194,8 @@ The encoding schemes are applied in `#rlpEcondeTxData`. rule #hashTxData( TXDATA ) => Keccak256raw( b"\x01" +Bytes #rlpEncodeTxData(TXDATA) ) requires isAccessListTx(TXDATA) rule #hashTxData( TXDATA ) => Keccak256raw( b"\x02" +Bytes #rlpEncodeTxData(TXDATA) ) requires isDynamicFeeTx(TXDATA) rule #hashTxData( TXDATA ) => Keccak256raw( b"\x03" +Bytes #rlpEncodeTxData(TXDATA) ) requires isBlobTx (TXDATA) -``` + rule #hashTxData( TXDATA ) => Keccak256raw( b"\x04" +Bytes #rlpEncodeTxData(TXDATA) ) requires isSetCodeTx (TXDATA) +``` The EVM test-sets are represented in JSON format with hex-encoding of the data and programs. Here we provide some standard parser/unparser functions for that format. @@ -413,6 +414,9 @@ Encoding rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [#parseList2JSONs(TVH)] ] ) + rule #rlpEncodeTxData( SetCodeTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], [TAUTH]) ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], [TAUTH]] ) + syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- rule #rlpEncodeMerkleTree ( .MerkleTree ) => b"\x80" From 357a1f706e10dea3cc69e6ae5203a59ca30cfcc2 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Sun, 4 May 2025 08:42:40 +0300 Subject: [PATCH 2/8] parse SetCode tx from JSON fixture files --- .../kevm_pyk/kproj/evm-semantics/driver.md | 15 ++++++++ .../kevm_pyk/kproj/evm-semantics/evm-types.md | 2 +- .../kproj/evm-semantics/serialization.md | 5 +-- .../kproj/evm-semantics/state-utils.md | 35 ++++++++++++++++++- 4 files changed, 53 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 223615f467..947f5bf29e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -630,6 +630,21 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : ("maxFeePerBlobGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("sender" : VALUE) => .K ... ListItem(TXID) ... TXID TW TR TS ... B requires #sender( #getTxData(TXID), TW, TR, TS, B ) ==K VALUE + rule check "transactions" : "authorizationList" : [ .JSONs ] => .K ... + rule check "transactions" : "authorizationList" : [ { "chainId": CID, "address": ADDR, "nonce": NONCE, "v": _, "r": SIGR, "s": SIGS, "signer": _, "yParity": SIGY } , REST ] + => check "transactions" : "authorizationList" : [ #hex2Bytes(CID), #hex2Bytes(ADDR), #hex2Bytes(NONCE), #hex2Bytes(SIGY), #hex2Bytes(SIGR), #hex2Bytes(SIGS) ] + ~> check "transactions" : "authorizationList" : [ REST ] + ... + + rule check "transactions" : "authorizationList" : [ AUTH ] => .K ... + ListItem(TXID) ... + TXID AUTHLIST ... requires #parseJSONs2List(AUTH) in AUTHLIST + + syntax Bytes ::= #hex2Bytes ( String ) [function] //TODO: Is this needed? + // ------------------------------------------------- + rule #hex2Bytes("0x00") => b"" + rule #hex2Bytes(S) => #parseByteStack(S) [owise] + syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function] | isInAccessList ( Account , Int , JSON ) [symbol(isInAccessList), function] // ------------------------------------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md index c1bd8d7d49..7a250c0244 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md @@ -476,7 +476,7 @@ Productions related to transactions syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)] syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)] syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: List ) [symbol(BlobTxData)] - syntax SetCodeTx ::= SetCodeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, authorizationList: JSONs) [symbol(SetCodeTxData)] + syntax SetCodeTx ::= SetCodeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, authorizationList: List) [symbol(SetCodeTxData)] // ------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------ endmodule ``` diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 7c2e18d735..eb9424b985 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -298,6 +298,7 @@ Unparsing // ---------------------------------------------------- rule #parseList2JSONs( .List ) => .JSONs rule #parseList2JSONs( ListItem(X:Bytes) REST ) => X , #parseList2JSONs(REST) + rule #parseList2JSONs( ListItem(X:List) REST) => [ #parseList2JSONs(X) ] , #parseList2JSONs(REST) ``` Recursive Length Prefix (RLP) @@ -414,8 +415,8 @@ Encoding rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [#parseList2JSONs(TVH)] ] ) - rule #rlpEncodeTxData( SetCodeTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], [TAUTH]) ) - => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], [TAUTH]] ) + rule #rlpEncodeTxData( SetCodeTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], AUTH) ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], [#parseList2JSONs(AUTH)]] ) syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function] // --------------------------------------------------------------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index 590505e22c..650c7a80cc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -199,6 +199,7 @@ The `"network"` key allows setting the fee schedule inside the test. // ---------------------------------------------------------- rule #parseJSONs2List ( .JSONs ) => .List rule #parseJSONs2List ( (VAL:Bytes) , REST ) => ListItem(VAL) #parseJSONs2List ( REST ) + rule #parseJSONs2List ( [VS:JSONs], REST ) => ListItem(#parseJSONs2List(VS)) #parseJSONs2List ( REST ) ``` The `"rlp"` key loads the block information. @@ -378,6 +379,18 @@ The `"rlp"` key loads the block information. requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob) + rule load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, AUTH , TY, TR, TS ]] , REST ] + => mkTX !ID:Int + ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP + , "nonce" : TN , "r" : TR , "s" : TS + , "to" : TT , "v" : TY , "value" : TV + , "accessList" : TA , "type" : TYPE , "chainID" : TC + , "maxFeePerGas" : TF , "authList" : AUTH , .JSONs } + ~> load "transaction" : [ REST ] + ... + + requires #asWord(TYPE) ==Int #dasmTxPrefix(SetCode) + syntax EthereumCommand ::= "loadTransaction" Int JSON // ----------------------------------------------------- rule loadTransaction _ { .JSONs } => .K ... @@ -429,7 +442,10 @@ The `"rlp"` key loads the block information. TXID _ => TB ... rule loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... - TXID _ => #parseJSONs2List(TVH) ... + TXID _ => #parseJSONs2List(TVH) ... + + rule loadTransaction TXID { "authList" : [AUTH:JSONs], REST => REST } ... + TXID _ => #parseJSONs2List(AUTH) ... ``` ### Getting State @@ -518,6 +534,23 @@ The `"rlp"` key loads the block information. Blob ... + + rule [[ #getTxData( TXID ) => SetCodeTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, AUTH) ]] + + TXID + TN + TG + TT + TV + DATA + CID + TA + TPF + TM + AUTH + SetCode + ... + ``` - `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559 From d1f93de273487a21a2ee094186ff2cc5797dede8 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Tue, 6 May 2025 17:37:17 +0300 Subject: [PATCH 3/8] recover authority from message data --- .../kevm_pyk/kproj/evm-semantics/driver.md | 4 ++ .../src/kevm_pyk/kproj/evm-semantics/evm.md | 65 +++++++++++++++++++ .../kevm_pyk/kproj/evm-semantics/schedule.md | 5 +- .../kproj/evm-semantics/serialization.md | 14 ++++ 4 files changed, 87 insertions(+), 1 deletion(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 947f5bf29e..6867f127dc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -109,6 +109,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule loadTx(ACCTFROM) => #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED) ~> #loadAccessList(TA) + ~> #loadAuthorities(AUTH) ~> #checkCreate ACCTFROM VALUE ~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE ~> #finishTx ~> #finalizeTx(false) ~> startTx @@ -129,6 +130,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a CODE TA TVH + AUTH ... _ => TVH @@ -147,6 +149,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a rule loadTx(ACCTFROM) => #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED) ~> #loadAccessList(TA) + ~> #loadAuthorities(AUTH) ~> #checkCall ACCTFROM VALUE ~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false ~> #finishTx ~> #finalizeTx(false) ~> startTx @@ -167,6 +170,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a DATA TA TVH + AUTH ... _ => TVH diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 2a3fc95d3c..e63c221008 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2573,6 +2573,71 @@ There are several helpers for calculating gas (most of them also specified in th rule #accountNonexistent(_) => true ... [owise] ``` +Processing SetCode Transaction Authority Entries +================================================ + +- The `#loadAuthorities` function processes the list of authorization entries in EIP-7702 SetCode transactions. +- First rule skips processing if transaction is not SetCode type or the auth list is empty. +- Second rule processes each authorization entry by recovering the signer, adding delegation, and continuing with remaining entries. +- The `#addAuthority` function implements the EIP's verification steps: + - Verifies chain ID matches (or is 0) + - Verifies the authority account's nonce matches authorization + - Sets delegation code (0xEF0100 + address) or clears it if address is 0 + - Increments the authority's nonce + - Provides gas refund for non-empty accounts + - Creates new accounts when needed + +```k + syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] + // -------------------------------------------------------------------------- + rule #loadAuthorities ( AUTH ) => .K ... + ListItem(TXID:Int) ... + + TXID + TXTYPE + ... + + requires (notBool TXTYPE ==K SetCode) + orBool AUTH ==K .List + + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) + => #addAuthority (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR, true) + ~> #loadAuthorities (REST) + ... + + syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes, Bool ) [symbol(#addAuthority)] + // ----------------------------------------------------------------------------------------------------- + rule #addAuthority(AUTHORITY, CID, NONCE, _ADDR, _EXISTS) => .K ... + ENV_CID + + AUTHORITY + ACCTCODE + ACCTNONCE + ... + + requires notBool ( AUTHORITY =/=K .Account + andBool (#range(ACCTCODE,0,4) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) + andBool #asWord(NONCE) ==Int ACCTNONCE + andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) ) + + rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, EXISTS) => #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY ... + ENV_CID + SCHED + REFUND => #if EXISTS #then REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > #else REFUND #fi + + AUTHORITY + ACCTCODE => #if notBool #asWord(ADDR) ==Int 0 #then EOA_DELEGATION_MARKER +Bytes ADDR #else .Bytes #fi + ACCTNONCE => ACCTNONCE +Int 1 + ... + + requires AUTHORITY =/=K .Account + andBool (#range(ACCTCODE,0,4) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) + andBool #asWord(NONCE) ==Int ACCTNONCE + andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) + + rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, _EXISTS) => #newAccount AUTHORITY ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, false) ... [owise] +``` + EVM Program Representations =========================== diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index b1d01a4b14..7827422c80 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -48,7 +48,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. | "Gblockhash" | "Gquadcoeff" | "maxCodeSize" | "Rb" | "Gquaddivisor" | "Gecadd" | "Gecmul" | "Gecpairconst" | "Gecpaircoeff" | "Gfround" | "Gcoldsload" | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress" | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore" - | "Gpointeval" + | "Gpointeval" | "Gauthbase" // ---------------------------------------------------------------------------------------------------------------------------------------------------- ``` @@ -82,6 +82,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GcallstipendDefault]: Gcallstipend < DEFAULT > => 2300 rule [GcallvalueDefault]: Gcallvalue < DEFAULT > => 9000 rule [GnewaccountDefault]: Gnewaccount < DEFAULT > => 25000 + rule [GauthbaseDefault]: Gauthbase < DEFAULT > => 0 rule [GcreateDefault]: Gcreate < DEFAULT > => 32000 rule [GcodedepositDefault]: Gcodedeposit < DEFAULT > => 200 @@ -421,7 +422,9 @@ A `ScheduleConst` is a constant determined by the fee schedule. ```k syntax Schedule ::= "PRAGUE" [symbol(PRAGUE_EVM), smtlib(schedule_PRAGUE)] // -------------------------------------------------------------------------- + rule [GauthbasePrague]: Gauthbase < PRAGUE > => 12500 rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN > + requires notBool ( SCHEDCONST ==K Gauthbase ) rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index eb9424b985..5ddbcc76ee 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -767,5 +767,19 @@ Tree Root Helper Functions +Bytes #rlpEncodeBytes( #parseByteStack( Keccak256(b"") ) ) , 192 ) +``` + +Processing authorities in SetCode Transactions +============================================== + +```k + syntax Bytes ::= "SET_CODE_TX_MAGIC" [macro] | "EOA_DELEGATION_MARKER" [macro] + // ------------------------------------------------------------------------------ + rule SET_CODE_TX_MAGIC => b"\x05" + rule EOA_DELEGATION_MARKER => b"\xEF\x01\x00" + + syntax Account ::= #recoverAuthority ( Bytes , Bytes , Bytes , Bytes , Bytes , Bytes ) [symbol(#recoverAuthority), function] + // ------------------------------------------------------------------------------------------------------------------------ + rule #recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS) => #sender( Keccak256raw(SET_CODE_TX_MAGIC +Bytes #rlpEncode([CID, ADDR, NONCE])), #asWord(YPAR) +Int 27, SIGR, SIGS ) endmodule ``` From bf7a7f3b3273c35a59e3b6d1e45d41b20f35113c Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Tue, 6 May 2025 17:50:13 +0300 Subject: [PATCH 4/8] add docstrings --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 5ddbcc76ee..7af225f978 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -771,6 +771,9 @@ Tree Root Helper Functions Processing authorities in SetCode Transactions ============================================== +- These rules define constants and functions used to process authority accounts in EIP-7702 SetCode transactions. +- The `SET_CODE_TX_MAGIC` (`0x05`) prefixes the message hash, while `EOA_DELEGATION_MARKER` (`0xEF0100`) marks delegated EOA code. +- The `#recoverAuthority` function recovers the signer address from parameters. ```k syntax Bytes ::= "SET_CODE_TX_MAGIC" [macro] | "EOA_DELEGATION_MARKER" [macro] @@ -781,5 +784,6 @@ Processing authorities in SetCode Transactions syntax Account ::= #recoverAuthority ( Bytes , Bytes , Bytes , Bytes , Bytes , Bytes ) [symbol(#recoverAuthority), function] // ------------------------------------------------------------------------------------------------------------------------ rule #recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS) => #sender( Keccak256raw(SET_CODE_TX_MAGIC +Bytes #rlpEncode([CID, ADDR, NONCE])), #asWord(YPAR) +Int 27, SIGR, SIGS ) + endmodule ``` From 46be55e5f8a00eed3ab40fe8cb30226584c2f0d4 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Sat, 24 May 2025 20:32:00 +0300 Subject: [PATCH 5/8] process delegated authority in #call rules --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 52 +++++++++++++++++-- .../kevm_pyk/kproj/evm-semantics/schedule.md | 7 ++- .../kproj/evm-semantics/serialization.md | 6 +-- .../kproj/evm-semantics/state-utils.md | 31 +++++++++++ tests/execution-spec-tests/failing.llvm | 8 --- 5 files changed, 86 insertions(+), 18 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 4e7f7f2b62..34c014eb46 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1584,6 +1584,25 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule #checkCall ACCT VALUE => #checkBalanceUnderflow ACCT VALUE ~> #checkDepthExceeded ... + rule [call.delegatedAuthority]: + #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC + => #callWithCode ACCTFROM ACCTTO TARGET_ACCT TARGET_CODE VALUE APPVALUE ARGS STATIC + ... + + SCHED + + ACCTCODE + CODE + ... + + + TARGET_ACCT + TARGET_CODE + ... + + requires Ghasauthority << SCHED >> + andBool #isValidDelegation (CODE) + rule [call.true]: #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC => #callWithCode ACCTFROM ACCTTO ACCTCODE CODE VALUE APPVALUE ARGS STATIC @@ -1594,6 +1613,9 @@ The various `CALL*` (and other inter-contract control flow) operations will be d CODE ... + SCHED + requires notBool Ghasauthority << SCHED >> + orBool (Ghasauthority << SCHED>> andBool notBool #isValidDelegation(CODE)) rule [call.false]: #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC @@ -2984,8 +3006,11 @@ Processing SetCode Transaction Authority Entries - Provides gas refund for non-empty accounts - Creates new accounts when needed +- `isValidDelegation` - checks whether the code of an account is a valid delegation designation with the delegation marker prefix (`0xef0100`) and a length of 23 bytes. + + ```k - syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] + syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] | "#DBG1" | "#DBG2" // -------------------------------------------------------------------------- rule #loadAuthorities ( AUTH ) => .K ... ListItem(TXID:Int) ... @@ -3000,7 +3025,7 @@ Processing SetCode Transaction Authority Entries rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) => #addAuthority (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR, true) ~> #loadAuthorities (REST) - ... + ... [owise] syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes, Bool ) [symbol(#addAuthority)] // ----------------------------------------------------------------------------------------------------- @@ -3008,12 +3033,12 @@ Processing SetCode Transaction Authority Entries ENV_CID AUTHORITY - ACCTCODE + ACCTCODE ACCTNONCE ... requires notBool ( AUTHORITY =/=K .Account - andBool (#range(ACCTCODE,0,4) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) + andBool (#range(ACCTCODE,0,3) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) andBool #asWord(NONCE) ==Int ACCTNONCE andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) ) @@ -3028,11 +3053,28 @@ Processing SetCode Transaction Authority Entries ... requires AUTHORITY =/=K .Account - andBool (#range(ACCTCODE,0,4) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) + andBool (ACCTCODE ==K .Bytes orBool notBool #isValidDelegation(ACCTCODE)) andBool #asWord(NONCE) ==Int ACCTNONCE andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, _EXISTS) => #newAccount AUTHORITY ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, false) ... [owise] + + syntax Bool ::= #isValidDelegation ( Bytes ) [symbol(#isValidDelegation), function, total] + // ------------------------------------------------------------------------------------------ + rule #isValidDelegation(CODE) => true requires #range(CODE, 0, 3) ==K EOA_DELEGATION_MARKER andBool lengthBytes(CODE) ==Int 23 + rule #isValidDelegation(_ ) => false [owise] + + syntax Bool ::= #checkAuthorityList ( List ) [symbol(#checkAuthorityList), function, total] + // ------------------------------------------------------------------------------------------- + rule #checkAuthorityList (.List) => true + rule #checkAuthorityList (ListItem(ListItem(CID:Bytes) ListItem(ADDR:Bytes) ListItem(NONCE:Bytes) ListItem(YPAR:Bytes) ListItem(SIGR:Bytes) ListItem(SIGS:Bytes)) REST ) => true andBool #checkAuthorityList(REST) + requires #rangeUInt(256, Bytes2Int(CID, BE, Unsigned)) + andBool #rangeUInt(64, Bytes2Int(NONCE, BE, Unsigned)) + andBool lengthBytes(ADDR) ==Int 20 + andBool #rangeUInt(8, Bytes2Int(YPAR, BE, Unsigned)) + andBool #rangeUInt(256, Bytes2Int(SIGR, BE, Unsigned)) + andBool #rangeUInt(256, Bytes2Int(SIGS, BE, Unsigned)) + rule #checkAuthorityList(_) => false [owise] ``` EVM Program Representations diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index 39098424ca..bebd9416b8 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -30,7 +30,7 @@ module SCHEDULE | "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero" | "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy" | "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash" - | "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" + | "Ghasbls12msmdiscount" | "Ghashistory" | "Ghasrequests" | "Ghasauthority" // ----------------------------------------------------------------- ``` @@ -178,6 +178,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhashistoryDefault]: Ghashistory << DEFAULT >> => false rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false rule [Ghasbls12msmdiscountDefault]: Ghasbls12msmdiscount << DEFAULT >> => false + rule [GhasauthorityDefault]: Ghasauthority << DEFAULT >> => false ``` ### Frontier Schedule @@ -482,10 +483,12 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true rule [GhashistoryPrague]: Ghashistory << PRAGUE >> => true rule [Ghasbls12msmdiscountPrague]: Ghasbls12msmdiscount << PRAGUE >> => true + rule [GhasauthorityPrague]: Ghasauthority << PRAGUE >> => true rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >> requires notBool ( SCHEDFLAG ==K Ghasrequests orBool SCHEDFLAG ==K Ghashistory - orBool SCHEDFLAG ==K Ghasbls12msmdiscount ) + orBool SCHEDFLAG ==K Ghasbls12msmdiscount + orBool SCHEDFLAG ==K Ghasauthority ) ``` ```k diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md index 18f4cf22f0..d1ab50d9b3 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -794,12 +794,12 @@ Processing authorities in SetCode Transactions ```k syntax Bytes ::= "SET_CODE_TX_MAGIC" [macro] | "EOA_DELEGATION_MARKER" [macro] - // ------------------------------------------------------------------------------ + // ---------------------------------------------------------------------- rule SET_CODE_TX_MAGIC => b"\x05" - rule EOA_DELEGATION_MARKER => b"\xEF\x01\x00" + rule EOA_DELEGATION_MARKER => #parseByteStack("0xef0100") syntax Account ::= #recoverAuthority ( Bytes , Bytes , Bytes , Bytes , Bytes , Bytes ) [symbol(#recoverAuthority), function] - // ------------------------------------------------------------------------------------------------------------------------ + // ---------------------------------------------------------------------------------------------------------------------------- rule #recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS) => #sender( Keccak256raw(SET_CODE_TX_MAGIC +Bytes #rlpEncode([CID, ADDR, NONCE])), #asWord(YPAR) +Int 27, SIGR, SIGS ) endmodule diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index bb8355ebc0..a7c9bed121 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -599,6 +599,37 @@ The `"rlp"` key loads the block information. ```k syntax Bool ::= #isValidTransaction( Int , Account ) [symbol(#isValidTransaction), function] // -------------------------------------------------------------------------------------------- + rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] + BASE_FEE + BLOCK_GAS_LIMIT + + ACCTFROM + BAL + ACCTCODE + ACCTNONCE + ... + + + TXID + TX_NONCE + TX_GAS_LIMIT + ACCTTO + VALUE + TX_MAX_PRIORITY_FEE + TX_MAX_FEE + TX_AUTH_LIST + SetCode + ... + + requires ACCTCODE ==K .Bytes + andBool notBool ACCTTO ==K .Account + andBool ACCTNONCE ==Int TX_NONCE + andBool BASE_FEE <=Int TX_MAX_FEE + andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE + andBool BAL >=Int TX_GAS_LIMIT *Int TX_MAX_FEE +Int VALUE + andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT + andBool size(TX_AUTH_LIST) >Int 0 andBool #checkAuthorityList(TX_AUTH_LIST) + rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] SCHED BASE_FEE diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index dfdcd6d866..0960547693 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1694,8 +1694,6 @@ blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requ 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_single_consolidation_request_from_eoa_max_pubkeys] 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_single_consolidation_request_from_eoa] blockchain_tests/prague/eip7251_consolidations/contract_deployment/system_contract_deployment.json,* -blockchain_tests/prague/eip7623_increase_calldata_cost/execution_gas/full_gas_consumption.json,tests/prague/eip7623_increase_calldata_cost/test_execution_gas.py::TestGasConsumption::test_full_gas_consumption[fork_Prague-blockchain_test_from_state_test-exact_gas-type_4] -blockchain_tests/prague/eip7623_increase_calldata_cost/execution_gas/full_gas_consumption.json,tests/prague/eip7623_increase_calldata_cost/test_execution_gas.py::TestGasConsumption::test_full_gas_consumption[fork_Prague-blockchain_test_from_state_test-extra_gas-type_4] blockchain_tests/prague/eip7623_increase_calldata_cost/execution_gas/gas_consumption_below_data_floor.json,* blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_EQUAL_TO_DATA_FLOOR] blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_GREATER_THAN_DATA_FLOOR] @@ -1840,7 +1838,6 @@ blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_normal.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_reentry.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_resets_an_empty_code_account_with_storage.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_reverts.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_pointer.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_precompile.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_static_reentry.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_static.json,* @@ -1849,18 +1846,15 @@ blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/address_from_set_code.j blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/authorization_reusing_nonce.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/call_into_chain_delegating_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/call_into_self_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/contract_create.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_and_set.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_failing_tx.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/empty_authorization_list.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/eoa_tx_after_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_chain_delegating_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_self_delegating_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_self_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/invalid_transaction_after_authorization.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/many_delegations.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_overflow_after_first_authorization.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,* @@ -1871,7 +1865,6 @@ blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_address_and_au blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_address_and_authority_warm_state.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_all_invalid_authorization_tuples.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_call_set_code.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/set_code_max_depth_call_stack.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_first_valid_authorization_tuples_same_signer.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_first_invalid_same_signer.json,* @@ -1890,7 +1883,6 @@ blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_sstore.json blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_system_contract.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_tstore_available_at_correct_address.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_tstore_reentry.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_transaction_fee_validations.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_using_chain_specific_id.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_using_valid_synthetic_signatures.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/signature_s_out_of_range.json,* From 61e095f48504752a0fb9506fbd00ba1fca018ea6 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 26 May 2025 19:11:24 +0300 Subject: [PATCH 6/8] compute gas costs --- .../kevm_pyk/kproj/evm-semantics/driver.md | 66 +++++++ .../src/kevm_pyk/kproj/evm-semantics/evm.md | 150 ++++++++-------- .../src/kevm_pyk/kproj/evm-semantics/gas.md | 51 +++--- kevm-pyk/src/tests/utils.py | 1 + tests/execution-spec-tests/failing.llvm | 166 +++++++++++------- 5 files changed, 269 insertions(+), 165 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 4e7b395631..85334b4ddb 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -279,6 +279,72 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a GLIMIT => GLIMIT -Int Gaccesslistaddress < SCHED > ``` +Processing SetCode Transaction Authority Entries +================================================ + +- The `#loadAuthorities` function processes the list of authorization entries in EIP-7702 SetCode transactions. +- First rule skips processing if transaction is not SetCode type or the auth list is empty. +- Second rule processes each authorization entry by recovering the signer, adding delegation, and continuing with remaining entries. +- The `#addAuthority` function implements the EIP's verification steps: + - Verifies chain ID matches (or is 0) + - Verifies the authority account's nonce matches authorization + - Sets delegation code (0xEF0100 + address) or clears it if address is 0 + - Increments the authority's nonce + - Provides gas refund for non-empty accounts + - Creates new accounts when needed + +```k + syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] | "#DBG1" | "#DBG2" + // -------------------------------------------------------------------------- + rule #loadAuthorities ( AUTH ) => .K ... + ListItem(TXID:Int) ... + + TXID + TXTYPE + ... + + requires (notBool TXTYPE ==K SetCode) + orBool AUTH ==K .List + + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) + => #addAuthority (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR, true) + ~> #loadAuthorities (REST) + ... + GLIMIT => GLIMIT -Int 25000 [owise] + + syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes, Bool ) [symbol(#addAuthority)] + // ----------------------------------------------------------------------------------------------------- + rule #addAuthority(AUTHORITY, CID, NONCE, _ADDR, _EXISTS) => .K ... + ENV_CID + + AUTHORITY + ACCTCODE + ACCTNONCE + ... + + requires notBool ( AUTHORITY =/=K .Account + andBool (#range(ACCTCODE,0,3) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) + andBool #asWord(NONCE) ==Int ACCTNONCE + andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) ) + + rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, EXISTS) => #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY ... + ENV_CID + SCHED + REFUND => #if EXISTS #then REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > #else REFUND #fi + + AUTHORITY + ACCTCODE => #if notBool #asWord(ADDR) ==Int 0 #then EOA_DELEGATION_MARKER +Bytes ADDR #else .Bytes #fi + ACCTNONCE => ACCTNONCE +Int 1 + ... + + requires AUTHORITY =/=K .Account + andBool (ACCTCODE ==K .Bytes orBool notBool #isValidDelegation(ACCTCODE)) + andBool #asWord(NONCE) ==Int ACCTNONCE + andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) + + rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, _EXISTS) => #newAccount AUTHORITY ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, false) ... [owise] +``` + - `exception` only clears from the `` cell if there is an exception preceding it. - `failure_` holds the name of a test that failed if a test does fail. - `success` sets the `` to `0` and the `` to `SUCCESS`. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 34c014eb46..cccba3a029 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1586,7 +1586,9 @@ The various `CALL*` (and other inter-contract control flow) operations will be d rule [call.delegatedAuthority]: #call ACCTFROM ACCTTO ACCTCODE VALUE APPVALUE ARGS STATIC - => #callWithCode ACCTFROM ACCTTO TARGET_ACCT TARGET_CODE VALUE APPVALUE ARGS STATIC + => #let DELEGATED_ACCOUNT = #getDelegatedAccount(CODE) #in + (#accessAccounts DELEGATED_ACCOUNT + ~> #callWithCode ACCTFROM ACCTTO ACCTCODE #getAccountCode(DELEGATED_ACCOUNT) VALUE APPVALUE ARGS STATIC ) ... SCHED @@ -1595,11 +1597,6 @@ The various `CALL*` (and other inter-contract control flow) operations will be d CODE ... - - TARGET_ACCT - TARGET_CODE - ... - requires Ghasauthority << SCHED >> andBool #isValidDelegation (CODE) @@ -2779,16 +2776,16 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, LOG(N) _ WIDTH) => (Glog < SCHED > +Int (Glogdata < SCHED > *Int WIDTH) +Int (N *Int Glogtopic < SCHED >)) ... rule #gasExec(SCHED, CALL GCAP ACCTTO VALUE _ _ _ _) - => Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS) ~> #allocateCallGas - ~> Ccall(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS) + => Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #allocateCallGas + ~> Ccall(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ... GAVAIL ACCTS rule #gasExec(SCHED, CALLCODE GCAP ACCTTO VALUE _ _ _ _) - => Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS) ~> #allocateCallGas - ~> Ccall(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS) + => Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #allocateCallGas + ~> Ccall(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, VALUE, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ... ACCTFROM @@ -2796,8 +2793,8 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). ACCTS rule #gasExec(SCHED, DELEGATECALL GCAP ACCTTO _ _ _ _) - => Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0, ACCTTO in ACCTS) ~> #allocateCallGas - ~> Ccall(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0, ACCTTO in ACCTS) + => Ccallgas(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #allocateCallGas + ~> Ccall(SCHED, #accountNonexistent(ACCTFROM), GCAP, GAVAIL, 0, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ... ACCTFROM @@ -2805,8 +2802,8 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). ACCTS rule #gasExec(SCHED, STATICCALL GCAP ACCTTO _ _ _ _) - => Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0, ACCTTO in ACCTS) ~> #allocateCallGas - ~> Ccall(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0, ACCTTO in ACCTS) + => Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ~> #allocateCallGas + ~> Ccall(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, 0, ACCTTO in ACCTS, #accountHasAuthority(ACCTTO), #accountAuthorityIsWarm(ACCTTO)) ... GAVAIL @@ -2962,15 +2959,15 @@ There are several helpers for calculating gas (most of them also specified in th ```k syntax Exp ::= Int | Gas syntax KResult ::= Int - syntax Exp ::= Ccall ( Schedule , BExp , Gas , Gas , Int , Bool ) [symbol(Ccall), strict(2)] - | Ccallgas ( Schedule , BExp , Gas , Gas , Int , Bool ) [symbol(Ccallgas), strict(2)] - | Cselfdestruct ( Schedule , BExp , Int ) [symbol(Cselfdestruct), strict(2)] - // ------------------------------------------------------------------------------------------------------------ - rule Ccall(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM) - => Cextra(SCHED, ISEMPTY, VALUE, ISWARM) +Gas Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM)) ... + syntax Exp ::= Ccall ( Schedule , BExp , Gas , Gas , Int , Bool , Bool , Bool ) [symbol(Ccall), strict(2)] + | Ccallgas ( Schedule , BExp , Gas , Gas , Int , Bool , Bool , Bool ) [symbol(Ccallgas), strict(2)] + | Cselfdestruct ( Schedule , BExp , Int ) [symbol(Cselfdestruct), strict(2)] + // -------------------------------------------------------------------------------------------------------------------------- + rule Ccall(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) + => Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) +Gas Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION)) ... - rule Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM) - => Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM)) +Gas #if VALUE ==Int 0 #then 0 #else Gcallstipend < SCHED > #fi ... + rule Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) + => Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION)) +Gas #if VALUE ==Int 0 #then 0 #else Gcallstipend < SCHED > #fi ... rule Cselfdestruct(SCHED, ISEMPTY:Bool, BAL) => Gselfdestruct < SCHED > +Int Cnew(SCHED, ISEMPTY andBool Gselfdestructnewaccount << SCHED >>, BAL) ... @@ -2994,75 +2991,48 @@ There are several helpers for calculating gas (most of them also specified in th Processing SetCode Transaction Authority Entries ================================================ - -- The `#loadAuthorities` function processes the list of authorization entries in EIP-7702 SetCode transactions. -- First rule skips processing if transaction is not SetCode type or the auth list is empty. -- Second rule processes each authorization entry by recovering the signer, adding delegation, and continuing with remaining entries. -- The `#addAuthority` function implements the EIP's verification steps: - - Verifies chain ID matches (or is 0) - - Verifies the authority account's nonce matches authorization - - Sets delegation code (0xEF0100 + address) or clears it if address is 0 - - Increments the authority's nonce - - Provides gas refund for non-empty accounts - - Creates new accounts when needed - -- `isValidDelegation` - checks whether the code of an account is a valid delegation designation with the delegation marker prefix (`0xef0100`) and a length of 23 bytes. - + - `#isValidDelegation` - checks whether the code of an account is a valid delegation designation with the delegation marker prefix (`0xef0100`) and a length of 23 bytes. + - `#accountHasAuthority` - returns wether the code of a given account is a valid delegation according to EIP-7702. + - `#accountAuthorityIsWarm` - for a given account, check if the delegated address inside the account code is present in `accessed_accounts`, returning `false` if the code is a non valid delegation. + - `#getDelegatedAccount` - extract the delegated address from a Bytes object, returning `.Account` if the Bytes argument is not a valid delegation. + - `#checkAuthorityList` - check if the authority list of a SetCode type transaction is valid. ```k - syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] | "#DBG1" | "#DBG2" - // -------------------------------------------------------------------------- - rule #loadAuthorities ( AUTH ) => .K ... - ListItem(TXID:Int) ... - - TXID - TXTYPE - ... - - requires (notBool TXTYPE ==K SetCode) - orBool AUTH ==K .List - - rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) - => #addAuthority (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR, true) - ~> #loadAuthorities (REST) - ... [owise] + syntax Bool ::= #isValidDelegation ( Bytes ) [symbol(#isValidDelegation), function, total] + // ------------------------------------------------------------------------------------------ + rule #isValidDelegation(CODE) => true requires #range(CODE, 0, 3) ==K EOA_DELEGATION_MARKER andBool lengthBytes(CODE) ==Int 23 + rule #isValidDelegation(_ ) => false [owise] - syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes, Bool ) [symbol(#addAuthority)] - // ----------------------------------------------------------------------------------------------------- - rule #addAuthority(AUTHORITY, CID, NONCE, _ADDR, _EXISTS) => .K ... - ENV_CID + syntax Bool ::= #accountHasAuthority ( Account ) [symbol(#accountHasAuthority), function, total] + // ------------------------------------------------------------------------------------------------ + rule [[#accountHasAuthority(ACCTTO) => true]] - AUTHORITY - ACCTCODE - ACCTNONCE - ... + ACCTTO + CODE + ... - requires notBool ( AUTHORITY =/=K .Account - andBool (#range(ACCTCODE,0,3) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) - andBool #asWord(NONCE) ==Int ACCTNONCE - andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) ) + requires #isValidDelegation(CODE) - rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, EXISTS) => #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY ... - ENV_CID - SCHED - REFUND => #if EXISTS #then REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > #else REFUND #fi + rule #accountHasAuthority(_) => false[owise] + + syntax Bool ::= #accountAuthorityIsWarm ( Account ) [symbol(#accountAuthorityIsWarm), function, total] + // ------------------------------------------------------------------------------------------------------ + rule [[#accountAuthorityIsWarm(ACCTTO) => true]] - AUTHORITY - ACCTCODE => #if notBool #asWord(ADDR) ==Int 0 #then EOA_DELEGATION_MARKER +Bytes ADDR #else .Bytes #fi - ACCTNONCE => ACCTNONCE +Int 1 - ... + ACCTTO + CODE + ... - requires AUTHORITY =/=K .Account - andBool (ACCTCODE ==K .Bytes orBool notBool #isValidDelegation(ACCTCODE)) - andBool #asWord(NONCE) ==Int ACCTNONCE - andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) + ACCTS + requires #isValidDelegation(CODE) + andBool (#asAccount(#range(CODE,3,20)) in ACCTS orBool #asAccount(#range(CODE,3,20)) ==K ACCTTO) - rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, _EXISTS) => #newAccount AUTHORITY ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, false) ... [owise] + rule #accountAuthorityIsWarm(_) => false [owise] - syntax Bool ::= #isValidDelegation ( Bytes ) [symbol(#isValidDelegation), function, total] - // ------------------------------------------------------------------------------------------ - rule #isValidDelegation(CODE) => true requires #range(CODE, 0, 3) ==K EOA_DELEGATION_MARKER andBool lengthBytes(CODE) ==Int 23 - rule #isValidDelegation(_ ) => false [owise] + syntax Account ::= #getDelegatedAccount ( Bytes ) [symbol(#getDelegatedAccount), function, total] + // ------------------------------------------------------------------------------------------------- + rule #getDelegatedAccount(CODE) => #asAccount(#range(CODE,3,20)) requires #isValidDelegation(CODE) + rule #getDelegatedAccount(_) => .Account [owise] syntax Bool ::= #checkAuthorityList ( List ) [symbol(#checkAuthorityList), function, total] // ------------------------------------------------------------------------------------------- @@ -3077,6 +3047,24 @@ Processing SetCode Transaction Authority Entries rule #checkAuthorityList(_) => false [owise] ``` +Account helper functions +======================== + + - `#getAccountCode(Account)` - K function to retrieve the code of an account, returning the empty bytes object if the account is not in the state. + +```k + syntax Bytes ::= #getAccountCode ( Account ) [symbol(#getAccountCode), function, total] + // --------------------------------------------------------------------------------------- + rule [[ #getAccountCode(ACCT) => CODE]] + + ACCT + CODE + ... + + + rule #getAccountCode(_) => .Bytes [owise] +``` + EVM Program Representations =========================== diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md index c7a0d55c88..c51b05065d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/gas.md @@ -106,26 +106,27 @@ module GAS-FEES syntax Gas ::= Cgascap ( Schedule , Gas , Gas , Int ) [symbol(Cgascap_Gas), overload(Cgascap), function, total, smtlib(gas_Cgascap_Gas)] syntax Int ::= Cgascap ( Schedule , Int , Int , Int ) [symbol(Cgascap_Int), overload(Cgascap), function, total, smtlib(gas_Cgascap_Int)] - syntax Int ::= Csstore ( Schedule , Int , Int , Int ) [symbol(Csstore), function, total, smtlib(gas_Csstore) ] - | Rsstore ( Schedule , Int , Int , Int ) [symbol(Rsstore), function, total, smtlib(gas_Rsstore) ] - | Cextra ( Schedule , Bool , Int , Bool ) [symbol(Cextra), function, total, smtlib(gas_Cextra) ] - | Cnew ( Schedule , Bool , Int ) [symbol(Cnew), function, total, smtlib(gas_Cnew) ] - | Cxfer ( Schedule , Int ) [symbol(Cxfer), function, total, smtlib(gas_Cxfer) ] - | Cmem ( Schedule , Int ) [symbol(Cmem), function, total, smtlib(gas_Cmem), memo ] - | Caddraccess ( Schedule , Bool ) [symbol(Caddraccess), function, total, smtlib(gas_Caddraccess) ] - | Cstorageaccess ( Schedule , Bool ) [symbol(Cstorageaccess), function, total, smtlib(gas_Cstorageaccess)] - | Csload ( Schedule , Bool ) [symbol(Csload), function, total, smtlib(gas_Csload) ] - | Cextcodesize ( Schedule ) [symbol(Cextcodesize), function, total, smtlib(gas_Cextcodesize) ] - | Cextcodecopy ( Schedule , Int ) [symbol(Cextcodecopy), function, total, smtlib(gas_Cextcodecopy) ] - | Cextcodehash ( Schedule ) [symbol(Cextcodehash), function, total, smtlib(gas_Cextcodehash) ] - | Cbalance ( Schedule ) [symbol(Cbalance), function, total, smtlib(gas_Cbalance) ] - | Cmodexp ( Schedule , Bytes , Int , Int , Int ) [symbol(Cmodexp), function, total, smtlib(gas_Cmodexp) ] - | Cinitcode ( Schedule , Int ) [symbol(Cinitcode), function, total, smtlib(gas_Cinitcode) ] - | Ctotalblob ( Schedule , Int ) [symbol(Ctotalblob), function, total, smtlib(gas_Ctotalblob) ] - | Cbasefeeperblob( Schedule , Int ) [symbol(Cbasefeeperblob),function, total, smtlib(gas_Cbasefeeperblob) ] - | Cblobfee ( Schedule , Int , Int ) [symbol(Cblobfee), function, total, smtlib(gas_Cblobfee) ] - | Cexcessblob ( Schedule , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ] - // ------------------------------------------------------------------------------------------------------------------------------------------ + syntax Int ::= Csstore ( Schedule , Int , Int , Int ) [symbol(Csstore), function, total, smtlib(gas_Csstore) ] + | Rsstore ( Schedule , Int , Int , Int ) [symbol(Rsstore), function, total, smtlib(gas_Rsstore) ] + | Cextra ( Schedule , Bool , Int , Bool , Bool , Bool )[symbol(Cextra), function, total, smtlib(gas_Cextra) ] + | Cnew ( Schedule , Bool , Int ) [symbol(Cnew), function, total, smtlib(gas_Cnew) ] + | Cxfer ( Schedule , Int ) [symbol(Cxfer), function, total, smtlib(gas_Cxfer) ] + | Cmem ( Schedule , Int ) [symbol(Cmem), function, total, smtlib(gas_Cmem), memo ] + | Caddraccess ( Schedule , Bool ) [symbol(Caddraccess), function, total, smtlib(gas_Caddraccess) ] + | Cstorageaccess ( Schedule , Bool ) [symbol(Cstorageaccess), function, total, smtlib(gas_Cstorageaccess) ] + | Csload ( Schedule , Bool ) [symbol(Csload), function, total, smtlib(gas_Csload) ] + | Cextcodesize ( Schedule ) [symbol(Cextcodesize), function, total, smtlib(gas_Cextcodesize) ] + | Cextcodecopy ( Schedule , Int ) [symbol(Cextcodecopy), function, total, smtlib(gas_Cextcodecopy) ] + | Cextcodehash ( Schedule ) [symbol(Cextcodehash), function, total, smtlib(gas_Cextcodehash) ] + | Cbalance ( Schedule ) [symbol(Cbalance), function, total, smtlib(gas_Cbalance) ] + | Cmodexp ( Schedule , Bytes , Int , Int , Int ) [symbol(Cmodexp), function, total, smtlib(gas_Cmodexp) ] + | Cinitcode ( Schedule , Int ) [symbol(Cinitcode), function, total, smtlib(gas_Cinitcode) ] + | Ctotalblob ( Schedule , Int ) [symbol(Ctotalblob), function, total, smtlib(gas_Ctotalblob) ] + | Cbasefeeperblob ( Schedule , Int ) [symbol(Cbasefeeperblob), function, total, smtlib(gas_Cbasefeeperblob) ] + | Cblobfee ( Schedule , Int , Int ) [symbol(Cblobfee), function, total, smtlib(gas_Cblobfee) ] + | Cexcessblob ( Schedule , Int , Int ) [symbol(Cexcessblob), function, total, smtlib(gas_Cexcessblob) ] + | Cdelegationaccess( Schedule, Bool, Bool ) [symbol(Cdelegationaccess), function, total, smtlib(gas_Cdelegationaccess)] + // --------------------------------------------------------------------------------------------------------------------------------------------------------- rule [Cgascap]: Cgascap(SCHED, GCAP:Int, GAVAIL:Int, GEXTRA) => #if GAVAIL > #then GCAP #else minInt(#allBut64th(GAVAIL -Int GEXTRA), GCAP) #fi @@ -171,8 +172,9 @@ module GAS-FEES requires notBool Ghasdirtysstore << SCHED >> [concrete] - rule [Cextra.new]: Cextra(SCHED, ISEMPTY, VALUE, ISWARM) => Caddraccess(SCHED, ISWARM) +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires Ghasaccesslist << SCHED >> - rule [Cextra.old]: Cextra(SCHED, ISEMPTY, VALUE, _ISWARM) => Gcall < SCHED > +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires notBool Ghasaccesslist << SCHED >> + rule [Cextra.delegation]: Cextra(SCHED, ISEMPTY, VALUE, ISWARM, ISDELEGATION, ISWARMDELEGATION) => Cdelegationaccess(SCHED, ISDELEGATION, ISWARMDELEGATION) +Int Caddraccess(SCHED, ISWARM) +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires Ghasaccesslist << SCHED >> andBool Ghasauthority << SCHED >> + rule [Cextra.new]: Cextra(SCHED, ISEMPTY, VALUE, ISWARM, _ISDELEGATION, _ISWARMDELEGATION) => Caddraccess(SCHED, ISWARM) +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires Ghasaccesslist << SCHED >> andBool notBool Ghasauthority << SCHED >> + rule [Cextra.old]: Cextra(SCHED, ISEMPTY, VALUE, _ISWARM, _ISDELEGATION, _ISWARMDELEGATION) => Gcall < SCHED > +Int Cnew(SCHED, ISEMPTY, VALUE) +Int Cxfer(SCHED, VALUE) requires notBool Ghasaccesslist << SCHED >> rule [Cnew]: Cnew(SCHED, ISEMPTY:Bool, VALUE) @@ -219,7 +221,10 @@ module GAS-FEES rule [Cblobfee]: Cblobfee(SCHED, EXCESS_BLOB_GAS, BLOB_VERSIONED_HASHES_SIZE) => Ctotalblob(SCHED, BLOB_VERSIONED_HASHES_SIZE) *Int Cbasefeeperblob(SCHED, EXCESS_BLOB_GAS) rule [Cexcessblob]: Cexcessblob(SCHED, EXCESS_BLOB_GAS, BLOB_GAS_USED) => EXCESS_BLOB_GAS +Int BLOB_GAS_USED -Int Gtargetblobgas < SCHED > requires Gtargetblobgas < SCHED > <=Int EXCESS_BLOB_GAS +Int BLOB_GAS_USED - rule [Cexcessblob.owise]: Cexcessblob(_, _, _ )=> 0 [owise] + rule [Cexcessblob.owise]: Cexcessblob(_, _, _) => 0 [owise] + + rule [Cdelegationaccess]: Cdelegationaccess(SCHED, true, ISWARM) => Caddraccess(SCHED, ISWARM) + rule [Cdelegationaccess.owise]: Cdelegationaccess(_, _, _) => 0 [owise] syntax Int ::= #fakeExponential(Int, Int, Int) [symbol(#fakeExponential), function] | #fakeExponential(Int, Int, Int, Int, Int) [function] diff --git a/kevm-pyk/src/tests/utils.py b/kevm-pyk/src/tests/utils.py index 2602a18a1e..d0be9e36a6 100644 --- a/kevm-pyk/src/tests/utils.py +++ b/kevm-pyk/src/tests/utils.py @@ -40,6 +40,7 @@ def _assert_exit_code_zero(pattern: Pattern) -> None: return pretty = kore_print(pattern, definition_dir=kdist.get('evm-semantics.llvm'), output=PrintOutput.PRETTY) + print(pretty) assert pretty == GOLDEN diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index 0960547693..d97ff0bfcf 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1695,11 +1695,7 @@ blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requ 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_single_consolidation_request_from_eoa] blockchain_tests/prague/eip7251_consolidations/contract_deployment/system_contract_deployment.json,* blockchain_tests/prague/eip7623_increase_calldata_cost/execution_gas/gas_consumption_below_data_floor.json,* -blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_EQUAL_TO_DATA_FLOOR] -blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_GREATER_THAN_DATA_FLOOR] blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_LESS_THAN_DATA_FLOOR] -blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY|STORAGE_CLEAR-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_EQUAL_TO_DATA_FLOOR] -blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY|STORAGE_CLEAR-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_GREATER_THAN_DATA_FLOOR] blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.AUTHORIZATION_EXISTING_AUTHORITY|STORAGE_CLEAR-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_LESS_THAN_DATA_FLOOR] blockchain_tests/prague/eip7623_increase_calldata_cost/refunds/gas_refunds_from_data_floor.json,tests/prague/eip7623_increase_calldata_cost/test_refunds.py::test_gas_refunds_from_data_floor[fork_Prague-blockchain_test_from_state_test-refund_type_RefundType.STORAGE_CLEAR-refund_test_type_RefundTestType.EXECUTION_GAS_MINUS_REFUND_LESS_THAN_DATA_FLOOR] blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_0.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_0[fork_Prague-blockchain_test_from_state_test--type_0-protected-exact_gas-floor_gas_greater_than_intrinsic_gas] @@ -1792,7 +1788,48 @@ blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/tran blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_3.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_3[fork_Prague-blockchain_test_from_state_test-type_3-single_blob-single_access_list_single_storage_key-exact_gas-floor_gas_greater_than_intrinsic_gas] blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_3.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_3[fork_Prague-blockchain_test_from_state_test-type_3-single_blob-single_access_list_single_storage_key-extra_gas-floor_gas_greater_than_intrinsic_gas] blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_3.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_3[fork_Prague-blockchain_test_from_state_test-type_3-single_blob-single_access_list_single_storage_key-insufficient_gas-floor_gas_greater_than_intrinsic_gas] -blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,* +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_multiple_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_multiple_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_multiple_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_no_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_no_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_no_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_single_storage_key-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_single_storage_key-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-multiple_access_lists_single_storage_key-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-no_access_list-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-no_access_list-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-no_access_list-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_multiple_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_multiple_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_multiple_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_no_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_no_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_no_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_single_storage_key-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_single_storage_key-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-multiple_authorizations-single_access_list_single_storage_key-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_multiple_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_multiple_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_multiple_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_no_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_no_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_no_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_single_storage_key-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_single_storage_key-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-multiple_access_lists_single_storage_key-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-no_access_list-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-no_access_list-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-no_access_list-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_multiple_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_multiple_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_multiple_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_no_storage_keys-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_no_storage_keys-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_no_storage_keys-insufficient_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_single_storage_key-exact_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_single_storage_key-extra_gas-floor_gas_greater_than_intrinsic_gas] +blockchain_tests/prague/eip7623_increase_calldata_cost/transaction_validity/transaction_validity_type_4.json,tests/prague/eip7623_increase_calldata_cost/test_transaction_validity.py::test_transaction_validity_type_4[fork_Prague-blockchain_test_from_state_test-type_4-single_authorization-single_access_list_single_storage_key-insufficient_gas-floor_gas_greater_than_intrinsic_gas] blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/invalid_deposit_withdrawal_consolidation_requests.json,* blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_request_from_same_tx.json,* blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-consolidation_from_contract+deposit_from_contract+withdrawal_from_contract] @@ -1821,75 +1858,82 @@ blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/ blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+deposit_from_eoa+consolidation_from_eoa] blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+deposit_from_eoa+withdrawal_from_contract] blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+withdrawal_from_contract+deposit_from_contract] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,* -blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,* -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,* -blockchain_tests/prague/eip7702_set_code_tx/gas/self_set_code_cost.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/call_pointer_to_created_from_create_after_oog_call_again.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/call_to_precompile_in_pointer_context.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/contract_storage_to_pointer_with_storage.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,* +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_empty_account_then_contract_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_empty_account_then_contract_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_self_sponsored_then_contract_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_self_sponsored_then_contract_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_then_contract_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_then_contract_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_multiple_signers-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_multiple_signers-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_single_signer-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_single_signer-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-pre_authorized_eoa_authority_no_re_authorization_self_sponsored-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-pre_authorized_eoa_authority_no_re_authorization_self_sponsored-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_invalid_nonce_authorization_single_signer-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_invalid_nonce_authorization_single_signer-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_authorization_invalid_contract_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_authorization_invalid_contract_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority-check_delegated_account_first_False] +blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority-check_delegated_account_first_True] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-many_valid_authorizations_multiple_signers] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-many_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-many_valid_authorizations_multiple_signers] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-many_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_eoa_self_sponsored_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-single_valid_re_authorization_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-many_valid_authorizations_multiple_signers] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-many_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_eoa_self_sponsored_authority] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_single_signer] +blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-single_valid_re_authorization_eoa_authority] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_A-first_delegation_DelegationTo.CONTRACT_A] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_A-first_delegation_DelegationTo.CONTRACT_B] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_B-first_delegation_DelegationTo.CONTRACT_A] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_B-first_delegation_DelegationTo.CONTRACT_B] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.RESET-first_delegation_DelegationTo.CONTRACT_A] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.RESET-first_delegation_DelegationTo.CONTRACT_B] blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/eoa_init_as_pointer.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_call_followed_by_direct_call.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_contract_pointer_loop.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_measurements.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_normal.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_reentry.json,* +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_BOTH_TX] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_NORMAL_TX_ONLY] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_POINTER_TX_ONLY] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.NONE] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.POINTER_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_NORMAL_TX_ONLY] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.POINTER_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.NONE] blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_resets_an_empty_code_account_with_storage.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_reverts.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_precompile.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_static_reentry.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_static.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/static_to_pointer.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/address_from_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/authorization_reusing_nonce.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/call_into_chain_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/call_into_self_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_and_set.json,* +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_pointer_to_precompile[fork_Prague-precompile_0x0000000000000000000000000000000000000002-blockchain_test_from_state_test] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_and_set.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_and_set[fork_Prague-blockchain_test_from_state_test-delegated_account] blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_failing_tx.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,* +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_tx_to[fork_Prague-blockchain_test_from_state_test-delegated_account-not_self_sponsored] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_tx_to[fork_Prague-blockchain_test_from_state_test-delegated_account-self_sponsored] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing[fork_Prague-blockchain_test_from_state_test-delegated_account-not_self_sponsored] +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing[fork_Prague-blockchain_test_from_state_test-delegated_account-self_sponsored] blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/eoa_tx_after_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_chain_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_self_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_self_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/ext_code_on_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/many_delegations.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_overflow_after_first_authorization.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,* +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,"tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=0,account_nonce=1]" +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,"tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=1,account_nonce=0]" +blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=2**64-1] blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/reset_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/self_code_on_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/self_sponsored_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_address_and_authority_warm_state_call_types.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_address_and_authority_warm_state.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_all_invalid_authorization_tuples.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_call_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_max_depth_call_stack.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_first_valid_authorization_tuples_same_signer.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_first_invalid_same_signer.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_same_signer_increasing_nonce_self_sponsored.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_same_signer_increasing_nonce.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_account_deployed_in_same_tx.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_contract_creator.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_log.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_non_empty_storage_non_zero_nonce.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_precompile.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_self_caller.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_self_destruct.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_self_destructing_account_deployed_in_same_tx.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_sstore_then_sload.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_sstore.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_system_contract.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_tstore_available_at_correct_address.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_tstore_reentry.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_using_chain_specific_id.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_using_valid_synthetic_signatures.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/signature_s_out_of_range.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/tx_into_chain_delegating_set_code.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/tx_into_self_delegating_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/valid_tx_invalid_auth_signature.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/valid_tx_invalid_chain_id.json,* blockchain_tests/shanghai/eip3860_initcode/initcode/contract_creating_tx.json,tests/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Prague-blockchain_test_from_state_test-max_size_ones] blockchain_tests/shanghai/eip3860_initcode/initcode/contract_creating_tx.json,tests/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Prague-blockchain_test_from_state_test-max_size_zeros] blockchain_tests/shanghai/eip3860_initcode/initcode/create_opcode_initcode.json,tests/shanghai/eip3860_initcode/test_initcode.py::TestCreateInitcode::test_create_opcode_initcode[fork_Prague-blockchain_test_from_state_test-create-49120_bytes] From bead956c7acf02420b29bd147f6194aad159c5c3 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Mon, 26 May 2025 19:57:50 +0300 Subject: [PATCH 7/8] update expected output in unit tests --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k | 4 ++-- tests/failing/ContractCreationSpam_d0g0v0.json.expected | 3 +++ ..._callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected | 3 +++ tests/specs/functional/infinite-gas-spec.k | 4 ++-- 4 files changed, 10 insertions(+), 4 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k index 221528a759..e6a8306d8d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/lemmas/lemmas.k @@ -158,10 +158,10 @@ module LEMMAS-WITHOUT-SLOT-UPDATES [symbolic] rule 0 <=Int Csstore(_, _, _, _) => true [simplification] rule 0 <=Int Cgascap(_, _:Int, _:Int, _) => true [simplification] rule 0 <=Int #allBut64th(_:Int) => true [simplification] - rule 0 <=Int Cextra(_, _, _, _) => true [simplification] + rule 0 <=Int Cextra(_, _, _, _, _, _) => true [simplification] rule 0 <=Int _:ScheduleConst < _:Schedule > => true [simplification] rule 0 <=Int G up/Int I => true requires 0 <=Int G andBool 0 true [simplification] + rule Cextra(_, _, _, _, _, _) true [simplification] rule G false requires Gsload < SCHED > <=Int G diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index 2166b31441..919580a197 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -337,6 +337,9 @@ .List + + .List + diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected index d4aa7e29a6..4a98068400 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -383,6 +383,9 @@ .List + + .List + diff --git a/tests/specs/functional/infinite-gas-spec.k b/tests/specs/functional/infinite-gas-spec.k index d0aacd73e0..6b40b995b0 100644 --- a/tests/specs/functional/infinite-gas-spec.k +++ b/tests/specs/functional/infinite-gas-spec.k @@ -73,8 +73,8 @@ module INFINITE-GAS-SPEC claim [gas.inf.13]: runLemma( #gas(VGAS +Int -6113) +Gas Cgascap(ISTANBUL, #gas(VGAS +Int -5413), #gas(VGAS +Int -5413), 700)) => doneLemma(#gas((VGAS +Int Cgascap(ISTANBUL, VGAS +Int -5413, VGAS +Int -5413, 700)) +Int -6113)) ... - claim [gas.inf.14]: runLemma( Cgascap(ISTANBUL, #gas(VGas +Int -2924), #gas(VGas +Int -2924), Cextra(ISTANBUL, ISEMPTY, VALUE, ISWARM)) ) - => doneLemma( #gas(Cgascap(ISTANBUL, (VGas +Int -2924), (VGas +Int -2924), Cextra(ISTANBUL, ISEMPTY, VALUE, ISWARM))) ) ... + claim [gas.inf.14]: runLemma( Cgascap(ISTANBUL, #gas(VGas +Int -2924), #gas(VGas +Int -2924), Cextra(ISTANBUL, ISEMPTY, VALUE, ISWARM, ISDELEGATED, ISWARMDELEGATED)) ) + => doneLemma( #gas(Cgascap(ISTANBUL, (VGas +Int -2924), (VGas +Int -2924), Cextra(ISTANBUL, ISEMPTY, VALUE, ISWARM, ISDELEGATED, ISWARMDELEGATED))) ) ... // Infinite Gas comparisons // ------------------------ From 4e8a2acd1b120bd4b1cadb8c07c3543d072bfa89 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 29 May 2025 00:44:25 +0300 Subject: [PATCH 8/8] refactor delegation processing in driver.md --- .../kevm_pyk/kproj/evm-semantics/driver.md | 77 +++++++++++-------- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 10 ++- .../kproj/evm-semantics/state-utils.md | 11 ++- tests/execution-spec-tests/failing.llvm | 67 +--------------- 4 files changed, 60 insertions(+), 105 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md index 85334b4ddb..0ab15f633c 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -117,7 +117,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a syntax EthereumCommand ::= loadTx ( Account ) [symbol(loadTx)] // -------------------------------------------------------------- rule loadTx(_) => startTx ... - _ => EVMC_OUT_OF_GAS + _ => EVMC_INVALID_BLOCK ListItem(TXID:Int) REST => REST SCHED @@ -207,18 +207,8 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a requires ACCTTO =/=K .Account andBool #isValidTransaction(TXID, ACCTFROM) - rule loadTx(ACCTFROM) => startTx ... - _ => EVMC_INVALID_BLOCK - ListItem(_TXID:Int) REST => REST - - ACCTFROM - ACCTCODE - ... - - requires notBool ACCTCODE ==K .Bytes - rule loadTx(_) => startTx ... - _ => EVMC_OUT_OF_GAS + _ => EVMC_INVALID_BLOCK ListItem(_TXID:Int) REST => REST [owise] syntax EthereumCommand ::= "#finishTx" @@ -294,55 +284,76 @@ Processing SetCode Transaction Authority Entries - Creates new accounts when needed ```k - syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] | "#DBG1" | "#DBG2" + syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)] // -------------------------------------------------------------------------- - rule #loadAuthorities ( AUTH ) => .K ... + rule #loadAuthorities(_) => .K ... ListItem(TXID:Int) ... TXID TXTYPE ... - requires (notBool TXTYPE ==K SetCode) - orBool AUTH ==K .List + requires notBool TXTYPE ==K SetCode + + rule #loadAuthorities( .List ) => .K ... + ListItem(TXID:Int) ... + + TXID + SetCode + ... + rule #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST ) - => #addAuthority (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR, true) + => #setDelegation (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR) ~> #loadAuthorities (REST) ... + ListItem(TXID:Int) ... + + TXID + SetCode + ... + GLIMIT => GLIMIT -Int 25000 [owise] - syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes, Bool ) [symbol(#addAuthority)] + syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes ) [symbol(#setDelegation)] + // ------------------------------------------------------------------------------------------------- + rule #setDelegation(.Account , _, _, _) => .K ... + + rule #setDelegation(AUTHORITY, CID, _NONCE, _ADDR) => .K ... ENV_CID + requires notBool AUTHORITY ==K .Account + andBool notBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) + + rule #setDelegation(AUTHORITY, CID, NONCE, ADDR) + => #let EXISTS = #accountExists(AUTHORITY) + #in (#if EXISTS #then .K #else #newAccount AUTHORITY #fi + ~> #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY + ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, EXISTS)) + ... + [owise] + + syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes , Bool) [symbol(#addAuthority)] // ----------------------------------------------------------------------------------------------------- - rule #addAuthority(AUTHORITY, CID, NONCE, _ADDR, _EXISTS) => .K ... - ENV_CID + rule #addAuthority(AUTHORITY, _CID, NONCE, _ADDR, _EXISTS) => .K ... AUTHORITY ACCTCODE ACCTNONCE ... - requires notBool ( AUTHORITY =/=K .Account - andBool (#range(ACCTCODE,0,3) ==K EOA_DELEGATION_MARKER orBool ACCTCODE ==K .Bytes) - andBool #asWord(NONCE) ==Int ACCTNONCE - andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) ) + requires notBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) + orBool notBool (#asWord(NONCE) ==K ACCTNONCE) - rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, EXISTS) => #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY ... - ENV_CID + rule #addAuthority(AUTHORITY, _CID, NONCE, ADDR, EXISTS) => .K ... SCHED REFUND => #if EXISTS #then REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > #else REFUND #fi AUTHORITY - ACCTCODE => #if notBool #asWord(ADDR) ==Int 0 #then EOA_DELEGATION_MARKER +Bytes ADDR #else .Bytes #fi + ACCTCODE => #if #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi ACCTNONCE => ACCTNONCE +Int 1 ... - requires AUTHORITY =/=K .Account - andBool (ACCTCODE ==K .Bytes orBool notBool #isValidDelegation(ACCTCODE)) - andBool #asWord(NONCE) ==Int ACCTNONCE - andBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)) - - rule #addAuthority(AUTHORITY, CID, NONCE, ADDR, _EXISTS) => #newAccount AUTHORITY ~> #addAuthority(AUTHORITY, CID, NONCE, ADDR, false) ... [owise] + requires (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE)) + andBool #asWord(NONCE) ==K ACCTNONCE ``` - `exception` only clears from the `` cell if there is an exception preceding it. diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index cccba3a029..514fc56564 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -3051,11 +3051,11 @@ Account helper functions ======================== - `#getAccountCode(Account)` - K function to retrieve the code of an account, returning the empty bytes object if the account is not in the state. - + - `#accountExists(Account)` - Function that checks if an account is present in the state. ```k syntax Bytes ::= #getAccountCode ( Account ) [symbol(#getAccountCode), function, total] // --------------------------------------------------------------------------------------- - rule [[ #getAccountCode(ACCT) => CODE]] + rule [[ #getAccountCode(ACCT) => CODE ]] ACCT CODE @@ -3063,6 +3063,12 @@ Account helper functions rule #getAccountCode(_) => .Bytes [owise] + + syntax Bool ::= #accountExists ( Account ) [symbol(#accountExists), function, total] + // ------------------------------------------------------------------------------------ + rule [[ #accountExists(ACCT) => true ]] ACCT ... + rule #accountExists(_) => false [owise] + ``` EVM Program Representations diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md index a7c9bed121..26201801ec 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md @@ -600,6 +600,7 @@ The `"rlp"` key loads the block information. syntax Bool ::= #isValidTransaction( Int , Account ) [symbol(#isValidTransaction), function] // -------------------------------------------------------------------------------------------- rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] + SCHED BASE_FEE BLOCK_GAS_LIMIT @@ -621,7 +622,7 @@ The `"rlp"` key loads the block information. SetCode ... - requires ACCTCODE ==K .Bytes + requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>) andBool notBool ACCTTO ==K .Account andBool ACCTNONCE ==Int TX_NONCE andBool BASE_FEE <=Int TX_MAX_FEE @@ -655,7 +656,7 @@ The `"rlp"` key loads the block information. Blob ... - requires ACCTCODE ==K .Bytes + requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>) andBool notBool ACCTTO ==K .Account andBool ACCTNONCE ==Int TX_NONCE andBool BASE_FEE <=Int TX_MAX_FEE @@ -667,6 +668,7 @@ The `"rlp"` key loads the block information. andBool Ctotalblob(SCHED, size(TVH)) <=Int Gmaxblobgas < SCHED> rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] + SCHED BASE_FEE BLOCK_GAS_LIMIT @@ -686,7 +688,7 @@ The `"rlp"` key loads the block information. DynamicFee ... - requires ACCTCODE ==K .Bytes + requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>) andBool ACCTNONCE ==Int TX_NONCE andBool BASE_FEE <=Int TX_MAX_FEE andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE @@ -694,6 +696,7 @@ The `"rlp"` key loads the block information. andBool TX_GAS_LIMIT <=Int BLOCK_GAS_LIMIT rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]] + SCHED BASE_FEE BLOCK_GAS_LIMIT @@ -713,7 +716,7 @@ The `"rlp"` key loads the block information. ... requires #dasmTxPrefix(TXTYPE) >) andBool ACCTNONCE ==Int TX_NONCE andBool BASE_FEE <=Int TX_GAS_PRICE andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index d97ff0bfcf..c41aede277 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1858,82 +1858,17 @@ blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/ blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+deposit_from_eoa+consolidation_from_eoa] blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+deposit_from_eoa+withdrawal_from_contract] blockchain_tests/prague/eip7685_general_purpose_el_requests/multi_type_requests/valid_deposit_withdrawal_consolidation_requests.json,tests/prague/eip7685_general_purpose_el_requests/test_multi_type_requests.py::test_valid_deposit_withdrawal_consolidation_requests[fork_Prague-blockchain_test-withdrawal_from_eoa+withdrawal_from_contract+deposit_from_contract] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_empty_account_then_contract_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_empty_account_then_contract_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_self_sponsored_then_contract_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_self_sponsored_then_contract_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_then_contract_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_authorizations_eoa_then_contract_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_multiple_signers-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_multiple_signers-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_single_signer-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_invalid_nonce_authorizations_single_signer-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-pre_authorized_eoa_authority_no_re_authorization_self_sponsored-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-pre_authorized_eoa_authority_no_re_authorization_self_sponsored-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_invalid_nonce_authorization_single_signer-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_invalid_nonce_authorization_single_signer-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_authorization_invalid_contract_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_authorization_invalid_contract_authority-check_delegated_account_first_True] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority-check_delegated_account_first_False] -blockchain_tests/prague/eip7702_set_code_tx/gas/account_warming.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_account_warming[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority-check_delegated_account_first_True] blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-many_valid_authorizations_multiple_signers] blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-many_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_eoa_self_sponsored_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-multiple_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_gas_cost[fork_Prague-blockchain_test_from_state_test-single_valid_re_authorization_eoa_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-many_valid_authorizations_multiple_signers] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-many_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_eoa_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_eoa_self_sponsored_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-multiple_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_False-single_valid_re_authorization_eoa_authority] blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-many_valid_authorizations_multiple_signers] blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-many_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_eoa_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_eoa_self_sponsored_authority] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-multiple_valid_authorizations_single_signer] -blockchain_tests/prague/eip7702_set_code_tx/gas/intrinsic_gas_cost.json,tests/prague/eip7702_set_code_tx/test_gas.py::test_intrinsic_gas_cost[fork_Prague-blockchain_test_from_state_test-valid_True-single_valid_re_authorization_eoa_authority] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_A-first_delegation_DelegationTo.CONTRACT_A] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_A-first_delegation_DelegationTo.CONTRACT_B] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_B-first_delegation_DelegationTo.CONTRACT_A] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.CONTRACT_B-first_delegation_DelegationTo.CONTRACT_B] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.RESET-first_delegation_DelegationTo.CONTRACT_A] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/double_auth.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_double_auth[fork_Prague-blockchain_test_from_state_test-second_delegation_DelegationTo.RESET-first_delegation_DelegationTo.CONTRACT_B] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/eoa_init_as_pointer.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_BOTH_TX] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_NORMAL_TX_ONLY] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_POINTER_TX_ONLY] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.CONTRACT_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.NONE] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.POINTER_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.IN_NORMAL_TX_ONLY] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/gas_diff_pointer_vs_direct_call.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_gas_diff_pointer_vs_direct_call[fork_Prague-blockchain_test-access_list_to_AccessListTo.POINTER_ADDRESS-pointer_definition_PointerDefinition.IN_BOTH_TX-access_list_rule_AccessListCall.NONE] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_resets_an_empty_code_account_with_storage.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs_2/pointer_to_precompile.json,tests/prague/eip7702_set_code_tx/test_set_code_txs_2.py::test_pointer_to_precompile[fork_Prague-precompile_0x0000000000000000000000000000000000000002-blockchain_test_from_state_test] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_and_set.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_and_set[fork_Prague-blockchain_test_from_state_test-delegated_account] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_failing_tx.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_tx_to[fork_Prague-blockchain_test_from_state_test-delegated_account-not_self_sponsored] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing_tx_to.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing_tx_to[fork_Prague-blockchain_test_from_state_test-delegated_account-self_sponsored] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing[fork_Prague-blockchain_test_from_state_test-delegated_account-not_self_sponsored] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/delegation_clearing.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_delegation_clearing[fork_Prague-blockchain_test_from_state_test-delegated_account-self_sponsored] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/eoa_tx_after_set_code.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/many_delegations.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_overflow_after_first_authorization.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,"tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=0,account_nonce=1]" -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,"tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=1,account_nonce=0]" blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/nonce_validity.json,tests/prague/eip7702_set_code_tx/test_set_code_txs.py::test_nonce_validity[fork_Prague-blockchain_test_from_state_test-nonce=2**64-1] -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/reset_code.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/set_code_multiple_valid_authorization_tuples_first_invalid_same_signer.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_same_signer_increasing_nonce_self_sponsored.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_multiple_valid_authorization_tuples_same_signer_increasing_nonce.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_to_sstore_then_sload.json,* blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_using_valid_synthetic_signatures.json,* -blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/valid_tx_invalid_auth_signature.json,* blockchain_tests/shanghai/eip3860_initcode/initcode/contract_creating_tx.json,tests/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Prague-blockchain_test_from_state_test-max_size_ones] blockchain_tests/shanghai/eip3860_initcode/initcode/contract_creating_tx.json,tests/shanghai/eip3860_initcode/test_initcode.py::test_contract_creating_tx[fork_Prague-blockchain_test_from_state_test-max_size_zeros] blockchain_tests/shanghai/eip3860_initcode/initcode/create_opcode_initcode.json,tests/shanghai/eip3860_initcode/test_initcode.py::TestCreateInitcode::test_create_opcode_initcode[fork_Prague-blockchain_test_from_state_test-create-49120_bytes]