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..bb610c60f8 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 @@ -442,6 +442,7 @@ Productions related to transactions | "Legacy" | "AccessList" | "DynamicFee" + | "Blob" // ------------------------------ syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function] @@ -449,20 +450,23 @@ Productions related to transactions 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: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: Bytes ) [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..ddc04cf40c 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 + .Bytes 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..7df1cf75aa 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. @@ -349,6 +350,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), 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..c521bafb93 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 @@ -426,6 +426,25 @@ The `"rlp"` key loads the block information. DynamicFee ... + + rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]] + + TXID + TN + TP + TG + TT + TV + DATA + CID + TA + TP + TF + TB + TVH + Blob + ... + ``` - `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559