{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.Protostar.CommitOpen where

import           Data.Zip                                    (zipWith)
import           Prelude                                     hiding (Num (..), length, pi, tail, zipWith, (&&))

import           ZkFold.Base.Algebra.Basic.Class             (AdditiveGroup (..))
import           ZkFold.Base.Data.Vector                     (Vector)
import           ZkFold.Base.Protocol.Protostar.Commit       (HomomorphicCommit (hcommit))
import           ZkFold.Base.Protocol.Protostar.Oracle
import           ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..))

newtype CommitOpen a = CommitOpen a

instance RandomOracle a b => RandomOracle (CommitOpen a) b where
    oracle :: CommitOpen a -> b
oracle (CommitOpen a
a) = a -> b
forall a b. RandomOracle a b => a -> b
oracle a
a

instance
    ( SpecialSoundProtocol f i p m c d k a
    , HomomorphicCommit m c
    ) => SpecialSoundProtocol f i p (m, c) c d k (CommitOpen a) where
      type VerifierOutput f i p (m, c) c d k (CommitOpen a) = (Vector k c, VerifierOutput f i p m c d k a)

      input :: CommitOpen a -> i f -> p f -> i f
input (CommitOpen a
a) = forall {k} {k1} f (i :: Type -> Type) (p :: Type -> Type) m
       (c :: k) (d :: k1) (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> i f
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> i f
input @_ @_ @_ @m @c @d @k a
a

      prover :: CommitOpen a -> i f -> p f -> f -> Natural -> (m, c)
prover (CommitOpen a
a) i f
pi0 p f
w f
r Natural
i =
            let m :: m
m = forall {k} {k1} f (i :: Type -> Type) (p :: Type -> Type) m
       (c :: k) (d :: k1) (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> f -> Natural -> m
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> f -> Natural -> m
prover @f @i @_ @m @c @d @k a
a i f
pi0 p f
w f
r Natural
i
            in (m
m, m -> c
forall a c. HomomorphicCommit a c => a -> c
hcommit m
m)

      verifier :: CommitOpen a
-> i f
-> Vector k (m, c)
-> Vector (k - 1) f
-> VerifierOutput f i p (m, c) c d k (CommitOpen a)
verifier (CommitOpen a
a) i f
pi Vector k (m, c)
pms Vector (k - 1) f
rs =
            let ms :: Vector k m
ms = ((m, c) -> m) -> Vector k (m, c) -> Vector k m
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (m, c) -> m
forall a b. (a, b) -> a
fst Vector k (m, c)
pms
                cs :: Vector k c
cs = ((m, c) -> c) -> Vector k (m, c) -> Vector k c
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (m, c) -> c
forall a b. (a, b) -> b
snd Vector k (m, c)
pms
            in ((c -> c -> c) -> Vector k c -> Vector k c -> Vector k c
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (-) ((m -> c) -> Vector k m -> Vector k c
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap m -> c
forall a c. HomomorphicCommit a c => a -> c
hcommit Vector k m
ms) Vector k c
cs, forall {k} {k1} f (i :: Type -> Type) (p :: Type -> Type) m
       (c :: k) (d :: k1) (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a
-> i f
-> Vector k2 m
-> Vector (k2 - 1) f
-> VerifierOutput f i p m c d k2 a
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a
-> i f
-> Vector k2 m
-> Vector (k2 - 1) f
-> VerifierOutput f i p m c d k2 a
verifier @f @_ @p @m @c @d @k a
a i f
pi Vector k m
ms Vector (k - 1) f
rs)