{-# LANGUAGE DerivingVia          #-}
{-# LANGUAGE OverloadedLists      #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -Wno-orphans #-}

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

import           Control.Monad                              (return, (>>))
import           Data.Binary                                (Binary (..))
import           Data.Bool                                  ((&&))
import           Data.Function                              (($))
import           Prelude                                    (Bool, Integer)
import qualified Prelude
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)
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq

-------------------------- 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 ---------------------------------------

type BN254_G1_Point = BN254_G1_PointOf Fp

type BN254_G1_PointOf field = Weierstrass "BN254_G1" (Point field)

instance Field field => WeierstrassCurve "BN254_G1" field where
  weierstrassB :: field
weierstrassB = Nat -> field
forall a b. FromConstant a b => a -> b
fromConstant (Nat
3 :: Natural)

instance CyclicGroup BN254_G1_Point where
  type ScalarFieldOf BN254_G1_Point = Fr
  pointGen :: BN254_G1_Point
pointGen = Fp -> Fp -> BN254_G1_Point
forall field point. Planar field point => field -> field -> point
pointXY Fp
1 Fp
2

instance Scale Fr BN254_G1_Point where
  scale :: Fr -> BN254_G1_Point -> BN254_G1_Point
scale Fr
n BN254_G1_Point
x = Nat -> BN254_G1_Point -> BN254_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) BN254_G1_Point
x

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

type BN254_G2_Point = BN254_G2_PointOf Fp2

type BN254_G2_PointOf field = Weierstrass "BN254_G2" (Point field)

instance WeierstrassCurve "BN254_G2" Fp2 where
  weierstrassB :: Fp2
weierstrassB =
    Fp -> Fp -> Fp2
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 Fp
0x2b149d40ceb8aaae81be18991be06ac3b5b4c5e559dbefa33267e6dc24a138e5
         Fp
0x9713b03af0fed4cd2cafadeed8fdf4a74fa084e52d1852e4a2bd0685c315d2

instance CyclicGroup BN254_G2_Point where
  type ScalarFieldOf BN254_G2_Point = Fr
  pointGen :: BN254_G2_Point
pointGen = Fp2 -> Fp2 -> BN254_G2_Point
forall field point. Planar field point => field -> field -> point
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)

instance Scale Fr BN254_G2_Point where
  scale :: Fr -> BN254_G2_Point -> BN254_G2_Point
scale Fr
n BN254_G2_Point
x = Nat -> BN254_G2_Point -> BN254_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) BN254_G2_Point
x

------------------------------- 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
Prelude.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
    , Conditional Prelude.Bool
    , Conditional (BooleanOf BN254_GT) BN254_GT
Conditional (BooleanOf BN254_GT) BN254_GT =>
(BN254_GT -> BN254_GT -> BooleanOf BN254_GT)
-> (BN254_GT -> BN254_GT -> BooleanOf BN254_GT) -> Eq BN254_GT
BN254_GT -> BN254_GT -> BooleanOf BN254_GT
forall a.
Conditional (BooleanOf a) a =>
(a -> a -> BooleanOf a) -> (a -> a -> BooleanOf a) -> Eq a
$c== :: BN254_GT -> BN254_GT -> BooleanOf BN254_GT
== :: BN254_GT -> BN254_GT -> BooleanOf BN254_GT
$c/= :: BN254_GT -> BN254_GT -> BooleanOf BN254_GT
/= :: BN254_GT -> BN254_GT -> BooleanOf BN254_GT
Eq
    )

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_Point BN254_G2_Point BN254_GT where
  pairing :: BN254_G1_Point -> BN254_G2_Point -> BN254_GT
pairing BN254_G1_Point
p BN254_G2_Point
q
    = Fp12 -> BN254_GT
BN254_GT
    (Fp12 -> BN254_GT) -> Fp12 -> BN254_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 Nat) =>
g -> g
finalExponentiation @Fr
    (Fp12 -> Fp12) -> Fp12 -> Fp12
forall a b. (a -> b) -> a -> b
$ Fp2 -> [Int8] -> BN254_G1_Point -> BN254_G2_Point -> Fp12
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) =>
fldD
-> [Int8]
-> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> g
millerAlgorithmBN Fp2
xi [Int8]
param BN254_G1_Point
p BN254_G2_Point
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 BN254_G1_Point where
  put :: BN254_G1_Point -> Put
put (Weierstrass (Point Fp
xp Fp
yp BooleanOf Fp
isInf)) =
    if Bool
BooleanOf Fp
isInf then forall t. Binary t => t -> Put
put @BN254_G1_Point (Fp -> Fp -> BN254_G1_Point
forall field point. Planar field point => field -> field -> point
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
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
yp
  get :: Get BN254_G1_Point
get = do
    Fp
xp <- Get Fp
forall t. Binary t => Get t
get
    Fp
yp <- Get Fp
forall t. Binary t => Get t
get
    BN254_G1_Point -> Get BN254_G1_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BN254_G1_Point -> Get BN254_G1_Point)
-> BN254_G1_Point -> Get BN254_G1_Point
forall a b. (a -> b) -> a -> b
$
      if Fp
xp Fp -> Fp -> BooleanOf Fp
forall a. Eq a => a -> a -> BooleanOf a
== Fp
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
&& Fp
yp Fp -> Fp -> BooleanOf Fp
forall a. Eq a => a -> a -> BooleanOf a
== Fp
forall a. AdditiveMonoid a => a
zero
      then BN254_G1_Point
forall point. HasPointInf point => point
pointInf
      else Fp -> Fp -> BN254_G1_Point
forall field point. Planar field point => field -> field -> point
pointXY Fp
xp Fp
yp

instance Binary BN254_G2_Point where
  put :: BN254_G2_Point -> Put
put (Weierstrass (Point Fp2
xp Fp2
yp BooleanOf Fp2
isInf)) =
    if Bool
BooleanOf Fp2
isInf then forall t. Binary t => t -> Put
put @BN254_G2_Point (Fp2 -> Fp2 -> BN254_G2_Point
forall field point. Planar field point => field -> field -> point
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
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
yp
  get :: Get BN254_G2_Point
get = do
    Fp2
xp <- Get Fp2
forall t. Binary t => Get t
get
    Fp2
yp <- Get Fp2
forall t. Binary t => Get t
get
    BN254_G2_Point -> Get BN254_G2_Point
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (BN254_G2_Point -> Get BN254_G2_Point)
-> BN254_G2_Point -> Get BN254_G2_Point
forall a b. (a -> b) -> a -> b
$
      if Fp2
xp Fp2 -> Fp2 -> BooleanOf Fp2
forall a. Eq a => a -> a -> BooleanOf a
== Fp2
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
&& Fp2
yp Fp2 -> Fp2 -> BooleanOf Fp2
forall a. Eq a => a -> a -> BooleanOf a
== Fp2
forall a. AdditiveMonoid a => a
zero
      then BN254_G2_Point
forall point. HasPointInf point => point
pointInf
      else Fp2 -> Fp2 -> BN254_G2_Point
forall field point. Planar field point => field -> field -> point
pointXY Fp2
xp Fp2
yp