{-# OPTIONS_GHC -Wno-orphans #-}

module ZkFold.Base.Algebra.EllipticCurve.Ed25519  where

import           Data.Void                               (Void)
import           Prelude                                 (otherwise, ($), (==))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class

-- | The Ed25519 curve used in EdDSA signature scheme.
-- @c@ represents the "computational context" used to store and perform operations on curve points.
--
data Ed25519 c

-- | 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 Void) where
    type BaseField (Ed25519 Void) = Zp Ed25519_Base
    type ScalarField (Ed25519 Void) = Zp Ed25519_Scalar

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

    gen :: Point (Ed25519 Void)
gen = BaseField (Ed25519 Void)
-> BaseField (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
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 Void)
-> Point (Ed25519 Void) -> Point (Ed25519 Void)
add Point (Ed25519 Void)
p1 Point (Ed25519 Void)
p2
      | Point (Ed25519 Void)
p1 Point (Ed25519 Void) -> Point (Ed25519 Void) -> Bool
forall a. Eq a => a -> a -> Bool
== Point (Ed25519 Void)
p2  = Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Double Point (Ed25519 Void)
p1
      | Bool
otherwise = Point (Ed25519 Void)
-> Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Add Point (Ed25519 Void)
p1 Point (Ed25519 Void)
p2

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


ed25519Add :: Point (Ed25519 Void) -> Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Add :: Point (Ed25519 Void)
-> Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Add Point (Ed25519 Void)
p Point (Ed25519 Void)
Inf = Point (Ed25519 Void)
p
ed25519Add Point (Ed25519 Void)
Inf Point (Ed25519 Void)
q = Point (Ed25519 Void)
q
ed25519Add (Point BaseField (Ed25519 Void)
x1 BaseField (Ed25519 Void)
y1) (Point BaseField (Ed25519 Void)
x2 BaseField (Ed25519 Void)
y2) = BaseField (Ed25519 Void)
-> BaseField (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField (Ed25519 Void)
Zp Ed25519_Base
x3 BaseField (Ed25519 Void)
Zp Ed25519_Base
y3
    where
        d :: BaseField (Ed25519 Void)
        d :: BaseField (Ed25519 Void)
d = BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
forall a. AdditiveGroup a => a -> a
negate (BaseField (Ed25519 Void) -> BaseField (Ed25519 Void))
-> BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
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 Void)
        a :: BaseField (Ed25519 Void)
a = BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
forall a. AdditiveGroup a => a -> a
negate (BaseField (Ed25519 Void) -> BaseField (Ed25519 Void))
-> BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
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 = (BaseField (Ed25519 Void)
Zp Ed25519_Base
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField (Ed25519 Void)
Zp Ed25519_Base
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
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
+ BaseField (Ed25519 Void)
Zp Ed25519_Base
d Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y2)
        y3 :: Zp Ed25519_Base
y3 = (BaseField (Ed25519 Void)
Zp Ed25519_Base
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- BaseField (Ed25519 Void)
Zp Ed25519_Base
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
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
- BaseField (Ed25519 Void)
Zp Ed25519_Base
d Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x2 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y1 Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y2)

ed25519Double :: Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Double :: Point (Ed25519 Void) -> Point (Ed25519 Void)
ed25519Double Point (Ed25519 Void)
Inf = Point (Ed25519 Void)
forall {k} (curve :: k). Point curve
Inf
ed25519Double (Point BaseField (Ed25519 Void)
x BaseField (Ed25519 Void)
y) = BaseField (Ed25519 Void)
-> BaseField (Ed25519 Void) -> Point (Ed25519 Void)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point BaseField (Ed25519 Void)
Zp Ed25519_Base
x3 BaseField (Ed25519 Void)
Zp Ed25519_Base
y3
    where
        a :: BaseField (Ed25519 Void)
        a :: BaseField (Ed25519 Void)
a = BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
forall a. AdditiveGroup a => a -> a
negate (BaseField (Ed25519 Void) -> BaseField (Ed25519 Void))
-> BaseField (Ed25519 Void) -> BaseField (Ed25519 Void)
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
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. Field a => a -> a -> a
// (BaseField (Ed25519 Void)
Zp Ed25519_Base
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField (Ed25519 Void)
Zp Ed25519_Base
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y)
        y3 :: Zp Ed25519_Base
y3 = (BaseField (Ed25519 Void)
Zp Ed25519_Base
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- BaseField (Ed25519 Void)
Zp Ed25519_Base
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
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
- BaseField (Ed25519 Void)
Zp Ed25519_Base
a Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
x Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. AdditiveGroup a => a -> a -> a
- BaseField (Ed25519 Void)
Zp Ed25519_Base
y Zp Ed25519_Base -> Zp Ed25519_Base -> Zp Ed25519_Base
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField (Ed25519 Void)
Zp Ed25519_Base
y)