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 d53577b5ea..b53dc37b9d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md @@ -397,6 +397,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 @@ -582,7 +583,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 ] ... @@ -593,6 +594,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 ... @@ -606,6 +612,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] @@ -620,6 +627,14 @@ 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 9c1efd77d1..430f17b033 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 @@ -337,6 +337,8 @@ Bytes helper functions - `#asInteger` will interpret a stack of bytes as a single arbitrary-precision integer (with MSB first). - `#asAccount` will interpret a stack of bytes as a single account id (with MSB first). Differs from `#asWord` only in that an empty stack represents the empty account, not account zero. +- `asAccountNotNil` will interpret a stack of bytes as a single account id (with MSB first), but will fail if the + stack is empty. - `#asByteStack` will split a single word up into a `Bytes`. - `#range(WS, N, W)` access the range of `WS` beginning with `N` of width `W`. - `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `Bytes` is the correct size. @@ -350,11 +352,14 @@ Bytes helper functions // ------------------------------------------------------------------------- rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete] - syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] - // ---------------------------------------------------------------------- + syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function] + syntax AccountNotNil ::= #asAccountNotNil ( Bytes ) [symbol(#asAccountNotNil), function] + // ---------------------------------------------------------------------------------------- rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0 rule #asAccount(BS) => #asWord(BS) [owise] + rule #asAccountNotNil(BS) => #asWord(BS) requires lengthBytes(BS) >Int 0 + syntax Bytes ::= #asByteStack ( Int ) [symbol(#asByteStack), function, total] // ----------------------------------------------------------------------------- rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete] @@ -385,7 +390,8 @@ Accounts ```k syntax Account ::= ".Account" | Int - // ----------------------------------- + syntax AccountNotNil = Int + // -------------------------- syntax AccountCode ::= Bytes // ---------------------------- @@ -442,28 +448,32 @@ Productions related to transactions | "Legacy" | "AccessList" | "DynamicFee" - // ------------------------------ + | "Blob" + // ------------------------ syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function] // ------------------------------------------------------------------------- rule #dasmTxPrefix (Legacy) => 0 rule #dasmTxPrefix (AccessList) => 1 rule #dasmTxPrefix (DynamicFee) => 2 + rule #dasmTxPrefix (Blob) => 3 syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function] // ----------------------------------------------------------------------- rule #asmTxPrefix (0) => Legacy rule #asmTxPrefix (1) => AccessList rule #asmTxPrefix (2) => DynamicFee + rule #asmTxPrefix (3) => Blob - syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx - // -------------------------------------------------------- + syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx + // ----------------------------------------------------------------- - 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 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: 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 9e8be97698..e34628b74d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -167,6 +167,8 @@ In the comments next to each cell, we've marked which component of the YellowPap 0 // T_f 0 // T_m .TxType // T_x + 0 + [ .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 13a582cb6c..f6ae417b26 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md @@ -141,7 +141,8 @@ The encoding schemes are applied in `#rlpEcondeTxData`. rule #hashTxData( TXDATA ) => Keccak256raw( #rlpEncodeTxData(TXDATA) ) requires isLegacyTx (TXDATA) 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) +``` 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. @@ -228,6 +229,7 @@ Unparsing ``` - `#addrBytes` Takes an Account and represents it as a 20-byte wide Bytes (or an empty Bytes for a null address) +- `#addrBytesNotNil` Takes an Account and represents it as a 20-byte wide Bytes. It throws an error if the account is null. - `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes ```k @@ -349,6 +351,9 @@ 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, #addrBytes({TT}:>Account), 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 22410352e1..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 @@ -426,6 +449,25 @@ The `"rlp"` key loads the block information. DynamicFee ... + + rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] + + TXID + TN + TP + TG + TT + TV + DATA + CID + TA + TPF + TM + TB + TVH + Blob + ... + ``` - `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559 diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index cbb2b47964..d0a29be279 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -319,6 +319,12 @@ Legacy + + 0 + + + [ .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 e8d4d81c45..2ad735c760 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -365,6 +365,12 @@ Legacy + + 0 + + + [ .JSONs ] +