{-# LANGUAGE AllowAmbiguousTypes   #-}
{-# LANGUAGE DeriveAnyClass        #-}
{-# LANGUAGE DuplicateRecordFields #-}
{-# LANGUAGE RebindableSyntax      #-}
{-# LANGUAGE TypeOperators         #-}
{-# LANGUAGE UndecidableInstances  #-}

module ZkFold.Base.Algebra.EllipticCurve.Class where

import           Data.Functor                     ((<&>))
import           Data.Kind                        (Type)
import           Data.String                      (fromString)
import           GHC.Generics                     (Generic)
import           Prelude                          (Integer, Show (..), fromInteger, type (~), (++), (.), (<$>))
import qualified Prelude                          as P
import           Test.QuickCheck                  hiding (scale)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Symbolic.Class            (Symbolic)
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq
import           ZkFold.Symbolic.Data.Ord

data Point (curve :: Type) = Point
  { forall curve. Point curve -> BaseField curve
_x     :: BaseField curve
  , forall curve. Point curve -> BaseField curve
_y     :: BaseField curve
  , forall curve. Point curve -> BooleanOf curve
_isInf :: BooleanOf curve
  } deriving ((forall x. Point curve -> Rep (Point curve) x)
-> (forall x. Rep (Point curve) x -> Point curve)
-> Generic (Point curve)
forall x. Rep (Point curve) x -> Point curve
forall x. Point curve -> Rep (Point curve) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall curve x. Rep (Point curve) x -> Point curve
forall curve x. Point curve -> Rep (Point curve) x
$cfrom :: forall curve x. Point curve -> Rep (Point curve) x
from :: forall x. Point curve -> Rep (Point curve) x
$cto :: forall curve x. Rep (Point curve) x -> Point curve
to :: forall x. Rep (Point curve) x -> Point curve
Generic)

instance
  ( EllipticCurve curve
  , bool ~ BooleanOf curve
  ) => Conditional bool (Point curve)

instance
  ( EllipticCurve curve
  , bool ~ BooleanOf curve
  ) => Eq bool (Point curve)

instance
  ( EllipticCurve curve
  , BooleanOf curve ~ P.Bool
  ) => P.Eq (Point curve) where
  == :: Point curve -> Point curve -> Bool
(==) = Point curve -> Point curve -> Bool
forall b a. Eq b a => a -> a -> b
(==)
  /= :: Point curve -> Point curve -> Bool
(/=) = Point curve -> Point curve -> Bool
forall b a. Eq b a => a -> a -> b
(/=)

instance
  ( Symbolic ctx
  , SymbolicOutput bool
  , SymbolicOutput field
  , bool ~ BooleanOf curve
  , field ~ BaseField curve
  , Context bool ~ ctx
  , Context field ~ ctx
  ) => SymbolicData (Point curve)

class Planar field plane where
  pointXY :: field -> field -> plane

instance
  ( field ~ BaseField curve
  , bool ~ BooleanOf curve
  , BoolType bool
  ) => Planar field (Point curve) where
  pointXY :: field -> field -> Point curve
pointXY field
x field
y = BaseField curve
-> BaseField curve -> BooleanOf curve -> Point curve
forall curve.
BaseField curve
-> BaseField curve -> BooleanOf curve -> Point curve
Point field
BaseField curve
x field
BaseField curve
y bool
BooleanOf curve
forall b. BoolType b => b
false

class ProjectivePlanar plane where
  pointInf :: plane

instance
  ( field ~ BaseField curve
  , BoolType (BooleanOf curve)
  , AdditiveMonoid field
  ) => ProjectivePlanar (Point curve) where
  pointInf :: Point curve
pointInf = BaseField curve
-> BaseField curve -> BooleanOf curve -> Point curve
forall curve.
BaseField curve
-> BaseField curve -> BooleanOf curve -> Point curve
Point field
BaseField curve
forall a. AdditiveMonoid a => a
zero field
BaseField curve
forall a. AdditiveMonoid a => a
zero BooleanOf curve
forall b. BoolType b => b
true

instance
  ( field ~ BaseField curve
  , BoolType (BooleanOf curve)
  , AdditiveMonoid field
  ) => ProjectivePlanar (CompressedPoint curve) where
  pointInf :: CompressedPoint curve
pointInf = BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
forall curve.
BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
CompressedPoint field
BaseField curve
forall a. AdditiveMonoid a => a
zero BooleanOf curve
forall b. BoolType b => b
false BooleanOf curve
forall b. BoolType b => b
true

class
    ( BoolType (BooleanOf curve)
    , AdditiveMonoid (BaseField curve)
    , Conditional (BooleanOf curve) (BaseField curve)
    , Conditional (BooleanOf curve) (BooleanOf curve)
    , Eq (BooleanOf curve) (BaseField curve)
    , Eq (BooleanOf curve) (BooleanOf curve)
    ) => EllipticCurve curve where

    type BaseField curve :: Type
    type ScalarField curve :: Type
    type BooleanOf curve :: Type
    type BooleanOf curve = P.Bool

    pointGen :: Point curve

    add :: Point curve -> Point curve -> Point curve

    mul :: ScalarField curve -> Point curve -> Point curve

instance
  ( EllipticCurve curve
  , Show (BaseField curve)
  , Conditional (BooleanOf curve) P.String
  ) => Show (Point curve) where
    show :: Point curve -> String
show (Point BaseField curve
x BaseField curve
y BooleanOf curve
isInf) = if BooleanOf curve
isInf then String
"Inf" else String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseField curve -> String
forall a. Show a => a -> String
show BaseField curve
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseField curve -> String
forall a. Show a => a -> String
show BaseField curve
y String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance EllipticCurve curve => AdditiveSemigroup (Point curve) where
    + :: Point curve -> Point curve -> Point curve
(+) = Point curve -> Point curve -> Point curve
forall curve.
EllipticCurve curve =>
Point curve -> Point curve -> Point curve
add

instance {-# OVERLAPPABLE #-}
    ( EllipticCurve curve
    , BooleanOf curve ~ P.Bool
    , P.Eq s
    , BinaryExpansion s
    , Bits s ~ [s]
    ) => Scale s (Point curve) where
    scale :: s -> Point curve -> Point curve
scale = s -> Point curve -> Point curve
forall curve s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul

instance EllipticCurve curve => Scale Natural (Point curve) where
    scale :: Natural -> Point curve -> Point curve
scale = Natural -> Point curve -> Point curve
forall a. AdditiveMonoid a => Natural -> a -> a
natScale

instance EllipticCurve curve => AdditiveMonoid (Point curve) where
    zero :: Point curve
zero = Point curve
forall plane. ProjectivePlanar plane => plane
pointInf

instance (EllipticCurve curve, AdditiveGroup (BaseField curve)) => Scale Integer (Point curve) where
    scale :: Integer -> Point curve -> Point curve
scale = Integer -> Point curve -> Point curve
forall a. AdditiveGroup a => Integer -> a -> a
intScale

instance (EllipticCurve curve, AdditiveGroup (BaseField curve)) => AdditiveGroup (Point curve) where
    negate :: Point curve -> Point curve
negate = Point curve -> Point curve
forall curve.
(EllipticCurve curve, AdditiveGroup (BaseField curve)) =>
Point curve -> Point curve
pointNegate

instance (EllipticCurve curve, Arbitrary (ScalarField curve)) => Arbitrary (Point curve) where
    arbitrary :: Gen (Point curve)
arbitrary = Gen (ScalarField curve)
forall a. Arbitrary a => Gen a
arbitrary Gen (ScalarField curve)
-> (ScalarField curve -> Point curve) -> Gen (Point curve)
forall (f :: Type -> Type) a b. Functor f => f a -> (a -> b) -> f b
<&> (ScalarField curve -> Point curve -> Point curve
forall curve.
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point curve
forall curve. EllipticCurve curve => Point curve
pointGen)

class (EllipticCurve curve1, EllipticCurve curve2, ScalarField curve1 ~ ScalarField curve2,
        P.Eq (TargetGroup curve1 curve2), MultiplicativeGroup (TargetGroup curve1 curve2),
        Exponent (TargetGroup curve1 curve2) (ScalarField curve1)) => Pairing curve1 curve2 where
    type TargetGroup curve1 curve2 :: Type
    pairing :: Point curve1 -> Point curve2 -> TargetGroup curve1 curve2

pointAdd
    :: EllipticCurve curve
    => Field (BaseField curve)
    => Point curve
    -> Point curve
    -> Point curve
pointAdd :: forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve -> Point curve
pointAdd p :: Point curve
p@(Point BaseField curve
x1 BaseField curve
y1 BooleanOf curve
isInf1) q :: Point curve
q@(Point BaseField curve
x2 BaseField curve
y2 BooleanOf curve
isInf2) =
  if BooleanOf curve
isInf2 then Point curve
p
  else if BooleanOf curve
isInf1 then Point curve
q
  else if BaseField curve
x1 BaseField curve -> BaseField curve -> BooleanOf curve
forall b a. Eq b a => a -> a -> b
== BaseField curve
x2 then Point curve
forall plane. ProjectivePlanar plane => plane
pointInf
  else BaseField curve -> BaseField curve -> Point curve
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField curve
x3 BaseField curve
y3
  where
    slope :: BaseField curve
slope  = (BaseField curve
y1 BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
y2) BaseField curve -> BaseField curve -> BaseField curve
forall a. Field a => a -> a -> a
// (BaseField curve
x1 BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x2)
    x3 :: BaseField curve
x3 = BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x1 BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x2
    y3 :: BaseField curve
y3 = BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField curve
x1 BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x3) BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
y1

pointDouble
    :: EllipticCurve curve
    => Field (BaseField curve)
    => Point curve -> Point curve
pointDouble :: forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve
pointDouble (Point BaseField curve
x BaseField curve
y BooleanOf curve
isInf) = if BooleanOf curve
isInf then Point curve
forall plane. ProjectivePlanar plane => plane
pointInf else BaseField curve -> BaseField curve -> Point curve
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField curve
x' BaseField curve
y'
  where
    slope :: BaseField curve
slope = (BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x) BaseField curve -> BaseField curve -> BaseField curve
forall a. Field a => a -> a -> a
// (BaseField curve
y BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField curve
y)
    x' :: BaseField curve
x' = BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x
    y' :: BaseField curve
y' = BaseField curve
slope BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
x') BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a -> a
- BaseField curve
y

addPoints
    :: EllipticCurve curve
    => Field (BaseField curve)
    => Point curve
    -> Point curve
    -> Point curve
addPoints :: forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve -> Point curve
addPoints Point curve
p1 Point curve
p2 = if Point curve
p1 Point curve -> Point curve -> BooleanOf curve
forall b a. Eq b a => a -> a -> b
== Point curve
p2 then Point curve -> Point curve
forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve
pointDouble Point curve
p1 else Point curve -> Point curve -> Point curve
forall curve.
(EllipticCurve curve, Field (BaseField curve)) =>
Point curve -> Point curve -> Point curve
pointAdd Point curve
p1 Point curve
p2

pointNegate
    :: EllipticCurve curve
    => AdditiveGroup (BaseField curve)
    => Point curve -> Point curve
pointNegate :: forall curve.
(EllipticCurve curve, AdditiveGroup (BaseField curve)) =>
Point curve -> Point curve
pointNegate (Point BaseField curve
x BaseField curve
y BooleanOf curve
isInf) = if BooleanOf curve
isInf then Point curve
forall plane. ProjectivePlanar plane => plane
pointInf else BaseField curve -> BaseField curve -> Point curve
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField curve
x (BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a
negate BaseField curve
y)

pointMul
    :: forall curve s
    .  EllipticCurve curve
    => BinaryExpansion (s)
    => Bits s ~ [s]
    => P.Eq s
    => s
    -> Point curve
    -> Point curve
pointMul :: forall curve s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul = Natural -> Point curve -> Point curve
forall a. AdditiveMonoid a => Natural -> a -> a
natScale (Natural -> Point curve -> Point curve)
-> (s -> Natural) -> s -> Point curve -> Point curve
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Natural] -> Natural
Bits Natural -> Natural
forall a. BinaryExpansion a => Bits a -> a
fromBinary ([Natural] -> Natural) -> (s -> [Natural]) -> s -> Natural
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [s] -> [Natural]
forall a b. (Semiring a, Eq a, Semiring b) => [a] -> [b]
castBits ([s] -> [Natural]) -> (s -> [s]) -> s -> [Natural]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. s -> [s]
s -> Bits s
forall a. BinaryExpansion a => a -> Bits a
binaryExpansion

-- An elliptic curve in standard form, y^2 = x^3 + a * x + b
class EllipticCurve curve => WeierstrassCurve curve where
  weierstrassA :: BaseField curve
  weierstrassB :: BaseField curve

data CompressedPoint curve = CompressedPoint
  { forall curve. CompressedPoint curve -> BaseField curve
_x     :: BaseField curve
  , forall curve. CompressedPoint curve -> BooleanOf curve
_bigY  :: BooleanOf curve
  , forall curve. CompressedPoint curve -> BooleanOf curve
_isInf :: BooleanOf curve
  } deriving (forall x. CompressedPoint curve -> Rep (CompressedPoint curve) x)
-> (forall x.
    Rep (CompressedPoint curve) x -> CompressedPoint curve)
-> Generic (CompressedPoint curve)
forall x. Rep (CompressedPoint curve) x -> CompressedPoint curve
forall x. CompressedPoint curve -> Rep (CompressedPoint curve) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall curve x.
Rep (CompressedPoint curve) x -> CompressedPoint curve
forall curve x.
CompressedPoint curve -> Rep (CompressedPoint curve) x
$cfrom :: forall curve x.
CompressedPoint curve -> Rep (CompressedPoint curve) x
from :: forall x. CompressedPoint curve -> Rep (CompressedPoint curve) x
$cto :: forall curve x.
Rep (CompressedPoint curve) x -> CompressedPoint curve
to :: forall x. Rep (CompressedPoint curve) x -> CompressedPoint curve
Generic

pointCompressed :: BoolType (BooleanOf curve) => BaseField curve -> BooleanOf curve -> CompressedPoint curve
pointCompressed :: forall curve.
BoolType (BooleanOf curve) =>
BaseField curve -> BooleanOf curve -> CompressedPoint curve
pointCompressed BaseField curve
x BooleanOf curve
bigY = BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
forall curve.
BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
CompressedPoint BaseField curve
x BooleanOf curve
bigY BooleanOf curve
forall b. BoolType b => b
false

instance
  ( EllipticCurve curve
  , bool ~ BooleanOf curve
  ) => Conditional bool (CompressedPoint curve)

instance
  ( EllipticCurve curve
  , bool ~ BooleanOf curve
  ) => Eq bool (CompressedPoint curve)

instance
  ( EllipticCurve curve
  , BooleanOf curve ~ P.Bool
  ) => P.Eq (CompressedPoint curve) where
  == :: CompressedPoint curve -> CompressedPoint curve -> Bool
(==) = CompressedPoint curve -> CompressedPoint curve -> Bool
forall b a. Eq b a => a -> a -> b
(==)
  /= :: CompressedPoint curve -> CompressedPoint curve -> Bool
(/=) = CompressedPoint curve -> CompressedPoint curve -> Bool
forall b a. Eq b a => a -> a -> b
(/=)

instance
  ( Show (BaseField curve)
  , Conditional (BooleanOf curve) P.String
  , Show (BooleanOf curve)
  ) => Show (CompressedPoint curve) where
    show :: CompressedPoint curve -> String
show (CompressedPoint BaseField curve
x BooleanOf curve
bigY BooleanOf curve
isInf) =
      if BooleanOf curve
isInf then String
"InfCompressed" else String
"(" String -> ShowS
forall a. [a] -> [a] -> [a]
++ BaseField curve -> String
forall a. Show a => a -> String
show BaseField curve
x String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
", " String -> ShowS
forall a. [a] -> [a] -> [a]
++ BooleanOf curve -> String
forall a. Show a => a -> String
show BooleanOf curve
bigY String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"

instance
  ( EllipticCurve curve
  , AdditiveGroup (BaseField curve)
  , Ord (BooleanOf curve) (BaseField curve)
  , Arbitrary (ScalarField curve)
  ) => Arbitrary (CompressedPoint curve) where
    arbitrary :: Gen (CompressedPoint curve)
arbitrary = Point curve -> CompressedPoint curve
forall curve.
(AdditiveGroup (BaseField curve), EllipticCurve curve,
 Ord (BooleanOf curve) (BaseField curve)) =>
Point curve -> CompressedPoint curve
compress (Point curve -> CompressedPoint curve)
-> Gen (Point curve) -> Gen (CompressedPoint curve)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (Point curve)
forall a. Arbitrary a => Gen a
arbitrary

compress
  :: ( AdditiveGroup (BaseField curve)
     , EllipticCurve curve
     , Ord (BooleanOf curve) (BaseField curve)
     )
  => Point curve -> CompressedPoint curve
compress :: forall curve.
(AdditiveGroup (BaseField curve), EllipticCurve curve,
 Ord (BooleanOf curve) (BaseField curve)) =>
Point curve -> CompressedPoint curve
compress = \case
  Point BaseField curve
x BaseField curve
y BooleanOf curve
isInf -> if BooleanOf curve
isInf then CompressedPoint curve
forall plane. ProjectivePlanar plane => plane
pointInf else BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
forall curve.
BaseField curve
-> BooleanOf curve -> BooleanOf curve -> CompressedPoint curve
CompressedPoint BaseField curve
x (BaseField curve
y BaseField curve -> BaseField curve -> BooleanOf curve
forall b a. Ord b a => a -> a -> b
> BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a
negate BaseField curve
y) BooleanOf curve
forall b. BoolType b => b
false

decompress
  :: forall curve .
     ( WeierstrassCurve curve
     , FiniteField (BaseField curve)
     , Ord (BooleanOf curve) (BaseField curve)
     )
  => CompressedPoint curve -> Point curve
decompress :: forall curve.
(WeierstrassCurve curve, FiniteField (BaseField curve),
 Ord (BooleanOf curve) (BaseField curve)) =>
CompressedPoint curve -> Point curve
decompress (CompressedPoint BaseField curve
x BooleanOf curve
bigY BooleanOf curve
isInf) =
  if BooleanOf curve
isInf then Point curve
forall plane. ProjectivePlanar plane => plane
pointInf else
    let a :: BaseField curve
a = forall curve. WeierstrassCurve curve => BaseField curve
weierstrassA @curve
        b :: BaseField curve
b = forall curve. WeierstrassCurve curve => BaseField curve
weierstrassB @curve
        p :: Natural
p = forall a. Finite a => Natural
order @(BaseField curve)
        sqrt_ :: BaseField curve -> BaseField curve
sqrt_ BaseField curve
z = BaseField curve
z BaseField curve -> Natural -> BaseField curve
forall a b. Exponent a b => a -> b -> a
^ ((Natural
p Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
1) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`P.div` Natural
2)
        y' :: BaseField curve
y' = BaseField curve -> BaseField curve
sqrt_ (BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField curve
a BaseField curve -> BaseField curve -> BaseField curve
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField curve
x BaseField curve -> BaseField curve -> BaseField curve
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField curve
b)
        y'' :: BaseField curve
y'' = BaseField curve -> BaseField curve
forall a. AdditiveGroup a => a -> a
negate BaseField curve
y'
        y :: BaseField curve
y = if BooleanOf curve
bigY then forall b a. Ord b a => a -> a -> a
max @(BooleanOf curve) BaseField curve
y' BaseField curve
y'' else forall b a. Ord b a => a -> a -> a
min @(BooleanOf curve) BaseField curve
y' BaseField curve
y''
    in
        BaseField curve -> BaseField curve -> Point curve
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField curve
x BaseField curve
y