Skip to content

EIP-7002 EIP-7251 - Implement Withdrawal and Consolidation request types #2762

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
wants to merge 10 commits into
base: master
Choose a base branch
from
Open

EIP-7002 EIP-7251 - Implement Withdrawal and Consolidation request types #2762

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
10 commits
Select commit Hold shift + click to select a range
9b54e11
refactor requests root generation
anvacaru May 8, 2025
01724b9
update expected output
anvacaru May 8, 2025
9bb5c2f
replace Bytes2Int with #asWord wrapper
anvacaru May 8, 2025
0bfb07d
Merge branch 'master' into eip-7685-2
anvacaru May 8, 2025
a22a28f
update execution-spec-tests/failing.llvm
anvacaru May 8, 2025
d7a099a
update execution-spec-tests/failing.llvm
anvacaru May 9, 2025
a7b259f
Merge branch 'eip-7685-2' into eip-7002
anvacaru May 12, 2025
16a0142
implement system calls to withdrawal and consolidation contracts
anvacaru May 12, 2025
2f081a6
update execution-spec-tests/failing.llvm
anvacaru May 12, 2025
8183ecb
Merge branch 'master' into eip-7002
anvacaru Jul 2, 2025
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
154 changes: 128 additions & 26 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -196,8 +196,9 @@ In the comments next to each cell, we've marked which component of the YellowPap
</withdrawals>

<requests>
<depositRequests> .List </depositRequests>
//other request types come here
<depositRequests> .Bytes </depositRequests>
<withdrawalRequests> .Bytes </withdrawalRequests>
<consolidationRequests> .Bytes </consolidationRequests>
</requests>

</network>
Expand Down Expand Up @@ -724,29 +725,21 @@ After executing a transaction, it's necessary to have the effect of the substate

### Fetching requests from event logs

While processing a block, multiple requests objects with different `request_types` will be produced by the system, and accumulated in the block requests list.
While processing a block, multiple deposit requests objects with will be produced by the system.
`#parseDepositRequest` function parses each log item produced in the block and fetches deposit requests.

```k
syntax KItem ::= "#filterLogs" Int [symbol(#filterLogs)]
// --------------------------------------------------------
rule <k> #filterLogs _ => .K ... </k> <schedule> SCHED </schedule> requires notBool Ghasrequests << SCHED >>

rule <k> #filterLogs IDX => .K ... </k>
<schedule> SCHED </schedule>
<log> LOGS </log>
<depositRequests> DRQSTS </depositRequests>
<requestsRoot> _ => #computeRequestsHash(DRQSTS) </requestsRoot>
requires Ghasrequests << SCHED >> andBool IDX >=Int size(LOGS)

rule <k> #filterLogs IDX
=> #parseDepositRequest {LOGS[IDX]}:>SubstateLogEntry
// parse other request types
~> #filterLogs IDX +Int 1
...
</k>
rule <k> #filterLogs IDX => #parseDepositRequest {LOGS[IDX]}:>SubstateLogEntry ~> #filterLogs IDX +Int 1 ... </k>
<statusCode> SC </statusCode>
<log> LOGS </log>
<schedule> SCHED </schedule>
requires IDX <Int size(LOGS) andBool Ghasrequests << SCHED >>
andBool notBool SC ==K EVMC_INVALID_BLOCK

rule <k> #filterLogs _ => .K ... </k> [owise]
rule <k> #halt ~> #filterLogs _ => .K ... </k>
```

Rules for parsing Deposit Requests according to EIP-6110.
Expand All @@ -755,7 +748,7 @@ Rules for parsing Deposit Requests according to EIP-6110.
syntax KItem ::= "#parseDepositRequest" SubstateLogEntry [symbol(#parseDepositRequest)]
// ---------------------------------------------------------------------------------------
rule <k> #parseDepositRequest { ADDR | TOPICS | DATA } => .K ... </k>
<depositRequests> RS => RS ListItem(Int2Bytes(1, DEPOSIT_REQUEST_TYPE, BE) +Bytes #extractDepositData(DATA)) </depositRequests>
<depositRequests> DEPOSIT_REQUESTS => DEPOSIT_REQUESTS +Bytes #extractDepositData(DATA) </depositRequests>
requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS
andBool size(TOPICS) >Int 0
andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH
Expand All @@ -769,6 +762,52 @@ Rules for parsing Deposit Requests according to EIP-6110.

rule <k> #parseDepositRequest _ => .K ... </k> [owise]
```

Retrieving requests from the output of a system call.
`#getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS` fetches the output of a system call and stores the output in the `<withdrawalRequests>` cell.
`#getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS` fetches the output of a system call and stores the output in the `<consolidationRequests>` cell.

```k
syntax KItem ::= "#getRequests" Int [symbol(#getRequests)]
// ----------------------------------------------------------
rule <k> #halt ~> #getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS => #popCallStack ~> #dropWorldState ~> #finalizeStorage(ListItem(WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS)) ... </k>
<output> WRQSTS </output>
<withdrawalRequests> _ => WRQSTS </withdrawalRequests>

rule <k> #halt ~> #getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS => #popCallStack ~> #dropWorldState ~> #finalizeStorage(ListItem(CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS)) ... </k>
<output> CRQSTS </output>
<consolidationRequests> _ => CRQSTS </consolidationRequests>

syntax KItem ::= "#checkRequestsRoot" Int [symbol(#checkRequestsRoot)]
| "#validateRequestsRoot" [symbol(#validateRequestsRoot)]
// ------------------------------------------------------------------------
rule <k> #validateRequestsRoot => #checkRequestsRoot #computeRequestsHash(ListItem(DEPOSIT_REQUEST_TYPE +Bytes DRQSTS) ListItem(WITHDRAWAL_REQUEST_TYPE +Bytes WRQSTS) ListItem(CONSOLIDATION_REQUEST_TYPE +Bytes CRQSTS)) ... </k>
<depositRequests> DRQSTS </depositRequests>
<withdrawalRequests> WRQSTS </withdrawalRequests>
<consolidationRequests> CRQSTS </consolidationRequests>

rule <k> #checkRequestsRoot REQUESTS_ROOT => .K ... </k> <requestsRoot> HEADER_REQUESTS_ROOT </requestsRoot> requires REQUESTS_ROOT ==K HEADER_REQUESTS_ROOT
rule <k> #checkRequestsRoot REQUESTS_ROOT => .K ... </k> <requestsRoot> HEADER_REQUESTS_ROOT </requestsRoot>
<statusCode> _ => EVMC_INVALID_BLOCK </statusCode>
requires notBool REQUESTS_ROOT ==K HEADER_REQUESTS_ROOT

syntax KItem ::= "#processGeneralPurposeRequests" [symbol(#processGeneralPurposeRequests)]
// ------------------------------------------------------------------------------------------
rule <k> #processGeneralPurposeRequests
=> #filterLogs 0
~> #systemCall WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS .Bytes ~> #getRequests WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS
~> #systemCall CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS .Bytes ~> #getRequests CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS
~> #validateRequestsRoot
...
</k>
<statusCode> SC </statusCode>
<schedule> SCHED </schedule>
requires Ghasrequests << SCHED >>
andBool SC in (SetItem(EVMC_SUCCESS) SetItem(EVMC_REVERT) SetItem(.StatusCode))

rule <k> #processGeneralPurposeRequests => .K ... </k> [owise]
```

### Blobs

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

```k
syntax EthereumCommand ::= "#executeBeaconRoots" [symbol(#executeBeaconRoots)]
// ------------------------------------------------------------------------------
syntax InternalOp ::= "#executeBeaconRoots" [symbol(#executeBeaconRoots)]
// -------------------------------------------------------------------------
rule <k> #executeBeaconRoots => .K ... </k>
<schedule> SCHED </schedule>
<timestamp> TS </timestamp>
<beaconRoot> BR </beaconRoot>
<account>
<acctID> 339909022928299415537769066420252604268194818 </acctID>
<acctID> BEACON_ROOTS_ADDRESS </acctID>
<storage> M:Map => M [(TS modInt 8191) <- TS] [(TS modInt 8191 +Int 8191) <- BR] </storage>
...
</account>
Expand All @@ -947,14 +986,14 @@ where `HISTORY_SERVE_WINDOW == 8191`.
Read more about EIP-2935 here [https://eips.ethereum.org/EIPS/eip-2935](https://eips.ethereum.org/EIPS/eip-2935).

```k
syntax EthereumCommand ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
// ----------------------------------------------------------------------------------------
syntax InternalOp ::= "#executeBlockHashHistory" [symbol(#executeBlockHashHistory)]
// -----------------------------------------------------------------------------------
rule <k> #executeBlockHashHistory => .K ... </k>
<schedule> SCHED </schedule>
<previousHash> HP </previousHash>
<number> BN </number>
<account>
<acctID> 21693734551179282564423033930679318143314229 </acctID>
<acctID> HISTORY_STORAGE_ADDRESS </acctID>
<storage> M:Map => M [((BN -Int 1) modInt 8191) <- HP] </storage>
...
</account>
Expand Down Expand Up @@ -1695,6 +1734,69 @@ The various `CALL*` (and other inter-contract control flow) operations will be d
rule #computeValidJumpDestsWithinBound(PGM, I, RESULT) => #computeValidJumpDests(PGM, I +Int #widthOpCode(PGM [ I ]), RESULT) requires notBool PGM [ I ] ==Int 91
```

System Calls
------------
Address Constants
- `SYSTEM_ADDRESS (0xfffffffffffffffffffffffffffffffffffffffe)`: Special address used for system operations
- `BEACON_ROOTS_ADDRESS (0x000F3df6D732807Ef1319fB7B8bB8522d0Beac02)`: Address for beacon chain root storage
- `HISTORY_STORAGE_ADDRESS (0x0000F90827F1C53a10cb7A02335B175320002935)`: Address for historical data storage

System Transaction Configuration
- `SYSTEMTXGAS (30000000)`: Special gas limit for system transactions
- Gas not counted against block gas limit
- No fee burn semantics apply to system transactions

## System Call Operations
- `#systemCall`: Top-level operation that initiates a system call
- Preserves execution context by pushing to call stack
- Preserves world state before making the call
- `#mkSystemCall`: Implementation operation that constructs the actual call
- Always sets caller to `SYSTEM_ADDRESS`
- Uses the system gas limit instead of standard call gas
- Performs call with zero value transfer

```k
syntax Int ::= "SYSTEM_ADDRESS" [alias]
| "BEACON_ROOTS_ADDRESS" [alias]
| "HISTORY_STORAGE_ADDRESS" [alias]
| "SYSTEMTXGAS" [macro]
// ------------------------------------
rule SYSTEM_ADDRESS => 1461501637330902918203684832716283019655932542974
rule BEACON_ROOTS_ADDRESS => 339909022928299415537769066420252604268194818
rule HISTORY_STORAGE_ADDRESS => 21693734551179282564423033930679318143314229
rule SYSTEMTXGAS => 30000000

syntax InternalOp ::= "#systemCall" Int Bytes [symbol(#systemCall)]
| "#mkSystemCall" Int Bytes [symbol(#mkSystemCall)]
// -----------------------------------------------------------------------
rule <k> #systemCall ACCTTO ARGS => #pushCallStack ~> #pushWorldState ~> #mkSystemCall ACCTTO ARGS ... </k>

rule <k> #mkSystemCall ACCTTO ARGS => #loadProgram CODE ~> #initVM ~> #execute ... </k>
<useGas> USEGAS:Bool </useGas>
<callDepth> CD => CD +Int 1 </callDepth>
<callData> _ => ARGS </callData>
<callValue> _ => 0 </callValue>
<id> _ => ACCTTO </id>
<gas> GAVAIL:Gas => #if USEGAS #then SYSTEMTXGAS:Gas #else GAVAIL:Gas #fi </gas>
<callGas> GCALL:Gas => #if USEGAS #then 0:Gas #else GCALL:Gas #fi </callGas>
<caller> _ => SYSTEM_ADDRESS </caller>
<static> _ => false </static>
<account>
<acctID> ACCTTO </acctID>
<code> CODE </code>
...
</account>

// rule <k> #mkSystemCall ACCTTO ARGS => #mkCall SYSTEM_ADDRESS ACCTTO ACCTTO CODE 0 ARGS false ... </k>
// <useGas> USEGAS </useGas>
// <callGas> GCALL => #if USEGAS #then SYSTEMTXGAS #else GCALL #fi </callGas>
// <account>
// <acctID> ACCTTO </acctID>
// <code> CODE </code>
// ...
// </account>
```

```k
syntax Int ::= #widthOpCode(Int) [symbol(#widthOpCode), function]
// -----------------------------------------------------------------
Expand Down
54 changes: 34 additions & 20 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -16,8 +16,10 @@ requests = request_type ++ request_data
```
Each request type will define its own requests object with its own `request_data` format.

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.
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.
Address constants:
- `DEPOSIT_CONTRACT_ADDRESS (0x00000000219ab540356cbb839cbe05303d7705fa)` : Predeployed contract for deposits.
- `WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS (0x00000961Ef480Eb55e80D19ad83579A64c007002)`: Predeployed contract for validator withdrawal requests (EIP-7002)
- `CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS (0x0000BBdDc7CE488642fb579f8B00f3a590007251)`: Predeployed contract for stake consolidation requests
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Just for consistency:

Suggested change
- `CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS (0x0000BBdDc7CE488642fb579f8B00f3a590007251)`: Predeployed contract for stake consolidation requests
- `CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS (0x0000BBdDc7CE488642fb579f8B00f3a590007251)`: Predeployed contract for stake consolidation requests (EIP-7251)


```k
syntax Int ::= #computeRequestsHash(List) [function, symbol(#computeRequestsHash)]
Expand All @@ -33,6 +35,22 @@ Items with empty `request_data` are excluded, i.e. the intermediate list skips r
requires lengthBytes(R) <=Int 1
rule #computeRequestsHashIntermediate(ListItem(R) RS, ACC) => #computeRequestsHashIntermediate(RS, ACC +Bytes Sha256raw(R))
requires lengthBytes(R) >Int 1

syntax Int ::= "DEPOSIT_EVENT_SIGNATURE_HASH" [alias]
| "WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS" [alias]
| "CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS" [alias]
// ----------------------------------------------------------------
rule DEPOSIT_CONTRACT_ADDRESS => 44667813780391404145283579356374304250
rule WITHDRAWAL_REQUEST_PREDEPLOY_ADDRESS => 817336022611862939366240017674853872070658
rule CONSOLIDATION_REQUEST_PREDEPLOY_ADDRESS => 16365465459783978374881923886502306505585233

syntax Bytes ::= "DEPOSIT_REQUEST_TYPE" [macro]
| "WITHDRAWAL_REQUEST_TYPE" [macro]
| "CONSOLIDATION_REQUEST_TYPE" [macro]
// -----------------------------------------------------
rule DEPOSIT_REQUEST_TYPE => b"\x00"
rule WITHDRAWAL_REQUEST_TYPE => b"\x01"
rule CONSOLIDATION_REQUEST_TYPE => b"\x02"
```

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

```k
syntax Int ::= "DEPOSIT_REQUEST_TYPE" [macro]
| "DEPOSIT_EVENT_LENGTH" [macro]
| "DEPOSIT_CONTRACT_ADDRESS" [alias]
| "DEPOSIT_EVENT_SIGNATURE_HASH" [alias]
// -----------------------------------------------------
rule DEPOSIT_REQUEST_TYPE => 0
rule DEPOSIT_CONTRACT_ADDRESS => #parseAddr("0x00000000219ab540356cbb839cbe05303d7705fa")
rule DEPOSIT_EVENT_SIGNATURE_HASH => #parseWord("0x649bbc62d0e31342afea4e5cd82d4049e7e1ee912fc0889aa790803be39038c5")
syntax Int ::= "DEPOSIT_EVENT_LENGTH" [macro]
| "DEPOSIT_CONTRACT_ADDRESS" [alias]
// -------------------------------------------------
rule DEPOSIT_EVENT_SIGNATURE_HASH => 45506446345753628416285423056165511379837572639148407563471291220684748896453
rule DEPOSIT_EVENT_LENGTH => 576

syntax Int ::= "PUBKEY_OFFSET" [macro]
Expand Down Expand Up @@ -94,16 +108,16 @@ The structure denoting the new deposit request consists of the following fields:
// ------------------------------------------------------------------------------------------------------
rule #isValidDepositEventData(DATA) => true
requires lengthBytes(DATA) ==Int DEPOSIT_EVENT_LENGTH
andBool Bytes2Int(substrBytes(DATA, 0, 32), BE, Unsigned) ==Int PUBKEY_OFFSET
andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_OFFSET
andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) ==Int AMOUNT_OFFSET
andBool Bytes2Int(substrBytes(DATA, 96, 128), BE, Unsigned) ==Int SIGNATURE_OFFSET
andBool Bytes2Int(substrBytes(DATA, 128, 160), BE, Unsigned) ==Int INDEX_OFFSET
andBool Bytes2Int(substrBytes(DATA, PUBKEY_OFFSET, PUBKEY_OFFSET +Int 32), BE, Unsigned) ==Int PUBKEY_SIZE
andBool Bytes2Int(substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32), BE, Unsigned) ==Int WITHDRAWAL_CREDENTIALS_SIZE
andBool Bytes2Int(substrBytes(DATA, AMOUNT_OFFSET, AMOUNT_OFFSET +Int 32), BE, Unsigned) ==Int AMOUNT_SIZE
andBool Bytes2Int(substrBytes(DATA, SIGNATURE_OFFSET, SIGNATURE_OFFSET +Int 32), BE, Unsigned) ==Int SIGNATURE_SIZE
andBool Bytes2Int(substrBytes(DATA, INDEX_OFFSET, INDEX_OFFSET +Int 32), BE, Unsigned) ==Int INDEX_SIZE
andBool #asWord(substrBytes(DATA, 0, 32)) ==Int PUBKEY_OFFSET
andBool #asWord(substrBytes(DATA, 32, 64)) ==Int WITHDRAWAL_CREDENTIALS_OFFSET
andBool #asWord(substrBytes(DATA, 64, 96)) ==Int AMOUNT_OFFSET
andBool #asWord(substrBytes(DATA, 96, 128)) ==Int SIGNATURE_OFFSET
andBool #asWord(substrBytes(DATA, 128, 160)) ==Int INDEX_OFFSET
andBool #asWord(substrBytes(DATA, PUBKEY_OFFSET, PUBKEY_OFFSET +Int 32)) ==Int PUBKEY_SIZE
andBool #asWord(substrBytes(DATA, WITHDRAWAL_CREDENTIALS_OFFSET, WITHDRAWAL_CREDENTIALS_OFFSET +Int 32)) ==Int WITHDRAWAL_CREDENTIALS_SIZE
andBool #asWord(substrBytes(DATA, AMOUNT_OFFSET, AMOUNT_OFFSET +Int 32)) ==Int AMOUNT_SIZE
andBool #asWord(substrBytes(DATA, SIGNATURE_OFFSET, SIGNATURE_OFFSET +Int 32)) ==Int SIGNATURE_SIZE
andBool #asWord(substrBytes(DATA, INDEX_OFFSET, INDEX_OFFSET +Int 32)) ==Int INDEX_SIZE

rule #isValidDepositEventData(_) => false [owise]
```
Expand Down
4 changes: 4 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/state-utils.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,9 @@ module STATE-UTILS
<excessBlobGas> _ => 0 </excessBlobGas>
<beaconRoot> _ => 0 </beaconRoot>
<requestsRoot> _ => 0 </requestsRoot>
<depositRequests> _ => .Bytes </depositRequests>
<withdrawalRequests> _ => .Bytes </withdrawalRequests>
<consolidationRequests> _ => .Bytes </consolidationRequests>

syntax EthereumCommand ::= "clearNETWORK"
// -----------------------------------------
Expand Down Expand Up @@ -193,6 +196,7 @@ The `"network"` key allows setting the fee schedule inside the test.
rule #asScheduleString("Cancun") => CANCUN
rule #asScheduleString("ShanghaiToCancunAtTime15k") => CANCUN
rule #asScheduleString("Prague") => PRAGUE
rule #asScheduleString("CancunToPragueAtTime15k") => PRAGUE
```

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