{-# LANGUAGE AllowAmbiguousTypes #-}

module ZkFold.Base.Protocol.Plonk.Prover
    ( plonkProve
    ) where

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

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number                    (KnownNat, Natural, value)
import           ZkFold.Base.Algebra.EllipticCurve.Class             (EllipticCurve (..), PointCompressed, compress)
import           ZkFold.Base.Algebra.Polynomials.Univariate          hiding (qr)
import           ZkFold.Base.Data.Vector                             ((!!))
import           ZkFold.Base.Protocol.NonInteractiveProof
import           ZkFold.Base.Protocol.Plonkup                        (with4n6)
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

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

        PlonkupCircuitPolynomials {PlonkupPolyExtended n c1
qlX :: PlonkupPolyExtended n c1
qrX :: PlonkupPolyExtended n c1
qoX :: PlonkupPolyExtended n c1
qmX :: PlonkupPolyExtended n c1
qcX :: PlonkupPolyExtended n c1
qkX :: PlonkupPolyExtended n c1
s1X :: PlonkupPolyExtended n c1
s2X :: PlonkupPolyExtended n c1
s3X :: PlonkupPolyExtended n c1
tX :: PlonkupPolyExtended n c1
qlX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qrX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qoX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qmX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qcX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
qkX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s1X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s2X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
s3X :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
tX :: forall {k} (n :: Nat) (c :: k).
PlonkupCircuitPolynomials n c -> PlonkupPolyExtended n c
..} = PlonkupCircuitPolynomials n c1
polynomials
        secret :: Nat -> ScalarField c1
secret Nat
i = Vector 19 (ScalarField c1)
ps Vector 19 (ScalarField c1) -> Nat -> ScalarField c1
forall (size :: Nat) a. Vector size a -> Nat -> a
!! (Nat
i Nat -> Nat -> Nat
-! Nat
1)

        n :: Nat
n = forall (n :: Nat). KnownNat n => Nat
value @n
        zhX :: PlonkupPolyExtended n c1
zhX = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ forall c (n :: Nat) (size :: Nat).
(Field c, KnownNat n, KnownNat size, Eq c) =>
PolyVec c size
polyVecZero @_ @n @(PlonkupPolyExtendedLength n)

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

        w1X :: PlonkupPolyExtended n c1
w1X = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ ScalarField c1
-> PolyVec (ScalarField c1) n -> PlonkupPolyExtended n c1
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
w1 :: PlonkupPolyExtended n c1
        w2X :: PlonkupPolyExtended n c1
w2X = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ ScalarField c1
-> PolyVec (ScalarField c1) n -> PlonkupPolyExtended n c1
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
w2 :: PlonkupPolyExtended n c1
        w3X :: PlonkupPolyExtended n c1
w3X = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ ScalarField c1
-> PolyVec (ScalarField c1) n -> PlonkupPolyExtended n c1
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
w3 :: PlonkupPolyExtended n c1

        pi :: PolyVec (ScalarField c1) n
pi  = forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @_ @n (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarField c1))] -> Vector (ScalarField c1))
-> [Item (Vector (ScalarField c1))] -> Vector (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ (ScalarField c1 -> [ScalarField c1])
-> l (ScalarField c1) -> [ScalarField c1]
forall m a. Monoid m => (a -> m) -> l a -> m
forall (t :: Type -> Type) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap (\ScalarField c1
x -> [ScalarField c1 -> ScalarField c1
forall a. AdditiveGroup a => a -> a
negate ScalarField c1
x]) l (ScalarField c1)
wPub
        piX :: PlonkupPolyExtended n c1
piX = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ ScalarField c1
-> PolyVec (ScalarField c1) n -> PlonkupPolyExtended n c1
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
pi  :: PlonkupPolyExtended n c1

        -- Round 1

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

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

        -- Round 2

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

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

        fX :: PlonkupPolyExtended n c1
fX = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ ScalarField c1 -> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (Nat -> ScalarField c1
secret Nat
7) (Nat -> ScalarField c1
secret Nat
8) PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall (size :: Nat).
KnownNat size =>
PolyVec (ScalarField c1) size
-> PolyVec (ScalarField c1) size -> PolyVec (ScalarField c1) size
@ PlonkupPolyExtended n c1
zhX PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
-> PolyVec (ScalarField c1) n -> PlonkupPolyExtended n c1
forall c (n :: Nat) (size :: Nat).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis ScalarField c1
omega PolyVec (ScalarField c1) n
f_zeta :: PlonkupPolyExtended n c1

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

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

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

        -- Round 3

        ts2 :: ts
ts2 = ts
ts1
            -- `transcript` compress cmF
            -- `transcript` compress cmH1
            -- `transcript` compress cmH2
        beta :: ScalarField c1
beta    = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
1 :: Word8))
        gamma :: ScalarField c1
gamma   = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
2 :: Word8))
        delta :: ScalarField c1
delta   = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
3 :: Word8))
        epsilon :: ScalarField c1
epsilon = ts -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge (ts
ts2 ts -> Word8 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
4 :: Word8))

        omegas :: PolyVec (ScalarField c1) n
omegas  = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ Int
-> (ScalarField c1 -> ScalarField c1)
-> ScalarField c1
-> Vector (ScalarField c1)
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Nat
n) (ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega) ScalarField c1
omega
        omegas' :: PlonkupPolyExtended n c1
omegas' = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ Vector (ScalarField c1) -> PlonkupPolyExtended n c1
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PlonkupPolyExtended n c1)
-> Vector (ScalarField c1) -> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$ Int
-> (ScalarField c1 -> ScalarField c1)
-> ScalarField c1
-> Vector (ScalarField c1)
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @(PlonkupPolyExtendedLength n)) (ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
omega) ScalarField c1
forall a. MultiplicativeMonoid a => a
one

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

        rotR :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
        rotR :: PolyVec (ScalarField c1) n -> PolyVec (ScalarField c1) n
rotR PolyVec (ScalarField c1) n
p = Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall c (size :: Nat).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c1) -> PolyVec (ScalarField c1) n)
-> Vector (ScalarField c1) -> PolyVec (ScalarField c1) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Int -> Vector a -> Vector a
V.drop (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @n Nat -> Nat -> Nat
-! Nat
1) (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p) Vector (ScalarField c1)
-> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Vector a -> Vector a -> Vector a
V.++ Int -> Vector (ScalarField c1) -> Vector (ScalarField c1)
forall a. Int -> Vector a -> Vector a
V.take (Nat -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Nat -> Int) -> Nat -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). KnownNat n => Nat
value @n Nat -> Nat -> Nat
-! Nat
1) (PolyVec (ScalarField c1) n -> Vector (ScalarField c1)
forall c (size :: Nat). PolyVec c size -> Vector c
fromPolyVec PolyVec (ScalarField c1) n
p)

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

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

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

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

        -- Round 4

        ts3 :: ts
ts3 = ts
ts2
            ts -> PointCompressed c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Point c1 -> PointCompressed c1
forall {k} (curve :: k).
(AdditiveGroup (BaseField curve), Ord (BaseField curve)) =>
Point curve -> PointCompressed curve
compress Point c1
cmZ1
            -- `transcript` compress 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 = alpha2 * alpha
        -- alpha4 = alpha3 * alpha
        -- alpha5 = alpha4 * alpha

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

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

        -- Round 5

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

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

        -- Round 6

        ts5 :: ts
ts5 = ts
ts4
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
a_xi
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
b_xi
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
c_xi
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
s1_xi
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
s2_xi
            -- `transcript` f_xi
            -- `transcript` t_xi
            -- `transcript` t_xi'
            ts -> ScalarField c1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` ScalarField c1
z1_xi'
            -- `transcript` z2_xi'
            -- `transcript` h1_xi'
            -- `transcript` 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 = PlonkupPolyExtended n c1
piX PlonkupPolyExtended n c1 -> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi
        zhX_xi :: ScalarField c1
zhX_xi = PlonkupPolyExtended n c1
zhX PlonkupPolyExtended n c1 -> ScalarField c1 -> ScalarField c1
forall c (size :: Nat). Ring c => PolyVec c size -> c -> c
`evalPolyVec` ScalarField c1
xi

        rX :: PlonkupPolyExtended n c1
rX = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
 -> PlonkupPolyExtended n c1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n c1)
-> PlonkupPolyExtended n c1
forall a b. (a -> b) -> a -> b
$
                PlonkupPolyExtended n c1
qmX PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* (ScalarField c1
a_xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
b_xi) PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
qlX PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
a_xi PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
qrX PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
b_xi PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
qoX PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
c_xi PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
pi_xi PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
qcX
              PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
alpha ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (((ScalarField c1
a_xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
beta ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
gamma) ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
b_xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
beta ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
k1 ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
gamma) ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
c_xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
beta ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
k2 ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarField c1
xi ScalarField c1 -> ScalarField c1 -> ScalarField c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
gamma)) ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n c1
z1X
                        PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
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
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n c1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
c_xi PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarField c1
beta ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n c1
s3X PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n c1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n c1
-> ScalarField c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarField c1
gamma)
                    )
              PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
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
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n c1
z1X PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveGroup a => a -> a -> a
- PlonkupPolyExtended n c1
forall a. MultiplicativeMonoid a => a
one)
            --   + (alpha3 * (a_xi - f_xi)) *. qkX
            --   + alpha4 *. (((one + delta) * (epsilon + f_xi) * ((epsilon * (one + delta)) + t_xi + delta * t_xi')) *. z2X
            --             - (z2_xi' * ((epsilon * (one + delta)) + h2_xi + delta * h1_xi')) *. (one .* (epsilon * (one + delta)) + h1X + one .* (delta * h2_xi))
            --         )
            --   + (alpha5 * lag1_xi) *. (z2X - one)
              PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveGroup a => a -> a -> a
- ScalarField c1
zhX_xi ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n c1
qlowX PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c1
xiScalarField c1 -> Nat -> ScalarField c1
forall a b. Exponent a b => a -> b -> a
^(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n c1
qmidX PlonkupPolyExtended n c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarField c1
xiScalarField c1 -> Nat -> ScalarField c1
forall a b. Exponent a b => a -> b -> a
^(Nat
2Nat -> Nat -> Nat
forall a. MultiplicativeSemigroup a => a -> a -> a
*Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
4)) ScalarField c1
-> PlonkupPolyExtended n c1 -> PlonkupPolyExtended n c1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n c1
qhighX)

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

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

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