{-# LANGUAGE DerivingVia #-}
{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Algebra.EllipticCurve.Pasta where

import           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

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

type FpModulus = 0x40000000000000000000000000000000224698fc094cf91b992d30ed00000001
instance Prime FpModulus

type FqModulus = 0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000001
instance Prime FqModulus

type Fp = Zp FpModulus
type Fq = Zp FqModulus

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

data Pallas

instance EllipticCurve Pallas where
    type ScalarField Pallas = Fq

    type BaseField Pallas = Fp

    inf :: Point Pallas
inf = Point Pallas
forall {k} (curve :: k). Point curve
Inf

    gen :: Point Pallas
gen = BaseField Pallas -> BaseField Pallas -> Point Pallas
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
        BaseField Pallas
Fp
0x40000000000000000000000000000000224698fc094cf91b992d30ed00000000
        BaseField Pallas
Fp
0x02

    add :: Point Pallas -> Point Pallas -> Point Pallas
add = Point Pallas -> Point Pallas -> Point Pallas
forall {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints

    mul :: ScalarField Pallas -> Point Pallas -> Point Pallas
mul = ScalarField Pallas -> Point Pallas -> Point Pallas
Fq -> Point Pallas -> Point Pallas
forall {k} (curve :: k) s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance StandardEllipticCurve Pallas where
    aParameter :: BaseField Pallas
aParameter = BaseField Pallas
Fp
forall a. AdditiveMonoid a => a
zero

    bParameter :: BaseField Pallas
bParameter = Nat -> Fp
forall a b. FromConstant a b => a -> b
fromConstant (Nat
5 :: Natural)

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

data Vesta

instance EllipticCurve Vesta where

    type ScalarField Vesta = Fp

    type BaseField Vesta = Fq

    inf :: Point Vesta
inf = Point Vesta
forall {k} (curve :: k). Point curve
Inf

    gen :: Point Vesta
gen = BaseField Vesta -> BaseField Vesta -> Point Vesta
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
        BaseField Vesta
Fq
0x40000000000000000000000000000000224698fc0994a8dd8c46eb2100000000
        BaseField Vesta
Fq
0x02

    add :: Point Vesta -> Point Vesta -> Point Vesta
add = Point Vesta -> Point Vesta -> Point Vesta
forall {k} (curve :: k).
(EllipticCurve curve, Field (BaseField curve),
 Eq (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints

    mul :: ScalarField Vesta -> Point Vesta -> Point Vesta
mul = ScalarField Vesta -> Point Vesta -> Point Vesta
Fp -> Point Vesta -> Point Vesta
forall {k} (curve :: k) s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance StandardEllipticCurve Vesta where
    aParameter :: BaseField Vesta
aParameter = BaseField Vesta
Fq
forall a. AdditiveMonoid a => a
zero

    bParameter :: BaseField Vesta
bParameter = Nat -> Fq
forall a b. FromConstant a b => a -> b
fromConstant (Nat
5 :: Natural)

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

instance Binary (Point Pallas) where
  put :: Point Pallas -> Put
put Point Pallas
Inf           = Point Pallas -> 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 @Pallas BaseField Pallas
Fp
forall a. AdditiveMonoid a => a
zero BaseField Pallas
Fp
forall a. AdditiveMonoid a => a
zero)
  put (Point BaseField Pallas
xp BaseField Pallas
yp) = Fp -> Put
forall t. Binary t => t -> Put
put BaseField Pallas
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 Pallas
Fp
yp
  get :: Get (Point Pallas)
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 Pallas -> Get (Point Pallas)
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Point Pallas -> Get (Point Pallas))
-> Point Pallas -> Get (Point Pallas)
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 Pallas
forall {k} (curve :: k). Point curve
Inf
      else BaseField Pallas -> BaseField Pallas -> Point Pallas
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField Pallas
Fp
xp BaseField Pallas
Fp
yp

instance Binary (Point Vesta) where
  put :: Point Vesta -> Put
put Point Vesta
Inf           = Point Vesta -> 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 @Vesta BaseField Vesta
Fq
forall a. AdditiveMonoid a => a
zero BaseField Vesta
Fq
forall a. AdditiveMonoid a => a
zero)
  put (Point BaseField Vesta
xp BaseField Vesta
yp) = Fq -> Put
forall t. Binary t => t -> Put
put BaseField Vesta
Fq
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
>> Fq -> Put
forall t. Binary t => t -> Put
put BaseField Vesta
Fq
yp
  get :: Get (Point Vesta)
get = do
    Fq
xp <- Get Fq
forall t. Binary t => Get t
get
    Fq
yp <- Get Fq
forall t. Binary t => Get t
get
    Point Vesta -> Get (Point Vesta)
forall a. a -> Get a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Point Vesta -> Get (Point Vesta))
-> Point Vesta -> Get (Point Vesta)
forall a b. (a -> b) -> a -> b
$
      if Fq
xp Fq -> Fq -> Bool
forall a. Eq a => a -> a -> Bool
== Fq
forall a. AdditiveMonoid a => a
zero Bool -> Bool -> Bool
&& Fq
yp Fq -> Fq -> Bool
forall a. Eq a => a -> a -> Bool
== Fq
forall a. AdditiveMonoid a => a
zero
      then Point Vesta
forall {k} (curve :: k). Point curve
Inf
      else BaseField Vesta -> BaseField Vesta -> Point Vesta
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField Vesta
Fq
xp BaseField Vesta
Fq
yp