Skip to content

EIP-7951 - ECDSA signature verification over the secp256r1 elliptic curve #2837

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

Draft
anvacaru wants to merge 3 commits into
base: master
Choose a base branch
from
Draft

EIP-7951 - ECDSA signature verification over the secp256r1 elliptic curve #2837

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
3 commits
Select commit Hold shift + click to select a range
2a0ee0f
implement p256verify precompile
anvacaru Dec 16, 2025
b9e6b4d
Merge remote-tracking branch 'origin/master' into eip-7951
anvacaru Jan 14, 2026
00272c4
update gas price of the P256VERIFY precompile
anvacaru Jan 14, 2026
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
17 changes: 15 additions & 2 deletions 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 @@ -1695,7 +1695,8 @@ The various `CALL*` (and other inter-contract control flow) operations will be d

syntax Bool ::= #isPrecompiledAccount ( Int , Schedule ) [symbol(isPrecompiledAccount), function, total, smtlib(isPrecompiledAccount)]
// --------------------------------------------------------------------------------------------------------------------------------------
rule [isPrecompiledAccount]: #isPrecompiledAccount(ACCTCODE, SCHED) => 0 <Int ACCTCODE andBool ACCTCODE <=Int #precompiledAccountsUB(SCHED)
rule [isPrecompiledAccountOsaka]: #isPrecompiledAccount(256, OSAKA) => true
rule [isPrecompiledAccount]: #isPrecompiledAccount(ACCTCODE, SCHED) => 0 <Int ACCTCODE andBool ACCTCODE <=Int #precompiledAccountsUB(SCHED)

syntax KItem ::= "#initVM"
// --------------------------
Expand Down Expand Up @@ -2174,6 +2175,7 @@ Precompiled Contracts
rule #precompiled(15) => BLS12_PAIRING_CHECK
rule #precompiled(16) => BLS12_MAP_FP_TO_G1
rule #precompiled(17) => BLS12_MAP_FP2_TO_G2
rule #precompiled(256) => P256VERIFY


syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total]
Expand All @@ -2199,7 +2201,8 @@ Precompiled Contracts
syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total]
syntax Set ::= #precompiledAccountsSetAux ( Int ) [symbol(#precompiledAccountsSetAux), function, total]
// ------------------------------------------------------------------------------------------------------------
rule #precompiledAccountsSet(SCHED) => #precompiledAccountsSetAux(#precompiledAccountsUB(SCHED))
rule #precompiledAccountsSet(OSAKA) => #precompiledAccountsSetAux(#precompiledAccountsUB(OSAKA)) SetItem(256)
rule #precompiledAccountsSet(SCHED) => #precompiledAccountsSetAux(#precompiledAccountsUB(SCHED)) [owise]

rule #precompiledAccountsSetAux(N) => .Set requires N <=Int 0
rule #precompiledAccountsSetAux(N) => SetItem(N) #precompiledAccountsSetAux(N -Int 1) [owise, preserves-definedness]
Expand Down Expand Up @@ -2682,6 +2685,14 @@ Precompiled Contracts
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned))
```

```k
syntax PrecompiledOp ::= "P256VERIFY"
// -------------------------------------
rule <k> P256VERIFY => #end EVMC_SUCCESS ... </k>
<callData> DATA </callData>
<output> _ => P256Verify(DATA) </output>
```

Ethereum Gas Calculation
========================

Expand Down Expand Up @@ -3044,6 +3055,8 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
rule <k> #gasExec(SCHED, BLS12_MAP_FP_TO_G1) => Gbls12mapfptog1 < SCHED > ... </k>
rule <k> #gasExec(SCHED, BLS12_MAP_FP2_TO_G2) => Gbls12mapfp2tog2 < SCHED > ... </k>

rule <k> #gasExec(SCHED, P256VERIFY) => Gp256verify < SCHED > ... </k>

syntax InternalOp ::= "#allocateCallGas"
// ----------------------------------------
rule <k> GCALL:Gas ~> #allocateCallGas => .K ... </k>
Expand Down
8 changes: 6 additions & 2 deletions 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 @@ -53,7 +53,7 @@ A `ScheduleConst` is a constant determined by the fee schedule.
| "Gaccessliststoragekey" | "Rmaxquotient" | "Ginitcodewordcost" | "maxInitCodeSize" | "Gwarmstoragedirtystore"
| "Gpointeval" | "Gmaxblobgas" | "Gminbasefee" | "Gtargetblobgas" | "Gperblob" | "Blobbasefeeupdatefraction"
| "Gbls12g1add" | "Gbls12g1mul" | "Gbls12g2add" | "Gbls12g2mul" | "Gbls12mapfptog1" | "Gbls12PairingCheckMul"
| "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor"
| "Gbls12PairingCheckAdd" | "Gauthbase" | "Gbls12mapfp2tog2" | "Gtxdatafloor" | "Gp256verify"
// -------------------------------------------------------------------------------------------------------------------------------------------------------
```

Expand Down Expand Up @@ -149,6 +149,8 @@ A `ScheduleConst` is a constant determined by the fee schedule.
rule [Gbls12mapfptog1Default]: Gbls12mapfptog1 < DEFAULT > => 0
rule [Gbls12mapfp2tog2Default]: Gbls12mapfp2tog2 < DEFAULT > => 0

rule [Gp256verifyDefault]: Gp256verify < DEFAULT > => 0

rule [GselfdestructnewaccountDefault]: Gselfdestructnewaccount << DEFAULT >> => false
rule [GstaticcalldepthDefault]: Gstaticcalldepth << DEFAULT >> => true
rule [GemptyisnonexistentDefault]: Gemptyisnonexistent << DEFAULT >> => false
Expand Down Expand Up @@ -504,7 +506,9 @@ A `ScheduleConst` is a constant determined by the fee schedule.
```k
syntax Schedule ::= "OSAKA" [symbol(OSAKA_EVM), smtlib(schedule_OSAKA)]
// -----------------------------------------------------------------------
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
rule [Gp256verifyOsaka]: Gp256verify < OSAKA > => 6900
rule [SCHEDCONSTOsaka]: SCHEDCONST < OSAKA > => SCHEDCONST < PRAGUE >
requires notBool ( SCHEDCONST ==K Gp256verify )

rule [GhasclzOsaka]: Ghasclz << OSAKA >> => true
rule [SCHEDFLAGOsaka]: SCHEDFLAG << OSAKA >> => SCHEDFLAG << PRAGUE >>
Expand Down
Loading