{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Plonkup.Setup where

import           Data.Binary                                       (Binary)
import           Data.Functor.Rep                                  (Rep, Representable)
import           Data.Maybe                                        (fromJust)
import qualified Data.Vector                                       as V
import           GHC.IsList                                        (IsList (..))
import           Prelude                                           hiding (Num (..), drop, length, sum, take, (!!), (/),
                                                                    (^))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number                  (KnownNat, value)
import           ZkFold.Base.Algebra.Basic.Permutations            (fromPermutation)
import           ZkFold.Base.Algebra.EllipticCurve.Class           (CyclicGroup (..), Pairing)
import           ZkFold.Base.Algebra.Polynomials.Univariate        (PolyVec, polyVecInLagrangeBasis, toPolyVec)
import           ZkFold.Base.Data.Vector                           (Vector (..))
import           ZkFold.Base.Protocol.NonInteractiveProof.Internal (CoreFunction (..))
import           ZkFold.Base.Protocol.Plonkup.Internal             (Plonkup (..), PlonkupPermutationSize,
                                                                    PlonkupPolyExtendedLength, with4n6)
import           ZkFold.Base.Protocol.Plonkup.Prover.Polynomials   (PlonkupCircuitPolynomials (..))
import           ZkFold.Base.Protocol.Plonkup.Relation             (PlonkupRelation (..), toPlonkupRelation)
import           ZkFold.Base.Protocol.Plonkup.Verifier.Commitments (PlonkupCircuitCommitments (..))
import           ZkFold.Symbolic.Class                             (Arithmetic)

data PlonkupSetup p i n l g1 g2 = PlonkupSetup
    { forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
omega       :: ScalarFieldOf g1
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k1          :: ScalarFieldOf g1
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k2          :: ScalarFieldOf g1
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> Vector g1
gs          :: V.Vector g1
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
h0          :: g2
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
h1          :: g2
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma1s     :: PolyVec (ScalarFieldOf g1) n
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s     :: PolyVec (ScalarFieldOf g1) n
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s     :: PolyVec (ScalarFieldOf g1) n
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
relation    :: PlonkupRelation p i n l (ScalarFieldOf g1)
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1
polynomials :: PlonkupCircuitPolynomials n g1
    , forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1
commitments :: PlonkupCircuitCommitments g1
    }

instance
        ( Show g1
        , Show g2
        , Show (ScalarFieldOf g1)
        , Show (PlonkupRelation p i n l (ScalarFieldOf g1))
        ) => Show (PlonkupSetup p i n l g1 g2) where
    show :: PlonkupSetup p i n l g1 g2 -> String
show PlonkupSetup {g2
Vector g1
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
ScalarFieldOf g1
PlonkupRelation p i n l (ScalarFieldOf g1)
PlonkupCircuitPolynomials n g1
omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> ScalarFieldOf g1
gs :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> Vector g1
h0 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> g2
sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PolyVec (ScalarFieldOf g1) n
relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2
-> PlonkupRelation p i n l (ScalarFieldOf g1)
polynomials :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitPolynomials n g1
commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2.
PlonkupSetup p i n l g1 g2 -> PlonkupCircuitCommitments g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
gs :: Vector g1
h0 :: g2
h1 :: g2
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
commitments :: PlonkupCircuitCommitments g1
..} =
        String
"Setup: "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
omega String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Vector g1 -> String
forall a. Show a => a -> String
show Vector g1
gs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ g2 -> String
forall a. Show a => a -> String
show g2
h0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ g2 -> String
forall a. Show a => a -> String
show g2
h1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarFieldOf g1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarFieldOf g1) n
sigma1s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarFieldOf g1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarFieldOf g1) n
sigma2s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarFieldOf g1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarFieldOf g1) n
sigma3s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupRelation p i n l (ScalarFieldOf g1) -> String
forall a. Show a => a -> String
show PlonkupRelation p i n l (ScalarFieldOf g1)
relation String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupCircuitPolynomials n g1 -> String
forall a. Show a => a -> String
show PlonkupCircuitPolynomials n g1
polynomials String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupCircuitCommitments g1 -> String
forall a. Show a => a -> String
show PlonkupCircuitCommitments g1
commitments

plonkupSetup :: forall i p n l g1 g2 gt ts core.
    ( KnownNat n
    , Representable p
    , Representable i
    , Representable l
    , Foldable l
    , Ord (Rep i)
    , Arithmetic (ScalarFieldOf g1)
    , Binary (ScalarFieldOf g2)
    , Pairing g1 g2 gt
    , CoreFunction g1 core) => Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
plonkupSetup :: forall {k} {k} (i :: Type -> Type) (p :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) g1 g2 gt (ts :: k) (core :: k).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarFieldOf g1),
 Binary (ScalarFieldOf g2), Pairing g1 g2 gt,
 CoreFunction g1 core) =>
Plonkup p i n l g1 g2 ts -> PlonkupSetup p i n l g1 g2
plonkupSetup Plonkup {g2
Vector (n + 5) g1
ArithmeticCircuit (ScalarFieldOf g1) p i l
ScalarFieldOf g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
ac :: ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: g2
gs' :: Vector (n + 5) g1
omega :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
k1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
k2 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> ScalarFieldOf g1
ac :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript
-> ArithmeticCircuit (ScalarFieldOf g1) p i l
h1 :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> g2
gs' :: forall {k} (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) g1 g2 (transcript :: k).
Plonkup p i n l g1 g2 transcript -> Vector (n + 5) g1
..} =
    let gs :: Vector g1
gs = Vector (n + 5) g1 -> Vector g1
forall (size :: Natural) a. Vector size a -> Vector a
toV Vector (n + 5) g1
gs'
        h0 :: g2
h0 = g2
forall g. CyclicGroup g => g
pointGen

        relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
relation@PlonkupRelation{PolyVec (ScalarFieldOf g1) n
Permutation (3 * n)
p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1) -> l (ScalarFieldOf g1)
p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1)
-> (PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n,
    PolyVec (ScalarFieldOf g1) n)
qM :: PolyVec (ScalarFieldOf g1) n
qL :: PolyVec (ScalarFieldOf g1) n
qR :: PolyVec (ScalarFieldOf g1) n
qO :: PolyVec (ScalarFieldOf g1) n
qC :: PolyVec (ScalarFieldOf g1) n
qK :: PolyVec (ScalarFieldOf g1) n
t :: PolyVec (ScalarFieldOf g1) n
sigma :: Permutation (3 * n)
witness :: p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1)
-> (PolyVec (ScalarFieldOf g1) n, PolyVec (ScalarFieldOf g1) n,
    PolyVec (ScalarFieldOf g1) n)
pubInput :: p (ScalarFieldOf g1)
-> i (ScalarFieldOf g1) -> l (ScalarFieldOf g1)
qM :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qL :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qR :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qO :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qC :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
qK :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
t :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> PolyVec a n
sigma :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> Permutation (3 * n)
witness :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a
-> p a -> i a -> (PolyVec a n, PolyVec a n, PolyVec a n)
pubInput :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
PlonkupRelation p i n l a -> p a -> i a -> l a
..} = Maybe (PlonkupRelation p i n l (ScalarFieldOf g1))
-> PlonkupRelation p i n l (ScalarFieldOf g1)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (PlonkupRelation p i n l (ScalarFieldOf g1))
 -> PlonkupRelation p i n l (ScalarFieldOf g1))
-> Maybe (PlonkupRelation p i n l (ScalarFieldOf g1))
-> PlonkupRelation p i n l (ScalarFieldOf g1)
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit (ScalarFieldOf g2) p i l
-> Maybe (PlonkupRelation p i n l (ScalarFieldOf g2))
forall (i :: Type -> Type) (p :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
(KnownNat n, Arithmetic a, Binary a, Ord (Rep i), Representable p,
 Representable i, Representable l, Foldable l) =>
ArithmeticCircuit a p i l -> Maybe (PlonkupRelation p i n l a)
toPlonkupRelation ArithmeticCircuit (ScalarFieldOf g1) p i l
ArithmeticCircuit (ScalarFieldOf g2) p i l
ac :: PlonkupRelation p i n l (ScalarFieldOf g1)

        f :: Natural -> ScalarFieldOf g2
f Natural
i = case (Natural
iNatural -> Natural -> Natural
-!Natural
1) Natural -> Natural -> Natural
forall a. Integral a => a -> a -> a
`Prelude.div` forall (n :: Natural). KnownNat n => Natural
value @n of
            Natural
0 -> ScalarFieldOf g1
ScalarFieldOf g2
omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2
forall a b. Exponent a b => a -> b -> a
^Natural
i
            Natural
1 -> ScalarFieldOf g1
ScalarFieldOf g2
k1 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
ScalarFieldOf g2
omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2
forall a b. Exponent a b => a -> b -> a
^Natural
i)
            Natural
2 -> ScalarFieldOf g1
ScalarFieldOf g2
k2 ScalarFieldOf g2 -> ScalarFieldOf g2 -> ScalarFieldOf g2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarFieldOf g1
ScalarFieldOf g2
omegaScalarFieldOf g2 -> Natural -> ScalarFieldOf g2
forall a b. Exponent a b => a -> b -> a
^Natural
i)
            Natural
_ -> String -> ScalarFieldOf g2
forall a. HasCallStack => String -> a
error String
"setup: invalid index"
        s :: Vector (ScalarFieldOf g2)
s = [Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2))
-> [Item (Vector (ScalarFieldOf g2))] -> Vector (ScalarFieldOf g2)
forall a b. (a -> b) -> a -> b
$ (Natural -> Item (Vector (ScalarFieldOf g2)))
-> [Natural] -> [Item (Vector (ScalarFieldOf g2))]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> Item (Vector (ScalarFieldOf g2))
Natural -> ScalarFieldOf g2
f ([Natural] -> [Item (Vector (ScalarFieldOf g2))])
-> [Natural] -> [Item (Vector (ScalarFieldOf g2))]
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). Permutation n -> [Natural]
fromPermutation @(PlonkupPermutationSize n) (Permutation (3 * n) -> [Natural])
-> Permutation (3 * n) -> [Natural]
forall a b. (a -> b) -> a -> b
$ Permutation (3 * n)
sigma
        sigma1s :: PolyVec (ScalarFieldOf g2) n
sigma1s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n)
-> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a. Int -> Vector a -> Vector a
V.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) Vector (ScalarFieldOf g2)
s
        sigma2s :: PolyVec (ScalarFieldOf g2) n
sigma2s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n)
-> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a. Int -> Vector a -> Vector a
V.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) (Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2))
-> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a. Int -> Vector a -> Vector a
V.drop (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) Vector (ScalarFieldOf g2)
s
        sigma3s :: PolyVec (ScalarFieldOf g2) n
sigma3s = Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n)
-> Vector (ScalarFieldOf g2) -> PolyVec (ScalarFieldOf g2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a. Int -> Vector a -> Vector a
V.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ forall (n :: Natural). KnownNat n => Natural
value @n) (Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2))
-> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarFieldOf g2) -> Vector (ScalarFieldOf g2)
forall a. Int -> Vector a -> Vector a
V.drop (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Natural -> Int) -> Natural -> Int
forall a b. (a -> b) -> a -> b
$ Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall (n :: Natural). KnownNat n => Natural
value @n) Vector (ScalarFieldOf g2)
s

        qmX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qmX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qM)
        qlX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qlX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qL)
        qrX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qrX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qR)
        qoX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qoX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qO)
        qcX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qcX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qC)
        qkX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qkX = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
qK)
        s1X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s1X = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
PolyVec (ScalarFieldOf g2) n
sigma1s)
        s2X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s2X = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
PolyVec (ScalarFieldOf g2) n
sigma2s)
        s3X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s3X = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
PolyVec (ScalarFieldOf g2) n
sigma3s)
        tX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
tX  = forall (n :: Natural) {r}.
KnownNat n =>
(KnownNat ((4 * n) + 6) => r) -> r
with4n6 @n (forall c (n :: Natural) (size :: Natural).
(Field c, Eq c, KnownNat n, KnownNat size) =>
c -> PolyVec c n -> PolyVec c size
polyVecInLagrangeBasis @(ScalarFieldOf g1) @n @(PlonkupPolyExtendedLength n) ScalarFieldOf g1
omega PolyVec (ScalarFieldOf g1) n
t)
        polynomials :: PlonkupCircuitPolynomials n g1
polynomials = PlonkupCircuitPolynomials {PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qmX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qlX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qrX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qoX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qcX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qkX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s1X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s2X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s3X :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
tX :: PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qlX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
qrX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
qoX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
qmX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
qcX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
qkX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
s1X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
s2X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
s3X :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
tX :: PolyVec (ScalarFieldOf g1) ((4 * n) + 6)
..}

        com :: Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
com = forall g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
forall {k} g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
msm @g1 @core
        cmQl :: g1
cmQl = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qlX
        cmQr :: g1
cmQr = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qrX
        cmQo :: g1
cmQo = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qoX
        cmQm :: g1
cmQm = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qmX
        cmQc :: g1
cmQc = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qcX
        cmQk :: g1
cmQk = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
qkX
        cmS1 :: g1
cmS1 = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s1X
        cmS2 :: g1
cmS2 = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s2X
        cmS3 :: g1
cmS3 = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
s3X
        cmT1 :: g1
cmT1  = Vector g1
gs Vector g1 -> PolyVec (ScalarFieldOf g2) ((4 * n) + 6) -> g1
`com` PolyVec (ScalarFieldOf g2) ((4 * n) + 6)
tX
        commitments :: PlonkupCircuitCommitments g1
commitments = PlonkupCircuitCommitments {g1
cmQl :: g1
cmQr :: g1
cmQo :: g1
cmQm :: g1
cmQc :: g1
cmQk :: g1
cmS1 :: g1
cmS2 :: g1
cmS3 :: g1
cmT1 :: g1
cmQl :: g1
cmQr :: g1
cmQo :: g1
cmQm :: g1
cmQc :: g1
cmQk :: g1
cmS1 :: g1
cmS2 :: g1
cmS3 :: g1
cmT1 :: g1
..}

    in PlonkupSetup {g2
Vector g1
PlonkupCircuitCommitments g1
PolyVec (ScalarFieldOf g1) n
PolyVec (ScalarFieldOf g2) 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
h0 :: g2
h1 :: g2
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
commitments :: PlonkupCircuitCommitments g1
omega :: ScalarFieldOf g1
k1 :: ScalarFieldOf g1
k2 :: ScalarFieldOf g1
h1 :: g2
gs :: Vector g1
h0 :: g2
relation :: PlonkupRelation p i n l (ScalarFieldOf g1)
sigma1s :: PolyVec (ScalarFieldOf g2) n
sigma2s :: PolyVec (ScalarFieldOf g2) n
sigma3s :: PolyVec (ScalarFieldOf g2) n
polynomials :: PlonkupCircuitPolynomials n g1
commitments :: PlonkupCircuitCommitments g1
..}