Skip to content

Commit 24787fb

Browse files
mariaKtanvacarudwightguth
authored
Eip4844 Point Evaluation precompile (#2701)
* Implementation of point evaluation precompile for EIP 4844. * Updated failing.llvm * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> * Update kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md - formatting Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> * Added definition of Gpointeval schedule constant, and updated #gasExec. * Added conditions to test the value of fields z and y vs BLS_MODULUS. * Replaced large constant BLS_MODULUS with a macro. * Updated failing.llvm list. --------- Co-authored-by: Andrei Văcaru <16517508+anvacaru@users.noreply.github.com> Co-authored-by: Dwight Guth <dwight.guth@pi2.network>
1 parent 5b0a0da commit 24787fb

File tree

4 files changed

+40
-34
lines changed

4 files changed

+40
-34
lines changed

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/evm.md‎

Lines changed: 29 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1914,6 +1914,7 @@ Precompiled Contracts
19141914
rule #precompiled(7) => ECMUL
19151915
rule #precompiled(8) => ECPAIRING
19161916
rule #precompiled(9) => BLAKE2F
1917+
rule #precompiled(10) => KZGPOINTEVAL
19171918
19181919
syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total]
19191920
// ----------------------------------------------------------------------------------------------------
@@ -1930,7 +1931,7 @@ Precompiled Contracts
19301931
rule #precompiledAccountsUB(LONDON) => #precompiledAccountsUB(BERLIN)
19311932
rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON)
19321933
rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE)
1933-
rule #precompiledAccountsUB(CANCUN) => #precompiledAccountsUB(SHANGHAI)
1934+
rule #precompiledAccountsUB(CANCUN) => 10
19341935
19351936
19361937
syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total]
@@ -1951,6 +1952,7 @@ Precompiled Contracts
19511952
- `ECMUL` performs scalar multiplication on the elliptic curve alt_bn128.
19521953
- `ECPAIRING` performs an optimal ate pairing check on the elliptic curve alt_bn128.
19531954
- `BLAKE2F` performs the compression function F used in the BLAKE2 hashing algorithm.
1955+
- `KZGPOINTEVAL` performs the point evaluation precompile that is part of EIP 4844.
19541956

19551957
```k
19561958
syntax PrecompiledOp ::= "ECREC"
@@ -2069,6 +2071,31 @@ Precompiled Contracts
20692071
rule <k> BLAKE2F => #end EVMC_PRECOMPILE_FAILURE ... </k>
20702072
<callData> DATA </callData>
20712073
requires lengthBytes( DATA ) =/=Int 213
2074+
2075+
syntax PrecompiledOp ::= "KZGPOINTEVAL"
2076+
// ---------------------------------------
2077+
// FIELD_ELEMENTS_PER_BLOB = 4096
2078+
rule <k> KZGPOINTEVAL => #end EVMC_SUCCESS ... </k>
2079+
<output> _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, blsModulus, BE) </output>
2080+
<callData> DATA </callData>
2081+
requires lengthBytes( DATA ) ==Int 192
2082+
andBool #kzg2vh(substrBytes(DATA, 96, 144)) ==K substrBytes(DATA, 0, 32)
2083+
andBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) <Int blsModulus
2084+
andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) <Int blsModulus
2085+
andBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192))
2086+
2087+
rule <k> KZGPOINTEVAL => #end EVMC_PRECOMPILE_FAILURE ... </k>
2088+
<callData> DATA </callData>
2089+
requires lengthBytes( DATA ) =/=Int 192
2090+
orBool #kzg2vh(substrBytes(DATA, 96, 144)) =/=K substrBytes(DATA, 0, 32)
2091+
orBool Bytes2Int(substrBytes(DATA, 32, 64), BE, Unsigned) >=Int blsModulus
2092+
orBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) >=Int blsModulus
2093+
orBool notBool verifyKZGProof(substrBytes(DATA, 96, 144), substrBytes(DATA, 32, 64), substrBytes(DATA, 64, 96), substrBytes(DATA, 144, 192))
2094+
2095+
syntax Bytes ::= #kzg2vh ( Bytes ) [symbol(#kzg2vh), function, total]
2096+
// ---------------------------------------------------------------------
2097+
// VERSIONED_HASH_VERSION_KZG = 0x01
2098+
rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1]
20722099
```
20732100

20742101

@@ -2421,6 +2448,7 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
24212448
rule <k> #gasExec(SCHED, ECMUL) => Gecmul < SCHED > ... </k>
24222449
rule <k> #gasExec(SCHED, ECPAIRING) => Gecpairconst < SCHED > +Int (lengthBytes(DATA) /Int 192) *Int Gecpaircoeff < SCHED > ... </k> <callData> DATA </callData>
24232450
rule <k> #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... </k> <callData> DATA </callData>
2451+
rule <k> #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... </k>
24242452
24252453
syntax InternalOp ::= "#allocateCallGas"
24262454
// ----------------------------------------

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/schedule.md‎

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -48,6 +48,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
4848
| "Gblockhash" | "Gquadcoeff" | "maxCodeSize" | "Rb" | "Gquaddivisor" | "Gecadd" | "Gecmul"
4949
| "Gecpairconst" | "Gecpaircoeff" | "Gfround" | "Gcoldsload" | "Gcoldaccountaccess" | "Gwarmstorageread" | "Gaccesslistaddress"
5050
| "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore"
51+
| "Gpointeval"
5152
// ----------------------------------------------------------------------------------------------------------------------------------------------------
5253
```
5354

@@ -117,6 +118,8 @@ A `ScheduleConst` is a constant determined by the fee schedule.
117118
rule Gwarmstorageread < DEFAULT > => 0
118119
rule Gwarmstoragedirtystore < DEFAULT > => 0
119120
121+
rule Gpointeval < DEFAULT > => 0
122+
120123
rule Gaccessliststoragekey < DEFAULT > => 0
121124
rule Gaccesslistaddress < DEFAULT > => 0
122125
@@ -390,8 +393,11 @@ A `ScheduleConst` is a constant determined by the fee schedule.
390393
syntax Schedule ::= "CANCUN" [symbol(CANCUN_EVM), smtlib(schedule_CANCUN)]
391394
// --------------------------------------------------------------------------
392395
rule Gwarmstoragedirtystore < CANCUN > => Gwarmstorageread < CANCUN >
396+
rule Gpointeval < CANCUN > => 50000
393397
rule SCHEDCONST < CANCUN > => SCHEDCONST < SHANGHAI >
394-
requires notBool (SCHEDCONST ==K Gwarmstoragedirtystore)
398+
requires notBool ( SCHEDCONST ==K Gwarmstoragedirtystore
399+
orBool SCHEDCONST ==K Gpointeval
400+
)
395401
396402
rule Ghastransient << CANCUN >> => true
397403
rule Ghasmcopy << CANCUN >> => true

‎kevm-pyk/src/kevm_pyk/kproj/evm-semantics/word.md‎

Lines changed: 4 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -466,6 +466,10 @@ The maximum and minimum values of each type are defined below.
466466
// ----------------------------------------------------------------------------------------------------------------------------------------
467467
rule eth => 1000000000000000000
468468
rule maxBlockNum => 57896044618658097711785492504343953926634992332820282019728792003956564819967
469+
470+
syntax Int ::= "blsModulus" [macro]
471+
// -----------------------------------
472+
rule blsModulus => 52435875175126190479447740508185965837690552500527637822603658699938581184513
469473
```
470474

471475
Range of types

‎tests/failing.llvm‎

Lines changed: 0 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -37,11 +37,9 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute
3737
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute_opcodes.json,*
3838
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_tx_attribute_value_opcode.json,*
3939
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/blob_type_tx_pre_fork.json,*
40-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/call_opcode_types.json,*
4140
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_decreasing_blob_gas_costs.json,*
4241
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_excess_blob_gas_calculation.json,*
4342
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/correct_increasing_blob_gas_costs.json,*
44-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/external_vectors.json,*
4543
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/fork_transition_excess_blob_gas.json,*
4644
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx_combinations.json,*
4745
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/insufficient_balance_blob_tx.json,*
@@ -53,7 +51,6 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_block_blo
5351
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_above_target_change.json,*
5452
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_change.json,*
5553
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_excess_blob_gas_target_blobs_increase_from_zero.json,*
56-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_inputs.json,*
5754
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_negative_excess_blob_gas.json,*
5855
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_non_multiple_excess_blob_gas.json,*
5956
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_normal_gas.json,*
@@ -64,15 +61,12 @@ BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_static_ex
6461
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_tx_blob_count.json,*
6562
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_tx_max_fee_per_blob_gas.json,*
6663
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/invalid_zero_excess_blob_gas_in_header.json,*
67-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/point_evaluation_precompile_gas_usage.json,*
6864
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/precompile_before_fork.json,*
6965
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/precompile_during_fork.json,*
7066
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/reject_valid_full_blob_in_block_rlp.json,*
7167
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/sufficient_balance_blob_tx.json,*
7268
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/sufficient_balance_blob_tx_pre_fund_tx.json,*
73-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/tx_entry_point.json,*
7469
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/valid_blob_tx_combinations.json,*
75-
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip4844_blobs/valid_inputs.json,*
7670
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/create_selfdestruct_same_tx.json,*
7771
BlockchainTests/GeneralStateTests/Pyspecs/cancun/eip6780_selfdestruct/dynamic_create2_selfdestruct_collision_multi_tx.json,*
7872
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
8781
BlockchainTests/GeneralStateTests/Pyspecs/frontier/opcodes/double_kill.json,*
8882
BlockchainTests/GeneralStateTests/Pyspecs/paris/security/tx_selfdestruct_balance_bug.json,*
8983
BlockchainTests/GeneralStateTests/Pyspecs/shanghai/eip4895_withdrawals/no_evm_execution.json,*
90-
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]
91-
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]
9284
BlockchainTests/GeneralStateTests/stEIP1559/lowFeeCap.json,*
9385
BlockchainTests/GeneralStateTests/stEIP1559/lowGasLimit.json,lowGasLimit_d0g0v0_Cancun
9486
BlockchainTests/GeneralStateTests/stEIP1559/lowGasPriceOldTypes.json,*
9587
BlockchainTests/GeneralStateTests/stEIP1559/tipTooHigh.json,*
9688
BlockchainTests/GeneralStateTests/stEIP1559/transactionIntinsicBug_Paris.json,*
97-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/idPrecomps.json,idPrecomps_d9g0v0_Cancun
98-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d117g0v0_Cancun
99-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d12g0v0_Cancun
100-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d135g0v0_Cancun
101-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d153g0v0_Cancun
102-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d171g0v0_Cancun
103-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d189g0v0_Cancun
104-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d207g0v0_Cancun
105-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d225g0v0_Cancun
106-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d243g0v0_Cancun
107-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d261g0v0_Cancun
108-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d279g0v0_Cancun
109-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d27g0v0_Cancun
110-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d297g0v0_Cancun
111-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d315g0v0_Cancun
112-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d333g0v0_Cancun
113-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d351g0v0_Cancun
114-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d369g0v0_Cancun
115-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d387g0v0_Cancun
116-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d45g0v0_Cancun
117-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d63g0v0_Cancun
118-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d81g0v0_Cancun
119-
BlockchainTests/GeneralStateTests/stPreCompiledContracts/precompsEIP2929Cancun.json,precompsEIP2929Cancun_d99g0v0_Cancun
120-
BlockchainTests/GeneralStateTests/stSpecialTest/failed_tx_xcf416c53_Paris.json,*

0 commit comments

Comments
 (0)