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

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

@@ -1696,7 +1696,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) [owise]
 
     syntax KItem ::= "#initVM"
  // --------------------------
@@ -2170,6 +2171,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]
@@ -2195,7 +2197,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]
@@ -2678,6 +2681,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
 ========================
 
@@ -3040,6 +3051,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>

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

@@ -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"
  // -------------------------------------------------------------------------------------------------------------------------------------------------------
 ```
 
@@ -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
@@ -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 >>