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

Open
wants to merge 6 commits into
base: master
Choose a base branch
from
+61 −34
Open

Eip4844 Point Evaluation precompile #2701

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
6 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
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
31 changes: 30 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 @@ -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]
// ----------------------------------------------------------------------------------------------------
Expand All @@ -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]
Expand All @@ -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"
Expand Down Expand Up @@ -2062,6 +2064,32 @@ 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
// BLS_MODULUS = 52435875175126190479447740508185965837690552500527637822603658699938581184513
rule <k> KZGPOINTEVAL => #end EVMC_SUCCESS ... </k>
<output> _ => Int2Bytes(32, 4096, BE) +Bytes Int2Bytes(32, 52435875175126190479447740508185965837690552500527637822603658699938581184513, 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 52435875175126190479447740508185965837690552500527637822603658699938581184513
andBool Bytes2Int(substrBytes(DATA, 64, 96), BE, Unsigned) <Int 52435875175126190479447740508185965837690552500527637822603658699938581184513
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 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]
// ---------------------------------------------------------------------
// VERSIONED_HASH_VERSION_KZG = 0x01
rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1]
```


Expand Down Expand Up @@ -2414,6 +2442,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
Loading
Loading