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

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

import           Data.Bool                               (otherwise)
import           Data.Eq                                 (Eq (..))
import           Data.Function                           (($), (.))
import           Data.Functor                            ((<$>))
import           Data.Int                                (Int8)
import           Data.Ord                                ((>))
import           Data.Tuple                              (snd)
import           Data.Type.Equality                      (type (~))
import           Numeric.Natural                         (Natural)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field
import           ZkFold.Base.Algebra.EllipticCurve.Class

-- 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 {k} (c :: k) 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), Scale (BaseField c) (BaseField d)) =>
  (Field (BaseField d), Eq (BaseField d)) =>
  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
  [Int8] -> Point c -> Point d -> g
millerAlgorithmBLS12 :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g) =>
[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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 EllipticCurve d, Field (BaseField d), Eq (BaseField d),
 Untwisted d i j ~ g, Field g) =>
Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
millerLoop Point c
p Point d
q [Int8]
xs (if Int8
x Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
> Int8
0 then Point d
q else Point d -> Point d
forall a. AdditiveGroup a => a -> a
negate Point d
q, g
forall a. MultiplicativeMonoid a => a
one)
millerAlgorithmBLS12 [Int8]
_ Point c
_ Point d
_ = g
forall a. MultiplicativeMonoid a => a
one

millerAlgorithmBN ::
  (PrimeField (BaseField c), Scale (BaseField c) (BaseField d)) =>
  (Field (BaseField d), Eq (BaseField d)) =>
  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
  BaseField d -> [Int8] -> Point c -> Point d -> g
millerAlgorithmBN :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g) =>
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g) =>
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 EllipticCurve d, Field (BaseField d), Eq (BaseField d),
 Untwisted d i j ~ g, Field g) =>
Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
millerLoop Point c
p Point d
q [Int8]
xs (if Int8
x Int8 -> Int8 -> Bool
forall a. Ord a => a -> a -> Bool
> Int8
0 then Point d
q else Point d -> Point d
forall a. AdditiveGroup a => a -> a
negate Point d
q, 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), Scale (BaseField c) (BaseField d)) =>
  (Field (BaseField d), Eq (BaseField d)) =>
  (EllipticCurve d, Untwisted d i j ~ g, Field g) =>
  BaseField d -> Point c -> Point d -> (Point d, g) -> g
finalStepBN :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(PrimeField (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), EllipticCurve d,
 Untwisted d i j ~ g, Field g) =>
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 {k} (c :: k).
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
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 {k} (c :: k).
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
t' Point d
q2

millerLoop ::
  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
  (EllipticCurve d, Field (BaseField d), Eq (BaseField d)) =>
  (Untwisted d i j ~ g, Field g) =>
  Point c -> Point d -> [Int8] -> (Point d, g) -> (Point d, g)
millerLoop :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 EllipticCurve d, Field (BaseField d), Eq (BaseField d),
 Untwisted d i j ~ g, Field g) =>
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
== 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
== 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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), Untwisted d i j ~ g,
 Field g) =>
Point c -> Point d -> (Point d, g) -> (Point d, g)
additionStep Point c
p Point d
q (Point d, g)
tf2
          | Bool
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), Untwisted d i j ~ g,
 Field g) =>
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), Untwisted d i j ~ g,
 Field g) =>
Point c -> (Point d, g) -> (Point d, g)
doublingStep Point c
p (Point d, g)
tf

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

frobTwisted ::
  forall c. Field (BaseField c) => Natural -> BaseField c -> Point c -> Point c
frobTwisted :: forall {k} (c :: k).
Field (BaseField c) =>
Natural -> BaseField c -> Point c -> Point c
frobTwisted Natural
q BaseField c
xi (Point BaseField c
x BaseField c
y) = BaseField c -> BaseField c -> Point c
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point ((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
frobTwisted Natural
_ BaseField c
_ Point c
_ = Point c
forall {k} (curve :: k). Point curve
Inf

additionStep ::
  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
  (Field (BaseField d), Eq (BaseField d)) =>
  (Untwisted d i j ~ g, Field g) =>
  Point c -> Point d -> (Point d, g) -> (Point d, g)
additionStep :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), Untwisted d i j ~ g,
 Field g) =>
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
q Point d
t

doublingStep ::
  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
  (Field (BaseField d), Eq (BaseField d)) =>
  (Untwisted d i j ~ g, Field g) =>
  Point c -> (Point d, g) -> (Point d, g)
doublingStep :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Field (BaseField d), Eq (BaseField d), Untwisted d i j ~ g,
 Field g) =>
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 {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction Point c
p Point d
t Point d
t

lineFunction ::
  (Field (BaseField c), Scale (BaseField c) (BaseField d)) =>
  (Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
  Point c -> Point d -> Point d -> (Point d, g)
lineFunction :: forall {k} {k} (c :: k) (d :: k) (i :: Symbol) (j :: Symbol) g.
(Field (BaseField c), Scale (BaseField c) (BaseField d),
 Untwisted d i j ~ g, Field (BaseField d), Eq (BaseField d)) =>
Point c -> Point d -> Point d -> (Point d, g)
lineFunction (Point BaseField c
x BaseField c
y) (Point BaseField d
x1 BaseField d
y1) (Point BaseField d
x2 BaseField d
y2)
  | BaseField d
x1 BaseField d -> BaseField d -> Bool
forall a. Eq a => a -> a -> Bool
/= BaseField d
x2 =
    (BaseField d -> BaseField d -> Point d
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point 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))
  | BaseField d
y1 BaseField d -> BaseField d -> BaseField d
forall a. AdditiveSemigroup a => a -> a -> a
+ BaseField d
y2 BaseField d -> BaseField d -> Bool
forall a. Eq a => a -> a -> Bool
== BaseField d
forall a. AdditiveMonoid a => a
zero =
    (Point d
forall {k} (curve :: k). Point curve
Inf, 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)
  | Bool
otherwise =
    (BaseField d -> BaseField d -> Point d
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point 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)
lineFunction Point c
_ Point d
_ Point d
_ = (Point d
forall {k} (curve :: k). Point curve
Inf, 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)