Skip to content

Commit 7fb1f9a

Browse files
anvacarugregorymakodzeba
anvacaru
and
gregorymakodzeba
authored
EIP 2537 - Precompile for BLS12-381 curve operations (#2759)
* implement precompiles for eip-2537 * update execution-spec-tests/failing.llvm * EIP-7691: Blob throughput increase (#2757) * update blob throughput values * update execution-spec-tests/failing.llvm * update execution-spec-tests/failing.llvm * adding funding.json to qualify evm-semantics for optimism retrofunding round (#2760) adding funding.json to qualify evm-semantics for optimism retrofunding round * replace #asWord with Bytes2Int in BLS12_G1ADD --------- Co-authored-by: Gregory Makodzeba <73550323+gregorymakodzeba@users.noreply.github.com>
1 parent 68b6d3c commit 7fb1f9a

4 files changed

Lines changed: 671 additions & 73 deletions

File tree

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

Lines changed: 339 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -2045,6 +2045,14 @@ Precompiled Contracts
20452045
rule #precompiled(8) => ECPAIRING
20462046
rule #precompiled(9) => BLAKE2F
20472047
rule #precompiled(10) => KZGPOINTEVAL
2048+
rule #precompiled(11) => BLS12_G1ADD
2049+
rule #precompiled(12) => BLS12_G1MSM
2050+
rule #precompiled(13) => BLS12_G2ADD
2051+
rule #precompiled(14) => BLS12_G2MSM
2052+
rule #precompiled(15) => BLS12_PAIRING_CHECK
2053+
rule #precompiled(16) => BLS12_MAP_FP_TO_G1
2054+
rule #precompiled(17) => BLS12_MAP_FP2_TO_G2
2055+
20482056
20492057
syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total]
20502058
// ----------------------------------------------------------------------------------------------------
@@ -2062,7 +2070,7 @@ Precompiled Contracts
20622070
rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON)
20632071
rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE)
20642072
rule #precompiledAccountsUB(CANCUN) => 10
2065-
rule #precompiledAccountsUB(PRAGUE) => #precompiledAccountsUB(CANCUN)
2073+
rule #precompiledAccountsUB(PRAGUE) => 17
20662074
20672075
20682076
syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total]
@@ -2229,6 +2237,327 @@ Precompiled Contracts
22292237
rule #kzg2vh ( C ) => Sha256rawWrapper(C)[0 <- 1]
22302238
```
22312239

2240+
- `BLS12_G1ADD` performs point addition in G1 (curve over base prime field)
2241+
- `BLS12_G1MSM` performs multi-scalar-multiplication (MSM) in G1 (curve over base prime field)
2242+
- `BLS12_G2ADD` performs point addition in G2 (curve over quadratic extension of the base prime field)
2243+
- `BLS12_G2MSM` to perform multi-scalar-multiplication (MSM) in G2 (curve over quadratic extension of the base prime field)
2244+
- `BLS12_PAIRING_CHECK` performs a pairing operations between a set of pairs of (G1, G2) points
2245+
- `BLS12_MAP_FP_TO_G1` maps base field element into the G1 point
2246+
- `BLS12_MAP_FP2_TO_G2` maps extension field element into the G2 point
2247+
2248+
```k
2249+
syntax Bytes ::= #bls12point ( G1Point ) [symbol(#bls12point1), function]
2250+
// -------------------------------------------------------------------------
2251+
rule #bls12point((X, Y)) => #padToWidth(64, #asByteStack(X)) +Bytes #padToWidth(64, #asByteStack(Y))
2252+
2253+
syntax Bytes ::= #bls12point ( G2Point ) [symbol(#bls12point2), function]
2254+
// -------------------------------------------------------------------------
2255+
rule #bls12point((X0 x X1, Y0 x Y1))
2256+
=> #padToWidth(64, #asByteStack(X0)) +Bytes #padToWidth(64, #asByteStack(X1))
2257+
+Bytes #padToWidth(64, #asByteStack(Y0)) +Bytes #padToWidth(64, #asByteStack(Y1))
2258+
2259+
syntax Bool ::= isValidBLS12Coordinate ( Int ) [symbol(isValidBLS12Coordinate), function, total]
2260+
// -----------------------------------------------------------------------------------------------
2261+
rule isValidBLS12Coordinate(X) => isValidBLS12Fp(X)
2262+
2263+
syntax Bool ::= isValidBLS12Fp ( Int ) [symbol(isValidBLS12Fp), function, total]
2264+
// -------------------------------------------------------------------------------
2265+
rule isValidBLS12Fp(X) => X >=Int 0 andBool X <Int (1 <<Int 384) andBool X <Int BLS12_FIELD_MODULUS
2266+
2267+
syntax Bool ::= isValidBLS12Scalar ( Int ) [symbol(isValidBLS12Scalar), function, total]
2268+
// ---------------------------------------------------------------------------------------
2269+
rule isValidBLS12Scalar(X) => X >=Int 0 andBool X <Int (1 <<Int 256)
2270+
```
2271+
2272+
```k
2273+
syntax PrecompiledOp ::= "BLS12_G1ADD"
2274+
// --------------------------------------
2275+
rule <k> BLS12_G1ADD => #end EVMC_SUCCESS ... </k>
2276+
<callData> DATA </callData>
2277+
<output>
2278+
_ => #bls12point(BLS12G1Add
2279+
( ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2280+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2281+
)
2282+
, ( Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2283+
, Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2284+
)
2285+
))
2286+
</output>
2287+
requires lengthBytes( DATA ) ==Int 256
2288+
andBool bls12ValidForAdd
2289+
( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2290+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2291+
, Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2292+
, Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2293+
)
2294+
2295+
rule <k> BLS12_G1ADD => #end EVMC_PRECOMPILE_FAILURE ... </k>
2296+
<callData> DATA </callData>
2297+
requires lengthBytes( DATA ) =/=Int 256
2298+
orBool notBool bls12ValidForAdd
2299+
( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2300+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2301+
, Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2302+
, Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2303+
)
2304+
2305+
syntax Bool ::= bls12ValidForAdd(Int, Int, Int, Int) [function, total]
2306+
// -----------------------------------------------------------------------
2307+
rule bls12ValidForAdd(X0, Y0, X1, Y1)
2308+
=> true
2309+
andBool isValidBLS12Coordinate(X0)
2310+
andBool isValidBLS12Coordinate(Y0)
2311+
andBool isValidBLS12Coordinate(X1)
2312+
andBool isValidBLS12Coordinate(Y1)
2313+
andBool BLS12G1OnCurve((X0, Y0))
2314+
andBool BLS12G1OnCurve((X1, Y1))
2315+
2316+
syntax PrecompiledOp ::= "BLS12_G1MSM"
2317+
// --------------------------------------
2318+
// Note that the implementation of `g1_lincomb_fast` has the following comment:
2319+
//
2320+
// * @remark While this function is significantly faster than g1_lincomb_naive(), we refrain from
2321+
// * using it in security-critical places (like verification) because the blst Pippenger code has not
2322+
// * been audited. In those critical places, we prefer using g1_lincomb_naive() which is much simpler.
2323+
//
2324+
// https://github.com/ethereum/c-kzg-4844/blob/cc33b779cd3a227f51b35ce519a83cf91d81ccea/src/common/lincomb.c#L54-L56
2325+
2326+
rule <k> BLS12_G1MSM => bls12G1Msm(DATA) ... </k> <callData> DATA </callData>
2327+
2328+
rule <k> g1MsmResult(P:G1Point) => #end EVMC_SUCCESS ... </k> <output> _ => #bls12point(P) </output>
2329+
2330+
rule <k> g1MsmError => #end EVMC_PRECOMPILE_FAILURE ... </k>
2331+
2332+
syntax G1MsmResult ::= "g1MsmError" | g1MsmResult(G1Point)
2333+
| bls12G1Msm(Bytes) [symbol(bls12G1Msm), function, total]
2334+
| #bls12G1Msm(Bytes, List, List) [function, total]
2335+
| #bls12G1MsmCheck(Bytes, List, List, Int, Int, Int) [function, total]
2336+
// -------------------------------------------------------------------------------------------
2337+
rule bls12G1Msm(B:Bytes) => g1MsmError requires lengthBytes(B) ==Int 0
2338+
rule bls12G1Msm(B:Bytes) => #bls12G1Msm(B, .List, .List) requires lengthBytes(B) >Int 0
2339+
2340+
rule #bls12G1Msm(B:Bytes, Ps:List, Ss:List) => g1MsmResult(BLS12G1Msm(... scalars: Ss, points: Ps))
2341+
requires lengthBytes(B) ==Int 0
2342+
rule #bls12G1Msm(B:Bytes, _:List, _:List) => g1MsmError
2343+
requires 0 <Int lengthBytes(B) andBool lengthBytes(B) <Int 160
2344+
rule #bls12G1Msm(B:Bytes, Ps:List, Ss:List)
2345+
=> #bls12G1MsmCheck
2346+
( substrBytes(B, 160, lengthBytes(B)), Ps, Ss
2347+
, Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
2348+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
2349+
, Bytes2Int(substrBytes(B, 128, 160), BE, Unsigned)
2350+
)
2351+
requires 160 <=Int lengthBytes(B)
2352+
2353+
rule #bls12G1MsmCheck(B:Bytes, Ps:List, Ss:List, X:Int, Y:Int, N:Int)
2354+
=> #bls12G1Msm(B, Ps ListItem( ( X , Y ) ), Ss ListItem( N ))
2355+
requires isValidBLS12Coordinate(X) andBool isValidBLS12Coordinate(Y)
2356+
andBool isValidBLS12Scalar(N)
2357+
andBool BLS12G1InSubgroup((X, Y))
2358+
rule #bls12G1MsmCheck(_, _, _, _, _, _) => g1MsmError [owise]
2359+
2360+
syntax PrecompiledOp ::= "BLS12_G2ADD"
2361+
// --------------------------------------
2362+
rule <k> BLS12_G2ADD => #end EVMC_SUCCESS ... </k>
2363+
<callData> DATA </callData>
2364+
<output>
2365+
_ => #bls12point(BLS12G2Add
2366+
( ( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2367+
x Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2368+
, Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2369+
x Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2370+
)
2371+
, ( Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned)
2372+
x Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned)
2373+
, Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned)
2374+
x Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned)
2375+
)
2376+
))
2377+
</output>
2378+
requires lengthBytes( DATA ) ==Int 512
2379+
andBool bls12ValidForAdd2
2380+
( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2381+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2382+
, Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2383+
, Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2384+
, Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned)
2385+
, Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned)
2386+
, Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned)
2387+
, Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned)
2388+
)
2389+
2390+
rule <k> BLS12_G2ADD => #end EVMC_PRECOMPILE_FAILURE ... </k>
2391+
<callData> DATA </callData>
2392+
requires lengthBytes( DATA ) =/=Int 512
2393+
orBool notBool bls12ValidForAdd2
2394+
( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2395+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2396+
, Bytes2Int(substrBytes(DATA, 128, 192), BE, Unsigned)
2397+
, Bytes2Int(substrBytes(DATA, 192, 256), BE, Unsigned)
2398+
, Bytes2Int(substrBytes(DATA, 256, 320), BE, Unsigned)
2399+
, Bytes2Int(substrBytes(DATA, 320, 384), BE, Unsigned)
2400+
, Bytes2Int(substrBytes(DATA, 384, 448), BE, Unsigned)
2401+
, Bytes2Int(substrBytes(DATA, 448, 512), BE, Unsigned)
2402+
)
2403+
2404+
syntax Bool ::= bls12ValidForAdd2(Int, Int, Int, Int, Int, Int, Int, Int) [function, total]
2405+
// --------------------------------------------------------------------------------------------
2406+
rule bls12ValidForAdd2(PX0, PX1, PY0, PY1, QX0, QX1, QY0, QY1)
2407+
=> true
2408+
andBool isValidBLS12Coordinate(PX0)
2409+
andBool isValidBLS12Coordinate(PX1)
2410+
andBool isValidBLS12Coordinate(PY0)
2411+
andBool isValidBLS12Coordinate(PY1)
2412+
andBool isValidBLS12Coordinate(QX0)
2413+
andBool isValidBLS12Coordinate(QX1)
2414+
andBool isValidBLS12Coordinate(QY0)
2415+
andBool isValidBLS12Coordinate(QY1)
2416+
andBool BLS12G2OnCurve((PX0 x PX1, PY0 x PY1))
2417+
andBool BLS12G2OnCurve((QX0 x QX1, QY0 x QY1))
2418+
2419+
syntax PrecompiledOp ::= "BLS12_G2MSM"
2420+
// -------------------------------------
2421+
rule <k> BLS12_G2MSM => bls12G2Msm(DATA) ... </k> <callData> DATA </callData>
2422+
2423+
rule <k> g2MsmResult(P:G2Point) => #end EVMC_SUCCESS ... </k>
2424+
<output> _ => #bls12point(P) </output>
2425+
2426+
rule <k> g2MsmError => #end EVMC_PRECOMPILE_FAILURE ... </k>
2427+
2428+
syntax G2MsmResult ::= "g2MsmError" | g2MsmResult(G2Point)
2429+
| bls12G2Msm(Bytes) [symbol(bls12G2Msm), function, total]
2430+
| #bls12G2Msm(Bytes, List, List) [function, total]
2431+
| #bls12G2MsmCheck(Bytes, List, List, Int, Int, Int, Int, Int) [function, total]
2432+
// -----------------------------------------------------------------------------------------------------
2433+
rule bls12G2Msm(B:Bytes) => g2MsmError requires lengthBytes(B) ==Int 0
2434+
rule bls12G2Msm(B:Bytes) => #bls12G2Msm(B, .List, .List) requires lengthBytes(B) >Int 0
2435+
2436+
rule #bls12G2Msm(B:Bytes, Ps:List, Ss:List) => g2MsmResult(BLS12G2Msm(... scalars: Ss, points: Ps))
2437+
requires lengthBytes(B) ==Int 0
2438+
rule #bls12G2Msm(B:Bytes, _:List, _:List) => g2MsmError
2439+
requires 0 <Int lengthBytes(B) andBool lengthBytes(B) <Int 288
2440+
rule #bls12G2Msm(B:Bytes, Ps:List, Ss:List)
2441+
=> #bls12G2MsmCheck
2442+
( substrBytes(B, 288, lengthBytes(B)), Ps, Ss
2443+
, Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
2444+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
2445+
, Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned)
2446+
, Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned)
2447+
, Bytes2Int(substrBytes(B, 256, 288), BE, Unsigned)
2448+
)
2449+
requires 288 <=Int lengthBytes(B)
2450+
2451+
rule #bls12G2MsmCheck(B:Bytes, Ps:List, Ss:List, X0:Int, X1:Int, Y0:Int, Y1:Int, N:Int)
2452+
=> #bls12G2Msm(B, Ps ListItem( ( X0 x X1, Y0 x Y1 ) ), Ss ListItem( N ))
2453+
requires isValidBLS12Coordinate(X0) andBool isValidBLS12Coordinate(X1)
2454+
andBool isValidBLS12Coordinate(Y0) andBool isValidBLS12Coordinate(Y1)
2455+
andBool isValidBLS12Scalar(N)
2456+
andBool BLS12G2InSubgroup(( X0 x X1, Y0 x Y1 ))
2457+
rule #bls12G2MsmCheck(_, _, _, _, _, _, _, _) => g2MsmError [owise]
2458+
2459+
syntax PrecompiledOp ::= "BLS12_PAIRING_CHECK"
2460+
// ----------------------------------------------
2461+
rule <k> BLS12_PAIRING_CHECK => bls12PairingCheck(DATA, .List, .List) ... </k> <callData> DATA </callData>
2462+
2463+
rule <k> bls12PairingResult(B:Bool) => #end EVMC_SUCCESS ... </k>
2464+
<output> _ => #if B #then Int2Bytes(32, 1, BE:Endianness) #else Int2Bytes(32, 0, BE:Endianness) #fi </output>
2465+
2466+
rule <k> bls12PairingError => #end EVMC_PRECOMPILE_FAILURE ... </k>
2467+
2468+
syntax Bls12PairingResult ::= "bls12PairingError" | bls12PairingResult(Bool)
2469+
| bls12PairingCheck(Bytes, List, List) [symbol(bls12PairingCheck), function, total]
2470+
// ---------------------------------------------------------------------------------------------------------------
2471+
rule bls12PairingCheck(B:Bytes, L1:List, L2:List) => bls12PairingResult(BLS12PairingCheck(L1, L2))
2472+
requires lengthBytes(B) ==Int 0
2473+
andBool validBls12G1PairingPoints(L1)
2474+
andBool validBls12G2PairingPoints(L2)
2475+
andBool size(L1) ==Int size(L2)
2476+
andBool size(L1) >Int 0
2477+
2478+
rule bls12PairingCheck(B:Bytes, L1:List, L2:List)
2479+
=> bls12PairingCheck
2480+
( substrBytes(B, 384, lengthBytes(B))
2481+
, L1 ListItem(
2482+
( Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
2483+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
2484+
)
2485+
)
2486+
, L2 ListItem(
2487+
( Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned)
2488+
x Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned)
2489+
, Bytes2Int(substrBytes(B, 256, 320), BE, Unsigned)
2490+
x Bytes2Int(substrBytes(B, 320, 384), BE, Unsigned)
2491+
)
2492+
)
2493+
)
2494+
requires lengthBytes(B) >=Int 384
2495+
2496+
rule bls12PairingCheck(_:Bytes, _:List, _:List) => bls12PairingError [owise]
2497+
2498+
syntax Bool ::= validBls12G1PairingPoints(List) [function, total]
2499+
| validBls12G1PairingPoint(G1Point) [function, total]
2500+
// --------------------------------------------------------------------
2501+
rule validBls12G1PairingPoints(.List) => true
2502+
rule validBls12G1PairingPoints(ListItem(P:G1Point) L:List) => validBls12G1PairingPoints(L)
2503+
requires validBls12G1PairingPoint(P)
2504+
rule validBls12G1PairingPoints(_) => false [owise]
2505+
2506+
rule validBls12G1PairingPoint((X, Y) #as P:G1Point)
2507+
=> isValidBLS12Coordinate(X)
2508+
andBool isValidBLS12Coordinate(Y)
2509+
andBool BLS12G1InSubgroup(P)
2510+
2511+
syntax Bool ::= validBls12G2PairingPoints(List) [function, total]
2512+
| validBls12G2PairingPoint(G2Point) [function, total]
2513+
// --------------------------------------------------------------------
2514+
rule validBls12G2PairingPoints(.List) => true
2515+
rule validBls12G2PairingPoints(ListItem(P:G2Point) L:List) => validBls12G2PairingPoints(L)
2516+
requires validBls12G2PairingPoint(P)
2517+
rule validBls12G2PairingPoints(_) => false [owise]
2518+
2519+
rule validBls12G2PairingPoint((X0 x X1, Y0 x Y1) #as P:G2Point)
2520+
=> isValidBLS12Coordinate(X0)
2521+
andBool isValidBLS12Coordinate(X1)
2522+
andBool isValidBLS12Coordinate(Y0)
2523+
andBool isValidBLS12Coordinate(Y1)
2524+
andBool BLS12G2InSubgroup(P)
2525+
2526+
syntax PrecompiledOp ::= "BLS12_MAP_FP_TO_G1"
2527+
// ---------------------------------------------
2528+
rule <k> BLS12_MAP_FP_TO_G1 => #end EVMC_SUCCESS ... </k>
2529+
<callData> DATA </callData>
2530+
<output> _ => #bls12point(BLS12MapFpToG1(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)))
2531+
</output>
2532+
requires lengthBytes( DATA ) ==Int 64
2533+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned))
2534+
2535+
rule <k> BLS12_MAP_FP_TO_G1 => #end EVMC_PRECOMPILE_FAILURE ... </k>
2536+
<callData> DATA </callData>
2537+
requires lengthBytes( DATA ) =/=Int 64
2538+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned))
2539+
2540+
2541+
syntax PrecompiledOp ::= "BLS12_MAP_FP2_TO_G2"
2542+
// ----------------------------------------------
2543+
rule <k> BLS12_MAP_FP2_TO_G2 => #end EVMC_SUCCESS ... </k>
2544+
<callData> DATA </callData>
2545+
<output>
2546+
_ => #bls12point(BLS12MapFp2ToG2
2547+
( Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned)
2548+
, Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned)
2549+
))
2550+
</output>
2551+
requires lengthBytes( DATA ) ==Int 128
2552+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned))
2553+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned))
2554+
2555+
rule <k> BLS12_MAP_FP2_TO_G2 => #end EVMC_PRECOMPILE_FAILURE ... </k>
2556+
<callData> DATA </callData>
2557+
requires lengthBytes( DATA ) =/=Int 128
2558+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 0, 64), BE, Unsigned))
2559+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(DATA, 64, 128), BE, Unsigned))
2560+
```
22322561

22332562
Ethereum Gas Calculation
22342563
========================
@@ -2582,6 +2911,15 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
25822911
rule <k> #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(DATA, 0, 4) ) ... </k> <callData> DATA </callData>
25832912
rule <k> #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... </k>
25842913
2914+
rule <k> #gasExec(SCHED, BLS12_G1ADD) => Gbls12g1add < SCHED > ... </k>
2915+
rule <k> #gasExec(SCHED, BLS12_G1MSM) => #let N = lengthBytes(DATA) /Int 160 #in N *Int Gbls12g1mul < SCHED > *Int Cbls12g1MsmDiscount(SCHED, N) /Int 1000 ... </k> <callData> DATA </callData>
2916+
rule <k> #gasExec(SCHED, BLS12_G2ADD) => Gbls12g2add < SCHED > ... </k>
2917+
rule <k> #gasExec(SCHED, BLS12_G2MSM) => #let N = lengthBytes(DATA) /Int 288 #in N *Int Gbls12g2mul < SCHED > *Int Cbls12g2MsmDiscount(SCHED, N) /Int 1000 ... </k> <callData> DATA </callData>
2918+
2919+
rule <k> #gasExec(SCHED, BLS12_PAIRING_CHECK) => #let N = lengthBytes(DATA) /Int 384 #in N *Int Gbls12PairingCheckMul < SCHED > +Int Gbls12PairingCheckAdd < SCHED > ... </k> <callData> DATA </callData>
2920+
rule <k> #gasExec(SCHED, BLS12_MAP_FP_TO_G1) => Gbls12mapfptog1 < SCHED > ... </k>
2921+
rule <k> #gasExec(SCHED, BLS12_MAP_FP2_TO_G2) => Gbls12mapfp2tog2 < SCHED > ... </k>
2922+
25852923
syntax InternalOp ::= "#allocateCallGas"
25862924
// ----------------------------------------
25872925
rule <k> GCALL:Gas ~> #allocateCallGas => .K ... </k>

0 commit comments

Comments
 (0)