{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Protostar.Commit (Commit (..), HomomorphicCommit (..), PedersonSetup (..)) where

import           Control.DeepSeq                             (NFData)
import           Data.Void                                   (Void)
import           Data.Zip                                    (zipWith)
import           GHC.IsList                                  (IsList (..))
import           Prelude                                     hiding (Num (..), sum, take, zipWith)
import           System.Random                               (Random (..), mkStdGen)

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Field             (Zp)
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
import           ZkFold.Base.Algebra.EllipticCurve.Class
import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
import           ZkFold.Base.Data.Vector                     (Vector)
import           ZkFold.Base.Protocol.Protostar.Oracle
import           ZkFold.Prelude                              (take)
import           ZkFold.Symbolic.Class                       (Symbolic)
import           ZkFold.Symbolic.Data.Ed25519                ()
import           ZkFold.Symbolic.Data.FFA                    (Size)

-- | Commit to the object @a@ with commitment key @ck@ and results of type @f@
--
class Commit a f where
    commit :: a -> f

instance RandomOracle a x => Commit a x where
    commit :: a -> x
commit = a -> x
forall a x. RandomOracle a x => a -> x
oracle

-- | Homomorphic commitment scheme, i.e. (hcommit x) * (hcommit y) == hcommit (x + y)
--
class AdditiveGroup c => HomomorphicCommit a c where
    hcommit :: a -> c

class PedersonSetup n c where
    groupElements :: Vector n c

instance KnownNat n => PedersonSetup n (Point BLS12_381_G1) where
    groupElements :: Vector n (Point BLS12_381_G1)
groupElements =
        -- TODO: This is just for testing purposes! Not to be used in production
        let x :: Zp BLS12_381_Scalar
x = (Zp BLS12_381_Scalar, StdGen) -> Zp BLS12_381_Scalar
forall a b. (a, b) -> a
fst ((Zp BLS12_381_Scalar, StdGen) -> Zp BLS12_381_Scalar)
-> (Zp BLS12_381_Scalar, StdGen) -> Zp BLS12_381_Scalar
forall a b. (a -> b) -> a -> b
$ StdGen -> (Zp BLS12_381_Scalar, StdGen)
forall g. RandomGen g => g -> (Zp BLS12_381_Scalar, g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random (StdGen -> (Zp BLS12_381_Scalar, StdGen))
-> StdGen -> (Zp BLS12_381_Scalar, StdGen)
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
0 :: Zp BLS12_381_Scalar
        in [Item (Vector n (Point BLS12_381_G1))]
-> Vector n (Point BLS12_381_G1)
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector n (Point BLS12_381_G1))]
 -> Vector n (Point BLS12_381_G1))
-> [Item (Vector n (Point BLS12_381_G1))]
-> Vector n (Point BLS12_381_G1)
forall a b. (a -> b) -> a -> b
$ Nat
-> [Item (Vector n (Point BLS12_381_G1))]
-> [Item (Vector n (Point BLS12_381_G1))]
forall a. HasCallStack => Nat -> [a] -> [a]
take (forall (n :: Nat). KnownNat n => Nat
value @n) ([Item (Vector n (Point BLS12_381_G1))]
 -> [Item (Vector n (Point BLS12_381_G1))])
-> [Item (Vector n (Point BLS12_381_G1))]
-> [Item (Vector n (Point BLS12_381_G1))]
forall a b. (a -> b) -> a -> b
$ (Point BLS12_381_G1 -> Point BLS12_381_G1)
-> Point BLS12_381_G1 -> [Point BLS12_381_G1]
forall a. (a -> a) -> a -> [a]
iterate (Zp BLS12_381_Scalar -> Point BLS12_381_G1 -> Point BLS12_381_G1
forall b a. Scale b a => b -> a -> a
scale Zp BLS12_381_Scalar
x) Point BLS12_381_G1
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen

instance (KnownNat n, Symbolic c, NFData (c (Vector Size)))
        => PedersonSetup n (Point (Ed25519 c)) where
    groupElements :: Vector n (Point (Ed25519 c))
groupElements =
        -- TODO: This is just for testing purposes! Not to be used in production
        let x :: ScalarField (Ed25519 Void)
x = (ScalarField (Ed25519 Void), StdGen) -> ScalarField (Ed25519 Void)
forall a b. (a, b) -> a
fst ((ScalarField (Ed25519 Void), StdGen)
 -> ScalarField (Ed25519 Void))
-> (ScalarField (Ed25519 Void), StdGen)
-> ScalarField (Ed25519 Void)
forall a b. (a -> b) -> a -> b
$ StdGen -> (ScalarField (Ed25519 Void), StdGen)
forall g. RandomGen g => g -> (ScalarField (Ed25519 Void), g)
forall a g. (Random a, RandomGen g) => g -> (a, g)
random (StdGen -> (ScalarField (Ed25519 Void), StdGen))
-> StdGen -> (ScalarField (Ed25519 Void), StdGen)
forall a b. (a -> b) -> a -> b
$ Int -> StdGen
mkStdGen Int
0 :: ScalarField (Ed25519 Void)
        in [Item (Vector n (Point (Ed25519 c)))]
-> Vector n (Point (Ed25519 c))
forall l. IsList l => [Item l] -> l
fromList ([Item (Vector n (Point (Ed25519 c)))]
 -> Vector n (Point (Ed25519 c)))
-> [Item (Vector n (Point (Ed25519 c)))]
-> Vector n (Point (Ed25519 c))
forall a b. (a -> b) -> a -> b
$ Nat
-> [Item (Vector n (Point (Ed25519 c)))]
-> [Item (Vector n (Point (Ed25519 c)))]
forall a. HasCallStack => Nat -> [a] -> [a]
take (forall (n :: Nat). KnownNat n => Nat
value @n) ([Item (Vector n (Point (Ed25519 c)))]
 -> [Item (Vector n (Point (Ed25519 c)))])
-> [Item (Vector n (Point (Ed25519 c)))]
-> [Item (Vector n (Point (Ed25519 c)))]
forall a b. (a -> b) -> a -> b
$ (Point (Ed25519 c) -> Point (Ed25519 c))
-> Point (Ed25519 c) -> [Point (Ed25519 c)]
forall a. (a -> a) -> a -> [a]
iterate (Zp Ed25519_Scalar -> Point (Ed25519 c) -> Point (Ed25519 c)
forall b a. Scale b a => b -> a -> a
scale Zp Ed25519_Scalar
x) Point (Ed25519 c)
forall {k} (curve :: k). EllipticCurve curve => Point curve
gen

instance (PedersonSetup n c, Scale f c, AdditiveGroup c) => HomomorphicCommit (Vector n f) c where
    hcommit :: Vector n f -> c
hcommit Vector n f
v = Vector n c -> c
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum (Vector n c -> c) -> Vector n c -> c
forall a b. (a -> b) -> a -> b
$ (f -> c -> c) -> Vector n f -> Vector n c -> Vector n c
forall a b c.
(a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith f -> c -> c
forall b a. Scale b a => b -> a -> a
scale Vector n f
v Vector n c
forall (n :: Nat) c. PedersonSetup n c => Vector n c
groupElements

instance (PedersonSetup 100 c, Scale f c, AdditiveGroup c) => HomomorphicCommit [f] c where
    hcommit :: [f] -> c
hcommit [f]
v = [c] -> c
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([c] -> c) -> [c] -> c
forall a b. (a -> b) -> a -> b
$ (f -> c -> c) -> [f] -> [c] -> [c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith f -> c -> c
forall b a. Scale b a => b -> a -> a
scale [f]
v (Vector 100 c -> [Item (Vector 100 c)]
forall l. IsList l => l -> [Item l]
toList (Vector 100 c -> [Item (Vector 100 c)])
-> Vector 100 c -> [Item (Vector 100 c)]
forall a b. (a -> b) -> a -> b
$ forall (n :: Nat) c. PedersonSetup n c => Vector n c
groupElements @100)