Skip to content

Commit d4f05a3

Browse files
anvacarupalinatolmach
anvacaru
and
palinatolmach
authored
EIP-7002 EIP-7251 - Implement Withdrawal and Consolidation request types (#2762)
* refactor requests root generation * update expected output * replace Bytes2Int with #asWord wrapper * update execution-spec-tests/failing.llvm * update execution-spec-tests/failing.llvm * implement system calls to withdrawal and consolidation contracts * update execution-spec-tests/failing.llvm * update failing.llvm * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md Co-authored-by: Palina <[email protected]> * fix typo * Remove commented code --------- Co-authored-by: Palina <[email protected]>
1 parent 4838fe2 commit d4f05a3

File tree

6 files changed

+173
-123
lines changed

6 files changed

+173
-123
lines changed

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

Lines changed: 119 additions & 26 deletions
Original file line numberDiff line numberDiff line change
@@ -196,8 +196,9 @@ In the comments next to each cell, we've marked which component of the YellowPap
196196
</withdrawals>
197197
198198
<requests>
199-
<depositRequests> .List </depositRequests>
200-
//other request types come here
199+
<depositRequests> .Bytes </depositRequests>
200+
<withdrawalRequests> .Bytes </withdrawalRequests>
201+
<consolidationRequests> .Bytes </consolidationRequests>
201202
</requests>
202203
203204
</network>
@@ -724,29 +725,21 @@ After executing a transaction, it's necessary to have the effect of the substate
724725

725726
### Fetching requests from event logs
726727

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+
While processing a block, multiple deposit requests objects with will be produced by the system.
729+
`#parseDepositRequest` function parses each log item produced in the block and fetches deposit requests.
728730

729731
```k
730732
syntax KItem ::= "#filterLogs" Int [symbol(#filterLogs)]
731733
// --------------------------------------------------------
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>
734+
rule <k> #filterLogs IDX => #parseDepositRequest {LOGS[IDX]}:>SubstateLogEntry ~> #filterLogs IDX +Int 1 ... </k>
735+
<statusCode> SC </statusCode>
747736
<log> LOGS </log>
748737
<schedule> SCHED </schedule>
749738
requires IDX <Int size(LOGS) andBool Ghasrequests << SCHED >>
739+
andBool notBool SC ==K EVMC_INVALID_BLOCK
740+
741+
rule <k> #filterLogs _ => .K ... </k> [owise]
742+
rule <k> #halt ~> #filterLogs _ => .K ... </k>
750743
```
751744

752745
Rules for parsing Deposit Requests according to EIP-6110.
@@ -755,7 +748,7 @@ Rules for parsing Deposit Requests according to EIP-6110.
755748
syntax KItem ::= "#parseDepositRequest" SubstateLogEntry [symbol(#parseDepositRequest)]
756749
// ---------------------------------------------------------------------------------------
757750
rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => .K ... </k>
758-
<depositRequests> RS => RS ListItem(Int2Bytes(1, DEPOSIT_REQUEST_TYPE, BE) +Bytes #extractDepositData(DATA)) </depositRequests>
751+
<depositRequests> DEPOSIT_REQUESTS => DEPOSIT_REQUESTS +Bytes #extractDepositData(DATA) </depositRequests>
759752
requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
760753
andBool size(TOPICS) >Int 0
761754
andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
@@ -769,6 +762,52 @@ Rules for parsing Deposit Requests according to EIP-6110.
769762
770763
rule <k> #parseDepositRequest _ => .K ... </k> [owise]
771764
```
765+
766+
Retrieving requests from the output of a system call.
767+
`#getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS` fetches the output of a system call and stores the output in the `<withdrawalRequests>` cell.
768+
`#getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS` fetches the output of a system call and stores the output in the `<consolidationRequests>` cell.
769+
770+
```k
771+
syntax KItem ::= "#getRequests" Int [symbol(#getRequests)]
772+
// ----------------------------------------------------------
773+
rule <k> #halt ~> #getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS => #popCallStack ~> #dropWorldState ~> #finalizeStorage(ListItem(WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS)) ... </k>
774+
<output> WRQSTS </output>
775+
<withdrawalRequests> _ => WRQSTS </withdrawalRequests>
776+
777+
rule <k> #halt ~> #getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS => #popCallStack ~> #dropWorldState ~> #finalizeStorage(ListItem(CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS)) ... </k>
778+
<output> CRQSTS </output>
779+
<consolidationRequests> _ => CRQSTS </consolidationRequests>
780+
781+
syntax KItem ::= "#checkRequestsRoot" Int [symbol(#checkRequestsRoot)]
782+
| "#validateRequestsRoot" [symbol(#validateRequestsRoot)]
783+
// ------------------------------------------------------------------------
784+
rule <k> #validateRequestsRoot => #checkRequestsRoot #computeRequestsHash(ListItem(DEPOSIT_REQUEST_TYPE +Bytes DRQSTS) ListItem(WITHDRAWAL_REQUEST_TYPE +Bytes WRQSTS) ListItem(CONSOLIDATION_REQUEST_TYPE +Bytes CRQSTS)) ... </k>
785+
<depositRequests> DRQSTS </depositRequests>
786+
<withdrawalRequests> WRQSTS </withdrawalRequests>
787+
<consolidationRequests> CRQSTS </consolidationRequests>
788+
789+
rule <k> #checkRequestsRoot REQUESTS_ROOT => .K ... </k> <requestsRoot> HEADER_REQUESTS_ROOT </requestsRoot> requires REQUESTS_ROOT ==K HEADER_REQUESTS_ROOT
790+
rule <k> #checkRequestsRoot REQUESTS_ROOT => .K ... </k> <requestsRoot> HEADER_REQUESTS_ROOT </requestsRoot>
791+
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
792+
requires notBool REQUESTS_ROOT ==K HEADER_REQUESTS_ROOT
793+
794+
syntax KItem ::= "#processGeneralPurposeRequests" [symbol(#processGeneralPurposeRequests)]
795+
// ------------------------------------------------------------------------------------------
796+
rule <k> #processGeneralPurposeRequests
797+
=> #filterLogs 0
798+
~> #systemCall WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS .Bytes ~> #getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS
799+
~> #systemCall CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS .Bytes ~> #getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS
800+
~> #validateRequestsRoot
801+
...
802+
</k>
803+
<statusCode> SC </statusCode>
804+
<schedule> SCHED </schedule>
805+
requires Ghasrequests << SCHED >>
806+
andBool SC in (SetItem(EVMC_SUCCESS) SetItem(EVMC_REVERT) SetItem(.StatusCode))
807+
808+
rule <k> #processGeneralPurposeRequests => .K ... </k> [owise]
809+
```
810+
772811
### Blobs
773812

774813
- `#validateBlockBlobs COUNT TXIDS`: Iterates through the transactions of the current block in order, counting up total versioned hashes (blob commitments) in the block.
@@ -848,7 +887,7 @@ Terminates validation successfully when all conditions are met or when blob vali
848887
rule <k> #finalizeBlock
849888
=> #if Ghaswithdrawals << SCHED >> #then #finalizeWithdrawals #else .K #fi
850889
~> #rewardOmmers(OMMERS)
851-
~> #filterLogs 0
890+
~> #processGeneralPurposeRequests
852891
~> #finalizeBlockBlobs
853892
...
854893
</k>
@@ -923,14 +962,14 @@ where `HISTORY_BUFFER_LENGTH == 8191`.
923962
Read more about EIP-4788 here [https://eips.ethereum.org/EIPS/eip-4788](https://eips.ethereum.org/EIPS/eip-4788).
924963

925964
```k
926-
syntax EthereumCommand ::= "#executeBeaconRoots" [symbol(#executeBeaconRoots)]
927-
// ------------------------------------------------------------------------------
965+
syntax InternalOp ::= "#executeBeaconRoots" [symbol(#executeBeaconRoots)]
966+
// -------------------------------------------------------------------------
928967
rule <k> #executeBeaconRoots => .K ... </k>
929968
<schedule> SCHED </schedule>
930969
<timestamp> TS </timestamp>
931970
<beaconRoot> BR </beaconRoot>
932971
<account>
933-
<acctID> 339909022928299415537769066420252604268194818 </acctID>
972+
<acctID> BEACON_ROOTS_ADDRESS </acctID>
934973
<storage> M:Map => M [(TS modInt 8191) <- TS] [(TS modInt 8191 +Int 8191) <- BR] </storage>
935974
...
936975
</account>
@@ -947,14 +986,14 @@ where `HISTORY_SERVE_WINDOW == 8191`.
947986
Read more about EIP-2935 here [https://eips.ethereum.org/EIPS/eip-2935](https://eips.ethereum.org/EIPS/eip-2935).
948987

949988
```k
950-
syntax EthereumCommand ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
951-
// ----------------------------------------------------------------------------------------
989+
syntax InternalOp ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
990+
// -----------------------------------------------------------------------------------
952991
rule <k> #executeBlockHashHistory => .K ... </k>
953992
<schedule> SCHED </schedule>
954993
<previousHash> HP </previousHash>
955994
<number> BN </number>
956995
<account>
957-
<acctID> 21693734551179282564423033930679318143314229 </acctID>
996+
<acctID> HISTORY_STORAGE_ADDRESS </acctID>
958997
<storage> M:Map => M [((BN -Int 1) modInt 8191) <- HP] </storage>
959998
...
960999
</account>
@@ -1695,6 +1734,60 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
16951734
rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) requires notBool PGM [ I ] ==Int 91
16961735
```
16971736

1737+
System Calls
1738+
------------
1739+
Address Constants
1740+
- `SYSTEM_ADDRESS (0xfffffffffffffffffffffffffffffffffffffffe)`: Special address used for system operations
1741+
- `BEACON_ROOTS_ADDRESS (0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02)`: Address for beacon chain root storage
1742+
- `HISTORY_STORAGE_ADDRESS (0x0000F90827F1C53a10cb7A02335B175320002935)`: Address for historical data storage
1743+
1744+
System Transaction Configuration
1745+
- `SYSTEMTXGAS (30000000)`: Special gas limit for system transactions
1746+
- Gas not counted against block gas limit
1747+
- No fee burn semantics apply to system transactions
1748+
1749+
## System Call Operations
1750+
- `#systemCall`: Top-level operation that initiates a system call
1751+
- Preserves execution context by pushing to call stack
1752+
- Preserves world state before making the call
1753+
- `#mkSystemCall`: Implementation operation that constructs the actual call
1754+
- Always sets caller to `SYSTEM_ADDRESS`
1755+
- Uses the system gas limit instead of standard call gas
1756+
- Performs call with zero value transfer
1757+
1758+
```k
1759+
syntax Int ::= "SYSTEM_ADDRESS" [alias]
1760+
| "BEACON_ROOTS_ADDRESS" [alias]
1761+
| "HISTORY_STORAGE_ADDRESS" [alias]
1762+
| "SYSTEMTXGAS" [macro]
1763+
// ------------------------------------
1764+
rule SYSTEM_ADDRESS => 1461501637330902918203684832716283019655932542974
1765+
rule BEACON_ROOTS_ADDRESS => 339909022928299415537769066420252604268194818
1766+
rule HISTORY_STORAGE_ADDRESS => 21693734551179282564423033930679318143314229
1767+
rule SYSTEMTXGAS => 30000000
1768+
1769+
syntax InternalOp ::= "#systemCall" Int Bytes [symbol(#systemCall)]
1770+
| "#mkSystemCall" Int Bytes [symbol(#mkSystemCall)]
1771+
// -----------------------------------------------------------------------
1772+
rule <k> #systemCall ACCTTO ARGS => #pushCallStack ~> #pushWorldState ~> #mkSystemCall ACCTTO ARGS ... </k>
1773+
1774+
rule <k> #mkSystemCall ACCTTO ARGS => #loadProgram CODE ~> #initVM ~> #execute ... </k>
1775+
<useGas> USEGAS:Bool </useGas>
1776+
<callDepth> CD => CD +Int 1 </callDepth>
1777+
<callData> _ => ARGS </callData>
1778+
<callValue> _ => 0 </callValue>
1779+
<id> _ => ACCTTO </id>
1780+
<gas> GAVAIL:Gas => #if USEGAS #then SYSTEMTXGAS:Gas #else GAVAIL:Gas #fi </gas>
1781+
<callGas> GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi </callGas>
1782+
<caller> _ => SYSTEM_ADDRESS </caller>
1783+
<static> _ => false </static>
1784+
<account>
1785+
<acctID> ACCTTO </acctID>
1786+
<code> CODE </code>
1787+
...
1788+
</account>
1789+
```
1790+
16981791
```k
16991792
syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function]
17001793
// -----------------------------------------------------------------

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

Lines changed: 34 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -16,8 +16,10 @@ requests = request_type ++ request_data
1616
```
1717
Each request type will define its own requests object with its own `request_data` format.
1818

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.
19+
Address constants:
20+
- `DEPOSIT_CONTRACT_ADDRESS (0x00000000219ab540356cbb839cbe05303d7705fa)` : Predeployed contract for deposits.
21+
- `WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS (0x00000961Ef480Eb55e80D19ad83579A64c007002)`: Predeployed contract for validator withdrawal requests (EIP-7002)
22+
- `CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS (0x0000BBdDc7CE488642fb579f8B00f3a590007251)`: Predeployed contract for stake consolidation requests (EIP-7251)
2123

2224
```k
2325
syntax Int ::= #computeRequestsHash(List) [function, symbol(#computeRequestsHash)]
@@ -33,6 +35,22 @@ Items with empty `request_data` are excluded, i.e. the intermediate list skips r
3335
requires lengthBytes(R) <=Int 1
3436
rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC +Bytes Sha256raw(R))
3537
requires lengthBytes(R) >Int 1
38+
39+
syntax Int ::= "DEPOSIT_EVENT_SIGNATURE_HASH" [alias]
40+
| "WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS" [alias]
41+
| "CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS" [alias]
42+
// ----------------------------------------------------------------
43+
rule DEPOSIT_CONTRACT_ADDRESS => 44667813780391404145283579356374304250
44+
rule WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS => 817336022611862939366240017674853872070658
45+
rule CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS => 16365465459783978374881923886502306505585233
46+
47+
syntax Bytes ::= "DEPOSIT_REQUEST_TYPE" [macro]
48+
| "WITHDRAWAL_REQUEST_TYPE" [macro]
49+
| "CONSOLIDATION_REQUEST_TYPE" [macro]
50+
// -----------------------------------------------------
51+
rule DEPOSIT_REQUEST_TYPE => b"\x00"
52+
rule WITHDRAWAL_REQUEST_TYPE => b"\x01"
53+
rule CONSOLIDATION_REQUEST_TYPE => b"\x02"
3654
```
3755

3856
Deposit Requests
@@ -46,14 +64,10 @@ The structure denoting the new deposit request consists of the following fields:
4664
5. `index: uint64`
4765

4866
```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")
67+
syntax Int ::= "DEPOSIT_EVENT_LENGTH" [macro]
68+
| "DEPOSIT_CONTRACT_ADDRESS" [alias]
69+
// -------------------------------------------------
70+
rule DEPOSIT_EVENT_SIGNATURE_HASH => 45506446345753628416285423056165511379837572639148407563471291220684748896453
5771
rule DEPOSIT_EVENT_LENGTH => 576
5872
5973
syntax Int ::= "PUBKEY_OFFSET" [macro]
@@ -94,16 +108,16 @@ The structure denoting the new deposit request consists of the following fields:
94108
// ------------------------------------------------------------------------------------------------------
95109
rule #isValidDepositEventData(DATA) => true
96110
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
111+
andBool #asWord(substrBytes(DATA, 0, 32)) ==Int PUBKEY_OFFSET
112+
andBool #asWord(substrBytes(DATA, 32, 64)) ==Int WITHDRAWAL_CREDENTIALS_OFFSET
113+
andBool #asWord(substrBytes(DATA, 64, 96)) ==Int AMOUNT_OFFSET
114+
andBool #asWord(substrBytes(DATA, 96, 128)) ==Int SIGNATURE_OFFSET
115+
andBool #asWord(substrBytes(DATA, 128, 160)) ==Int INDEX_OFFSET
116+
andBool #asWord(substrBytes(DATA, PUBKEY_OFFSET, PUBKEY_OFFSET +Int 32)) ==Int PUBKEY_SIZE
117+
andBool #asWord(substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32)) ==Int WITHDRAWAL_CREDENTIALS_SIZE
118+
andBool #asWord(substrBytes(DATA, AMOUNT_OFFSET, AMOUNT_OFFSET +Int 32)) ==Int AMOUNT_SIZE
119+
andBool #asWord(substrBytes(DATA, SIGNATURE_OFFSET, SIGNATURE_OFFSET +Int 32)) ==Int SIGNATURE_SIZE
120+
andBool #asWord(substrBytes(DATA, INDEX_OFFSET, INDEX_OFFSET +Int 32)) ==Int INDEX_SIZE
107121
108122
rule #isValidDepositEventData(_) => false [owise]
109123
```

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

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -78,6 +78,9 @@ module STATE-UTILS
7878
<excessBlobGas> _ => 0 </excessBlobGas>
7979
<beaconRoot> _ => 0 </beaconRoot>
8080
<requestsRoot> _ => 0 </requestsRoot>
81+
<depositRequests> _ => .Bytes </depositRequests>
82+
<withdrawalRequests> _ => .Bytes </withdrawalRequests>
83+
<consolidationRequests> _ => .Bytes </consolidationRequests>
8184
8285
syntax EthereumCommand ::= "clearNETWORK"
8386
// -----------------------------------------
@@ -193,6 +196,7 @@ The `"network"` key allows setting the fee schedule inside the test.
193196
rule #asScheduleString("Cancun") => CANCUN
194197
rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN
195198
rule #asScheduleString("Prague") => PRAGUE
199+
rule #asScheduleString("CancunToPragueAtTime15k") => PRAGUE
196200
```
197201

198202
- `#parseJSONs2List` parse a JSON object with string values into a list of value.

0 commit comments

Comments
 (0)