{-# 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
  inf :: Point BN254_G1
inf = Point BN254_G1
forall {k} (curve :: k). Point curve
Inf
  gen :: Point BN254_G1
gen = BaseField BN254_G1 -> BaseField BN254_G1 -> Point BN254_G1
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField BN254_G1
Fp
1 BaseField BN254_G1
Fp
2
  add :: Point BN254_G1 -> Point BN254_G1 -> Point BN254_G1
add = Point BN254_G1 -> Point BN254_G1 -> Point BN254_G1
forall {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints
  mul :: ScalarField BN254_G1 -> Point BN254_G1 -> Point BN254_G1
mul = ScalarField BN254_G1 -> Point BN254_G1 -> Point BN254_G1
Fr -> Point BN254_G1 -> Point BN254_G1
forall {k} (curve :: k) s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance StandardEllipticCurve BN254_G1 where
  aParameter :: BaseField BN254_G1
aParameter = BaseField BN254_G1
Fp
0
  bParameter :: BaseField BN254_G1
bParameter = BaseField BN254_G1
Fp
3

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

data BN254_G2

instance EllipticCurve BN254_G2 where
  type ScalarField BN254_G2 = Fr
  type BaseField BN254_G2 = Fp2
  inf :: Point BN254_G2
inf = Point BN254_G2
forall {k} (curve :: k). Point curve
Inf
  gen :: Point BN254_G2
gen = BaseField BN254_G2 -> BaseField BN254_G2 -> Point BN254_G2
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
    (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 {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints
  mul :: ScalarField BN254_G2 -> Point BN254_G2 -> Point BN254_G2
mul = ScalarField BN254_G2 -> Point BN254_G2 -> Point BN254_G2
Fr -> Point BN254_G2 -> Point BN254_G2
forall {k} (curve :: k) s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance StandardEllipticCurve BN254_G2 where
  aParameter :: BaseField BN254_G2
aParameter = BaseField BN254_G2
Fp2
forall a. AdditiveMonoid a => a
zero
  bParameter :: BaseField BN254_G2
bParameter =
    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 {k} (c :: k) g (i :: Symbol) (j :: Symbol).
(Finite (ScalarField c), Finite (BaseField c), g ~ Untwisted c i j,
 Exponent g Nat) =>
g -> g
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 {k1} {k2} (c :: k1) (d :: k2) (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g) =>
BaseField d -> [Int8] -> Point c -> Point d -> g
millerAlgorithmBN BaseField BN254_G2
Fp2
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 BN254_G1
Inf           = Point BN254_G1 -> Put
forall t. Binary t => t -> Put
put (forall curve. BaseField curve -> BaseField curve -> Point curve
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point @BN254_G1 BaseField BN254_G1
Fp
forall a. AdditiveMonoid a => a
zero BaseField BN254_G1
Fp
forall a. AdditiveMonoid a => a
zero)
  put (Point BaseField BN254_G1
xp BaseField BN254_G1
yp) = Fp -> Put
forall t. Binary t => t -> Put
put BaseField BN254_G1
Fp
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 BaseField BN254_G1
Fp
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 {k} (curve :: k). Point curve
Inf
      else BaseField BN254_G1 -> BaseField BN254_G1 -> Point BN254_G1
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField BN254_G1
Fp
xp BaseField BN254_G1
Fp
yp

instance Binary (Point BN254_G2) where
  put :: Point BN254_G2 -> Put
put Point BN254_G2
Inf           = Point BN254_G2 -> Put
forall t. Binary t => t -> Put
put (forall curve. BaseField curve -> BaseField curve -> Point curve
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point @BN254_G2 BaseField BN254_G2
Fp2
forall a. AdditiveMonoid a => a
zero BaseField BN254_G2
Fp2
forall a. AdditiveMonoid a => a
zero)
  put (Point BaseField BN254_G2
xp BaseField BN254_G2
yp) = Fp2 -> Put
forall t. Binary t => t -> Put
put BaseField BN254_G2
Fp2
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 BaseField BN254_G2
Fp2
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 {k} (curve :: k). Point curve
Inf
      else BaseField BN254_G2 -> BaseField BN254_G2 -> Point BN254_G2
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField BN254_G2
Fp2
xp BaseField BN254_G2
Fp2
yp