Skip to content

Commit eaef051

Browse files
RobertorosmaninhoRobertorosmaninho
authored
Merge branch 'master' into eip-7610
2 parents 983a41a + 6cf81f6 commit eaef051

File tree

7 files changed

+106
-20
lines changed

7 files changed

+106
-20
lines changed

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md

Lines changed: 16 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -397,6 +397,7 @@ Note that `TEST` is sorted here so that key `"network"` comes before key `"pre"`
397397
rule <k> loadTransaction _ { "s" : (TS:Bytes => #padToWidth(32, TS)), _ } ... </k> requires lengthBytes(TS) <Int 32
398398
rule <k> loadTransaction _ { "maxPriorityFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
399399
rule <k> loadTransaction _ { "maxFeePerGas" : (V:Bytes => #asWord(V)), _ } ... </k>
400+
rule <k> loadTransaction _ { "maxFeePerBlobGas" : (V:Bytes => #asWord(V)), _ } ... </k>
400401
```
401402

402403
### Checking State
@@ -582,7 +583,7 @@ Here we check the other post-conditions associated with an EVM test.
582583
rule <k> check "transactions" : (_KEY : (VALUE:String => #parseByteStack(VALUE))) ... </k>
583584
rule <k> check "transactions" : ("to" : (VALUE:Bytes => #asAccount(VALUE))) ... </k>
584585
rule <k> check "transactions" : ( KEY : (VALUE:Bytes => #padToWidth(32, VALUE))) ... </k> requires KEY in (SetItem("r") SetItem("s")) andBool lengthBytes(VALUE) <Int 32
585-
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"))
586+
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"))
586587
rule <k> check "transactions" : ("type" : (VALUE:Int => #asmTxPrefix(VALUE))) ... </k>
587588
588589
rule <k> check "transactions" : "accessList" : [ ACCESSLIST , REST ] => check "transactions" : "accessList" : ACCESSLIST ~> check "transactions" : "accessList" : [ REST ] ... </k>
@@ -593,6 +594,11 @@ Here we check the other post-conditions associated with an EVM test.
593594
rule <k> check "transactions" : "accessList" : [ .JSONs ] => .K ... </k>
594595
595596
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)
597+
598+
rule <k> check "transactions" : "blobVersionedHashes" : [ .JSONs ] => .K ... </k>
599+
rule <k> check "transactions" : "blobVersionedHashes" : [ VHASH, REST ] => check "transactions" : "blobVersionedHashes" : VHASH ~> check "transactions" : "blobVersionedHashes" : [ REST ] ... </k>
600+
rule <k> check "transactions" : ("blobVersionedHashes" : VHASH ) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txVersionedHashes> VH </txVersionedHashes> ... </message> requires isInVersionedHashes(VHASH, VH)
601+
596602
rule <k> check "transactions" : ("data" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <data> VALUE </data> ... </message>
597603
rule <k> check "transactions" : ("gasLimit" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasLimit> VALUE </txGasLimit> ... </message>
598604
rule <k> check "transactions" : ("gasPrice" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txGasPrice> VALUE </txGasPrice> ... </message>
@@ -606,6 +612,7 @@ Here we check the other post-conditions associated with an EVM test.
606612
rule <k> check "transactions" : ("type" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txType> VALUE </txType> ... </message>
607613
rule <k> check "transactions" : ("maxFeePerGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxFee> VALUE </txMaxFee> ... </message>
608614
rule <k> check "transactions" : ("maxPriorityFeePerGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txPriorityFee> VALUE </txPriorityFee> ... </message>
615+
rule <k> check "transactions" : ("maxFeePerBlobGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxBlobFee> VALUE </txMaxBlobFee> ... </message>
609616
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
610617
611618
syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function]
@@ -620,6 +627,14 @@ Here we check the other post-conditions associated with an EVM test.
620627
rule isInAccessListStorage(KEY, [SKEY, REST]) => #if KEY ==Int #asWord(SKEY)
621628
#then true
622629
#else isInAccessListStorage(KEY, [REST]) #fi
630+
631+
// 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]
632+
syntax Bool ::= isInVersionedHashes(Bytes, JSON) [symbol(isInVersionedHashes), function]
633+
// ---------------------------------------------------------------------------------------
634+
rule isInVersionedHashes(_, [.JSONs]) => false
635+
rule isInVersionedHashes(KEY, [SKEY, REST]) => #if KEY ==K SKEY
636+
#then true
637+
#else isInVersionedHashes(KEY, [REST]) #fi
623638
```
624639

625640
TODO: case with nonzero ommers.

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm-types.md

Lines changed: 21 additions & 11 deletions
Original file line numberDiff line numberDiff line change
@@ -337,6 +337,8 @@ Bytes helper functions
337337
- `#asInteger` will interpret a stack of bytes as a single arbitrary-precision integer (with MSB first).
338338
- `#asAccount` will interpret a stack of bytes as a single account id (with MSB first).
339339
Differs from `#asWord` only in that an empty stack represents the empty account, not account zero.
340+
- `asAccountNotNil` will interpret a stack of bytes as a single account id (with MSB first), but will fail if the
341+
stack is empty.
340342
- `#asByteStack` will split a single word up into a `Bytes`.
341343
- `#range(WS, N, W)` access the range of `WS` beginning with `N` of width `W`.
342344
- `#padToWidth(N, WS)` and `#padRightToWidth` make sure that a `Bytes` is the correct size.
@@ -350,11 +352,14 @@ Bytes helper functions
350352
// -------------------------------------------------------------------------
351353
rule #asInteger(WS) => Bytes2Int(WS, BE, Unsigned) [concrete]
352354
353-
syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function]
354-
// ----------------------------------------------------------------------
355+
syntax Account ::= #asAccount ( Bytes ) [symbol(#asAccount), function]
356+
syntax AccountNotNil ::= #asAccountNotNil ( Bytes ) [symbol(#asAccountNotNil), function]
357+
// ----------------------------------------------------------------------------------------
355358
rule #asAccount(BS) => .Account requires lengthBytes(BS) ==Int 0
356359
rule #asAccount(BS) => #asWord(BS) [owise]
357360
361+
rule #asAccountNotNil(BS) => #asWord(BS) requires lengthBytes(BS) >Int 0
362+
358363
syntax Bytes ::= #asByteStack ( Int ) [symbol(#asByteStack), function, total]
359364
// -----------------------------------------------------------------------------
360365
rule #asByteStack(W) => Int2Bytes(W, BE, Unsigned) [concrete]
@@ -385,7 +390,8 @@ Accounts
385390

386391
```k
387392
syntax Account ::= ".Account" | Int
388-
// -----------------------------------
393+
syntax AccountNotNil = Int
394+
// --------------------------
389395
390396
syntax AccountCode ::= Bytes
391397
// ----------------------------
@@ -442,28 +448,32 @@ Productions related to transactions
442448
| "Legacy"
443449
| "AccessList"
444450
| "DynamicFee"
445-
// ------------------------------
451+
| "Blob"
452+
// ------------------------
446453
447454
syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function]
448455
// -------------------------------------------------------------------------
449456
rule #dasmTxPrefix (Legacy) => 0
450457
rule #dasmTxPrefix (AccessList) => 1
451458
rule #dasmTxPrefix (DynamicFee) => 2
459+
rule #dasmTxPrefix (Blob) => 3
452460
453461
syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function]
454462
// -----------------------------------------------------------------------
455463
rule #asmTxPrefix (0) => Legacy
456464
rule #asmTxPrefix (1) => AccessList
457465
rule #asmTxPrefix (2) => DynamicFee
466+
rule #asmTxPrefix (3) => Blob
458467
459-
syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx
460-
// --------------------------------------------------------
468+
syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx
469+
// -----------------------------------------------------------------
461470
462-
syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)]
463-
| LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)]
464-
syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)]
465-
syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)]
466-
// ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
471+
syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)]
472+
| LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)]
473+
syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)]
474+
syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)]
475+
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)]
476+
// ----------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
467477
468478
endmodule
469479
```

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -167,6 +167,8 @@ In the comments next to each cell, we've marked which component of the YellowPap
167167
<txPriorityFee> 0 </txPriorityFee> // T_f
168168
<txMaxFee> 0 </txMaxFee> // T_m
169169
<txType> .TxType </txType> // T_x
170+
<txMaxBlobFee> 0 </txMaxBlobFee>
171+
<txVersionedHashes> [ .JSONs ] </txVersionedHashes>
170172
</message>
171173
</messages>
172174

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -141,7 +141,8 @@ The encoding schemes are applied in `#rlpEcondeTxData`.
141141
rule #hashTxData( TXDATA ) => Keccak256raw( #rlpEncodeTxData(TXDATA) ) requires isLegacyTx (TXDATA)
142142
rule #hashTxData( TXDATA ) => Keccak256raw( b"\x01" +Bytes #rlpEncodeTxData(TXDATA) ) requires isAccessListTx(TXDATA)
143143
rule #hashTxData( TXDATA ) => Keccak256raw( b"\x02" +Bytes #rlpEncodeTxData(TXDATA) ) requires isDynamicFeeTx(TXDATA)
144-
```
144+
rule #hashTxData( TXDATA ) => Keccak256raw( b"\x03" +Bytes #rlpEncodeTxData(TXDATA) ) requires isBlobTx (TXDATA)
145+
```
145146

146147
The EVM test-sets are represented in JSON format with hex-encoding of the data and programs.
147148
Here we provide some standard parser/unparser functions for that format.
@@ -228,6 +229,7 @@ Unparsing
228229
```
229230

230231
- `#addrBytes` Takes an Account and represents it as a 20-byte wide Bytes (or an empty Bytes for a null address)
232+
- `#addrBytesNotNil` Takes an Account and represents it as a 20-byte wide Bytes. It throws an error if the account is null.
231233
- `#wordBytes` Takes an Int and represents it as a 32-byte wide Bytes
232234

233235
```k
@@ -349,6 +351,9 @@ Encoding
349351
350352
rule #rlpEncodeTxData( DynamicFeeTxData(TN, TF, TM, TG, TT, TV, DATA, TC, [TA]) )
351353
=> #rlpEncode( [ TC, TN, TF, TM, TG, #addrBytes(TT), TV, DATA, [TA] ] )
354+
355+
rule #rlpEncodeTxData( BlobTxData(TN, TF, TM, TG, TT, TV, DATA, CID, [TA], TB, [TVH]) )
356+
=> #rlpEncode( [ CID, TN, TF, TM, TG, #addrBytes({TT}:>Account), TV, DATA, [TA], TB, [TVH] ] )
352357
353358
syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
354359
// ---------------------------------------------------------------------------------------------

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md

Lines changed: 49 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -276,19 +276,21 @@ The `"rlp"` key loads the block information.
276276
, "nonce" : TN , "r" : TR , "s" : TS
277277
, "to" : TT , "v" : TW , "value" : TV
278278
, "type" : #dasmTxPrefix(Legacy) , "maxPriorityFeePerGas" : TP
279-
, "maxFeePerGas": TP , .JSONs
279+
, "maxFeePerGas": TP , "maxFeePerBlobGas" : 0
280+
, "blobVersionedHashes" : [ .JSONs ] , .JSONs
280281
}
281282
~> load "transaction" : [ REST ]
282283
...
283284
</k>
284285
285286
rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TG, TT, TV, TI, TA, TY , TR, TS ]] , REST ]
286287
=> mkTX !ID:Int
287-
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP
288-
, "nonce" : TN , "r" : TR , "s" : TS
289-
, "to" : TT , "v" : TY , "value" : TV
290-
, "accessList" : TA , "type" : TYPE , "chainID" : TC
291-
, "maxPriorityFeePerGas" : TP , "maxFeePerGas": TP
288+
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "gasPrice" : TP
289+
, "nonce" : TN , "r" : TR , "s" : TS
290+
, "to" : TT , "v" : TY , "value" : TV
291+
, "accessList" : TA , "type" : TYPE , "chainID" : TC
292+
, "maxPriorityFeePerGas" : TP , "maxFeePerGas" : TP
293+
, "maxFeePerBlobGas" : 0 , "blobVersionedHashes" : [ .JSONs ]
292294
, .JSONs
293295
}
294296
~> load "transaction" : [ REST ]
@@ -303,13 +305,28 @@ The `"rlp"` key loads the block information.
303305
, "nonce" : TN , "r" : TR , "s" : TS
304306
, "to" : TT , "v" : TY , "value" : TV
305307
, "accessList" : TA , "type" : TYPE , "chainID" : TC
306-
, "maxFeePerGas" : TF , .JSONs
308+
, "maxFeePerGas" : TF , "maxFeePerBlobGas" : 0
309+
, "blobVersionedHashes" : [ .JSONs ] , .JSONs
307310
}
308311
~> load "transaction" : [ REST ]
309312
...
310313
</k>
311314
requires #asWord(TYPE) ==Int #dasmTxPrefix(DynamicFee)
312315
316+
rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TY, TVH, TB, TR, TS ]] , REST ]
317+
=> mkTX !ID:Int
318+
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP
319+
, "nonce" : TN , "r" : TR , "s" : TS
320+
, "to" : TT , "v" : TY , "value" : TV
321+
, "accessList" : TA , "type" : TYPE , "chainID" : TC
322+
, "maxFeePerGas" : TF , "maxFeePerBlobGas" : TB , "blobVersionedHashes" : TVH
323+
, .JSONs
324+
}
325+
~> load "transaction" : [ REST ]
326+
...
327+
</k>
328+
requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob)
329+
313330
syntax EthereumCommand ::= "loadTransaction" Int JSON
314331
// -----------------------------------------------------
315332
rule <k> loadTransaction _ { .JSONs } => .K ... </k>
@@ -356,6 +373,12 @@ The `"rlp"` key loads the block information.
356373
357374
rule <k> loadTransaction TXID { "maxFeePerGas" : TF:Int, REST => REST } ... </k>
358375
<message> <msgID> TXID </msgID> <txMaxFee> _ => TF </txMaxFee> ... </message>
376+
377+
rule <k> loadTransaction TXID { "maxFeePerBlobGas" : TB:Int, REST => REST } ... </k>
378+
<message> <msgID> TXID </msgID> <txMaxBlobFee> _ => TB </txMaxBlobFee> ... </message>
379+
380+
rule <k> loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... </k>
381+
<message> <msgID> TXID </msgID> <txVersionedHashes> _ => [TVH] </txVersionedHashes> ... </message>
359382
```
360383

361384
### Getting State
@@ -426,6 +449,25 @@ The `"rlp"` key loads the block information.
426449
<txType> DynamicFee </txType>
427450
...
428451
</message>
452+
453+
rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]]
454+
<message>
455+
<msgID> TXID </msgID>
456+
<txNonce> TN </txNonce>
457+
<txGasPrice> TP </txGasPrice>
458+
<txGasLimit> TG </txGasLimit>
459+
<to> TT </to>
460+
<value> TV </value>
461+
<data> DATA </data>
462+
<txChainID> CID </txChainID>
463+
<txAccess> TA </txAccess>
464+
<txPriorityFee> TPF </txPriorityFee>
465+
<txMaxFee> TM </txMaxFee>
466+
<txMaxBlobFee> TB </txMaxBlobFee>
467+
<txVersionedHashes> TVH </txVersionedHashes>
468+
<txType> Blob </txType>
469+
...
470+
</message>
429471
```
430472

431473
- `#effectiveGasPrice` will compute the gas price for TXID, as specified by EIP-1559

‎tests/failing/ContractCreationSpam_d0g0v0.json.expected

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -319,6 +319,12 @@
319319
<txType>
320320
Legacy
321321
</txType>
322+
<txMaxBlobFee>
323+
0
324+
</txMaxBlobFee>
325+
<txVersionedHashes>
326+
[ .JSONs ]
327+
</txVersionedHashes>
322328
</message>
323329
</messages>
324330
</network>

‎tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -365,6 +365,12 @@
365365
<txType>
366366
Legacy
367367
</txType>
368+
<txMaxBlobFee>
369+
0
370+
</txMaxBlobFee>
371+
<txVersionedHashes>
372+
[ .JSONs ]
373+
</txVersionedHashes>
368374
</message>
369375
</messages>
370376
</network>

0 commit comments

Comments
 (0)