Skip to content

Commit

Permalink
EIP-4844: Add Blob transaction type (#2690)
Browse files Browse the repository at this point in the history 
* EIP-4844: Add DynamicFee transaction type

* Fix test-integrations

* Set field `to` to be not `nil` in Blob transactions
From the EIP specification: "The field `to` deviates slightly from the semantics with the exception that it *MUST NOT* be `nil` and therefore must always represent a 20-byte address. This means that blob transactions cannot have the form of a create transaction."

* Setting `txVersionedHashes` as `JSONs`
Implementing parsing features for `txVersionedHashes` and `txMaxBlobFee`

* Fromatting

* Fixing `AccountNotNil` as an alias

* Fix typo

Co-authored-by: Andrei Văcaru <[email protected]>

* Fix indentation

Co-authored-by: Andrei Văcaru <[email protected]>

* Fix dash size

Co-authored-by: Andrei Văcaru <[email protected]>

* Fix dash size

Co-authored-by: Andrei Văcaru <[email protected]>

* Fix dash size

Co-authored-by: Andrei Văcaru <[email protected]>

* Fix dash size

Co-authored-by: Andrei Văcaru <[email protected]>

* Deleting `#addrBytesNotNil` and using `#addrBytes({TT}:>Account)` instead

* Fix indentetion and dash size

---------

Co-authored-by: Andrei Văcaru <[email protected]>
  • Loading branch information
@Robertorosmaninho @anvacaru
Robertorosmaninho and anvacaru authored Jan 23, 2025
1 parent f7435ba commit 6cf81f6
Show file tree
Hide file tree
Showing 7 changed files with 106 additions and 20 deletions.
17 changes: 16 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md
View file
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
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
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
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
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
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
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

0 comments on commit 6cf81f6

Please sign in to comment.