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

{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Algebra.EllipticCurve.BN254
  ( BN254_Scalar
  , BN254_Base
  , Fr
  , Fp
  , Fp2
  , Fp6
  , Fp12
  , BN254_G1
  , BN254_G2
  , BN254_GT) where

import           Control.Monad                              (return, (>>))
import           Data.Binary                                (Binary (..))
import           Data.Bool                                  ((&&))
import           Data.Eq                                    (Eq (..))
import           Data.Function                              (($))
import           Prelude                                    (Integer)
import           Text.Show                                  (Show)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field            (Ext2 (..), Ext3 (..), IrreduciblePoly (..), Zp)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.EllipticCurve.Pairing
import           ZkFold.Base.Algebra.Polynomials.Univariate (toPoly)

-------------------------- Scalar field & field towers -------------------------

-- Designations of curve parameters are as in:
-- https://pkg.go.dev/github.com/consensys/gnark-crypto/ecc/bn254

type BN254_Scalar = 21888242871839275222246405745257275088548364400416034343698204186575808495617
instance Prime BN254_Scalar

type BN254_Base = 21888242871839275222246405745257275088696311157297823662689037894645226208583
instance Prime BN254_Base

type Fr = Zp BN254_Scalar
type Fp = Zp BN254_Base

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

type Fp2 = Ext2 Fp "IP1"

-- cubic nonresidue in @Fp2@.
xi :: Fp2
xi :: Fp2
xi = Fp -> Fp -> Fp2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fp
9 Fp
1

instance IrreduciblePoly Fp2 "IP2" where
  irreduciblePoly :: Poly Fp2
irreduciblePoly = Vector Fp2 -> Poly Fp2
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Fp2 -> Fp2
forall a. AdditiveGroup a => a -> a
negate Fp2
xi, Item (Vector Fp2)
Fp2
forall a. AdditiveMonoid a => a
zero, Item (Vector Fp2)
Fp2
forall a. AdditiveMonoid a => a
zero, Item (Vector Fp2)
Fp2
forall a. MultiplicativeMonoid a => a
one]

type Fp6 = Ext3 Fp2 "IP2"

instance IrreduciblePoly Fp6 "IP3" where
  irreduciblePoly :: Poly Fp6
irreduciblePoly = Vector Fp6 -> Poly Fp6
forall c. (Ring c, Eq c) => Vector c -> Poly c
toPoly [Fp2 -> Fp2 -> Fp2 -> Fp6
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 Fp2
forall a. AdditiveMonoid a => a
zero (Fp2 -> Fp2
forall a. AdditiveGroup a => a -> a
negate Fp2
forall a. MultiplicativeMonoid a => a
one) Fp2
forall a. AdditiveMonoid a => a
zero, Item (Vector Fp6)
Fp6
forall a. AdditiveMonoid a => a
zero, Item (Vector Fp6)
Fp6
forall a. MultiplicativeMonoid a => a
one]

type Fp12 = Ext2 Fp6 "IP3"

------------------------------- bn254 G1 ---------------------------------------

data BN254_G1

instance EllipticCurve BN254_G1 where
  type ScalarField BN254_G1 = Fr
  type BaseField BN254_G1 = Fp
  pointGen :: Point BN254_G1
pointGen = Fp -> Fp -> Point BN254_G1
forall field plane. Planar field plane => field -> field -> plane
pointXY Fp
1 Fp
2
  add :: Point BN254_G1 -> Point BN254_G1 -> Point BN254_G1
add = Point BN254_G1 -> Point BN254_G1 -> Point BN254_G1
forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints
  mul :: ScalarField BN254_G1 -> Point BN254_G1 -> Point BN254_G1
mul = Fr -> Point BN254_G1 -> Point BN254_G1
ScalarField BN254_G1 -> Point BN254_G1 -> Point BN254_G1
forall curve s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance WeierstrassCurve BN254_G1 where
  weierstrassA :: BaseField BN254_G1
weierstrassA = Fp
BaseField BN254_G1
0
  weierstrassB :: BaseField BN254_G1
weierstrassB = Fp
BaseField BN254_G1
3

------------------------------- bn254 G2 ---------------------------------------

data BN254_G2

instance EllipticCurve BN254_G2 where
  type ScalarField BN254_G2 = Fr
  type BaseField BN254_G2 = Fp2
  pointGen :: Point BN254_G2
pointGen = Fp2 -> Fp2 -> Point BN254_G2
forall field plane. Planar field plane => field -> field -> plane
pointXY
    (Fp -> Fp -> Fp2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fp
0x1800deef121f1e76426a00665e5c4479674322d4f75edadd46debd5cd992f6ed
          Fp
0x198e9393920d483a7260bfb731fb5d25f1aa493335a9e71297e485b7aef312c2)
    (Fp -> Fp -> Fp2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fp
0x12c85ea5db8c6deb4aab71808dcb408fe3d1e7690c43d37b4ce6cc0166fa7daa
          Fp
0x90689d0585ff075ec9e99ad690c3395bc4b313370b38ef355acdadcd122975b)
  add :: Point BN254_G2 -> Point BN254_G2 -> Point BN254_G2
add = Point BN254_G2 -> Point BN254_G2 -> Point BN254_G2
forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints
  mul :: ScalarField BN254_G2 -> Point BN254_G2 -> Point BN254_G2
mul = Fr -> Point BN254_G2 -> Point BN254_G2
ScalarField BN254_G2 -> Point BN254_G2 -> Point BN254_G2
forall curve s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance WeierstrassCurve BN254_G2 where
  weierstrassA :: BaseField BN254_G2
weierstrassA = Fp2
BaseField BN254_G2
forall a. AdditiveMonoid a => a
zero
  weierstrassB :: BaseField BN254_G2
weierstrassB =
    Fp -> Fp -> Fp2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fp
0x2b149d40ceb8aaae81be18991be06ac3b5b4c5e559dbefa33267e6dc24a138e5
         Fp
0x9713b03af0fed4cd2cafadeed8fdf4a74fa084e52d1852e4a2bd0685c315d2

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

newtype BN254_GT = BN254_GT Fp12
  deriving (BN254_GT -> BN254_GT -> Bool
(BN254_GT -> BN254_GT -> Bool)
-> (BN254_GT -> BN254_GT -> Bool) -> Eq BN254_GT
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: BN254_GT -> BN254_GT -> Bool
== :: BN254_GT -> BN254_GT -> Bool
$c/= :: BN254_GT -> BN254_GT -> Bool
/= :: BN254_GT -> BN254_GT -> Bool
Eq, Int -> BN254_GT -> ShowS
[BN254_GT] -> ShowS
BN254_GT -> String
(Int -> BN254_GT -> ShowS)
-> (BN254_GT -> String) -> ([BN254_GT] -> ShowS) -> Show BN254_GT
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> BN254_GT -> ShowS
showsPrec :: Int -> BN254_GT -> ShowS
$cshow :: BN254_GT -> String
show :: BN254_GT -> String
$cshowList :: [BN254_GT] -> ShowS
showList :: [BN254_GT] -> ShowS
Show, Scale BN254_GT BN254_GT
FromConstant BN254_GT BN254_GT
(FromConstant BN254_GT BN254_GT, Scale BN254_GT BN254_GT) =>
(BN254_GT -> BN254_GT -> BN254_GT)
-> MultiplicativeSemigroup BN254_GT
BN254_GT -> BN254_GT -> BN254_GT
forall a.
(FromConstant a a, Scale a a) =>
(a -> a -> a) -> MultiplicativeSemigroup a
$c* :: BN254_GT -> BN254_GT -> BN254_GT
* :: BN254_GT -> BN254_GT -> BN254_GT
MultiplicativeSemigroup, Exponent BN254_GT Nat
MultiplicativeSemigroup BN254_GT
BN254_GT
(MultiplicativeSemigroup BN254_GT, Exponent BN254_GT Nat) =>
BN254_GT -> MultiplicativeMonoid BN254_GT
forall a.
(MultiplicativeSemigroup a, Exponent a Nat) =>
a -> MultiplicativeMonoid a
$cone :: BN254_GT
one :: BN254_GT
MultiplicativeMonoid)

instance Exponent BN254_GT Natural where
  BN254_GT Fp12
e ^ :: BN254_GT -> Nat -> BN254_GT
^ Nat
p = Fp12 -> BN254_GT
BN254_GT (Fp12
e Fp12 -> Nat -> Fp12
forall a b. Exponent a b => a -> b -> a
^ Nat
p)

instance Exponent BN254_GT Integer where
  BN254_GT Fp12
e ^ :: BN254_GT -> Integer -> BN254_GT
^ Integer
p = Fp12 -> BN254_GT
BN254_GT (Fp12
e Fp12 -> Integer -> Fp12
forall a b. Exponent a b => a -> b -> a
^ Integer
p)

deriving via (NonZero Fp12) instance MultiplicativeGroup BN254_GT

instance Finite BN254_GT where
  type Order BN254_GT = BN254_Scalar

instance Pairing BN254_G1 BN254_G2 where
  type TargetGroup BN254_G1 BN254_G2 = BN254_GT
  pairing :: Point BN254_G1 -> Point BN254_G2 -> TargetGroup BN254_G1 BN254_G2
pairing Point BN254_G1
p Point BN254_G2
q
    = Fp12 -> BN254_GT
BN254_GT
    (Fp12 -> BN254_GT) -> Fp12 -> BN254_GT
forall a b. (a -> b) -> a -> b
$ forall c g (i :: Symbol) (j :: Symbol).
(Finite (ScalarField c), Finite (BaseField c), g ~ Untwisted c i j,
 Exponent g Nat) =>
g -> g
finalExponentiation @BN254_G2
    (Fp12 -> Fp12) -> Fp12 -> Fp12
forall a b. (a -> b) -> a -> b
$ BaseField BN254_G2
-> [Int8] -> Point BN254_G1 -> Point BN254_G2 -> Fp12
forall c d (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
BaseField d -> [Int8] -> Point c -> Point d -> g
millerAlgorithmBN Fp2
BaseField BN254_G2
xi [Int8]
param Point BN254_G1
p Point BN254_G2
q
    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]
1, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
1
        , 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]
1, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
1
        , Item [Int8]
1, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
1, Item [Int8]
1, Item [Int8]
0
        , Item [Int8]
0, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0,-Item [Int8]
1, Item [Int8]
0, Item [Int8]
1, Item [Int8]
0, Item [Int8]
1, Item [Int8]
0, Item [Int8]
0, Item [Int8]
0
        ]

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

instance Binary (Point BN254_G1) where
  put :: Point BN254_G1 -> Put
put (Point BaseField BN254_G1
xp BaseField BN254_G1
yp BooleanOf BN254_G1
isInf) =
    if Bool
BooleanOf BN254_G1
isInf then forall t. Binary t => t -> Put
put @(Point BN254_G1) (Fp -> Fp -> Point BN254_G1
forall field plane. Planar field plane => field -> field -> plane
pointXY Fp
forall a. AdditiveMonoid a => a
zero Fp
forall a. AdditiveMonoid a => a
zero) else Fp -> Put
forall t. Binary t => t -> Put
put Fp
BaseField BN254_G1
xp Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Fp -> Put
forall t. Binary t => t -> Put
put Fp
BaseField BN254_G1
yp
  get :: Get (Point BN254_G1)
get = do
    Fp
xp <- Get Fp
forall t. Binary t => Get t
get
    Fp
yp <- Get Fp
forall t. Binary t => Get t
get
    Point BN254_G1 -> Get (Point BN254_G1)
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Point BN254_G1 -> Get (Point BN254_G1))
-> Point BN254_G1 -> Get (Point BN254_G1)
forall a b. (a -> b) -> a -> b
$
      if Fp
xp Fp -> Fp -> Bool
forall a. Eq a => a -> a -> Bool
== Fp
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
&& Fp
yp Fp -> Fp -> Bool
forall a. Eq a => a -> a -> Bool
== Fp
forall a. AdditiveMonoid a => a
zero
      then Point BN254_G1
forall plane. ProjectivePlanar plane => plane
pointInf
      else Fp -> Fp -> Point BN254_G1
forall field plane. Planar field plane => field -> field -> plane
pointXY Fp
xp Fp
yp

instance Binary (Point BN254_G2) where
  put :: Point BN254_G2 -> Put
put (Point BaseField BN254_G2
xp BaseField BN254_G2
yp BooleanOf BN254_G2
isInf) =
    if Bool
BooleanOf BN254_G2
isInf then forall t. Binary t => t -> Put
put @(Point BN254_G2) (Fp2 -> Fp2 -> Point BN254_G2
forall field plane. Planar field plane => field -> field -> plane
pointXY Fp2
forall a. AdditiveMonoid a => a
zero Fp2
forall a. AdditiveMonoid a => a
zero) else Fp2 -> Put
forall t. Binary t => t -> Put
put Fp2
BaseField BN254_G2
xp Put -> Put -> Put
forall a b. PutM a -> PutM b -> PutM b
forall (m :: Type -> Type) a b. Monad m => m a -> m b -> m b
>> Fp2 -> Put
forall t. Binary t => t -> Put
put Fp2
BaseField BN254_G2
yp
  get :: Get (Point BN254_G2)
get = do
    Fp2
xp <- Get Fp2
forall t. Binary t => Get t
get
    Fp2
yp <- Get Fp2
forall t. Binary t => Get t
get
    Point BN254_G2 -> Get (Point BN254_G2)
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Point BN254_G2 -> Get (Point BN254_G2))
-> Point BN254_G2 -> Get (Point BN254_G2)
forall a b. (a -> b) -> a -> b
$
      if Fp2
xp Fp2 -> Fp2 -> Bool
forall a. Eq a => a -> a -> Bool
== Fp2
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
&& Fp2
yp Fp2 -> Fp2 -> Bool
forall a. Eq a => a -> a -> Bool
== Fp2
forall a. AdditiveMonoid a => a
zero
      then Point BN254_G2
forall plane. ProjectivePlanar plane => plane
pointInf
      else Fp2 -> Fp2 -> Point BN254_G2
forall field plane. Planar field plane => field -> field -> plane
pointXY Fp2
xp Fp2
yp