{-# LANGUAGE OverloadedLists      #-}
{-# LANGUAGE TypeApplications     #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.ARK.Plonk where

import           Data.Map                                    (Map, elems, singleton)
import qualified Data.Map                                    as Map
import qualified Data.Vector                                 as V
import           GHC.IsList                                  (IsList (..))
import           Numeric.Natural                             (Natural)
import           Prelude                                     hiding (Num (..), div, drop, length, replicate, sum, take,
                                                              (!!), (/), (^))
import qualified Prelude                                     as P
import           Test.QuickCheck                             (Arbitrary (..))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field             (Zp, fromZp)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.Basic.Permutations      (fromCycles, fromPermutation, mkIndexPartition)
import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.Polynomials.Univariate  hiding (qr)
import           ZkFold.Base.Protocol.ARK.Plonk.Internal     (getParams, toPlonkArithmetization)
import           ZkFold.Base.Protocol.Commitment.KZG         (com)
import           ZkFold.Base.Protocol.NonInteractiveProof
import           ZkFold.Prelude                              ((!))
import           ZkFold.Symbolic.Compiler

-- TODO (Issue #25): make this module generic in the elliptic curve with pairing

type F = Zp BLS12_381_Scalar
type G1 = Point BLS12_381_G1
type G2 = Point BLS12_381_G2

{-
    NOTE: we need to parametrize the type of transcripts because we use BuiltinByteString on-chain and ByteString off-chain.
    Additionally, we don't want this library to depend on Cardano libraries.
-}
data Plonk (d :: Natural) t = Plonk F F F (Map Natural F) (ArithmeticCircuit F) F
    deriving (Int -> Plonk d t -> ShowS
[Plonk d t] -> ShowS
Plonk d t -> String
(Int -> Plonk d t -> ShowS)
-> (Plonk d t -> String)
-> ([Plonk d t] -> ShowS)
-> Show (Plonk d t)
forall (d :: Natural) k (t :: k). Int -> Plonk d t -> ShowS
forall (d :: Natural) k (t :: k). [Plonk d t] -> ShowS
forall (d :: Natural) k (t :: k). Plonk d t -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (d :: Natural) k (t :: k). Int -> Plonk d t -> ShowS
showsPrec :: Int -> Plonk d t -> ShowS
$cshow :: forall (d :: Natural) k (t :: k). Plonk d t -> String
show :: Plonk d t -> String
$cshowList :: forall (d :: Natural) k (t :: k). [Plonk d t] -> ShowS
showList :: [Plonk d t] -> ShowS
Show)
-- TODO (Issue #25): make a proper implementation of Arbitrary
instance Arbitrary (Plonk d t) where
    arbitrary :: Gen (Plonk d t)
arbitrary = do
        let (F
omega, F
k1, F
k2) = Natural -> (F, F, F)
getParams Natural
5
        ArithmeticCircuit F
ac <- Gen (ArithmeticCircuit F)
forall a. Arbitrary a => Gen a
arbitrary
        F
-> F -> F -> Map Natural F -> ArithmeticCircuit F -> F -> Plonk d t
forall {k} (d :: Natural) (t :: k).
F
-> F -> F -> Map Natural F -> ArithmeticCircuit F -> F -> Plonk d t
Plonk F
omega F
k1 F
k2 (Natural -> F -> Map Natural F
forall k a. k -> a -> Map k a
singleton (ArithmeticCircuit F -> Natural
forall a. ArithmeticCircuit a -> Natural
acOutput ArithmeticCircuit F
ac) F
15) ArithmeticCircuit F
ac (F -> Plonk d t) -> Gen F -> Gen (Plonk d t)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen F
forall a. Arbitrary a => Gen a
arbitrary

type PlonkPermutationSize d = 3 * d

-- TODO (Issue #25): check that the extended polynomials are of the right size
type PlonkMaxPolyDegree d = 4 * d + 7

type PlonkPolyExtended d = PolyVec F (PlonkMaxPolyDegree d)

data PlonkSetupParams = PlonkSetupParams {
        PlonkSetupParams -> F
omega :: F,
        PlonkSetupParams -> F
k1    :: F,
        PlonkSetupParams -> F
k2    :: F,
        PlonkSetupParams -> Vector G1
gs    :: V.Vector G1,
        PlonkSetupParams -> G2
h0    :: G2,
        PlonkSetupParams -> G2
h1    :: G2
    }
    deriving (Int -> PlonkSetupParams -> ShowS
[PlonkSetupParams] -> ShowS
PlonkSetupParams -> String
(Int -> PlonkSetupParams -> ShowS)
-> (PlonkSetupParams -> String)
-> ([PlonkSetupParams] -> ShowS)
-> Show PlonkSetupParams
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PlonkSetupParams -> ShowS
showsPrec :: Int -> PlonkSetupParams -> ShowS
$cshow :: PlonkSetupParams -> String
show :: PlonkSetupParams -> String
$cshowList :: [PlonkSetupParams] -> ShowS
showList :: [PlonkSetupParams] -> ShowS
Show)

data PlonkCircuitPolynomials d = PlonkCircuitPolynomials {
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
ql     :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qr     :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qo     :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qm     :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qc     :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma1 :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma2 :: PlonkPolyExtended d,
        forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma3 :: PlonkPolyExtended d
    }
    deriving (Int -> PlonkCircuitPolynomials d -> ShowS
[PlonkCircuitPolynomials d] -> ShowS
PlonkCircuitPolynomials d -> String
(Int -> PlonkCircuitPolynomials d -> ShowS)
-> (PlonkCircuitPolynomials d -> String)
-> ([PlonkCircuitPolynomials d] -> ShowS)
-> Show (PlonkCircuitPolynomials d)
forall (d :: Natural). Int -> PlonkCircuitPolynomials d -> ShowS
forall (d :: Natural). [PlonkCircuitPolynomials d] -> ShowS
forall (d :: Natural). PlonkCircuitPolynomials d -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (d :: Natural). Int -> PlonkCircuitPolynomials d -> ShowS
showsPrec :: Int -> PlonkCircuitPolynomials d -> ShowS
$cshow :: forall (d :: Natural). PlonkCircuitPolynomials d -> String
show :: PlonkCircuitPolynomials d -> String
$cshowList :: forall (d :: Natural). [PlonkCircuitPolynomials d] -> ShowS
showList :: [PlonkCircuitPolynomials d] -> ShowS
Show)

data PlonkCircuitCommitments = PlonkCircuitCommitments {
        PlonkCircuitCommitments -> G1
cmQl :: G1,
        PlonkCircuitCommitments -> G1
cmQr :: G1,
        PlonkCircuitCommitments -> G1
cmQo :: G1,
        PlonkCircuitCommitments -> G1
cmQm :: G1,
        PlonkCircuitCommitments -> G1
cmQc :: G1,
        PlonkCircuitCommitments -> G1
cmS1 :: G1,
        PlonkCircuitCommitments -> G1
cmS2 :: G1,
        PlonkCircuitCommitments -> G1
cmS3 :: G1
    }
    deriving (Int -> PlonkCircuitCommitments -> ShowS
[PlonkCircuitCommitments] -> ShowS
PlonkCircuitCommitments -> String
(Int -> PlonkCircuitCommitments -> ShowS)
-> (PlonkCircuitCommitments -> String)
-> ([PlonkCircuitCommitments] -> ShowS)
-> Show PlonkCircuitCommitments
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PlonkCircuitCommitments -> ShowS
showsPrec :: Int -> PlonkCircuitCommitments -> ShowS
$cshow :: PlonkCircuitCommitments -> String
show :: PlonkCircuitCommitments -> String
$cshowList :: [PlonkCircuitCommitments] -> ShowS
showList :: [PlonkCircuitCommitments] -> ShowS
Show)

data PlonkPermutation d = PlonkPermutation {
        forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s1 :: PolyVec F d,
        forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s2 :: PolyVec F d,
        forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s3 :: PolyVec F d
    }
    deriving (Int -> PlonkPermutation d -> ShowS
[PlonkPermutation d] -> ShowS
PlonkPermutation d -> String
(Int -> PlonkPermutation d -> ShowS)
-> (PlonkPermutation d -> String)
-> ([PlonkPermutation d] -> ShowS)
-> Show (PlonkPermutation d)
forall (d :: Natural). Int -> PlonkPermutation d -> ShowS
forall (d :: Natural). [PlonkPermutation d] -> ShowS
forall (d :: Natural). PlonkPermutation d -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: forall (d :: Natural). Int -> PlonkPermutation d -> ShowS
showsPrec :: Int -> PlonkPermutation d -> ShowS
$cshow :: forall (d :: Natural). PlonkPermutation d -> String
show :: PlonkPermutation d -> String
$cshowList :: forall (d :: Natural). [PlonkPermutation d] -> ShowS
showList :: [PlonkPermutation d] -> ShowS
Show)

newtype PlonkWitnessMap d = PlonkWitnessMap (Map.Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d))
-- TODO (Issue #25): make a proper implementation of Show
instance Show (PlonkWitnessMap d) where
    show :: PlonkWitnessMap d -> String
show PlonkWitnessMap d
_ = String
"PlonkWitnessMap"

newtype PlonkWitnessInput = PlonkWitnessInput (Map.Map Natural F)
-- TODO (Issue #25): make a proper implementation of Show
instance Show PlonkWitnessInput where
    show :: PlonkWitnessInput -> String
show PlonkWitnessInput
_ = String
"PlonkWitnessInput"
-- TODO (Issue #25): make a proper implementation of Arbitrary
instance Arbitrary PlonkWitnessInput where
    arbitrary :: Gen PlonkWitnessInput
arbitrary = do
        F
x <- Gen F
forall a. Arbitrary a => Gen a
arbitrary
        PlonkWitnessInput -> Gen PlonkWitnessInput
forall a. a -> Gen a
forall (m :: Type -> Type) a. Monad m => a -> m a
return (PlonkWitnessInput -> Gen PlonkWitnessInput)
-> PlonkWitnessInput -> Gen PlonkWitnessInput
forall a b. (a -> b) -> a -> b
$ Map Natural F -> PlonkWitnessInput
PlonkWitnessInput (Map Natural F -> PlonkWitnessInput)
-> Map Natural F -> PlonkWitnessInput
forall a b. (a -> b) -> a -> b
$ [Item (Map Natural F)] -> Map Natural F
forall l. IsList l => [Item l] -> l
fromList [(Natural
1, F
x), (Natural
2, F
15F -> F -> F
forall a. Field a => a -> a -> a
//F
x)]

data PlonkProverSecret = PlonkProverSecret F F F F F F F F F F F
    deriving (Int -> PlonkProverSecret -> ShowS
[PlonkProverSecret] -> ShowS
PlonkProverSecret -> String
(Int -> PlonkProverSecret -> ShowS)
-> (PlonkProverSecret -> String)
-> ([PlonkProverSecret] -> ShowS)
-> Show PlonkProverSecret
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PlonkProverSecret -> ShowS
showsPrec :: Int -> PlonkProverSecret -> ShowS
$cshow :: PlonkProverSecret -> String
show :: PlonkProverSecret -> String
$cshowList :: [PlonkProverSecret] -> ShowS
showList :: [PlonkProverSecret] -> ShowS
Show)
instance Arbitrary PlonkProverSecret where
    arbitrary :: Gen PlonkProverSecret
arbitrary = F
-> F
-> F
-> F
-> F
-> F
-> F
-> F
-> F
-> F
-> F
-> PlonkProverSecret
PlonkProverSecret (F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> F
 -> PlonkProverSecret)
-> Gen F
-> Gen
     (F
      -> F -> F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$>
        Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen
  (F
   -> F -> F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F
-> Gen
     (F -> F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen
  (F -> F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F
-> Gen (F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F
-> Gen (F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> F -> F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary
        Gen (F -> F -> F -> F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> F -> PlonkProverSecret)
-> Gen F -> Gen (F -> PlonkProverSecret)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary Gen (F -> PlonkProverSecret) -> Gen F -> Gen PlonkProverSecret
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> Gen F
forall a. Arbitrary a => Gen a
arbitrary

newtype PlonkInput = PlonkInput (V.Vector F)
    deriving (Int -> PlonkInput -> ShowS
[PlonkInput] -> ShowS
PlonkInput -> String
(Int -> PlonkInput -> ShowS)
-> (PlonkInput -> String)
-> ([PlonkInput] -> ShowS)
-> Show PlonkInput
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PlonkInput -> ShowS
showsPrec :: Int -> PlonkInput -> ShowS
$cshow :: PlonkInput -> String
show :: PlonkInput -> String
$cshowList :: [PlonkInput] -> ShowS
showList :: [PlonkInput] -> ShowS
Show)

data PlonkProof = PlonkProof G1 G1 G1 G1 G1 G1 G1 G1 G1 F F F F F F
    deriving (Int -> PlonkProof -> ShowS
[PlonkProof] -> ShowS
PlonkProof -> String
(Int -> PlonkProof -> ShowS)
-> (PlonkProof -> String)
-> ([PlonkProof] -> ShowS)
-> Show PlonkProof
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> PlonkProof -> ShowS
showsPrec :: Int -> PlonkProof -> ShowS
$cshow :: PlonkProof -> String
show :: PlonkProof -> String
$cshowList :: [PlonkProof] -> ShowS
showList :: [PlonkProof] -> ShowS
Show)

-- TODO (Issue #18): make the code safer, check list lengths (?)
instance forall d t .
        (KnownNat d,
         KnownNat (PlonkPermutationSize d),
         KnownNat (PlonkMaxPolyDegree d),
         ToTranscript t F,
         ToTranscript t G1,
         FromTranscript t F) => NonInteractiveProof (Plonk d t) where
    type Transcript (Plonk d t)   = t
    type Setup (Plonk d t)        = (PlonkSetupParams, PlonkPermutation d, PlonkCircuitPolynomials d, PlonkCircuitCommitments,
        PlonkInput, PlonkWitnessMap d)
    type Witness (Plonk d t)      = (PlonkWitnessInput, PlonkProverSecret)
    type Input (Plonk d t)        = PlonkInput
    type Proof (Plonk d t)        = PlonkProof

    setup :: Plonk d t -> Setup (Plonk d t)
    setup :: Plonk d t -> Setup (Plonk d t)
setup (Plonk F
omega F
k1 F
k2 Map Natural F
inputs ArithmeticCircuit F
ac F
x) =
        let wmap :: Map Natural F -> Map Natural F
wmap = ArithmeticCircuit F -> Map Natural F -> Map Natural F
forall a. ArithmeticCircuit a -> Map Natural a -> Map Natural a
acWitness (ArithmeticCircuit F -> Map Natural F -> Map Natural F)
-> ArithmeticCircuit F -> Map Natural F -> Map Natural F
forall a b. (a -> b) -> a -> b
$ ArithmeticCircuit F -> ArithmeticCircuit F
forall a.
MultiplicativeMonoid a =>
ArithmeticCircuit a -> ArithmeticCircuit a
mapVarArithmeticCircuit ArithmeticCircuit F
ac
            (PolyVec F d
qlAC, PolyVec F d
qrAC, PolyVec F d
qoAC, PolyVec F d
qmAC, PolyVec F d
qcAC, PolyVec F d
a, PolyVec F d
b, PolyVec F d
c) = Map Natural F
-> ArithmeticCircuit F
-> (PolyVec F d, PolyVec F d, PolyVec F d, PolyVec F d,
    PolyVec F d, PolyVec F d, PolyVec F d, PolyVec F d)
forall (a :: Natural).
KnownNat a =>
Map Natural F
-> ArithmeticCircuit F
-> (PolyVec F a, PolyVec F a, PolyVec F a, PolyVec F a,
    PolyVec F a, PolyVec F a, PolyVec F a, PolyVec F a)
toPlonkArithmetization Map Natural F
Map Natural F
inputs ArithmeticCircuit F
ArithmeticCircuit F
ac
            wPub :: Vector F
wPub = [Item (Vector F)] -> Vector F
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector F)] -> Vector F) -> [Item (Vector F)] -> Vector F
forall a b. (a -> b) -> a -> b
$ (F -> Item (Vector F)) -> [F] -> [Item (Vector F)]
forall a b. (a -> b) -> [a] -> [b]
map F -> Item (Vector F)
F -> F
forall a. AdditiveGroup a => a -> a
negate ([F] -> [Item (Vector F)]) -> [F] -> [Item (Vector F)]
forall a b. (a -> b) -> a -> b
$ Map Natural F -> [F]
forall k a. Map k a -> [a]
elems Map Natural F
inputs

            d :: Natural
d = forall (n :: Natural). KnownNat n => Natural
value @d Natural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+ Natural
6
            xs :: Vector F
xs = [Item (Vector F)] -> Vector F
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector F)] -> Vector F) -> [Item (Vector F)] -> Vector F
forall a b. (a -> b) -> a -> b
$ (Natural -> F) -> [Natural] -> [F]
forall a b. (a -> b) -> [a] -> [b]
map (F
xF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^) [Natural
Item [Natural]
0..Natural
dNatural -> Natural -> Natural
-!Natural
1]
            gs :: Vector G1
gs = (F -> G1) -> Vector F -> Vector G1
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen) Vector F
xs
            h0 :: G2
h0 = G2
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen
            h1 :: G2
h1 = ScalarField BLS12_381_G2
F
x ScalarField BLS12_381_G2 -> G2 -> G2
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G2
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen

            s :: [Natural]
s = forall (n :: Natural). Permutation n -> [Natural]
fromPermutation @(PlonkPermutationSize d) (Permutation (PlonkPermutationSize d) -> [Natural])
-> Permutation (PlonkPermutationSize d) -> [Natural]
forall a b. (a -> b) -> a -> b
$ IndexPartition Natural -> Permutation (PlonkPermutationSize d)
forall (n :: Natural) a.
KnownNat n =>
IndexPartition a -> Permutation n
fromCycles (IndexPartition Natural -> Permutation (PlonkPermutationSize d))
-> IndexPartition Natural -> Permutation (PlonkPermutationSize d)
forall a b. (a -> b) -> a -> b
$
                    Vector Natural -> IndexPartition Natural
forall a. Ord a => Vector a -> IndexPartition a
mkIndexPartition (Vector Natural -> IndexPartition Natural)
-> Vector Natural -> IndexPartition Natural
forall a b. (a -> b) -> a -> b
$ (F -> Natural) -> Vector F -> Vector Natural
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap F -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp (Vector F -> Vector Natural) -> Vector F -> Vector Natural
forall a b. (a -> b) -> a -> b
$ PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
a Vector F -> Vector F -> Vector F
forall a. Vector a -> Vector a -> Vector a
V.++ PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
b Vector F -> Vector F -> Vector F
forall a. Vector a -> Vector a -> Vector a
V.++ PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
c
            f :: Natural -> F
f Natural
i = case (Natural
iNatural -> Natural -> Natural
-!Natural
1) Natural -> Natural -> Natural
forall a. EuclideanDomain a => a -> a -> a
`div` forall (n :: Natural). KnownNat n => Natural
value @d of
                Natural
0 -> F
omegaF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^Natural
i
                Natural
1 -> F
k1 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
omegaF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^Natural
i)
                Natural
2 -> F
k2 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
omegaF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^Natural
i)
                Natural
_ -> String -> F
forall a. HasCallStack => String -> a
error String
"setup: invalid index"
            s' :: Vector F
s' = [Item (Vector F)] -> Vector F
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector F)] -> Vector F) -> [Item (Vector F)] -> Vector F
forall a b. (a -> b) -> a -> b
$ (Natural -> F) -> [Natural] -> [F]
forall a b. (a -> b) -> [a] -> [b]
map Natural -> F
f [Natural]
s
            s1 :: PolyVec F d
s1 = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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 @d) Vector F
s'
            s2 :: PolyVec F d
s2 = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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 @d) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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 @d) Vector F
s'
            s3 :: PolyVec F d
s3 = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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 @d) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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 @d) Vector F
s'
            w1 :: Map Natural F -> PolyVec F d
w1 Map Natural F
i    = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ (F -> F) -> Vector F -> Vector F
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Map Natural F -> Map Natural F
wmap Map Natural F
i Map Natural F -> Natural -> F
forall k a. Ord k => Map k a -> k -> a
!) (Natural -> F) -> (F -> Natural) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp) (PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
a)
            w2 :: Map Natural F -> PolyVec F d
w2 Map Natural F
i    = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ (F -> F) -> Vector F -> Vector F
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Map Natural F -> Map Natural F
wmap Map Natural F
i Map Natural F -> Natural -> F
forall k a. Ord k => Map k a -> k -> a
!) (Natural -> F) -> (F -> Natural) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp) (PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
b)
            w3 :: Map Natural F -> PolyVec F d
w3 Map Natural F
i    = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ (F -> F) -> Vector F -> Vector F
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Map Natural F -> Map Natural F
wmap Map Natural F
i Map Natural F -> Natural -> F
forall k a. Ord k => Map k a -> k -> a
!) (Natural -> F) -> (F -> Natural) -> F -> F
forall b c a. (b -> c) -> (a -> b) -> a -> c
. F -> Natural
forall (p :: Natural). Zp p -> Natural
fromZp) (PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
PolyVec F d
c)
            wmap' :: Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d)
wmap' Map Natural F
i = (Map Natural F -> PolyVec F d
w1 Map Natural F
i, Map Natural F -> PolyVec F d
w2 Map Natural F
i, Map Natural F -> PolyVec F d
w3 Map Natural F
i)

            qm :: PolyVec F (PlonkMaxPolyDegree d)
qm     = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
PolyVec F d
qmAC
            ql :: PolyVec F (PlonkMaxPolyDegree d)
ql     = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
PolyVec F d
qlAC
            qr :: PolyVec F (PlonkMaxPolyDegree d)
qr     = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
PolyVec F d
qrAC
            qo :: PolyVec F (PlonkMaxPolyDegree d)
qo     = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
PolyVec F d
qoAC
            qc :: PolyVec F (PlonkMaxPolyDegree d)
qc     = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
PolyVec F d
qcAC
            sigma1 :: PolyVec F (PlonkMaxPolyDegree d)
sigma1 = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
s1
            sigma2 :: PolyVec F (PlonkMaxPolyDegree d)
sigma2 = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
s2
            sigma3 :: PolyVec F (PlonkMaxPolyDegree d)
sigma3 = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
s3

            cmQl :: G1
cmQl = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
ql
            cmQr :: G1
cmQr = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
qr
            cmQo :: G1
cmQo = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
qo
            cmQm :: G1
cmQm = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
qm
            cmQc :: G1
cmQc = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
qc
            cmS1 :: G1
cmS1 = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
sigma1
            cmS2 :: G1
cmS2 = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
sigma2
            cmS3 :: G1
cmS3 = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
sigma3
        in (PlonkSetupParams {Vector G1
G2
F
omega :: F
k1 :: F
k2 :: F
gs :: Vector G1
h0 :: G2
h1 :: G2
omega :: F
k1 :: F
k2 :: F
gs :: Vector G1
h0 :: G2
h1 :: G2
..}, PlonkPermutation {PolyVec F d
s1 :: PolyVec F d
s2 :: PolyVec F d
s3 :: PolyVec F d
s1 :: PolyVec F d
s2 :: PolyVec F d
s3 :: PolyVec F d
..}, PlonkCircuitPolynomials {PolyVec F (PlonkMaxPolyDegree d)
ql :: PolyVec F (PlonkMaxPolyDegree d)
qr :: PolyVec F (PlonkMaxPolyDegree d)
qo :: PolyVec F (PlonkMaxPolyDegree d)
qm :: PolyVec F (PlonkMaxPolyDegree d)
qc :: PolyVec F (PlonkMaxPolyDegree d)
sigma1 :: PolyVec F (PlonkMaxPolyDegree d)
sigma2 :: PolyVec F (PlonkMaxPolyDegree d)
sigma3 :: PolyVec F (PlonkMaxPolyDegree d)
qm :: PolyVec F (PlonkMaxPolyDegree d)
ql :: PolyVec F (PlonkMaxPolyDegree d)
qr :: PolyVec F (PlonkMaxPolyDegree d)
qo :: PolyVec F (PlonkMaxPolyDegree d)
qc :: PolyVec F (PlonkMaxPolyDegree d)
sigma1 :: PolyVec F (PlonkMaxPolyDegree d)
sigma2 :: PolyVec F (PlonkMaxPolyDegree d)
sigma3 :: PolyVec F (PlonkMaxPolyDegree d)
..}, PlonkCircuitCommitments {G1
cmQl :: G1
cmQr :: G1
cmQo :: G1
cmQm :: G1
cmQc :: G1
cmS1 :: G1
cmS2 :: G1
cmS3 :: G1
cmQl :: G1
cmQr :: G1
cmQo :: G1
cmQm :: G1
cmQc :: G1
cmS1 :: G1
cmS2 :: G1
cmS3 :: G1
..},
            Vector F -> PlonkInput
PlonkInput Vector F
wPub, (Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d))
-> PlonkWitnessMap d
forall (d :: Natural).
(Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d))
-> PlonkWitnessMap d
PlonkWitnessMap Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d)
wmap')

    prove :: Setup (Plonk d t) -> Witness (Plonk d t) -> (Input (Plonk d t), Proof (Plonk d t))
    prove :: Setup (Plonk d t)
-> Witness (Plonk d t) -> (Input (Plonk d t), Proof (Plonk d t))
prove (PlonkSetupParams {Vector G1
G2
F
omega :: PlonkSetupParams -> F
k1 :: PlonkSetupParams -> F
k2 :: PlonkSetupParams -> F
gs :: PlonkSetupParams -> Vector G1
h0 :: PlonkSetupParams -> G2
h1 :: PlonkSetupParams -> G2
omega :: F
k1 :: F
k2 :: F
gs :: Vector G1
h0 :: G2
h1 :: G2
..}, PlonkPermutation {PolyVec F d
s1 :: forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s2 :: forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s3 :: forall (d :: Natural). PlonkPermutation d -> PolyVec F d
s1 :: PolyVec F d
s2 :: PolyVec F d
s3 :: PolyVec F d
..}, PlonkCircuitPolynomials {PolyVec F (PlonkMaxPolyDegree d)
ql :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qr :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qo :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qm :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
qc :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma1 :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma2 :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
sigma3 :: forall (d :: Natural).
PlonkCircuitPolynomials d -> PlonkPolyExtended d
ql :: PolyVec F (PlonkMaxPolyDegree d)
qr :: PolyVec F (PlonkMaxPolyDegree d)
qo :: PolyVec F (PlonkMaxPolyDegree d)
qm :: PolyVec F (PlonkMaxPolyDegree d)
qc :: PolyVec F (PlonkMaxPolyDegree d)
sigma1 :: PolyVec F (PlonkMaxPolyDegree d)
sigma2 :: PolyVec F (PlonkMaxPolyDegree d)
sigma3 :: PolyVec F (PlonkMaxPolyDegree d)
..}, PlonkCircuitCommitments
_, PlonkInput Vector F
wPub, PlonkWitnessMap Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d)
wmap)
        (PlonkWitnessInput Map Natural F
wInput, PlonkProverSecret F
b1 F
b2 F
b3 F
b4 F
b5 F
b6 F
b7 F
b8 F
b9 F
b10 F
b11)
            = (Vector F -> PlonkInput
PlonkInput Vector F
wPub, G1
-> G1
-> G1
-> G1
-> G1
-> G1
-> G1
-> G1
-> G1
-> F
-> F
-> F
-> F
-> F
-> F
-> PlonkProof
PlonkProof G1
cmA G1
cmB G1
cmC G1
cmZ G1
cmT1 G1
cmT2 G1
cmT3 G1
proof1 G1
proof2 F
a_xi F
b_xi F
c_xi F
s1_xi F
s2_xi F
z_xi)
        where
            n :: Natural
n = forall (n :: Natural). KnownNat n => Natural
value @d
            zH :: PolyVec F (PlonkMaxPolyDegree d)
zH = forall c (size :: Natural) (size' :: Natural).
(Field c, KnownNat size, KnownNat size', Eq c) =>
PolyVec c size'
polyVecZero @F @d @(PlonkMaxPolyDegree d)

            (PolyVec F d
w1, PolyVec F d
w2, PolyVec F d
w3) = Map Natural F -> (PolyVec F d, PolyVec F d, PolyVec F d)
wmap Map Natural F
wInput
            pubPoly :: PolyVec F (PlonkMaxPolyDegree d)
pubPoly = F -> PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis F
omega (PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d))
-> PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d)
forall a b. (a -> b) -> a -> b
$ forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @F @d Vector F
wPub

            a :: PolyVec F (PlonkMaxPolyDegree d)
a = F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
b2 F
b1 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
zH PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis F
omega PolyVec F d
w1
            b :: PolyVec F (PlonkMaxPolyDegree d)
b = F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
b4 F
b3 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
zH PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis F
omega PolyVec F d
w2
            c :: PolyVec F (PlonkMaxPolyDegree d)
c = F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
b6 F
b5 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
zH PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> PolyVec F d -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis F
omega PolyVec F d
w3

            cmA :: G1
cmA = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
a
            cmB :: G1
cmB = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
b
            cmC :: G1
cmC = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
c

            (F
beta, t
ts) = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
forall a. Monoid a => a
mempty
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmA
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmB
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmC
            (F
gamma, t
ts') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge t
ts

            omegas :: PolyVec F d
omegas  = Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F d) -> Vector F -> PolyVec F d
forall a b. (a -> b) -> a -> b
$ Int -> (F -> F) -> F -> Vector F
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
omega) F
omega
            omegas' :: Vector F
omegas' =  Int -> (F -> F) -> F -> Vector F
forall a. Int -> (a -> a) -> a -> Vector a
V.iterateN (Vector F -> Int
forall a. Vector a -> Int
V.length (PolyVec F (PlonkMaxPolyDegree d) -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F (PlonkMaxPolyDegree d)
z) Int -> Int -> Int
forall a. Num a => a -> a -> a
P.+ Int
1) (F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
omega) F
forall a. MultiplicativeMonoid a => a
one
            zs1 :: PolyVec F d
zs1 = PolyVec F d -> PolyVec F d -> PolyVec F d -> F -> F -> PolyVec F d
forall c (size :: Natural).
(Field c, KnownNat size) =>
PolyVec c size
-> PolyVec c size -> PolyVec c size -> c -> c -> PolyVec c size
polyVecGrandProduct PolyVec F d
w1 PolyVec F d
omegas PolyVec F d
s1 F
beta F
gamma
            zs2 :: PolyVec F d
zs2 = PolyVec F d -> PolyVec F d -> PolyVec F d -> F -> F -> PolyVec F d
forall c (size :: Natural).
(Field c, KnownNat size) =>
PolyVec c size
-> PolyVec c size -> PolyVec c size -> c -> c -> PolyVec c size
polyVecGrandProduct PolyVec F d
w2 (F -> PolyVec F d -> PolyVec F d
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
k1 PolyVec F d
omegas) PolyVec F d
s2 F
beta F
gamma
            zs3 :: PolyVec F d
zs3 = PolyVec F d -> PolyVec F d -> PolyVec F d -> F -> F -> PolyVec F d
forall c (size :: Natural).
(Field c, KnownNat size) =>
PolyVec c size
-> PolyVec c size -> PolyVec c size -> c -> c -> PolyVec c size
polyVecGrandProduct PolyVec F d
w3 (F -> PolyVec F d -> PolyVec F d
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
k2 PolyVec F d
omegas) PolyVec F d
s3 F
beta F
gamma
            gp :: PolyVec F d
gp = (Vector F -> Vector F) -> PolyVec F d -> PolyVec F d
forall c (size :: Natural).
(Vector c -> Vector c) -> PolyVec c size -> PolyVec c size
rewrapPolyVec ((F -> F -> F) -> Vector F -> Vector F -> Vector F
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) ((F -> F -> F) -> Vector F -> Vector F -> Vector F
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
zs1) (PolyVec F d -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F d
zs2))) PolyVec F d
zs3
            z :: PolyVec F (PlonkMaxPolyDegree d)
z  = F -> F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> c -> PolyVec c size
polyVecQuadratic F
b9 F
b8 F
b7 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
zH PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega PolyVec F d
gp
            zo :: PolyVec F (PlonkMaxPolyDegree d)
zo = Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F (PlonkMaxPolyDegree d))
-> Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall a b. (a -> b) -> a -> b
$ (F -> F -> F) -> Vector F -> Vector F -> Vector F
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
(*) (PolyVec F (PlonkMaxPolyDegree d) -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F (PlonkMaxPolyDegree d)
z) Vector F
omegas'
            cmZ :: G1
cmZ = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
z

            (F
alpha, Transcript (Plonk d t)
ts'') = Transcript (Plonk d t) -> (F, Transcript (Plonk d t))
forall t a. FromTranscript t a => t -> (a, t)
challenge (Transcript (Plonk d t) -> (F, Transcript (Plonk d t)))
-> Transcript (Plonk d t) -> (F, Transcript (Plonk d t))
forall a b. (a -> b) -> a -> b
$ t
ts' t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmZ :: (F, Transcript (Plonk d t))

            t1 :: PolyVec F (PlonkMaxPolyDegree d)
t1  = PolyVec F (PlonkMaxPolyDegree d)
a PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
b PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
qm PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
a PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
ql PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
b PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
qr PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
c PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
qo PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
pubPoly PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
qc
            t2 :: PolyVec F (PlonkMaxPolyDegree d)
t2  = (PolyVec F (PlonkMaxPolyDegree d)
a PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
gamma F
beta)
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* (PolyVec F (PlonkMaxPolyDegree d)
b PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
gamma (F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k1))
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* (PolyVec F (PlonkMaxPolyDegree d)
c PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear F
gamma (F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k2))
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
z
            t3 :: PolyVec F (PlonkMaxPolyDegree d)
t3  = (PolyVec F (PlonkMaxPolyDegree d)
a PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
beta PolyVec F (PlonkMaxPolyDegree d)
sigma1 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
gamma PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* (PolyVec F (PlonkMaxPolyDegree d)
b PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
beta PolyVec F (PlonkMaxPolyDegree d)
sigma2 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
gamma PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* (PolyVec F (PlonkMaxPolyDegree d)
c PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
beta PolyVec F (PlonkMaxPolyDegree d)
sigma3 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
gamma PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* PolyVec F (PlonkMaxPolyDegree d)
zo
            t4 :: PolyVec F (PlonkMaxPolyDegree d)
t4 = (PolyVec F (PlonkMaxPolyDegree d)
z PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeSemigroup a => a -> a -> a
* forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
Natural -> c -> PolyVec c size'
polyVecLagrange @F @d @(PlonkMaxPolyDegree d) Natural
1 F
omega
            t :: PolyVec F (PlonkMaxPolyDegree d)
t = (PolyVec F (PlonkMaxPolyDegree d)
t1 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
alpha (PolyVec F (PlonkMaxPolyDegree d)
t2 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec F (PlonkMaxPolyDegree d)
t3) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
alpha) PolyVec F (PlonkMaxPolyDegree d)
t4) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` PolyVec F (PlonkMaxPolyDegree d)
zH

            t_lo' :: PolyVec F (PlonkMaxPolyDegree d)
t_lo'  = Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F (PlonkMaxPolyDegree d))
-> Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
forall a. Int -> Vector a -> Vector a
V.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ PolyVec F (PlonkMaxPolyDegree d) -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F (PlonkMaxPolyDegree d)
t
            t_mid' :: PolyVec F (PlonkMaxPolyDegree d)
t_mid' = Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F (PlonkMaxPolyDegree d))
-> Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
forall a. Int -> Vector a -> Vector a
V.take (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
forall a. Int -> Vector a -> Vector a
V.drop (Natural -> Int
forall a b. (Integral a, Num b) => a -> b
fromIntegral Natural
n) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ PolyVec F (PlonkMaxPolyDegree d) -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F (PlonkMaxPolyDegree d)
t
            t_hi' :: PolyVec F (PlonkMaxPolyDegree d)
t_hi'  = Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec (Vector F -> PolyVec F (PlonkMaxPolyDegree d))
-> Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall a b. (a -> b) -> a -> b
$ Int -> Vector F -> Vector F
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
2Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
*Natural
n) (Vector F -> Vector F) -> Vector F -> Vector F
forall a b. (a -> b) -> a -> b
$ PolyVec F (PlonkMaxPolyDegree d) -> Vector F
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec F (PlonkMaxPolyDegree d)
t
            t_lo :: PolyVec F (PlonkMaxPolyDegree d)
t_lo   = PolyVec F (PlonkMaxPolyDegree d)
t_lo' PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b10 (forall c (size :: Natural) (size' :: Natural).
(Field c, KnownNat size, KnownNat size', Eq c) =>
PolyVec c size'
polyVecZero @F @d @(PlonkMaxPolyDegree d) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
            t_mid :: PolyVec F (PlonkMaxPolyDegree d)
t_mid  = PolyVec F (PlonkMaxPolyDegree d)
t_mid' PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b11 (forall c (size :: Natural) (size' :: Natural).
(Field c, KnownNat size, KnownNat size', Eq c) =>
PolyVec c size'
polyVecZero @F @d @(PlonkMaxPolyDegree d) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b10 PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one
            t_hi :: PolyVec F (PlonkMaxPolyDegree d)
t_hi   = PolyVec F (PlonkMaxPolyDegree d)
t_hi' PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b11 PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one
            cmT1 :: G1
cmT1   = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
t_lo
            cmT2 :: G1
cmT2   = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
t_mid
            cmT3 :: G1
cmT3   = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
t_hi

            (F
xi, t
ts''') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
Transcript (Plonk d t)
ts''
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT1
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT2
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT3

            a_xi :: F
a_xi  = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
a F
xi
            b_xi :: F
b_xi  = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
b F
xi
            c_xi :: F
c_xi  = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
c F
xi
            s1_xi :: F
s1_xi = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
sigma1 F
xi
            s2_xi :: F
s2_xi = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
sigma2 F
xi
            z_xi :: F
z_xi  = PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
evalPolyVec PolyVec F (PlonkMaxPolyDegree d)
z (F
xi F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
omega)

            (F
v, t
_) = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
ts'''
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
a_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
b_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
c_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
s1_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
s2_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
z_xi

            lagrange1_xi :: F
lagrange1_xi = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
Natural -> c -> PolyVec c size'
polyVecLagrange @F @d @(PlonkMaxPolyDegree d) Natural
1 F
omega PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi
            zH_xi :: F
zH_xi = PolyVec F (PlonkMaxPolyDegree d)
zH PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi
            r :: PolyVec F (PlonkMaxPolyDegree d)
r   = F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
a_xi F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
b_xi) PolyVec F (PlonkMaxPolyDegree d)
qm
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
a_xi PolyVec F (PlonkMaxPolyDegree d)
ql
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b_xi PolyVec F (PlonkMaxPolyDegree d)
qr
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
c_xi PolyVec F (PlonkMaxPolyDegree d)
qo
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (PolyVec F (PlonkMaxPolyDegree d)
pubPoly PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi) PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
qc
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
alpha (
                    F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (
                          (F
a_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
b_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k1 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
c_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k2 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        ) PolyVec F (PlonkMaxPolyDegree d)
z
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (
                          (F
a_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s1_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
b_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s2_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
z_xi
                        ) (F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
beta PolyVec F (PlonkMaxPolyDegree d)
sigma3 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
c_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma) PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                    )
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
lagrange1_xi) (PolyVec F (PlonkMaxPolyDegree d)
z PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
zH_xi (F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
xiF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^(Natural
2 Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
* Natural
n)) PolyVec F (PlonkMaxPolyDegree d)
t_hi PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
xiF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^Natural
n) PolyVec F (PlonkMaxPolyDegree d)
t_mid PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ PolyVec F (PlonkMaxPolyDegree d)
t_lo)

            proof1Poly :: PolyVec F (PlonkMaxPolyDegree d)
proof1Poly = (PolyVec F (PlonkMaxPolyDegree d)
r
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
v (PolyVec F (PlonkMaxPolyDegree d)
a PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
a_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) (PolyVec F (PlonkMaxPolyDegree d)
b PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
b_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) (PolyVec F (PlonkMaxPolyDegree d)
c PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
c_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) (PolyVec F (PlonkMaxPolyDegree d)
sigma1 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
s1_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                    PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveSemigroup a => a -> a -> a
+ F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) (PolyVec F (PlonkMaxPolyDegree d)
sigma2 PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
s2_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one)
                ) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` F -> F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
polyVecLinear (F -> F
forall a. AdditiveGroup a => a -> a
negate F
xi) F
forall a. MultiplicativeMonoid a => a
one
            proof2Poly :: PolyVec F (PlonkMaxPolyDegree d)
proof2Poly = (PolyVec F (PlonkMaxPolyDegree d)
z PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall a. AdditiveGroup a => a -> a -> a
- F
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV F
z_xi PolyVec F (PlonkMaxPolyDegree d)
forall a. MultiplicativeMonoid a => a
one) PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
-> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` Vector F -> PolyVec F (PlonkMaxPolyDegree d)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec [F -> F
forall a. AdditiveGroup a => a -> a
negate (F
xi F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
omega), Item (Vector F)
F
forall a. MultiplicativeMonoid a => a
one]
            proof1 :: G1
proof1 = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
proof1Poly
            proof2 :: G1
proof2 = Vector G1
gs Vector G1 -> PolyVec F (PlonkMaxPolyDegree d) -> G1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec F (PlonkMaxPolyDegree d)
proof2Poly

    verify :: Setup (Plonk d t) -> Input (Plonk d t) -> Proof (Plonk d t) -> Bool
    verify :: Setup (Plonk d t) -> Input (Plonk d t) -> Proof (Plonk d t) -> Bool
verify
        (PlonkSetupParams {Vector G1
G2
F
omega :: PlonkSetupParams -> F
k1 :: PlonkSetupParams -> F
k2 :: PlonkSetupParams -> F
gs :: PlonkSetupParams -> Vector G1
h0 :: PlonkSetupParams -> G2
h1 :: PlonkSetupParams -> G2
omega :: F
k1 :: F
k2 :: F
gs :: Vector G1
h0 :: G2
h1 :: G2
..}, PlonkPermutation d
_, PlonkCircuitPolynomials d
_, PlonkCircuitCommitments {G1
cmQl :: PlonkCircuitCommitments -> G1
cmQr :: PlonkCircuitCommitments -> G1
cmQo :: PlonkCircuitCommitments -> G1
cmQm :: PlonkCircuitCommitments -> G1
cmQc :: PlonkCircuitCommitments -> G1
cmS1 :: PlonkCircuitCommitments -> G1
cmS2 :: PlonkCircuitCommitments -> G1
cmS3 :: PlonkCircuitCommitments -> G1
cmQl :: G1
cmQr :: G1
cmQo :: G1
cmQm :: G1
cmQc :: G1
cmS1 :: G1
cmS2 :: G1
cmS3 :: G1
..}, PlonkInput
_, PlonkWitnessMap d
_)
        (PlonkInput Vector F
ws)
        (PlonkProof G1
cmA G1
cmB G1
cmC G1
cmZ G1
cmT1 G1
cmT2 G1
cmT3 G1
proof1 G1
proof2 F
a_xi F
b_xi F
c_xi F
s1_xi F
s2_xi F
z_xi) = BLS12_381_GT
p1 BLS12_381_GT -> BLS12_381_GT -> Bool
forall a. Eq a => a -> a -> Bool
== BLS12_381_GT
p2
        where
            n :: Natural
n = forall (n :: Natural). KnownNat n => Natural
value @d

            (F
beta, Transcript (Plonk d t)
ts) = Transcript (Plonk d t) -> (F, Transcript (Plonk d t))
forall t a. FromTranscript t a => t -> (a, t)
challenge (Transcript (Plonk d t) -> (F, Transcript (Plonk d t)))
-> Transcript (Plonk d t) -> (F, Transcript (Plonk d t))
forall a b. (a -> b) -> a -> b
$ t
forall a. Monoid a => a
mempty
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmA
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmB
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmC :: (F, Transcript (Plonk d t))
            (F
gamma, t
ts') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge t
Transcript (Plonk d t)
ts

            (F
alpha, t
ts'') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
ts' t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmZ

            (F
xi, t
ts''') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
ts''
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT1
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT2
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
cmT3

            (F
v, t
ts'''') = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
ts'''
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
a_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
b_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
c_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
s1_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
s2_xi
                t -> F -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` F
z_xi

            (F
u, t
_) = t -> (F, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge (t -> (F, t)) -> t -> (F, t)
forall a b. (a -> b) -> a -> b
$ t
ts''''
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
proof1
                t -> G1 -> t
forall t a. ToTranscript t a => t -> a -> t
`transcript` G1
proof2

            zH_xi :: F
zH_xi        = forall c (size :: Natural) (size' :: Natural).
(Field c, KnownNat size, KnownNat size', Eq c) =>
PolyVec c size'
polyVecZero @F @d @(PlonkMaxPolyDegree d) PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi
            lagrange1_xi :: F
lagrange1_xi = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
Natural -> c -> PolyVec c size'
polyVecLagrange @F @d @(PlonkMaxPolyDegree d) Natural
1 F
omega PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi
            pubPoly_xi :: F
pubPoly_xi   = forall c (size :: Natural) (size' :: Natural).
(Field c, Eq c, KnownNat size, KnownNat size') =>
c -> PolyVec c size -> PolyVec c size'
polyVecInLagrangeBasis @F @d @(PlonkMaxPolyDegree d) F
omega (Vector F -> PolyVec F d
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec Vector F
ws) PolyVec F (PlonkMaxPolyDegree d) -> F -> F
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` F
xi

            r0 :: F
r0 =
                  F
pubPoly_xi
                F -> F -> F
forall a. AdditiveGroup a => a -> a -> a
- F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
lagrange1_xi
                F -> F -> F
forall a. AdditiveGroup a => a -> a -> a
- F
alpha
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
a_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s1_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
b_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s2_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
c_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
z_xi
            d :: G1
d  =
                  F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul (F
a_xi F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
b_xi) G1
cmQm
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul F
F
a_xi G1
cmQl
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul F
F
b_xi G1
cmQr
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul F
F
c_xi G1
cmQo
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ G1
cmQc
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul (
                          F
alpha
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
a_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
b_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k1 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                        F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
c_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
k2 F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+     F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
alpha F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
lagrange1_xi
                    F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+     F
u
                    ) G1
cmZ
                G1 -> G1 -> G1
forall a. AdditiveGroup a => a -> a -> a
- F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul (
                      F
alpha
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
beta
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
a_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s1_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* (F
b_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
beta F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s2_xi F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
gamma)
                    F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
z_xi
                    ) G1
cmS3
                G1 -> G1 -> G1
forall a. AdditiveGroup a => a -> a -> a
- F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul F
F
zH_xi (G1
cmT1 G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
xiF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^Natural
n) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmT2 G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
xiF -> Natural -> F
forall a b. Exponent a b => a -> b -> a
^(Natural
2Natural -> Natural -> Natural
forall a. MultiplicativeSemigroup a => a -> a -> a
*Natural
n)) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmT3)
            f :: G1
f  =
                  G1
d
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F
F
v F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmA
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmB
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmC
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmS1
                G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
cmS2
            e :: G1
e  = (
                - F
r0
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
a_xi
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
b_xi
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
c_xi
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s1_xi
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
v F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
s2_xi
                F -> F -> F
forall a. AdditiveSemigroup a => a -> a -> a
+ F
u F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
z_xi
                ) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Vector G1 -> G1
forall a. Vector a -> a
V.head Vector G1
gs

            p1 :: BLS12_381_GT
p1 = G1 -> G2 -> BLS12_381_GT
forall {k} {k1} (curve1 :: k) (curve2 :: k1) t.
Pairing curve1 curve2 t =>
Point curve1 -> Point curve2 -> t
pairing (F
F
xi F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
proof1 G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ (F
u F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
xi F -> F -> F
forall a. MultiplicativeSemigroup a => a -> a -> a
* F
omega) F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
proof2 G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ G1
f G1 -> G1 -> G1
forall a. AdditiveGroup a => a -> a -> a
- G1
e) G2
h0
            p2 :: BLS12_381_GT
p2 = G1 -> G2 -> BLS12_381_GT
forall {k} {k1} (curve1 :: k) (curve2 :: k1) t.
Pairing curve1 curve2 t =>
Point curve1 -> Point curve2 -> t
pairing (G1
proof1 G1 -> G1 -> G1
forall a. AdditiveSemigroup a => a -> a -> a
+ F
F
u F -> G1 -> G1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` G1
proof2) G2
h1