Skip to content

Commit ea99e16

Browse files
virgil-serbanutavirgil-serbanuta
committed
Precompiled contracts for EIP2357/BLS12
1 parent 4ebba29 commit ea99e16

File tree

4 files changed

+760
-20
lines changed

4 files changed

+760
-20
lines changed

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

Lines changed: 327 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -1026,6 +1026,13 @@ Precompiled Contracts
10261026
rule #precompiled(8) => ECPAIRING
10271027
rule #precompiled(9) => BLAKE2F
10281028
rule #precompiled(10) => KZGPOINTEVAL
1029+
rule #precompiled(11) => BLS12G1ADD
1030+
rule #precompiled(12) => BLS12G1MSM
1031+
rule #precompiled(13) => BLS12G2ADD
1032+
rule #precompiled(14) => BLS12G2MSM
1033+
rule #precompiled(15) => BLS12PAIRING_CHECK
1034+
rule #precompiled(16) => BLS12MAPFPTOG1
1035+
rule #precompiled(17) => BLS12MAPFP2TOG2
10291036
10301037
syntax Int ::= #precompiledAccountsUB ( Schedule ) [symbol(#precompiledAccountsUB), function, total]
10311038
// ----------------------------------------------------------------------------------------------------
@@ -1042,7 +1049,7 @@ Precompiled Contracts
10421049
rule #precompiledAccountsUB(MERGE) => #precompiledAccountsUB(LONDON)
10431050
rule #precompiledAccountsUB(SHANGHAI) => #precompiledAccountsUB(MERGE)
10441051
rule #precompiledAccountsUB(CANCUN) => 10
1045-
rule #precompiledAccountsUB(PRAGUE) => #precompiledAccountsUB(CANCUN)
1052+
rule #precompiledAccountsUB(PRAGUE) => 17
10461053
10471054
10481055
syntax Set ::= #precompiledAccountsSet ( Schedule ) [symbol(#precompiledAccountsSet), function, total]
@@ -1193,9 +1200,320 @@ Precompiled Contracts
11931200
// ---------------------------------------------------------------------
11941201
// VERSIONED_HASH_VERSION_KZG = 0x01
11951202
rule #kzg2vh ( C ) => Sha256raw(C)[0 <- 1]
1196-
```
11971203
11981204
1205+
syntax Bytes ::= #bls12point ( G1Point ) [symbol(#bls12point1), function]
1206+
// -------------------------------------------------------------------------
1207+
rule #bls12point((X, Y)) => #padToWidth(64, #asByteStack(X)) +Bytes #padToWidth(64, #asByteStack(Y))
1208+
1209+
syntax Bytes ::= #bls12point ( G2Point ) [symbol(#bls12point2), function]
1210+
// -------------------------------------------------------------------------
1211+
rule #bls12point((X0 x X1, Y0 x Y1))
1212+
=> #padToWidth(64, #asByteStack(X0)) +Bytes #padToWidth(64, #asByteStack(X1))
1213+
+Bytes #padToWidth(64, #asByteStack(Y0)) +Bytes #padToWidth(64, #asByteStack(Y1))
1214+
1215+
syntax Bool ::= isValidBLS12Coordinate ( Int ) [symbol(isValidBLS12Coordinate), function, total]
1216+
// -----------------------------------------------------------------------------------------------
1217+
rule isValidBLS12Coordinate(X) => isValidBLS12Fp(X)
1218+
1219+
syntax Bool ::= isValidBLS12Fp ( Int ) [symbol(isValidBLS12Fp), function, total]
1220+
// -------------------------------------------------------------------------------
1221+
rule isValidBLS12Fp(X) => X >=Int 0 andBool X <Int (1 <<Int 384) andBool X <Int BLS12_FIELD_MODULUS
1222+
1223+
syntax Bool ::= isValidBLS12Scalar ( Int ) [symbol(isValidBLS12Scalar), function, total]
1224+
// ---------------------------------------------------------------------------------------
1225+
rule isValidBLS12Scalar(X) => X >=Int 0 andBool X <Int (1 <<Int 256)
1226+
1227+
syntax PrecompiledOp ::= "BLS12G1ADD"
1228+
// -------------------------------------
1229+
rule <k> BLS12G1ADD => #end EVMC_SUCCESS ... </k>
1230+
<output>
1231+
_ => #bls12point(BLS12G1Add
1232+
( ( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1233+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1234+
)
1235+
, ( Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1236+
, Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1237+
)
1238+
))
1239+
</output>
1240+
requires lengthBytes( CallData() ) ==Int 256
1241+
andBool bls12ValidForAdd
1242+
( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1243+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1244+
, Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1245+
, Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1246+
)
1247+
1248+
rule <k> BLS12G1ADD => #end EVMC_PRECOMPILE_FAILURE ... </k>
1249+
requires lengthBytes( CallData() ) =/=Int 256
1250+
orBool notBool bls12ValidForAdd
1251+
( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1252+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1253+
, Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1254+
, Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1255+
)
1256+
1257+
syntax Bool ::= bls12ValidForAdd(Int, Int, Int, Int) [function, total]
1258+
// -----------------------------------------------------------------------
1259+
rule bls12ValidForAdd(X0, Y0, X1, Y1)
1260+
=> true
1261+
andBool isValidBLS12Coordinate(X0)
1262+
andBool isValidBLS12Coordinate(Y0)
1263+
andBool isValidBLS12Coordinate(X1)
1264+
andBool isValidBLS12Coordinate(Y1)
1265+
andBool BLS12G1OnCurve((X0, Y0))
1266+
andBool BLS12G1OnCurve((X1, Y1))
1267+
1268+
syntax PrecompiledOp ::= "BLS12G1MSM"
1269+
// -------------------------------------
1270+
// TODO: implement `bls12G1Msm` as a hook, using Pippenger's algorithm (blst_p1s_mult_pippenger)
1271+
// However, note that the implementation of `g1_lincomb_fast` has the
1272+
// following comment:
1273+
//
1274+
// * @remark While this function is significantly faster than g1_lincomb_naive(), we refrain from
1275+
// * using it in security-critical places (like verification) because the blst Pippenger code has not
1276+
// * been audited. In those critical places, we prefer using g1_lincomb_naive() which is much simpler.
1277+
//
1278+
// https://github.com/ethereum/c-kzg-4844/blob/cc33b779cd3a227f51b35ce519a83cf91d81ccea/src/common/lincomb.c#L54-L56
1279+
1280+
rule BLS12G1MSM => bls12G1Msm(CallData())
1281+
1282+
rule <k> g1MsmResult(P:G1Point) => #end EVMC_SUCCESS ... </k>
1283+
<output>
1284+
_ => #bls12point(P)
1285+
</output>
1286+
rule <k> g1MsmError => #end EVMC_PRECOMPILE_FAILURE ... </k>
1287+
1288+
syntax G1MsmResult ::= "g1MsmError" | g1MsmResult(G1Point)
1289+
// ----------------------------------------------------------
1290+
syntax G1MsmResult ::= bls12G1Msm(Bytes) [symbol(bls12G1Msm), function, total]
1291+
syntax G1MsmResult ::= #bls12G1Msm(G1MsmResult, G1MsmResult) [function, total]
1292+
syntax G1MsmResult ::= #bls12G1MsmMulCheck(Int, Int, Int) [function, total]
1293+
rule bls12G1Msm(B:Bytes) => g1MsmError requires lengthBytes(B) <Int 160
1294+
rule bls12G1Msm(B:Bytes)
1295+
=> #bls12G1MsmMulCheck
1296+
( Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
1297+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
1298+
, Bytes2Int(substrBytes(B, 128, 160), BE, Unsigned)
1299+
)
1300+
requires lengthBytes( B ) ==Int 160
1301+
rule bls12G1Msm(B:Bytes)
1302+
=> #bls12G1Msm(bls12G1Msm(substrBytes(B, 0, 160)), bls12G1Msm(substrBytes(B, 160, lengthBytes(B))))
1303+
requires lengthBytes(B) >Int 160
1304+
rule bls12G1Msm(_) => g1MsmError [owise]
1305+
1306+
rule #bls12G1MsmMulCheck(X:Int, Y:Int, N:Int)
1307+
=> g1MsmResult(BLS12G1Mul( ( X , Y ), N ))
1308+
requires isValidBLS12Coordinate(X) andBool isValidBLS12Coordinate(Y)
1309+
andBool isValidBLS12Scalar(N)
1310+
andBool BLS12G1InSubgroup((X, Y))
1311+
rule #bls12G1MsmMulCheck(_, _, _) => g1MsmError [owise]
1312+
1313+
rule #bls12G1Msm(g1MsmResult(P1:G1Point), g1MsmResult(P2:G1Point))
1314+
=> g1MsmResult(BLS12G1Add(P1, P2))
1315+
rule #bls12G1Msm(_, _) => g1MsmError [owise]
1316+
1317+
syntax PrecompiledOp ::= "BLS12G2ADD"
1318+
// -------------------------------------
1319+
rule <k> BLS12G2ADD => #end EVMC_SUCCESS ... </k>
1320+
<output>
1321+
_ => #bls12point(BLS12G2Add
1322+
( ( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1323+
x Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1324+
, Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1325+
x Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1326+
)
1327+
, ( Bytes2Int(substrBytes(CallData(), 256, 320), BE, Unsigned)
1328+
x Bytes2Int(substrBytes(CallData(), 320, 384), BE, Unsigned)
1329+
, Bytes2Int(substrBytes(CallData(), 384, 448), BE, Unsigned)
1330+
x Bytes2Int(substrBytes(CallData(), 448, 512), BE, Unsigned)
1331+
)
1332+
))
1333+
</output>
1334+
requires lengthBytes( CallData() ) ==Int 512
1335+
andBool bls12ValidForAdd2
1336+
( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1337+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1338+
, Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1339+
, Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1340+
, Bytes2Int(substrBytes(CallData(), 256, 320), BE, Unsigned)
1341+
, Bytes2Int(substrBytes(CallData(), 320, 384), BE, Unsigned)
1342+
, Bytes2Int(substrBytes(CallData(), 384, 448), BE, Unsigned)
1343+
, Bytes2Int(substrBytes(CallData(), 448, 512), BE, Unsigned)
1344+
)
1345+
1346+
rule <k> BLS12G2ADD => #end EVMC_PRECOMPILE_FAILURE ... </k>
1347+
requires lengthBytes( CallData() ) =/=Int 512
1348+
orBool notBool bls12ValidForAdd2
1349+
( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1350+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1351+
, Bytes2Int(substrBytes(CallData(), 128, 192), BE, Unsigned)
1352+
, Bytes2Int(substrBytes(CallData(), 192, 256), BE, Unsigned)
1353+
, Bytes2Int(substrBytes(CallData(), 256, 320), BE, Unsigned)
1354+
, Bytes2Int(substrBytes(CallData(), 320, 384), BE, Unsigned)
1355+
, Bytes2Int(substrBytes(CallData(), 384, 448), BE, Unsigned)
1356+
, Bytes2Int(substrBytes(CallData(), 448, 512), BE, Unsigned)
1357+
)
1358+
1359+
syntax Bool ::= bls12ValidForAdd2(Int, Int, Int, Int, Int, Int, Int, Int) [function, total]
1360+
// --------------------------------------------------------------------------------------------
1361+
rule bls12ValidForAdd2(PX0, PX1, PY0, PY1, QX0, QX1, QY0, QY1)
1362+
=> true
1363+
andBool isValidBLS12Coordinate(PX0)
1364+
andBool isValidBLS12Coordinate(PX1)
1365+
andBool isValidBLS12Coordinate(PY0)
1366+
andBool isValidBLS12Coordinate(PY1)
1367+
andBool isValidBLS12Coordinate(QX0)
1368+
andBool isValidBLS12Coordinate(QX1)
1369+
andBool isValidBLS12Coordinate(QY0)
1370+
andBool isValidBLS12Coordinate(QY1)
1371+
andBool BLS12G2OnCurve((PX0 x PX1, PY0 x PY1))
1372+
andBool BLS12G2OnCurve((QX0 x QX1, QY0 x QY1))
1373+
1374+
syntax PrecompiledOp ::= "BLS12G2MSM"
1375+
// -------------------------------------
1376+
// TODO: implement this as a hook, using pippenger's algorithm (blst_p1s_mult_pippenger)
1377+
// (see the similar comment for `BLS12G1MSM` for details)
1378+
rule BLS12G2MSM => bls12G2Msm(CallData())
1379+
1380+
rule <k> g2MsmResult(P:G2Point) => #end EVMC_SUCCESS ... </k>
1381+
<output>
1382+
_ => #bls12point(P)
1383+
</output>
1384+
rule <k> g2MsmError => #end EVMC_PRECOMPILE_FAILURE ... </k>
1385+
1386+
syntax G2MsmResult ::= "g2MsmError" | g2MsmResult(G2Point)
1387+
// ----------------------------------------------------------
1388+
syntax G2MsmResult ::= bls12G2Msm(Bytes) [symbol(bls12G2Msm), function, total]
1389+
syntax G2MsmResult ::= #bls12G2Msm(G2MsmResult, G2MsmResult) [function, total]
1390+
syntax G2MsmResult ::= #bls12G2MsmMulCheck(Int, Int, Int, Int, Int) [function, total]
1391+
rule bls12G2Msm(B:Bytes) => g2MsmError requires lengthBytes(B) <Int 288
1392+
rule bls12G2Msm(B:Bytes)
1393+
=> #bls12G2MsmMulCheck
1394+
( Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
1395+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
1396+
, Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned)
1397+
, Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned)
1398+
, Bytes2Int(substrBytes(B, 256, 288), BE, Unsigned)
1399+
)
1400+
requires lengthBytes( B ) ==Int 288
1401+
rule bls12G2Msm(B:Bytes)
1402+
=> #bls12G2Msm(bls12G2Msm(substrBytes(B, 0, 288)), bls12G2Msm(substrBytes(B, 288, lengthBytes(B))))
1403+
requires lengthBytes(B) >Int 288
1404+
rule bls12G2Msm(_) => g2MsmError [owise]
1405+
1406+
rule #bls12G2MsmMulCheck(X0:Int, X1:Int, Y0:Int, Y1:Int, N:Int)
1407+
=> g2MsmResult(BLS12G2Mul( ( X0 x X1, Y0 x Y1 ), N ))
1408+
requires isValidBLS12Coordinate(X0) andBool isValidBLS12Coordinate(X1)
1409+
andBool isValidBLS12Coordinate(Y0) andBool isValidBLS12Coordinate(Y1)
1410+
andBool isValidBLS12Scalar(N)
1411+
andBool BLS12G2InSubgroup(( X0 x X1, Y0 x Y1 ))
1412+
rule #bls12G2MsmMulCheck(_, _, _, _, _) => g2MsmError [owise]
1413+
1414+
rule #bls12G2Msm(g2MsmResult(P1:G2Point), g2MsmResult(P2:G2Point))
1415+
=> g2MsmResult(BLS12G2Add(P1, P2))
1416+
rule #bls12G2Msm(_, _) => g2MsmError [owise]
1417+
1418+
syntax PrecompiledOp ::= "BLS12PAIRING_CHECK"
1419+
// ---------------------------------------------
1420+
rule BLS12PAIRING_CHECK => bls12PairingCheck(CallData(), .List, .List)
1421+
1422+
rule <k> bls12PairingResult(B:Bool) => #end EVMC_SUCCESS ... </k>
1423+
<output>
1424+
_ => #if B #then Int2Bytes(32, 1, BE:Endianness) #else Int2Bytes(32, 0, BE:Endianness) #fi
1425+
</output>
1426+
rule <k> bls12PairingError => #end EVMC_PRECOMPILE_FAILURE ... </k>
1427+
1428+
syntax Bls12PairingResult ::= "bls12PairingError" | bls12PairingResult(Bool)
1429+
// ----------------------------------------------------------------------------
1430+
syntax Bls12PairingResult ::= bls12PairingCheck(Bytes, List, List) [symbol(bls12PairingCheck), function, total]
1431+
rule bls12PairingCheck(B:Bytes, L1:List, L2:List) => bls12PairingResult(BLS12PairingCheck(L1, L2))
1432+
requires lengthBytes(B) ==Int 0
1433+
andBool validBls12G1PairingPoints(L1)
1434+
andBool validBls12G2PairingPoints(L2)
1435+
andBool size(L1) ==Int size(L2)
1436+
andBool size(L1) >Int 0
1437+
rule bls12PairingCheck(B:Bytes, L1:List, L2:List)
1438+
=> bls12PairingCheck
1439+
( substrBytes(B, 384, lengthBytes(B))
1440+
, L1 ListItem(
1441+
( Bytes2Int(substrBytes(B, 0, 64), BE, Unsigned)
1442+
, Bytes2Int(substrBytes(B, 64, 128), BE, Unsigned)
1443+
)
1444+
)
1445+
, L2 ListItem(
1446+
( Bytes2Int(substrBytes(B, 128, 192), BE, Unsigned)
1447+
x Bytes2Int(substrBytes(B, 192, 256), BE, Unsigned)
1448+
, Bytes2Int(substrBytes(B, 256, 320), BE, Unsigned)
1449+
x Bytes2Int(substrBytes(B, 320, 384), BE, Unsigned)
1450+
)
1451+
)
1452+
)
1453+
requires lengthBytes(B) >=Int 384
1454+
rule bls12PairingCheck(_:Bytes, _:List, _:List) => bls12PairingError [owise]
1455+
1456+
syntax Bool ::= validBls12G1PairingPoints(List) [function, total]
1457+
syntax Bool ::= validBls12G1PairingPoint(G1Point) [function, total]
1458+
rule validBls12G1PairingPoints(.List) => true
1459+
rule validBls12G1PairingPoints(ListItem(P:G1Point) L:List) => validBls12G1PairingPoints(L)
1460+
requires validBls12G1PairingPoint(P)
1461+
rule validBls12G1PairingPoints(_) => false [owise]
1462+
1463+
rule validBls12G1PairingPoint((X, Y) #as P:G1Point)
1464+
=> isValidBLS12Coordinate(X)
1465+
andBool isValidBLS12Coordinate(Y)
1466+
andBool BLS12G1InSubgroup(P)
1467+
1468+
syntax Bool ::= validBls12G2PairingPoints(List) [function, total]
1469+
syntax Bool ::= validBls12G2PairingPoint(G2Point) [function, total]
1470+
rule validBls12G2PairingPoints(.List) => true
1471+
rule validBls12G2PairingPoints(ListItem(P:G2Point) L:List) => validBls12G2PairingPoints(L)
1472+
requires validBls12G2PairingPoint(P)
1473+
rule validBls12G2PairingPoints(_) => false [owise]
1474+
1475+
rule validBls12G2PairingPoint((X0 x X1, Y0 x Y1) #as P:G2Point)
1476+
=> isValidBLS12Coordinate(X0)
1477+
andBool isValidBLS12Coordinate(X1)
1478+
andBool isValidBLS12Coordinate(Y0)
1479+
andBool isValidBLS12Coordinate(Y1)
1480+
andBool BLS12G2InSubgroup(P)
1481+
1482+
syntax PrecompiledOp ::= "BLS12MAPFPTOG1"
1483+
// -----------------------------------------
1484+
rule <k> BLS12MAPFPTOG1 => #end EVMC_SUCCESS ... </k>
1485+
<output>
1486+
_ => #bls12point(BLS12MapFpToG1(Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned), (0, 0)))
1487+
</output>
1488+
requires lengthBytes( CallData() ) ==Int 64
1489+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned))
1490+
1491+
rule <k> BLS12MAPFPTOG1 => #end EVMC_PRECOMPILE_FAILURE ... </k>
1492+
requires lengthBytes( CallData() ) =/=Int 64
1493+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned))
1494+
1495+
1496+
syntax PrecompiledOp ::= "BLS12MAPFP2TOG2"
1497+
// ------------------------------------------
1498+
rule <k> BLS12MAPFP2TOG2 => #end EVMC_SUCCESS ... </k>
1499+
<output>
1500+
_ => #bls12point(BLS12MapFp2ToG2
1501+
( Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned)
1502+
, Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned)
1503+
, ( 0 x 0 , 0 x 0 )
1504+
))
1505+
</output>
1506+
requires lengthBytes( CallData() ) ==Int 128
1507+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned))
1508+
andBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned))
1509+
1510+
rule <k> BLS12MAPFP2TOG2 => #end EVMC_PRECOMPILE_FAILURE ... </k>
1511+
requires lengthBytes( CallData() ) =/=Int 128
1512+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 0, 64), BE, Unsigned))
1513+
orBool notBool isValidBLS12Fp(Bytes2Int(substrBytes(CallData(), 64, 128), BE, Unsigned))
1514+
1515+
```
1516+
11991517
Ethereum Gas Calculation
12001518
========================
12011519

@@ -1527,7 +1845,13 @@ The intrinsic gas calculation mirrors the style of the YellowPaper (appendix H).
15271845
rule <k> #gasExec(SCHED, ECPAIRING) => Gecpairconst < SCHED > +Int (lengthBytes(CallData()) /Int 192) *Int Gecpaircoeff < SCHED > ... </k>
15281846
rule <k> #gasExec(SCHED, BLAKE2F) => Gfround < SCHED > *Int #asWord(#range(CallData(), 0, 4) ) ... </k>
15291847
rule <k> #gasExec(SCHED, KZGPOINTEVAL) => Gpointeval < SCHED > ... </k>
1530-
1848+
rule <k> #gasExec(SCHED, BLS12G1ADD) => Gbls12g1add < SCHED > ... </k>
1849+
rule <k> #gasExec(SCHED, BLS12G1MSM) => #let N = lengthBytes(CallData()) /Int 160 #in N *Int Gbls12g1mul < SCHED > *Int Cbls12g1MsmDiscount(SCHED, N) /Int 1000 ... </k>
1850+
rule <k> #gasExec(SCHED, BLS12G2ADD) => Gbls12g2add < SCHED > ... </k>
1851+
rule <k> #gasExec(SCHED, BLS12G2MSM) => #let N = lengthBytes(CallData()) /Int 288 #in N *Int Gbls12g2mul < SCHED > *Int Cbls12g2MsmDiscount(SCHED, N) /Int 1000 ... </k>
1852+
rule <k> #gasExec(SCHED, BLS12PAIRING_CHECK) => #let N = lengthBytes(CallData()) /Int 384 #in N *Int Gbls12PairingCheckMul < SCHED > +Int Gbls12PairingCheckAdd < SCHED > ... </k>
1853+
rule <k> #gasExec(SCHED, BLS12MAPFPTOG1) => Gbls12mapfptog1 < SCHED > ... </k>
1854+
rule <k> #gasExec(SCHED, BLS12MAPFP2TOG2) => Gbls12mapfp2tog2 < SCHED > ... </k>
15311855
syntax InternalOp ::= "#allocateCallGas"
15321856
// ----------------------------------------
15331857
rule <k> GCALL:Gas ~> #allocateCallGas => .K ... </k>

0 commit comments

Comments
 (0)