{-# 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)