{-# 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 (..)
  , 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 bool (BaseFieldOf point)
  , Planar (BaseFieldOf point) point
  , AdditiveGroup point
  ) => EllipticCurve bool 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 -> bool

{- | 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

{- | 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 Compressible bool point where
  type Compressed point :: Type
  pointCompressed :: BaseFieldOf point -> bool -> 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 Prelude.Bool field)))
  , CyclicGroup (Weierstrass curve (Point Prelude.Bool field))
  ) => Arbitrary (Weierstrass curve (Point Prelude.Bool field)) where
    arbitrary :: Gen (Weierstrass curve (Point Bool field))
arbitrary = do
      ScalarFieldOf (Weierstrass curve (Point Bool field))
c <- forall a. Arbitrary a => Gen a
arbitrary @(ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
      Weierstrass curve (Point Bool field)
-> Gen (Weierstrass curve (Point Bool field))
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Weierstrass curve (Point Bool field)
 -> Gen (Weierstrass curve (Point Bool field)))
-> Weierstrass curve (Point Bool field)
-> Gen (Weierstrass curve (Point Bool field))
forall a b. (a -> b) -> a -> b
$ ScalarFieldOf (Weierstrass curve (Point Bool field))
-> Weierstrass curve (Point Bool field)
-> Weierstrass curve (Point Bool field)
forall b a. Scale b a => b -> a -> a
scale ScalarFieldOf (Weierstrass curve (Point Bool field))
c Weierstrass curve (Point Bool field)
forall g. CyclicGroup g => g
pointGen
instance
  ( Arbitrary (ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
  , CyclicGroup (Weierstrass curve (Point Prelude.Bool field))
  , Compressible Prelude.Bool (Weierstrass curve (Point Prelude.Bool field))
  , Compressed (Weierstrass curve (Point Prelude.Bool field)) ~ Weierstrass curve (CompressedPoint Prelude.Bool field)
  ) => Arbitrary (Weierstrass curve (CompressedPoint Prelude.Bool field)) where
    arbitrary :: Gen (Weierstrass curve (CompressedPoint Bool field))
arbitrary = do
      ScalarFieldOf (Weierstrass curve (Point Bool field))
c <- forall a. Arbitrary a => Gen a
arbitrary @(ScalarFieldOf (Weierstrass curve (Point Prelude.Bool field)))
      Weierstrass curve (CompressedPoint Bool field)
-> Gen (Weierstrass curve (CompressedPoint Bool field))
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (Weierstrass curve (CompressedPoint Bool field)
 -> Gen (Weierstrass curve (CompressedPoint Bool field)))
-> Weierstrass curve (CompressedPoint Bool field)
-> Gen (Weierstrass curve (CompressedPoint Bool field))
forall a b. (a -> b) -> a -> b
$ forall bool point.
Compressible bool point =>
point -> Compressed point
compress @Prelude.Bool (ScalarFieldOf (Weierstrass curve (Point Bool field))
-> Weierstrass curve (Point Bool field)
-> Weierstrass curve (Point Bool field)
forall b a. Scale b a => b -> a -> a
scale ScalarFieldOf (Weierstrass curve (Point Bool field))
c (forall g. CyclicGroup g => g
pointGen @(Weierstrass curve (Point Prelude.Bool field))))
instance
  ( WeierstrassCurve curve field
  , Conditional bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => EllipticCurve bool (Weierstrass curve (Point bool field)) where
    type CurveOf (Weierstrass curve (Point bool field)) = curve
    type BaseFieldOf (Weierstrass curve (Point bool field)) = field
    isOnCurve :: Weierstrass curve (Point bool field) -> bool
isOnCurve (Weierstrass (Point field
x field
y bool
isInf)) =
      if bool
isInf then field
x field -> field -> bool
forall b a. Eq b a => a -> a -> b
== 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 -> bool
forall b a. Eq b a => a -> a -> b
== 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
  ( SymbolicOutput bool
  , SymbolicOutput field
  , Context field ~ Context bool
  ) => SymbolicData (Weierstrass curve (Point bool field))
instance
  ( SymbolicInput field
  , Context field ~ ctx
  , Symbolic ctx
  , WeierstrassCurve curve field
  , Eq (Bool ctx) field
  , Conditional (Bool ctx) field
  ) => SymbolicInput (Weierstrass curve (Point (Bool ctx) field)) where
    isValid :: Weierstrass curve (Point (Bool ctx) field)
-> Bool (Context (Weierstrass curve (Point (Bool ctx) field)))
isValid = Weierstrass curve (Point (Bool ctx) field) -> Bool ctx
Weierstrass curve (Point (Bool ctx) field)
-> Bool (Context (Weierstrass curve (Point (Bool ctx) field)))
forall bool point. EllipticCurve bool point => point -> bool
isOnCurve
deriving newtype instance Conditional bool point
  => Conditional bool (Weierstrass curve point)
deriving newtype instance Eq bool point
  => Eq bool (Weierstrass curve point)
deriving newtype instance HasPointInf point
  => HasPointInf (Weierstrass curve point)
deriving newtype instance Planar field point
  => Planar field (Weierstrass curve point)
instance
  ( WeierstrassCurve curve field
  , Conditional bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => AdditiveSemigroup (Weierstrass curve (Point bool field)) where
    pt0 :: Weierstrass curve (Point bool field)
pt0@(Weierstrass (Point field
x0 field
y0 bool
isInf0)) + :: Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
+ pt1 :: Weierstrass curve (Point bool field)
pt1@(Weierstrass (Point field
x1 field
y1 bool
isInf1)) =
      if bool
isInf0 then Weierstrass curve (Point bool field)
pt1 else if bool
isInf1 then Weierstrass curve (Point bool field)
pt0 -- additive identity
      else if field
x0 field -> field -> bool
forall b a. Eq b a => a -> a -> b
== field
x1 bool -> bool -> bool
forall b. BoolType b => b -> b -> b
&& field
y0 field -> field -> field
forall a. AdditiveSemigroup a => a -> a -> a
+ field
y1 field -> field -> bool
forall b a. Eq b a => a -> a -> b
== field
forall a. AdditiveMonoid a => a
zero :: bool then Weierstrass curve (Point bool field)
forall point. HasPointInf point => point
pointInf -- additive inverse
      else let slope :: field
slope = if field
x0 field -> field -> bool
forall b a. Eq b a => a -> a -> b
== field
x1 bool -> bool -> bool
forall b. BoolType b => b -> b -> b
&& field
y0 field -> field -> bool
forall b a. Eq b a => a -> a -> b
== field
y1 :: bool
                       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 bool field)
forall field point. Planar field point => field -> field -> point
pointXY field
x2 field
y2
instance
  ( WeierstrassCurve curve field
  , Conditional bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => AdditiveMonoid (Weierstrass curve (Point bool field)) where
    zero :: Weierstrass curve (Point bool field)
zero = Weierstrass curve (Point bool field)
forall point. HasPointInf point => point
pointInf
instance
  ( WeierstrassCurve curve field
  , Conditional bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => AdditiveGroup (Weierstrass curve (Point bool field)) where
    negate :: Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
negate pt :: Weierstrass curve (Point bool field)
pt@(Weierstrass (Point field
x field
y bool
isInf)) =
      if bool
isInf then Weierstrass curve (Point bool field)
pt else field -> field -> Weierstrass curve (Point bool 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 bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => Scale Natural (Weierstrass curve (Point bool field)) where
  scale :: Natural
-> Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
scale = Natural
-> Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
forall a. AdditiveMonoid a => Natural -> a -> a
natScale
instance
  ( WeierstrassCurve curve field
  , Conditional bool bool
  , Conditional bool field
  , Eq bool field
  , Field field
  ) => Scale Integer (Weierstrass curve (Point bool field)) where
  scale :: Integer
-> Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool field)
scale = Integer
-> Weierstrass curve (Point bool field)
-> Weierstrass curve (Point bool 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 bool field
  ) => EllipticCurve bool (TwistedEdwards curve (AffinePoint field)) where
    type CurveOf (TwistedEdwards curve (AffinePoint field)) = curve
    type BaseFieldOf (TwistedEdwards curve (AffinePoint field)) = field
    isOnCurve :: TwistedEdwards curve (AffinePoint field) -> bool
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 -> bool
forall b a. Eq b a => a -> a -> b
== 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 SymbolicOutput field
  => SymbolicData (TwistedEdwards curve (AffinePoint field))
instance
  ( SymbolicInput field
  , Context field ~ ctx
  , Symbolic ctx
  , TwistedEdwardsCurve curve field
  , Eq (Bool ctx) field
  , Conditional (Bool ctx) field
  ) => SymbolicInput (TwistedEdwards curve (AffinePoint field)) where
    isValid :: TwistedEdwards curve (AffinePoint field)
-> Bool (Context (TwistedEdwards curve (AffinePoint field)))
isValid = TwistedEdwards curve (AffinePoint field) -> Bool ctx
TwistedEdwards curve (AffinePoint field)
-> Bool (Context (TwistedEdwards curve (AffinePoint field)))
forall bool point. EllipticCurve bool point => point -> bool
isOnCurve
deriving newtype instance Conditional bool point
  => Conditional bool (TwistedEdwards curve point)
deriving newtype instance Eq bool point
  => Eq bool (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

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

data CompressedPoint bool field = CompressedPoint
  { forall bool field. CompressedPoint bool field -> field
_x    :: field
  , forall bool field. CompressedPoint bool field -> bool
_yBit :: bool
  , forall bool field. CompressedPoint bool field -> bool
_zBit :: bool
  } deriving ((forall x.
 CompressedPoint bool field -> Rep (CompressedPoint bool field) x)
-> (forall x.
    Rep (CompressedPoint bool field) x -> CompressedPoint bool field)
-> Generic (CompressedPoint bool field)
forall x.
Rep (CompressedPoint bool field) x -> CompressedPoint bool field
forall x.
CompressedPoint bool field -> Rep (CompressedPoint bool field) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall bool field x.
Rep (CompressedPoint bool field) x -> CompressedPoint bool field
forall bool field x.
CompressedPoint bool field -> Rep (CompressedPoint bool field) x
$cfrom :: forall bool field x.
CompressedPoint bool field -> Rep (CompressedPoint bool field) x
from :: forall x.
CompressedPoint bool field -> Rep (CompressedPoint bool field) x
$cto :: forall bool field x.
Rep (CompressedPoint bool field) x -> CompressedPoint bool field
to :: forall x.
Rep (CompressedPoint bool field) x -> CompressedPoint bool field
Generic, Int -> CompressedPoint bool field -> ShowS
[CompressedPoint bool field] -> ShowS
CompressedPoint bool field -> String
(Int -> CompressedPoint bool field -> ShowS)
-> (CompressedPoint bool field -> String)
-> ([CompressedPoint bool field] -> ShowS)
-> Show (CompressedPoint bool field)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall bool field.
(Show field, Show bool) =>
Int -> CompressedPoint bool field -> ShowS
forall bool field.
(Show field, Show bool) =>
[CompressedPoint bool field] -> ShowS
forall bool field.
(Show field, Show bool) =>
CompressedPoint bool field -> String
$cshowsPrec :: forall bool field.
(Show field, Show bool) =>
Int -> CompressedPoint bool field -> ShowS
showsPrec :: Int -> CompressedPoint bool field -> ShowS
$cshow :: forall bool field.
(Show field, Show bool) =>
CompressedPoint bool field -> String
show :: CompressedPoint bool field -> String
$cshowList :: forall bool field.
(Show field, Show bool) =>
[CompressedPoint bool field] -> ShowS
showList :: [CompressedPoint bool field] -> ShowS
Prelude.Show, CompressedPoint bool field -> CompressedPoint bool field -> Bool
(CompressedPoint bool field -> CompressedPoint bool field -> Bool)
-> (CompressedPoint bool field
    -> CompressedPoint bool field -> Bool)
-> Eq (CompressedPoint bool field)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall bool field.
(Eq field, Eq bool) =>
CompressedPoint bool field -> CompressedPoint bool field -> Bool
$c== :: forall bool field.
(Eq field, Eq bool) =>
CompressedPoint bool field -> CompressedPoint bool field -> Bool
== :: CompressedPoint bool field -> CompressedPoint bool field -> Bool
$c/= :: forall bool field.
(Eq field, Eq bool) =>
CompressedPoint bool field -> CompressedPoint bool field -> Bool
/= :: CompressedPoint bool field -> CompressedPoint bool field -> Bool
Prelude.Eq)
instance
  ( SymbolicOutput bool
  , SymbolicOutput field
  , Context field ~ Context bool
  ) => SymbolicData (CompressedPoint bool field)
instance (BoolType bool, AdditiveMonoid field)
  => HasPointInf (CompressedPoint bool field) where
    pointInf :: CompressedPoint bool field
pointInf = field -> bool -> bool -> CompressedPoint bool field
forall bool field.
field -> bool -> bool -> CompressedPoint bool field
CompressedPoint field
forall a. AdditiveMonoid a => a
zero bool
forall b. BoolType b => b
true bool
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
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
  ( BoolType bool
  , Eq bool field
  , Field field
  ) => Eq bool (AffinePoint field)