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

module ZkFold.Base.Protocol.Plonk.Verifier
    ( plonkVerify
    ) 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

plonkVerify :: forall p i n l g1 g2 gt ts .
    ( KnownNat 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
plonkVerify :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 g2 gt ts.
(KnownNat 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
plonkVerify
    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
            -- `transcript` compress cmF
            -- `transcript` compress cmH1
            -- `transcript` compress 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   = challenge (ts2 `transcript` (3 :: Word8))
        -- epsilon = challenge (ts2 `transcript` (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
            -- `transcript` compress 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 = alpha2 * alpha
        -- alpha4 = alpha3 * alpha
        -- alpha5 = alpha4 * 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
            -- `transcript` f_xi
            -- `transcript` t_xi
            -- `transcript` t_xi'
            ts -> ScalarFieldOf g2 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
ScalarFieldOf g2
z1_xi'
            -- `transcript` z2_xi'
            -- `transcript` h1_xi'
            -- `transcript` 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 (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => ScalarFieldOf g1) -> ScalarFieldOf g1)
-> (KnownNat ((4 * n) + 6) => ScalarFieldOf g1) -> ScalarFieldOf g1
forall a b. (a -> b) -> a -> b
$ 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) ((4 * n) + 6)
-> 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 (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => ScalarFieldOf g2) -> ScalarFieldOf g2)
-> (KnownNat ((4 * n) + 6) => ScalarFieldOf g2) -> ScalarFieldOf g2
forall a b. (a -> b) -> a -> b
$ 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) ((4 * n) + 6)
-> 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 (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => ScalarFieldOf g2) -> ScalarFieldOf g2)
-> (KnownNat ((4 * n) + 6) => ScalarFieldOf g2) -> ScalarFieldOf g2
forall a b. (a -> b) -> a -> b
$ 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) ((4 * n) + 6)
-> 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 = 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
            -- - alpha4 * z2_xi' * (epsilon * (one + delta) + delta * h2_xi) * (epsilon * (one + delta) + h2_xi + delta * h1_xi')
            -- - alpha5 * 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
            --   + ((a_xi - f_xi) * alpha3) `scale` cmQk
            --   + ((one + delta) * (epsilon + f_xi) * (epsilon * (one + delta) + t_xi + delta * t_xi') * alpha4 + lagrange1_xi * alpha5) `scale` cmZ2
            --   - (z2_xi' * (epsilon * (one + delta) + h2_xi + delta * h1_xi') * alpha4) `scale` 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
            -- + vn 6 `scale` cmF
            -- + vn 7 `scale` cmT_zeta
            -- + vn 8 `scale` 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
            -- + (eta * v) `scale` cmT_zeta
            -- + (eta * vn 2) `scale` cmZ2
            -- + (eta * vn 3) `scale` 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
+ ScalarFieldOf g2
eta 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
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)