{-# 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 (fromVector, (!!))
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 i n l c1 c2 ts core .
( KnownNat n
, KnownNat (PlonkupPolyExtendedLength n)
, 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 i n l c1 c2 -> (PlonkupWitnessInput i c1, PlonkupProverSecret c1) -> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
plonkupProve :: forall {k} {k1} {k1} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k) (c2 :: k1) ts (core :: k1).
(KnownNat n, KnownNat (PlonkupPolyExtendedLength n),
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 i n l c1 c2
-> (PlonkupWitnessInput i c1, PlonkupProverSecret c1)
-> (PlonkupInput l c1, PlonkupProof c1, PlonkupProverTestInfo n c1)
plonkupProve PlonkupProverSetup {Vector (Point c1)
ScalarField c1
PolyVec (ScalarField c1) n
PlonkupRelation 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 i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
omega :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> ScalarField c1
k1 :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> ScalarField c1
k2 :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> ScalarField c1
gs :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> Vector (Point c1)
sigma1s :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2
-> PlonkupRelation i n l (ScalarField c1)
polynomials :: forall {k1} {k2} (i :: Natural) (n :: Natural) (l :: Natural)
(c1 :: k1) (c2 :: k2).
PlonkupProverSetup i n l c1 c2 -> PlonkupCircuitPolynomials n c1
..}
(PlonkupWitnessInput Vector i (ScalarField c1)
wInput, PlonkupProverSecret Vector 19 (ScalarField c1)
ps)
= (Vector l (ScalarField c1) -> PlonkupInput l c1
forall {k} (l :: Natural) (c :: k).
Vector l (ScalarField c) -> PlonkupInput l c
PlonkupInput Vector 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 :: Natural).
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 :: Natural).
(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 :: Natural).
(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 :: Natural).
(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 :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qrX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qoX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qmX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qcX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qkX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s1X :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s2X :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s3X :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
tX :: forall {k} (n :: Natural) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
..} = PlonkupCircuitPolynomials n c1
polynomials
secret :: Natural -> ScalarField c1
secret Natural
i = Vector 19 (ScalarField c1)
ps Vector 19 (ScalarField c1) -> Natural -> ScalarField c1
forall (size :: Natural) a. Vector size a -> Natural -> a
!! (Natural
i Natural -> Natural -> Natural
-! Natural
1)
n :: Natural
n = forall (n :: Natural). KnownNat n => Natural
value @n
zhX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
zhX = forall c (n :: Natural) (size :: Natural).
(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 i n l (ScalarField c1)
-> Vector i (ScalarField c1)
-> (PolyVec (ScalarField c1) n, PolyVec (ScalarField c1) n,
PolyVec (ScalarField c1) n)
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a
-> Vector i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
witness PlonkupRelation i n l (ScalarField c1)
relation Vector i (ScalarField c1)
wInput
wPub :: Vector l (ScalarField c1)
wPub = PlonkupRelation i n l (ScalarField c1)
-> Vector i (ScalarField c1) -> Vector l (ScalarField c1)
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> Vector i a -> Vector l a
pubInput PlonkupRelation i n l (ScalarField c1)
relation Vector 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 :: Natural) (size :: Natural).
(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 :: Natural) (size :: Natural).
(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 :: Natural) (size :: Natural).
(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
pi :: PolyVec (ScalarField c1) n
pi = forall c (size :: Natural).
(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
$ Vector l (ScalarField c1) -> [ScalarField c1]
forall (size :: Natural) a. Vector size a -> [a]
fromVector (ScalarField c1 -> ScalarField c1
forall a. AdditiveGroup a => a -> a
negate (ScalarField c1 -> ScalarField c1)
-> Vector l (ScalarField c1) -> Vector l (ScalarField c1)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector 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 :: Natural) (size :: Natural).
(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
aX :: PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
aX = ScalarField c1
-> ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Natural -> ScalarField c1
secret Natural
1) (Natural -> ScalarField c1
secret Natural
2) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Natural -> ScalarField c1
secret Natural
3) (Natural -> ScalarField c1
secret Natural
4) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Natural -> ScalarField c1
secret Natural
5) (Natural -> ScalarField c1
secret Natural
6) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
forall {k} {k1} (curve :: k) (core :: k1) f (size :: Natural).
(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
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
t_zeta :: PolyVec (ScalarField c1) n
t_zeta = PlonkupRelation i n l (ScalarField c1)
-> PolyVec (ScalarField c1) n
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
t PlonkupRelation 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 i n l (ScalarField c1)
-> PolyVec (ScalarField c1) n
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
qK PlonkupRelation 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 i n l (ScalarField c1)
-> PolyVec (ScalarField c1) n
forall (i :: Natural) (n :: Natural) (l :: Natural) a.
PlonkupRelation i n l a -> PolyVec a n
t PlonkupRelation 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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Natural -> ScalarField c1
secret Natural
7) (Natural -> ScalarField c1
secret Natural
8) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural) (size :: Natural).
(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 :: Natural).
(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 :: Natural).
(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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Natural -> ScalarField c1
secret Natural
9) (Natural -> ScalarField c1
secret Natural
10) (Natural -> ScalarField c1
secret Natural
11) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural) (size :: Natural).
(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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Natural -> ScalarField c1
secret Natural
12) (Natural -> ScalarField c1
secret Natural
13) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural) (size :: Natural).
(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
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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
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 :: Natural).
(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 :: Natural). 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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
1) (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Natural). 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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
-! Natural
1) (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Natural). 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 :: Natural).
(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 :: Natural). 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 :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p)
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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Natural -> ScalarField c1
secret Natural
14) (Natural -> ScalarField c1
secret Natural
15) (Natural -> ScalarField c1
secret Natural
16) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural) (size :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic (Natural -> ScalarField c1
secret Natural
17) (Natural -> ScalarField c1
secret Natural
18) (Natural -> ScalarField c1
secret Natural
19) PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall (size :: Natural).
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 :: Natural) (size :: Natural).
(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
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
KnownNat size =>
PolyVec (ScalarField c1) size
-> PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size
@ forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Natural -> c -> PolyVec c size
polyVecLagrange @_ @n Natural
1 ScalarField c1
omega PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
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 :: Natural).
KnownNat size =>
PolyVec (ScalarField c1) size
-> PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size
@ forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Natural -> c -> PolyVec c size
polyVecLagrange @_ @n Natural
1 ScalarField c1
omega PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
(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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
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 :: Natural). 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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
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 :: Natural). 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 :: Natural).
(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 (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural
2Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
*(Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
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 :: Natural). 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
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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). 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 :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
lag1_xi :: ScalarField c1
lag1_xi = forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
Natural -> c -> PolyVec c size
polyVecLagrange @_ @n @(PlonkupPolyExtendedLength n) Natural
1 ScalarField c1
omega PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> ScalarField c1 -> ScalarField c1
forall c (size :: Natural). 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
// (Natural -> ScalarField c1 -> ScalarField c1
forall b a. Scale b a => b -> a -> a
scale Natural
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))
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 :: Natural). 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 :: Natural). 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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 :: Natural).
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 -> Natural -> ScalarField c1
forall a b. Exponent a b => a -> b -> a
^(Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
2)) ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 -> Natural -> ScalarField c1
forall a b. Exponent a b => a -> b -> a
^(Natural
2Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
*Natural
nNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
4)) ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
qhighX)
vn :: Natural -> ScalarField c1
vn Natural
i = ScalarField c1
v ScalarField c1 -> Natural -> ScalarField c1
forall a b. Exponent a b => a -> b -> a
^ (Natural
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
+ (Natural -> ScalarField c1
vn Natural
1 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
2 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
3 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
4 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
5 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
6 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
7 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
8 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
(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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
1 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
2 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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
+ (Natural -> ScalarField c1
vn Natural
3 ScalarField c1
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
-> PolyVec (ScalarField c1) (PlonkupPolyExtendedLength n)
forall c (size :: Natural).
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 :: Natural).
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 :: Natural).
(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 :: Natural).
(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