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 7 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
16 changes: 15 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 @@ -392,6 +392,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 @@ -577,7 +578,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 @@ -588,6 +589,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 @@ -601,6 +607,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 @@ -615,6 +622,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]
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
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
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
```

TODO: case with nonzero ommers.
Expand Down
24 changes: 17 additions & 7 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]
// ----------------------------------------------------------------------
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
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,6 +390,7 @@ Accounts

```k
syntax Account ::= ".Account" | Int
syntax AccountNotNil ::= Int
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
// -----------------------------------

syntax AccountCode ::= Bytes
Expand Down Expand Up @@ -442,27 +448,31 @@ Productions related to transactions
| "Legacy"
| "AccessList"
| "DynamicFee"
| "Blob"
// ------------------------------
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved

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)]
// ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved

endmodule
Expand Down
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
21 changes: 14 additions & 7 deletions 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,15 +229,18 @@ 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
syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function]
| #wordBytes ( Int ) [symbol(#wordBytes), function]
// ----------------------------------------------------------------------
rule #addrBytes(.Account) => .Bytes
rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT)
rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD)
syntax Bytes ::= #addrBytes ( Account ) [symbol(#addrBytes), function]
| #addrBytesNotNil ( AccountNotNil ) [symbol(#addrBytesNotNil), function]
| #wordBytes ( Int ) [symbol(#wordBytes), function]
// ----------------------------------------------------------------------------------------
Robertorosmaninho marked this conversation as resolved.
Show resolved Hide resolved
rule #addrBytes(.Account) => .Bytes
rule #addrBytes(ACCT) => #padToWidth(20, #asByteStack(ACCT)) requires #rangeAddress(ACCT)
rule #addrBytesNotNil(ACCTNN) => #padToWidth(20, #asByteStack(ACCTNN)) requires #rangeAddress(ACCTNN)
rule #wordBytes(WORD) => #padToWidth(32, #asByteStack(WORD)) requires #rangeUInt(256, WORD)
```

Recursive Length Prefix (RLP)
Expand Down Expand Up @@ -349,6 +353,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, #addrBytesNotNil(TT), TV, DATA, [TA], TB, [TVH] ] )
anvacaru marked this conversation as resolved.
Show resolved Hide resolved

syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
// ---------------------------------------------------------------------------------------------
Expand Down
Loading
Loading