Skip to content

Commit

Permalink
Setting txVersionedHashes as JSONs
Browse files Browse the repository at this point in the history 
Implementing parsing features for `txVersionedHashes` and `txMaxBlobFee`
  • Loading branch information
@Robertorosmaninho
Robertorosmaninho committed Jan 22, 2025
1 parent 93142fc commit 71fb9fd
Show file tree
Hide file tree
Showing 7 changed files with 56 additions and 19 deletions.
16 changes: 15 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 @@ -360,6 +360,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 @@ -545,7 +546,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 @@ -556,6 +557,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 @@ -569,6 +575,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 @@ -583,6 +590,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]
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
2 changes: 1 addition & 1 deletion 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 @@ -472,7 +472,7 @@ Productions related to transactions
| 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: Bytes ) [symbol(BlobTxData)]
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
Expand Down
2 changes: 1 addition & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -168,7 +168,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
<txMaxFee> 0 </txMaxFee> // T_m
<txType> .TxType </txType> // T_x
<txMaxBlobFee> 0 </txMaxBlobFee>
<txVersionedHashes> .Bytes </txVersionedHashes>
<txVersionedHashes> [ .JSONs ] </txVersionedHashes>
</message>
</messages>
Expand Down
4 changes: 2 additions & 2 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/serialization.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -354,8 +354,8 @@ 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 ] )
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] ] )
syntax Bytes ::= #rlpEncodeMerkleTree ( MerkleTree ) [symbol(#rlpEncodeMerkleTree), function]
// ---------------------------------------------------------------------------------------------
Expand Down
47 changes: 35 additions & 12 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 @@ -427,7 +450,7 @@ The `"rlp"` key loads the block information.
...
</message>
rule [[ #getTxData( TXID ) => BlobTxData(TN, TP, TF, TG, TT, TV, DATA, CID, TA, TB, TVH) ]]
rule [[ #getTxData( TXID ) => BlobTxData(TN, TPF, TM, TG, TT, TV, DATA, CID, TA, TB, TVH) ]]
<message>
<msgID> TXID </msgID>
<txNonce> TN </txNonce>
Expand All @@ -438,10 +461,10 @@ The `"rlp"` key loads the block information.
<data> DATA </data>
<txChainID> CID </txChainID>
<txAccess> TA </txAccess>
<txPriorityFee> TP </txPriorityFee>
<txMaxFee> TF </txMaxFee>
<txMaxBlobFee> TB </txMaxBlobFee>
<txVersionedHashes> TVH </txVersionedHashes>
<txPriorityFee> TPF </txPriorityFee>
<txMaxFee> TM </txMaxFee>
<txMaxBlobFee> TB </txMaxBlobFee>
<txVersionedHashes> TVH </txVersionedHashes>
<txType> Blob </txType>
...
</message>
Expand Down
2 changes: 1 addition & 1 deletion tests/failing/ContractCreationSpam_d0g0v0.json.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -323,7 +323,7 @@
0
</txMaxBlobFee>
<txVersionedHashes>
b""
[ .JSONs ]
</txVersionedHashes>
</message>
</messages>
Expand Down
2 changes: 1 addition & 1 deletion tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -369,7 +369,7 @@
0
</txMaxBlobFee>
<txVersionedHashes>
b""
[ .JSONs ]
</txVersionedHashes>
</message>
</messages>
Expand Down

0 comments on commit 71fb9fd

Please sign in to comment.