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

module ZkFold.Base.Protocol.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           Data.Word                                  (Word8)
import           Prelude                                    hiding (Num (..), length, sum, (/), (^))
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 (d :: Natural) = KZG (ScalarField c1)
instance Show (ScalarField c1) => Show (KZG c1 c2 d) where
    show :: KZG c1 c2 d -> String
show (KZG ScalarField c1
x) = String
"KZG " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ScalarField c1 -> String
forall a. Show a => a -> String
show ScalarField c1
x
instance Eq (ScalarField c1) => Eq (KZG c1 c2 d) where
    KZG ScalarField c1
x == :: KZG c1 c2 d -> KZG c1 c2 d -> Bool
== KZG ScalarField c1
y = ScalarField c1
x ScalarField c1 -> ScalarField c1 -> Bool
forall a. Eq a => a -> a -> Bool
== ScalarField c1
y
instance Arbitrary (ScalarField c1) => Arbitrary (KZG c1 c2 d) where
    arbitrary :: Gen (KZG c1 c2 d)
arbitrary = ScalarField c1 -> KZG c1 c2 d
forall {k} {k} (c1 :: k) (c2 :: k) (d :: Natural).
ScalarField c1 -> KZG c1 c2 d
KZG (ScalarField c1 -> KZG c1 c2 d)
-> Gen (ScalarField c1) -> Gen (KZG c1 c2 d)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ScalarField c1)
forall a. Arbitrary a => Gen a
arbitrary

newtype WitnessKZG c1 c2 d = WitnessKZG { forall {k} {k} (c1 :: k) (c2 :: k) (d :: Natural).
WitnessKZG c1 c2 d
-> Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
runWitness :: Map (ScalarField c1) (V.Vector (PolyVec (ScalarField c1) d)) }
instance (Show (ScalarField c1)) => Show (WitnessKZG c1 c2 d) where
    show :: WitnessKZG c1 c2 d -> String
show (WitnessKZG Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
w) = String
"WitnessKZG " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
-> String
forall a. Show a => a -> String
show Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
w
instance (EllipticCurve c1, f ~ ScalarField c1, KnownNat d, Ring f, Arbitrary f, Ord f) => Arbitrary (WitnessKZG c1 c2 d) where
    arbitrary :: Gen (WitnessKZG c1 c2 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 d
Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
-> WitnessKZG c1 c2 d
forall {k} {k} (c1 :: k) (c2 :: k) (d :: Natural).
Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) d))
-> WitnessKZG c1 c2 d
WitnessKZG (Map f (Vector (PolyVec f d)) -> WitnessKZG c1 c2 d)
-> ([(f, Vector (PolyVec f d))] -> Map f (Vector (PolyVec f d)))
-> [(f, Vector (PolyVec f d))]
-> WitnessKZG c1 c2 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 d)
-> Gen [(f, Vector (PolyVec f d))] -> Gen (WitnessKZG c1 c2 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) d kzg f g1 core.
    ( KZG c1 c2 d ~ kzg
    , ScalarField c1 ~ f
    , Point c1 ~ g1
    , KnownNat d
    , Ord (ScalarField c1)
    , Binary (ScalarField c1)
    , FiniteField (ScalarField c1)
    , AdditiveGroup (BaseField c1)
    , Binary (Point c1)
    , Pairing c1 c2
    , CoreFunction c1 core
    ) => NonInteractiveProof (KZG c1 c2 d) core where
    type Transcript (KZG c1 c2 d)  = ByteString
    type SetupProve (KZG c1 c2 d)  = V.Vector (Point c1)
    type SetupVerify (KZG c1 c2 d) = (V.Vector (Point c1), Point c2, Point c2)
    type Witness (KZG c1 c2 d)     = WitnessKZG c1 c2 d
    type Input (KZG c1 c2 d)       = Map (ScalarField c1) (V.Vector (Point c1), V.Vector (ScalarField c1))
    type Proof (KZG c1 c2 d)       = Map (ScalarField c1) (Point c1)

    setupProve :: kzg -> SetupProve kzg
    setupProve :: kzg -> SetupProve kzg
setupProve (KZG ScalarField c1
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
ScalarField c1
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 ScalarField c1
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
ScalarField c1
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, ScalarField c1
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 (ScalarField c1) (Vector (PolyVec (ScalarField c1) 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))
Map (ScalarField c1) (Vector (PolyVec (ScalarField c1) 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
ts0, (Input kzg
iMap, Proof kzg
pMap)) (f
z, Vector (PolyVec f d)
fs) = (ByteString
Transcript kzg
ts3, (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
`com` PolyVec f d
h) Map f (Point c1)
Proof kzg
pMap))
                where
                    com :: Vector (Point c1) -> PolyVec f d -> Point c1
com = forall curve (core :: k) f (size :: Natural).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
forall {k} {k1} (curve :: k) (core :: k1) f (size :: Natural).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
msm @c1 @core
                    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
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

                    ts1 :: ByteString
ts1 = ByteString
Transcript kzg
ts0 ByteString -> f -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` f
z ByteString -> Vector f -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Vector f
fzs ByteString -> Vector (Point c1) -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Vector (Point c1)
cms
                    ([f]
gamma, ByteString
ts2) = ByteString -> Natural -> ([f], ByteString)
forall ts a.
(ToTranscript ts Word8, FromTranscript ts a) =>
ts -> Natural -> ([a], ts)
challenges ByteString
ts1 (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)
                    ts3 :: ByteString
ts3 = ByteString
ts2 ByteString -> Word8 -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
0 :: Word8)

                    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

    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 (g1
e0, g1
e1) = (ByteString, (g1, g1)) -> (g1, g1)
forall a b. (a, b) -> b
snd ((ByteString, (g1, g1)) -> (g1, g1))
-> (ByteString, (g1, g1)) -> (g1, g1)
forall a b. (a -> b) -> a -> b
$ ((ByteString, (g1, g1)) -> f -> (ByteString, (g1, g1)))
-> (ByteString, (g1, g1)) -> [f] -> (ByteString, (g1, g1))
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 g1, Vector f), Map f g1)
-> (Transcript kzg, (g1, g1))
-> ScalarField c1
-> (Transcript kzg, (g1, g1))
prepareVerifyOne (Map f (Vector g1, Vector f)
Input kzg
input, Map f g1
Proof kzg
proof)) (ByteString
empty, (g1
Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
inf, g1
Point c1
forall {k} (curve :: k). EllipticCurve curve => Point curve
inf)) ([f] -> (ByteString, (g1, g1))) -> [f] -> (ByteString, (g1, g1))
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 :: TargetGroup c1 c2
p1 = Point c1 -> Point c2 -> TargetGroup c1 c2
forall {k} {k1} (curve1 :: k) (curve2 :: k1).
Pairing curve1 curve2 =>
Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
pairing g1
Point c1
e0 Point c2
h0
                p2 :: TargetGroup c1 c2
p2 = Point c1 -> Point c2 -> TargetGroup c1 c2
forall {k} {k1} (curve1 :: k) (curve2 :: k1).
Pairing curve1 curve2 =>
Point curve1 -> Point curve2 -> TargetGroup curve1 curve2
pairing g1
Point c1
e1 Point c2
h1
            in TargetGroup c1 c2
p1 TargetGroup c1 c2 -> TargetGroup c1 c2 -> Bool
forall a. Eq a => a -> a -> Bool
== TargetGroup c1 c2
p2
        where
            prepareVerifyOne
                :: (Map f (V.Vector g1, V.Vector f), Map f g1)
                -> (Transcript kzg, (g1, g1))
                -> ScalarField c1
                -> (Transcript kzg, (g1, g1))
            prepareVerifyOne :: (Map f (Vector g1, Vector f), Map f g1)
-> (Transcript kzg, (g1, g1))
-> ScalarField c1
-> (Transcript kzg, (g1, g1))
prepareVerifyOne (Map f (Vector g1, Vector f)
iMap, Map f g1
pMap) (Transcript kzg
ts0, (g1
v0, g1
v1)) ScalarField c1
z = (ByteString
Transcript kzg
ts3, (g1
v0 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
Point c1
v0', g1
v1 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
Point c1
v1'))
                where
                    (Vector g1
cms, Vector f
fzs) = Map f (Vector g1, Vector f)
iMap Map f (Vector g1, Vector f) -> f -> (Vector g1, Vector f)
forall k a. Ord k => Map k a -> k -> a
! f
ScalarField c1
z
                    w :: g1
w          = Map f g1
pMap Map f g1 -> f -> g1
forall k a. Ord k => Map k a -> k -> a
! f
ScalarField c1
z

                    ts1 :: ByteString
ts1 = ByteString
Transcript kzg
ts0 ByteString -> f -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` f
ScalarField c1
z ByteString -> Vector f -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Vector f
fzs ByteString -> Vector g1 -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` Vector g1
cms
                    ([f]
gamma', ByteString
ts2) = ByteString -> Natural -> ([f], ByteString)
forall ts a.
(ToTranscript ts Word8, FromTranscript ts a) =>
ts -> Natural -> ([a], ts)
challenges ByteString
ts1 (Int -> Natural
forall a b. (Integral a, Num b) => a -> b
fromIntegral (Int -> Natural) -> Int -> Natural
forall a b. (a -> b) -> a -> b
$ Vector g1 -> Int
forall a. Vector a -> Int
V.length Vector g1
cms)

                    ts3 :: ByteString
ts3 = ByteString
ts2 ByteString -> Word8 -> ByteString
forall ts a. ToTranscript ts a => ts -> a -> ts
`transcript` (Word8
0 :: Word8)
                    r :: ScalarField c1
r   = ByteString -> ScalarField c1
forall ts a. FromTranscript ts a => ts -> a
challenge ByteString
ts3

                    gamma :: Vector f
gamma = [f] -> Vector f
forall a. [a] -> Vector a
V.fromList [f]
gamma'

                    com :: Vector (Point c1) -> PolyVec f d -> Point c1
com = forall curve (core :: k) f (size :: Natural).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
forall {k} {k1} (curve :: k) (core :: k1) f (size :: Natural).
(CoreFunction curve core, f ~ ScalarField curve) =>
Vector (Point curve) -> PolyVec f size -> Point curve
msm @c1 @core

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