From 70cf86b99c32e5cf7edc81c1dcf7007345ebbda5 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Thu, 23 Jan 2025 12:59:36 -0600 Subject: [PATCH 1/8] Implementation of point evaluation precompile for EIP 4844. --- .../src/kevm_pyk/kproj/evm-semantics/evm.md | 27 ++++++++++++++++++- 1 file changed, 26 insertions(+), 1 deletion(-) 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 0eea58e296..3321766fd9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1907,6 +1907,7 @@ Precompiled Contracts rule #precompiled(7) => ECMUL rule #precompiled(8) => ECPAIRING rule #precompiled(9) => BLAKE2F + rule #precompiled(10) => KZGPOINTEVAL syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total] // ---------------------------------------------------------------------------------------------------- @@ -1923,7 +1924,7 @@ Precompiled Contracts rule #precompiledAccountsUB(LONDON) => #precompiledAccountsUB(BERLIN) rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON) rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE) - rule #precompiledAccountsUB(CANCUN) => #precompiledAccountsUB(SHANGHAI) + rule #precompiledAccountsUB(CANCUN) => 10 syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total] @@ -1944,6 +1945,7 @@ Precompiled Contracts - `ECMUL` performs scalar multiplication on the elliptic curve alt_bn128. - `ECPAIRING` performs an optimal ate pairing check on the elliptic curve alt_bn128. - `BLAKE2F` performs the compression function F used in the BLAKE2 hashing algorithm. +- `KZGPOINTEVAL` performs the point evaluation precompile that is part of EIP 4844. ```k syntax PrecompiledOp ::= "ECREC" @@ -2062,6 +2064,28 @@ Precompiled Contracts rule BLAKE2F => #end EVMC_PRECOMPILE_FAILURE ... DATA requires lengthBytes( DATA ) =/=Int 213 + + syntax PrecompiledOp ::= "KZGPOINTEVAL" + // ---------------------------------- + // FIELD_ELEMENTS_PER_BLOB = 4096 + // BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513 + rule KZGPOINTEVAL => #end EVMC_SUCCESS ... + _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, 52435875175126190479447740508185965837690552500527637822603658699938581184513, BE) + DATA + requires lengthBytes( DATA ) ==Int 192 + andBool #kzg2vh(substrBytes(DATA, 96, 144)) ==K substrBytes(DATA, 0, 32) + andBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192)) + + rule KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... + DATA + requires lengthBytes( DATA ) =/=Int 192 + orBool #kzg2vh(substrBytes(DATA, 96, 144)) =/=K substrBytes(DATA, 0, 32) + orBool notBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192)) + + syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total] + // ------------------------------------------------------------------------------------------------------------- + // VERSIONED_HASH_VERSION_KZG = 0x01 + rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1] ``` @@ -2414,6 +2438,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, ECMUL) => Gecmul < SCHED > ... rule #gasExec(SCHED, ECPAIRING) => Gecpairconst < SCHED > +Int (lengthBytes(DATA) /Int 192) *Int Gecpaircoeff < SCHED > ... DATA rule #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... DATA + rule #gasExec(_, KZGPOINTEVAL) => 50000 ... syntax InternalOp ::= "#allocateCallGas" // ---------------------------------------- From 5ebd32a1fd9948b5b9fe2a0ad833fd857a661192 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Mon, 3 Feb 2025 13:54:23 -0600 Subject: [PATCH 2/8] Updated failing.llvm --- tests/failing.llvm | 56 ++++++++++++++++++++-------------------------- 1 file changed, 24 insertions(+), 32 deletions(-) diff --git a/tests/failing.llvm b/tests/failing.llvm index 4bdedde40f..2c5fdf07a7 100644 --- a/tests/failing.llvm +++ b/tests/failing.llvm @@ -37,11 +37,33 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute_opcodes.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute_value_opcode.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_type_tx_pre_fork.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/call_opcode_types.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_decreasing_blob_gas_costs.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_excess_blob_gas_calculation.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_increasing_blob_gas_costs.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,* +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_1ce8e4f69d5df899] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_26b753dec0560daa] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_31ebd010e6098750] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_392169c16a2e5ef6] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_3c1e8b38219e3e12] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_3c87ec986c2656c2] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_420f2a187ce77035] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_444b73ff54a19b44] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_7db4f140a955dd1a] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_83e53423a2dd93fe] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_9b24f8997145435c] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_af669445747d2585] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_af8b75f664ed7d43] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_b6cb6698327d9835] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_b6ec3736f9ff2c62] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_c5e1490d672d026d] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_cae5d3491190b777] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_d0992bc0387790a4] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_d736268229bd87ec] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_e68d7111a2364a49] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_ed6b180ec759bcf6] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f0ed3dc11cdeb130] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f47eb9fc139f6bfd] +BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f7f44e1e864aa967] BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/fork_transition_excess_blob_gas.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx_combinations.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx.json,* @@ -53,7 +75,6 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_block_blo BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_above_target_change.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_change.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_target_blobs_increase_from_zero.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_inputs.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_negative_excess_blob_gas.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_non_multiple_excess_blob_gas.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_normal_gas.json,* @@ -64,15 +85,12 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_static_ex BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_tx_blob_count.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_tx_max_fee_per_blob_gas.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_zero_excess_blob_gas_in_header.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/point_evaluation_precompile_gas_usage.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/precompile_before_fork.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/precompile_during_fork.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/reject_valid_full_blob_in_block_rlp.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/sufficient_balance_blob_tx.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/sufficient_balance_blob_tx_pre_fund_tx.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/tx_entry_point.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/valid_blob_tx_combinations.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/valid_inputs.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/create_selfdestruct_same_tx.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision_multi_tx.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision_two_different_transactions.json,* @@ -87,34 +105,8 @@ BlockchainTests/GeneralStateTests/Pyspecs/constantinople/eip1014_create2/recreat BlockchainTests/GeneralStateTests/Pyspecs/frontier/opcodes/double_kill.json,* BlockchainTests/GeneralStateTests/Pyspecs/paris/security/tx_selfdestruct_balance_bug.json,* BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/no_evm_execution.json,* -BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/withdrawing_to_precompiles.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_0x000000000000000000000000000000000000000a-blockchain_test-amount_0] -BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/withdrawing_to_precompiles.json,src/GeneralStateTestsFiller/Pyspecs/shanghai/eip4895_withdrawals/test_withdrawals.py::test_withdrawing_to_precompiles[fork_Cancun-precompile_0x000000000000000000000000000000000000000a-blockchain_test-amount_1] BlockchainTests/GeneralStateTests/stEIP1559/lowFeeCap.json,* BlockchainTests/GeneralStateTests/stEIP1559/lowGasLimit.json,lowGasLimit_d0g0v0_Cancun BlockchainTests/GeneralStateTests/stEIP1559/lowGasPriceOldTypes.json,* BlockchainTests/GeneralStateTests/stEIP1559/tipTooHigh.json,* BlockchainTests/GeneralStateTests/stEIP1559/transactionIntinsicBug_Paris.json,* -BlockchainTests/GeneralStateTests/stPreCompiledContracts/idPrecomps.json,idPrecomps_d9g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d117g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d12g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d135g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d153g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d171g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d189g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d207g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d225g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d243g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d261g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d279g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d27g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d297g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d315g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d333g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d351g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d369g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d387g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d45g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d63g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d81g0v0_Cancun -BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d99g0v0_Cancun -BlockchainTests/GeneralStateTests/stSpecialTest/failed_tx_xcf416c53_Paris.json,* From 09a43ade68c06fbec2059cc9873b472aa25ca64a Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 4 Feb 2025 11:50:06 -0600 Subject: [PATCH 3/8] Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 3321766fd9..09898ecf53 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2066,7 +2066,7 @@ Precompiled Contracts requires lengthBytes( DATA ) =/=Int 213 syntax PrecompiledOp ::= "KZGPOINTEVAL" - // ---------------------------------- + // --------------------------------------- // FIELD_ELEMENTS_PER_BLOB = 4096 // BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513 rule KZGPOINTEVAL => #end EVMC_SUCCESS ... From 9ecc99febcada6f44470427863abb50aa0d41d73 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 4 Feb 2025 11:50:39 -0600 Subject: [PATCH 4/8] Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 09898ecf53..9b44f5671b 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2083,7 +2083,7 @@ Precompiled Contracts orBool notBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192)) syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total] - // ------------------------------------------------------------------------------------------------------------- + // --------------------------------------------------------------------- // VERSIONED_HASH_VERSION_KZG = 0x01 rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1] ``` From 77920f60cfb41559942fd547c22e6a3e25ca7cf8 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 4 Feb 2025 12:58:06 -0600 Subject: [PATCH 5/8] Added definition of Gpointeval schedule constant, and updated #gasExec. --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 2 +- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md | 8 +++++++- 2 files changed, 8 insertions(+), 2 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 9b44f5671b..b6996200c9 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2438,7 +2438,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H). rule #gasExec(SCHED, ECMUL) => Gecmul < SCHED > ... rule #gasExec(SCHED, ECPAIRING) => Gecpairconst < SCHED > +Int (lengthBytes(DATA) /Int 192) *Int Gecpaircoeff < SCHED > ... DATA rule #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... DATA - rule #gasExec(_, KZGPOINTEVAL) => 50000 ... + rule #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... syntax InternalOp ::= "#allocateCallGas" // ---------------------------------------- diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md index 74ddf6fdcb..651aae5327 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md @@ -48,6 +48,7 @@ A `ScheduleConst` is a constant determined by the fee schedule. | "Gblockhash" | "Gquadcoeff" | "maxCodeSize" | "Rb" | "Gquaddivisor" | "Gecadd" | "Gecmul" | "Gecpairconst" | "Gecpaircoeff" | "Gfround" | "Gcoldsload" | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress" | "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore" + | "Gpointeval" // ---------------------------------------------------------------------------------------------------------------------------------------------------- ``` @@ -117,6 +118,8 @@ A `ScheduleConst` is a constant determined by the fee schedule. rule Gwarmstorageread < DEFAULT > => 0 rule Gwarmstoragedirtystore < DEFAULT > => 0 + rule Gpointeval < DEFAULT > => 0 + rule Gaccessliststoragekey < DEFAULT > => 0 rule Gaccesslistaddress < DEFAULT > => 0 @@ -390,8 +393,11 @@ A `ScheduleConst` is a constant determined by the fee schedule. syntax Schedule ::= "CANCUN" [symbol(CANCUN_EVM), smtlib(schedule_CANCUN)] // -------------------------------------------------------------------------- rule Gwarmstoragedirtystore < CANCUN > => Gwarmstorageread < CANCUN > + rule Gpointeval < CANCUN > => 50000 rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI > - requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore) + requires notBool ( SCHEDCONST ==K Gwarmstoragedirtystore + orBool SCHEDCONST ==K Gpointeval + ) rule Ghastransient << CANCUN >> => true rule Ghasmcopy << CANCUN >> => true From 7e40cbf48bcf000dc5bc36904a6a03994b8d3524 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Tue, 4 Feb 2025 17:46:04 -0600 Subject: [PATCH 6/8] Added conditions to test the value of fields z and y vs BLS_MODULUS. --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 4 ++++ 1 file changed, 4 insertions(+) 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 b6996200c9..f953ab949e 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2074,12 +2074,16 @@ Precompiled Contracts DATA requires lengthBytes( DATA ) ==Int 192 andBool #kzg2vh(substrBytes(DATA, 96, 144)) ==K substrBytes(DATA, 0, 32) + andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... DATA requires lengthBytes( DATA ) =/=Int 192 orBool #kzg2vh(substrBytes(DATA, 96, 144)) =/=K substrBytes(DATA, 0, 32) + orBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) >=Int 52435875175126190479447740508185965837690552500527637822603658699938581184513 + orBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) >=Int 52435875175126190479447740508185965837690552500527637822603658699938581184513 orBool notBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192)) syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total] From 99c8d82e85d3db2cc1bf5eaaebd50f33b2235479 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Thu, 6 Feb 2025 14:59:13 -0600 Subject: [PATCH 7/8] Replaced large constant BLS_MODULUS with a macro. --- kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md | 11 +++++------ kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md | 4 ++++ 2 files changed, 9 insertions(+), 6 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 922cee534f..220674dbcc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -2075,22 +2075,21 @@ Precompiled Contracts syntax PrecompiledOp ::= "KZGPOINTEVAL" // --------------------------------------- // FIELD_ELEMENTS_PER_BLOB = 4096 - // BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513 rule KZGPOINTEVAL => #end EVMC_SUCCESS ... - _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, 52435875175126190479447740508185965837690552500527637822603658699938581184513, BE) + _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, blsModulus, BE) DATA requires lengthBytes( DATA ) ==Int 192 andBool #kzg2vh(substrBytes(DATA, 96, 144)) ==K substrBytes(DATA, 0, 32) - andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... DATA requires lengthBytes( DATA ) =/=Int 192 orBool #kzg2vh(substrBytes(DATA, 96, 144)) =/=K substrBytes(DATA, 0, 32) - orBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) >=Int 52435875175126190479447740508185965837690552500527637822603658699938581184513 - orBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) >=Int 52435875175126190479447740508185965837690552500527637822603658699938581184513 + orBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) >=Int blsModulus + orBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) >=Int blsModulus orBool notBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192)) syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total] diff --git a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md index dd631d43bf..07f848a89d 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md @@ -466,6 +466,10 @@ The maximum and minimum values of each type are defined below. // ---------------------------------------------------------------------------------------------------------------------------------------- rule eth => 1000000000000000000 rule maxBlockNum => 57896044618658097711785492504343953926634992332820282019728792003956564819967 + + syntax Int ::= "blsModulus" [macro] + // ----------------------------------- + rule blsModulus => 52435875175126190479447740508185965837690552500527637822603658699938581184513 ``` Range of types From 9a335d03ed2ae5520ecaf43b2374e8cdeb9b4917 Mon Sep 17 00:00:00 2001 From: Maria Kotsifakou Date: Fri, 7 Feb 2025 18:05:39 -0600 Subject: [PATCH 8/8] Updated failing.llvm list. --- tests/failing.llvm | 24 ------------------------ 1 file changed, 24 deletions(-) diff --git a/tests/failing.llvm b/tests/failing.llvm index 2c5fdf07a7..61f5dcf34c 100644 --- a/tests/failing.llvm +++ b/tests/failing.llvm @@ -40,30 +40,6 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_type_tx_pre_ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_decreasing_blob_gas_costs.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_excess_blob_gas_calculation.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_increasing_blob_gas_costs.json,* -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_1ce8e4f69d5df899] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_26b753dec0560daa] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_31ebd010e6098750] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_392169c16a2e5ef6] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_3c1e8b38219e3e12] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_3c87ec986c2656c2] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_420f2a187ce77035] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_444b73ff54a19b44] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_7db4f140a955dd1a] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_83e53423a2dd93fe] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_9b24f8997145435c] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_af669445747d2585] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_af8b75f664ed7d43] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_b6cb6698327d9835] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_b6ec3736f9ff2c62] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_c5e1490d672d026d] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_cae5d3491190b777] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_d0992bc0387790a4] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_d736268229bd87ec] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_e68d7111a2364a49] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_ed6b180ec759bcf6] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f0ed3dc11cdeb130] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f47eb9fc139f6bfd] -BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,src/GeneralStateTestsFiller/Pyspecs/cancun/eip4844_blobs/test_point_evaluation_precompile.py::test_external_vectors[fork_Cancun-blockchain_test-versioned_hash_None-verify_kzg_proof_case_correct_proof_f7f44e1e864aa967] BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/fork_transition_excess_blob_gas.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx_combinations.json,* BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx.json,*