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

module ZkFold.Base.Algebra.EllipticCurve.Pasta
  ( Pasta_Point
  , Pallas_Point
  , Vesta_Point
  , FpModulus
  , FqModulus
  , Fp
  , Fq
  ) where

import           Control.Monad
import           Prelude                                 (type (~), ($))
import qualified Prelude

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.Data.ByteString
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Eq

-------------------------------- Introducing Fields ----------------------------------

type FpModulus = 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
instance Prime FpModulus

type FqModulus = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
instance Prime FqModulus

type Fp = Zp FpModulus
type Fq = Zp FqModulus

------------------------------------ Pasta -------------------------------------

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

type Pasta_Point field = Weierstrass "Pasta" (Point field)

------------------------------------ Pallas ------------------------------------

type Pallas_Point = Pasta_Point Fp

instance CyclicGroup Pallas_Point where
  type ScalarFieldOf Pallas_Point = Fq
  pointGen :: Pallas_Point
pointGen = Zp FpModulus -> Zp FpModulus -> Pallas_Point
forall field point. Planar field point => field -> field -> point
pointXY
    Zp FpModulus
0x40000000000000000000000000000000224698fc094cf91b992d30ed00000000
    Zp FpModulus
0x02

instance Scale Fq Pallas_Point where
    scale :: Fq -> Pallas_Point -> Pallas_Point
scale Fq
n Pallas_Point
x = Nat -> Pallas_Point -> Pallas_Point
forall b a. Scale b a => b -> a -> a
scale (Fq -> Const Fq
forall a. ToConstant a => a -> Const a
toConstant Fq
n) Pallas_Point
x

------------------------------------ Vesta ------------------------------------

type Vesta_Point = Pasta_Point Fq

instance CyclicGroup Vesta_Point where
  type ScalarFieldOf Vesta_Point = Fp
  pointGen :: Vesta_Point
pointGen = Fq -> Fq -> Vesta_Point
forall field point. Planar field point => field -> field -> point
pointXY
    Fq
0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000000
    Fq
0x02

instance Scale Fp Vesta_Point where
    scale :: Zp FpModulus -> Vesta_Point -> Vesta_Point
scale Zp FpModulus
n Vesta_Point
x = Nat -> Vesta_Point -> Vesta_Point
forall b a. Scale b a => b -> a -> a
scale (Zp FpModulus -> Const (Zp FpModulus)
forall a. ToConstant a => a -> Const a
toConstant Zp FpModulus
n) Vesta_Point
x

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

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