Skip to content

Commit 12289cb

Browse files
anvacarupalinatolmach
anvacaru
and
palinatolmach
authored
Implement Deposit Requests (#2748)
* fix typos in Makefile * define Prague schedule * update execution-spec-tests/failing.llvm * set Prague as the default schedule for testing * update expected output * implement execution layer requests * update execution-spec-tests/failing.llvm * update golden files * update execution-spec-tests/failing.llvm * update proof files * update expected output for integration tests * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/driver.md Co-authored-by: Palina <polina.tolmach@gmail.com> * update execution-specs-tests/failing.llvm * change cryptografic function to sha256 --------- Co-authored-by: Palina <polina.tolmach@gmail.com>
1 parent 183e857 commit 12289cb

File tree

146 files changed

+690
-759
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

146 files changed

+690
-759
lines changed

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

Lines changed: 8 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -545,7 +545,7 @@ Here we check the other post-conditions associated with an EVM test.
545545
SetItem("mixHash") SetItem("nonce") SetItem("number") SetItem("parentHash")
546546
SetItem("receiptTrie") SetItem("stateRoot") SetItem("timestamp")
547547
SetItem("transactionsTrie") SetItem("uncleHash") SetItem("baseFeePerGas") SetItem("withdrawalsRoot")
548-
SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot")
548+
SetItem("blobGasUsed") SetItem("excessBlobGas") SetItem("parentBeaconBlockRoot") SetItem("requestsHash")
549549
)
550550
551551
rule <k> check "blockHeader" : { "bloom" : VALUE } => .K ... </k> <logsBloom> VALUE </logsBloom>
@@ -568,6 +568,7 @@ Here we check the other post-conditions associated with an EVM test.
568568
rule <k> check "blockHeader" : { "blobGasUsed" : VALUE } => .K ... </k> <blobGasUsed> VALUE </blobGasUsed>
569569
rule <k> check "blockHeader" : { "excessBlobGas" : VALUE } => .K ... </k> <excessBlobGas> VALUE </excessBlobGas>
570570
rule <k> check "blockHeader" : { "parentBeaconBlockRoot": VALUE } => .K ... </k> <beaconRoot> VALUE </beaconRoot>
571+
rule <k> check "blockHeader" : { "requestsHash" : VALUE } => .K ... </k> <requestsRoot> VALUE </requestsRoot>
571572
572573
573574
rule <k> check "blockHeader" : { "hash": HASH:Bytes } => .K ...</k>
@@ -591,10 +592,12 @@ Here we check the other post-conditions associated with an EVM test.
591592
<blobGasUsed> UB </blobGasUsed>
592593
<excessBlobGas> EB </excessBlobGas>
593594
<beaconRoot> BR </beaconRoot>
594-
requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) ==Int #asWord(HASH)
595-
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF) ==Int #asWord(HASH)
596-
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR) ==Int #asWord(HASH)
597-
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
595+
<requestsRoot> RR </requestsRoot>
596+
requires #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN) ==Int #asWord(HASH)
597+
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF) ==Int #asWord(HASH)
598+
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR) ==Int #asWord(HASH)
599+
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR) ==Int #asWord(HASH)
600+
orBool #blockHeaderHash(HP, HO, HC, HR, HT, HE, HB, HD, HI, HL, HG, HS, HX, HM, HN, HF, WR, UB, EB, BR, RR) ==Int #asWord(HASH)
598601
599602
rule check TESTID : { "genesisBlockHeader" : BLOCKHEADER } => check "genesisBlockHeader" : BLOCKHEADER ~> failure TESTID
600603
// ------------------------------------------------------------------------------------------------------------------------

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

Lines changed: 61 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -11,12 +11,14 @@ This file only defines the local execution operations, the file `driver.md` will
1111
requires "data.md"
1212
requires "network.md"
1313
requires "gas.md"
14+
requires "requests.md"
1415
1516
module EVM
1617
imports STRING
1718
imports EVM-DATA
1819
imports NETWORK
1920
imports GAS
21+
imports EVM-REQUESTS
2022
```
2123

2224
Configuration
@@ -118,6 +120,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
118120
<blobGasUsed> 0 </blobGasUsed>
119121
<excessBlobGas> 0 </excessBlobGas>
120122
<beaconRoot> 0 </beaconRoot>
123+
<requestsRoot> 0 </requestsRoot>
121124
122125
<ommerBlockHeaders> [ .JSONs ] </ommerBlockHeaders>
123126
</block>
@@ -192,6 +195,11 @@ In the comments next to each cell, we've marked which component of the YellowPap
192195
</withdrawal>
193196
</withdrawals>
194197
198+
<requests>
199+
<depositRequests> .List </depositRequests>
200+
//other request types come here
201+
</requests>
202+
195203
</network>
196204
197205
</ethereum>
@@ -714,6 +722,53 @@ After executing a transaction, it's necessary to have the effect of the substate
714722
rule <k> #deleteAccounts(.List) => .K ... </k>
715723
```
716724

725+
### Fetching requests from event logs
726+
727+
While processing a block, multiple requests objects with different `request_types` will be produced by the system, and accumulated in the block requests list.
728+
729+
```k
730+
syntax KItem ::= "#filterLogs" Int [symbol(#filterLogs)]
731+
// --------------------------------------------------------
732+
rule <k> #filterLogs _ => .K ... </k> <schedule> SCHED </schedule> requires notBool Ghasrequests << SCHED >>
733+
734+
rule <k> #filterLogs IDX => .K ... </k>
735+
<schedule> SCHED </schedule>
736+
<log> LOGS </log>
737+
<depositRequests> DRQSTS </depositRequests>
738+
<requestsRoot> _ => #computeRequestsHash(DRQSTS) </requestsRoot>
739+
requires Ghasrequests << SCHED >> andBool IDX >=Int size(LOGS)
740+
741+
rule <k> #filterLogs IDX
742+
=> #parseDepositRequest {LOGS[IDX]}:>SubstateLogEntry
743+
// parse other request types
744+
~> #filterLogs IDX +Int 1
745+
...
746+
</k>
747+
<log> LOGS </log>
748+
<schedule> SCHED </schedule>
749+
requires IDX <Int size(LOGS) andBool Ghasrequests << SCHED >>
750+
```
751+
752+
Rules for parsing Deposit Requests according to EIP-6110.
753+
754+
```k
755+
syntax KItem ::= "#parseDepositRequest" SubstateLogEntry [symbol(#parseDepositRequest)]
756+
// ---------------------------------------------------------------------------------------
757+
rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => .K ... </k>
758+
<depositRequests> RS => RS ListItem(Int2Bytes(1, DEPOSIT_REQUEST_TYPE, BE) +Bytes #extractDepositData(DATA)) </depositRequests>
759+
requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
760+
andBool size(TOPICS) >Int 0
761+
andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
762+
andBool #isValidDepositEventData(DATA)
763+
764+
rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => #end EVMC_INVALID_BLOCK ... </k>
765+
requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
766+
andBool size(TOPICS) >Int 0
767+
andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
768+
andBool notBool #isValidDepositEventData(DATA)
769+
770+
rule <k> #parseDepositRequest _ => .K ... </k> [owise]
771+
```
717772
### Blobs
718773

719774
- `#validateBlockBlobs COUNT TXIDS`: Iterates through the transactions of the current block in order, counting up total versioned hashes (blob commitments) in the block.
@@ -790,9 +845,13 @@ Terminates validation successfully when all conditions are met or when blob vali
790845
syntax EthereumCommand ::= "#finalizeBlock"
791846
| #rewardOmmers ( JSONs ) [symbol(#rewardOmmers)]
792847
// --------------------------------------------------------------------------
793-
rule <k> #finalizeBlock => #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi
848+
rule <k> #finalizeBlock
849+
=> #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi
794850
~> #rewardOmmers(OMMERS)
795-
~> #finalizeBlockBlobs ... </k>
851+
~> #filterLogs 0
852+
~> #finalizeBlockBlobs
853+
...
854+
</k>
796855
<schedule> SCHED </schedule>
797856
<ommerBlockHeaders> [ OMMERS ] </ommerBlockHeaders>
798857
<coinbase> MINER </coinbase>

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

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,7 +48,7 @@ The following codes all indicate that the VM ended execution with an exception,
4848
| "EVMC_PRECOMPILE_FAILURE"
4949
| "EVMC_NONCE_EXCEEDED"
5050
| "EVMC_INVALID_BLOCK"
51-
// -------------------------------------------------------------
51+
// -----------------------------------------------------
5252
rule StatusCode2String(EVMC_FAILURE) => "EVMC_FAILURE"
5353
rule StatusCode2String(EVMC_INVALID_INSTRUCTION) => "EVMC_INVALID_INSTRUCTION"
5454
rule StatusCode2String(EVMC_UNDEFINED_INSTRUCTION) => "EVMC_UNDEFINED_INSTRUCTION"

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

Lines changed: 113 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,113 @@
1+
Implementation of Execution Layer Requests
2+
------------------------------------------
3+
```k
4+
requires "serialization.md"
5+
```
6+
7+
```k
8+
module EVM-REQUESTS
9+
imports SERIALIZATION
10+
```
11+
12+
A `requests` object consists of a `request_type` byte prepended to an opaque byte array `request_data`.
13+
The `request_data` contains zero or more encoded request objects.
14+
```
15+
requests = request_type ++ request_data
16+
```
17+
Each request type will define its own requests object with its own `request_data` format.
18+
19+
In order to compute the commitment, an intermediate hash list is first built by hashing all non-empty requests elements of the block requests list.
20+
Items with empty `request_data` are excluded, i.e. the intermediate list skips requests items which contain only the `request_type` (1 byte) and nothing else.
21+
22+
```k
23+
syntax Int ::= #computeRequestsHash(List) [function, symbol(#computeRequestsHash)]
24+
// ----------------------------------------------------------------------------------
25+
rule #computeRequestsHash(RS) => #parseHexWord(Sha256(#computeRequestsHashIntermediate(RS)))
26+
27+
syntax Bytes ::= #computeRequestsHashIntermediate(List) [function, symbol(#computeRequestsHashIntermediate)]
28+
| #computeRequestsHashIntermediate(List, Bytes) [function, symbol(#computeRequestsHashIntermediateAux)]
29+
// ----------------------------------------------------------------------------------------------------------------------
30+
rule #computeRequestsHashIntermediate(RS) => #computeRequestsHashIntermediate(RS, .Bytes)
31+
rule #computeRequestsHashIntermediate(.List, ACC) => ACC
32+
rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC)
33+
requires lengthBytes(R) <=Int 1
34+
rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC +Bytes Sha256raw(R))
35+
requires lengthBytes(R) >Int 1
36+
```
37+
38+
Deposit Requests
39+
----------------
40+
The structure denoting the new deposit request consists of the following fields:
41+
42+
1. `pubkey: Bytes48`
43+
2. `withdrawal_credentials: Bytes32`
44+
3. `amount: uint64`
45+
4. `signature: Bytes96`
46+
5. `index: uint64`
47+
48+
```k
49+
syntax Int ::= "DEPOSIT_REQUEST_TYPE" [macro]
50+
| "DEPOSIT_EVENT_LENGTH" [macro]
51+
| "DEPOSIT_CONTRACT_ADDRESS" [alias]
52+
| "DEPOSIT_EVENT_SIGNATURE_HASH" [alias]
53+
// -----------------------------------------------------
54+
rule DEPOSIT_REQUEST_TYPE => 0
55+
rule DEPOSIT_CONTRACT_ADDRESS => #parseAddr("0x00000000219ab540356cbb839cbe05303d7705fa")
56+
rule DEPOSIT_EVENT_SIGNATURE_HASH => #parseWord("0x649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c5")
57+
rule DEPOSIT_EVENT_LENGTH => 576
58+
59+
syntax Int ::= "PUBKEY_OFFSET" [macro]
60+
| "WITHDRAWAL_CREDENTIALS_OFFSET"[macro]
61+
| "AMOUNT_OFFSET" [macro]
62+
| "SIGNATURE_OFFSET" [macro]
63+
| "INDEX_OFFSET" [macro]
64+
| "PUBKEY_SIZE" [macro]
65+
| "WITHDRAWAL_CREDENTIALS_SIZE" [macro]
66+
| "AMOUNT_SIZE" [macro]
67+
| "SIGNATURE_SIZE" [macro]
68+
| "INDEX_SIZE" [macro]
69+
// -----------------------------------------------------
70+
rule PUBKEY_OFFSET => 160
71+
rule WITHDRAWAL_CREDENTIALS_OFFSET => 256
72+
rule AMOUNT_OFFSET => 320
73+
rule SIGNATURE_OFFSET => 384
74+
rule INDEX_OFFSET => 512
75+
rule PUBKEY_SIZE => 48
76+
rule WITHDRAWAL_CREDENTIALS_SIZE => 32
77+
rule AMOUNT_SIZE => 8
78+
rule SIGNATURE_SIZE => 96
79+
rule INDEX_SIZE => 8
80+
```
81+
82+
83+
84+
```k
85+
syntax Bytes ::= #extractDepositData ( Bytes ) [function, symbol(#extractDepositData)]
86+
// --------------------------------------------------------------------------------------
87+
rule #extractDepositData(DATA) => substrBytes(DATA, PUBKEY_OFFSET +Int 32, PUBKEY_OFFSET +Int 32 +Int PUBKEY_SIZE)
88+
+Bytes substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32 +Int WITHDRAWAL_CREDENTIALS_SIZE)
89+
+Bytes substrBytes(DATA, AMOUNT_OFFSET +Int 32, AMOUNT_OFFSET +Int 32 +Int AMOUNT_SIZE)
90+
+Bytes substrBytes(DATA, SIGNATURE_OFFSET +Int 32, SIGNATURE_OFFSET +Int 32 +Int SIGNATURE_SIZE)
91+
+Bytes substrBytes(DATA, INDEX_OFFSET +Int 32, INDEX_OFFSET +Int 32 +Int INDEX_SIZE)
92+
93+
syntax Bool ::= #isValidDepositEventData ( Bytes ) [function, symbol(#isValidDepositEventData), total]
94+
// ------------------------------------------------------------------------------------------------------
95+
rule #isValidDepositEventData(DATA) => true
96+
requires lengthBytes(DATA) ==Int DEPOSIT_EVENT_LENGTH
97+
andBool Bytes2Int(substrBytes(DATA, 0, 32), BE, Unsigned) ==Int PUBKEY_OFFSET
98+
andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_OFFSET
99+
andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) ==Int AMOUNT_OFFSET
100+
andBool Bytes2Int(substrBytes(DATA, 96, 128), BE, Unsigned) ==Int SIGNATURE_OFFSET
101+
andBool Bytes2Int(substrBytes(DATA, 128, 160), BE, Unsigned) ==Int INDEX_OFFSET
102+
andBool Bytes2Int(substrBytes(DATA, PUBKEY_OFFSET, PUBKEY_OFFSET +Int 32), BE, Unsigned) ==Int PUBKEY_SIZE
103+
andBool Bytes2Int(substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_SIZE
104+
andBool Bytes2Int(substrBytes(DATA, AMOUNT_OFFSET, AMOUNT_OFFSET +Int 32), BE, Unsigned) ==Int AMOUNT_SIZE
105+
andBool Bytes2Int(substrBytes(DATA, SIGNATURE_OFFSET, SIGNATURE_OFFSET +Int 32), BE, Unsigned) ==Int SIGNATURE_SIZE
106+
andBool Bytes2Int(substrBytes(DATA, INDEX_OFFSET, INDEX_OFFSET +Int 32), BE, Unsigned) ==Int INDEX_SIZE
107+
108+
rule #isValidDepositEventData(_) => false [owise]
109+
```
110+
111+
```k
112+
endmodule
113+
```

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

Lines changed: 6 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,6 +30,8 @@ module SCHEDULE
3030
| "Ghasrejectedfirstbyte" | "Ghasprevrandao" | "Ghasmaxinitcodesize" | "Ghaspushzero"
3131
| "Ghaswarmcoinbase" | "Ghaswithdrawals" | "Ghastransient" | "Ghasmcopy"
3232
| "Ghasbeaconroot" | "Ghaseip6780" | "Ghasblobbasefee" | "Ghasblobhash"
33+
| "Ghasrequests"
34+
// --------------------------------------
3335
```
3436

3537
### Schedule Constants
@@ -161,6 +163,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
161163
rule [GhasbeaconrootDefault]: Ghasbeaconroot << DEFAULT >> => false
162164
rule [Ghaseip6780Default]: Ghaseip6780 << DEFAULT >> => false
163165
rule [GhasblobhashDefault]: Ghasblobhash << DEFAULT >> => false
166+
rule [GhasrequestsDefault]: Ghasrequests << DEFAULT >> => false
164167
```
165168

166169
### Frontier Schedule
@@ -438,8 +441,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
438441
// --------------------------------------------------------------------------
439442
rule [SCHEDCONSTPrague]: SCHEDCONST < PRAGUE > => SCHEDCONST < CANCUN >
440443
441-
rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >>
442-
444+
rule [GhasrequestsPrague]: Ghasrequests << PRAGUE >> => true
445+
rule [SCHEDFLAGPrague]: SCHEDFLAG << PRAGUE >> => SCHEDFLAG << CANCUN >>
446+
requires notBool ( SCHEDFLAG ==K Ghasrequests )
443447
```
444448

445449
```k

0 commit comments

Comments
 (0)