{-# 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             (EllipticCurve (..), PointCompressed, compress)
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
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

plonkupProve :: forall p i n l c1 c2 ts core .
    ( KnownNat n
    , KnownNat (PlonkupPolyExtendedLength n)
    , Foldable l
    , Ord (BaseField c1)
    , AdditiveGroup (BaseField c1)
    , Arithmetic (ScalarField c1)
    , ToTranscript ts Word8
    , ToTranscript ts (ScalarField c1)
    , ToTranscript ts (PointCompressed c1)
    , FromTranscript ts (ScalarField c1)
    , CoreFunction c1 core
    ) => PlonkupProverSetup p i n l c1 c2 -> (PlonkupWitnessInput p i c1, PlonkupProverSecret c1) -> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
plonkupProve :: forall {k} {k1} {k1} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Nat) (l :: Type -> Type) (c1 :: k) (c2 :: k1) ts
       (core :: k1).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n), Foldable l,
 Ord (BaseField c1), AdditiveGroup (BaseField c1),
 Arithmetic (ScalarField c1), ToTranscript ts Word8,
 ToTranscript ts (ScalarField c1),
 ToTranscript ts (PointCompressed c1),
 FromTranscript ts (ScalarField c1), CoreFunction c1 core) =>
PlonkupProverSetup p i n l c1 c2
-> (PlonkupWitnessInput p i c1, PlonkupProverSecret c1)
-> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
plonkupProve PlonkupProverSetup {Vector (Point c1)
ScalarField c1
PolyVec (ScalarField c1) n
PlonkupRelation p i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation p i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
omega :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> ScalarField c1
k1 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> ScalarField c1
k2 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> ScalarField c1
gs :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> Vector (Point c1)
sigma1s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2
-> PlonkupRelation p i n l (ScalarField c1)
polynomials :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type) (n :: Nat)
       (l :: Type -> Type) (c1 :: k1) (c2 :: k2).
PlonkupProverSetup p i n l c1 c2 -> PlonkupCircuitPolynomials n c1
..}
        (PlonkupWitnessInput p (ScalarField c1)
wExtra i (ScalarField c1)
wInput, PlonkupProverSecret Vector 19 (ScalarField c1)
ps)
    = (l (ScalarField c1) -> PlonkupInput l c1
forall {k} (l :: Type -> Type) (c :: k).
l (ScalarField c) -> PlonkupInput l c
PlonkupInput l (ScalarField c1)
wPub, PlonkupProof {ScalarField c1
Point c1
cmA :: Point c1
cmB :: Point c1
cmC :: Point c1
cmF :: Point c1
cmH1 :: Point c1
cmH2 :: Point c1
cmZ1 :: Point c1
cmZ2 :: Point c1
cmQlow :: Point c1
cmQmid :: Point c1
cmQhigh :: Point c1
a_xi :: ScalarField c1
b_xi :: ScalarField c1
c_xi :: ScalarField c1
s1_xi :: ScalarField c1
s2_xi :: ScalarField c1
f_xi :: ScalarField c1
t_xi :: ScalarField c1
t_xi' :: ScalarField c1
z1_xi' :: ScalarField c1
z2_xi' :: ScalarField c1
h1_xi' :: ScalarField c1
h2_xi :: ScalarField c1
l1_xi :: ScalarField c1
proof1 :: Point c1
proof2 :: Point c1
cmA :: Point c1
cmB :: Point c1
cmC :: Point c1
cmF :: Point c1
cmH1 :: Point c1
cmH2 :: Point c1
cmZ1 :: Point c1
cmZ2 :: Point c1
cmQlow :: Point c1
cmQmid :: Point c1
cmQhigh :: Point c1
proof1 :: Point c1
proof2 :: Point c1
a_xi :: ScalarField c1
b_xi :: ScalarField c1
c_xi :: ScalarField c1
s1_xi :: ScalarField c1
s2_xi :: ScalarField c1
f_xi :: ScalarField c1
t_xi :: ScalarField c1
t_xi' :: ScalarField c1
z1_xi' :: ScalarField c1
z2_xi' :: ScalarField c1
h1_xi' :: ScalarField c1
h2_xi :: ScalarField c1
l1_xi :: ScalarField c1
..}, PlonkupProverTestInfo {ScalarField c1
PolyVec (ScalarField c1) n
PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
qlX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
zhX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
w1 :: PolyVec (ScalarField c1) n
w2 :: PolyVec (ScalarField c1) n
w3 :: PolyVec (ScalarField c1) n
piX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
aX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
bX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
cX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
fX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
beta :: ScalarField c1
gamma :: ScalarField c1
delta :: ScalarField c1
epsilon :: ScalarField c1
omegas :: PolyVec (ScalarField c1) n
omegas' :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
grandProduct1 :: PolyVec (ScalarField c1) n
z1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
alpha :: ScalarField c1
qX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qlowX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmidX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qhighX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
xi :: ScalarField c1
rX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
qlX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
aX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
bX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
cX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
piX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
fX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
zhX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qlowX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmidX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qhighX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
rX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
alpha :: ScalarField c1
beta :: ScalarField c1
gamma :: ScalarField c1
delta :: ScalarField c1
epsilon :: ScalarField c1
xi :: ScalarField c1
omegas :: PolyVec (ScalarField c1) n
omegas' :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
grandProduct1 :: PolyVec (ScalarField c1) n
w1 :: PolyVec (ScalarField c1) n
w2 :: PolyVec (ScalarField c1) n
w3 :: PolyVec (ScalarField c1) n
..})
    where
        (@) :: forall size . (KnownNat size) => PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size
        @ :: forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarField c1) size
-> PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size
(@) PolyVec (ScalarField c1) size
a PolyVec (ScalarField c1) size
b = Poly (ScalarField c1) -> PolyVec (ScalarField c1) size
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Poly c -> PolyVec c size
poly2vec (Poly (ScalarField c1) -> PolyVec (ScalarField c1) size)
-> Poly (ScalarField c1) -> PolyVec (ScalarField c1) size
forall a b. (a -> b) -> a -> b
$ forall (curve :: k) (core :: k1) f.
(CoreFunction curve core, f ~ ScalarField curve, Field f, Eq f) =>
Poly f -> Poly f -> Poly f
forall {k} {k1} (curve :: k) (core :: k1) f.
(CoreFunction curve core, f ~ ScalarField curve, Field f, Eq f) =>
Poly f -> Poly f -> Poly f
polyMul @c1 @core (PolyVec (ScalarField c1) size -> Poly (ScalarField c1)
forall c (size :: Nat). (Ring c, Eq c) => PolyVec c size -> Poly c
vec2poly PolyVec (ScalarField c1) size
a) (PolyVec (ScalarField c1) size -> Poly (ScalarField c1)
forall c (size :: Nat). (Ring c, Eq c) => PolyVec c size -> Poly c
vec2poly PolyVec (ScalarField c1) size
b)

        PlonkupCircuitPolynomials {PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qlX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qrX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qoX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qcX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qkX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s1X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s2X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s3X :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
tX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qlX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qrX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qoX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qmX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qcX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qkX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s1X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s2X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s3X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
tX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
..} = PlonkupCircuitPolynomials n c1
polynomials
        secret :: Nat -> ScalarField c1
secret Nat
i = Vector 19 (ScalarField c1)
ps Vector 19 (ScalarField c1) -> Nat -> ScalarField c1
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 (ScalarField c1) (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 (ScalarField c1) n
w1, PolyVec (ScalarField c1) n
w2, PolyVec (ScalarField c1) n
w3) = PlonkupRelation p i n l (ScalarField c1)
-> p (ScalarField c1)
-> i (ScalarField c1)
-> (PolyVec (ScalarField c1) n, PolyVec (ScalarField c1) n,
    PolyVec (ScalarField c1) 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 (ScalarField c1)
relation p (ScalarField c1)
wExtra i (ScalarField c1)
wInput
        wPub :: l (ScalarField c1)
wPub = PlonkupRelation p i n l (ScalarField c1)
-> p (ScalarField c1) -> i (ScalarField c1) -> l (ScalarField c1)
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 (ScalarField c1)
relation p (ScalarField c1)
wExtra i (ScalarField c1)
wInput

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

        -- Is this really correct?
        -- How is \(n\) related to the length of public input?
        pi :: PolyVec (ScalarField c1) n
pi  = forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @_ @n (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarField c1))] -> Vector (ScalarField c1))
-> [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ (ScalarField c1 -> [ScalarField c1])
-> l (ScalarField c1) -> [ScalarField c1]
forall m a. Monoid m => (a -> m) -> l a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\ScalarField c1
x -> [ScalarField c1 -> ScalarField c1
forall a. AdditiveGroup a => a -> a
negate ScalarField c1
x]) l (ScalarField c1)
wPub
        piX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
piX = ScalarField c1
-> PolyVec (ScalarField c1) n
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
pi  :: PlonkupPolyExtended n c1

        -- Round 1

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

        com :: Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
com = forall (curve :: k) (core :: k1) f (size :: Nat).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
forall {k} {k1} (curve :: k) (core :: k1) f (size :: Nat).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
msm @c1 @core @_ @(PlonkupPolyExtendedLength n)
        cmA :: Point c1
cmA = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
aX
        cmB :: Point c1
cmB = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
bX
        cmC :: Point c1
cmC = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
cX

        -- Round 2

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

        t_zeta :: PolyVec (ScalarField c1) n
t_zeta = PlonkupRelation p i n l (ScalarField c1)
-> PolyVec (ScalarField c1) 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 (ScalarField c1)
relation
        f_zeta :: PolyVec (ScalarField c1) n
f_zeta = [Item (PolyVec (ScalarField c1) n)] -> PolyVec (ScalarField c1) n
forall l. IsList l => [Item l] -> l
fromList ([Item (PolyVec (ScalarField c1) n)] -> PolyVec (ScalarField c1) n)
-> [Item (PolyVec (ScalarField c1) n)]
-> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ (ScalarField c1
 -> ScalarField c1 -> ScalarField c1 -> ScalarField c1)
-> [ScalarField c1]
-> [ScalarField c1]
-> [ScalarField c1]
-> [ScalarField c1]
forall a b c d. (a -> b -> c -> d) -> [a] -> [b] -> [c] -> [d]
zipWith3 (\ScalarField c1
lk ScalarField c1
ti ScalarField c1
ai -> ScalarField c1 -> ScalarField c1 -> Bool -> ScalarField c1
forall a. a -> a -> Bool -> a
bool ScalarField c1
ti ScalarField c1
ai (ScalarField c1
lk ScalarField c1 -> ScalarField c1 -> Bool
forall a. Eq a => a -> a -> Bool
== ScalarField c1
forall a. MultiplicativeMonoid a => a
one)) (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)])
-> PolyVec (ScalarField c1) n
-> [Item (PolyVec (ScalarField c1) n)]
forall a b. (a -> b) -> a -> b
$ PlonkupRelation p i n l (ScalarField c1)
-> PolyVec (ScalarField c1) 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 (ScalarField c1)
relation) (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)])
-> PolyVec (ScalarField c1) n
-> [Item (PolyVec (ScalarField c1) n)]
forall a b. (a -> b) -> a -> b
$ PlonkupRelation p i n l (ScalarField c1)
-> PolyVec (ScalarField c1) 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 (ScalarField c1)
relation) (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarField c1) n
w1) :: PolyVec (ScalarField c1) n

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

        s :: [Item (PolyVec (ScalarField c1) n)]
s  = [Item (PolyVec (ScalarField c1) n)]
-> [Item (PolyVec (ScalarField c1) n)]
-> [Item (PolyVec (ScalarField c1) n)]
forall a. Ord a => [a] -> [a] -> [a]
sortByList (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarField c1) n
f_zeta [Item (PolyVec (ScalarField c1) n)]
-> [Item (PolyVec (ScalarField c1) n)]
-> [Item (PolyVec (ScalarField c1) n)]
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarField c1) n
t_zeta) (PolyVec (ScalarField c1) n -> [Item (PolyVec (ScalarField c1) n)]
forall l. IsList l => l -> [Item l]
toList PolyVec (ScalarField c1) n
t_zeta)
        h1 :: PolyVec (ScalarField c1) n
h1 = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ (Int -> ScalarField c1 -> Bool)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. (Int -> a -> Bool) -> Vector a -> Vector a
V.ifilter (\Int
i ScalarField c1
_ -> Int -> Bool
forall a. Integral a => a -> Bool
odd Int
i) (Vector (ScalarField c1) -> Vector (ScalarField c1))
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall l. IsList l => [Item l] -> l
fromList [Item (Vector (ScalarField c1))]
[Item (PolyVec (ScalarField c1) n)]
s  :: PolyVec (ScalarField c1) n
        h2 :: PolyVec (ScalarField c1) n
h2 = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ (Int -> ScalarField c1 -> Bool)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. (Int -> a -> Bool) -> Vector a -> Vector a
V.ifilter (\Int
i ScalarField c1
_ -> Int -> Bool
forall a. Integral a => a -> Bool
even Int
i) (Vector (ScalarField c1) -> Vector (ScalarField c1))
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall l. IsList l => [Item l] -> l
fromList [Item (Vector (ScalarField c1))]
[Item (PolyVec (ScalarField c1) n)]
s :: PolyVec (ScalarField c1) n

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

        cmF :: Point c1
cmF  = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
fX
        cmH1 :: Point c1
cmH1 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h1X
        cmH2 :: Point c1
cmH2 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h2X

        -- Round 3

        ts2 :: ts
ts2 = ts
ts1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmF
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmH1
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmH2
        beta :: ScalarField c1
beta    = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
1 :: Word8))
        gamma :: ScalarField c1
gamma   = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
2 :: Word8))
        delta :: ScalarField c1
delta   = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
3 :: Word8))
        epsilon :: ScalarField c1
epsilon = ts -> ScalarField c1
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 (ScalarField c1) n
omegas  = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ Int
-> (ScalarField c1 -> ScalarField c1)
-> ScalarField c1
-> Vector (ScalarField c1)
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n) (ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega) ScalarField c1
omega
        omegas' :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
omegas' = Vector (ScalarField c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1)
 -> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n))
-> Vector (ScalarField c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall a b. (a -> b) -> a -> b
$ Int
-> (ScalarField c1 -> ScalarField c1)
-> ScalarField c1
-> Vector (ScalarField c1)
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)) (ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega) ScalarField c1
forall a. MultiplicativeMonoid a => a
one

        cumprod :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
        cumprod :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
cumprod = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> (PolyVec (ScalarField c1) n -> Vector (ScalarField c1))
-> PolyVec (ScalarField c1) n
-> PolyVec (ScalarField c1) n
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ScalarField c1 -> ScalarField c1 -> ScalarField c1)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. (a -> a -> a) -> Vector a -> Vector a
V.scanl1' ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (Vector (ScalarField c1) -> Vector (ScalarField c1))
-> (PolyVec (ScalarField c1) n -> Vector (ScalarField c1))
-> PolyVec (ScalarField c1) n
-> Vector (ScalarField c1)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec

        rotR :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
        rotR :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
rotR PolyVec (ScalarField c1) n
p = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
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 (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p) Vector (ScalarField c1)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Vector a -> Vector a -> Vector a
V.++ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
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 (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p)

        rotL :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
        rotL :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
rotL PolyVec (ScalarField c1) n
p = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Int -> Vector a -> Vector a
V.drop Int
1 (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p) Vector (ScalarField c1)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Vector a -> Vector a -> Vector a
V.++ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Int -> Vector a -> Vector a
V.take Int
1 (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p)

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

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

        cmZ1 :: Point c1
cmZ1 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z1X
        cmZ2 :: Point c1
cmZ2 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z2X

        -- Round 4

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

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

        cmQlow :: Point c1
cmQlow = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qlowX
        cmQmid :: Point c1
cmQmid = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qmidX
        cmQhigh :: Point c1
cmQhigh = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qhighX

        -- Round 5

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

        a_xi :: ScalarField c1
a_xi    = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
aX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        b_xi :: ScalarField c1
b_xi    = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
bX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        c_xi :: ScalarField c1
c_xi    = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
cX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        s1_xi :: ScalarField c1
s1_xi   = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s1X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        s2_xi :: ScalarField c1
s2_xi   = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
s2X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        f_xi :: ScalarField c1
f_xi    = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
fX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        t_xi :: ScalarField c1
t_xi    = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        t_xi' :: ScalarField c1
t_xi'   = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
tX PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega)
        z1_xi' :: ScalarField c1
z1_xi'  = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z1X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega)
        z2_xi' :: ScalarField c1
z2_xi'  = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
z2X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega)
        h1_xi' :: ScalarField c1
h1_xi'  = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h1X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` (ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega)
        h2_xi :: ScalarField c1
h2_xi   = PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
h2X PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        lag1_xi :: ScalarField c1
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 ScalarField c1
omega PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        l1_xi :: ScalarField c1
l1_xi   = ScalarField c1
forall a. MultiplicativeMonoid a => a
one ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. Field a => a -> a -> a
// (Nat -> ScalarField c1 -> ScalarField c1
forall b a. Scale b a => b -> a -> a
scale Nat
n ScalarField c1
forall a. MultiplicativeMonoid a => a
one ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c1
omega))

        -- Round 6

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

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

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

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

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

        proof1 :: Point c1
proof1 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
proofX1
        proof2 :: Point c1
proof2 = Vector (Point c1)
gs Vector (Point c1)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> Point c1
`com` PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
proofX2