{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DerivingStrategies    #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RebindableSyntax      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}

module ZkFold.Base.Algebra.EllipticCurve.Class
  ( -- * curve classes
    EllipticCurve (..)
  , CyclicGroup (..)
  , CycleOfCurves
  , WeierstrassCurve (..)
  , TwistedEdwardsCurve (..)
  , Compressible (..)
  , Pairing (..)
    -- * point classes
  , Planar (..)
  , HasPointInf (..)
    -- * point types
  , Weierstrass (..)
  , TwistedEdwards (..)
  , Point (..)
  , CompressedPoint (..)
  , AffinePoint (..)
  ) where

import           Data.Kind                        (Type)
import           Data.String                      (fromString)
import           GHC.Generics
import           GHC.TypeLits                     (Symbol)
import           Prelude                          (Integer, return, type (~), ($), (>>=))
import qualified Prelude
import           Test.QuickCheck                  hiding (scale)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.Input

{- | Elliptic curves are plane algebraic curves that form `AdditiveGroup`s.
Elliptic curves always have genus @1@ and are birationally equivalent
to a projective curve of degree @3@. As such, elliptic curves are
the simplest curves after conic sections, curves of degree @2@,
and lines, curves of degree @1@. Bézout's theorem implies
that a line in general position will intersect with an
elliptic curve at 3 points counting multiplicity;
@point0@, @point1@ and @point2@.
The geometric group law of the elliptic curve is:

> point0 + point1 + point2 = zero
-}
class
  ( Field (BaseFieldOf point)
  , Eq (BaseFieldOf point)
  , Planar (BaseFieldOf point) point
  , AdditiveGroup point
  ) => EllipticCurve point where
    type CurveOf point :: Symbol
    type BaseFieldOf point :: Type
    -- | `isOnCurve` validates an equation for a plane algebraic curve
    -- which has degree 3 up to some birational equivalence.
    isOnCurve :: point -> BooleanOf (BaseFieldOf point)

{- | Both the ECDSA and ECDH algorithms make use of
the elliptic curve discrete logarithm problem, ECDLP.
There may be a discrete "exponential" function
from a `PrimeField` of scalars
into the `AdditiveGroup` of points on an elliptic curve.
It's given naturally by scaling a point of prime order,
if there is one on the curve.

prop> scale order pointGen = zero

>>> let discreteExp scalar = scale scalar pointGen

Then the inverse of `discreteExp` is hard to compute.
-}
class
  ( AdditiveGroup g
  , FiniteField (ScalarFieldOf g)
  , Scale (ScalarFieldOf g) g
  ) => CyclicGroup g where
    type ScalarFieldOf g :: Type
    -- | generator of a cyclic subgroup
    --
    -- prop> scale (order @(ScalarFieldOf g)) pointGen = zero
    pointGen :: g

{- |
A cycle of two curves elliptic curves over finite fields
such that the number of points on one curve is equal to
the size of the field of definition of the next, in a cyclic way.
-}
type CycleOfCurves g1 g2 =
  ( EllipticCurve g1
  , EllipticCurve g2
  , CyclicGroup g1
  , CyclicGroup g2
  , ScalarFieldOf g1 ~ BaseFieldOf g2
  , BaseFieldOf g1 ~ ScalarFieldOf g2
  )

{- | The standard form of an elliptic curve is the Weierstrass equation:

> y^2 = x^3 + a*x + b

* Weierstrass curves have x-axis symmetry.
* The characteristic of the field must not be @2@ or @3@.
* The curve must have nonzero discriminant @Δ = -16 * (4*a^3 + 27*b^3)@.
* When @a = 0@ some computations can be simplified so all the public
  Weierstrass curves have @a = zero@ and nonzero @b@ and we do too.
-}
class Field field => WeierstrassCurve (curve :: Symbol) field where
  weierstrassB :: field

{- | A twisted Edwards curve is defined by the equation:

> a*x^2 + y^2 = 1 + d*x^2*y^2

* Twisted Edwards curves have y-axis symmetry.
* The characteristic of the field must not be @2@.
* @a@ and @d@ must be nonzero.
-}
class Field field => TwistedEdwardsCurve (curve :: Symbol) field where
  twistedEdwardsA :: field
  twistedEdwardsD :: field

class Eq (BaseFieldOf point) => Compressible point where
  type Compressed point :: Type
  pointCompressed
    :: BaseFieldOf point
    -> BooleanOf (BaseFieldOf point)
    -> Compressed point
  compress :: point -> Compressed point
  decompress :: Compressed point -> point

class
  ( CyclicGroup g1
  , CyclicGroup g2
  , ScalarFieldOf g1 ~ ScalarFieldOf g2
  , MultiplicativeGroup gt
  , Exponent gt (ScalarFieldOf g1)
  ) => Pairing g1 g2 gt | g1 g2 -> gt where
    pairing :: g1 -> g2 -> gt

{- | A class for smart constructor method
`pointXY` for constructing points from an @x@ and @y@ coordinate. -}
class Planar field point | point -> field where
  pointXY :: field -> field -> point

{- | A class for smart constructor method
`pointInf` for constructing the point at infinity. -}
class HasPointInf point where pointInf :: point

{- | `Weierstrass` tags a `ProjectivePlanar` @point@, over a `Field` @field@,
with a phantom `WeierstrassCurve` @curve@. -}
newtype Weierstrass curve point = Weierstrass {forall {k} (curve :: k) point. Weierstrass curve point -> point
pointWeierstrass :: point}
  deriving (forall x.
 Weierstrass curve point -> Rep (Weierstrass curve point) x)
-> (forall x.
    Rep (Weierstrass curve point) x -> Weierstrass curve point)
-> Generic (Weierstrass curve point)
forall x.
Rep (Weierstrass curve point) x -> Weierstrass curve point
forall x.
Weierstrass curve point -> Rep (Weierstrass curve point) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (curve :: k) point x.
Rep (Weierstrass curve point) x -> Weierstrass curve point
forall k (curve :: k) point x.
Weierstrass curve point -> Rep (Weierstrass curve point) x
$cfrom :: forall k (curve :: k) point x.
Weierstrass curve point -> Rep (Weierstrass curve point) x
from :: forall x.
Weierstrass curve point -> Rep (Weierstrass curve point) x
$cto :: forall k (curve :: k) point x.
Rep (Weierstrass curve point) x -> Weierstrass curve point
to :: forall x.
Rep (Weierstrass curve point) x -> Weierstrass curve point
Generic
deriving newtype instance Prelude.Eq point
  => Prelude.Eq (Weierstrass curve point)
deriving newtype instance Prelude.Show point
  => Prelude.Show (Weierstrass curve point)
instance
  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point field)))
  , CyclicGroup (Weierstrass curve (Point field))
  ) => Arbitrary (Weierstrass curve (Point field)) where
    arbitrary :: Gen (Weierstrass curve (Point field))
arbitrary = do
      ScalarFieldOf (Weierstrass curve (Point field))
c <- forall a. Arbitrary a => Gen a
arbitrary @(ScalarFieldOf (Weierstrass curve (Point field)))
      Weierstrass curve (Point field)
-> Gen (Weierstrass curve (Point field))
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Weierstrass curve (Point field)
 -> Gen (Weierstrass curve (Point field)))
-> Weierstrass curve (Point field)
-> Gen (Weierstrass curve (Point field))
forall a b. (a -> b) -> a -> b
$ ScalarFieldOf (Weierstrass curve (Point field))
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
forall b a. Scale b a => b -> a -> a
scale ScalarFieldOf (Weierstrass curve (Point field))
c Weierstrass curve (Point field)
forall g. CyclicGroup g => g
pointGen
instance
  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point field)))
  , CyclicGroup (Weierstrass curve (Point field))
  , Compressible (Weierstrass curve (Point field))
  , Compressed (Weierstrass curve (Point field))
    ~ Weierstrass curve (CompressedPoint field)
  ) => Arbitrary (Weierstrass curve (CompressedPoint field)) where
    arbitrary :: Gen (Weierstrass curve (CompressedPoint field))
arbitrary = do
      Weierstrass curve (Point field)
c <- forall a. Arbitrary a => Gen a
arbitrary @(Weierstrass curve (Point field))
      Weierstrass curve (CompressedPoint field)
-> Gen (Weierstrass curve (CompressedPoint field))
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Weierstrass curve (CompressedPoint field)
 -> Gen (Weierstrass curve (CompressedPoint field)))
-> Weierstrass curve (CompressedPoint field)
-> Gen (Weierstrass curve (CompressedPoint field))
forall a b. (a -> b) -> a -> b
$ Weierstrass curve (Point field)
-> Compressed (Weierstrass curve (Point field))
forall point. Compressible point => point -> Compressed point
compress Weierstrass curve (Point field)
c
instance
  ( WeierstrassCurve curve field
  , Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => EllipticCurve (Weierstrass curve (Point field)) where
    type CurveOf (Weierstrass curve (Point field)) = curve
    type BaseFieldOf (Weierstrass curve (Point field)) = field
    isOnCurve :: Weierstrass curve (Point field)
-> BooleanOf (BaseFieldOf (Weierstrass curve (Point field)))
isOnCurve (Weierstrass (Point field
x field
y BooleanOf field
isInf)) =
      if BooleanOf field
isInf then field
x field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
forall a. AdditiveMonoid a => a
zero else
      let b :: field
b = forall (curve :: Symbol) field.
WeierstrassCurve curve field =>
field
weierstrassB @curve in field
yfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
y field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
xfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
xfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
x field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
b
deriving newtype instance
  ( SymbolicEq field
  ) => SymbolicData (Weierstrass curve (Point field))
instance
  ( WeierstrassCurve curve field
  , SymbolicEq field
  ) => SymbolicInput (Weierstrass curve (Point field)) where
    isValid :: Weierstrass curve (Point field)
-> Bool (Context (Weierstrass curve (Point field)))
isValid = Weierstrass curve (Point field)
-> Bool (Context (Weierstrass curve (Point field)))
Weierstrass curve (Point field)
-> BooleanOf (BaseFieldOf (Weierstrass curve (Point field)))
forall point.
EllipticCurve point =>
point -> BooleanOf (BaseFieldOf point)
isOnCurve
deriving newtype instance Conditional bool point
  => Conditional bool (Weierstrass curve point)
deriving newtype instance Eq point
  => Eq (Weierstrass curve point)
deriving newtype instance HasPointInf point
  => HasPointInf (Weierstrass curve point)
deriving newtype instance Planar field point
  => Planar field (Weierstrass curve point)
instance
  ( Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => AdditiveSemigroup (Weierstrass curve (Point field)) where
    pt0 :: Weierstrass curve (Point field)
pt0@(Weierstrass (Point field
x0 field
y0 BooleanOf field
isInf0)) + :: Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
+ pt1 :: Weierstrass curve (Point field)
pt1@(Weierstrass (Point field
x1 field
y1 BooleanOf field
isInf1)) =
      if BooleanOf field
isInf0 then Weierstrass curve (Point field)
pt1 else if BooleanOf field
isInf1 then Weierstrass curve (Point field)
pt0 -- additive identity
      else if field
x0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
x1 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& field
y0 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
y1 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
forall a. AdditiveMonoid a => a
zero then Weierstrass curve (Point field)
forall point. HasPointInf point => point
pointInf -- additive inverse
      else let slope :: field
slope = if field
x0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
x1 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& field
y0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
y1
                       then (field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0) field -> field -> field
forall a. Field a => a -> a -> a
// (field
y0 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
y0) -- tangent
                       else (field
y1 field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
y0) field -> field -> field
forall a. Field a => a -> a -> a
// (field
x1 field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
x0) -- secant
               x2 :: field
x2 = field
slope field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
slope field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
x0 field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
x1
               y2 :: field
y2 = field
slope field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* (field
x0 field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
x2) field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
y0
            in field -> field -> Weierstrass curve (Point field)
forall field point. Planar field point => field -> field -> point
pointXY field
x2 field
y2
instance
  ( WeierstrassCurve curve field
  , Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => AdditiveMonoid (Weierstrass curve (Point field)) where
    zero :: Weierstrass curve (Point field)
zero = Weierstrass curve (Point field)
forall point. HasPointInf point => point
pointInf
instance
  ( WeierstrassCurve curve field
  , Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => AdditiveGroup (Weierstrass curve (Point field)) where
    negate :: Weierstrass curve (Point field) -> Weierstrass curve (Point field)
negate pt :: Weierstrass curve (Point field)
pt@(Weierstrass (Point field
x field
y BooleanOf field
isInf)) =
      if BooleanOf field
isInf then Weierstrass curve (Point field)
pt else field -> field -> Weierstrass curve (Point field)
forall field point. Planar field point => field -> field -> point
pointXY field
x (field -> field
forall a. AdditiveGroup a => a -> a
negate field
y)
instance
  ( WeierstrassCurve curve field
  , Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => Scale Natural (Weierstrass curve (Point field)) where
  scale :: Natural
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
scale = Natural
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
forall a. AdditiveMonoid a => Natural -> a -> a
natScale
instance
  ( WeierstrassCurve curve field
  , Conditional (BooleanOf field) (BooleanOf field)
  , Conditional (BooleanOf field) field
  , Eq field
  , Field field
  ) => Scale Integer (Weierstrass curve (Point field)) where
  scale :: Integer
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
scale = Integer
-> Weierstrass curve (Point field)
-> Weierstrass curve (Point field)
forall a. AdditiveGroup a => Integer -> a -> a
intScale

{- | `TwistedEdwards` tags a `Planar` @point@, over a `Field` @field@,
with a phantom `TwistedEdwardsCurve` @curve@. -}
newtype TwistedEdwards curve point = TwistedEdwards {forall {k} (curve :: k) point. TwistedEdwards curve point -> point
pointTwistedEdwards :: point}
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  , Eq field
  ) => EllipticCurve (TwistedEdwards curve (AffinePoint field)) where
    type CurveOf (TwistedEdwards curve (AffinePoint field)) = curve
    type BaseFieldOf (TwistedEdwards curve (AffinePoint field)) = field
    isOnCurve :: TwistedEdwards curve (AffinePoint field)
-> BooleanOf
     (BaseFieldOf (TwistedEdwards curve (AffinePoint field)))
isOnCurve (TwistedEdwards (AffinePoint field
x field
y)) =
      let a :: field
a = forall (curve :: Symbol) field.
TwistedEdwardsCurve curve field =>
field
twistedEdwardsA @curve
          d :: field
d = forall (curve :: Symbol) field.
TwistedEdwardsCurve curve field =>
field
twistedEdwardsD @curve
      in field
afield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
xfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
x field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
yfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
y field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
forall a. MultiplicativeMonoid a => a
one field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
dfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
xfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
xfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
yfield -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
y
deriving newtype instance Prelude.Eq point
  => Prelude.Eq (TwistedEdwards curve point)
deriving newtype instance Prelude.Show point
  => Prelude.Show (TwistedEdwards curve point)
deriving newtype instance SymbolicOutput field
  => SymbolicData (TwistedEdwards curve (AffinePoint field))
instance
  ( Context field ~ ctx
  , Symbolic ctx
  , TwistedEdwardsCurve curve field
  , SymbolicEq field
  ) => SymbolicInput (TwistedEdwards curve (AffinePoint field)) where
    isValid :: TwistedEdwards curve (AffinePoint field)
-> Bool (Context (TwistedEdwards curve (AffinePoint field)))
isValid = TwistedEdwards curve (AffinePoint field)
-> Bool (Context (TwistedEdwards curve (AffinePoint field)))
TwistedEdwards curve (AffinePoint field)
-> BooleanOf
     (BaseFieldOf (TwistedEdwards curve (AffinePoint field)))
forall point.
EllipticCurve point =>
point -> BooleanOf (BaseFieldOf point)
isOnCurve
deriving newtype instance Conditional bool point
  => Conditional bool (TwistedEdwards curve point)
deriving newtype instance Eq point
  => Eq (TwistedEdwards curve point)
deriving newtype instance HasPointInf point
  => HasPointInf (TwistedEdwards curve point)
deriving newtype instance Planar field point
  => Planar field (TwistedEdwards curve point)
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  ) => AdditiveSemigroup (TwistedEdwards curve (AffinePoint field)) where
    TwistedEdwards (AffinePoint field
x0 field
y0) + :: TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
+ TwistedEdwards (AffinePoint field
x1 field
y1) =
      let a :: field
a = forall (curve :: Symbol) field.
TwistedEdwardsCurve curve field =>
field
twistedEdwardsA @curve
          d :: field
d = forall (curve :: Symbol) field.
TwistedEdwardsCurve curve field =>
field
twistedEdwardsD @curve
          x2 :: field
x2 = (field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y1 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
y0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x1) field -> field -> field
forall a. Field a => a -> a -> a
// (field
forall a. MultiplicativeMonoid a => a
one field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
d field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x1 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y1)
          y2 :: field
y2 = (field
y0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y1 field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
a field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x1) field -> field -> field
forall a. Field a => a -> a -> a
// (field
forall a. MultiplicativeMonoid a => a
one field -> field -> field
forall a. AdditiveGroup a => a -> a -> a
- field
d field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
x1 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y0 field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
* field
y1)
      in field -> field -> TwistedEdwards curve (AffinePoint field)
forall field point. Planar field point => field -> field -> point
pointXY field
x2 field
y2
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  ) => AdditiveMonoid (TwistedEdwards curve (AffinePoint field)) where
    zero :: TwistedEdwards curve (AffinePoint field)
zero = field -> field -> TwistedEdwards curve (AffinePoint field)
forall field point. Planar field point => field -> field -> point
pointXY field
forall a. AdditiveMonoid a => a
zero field
forall a. MultiplicativeMonoid a => a
one
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  ) => AdditiveGroup (TwistedEdwards curve (AffinePoint field)) where
    negate :: TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
negate (TwistedEdwards (AffinePoint field
x field
y)) = field -> field -> TwistedEdwards curve (AffinePoint field)
forall field point. Planar field point => field -> field -> point
pointXY (field -> field
forall a. AdditiveGroup a => a -> a
negate field
x) field
y
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  ) => Scale Natural (TwistedEdwards curve (AffinePoint field)) where
  scale :: Natural
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
scale = Natural
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
forall a. AdditiveMonoid a => Natural -> a -> a
natScale
instance
  ( TwistedEdwardsCurve curve field
  , Field field
  ) => Scale Integer (TwistedEdwards curve (AffinePoint field)) where
  scale :: Integer
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
scale = Integer
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
forall a. AdditiveGroup a => Integer -> a -> a
intScale
instance
  ( Arbitrary (ScalarFieldOf (TwistedEdwards curve (AffinePoint field)))
  , CyclicGroup (TwistedEdwards curve (AffinePoint field))
  ) => Arbitrary (TwistedEdwards curve (AffinePoint field)) where
    arbitrary :: Gen (TwistedEdwards curve (AffinePoint field))
arbitrary = do
      ScalarFieldOf (TwistedEdwards curve (AffinePoint field))
c <- forall a. Arbitrary a => Gen a
arbitrary @(ScalarFieldOf (TwistedEdwards curve (AffinePoint field)))
      TwistedEdwards curve (AffinePoint field)
-> Gen (TwistedEdwards curve (AffinePoint field))
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (TwistedEdwards curve (AffinePoint field)
 -> Gen (TwistedEdwards curve (AffinePoint field)))
-> TwistedEdwards curve (AffinePoint field)
-> Gen (TwistedEdwards curve (AffinePoint field))
forall a b. (a -> b) -> a -> b
$ ScalarFieldOf (TwistedEdwards curve (AffinePoint field))
-> TwistedEdwards curve (AffinePoint field)
-> TwistedEdwards curve (AffinePoint field)
forall b a. Scale b a => b -> a -> a
scale ScalarFieldOf (TwistedEdwards curve (AffinePoint field))
c TwistedEdwards curve (AffinePoint field)
forall g. CyclicGroup g => g
pointGen

{- | A type of points in the projective plane. -}
data Point field = Point
  { forall field. Point field -> field
_x    :: field
  , forall field. Point field -> field
_y    :: field
  , forall field. Point field -> BooleanOf field
_zBit :: BooleanOf field
  } deriving ((forall x. Point field -> Rep (Point field) x)
-> (forall x. Rep (Point field) x -> Point field)
-> Generic (Point field)
forall x. Rep (Point field) x -> Point field
forall x. Point field -> Rep (Point field) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall field x. Rep (Point field) x -> Point field
forall field x. Point field -> Rep (Point field) x
$cfrom :: forall field x. Point field -> Rep (Point field) x
from :: forall x. Point field -> Rep (Point field) x
$cto :: forall field x. Rep (Point field) x -> Point field
to :: forall x. Rep (Point field) x -> Point field
Generic)
deriving instance (Prelude.Eq (BooleanOf field), Prelude.Eq field)
  => Prelude.Eq (Point field)
instance
  ( SymbolicOutput (BooleanOf field)
  , SymbolicOutput field
  , Context field ~ Context (BooleanOf field)
  ) => SymbolicData (Point field)
instance Eq field => Planar field (Point field) where
  pointXY :: field -> field -> Point field
pointXY field
x field
y = field -> field -> BooleanOf field -> Point field
forall field. field -> field -> BooleanOf field -> Point field
Point field
x field
y BooleanOf field
forall b. BoolType b => b
false
instance (Semiring field, Eq field) => HasPointInf (Point field) where
  pointInf :: Point field
pointInf = field -> field -> BooleanOf field -> Point field
forall field. field -> field -> BooleanOf field -> Point field
Point field
forall a. AdditiveMonoid a => a
zero field
forall a. MultiplicativeMonoid a => a
one BooleanOf field
forall b. BoolType b => b
true
instance (Prelude.Show field, BooleanOf field ~ Prelude.Bool)
  => Prelude.Show (Point field) where
  show :: Point field -> String
show (Point field
x field
y BooleanOf field
isInf) =
    if Bool
BooleanOf field
isInf then String
"pointInf" else [String] -> String
forall a. Monoid a => [a] -> a
Prelude.mconcat
      [String
"(", field -> String
forall a. Show a => a -> String
Prelude.show field
x, String
", ", field -> String
forall a. Show a => a -> String
Prelude.show field
y, String
")"]
instance
  ( Conditional bool bool
  , Conditional bool field
  , bool ~ BooleanOf field
  ) => Conditional bool (Point field)
instance
  ( BooleanOf (BooleanOf field) ~ BooleanOf field
  , Eq (BooleanOf field)
  , Eq field
  , Field field
  ) => Eq (Point field) where
    Point field
x0 field
y0 BooleanOf field
isInf0 == :: Point field -> Point field -> BooleanOf (Point field)
== Point field
x1 field
y1 BooleanOf field
isInf1 =
      if BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b
not BooleanOf field
isInf0 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b
not BooleanOf field
isInf1
      then field
x0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
x1 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& field
y0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
y1
      else BooleanOf field
isInf0 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& BooleanOf field
isInf1 BooleanOf field -> BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b -> b
&& field
x1field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
y0 field -> field -> BooleanOf field
forall a. Eq a => a -> a -> BooleanOf a
== field
x0field -> field -> field
forall a. MultiplicativeSemigroup a => a -> a -> a
*field
y1 -- same slope y0//x0 = y1//x1
    Point field
pt0 /= :: Point field -> Point field -> BooleanOf (Point field)
/= Point field
pt1 = BooleanOf field -> BooleanOf field
forall b. BoolType b => b -> b
not (Point field
pt0 Point field -> Point field -> BooleanOf (Point field)
forall a. Eq a => a -> a -> BooleanOf a
== Point field
pt1)

data CompressedPoint field = CompressedPoint
  { forall field. CompressedPoint field -> field
_x    :: field
  , forall field. CompressedPoint field -> BooleanOf field
_yBit :: BooleanOf field
  , forall field. CompressedPoint field -> BooleanOf field
_zBit :: BooleanOf field
  } deriving (forall x. CompressedPoint field -> Rep (CompressedPoint field) x)
-> (forall x.
    Rep (CompressedPoint field) x -> CompressedPoint field)
-> Generic (CompressedPoint field)
forall x. Rep (CompressedPoint field) x -> CompressedPoint field
forall x. CompressedPoint field -> Rep (CompressedPoint field) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall field x.
Rep (CompressedPoint field) x -> CompressedPoint field
forall field x.
CompressedPoint field -> Rep (CompressedPoint field) x
$cfrom :: forall field x.
CompressedPoint field -> Rep (CompressedPoint field) x
from :: forall x. CompressedPoint field -> Rep (CompressedPoint field) x
$cto :: forall field x.
Rep (CompressedPoint field) x -> CompressedPoint field
to :: forall x. Rep (CompressedPoint field) x -> CompressedPoint field
Generic
deriving instance (Prelude.Show (BooleanOf field), Prelude.Show field)
  => Prelude.Show (CompressedPoint field)
deriving instance (Prelude.Eq (BooleanOf field), Prelude.Eq field)
  => Prelude.Eq (CompressedPoint field)
instance
  ( SymbolicOutput (BooleanOf field)
  , SymbolicOutput field
  , Context field ~ Context (BooleanOf field)
  ) => SymbolicData (CompressedPoint field)
instance (BoolType (BooleanOf field), AdditiveMonoid field)
  => HasPointInf (CompressedPoint field) where
    pointInf :: CompressedPoint field
pointInf = field
-> BooleanOf field -> BooleanOf field -> CompressedPoint field
forall field.
field
-> BooleanOf field -> BooleanOf field -> CompressedPoint field
CompressedPoint field
forall a. AdditiveMonoid a => a
zero BooleanOf field
forall b. BoolType b => b
true BooleanOf field
forall b. BoolType b => b
true

data AffinePoint field = AffinePoint
  { forall field. AffinePoint field -> field
_x :: field
  , forall field. AffinePoint field -> field
_y :: field
  } deriving ((forall x. AffinePoint field -> Rep (AffinePoint field) x)
-> (forall x. Rep (AffinePoint field) x -> AffinePoint field)
-> Generic (AffinePoint field)
forall x. Rep (AffinePoint field) x -> AffinePoint field
forall x. AffinePoint field -> Rep (AffinePoint field) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall field x. Rep (AffinePoint field) x -> AffinePoint field
forall field x. AffinePoint field -> Rep (AffinePoint field) x
$cfrom :: forall field x. AffinePoint field -> Rep (AffinePoint field) x
from :: forall x. AffinePoint field -> Rep (AffinePoint field) x
$cto :: forall field x. Rep (AffinePoint field) x -> AffinePoint field
to :: forall x. Rep (AffinePoint field) x -> AffinePoint field
Generic, AffinePoint field -> AffinePoint field -> Bool
(AffinePoint field -> AffinePoint field -> Bool)
-> (AffinePoint field -> AffinePoint field -> Bool)
-> Eq (AffinePoint field)
forall field.
Eq field =>
AffinePoint field -> AffinePoint field -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall field.
Eq field =>
AffinePoint field -> AffinePoint field -> Bool
== :: AffinePoint field -> AffinePoint field -> Bool
$c/= :: forall field.
Eq field =>
AffinePoint field -> AffinePoint field -> Bool
/= :: AffinePoint field -> AffinePoint field -> Bool
Prelude.Eq)
instance SymbolicOutput field => SymbolicData (AffinePoint field)
instance Planar field (AffinePoint field) where pointXY :: field -> field -> AffinePoint field
pointXY = field -> field -> AffinePoint field
forall field. field -> field -> AffinePoint field
AffinePoint
instance Conditional bool field => Conditional bool (AffinePoint field)
instance
  ( Eq field
  , Field field
  ) => Eq (AffinePoint field)
instance Prelude.Show field => Prelude.Show (AffinePoint field) where
  show :: AffinePoint field -> String
show (AffinePoint field
x field
y) = [String] -> String
forall a. Monoid a => [a] -> a
Prelude.mconcat
    [String
"(", field -> String
forall a. Show a => a -> String
Prelude.show field
x, String
", ", field -> String
forall a. Show a => a -> String
Prelude.show field
y, String
")"]