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

module ZkFold.Base.Protocol.Protostar.FiatShamir where

import           Data.Constraint                             (withDict)
import           Data.Constraint.Nat                         (plusMinusInverse1)
import           GHC.Generics                                (Generic)
import           Prelude                                     hiding (Bool (..), Eq (..), init, length, pi, scanl, unzip)

import           ZkFold.Base.Algebra.Basic.Class             (Ring)
import           ZkFold.Base.Algebra.Basic.Number            (KnownNat, type (-))
import           ZkFold.Base.Data.Vector                     (Vector, init, item, scanl, unfold)
import           ZkFold.Base.Protocol.Protostar.Commit       (HomomorphicCommit)
import           ZkFold.Base.Protocol.Protostar.CommitOpen
import           ZkFold.Base.Protocol.Protostar.Oracle       (RandomOracle (..))
import           ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..))

newtype FiatShamir a = FiatShamir a
    deriving (forall x. FiatShamir a -> Rep (FiatShamir a) x)
-> (forall x. Rep (FiatShamir a) x -> FiatShamir a)
-> Generic (FiatShamir a)
forall x. Rep (FiatShamir a) x -> FiatShamir a
forall x. FiatShamir a -> Rep (FiatShamir a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall a x. Rep (FiatShamir a) x -> FiatShamir a
forall a x. FiatShamir a -> Rep (FiatShamir a) x
$cfrom :: forall a x. FiatShamir a -> Rep (FiatShamir a) x
from :: forall x. FiatShamir a -> Rep (FiatShamir a) x
$cto :: forall a x. Rep (FiatShamir a) x -> FiatShamir a
to :: forall x. Rep (FiatShamir a) x -> FiatShamir a
Generic

-- The transcript of the Fiat-Shamired protocol (ignoring the last round)
transcriptFiatShamir :: forall f c k . (Ring f, RandomOracle f f, RandomOracle c f) => f -> Vector k c -> Vector (k-1) f
transcriptFiatShamir :: forall f c (k :: Natural).
(Ring f, RandomOracle f f, RandomOracle c f) =>
f -> Vector k c -> Vector (k - 1) f
transcriptFiatShamir f
r0 Vector k c
cs = Dict (((k + 1) - 1) ~ k)
-> ((((k + 1) - 1) ~ k) => Vector (k - 1) f) -> Vector (k - 1) f
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural). Dict (((m + n) - n) ~ m)
plusMinusInverse1 @1 @k) (((((k + 1) - 1) ~ k) => Vector (k - 1) f) -> Vector (k - 1) f)
-> ((((k + 1) - 1) ~ k) => Vector (k - 1) f) -> Vector (k - 1) f
forall a b. (a -> b) -> a -> b
$ Vector k f -> Vector (k - 1) f
forall (size :: Natural) a. Vector size a -> Vector (size - 1) a
init (Vector k f -> Vector (k - 1) f) -> Vector k f -> Vector (k - 1) f
forall a b. (a -> b) -> a -> b
$ Vector (k + 1) f -> Vector ((k + 1) - 1) f
forall (size :: Natural) a. Vector size a -> Vector (size - 1) a
init (Vector (k + 1) f -> Vector ((k + 1) - 1) f)
-> Vector (k + 1) f -> Vector ((k + 1) - 1) f
forall a b. (a -> b) -> a -> b
$ (f -> c -> f) -> f -> Vector k c -> Vector (k + 1) f
forall (size :: Natural) a b.
(b -> a -> b) -> b -> Vector size a -> Vector (size + 1) b
scanl (((f, c) -> f) -> f -> c -> f
forall a b c. ((a, b) -> c) -> a -> b -> c
curry (forall a b. RandomOracle a b => a -> b
oracle @(f, c))) f
r0 Vector k c
cs

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

        input :: FiatShamir (CommitOpen a) -> i f -> p f -> i f
input (FiatShamir 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) @c @d @k CommitOpen a
a

        prover :: FiatShamir (CommitOpen a)
-> i f -> p f -> f -> Natural -> Vector k (m, c)
prover (FiatShamir CommitOpen a
a) i f
pi0 p f
w f
_ Natural
_ =
            let r0 :: f
r0 = i f -> f
forall a b. RandomOracle a b => a -> b
oracle i f
pi0
                f :: (f, Natural) -> ((m, c), (f, Natural))
f (f
r, Natural
k) =
                    let (m
m', c
c') = 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) @c @d @k CommitOpen a
a i f
pi0 p f
w f
r Natural
k
                    in ((m
m', c
c'), ((f, c) -> f
forall a b. RandomOracle a b => a -> b
oracle (f
r, c
c'), Natural
k Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1))
            in ((f, Natural) -> ((m, c), (f, Natural)))
-> (f, Natural) -> Vector k (m, c)
forall (size :: Natural) a b.
KnownNat size =>
(b -> (a, b)) -> b -> Vector size a
unfold (f, Natural) -> ((m, c), (f, Natural))
f (f
r0, Natural
1)

        verifier :: FiatShamir (CommitOpen a)
-> i f
-> Vector 1 (Vector k (m, c))
-> Vector (1 - 1) f
-> VerifierOutput
     f i p (Vector k (m, c)) c d 1 (FiatShamir (CommitOpen a))
verifier (FiatShamir CommitOpen a
a) i f
pi Vector 1 (Vector k (m, c))
pms' Vector (1 - 1) f
_ =
            let pms :: Vector k (m, c)
pms = Vector 1 (Vector k (m, c)) -> Vector k (m, c)
forall a. Vector 1 a -> a
item Vector 1 (Vector k (m, c))
pms'
                r0 :: f
r0 = i f -> f
forall a b. RandomOracle a b => a -> b
oracle i f
pi :: f
                rs :: Vector (k - 1) f
rs = f -> Vector k c -> Vector (k - 1) f
forall f c (k :: Natural).
(Ring f, RandomOracle f f, RandomOracle c f) =>
f -> Vector k c -> Vector (k - 1) f
transcriptFiatShamir f
r0 (Vector k c -> Vector (k - 1) f) -> Vector k c -> Vector (k - 1) f
forall a b. (a -> b) -> a -> b
$ ((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 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 @i @p @(m, c) @c @d @k CommitOpen a
a i f
pi Vector k (m, c)
pms Vector (k - 1) f
rs