Skip to content

Commit 0957714

Browse files
anvacaruanvacaru
authored
EIP 7702 Implement SetCode transactions (#2755)
* define SetCode transaction * parse SetCode tx from JSON fixture files * recover authority from message data * add docstrings * process delegated authority in #call rules * compute gas costs * update expected output in unit tests * refactor delegation processing in driver.md * load previous blob gas values for latest RLP encoded values * Tweak nonce validation in SetCode tx * pad sig values to 32 bytes during recoverAuthority * readability tweaks * refactor addAuthority rules
1 parent d4f05a3 commit 0957714

File tree

12 files changed

+395
-1453
lines changed

12 files changed

+395
-1453
lines changed

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

Lines changed: 126 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -120,6 +120,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
120120
=> #accessAccounts ACCTFROM #newAddr(ACCTFROM, NONCE) #precompiledAccountsSet(SCHED)
121121
~> #deductBlobGas
122122
~> #loadAccessList(TA)
123+
~> #loadAuthorities(AUTH)
123124
~> #checkCreate ACCTFROM VALUE
124125
~> #create ACCTFROM #newAddr(ACCTFROM, NONCE) VALUE CODE
125126
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, CODE)) ~> startTx
@@ -133,12 +134,13 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
133134
<txPending> ListItem(TXID:Int) ... </txPending>
134135
<coinbase> MINER </coinbase>
135136
<message>
136-
<msgID> TXID </msgID>
137-
<txGasLimit> GLIMIT </txGasLimit>
138-
<to> .Account </to>
139-
<value> VALUE </value>
140-
<data> CODE </data>
141-
<txAccess> TA </txAccess>
137+
<msgID> TXID </msgID>
138+
<txGasLimit> GLIMIT </txGasLimit>
139+
<to> .Account </to>
140+
<value> VALUE </value>
141+
<data> CODE </data>
142+
<txAccess> TA </txAccess>
143+
<txAuthList> AUTH </txAuthList>
142144
...
143145
</message>
144146
<account>
@@ -157,6 +159,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
157159
=> #accessAccounts ACCTFROM ACCTTO #precompiledAccountsSet(SCHED)
158160
~> #deductBlobGas
159161
~> #loadAccessList(TA)
162+
~> #loadAuthorities(AUTH)
160163
~> #checkCall ACCTFROM VALUE
161164
~> #call ACCTFROM ACCTTO ACCTTO VALUE VALUE DATA false
162165
~> #finishTx ~> #finalizeTx(false, Ctxfloor(SCHED, DATA)) ~> startTx
@@ -177,6 +180,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
177180
<data> DATA </data>
178181
<txAccess> TA </txAccess>
179182
<txVersionedHashes> TVH </txVersionedHashes>
183+
<txAuthList> AUTH </txAuthList>
180184
...
181185
</message>
182186
<versionedHashes> _ => TVH </versionedHashes>
@@ -193,7 +197,7 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
193197
andBool GLIMIT >=Int maxInt(G0(SCHED, DATA, false), Ctxfloor(SCHED, DATA))
194198
195199
rule <k> loadTx(_) => startTx ... </k>
196-
<statusCode> _ => EVMC_OUT_OF_GAS </statusCode>
200+
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
197201
<txPending> ListItem(_TXID:Int) REST => REST </txPending> [owise]
198202
199203
syntax EthereumCommand ::= "#finishTx"
@@ -254,6 +258,106 @@ To do so, we'll extend sort `JSON` with some EVM specific syntax, and provide a
254258
<callGas> GLIMIT => GLIMIT -Int Gaccesslistaddress < SCHED > </callGas>
255259
```
256260

261+
Processing SetCode Transaction Authority Entries
262+
================================================
263+
264+
- The `#loadAuthorities` function processes authorization entries in EIP-7702 SetCode transactions, charging 25000 gas per tuple regardless of validity.
265+
- Skips processing if transaction is not SetCode type; processes each authorization tuple by recovering the signer and attempting delegation.
266+
- The `#addAuthority` function implements EIP-7702 verification and delegation:
267+
- Validates that the chain ID matches current chain (or is 0) and nonce is within bounds
268+
- Checks if authority account code is empty or already delegated
269+
- Verifies that the authority nonce equals authorization nonce
270+
- Sets delegation code (0xEF0100 + address) and increments nonce on success
271+
- Provides refund (25000 - 12500 = 12500 gas) only for accounts that existed before processing
272+
- A new account will be created for Authorities that are not in the `<accounts>` state, without increasing the refund amount
273+
274+
```k
275+
syntax InternalOp ::= #loadAuthorities ( List ) [symbol(#loadAuthorities)]
276+
// --------------------------------------------------------------------------
277+
rule <k> #loadAuthorities(_) => .K ... </k>
278+
<txPending> ListItem(TXID:Int) ... </txPending>
279+
<message>
280+
<msgID> TXID </msgID>
281+
<txType> TXTYPE </txType>
282+
...
283+
</message>
284+
requires notBool TXTYPE ==K SetCode
285+
286+
rule <k> #loadAuthorities( .List ) => .K ... </k>
287+
<txPending> ListItem(TXID:Int) ... </txPending>
288+
<message>
289+
<msgID> TXID </msgID>
290+
<txType> SetCode </txType>
291+
...
292+
</message>
293+
294+
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)
296+
~> #loadAuthorities (REST)
297+
... </k>
298+
<txPending> ListItem(TXID:Int) ... </txPending>
299+
<message>
300+
<msgID> TXID </msgID>
301+
<txType> SetCode </txType>
302+
...
303+
</message>
304+
<callGas> GLIMIT => GLIMIT -Int 25000 </callGas> [owise]
305+
306+
syntax InternalOp ::= #setDelegation ( Account , Bytes , Bytes , Bytes ) [symbol(#setDelegation)]
307+
// -------------------------------------------------------------------------------------------------
308+
rule <k> #setDelegation(AUTHORITY, CID, NONCE, _ADDR) => .K ... </k> <chainID> ENV_CID </chainID>
309+
requires AUTHORITY ==K .Account
310+
orBool (notBool #asWord(CID) in (SetItem(ENV_CID) SetItem(0)))
311+
orBool (#asWord(NONCE) >=Int maxUInt64)
312+
313+
rule <k> #setDelegation(AUTHORITY, CID, NONCE, ADDR)
314+
=> #touchAccounts AUTHORITY ~> #accessAccounts AUTHORITY
315+
~> #addAuthority(AUTHORITY, CID, NONCE, ADDR)
316+
...
317+
</k> [owise]
318+
319+
syntax InternalOp ::= #addAuthority ( Account , Bytes , Bytes , Bytes ) [symbol(#addAuthority)]
320+
// -----------------------------------------------------------------------------------------------
321+
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, _ADDR) => .K ... </k>
322+
<account>
323+
<acctID> AUTHORITY </acctID>
324+
<code> ACCTCODE </code>
325+
<nonce> ACCTNONCE </nonce>
326+
...
327+
</account>
328+
requires notBool (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE))
329+
orBool (notBool #asWord(NONCE) ==K ACCTNONCE)
330+
331+
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... </k>
332+
<schedule> SCHED </schedule>
333+
<refund> REFUND => REFUND +Int Gnewaccount < SCHED > -Int Gauthbase < SCHED > </refund>
334+
<account>
335+
<acctID> AUTHORITY </acctID>
336+
<code> ACCTCODE => #if #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi </code>
337+
<nonce> ACCTNONCE => ACCTNONCE +Int 1 </nonce>
338+
...
339+
</account>
340+
requires (ACCTCODE ==K .Bytes orBool #isValidDelegation(ACCTCODE))
341+
andBool #asWord(NONCE) ==K ACCTNONCE
342+
343+
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, ADDR) => .K ... </k>
344+
<accounts>
345+
( .Bag
346+
=>
347+
<account>
348+
<acctID> AUTHORITY </acctID>
349+
<code> #if #asWord(ADDR) ==Int 0 #then .Bytes #else EOA_DELEGATION_MARKER +Bytes ADDR #fi </code>
350+
<nonce> 1 </nonce>
351+
...
352+
</account>
353+
)
354+
...
355+
</accounts>
356+
requires #asWord(NONCE) ==Int 0 andBool notBool #accountExists(AUTHORITY)
357+
358+
rule <k> #addAuthority(AUTHORITY, _CID, NONCE, _ADDR) => .K ... </k> requires notBool (#accountExists(AUTHORITY) orBool #asWord(NONCE) ==Int 0)
359+
```
360+
257361
- `exception` only clears from the `<k>` cell if there is an exception preceding it.
258362
- `failure_` holds the name of a test that failed if a test does fail.
259363
- `success` sets the `<exit-code>` to `0` and the `<mode>` to `SUCCESS`.
@@ -633,6 +737,21 @@ Here we check the other post-conditions associated with an EVM test.
633737
rule <k> check "transactions" : ("maxFeePerBlobGas" : VALUE) => .K ... </k> <txOrder> ListItem(TXID) ... </txOrder> <message> <msgID> TXID </msgID> <txMaxBlobFee> VALUE </txMaxBlobFee> ... </message>
634738
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
635739
740+
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 ]
744+
...
745+
</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
749+
750+
syntax Bytes ::= #hex2Bytes ( String ) [function] //TODO: Is this needed?
751+
// -------------------------------------------------
752+
rule #hex2Bytes("0x00") => b""
753+
rule #hex2Bytes(S) => #parseByteStack(S) [owise]
754+
636755
syntax Bool ::= isInAccessListStorage ( Int , JSON ) [symbol(isInAccessListStorage), function]
637756
| isInAccessList ( Account , Int , JSON ) [symbol(isInAccessList), function]
638757
// -------------------------------------------------------------------------------------------------

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

Lines changed: 7 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -443,30 +443,33 @@ Productions related to transactions
443443
| "AccessList"
444444
| "DynamicFee"
445445
| "Blob"
446-
// ------------------------
446+
| "SetCode"
447+
// ---------------------------
447448
448449
syntax Int ::= #dasmTxPrefix ( TxType ) [symbol(#dasmTxPrefix), function]
449450
// -------------------------------------------------------------------------
450451
rule #dasmTxPrefix (Legacy) => 0
451452
rule #dasmTxPrefix (AccessList) => 1
452453
rule #dasmTxPrefix (DynamicFee) => 2
453454
rule #dasmTxPrefix (Blob) => 3
455+
rule #dasmTxPrefix (SetCode) => 4
454456
455457
syntax TxType ::= #asmTxPrefix ( Int ) [symbol(#asmTxPrefix), function]
456458
// -----------------------------------------------------------------------
457459
rule #asmTxPrefix (0) => Legacy
458460
rule #asmTxPrefix (1) => AccessList
459461
rule #asmTxPrefix (2) => DynamicFee
460462
rule #asmTxPrefix (3) => Blob
463+
rule #asmTxPrefix (4) => SetCode
461464
462-
syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx
463-
// -----------------------------------------------------------------
464-
465+
syntax TxData ::= LegacyTx | AccessListTx | DynamicFeeTx | BlobTx | SetCodeTx
466+
// -----------------------------------------------------------------------------
465467
syntax LegacyTx ::= LegacyTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes ) [symbol(LegacyTxData)]
466468
| LegacySignedTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, networkChainId: Int ) [symbol(LegacySignedTxData)]
467469
syntax AccessListTx ::= AccessListTxData ( nonce: Int, gasPrice: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs ) [symbol(AccessListTxData)]
468470
syntax DynamicFeeTx ::= DynamicFeeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs) [symbol(DynamicFeeTxData)]
469471
syntax BlobTx ::= BlobTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, maxBlobGasFee: Int, blobVersionedHashes: List ) [symbol(BlobTxData)]
472+
syntax SetCodeTx ::= SetCodeTxData ( nonce: Int, priorityGasFee: Int, maxGasFee: Int, gasLimit: Int, to: Account, value: Int, data: Bytes, chainId: Int, accessLists: JSONs, authorizationList: List) [symbol(SetCodeTxData)]
470473
// ---------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------------
471474
472475
endmodule

0 commit comments

Comments
 (0)