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

module ZkFold.Base.Protocol.Plonkup.Setup where

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
import           ZkFold.Base.Algebra.Basic.Permutations              (fromPermutation)
import           ZkFold.Base.Algebra.EllipticCurve.Class             (EllipticCurve (..), Pairing, Point)
import           ZkFold.Base.Algebra.Polynomials.Univariate          hiding (qr)
import           ZkFold.Base.Protocol.NonInteractiveProof            (CoreFunction (..))
import           ZkFold.Base.Protocol.Plonkup.Internal
import           ZkFold.Base.Protocol.Plonkup.Prover
import           ZkFold.Base.Protocol.Plonkup.Relation               (PlonkupRelation (..), toPlonkupRelation)
import           ZkFold.Base.Protocol.Plonkup.Verifier
import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal

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

instance
        ( EllipticCurve c1
        , EllipticCurve c2
        , Show (BaseField c1)
        , Show (BaseField c2)
        , Show (ScalarField c1)
        , Show (PlonkupRelation p i n l (ScalarField c1))
        , BooleanOf c1 ~ Bool
        , BooleanOf c2 ~ Bool
        ) => Show (PlonkupSetup p i n l c1 c2) where
    show :: PlonkupSetup p i n l c1 c2 -> String
show PlonkupSetup {Vector (Point c1)
PolyVec (ScalarField c1) n
ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PlonkupRelation p i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> ScalarField c1
k1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> ScalarField c1
k2 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> ScalarField c1
gs :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> Vector (Point c1)
h0 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> Point c2
h1 :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> Point c2
sigma1s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma2s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
sigma3s :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> PolyVec (ScalarField c1) n
relation :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2
-> PlonkupRelation p i n l (ScalarField c1)
polynomials :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> PlonkupCircuitPolynomials n c1
commitments :: forall (p :: Type -> Type) (i :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) c1 c2.
PlonkupSetup p i n l c1 c2 -> PlonkupCircuitCommitments c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
h0 :: Point c2
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation p i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
commitments :: PlonkupCircuitCommitments c1
..} =
        String
"Setup: "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarField c1 -> String
forall a. Show a => a -> String
show ScalarField c1
omega String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarField c1 -> String
forall a. Show a => a -> String
show ScalarField c1
k1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ ScalarField c1 -> String
forall a. Show a => a -> String
show ScalarField c1
k2 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Vector (Point c1) -> String
forall a. Show a => a -> String
show Vector (Point c1)
gs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Point c2 -> String
forall a. Show a => a -> String
show Point c2
h0 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ Point c2 -> String
forall a. Show a => a -> String
show Point c2
h1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarField c1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarField c1) n
sigma1s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarField c1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarField c1) n
sigma2s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PolyVec (ScalarField c1) n -> String
forall a. Show a => a -> String
show PolyVec (ScalarField c1) n
sigma3s String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupRelation p i n l (ScalarField c1) -> String
forall a. Show a => a -> String
show PlonkupRelation p i n l (ScalarField c1)
relation String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupCircuitPolynomials n c1 -> String
forall a. Show a => a -> String
show PlonkupCircuitPolynomials n c1
polynomials String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" "
        String -> ShowS
forall a. [a] -> [a] -> [a]
++ PlonkupCircuitCommitments c1 -> String
forall a. Show a => a -> String
show PlonkupCircuitCommitments c1
commitments

plonkupSetup :: forall i p n l c1 c2 ts core.
    ( KnownNat n
    , Representable p
    , Representable i
    , Representable l
    , Foldable l
    , Ord (Rep i)
    , Arithmetic (ScalarField c1)
    , Pairing c1 c2
    , CoreFunction c1 core) => Plonkup p i n l c1 c2 ts -> PlonkupSetup p i n l c1 c2
plonkupSetup :: forall {k1} {k} (i :: Type -> Type) (p :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) c1 c2 (ts :: k1) (core :: k).
(KnownNat n, Representable p, Representable i, Representable l,
 Foldable l, Ord (Rep i), Arithmetic (ScalarField c1),
 Pairing c1 c2, CoreFunction c1 core) =>
Plonkup p i n l c1 c2 ts -> PlonkupSetup p i n l c1 c2
plonkupSetup Plonkup {ArithmeticCircuit (ScalarField c1) p i l
ScalarField c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
ac :: ArithmeticCircuit (ScalarField c1) p i l
x :: ScalarField c1
omega :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) curve1 (curve2 :: k1)
       (transcript :: k2).
Plonkup p i n l curve1 curve2 transcript -> ScalarField curve1
k1 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) curve1 (curve2 :: k1)
       (transcript :: k2).
Plonkup p i n l curve1 curve2 transcript -> ScalarField curve1
k2 :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) curve1 (curve2 :: k1)
       (transcript :: k2).
Plonkup p i n l curve1 curve2 transcript -> ScalarField curve1
ac :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) curve1 (curve2 :: k1)
       (transcript :: k2).
Plonkup p i n l curve1 curve2 transcript
-> ArithmeticCircuit (ScalarField curve1) p i l
x :: forall {k1} {k2} (p :: Type -> Type) (i :: Type -> Type)
       (n :: Natural) (l :: Type -> Type) curve1 (curve2 :: k1)
       (transcript :: k2).
Plonkup p i n l curve1 curve2 transcript -> ScalarField curve1
..} =
    let xs :: Vector (ScalarField c2)
xs   = [Item (Vector (ScalarField c2))] -> Vector (ScalarField c2)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarField c2))] -> Vector (ScalarField c2))
-> [Item (Vector (ScalarField c2))] -> Vector (ScalarField c2)
forall a b. (a -> b) -> a -> b
$ (Natural -> ScalarField c2) -> [Natural] -> [ScalarField c2]
forall a b. (a -> b) -> [a] -> [b]
map (ScalarField c1
ScalarField c2
xScalarField c2 -> Natural -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^) [Natural
0 .. (forall (n :: Natural). KnownNat n => Natural
value @n Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
5)]
        gs :: Vector (Point c1)
gs   = (ScalarField c2 -> Point c1)
-> Vector (ScalarField c2) -> Vector (Point c1)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScalarField c1 -> Point c1 -> Point c1
forall curve.
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
forall curve. EllipticCurve curve => Point curve
pointGen) Vector (ScalarField c2)
xs
        h0 :: Point c2
h0   = Point c2
forall curve. EllipticCurve curve => Point curve
pointGen
        h1 :: Point c2
h1   = ScalarField c1
ScalarField c2
x ScalarField c2 -> Point c2 -> Point c2
forall curve.
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c2
forall curve. EllipticCurve curve => Point curve
pointGen

        relation :: PlonkupRelation p i n l (ScalarField c1)
relation@PlonkupRelation{PolyVec (ScalarField c1) n
Permutation (3 * n)
p (ScalarField c1) -> i (ScalarField c1) -> l (ScalarField c1)
p (ScalarField c1)
-> i (ScalarField c1)
-> (PolyVec (ScalarField c1) n, PolyVec (ScalarField c1) n,
    PolyVec (ScalarField c1) n)
qM :: PolyVec (ScalarField c1) n
qL :: PolyVec (ScalarField c1) n
qR :: PolyVec (ScalarField c1) n
qO :: PolyVec (ScalarField c1) n
qC :: PolyVec (ScalarField c1) n
qK :: PolyVec (ScalarField c1) n
t :: PolyVec (ScalarField c1) n
sigma :: Permutation (3 * n)
witness :: p (ScalarField c1)
-> i (ScalarField c1)
-> (PolyVec (ScalarField c1) n, PolyVec (ScalarField c1) n,
    PolyVec (ScalarField c1) n)
pubInput :: p (ScalarField c1) -> i (ScalarField c1) -> l (ScalarField c1)
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 (ScalarField c1))
-> PlonkupRelation p i n l (ScalarField c1)
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe (PlonkupRelation p i n l (ScalarField c1))
 -> PlonkupRelation p i n l (ScalarField c1))
-> Maybe (PlonkupRelation p i n l (ScalarField c1))
-> PlonkupRelation p i n l (ScalarField c1)
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit (ScalarField c2) p i l
-> Maybe (PlonkupRelation p i n l (ScalarField c2))
forall (i :: Type -> Type) (p :: Type -> Type) (n :: Natural)
       (l :: Type -> Type) a.
(KnownNat n, Arithmetic 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 (ScalarField c1) p i l
ArithmeticCircuit (ScalarField c2) p i l
ac :: PlonkupRelation p i n l (ScalarField c1)

        f :: Natural -> ScalarField c2
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 -> ScalarField c1
ScalarField c2
omegaScalarField c2 -> Natural -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^Natural
i
            Natural
1 -> ScalarField c1
ScalarField c2
k1 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
omegaScalarField c2 -> Natural -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^Natural
i)
            Natural
2 -> ScalarField c1
ScalarField c2
k2 ScalarField c2 -> ScalarField c2 -> ScalarField c2
forall a. MultiplicativeSemigroup a => a -> a -> a
* (ScalarField c1
ScalarField c2
omegaScalarField c2 -> Natural -> ScalarField c2
forall a b. Exponent a b => a -> b -> a
^Natural
i)
            Natural
_ -> String -> ScalarField c2
forall a. HasCallStack => String -> a
error String
"setup: invalid index"
        s :: Vector (ScalarField c2)
s = [Item (Vector (ScalarField c2))] -> Vector (ScalarField c2)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector (ScalarField c2))] -> Vector (ScalarField c2))
-> [Item (Vector (ScalarField c2))] -> Vector (ScalarField c2)
forall a b. (a -> b) -> a -> b
$ (Natural -> Item (Vector (ScalarField c2)))
-> [Natural] -> [Item (Vector (ScalarField c2))]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> Item (Vector (ScalarField c2))
Natural -> ScalarField c2
f ([Natural] -> [Item (Vector (ScalarField c2))])
-> [Natural] -> [Item (Vector (ScalarField c2))]
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 (ScalarField c2) n
sigma1s = Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c2) -> PolyVec (ScalarField c2) n)
-> Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c2) -> Vector (ScalarField c2)
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 (ScalarField c2)
s
        sigma2s :: PolyVec (ScalarField c2) n
sigma2s = Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c2) -> PolyVec (ScalarField c2) n)
-> Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c2) -> Vector (ScalarField c2)
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 (ScalarField c2) -> Vector (ScalarField c2))
-> Vector (ScalarField c2) -> Vector (ScalarField c2)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c2) -> Vector (ScalarField c2)
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 (ScalarField c2)
s
        sigma3s :: PolyVec (ScalarField c2) n
sigma3s = Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector (ScalarField c2) -> PolyVec (ScalarField c2) n)
-> Vector (ScalarField c2) -> PolyVec (ScalarField c2) n
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c2) -> Vector (ScalarField c2)
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 (ScalarField c2) -> Vector (ScalarField c2))
-> Vector (ScalarField c2) -> Vector (ScalarField c2)
forall a b. (a -> b) -> a -> b
$ Int -> Vector (ScalarField c2) -> Vector (ScalarField c2)
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 (ScalarField c2)
s

        qmX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qM)
        qlX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qL)
        qrX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qR)
        qoX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qO)
        qcX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qC)
        qkX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
qK)
        s1X :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
PolyVec (ScalarField c2) n
sigma1s)
        s2X :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
PolyVec (ScalarField c2) n
sigma2s)
        s3X :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
PolyVec (ScalarField c2) n
sigma3s)
        tX :: PolyVec (ScalarField c2) ((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 @(ScalarField c1) @n @(PlonkupPolyExtendedLength n) ScalarField c1
omega PolyVec (ScalarField c1) n
t)
        polynomials :: PlonkupCircuitPolynomials n c1
polynomials = PlonkupCircuitPolynomials {PolyVec (ScalarField c1) ((4 * n) + 6)
PolyVec (ScalarField c2) ((4 * n) + 6)
qmX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qlX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qrX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qoX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qcX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qkX :: PolyVec (ScalarField c2) ((4 * n) + 6)
s1X :: PolyVec (ScalarField c2) ((4 * n) + 6)
s2X :: PolyVec (ScalarField c2) ((4 * n) + 6)
s3X :: PolyVec (ScalarField c2) ((4 * n) + 6)
tX :: PolyVec (ScalarField c2) ((4 * n) + 6)
qlX :: PolyVec (ScalarField c1) ((4 * n) + 6)
qrX :: PolyVec (ScalarField c1) ((4 * n) + 6)
qoX :: PolyVec (ScalarField c1) ((4 * n) + 6)
qmX :: PolyVec (ScalarField c1) ((4 * n) + 6)
qcX :: PolyVec (ScalarField c1) ((4 * n) + 6)
qkX :: PolyVec (ScalarField c1) ((4 * n) + 6)
s1X :: PolyVec (ScalarField c1) ((4 * n) + 6)
s2X :: PolyVec (ScalarField c1) ((4 * n) + 6)
s3X :: PolyVec (ScalarField c1) ((4 * n) + 6)
tX :: PolyVec (ScalarField c1) ((4 * n) + 6)
..}

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

    in PlonkupSetup {Vector (Point c1)
PolyVec (ScalarField c1) n
PolyVec (ScalarField c2) n
ScalarField c1
Point c2
PlonkupCircuitCommitments c1
PlonkupRelation p i n l (ScalarField c1)
PlonkupCircuitPolynomials n c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
h0 :: Point c2
h1 :: Point c2
sigma1s :: PolyVec (ScalarField c1) n
sigma2s :: PolyVec (ScalarField c1) n
sigma3s :: PolyVec (ScalarField c1) n
relation :: PlonkupRelation p i n l (ScalarField c1)
polynomials :: PlonkupCircuitPolynomials n c1
commitments :: PlonkupCircuitCommitments c1
omega :: ScalarField c1
k1 :: ScalarField c1
k2 :: ScalarField c1
gs :: Vector (Point c1)
h0 :: Point c2
h1 :: Point c2
relation :: PlonkupRelation p i n l (ScalarField c1)
sigma1s :: PolyVec (ScalarField c2) n
sigma2s :: PolyVec (ScalarField c2) n
sigma3s :: PolyVec (ScalarField c2) n
polynomials :: PlonkupCircuitPolynomials n c1
commitments :: PlonkupCircuitCommitments c1
..}