{-# 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.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 g1 g2 (d :: Natural) = KZG (ScalarFieldOf g1)
instance Show (ScalarFieldOf g1) => Show (KZG g1 g2 d) where
    show :: KZG g1 g2 d -> String
show (KZG ScalarFieldOf g1
x) = String
"KZG " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> ScalarFieldOf g1 -> String
forall a. Show a => a -> String
show ScalarFieldOf g1
x
instance Eq (ScalarFieldOf g1) => Eq (KZG g1 g2 d) where
    KZG ScalarFieldOf g1
x == :: KZG g1 g2 d -> KZG g1 g2 d -> Bool
== KZG ScalarFieldOf g1
y = ScalarFieldOf g1
x ScalarFieldOf g1 -> ScalarFieldOf g1 -> Bool
forall a. Eq a => a -> a -> Bool
== ScalarFieldOf g1
y
instance Arbitrary (ScalarFieldOf g1) => Arbitrary (KZG g1 g2 d) where
    arbitrary :: Gen (KZG g1 g2 d)
arbitrary = ScalarFieldOf g1 -> KZG g1 g2 d
forall {k} g1 (g2 :: k) (d :: Natural).
ScalarFieldOf g1 -> KZG g1 g2 d
KZG (ScalarFieldOf g1 -> KZG g1 g2 d)
-> Gen (ScalarFieldOf g1) -> Gen (KZG g1 g2 d)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ScalarFieldOf g1)
forall a. Arbitrary a => Gen a
arbitrary

newtype WitnessKZG g1 g2 d = WitnessKZG
  { forall {k} g1 (g2 :: k) (d :: Natural).
WitnessKZG g1 g2 d
-> Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
runWitness :: Map (ScalarFieldOf g1) (V.Vector (PolyVec (ScalarFieldOf g1) d)) }
instance (Show (ScalarFieldOf g1)) => Show (WitnessKZG g1 g2 d) where
    show :: WitnessKZG g1 g2 d -> String
show (WitnessKZG Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
w) = String
"WitnessKZG " String -> ShowS
forall a. Semigroup a => a -> a -> a
<> Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
-> String
forall a. Show a => a -> String
show Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
w
instance
  ( KnownNat d
  , Arbitrary (ScalarFieldOf g1)
  , Ord (ScalarFieldOf g1)
  , Ring (ScalarFieldOf g1)
  ) => Arbitrary (WitnessKZG g1 g2 d) where
    arbitrary :: Gen (WitnessKZG g1 g2 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 (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
-> WitnessKZG g1 g2 d
forall {k} g1 (g2 :: k) (d :: Natural).
Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
-> WitnessKZG g1 g2 d
WitnessKZG (Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
 -> WitnessKZG g1 g2 d)
-> ([(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
    -> Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d)))
-> [(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
-> WitnessKZG g1 g2 d
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
-> Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) d))
forall k a. Ord k => [(k, a)] -> Map k a
fromList ([(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
 -> WitnessKZG g1 g2 d)
-> Gen [(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
-> Gen (WitnessKZG g1 g2 d)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Gen (ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))
-> Gen [(ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d))]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
n ((,) (ScalarFieldOf g1
 -> Vector (PolyVec (ScalarFieldOf g1) d)
 -> (ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d)))
-> Gen (ScalarFieldOf g1)
-> Gen
     (Vector (PolyVec (ScalarFieldOf g1) d)
      -> (ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d)))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Gen (ScalarFieldOf g1)
forall a. Arbitrary a => Gen a
arbitrary Gen
  (Vector (PolyVec (ScalarFieldOf g1) d)
   -> (ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) d)))
-> Gen (Vector (PolyVec (ScalarFieldOf g1) d))
-> Gen (ScalarFieldOf g1, Vector (PolyVec (ScalarFieldOf g1) 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 (ScalarFieldOf g1) d]
-> Vector (PolyVec (ScalarFieldOf g1) d)
forall a. [a] -> Vector a
V.fromList ([PolyVec (ScalarFieldOf g1) d]
 -> Vector (PolyVec (ScalarFieldOf g1) d))
-> Gen [PolyVec (ScalarFieldOf g1) d]
-> Gen (Vector (PolyVec (ScalarFieldOf g1) d))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Int
-> Gen (PolyVec (ScalarFieldOf g1) d)
-> Gen [PolyVec (ScalarFieldOf g1) d]
forall (m :: Type -> Type) a. Applicative m => Int -> m a -> m [a]
replicateM Int
m Gen (PolyVec (ScalarFieldOf g1) d)
forall a. Arbitrary a => Gen a
arbitrary))

-- TODO (Issue #18): check list lengths
instance forall f g1 g2 gt d kzg core.
    ( KZG g1 g2 d ~ kzg
    , KnownNat d
    , Ord f
    , Binary f
    , FiniteField f
    , AdditiveGroup f
    , f ~ ScalarFieldOf g1
    , Binary g1
    , Pairing g1 g2 gt
    , Eq gt
    , CoreFunction g1 core
    ) => NonInteractiveProof (KZG g1 g2 d) core where
    type Transcript (KZG g1 g2 d)  = ByteString
    type SetupProve (KZG g1 g2 d)  = V.Vector g1
    type SetupVerify (KZG g1 g2 d) = (V.Vector g1, g2, g2)
    type Witness (KZG g1 g2 d)     = WitnessKZG g1 g2 d
    type Input (KZG g1 g2 d)       = Map (ScalarFieldOf g1) (V.Vector g1, V.Vector (ScalarFieldOf g1))
    type Proof (KZG g1 g2 d)       = Map (ScalarFieldOf g1) g1

    setupProve :: kzg -> SetupProve kzg
    setupProve :: kzg -> SetupProve kzg
setupProve (KZG ScalarFieldOf g1
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
ScalarFieldOf g1
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 b a. Scale b a => b -> a -> a
`scale` forall g. CyclicGroup g => g
pointGen @g1) Vector f
xs
        in Vector g1
SetupProve kzg
gs

    setupVerify :: kzg -> SetupVerify kzg
    setupVerify :: kzg -> SetupVerify kzg
setupVerify (KZG ScalarFieldOf g1
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
ScalarFieldOf g1
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 b a. Scale b a => b -> a -> a
`scale` forall g. CyclicGroup g => g
pointGen @g1) Vector f
xs
        in (Vector g1
gs, forall g. CyclicGroup g => g
pointGen @g2, f
ScalarFieldOf g1
x f -> g2 -> g2
forall b a. Scale b a => b -> a -> a
`scale` forall g. CyclicGroup g => g
pointGen @g2)

    prove :: SetupProve kzg
          -> Witness kzg
          -> (Input kzg, Proof kzg)
    prove :: SetupProve kzg -> Witness kzg -> (Input kzg, Proof kzg)
prove SetupProve kzg
gs (WitnessKZG Map (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) 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 g1, Vector f), Map f g1))
 -> (f, Vector (PolyVec f d))
 -> (ByteString, (Map f (Vector g1, Vector f), Map f g1)))
-> (ByteString, (Map f (Vector g1, Vector f), Map f g1))
-> [(f, Vector (PolyVec f d))]
-> (ByteString, (Map f (Vector g1, Vector f), Map f 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 (ByteString, (Map f (Vector g1, Vector f), Map f g1))
-> (f, Vector (PolyVec f d))
-> (ByteString, (Map f (Vector g1, Vector f), Map f g1))
(Transcript kzg, (Input kzg, Proof kzg))
-> (f, Vector (PolyVec f d))
-> (Transcript kzg, (Input kzg, Proof kzg))
proveOne (ByteString
empty, (Map f (Vector g1, Vector f)
forall a. Monoid a => a
mempty, Map f g1
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 (ScalarFieldOf g1) (Vector (PolyVec (ScalarFieldOf g1) 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 g1, Vector f)
-> Map f (Vector g1, Vector f)
-> Map f (Vector g1, Vector f)
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert f
z (Vector g1
cms, Vector f
fzs) Map f (Vector g1, Vector f)
Input kzg
iMap, f -> g1 -> Map f g1 -> Map f g1
forall k a. Ord k => k -> a -> Map k a -> Map k a
insert f
z (Vector g1
SetupProve kzg
gs Vector g1 -> PolyVec f d -> g1
`com` PolyVec f d
h) Map f g1
Proof kzg
pMap))
                where
                    com :: Vector g1 -> PolyVec f d -> g1
com = forall g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
forall {k} g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
msm @g1 @core
                    cms :: Vector g1
cms  = (PolyVec f d -> g1) -> Vector (PolyVec f d) -> 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 (Vector g1 -> PolyVec f d -> g1
com Vector g1
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 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)

                    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 g1
gs, g2
h0, g2
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)) -> f -> (Transcript kzg, (g1, g1))
prepareVerifyOne (Map f (Vector g1, Vector f)
Input kzg
input, Map f g1
Proof kzg
proof)) (ByteString
empty, (g1
forall a. AdditiveMonoid a => a
zero, g1
forall a. AdditiveMonoid a => a
zero)) ([f] -> (ByteString, (g1, g1))) -> [f] -> (ByteString, (g1, g1))
forall a b. (a -> b) -> a -> b
$ Map f (Vector g1, Vector f) -> [f]
forall k a. Map k a -> [k]
keys Map f (Vector g1, Vector f)
Input kzg
input
                p1 :: gt
p1 = g1 -> g2 -> gt
forall g1 g2 gt. Pairing g1 g2 gt => g1 -> g2 -> gt
pairing g1
e0 g2
h0
                p2 :: gt
p2 = g1 -> g2 -> gt
forall g1 g2 gt. Pairing g1 g2 gt => g1 -> g2 -> gt
pairing g1
e1 g2
h1
            in gt
p1 gt -> gt -> Bool
forall a. Eq a => a -> a -> Bool
== gt
p2
        where
            prepareVerifyOne
                :: (Map f (V.Vector g1, V.Vector f), Map f g1)
                -> (Transcript kzg, (g1, g1))
                -> f
                -> (Transcript kzg, (g1, g1))
            prepareVerifyOne :: (Map f (Vector g1, Vector f), Map f g1)
-> (Transcript kzg, (g1, g1)) -> f -> (Transcript kzg, (g1, g1))
prepareVerifyOne (Map f (Vector g1, Vector f)
iMap, Map f g1
pMap) (Transcript kzg
ts0, (g1
v0, g1
v1)) f
z = (ByteString
Transcript kzg
ts3, (g1
v0 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
v0', g1
v1 g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ g1
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
z
                    w :: g1
w          = Map f g1
pMap Map f g1 -> f -> g1
forall k a. Ord k => Map k a -> k -> a
! f
z

                    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 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 :: f
r   = ByteString -> f
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 g1 -> PolyVec f d -> g1
com = forall g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
forall {k} g (core :: k) f (size :: Natural).
(CoreFunction g core, f ~ ScalarFieldOf g) =>
Vector g -> PolyVec f size -> g
msm @g1 @core

                    v0' :: g1
v0' = f
r f -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` Vector g1 -> g1
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((f -> g1 -> g1) -> Vector f -> Vector g1 -> Vector g1
forall a b c. (a -> b -> c) -> Vector a -> Vector b -> Vector c
V.zipWith f -> g1 -> g1
forall b a. Scale b a => b -> a -> a
scale Vector f
gamma Vector g1
cms)
                        g1 -> g1 -> g1
forall a. AdditiveGroup a => a -> a -> a
- f
r f -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` (Vector g1
gs Vector g1 -> PolyVec f d -> g1
`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 (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])
                        g1 -> g1 -> g1
forall a. AdditiveSemigroup a => a -> a -> a
+ (f
r f -> f -> f
forall a. MultiplicativeSemigroup a => a -> a -> a
* f
z) f -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
w
                    v1' :: g1
v1' = f
r f -> g1 -> g1
forall b a. Scale b a => b -> a -> a
`scale` g1
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]