pairing-1.1.0: src/Data/Pairing/Ate.hs
module Data.Pairing.Ate
( module Data.Pairing
-- * Optimal ate pairing of BLS curves
, millerAlgorithmBLS12
, finalExponentiationBLS12
-- * Optimal ate pairing of BN curves
, millerAlgorithmBN
, finalExponentiationBN
) where
import Protolude
import Data.Curve.Weierstrass (Curve(..), Point(..))
import Data.Field.Galois as F
import Data.Pairing
-------------------------------------------------------------------------------
-- Miller algorithm
-------------------------------------------------------------------------------
-- | [Miller algorithm for Barreto-Lynn-Scott degree 12 curves]
-- (https://eprint.iacr.org/2016/130.pdf).
millerAlgorithmBLS12 :: ECPairing e q r u v w
=> [Int8] -> G1 e -> G2 e -> GT e
millerAlgorithmBLS12 (x:xs) p q = snd $
millerLoop p q xs (if x > 0 then q else inv q, mempty)
millerAlgorithmBLS12 _ _ _ = mempty
{-# INLINABLE millerAlgorithmBLS12 #-}
-- | [Miller algorithm for Barreto-Naehrig curves]
-- (https://eprint.iacr.org/2010/354.pdf).
millerAlgorithmBN :: ECPairing e q r u v w
=> Extension u (Prime q) -> [Int8] -> G1 e -> G2 e -> GT e
millerAlgorithmBN xi (x:xs) p q = finalStepBN xi p q $
millerLoop p q xs (if x > 0 then q else inv q, mempty)
millerAlgorithmBN _ _ _ _ = mempty
{-# INLINABLE millerAlgorithmBN #-}
-- Miller loop, line 2 to line 10.
millerLoop :: ECPairing e q r u v w
=> G1 e -> G2 e -> [Int8] -> (G2 e, GT e) -> (G2 e, GT e)
millerLoop p q = millerLoop'
where
millerLoop' [] tf = tf
millerLoop' (x:xs) tf = case doublingStep p tf of
tf2
| x == 0 -> millerLoop' xs tf2
| x == 1 -> millerLoop' xs $ additionStep p q tf2
| otherwise -> millerLoop' xs $ additionStep p (inv q) tf2
{-# INLINABLE millerLoop #-}
-- Doubling step, line 4.
doublingStep :: ECPairing e q r u v w
=> G1 e -> (G2 e, GT e) -> (G2 e, GT e)
doublingStep p (t, f) = (<>) f . (<>) f <$> lineFunction p t t
{-# INLINABLE doublingStep #-}
-- Addition step, line 6 and line 8.
additionStep :: ECPairing e q r u v w
=> G1 e -> G2 e -> (G2 e, GT e) -> (G2 e, GT e)
additionStep p q (t, f) = (<>) f <$> lineFunction p q t
{-# INLINABLE additionStep #-}
-- Final step for BN curves, line 11 to line 13.
finalStepBN :: ECPairing e q r u v w
=> Extension u (Prime q) -> G1 e -> G2 e -> (G2 e, GT e) -> GT e
finalStepBN xi p q (t, f) = case lineFunction p t q1 of
(t', f') -> case lineFunction p t' q2 of
(_, f'') -> f <> f' <> f''
where
q1 = frobTwisted xi q
q2 = inv $ frobTwisted xi q1
{-# INLINABLE finalStepBN #-}
-------------------------------------------------------------------------------
-- Final exponentiation
-------------------------------------------------------------------------------
-- | [Final exponentiation for Barreto-Lynn-Scott degree 12 curves]
-- (https://eprint.iacr.org/2016/130.pdf).
finalExponentiationBLS12 :: ECPairing e q r u v w
=> Integer -> GT e -> GT e
finalExponentiationBLS12 u = (<$>) $ hardPart . easyPart
where
easyPart = p2 . p6
where
p6 = (*) <$> conj <*> recip -- f^(p^6 - 1)
p2 = (*) <$> identity <*> F.frob . F.frob -- f^(p^2 + 1)
hardPart f = p4
where
f2 = f * f -- f^2
y3 = powUnitary (powUnitary f u * conj f2) u * f -- f^(lambda_3)
y2 = powUnitary y3 u -- f^(lambda_2)
y1 = powUnitary y2 u * conj y3 -- f^(lambda_1)
y0 = powUnitary y1 u * f2 * f -- f^(lambda_0)
p4 = y0 * F.frob (y1 * F.frob (y2 * (F.frob y3))) -- f^((p^4 - p^2 + 1) / r)
{-# INLINABLE finalExponentiationBLS12 #-}
-- | [Final exponentiation for Barreto-Naehrig curves]
-- (https://eprint.iacr.org/2010/354.pdf).
finalExponentiationBN :: ECPairing e q r u v w
=> Integer -> GT e -> GT e
finalExponentiationBN u = (<$>) $ hardPart . easyPart
where
easyPart = p2 . p6
where
p6 = (*) <$> conj <*> recip -- f^(p^6 - 1)
p2 = (*) <$> identity <*> F.frob . F.frob -- f^(p^2 + 1)
hardPart f = p4
where
fu = powUnitary f u -- f^u
fu2 = powUnitary fu u -- f^(u^2)
fu3 = powUnitary fu2 u -- f^(u^3)
fpu = F.frob fu2 -- f^(pu^2)
y0 = F.frob (f * F.frob (f * F.frob f)) -- f^(p + p^2 + p^3)
y1 = conj f -- f^(-1)
y2 = F.frob fpu -- f^(p^2u^2)
y3 = conj $ F.frob fu -- f^(-pu)
y4 = conj $ fu * fpu -- f^(-u - pu^2)
y5 = conj fu2 -- f^(-u^2)
y6 = conj $ fu3 * F.frob fu3 -- f^(-u^3 - pu^3)
p4 = p4' * y0 * join (*) (p4' * y1) -- f^((p^4 - p^2 + 1) / r)
where
p4' = join (*) $ p4'' * y2 * join (*) (p4'' * y3 * y5)
p4'' = y4 * y5 * join (*) y6
{-# INLINABLE finalExponentiationBN #-}
-------------------------------------------------------------------------------
-- Auxiliary functions
-------------------------------------------------------------------------------
-- | Line function evaluation @Line(T, Q, P)@.
--
-- Compute the line function between two points @T@ and @Q@ in @G2@,
-- evaluate the line function at a point @P@ in @G1@,
-- and embed the line function evaluation in @GT@.
lineFunction :: ECPairing e q r u v w
=> G1 e -- ^ Point @P@.
-> G2 e -- ^ Point @T@.
-> G2 e -- ^ Point @Q@.
-> (G2 e, GT e) -- ^ Points @T + Q@ and @Line(T, Q, P)@.
lineFunction (A x y) (A x1 y1) (A x2 y2)
| x1 /= x2 = (A x3 y3 , toU' [embed $ -y, [x *^ l , y1 - l * x1]])
| y1 + y2 == 0 = (O , toU' [embed x, embed $ -x1 ])
| otherwise = (A x3' y3', toU' [embed $ -y, [x *^ l', y1 - l' * x1]])
where
l = (y2 - y1) / (x2 - x1)
x3 = l * l - x1 - x2
y3 = l * (x1 - x3) - y1
x12 = x1 * x1
l' = (x12 + x12 + x12) / (y1 + y1)
x3' = l' * l' - x1 - x2
y3' = l' * (x1 - x3') - y1
lineFunction _ _ _ = (O, mempty)
{-# INLINABLE lineFunction #-}
-- | Twisted Frobenius endomorphism @Frob(P)@.
--
-- Compute the Frobenius endomorphism on a point @P@ given a twist @xi@.
frobTwisted :: forall e q r u v w . ECPairing e q r u v w
=> Extension u (Prime q) -- ^ Twist @xi@.
-> G2 e -- ^ Point @P@.
-> G2 e -- ^ Point @Frob(P)@.
frobTwisted xi (A x y) = A (F.frob x * pow xi tx) (F.frob y * pow xi ty)
where
tx = quot (F.char (witness :: Prime q) - 1) 3
ty = shiftR (F.char (witness :: Prime q)) 1
frobTwisted _ _ = O
-- | Unitary exponentiation @^@.
--
-- Exponentiation of a unitary element @x@ to an arbitrary integer @n@
-- in a specified cyclotomic subgroup.
powUnitary :: IrreducibleMonic p k
=> Extension p k -- ^ Element @x@ in cyclotomic subgroup.
-> Integer -- ^ Integer @n@.
-> Extension p k -- ^ Element @x ^ n@.
powUnitary x n
| n < 0 = pow (conj x) (negate n)
| otherwise = pow x n
{-# INLINE powUnitary #-}