{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DeriveAnyClass      #-}
{-# LANGUAGE TypeApplications    #-}

module ZkFold.Base.Protocol.NonInteractiveProof where

import           Control.DeepSeq             (NFData)
import           Crypto.Hash.SHA256          (hash)
import           Data.ByteString             (ByteString, cons)
import           Data.Maybe                  (fromJust)
import           GHC.Generics                (Generic)
import           Numeric.Natural             (Natural)
import           Prelude
import           Test.QuickCheck             (Arbitrary (..), generate, vectorOf)

import           ZkFold.Base.Data.ByteString

class Monoid t => ToTranscript t a where
    toTranscript :: a -> t

instance Binary a => ToTranscript ByteString a where
    toTranscript :: a -> ByteString
toTranscript = a -> ByteString
forall a. Binary a => a -> ByteString
toByteString

transcript :: ToTranscript t a => t -> a -> t
transcript :: forall t a. ToTranscript t a => t -> a -> t
transcript t
ts a
a = t
ts t -> t -> t
forall a. Semigroup a => a -> a -> a
<> a -> t
forall t a. ToTranscript t a => a -> t
toTranscript a
a

class Monoid t => FromTranscript t a where
    newTranscript  :: t -> t
    fromTranscript :: t -> a

instance Binary a => FromTranscript ByteString a where
    newTranscript :: ByteString -> ByteString
newTranscript  = Word8 -> ByteString -> ByteString
cons Word8
0
    fromTranscript :: ByteString -> a
fromTranscript = Maybe a -> a
forall a. HasCallStack => Maybe a -> a
fromJust (Maybe a -> a) -> (ByteString -> Maybe a) -> ByteString -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> Maybe a
forall a. Binary a => ByteString -> Maybe a
fromByteString (ByteString -> Maybe a)
-> (ByteString -> ByteString) -> ByteString -> Maybe a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ByteString -> ByteString
hash

challenge :: forall t a . FromTranscript t a => t -> (a, t)
challenge :: forall t a. FromTranscript t a => t -> (a, t)
challenge t
ts =
    let ts' :: t
ts' = forall t a. FromTranscript t a => t -> t
newTranscript @t @a t
ts
    in (t -> a
forall t a. FromTranscript t a => t -> a
fromTranscript t
ts', t
ts')

challenges :: FromTranscript t a => t -> Natural -> ([a], t)
challenges :: forall t a. FromTranscript t a => t -> Natural -> ([a], t)
challenges t
ts0 Natural
n = t -> Natural -> [a] -> ([a], t)
forall {t} {t} {a}.
(Eq t, Num t, FromTranscript t a) =>
t -> t -> [a] -> ([a], t)
go t
ts0 Natural
n []
  where
    go :: t -> t -> [a] -> ([a], t)
go t
ts t
0 [a]
acc = ([a]
acc, t
ts)
    go t
ts t
k [a]
acc =
        let (a
c, t
ts') = t -> (a, t)
forall t a. FromTranscript t a => t -> (a, t)
challenge t
ts
        in t -> t -> [a] -> ([a], t)
go t
ts' (t
k t -> t -> t
forall a. Num a => a -> a -> a
- t
1) (a
c a -> [a] -> [a]
forall a. a -> [a] -> [a]
: [a]
acc)

class NonInteractiveProof a where
    type Transcript a

    type SetupProve a

    type SetupVerify a

    type Witness a

    type Input a

    type Proof a

    setupProve :: a -> SetupProve a

    setupVerify :: a -> SetupVerify a

    prove :: SetupProve a -> Witness a -> (Input a, Proof a)

    verify :: SetupVerify a -> Input a -> Proof a -> Bool

data ProveAPIResult = ProveAPISuccess ByteString | ProveAPIErrorSetup | ProveAPIErrorWitness
    deriving (Int -> ProveAPIResult -> ShowS
[ProveAPIResult] -> ShowS
ProveAPIResult -> String
(Int -> ProveAPIResult -> ShowS)
-> (ProveAPIResult -> String)
-> ([ProveAPIResult] -> ShowS)
-> Show ProveAPIResult
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> ProveAPIResult -> ShowS
showsPrec :: Int -> ProveAPIResult -> ShowS
$cshow :: ProveAPIResult -> String
show :: ProveAPIResult -> String
$cshowList :: [ProveAPIResult] -> ShowS
showList :: [ProveAPIResult] -> ShowS
Show, ProveAPIResult -> ProveAPIResult -> Bool
(ProveAPIResult -> ProveAPIResult -> Bool)
-> (ProveAPIResult -> ProveAPIResult -> Bool) -> Eq ProveAPIResult
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: ProveAPIResult -> ProveAPIResult -> Bool
== :: ProveAPIResult -> ProveAPIResult -> Bool
$c/= :: ProveAPIResult -> ProveAPIResult -> Bool
/= :: ProveAPIResult -> ProveAPIResult -> Bool
Eq, (forall x. ProveAPIResult -> Rep ProveAPIResult x)
-> (forall x. Rep ProveAPIResult x -> ProveAPIResult)
-> Generic ProveAPIResult
forall x. Rep ProveAPIResult x -> ProveAPIResult
forall x. ProveAPIResult -> Rep ProveAPIResult x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall x. ProveAPIResult -> Rep ProveAPIResult x
from :: forall x. ProveAPIResult -> Rep ProveAPIResult x
$cto :: forall x. Rep ProveAPIResult x -> ProveAPIResult
to :: forall x. Rep ProveAPIResult x -> ProveAPIResult
Generic, ProveAPIResult -> ()
(ProveAPIResult -> ()) -> NFData ProveAPIResult
forall a. (a -> ()) -> NFData a
$crnf :: ProveAPIResult -> ()
rnf :: ProveAPIResult -> ()
NFData)

proveAPI
    :: forall a
    . (NonInteractiveProof a
    , Binary (SetupProve a)
    , Binary (Witness a)
    , Binary (Input a)
    , Binary (Proof a))
    => ByteString
    -> ByteString
    -> ProveAPIResult
proveAPI :: forall a.
(NonInteractiveProof a, Binary (SetupProve a), Binary (Witness a),
 Binary (Input a), Binary (Proof a)) =>
ByteString -> ByteString -> ProveAPIResult
proveAPI ByteString
bsS ByteString
bsW =
    let mS :: Maybe (SetupProve a)
mS = ByteString -> Maybe (SetupProve a)
forall a. Binary a => ByteString -> Maybe a
fromByteString ByteString
bsS
        mW :: Maybe (Witness a)
mW = ByteString -> Maybe (Witness a)
forall a. Binary a => ByteString -> Maybe a
fromByteString ByteString
bsW
    in case (Maybe (SetupProve a)
mS, Maybe (Witness a)
mW) of
        (Maybe (SetupProve a)
Nothing, Maybe (Witness a)
_)     -> ProveAPIResult
ProveAPIErrorSetup
        (Maybe (SetupProve a)
_, Maybe (Witness a)
Nothing)     -> ProveAPIResult
ProveAPIErrorWitness
        (Just SetupProve a
s, Just Witness a
w) -> ByteString -> ProveAPIResult
ProveAPISuccess (ByteString -> ProveAPIResult) -> ByteString -> ProveAPIResult
forall a b. (a -> b) -> a -> b
$ (Input a, Proof a) -> ByteString
forall a. Binary a => a -> ByteString
toByteString ((Input a, Proof a) -> ByteString)
-> (Input a, Proof a) -> ByteString
forall a b. (a -> b) -> a -> b
$ forall a.
NonInteractiveProof a =>
SetupProve a -> Witness a -> (Input a, Proof a)
prove @a SetupProve a
s Witness a
w

testVector :: forall a .
    NonInteractiveProof a =>
    Arbitrary a =>
    Arbitrary (Witness a) =>
    Binary (SetupProve a) =>
    Binary (Input a) =>
    Binary (Proof a) =>
    Int -> IO [(ByteString, ByteString, ByteString)]
testVector :: forall a.
(NonInteractiveProof a, Arbitrary a, Arbitrary (Witness a),
 Binary (SetupProve a), Binary (Input a), Binary (Proof a)) =>
Int -> IO [(ByteString, ByteString, ByteString)]
testVector Int
n = Gen [(ByteString, ByteString, ByteString)]
-> IO [(ByteString, ByteString, ByteString)]
forall a. Gen a -> IO a
generate (Gen [(ByteString, ByteString, ByteString)]
 -> IO [(ByteString, ByteString, ByteString)])
-> (Gen (ByteString, ByteString, ByteString)
    -> Gen [(ByteString, ByteString, ByteString)])
-> Gen (ByteString, ByteString, ByteString)
-> IO [(ByteString, ByteString, ByteString)]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Int
-> Gen (ByteString, ByteString, ByteString)
-> Gen [(ByteString, ByteString, ByteString)]
forall a. Int -> Gen a -> Gen [a]
vectorOf Int
n (Gen (ByteString, ByteString, ByteString)
 -> IO [(ByteString, ByteString, ByteString)])
-> Gen (ByteString, ByteString, ByteString)
-> IO [(ByteString, ByteString, ByteString)]
forall a b. (a -> b) -> a -> b
$ (,)
    (a -> Witness a -> (a, Witness a))
-> Gen a -> Gen (Witness a -> (a, Witness a))
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Arbitrary a => Gen a
arbitrary @a
    Gen (Witness a -> (a, Witness a))
-> Gen (Witness a) -> Gen (a, Witness a)
forall a b. Gen (a -> b) -> Gen a -> Gen b
forall (f :: Type -> Type) a b.
Applicative f =>
f (a -> b) -> f a -> f b
<*> forall a. Arbitrary a => Gen a
arbitrary @(Witness a)
    Gen (a, Witness a)
-> ((a, Witness a) -> Gen (ByteString, ByteString, ByteString))
-> Gen (ByteString, ByteString, ByteString)
forall a b. Gen a -> (a -> Gen b) -> Gen b
forall (m :: Type -> Type) a b. Monad m => m a -> (a -> m b) -> m b
>>= \(a
a, Witness a
w) -> do
        let s :: SetupProve a
s = forall a. NonInteractiveProof a => a -> SetupProve a
setupProve @a a
a
        let (Input a
i, Proof a
p) = forall a.
NonInteractiveProof a =>
SetupProve a -> Witness a -> (Input a, Proof a)
prove @a SetupProve a
s Witness a
w
        (ByteString, ByteString, ByteString)
-> Gen (ByteString, ByteString, ByteString)
forall a. a -> Gen a
forall (f :: Type -> Type) a. Applicative f => a -> f a
pure (SetupProve a -> ByteString
forall a. Binary a => a -> ByteString
toByteString SetupProve a
s, Input a -> ByteString
forall a. Binary a => a -> ByteString
toByteString Input a
i, Proof a -> ByteString
forall a. Binary a => a -> ByteString
toByteString Proof a
p)