Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

EIP-4844: Add Blob transaction type #2690

Merged
merged 17 commits into from
Jan 23, 2025
Merged

EIP-4844: Add Blob transaction type #2690

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
17 commits
Select commit Hold shift + click to select a range
4ac42c7
EIP-4844: Add DynamicFee transaction type
Robertorosmaninho Jan 21, 2025
189b694
Fix test-integrations
Robertorosmaninho Jan 21, 2025
1aec9d4
Set field `to` to be not `nil` in Blob transactions
Robertorosmaninho Jan 21, 2025
93142fc
Merge branch 'master' into pi2/robertorosmaninho/eip-4844
Robertorosmaninho Jan 21, 2025
71fb9fd
Setting `txVersionedHashes` as `JSONs`
Robertorosmaninho Jan 22, 2025
969520f
Fromatting
Robertorosmaninho Jan 22, 2025
07cecad
Merge branch 'master' into pi2/robertorosmaninho/eip-4844
Robertorosmaninho Jan 22, 2025
c97e10e
Fixing `AccountNotNil` as an alias
Robertorosmaninho Jan 22, 2025
d7c1f5a
Fix typo
Robertorosmaninho Jan 23, 2025
31d7a6d
Fix indentation
Robertorosmaninho Jan 23, 2025
5f51895
Fix dash size
Robertorosmaninho Jan 23, 2025
3dc6e5a
Fix dash size
Robertorosmaninho Jan 23, 2025
3c4b326
Fix dash size
Robertorosmaninho Jan 23, 2025
7827f08
Fix dash size
Robertorosmaninho Jan 23, 2025
791f202
Merge branch 'master' into pi2/robertorosmaninho/eip-4844
Robertorosmaninho Jan 23, 2025
d0deb5d
Deleting `#addrBytesNotNil` and using `#addrBytes({TT}:>Account)` ins…
Robertorosmaninho Jan 23, 2025
db28fab
Fix indentetion and dash size
Robertorosmaninho Jan 23, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
17 changes: 16 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -397,6 +397,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
rule <k> loadTransaction _ { "s" : (TS:Bytes => #padToWidth(32, TS)), _ } ... </k> requires lengthBytes(TS) <Int 32
rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
rule <k> loadTransaction _ { "maxFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
rule <k> loadTransaction _ { "maxFeePerBlobGas" : (V:Bytes => #asWord(V)), _ } ... </k>
```

### Checking State
Expand Down Expand Up @@ -582,7 +583,7 @@ Here we check the other post-conditions associated with an EVM test.
rule <k> check "transactions" : (_KEY : (VALUE:String => #parseByteStack(VALUE))) ... </k>
rule <k> check "transactions" : ("to" : (VALUE:Bytes => #asAccount(VALUE))) ... </k>
rule <k> check "transactions" : ( KEY : (VALUE:Bytes => #padToWidth(32, VALUE))) ... </k> requires KEY in (SetItem("r") SetItem("s")) andBool lengthBytes(VALUE) <Int 32
rule <k> check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas"))
rule <k> check "transactions" : ( KEY : (VALUE:Bytes => #asWord(VALUE))) ... </k> requires KEY in (SetItem("gasLimit") SetItem("gasPrice") SetItem("nonce") SetItem("v") SetItem("value") SetItem("chainId") SetItem("type") SetItem("maxFeePerGas") SetItem("maxPriorityFeePerGas") SetItem("maxFeePerBlobGas"))
rule <k> check "transactions" : ("type" : (VALUE:Int => #asmTxPrefix(VALUE))) ... </k>

rule <k> check "transactions" : "accessList" : [ ACCESSLIST , REST ] => check "transactions" : "accessList" : ACCESSLIST ~> check "transactions" : "accessList" : [ REST ] ... </k>
Expand All @@ -593,6 +594,11 @@ Here we check the other post-conditions associated with an EVM test.
rule <k> check "transactions" : "accessList" : [ .JSONs ] => .K ... </k>

rule <k> check "transactions" : "accessList" : "address" : ADDR : "storageKeys" : KEY => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txAccess> TA </txAccess> ... </message> requires isInAccessList(ADDR, KEY, TA)

rule <k> check "transactions" : "blobVersionedHashes" : [ .JSONs ] => .K ... </k>
rule <k> check "transactions" : "blobVersionedHashes" : [ VHASH, REST ] => check "transactions" : "blobVersionedHashes" : VHASH ~> check "transactions" : "blobVersionedHashes" : [ REST ] ... </k>
rule <k> check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txVersionedHashes> VH </txVersionedHashes> ... </message> requires isInVersionedHashes(VHASH, VH)

rule <k> check "transactions" : ("data" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <data> VALUE </data> ... </message>
rule <k> check "transactions" : ("gasLimit" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasLimit> VALUE </txGasLimit> ... </message>
rule <k> check "transactions" : ("gasPrice" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasPrice> VALUE </txGasPrice> ... </message>
Expand All @@ -606,6 +612,7 @@ Here we check the other post-conditions associated with an EVM test.
rule <k> check "transactions" : ("type" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txType> VALUE </txType> ... </message>
rule <k> check "transactions" : ("maxFeePerGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxFee> VALUE </txMaxFee> ... </message>
rule <k> check "transactions" : ("maxPriorityFeePerGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txPriorityFee> VALUE </txPriorityFee> ... </message>
rule <k> check "transactions" : ("maxFeePerBlobGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxBlobFee> VALUE </txMaxBlobFee> ... </message>
rule <k> check "transactions" : ("sender" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <sigV> TW </sigV> <sigR> TR </sigR> <sigS> TS </sigS> ... </message> <chainID> B </chainID> requires #sender( #getTxData(TXID), TW, TR, TS, B ) ==K VALUE

syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function]
Expand All @@ -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.
Expand Down
32 changes: 21 additions & 11 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand All @@ -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]
Expand Down Expand Up @@ -385,7 +390,8 @@ Accounts

```k
syntax Account ::= ".Account" | Int
// -----------------------------------
syntax AccountNotNil = Int
// --------------------------

syntax AccountCode ::= Bytes
// ----------------------------
Expand Down Expand Up @@ -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
```
2 changes: 2 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -167,6 +167,8 @@ In the comments next to each cell, we've marked which component of the YellowPap
<txPriorityFee> 0 </txPriorityFee> // T_f
<txMaxFee> 0 </txMaxFee> // T_m
<txType> .TxType </txType> // T_x
<txMaxBlobFee> 0 </txMaxBlobFee>
<txVersionedHashes> [ .JSONs ] </txVersionedHashes>
</message>
</messages>

Expand Down
7 changes: 6 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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]
// ---------------------------------------------------------------------------------------------
Expand Down
56 changes: 49 additions & 7 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -276,19 +276,21 @@ 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 ]
...
</k>

rule <k> 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 ]
Expand All @@ -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 ]
...
</k>
requires #asWord(TYPE) ==Int #dasmTxPrefix(DynamicFee)

rule <k> 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 ]
...
</k>
requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob)

syntax EthereumCommand ::= "loadTransaction" Int JSON
// -----------------------------------------------------
rule <k> loadTransaction _ { .JSONs } => .K ... </k>
Expand Down Expand Up @@ -356,6 +373,12 @@ The `"rlp"` key loads the block information.

rule <k> loadTransaction TXID { "maxFeePerGas" : TF:Int, REST => REST } ... </k>
<message> <msgID> TXID </msgID> <txMaxFee> _ => TF </txMaxFee> ... </message>

rule <k> loadTransaction TXID { "maxFeePerBlobGas" : TB:Int, REST => REST } ... </k>
<message> <msgID> TXID </msgID> <txMaxBlobFee> _ => TB </txMaxBlobFee> ... </message>

rule <k> loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... </k>
<message> <msgID> TXID </msgID> <txVersionedHashes> _ => [TVH] </txVersionedHashes> ... </message>
```

### Getting State
Expand Down Expand Up @@ -426,6 +449,25 @@ The `"rlp"` key loads the block information.
<txType> DynamicFee </txType>
...
</message>

rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]]
<message>
<msgID> TXID </msgID>
<txNonce> TN </txNonce>
<txGasPrice> TP </txGasPrice>
<txGasLimit> TG </txGasLimit>
<to> TT </to>
<value> TV </value>
<data> DATA </data>
<txChainID> CID </txChainID>
<txAccess> TA </txAccess>
<txPriorityFee> TPF </txPriorityFee>
<txMaxFee> TM </txMaxFee>
<txMaxBlobFee> TB </txMaxBlobFee>
<txVersionedHashes> TVH </txVersionedHashes>
<txType> Blob </txType>
...
</message>
```

- `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559
Expand Down
6 changes: 6 additions & 0 deletions tests/failing/ContractCreationSpam_d0g0v0.json.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -319,6 +319,12 @@
<txType>
Legacy
</txType>
<txMaxBlobFee>
0
</txMaxBlobFee>
<txVersionedHashes>
[ .JSONs ]
</txVersionedHashes>
</message>
</messages>
</network>
Expand Down
6 changes: 6 additions & 0 deletions tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -365,6 +365,12 @@
<txType>
Legacy
</txType>
<txMaxBlobFee>
0
</txMaxBlobFee>
<txVersionedHashes>
[ .JSONs ]
</txVersionedHashes>
</message>
</messages>
</network>
Expand Down
Loading