Skip to content

EIP-7685 - Refactor requests root generation #2758

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.

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

Closed
wants to merge 8 commits into from
Closed
Show file tree
Hide file tree
Changes from all commits
Commits
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
6 changes: 3 additions & 3 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
Original file line number Diff line number Diff line change
Expand Up @@ -196,7 +196,7 @@ In the comments next to each cell, we've marked which component of the YellowPap
</withdrawals>

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

Expand Down Expand Up @@ -735,7 +735,7 @@ While processing a block, multiple requests objects with different `request_type
<schedule> SCHED </schedule>
<log> LOGS </log>
<depositRequests> DRQSTS </depositRequests>
<requestsRoot> _ => #computeRequestsHash(DRQSTS) </requestsRoot>
<requestsRoot> _ => #computeRequestsHash(ListItem(DEPOSIT_REQUEST_TYPE +Bytes DRQSTS)) </requestsRoot>
requires Ghasrequests << SCHED >> andBool IDX >=Int size(LOGS)

rule <k> #filterLogs IDX
Expand All @@ -755,7 +755,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 Down
31 changes: 15 additions & 16 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,9 +16,6 @@ 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.

```k
syntax Int ::= #computeRequestsHash(List) [function, symbol(#computeRequestsHash)]
// ----------------------------------------------------------------------------------
Expand All @@ -33,6 +30,10 @@ 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 Bytes ::= "DEPOSIT_REQUEST_TYPE" [macro]
// -----------------------------------------------
rule DEPOSIT_REQUEST_TYPE => b"\x00"
```

Deposit Requests
Expand All @@ -46,12 +47,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]
syntax Int ::= "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")
rule DEPOSIT_EVENT_LENGTH => 576
Expand Down Expand Up @@ -94,16 +93,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
9 changes: 0 additions & 9 deletions tests/execution-spec-tests/failing.llvm
Original file line number Diff line number Diff line change
Expand Up @@ -1639,17 +1639,8 @@ blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/
blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/block_hashes_history.json,*
blockchain_tests/prague/eip2935_historical_block_hashes_from_state/contract_deployment/system_contract_deployment.json,*
blockchain_tests/prague/eip6110_deposits/deposits/deposit_negative.json,*
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-many_deposits_from_contract]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposit_from_different_eoa]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposit_from_same_eoa_first_reverts]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposit_from_same_eoa_high_count]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposit_from_same_eoa_last_reverts]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposit_from_same_eoa]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-multiple_deposits_from_contract]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-single_deposit_from_contract_between_eoa_deposits]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-single_deposit_from_contract_single_deposit_from_eoa]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-single_deposit_from_eoa_between_contract_deposits]
blockchain_tests/prague/eip6110_deposits/deposits/deposit.json,tests/prague/eip6110_deposits/test_deposits.py::test_deposit[fork_Prague-blockchain_test-single_deposit_from_eoa_single_deposit_from_contract]
blockchain_tests/prague/eip7002_el_triggerable_withdrawals/contract_deployment/system_contract_deployment.json,*
blockchain_tests/prague/eip7002_el_triggerable_withdrawals/modified_withdrawal_contract/extra_withdrawals_pseudo_contract.json,tests/prague/eip7002_el_triggerable_withdrawals/test_modified_withdrawal_contract.py::test_extra_withdrawals_pseudo_contract[fork_Prague-blockchain_test-1_withdrawal_request]
blockchain_tests/prague/eip7002_el_triggerable_withdrawals/modified_withdrawal_contract/extra_withdrawals_pseudo_contract.json,tests/prague/eip7002_el_triggerable_withdrawals/test_modified_withdrawal_contract.py::test_extra_withdrawals_pseudo_contract[fork_Prague-blockchain_test-15_withdrawal_requests]
Expand Down
2 changes: 1 addition & 1 deletion tests/failing/ContractCreationSpam_d0g0v0.json.expected
Original file line number Diff line number Diff line change
Expand Up @@ -350,7 +350,7 @@
</withdrawals>
<requests>
<depositRequests>
.List
b""
</depositRequests>
</requests>
</network>
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -396,7 +396,7 @@
</withdrawals>
<requests>
<depositRequests>
.List
b""
</depositRequests>
</requests>
</network>
Expand Down