{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE RebindableSyntax    #-}
{-# LANGUAGE TypeOperators       #-}

module ZkFold.Base.Algebra.EllipticCurve.Pairing
  ( millerAlgorithmBN
  , millerAlgorithmBLS12
  , finalExponentiation
  ) where

import qualified Data.Bool                               as H
import           Data.Function                           (($), (.))
import           Data.Functor                            ((<$>))
import           Data.Int                                (Int8)
import           Data.Tuple                              (snd)
import           Data.Type.Equality                      (type (~))
import           Numeric.Natural                         (Natural)
import           Prelude                                 (fromInteger)
import qualified Prelude

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Symbolic.Data.Bool               hiding (Bool)
import           ZkFold.Symbolic.Data.Conditional
import           ZkFold.Symbolic.Data.Eq

-- Ate pairing implementation adapted from:
-- https://github.com/sdiehl/pairing/blob/master/src/Data/Pairing/Ate.hs

type Untwisted baseField i j = Ext2 (Ext3 baseField i) j

finalExponentiation ::
  forall scalarField baseField g i j.
  (Finite scalarField, Finite baseField) =>
  (g ~ Untwisted baseField i j, Exponent g Natural) =>
  g -> g
finalExponentiation :: forall scalarField baseField g (i :: Symbol) (j :: Symbol).
(Finite scalarField, Finite baseField, g ~ Untwisted baseField i j,
 Exponent g Natural) =>
g -> g
finalExponentiation g
x = g
x g -> Natural -> g
forall a b. Exponent a b => a -> b -> a
^ ((Natural
p Natural -> Natural -> Natural
forall a b. Exponent a b => a -> b -> a
^ (Natural
12 :: Natural) Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
r)
  where
    p :: Natural
p = forall a. Finite a => Natural
order @baseField
    r :: Natural
r = forall a. Finite a => Natural
order @scalarField

millerAlgorithmBLS12 ::forall c d fldC fldD i j g.
  WeierstrassCurve d fldD =>
  Eq fldD =>
  FiniteField fldC =>
  Scale fldC fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  BooleanOf fldC ~ BooleanOf fldD =>
  Untwisted fldD i j ~ g =>
  Field g =>
  [Int8] ->
  Weierstrass c (Point fldC) ->
  Weierstrass d (Point fldD) ->
  g
millerAlgorithmBLS12 :: forall {k} (c :: k) (d :: Symbol) fldC fldD (i :: Symbol)
       (j :: Symbol) g.
(WeierstrassCurve d fldD, Eq fldD, FiniteField fldC,
 Scale fldC fldD, Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
[Int8]
-> Weierstrass c (Point fldC) -> Weierstrass d (Point fldD) -> g
millerAlgorithmBLS12 (Int8
x:[Int8]
xs) Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q = (Weierstrass d (Point fldD), g) -> g
forall a b. (a, b) -> b
snd ((Weierstrass d (Point fldD), g) -> g)
-> (Weierstrass d (Point fldD), g) -> g
forall a b. (a -> b) -> a -> b
$
  Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
millerLoop Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q [Int8]
xs (Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD) -> Bool -> Weierstrass d (Point fldD)
forall a. a -> a -> Bool -> a
H.bool (Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall a. AdditiveGroup a => a -> a
negate Weierstrass d (Point fldD)
q) Weierstrass d (Point fldD)
q (Int8
x Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> Int8
0), g
forall a. MultiplicativeMonoid a => a
one)
millerAlgorithmBLS12 [Int8]
_ Weierstrass c (Point fldC)
_ Weierstrass d (Point fldD)
_ = g
forall a. MultiplicativeMonoid a => a
one

millerAlgorithmBN :: forall c d fldC fldD i j g.
  WeierstrassCurve d fldD =>
  Eq fldD =>
  FiniteField fldC =>
  Scale fldC fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  BooleanOf fldC ~ BooleanOf fldD =>
  Untwisted fldD i j ~ g =>
  Field g =>
  fldD ->
  [Int8] ->
  Weierstrass c (Point fldC) ->
  Weierstrass d (Point fldD) ->
  g
millerAlgorithmBN :: forall {k} (c :: k) (d :: Symbol) fldC fldD (i :: Symbol)
       (j :: Symbol) g.
(WeierstrassCurve d fldD, Eq fldD, FiniteField fldC,
 Scale fldC fldD, Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
fldD
-> [Int8]
-> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> g
millerAlgorithmBN fldD
xi (Int8
x:[Int8]
xs) Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q = fldD
-> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> g
forall {k} (c :: k) (d :: Symbol) fldC fldD (i :: Symbol)
       (j :: Symbol) g.
(WeierstrassCurve d fldD, Eq fldD, FiniteField fldC,
 Scale fldC fldD, Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
fldD
-> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> g
finalStepBN fldD
xi Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q ((Weierstrass d (Point fldD), g) -> g)
-> (Weierstrass d (Point fldD), g) -> g
forall a b. (a -> b) -> a -> b
$
  Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
millerLoop Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q [Int8]
xs (Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD) -> Bool -> Weierstrass d (Point fldD)
forall a. a -> a -> Bool -> a
H.bool (Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall a. AdditiveGroup a => a -> a
negate Weierstrass d (Point fldD)
q) Weierstrass d (Point fldD)
q (Int8
x Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> Int8
0), g
forall a. MultiplicativeMonoid a => a
one)
millerAlgorithmBN fldD
_ [Int8]
_ Weierstrass c (Point fldC)
_ Weierstrass d (Point fldD)
_ = g
forall a. MultiplicativeMonoid a => a
one

-- --------------------------------------------------------------------------------

finalStepBN :: forall c d fldC fldD i j g.
  WeierstrassCurve d fldD =>
  Eq fldD =>
  FiniteField fldC =>
  Scale fldC fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  BooleanOf fldC ~ BooleanOf fldD =>
  Untwisted fldD i j ~ g =>
  Field g =>
  fldD ->
  Weierstrass c (Point fldC) ->
  Weierstrass d (Point fldD) ->
  (Weierstrass d (Point fldD), g) ->
  g
finalStepBN :: forall {k} (c :: k) (d :: Symbol) fldC fldD (i :: Symbol)
       (j :: Symbol) g.
(WeierstrassCurve d fldD, Eq fldD, FiniteField fldC,
 Scale fldC fldD, Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
fldD
-> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> g
finalStepBN fldD
xi Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q (Weierstrass d (Point fldD)
t, g
f) = g
f g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f' g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f''
  where
    o :: Natural
o = forall a. Finite a => Natural
order @fldC
    q1 :: Weierstrass d (Point fldD)
q1 = Natural
-> fldD -> Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall (c :: Symbol) fld.
(WeierstrassCurve c fld,
 Conditional (BooleanOf fld) (BooleanOf fld), Eq fld) =>
Natural
-> fld -> Weierstrass c (Point fld) -> Weierstrass c (Point fld)
frobTwisted Natural
o fldD
xi Weierstrass d (Point fldD)
q
    (Weierstrass d (Point fldD)
t', g
f') = Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
forall {k} (c :: k) (d :: Symbol) baseFieldC baseFieldD
       (i :: Symbol) (j :: Symbol) g.
(WeierstrassCurve d baseFieldD, Field baseFieldC,
 Scale baseFieldC baseFieldD,
 Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD),
 Eq baseFieldD, BooleanOf baseFieldC ~ BooleanOf baseFieldD,
 Untwisted baseFieldD i j ~ g) =>
Weierstrass c (Point baseFieldC)
-> Weierstrass d (Point baseFieldD)
-> Weierstrass d (Point baseFieldD)
-> (Weierstrass d (Point baseFieldD), g)
lineFunction Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
t Weierstrass d (Point fldD)
q1
    q2 :: Weierstrass d (Point fldD)
q2 = Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall a. AdditiveGroup a => a -> a
negate (Natural
-> fldD -> Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall (c :: Symbol) fld.
(WeierstrassCurve c fld,
 Conditional (BooleanOf fld) (BooleanOf fld), Eq fld) =>
Natural
-> fld -> Weierstrass c (Point fld) -> Weierstrass c (Point fld)
frobTwisted Natural
o fldD
xi Weierstrass d (Point fldD)
q1)
    (Weierstrass d (Point fldD)
_, g
f'') = Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
forall {k} (c :: k) (d :: Symbol) baseFieldC baseFieldD
       (i :: Symbol) (j :: Symbol) g.
(WeierstrassCurve d baseFieldD, Field baseFieldC,
 Scale baseFieldC baseFieldD,
 Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD),
 Eq baseFieldD, BooleanOf baseFieldC ~ BooleanOf baseFieldD,
 Untwisted baseFieldD i j ~ g) =>
Weierstrass c (Point baseFieldC)
-> Weierstrass d (Point baseFieldD)
-> Weierstrass d (Point baseFieldD)
-> (Weierstrass d (Point baseFieldD), g)
lineFunction Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
t' Weierstrass d (Point fldD)
q2

millerLoop ::
  WeierstrassCurve d fldD =>
  Eq fldD =>
  Field fldC =>
  Scale fldC fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  BooleanOf fldC ~ BooleanOf fldD =>
  Untwisted fldD i j ~ g =>
  Field g =>
  Weierstrass c (Point fldC) ->
  Weierstrass d (Point fldD) ->
  [Int8] ->
  (Weierstrass d (Point fldD), g) ->
  (Weierstrass d (Point fldD), g)
millerLoop :: forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
millerLoop Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q = [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
impl
  where impl :: [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
impl []     (Weierstrass d (Point fldD), g)
tf = (Weierstrass d (Point fldD), g)
tf
        impl (Int8
x:[Int8]
xs) (Weierstrass d (Point fldD), g)
tf
          | Int8
x Int8 -> Int8 -> Bool
forall a. Eq a => a -> a -> Bool
Prelude.== Int8
0    = [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
impl [Int8]
xs (Weierstrass d (Point fldD), g)
tf2
          | Int8
x Int8 -> Int8 -> Bool
forall a. Eq a => a -> a -> Bool
Prelude.== Int8
1    = [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
impl [Int8]
xs ((Weierstrass d (Point fldD), g)
 -> (Weierstrass d (Point fldD), g))
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall a b. (a -> b) -> a -> b
$ Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 BooleanOf fldC ~ BooleanOf fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 Untwisted fldD i j ~ g, Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
additionStep Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q (Weierstrass d (Point fldD), g)
tf2
          | Bool
H.otherwise = [Int8]
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
impl [Int8]
xs ((Weierstrass d (Point fldD), g)
 -> (Weierstrass d (Point fldD), g))
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall a b. (a -> b) -> a -> b
$ Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 BooleanOf fldC ~ BooleanOf fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 Untwisted fldD i j ~ g, Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
additionStep Weierstrass c (Point fldC)
p (Weierstrass d (Point fldD) -> Weierstrass d (Point fldD)
forall a. AdditiveGroup a => a -> a
negate Weierstrass d (Point fldD)
q) (Weierstrass d (Point fldD), g)
tf2
          where tf2 :: (Weierstrass d (Point fldD), g)
tf2 = Weierstrass c (Point fldC)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
Weierstrass c (Point fldC)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
doublingStep Weierstrass c (Point fldC)
p (Weierstrass d (Point fldD), g)
tf

--------------------------------------------------------------------------------

frobTwisted ::
  forall c fld.
  ( WeierstrassCurve c fld
  , Conditional (BooleanOf fld) (BooleanOf fld)
  , Eq fld
  ) => Natural -> fld -> Weierstrass c (Point fld) -> Weierstrass c (Point fld)
frobTwisted :: forall (c :: Symbol) fld.
(WeierstrassCurve c fld,
 Conditional (BooleanOf fld) (BooleanOf fld), Eq fld) =>
Natural
-> fld -> Weierstrass c (Point fld) -> Weierstrass c (Point fld)
frobTwisted Natural
q fld
xi (Weierstrass (Point fld
x fld
y BooleanOf fld
isInf)) =
  if BooleanOf fld
isInf then Weierstrass c (Point fld)
forall point. HasPointInf point => point
pointInf else fld -> fld -> Weierstrass c (Point fld)
forall field point. Planar field point => field -> field -> point
pointXY ((fld
x fld -> Natural -> fld
forall a b. Exponent a b => a -> b -> a
^ Natural
q) fld -> fld -> fld
forall a. MultiplicativeSemigroup a => a -> a -> a
* (fld
xi fld -> Natural -> fld
forall a b. Exponent a b => a -> b -> a
^ Natural
tx)) ((fld
y fld -> Natural -> fld
forall a b. Exponent a b => a -> b -> a
^ Natural
q) fld -> fld -> fld
forall a. MultiplicativeSemigroup a => a -> a -> a
* (fld
xi fld -> Natural -> fld
forall a b. Exponent a b => a -> b -> a
^ Natural
ty))
  where
    tx :: Natural
tx = (Natural
q Natural -> Natural -> Natural
-! Natural
1) Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
3
    ty :: Natural
ty = Natural
q Natural -> Natural -> Natural
forall a. SemiEuclidean a => a -> a -> a
`div` Natural
2

additionStep ::
  WeierstrassCurve d fldD =>
  Eq fldD =>
  Field fldC =>
  Scale fldC fldD =>
  BooleanOf fldC ~ BooleanOf fldD =>
  -- Conditional bool fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  Untwisted fldD i j ~ g =>
  Field g =>
  Weierstrass c (Point fldC) ->
  Weierstrass d (Point fldD) ->
  (Weierstrass d (Point fldD), g) ->
  (Weierstrass d (Point fldD), g)
additionStep :: forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 BooleanOf fldC ~ BooleanOf fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 Untwisted fldD i j ~ g, Field g) =>
Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
additionStep Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q (Weierstrass d (Point fldD)
t, g
f) = (g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f) (g -> g)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
forall {k} (c :: k) (d :: Symbol) baseFieldC baseFieldD
       (i :: Symbol) (j :: Symbol) g.
(WeierstrassCurve d baseFieldD, Field baseFieldC,
 Scale baseFieldC baseFieldD,
 Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD),
 Eq baseFieldD, BooleanOf baseFieldC ~ BooleanOf baseFieldD,
 Untwisted baseFieldD i j ~ g) =>
Weierstrass c (Point baseFieldC)
-> Weierstrass d (Point baseFieldD)
-> Weierstrass d (Point baseFieldD)
-> (Weierstrass d (Point baseFieldD), g)
lineFunction Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
q Weierstrass d (Point fldD)
t

doublingStep ::
  WeierstrassCurve d fldD =>
  Eq fldD =>
  Field fldC =>
  Scale fldC fldD =>
  Conditional (BooleanOf fldD) (BooleanOf fldD) =>
  BooleanOf fldC ~ BooleanOf fldD =>
  Untwisted fldD i j ~ g =>
  Field g =>
  Weierstrass c (Point fldC) ->
  (Weierstrass d (Point fldD), g) ->
  (Weierstrass d (Point fldD), g)
doublingStep :: forall {k} (d :: Symbol) fldD fldC (i :: Symbol) (j :: Symbol) g
       (c :: k).
(WeierstrassCurve d fldD, Eq fldD, Field fldC, Scale fldC fldD,
 Conditional (BooleanOf fldD) (BooleanOf fldD),
 BooleanOf fldC ~ BooleanOf fldD, Untwisted fldD i j ~ g,
 Field g) =>
Weierstrass c (Point fldC)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
doublingStep Weierstrass c (Point fldC)
p (Weierstrass d (Point fldD)
t, g
f) = (g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f) (g -> g) -> (g -> g) -> g -> g
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f) (g -> g)
-> (Weierstrass d (Point fldD), g)
-> (Weierstrass d (Point fldD), g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Weierstrass c (Point fldC)
-> Weierstrass d (Point fldD)
-> Weierstrass d (Point fldD)
-> (Weierstrass d (Point fldD), g)
forall {k} (c :: k) (d :: Symbol) baseFieldC baseFieldD
       (i :: Symbol) (j :: Symbol) g.
(WeierstrassCurve d baseFieldD, Field baseFieldC,
 Scale baseFieldC baseFieldD,
 Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD),
 Eq baseFieldD, BooleanOf baseFieldC ~ BooleanOf baseFieldD,
 Untwisted baseFieldD i j ~ g) =>
Weierstrass c (Point baseFieldC)
-> Weierstrass d (Point baseFieldD)
-> Weierstrass d (Point baseFieldD)
-> (Weierstrass d (Point baseFieldD), g)
lineFunction Weierstrass c (Point fldC)
p Weierstrass d (Point fldD)
t Weierstrass d (Point fldD)
t


lineFunction :: forall c d baseFieldC baseFieldD i j g.
  WeierstrassCurve d baseFieldD =>
  Field baseFieldC =>
  Scale baseFieldC baseFieldD =>
  Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD) =>
  -- Conditional bool baseFieldD =>
  Eq baseFieldD =>
  BooleanOf baseFieldC ~ BooleanOf baseFieldD =>
  Untwisted baseFieldD i j ~ g =>
  Weierstrass c (Point baseFieldC) ->
  Weierstrass d (Point baseFieldD) ->
  Weierstrass d (Point baseFieldD) ->
  (Weierstrass d (Point baseFieldD), g)
lineFunction :: forall {k} (c :: k) (d :: Symbol) baseFieldC baseFieldD
       (i :: Symbol) (j :: Symbol) g.
(WeierstrassCurve d baseFieldD, Field baseFieldC,
 Scale baseFieldC baseFieldD,
 Conditional (BooleanOf baseFieldD) (BooleanOf baseFieldD),
 Eq baseFieldD, BooleanOf baseFieldC ~ BooleanOf baseFieldD,
 Untwisted baseFieldD i j ~ g) =>
Weierstrass c (Point baseFieldC)
-> Weierstrass d (Point baseFieldD)
-> Weierstrass d (Point baseFieldD)
-> (Weierstrass d (Point baseFieldD), g)
lineFunction
  (Weierstrass (Point baseFieldC
x baseFieldC
y BooleanOf baseFieldC
isInf))
  (Weierstrass (Point baseFieldD
x1 baseFieldD
y1 BooleanOf baseFieldD
isInf1))
  (Weierstrass (Point baseFieldD
x2 baseFieldD
y2 BooleanOf baseFieldD
isInf2)) =
  if BooleanOf baseFieldC
BooleanOf baseFieldD
isInf BooleanOf baseFieldD
-> BooleanOf baseFieldD -> BooleanOf baseFieldD
forall b. BoolType b => b -> b -> b
|| BooleanOf baseFieldD
isInf1 BooleanOf baseFieldD
-> BooleanOf baseFieldD -> BooleanOf baseFieldD
forall b. BoolType b => b -> b -> b
|| BooleanOf baseFieldD
isInf2 then (Weierstrass d (Point baseFieldD)
forall point. HasPointInf point => point
pointInf, Ext3 baseFieldD i -> Ext3 baseFieldD i -> Untwisted baseFieldD i j
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 (baseFieldD -> baseFieldD -> baseFieldD -> Ext3 baseFieldD i
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 baseFieldD
forall a. MultiplicativeMonoid a => a
one baseFieldD
forall a. AdditiveMonoid a => a
zero baseFieldD
forall a. AdditiveMonoid a => a
zero) Ext3 baseFieldD i
forall a. AdditiveMonoid a => a
zero)
  else if baseFieldD
x1 baseFieldD -> baseFieldD -> BooleanOf baseFieldD
forall a. Eq a => a -> a -> BooleanOf a
/= baseFieldD
x2 then (baseFieldD -> baseFieldD -> Weierstrass d (Point baseFieldD)
forall field point. Planar field point => field -> field -> point
pointXY baseFieldD
x3 baseFieldD
y3, baseFieldC -> baseFieldD -> baseFieldD -> Untwisted baseFieldD i j
forall {f} {b} {e :: Symbol} {e :: Symbol}.
(MultiplicativeMonoid f, AdditiveMonoid f, Scale b f) =>
b -> f -> f -> Ext2 (Ext3 f e) e
untwist (baseFieldC -> baseFieldC
forall a. AdditiveGroup a => a -> a
negate baseFieldC
y) (baseFieldC
x baseFieldC -> baseFieldD -> baseFieldD
forall b a. Scale b a => b -> a -> a
`scale` baseFieldD
l) (baseFieldD
y1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
l baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* baseFieldD
x1))
  else if baseFieldD
y1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveSemigroup a => a -> a -> a
+ baseFieldD
y2 baseFieldD -> baseFieldD -> BooleanOf baseFieldD
forall a. Eq a => a -> a -> BooleanOf a
== baseFieldD
forall a. AdditiveMonoid a => a
zero then (Weierstrass d (Point baseFieldD)
forall point. HasPointInf point => point
pointInf, baseFieldC -> baseFieldD -> baseFieldD -> Untwisted baseFieldD i j
forall {f} {b} {e :: Symbol} {e :: Symbol}.
(MultiplicativeMonoid f, AdditiveMonoid f, Scale b f) =>
b -> f -> f -> Ext2 (Ext3 f e) e
untwist baseFieldC
x (baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a
negate baseFieldD
x1) baseFieldD
forall a. AdditiveMonoid a => a
zero)
  else (baseFieldD -> baseFieldD -> Weierstrass d (Point baseFieldD)
forall field point. Planar field point => field -> field -> point
pointXY baseFieldD
x3' baseFieldD
y3', baseFieldC -> baseFieldD -> baseFieldD -> Untwisted baseFieldD i j
forall {f} {b} {e :: Symbol} {e :: Symbol}.
(MultiplicativeMonoid f, AdditiveMonoid f, Scale b f) =>
b -> f -> f -> Ext2 (Ext3 f e) e
untwist (baseFieldC -> baseFieldC
forall a. AdditiveGroup a => a -> a
negate baseFieldC
y) (baseFieldC
x baseFieldC -> baseFieldD -> baseFieldD
forall b a. Scale b a => b -> a -> a
`scale` baseFieldD
l') (baseFieldD
y1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
l' baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* baseFieldD
x1))
  where
    l :: baseFieldD
l   = (baseFieldD
y2 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
y1) baseFieldD -> baseFieldD -> baseFieldD
forall a. Field a => a -> a -> a
// (baseFieldD
x2 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x1)
    x3 :: baseFieldD
x3  = baseFieldD
l baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* baseFieldD
l baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x2
    y3 :: baseFieldD
y3  = baseFieldD
l baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* (baseFieldD
x1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x3) baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
y1
    x12 :: baseFieldD
x12 = baseFieldD
x1 baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* baseFieldD
x1
    l' :: baseFieldD
l'  = (baseFieldD
x12 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveSemigroup a => a -> a -> a
+ baseFieldD
x12 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveSemigroup a => a -> a -> a
+ baseFieldD
x12) baseFieldD -> baseFieldD -> baseFieldD
forall a. Field a => a -> a -> a
// (baseFieldD
y1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveSemigroup a => a -> a -> a
+ baseFieldD
y1)
    x3' :: baseFieldD
x3' = baseFieldD
l' baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* baseFieldD
l' baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x2
    y3' :: baseFieldD
y3' = baseFieldD
l' baseFieldD -> baseFieldD -> baseFieldD
forall a. MultiplicativeSemigroup a => a -> a -> a
* (baseFieldD
x1 baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
x3') baseFieldD -> baseFieldD -> baseFieldD
forall a. AdditiveGroup a => a -> a -> a
- baseFieldD
y1
    untwist :: b -> f -> f -> Ext2 (Ext3 f e) e
untwist b
a f
b f
c = Ext3 f e -> Ext3 f e -> Ext2 (Ext3 f e) e
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 (f -> f -> f -> Ext3 f e
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 (b
a b -> f -> f
forall b a. Scale b a => b -> a -> a
`scale` f
forall a. MultiplicativeMonoid a => a
one) f
forall a. AdditiveMonoid a => a
zero f
forall a. AdditiveMonoid a => a
zero) (f -> f -> f -> Ext3 f e
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 f
b f
c f
forall a. AdditiveMonoid a => a
zero)