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

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Algebra.EllipticCurve.BLS12_381 where

import           Control.Monad
import           Data.Bits
import           Data.Foldable
import           Data.Word
import           Prelude                                    hiding (Num (..), (/), (^))

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.EllipticCurve.Pairing
import           ZkFold.Base.Algebra.Polynomials.Univariate
import           ZkFold.Base.Data.ByteString
import qualified ZkFold.Symbolic.Data.Conditional           as Symbolic
import qualified ZkFold.Symbolic.Data.Eq                    as Symbolic

-------------------------------- 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 Fq6
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 Fq6 -> Poly Fq6
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Item (Vector Fq6)
Fq6
forall {e :: Symbol}. Ext3 Fq2 e
e, Item (Vector Fq6)
Fq6
forall a. AdditiveMonoid a => a
zero, Item (Vector Fq6)
Fq6
forall a. MultiplicativeMonoid a => a
one]
type Fq12 = Ext2 Fq6 IP3

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

instance Field field => WeierstrassCurve "BLS12-381-G1" field where
  weierstrassB :: field
weierstrassB = Natural -> field
forall a b. FromConstant a b => a -> b
fromConstant (Natural
4 :: Natural)

type BLS12_381_G1_Point = Weierstrass "BLS12-381-G1" (Point Fq)

type BLS12_381_G1_CompressedPoint =
  Weierstrass "BLS12-381-G1" (CompressedPoint Fq)

instance Compressible BLS12_381_G1_Point where
    type Compressed BLS12_381_G1_Point = BLS12_381_G1_CompressedPoint
    pointCompressed :: BaseFieldOf BLS12_381_G1_Point
-> BooleanOf (BaseFieldOf BLS12_381_G1_Point)
-> Compressed BLS12_381_G1_Point
pointCompressed BaseFieldOf BLS12_381_G1_Point
x BooleanOf (BaseFieldOf BLS12_381_G1_Point)
yBit = CompressedPoint Fq
-> Weierstrass "BLS12-381-G1" (CompressedPoint Fq)
forall {k} (curve :: k) point. point -> Weierstrass curve point
Weierstrass (Fq -> BooleanOf Fq -> BooleanOf Fq -> CompressedPoint Fq
forall field.
field
-> BooleanOf field -> BooleanOf field -> CompressedPoint field
CompressedPoint Fq
BaseFieldOf BLS12_381_G1_Point
x BooleanOf Fq
BooleanOf (BaseFieldOf BLS12_381_G1_Point)
yBit Bool
BooleanOf Fq
False)
    compress :: BLS12_381_G1_Point -> Compressed BLS12_381_G1_Point
compress (Weierstrass (Point Fq
x Fq
y BooleanOf Fq
isInf)) =
      if Bool
BooleanOf Fq
isInf then Weierstrass "BLS12-381-G1" (CompressedPoint Fq)
Compressed BLS12_381_G1_Point
forall point. HasPointInf point => point
pointInf
      else forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G1_Point Fq
BaseFieldOf BLS12_381_G1_Point
x (Fq
y Fq -> Fq -> Bool
forall a. Ord a => a -> a -> Bool
> Fq -> Fq
forall a. AdditiveGroup a => a -> a
negate Fq
y)
    decompress :: Compressed BLS12_381_G1_Point -> BLS12_381_G1_Point
decompress (Weierstrass (CompressedPoint Fq
x BooleanOf Fq
bigY BooleanOf Fq
isInf)) =
      if Bool
BooleanOf Fq
isInf then BLS12_381_G1_Point
forall point. HasPointInf point => point
pointInf else
        let b :: Fq
b = forall (curve :: Symbol) field.
WeierstrassCurve curve field =>
field
weierstrassB @"BLS12-381-G1"
            q :: Natural
q = forall a. Finite a => Natural
order @Fq
            sqrt_ :: a -> a
sqrt_ a
z = a
z a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ ((Natural
q Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Prelude.div` Natural
2)
            y' :: Fq
y' = Fq -> Fq
forall {a}. Exponent a Natural => a -> a
sqrt_ (Fq
x Fq -> Fq -> Fq
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq
x Fq -> Fq -> Fq
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq
x Fq -> Fq -> Fq
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq
b)
            y'' :: Fq
y'' = Fq -> Fq
forall a. AdditiveGroup a => a -> a
negate Fq
y'
            y :: Fq
y = if Bool
BooleanOf Fq
bigY then Fq -> Fq -> Fq
forall a. Ord a => a -> a -> a
max Fq
y' Fq
y'' else Fq -> Fq -> Fq
forall a. Ord a => a -> a -> a
min Fq
y' Fq
y''
        in  Fq -> Fq -> BLS12_381_G1_Point
forall field point. Planar field point => field -> field -> point
pointXY Fq
x Fq
y

instance CyclicGroup BLS12_381_G1_Point where
  type ScalarFieldOf BLS12_381_G1_Point = Fr
  pointGen :: BLS12_381_G1_Point
pointGen = Fq -> Fq -> BLS12_381_G1_Point
forall field point. Planar field point => field -> field -> point
pointXY
    Fq
0x17f1d3a73197d7942695638c4fa9ac0fc3688c4f9774b905a14e3a3f171bac586c55e83ff97a1aeffb3af00adb22c6bb
    Fq
0x8b3f481e3aaa0f1a09e30ed741d8ae4fcf5e095d5d00af600db18cb2c04b3edd03cc744a2888ae40caa232946c5e7e1

instance Scale Fr BLS12_381_G1_Point where
  scale :: Fr -> BLS12_381_G1_Point -> BLS12_381_G1_Point
scale Fr
n BLS12_381_G1_Point
x = Natural -> BLS12_381_G1_Point -> BLS12_381_G1_Point
forall b a. Scale b a => b -> a -> a
scale (Fr -> Const Fr
forall a. ToConstant a => a -> Const a
toConstant Fr
n) BLS12_381_G1_Point
x

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

instance WeierstrassCurve "BLS12-381-G2" Fq2 where
  weierstrassB :: Fq2
weierstrassB = Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
4 Fq
4

type BLS12_381_G2_Point = Weierstrass "BLS12-381-G2" (Point Fq2)

type BLS12_381_G2_CompressedPoint =
  Weierstrass "BLS12-381-G2" (CompressedPoint Fq2)

instance CyclicGroup BLS12_381_G2_Point where
  type ScalarFieldOf BLS12_381_G2_Point = Fr
  pointGen :: BLS12_381_G2_Point
pointGen = Fq2 -> Fq2 -> BLS12_381_G2_Point
forall field point. Planar field point => field -> field -> point
pointXY
    (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)

instance Scale Fr BLS12_381_G2_Point where
  scale :: Fr -> BLS12_381_G2_Point -> BLS12_381_G2_Point
scale Fr
n BLS12_381_G2_Point
x = Natural -> BLS12_381_G2_Point -> BLS12_381_G2_Point
forall b a. Scale b a => b -> a -> a
scale (Fr -> Const Fr
forall a. ToConstant a => a -> Const a
toConstant Fr
n) BLS12_381_G2_Point
x

instance Compressible BLS12_381_G2_Point where
    type Compressed BLS12_381_G2_Point = BLS12_381_G2_CompressedPoint
    pointCompressed :: BaseFieldOf BLS12_381_G2_Point
-> BooleanOf (BaseFieldOf BLS12_381_G2_Point)
-> Compressed BLS12_381_G2_Point
pointCompressed BaseFieldOf BLS12_381_G2_Point
x BooleanOf (BaseFieldOf BLS12_381_G2_Point)
yBit = CompressedPoint Fq2
-> Weierstrass "BLS12-381-G2" (CompressedPoint Fq2)
forall {k} (curve :: k) point. point -> Weierstrass curve point
Weierstrass (Fq2 -> BooleanOf Fq2 -> BooleanOf Fq2 -> CompressedPoint Fq2
forall field.
field
-> BooleanOf field -> BooleanOf field -> CompressedPoint field
CompressedPoint Fq2
BaseFieldOf BLS12_381_G2_Point
x BooleanOf Fq2
BooleanOf (BaseFieldOf BLS12_381_G2_Point)
yBit Bool
BooleanOf Fq2
False)
    compress :: BLS12_381_G2_Point -> Compressed BLS12_381_G2_Point
compress (Weierstrass (Point Fq2
x Fq2
y BooleanOf Fq2
isInf)) =
      if Bool
BooleanOf Fq2
isInf then Weierstrass "BLS12-381-G2" (CompressedPoint Fq2)
Compressed BLS12_381_G2_Point
forall point. HasPointInf point => point
pointInf
      else forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G2_Point Fq2
BaseFieldOf BLS12_381_G2_Point
x (Fq2
y Fq2 -> Fq2 -> Bool
forall a. Ord a => a -> a -> Bool
> Fq2 -> Fq2
forall a. AdditiveGroup a => a -> a
negate Fq2
y)
    decompress :: Compressed BLS12_381_G2_Point -> BLS12_381_G2_Point
decompress (Weierstrass (CompressedPoint Fq2
x BooleanOf Fq2
bigY BooleanOf Fq2
isInf)) =
      if Bool
BooleanOf Fq2
isInf then BLS12_381_G2_Point
forall point. HasPointInf point => point
pointInf else
        let b :: Fq2
b = forall (curve :: Symbol) field.
WeierstrassCurve curve field =>
field
weierstrassB @"BLS12-381-G2"
            q :: Natural
q = forall a. Finite a => Natural
order @Fq2
            sqrt_ :: a -> a
sqrt_ a
z = a
z a -> Natural -> a
forall a b. Exponent a b => a -> b -> a
^ ((Natural
q Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Prelude.div` Natural
2)
            y' :: Fq2
y' = Fq2 -> Fq2
forall {a}. Exponent a Natural => a -> a
sqrt_ (Fq2
x Fq2 -> Fq2 -> Fq2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq2
x Fq2 -> Fq2 -> Fq2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Fq2
x Fq2 -> Fq2 -> Fq2
forall a. AdditiveSemigroup a => a -> a -> a
+ Fq2
b)
            y'' :: Fq2
y'' = Fq2 -> Fq2
forall a. AdditiveGroup a => a -> a
negate Fq2
y'
            y :: Fq2
y = if Bool
BooleanOf Fq2
bigY then Fq2 -> Fq2 -> Fq2
forall a. Ord a => a -> a -> a
max Fq2
y' Fq2
y'' else Fq2 -> Fq2 -> Fq2
forall a. Ord a => a -> a -> a
min Fq2
y' Fq2
y''
        in  Fq2 -> Fq2 -> BLS12_381_G2_Point
forall field point. Planar field point => field -> field -> point
pointXY Fq2
x Fq2
y

------------------------------------ Encoding ------------------------------------

-- infinite list of divMod 256's, little endian order
leBytesOf :: Natural -> [(Natural, Word8)]
leBytesOf :: Natural -> [(Natural, Word8)]
leBytesOf Natural
n =
    let
        (Natural
n', Natural
r) = Natural
n Natural -> Natural -> (Natural, Natural)
forall a. Integral a => a -> a -> (a, a)
`Prelude.divMod` Natural
256
    in
        (Natural
n', Natural -> Word8
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
r) (Natural, Word8) -> [(Natural, Word8)] -> [(Natural, Word8)]
forall a. a -> [a] -> [a]
: Natural -> [(Natural, Word8)]
leBytesOf Natural
n'

-- finite list of bytes, big endian order
bytesOf :: (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf :: forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
n
    = [Word8] -> [Word8]
forall a. [a] -> [a]
reverse
    ([Word8] -> [Word8]) -> (a -> [Word8]) -> a -> [Word8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int -> [Word8] -> [Word8]
forall a. Int -> [a] -> [a]
take Int
n
    ([Word8] -> [Word8]) -> (a -> [Word8]) -> a -> [Word8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((Natural, Word8) -> Word8) -> [(Natural, Word8)] -> [Word8]
forall a b. (a -> b) -> [a] -> [b]
map (Natural, Word8) -> Word8
forall a b. (a, b) -> b
snd
    ([(Natural, Word8)] -> [Word8])
-> (a -> [(Natural, Word8)]) -> a -> [Word8]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Natural -> [(Natural, Word8)]
leBytesOf
    (Natural -> [(Natural, Word8)])
-> (a -> Natural) -> a -> [(Natural, Word8)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Natural
a -> Const a
forall a. ToConstant a => a -> Const a
toConstant

-- big endian decoding
ofBytes :: FromConstant Natural a => [Word8] -> a
ofBytes :: forall a. FromConstant Natural a => [Word8] -> a
ofBytes
  = forall a b. FromConstant a b => a -> b
fromConstant @Natural
  (Natural -> a) -> ([Word8] -> Natural) -> [Word8] -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Natural -> Word8 -> Natural) -> Natural -> [Word8] -> Natural
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' (\Natural
n Word8
w8 -> Natural
n Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
256 Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Word8 -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral Word8
w8) Natural
0

instance Binary BLS12_381_G1_Point where
    put :: BLS12_381_G1_Point -> Put
put (Weierstrass (Point Fq
x Fq
y BooleanOf Fq
isInf)) =
        if Bool
BooleanOf Fq
isInf then (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 (Word8 -> Word8
bitReverse8 (Int -> Word8
forall a. Bits a => Int -> a
bit Int
1) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
95 Word8
0)
                 else (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 (Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x [Word8] -> [Word8] -> [Word8]
forall a. Semigroup a => a -> a -> a
<> Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
y)
    get :: Get BLS12_381_G1_Point
get = do
        Word8
byte <- Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Get Word8 -> Get Word8
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word8
getWord8
        let compressed :: Bool
compressed = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
0
            infinite :: Bool
infinite = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
1
        if Bool
infinite then do
            Int -> Get ()
skip (if Bool
compressed then Int
47 else Int
95)
            BLS12_381_G1_Point -> Get BLS12_381_G1_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BLS12_381_G1_Point
forall point. HasPointInf point => point
pointInf
        else do
            let byteXhead :: Word8
byteXhead = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit Word8
byte Int
0) Int
1) Int
2
            [Word8]
bytesXtail <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
47 Get Word8
getWord8
            let x :: Fq
x = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes (Word8
byteXheadWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
bytesXtail)
                bigY :: Bool
bigY = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
2
            if Bool
compressed then BLS12_381_G1_Point -> Get BLS12_381_G1_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BLS12_381_G1_Point -> Get BLS12_381_G1_Point)
-> BLS12_381_G1_Point -> Get BLS12_381_G1_Point
forall a b. (a -> b) -> a -> b
$
              forall point. Compressible point => Compressed point -> point
decompress @BLS12_381_G1_Point
                (forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G1_Point Fq
BaseFieldOf BLS12_381_G1_Point
x Bool
BooleanOf (BaseFieldOf BLS12_381_G1_Point)
bigY)
            else do
                [Word8]
bytesY <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                let y :: Fq
y = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY
                BLS12_381_G1_Point -> Get BLS12_381_G1_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Fq -> Fq -> BLS12_381_G1_Point
forall field point. Planar field point => field -> field -> point
pointXY Fq
x Fq
y)

instance Binary BLS12_381_G1_CompressedPoint where
    put :: Weierstrass "BLS12-381-G1" (CompressedPoint Fq) -> Put
put (Weierstrass (CompressedPoint Fq
x BooleanOf Fq
bigY BooleanOf Fq
isInf)) =
        if Bool
BooleanOf Fq
isInf then (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 (Word8 -> Word8
bitReverse8 (Int -> Word8
forall a. Bits a => Int -> a
bit Int
0 Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. Int -> Word8
forall a. Bits a => Int -> a
bit Int
1) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
47 Word8
0) else
        let
            flags :: Word8
flags = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ if Bool
BooleanOf Fq
bigY then Int -> Word8
forall a. Bits a => Int -> a
bit Int
0 Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. Int -> Word8
forall a. Bits a => Int -> a
bit Int
2 else Int -> Word8
forall a. Bits a => Int -> a
bit Int
0
            bytes :: [Word8]
bytes = Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x
        in (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 ((Word8
flags Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. [Word8] -> Word8
forall a. HasCallStack => [a] -> a
head [Word8]
bytes) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: [Word8] -> [Word8]
forall a. HasCallStack => [a] -> [a]
tail [Word8]
bytes)
    get :: Get (Weierstrass "BLS12-381-G1" (CompressedPoint Fq))
get = do
        Word8
byte <- Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Get Word8 -> Get Word8
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word8
getWord8
        let compressed :: Bool
compressed = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
0
            infinite :: Bool
infinite = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
1
        if Bool
infinite then do
            Int -> Get ()
skip (if Bool
compressed then Int
47 else Int
95)
            Weierstrass "BLS12-381-G1" (CompressedPoint Fq)
-> Get (Weierstrass "BLS12-381-G1" (CompressedPoint Fq))
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Weierstrass "BLS12-381-G1" (CompressedPoint Fq)
forall point. HasPointInf point => point
pointInf
        else do
            let byteXhead :: Word8
byteXhead = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit Word8
byte Int
0) Int
1) Int
2
            [Word8]
bytesXtail <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
47 Get Word8
getWord8
            let x :: Fq
x = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes (Word8
byteXheadWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
bytesXtail)
                bigY :: Bool
bigY = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
2
            forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G1_Point Fq
BaseFieldOf BLS12_381_G1_Point
x (Bool -> Weierstrass "BLS12-381-G1" (CompressedPoint Fq))
-> Get Bool
-> Get (Weierstrass "BLS12-381-G1" (CompressedPoint Fq))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              if Bool
compressed then Bool -> Get Bool
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
bigY else do
                [Word8]
bytesY <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                let Fq
y :: Fq = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY
                    bigY' :: Bool
bigY' = Fq
y Fq -> Fq -> Bool
forall a. Ord a => a -> a -> Bool
> Fq -> Fq
forall a. AdditiveGroup a => a -> a
negate Fq
y
                Bool -> Get Bool
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
bigY'

instance Binary BLS12_381_G2_Point where
    put :: BLS12_381_G2_Point -> Put
put (Weierstrass (Point (Ext2 Fq
x0 Fq
x1) (Ext2 Fq
y0 Fq
y1) BooleanOf Fq2
isInf)) =
        if Bool
BooleanOf Fq2
isInf then (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 (Word8 -> Word8
bitReverse8 (Int -> Word8
forall a. Bits a => Int -> a
bit Int
1) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
191  Word8
0) else
        let
            bytes :: [Word8]
bytes = Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x1
              [Word8] -> [Word8] -> [Word8]
forall a. Semigroup a => a -> a -> a
<> Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x0
              [Word8] -> [Word8] -> [Word8]
forall a. Semigroup a => a -> a -> a
<> Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
y1
              [Word8] -> [Word8] -> [Word8]
forall a. Semigroup a => a -> a -> a
<> Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
y0
        in
            (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 [Word8]
bytes
    get :: Get BLS12_381_G2_Point
get = do
        Word8
byte <- Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Get Word8 -> Get Word8
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word8
getWord8
        let compressed :: Bool
compressed = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
0
            infinite :: Bool
infinite = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
1
        if Bool
infinite then do
            Int -> Get ()
skip (if Bool
compressed then Int
95 else Int
191)
            BLS12_381_G2_Point -> Get BLS12_381_G2_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return BLS12_381_G2_Point
forall point. HasPointInf point => point
pointInf
        else do
            let byteX1head :: Word8
byteX1head = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit Word8
byte Int
0) Int
1) Int
2
            [Word8]
bytesX1tail <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
47 Get Word8
getWord8
            [Word8]
bytesX0 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
            let x1 :: Fq
x1 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes (Word8
byteX1headWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
bytesX1tail)
                x0 :: Fq
x0 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesX0
                bigY :: Bool
bigY = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
2
            if Bool
compressed then BLS12_381_G2_Point -> Get BLS12_381_G2_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BLS12_381_G2_Point -> Get BLS12_381_G2_Point)
-> BLS12_381_G2_Point -> Get BLS12_381_G2_Point
forall a b. (a -> b) -> a -> b
$
              forall point. Compressible point => Compressed point -> point
decompress @BLS12_381_G2_Point
                (forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G2_Point (Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
x0 Fq
x1) Bool
BooleanOf (BaseFieldOf BLS12_381_G2_Point)
bigY)
            else do
                [Word8]
bytesY1 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                [Word8]
bytesY0 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                let y0 :: Fq
y0 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY0
                    y1 :: Fq
y1 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY1
                BLS12_381_G2_Point -> Get BLS12_381_G2_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Fq2 -> Fq2 -> BLS12_381_G2_Point
forall field point. Planar field point => field -> field -> point
pointXY (Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
x0 Fq
x1) (Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
y0 Fq
y1))

instance Binary BLS12_381_G2_CompressedPoint where
    put :: Weierstrass "BLS12-381-G2" (CompressedPoint Fq2) -> Put
put (Weierstrass (CompressedPoint (Ext2 Fq
x0 Fq
x1) BooleanOf Fq2
bigY BooleanOf Fq2
isInf)) =
        if Bool
BooleanOf Fq2
isInf then (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 (Word8 -> Word8
bitReverse8 (Int -> Word8
forall a. Bits a => Int -> a
bit Int
0 Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. Int -> Word8
forall a. Bits a => Int -> a
bit Int
1) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: Int -> Word8 -> [Word8]
forall a. Int -> a -> [a]
replicate Int
95 Word8
0) else
        let
            flags :: Word8
flags = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ if Bool
BooleanOf Fq2
bigY then Int -> Word8
forall a. Bits a => Int -> a
bit Int
0 Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. Int -> Word8
forall a. Bits a => Int -> a
bit Int
2 else Int -> Word8
forall a. Bits a => Int -> a
bit Int
0
            bytes :: [Word8]
bytes = Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x1 [Word8] -> [Word8] -> [Word8]
forall a. Semigroup a => a -> a -> a
<> Int -> Fq -> [Word8]
forall a. (ToConstant a, Const a ~ Natural) => Int -> a -> [Word8]
bytesOf Int
48 Fq
x0
        in
            (Word8 -> Put) -> [Word8] -> Put
forall m a. Monoid m => (a -> m) -> [a] -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap Word8 -> Put
putWord8 ((Word8
flags Word8 -> Word8 -> Word8
forall a. Bits a => a -> a -> a
.|. [Word8] -> Word8
forall a. HasCallStack => [a] -> a
head [Word8]
bytes) Word8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
: [Word8] -> [Word8]
forall a. HasCallStack => [a] -> [a]
tail [Word8]
bytes)
    get :: Get (Weierstrass "BLS12-381-G2" (CompressedPoint Fq2))
get = do
        Word8
byte <- Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Get Word8 -> Get Word8
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get Word8
getWord8
        let compressed :: Bool
compressed = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
0
            infinite :: Bool
infinite = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
1
        if Bool
infinite then do
            Int -> Get ()
skip (if Bool
compressed then Int
95 else Int
191)
            Weierstrass "BLS12-381-G2" (CompressedPoint Fq2)
-> Get (Weierstrass "BLS12-381-G2" (CompressedPoint Fq2))
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Weierstrass "BLS12-381-G2" (CompressedPoint Fq2)
forall point. HasPointInf point => point
pointInf
        else do
            let byteX1head :: Word8
byteX1head = Word8 -> Word8
bitReverse8 (Word8 -> Word8) -> Word8 -> Word8
forall a b. (a -> b) -> a -> b
$ Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit (Word8 -> Int -> Word8
forall a. Bits a => a -> Int -> a
clearBit Word8
byte Int
0) Int
1) Int
2
            [Word8]
bytesX1tail <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
47 Get Word8
getWord8
            [Word8]
bytesX0 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
            let x1 :: Fq
x1 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes (Word8
byteX1headWord8 -> [Word8] -> [Word8]
forall a. a -> [a] -> [a]
:[Word8]
bytesX1tail)
                x0 :: Fq
x0 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesX0
                x :: Fq2
x = Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
x0 Fq
x1
                bigY :: Bool
bigY = Word8 -> Int -> Bool
forall a. Bits a => a -> Int -> Bool
testBit Word8
byte Int
2
            forall point.
Compressible point =>
BaseFieldOf point
-> BooleanOf (BaseFieldOf point) -> Compressed point
pointCompressed @BLS12_381_G2_Point Fq2
BaseFieldOf BLS12_381_G2_Point
x (Bool -> Weierstrass "BLS12-381-G2" (CompressedPoint Fq2))
-> Get Bool
-> Get (Weierstrass "BLS12-381-G2" (CompressedPoint Fq2))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
              if Bool
compressed then Bool -> Get Bool
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
bigY else do
                [Word8]
bytesY1 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                [Word8]
bytesY0 <- Int -> Get Word8 -> Get [Word8]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
48 Get Word8
getWord8
                let y0 :: Fq
y0 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY0
                    y1 :: Fq
y1 = [Word8] -> Fq
forall a. FromConstant Natural a => [Word8] -> a
ofBytes [Word8]
bytesY1
                    Fq2
y :: Fq2 = Fq -> Fq -> Fq2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fq
y0 Fq
y1
                    bigY' :: Bool
bigY' = Fq2
y Fq2 -> Fq2 -> Bool
forall a. Ord a => a -> a -> Bool
> Fq2 -> Fq2
forall a. AdditiveGroup a => a -> a
negate Fq2
y
                Bool -> Get Bool
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return Bool
bigY'

--------------------------------------- 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
        , Int -> BLS12_381_GT -> ShowS
[BLS12_381_GT] -> ShowS
BLS12_381_GT -> String
(Int -> BLS12_381_GT -> ShowS)
-> (BLS12_381_GT -> String)
-> ([BLS12_381_GT] -> ShowS)
-> Show BLS12_381_GT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BLS12_381_GT -> ShowS
showsPrec :: Int -> BLS12_381_GT -> ShowS
$cshow :: BLS12_381_GT -> String
show :: BLS12_381_GT -> String
$cshowList :: [BLS12_381_GT] -> ShowS
showList :: [BLS12_381_GT] -> ShowS
Show
        , Scale BLS12_381_GT BLS12_381_GT
FromConstant BLS12_381_GT BLS12_381_GT
(FromConstant BLS12_381_GT BLS12_381_GT,
 Scale BLS12_381_GT BLS12_381_GT) =>
(BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT)
-> MultiplicativeSemigroup BLS12_381_GT
BLS12_381_GT -> BLS12_381_GT -> BLS12_381_GT
forall a.
(FromConstant a a, Scale a 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
        , Symbolic.Conditional Prelude.Bool
        , Conditional (BooleanOf BLS12_381_GT) BLS12_381_GT
Conditional (BooleanOf BLS12_381_GT) BLS12_381_GT =>
(BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT)
-> (BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT)
-> Eq BLS12_381_GT
BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT
forall a.
Conditional (BooleanOf a) a =>
(a -> a -> BooleanOf a) -> (a -> a -> BooleanOf a) -> Eq a
$c== :: BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT
== :: BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT
$c/= :: BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT
/= :: BLS12_381_GT -> BLS12_381_GT -> BooleanOf BLS12_381_GT
Symbolic.Eq
        )

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_Point BLS12_381_G2_Point BLS12_381_GT where
    pairing :: BLS12_381_G1_Point -> BLS12_381_G2_Point -> BLS12_381_GT
pairing BLS12_381_G1_Point
a BLS12_381_G2_Point
b
      = Fq12 -> BLS12_381_GT
BLS12_381_GT
      (Fq12 -> BLS12_381_GT) -> Fq12 -> BLS12_381_GT
forall a b. (a -> b) -> a -> b
$ forall scalarField baseField g (i :: Symbol) (j :: Symbol).
(Finite scalarField, Finite baseField, g ~ Untwisted baseField i j,
 Exponent g Natural) =>
g -> g
finalExponentiation @Fr
      (Fq12 -> Fq12) -> Fq12 -> Fq12
forall a b. (a -> b) -> a -> b
$ [Int8] -> BLS12_381_G1_Point -> BLS12_381_G2_Point -> Fq12
forall {k} (c :: k) (d :: Symbol) fldC fldD (i :: Symbol)
       (j :: Symbol) g.
(WeierstrassCurve d fldD, Eq fldD, FiniteField fldC,
 Scale fldC fldD, Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
[Int8]
-> Weierstrass c (Point fldC) -> Weierstrass d (Point fldD) -> g
millerAlgorithmBLS12 [Int8]
param BLS12_381_G1_Point
a BLS12_381_G2_Point
b
      where
        param :: [Int8]
param = [-Item [Int8]
1
          ,-Item [Int8]
1, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0
          , Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0
          , Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0
          , Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0
          ]