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 b43471d28d..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
@@ -132,6 +132,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
=> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
+ ~> #loadAuthorities(AUTH)
~> #checkCreate ACCTFROM VALUE
~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
~> #finishTx ~> #finalizeTx(false) ~> startTx
@@ -145,12 +146,13 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
ListItem(TXID:Int) ...
MINER
- TXID
- GLIMIT
- .Account
- VALUE
- CODE
- TA
+ TXID
+ GLIMIT
+ .Account
+ VALUE
+ CODE
+ TA
+ AUTH
...
@@ -169,6 +171,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
~> #deductBlobGas
~> #loadAccessList(TA)
+ ~> #loadAuthorities(AUTH)
~> #checkCall ACCTFROM VALUE
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
~> #finishTx ~> #finalizeTx(false) ~> startTx
@@ -189,6 +192,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
DATA
TA
TVH
+ AUTH
...
_ => TVH
@@ -203,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"
@@ -275,6 +269,93 @@ 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)]
+ // --------------------------------------------------------------------------
+ rule #loadAuthorities(_) => .K ...
+ ListItem(TXID:Int) ...
+
+ TXID
+ TXTYPE
+ ...
+
+ 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 )
+ => #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 ::= #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 ...
+
+ AUTHORITY
+ ACCTCODE
+ ACCTNONCE
+ ...
+
+ requires notBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE))
+ orBool notBool (#asWord(NONCE) ==K ACCTNONCE)
+
+ 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 #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi
+ ACCTNONCE => ACCTNONCE +Int 1
+ ...
+
+ 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.
- `failure_` holds the name of a test that failed if a test does fail.
- `success` sets the `` to `0` and the `` to `SUCCESS`.
@@ -654,6 +735,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 07c24cb70f..182f371a4d 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
@@ -443,7 +443,8 @@ Productions related to transactions
| "AccessList"
| "DynamicFee"
| "Blob"
- // ------------------------
+ | "SetCode"
+ // ---------------------------
syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function]
// -------------------------------------------------------------------------
@@ -451,6 +452,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]
// -----------------------------------------------------------------------
@@ -458,15 +460,16 @@ 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: Account, 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: List) [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 e37b4ff803..514fc56564 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
@@ -176,6 +176,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
.TxType // T_x
0
.List
+ .List
@@ -1583,6 +1584,22 @@ 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
+ => #let DELEGATED_ACCOUNT = #getDelegatedAccount(CODE) #in
+ (#accessAccounts DELEGATED_ACCOUNT
+ ~> #callWithCode ACCTFROM ACCTTO ACCTCODE #getAccountCode(DELEGATED_ACCOUNT) VALUE APPVALUE ARGS STATIC )
+ ...
+
+ SCHED
+
+ ACCTCODE
+ 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
@@ -1593,6 +1610,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
@@ -2756,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
@@ -2773,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
@@ -2782,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
@@ -2939,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) ...
@@ -2969,6 +2989,88 @@ There are several helpers for calculating gas (most of them also specified in th
rule #accountNonexistent(_) => true ... [owise]
```
+Processing SetCode Transaction Authority Entries
+================================================
+ - `#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 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 ::= #accountHasAuthority ( Account ) [symbol(#accountHasAuthority), function, total]
+ // ------------------------------------------------------------------------------------------------
+ rule [[#accountHasAuthority(ACCTTO) => true]]
+
+ ACCTTO
+ CODE
+ ...
+
+ requires #isValidDelegation(CODE)
+
+ rule #accountHasAuthority(_) => false[owise]
+
+ syntax Bool ::= #accountAuthorityIsWarm ( Account ) [symbol(#accountAuthorityIsWarm), function, total]
+ // ------------------------------------------------------------------------------------------------------
+ rule [[#accountAuthorityIsWarm(ACCTTO) => true]]
+
+ ACCTTO
+ CODE
+ ...
+
+ ACCTS
+ requires #isValidDelegation(CODE)
+ andBool (#asAccount(#range(CODE,3,20)) in ACCTS orBool #asAccount(#range(CODE,3,20)) ==K ACCTTO)
+
+ rule #accountAuthorityIsWarm(_) => 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]
+ // -------------------------------------------------------------------------------------------
+ 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]
+```
+
+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 ]]
+
+ ACCT
+ CODE
+ ...
+
+
+ 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/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/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/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
index dd13372764..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"
// -----------------------------------------------------------------
```
@@ -52,7 +52,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
| "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore"
| "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction"
| "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul"
- | "Gbls12PairingCheckAdd" | "Gbls12mapfp2tog2"
+ | "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```
@@ -86,6 +86,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
@@ -177,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
@@ -463,6 +465,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [Gbls12PairingCheckAddPrague]: Gbls12PairingCheckAdd < PRAGUE > => 37700
rule [Gbls12mapfptog1Prague]: Gbls12mapfptog1 < PRAGUE > => 5500
rule [Gbls12mapfp2tog2Prague]: Gbls12mapfp2tog2 < PRAGUE > => 23800
+ rule [GauthbasePrague]: Gauthbase < PRAGUE > => 12500
rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
requires notBool ( SCHEDCONST ==K Gmaxblobgas
orBool SCHEDCONST ==K Gtargetblobgas
@@ -474,15 +477,18 @@ A `ScheduleConst` is a constant determined by the fee schedule.
orBool SCHEDCONST ==K Gbls12PairingCheckMul
orBool SCHEDCONST ==K Gbls12PairingCheckAdd
orBool SCHEDCONST ==K Gbls12mapfptog1
- orBool SCHEDCONST ==K Gbls12mapfp2tog2 )
+ orBool SCHEDCONST ==K Gbls12mapfp2tog2
+ orBool SCHEDCONST ==K Gauthbase )
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 8785f6472d..d1ab50d9b3 100644
--- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
+++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
@@ -211,7 +211,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.
@@ -314,6 +315,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)
@@ -430,6 +432,9 @@ Encoding
rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) )
=> #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA], TB, [#parseList2JSONs(TVH)] ] )
+ 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]
// ---------------------------------------------------------------------------------------------
rule #rlpEncodeMerkleTree ( .MerkleTree ) => b"\x80"
@@ -779,5 +784,23 @@ Tree Root Helper Functions
+Bytes #rlpEncodeBytes( #parseByteStack( Keccak256(b"") ) )
, 192
)
+```
+
+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]
+ // ----------------------------------------------------------------------
+ rule SET_CODE_TX_MAGIC => b"\x05"
+ 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 667a9ebc51..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
@@ -201,6 +201,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.
@@ -391,6 +392,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 ...
@@ -442,7 +455,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
@@ -531,6 +547,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
@@ -566,6 +599,38 @@ The `"rlp"` key loads the block information.
```k
syntax Bool ::= #isValidTransaction( Int , Account ) [symbol(#isValidTransaction), function]
// --------------------------------------------------------------------------------------------
+ rule [[ #isValidTransaction (TXID, ACCTFROM) => true ]]
+ SCHED
+ 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 orBool Ghasauthority << SCHED >>)
+ 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
@@ -591,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
@@ -603,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
@@ -622,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
@@ -630,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
@@ -649,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/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 dfdcd6d866..c41aede277 100644
--- a/tests/execution-spec-tests/failing.llvm
+++ b/tests/execution-spec-tests/failing.llvm
@@ -1694,14 +1694,8 @@ 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]
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]
@@ -1794,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]
@@ -1823,81 +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,*
-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/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/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,*
-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/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/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/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/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/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/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/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/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,*
-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_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,*
-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]
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
// ------------------------