{-# 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
type F = Zp BLS12_381_Scalar
type G1 = Point BLS12_381_G1
type G2 = Point BLS12_381_G2
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)
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
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))
instance Show (PlonkWitnessMap d) where
show :: PlonkWitnessMap d -> String
show PlonkWitnessMap d
_ = String
"PlonkWitnessMap"
newtype PlonkWitnessInput = PlonkWitnessInput (Map.Map Natural F)
instance Show PlonkWitnessInput where
show :: PlonkWitnessInput -> String
show PlonkWitnessInput
_ = String
"PlonkWitnessInput"
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)
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