{-# LANGUAGE CPP, DataKinds, DerivingStrategies, FlexibleInstances, PolyKinds #-}
{-# LANGUAGE MultiParamTypeClasses, NoImplicitPrelude, Safe, ScopedTypeVariables #-}
module Curves (Curve(..), CurvePt(..), Point(..)) where
import Prelude hiding (drop, length, sqrt)
import Control.Monad (mfilter)
import Data.ByteString (ByteString, cons, drop, index, length, pack)
import Data.Maybe (fromJust)
import Data.Typeable (Proxy (Proxy))
import GHC.TypeLits (Nat, KnownNat, natVal)
import Fields (Field (..))
data Point (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f =
Projective {Point a b baseX baseY f -> f
_x :: f, Point a b baseX baseY f -> f
_y :: f, Point a b baseX baseY f -> f
_z :: f} deriving stock (Int -> Point a b baseX baseY f -> ShowS
[Point a b baseX baseY f] -> ShowS
Point a b baseX baseY f -> String
(Int -> Point a b baseX baseY f -> ShowS)
-> (Point a b baseX baseY f -> String)
-> ([Point a b baseX baseY f] -> ShowS)
-> Show (Point a b baseX baseY f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
Int -> Point a b baseX baseY f -> ShowS
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
[Point a b baseX baseY f] -> ShowS
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
Point a b baseX baseY f -> String
showList :: [Point a b baseX baseY f] -> ShowS
$cshowList :: forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
[Point a b baseX baseY f] -> ShowS
show :: Point a b baseX baseY f -> String
$cshow :: forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
Point a b baseX baseY f -> String
showsPrec :: Int -> Point a b baseX baseY f -> ShowS
$cshowsPrec :: forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Show f =>
Int -> Point a b baseX baseY f -> ShowS
Show)
#define A natVal (Proxy :: Proxy a)
#define B natVal (Proxy :: Proxy b)
#define BASE_X natVal (Proxy :: Proxy baseX)
#define BASE_Y natVal (Proxy :: Proxy baseY)
instance (Field f, KnownNat a, KnownNat b, KnownNat baseX, KnownNat baseY) =>
Eq (Point a b baseX baseY f) where
== :: Point a b baseX baseY f -> Point a b baseX baseY f -> Bool
(==) (Projective f
x1 f
y1 f
z1) (Projective f
x2 f
y2 f
z2) =
(f
x1 f -> f -> f
forall a. Num a => a -> a -> a
* f
z2 f -> f -> Bool
forall a. Eq a => a -> a -> Bool
== f
x2 f -> f -> f
forall a. Num a => a -> a -> a
* f
z1) Bool -> Bool -> Bool
&& (f
y1 f -> f -> f
forall a. Num a => a -> a -> a
* f
z2 f -> f -> Bool
forall a. Eq a => a -> a -> Bool
== f
y2 f -> f -> f
forall a. Num a => a -> a -> a
* f
z1)
class CurvePt a where
base :: a
fromBytesC :: ByteString -> Maybe a
isOnCurve :: a -> Bool
negatePt :: a -> a
neutral :: a
pointAdd :: a -> a -> a
toBytesC :: a -> ByteString
instance (Field f, KnownNat a, KnownNat b, KnownNat baseX, KnownNat baseY) =>
CurvePt (Point a b baseX baseY f) where
base :: Point a b baseX baseY f
base = f -> f -> f -> Point a b baseX baseY f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective (Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ Proxy baseX -> Integer
forall (n :: Nat) (proxy :: Nat -> *).
KnownNat n =>
proxy n -> Integer
BASE_X) (fromInteger $ BASE_Y) 1
fromBytesC :: ByteString -> Maybe (Point a b baseX baseY f)
fromBytesC ByteString
bytes
| ByteString -> Int
length ByteString
bytes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
1 Bool -> Bool -> Bool
&& ByteString -> Int -> Word8
index ByteString
bytes Int
0 Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0 = Point a b baseX baseY f -> Maybe (Point a b baseX baseY f)
forall a. a -> Maybe a
Just Point a b baseX baseY f
forall a. CurvePt a => a
neutral
| ByteString -> Int
length ByteString
bytes Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
corLen Bool -> Bool -> Bool
&& (ByteString -> Int -> Word8
index ByteString
bytes Int
0 Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0x2 Bool -> Bool -> Bool
|| ByteString -> Int -> Word8
index ByteString
bytes Int
0 Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0x03) = Maybe (Point a b baseX baseY f)
result
where
corLen :: Int
corLen = Int
1 Int -> Int -> Int
forall a. Num a => a -> a -> a
+ ByteString -> Int
length (f -> ByteString
forall a. Field a => a -> ByteString
toBytesF (Integer -> f
forall a. Num a => Integer -> a
fromInteger (A) :: f))
x :: Maybe f
x = ByteString -> Maybe f
forall a. Field a => ByteString -> Maybe a
fromBytesF (Int -> ByteString -> ByteString
drop Int
1 ByteString
bytes) :: Maybe f
sgn0y :: Integer
sgn0y = if ByteString -> Int -> Word8
index ByteString
bytes Int
0 Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0x02 then Integer
0 else Integer
1 :: Integer
alpha :: Maybe f
alpha = (\f
t -> f
t f -> Integer -> f
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
3 :: Integer) f -> f -> f
forall a. Num a => a -> a -> a
+ ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ A) :: f) * t + ((fromInteger $ B) :: f -> f -> f
forall a. Num a => a -> a -> a
f)) <$> x
beta :: Maybe f
beta = Maybe f
alpha Maybe f -> (f -> Maybe f) -> Maybe f
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= f -> Maybe f
forall a. Field a => a -> Maybe a
sqrt
y :: Maybe f
y = (\f
t -> if f -> Integer
forall a. Field a => a -> Integer
sgn0 f
t Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
sgn0y then f
t else f -> f
forall a. Num a => a -> a
negate f
t) (f -> f) -> Maybe f -> Maybe f
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe f
beta
proposed :: Maybe (Point a b baseX baseY f)
proposed = (f -> f -> f -> Point a b baseX baseY f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective (f -> f -> f -> Point a b baseX baseY f)
-> Maybe f -> Maybe (f -> f -> Point a b baseX baseY f)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Maybe f
x Maybe (f -> f -> Point a b baseX baseY f)
-> Maybe f -> Maybe (f -> Point a b baseX baseY f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Maybe f
y Maybe (f -> Point a b baseX baseY f)
-> Maybe f -> Maybe (Point a b baseX baseY f)
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> f -> Maybe f
forall a. a -> Maybe a
Just f
1) :: Maybe (Point a b baseX baseY f)
result :: Maybe (Point a b baseX baseY f)
result = (Point a b baseX baseY f -> Bool)
-> Maybe (Point a b baseX baseY f)
-> Maybe (Point a b baseX baseY f)
forall (m :: * -> *) a. MonadPlus m => (a -> Bool) -> m a -> m a
mfilter Point a b baseX baseY f -> Bool
forall a. CurvePt a => a -> Bool
isOnCurve Maybe (Point a b baseX baseY f)
proposed
fromBytesC ByteString
_ = Maybe (Point a b baseX baseY f)
forall a. Maybe a
Nothing
isOnCurve :: Point a b baseX baseY f -> Bool
isOnCurve (Projective f
x f
y f
z) = f
z f -> f -> f
forall a. Num a => a -> a -> a
* f
y f -> Integer -> f
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
2 :: Integer) f -> f -> Bool
forall a. Eq a => a -> a -> Bool
== f
x f -> Integer -> f
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
3 :: Integer) f -> f -> f
forall a. Num a => a -> a -> a
+
Integer -> f
forall a. Num a => Integer -> a
fromInteger (A) * x * z ^ (2 :: Integer) + fromInteger (B) * z ^ f -> f -> f
forall a. Num a => a -> a -> a
(3 :: Integer)
negatePt :: Point a b baseX baseY f -> Point a b baseX baseY f
negatePt (Projective f
x f
y f
z) = f -> f -> f -> Point a b baseX baseY f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective f
x (- f
y) f
z
neutral :: Point a b baseX baseY f
neutral = f -> f -> f -> Point a b baseX baseY f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective f
0 f
1 f
0
pointAdd :: Point a b baseX baseY f
-> Point a b baseX baseY f -> Point a b baseX baseY f
pointAdd (Projective f
x1 f
y1 f
z1) (Projective f
x2 f
y2 f
z2) = Point a b baseX baseY f
result
where
m0 :: f
m0 = f
x1 f -> f -> f
forall a. Num a => a -> a -> a
* f
x2
m1 :: f
m1 = f
y1 f -> f -> f
forall a. Num a => a -> a -> a
* f
y2
m2 :: f
m2 = f
z1 f -> f -> f
forall a. Num a => a -> a -> a
* f
z2
m3 :: f
m3 = (f
x1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
y1) f -> f -> f
forall a. Num a => a -> a -> a
* (f
x2 f -> f -> f
forall a. Num a => a -> a -> a
+ f
y2)
m4 :: f
m4 = (f
x1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
z1) f -> f -> f
forall a. Num a => a -> a -> a
* (f
x2 f -> f -> f
forall a. Num a => a -> a -> a
+ f
z2)
m5 :: f
m5 = (f
y1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
z1) f -> f -> f
forall a. Num a => a -> a -> a
* (f
y2 f -> f -> f
forall a. Num a => a -> a -> a
+ f
z2)
m6 :: f
m6 = ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ A) :: f) * (- m0 - m2 + m4)
m7 :: f
m7 = ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ Integer
3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* B) :: f) * m2
m8 :: f
m8 = (f
m1 f -> f -> f
forall a. Num a => a -> a -> a
- f
m6 f -> f -> f
forall a. Num a => a -> a -> a
- f
m7) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m6 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m7)
m9 :: f
m9 = ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ A) :: f) * m2
m10 :: f
m10 = ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ Integer
3 Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* B) :: f) * (- m0 - m2 + m4)
m11 :: f
m11 = ((Integer -> f
forall a. Num a => Integer -> a
fromInteger (Integer -> f) -> Integer -> f
forall a b. (a -> b) -> a -> b
$ A) :: f) * (m0 - m9)
m12 :: f
m12 = (f
m0 f -> f -> f
forall a. Num a => a -> a -> a
* f
3 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m9) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m10 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m11)
m13 :: f
m13 = (- f
m1 f -> f -> f
forall a. Num a => a -> a -> a
- f
m2 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m5) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m10 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m11)
m14 :: f
m14 = (- f
m0 f -> f -> f
forall a. Num a => a -> a -> a
- f
m1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m3) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m1 f -> f -> f
forall a. Num a => a -> a -> a
- f
m6 f -> f -> f
forall a. Num a => a -> a -> a
- f
m7)
m15 :: f
m15 = (- f
m0 f -> f -> f
forall a. Num a => a -> a -> a
- f
m1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m3) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m0 f -> f -> f
forall a. Num a => a -> a -> a
* f
3 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m9)
m16 :: f
m16 = (- f
m1 f -> f -> f
forall a. Num a => a -> a -> a
- f
m2 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m5) f -> f -> f
forall a. Num a => a -> a -> a
* (f
m1 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m6 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m7)
result :: Point a b baseX baseY f
result = f -> f -> f -> Point a b baseX baseY f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective (-f
m13 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m14) (f
m8 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m12) (f
m15 f -> f -> f
forall a. Num a => a -> a -> a
+ f
m16) :: Point a b baseX baseY f
toBytesC :: Point a b baseX baseY f -> ByteString
toBytesC Point a b baseX baseY f
pt
| Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Point a b baseX baseY f -> Bool
forall a. CurvePt a => a -> Bool
isOnCurve Point a b baseX baseY f
pt = String -> ByteString
forall a. HasCallStack => String -> a
error String
"trying to serialize point not on curve"
| Point a b baseX baseY f -> f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Point a b baseX baseY f -> f
_z Point a b baseX baseY f
pt f -> f -> Bool
forall a. Eq a => a -> a -> Bool
== f
0 = [Word8] -> ByteString
pack [Word8
0]
| f -> Integer
forall a. Field a => a -> Integer
sgn0 f
y Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = Word8 -> ByteString -> ByteString
cons Word8
0x02 (f -> ByteString
forall a. Field a => a -> ByteString
toBytesF f
x)
| Bool
otherwise = Word8 -> ByteString -> ByteString
cons Word8
0x03 (f -> ByteString
forall a. Field a => a -> ByteString
toBytesF f
x)
where
x :: f
x = Point a b baseX baseY f -> f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Point a b baseX baseY f -> f
_x Point a b baseX baseY f
pt f -> f -> f
forall a. Num a => a -> a -> a
* f -> f
forall a. Field a => a -> a
inv0 (Point a b baseX baseY f -> f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Point a b baseX baseY f -> f
_z Point a b baseX baseY f
pt)
y :: f
y = Point a b baseX baseY f -> f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Point a b baseX baseY f -> f
_y Point a b baseX baseY f
pt f -> f -> f
forall a. Num a => a -> a -> a
* f -> f
forall a. Field a => a -> a
inv0 (Point a b baseX baseY f -> f
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
Point a b baseX baseY f -> f
_z Point a b baseX baseY f
pt)
class (CurvePt a, Field b) => Curve a b where
pointMul :: b -> a -> a
mapToCurveSimpleSwu :: b -> b -> a
instance (Field f1, Field f2, KnownNat a, KnownNat b, KnownNat baseX, KnownNat baseY) =>
Curve (Point a b baseX baseY f1) f2 where
pointMul :: f2 -> Point a b baseX baseY f1 -> Point a b baseX baseY f1
pointMul f2
s Point a b baseX baseY f1
pt = f2
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
pointMul' f2
s Point a b baseX baseY f1
pt Point a b baseX baseY f1
forall a. CurvePt a => a
neutral
where
pointMul' :: f2 -> Point a b baseX baseY f1 -> Point a b baseX baseY f1 -> Point a b baseX baseY f1
pointMul' :: f2
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
pointMul' f2
scalar Point a b baseX baseY f1
p1 Point a b baseX baseY f1
accum
| f2
scalar f2 -> f2 -> Bool
forall a. Eq a => a -> a -> Bool
== f2
0 = Point a b baseX baseY f1
accum
| f2 -> Integer
forall a. Field a => a -> Integer
sgn0 f2
scalar Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= Integer
0 = f2
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
pointMul' (f2 -> f2
forall a. Field a => a -> a
shiftR1 f2
scalar) Point a b baseX baseY f1
doublePt (Point a b baseX baseY f1
-> Point a b baseX baseY f1 -> Point a b baseX baseY f1
forall a. CurvePt a => a -> a -> a
pointAdd Point a b baseX baseY f1
accum Point a b baseX baseY f1
p1)
| f2 -> Integer
forall a. Field a => a -> Integer
sgn0 f2
scalar Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 = f2
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
-> Point a b baseX baseY f1
pointMul' (f2 -> f2
forall a. Field a => a -> a
shiftR1 f2
scalar) Point a b baseX baseY f1
doublePt Point a b baseX baseY f1
accum
| Bool
otherwise = String -> Point a b baseX baseY f1
forall a. HasCallStack => String -> a
error String
"pointMul' pattern match fail (should never happen)"
where
doublePt :: Point a b baseX baseY f1
doublePt = Point a b baseX baseY f1
-> Point a b baseX baseY f1 -> Point a b baseX baseY f1
forall a. CurvePt a => a -> a -> a
pointAdd Point a b baseX baseY f1
p1 Point a b baseX baseY f1
p1
mapToCurveSimpleSwu :: f2 -> f2 -> Point a b baseX baseY f1
mapToCurveSimpleSwu f2
fu f2
fz = if A * B /= 0 then result else error "Curve params A*B must not be zero"
where
u :: f1
u = (Integer -> f1
forall a. Num a => Integer -> a
fromInteger (Integer -> f1) -> Integer -> f1
forall a b. (a -> b) -> a -> b
$ f2 -> Integer
forall a. Field a => a -> Integer
toI f2
fu) :: f1
z :: f1
z = (Integer -> f1
forall a. Num a => Integer -> a
fromInteger (Integer -> f1) -> Integer -> f1
forall a b. (a -> b) -> a -> b
$ f2 -> Integer
forall a. Field a => a -> Integer
toI f2
fz) :: f1
tv1 :: f1
tv1 = f1 -> f1
forall a. Field a => a -> a
inv0 (f1
z f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
2 :: Integer) f1 -> f1 -> f1
forall a. Num a => a -> a -> a
* f1
u f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
4 :: Integer) f1 -> f1 -> f1
forall a. Num a => a -> a -> a
+ f1
z f1 -> f1 -> f1
forall a. Num a => a -> a -> a
* f1
u f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
2 :: Integer))
x1a :: f1
x1a = (Integer -> f1
forall a. Num a => Integer -> a
fromInteger ((-Integer
1) Integer -> Integer -> Integer
forall a. Num a => a -> a -> a
* B) * inv0 (fromInteger (A))f1 -> f1 -> f1
forall a. Num a => a -> a -> a
) * (1 + tv1)
x1 :: f1
x1 = if f1 -> Integer
forall a. Field a => a -> Integer
toI f1
tv1 Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
== Integer
0 then Integer -> f1
forall a. Num a => Integer -> a
fromInteger (B) * inv0 (z * fromInteger f1 -> f1 -> f1
forall a. Num a => a -> a -> a
(A)) else x1a
gx1 :: f1
gx1 = f1
x1 f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
3 :: Integer) f1 -> f1 -> f1
forall a. Num a => a -> a -> a
+ Integer -> f1
forall a. Num a => Integer -> a
fromInteger (A) * x1 + fromInteger (B)
x2 :: f1
x2 = f1
z f1 -> f1 -> f1
forall a. Num a => a -> a -> a
* f1
u f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
2 :: Integer) f1 -> f1 -> f1
forall a. Num a => a -> a -> a
* f1
x1
gx2 :: f1
gx2 = f1
x2 f1 -> Integer -> f1
forall a b. (Num a, Integral b) => a -> b -> a
^ (Integer
3 :: Integer) f1 -> f1 -> f1
forall a. Num a => a -> a -> a
+ Integer -> f1
forall a. Num a => Integer -> a
fromInteger (A) * x2 + fromInteger (B)
(f1
x, f1
ya) = if f1 -> Bool
forall a. Field a => a -> Bool
isSqr f1
gx1 then (f1
x1, Maybe f1 -> f1
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe f1 -> f1) -> Maybe f1 -> f1
forall a b. (a -> b) -> a -> b
$ f1 -> Maybe f1
forall a. Field a => a -> Maybe a
sqrt f1
gx1) else (f1
x2, Maybe f1 -> f1
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe f1 -> f1) -> Maybe f1 -> f1
forall a b. (a -> b) -> a -> b
$ f1 -> Maybe f1
forall a. Field a => a -> Maybe a
sqrt f1
gx2)
y :: f1
y = if f1 -> Integer
forall a. Field a => a -> Integer
sgn0 f1
u Integer -> Integer -> Bool
forall a. Eq a => a -> a -> Bool
/= f1 -> Integer
forall a. Field a => a -> Integer
sgn0 f1
ya then -f1
ya else f1
ya
result :: Point a b baseX baseY f1
result = f1 -> f1 -> f1 -> Point a b baseX baseY f1
forall (a :: Nat) (b :: Nat) (baseX :: Nat) (baseY :: Nat) f.
f -> f -> f -> Point a b baseX baseY f
Projective f1
x f1
y f1
1 :: Point a b baseX baseY f1