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 40828738bd..220674dbcc 100644 --- a/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md +++ b/kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md @@ -1914,6 +1914,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] // ---------------------------------------------------------------------------------------------------- @@ -1930,7 +1931,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] @@ -1951,6 +1952,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" @@ -2069,6 +2071,31 @@ Precompiled Contracts rule BLAKE2F => #end EVMC_PRECOMPILE_FAILURE ... DATA requires lengthBytes( DATA ) =/=Int 213 + + syntax PrecompiledOp ::= "KZGPOINTEVAL" + // --------------------------------------- + // FIELD_ELEMENTS_PER_BLOB = 4096 + rule KZGPOINTEVAL => #end EVMC_SUCCESS ... + _ => 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 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] + // --------------------------------------------------------------------- + // VERSIONED_HASH_VERSION_KZG = 0x01 + rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1] ``` @@ -2421,6 +2448,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(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 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 diff --git a/tests/failing.llvm b/tests/failing.llvm index 4bdedde40f..61f5dcf34c 100644 --- a/tests/failing.llvm +++ b/tests/failing.llvm @@ -37,11 +37,9 @@ 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/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 +51,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 +61,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 +81,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,*