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

module ZkFold.Base.Protocol.Protostar.CommitOpen where

import           GHC.Generics
import           Prelude                                     hiding (Eq (..), length, (&&), (/=), (==))

import           ZkFold.Base.Data.ByteString
import           ZkFold.Base.Protocol.Protostar.Oracle
import           ZkFold.Base.Protocol.Protostar.SpecialSound (AlgebraicMap (..), SpecialSoundProtocol (..),
                                                              SpecialSoundTranscript)
import           ZkFold.Prelude                              (length)
import           ZkFold.Symbolic.Data.Bool
import           ZkFold.Symbolic.Data.Eq

data CommitOpen m c a = CommitOpen ([m] -> c) a

instance RandomOracle a b => RandomOracle (CommitOpen m c a) b where
    oracle :: CommitOpen m c a -> b
oracle (CommitOpen [m] -> c
_ a
a) = a -> b
forall a b. RandomOracle a b => a -> b
oracle a
a

data CommitOpenProverMessage m c = Commit c | Open [m]
    deriving (forall x.
 CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x)
-> (forall x.
    Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c)
-> Generic (CommitOpenProverMessage m c)
forall x.
Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c
forall x.
CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall m c x.
Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c
forall m c x.
CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x
$cfrom :: forall m c x.
CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x
from :: forall x.
CommitOpenProverMessage m c -> Rep (CommitOpenProverMessage m c) x
$cto :: forall m c x.
Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c
to :: forall x.
Rep (CommitOpenProverMessage m c) x -> CommitOpenProverMessage m c
Generic

instance (Binary c, Binary m) => Binary (CommitOpenProverMessage m c) where
      put :: CommitOpenProverMessage m c -> Put
put (Commit c
c)  = Word8 -> Put
putWord8 Word8
0 Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> c -> Put
forall t. Binary t => t -> Put
put c
c
      put (Open [m]
msgs) = Word8 -> Put
putWord8 Word8
1 Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> [m] -> Put
forall t. Binary t => t -> Put
put [m]
msgs
      get :: Get (CommitOpenProverMessage m c)
get = do
            Word8
flag <- Get Word8
getWord8
            if Word8
flag Word8 -> Word8 -> Bool
forall b a. Eq b a => a -> a -> b
== Word8
0 then c -> CommitOpenProverMessage m c
forall m c. c -> CommitOpenProverMessage m c
Commit (c -> CommitOpenProverMessage m c)
-> Get c -> Get (CommitOpenProverMessage m c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get c
forall t. Binary t => Get t
get
            else if Word8
flag Word8 -> Word8 -> Bool
forall b a. Eq b a => a -> a -> b
== Word8
1 then [m] -> CommitOpenProverMessage m c
forall m c. [m] -> CommitOpenProverMessage m c
Open ([m] -> CommitOpenProverMessage m c)
-> Get [m] -> Get (CommitOpenProverMessage m c)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [m]
forall t. Binary t => Get t
get
            else String -> Get (CommitOpenProverMessage m c)
forall a. String -> Get a
forall (m :: Type -> Type) a. MonadFail m => String -> m a
fail (String
"Binary (CommitOpenProverMessage t c a): unexpected flag " String -> String -> String
forall a. Semigroup a => a -> a -> a
<> Word8 -> String
forall a. Show a => a -> String
show Word8
flag)

instance
    ( SpecialSoundProtocol f a
    , BoolType (VerifierOutput f a)
    , Eq (VerifierOutput f a) [c]
    , m ~ ProverMessage f a
    ) => SpecialSoundProtocol f (CommitOpen m c a) where
      type Witness f (CommitOpen m c a)         = (Witness f a, [m])
      type Input f (CommitOpen m c a)           = Input f a
      type ProverMessage f (CommitOpen m c a)   = CommitOpenProverMessage m c
      type VerifierMessage f (CommitOpen m c a) = VerifierMessage f a
      type VerifierOutput f (CommitOpen m c a)  = VerifierOutput f a

      type Degree (CommitOpen m c a)            = Degree a

      outputLength :: CommitOpen m c a -> Natural
outputLength (CommitOpen [m] -> c
_ a
a) = forall f a. SpecialSoundProtocol f a => a -> Natural
outputLength @f a
a

      rounds :: CommitOpen m c a -> Natural
rounds (CommitOpen [m] -> c
_ a
a) = forall f a. SpecialSoundProtocol f a => a -> Natural
rounds @f a
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1

      prover :: CommitOpen m c a
-> Witness f (CommitOpen m c a)
-> Input f (CommitOpen m c a)
-> SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a)
prover (CommitOpen [m] -> c
cm a
a) (Witness f a
w, [m]
ms) Input f (CommitOpen m c a)
i SpecialSoundTranscript f (CommitOpen m c a)
ts
            | [(CommitOpenProverMessage m c, VerifierMessage f a)] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length SpecialSoundTranscript f (CommitOpen m c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts Natural -> Natural -> Bool
forall b a. Eq b a => a -> a -> b
/= [m] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length [m]
ms  = String -> CommitOpenProverMessage m c
forall a. HasCallStack => String -> a
error String
"Invalid transcript length"
            | [(CommitOpenProverMessage m c, VerifierMessage f a)] -> Natural
forall (t :: Type -> Type) a. Foldable t => t a -> Natural
length SpecialSoundTranscript f (CommitOpen m c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts Natural -> Natural -> Bool
forall a. Ord a => a -> a -> Bool
< forall f a. SpecialSoundProtocol f a => a -> Natural
rounds @f a
a = c -> CommitOpenProverMessage m c
forall m c. c -> CommitOpenProverMessage m c
Commit (c -> CommitOpenProverMessage m c)
-> c -> CommitOpenProverMessage m c
forall a b. (a -> b) -> a -> b
$ [m] -> c
cm [forall f a.
SpecialSoundProtocol f a =>
a
-> Witness f a
-> Input f a
-> SpecialSoundTranscript f a
-> ProverMessage f a
prover @f a
a Witness f a
w Input f a
Input f (CommitOpen m c a)
i (SpecialSoundTranscript f a -> ProverMessage f a)
-> SpecialSoundTranscript f a -> ProverMessage f a
forall a b. (a -> b) -> a -> b
$ [ProverMessage f a]
-> [VerifierMessage f a] -> SpecialSoundTranscript f a
forall a b. [a] -> [b] -> [(a, b)]
zip [m]
[ProverMessage f a]
ms ([VerifierMessage f a] -> SpecialSoundTranscript f a)
-> [VerifierMessage f a] -> SpecialSoundTranscript f a
forall a b. (a -> b) -> a -> b
$ ((CommitOpenProverMessage m c, VerifierMessage f a)
 -> VerifierMessage f a)
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [VerifierMessage f a]
forall a b. (a -> b) -> [a] -> [b]
map (CommitOpenProverMessage m c, VerifierMessage f a)
-> VerifierMessage f a
forall a b. (a, b) -> b
snd SpecialSoundTranscript f (CommitOpen m c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts]
            | Bool
otherwise               = [m] -> CommitOpenProverMessage m c
forall m c. [m] -> CommitOpenProverMessage m c
Open [m]
ms

      verifier :: CommitOpen m c a
-> Input f (CommitOpen m c a)
-> [ProverMessage f (CommitOpen m c a)]
-> [f]
-> VerifierOutput f (CommitOpen m c a)
verifier (CommitOpen [m] -> c
cm a
a) Input f (CommitOpen m c a)
i ((Open [m]
ms):[ProverMessage f (CommitOpen m c a)]
mss) (f
_:[f]
ts) = (m -> c) -> [m] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map ([m] -> c
cm ([m] -> c) -> (m -> [m]) -> m -> c
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> [m]
forall a. a -> [a]
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure) [m]
ms [c] -> [c] -> VerifierOutput f a
forall b a. Eq b a => a -> a -> b
== (CommitOpenProverMessage m c -> c)
-> [CommitOpenProverMessage m c] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map CommitOpenProverMessage m c -> c
forall {m} {c}. CommitOpenProverMessage m c -> c
f [ProverMessage f (CommitOpen m c a)]
[CommitOpenProverMessage m c]
mss VerifierOutput f a -> VerifierOutput f a -> VerifierOutput f a
forall b. BoolType b => b -> b -> b
&& forall f a.
SpecialSoundProtocol f a =>
a -> Input f a -> [ProverMessage f a] -> [f] -> VerifierOutput f a
verifier @f a
a Input f a
Input f (CommitOpen m c a)
i [m]
[ProverMessage f a]
ms [f]
ts
            where f :: CommitOpenProverMessage m c -> c
f (Commit c
c) = c
c
                  f CommitOpenProverMessage m c
_          = String -> c
forall a. HasCallStack => String -> a
error String
"Invalid message"
      verifier CommitOpen m c a
_ Input f (CommitOpen m c a)
_ [ProverMessage f (CommitOpen m c a)]
_ [f]
_ = String -> VerifierOutput f a
forall a. HasCallStack => String -> a
error String
"Invalid transcript"

instance (AlgebraicMap f a, m ~ MapMessage f a) => AlgebraicMap f (CommitOpen m c a) where
      type MapInput f (CommitOpen m c a)     = MapInput f a
      type MapMessage f (CommitOpen m c a)   = CommitOpenProverMessage m c

      algebraicMap :: CommitOpen m c a
-> MapInput f (CommitOpen m c a)
-> [MapMessage f (CommitOpen m c a)]
-> [f]
-> f
-> [f]
algebraicMap (CommitOpen [m] -> c
_ a
a) MapInput f (CommitOpen m c a)
i ((Open [m]
ms):[MapMessage f (CommitOpen m c a)]
_) [f]
ts = forall f a.
AlgebraicMap f a =>
a -> MapInput f a -> [MapMessage f a] -> [f] -> f -> [f]
algebraicMap @f a
a MapInput f a
MapInput f (CommitOpen m c a)
i [m]
[MapMessage f a]
ms [f]
ts
      algebraicMap CommitOpen m c a
_ MapInput f (CommitOpen m c a)
_ [MapMessage f (CommitOpen m c a)]
_ [f]
_                             = String -> f -> [f]
forall a. HasCallStack => String -> a
error String
"CommitOpen algebraic map: invalid transcript"


commits
    :: forall f a c m
    .  SpecialSoundTranscript f (CommitOpen m c a) -> [c]
commits :: forall f a c m. SpecialSoundTranscript f (CommitOpen m c a) -> [c]
commits = ((CommitOpenProverMessage m c, VerifierMessage f a) -> c)
-> [(CommitOpenProverMessage m c, VerifierMessage f a)] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map (ProverMessage f (CommitOpen m c a),
 VerifierMessage f (CommitOpen m c a))
-> c
(CommitOpenProverMessage m c, VerifierMessage f a) -> c
f
      where
          f :: (ProverMessage f (CommitOpen m c a), VerifierMessage f (CommitOpen m c a)) -> c
          f :: (ProverMessage f (CommitOpen m c a),
 VerifierMessage f (CommitOpen m c a))
-> c
f (Commit c
c, VerifierMessage f (CommitOpen m c a)
_) = c
c
          f (ProverMessage f (CommitOpen m c a),
 VerifierMessage f (CommitOpen m c a))
_             = String -> c
forall a. HasCallStack => String -> a
error String
"Invalid message"

opening
    :: 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 :: 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 a' :: CommitOpen m c a
a'@(CommitOpen [m] -> c
_ a
a) Witness f a
w Input f a
i SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a
challenge =
      let f :: ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
-> Natural
-> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
f ([m]
ms, [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts) Natural
_ =
                  let rs :: [VerifierMessage f a]
rs  = (CommitOpenProverMessage m c, VerifierMessage f a)
-> VerifierMessage f a
forall a b. (a, b) -> b
snd ((CommitOpenProverMessage m c, VerifierMessage f a)
 -> VerifierMessage f a)
-> [(CommitOpenProverMessage m c, VerifierMessage f a)]
-> [VerifierMessage f a]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> [(CommitOpenProverMessage m c, VerifierMessage f a)]
ts
                      tsA :: [(m, VerifierMessage f a)]
tsA = [m] -> [VerifierMessage f a] -> [(m, VerifierMessage f a)]
forall a b. [a] -> [b] -> [(a, b)]
zip [m]
ms [VerifierMessage f a]
rs
                      m :: ProverMessage f a
m   = forall f a.
SpecialSoundProtocol f a =>
a
-> Witness f a
-> Input f a
-> SpecialSoundTranscript f a
-> ProverMessage f a
prover @f a
a Witness f a
w Input f a
i [(m, VerifierMessage f a)]
SpecialSoundTranscript f a
tsA
                      c :: ProverMessage f (CommitOpen m c a)
c   = forall f a.
SpecialSoundProtocol f a =>
a
-> Witness f a
-> Input f a
-> SpecialSoundTranscript f a
-> ProverMessage f a
prover @f CommitOpen m c a
a' (Witness f a
w, [m]
ms) Input f a
Input f (CommitOpen m c a)
i SpecialSoundTranscript f (CommitOpen m c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts
                  in ([m]
ms [m] -> [m] -> [m]
forall a. [a] -> [a] -> [a]
++ [m
ProverMessage f a
m], [(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]
++ [(ProverMessage f (CommitOpen m c a)
CommitOpenProverMessage m c
c, SpecialSoundTranscript f (CommitOpen m c a)
-> ProverMessage f (CommitOpen m c a) -> VerifierMessage f a
challenge SpecialSoundTranscript f (CommitOpen m c a)
[(CommitOpenProverMessage m c, VerifierMessage f a)]
ts ProverMessage f (CommitOpen m c a)
c)])
      in (([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
 -> Natural
 -> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)]))
-> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
-> [Natural]
-> ([m], [(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 ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
-> Natural
-> ([m], [(CommitOpenProverMessage m c, VerifierMessage f a)])
f ([], []) [Natural
1 .. forall f a. SpecialSoundProtocol f a => a -> Natural
rounds @f a
a]