From 9b54e11c93991d53d860ede0fbc0968585b5b2e5 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 8 May 2025 10:56:14 +0300 Subject: [PATCH 1/5] refactor requests root generation --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 6 +++--- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md | 11 +++++------ 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md index 6d3b725789..83580d9722 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -196,7 +196,7 @@ In the comments next to each cell, we've marked which component of the YellowPap - .List + .Bytes //other request types come here @@ -735,7 +735,7 @@ While processing a block, multiple requests objects with different `request_type SCHED LOGS DRQSTS - _ => #computeRequestsHash(DRQSTS) + _ => #computeRequestsHash(ListItem(DEPOSIT_REQUEST_TYPE +Bytes DRQSTS)) requires Ghasrequests << SCHED >> andBool IDX >=Int size(LOGS) rule #filterLogs IDX @@ -755,7 +755,7 @@ Rules for parsing Deposit Requests according to EIP-6110. syntax KItem ::= "#parseDepositRequest" SubstateLogEntry [symbol(#parseDepositRequest)] // --------------------------------------------------------------------------------------- rule #parseDepositRequest { ADDR | TOPICS | DATA } => .K ... - RS => RS ListItem(Int2Bytes(1, DEPOSIT_REQUEST_TYPE, BE) +Bytes #extractDepositData(DATA)) + DEPOSIT_REQUESTS => DEPOSIT_REQUESTS +Bytes #extractDepositData(DATA) requires ADDR ==K DEPOSIT_CONTRACT_ADDRESS andBool size(TOPICS) >Int 0 andBool {TOPICS[0]}:>Int ==Int DEPOSIT_EVENT_SIGNATURE_HASH diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md index 6a2bdf5ee2..97b790c800 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md @@ -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)] // ---------------------------------------------------------------------------------- @@ -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 @@ -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 From 01724b9f367eca92f83abbf3443b9d2a17961a2a Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 8 May 2025 12:00:37 +0300 Subject: [PATCH 2/5] update expected output --- tests/failing/ContractCreationSpam_d0g0v0.json.expected | 2 +- ...ic_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/tests/failing/ContractCreationSpam_d0g0v0.json.expected b/tests/failing/ContractCreationSpam_d0g0v0.json.expected index 2166b31441..a339be6ce7 100644 --- a/tests/failing/ContractCreationSpam_d0g0v0.json.expected +++ b/tests/failing/ContractCreationSpam_d0g0v0.json.expected @@ -350,7 +350,7 @@ - .List + b"" diff --git a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected index d4aa7e29a6..e37923678d 100644 --- a/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected +++ b/tests/failing/static_callcodecallcodecall_110_OOGMAfter_2_d0g0v0.json.expected @@ -396,7 +396,7 @@ - .List + b"" From 9bb5c2f3d025818b2c3628bea2b4f85624bcccb1 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 8 May 2025 12:24:49 +0300 Subject: [PATCH 3/5] replace Bytes2Int with #asWord wrapper --- .../kevm_pyk/kproj/evm-semantics/requests.md | 20 +++++++++---------- 1 file changed, 10 insertions(+), 10 deletions(-) diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md index 97b790c800..327ac57217 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/requests.md @@ -93,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] ``` From a22a28f5e63550ff08bebbdeb9fa69f2631b72f2 Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Thu, 8 May 2025 16:46:19 +0300 Subject: [PATCH 4/5] update execution-spec-tests/failing.llvm --- tests/execution-spec-tests/failing.llvm | 11 ----------- 1 file changed, 11 deletions(-) diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index faaf4259e5..43a2b55aaa 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1693,18 +1693,7 @@ blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_inp blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/block_hashes_history_at_transition.json,* 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] From d7a099a878c147202e196ee38adefd4a2259590f Mon Sep 17 00:00:00 2001 From: Andrei <16517508+anvacaru@users.noreply.github.com> Date: Fri, 9 May 2025 13:47:33 +0300 Subject: [PATCH 5/5] update execution-spec-tests/failing.llvm --- tests/execution-spec-tests/failing.llvm | 2 ++ 1 file changed, 2 insertions(+) diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index 43a2b55aaa..4d4c81216f 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -1693,6 +1693,8 @@ blockchain_tests/prague/eip2537_bls_12_381_precompiles/bls12_variable_length_inp blockchain_tests/prague/eip2935_historical_block_hashes_from_state/block_hashes/block_hashes_history_at_transition.json,* 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-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_last_reverts] 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]