{-# 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 (..), Ord (..), 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

plonkupVerify :: forall p i n l g1 g2 gt ts .
    ( KnownNat n
    , KnownNat (PlonkupPolyExtendedLength n)
    , Foldable l
    , Pairing g1 g2 gt
    , Compressible g1
    , Eq (ScalarFieldOf g1)
    , Eq gt
    , ToTranscript ts Word8
    , ToTranscript ts (ScalarFieldOf g1)
    , ToTranscript ts (Compressed g1)
    , FromTranscript ts (ScalarFieldOf g1)
    ) => PlonkupVerifierSetup p i n l g1 g2 -> PlonkupInput l g1 -> PlonkupProof g1 -> Bool
plonkupVerify :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt ts.
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Foldable l,
 Pairing g1 g2 gt, Compressible g1, Eq (ScalarFieldOf g1), Eq gt,
 ToTranscript ts Word8, ToTranscript ts (ScalarFieldOf g1),
 ToTranscript ts (Compressed g1),
 FromTranscript ts (ScalarFieldOf g1)) =>
PlonkupVerifierSetup p i n l g1 g2
-> PlonkupInput l g1 -> PlonkupProof g1 -> Bool
plonkupVerify
    PlonkupVerifierSetup {g2
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
commitments :: PlonkupCircuitCommitments g1
omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> ScalarFieldOf g1
k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> ScalarFieldOf g1
k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> ScalarFieldOf g1
h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> g2
sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2.
PlonkupVerifierSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1
..}
    (PlonkupInput l (ScalarFieldOf g1)
wPub)
    (PlonkupProof {g1
ScalarFieldOf g1
cmA :: g1
cmB :: g1
cmC :: g1
cmF :: g1
cmH1 :: g1
cmH2 :: g1
cmZ1 :: g1
cmZ2 :: g1
cmQlow :: g1
cmQmid :: g1
cmQhigh :: g1
proof1 :: g1
proof2 :: g1
a_xi :: ScalarFieldOf g1
b_xi :: ScalarFieldOf g1
c_xi :: ScalarFieldOf g1
s1_xi :: ScalarFieldOf g1
s2_xi :: ScalarFieldOf g1
f_xi :: ScalarFieldOf g1
t_xi :: ScalarFieldOf g1
t_xi' :: ScalarFieldOf g1
z1_xi' :: ScalarFieldOf g1
z2_xi' :: ScalarFieldOf g1
h1_xi' :: ScalarFieldOf g1
h2_xi :: ScalarFieldOf g1
l1_xi :: ScalarFieldOf g1
cmA :: forall g. PlonkupProof g -> g
cmB :: forall g. PlonkupProof g -> g
cmC :: forall g. PlonkupProof g -> g
cmF :: forall g. PlonkupProof g -> g
cmH1 :: forall g. PlonkupProof g -> g
cmH2 :: forall g. PlonkupProof g -> g
cmZ1 :: forall g. PlonkupProof g -> g
cmZ2 :: forall g. PlonkupProof g -> g
cmQlow :: forall g. PlonkupProof g -> g
cmQmid :: forall g. PlonkupProof g -> g
cmQhigh :: forall g. PlonkupProof g -> g
proof1 :: forall g. PlonkupProof g -> g
proof2 :: forall g. PlonkupProof g -> g
a_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
b_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
c_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
s1_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
s2_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
f_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
t_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
t_xi' :: forall g. PlonkupProof g -> ScalarFieldOf g
z1_xi' :: forall g. PlonkupProof g -> ScalarFieldOf g
z2_xi' :: forall g. PlonkupProof g -> ScalarFieldOf g
h1_xi' :: forall g. PlonkupProof g -> ScalarFieldOf g
h2_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
l1_xi :: forall g. PlonkupProof g -> ScalarFieldOf g
..}) = gt
p1 gt -> gt -> Bool
forall a. Eq a => a -> a -> Bool
== gt
p2
    where
        PlonkupCircuitCommitments {g1
cmQl :: g1
cmQr :: g1
cmQo :: g1
cmQm :: g1
cmQc :: g1
cmQk :: g1
cmS1 :: g1
cmS2 :: g1
cmS3 :: g1
cmT1 :: g1
cmQl :: forall g. PlonkupCircuitCommitments g -> g
cmQr :: forall g. PlonkupCircuitCommitments g -> g
cmQo :: forall g. PlonkupCircuitCommitments g -> g
cmQm :: forall g. PlonkupCircuitCommitments g -> g
cmQc :: forall g. PlonkupCircuitCommitments g -> g
cmQk :: forall g. PlonkupCircuitCommitments g -> g
cmS1 :: forall g. PlonkupCircuitCommitments g -> g
cmS2 :: forall g. PlonkupCircuitCommitments g -> g
cmS3 :: forall g. PlonkupCircuitCommitments g -> g
cmT1 :: forall g. PlonkupCircuitCommitments g -> g
..} = PlonkupCircuitCommitments g1
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 -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmA
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmB
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmC :: ts

        ts2 :: ts
ts2 = ts
ts1
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmF
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmH1
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmH2
        beta :: ScalarFieldOf g2
beta    = ts -> ScalarFieldOf g2
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 :: ScalarFieldOf g2
gamma   = ts -> ScalarFieldOf g2
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 :: ScalarFieldOf g2
delta   = ts -> ScalarFieldOf g2
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 :: ScalarFieldOf g2
epsilon = ts -> ScalarFieldOf g2
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 -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmZ1
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmZ2
        alpha :: ScalarFieldOf g2
alpha  = ts -> ScalarFieldOf g2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts3
        alpha2 :: ScalarFieldOf g2
alpha2 = ScalarFieldOf g2
alpha ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha
        alpha3 :: ScalarFieldOf g2
alpha3 = ScalarFieldOf g2
alpha2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha
        alpha4 :: ScalarFieldOf g2
alpha4 = ScalarFieldOf g2
alpha3 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha
        alpha5 :: ScalarFieldOf g2
alpha5 = ScalarFieldOf g2
alpha4 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha

        ts4 :: ts
ts4 = ts
ts3
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQlow
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQmid
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQhigh
        xi :: ScalarFieldOf g2
xi = ts -> ScalarFieldOf g2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts4

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

        ts6 :: ts
ts6 = ts
ts5
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
proof1
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
proof2
        eta :: ScalarFieldOf g2
eta = ts -> ScalarFieldOf g2
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts6

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

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

        -- Step 7: Compute public polynomial evaluation
        pi_xi :: ScalarFieldOf g2
pi_xi = forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega
            (Vector (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) n)
-> Vector (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) n
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarFieldOf g1))] -> Vector (ScalarFieldOf g1)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarFieldOf g1))] -> Vector (ScalarFieldOf g1))
-> [Item (Vector (ScalarFieldOf g1))] -> Vector (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ (ScalarFieldOf g2 -> [ScalarFieldOf g2])
-> l (ScalarFieldOf g2) -> [ScalarFieldOf g2]
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 (\ScalarFieldOf g2
x -> [ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveGroup a => a -> a
negate ScalarFieldOf g2
x]) l (ScalarFieldOf g1)
l (ScalarFieldOf g2)
wPub)
            PolyVec (ScalarFieldOf g2) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g2 -> ScalarFieldOf g2
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g2
xi

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

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

        -- Step 10: Compute D
        d :: g1
d =
                (ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
b_xi) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQm g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQl g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
b_xi ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQr g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
c_xi ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQo g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
cmQc
              g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
gamma) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
ScalarFieldOf g2
b_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
k1 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
gamma) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
ScalarFieldOf g2
c_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
k2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
gamma) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
lagrange1_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha2) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmZ1
              g1 -> g1 -> g1
forall a. AdditiveGroup a => a -> a -> a
- ((ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
s1_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
gamma) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
ScalarFieldOf g2
b_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
s2_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
gamma) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
beta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
z1_xi') ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmS3
              g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
ScalarFieldOf g2
f_xi) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha3) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQk
              g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarFieldOf g2
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
delta) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g2
epsilon ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
f_xi) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g2
epsilon ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g2
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
delta) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
t_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
delta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
t_xi') ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha4 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
lagrange1_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha5) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmZ2
              g1 -> g1 -> g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
ScalarFieldOf g2
z2_xi' ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g2
epsilon ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g2
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
delta) ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
ScalarFieldOf g2
h2_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
delta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
h1_xi') ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
alpha4) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmH1
              g1 -> g1 -> g1
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
ScalarFieldOf g2
zhX_xi ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` (g1
cmQlow g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
xiScalarFieldOf g2 -> Nat -> ScalarFieldOf g2
forall a b. Exponent a b => a -> b -> a
^(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQmid g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
xiScalarFieldOf g2 -> Nat -> ScalarFieldOf g2
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)) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmQhigh)

        -- Step 11: Compute F
        f :: g1
f = g1
d
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
v ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmA
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
2 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmB
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
3 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmC
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
4 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmS1
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
5 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmS2
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
6 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmF
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
7 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmT_zeta
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
8 ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmH2
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmZ1
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
v) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmT_zeta
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarFieldOf g2
vn Nat
2) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmZ2
            g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarFieldOf g2
vn Nat
3) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
cmH1

        -- Step 12: Compute E
        e :: g1
e = (
                ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveGroup a => a -> a
negate ScalarFieldOf g2
r0 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
v ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
a_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
b_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
3 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
c_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
4 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
s1_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
5 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
s2_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
6 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
f_xi
                ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
7 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
t_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ Nat -> ScalarFieldOf g2
vn Nat
8 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
h2_xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
z1_xi' ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
v ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
t_xi' ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarFieldOf g2
vn Nat
2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
z2_xi' ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* Nat -> ScalarFieldOf g2
vn Nat
3 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
h1_xi'
            ) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
forall g. CyclicGroup g => g
pointGen

        -- Step 13: Compute the pairing
        p1 :: gt
p1 = g1 -> g2 -> gt
forall g1 g2 gt. Pairing g1 g2 gt => g1 -> g2 -> gt
pairing (g1
proof1 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g2
eta ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
proof2) g2
h1
        p2 :: gt
p2 = g1 -> g2 -> gt
forall g1 g2 gt. Pairing g1 g2 gt => g1 -> g2 -> gt
pairing (ScalarFieldOf g2
xi ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
proof1 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g2
eta ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g2
xi ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
ScalarFieldOf g2
omega) ScalarFieldOf g2 -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
proof2 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
f g1 -> g1 -> g1
forall a. AdditiveGroup a => a -> a -> a
- g1
e) (forall g. CyclicGroup g => g
pointGen @g2)