Skip to content

Commit 21fde76

Browse files
anvacaruanvacaru
authored
update check rules for SetCode transactions (#2818)
1 parent 0d52fed commit 21fde76

File tree

3 files changed

+29
-26
lines changed

3 files changed

+29
-26
lines changed

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

Lines changed: 12 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -292,7 +292,7 @@ Processing SetCode Transaction Authority Entries
292292
</message>
293293
294294
rule <k> #loadAuthorities (ListItem(ListItem(CID) ListItem(ADDR) ListItem(NONCE) ListItem(YPAR) ListItem(SIGR) ListItem(SIGS)) REST )
295-
=> #setDelegation (#recoverAuthority (CID, ADDR, NONCE, YPAR, SIGR, SIGS ), CID, NONCE, ADDR)
295+
=> #setDelegation (#recoverAuthority(CID, ADDR, NONCE, YPAR, SIGR, SIGS), CID, NONCE, ADDR)
296296
~> #loadAuthorities (REST)
297297
... </k>
298298
<txPending> ListItem(TXID:Int) ... </txPending>
@@ -738,14 +738,19 @@ Here we check the other post-conditions associated with an EVM test.
738738
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
739739
740740
rule <k> check "transactions" : "authorizationList" : [ .JSONs ] => .K ... </k>
741-
rule <k> check "transactions" : "authorizationList" : [ { "chainId": CID, "address": ADDR, "nonce": NONCE, "v": _, "r": SIGR, "s": SIGS, "signer": _, "yParity": SIGY } , REST ]
742-
=> check "transactions" : "authorizationList" : [ #hex2Bytes(CID), #hex2Bytes(ADDR), #hex2Bytes(NONCE), #hex2Bytes(SIGY), #hex2Bytes(SIGR), #hex2Bytes(SIGS) ]
743-
~> check "transactions" : "authorizationList" : [ REST ]
741+
rule <k> check "transactions" : "authorizationList" : [ { "chainId": CID, "address": ADDR, "nonce": NONCE, "v": SIGV, "r": SIGR, "s": SIGS, "signer": _ , "yParity": SIGY }, REST ]
742+
=> check "transactions" : "authorizationList" : [ { "chainId": CID, "address": ADDR, "nonce": NONCE, "v": SIGV, "r": SIGR, "s": SIGS, "yParity": SIGY }, REST ]
744743
...
745744
</k>
746-
rule <k> check "transactions" : "authorizationList" : [ AUTH ] => .K ... </k>
747-
<txOrder> ListItem(TXID) ... </txOrder>
748-
<message> <msgID> TXID </msgID> <txAuthList> AUTHLIST </txAuthList> ... </message> requires #parseJSONs2List(AUTH) in AUTHLIST
745+
746+
rule <k> check "transactions" : "authorizationList" : [ { "chainId": CID, "address": ADDR, "nonce": NONCE, "v": _, "r": SIGR, "s": SIGS, "yParity": SIGY }, REST ]
747+
=> (ListItem(#hex2Bytes(CID)) ListItem(#hex2Bytes(ADDR)) ListItem(#hex2Bytes(NONCE)) ListItem(#hex2Bytes(SIGY)) ListItem(#hex2Bytes(SIGR)) ListItem(#hex2Bytes(SIGS)) .List) ~> check "transactions" : "authorizationList" : [ REST ]
748+
...
749+
</k>
750+
751+
rule <k> (AUTH:List => .K) ~> check "transactions" : "authorizationList" : _ ... </k>
752+
<txOrder> ListItem(TXID) ... </txOrder>
753+
<message> <msgID> TXID </msgID> <txAuthList> AUTHLIST </txAuthList> ... </message> requires AUTH in AUTHLIST
749754
750755
syntax Bytes ::= #hex2Bytes ( String ) [function] //TODO: Is this needed?
751756
// -------------------------------------------------

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

Lines changed: 17 additions & 17 deletions
Original file line numberDiff line numberDiff line change
@@ -361,7 +361,7 @@ The `"rlp"` key loads the block information.
361361
, "to" : TT , "v" : TY , "value" : TV
362362
, "accessList" : TA , "type" : TYPE , "chainID" : TC
363363
, "maxPriorityFeePerGas" : TP , "maxFeePerGas" : TP
364-
, "maxFeePerBlobGas" : 0 , "blobVersionedHashes" : [ .JSONs ]
364+
, "maxFeePerBlobGas" : 0 , "blobVersionedHashes" : [ .JSONs ]
365365
, .JSONs
366366
}
367367
~> load "transaction" : [ REST ]
@@ -386,25 +386,25 @@ The `"rlp"` key loads the block information.
386386
387387
rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, TB, TVH, TY, TR, TS ]] , REST ]
388388
=> mkTX !ID:Int
389-
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP
390-
, "nonce" : TN , "r" : TR , "s" : TS
391-
, "to" : TT , "v" : TY , "value" : TV
392-
, "accessList" : TA , "type" : TYPE , "chainID" : TC
393-
, "maxFeePerGas" : TF , "maxFeePerBlobGas" : TB , "blobVersionedHashes" : TVH
389+
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP
390+
, "nonce" : TN , "r" : TR , "s" : TS
391+
, "to" : TT , "v" : TY , "value" : TV
392+
, "accessList" : TA , "type" : TYPE , "chainID" : TC
393+
, "maxFeePerGas" : TF , "maxFeePerBlobGas" : TB , "blobVersionedHashes" : TVH
394394
, .JSONs
395395
}
396396
~> load "transaction" : [ REST ]
397397
...
398398
</k>
399399
requires #asWord(TYPE) ==Int #dasmTxPrefix(Blob)
400400
401-
rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, AUTH , TY, TR, TS ]] , REST ]
401+
rule <k> load "transaction" : [ [TYPE , [TC, TN, TP, TF, TG, TT, TV, TI, TA, AUTH, TY, TR, TS ]] , REST ]
402402
=> mkTX !ID:Int
403-
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP
404-
, "nonce" : TN , "r" : TR , "s" : TS
405-
, "to" : TT , "v" : TY , "value" : TV
406-
, "accessList" : TA , "type" : TYPE , "chainID" : TC
407-
, "maxFeePerGas" : TF , "authList" : AUTH , .JSONs }
403+
~> loadTransaction !ID { "data" : TI , "gasLimit" : TG , "maxPriorityFeePerGas" : TP
404+
, "nonce" : TN , "r" : TR , "s" : TS
405+
, "to" : TT , "v" : TY , "value" : TV
406+
, "accessList" : TA , "type" : TYPE , "chainID" : TC
407+
, "maxFeePerGas" : TF , "authorizationList" : AUTH , .JSONs }
408408
~> load "transaction" : [ REST ]
409409
...
410410
</k>
@@ -463,7 +463,7 @@ The `"rlp"` key loads the block information.
463463
rule <k> loadTransaction TXID { "blobVersionedHashes" : [TVH:JSONs], REST => REST } ... </k>
464464
<message> <msgID> TXID </msgID> <txVersionedHashes> _ => #parseJSONs2List(TVH) </txVersionedHashes> ... </message>
465465
466-
rule <k> loadTransaction TXID { "authList" : [AUTH:JSONs], REST => REST } ... </k>
466+
rule <k> loadTransaction TXID { "authorizationList" : [AUTH:JSONs], REST => REST } ... </k>
467467
<message> <msgID> TXID </msgID> <txAuthList> _ => #parseJSONs2List(AUTH) </txAuthList> ... </message>
468468
```
469469

@@ -628,7 +628,7 @@ The `"rlp"` key loads the block information.
628628
<txType> SetCode </txType>
629629
...
630630
</message>
631-
requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>)
631+
requires (ACCTCODE ==K .Bytes orBool (Ghasauthority << SCHED >> andBool #isValidDelegation(ACCTCODE)))
632632
andBool notBool ACCTTO ==K .Account
633633
andBool ACCTNONCE ==Int TX_NONCE
634634
andBool BASE_FEE <=Int TX_MAX_FEE
@@ -662,7 +662,7 @@ The `"rlp"` key loads the block information.
662662
<txType> Blob </txType>
663663
...
664664
</message>
665-
requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>)
665+
requires (ACCTCODE ==K .Bytes orBool (Ghasauthority << SCHED >> andBool #isValidDelegation(ACCTCODE)))
666666
andBool notBool ACCTTO ==K .Account
667667
andBool ACCTNONCE ==Int TX_NONCE
668668
andBool BASE_FEE <=Int TX_MAX_FEE
@@ -694,7 +694,7 @@ The `"rlp"` key loads the block information.
694694
<txType> DynamicFee </txType>
695695
...
696696
</message>
697-
requires (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>)
697+
requires (ACCTCODE ==K .Bytes orBool (Ghasauthority << SCHED >> andBool #isValidDelegation(ACCTCODE)))
698698
andBool ACCTNONCE ==Int TX_NONCE
699699
andBool BASE_FEE <=Int TX_MAX_FEE
700700
andBool TX_MAX_PRIORITY_FEE <=Int TX_MAX_FEE
@@ -722,7 +722,7 @@ The `"rlp"` key loads the block information.
722722
...
723723
</message>
724724
requires #dasmTxPrefix(TXTYPE) <Int 2
725-
andBool (ACCTCODE ==K .Bytes orBool Ghasauthority << SCHED >>)
725+
andBool (ACCTCODE ==K .Bytes orBool (Ghasauthority << SCHED >> andBool #isValidDelegation(ACCTCODE)))
726726
andBool ACCTNONCE ==Int TX_NONCE
727727
andBool BASE_FEE <=Int TX_GAS_PRICE
728728
andBool BAL >=Int TX_GAS_LIMIT *Int TX_GAS_PRICE +Int VALUE

‎tests/execution-spec-tests/failing.llvm‎

Lines changed: 0 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -26,5 +26,3 @@ blockchain_tests/prague/eip7251_consolidations/consolidations_during_fork/consol
2626
blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requests.json,tests/prague/eip7251_consolidations/test_consolidations.py::test_consolidation_requests[fork_Prague-blockchain_test-multiple_block_fee_increments]
2727
blockchain_tests/prague/eip7251_consolidations/consolidations/consolidation_requests.json,tests/prague/eip7251_consolidations/test_consolidations.py::test_consolidation_requests[fork_Prague-blockchain_test-single_block_multiple_consolidation_request_last_oog]
2828
blockchain_tests/prague/eip7251_consolidations/contract_deployment/system_contract_deployment.json,*
29-
blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/set_code_from_account_with_non_delegating_code.json,*
30-
blockchain_tests/prague/eip7702_set_code_tx/set_code_txs/valid_tx_invalid_auth_signature.json,*

0 commit comments

Comments
 (0)