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

module ZkFold.Base.Protocol.Commitment.KZG where

import           Control.Monad                              (replicateM)
import           Data.ByteString                            (ByteString, empty)
import           Data.Kind                                  (Type)
import           Data.Map.Strict                            (Map, fromList, insert, keys, toList, (!))
import qualified Data.Vector                                as V
import           Data.Vector.Binary                         ()
import           Numeric.Natural                            (Natural)
import           Prelude                                    hiding (Num (..), length, sum, (/), (^))
import qualified Prelude                                    as P
import           Test.QuickCheck                            (Arbitrary (..), chooseInt)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.Polynomials.Univariate
import           ZkFold.Base.Data.ByteString                (Binary)
import           ZkFold.Base.Protocol.NonInteractiveProof

-- | `d` is the degree of polynomials in the protocol
newtype KZG c1 c2 t f (d :: Natural) = KZG f
    deriving (Int -> KZG c1 c2 t f d -> ShowS
[KZG c1 c2 t f d] -> ShowS
KZG c1 c2 t f d -> String
(Int -> KZG c1 c2 t f d -> ShowS)
-> (KZG c1 c2 t f d -> String)
-> ([KZG c1 c2 t f d] -> ShowS)
-> Show (KZG c1 c2 t f d)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
Int -> KZG c1 c2 t f d -> ShowS
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
[KZG c1 c2 t f d] -> ShowS
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
KZG c1 c2 t f d -> String
$cshowsPrec :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
Int -> KZG c1 c2 t f d -> ShowS
showsPrec :: Int -> KZG c1 c2 t f d -> ShowS
$cshow :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
KZG c1 c2 t f d -> String
show :: KZG c1 c2 t f d -> String
$cshowList :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Show f =>
[KZG c1 c2 t f d] -> ShowS
showList :: [KZG c1 c2 t f d] -> ShowS
Show, KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
(KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool)
-> (KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool)
-> Eq (KZG c1 c2 t f d)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Eq f =>
KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
$c== :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Eq f =>
KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
== :: KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
$c/= :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Eq f =>
KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
/= :: KZG c1 c2 t f d -> KZG c1 c2 t f d -> Bool
Eq, Gen (KZG c1 c2 t f d)
Gen (KZG c1 c2 t f d)
-> (KZG c1 c2 t f d -> [KZG c1 c2 t f d])
-> Arbitrary (KZG c1 c2 t f d)
KZG c1 c2 t f d -> [KZG c1 c2 t f d]
forall a. Gen a -> (a -> [a]) -> Arbitrary a
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Arbitrary f =>
Gen (KZG c1 c2 t f d)
forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Arbitrary f =>
KZG c1 c2 t f d -> [KZG c1 c2 t f d]
$carbitrary :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Arbitrary f =>
Gen (KZG c1 c2 t f d)
arbitrary :: Gen (KZG c1 c2 t f d)
$cshrink :: forall k (c1 :: k) k (c2 :: k) k (t :: k) f (d :: Natural).
Arbitrary f =>
KZG c1 c2 t f d -> [KZG c1 c2 t f d]
shrink :: KZG c1 c2 t f d -> [KZG c1 c2 t f d]
Arbitrary)

newtype WitnessKZG c1 c2 t f d = WitnessKZG { forall {k} {k} {k} (c1 :: k) (c2 :: k) (t :: k) f (d :: Natural).
WitnessKZG c1 c2 t f d -> Map f (Vector (PolyVec f d))
runWitness :: Map f (V.Vector (PolyVec f d)) }
instance (EllipticCurve c1, f ~ ScalarField c1, Show f) => Show (WitnessKZG c1 c2 t f d) where
    show :: WitnessKZG c1 c2 t f d -> String
show (WitnessKZG Map f (Vector (PolyVec f d))
w) = String
"WitnessKZG " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map f (Vector (PolyVec f d)) -> String
forall a. Show a => a -> String
show Map f (Vector (PolyVec f d))
w
instance (EllipticCurve c1, f ~ ScalarField c1, KnownNat d, Ring f, Arbitrary f, Ord f) => Arbitrary (WitnessKZG c1 c2 t f d) where
    arbitrary :: Gen (WitnessKZG c1 c2 t f d)
arbitrary = do
        Int
n <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
3)
        Int
m <- (Int, Int) -> Gen Int
chooseInt (Int
1, Int
5)
        Map f (Vector (PolyVec f d)) -> WitnessKZG c1 c2 t f d
forall {k} {k} {k} (c1 :: k) (c2 :: k) (t :: k) f (d :: Natural).
Map f (Vector (PolyVec f d)) -> WitnessKZG c1 c2 t f d
WitnessKZG (Map f (Vector (PolyVec f d)) -> WitnessKZG c1 c2 t f d)
-> ([(f, Vector (PolyVec f d))] -> Map f (Vector (PolyVec f d)))
-> [(f, Vector (PolyVec f d))]
-> WitnessKZG c1 c2 t f d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(f, Vector (PolyVec f d))] -> Map f (Vector (PolyVec f d))
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(f, Vector (PolyVec f d))] -> WitnessKZG c1 c2 t f d)
-> Gen [(f, Vector (PolyVec f d))] -> Gen (WitnessKZG c1 c2 t f d)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Gen (f, Vector (PolyVec f d)) -> Gen [(f, Vector (PolyVec f d))]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n ((,) (f -> Vector (PolyVec f d) -> (f, Vector (PolyVec f d)))
-> Gen f -> Gen (Vector (PolyVec f d) -> (f, Vector (PolyVec f d)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen f
forall a. Arbitrary a => Gen a
arbitrary Gen (Vector (PolyVec f d) -> (f, Vector (PolyVec f d)))
-> Gen (Vector (PolyVec f d)) -> Gen (f, Vector (PolyVec f d))
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
<*> ([PolyVec f d] -> Vector (PolyVec f d)
forall a. [a] -> Vector a
V.fromList ([PolyVec f d] -> Vector (PolyVec f d))
-> Gen [PolyVec f d] -> Gen (Vector (PolyVec f d))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int -> Gen (PolyVec f d) -> Gen [PolyVec f d]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
m Gen (PolyVec f d)
forall a. Arbitrary a => Gen a
arbitrary))

-- TODO (Issue #18): check list lengths
instance forall (c1 :: Type) (c2 :: Type) t f d kzg .
    ( f ~ ScalarField c1
    , f ~ ScalarField c2
    , Pairing c1 c2 t
    , Binary f
    , KnownNat d
    , KZG c1 c2 t f d ~ kzg
    , P.Num f
    , Ord f
    , Ring f
    , Finite f
    , Field f
    , AdditiveGroup (BaseField c1)
    , Binary (BaseField c1)
    ) => NonInteractiveProof (KZG c1 c2 t f d) where
    type Transcript (KZG c1 c2 t f d)  = ByteString
    type SetupProve (KZG c1 c2 t f d)  = V.Vector (Point c1)
    type SetupVerify (KZG c1 c2 t f d) = (V.Vector (Point c1), Point c2, Point c2)
    type Witness (KZG c1 c2 t f d)     = WitnessKZG c1 c2 t f d
    type Input (KZG c1 c2 t f d)       = Map f (V.Vector (Point c1), V.Vector f)
    type Proof (KZG c1 c2 t f d)       = Map f (Point c1)

    setupProve :: kzg -> SetupProve kzg
    setupProve :: kzg -> SetupProve kzg
setupProve (KZG f
x) =
        let d :: Natural
d  = forall (n :: Natural). KnownNat n => Natural
value @d
            xs :: Vector f
xs = [f] -> Vector f
forall a. [a] -> Vector a
V.fromList ([f] -> Vector f) -> [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 (Point c1)
gs = (f -> Point c1) -> Vector f -> Vector (Point c1)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen) Vector f
xs
        in Vector (Point c1)
SetupProve kzg
gs

    setupVerify :: kzg -> SetupVerify kzg
    setupVerify :: kzg -> SetupVerify kzg
setupVerify (KZG f
x) =
        let d :: Natural
d  = forall (n :: Natural). KnownNat n => Natural
value @d
            xs :: Vector f
xs = [f] -> Vector f
forall a. [a] -> Vector a
V.fromList ([f] -> Vector f) -> [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 (Point c1)
gs = (f -> Point c1) -> Vector f -> Vector (Point c1)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen) Vector f
xs
        in (Vector (Point c1)
gs, Point c2
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen, f
ScalarField c2
x ScalarField c2 -> Point c2 -> Point c2
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c2
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen)

    prove :: SetupProve kzg
          -> Witness kzg
          -> (Input kzg, Proof kzg)
    prove :: SetupProve kzg -> Witness kzg -> (Input kzg, Proof kzg)
prove SetupProve kzg
gs (WitnessKZG Map f (Vector (PolyVec f d))
w) = (ByteString, (Input kzg, Proof kzg)) -> (Input kzg, Proof kzg)
forall a b. (a, b) -> b
snd ((ByteString, (Input kzg, Proof kzg)) -> (Input kzg, Proof kzg))
-> (ByteString, (Input kzg, Proof kzg)) -> (Input kzg, Proof kzg)
forall a b. (a -> b) -> a -> b
$ ((ByteString,
  (Map f (Vector (Point c1), Vector f), Map f (Point c1)))
 -> (f, Vector (PolyVec f d))
 -> (ByteString,
     (Map f (Vector (Point c1), Vector f), Map f (Point c1))))
-> (ByteString,
    (Map f (Vector (Point c1), Vector f), Map f (Point c1)))
-> [(f, Vector (PolyVec f d))]
-> (ByteString,
    (Map f (Vector (Point c1), Vector f), Map f (Point c1)))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (ByteString,
 (Map f (Vector (Point c1), Vector f), Map f (Point c1)))
-> (f, Vector (PolyVec f d))
-> (ByteString,
    (Map f (Vector (Point c1), Vector f), Map f (Point c1)))
(Transcript kzg, (Input kzg, Proof kzg))
-> (f, Vector (PolyVec f d))
-> (Transcript kzg, (Input kzg, Proof kzg))
proveOne (ByteString
empty, (Map f (Vector (Point c1), Vector f)
forall a. Monoid a => a
mempty, Map f (Point c1)
forall a. Monoid a => a
mempty)) (Map f (Vector (PolyVec f d)) -> [(f, Vector (PolyVec f d))]
forall k a. Map k a -> [(k, a)]
toList Map f (Vector (PolyVec f d))
w)
        where
            proveOne :: (Transcript kzg, (Input kzg, Proof kzg))
                     -> (f, V.Vector (PolyVec f d))
                     -> (Transcript kzg, (Input kzg, Proof kzg))
            proveOne :: (Transcript kzg, (Input kzg, Proof kzg))
-> (f, Vector (PolyVec f d))
-> (Transcript kzg, (Input kzg, Proof kzg))
proveOne (Transcript kzg
ts, (Input kzg
iMap, Proof kzg
pMap)) (f
z, Vector (PolyVec f d)
fs) = (ByteString
Transcript kzg
ts'', (f
-> (Vector (Point c1), Vector f)
-> Map f (Vector (Point c1), Vector f)
-> Map f (Vector (Point c1), Vector f)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert f
z (Vector (Point c1)
cms, Vector f
fzs) Map f (Vector (Point c1), Vector f)
Input kzg
iMap, f -> Point c1 -> Map f (Point c1) -> Map f (Point c1)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert f
z (Vector (Point c1)
SetupProve kzg
gs Vector (Point c1) -> PolyVec f d -> Point c1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` PolyVec f d
h) Map f (Point c1)
Proof kzg
pMap))
                where
                    cms :: Vector (Point c1)
cms  = (PolyVec f d -> Point c1)
-> Vector (PolyVec f d) -> Vector (Point c1)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vector (Point c1) -> PolyVec f d -> Point c1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
com Vector (Point c1)
SetupProve kzg
gs) Vector (PolyVec f d)
fs
                    fzs :: Vector f
fzs  = (PolyVec f d -> f) -> Vector (PolyVec f d) -> 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 (PolyVec f d -> f -> f
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` f
z) Vector (PolyVec f d)
fs

                    ([f]
gamma, ByteString
ts') = (ByteString -> Natural -> ([f], ByteString))
-> Natural -> ByteString -> ([f], ByteString)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ByteString -> Natural -> ([f], ByteString)
forall t a. FromTranscript t a => t -> Natural -> ([a], t)
challenges (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Vector (Point c1) -> Int
forall a. Vector a -> Int
V.length Vector (Point c1)
cms) (ByteString -> ([f], ByteString))
-> ByteString -> ([f], ByteString)
forall a b. (a -> b) -> a -> b
$ ByteString
Transcript kzg
ts
                        ByteString -> f -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` f
z
                        ByteString -> Vector f -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` Vector f
fzs
                        ByteString -> Vector (Point c1) -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` Vector (Point c1)
cms
                    h :: PolyVec f d
h            = Vector (PolyVec f d) -> PolyVec f d
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum (Vector (PolyVec f d) -> PolyVec f d)
-> Vector (PolyVec f d) -> PolyVec f d
forall a b. (a -> b) -> a -> b
$ (f -> PolyVec f d -> PolyVec f d)
-> Vector f -> Vector (PolyVec f d) -> Vector (PolyVec f d)
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith f -> PolyVec f d -> PolyVec f d
forall c (size :: Natural).
Ring c =>
c -> PolyVec c size -> PolyVec c size
scalePV ([f] -> Vector f
forall a. [a] -> Vector a
V.fromList [f]
gamma) (Vector (PolyVec f d) -> Vector (PolyVec f d))
-> Vector (PolyVec f d) -> Vector (PolyVec f d)
forall a b. (a -> b) -> a -> b
$ (PolyVec f d -> PolyVec f d)
-> Vector (PolyVec f d) -> Vector (PolyVec f d)
forall a b. (a -> b) -> Vector a -> Vector b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (PolyVec f d -> f -> PolyVec f d
forall (size :: Natural) f.
(KnownNat size, FiniteField f, Eq f) =>
PolyVec f size -> f -> PolyVec f size
`provePolyVecEval` f
z) Vector (PolyVec f d)
fs
                    ts'' :: ByteString
ts''         = if ByteString
Transcript kzg
ts ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
empty then ByteString
ts' else (f, Transcript kzg) -> Transcript kzg
forall a b. (a, b) -> b
snd ((f, Transcript kzg) -> Transcript kzg)
-> (f, Transcript kzg) -> Transcript kzg
forall a b. (a -> b) -> a -> b
$ forall t a. FromTranscript t a => t -> (a, t)
challenge @(Transcript kzg) @f ByteString
Transcript kzg
ts'

    verify :: SetupVerify kzg -> Input kzg -> Proof kzg -> Bool
    verify :: SetupVerify kzg -> Input kzg -> Proof kzg -> Bool
verify (Vector (Point c1)
gs, Point c2
h0, Point c2
h1) Input kzg
input Proof kzg
proof =
            let (Point c1
e0, Point c1
e1) = (ByteString, (Point c1, Point c1)) -> (Point c1, Point c1)
forall a b. (a, b) -> b
snd ((ByteString, (Point c1, Point c1)) -> (Point c1, Point c1))
-> (ByteString, (Point c1, Point c1)) -> (Point c1, Point c1)
forall a b. (a -> b) -> a -> b
$ ((ByteString, (Point c1, Point c1))
 -> f -> (ByteString, (Point c1, Point c1)))
-> (ByteString, (Point c1, Point c1))
-> [f]
-> (ByteString, (Point c1, Point c1))
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl ((Map f (Vector (Point c1), Vector f), Map f (Point c1))
-> (Transcript kzg, (Point c1, Point c1))
-> f
-> (Transcript kzg, (Point c1, Point c1))
prepareVerifyOne (Map f (Vector (Point c1), Vector f)
Input kzg
input, Map f (Point c1)
Proof kzg
proof)) (ByteString
empty, (Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
inf, Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
inf)) ([f] -> (ByteString, (Point c1, Point c1)))
-> [f] -> (ByteString, (Point c1, Point c1))
forall a b. (a -> b) -> a -> b
$ Map f (Vector (Point c1), Vector f) -> [f]
forall k a. Map k a -> [k]
keys Map f (Vector (Point c1), Vector f)
Input kzg
input
                p1 :: t
p1 = Point c1 -> Point c2 -> t
forall {k} {k1} (curve1 :: k) (curve2 :: k1) t.
Pairing curve1 curve2 t =>
Point curve1 -> Point curve2 -> t
pairing Point c1
e0 Point c2
h0
                p2 :: t
p2 = Point c1 -> Point c2 -> t
forall {k} {k1} (curve1 :: k) (curve2 :: k1) t.
Pairing curve1 curve2 t =>
Point curve1 -> Point curve2 -> t
pairing Point c1
e1 Point c2
h1
            in t
p1 t -> t -> Bool
forall a. Eq a => a -> a -> Bool
== t
p2
        where
            prepareVerifyOne
                :: (Map f (V.Vector (Point c1), V.Vector f), Map f (Point c1))
                -> (Transcript kzg, (Point c1, Point c1))
                -> f
                -> (Transcript kzg, (Point c1, Point c1))
            prepareVerifyOne :: (Map f (Vector (Point c1), Vector f), Map f (Point c1))
-> (Transcript kzg, (Point c1, Point c1))
-> f
-> (Transcript kzg, (Point c1, Point c1))
prepareVerifyOne (Map f (Vector (Point c1), Vector f)
iMap, Map f (Point c1)
pMap) (Transcript kzg
ts, (Point c1
v0, Point c1
v1)) f
z = (ByteString
Transcript kzg
ts'', (Point c1
v0 Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Point c1
v0', Point c1
v1 Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ Point c1
v1'))
                where
                    (Vector (Point c1)
cms, Vector f
fzs) = Map f (Vector (Point c1), Vector f)
iMap Map f (Vector (Point c1), Vector f)
-> f -> (Vector (Point c1), Vector f)
forall k a. Ord k => Map k a -> k -> a
! f
z
                    w :: Point c1
w          = Map f (Point c1)
pMap Map f (Point c1) -> f -> Point c1
forall k a. Ord k => Map k a -> k -> a
! f
z

                    ([f]
gamma', ByteString
ts') = (ByteString -> Natural -> ([f], ByteString))
-> Natural -> ByteString -> ([f], ByteString)
forall a b c. (a -> b -> c) -> b -> a -> c
flip ByteString -> Natural -> ([f], ByteString)
forall t a. FromTranscript t a => t -> Natural -> ([a], t)
challenges (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Vector (Point c1) -> Int
forall a. Vector a -> Int
V.length Vector (Point c1)
cms) (ByteString -> ([f], ByteString))
-> ByteString -> ([f], ByteString)
forall a b. (a -> b) -> a -> b
$ ByteString
Transcript kzg
ts
                        ByteString -> f -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` f
z
                        ByteString -> Vector f -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` Vector f
fzs
                        ByteString -> Vector (Point c1) -> ByteString
forall t a. ToTranscript t a => t -> a -> t
`transcript` Vector (Point c1)
cms
                    gamma :: Vector f
gamma = [f] -> Vector f
forall a. [a] -> Vector a
V.fromList [f]
gamma'
                    (f
r, ByteString
ts'')    = if ByteString
Transcript kzg
ts ByteString -> ByteString -> Bool
forall a. Eq a => a -> a -> Bool
== ByteString
empty then (f
forall a. MultiplicativeMonoid a => a
one, ByteString
ts') else ByteString -> (f, ByteString)
forall t a. FromTranscript t a => t -> (a, t)
challenge ByteString
ts'

                    v0' :: Point c1
v0' = f
ScalarField c1
r ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Vector (Point c1) -> Point c1
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((f -> Point c1 -> Point c1)
-> Vector f -> Vector (Point c1) -> Vector (Point c1)
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith f -> Point c1 -> Point c1
ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul Vector f
gamma Vector (Point c1)
cms)
                        Point c1 -> Point c1 -> Point c1
forall a. AdditiveGroup a => a -> a -> a
- f
ScalarField c1
r ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` (Vector (Point c1)
gs Vector (Point c1) -> PolyVec f d -> Point c1
forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
`com` forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec @f @d [Vector (Item (Vector f)) -> Item (Vector f)
forall a. Num a => Vector a -> a
V.sum (Vector (Item (Vector f)) -> Item (Vector f))
-> Vector (Item (Vector f)) -> Item (Vector f)
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
(*) Vector f
gamma Vector f
fzs])
                        Point c1 -> Point c1 -> Point c1
forall a. AdditiveSemigroup a => a -> a -> a
+ (f
r f -> f -> f
forall a. MultiplicativeSemigroup a => a -> a -> a
* f
z) ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
w
                    v1' :: Point c1
v1' = f
ScalarField c1
r ScalarField c1 -> Point c1 -> Point c1
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
`mul` Point c1
w

------------------------------------ Helper functions ------------------------------------

provePolyVecEval :: forall size f . (KnownNat size, FiniteField f, Eq f) => PolyVec f size -> f -> PolyVec f size
provePolyVecEval :: forall (size :: Natural) f.
(KnownNat size, FiniteField f, Eq f) =>
PolyVec f size -> f -> PolyVec f size
provePolyVecEval PolyVec f size
f f
z = (PolyVec f size
f PolyVec f size -> PolyVec f size -> PolyVec f size
forall a. AdditiveGroup a => a -> a -> a
- Vector f -> PolyVec f size
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec [Item (Vector f) -> Item (Vector f)
forall a. AdditiveGroup a => a -> a
negate (Item (Vector f) -> Item (Vector f))
-> Item (Vector f) -> Item (Vector f)
forall a b. (a -> b) -> a -> b
$ PolyVec f size
f PolyVec f size -> f -> f
forall c (size :: Natural). Ring c => PolyVec c size -> c -> c
`evalPolyVec` f
z]) PolyVec f size -> PolyVec f size -> PolyVec f size
forall c (size :: Natural).
(Field c, KnownNat size, Eq c) =>
PolyVec c size -> PolyVec c size -> PolyVec c size
`polyVecDiv` Vector f -> PolyVec f size
forall c (size :: Natural).
(Ring c, KnownNat size) =>
Vector c -> PolyVec c size
toPolyVec [f -> f
forall a. AdditiveGroup a => a -> a
negate f
z, f
Item (Vector f)
forall a. MultiplicativeMonoid a => a
one]

com :: (EllipticCurve curve, f ~ ScalarField curve) => V.Vector (Point curve) -> PolyVec f size -> Point curve
com :: forall {k} (curve :: k) f (size :: Natural).
(EllipticCurve curve, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
com Vector (Point curve)
gs PolyVec f size
f = Vector (Point curve) -> Point curve
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum (Vector (Point curve) -> Point curve)
-> Vector (Point curve) -> Point curve
forall a b. (a -> b) -> a -> b
$ (f -> Point curve -> Point curve)
-> Vector f -> Vector (Point curve) -> Vector (Point curve)
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith f -> Point curve -> Point curve
ScalarField curve -> Point curve -> Point curve
forall {k} (curve :: k).
EllipticCurve curve =>
ScalarField curve -> Point curve -> Point curve
mul (PolyVec f size -> Vector f
forall c (size :: Natural). PolyVec c size -> Vector c
fromPolyVec PolyVec f size
f) Vector (Point curve)
gs