{-# LANGUAGE AllowAmbiguousTypes #-}

module ZkFold.Base.Protocol.Plonkup.Prover
    ( module ZkFold.Base.Protocol.Plonkup.Prover.Polynomials
    , module ZkFold.Base.Protocol.Plonkup.Prover.Secret
    , module ZkFold.Base.Protocol.Plonkup.Prover.Setup
    , plonkupProve
    ) where

import           Data.Bool                                       (bool)
import qualified Data.Vector                                     as V
import           Data.Word                                       (Word8)
import           GHC.IsList                                      (IsList (..))
import           Prelude                                         hiding (Num (..), drop, length, pi, sum, take, (!!),
                                                                  (/), (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number                (KnownNat, Natural, value)
import           ZkFold.Base.Algebra.EllipticCurve.Class         (Compressible (..), CyclicGroup (..))
import           ZkFold.Base.Algebra.Polynomials.Univariate      hiding (qr)
import           ZkFold.Base.Data.Vector                         ((!!))
import           ZkFold.Base.Protocol.NonInteractiveProof
import           ZkFold.Base.Protocol.Plonkup.Input
import           ZkFold.Base.Protocol.Plonkup.Internal           (PlonkupPolyExtended, PlonkupPolyExtendedLength)
import           ZkFold.Base.Protocol.Plonkup.Proof
import           ZkFold.Base.Protocol.Plonkup.Prover.Polynomials
import           ZkFold.Base.Protocol.Plonkup.Prover.Secret
import           ZkFold.Base.Protocol.Plonkup.Prover.Setup
import           ZkFold.Base.Protocol.Plonkup.Relation           (PlonkupRelation (..))
import           ZkFold.Base.Protocol.Plonkup.Testing            (PlonkupProverTestInfo (..))
import           ZkFold.Base.Protocol.Plonkup.Utils              (sortByList)
import           ZkFold.Base.Protocol.Plonkup.Witness

plonkupProve :: forall p i n l g1 g2 ts core .
    ( KnownNat n
    , KnownNat (PlonkupPolyExtendedLength n)
    , Foldable l
    , Ord (ScalarFieldOf g1)
    , Compressible g1
    , ToTranscript ts Word8
    , ToTranscript ts (ScalarFieldOf g1)
    , ToTranscript ts (Compressed g1)
    , FromTranscript ts (ScalarFieldOf g1)
    , CoreFunction g1 core
    ) => PlonkupProverSetup p i n l g1 g2 -> (PlonkupWitnessInput p i g1, PlonkupProverSecret g1) -> (PlonkupInput l g1, PlonkupProof g1, PlonkupProverTestInfo n g1)
plonkupProve :: forall {k} {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k) ts (core :: k).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Foldable l,
 Ord (ScalarFieldOf g1), Compressible g1, ToTranscript ts Word8,
 ToTranscript ts (ScalarFieldOf g1),
 ToTranscript ts (Compressed g1),
 FromTranscript ts (ScalarFieldOf g1), CoreFunction g1 core) =>
PlonkupProverSetup p i n l g1 g2
-> (PlonkupWitnessInput p i g1, PlonkupProverSecret g1)
-> (PlonkupInput l g1, PlonkupProof g1, PlonkupProverTestInfo n g1)
plonkupProve PlonkupProverSetup {Vector g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
PlonkupCircuitPolynomials n g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
sigma1s :: PolyVec (ScalarFieldOf g1) n
sigma2s :: PolyVec (ScalarFieldOf g1) n
sigma3s :: PolyVec (ScalarFieldOf g1) n
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: PlonkupCircuitPolynomials n g1
omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> ScalarFieldOf g1
k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> ScalarFieldOf g1
k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> ScalarFieldOf g1
gs :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> Vector g1
sigma1s :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
relation :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) g1 (g2 :: k).
PlonkupProverSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1
..}
        (PlonkupWitnessInput p (ScalarFieldOf g1)
wExtra i (ScalarFieldOf g1)
wInput, PlonkupProverSecret Vector 19 (ScalarFieldOf g1)
ps)
    = (l (ScalarFieldOf g1) -> PlonkupInput l g1
forall (l :: Type -> Type) g.
l (ScalarFieldOf g) -> PlonkupInput l g
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
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
proof1 :: g1
proof2 :: 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
..}, PlonkupProverTestInfo {PolyVec (ScalarFieldOf g1) n
PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
ScalarFieldOf g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
qlX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w1 :: PolyVec (ScalarFieldOf g1) n
w2 :: PolyVec (ScalarFieldOf g1) n
w3 :: PolyVec (ScalarFieldOf g1) n
piX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
beta :: ScalarFieldOf g1
gamma :: ScalarFieldOf g1
delta :: ScalarFieldOf g1
epsilon :: ScalarFieldOf g1
omegas :: PolyVec (ScalarFieldOf g1) n
omegas' :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
grandProduct1 :: PolyVec (ScalarFieldOf g1) n
z1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
alpha :: ScalarFieldOf g1
qX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlowX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmidX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qhighX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
xi :: ScalarFieldOf g1
rX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
qlX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
piX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlowX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmidX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qhighX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
rX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
alpha :: ScalarFieldOf g1
beta :: ScalarFieldOf g1
gamma :: ScalarFieldOf g1
delta :: ScalarFieldOf g1
epsilon :: ScalarFieldOf g1
xi :: ScalarFieldOf g1
omegas :: PolyVec (ScalarFieldOf g1) n
omegas' :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
grandProduct1 :: PolyVec (ScalarFieldOf g1) n
w1 :: PolyVec (ScalarFieldOf g1) n
w2 :: PolyVec (ScalarFieldOf g1) n
w3 :: PolyVec (ScalarFieldOf g1) n
..})
    where
        (@) :: forall size . (KnownNat size) => PolyVec (ScalarFieldOf g1) size -> PolyVec (ScalarFieldOf g1) size -> PolyVec (ScalarFieldOf g1) size
        @ :: forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
(@) PolyVec (ScalarFieldOf g1) size
a PolyVec (ScalarFieldOf g1) size
b = Poly (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) size
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Poly c -> PolyVec c size
poly2vec (Poly (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) size)
-> Poly (ScalarFieldOf g1) -> PolyVec (ScalarFieldOf g1) size
forall a b. (a -> b) -> a -> b
$ forall g (core :: k) f.
(CoreFunction g core, f ~ ScalarFieldOf g, Field f, Eq f) =>
Poly f -> Poly f -> Poly f
forall {k} g (core :: k) f.
(CoreFunction g core, f ~ ScalarFieldOf g, Field f, Eq f) =>
Poly f -> Poly f -> Poly f
polyMul @g1 @core (PolyVec (ScalarFieldOf g1) size -> Poly (ScalarFieldOf g1)
forall c (size :: Nat). (Ring c, Eq c) => PolyVec c size -> Poly c
vec2poly PolyVec (ScalarFieldOf g1) size
a) (PolyVec (ScalarFieldOf g1) size -> Poly (ScalarFieldOf g1)
forall c (size :: Nat). (Ring c, Eq c) => PolyVec c size -> Poly c
vec2poly PolyVec (ScalarFieldOf g1) size
b)

        PlonkupCircuitPolynomials {PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
qrX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
qoX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
qmX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
qcX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
qkX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
s1X :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
s2X :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
s3X :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
tX :: forall (n :: Nat) g.
PlonkupCircuitPolynomials n g -> PlonkupPolyExtended n g
..} = PlonkupCircuitPolynomials n g1
polynomials
        secret :: Nat -> ScalarFieldOf g1
secret Nat
i = Vector 19 (ScalarFieldOf g1)
ps Vector 19 (ScalarFieldOf g1) -> Nat -> ScalarFieldOf g1
forall (size :: Nat) a. Vector size a -> Nat -> a
!! (Nat
i Nat -> Nat -> Nat
-! Nat
1)

        n :: Nat
n = forall (n :: Nat). KnownNat n => Nat
value @n
        zhX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX = forall c (n :: Nat) (size :: Nat).
(Field c, KnownNat n, KnownNat size, Eq c) =>
PolyVec c size
polyVecZero @_ @n @(PlonkupPolyExtendedLength n)

        (PolyVec (ScalarFieldOf g1) n
w1, PolyVec (ScalarFieldOf g1) n
w2, PolyVec (ScalarFieldOf g1) n
w3) = PlonkupRelation p i n l (ScalarFieldOf g1)
-> p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1)
-> (PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n,
    PolyVec (ScalarFieldOf g1) n)
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a
-> p a -> i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
witness PlonkupRelation p i n l (ScalarFieldOf g1)
relation p (ScalarFieldOf g1)
wExtra i (ScalarFieldOf g1)
wInput
        wPub :: l (ScalarFieldOf g1)
wPub = PlonkupRelation p i n l (ScalarFieldOf g1)
-> p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1)
-> l (ScalarFieldOf g1)
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> p a -> i a -> l a
pubInput PlonkupRelation p i n l (ScalarFieldOf g1)
relation p (ScalarFieldOf g1)
wExtra i (ScalarFieldOf g1)
wInput

        w1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w1X = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
w1 :: PlonkupPolyExtended n g1
        w2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w2X = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
w2 :: PlonkupPolyExtended n g1
        w3X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w3X = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
w3 :: PlonkupPolyExtended n g1

        -- Is this really correct?
        -- How is \(n\) related to the length of public input?
        pi :: PolyVec (ScalarFieldOf g1) n
pi  = forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @_ @n (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 g1 -> [ScalarFieldOf g1])
-> l (ScalarFieldOf g1) -> [ScalarFieldOf g1]
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 g1
x -> [ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a
negate ScalarFieldOf g1
x]) l (ScalarFieldOf g1)
wPub
        piX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
piX = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
pi  :: PlonkupPolyExtended n g1

        -- Round 1

        aX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX = ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarFieldOf g1
secret Nat
1) (Nat -> ScalarFieldOf g1
secret Nat
2) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w1X :: PlonkupPolyExtended n g1
        bX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX = ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarFieldOf g1
secret Nat
3) (Nat -> ScalarFieldOf g1
secret Nat
4) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w2X :: PlonkupPolyExtended n g1
        cX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX = ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarFieldOf g1
secret Nat
5) (Nat -> ScalarFieldOf g1
secret Nat
6) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
w3X :: PlonkupPolyExtended n g1

        com :: Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
com = forall g (core :: k) f (size :: Nat).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
forall {k} g (core :: k) f (size :: Nat).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
msm @g1 @core
        cmA :: g1
cmA = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX
        cmB :: g1
cmB = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX
        cmC :: g1
cmC = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX

        -- Round 2

        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
        -- zeta = challenge ts1 :: ScalarFieldOf g1

        t_zeta :: PolyVec (ScalarFieldOf g1) n
t_zeta = PlonkupRelation p i n l (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) n
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
t PlonkupRelation p i n l (ScalarFieldOf g1)
relation
        f_zeta :: PolyVec (ScalarFieldOf g1) n
f_zeta = [Item (PolyVec (ScalarFieldOf g1) n)]
-> PolyVec (ScalarFieldOf g1) n
forall l. IsList l => [Item l] -> l
fromList ([Item (PolyVec (ScalarFieldOf g1) n)]
 -> PolyVec (ScalarFieldOf g1) n)
-> [Item (PolyVec (ScalarFieldOf g1) n)]
-> PolyVec (ScalarFieldOf g1) n
forall a b. (a -> b) -> a -> b
$ (ScalarFieldOf g1
 -> ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1)
-> [ScalarFieldOf g1]
-> [ScalarFieldOf g1]
-> [ScalarFieldOf g1]
-> [ScalarFieldOf g1]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (\ScalarFieldOf g1
lk ScalarFieldOf g1
ti ScalarFieldOf g1
ai -> ScalarFieldOf g1 -> ScalarFieldOf g1 -> Bool -> ScalarFieldOf g1
forall a. a -> a -> Bool -> a
bool ScalarFieldOf g1
ti ScalarFieldOf g1
ai (ScalarFieldOf g1
lk ScalarFieldOf g1 -> ScalarFieldOf g1 -> Bool
forall a. Eq a => a -> a -> Bool
== ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one)) (PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList (PolyVec (ScalarFieldOf g1) n
 -> [Item (PolyVec (ScalarFieldOf g1) n)])
-> PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall a b. (a -> b) -> a -> b
$ PlonkupRelation p i n l (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) n
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qK PlonkupRelation p i n l (ScalarFieldOf g1)
relation) (PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList (PolyVec (ScalarFieldOf g1) n
 -> [Item (PolyVec (ScalarFieldOf g1) n)])
-> PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall a b. (a -> b) -> a -> b
$ PlonkupRelation p i n l (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) n
forall (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
t PlonkupRelation p i n l (ScalarFieldOf g1)
relation) (PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarFieldOf g1) n
w1) :: PolyVec (ScalarFieldOf g1) n

        fX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX = ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarFieldOf g1
secret Nat
7) (Nat -> ScalarFieldOf g1
secret Nat
8) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
f_zeta :: PlonkupPolyExtended n g1

        s :: [Item (PolyVec (ScalarFieldOf g1) n)]
s  = [Item (PolyVec (ScalarFieldOf g1) n)]
-> [Item (PolyVec (ScalarFieldOf g1) n)]
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall a. Ord a => [a] -> [a] -> [a]
sortByList (PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarFieldOf g1) n
f_zeta [Item (PolyVec (ScalarFieldOf g1) n)]
-> [Item (PolyVec (ScalarFieldOf g1) n)]
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarFieldOf g1) n
t_zeta) (PolyVec (ScalarFieldOf g1) n
-> [Item (PolyVec (ScalarFieldOf g1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarFieldOf g1) n
t_zeta)
        h1 :: PolyVec (ScalarFieldOf g1) n
h1 = 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
$ (Int -> ScalarFieldOf g1 -> Bool)
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. (Int -> a -> Bool) -> Vector a -> Vector a
V.ifilter (\Int
i ScalarFieldOf g1
_ -> Int -> Bool
forall a. Integral a => a -> Bool
odd Int
i) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
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))]
[Item (PolyVec (ScalarFieldOf g1) n)]
s  :: PolyVec (ScalarFieldOf g1) n
        h2 :: PolyVec (ScalarFieldOf g1) n
h2 = 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
$ (Int -> ScalarFieldOf g1 -> Bool)
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. (Int -> a -> Bool) -> Vector a -> Vector a
V.ifilter (\Int
i ScalarFieldOf g1
_ -> Int -> Bool
forall a. Integral a => a -> Bool
even Int
i) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
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))]
[Item (PolyVec (ScalarFieldOf g1) n)]
s :: PolyVec (ScalarFieldOf g1) n

        h1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X = ScalarFieldOf g1
-> ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Nat -> ScalarFieldOf g1
secret Nat
9) (Nat -> ScalarFieldOf g1
secret Nat
10) (Nat -> ScalarFieldOf g1
secret Nat
11) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
h1 :: PlonkupPolyExtended n g1
        h2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X = ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarFieldOf g1
secret Nat
12) (Nat -> ScalarFieldOf g1
secret Nat
13) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
h2 :: PlonkupPolyExtended n g1

        cmF :: g1
cmF  = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX
        cmH1 :: g1
cmH1 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X
        cmH2 :: g1
cmH2 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X

        -- Round 3

        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 g1
beta    = ts -> ScalarFieldOf g1
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 g1
gamma   = ts -> ScalarFieldOf g1
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 g1
delta   = ts -> ScalarFieldOf g1
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 g1
epsilon = ts -> ScalarFieldOf g1
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))

        omegas :: PolyVec (ScalarFieldOf g1) n
omegas  = 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
$ Int
-> (ScalarFieldOf g1 -> ScalarFieldOf g1)
-> ScalarFieldOf g1
-> Vector (ScalarFieldOf g1)
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n) (ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega) ScalarFieldOf g1
omega
        omegas' :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omegas' = Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g1)
 -> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n))
-> Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a b. (a -> b) -> a -> b
$ Int
-> (ScalarFieldOf g1 -> ScalarFieldOf g1)
-> ScalarFieldOf g1
-> Vector (ScalarFieldOf g1)
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @(PlonkupPolyExtendedLength n)) (ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega) ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one

        cumprod :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
        cumprod :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
cumprod = 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)
-> (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1))
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1)
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. (a -> a -> a) -> Vector a -> Vector a
V.scanl1' ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1))
-> PolyVec (ScalarFieldOf g1) n
-> Vector (ScalarFieldOf g1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec

        rotR :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
        rotR :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotR PolyVec (ScalarFieldOf g1) n
p = 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
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.drop (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @n Nat -> Nat -> Nat
-! Nat
1) (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) n
p) Vector (ScalarFieldOf g1)
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Vector a -> Vector a -> Vector a
V.++ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.take (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @n Nat -> Nat -> Nat
-! Nat
1) (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) n
p)

        rotL :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
        rotL :: PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotL PolyVec (ScalarFieldOf g1) n
p = 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
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.drop Int
1 (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) n
p) Vector (ScalarFieldOf g1)
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Vector a -> Vector a -> Vector a
V.++ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.take Int
1 (PolyVec (ScalarFieldOf g1) n -> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) n
p)

        -- TODO: check operation order
        grandProduct1 :: PolyVec (ScalarFieldOf g1) n
grandProduct1 = PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotR (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
cumprod (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a b. (a -> b) -> a -> b
$
                (PolyVec (ScalarFieldOf g1) n
w1 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
omegas) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. (PolyVec (ScalarFieldOf g1) n
w2 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k1) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
omegas) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. (PolyVec (ScalarFieldOf g1) n
w3 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ ((ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k2) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
omegas) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
./. (PolyVec (ScalarFieldOf g1) n
w1 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
sigma1s) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
./. (PolyVec (ScalarFieldOf g1) n
w2 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
sigma2s) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
./. (PolyVec (ScalarFieldOf g1) n
w3 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
sigma3s) PolyVec (ScalarFieldOf g1) n
-> ScalarFieldOf g1 -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.+ ScalarFieldOf g1
gamma)
        z1X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X = ScalarFieldOf g1
-> ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Nat -> ScalarFieldOf g1
secret Nat
14) (Nat -> ScalarFieldOf g1
secret Nat
15) (Nat -> ScalarFieldOf g1
secret Nat
16) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
grandProduct1 :: PlonkupPolyExtended n g1

        grandProduct2 :: PolyVec (ScalarFieldOf g1) n
grandProduct2 = PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotR (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
cumprod (PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n)
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a b. (a -> b) -> a -> b
$
                (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (ScalarFieldOf g1
epsilon ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
+. PolyVec (ScalarFieldOf g1) n
f_zeta)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. ((ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
+. PolyVec (ScalarFieldOf g1) n
t_zeta PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotL PolyVec (ScalarFieldOf g1) n
t_zeta)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
./. ((ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
+. PolyVec (ScalarFieldOf g1) n
h1 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n
h2)
            PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
./. ((ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
+. PolyVec (ScalarFieldOf g1) n
h2 PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) n -> PolyVec (ScalarFieldOf g1) n
rotL PolyVec (ScalarFieldOf g1) n
h1)
        z2X :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X = ScalarFieldOf g1
-> ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Nat -> ScalarFieldOf g1
secret Nat
17) (Nat -> ScalarFieldOf g1
secret Nat
18) (Nat -> ScalarFieldOf g1
secret Nat
19) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) n
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
grandProduct2 :: PlonkupPolyExtended n g1

        cmZ1 :: g1
cmZ1 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X
        cmZ2 :: g1
cmZ2 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X

        -- Round 4

        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 g1
alpha  = ts -> ScalarFieldOf g1
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts3
        alpha2 :: ScalarFieldOf g1
alpha2 = ScalarFieldOf g1
alpha ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
alpha
        alpha3 :: ScalarFieldOf g1
alpha3 = ScalarFieldOf g1
alpha2 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
alpha
        alpha4 :: ScalarFieldOf g1
alpha4 = ScalarFieldOf g1
alpha3 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
alpha
        alpha5 :: ScalarFieldOf g1
alpha5 = ScalarFieldOf g1
alpha4 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
alpha

        gammaX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
gammaX   = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV ScalarFieldOf g1
gamma PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one
        deltaX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX   = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV ScalarFieldOf g1
delta PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one
        epsilonX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
epsilonX = ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV ScalarFieldOf g1
epsilon PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one
        qX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qX = (
                (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qrX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qoX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
piX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qcX)
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear ScalarFieldOf g1
beta ScalarFieldOf g1
gamma) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k1) ScalarFieldOf g1
gamma) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k2) ScalarFieldOf g1
gamma) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
gammaX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
gammaX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s3X) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
gammaX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omegas') PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Nat -> c -> PolyVec c size
polyVecLagrange @_ @n Nat
1 ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha2
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qkX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha3
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
epsilonX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ ((PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
epsilonX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX)) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omegas')) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha4
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omegas') PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ ((PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
epsilonX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX)) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ ((PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
epsilonX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX)) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
deltaX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
.*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
omegas')) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha4
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
-> PolyVec (ScalarFieldOf g1) size
@ forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Nat -> c -> PolyVec c size
polyVecLagrange @_ @n Nat
1 ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
alpha5
            ) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX
        qlowX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlowX  = Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g1)
 -> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n))
-> Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.take (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qX
        qmidX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmidX  = Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g1)
 -> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n))
-> Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.take (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.drop (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qX
        qhighX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qhighX = Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g1)
 -> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n))
-> Vector (ScalarFieldOf g1)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a. Int -> Vector a -> Vector a
V.drop (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat
2Nat -> Nat -> Nat
forall a. MultiplicativeSemigroup a => a -> a -> a
*(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2))) (Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1))
-> Vector (ScalarFieldOf g1) -> Vector (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> Vector (ScalarFieldOf g1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qX

        cmQlow :: g1
cmQlow = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlowX
        cmQmid :: g1
cmQmid = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmidX
        cmQhigh :: g1
cmQhigh = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qhighX

        -- Round 5

        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 g1
xi = ts -> ScalarFieldOf g1
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts4

        a_xi :: ScalarFieldOf g1
a_xi    = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        b_xi :: ScalarFieldOf g1
b_xi    = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        c_xi :: ScalarFieldOf g1
c_xi    = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        s1_xi :: ScalarFieldOf g1
s1_xi   = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        s2_xi :: ScalarFieldOf g1
s2_xi   = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        f_xi :: ScalarFieldOf g1
f_xi    = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        t_xi :: ScalarFieldOf g1
t_xi    = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        t_xi' :: ScalarFieldOf g1
t_xi'   = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega)
        z1_xi' :: ScalarFieldOf g1
z1_xi'  = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega)
        z2_xi' :: ScalarFieldOf g1
z2_xi'  = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega)
        h1_xi' :: ScalarFieldOf g1
h1_xi'  = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega)
        h2_xi :: ScalarFieldOf g1
h2_xi   = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        lag1_xi :: ScalarFieldOf g1
lag1_xi = forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Nat -> c -> PolyVec c size
polyVecLagrange @_ @n @(PlonkupPolyExtendedLength n) Nat
1 ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        l1_xi :: ScalarFieldOf g1
l1_xi   = ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. Field a => a -> a -> a
// (Nat -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall b a. Scale b a => b -> a -> a
scale Nat
n ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
omega))

        -- Round 6

        ts5 :: ts
ts5 = ts
ts4
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
a_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
b_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
c_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
s1_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
s2_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
f_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
t_xi
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
t_xi'
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
z1_xi'
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
z2_xi'
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
h1_xi'
            ts -> ScalarFieldOf g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarFieldOf g1
h2_xi
        v :: ScalarFieldOf g1
v = ts -> ScalarFieldOf g1
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts5

        pi_xi :: ScalarFieldOf g1
pi_xi = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
piX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi
        zhX_xi :: ScalarFieldOf g1
zhX_xi = PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
zhX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1 -> ScalarFieldOf g1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarFieldOf g1
xi

        rX :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
rX =
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* (ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
b_xi) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
a_xi PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qrX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
b_xi PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qoX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
c_xi PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
pi_xi PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qcX
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
alpha ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (((ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
b_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k1 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
c_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k2 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X
                        PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- ((ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
s1_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
b_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
s2_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
z1_xi') ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
c_xi PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s3X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
gamma)
                    )
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
alpha2 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
lag1_xi) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
alpha3 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
f_xi)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qkX
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
alpha4 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (((ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
f_xi) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
t_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
t_xi')) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X
                        PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
z2_xi' ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ((ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
h2_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
h1_xi')) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* (ScalarFieldOf g1
epsilon ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
delta)) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* (ScalarFieldOf g1
delta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
h2_xi))
                    )
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
alpha5 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
lag1_xi) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)
              PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
zhX_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qlowX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
xiScalarFieldOf g1 -> Nat -> ScalarFieldOf g1
forall a b. Exponent a b => a -> b -> a
^(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qmidX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
xiScalarFieldOf g1 -> Nat -> ScalarFieldOf g1
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 g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
qhighX)

        vn :: Nat -> ScalarFieldOf g1
vn Nat
i = ScalarFieldOf g1
v ScalarFieldOf g1 -> Nat -> ScalarFieldOf g1
forall a b. Exponent a b => a -> b -> a
^ (Nat
i :: Natural)

        proofX1 :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
proofX1 = (
                  PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
rX
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
1 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
a_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
2 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
b_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
3 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
c_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
4 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
s1_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
5 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
s2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
s2_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
6 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
fX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
f_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
7 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
t_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
8 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
h2_xi ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
            ) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one (ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a
negate ScalarFieldOf g1
xi)
        proofX2 :: PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
proofX2 = (
                  PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
z1_xi' ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
1 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
t_xi' ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
2 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
z2_xi' ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
                PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
3 ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
h1_xi' ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall a. MultiplicativeMonoid a => a
one)))
            ) PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` ScalarFieldOf g1
-> ScalarFieldOf g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one (ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a
negate (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega))

        proof1 :: g1
proof1 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
proofX1
        proof2 :: g1
proof2 = Vector g1
gs Vector g1
-> PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n) -> g1
`com` PolyVec (ScalarFieldOf g1) (PlonkupPolyExtendedLength n)
proofX2