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 aec91f92b7..93b6deeb56 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -360,6 +360,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"` rule loadTransaction _ { "s" : (TS:Bytes => #padToWidth(32, TS)), _ } ... requires lengthBytes(TS) loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes => #asWord(V)), _ } ... rule loadTransaction _ { "maxFeePerGas" : (V:Bytes => #asWord(V)), _ } ... + rule loadTransaction _ { "maxFeePerBlobGas" : (V:Bytes => #asWord(V)), _ } ... ``` ### Checking State @@ -545,7 +546,7 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : (_KEY : (VALUE:String => #parseByteStack(VALUE))) ... rule check "transactions" : ("to" : (VALUE:Bytes => #asAccount(VALUE))) ... rule check "transactions" : ( KEY : (VALUE:Bytes => #padToWidth(32, VALUE))) ... requires KEY in (SetItem("r") SetItem("s")) andBool lengthBytes(VALUE) check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas")) + rule check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas") SetItem("maxFeePerBlobGas")) rule check "transactions" : ("type" : (VALUE:Int => #asmTxPrefix(VALUE))) ... rule check "transactions" : "accessList" : [ ACCESSLIST , REST ] => check "transactions" : "accessList" : ACCESSLIST ~> check "transactions" : "accessList" : [ REST ] ... @@ -556,6 +557,11 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : "accessList" : [ .JSONs ] => .K ... rule check "transactions" : "accessList" : "address" : ADDR : "storageKeys" : KEY => .K ... ListItem(TXID) ... TXID TA ... requires isInAccessList(ADDR, KEY, TA) + + rule check "transactions" : "blobVersionedHashes" : [ .JSONs ] => .K ... + rule check "transactions" : "blobVersionedHashes" : [ VHASH, REST ] => check "transactions" : "blobVersionedHashes" : VHASH ~> check "transactions" : "blobVersionedHashes" : [ REST ] ... + rule check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... ListItem(TXID) ... TXID VH ... requires isInVersionedHashes(VHASH, VH) + rule check "transactions" : ("data" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("gasLimit" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("gasPrice" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... @@ -569,6 +575,7 @@ Here we check the other post-conditions associated with an EVM test. rule check "transactions" : ("type" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("maxFeePerGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... rule check "transactions" : ("maxPriorityFeePerGas" : VALUE) => .K ... ListItem(TXID) ... TXID VALUE ... + 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 syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function] @@ -583,6 +590,13 @@ Here we check the other post-conditions associated with an EVM test. rule isInAccessListStorage(KEY, [SKEY, REST]) => #if KEY ==Int #asWord(SKEY) #then true #else isInAccessListStorage(KEY, [REST]) #fi + + // Different from AccessList, Versioned Hashs doesn't contains a list of key-value jsons, but a list of strings finishing in .JSOns like [ "0x01...", "0x02", .JSONs] + syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function] + rule isInVersionedHashes(_, [.JSONs]) => false + rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY + #then true + #else isInVersionedHashes(KEY, [REST]) #fi ``` TODO: case with nonzero ommers. 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 b995f60cad..124566f191 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 @@ -472,7 +472,7 @@ Productions related to transactions | 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: Bytes ) [symbol(BlobTxData)] + syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: AccountNotNil, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: JSONs ) [symbol(BlobTxData)] // ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------- 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 ddc04cf40c..e34628b74d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -168,7 +168,7 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 // T_m .TxType // T_x 0 - .Bytes + [ .JSONs ] 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 1fb06a7cc7..07524b6150 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -354,8 +354,8 @@ Encoding rule #rlpEncodeTxData( DynamicFeeTxData(TN, TF, TM, TG, TT, TV, DATA, TC, [TA]) ) => #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] ) - rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, TVH) ) - => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, TVH ] ) + rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, [TVH]) ) + => #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytesNotNil(TT), TV, DATA, [TA], TB, [TVH] ] ) 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 c521bafb93..a61626e59c 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 @@ -276,7 +276,8 @@ The `"rlp"` key loads the block information. , "nonce" : TN , "r" : TR , "s" : TS , "to" : TT , "v" : TW , "value" : TV , "type" : #dasmTxPrefix(Legacy) , "maxPriorityFeePerGas" : TP - , "maxFeePerGas": TP , .JSONs + , "maxFeePerGas": TP , "maxFeePerBlobGas" : 0 + , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] ... @@ -284,11 +285,12 @@ The `"rlp"` key loads the block information. rule load "transaction" : [ [TYPE , [TC, TN, TP, TG, TT, TV, TI, TA, TY , TR, TS ]] , REST ] => mkTX !ID:Int - ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP - , "nonce" : TN , "r" : TR , "s" : TS - , "to" : TT , "v" : TY , "value" : TV - , "accessList" : TA , "type" : TYPE , "chainID" : TC - , "maxPriorityFeePerGas" : TP , "maxFeePerGas": TP + ~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP + , "nonce" : TN , "r" : TR , "s" : TS + , "to" : TT , "v" : TY , "value" : TV + , "accessList" : TA , "type" : TYPE , "chainID" : TC + , "maxPriorityFeePerGas" : TP , "maxFeePerGas" : TP + , "maxFeePerBlobGas" : 0 , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] @@ -303,13 +305,28 @@ The `"rlp"` key loads the block information. , "nonce" : TN , "r" : TR , "s" : TS , "to" : TT , "v" : TY , "value" : TV , "accessList" : TA , "type" : TYPE , "chainID" : TC - , "maxFeePerGas" : TF , .JSONs + , "maxFeePerGas" : TF , "maxFeePerBlobGas" : 0 + , "blobVersionedHashes" : [ .JSONs ] , .JSONs } ~> load "transaction" : [ REST ] ... requires #asWord(TYPE) ==Int #dasmTxPrefix(DynamicFee) + rule load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TY, TVH, TB, 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 , "maxFeePerBlobGas" : TB , "blobVersionedHashes" : TVH + , .JSONs + } + ~> load "transaction" : [ REST ] + ... + + requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob) + syntax EthereumCommand ::= "loadTransaction" Int JSON // ----------------------------------------------------- rule loadTransaction _ { .JSONs } => .K ... @@ -356,6 +373,12 @@ The `"rlp"` key loads the block information. rule loadTransaction TXID { "maxFeePerGas" : TF:Int, REST => REST } ... TXID _ => TF ... + + rule loadTransaction TXID { "maxFeePerBlobGas" : TB:Int, REST => REST } ... + TXID _ => TB ... + + rule loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... + TXID _ => [TVH] ... ``` ### Getting State @@ -427,7 +450,7 @@ The `"rlp"` key loads the block information. ... - rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] + rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] TXID TN @@ -438,10 +461,10 @@ The `"rlp"` key loads the block information. DATA CID TA - TP - TF - TB - TVH + TPF + TM + TB + TVH Blob ... diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index 0e4f7eb1d4..d0a29be279 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -323,7 +323,7 @@ 0 - b"" + [ .JSONs ] 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 5a4dc876c7..2ad735c760 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -369,7 +369,7 @@ 0 - b"" + [ .JSONs ]