{-# LANGUAGE DerivingVia      #-}
{-# LANGUAGE OverloadedLists  #-}
{-# LANGUAGE TypeApplications #-}

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Algebra.EllipticCurve.BLS12_381 where

import           Data.Bits                                  (shiftR)
import           Data.List                                  (unfoldr)
import           Numeric.Natural                            (Natural)
import           Prelude                                    hiding (Num (..), (/), (^))
import qualified Prelude                                    as Haskell

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.Polynomials.Univariate

-------------------------------- Introducing Fields ----------------------------------

type BLS12_381_Scalar = 0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001
instance Prime BLS12_381_Scalar

type BLS12_381_Base = 0x1a0111ea397fe69a4b1ba7b6434bacd764774b84f38512bf6730d2a0f6b0f6241eabfffeb153ffffb9feffffffffaaab
instance Prime BLS12_381_Base

type Fr = Zp BLS12_381_Scalar
type Fq = Zp BLS12_381_Base

type IP1 = "IP1"
instance IrreduciblePoly Fq IP1 where
    irreduciblePoly :: Poly Fq
irreduciblePoly = Vector Fq -> Poly Fq
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Item (Vector Fq)
Fq
1, Item (Vector Fq)
Fq
0, Item (Vector Fq)
Fq
1]
type Fq2 = Ext2 Fq IP1

type IP2 = "IP2"
instance IrreduciblePoly Fq2 IP2 where
    irreduciblePoly :: Poly Fq2
irreduciblePoly =
        let e :: Ext2 Fq e
e = Fq -> Fq -> Ext2 Fq e
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2
                Fq
0xd0088f51cbff34d258dd3db21a5d66bb23ba5c279c2895fb39869507b587b120f55ffff58a9ffffdcff7fffffffd556
                Fq
0xd0088f51cbff34d258dd3db21a5d66bb23ba5c279c2895fb39869507b587b120f55ffff58a9ffffdcff7fffffffd555
        in Vector Fq2 -> Poly Fq2
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Fq2 -> Fq2
forall a. AdditiveGroup a => a -> a
negate Fq2
forall {e :: Symbol}. Ext2 Fq e
e, Item (Vector Fq2)
Fq2
forall a. AdditiveMonoid a => a
zero, Item (Vector Fq2)
Fq2
forall a. AdditiveMonoid a => a
zero, Item (Vector Fq2)
Fq2
forall a. MultiplicativeMonoid a => a
one]
type Fq6 = Ext3 Fq2 IP2

type IP3 = "IP3"
instance IrreduciblePoly Fq6 IP3 where
    irreduciblePoly :: Poly (Ext3 Fq2 IP2)
irreduciblePoly =
        let e :: Ext3 Fq2 e
e = Fq2 -> Fq2 -> Fq2 -> Ext3 Fq2 e
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 Fq2
forall a. AdditiveMonoid a => a
zero (Fq2 -> Fq2
forall a. AdditiveGroup a => a -> a
negate Fq2
forall a. MultiplicativeMonoid a => a
one) Fq2
forall a. AdditiveMonoid a => a
zero
        in Vector (Ext3 Fq2 IP2) -> Poly (Ext3 Fq2 IP2)
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Item (Vector (Ext3 Fq2 IP2))
Ext3 Fq2 IP2
forall {e :: Symbol}. Ext3 Fq2 e
e, Item (Vector (Ext3 Fq2 IP2))
Ext3 Fq2 IP2
forall a. AdditiveMonoid a => a
zero, Item (Vector (Ext3 Fq2 IP2))
Ext3 Fq2 IP2
forall a. MultiplicativeMonoid a => a
one]
type Fq12 = Ext2 Fq6 IP3

------------------------------------ BLS12-381 G1 ------------------------------------

data BLS12_381_G1


instance EllipticCurve BLS12_381_G1 where
    type ScalarField BLS12_381_G1 = Fr

    type BaseField BLS12_381_G1 = Fq

    inf :: Point BLS12_381_G1
inf = Point BLS12_381_G1
forall {k} (curve :: k). Point curve
Inf

    gen :: Point BLS12_381_G1
gen = BaseField BLS12_381_G1
-> BaseField BLS12_381_G1 -> Point BLS12_381_G1
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
        BaseField BLS12_381_G1
Fq
0x17f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
        BaseField BLS12_381_G1
Fq
0x8b3f481e3aaa0f1a09e30ed741d8ae4fcf5e095d5d00af600db18cb2c04b3edd03cc744a2888ae40caa232946c5e7e1

    add :: Point BLS12_381_G1 -> Point BLS12_381_G1 -> Point BLS12_381_G1
add = Point BLS12_381_G1 -> Point BLS12_381_G1 -> Point BLS12_381_G1
forall {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints

    mul :: ScalarField BLS12_381_G1
-> Point BLS12_381_G1 -> Point BLS12_381_G1
mul = ScalarField BLS12_381_G1
-> Point BLS12_381_G1 -> Point BLS12_381_G1
forall {k} (curve :: k).
(EllipticCurve curve, BinaryExpansion (ScalarField curve),
 Eq (ScalarField curve)) =>
ScalarField curve -> Point curve -> Point curve
pointMul

------------------------------------ BLS12-381 G2 ------------------------------------

data BLS12_381_G2

instance EllipticCurve BLS12_381_G2 where

    type ScalarField BLS12_381_G2 = Fr

    type BaseField BLS12_381_G2 = Fq2

    inf :: Point BLS12_381_G2
inf = Point BLS12_381_G2
forall {k} (curve :: k). Point curve
Inf

    gen :: Point BLS12_381_G2
gen = BaseField BLS12_381_G2
-> BaseField BLS12_381_G2 -> Point BLS12_381_G2
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
        (Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2
            Fq
0x24aa2b2f08f0a91260805272dc51051c6e47ad4fa403b02b4510b647ae3d1770bac0326a805bbefd48056c8c121bdb8
            Fq
0x13e02b6052719f607dacd3a088274f65596bd0d09920b61ab5da61bbdc7f5049334cf11213945d57e5ac7d055d042b7e)
        (Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2
            Fq
0xce5d527727d6e118cc9cdc6da2e351aadfd9baa8cbdd3a76d429a695160d12c923ac9cc3baca289e193548608b82801
            Fq
0x606c4a02ea734cc32acd2b02bc28b99cb3e287e85a763af267492ab572e99ab3f370d275cec1da1aaa9075ff05f79be)

    add :: Point BLS12_381_G2 -> Point BLS12_381_G2 -> Point BLS12_381_G2
add = Point BLS12_381_G2 -> Point BLS12_381_G2 -> Point BLS12_381_G2
forall {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints

    mul :: ScalarField BLS12_381_G2
-> Point BLS12_381_G2 -> Point BLS12_381_G2
mul = ScalarField BLS12_381_G2
-> Point BLS12_381_G2 -> Point BLS12_381_G2
forall {k} (curve :: k).
(EllipticCurve curve, BinaryExpansion (ScalarField curve),
 Eq (ScalarField curve)) =>
ScalarField curve -> Point curve -> Point curve
pointMul

--------------------------------------- Pairing ---------------------------------------

-- | An image of a pairing is a cyclic multiplicative subgroup of @'Fq12'@
-- of order @'BLS12_381_Scalar'@.
newtype BLS12_381_GT = BLS12_381_GT Fq12
    deriving newtype (BLS12_381_GT -> BLS12_381_GT -> Bool
(BLS12_381_GT -> BLS12_381_GT -> Bool)
-> (BLS12_381_GT -> BLS12_381_GT -> Bool) -> Eq BLS12_381_GT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BLS12_381_GT -> BLS12_381_GT -> Bool
== :: BLS12_381_GT -> BLS12_381_GT -> Bool
$c/= :: BLS12_381_GT -> BLS12_381_GT -> Bool
/= :: BLS12_381_GT -> BLS12_381_GT -> Bool
Eq, BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT
(BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT)
-> MultiplicativeSemigroup BLS12_381_GT
forall a. (a -> a -> a) -> MultiplicativeSemigroup a
$c* :: BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT
* :: BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT
MultiplicativeSemigroup, Exponent BLS12_381_GT Natural
MultiplicativeSemigroup BLS12_381_GT
BLS12_381_GT
(MultiplicativeSemigroup BLS12_381_GT,
 Exponent BLS12_381_GT Natural) =>
BLS12_381_GT -> MultiplicativeMonoid BLS12_381_GT
forall a.
(MultiplicativeSemigroup a, Exponent a Natural) =>
a -> MultiplicativeMonoid a
$cone :: BLS12_381_GT
one :: BLS12_381_GT
MultiplicativeMonoid)

instance Exponent BLS12_381_GT Natural where
    BLS12_381_GT Fq12
a ^ :: BLS12_381_GT -> Natural -> BLS12_381_GT
^ Natural
p = Fq12 -> BLS12_381_GT
BLS12_381_GT (Fq12
a Fq12 -> Natural -> Fq12
forall a b. Exponent a b => a -> b -> a
^ Natural
p)

instance Exponent BLS12_381_GT Integer where
    BLS12_381_GT Fq12
a ^ :: BLS12_381_GT -> Integer -> BLS12_381_GT
^ Integer
p = Fq12 -> BLS12_381_GT
BLS12_381_GT (Fq12
a Fq12 -> Integer -> Fq12
forall a b. Exponent a b => a -> b -> a
^ Integer
p)

deriving via (NonZero Fq12) instance MultiplicativeGroup BLS12_381_GT

instance Finite BLS12_381_GT where
    type Order BLS12_381_GT = BLS12_381_Scalar

instance Pairing BLS12_381_G1 BLS12_381_G2 BLS12_381_GT where
    pairing :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> BLS12_381_GT
pairing Point BLS12_381_G1
a Point BLS12_381_G2
b = Fq12 -> BLS12_381_GT
BLS12_381_GT (Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
pairingBLS Point BLS12_381_G1
a Point BLS12_381_G2
b)

-- Adapted from https://github.com/nccgroup/pairing-bls12381/blob/master/Crypto/Pairing_bls12381.hs

-- Untwist point on E2 for pairing calculation
untwist :: Point BLS12_381_G2 -> (Fq12, Fq12)
untwist :: Point BLS12_381_G2 -> (Fq12, Fq12)
untwist (Point BaseField BLS12_381_G2
x1 BaseField BLS12_381_G2
y1) = (Fq12
wideX, Fq12
wideY)
  where
    root :: Ext3 Fq2 e
root = Fq2 -> Fq2 -> Fq2 -> Ext3 Fq2 e
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 Fq2
forall a. AdditiveMonoid a => a
zero Fq2
forall a. MultiplicativeMonoid a => a
one Fq2
forall a. AdditiveMonoid a => a
zero
    wideX :: Fq12
wideX = Ext3 Fq2 IP2 -> Ext3 Fq2 IP2 -> Fq12
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Ext3 Fq2 IP2
forall a. AdditiveMonoid a => a
zero (Fq2 -> Fq2 -> Fq2 -> Ext3 Fq2 IP2
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 Fq2
forall a. AdditiveMonoid a => a
zero Fq2
forall a. AdditiveMonoid a => a
zero BaseField BLS12_381_G2
Fq2
x1) Fq12 -> Fq12 -> Fq12
forall a. Field a => a -> a -> a
// Ext3 Fq2 IP2 -> Ext3 Fq2 IP2 -> Fq12
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Ext3 Fq2 IP2
forall a. AdditiveMonoid a => a
zero Ext3 Fq2 IP2
forall {e :: Symbol}. Ext3 Fq2 e
root
    wideY :: Fq12
wideY = Ext3 Fq2 IP2 -> Ext3 Fq2 IP2 -> Fq12
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Ext3 Fq2 IP2
forall a. AdditiveMonoid a => a
zero (Fq2 -> Fq2 -> Fq2 -> Ext3 Fq2 IP2
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 Fq2
forall a. AdditiveMonoid a => a
zero Fq2
forall a. AdditiveMonoid a => a
zero BaseField BLS12_381_G2
Fq2
y1) Fq12 -> Fq12 -> Fq12
forall a. Field a => a -> a -> a
// Ext3 Fq2 IP2 -> Ext3 Fq2 IP2 -> Fq12
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Ext3 Fq2 IP2
forall {e :: Symbol}. Ext3 Fq2 e
root Ext3 Fq2 IP2
forall a. AdditiveMonoid a => a
zero
untwist Point BLS12_381_G2
Inf = [Char] -> (Fq12, Fq12)
forall a. HasCallStack => [Char] -> a
error [Char]
"untwist: point at infinity"

-- Used in miller loop for computing line functions l_r,r and v_2r
doubleEval :: Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
doubleEval :: Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
doubleEval Point BLS12_381_G2
r (Point BaseField BLS12_381_G1
px BaseField BLS12_381_G1
py) = Fq -> Fq12
forall a b. FromConstant a b => a -> b
fromConstant BaseField BLS12_381_G1
Fq
py Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- (Fq -> Fq12
forall a b. FromConstant a b => a -> b
fromConstant BaseField BLS12_381_G1
Fq
px Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
slope) Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
v
  where
    (Fq12
rx, Fq12
ry) = Point BLS12_381_G2 -> (Fq12, Fq12)
untwist Point BLS12_381_G2
r
    slope :: Fq12
slope = (Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
rx) Fq12 -> Fq12 -> Fq12
forall a. Field a => a -> a -> a
// (Fq12
ry Fq12 -> Fq12 -> Fq12
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq12
ry)
    v :: Fq12
v = Fq12
ry Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
slope Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
rx
doubleEval Point BLS12_381_G2
_ Point BLS12_381_G1
Inf = [Char] -> Fq12
forall a. HasCallStack => [Char] -> a
error [Char]
"doubleEval: point at infinity"

-- Used in miller loop for computer line function l_r,p and v_r+p
addEval :: Point BLS12_381_G2 -> Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
addEval :: Point BLS12_381_G2
-> Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
addEval Point BLS12_381_G2
r Point BLS12_381_G2
q p :: Point BLS12_381_G1
p@(Point BaseField BLS12_381_G1
px BaseField BLS12_381_G1
_) = if (Fq12
rx Fq12 -> Fq12 -> Bool
forall a. Eq a => a -> a -> Bool
== Fq12
qx) Bool -> Bool -> Bool
&& (Fq12
ry Fq12 -> Fq12 -> Fq12
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq12
qy Fq12 -> Fq12 -> Bool
forall a. Eq a => a -> a -> Bool
== Fq12
forall a. AdditiveMonoid a => a
zero)
                then Fq -> Fq12
forall a b. FromConstant a b => a -> b
fromConstant BaseField BLS12_381_G1
Fq
px Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
rx
                else (Fq12, Fq12) -> (Fq12, Fq12) -> Point BLS12_381_G1 -> Fq12
addEval' (Fq12
rx, Fq12
ry) (Fq12
qx, Fq12
qy) Point BLS12_381_G1
p
  where
    (Fq12
rx, Fq12
ry) = Point BLS12_381_G2 -> (Fq12, Fq12)
untwist Point BLS12_381_G2
r
    (Fq12
qx, Fq12
qy) = Point BLS12_381_G2 -> (Fq12, Fq12)
untwist Point BLS12_381_G2
q
addEval Point BLS12_381_G2
_ Point BLS12_381_G2
_ Point BLS12_381_G1
Inf = [Char] -> Fq12
forall a. HasCallStack => [Char] -> a
error [Char]
"addEval: point at infinity"

-- Helper function for addEval
addEval' :: (Fq12, Fq12) -> (Fq12, Fq12) -> Point BLS12_381_G1 -> Fq12
addEval' :: (Fq12, Fq12) -> (Fq12, Fq12) -> Point BLS12_381_G1 -> Fq12
addEval' (Fq12
rx, Fq12
ry) (Fq12
qx, Fq12
qy) (Point BaseField BLS12_381_G1
px BaseField BLS12_381_G1
py) = Fq -> Fq12
forall a b. FromConstant a b => a -> b
fromConstant BaseField BLS12_381_G1
Fq
py Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- (Fq -> Fq12
forall a b. FromConstant a b => a -> b
fromConstant BaseField BLS12_381_G1
Fq
px Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
slope) Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
v
  where
    slope :: Fq12
slope = (Fq12
qy Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
ry) Fq12 -> Fq12 -> Fq12
forall a. Field a => a -> a -> a
// (Fq12
qx Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
rx)
    v :: Fq12
v = ((Fq12
qy Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
rx) Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- (Fq12
ry Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
qx)) Fq12 -> Fq12 -> Fq12
forall a. Field a => a -> a -> a
// (Fq12
rx Fq12 -> Fq12 -> Fq12
forall a. AdditiveGroup a => a -> a -> a
- Fq12
qx)
addEval' (Fq12, Fq12)
_ (Fq12, Fq12)
_ Point BLS12_381_G1
Inf = [Char] -> Fq12
forall a. HasCallStack => [Char] -> a
error [Char]
"addEval': point at infinity"

-- Classic Miller loop for Ate pairing
miller :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
miller :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
miller Point BLS12_381_G1
p Point BLS12_381_G2
q = Point BLS12_381_G1
-> Point BLS12_381_G2
-> Point BLS12_381_G2
-> [Bool]
-> Fq12
-> Fq12
miller' Point BLS12_381_G1
p Point BLS12_381_G2
q Point BLS12_381_G2
q [Bool]
iterations Fq12
forall a. MultiplicativeMonoid a => a
one
  where
    iterations :: [Bool]
iterations = [Bool] -> [Bool]
forall a. HasCallStack => [a] -> [a]
tail ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$ [Bool] -> [Bool]
forall a. [a] -> [a]
reverse ([Bool] -> [Bool]) -> [Bool] -> [Bool]
forall a b. (a -> b) -> a -> b
$  -- list of true/false per bits of operand
      (Integer -> Maybe (Bool, Integer)) -> Integer -> [Bool]
forall b a. (b -> Maybe (a, b)) -> b -> [a]
unfoldr (\Integer
b -> if Integer
b Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== (Integer
0 :: Integer) then Maybe (Bool, Integer)
forall a. Maybe a
Nothing
                     else (Bool, Integer) -> Maybe (Bool, Integer)
forall a. a -> Maybe a
Just(Integer -> Bool
forall a. Integral a => a -> Bool
odd Integer
b, Integer -> Int -> Integer
forall a. Bits a => a -> Int -> a
shiftR Integer
b Int
1)) Integer
0xd201000000010000

-- Double and add loop helper for Miller (iterative)
miller' :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> Point BLS12_381_G2 -> [Bool] -> Fq12 -> Fq12
miller' :: Point BLS12_381_G1
-> Point BLS12_381_G2
-> Point BLS12_381_G2
-> [Bool]
-> Fq12
-> Fq12
miller' Point BLS12_381_G1
_ Point BLS12_381_G2
_ Point BLS12_381_G2
_ [] Fq12
result = Fq12
result
miller' Point BLS12_381_G1
p Point BLS12_381_G2
q Point BLS12_381_G2
r (Bool
i:[Bool]
iters) Fq12
result =
  if Bool
i then Point BLS12_381_G1
-> Point BLS12_381_G2
-> Point BLS12_381_G2
-> [Bool]
-> Fq12
-> Fq12
miller' Point BLS12_381_G1
p Point BLS12_381_G2
q (Point BLS12_381_G2 -> Point BLS12_381_G2 -> Point BLS12_381_G2
forall {k} (curve :: k).
(Field (BaseField curve), Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
pointAdd Point BLS12_381_G2
doubleR Point BLS12_381_G2
q) [Bool]
iters (Fq12
accum Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Point BLS12_381_G2
-> Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
addEval Point BLS12_381_G2
doubleR Point BLS12_381_G2
q Point BLS12_381_G1
p)
       else Point BLS12_381_G1
-> Point BLS12_381_G2
-> Point BLS12_381_G2
-> [Bool]
-> Fq12
-> Fq12
miller' Point BLS12_381_G1
p Point BLS12_381_G2
q Point BLS12_381_G2
doubleR [Bool]
iters Fq12
accum
  where
    accum :: Fq12
accum = Fq12
result Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq12
result Fq12 -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> a -> a
* Point BLS12_381_G2 -> Point BLS12_381_G1 -> Fq12
doubleEval Point BLS12_381_G2
r Point BLS12_381_G1
p
    doubleR :: Point BLS12_381_G2
doubleR = Point BLS12_381_G2 -> Point BLS12_381_G2
forall {k} (curve :: k).
Field (BaseField curve) =>
Point curve -> Point curve
pointDouble Point BLS12_381_G2
r

-- | Pairing calculation for a valid point in G1 and another valid point in G2.
pairingBLS :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
pairingBLS :: Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
pairingBLS Point BLS12_381_G1
Inf Point BLS12_381_G2
_ = Fq12
forall a. AdditiveMonoid a => a
zero
pairingBLS Point BLS12_381_G1
_ Point BLS12_381_G2
Inf = Fq12
forall a. AdditiveMonoid a => a
zero
pairingBLS Point BLS12_381_G1
p Point BLS12_381_G2
q   = Fq12 -> Natural -> Fq12 -> Fq12
forall a. MultiplicativeSemigroup a => a -> Natural -> a -> a
pow' (Point BLS12_381_G1 -> Point BLS12_381_G2 -> Fq12
miller Point BLS12_381_G1
p Point BLS12_381_G2
q) (((forall a. Finite a => Natural
order @(BaseField BLS12_381_G1))Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^(Natural
12 :: Natural) Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Haskell.div` (forall a. Finite a => Natural
order @(ScalarField BLS12_381_G1))) Fq12
forall a. MultiplicativeMonoid a => a
one

-- Used for the final exponentiation; opportunity for further perf optimization
pow' :: MultiplicativeSemigroup a => a -> Natural -> a -> a
pow' :: forall a. MultiplicativeSemigroup a => a -> Natural -> a -> a
pow' a
a0 Natural
e a
result
  | Natural
e Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
<= Natural
1    = a
a0
  | Natural -> Bool
forall a. Integral a => a -> Bool
even Natural
e    = a
accum2
  | Bool
otherwise = a
accum2 a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
a0
  where
    accum :: a
accum  = a -> Natural -> a -> a
forall a. MultiplicativeSemigroup a => a -> Natural -> a -> a
pow' a
a0 (Natural -> Int -> Natural
forall a. Bits a => a -> Int -> a
shiftR Natural
e Int
1) a
result
    accum2 :: a
accum2 = a
accum a -> a -> a
forall a. MultiplicativeSemigroup a => a -> a -> a
* a
accum