{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.NonInteractiveProof.Testing where

import           Prelude

import           ZkFold.Base.Protocol.NonInteractiveProof.Internal

class (NonInteractiveProof a core, NonInteractiveProof b core) => CompatibleNonInteractiveProofs a b core where
    nipSetupTransform    :: SetupVerify a -> SetupVerify b
    nipInputTransform    :: Input a -> Input b
    nipProofTransform    :: Proof a -> Proof b

nipCompatibility :: forall a b core . CompatibleNonInteractiveProofs a b core
    => a -> Witness a -> Bool
nipCompatibility :: forall {k} a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
a -> Witness a -> Bool
nipCompatibility a
a Witness a
w =
    let (Input a
i, Proof a
p) = forall a (core :: k).
NonInteractiveProof a core =>
SetupProve a -> Witness a -> (Input a, Proof a)
forall {k} a (core :: k).
NonInteractiveProof a core =>
SetupProve a -> Witness a -> (Input a, Proof a)
prove @a @core (forall a (core :: k).
NonInteractiveProof a core =>
a -> SetupProve a
forall {k} a (core :: k).
NonInteractiveProof a core =>
a -> SetupProve a
setupProve @a @core a
a) Witness a
w
        s' :: SetupVerify b
s'     = forall a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
SetupVerify a -> SetupVerify b
forall {k} a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
SetupVerify a -> SetupVerify b
nipSetupTransform @a @b @core (forall a (core :: k).
NonInteractiveProof a core =>
a -> SetupVerify a
forall {k} a (core :: k).
NonInteractiveProof a core =>
a -> SetupVerify a
setupVerify @a @core a
a)
        i' :: Input b
i'     = forall a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
Input a -> Input b
forall {k} a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
Input a -> Input b
nipInputTransform @a @b @core Input a
i
        p' :: Proof b
p'     = forall a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
Proof a -> Proof b
forall {k} a b (core :: k).
CompatibleNonInteractiveProofs a b core =>
Proof a -> Proof b
nipProofTransform @a @b @core Proof a
p
    in forall a (core :: k).
NonInteractiveProof a core =>
SetupVerify a -> Input a -> Proof a -> Bool
forall {k} a (core :: k).
NonInteractiveProof a core =>
SetupVerify a -> Input a -> Proof a -> Bool
verify @b @core SetupVerify b
s' Input b
i' Proof b
p'

instance NonInteractiveProof a core => CompatibleNonInteractiveProofs a a core where
    nipSetupTransform :: SetupVerify a -> SetupVerify a
nipSetupTransform    = SetupVerify a -> SetupVerify a
forall a. a -> a
id
    nipInputTransform :: Input a -> Input a
nipInputTransform    = Input a -> Input a
forall a. a -> a
id
    nipProofTransform :: Proof a -> Proof a
nipProofTransform    = Proof a -> Proof a
forall a. a -> a
id