{-# 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         (Compressible (..), CyclicGroup (..))
import           ZkFold.Base.Algebra.Polynomials.Univariate      hiding (qr)
import           ZkFold.Base.Data.Vector                         ((!!))
import           ZkFold.Base.Protocol.NonInteractiveProof
import           ZkFold.Base.Protocol.Plonkup                    (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

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

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

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

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

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

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

        -- Round 1

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

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

        -- Round 2

        ts1 :: ts
ts1   = ts
forall a. Monoid a => a
mempty
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmA
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmB
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmC :: ts
        -- zeta = challenge ts1 :: ScalarFieldOf g1

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

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

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

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

        cmF :: g1
cmF  = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
fX
        cmH1 :: g1
cmH1 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
h1X
        cmH2 :: g1
cmH2 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
h2X

        -- Round 3

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

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

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

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

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

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

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

        cmZ1 :: g1
cmZ1 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
z1X
        cmZ2 :: g1
cmZ2 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
z2X

        -- Round 4

        ts3 :: ts
ts3 = ts
ts2
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmZ1
            -- `transcript` compress cmZ2
        alpha :: ScalarFieldOf g1
alpha  = ts -> ScalarFieldOf g1
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts3
        alpha2 :: ScalarFieldOf g1
alpha2 = ScalarFieldOf g1
alpha ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
alpha
        -- alpha3 = alpha2 * alpha
        -- alpha4 = alpha3 * alpha
        -- alpha5 = alpha4 * alpha

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

        cmQlow :: g1
cmQlow = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
qlowX
        cmQmid :: g1
cmQmid = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
qmidX
        cmQhigh :: g1
cmQhigh = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
qhighX

        -- Round 5

        ts4 :: ts
ts4 = ts
ts3
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQlow
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQmid
            ts -> Compressed g1 -> ts
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` g1 -> Compressed g1
forall point. Compressible point => point -> Compressed point
compress g1
cmQhigh
        xi :: ScalarFieldOf g1
xi = ts -> ScalarFieldOf g1
forall ts a. FromTranscript ts a => ts -> a
challenge ts
ts4

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

        -- Round 6

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

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

        rX :: PlonkupPolyExtended n g1
rX = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
 -> PlonkupPolyExtended n g1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
-> PlonkupPolyExtended n g1
forall a b. (a -> b) -> a -> b
$
                PlonkupPolyExtended n g1
qmX PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* (ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
b_xi) PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
qlX PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
a_xi PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
qrX PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
b_xi PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
qoX PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
c_xi PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
pi_xi PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
qcX
              PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
alpha ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (((ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
b_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k1 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
c_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
k2 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma)) ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
z1X
                        PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- ((ScalarFieldOf g1
a_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
s1_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
b_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
s2_xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
gamma) ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
z1_xi') ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
c_xi PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ ScalarFieldOf g1
beta ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
s3X PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one PlonkupPolyExtended n g1
-> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
PolyVec c size -> c -> PolyVec c size
.* ScalarFieldOf g1
gamma)
                    )
              PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
alpha2 ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
lag1_xi) ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
z1X PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- PlonkupPolyExtended n g1
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 g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- ScalarFieldOf g1
zhX_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
qlowX PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
xiScalarFieldOf g1 -> Nat -> ScalarFieldOf g1
forall a b. Exponent a b => a -> b -> a
^(Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
2)) ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
qmidX PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (ScalarFieldOf g1
xiScalarFieldOf g1 -> Nat -> ScalarFieldOf g1
forall a b. Exponent a b => a -> b -> a
^(Nat
2Nat -> Nat -> Nat
forall a. MultiplicativeSemigroup a => a -> a -> a
*Nat
nNat -> Nat -> Nat
forall a. AdditiveSemigroup a => a -> a -> a
+Nat
4)) ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
qhighX)

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

        proofX1 :: PlonkupPolyExtended n g1
proofX1 = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
 -> PlonkupPolyExtended n g1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
-> PlonkupPolyExtended n g1
forall a b. (a -> b) -> a -> b
$ (
                  PlonkupPolyExtended n g1
rX
                PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
1 ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
aX PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
a_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one)))
                PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
2 ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
bX PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
b_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one)))
                PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
3 ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
cX PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
c_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one)))
                PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
4 ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
s1X PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
s1_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
forall a. MultiplicativeMonoid a => a
one)))
                PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (Nat -> ScalarFieldOf g1
vn Nat
5 ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. (PlonkupPolyExtended n g1
s2X PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
s2_xi ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
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 g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` ScalarFieldOf g1 -> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one (ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a
negate ScalarFieldOf g1
xi)
        proofX2 :: PlonkupPolyExtended n g1
proofX2 = forall (n :: Nat) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n ((KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
 -> PlonkupPolyExtended n g1)
-> (KnownNat ((4 * n) + 6) => PlonkupPolyExtended n g1)
-> PlonkupPolyExtended n g1
forall a b. (a -> b) -> a -> b
$ (
                  PlonkupPolyExtended n g1
z1X PlonkupPolyExtended n g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall a. AdditiveGroup a => a -> a -> a
- (ScalarFieldOf g1
z1_xi' ScalarFieldOf g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
Field c =>
c -> PolyVec c size -> PolyVec c size
*. PlonkupPolyExtended n g1
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 g1
-> PlonkupPolyExtended n g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` ScalarFieldOf g1 -> ScalarFieldOf g1 -> PlonkupPolyExtended n g1
forall c (size :: Nat).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear ScalarFieldOf g1
forall a. MultiplicativeMonoid a => a
one (ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. AdditiveGroup a => a -> a
negate (ScalarFieldOf g1
xi ScalarFieldOf g1 -> ScalarFieldOf g1 -> ScalarFieldOf g1
forall a. MultiplicativeSemigroup a => a -> a -> a
* ScalarFieldOf g1
omega))

        proof1 :: g1
proof1 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
proofX1
        proof2 :: g1
proof2 = Vector g1
gs Vector g1 -> PlonkupPolyExtended n g1 -> g1
`com` PlonkupPolyExtended n g1
proofX2