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

module ZkFold.Base.Protocol.ARK.Protostar.CommitOpen where

import           Prelude                                         hiding (length)

import           ZkFold.Base.Data.ByteString
import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound (SpecialSoundProtocol (..), SpecialSoundTranscript)
import           ZkFold.Prelude                                  (length)

data CommitOpen f c a = CommitOpen (ProverMessage f a -> c) a

data CommitOpenProverMessage t c a = Commit c | Open [ProverMessage t a]
instance (Binary c, Binary (ProverMessage t a)) => Binary (CommitOpenProverMessage t c a) where
      put :: CommitOpenProverMessage t c a -> 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 [ProverMessage t a]
msgs) = Word8 -> Put
putWord8 Word8
1 Put -> Put -> Put
forall a. Semigroup a => a -> a -> a
<> [ProverMessage t a] -> Put
forall t. Binary t => t -> Put
put [ProverMessage t a]
msgs
      get :: Get (CommitOpenProverMessage t c a)
get = do
            Word8
flag <- Get Word8
getWord8
            if Word8
flag Word8 -> Word8 -> Bool
forall a. Eq a => a -> a -> Bool
== Word8
0 then c -> CommitOpenProverMessage t c a
forall t c a. c -> CommitOpenProverMessage t c a
Commit (c -> CommitOpenProverMessage t c a)
-> Get c -> Get (CommitOpenProverMessage t c a)
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 a. Eq a => a -> a -> Bool
== Word8
1 then [ProverMessage t a] -> CommitOpenProverMessage t c a
forall t c a. [ProverMessage t a] -> CommitOpenProverMessage t c a
Open ([ProverMessage t a] -> CommitOpenProverMessage t c a)
-> Get [ProverMessage t a] -> Get (CommitOpenProverMessage t c a)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Get [ProverMessage t a]
forall t. Binary t => Get t
get
            else String -> Get (CommitOpenProverMessage t c a)
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, Eq c) => SpecialSoundProtocol f (CommitOpen f c a) where
      type Witness f (CommitOpen f c a)         = (Witness f a, [ProverMessage f a])
      type Input f (CommitOpen f c a)           = Input f a
      type ProverMessage t (CommitOpen f c a)   = CommitOpenProverMessage t c a
      type VerifierMessage t (CommitOpen f c a) = VerifierMessage t a

      type Dimension (CommitOpen f c a)         = Dimension a
      type Degree (CommitOpen f c a)            = Degree a

      rounds :: CommitOpen f c a -> Natural
rounds CommitOpen f c a
a = forall f a. SpecialSoundProtocol f a => a -> Natural
rounds @f CommitOpen f c a
a Natural -> Natural -> Natural
forall a. Num a => a -> a -> a
+ Natural
1

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

      -- TODO: Implement this
      verifier' :: CommitOpen f c a
-> Input f (CommitOpen f c a)
-> SpecialSoundTranscript Natural (CommitOpen f c a)
-> Vector (Dimension (CommitOpen f c a)) (Polynomial' f)
verifier' = CommitOpen f c a
-> Input f a
-> [(CommitOpenProverMessage Natural c a,
     VerifierMessage Natural a)]
-> Vector (Dimension a) (Polynomial' f)
CommitOpen f c a
-> Input f (CommitOpen f c a)
-> SpecialSoundTranscript Natural (CommitOpen f c a)
-> Vector (Dimension (CommitOpen f c a)) (Polynomial' f)
forall a. HasCallStack => a
undefined

      verifier :: CommitOpen f c a
-> Input f (CommitOpen f c a)
-> SpecialSoundTranscript f (CommitOpen f c a)
-> Bool
verifier (CommitOpen ProverMessage f a -> c
cm a
a) Input f (CommitOpen f c a)
i ((Open [ProverMessage f a]
ms, VerifierMessage f (CommitOpen f c a)
_) : SpecialSoundTranscript f (CommitOpen f c a)
ts) = (ProverMessage f a -> c) -> [ProverMessage f a] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map ProverMessage f a -> c
cm [ProverMessage f a]
ms [c] -> [c] -> Bool
forall a. Eq a => a -> a -> Bool
== ((CommitOpenProverMessage f c a, VerifierMessage f a) -> c)
-> [(CommitOpenProverMessage f c a, VerifierMessage f a)] -> [c]
forall a b. (a -> b) -> [a] -> [b]
map (CommitOpenProverMessage f c a, VerifierMessage f a) -> c
forall {t} {c} {a} {b}. (CommitOpenProverMessage t c a, b) -> c
f SpecialSoundTranscript f (CommitOpen f c a)
[(CommitOpenProverMessage f c a, VerifierMessage f a)]
ts Bool -> Bool -> Bool
&& forall f a.
SpecialSoundProtocol f a =>
a -> Input f a -> SpecialSoundTranscript f a -> Bool
verifier @f a
a Input f a
Input f (CommitOpen f c a)
i ([ProverMessage f a]
-> [VerifierMessage f a] -> SpecialSoundTranscript f a
forall a b. [a] -> [b] -> [(a, b)]
zip [ProverMessage f a]
ms ([VerifierMessage f a] -> SpecialSoundTranscript f a)
-> [VerifierMessage f a] -> SpecialSoundTranscript f a
forall a b. (a -> b) -> a -> b
$ ((CommitOpenProverMessage f c a, VerifierMessage f a)
 -> VerifierMessage f a)
-> [(CommitOpenProverMessage f c a, VerifierMessage f a)]
-> [VerifierMessage f a]
forall a b. (a -> b) -> [a] -> [b]
map (CommitOpenProverMessage f c a, VerifierMessage f a)
-> VerifierMessage f a
forall a b. (a, b) -> b
snd SpecialSoundTranscript f (CommitOpen f c a)
[(CommitOpenProverMessage f c a, VerifierMessage f a)]
ts)
            where f :: (CommitOpenProverMessage t c a, b) -> c
f (Commit c
c, b
_) = c
c
                  f (CommitOpenProverMessage t c a, b)
_             = String -> c
forall a. HasCallStack => String -> a
error String
"Invalid message"
      verifier CommitOpen f c a
_ Input f (CommitOpen f c a)
_ SpecialSoundTranscript f (CommitOpen f c a)
_ = String -> Bool
forall a. HasCallStack => String -> a
error String
"Invalid transcript"

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

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