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

module ZkFold.Base.Protocol.Protostar.FiatShamir where

import           Data.ByteString                             (ByteString)
import           GHC.Generics
import           Prelude                                     hiding (Bool (..), Eq (..), length)
import qualified Prelude                                     as P

import           ZkFold.Base.Data.ByteString                 (Binary (..))
import           ZkFold.Base.Protocol.NonInteractiveProof    (NonInteractiveProof (..), ToTranscript (..), challenge)
import           ZkFold.Base.Protocol.Protostar.CommitOpen
import qualified ZkFold.Base.Protocol.Protostar.SpecialSound as SpS
import           ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Eq

data FiatShamir f a = FiatShamir a (SpS.Input f a)
    deriving (forall x. FiatShamir f a -> Rep (FiatShamir f a) x)
-> (forall x. Rep (FiatShamir f a) x -> FiatShamir f a)
-> Generic (FiatShamir f a)
forall x. Rep (FiatShamir f a) x -> FiatShamir f a
forall x. FiatShamir f a -> Rep (FiatShamir f a) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall f a x. Rep (FiatShamir f a) x -> FiatShamir f a
forall f a x. FiatShamir f a -> Rep (FiatShamir f a) x
$cfrom :: forall f a x. FiatShamir f a -> Rep (FiatShamir f a) x
from :: forall x. FiatShamir f a -> Rep (FiatShamir f a) x
$cto :: forall f a x. Rep (FiatShamir f a) x -> FiatShamir f a
to :: forall x. Rep (FiatShamir f a) x -> FiatShamir f a
Generic

fsChallenge
    :: forall f a c m
    .  Binary (SpS.Input f a)
    => Binary (VerifierMessage f a)
    => Binary c
    => Binary (ProverMessage f a)
    => m ~ ProverMessage f a
    => FiatShamir f (CommitOpen m c a)
    -> SpecialSoundTranscript f (CommitOpen m c a) -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a
fsChallenge :: forall f a c m.
(Binary (Input f a), Binary (VerifierMessage f a), Binary c,
 Binary (ProverMessage f a), m ~ ProverMessage f a) =>
FiatShamir f (CommitOpen m c a)
-> SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a)
-> VerifierMessage f a
fsChallenge (FiatShamir CommitOpen m c a
_ Input f (CommitOpen m c a)
ip) []           ProverMessage f (CommitOpen m c a)
c =
      let r0 :: VerifierMessage f a
r0 = forall ts a. FromTranscript ts a => ts -> a
challenge @ByteString (ByteString -> VerifierMessage f a)
-> ByteString -> VerifierMessage f a
forall a b. (a -> b) -> a -> b
$ Input f a -> ByteString
forall ts a. ToTranscript ts a => a -> ts
toTranscript Input f a
Input f (CommitOpen m c a)
ip :: VerifierMessage f a
      in forall ts a. FromTranscript ts a => ts -> a
challenge @ByteString (ByteString -> VerifierMessage f a)
-> ByteString -> VerifierMessage f a
forall a b. (a -> b) -> a -> b
$ VerifierMessage f a -> ByteString
forall ts a. ToTranscript ts a => a -> ts
toTranscript VerifierMessage f a
r0 ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> CommitOpenProverMessage m c -> ByteString
forall ts a. ToTranscript ts a => a -> ts
toTranscript ProverMessage f (CommitOpen m c a)
CommitOpenProverMessage m c
c
fsChallenge FiatShamir f (CommitOpen m c a)
_                 ((ProverMessage f (CommitOpen m c a)
_, VerifierMessage f (CommitOpen m c a)
r) : [(ProverMessage f (CommitOpen m c a),
  VerifierMessage f (CommitOpen m c a))]
_) ProverMessage f (CommitOpen m c a)
c = forall ts a. FromTranscript ts a => ts -> a
challenge @ByteString (ByteString -> VerifierMessage f a)
-> ByteString -> VerifierMessage f a
forall a b. (a -> b) -> a -> b
$ VerifierMessage f a -> ByteString
forall ts a. ToTranscript ts a => a -> ts
toTranscript VerifierMessage f a
VerifierMessage f (CommitOpen m c a)
r ByteString -> ByteString -> ByteString
forall a. Semigroup a => a -> a -> a
<> CommitOpenProverMessage m c -> ByteString
forall ts a. ToTranscript ts a => a -> ts
toTranscript ProverMessage f (CommitOpen m c a)
CommitOpenProverMessage m c
c

instance
    ( SpS.SpecialSoundProtocol f a
    , Binary (SpS.Input f a)
    , Binary (VerifierMessage f a)
    , VerifierMessage f a ~ f
    , ProverMessage f a ~ m
    , Binary c
    , Binary (ProverMessage f a)
    , BoolType (VerifierOutput f a)
    , Eq (VerifierOutput f a) [c]
    , VerifierOutput f a ~ P.Bool
    ) => NonInteractiveProof (FiatShamir f (CommitOpen m c a)) core where
      type Transcript (FiatShamir f (CommitOpen m c a))  = ByteString
      type SetupProve (FiatShamir f (CommitOpen m c a))  = FiatShamir f (CommitOpen m c a)
      type SetupVerify (FiatShamir f (CommitOpen m c a)) = FiatShamir f (CommitOpen m c a)
      type Witness (FiatShamir f (CommitOpen m c a))     = SpS.Witness f a
      type Input (FiatShamir f (CommitOpen m c a))       = (SpS.Input f a, [c])
      type Proof (FiatShamir f (CommitOpen m c a))       = [ProverMessage f a]

      setupProve :: FiatShamir f (CommitOpen m c a)
-> SetupProve (FiatShamir f (CommitOpen m c a))
setupProve FiatShamir f (CommitOpen m c a)
x = SetupProve (FiatShamir f (CommitOpen m c a))
FiatShamir f (CommitOpen m c a)
x

      setupVerify :: FiatShamir f (CommitOpen m c a)
-> SetupVerify (FiatShamir f (CommitOpen m c a))
setupVerify FiatShamir f (CommitOpen m c a)
x = SetupVerify (FiatShamir f (CommitOpen m c a))
FiatShamir f (CommitOpen m c a)
x

      prove :: SetupProve (FiatShamir f (CommitOpen m c a))
-> Witness (FiatShamir f (CommitOpen m c a))
-> (Input (FiatShamir f (CommitOpen m c a)),
    Proof (FiatShamir f (CommitOpen m c a)))
prove fs :: SetupProve (FiatShamir f (CommitOpen m c a))
fs@(FiatShamir CommitOpen m c a
a Input f (CommitOpen m c a)
ip) Witness (FiatShamir f (CommitOpen m c a))
w =
            let ([m]
ms, SpecialSoundTranscript f (CommitOpen m c a)
ts) = forall f a c m.
(SpecialSoundProtocol f a, BoolType (VerifierOutput f a),
 Eq (VerifierOutput f a) [c], m ~ ProverMessage f a) =>
CommitOpen m c a
-> Witness f a
-> Input f a
-> (SpecialSoundTranscript f (CommitOpen m c a)
    -> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a)
-> ([m], SpecialSoundTranscript f (CommitOpen m c a))
opening @f @a @c @m CommitOpen m c a
a Witness f a
Witness (FiatShamir f (CommitOpen m c a))
w Input f a
Input f (CommitOpen m c a)
ip (FiatShamir f (CommitOpen (ProverMessage f a) c a)
-> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a)
-> ProverMessage f (CommitOpen (ProverMessage f a) c a)
-> VerifierMessage f a
forall f a c m.
(Binary (Input f a), Binary (VerifierMessage f a), Binary c,
 Binary (ProverMessage f a), m ~ ProverMessage f a) =>
FiatShamir f (CommitOpen m c a)
-> SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a)
-> VerifierMessage f a
fsChallenge SetupProve (FiatShamir f (CommitOpen m c a))
FiatShamir f (CommitOpen (ProverMessage f a) c a)
fs)
            in ((Input f a
Input f (CommitOpen m c a)
ip, forall f a c m. SpecialSoundTranscript f (CommitOpen m c a) -> [c]
commits @f @a @c @m SpecialSoundTranscript f (CommitOpen m c a)
ts), [m]
Proof (FiatShamir f (CommitOpen m c a))
ms)

      verify :: SetupVerify (FiatShamir f (CommitOpen m c a))
-> Input (FiatShamir f (CommitOpen m c a))
-> Proof (FiatShamir f (CommitOpen m c a))
-> Bool
verify fs :: SetupVerify (FiatShamir f (CommitOpen m c a))
fs@(FiatShamir CommitOpen m c a
a Input f (CommitOpen m c a)
_) (Input f a
ip, [c]
cs) Proof (FiatShamir f (CommitOpen m c a))
ms =
            let ts' :: [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts' = ([(CommitOpenProverMessage m c, VerifierMessage f a)]
 -> CommitOpenProverMessage m c
 -> [(CommitOpenProverMessage m c, VerifierMessage f a)])
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [CommitOpenProverMessage m c]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
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 (\[(CommitOpenProverMessage m c, VerifierMessage f a)]
acc CommitOpenProverMessage m c
c -> [(CommitOpenProverMessage m c, VerifierMessage f a)]
acc [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
forall a. [a] -> [a] -> [a]
++ [(CommitOpenProverMessage m c
c, FiatShamir f (CommitOpen (ProverMessage f a) c a)
-> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a)
-> ProverMessage f (CommitOpen (ProverMessage f a) c a)
-> VerifierMessage f a
forall f a c m.
(Binary (Input f a), Binary (VerifierMessage f a), Binary c,
 Binary (ProverMessage f a), m ~ ProverMessage f a) =>
FiatShamir f (CommitOpen m c a)
-> SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a)
-> VerifierMessage f a
fsChallenge SetupVerify (FiatShamir f (CommitOpen m c a))
FiatShamir f (CommitOpen (ProverMessage f a) c a)
fs SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
acc ProverMessage f (CommitOpen (ProverMessage f a) c a)
CommitOpenProverMessage m c
c)]) [] ([CommitOpenProverMessage m c]
 -> [(CommitOpenProverMessage m c, VerifierMessage f a)])
-> [CommitOpenProverMessage m c]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
forall a b. (a -> b) -> a -> b
$ (c -> CommitOpenProverMessage m c)
-> [c] -> [CommitOpenProverMessage m c]
forall a b. (a -> b) -> [a] -> [b]
map c -> CommitOpenProverMessage m c
forall m c. c -> CommitOpenProverMessage m c
Commit [c]
cs
                ts :: [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts  = [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts' [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
forall a. [a] -> [a] -> [a]
++ [([m] -> CommitOpenProverMessage m c
forall m c. [m] -> CommitOpenProverMessage m c
Open [m]
Proof (FiatShamir f (CommitOpen m c a))
ms, FiatShamir f (CommitOpen (ProverMessage f a) c a)
-> SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a)
-> ProverMessage f (CommitOpen (ProverMessage f a) c a)
-> VerifierMessage f a
forall f a c m.
(Binary (Input f a), Binary (VerifierMessage f a), Binary c,
 Binary (ProverMessage f a), m ~ ProverMessage f a) =>
FiatShamir f (CommitOpen m c a)
-> SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a)
-> VerifierMessage f a
fsChallenge SetupVerify (FiatShamir f (CommitOpen m c a))
FiatShamir f (CommitOpen (ProverMessage f a) c a)
fs SpecialSoundTranscript f (CommitOpen (ProverMessage f a) c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts' (ProverMessage f (CommitOpen (ProverMessage f a) c a)
 -> VerifierMessage f a)
-> ProverMessage f (CommitOpen (ProverMessage f a) c a)
-> VerifierMessage f a
forall a b. (a -> b) -> a -> b
$ [m] -> CommitOpenProverMessage m c
forall m c. [m] -> CommitOpenProverMessage m c
Open [m]
Proof (FiatShamir f (CommitOpen m c a))
ms)]
                ([CommitOpenProverMessage m c]
ri, [VerifierMessage f a]
ci) = [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> ([CommitOpenProverMessage m c], [VerifierMessage f a])
forall a b. [(a, b)] -> ([a], [b])
unzip [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts
            in CommitOpen m c a
-> Input (VerifierMessage f a) (CommitOpen m c a)
-> [ProverMessage (VerifierMessage f a) (CommitOpen m c a)]
-> [VerifierMessage f a]
-> VerifierOutput (VerifierMessage f a) (CommitOpen m c a)
forall f a.
SpecialSoundProtocol f a =>
a -> Input f a -> [ProverMessage f a] -> [f] -> VerifierOutput f a
verifier CommitOpen m c a
a Input f a
Input (VerifierMessage f a) (CommitOpen m c a)
ip [ProverMessage (VerifierMessage f a) (CommitOpen m c a)]
[CommitOpenProverMessage m c]
ri [VerifierMessage f a]
ci