{-# 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 c i j = Ext2 (Ext3 (BaseField c) i) j

finalExponentiation ::
  forall c g i j.
  (Finite (ScalarField c), Finite (BaseField c)) =>
  (g ~ Untwisted c i j, Exponent g Natural) =>
  g -> g
finalExponentiation :: forall c g (i :: Symbol) (j :: Symbol).
(Finite (ScalarField c), Finite (BaseField c), g ~ Untwisted c 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 c)
    r :: Natural
r = forall a. Finite a => Natural
order @(ScalarField c)

millerAlgorithmBLS12 ::
  Field (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  EllipticCurve d =>
  Untwisted d i j ~ g =>
  Field g =>
  BooleanOf c ~ BooleanOf d =>
  [Int8] -> Point c -> Point d -> g
millerAlgorithmBLS12 :: forall c d (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
[Int8] -> Point c -> Point d -> g
millerAlgorithmBLS12 (Int8
x:[Int8]
xs) Point c
p Point d
q = (Point d, g) -> g
forall a b. (a, b) -> b
snd ((Point d, g) -> g) -> (Point d, g) -> g
forall a b. (a -> b) -> a -> b
$
  Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
forall c d (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
millerLoop Point c
p Point d
q [Int8]
xs (Point d -> Point d -> Bool -> Point d
forall a. a -> a -> Bool -> a
H.bool (Point d -> Point d
forall a. AdditiveGroup a => a -> a
negate Point d
q) Point d
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]
_ Point c
_ Point d
_ = g
forall a. MultiplicativeMonoid a => a
one

millerAlgorithmBN ::
  PrimeField (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  EllipticCurve d =>
  Untwisted d i j ~ g =>
  Field g =>
  BooleanOf c ~ BooleanOf d =>
  BaseField d -> [Int8] -> Point c -> Point d -> g
millerAlgorithmBN :: forall c d (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
BaseField d -> [Int8] -> Point c -> Point d -> g
millerAlgorithmBN BaseField d
xi (Int8
x:[Int8]
xs) Point c
p Point d
q = BaseField d -> Point c -> Point d -> (Point d, g) -> g
forall c d (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
BaseField d -> Point c -> Point d -> (Point d, g) -> g
finalStepBN BaseField d
xi Point c
p Point d
q ((Point d, g) -> g) -> (Point d, g) -> g
forall a b. (a -> b) -> a -> b
$
  Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
forall c d (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
millerLoop Point c
p Point d
q [Int8]
xs (Point d -> Point d -> Bool -> Point d
forall a. a -> a -> Bool -> a
H.bool (Point d -> Point d
forall a. AdditiveGroup a => a -> a
negate Point d
q) Point d
q (Int8
x Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
Prelude.> Int8
0), g
forall a. MultiplicativeMonoid a => a
one)
millerAlgorithmBN BaseField d
_ [Int8]
_ Point c
_ Point d
_ = g
forall a. MultiplicativeMonoid a => a
one

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

finalStepBN ::
  forall c d i j g.
  PrimeField (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  EllipticCurve d =>
  Untwisted d i j ~ g =>
  Field g =>
  BooleanOf c ~ BooleanOf d =>
  BaseField d -> Point c -> Point d -> (Point d, g) -> g
finalStepBN :: forall c d (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
BaseField d -> Point c -> Point d -> (Point d, g) -> g
finalStepBN BaseField d
xi Point c
p Point d
q (Point d
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 @(BaseField c)
    q1 :: Point d
q1 = Natural -> BaseField d -> Point d -> Point d
forall c.
(EllipticCurve c, Field (BaseField c)) =>
Natural -> BaseField c -> Point c -> Point c
frobTwisted Natural
o BaseField d
xi Point d
q
    (Point d
t', g
f') = Point c -> Point d -> Point d -> (Point d, g)
forall d c (i :: Symbol) (j :: Symbol) g.
(EllipticCurve d, Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), BooleanOf c ~ BooleanOf d,
 Untwisted d i j ~ g) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
t Point d
q1
    q2 :: Point d
q2 = Point d -> Point d
forall a. AdditiveGroup a => a -> a
negate (Natural -> BaseField d -> Point d -> Point d
forall c.
(EllipticCurve c, Field (BaseField c)) =>
Natural -> BaseField c -> Point c -> Point c
frobTwisted Natural
o BaseField d
xi Point d
q1)
    (Point d
_, g
f'') = Point c -> Point d -> Point d -> (Point d, g)
forall d c (i :: Symbol) (j :: Symbol) g.
(EllipticCurve d, Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), BooleanOf c ~ BooleanOf d,
 Untwisted d i j ~ g) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
t' Point d
q2

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

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

frobTwisted ::
  forall c. (EllipticCurve c, Field (BaseField c)) => Natural -> BaseField c -> Point c -> Point c
frobTwisted :: forall c.
(EllipticCurve c, Field (BaseField c)) =>
Natural -> BaseField c -> Point c -> Point c
frobTwisted Natural
q BaseField c
xi (Point BaseField c
x BaseField c
y BooleanOf c
isInf) =
  if BooleanOf c
isInf then Point c
forall plane. ProjectivePlanar plane => plane
pointInf else BaseField c -> BaseField c -> Point c
forall field plane. Planar field plane => field -> field -> plane
pointXY ((BaseField c
x BaseField c -> Natural -> BaseField c
forall a b. Exponent a b => a -> b -> a
^ Natural
q) BaseField c -> BaseField c -> BaseField c
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField c
xi BaseField c -> Natural -> BaseField c
forall a b. Exponent a b => a -> b -> a
^ Natural
tx)) ((BaseField c
y BaseField c -> Natural -> BaseField c
forall a b. Exponent a b => a -> b -> a
^ Natural
q) BaseField c -> BaseField c -> BaseField c
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField c
xi BaseField c -> Natural -> BaseField c
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 ::
  Field (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  EllipticCurve d =>
  Untwisted d i j ~ g =>
  Field g =>
  BooleanOf c ~ BooleanOf d =>
  Point c -> Point d -> (Point d, g) -> (Point d, g)
additionStep :: forall c d (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
Point c -> Point d -> (Point d, g) -> (Point d, g)
additionStep Point c
p Point d
q (Point d
t, g
f) = (g -> g -> g
forall a. MultiplicativeSemigroup a => a -> a -> a
* g
f) (g -> g) -> (Point d, g) -> (Point d, g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Point c -> Point d -> Point d -> (Point d, g)
forall d c (i :: Symbol) (j :: Symbol) g.
(EllipticCurve d, Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), BooleanOf c ~ BooleanOf d,
 Untwisted d i j ~ g) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
q Point d
t

doublingStep ::
  Field (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  EllipticCurve d =>
  Untwisted d i j ~ g =>
  Field g =>
  BooleanOf c ~ BooleanOf d =>
  Point c -> (Point d, g) -> (Point d, g)
doublingStep :: forall c d (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g, BooleanOf c ~ BooleanOf d) =>
Point c -> (Point d, g) -> (Point d, g)
doublingStep Point c
p (Point d
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) -> (Point d, g) -> (Point d, g)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Point c -> Point d -> Point d -> (Point d, g)
forall d c (i :: Symbol) (j :: Symbol) g.
(EllipticCurve d, Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), BooleanOf c ~ BooleanOf d,
 Untwisted d i j ~ g) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
t Point d
t

lineFunction ::
  EllipticCurve d =>
  Field (BaseField c) =>
  Field (BaseField d) =>
  Scale (BaseField c) (BaseField d) =>
  BooleanOf c ~ BooleanOf d =>
  Untwisted d i j ~ g =>
  Point c -> Point d -> Point d -> (Point d, g)
lineFunction :: forall d c (i :: Symbol) (j :: Symbol) g.
(EllipticCurve d, Field (BaseField c), Field (BaseField d),
 Scale (BaseField c) (BaseField d), BooleanOf c ~ BooleanOf d,
 Untwisted d i j ~ g) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction (Point BaseField c
x BaseField c
y BooleanOf c
isInf) (Point BaseField d
x1 BaseField d
y1 BooleanOf d
isInf1) (Point BaseField d
x2 BaseField d
y2 BooleanOf d
isInf2) =
  if BooleanOf d
BooleanOf c
isInf BooleanOf d -> BooleanOf d -> BooleanOf d
forall b. BoolType b => b -> b -> b
|| BooleanOf d
isInf1 BooleanOf d -> BooleanOf d -> BooleanOf d
forall b. BoolType b => b -> b -> b
|| BooleanOf d
isInf2 then (Point d
forall plane. ProjectivePlanar plane => plane
pointInf, Ext3 (BaseField d) i -> Ext3 (BaseField d) i -> Untwisted d i j
forall f (e :: Symbol). f -> f -> Ext2 f e
Ext2 (BaseField d -> BaseField d -> BaseField d -> Ext3 (BaseField d) i
forall f (e :: Symbol). f -> f -> f -> Ext3 f e
Ext3 BaseField d
forall a. MultiplicativeMonoid a => a
one BaseField d
forall a. AdditiveMonoid a => a
zero BaseField d
forall a. AdditiveMonoid a => a
zero) Ext3 (BaseField d) i
forall a. AdditiveMonoid a => a
zero)
  else if BaseField d
x1 BaseField d -> BaseField d -> BooleanOf d
forall b a. Eq b a => a -> a -> b
/= BaseField d
x2 then (BaseField d -> BaseField d -> Point d
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField d
x3 BaseField d
y3, BaseField c -> BaseField d -> BaseField d -> Untwisted d 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 (BaseField c -> BaseField c
forall a. AdditiveGroup a => a -> a
negate BaseField c
y) (BaseField c
x BaseField c -> BaseField d -> BaseField d
forall b a. Scale b a => b -> a -> a
`scale` BaseField d
l) (BaseField d
y1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
l BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField d
x1))
  else if BaseField d
y1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField d
y2 BaseField d -> BaseField d -> BooleanOf d
forall b a. Eq b a => a -> a -> b
== BaseField d
forall a. AdditiveMonoid a => a
zero then (Point d
forall plane. ProjectivePlanar plane => plane
pointInf, BaseField c -> BaseField d -> BaseField d -> Untwisted d 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 BaseField c
x (BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a
negate BaseField d
x1) BaseField d
forall a. AdditiveMonoid a => a
zero)
  else (BaseField d -> BaseField d -> Point d
forall field plane. Planar field plane => field -> field -> plane
pointXY BaseField d
x3' BaseField d
y3', BaseField c -> BaseField d -> BaseField d -> Untwisted d 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 (BaseField c -> BaseField c
forall a. AdditiveGroup a => a -> a
negate BaseField c
y) (BaseField c
x BaseField c -> BaseField d -> BaseField d
forall b a. Scale b a => b -> a -> a
`scale` BaseField d
l') (BaseField d
y1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
l' BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField d
x1))
  where
    l :: BaseField d
l   = (BaseField d
y2 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
y1) BaseField d -> BaseField d -> BaseField d
forall a. Field a => a -> a -> a
// (BaseField d
x2 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x1)
    x3 :: BaseField d
x3  = BaseField d
l BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField d
l BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x2
    y3 :: BaseField d
y3  = BaseField d
l BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField d
x1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x3) BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
y1
    x12 :: BaseField d
x12 = BaseField d
x1 BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField d
x1
    l' :: BaseField d
l'  = (BaseField d
x12 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField d
x12 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField d
x12) BaseField d -> BaseField d -> BaseField d
forall a. Field a => a -> a -> a
// (BaseField d
y1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField d
y1)
    x3' :: BaseField d
x3' = BaseField d
l' BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* BaseField d
l' BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x2
    y3' :: BaseField d
y3' = BaseField d
l' BaseField d -> BaseField d -> BaseField d
forall a. MultiplicativeSemigroup a => a -> a -> a
* (BaseField d
x1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
x3') BaseField d -> BaseField d -> BaseField d
forall a. AdditiveGroup a => a -> a -> a
- BaseField d
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)