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

module ZkFold.Base.Algebra.EllipticCurve.Ed25519  where

import           Prelude                                 (fromInteger, ($))

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

-- | The Ed25519 curve used in EdDSA signature scheme.
data Ed25519

-- | 2^252 + 27742317777372353535851937790883648493 is the order of the multiplicative group in Ed25519
-- with the generator point defined below in @instance EllipticCurve (Ed25519 Void r)@
--
type Ed25519_Scalar = 7237005577332262213973186563042994240857116359379907606001950938285454250989
instance Prime Ed25519_Scalar

-- | 2^255 - 19 is the order of the base field from which point coordinates are taken.
--
type Ed25519_Base = 57896044618658097711785492504343953926634992332820282019728792003956564819949
instance Prime Ed25519_Base

-- | The purely mathematical implementation of Ed25519.
-- It is available for use as-is and serves as "backend" for the @UInt 256 (Zp p)@ implementation as well.
--
instance EllipticCurve Ed25519 where
    type BaseField Ed25519 = Zp Ed25519_Base
    type ScalarField Ed25519 = Zp Ed25519_Scalar

    gen :: Point Ed25519
gen = Zp Ed25519_Base -> Zp Ed25519_Base -> Point Ed25519
forall field plane. Planar field plane => field -> field -> plane
point
            (forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp @Ed25519_Base (Integer -> Zp Ed25519_Base) -> Integer -> Zp Ed25519_Base
forall a b. (a -> b) -> a -> b
$ Integer
15112221349535400772501151409588531511454012693041857206046113283949847762202)
            (forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp @Ed25519_Base (Integer -> Zp Ed25519_Base) -> Integer -> Zp Ed25519_Base
forall a b. (a -> b) -> a -> b
$ Integer
46316835694926478169428394003475163141307993866256225615783033603165251855960)

    add :: Point Ed25519 -> Point Ed25519 -> Point Ed25519
add Point Ed25519
p1 Point Ed25519
p2 = if Point Ed25519
p1 Point Ed25519 -> Point Ed25519 -> Bool
forall b a. Eq b a => a -> a -> b
== Point Ed25519
p2 then Point Ed25519 -> Point Ed25519
ed25519Double Point Ed25519
p1 else Point Ed25519 -> Point Ed25519 -> Point Ed25519
ed25519Add Point Ed25519
p1 Point Ed25519
p2

    mul :: ScalarField Ed25519 -> Point Ed25519 -> Point Ed25519
mul = Zp Ed25519_Scalar -> Point Ed25519 -> Point Ed25519
ScalarField Ed25519 -> Point Ed25519 -> Point Ed25519
forall curve s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul


ed25519Add :: Point Ed25519 -> Point Ed25519 -> Point Ed25519
ed25519Add :: Point Ed25519 -> Point Ed25519 -> Point Ed25519
ed25519Add p :: Point Ed25519
p@(Point BaseField Ed25519
x1 BaseField Ed25519
y1 BooleanOf Ed25519
isInf1) q :: Point Ed25519
q@(Point BaseField Ed25519
x2 BaseField Ed25519
y2 BooleanOf Ed25519
isInf2) =
    if Bool
BooleanOf Ed25519
isInf2 then Point Ed25519
p else if Bool
BooleanOf Ed25519
isInf1 then Point Ed25519
q else Zp Ed25519_Base -> Zp Ed25519_Base -> Point Ed25519
forall field plane. Planar field plane => field -> field -> plane
point Zp Ed25519_Base
x3 Zp Ed25519_Base
y3
    where
        d :: BaseField Ed25519
        d :: BaseField Ed25519
d = BaseField Ed25519 -> BaseField Ed25519
forall a. AdditiveGroup a => a -> a
negate (BaseField Ed25519 -> BaseField Ed25519)
-> BaseField Ed25519 -> BaseField Ed25519
forall a b. (a -> b) -> a -> b
$ Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
121665 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
121666

        a :: BaseField Ed25519
        a :: BaseField Ed25519
a = BaseField Ed25519 -> BaseField Ed25519
forall a. AdditiveGroup a => a -> a
negate (BaseField Ed25519 -> BaseField Ed25519)
-> BaseField Ed25519 -> BaseField Ed25519
forall a b. (a -> b) -> a -> b
$ Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
1

        x3 :: Zp Ed25519_Base
x3 = (Zp Ed25519_Base
BaseField Ed25519
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveSemigroup a => a -> a -> a
+ Zp Ed25519_Base
BaseField Ed25519
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x2) Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveSemigroup a => a -> a -> a
+ Zp Ed25519_Base
BaseField Ed25519
d Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y2)
        y3 :: Zp Ed25519_Base
y3 = (Zp Ed25519_Base
BaseField Ed25519
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- Zp Ed25519_Base
BaseField Ed25519
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x2) Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- Zp Ed25519_Base
BaseField Ed25519
d Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y2)

ed25519Double :: Point Ed25519 -> Point Ed25519
ed25519Double :: Point Ed25519 -> Point Ed25519
ed25519Double (Point BaseField Ed25519
x BaseField Ed25519
y BooleanOf Ed25519
isInf) = if Bool
BooleanOf Ed25519
isInf then Point Ed25519
forall plane. ProjectivePlanar plane => plane
inf else Zp Ed25519_Base -> Zp Ed25519_Base -> Point Ed25519
forall field plane. Planar field plane => field -> field -> plane
point Zp Ed25519_Base
x3 Zp Ed25519_Base
y3
    where
        a :: BaseField Ed25519
        a :: BaseField Ed25519
a = BaseField Ed25519 -> BaseField Ed25519
forall a. AdditiveGroup a => a -> a
negate (BaseField Ed25519 -> BaseField Ed25519)
-> BaseField Ed25519 -> BaseField Ed25519
forall a b. (a -> b) -> a -> b
$ Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
1

        x3 :: Zp Ed25519_Base
x3 = Zp Ed25519_Base
2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (Zp Ed25519_Base
BaseField Ed25519
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveSemigroup a => a -> a -> a
+ Zp Ed25519_Base
BaseField Ed25519
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y)
        y3 :: Zp Ed25519_Base
y3 = (Zp Ed25519_Base
BaseField Ed25519
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- Zp Ed25519_Base
BaseField Ed25519
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x) Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (Integer -> Zp Ed25519_Base
forall (p :: Nat). KnownNat p => Integer -> Zp p
toZp Integer
2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- Zp Ed25519_Base
BaseField Ed25519
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- Zp Ed25519_Base
BaseField Ed25519
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* Zp Ed25519_Base
BaseField Ed25519
y)