{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Plonkup.Verifier
    ( module ZkFold.Base.Protocol.Plonkup.Verifier.Commitments
    , module ZkFold.Base.Protocol.Plonkup.Verifier.Setup
    , plonkupVerify
    ) where

import           Data.Word                                           (Word8)
import           GHC.IsList                                          (IsList (..))
import           Prelude                                             hiding (Num (..), drop, length, sum, take, (!!),
                                                                      (/), (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.Polynomials.Univariate          hiding (qr)
import           ZkFold.Base.Protocol.NonInteractiveProof            hiding (verify)
import           ZkFold.Base.Protocol.Plonkup.Input
import           ZkFold.Base.Protocol.Plonkup.Internal
import           ZkFold.Base.Protocol.Plonkup.Proof
import           ZkFold.Base.Protocol.Plonkup.Verifier.Commitments
import           ZkFold.Base.Protocol.Plonkup.Verifier.Setup
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

plonkupVerify :: forall p i n l c1 c2 ts .
    ( KnownNat n
    , KnownNat (PlonkupPolyExtendedLength n)
    , Foldable l
    , Pairing c1 c2
    , Ord (BaseField c1)
    , AdditiveGroup (BaseField c1)
    , Arithmetic (ScalarField c1)
    , ToTranscript ts Word8
    , ToTranscript ts (ScalarField c1)
    , ToTranscript ts (PointCompressed c1)
    , FromTranscript ts (ScalarField c1)
    ) => PlonkupVerifierSetup p i n l c1 c2 -> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
plonkupVerify :: forall {k} {k1} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k) (c2 :: k1) ts.
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Foldable l,
 Pairing c1 c2, Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1)) =>
PlonkupVerifierSetup p i n l c1 c2
-> PlonkupInput l c1 -> PlonkupProof c1 -> Bool
plonkupVerify
    PlonkupVerifierSetup {ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PolyVec (ScalarField c1) n
PlonkupRelation p i n l (ScalarField c1)
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation p i n l (ScalarField c1)
commitments :: PlonkupCircuitCommitments c1
omega :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> ScalarField c1
k1 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> ScalarField c1
k2 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> ScalarField c1
h1 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> Point c2
sigma1s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2
-> PlonkupRelation p i n l (ScalarField c1)
commitments :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupVerifierSetup p i n l c1 c2 -> PlonkupCircuitCommitments c1
..}
    (PlonkupInput l (ScalarField c1)
wPub)
    (PlonkupProof {ScalarField c1
Point c1
cmA :: Point c1
cmB :: Point c1
cmC :: Point c1
cmF :: Point c1
cmH1 :: Point c1
cmH2 :: Point c1
cmZ1 :: Point c1
cmZ2 :: Point c1
cmQlow :: Point c1
cmQmid :: Point c1
cmQhigh :: Point c1
proof1 :: Point c1
proof2 :: Point c1
a_xi :: ScalarField c1
b_xi :: ScalarField c1
c_xi :: ScalarField c1
s1_xi :: ScalarField c1
s2_xi :: ScalarField c1
f_xi :: ScalarField c1
t_xi :: ScalarField c1
t_xi' :: ScalarField c1
z1_xi' :: ScalarField c1
z2_xi' :: ScalarField c1
h1_xi' :: ScalarField c1
h2_xi :: ScalarField c1
l1_xi :: ScalarField c1
cmA :: forall {k} (c :: k). PlonkupProof c -> Point c
cmB :: forall {k} (c :: k). PlonkupProof c -> Point c
cmC :: forall {k} (c :: k). PlonkupProof c -> Point c
cmF :: forall {k} (c :: k). PlonkupProof c -> Point c
cmH1 :: forall {k} (c :: k). PlonkupProof c -> Point c
cmH2 :: forall {k} (c :: k). PlonkupProof c -> Point c
cmZ1 :: forall {k} (c :: k). PlonkupProof c -> Point c
cmZ2 :: forall {k} (c :: k). PlonkupProof c -> Point c
cmQlow :: forall {k} (c :: k). PlonkupProof c -> Point c
cmQmid :: forall {k} (c :: k). PlonkupProof c -> Point c
cmQhigh :: forall {k} (c :: k). PlonkupProof c -> Point c
proof1 :: forall {k} (c :: k). PlonkupProof c -> Point c
proof2 :: forall {k} (c :: k). PlonkupProof c -> Point c
a_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
b_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
c_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
s1_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
s2_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
f_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
t_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
t_xi' :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
z1_xi' :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
z2_xi' :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
h1_xi' :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
h2_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
l1_xi :: forall {k} (c :: k). PlonkupProof c -> ScalarField c
..}) = TargetGroup c1 c2
p1 TargetGroup c1 c2 -> TargetGroup c1 c2 -> Bool
forall a. Eq a => a -> a -> Bool
== TargetGroup c1 c2
p2
    where
        PlonkupCircuitCommitments {Point c1
cmQl :: Point c1
cmQr :: Point c1
cmQo :: Point c1
cmQm :: Point c1
cmQc :: Point c1
cmQk :: Point c1
cmS1 :: Point c1
cmS2 :: Point c1
cmS3 :: Point c1
cmT1 :: Point c1
cmQl :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmQr :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmQo :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmQm :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmQc :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmQk :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmS1 :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmS2 :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmS3 :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
cmT1 :: forall {k} (c :: k). PlonkupCircuitCommitments c -> Point c
..} = PlonkupCircuitCommitments c1
commitments

        n :: Nat
n = forall (n :: Nat). KnownNat n => Nat
value @n

        -- Step 4: Compute challenges

        ts1 :: ts
ts1   = ts
forall a. Monoid a => a
mempty
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmA
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmB
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmC :: ts

        ts2 :: ts
ts2 = ts
ts1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmF
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmH1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmH2
        beta :: ScalarField c2
beta    = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
1 :: Word8))
        gamma :: ScalarField c2
gamma   = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
2 :: Word8))
        delta :: ScalarField c2
delta   = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
3 :: Word8))
        epsilon :: ScalarField c2
epsilon = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
4 :: Word8))

        ts3 :: ts
ts3 = ts
ts2
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmZ1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmZ2
        alpha :: ScalarField c2
alpha  = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts3
        alpha2 :: ScalarField c2
alpha2 = ScalarField c2
alpha ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha
        alpha3 :: ScalarField c2
alpha3 = ScalarField c2
alpha2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha
        alpha4 :: ScalarField c2
alpha4 = ScalarField c2
alpha3 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha
        alpha5 :: ScalarField c2
alpha5 = ScalarField c2
alpha4 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha

        ts4 :: ts
ts4 = ts
ts3
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmQlow
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmQmid
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmQhigh
        xi :: ScalarField c2
xi = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts4

        ts5 :: ts
ts5 = ts
ts4
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
a_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
b_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
c_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
s1_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
s2_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
f_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
t_xi
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
t_xi'
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
z1_xi'
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
z2_xi'
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
h1_xi'
            ts -> ScalarField c2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
ScalarField c2
h2_xi
        v :: ScalarField c2
v = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts5
        vn :: Nat -> ScalarField c2
vn Nat
i = ScalarField c2
v ScalarField c2 -> Nat -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^ (Nat
i :: Natural)

        ts6 :: ts
ts6 = ts
ts5
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
proof1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
proof2
        eta :: ScalarField c2
eta = ts -> ScalarField c2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts6

        -- Step 5: Compute zero polynomial evaluation
        zhX_xi :: ScalarField c1
zhX_xi = forall c (n :: Nat) (size :: Nat).
(Field c, KnownNat n, KnownNat size, Eq c) =>
PolyVec c size
polyVecZero @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) PolyVec (ScalarField c2) (PlonkupPolyExtendedLength n)
-> ScalarField c2 -> ScalarField c2
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c2
xi :: ScalarField c1

        -- Step 6: Compute Lagrange polynomial evaluation
        lagrange1_xi :: ScalarField c2
lagrange1_xi = forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Nat -> c -> PolyVec c size
polyVecLagrange @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) Nat
1 ScalarField c1
omega PolyVec (ScalarField c2) (PlonkupPolyExtendedLength n)
-> ScalarField c2 -> ScalarField c2
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c2
xi

        -- Step 7: Compute public polynomial evaluation
        pi_xi :: ScalarField c2
pi_xi = forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega
            (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarField c1))] -> Vector (ScalarField c1))
-> [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ (ScalarField c2 -> [ScalarField c2])
-> l (ScalarField c2) -> [ScalarField c2]
forall m a. Monoid m => (a -> m) -> l a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\ScalarField c2
x -> [ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a
negate ScalarField c2
x]) l (ScalarField c1)
l (ScalarField c2)
wPub)
            PolyVec (ScalarField c2) (PlonkupPolyExtendedLength n)
-> ScalarField c2 -> ScalarField c2
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c2
xi

        -- Step 8: Compute the public table commitment
        cmT_zeta :: Point c1
cmT_zeta = Point c1
cmT1

        -- Step 9: Compute r0
        r0 :: ScalarField c2
r0 = ScalarField c2
pi_xi
            ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c2
alpha ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s1_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
b_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
c_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
z1_xi'
            ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c2
alpha2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
lagrange1_xi
            ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c2
alpha4 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
z2_xi' ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
epsilon ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
forall a. MultiplicativeMonoid a => a
one ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
h2_xi) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
epsilon ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
forall a. MultiplicativeMonoid a => a
one ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
h2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
h1_xi')
            ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c2
alpha5 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
lagrange1_xi

        -- Step 10: Compute D
        d :: Point c1
d =
                (ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
b_xi) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQm Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
a_xi ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQl Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
b_xi ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQr Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
c_xi ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQo Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Point c1
cmQc
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
b_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
k1 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
c_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
k2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
lagrange1_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha2) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmZ1
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveGroup a => a -> a -> a
- ((ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s1_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
b_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
gamma) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
beta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
z1_xi') ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmS3
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c1
ScalarField c2
f_xi) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha3) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQk
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarField c2
forall a. MultiplicativeMonoid a => a
one ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
epsilon ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
f_xi) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
epsilon ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
forall a. MultiplicativeMonoid a => a
one ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
t_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
t_xi') ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha4 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
lagrange1_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha5) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmZ2
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarField c1
ScalarField c2
z2_xi' ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
epsilon ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c2
forall a. MultiplicativeMonoid a => a
one ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta) ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
h2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
delta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
h1_xi') ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
alpha4) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmH1
              Point c1 -> Point c1 -> Point c1
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c1
zhX_xi ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` (Point c1
cmQlow Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
xiScalarField c2 -> Nat -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQmid Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
xiScalarField c2 -> Nat -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^(Nat
2Nat -> Nat -> Nat
forall a. MultiplicativeSemigroup a => a -> a -> a
*Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
4)) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmQhigh)

        -- Step 11: Compute F
        f :: Point c1
f = Point c1
d
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
v ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmA
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
2 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmB
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
3 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmC
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
4 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmS1
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
5 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmS2
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
6 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmF
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
7 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmT_zeta
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
8 ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmH2
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
eta ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmZ1
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
v) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmT_zeta
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarField c2
vn Nat
2) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmZ2
            Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarField c2
vn Nat
3) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
cmH1

        -- Step 12: Compute E
        e :: Point c1
e = (
                ScalarField c2 -> ScalarField c2
forall a. AdditiveGroup a => a -> a
negate ScalarField c2
r0 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
v ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
a_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
b_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
3 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
c_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
4 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s1_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
5 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
s2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
6 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
f_xi
                ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
7 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
t_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarField c2
vn Nat
8 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
h2_xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
z1_xi' ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
v ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
t_xi' ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarField c2
vn Nat
2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
z2_xi' ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarField c2
vn Nat
3 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
h1_xi'
            ) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen

        -- Step 13: Compute the pairing
        p1 :: TargetGroup c1 c2
p1 = Point c1 -> Point c2 -> TargetGroup c1 c2
forall {k} {k1} (curve1 :: k) (curve2 :: k1).
Pairing curve1 curve2 =>
Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
pairing (Point c1
proof1 Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
ScalarField c2
eta ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
proof2) Point c2
h1
        p2 :: TargetGroup c1 c2
p2 = Point c1 -> Point c2 -> TargetGroup c1 c2
forall {k} {k1} (curve1 :: k) (curve2 :: k1).
Pairing curve1 curve2 =>
Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
pairing (ScalarField c1
ScalarField c2
xi ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
proof1 Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c2
eta ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c2
xi ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
ScalarField c2
omega) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
proof2 Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Point c1
f Point c1 -> Point c1 -> Point c1
forall a. AdditiveGroup a => a -> a -> a
- Point c1
e) (forall (curve :: k1). EllipticCurve curve => Point curve
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen @c2)