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 e37b4ff803..0d193b12e6 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..327ac57217 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 @@ -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] ``` diff --git a/tests/execution-spec-tests/failing.llvm b/tests/execution-spec-tests/failing.llvm index dfdcd6d866..935058a89e 100644 --- a/tests/execution-spec-tests/failing.llvm +++ b/tests/execution-spec-tests/failing.llvm @@ -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] 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""