{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

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

import           Data.Foldable                               (Foldable, toList)
import           Data.Functor.Rep                            (Representable)
import           Prelude                                     (Traversable, type (~), zipWith, ($), (<$>))

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
import           ZkFold.Base.Algebra.EllipticCurve.Class     as EC
import           ZkFold.Base.Algebra.EllipticCurve.Ed25519
import           ZkFold.Base.Protocol.Protostar.Oracle
import           ZkFold.Symbolic.Class
import           ZkFold.Symbolic.Data.Class
import           ZkFold.Symbolic.Data.Ed25519                ()
import           ZkFold.Symbolic.Data.FieldElement

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

instance (RandomOracle ck x, RandomOracle a x, Ring x) => Commit ck a x where
    commit :: ck -> a -> x
commit ck
ck a
a = [x] -> x
forall a b. RandomOracle a b => a -> b
oracle [forall a b. RandomOracle a b => a -> b
oracle @ck @x ck
ck, forall a b. RandomOracle a b => a -> b
oracle @a @x a
a]

-- | Homomorphic commitment scheme, i.e. (hcommit ck1 a1) * (hcommit ck2 a2) == hcommit (ck1 + ck2) (a1 + a2)
--
class HomomorphicCommit ck a c where
    hcommit :: ck -> a -> c

class PedersonSetup a where
    pedersonGH :: (a, a)

instance PedersonSetup (Point BLS12_381_G1) where
    pedersonGH :: (Point BLS12_381_G1, Point BLS12_381_G1)
pedersonGH = (Point BLS12_381_G1
g, Point BLS12_381_G1
h)
        where
            -- Random points on BLS12_381_G1
            -- The only requirement for them is so that nobody knows discrete logarithm of g base h
            -- Keeping these numbers open seems safe as there is no known efficient algorithm to calculate discrete logarithm
            -- TODO: Consider choosing these elements randomly each time instead of hardcoding them
            g :: Point BLS12_381_G1
g = BaseField BLS12_381_G1
-> BaseField BLS12_381_G1 -> Point BLS12_381_G1
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
                  BaseField BLS12_381_G1
374634537115484260972239972618177817162837837681489433937595987156473628121582176081070052390732339994821123215324
                  BaseField BLS12_381_G1
3101937092382348684068486219386062896291823016251987968533318607938307290692317713596471528583601314350111497326114

            h :: Point BLS12_381_G1
h = BaseField BLS12_381_G1
-> BaseField BLS12_381_G1 -> Point BLS12_381_G1
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
                  BaseField BLS12_381_G1
89212312271530513649036778047014309438687633223023480439497929919626414549107721779839342336160039318198182187102
                  BaseField BLS12_381_G1
1428833674135004724206317422667541391548200977592780696082498356495280179807693517101023736214529698214586243870416

instance
  ( Symbolic c
  , FromConstant Natural (EC.BaseField (Ed25519 c))
  )=> PedersonSetup (Point (Ed25519 c)) where
    pedersonGH :: (Point (Ed25519 c), Point (Ed25519 c))
pedersonGH = (Point (Ed25519 c)
g, Point (Ed25519 c)
h)
        where
            -- Random points on Ed25519
            -- The only requirement for them is so that nobody knows discrete logarithm of g base h
            -- Keeping these numbers open seems safe as there is no known efficient algorithm to calculate discrete logarithm
            -- TODO: Consider choosing these elements randomly each time instead of hardcoding them
            g :: Point (Ed25519 c)
g = BaseField (Ed25519 c) -> BaseField (Ed25519 c) -> Point (Ed25519 c)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
                  (forall a b. FromConstant a b => a -> b
fromConstant @Natural Nat
45227885944482439959027551729127369191274275081056396600348249292591790930260)
                  (forall a b. FromConstant a b => a -> b
fromConstant @Natural Nat
9659338654347744907807571808778983510552562195096080698048062169240435167699)

            h :: Point (Ed25519 c)
h = BaseField (Ed25519 c) -> BaseField (Ed25519 c) -> Point (Ed25519 c)
forall {k} (curve :: k).
BaseField curve -> BaseField curve -> Point curve
Point
                  (forall a b. FromConstant a b => a -> b
fromConstant @Natural Nat
11786464992768388791034908016886244722767117967376829028161961151214849049496)
                  (forall a b. FromConstant a b => a -> b
fromConstant @Natural Nat
37077270161988888430676469598430826385740357039952739548288460740953233965539)

-- | Pedersen commitment scheme
-- Commitment key consists of field elements g and h, and randomness r
--
instance
    ( Symbolic ctx
    , EllipticCurve c
    , SymbolicData (Point c)
    , Context (Point c) ~ ctx
    , PedersonSetup (Point c)
    , Layout (Point c) ~ l
    , Representable l
    , Traversable l
    ) => HomomorphicCommit (FieldElement ctx) (FieldElement ctx) (Point c) where
    hcommit :: FieldElement ctx -> FieldElement ctx -> Point c
hcommit FieldElement ctx
r FieldElement ctx
b = let (Point c
g, Point c
h) = forall a. PedersonSetup a => (a, a)
pedersonGH @(Point c)
                   in FieldElement ctx -> Point c -> Point c
forall b a. Scale b a => b -> a -> a
scale FieldElement ctx
b Point c
g Point c -> Point c -> Point c
forall a. AdditiveSemigroup a => a -> a -> a
+ FieldElement ctx -> Point c -> Point c
forall b a. Scale b a => b -> a -> a
scale FieldElement ctx
r Point c
h


-- Pedersen commitment scheme for lists extending the homomorphism to elementwise sums:
-- (hcommit ck l1) + (hcommit ck l2) = hcommit ck (zipWith (+) l1 l2), provided l1 and l2 have the same length.
-- This is required for AccumulatorScheme
--
instance (EllipticCurve c, HomomorphicCommit a b (Point c), Foldable t) => HomomorphicCommit a (t b) (Point c) where
    hcommit :: a -> t b -> Point c
hcommit a
ck t b
t = [Point c] -> Point c
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ([Point c] -> Point c) -> [Point c] -> Point c
forall a b. (a -> b) -> a -> b
$ (Nat -> Point c -> Point c) -> [Nat] -> [Point c] -> [Point c]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Nat -> Point c -> Point c
forall {k} (curve :: k) s.
(EllipticCurve curve, BinaryExpansion s, Bits s ~ [s], Eq s) =>
s -> Point curve -> Point curve
pointMul [Nat
1 :: Natural ..] (a -> b -> Point c
forall ck a c. HomomorphicCommit ck a c => ck -> a -> c
hcommit a
ck (b -> Point c) -> [b] -> [Point c]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> t b -> [b]
forall a. t a -> [a]
forall (t :: Type -> Type) a. Foldable t => t a -> [a]
toList t b
t)