Skip to content
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.

Sign up for GitHub

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

Eip4844 Point Evaluation precompile #2701

Merged
merged 11 commits into from
Feb 10, 2025
Merged

Eip4844 Point Evaluation precompile #2701

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
70cf86b
Implementation of point evaluation precompile for EIP 4844.
mariaKt Jan 23, 2025
5ebd32a
Updated failing.llvm
mariaKt Feb 3, 2025
09a43ad
Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting
mariaKt Feb 4, 2025
9ecc99f
Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting
mariaKt Feb 4, 2025
77920f6
Added definition of Gpointeval schedule constant, and updated #gasExec.
mariaKt Feb 4, 2025
7e40cbf
Added conditions to test the value of fields z and y vs BLS_MODULUS.
mariaKt Feb 4, 2025
b0c075e
Merge branch 'master' into eip4844-pointevalprec
mariaKt Feb 6, 2025
eaf0320
Merge branch 'master' into eip4844-pointevalprec
dwightguth Feb 6, 2025
99c8d82
Replaced large constant BLS_MODULUS with a macro.
mariaKt Feb 6, 2025
9a335d0
Updated failing.llvm list.
mariaKt Feb 8, 2025
bfc3950
Merge branch 'master' into eip4844-pointevalprec
dwightguth Feb 10, 2025
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
30 changes: 29 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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]
// ----------------------------------------------------------------------------------------------------
Expand All @@ -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]
Expand All @@ -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"
Expand Down Expand Up @@ -2069,6 +2071,31 @@ Precompiled Contracts
rule <k> BLAKE2F => #end EVMC_PRECOMPILE_FAILURE ... </k>
<callData> DATA </callData>
requires lengthBytes( DATA ) =/=Int 213

syntax PrecompiledOp ::= "KZGPOINTEVAL"
// ---------------------------------------
// FIELD_ELEMENTS_PER_BLOB = 4096
rule <k> KZGPOINTEVAL => #end EVMC_SUCCESS ... </k>
<output> _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, blsModulus, BE) </output>
<callData> DATA </callData>
requires lengthBytes( DATA ) ==Int 192
andBool #kzg2vh(substrBytes(DATA, 96, 144)) ==K substrBytes(DATA, 0, 32)
andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) <Int blsModulus
andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) <Int blsModulus
andBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192))

rule <k> KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... </k>
<callData> DATA </callData>
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]
```


Expand Down Expand Up @@ -2421,6 +2448,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
rule <k> #gasExec(SCHED, ECMUL) => Gecmul < SCHED > ... </k>
rule <k> #gasExec(SCHED, ECPAIRING) => Gecpairconst < SCHED > +Int (lengthBytes(DATA) /Int 192) *Int Gecpaircoeff < SCHED > ... </k> <callData> DATA </callData>
rule <k> #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... </k> <callData> DATA </callData>
rule <k> #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... </k>

syntax InternalOp ::= "#allocateCallGas"
// ----------------------------------------
Expand Down
8 changes: 7 additions & 1 deletion kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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"
// ----------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -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

Expand Down Expand Up @@ -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
Expand Down
4 changes: 4 additions & 0 deletions kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down
32 changes: 0 additions & 32 deletions tests/failing.llvm
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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,*
Expand All @@ -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,*
Expand All @@ -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,*
Expand All @@ -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,*
Loading