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

module ZkFold.Base.Protocol.Protostar.NARK where

import           Control.DeepSeq                             (NFData (..))
import           Data.Zip                                    (unzip)
import           GHC.Generics
import           Prelude                                     hiding (head, length, pi, unzip)

import           ZkFold.Base.Algebra.Basic.Class             (Ring)
import           ZkFold.Base.Algebra.Basic.Number            (KnownNat)
import           ZkFold.Base.Data.Vector                     (Vector)
import           ZkFold.Base.Protocol.Protostar.Commit       (HomomorphicCommit)
import           ZkFold.Base.Protocol.Protostar.CommitOpen   (CommitOpen (..))
import           ZkFold.Base.Protocol.Protostar.FiatShamir   (FiatShamir)
import           ZkFold.Base.Protocol.Protostar.Oracle       (RandomOracle (..))
import           ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..))

-- Page 18, section 3.4, The accumulation predicate
--
data NARKProof m c k
    = NARKProof
        { forall m c (k :: Natural). NARKProof m c k -> Vector k c
narkCommits :: Vector k c -- Commits [C_i] ∈  C^k
        , forall m c (k :: Natural). NARKProof m c k -> Vector k m
narkWitness :: Vector k m -- prover messages in the special-sound protocol [m_i]
        }
    deriving (Int -> NARKProof m c k -> ShowS
[NARKProof m c k] -> ShowS
NARKProof m c k -> String
(Int -> NARKProof m c k -> ShowS)
-> (NARKProof m c k -> String)
-> ([NARKProof m c k] -> ShowS)
-> Show (NARKProof m c k)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall m c (k :: Natural).
(Show c, Show m) =>
Int -> NARKProof m c k -> ShowS
forall m c (k :: Natural).
(Show c, Show m) =>
[NARKProof m c k] -> ShowS
forall m c (k :: Natural).
(Show c, Show m) =>
NARKProof m c k -> String
$cshowsPrec :: forall m c (k :: Natural).
(Show c, Show m) =>
Int -> NARKProof m c k -> ShowS
showsPrec :: Int -> NARKProof m c k -> ShowS
$cshow :: forall m c (k :: Natural).
(Show c, Show m) =>
NARKProof m c k -> String
show :: NARKProof m c k -> String
$cshowList :: forall m c (k :: Natural).
(Show c, Show m) =>
[NARKProof m c k] -> ShowS
showList :: [NARKProof m c k] -> ShowS
Show, (forall x. NARKProof m c k -> Rep (NARKProof m c k) x)
-> (forall x. Rep (NARKProof m c k) x -> NARKProof m c k)
-> Generic (NARKProof m c k)
forall x. Rep (NARKProof m c k) x -> NARKProof m c k
forall x. NARKProof m c k -> Rep (NARKProof m c k) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall m c (k :: Natural) x.
Rep (NARKProof m c k) x -> NARKProof m c k
forall m c (k :: Natural) x.
NARKProof m c k -> Rep (NARKProof m c k) x
$cfrom :: forall m c (k :: Natural) x.
NARKProof m c k -> Rep (NARKProof m c k) x
from :: forall x. NARKProof m c k -> Rep (NARKProof m c k) x
$cto :: forall m c (k :: Natural) x.
Rep (NARKProof m c k) x -> NARKProof m c k
to :: forall x. Rep (NARKProof m c k) x -> NARKProof m c k
Generic, NARKProof m c k -> ()
(NARKProof m c k -> ()) -> NFData (NARKProof m c k)
forall a. (a -> ()) -> NFData a
forall m c (k :: Natural).
(NFData c, NFData m) =>
NARKProof m c k -> ()
$crnf :: forall m c (k :: Natural).
(NFData c, NFData m) =>
NARKProof m c k -> ()
rnf :: NARKProof m c k -> ()
NFData)

narkProof :: forall f i p m c d k a .
    ( SpecialSoundProtocol f i p m c d k a
    , Ring f
    , HomomorphicCommit m c
    , RandomOracle (i f) f
    , RandomOracle c f
    , KnownNat k
    ) => FiatShamir (CommitOpen a) -> i f -> p f -> NARKProof m c k
narkProof :: forall {k1} f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k :: Natural) a.
(SpecialSoundProtocol f i p m c d k a, Ring f,
 HomomorphicCommit m c, RandomOracle (i f) f, RandomOracle c f,
 KnownNat k) =>
FiatShamir (CommitOpen a) -> i f -> p f -> NARKProof m c k
narkProof FiatShamir (CommitOpen a)
a i f
pi0 p f
w =
    let (Vector k m
ms, Vector k c
cs) = Vector k (m, c) -> (Vector k m, Vector k c)
forall a b. Vector k (a, b) -> (Vector k a, Vector k b)
forall (f :: Type -> Type) a b. Unzip f => f (a, b) -> (f a, f b)
unzip (Vector k (m, c) -> (Vector k m, Vector k c))
-> Vector k (m, c) -> (Vector k m, Vector k c)
forall a b. (a -> b) -> a -> b
$ forall {k} {k1} f (i :: Type -> Type) (p :: Type -> Type) m
       (c :: k) (d :: k1) (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> f -> Natural -> m
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> f -> Natural -> m
prover @f @i @_ @_ @c @d @1 FiatShamir (CommitOpen a)
a i f
pi0 p f
w (i f -> f
forall a b. RandomOracle a b => a -> b
oracle i f
pi0) Natural
0
    in Vector k c -> Vector k m -> NARKProof m c k
forall m c (k :: Natural).
Vector k c -> Vector k m -> NARKProof m c k
NARKProof Vector k c
cs Vector k m
ms

data NARKInstanceProof f i m c k = NARKInstanceProof (i f) (NARKProof m c k)
    deriving (Int -> NARKInstanceProof f i m c k -> ShowS
[NARKInstanceProof f i m c k] -> ShowS
NARKInstanceProof f i m c k -> String
(Int -> NARKInstanceProof f i m c k -> ShowS)
-> (NARKInstanceProof f i m c k -> String)
-> ([NARKInstanceProof f i m c k] -> ShowS)
-> Show (NARKInstanceProof f i m c k)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
Int -> NARKInstanceProof f i m c k -> ShowS
forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
[NARKInstanceProof f i m c k] -> ShowS
forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
NARKInstanceProof f i m c k -> String
$cshowsPrec :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
Int -> NARKInstanceProof f i m c k -> ShowS
showsPrec :: Int -> NARKInstanceProof f i m c k -> ShowS
$cshow :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
NARKInstanceProof f i m c k -> String
show :: NARKInstanceProof f i m c k -> String
$cshowList :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(Show c, Show m, Show (i f)) =>
[NARKInstanceProof f i m c k] -> ShowS
showList :: [NARKInstanceProof f i m c k] -> ShowS
Show, (forall x.
 NARKInstanceProof f i m c k -> Rep (NARKInstanceProof f i m c k) x)
-> (forall x.
    Rep (NARKInstanceProof f i m c k) x -> NARKInstanceProof f i m c k)
-> Generic (NARKInstanceProof f i m c k)
forall x.
Rep (NARKInstanceProof f i m c k) x -> NARKInstanceProof f i m c k
forall x.
NARKInstanceProof f i m c k -> Rep (NARKInstanceProof f i m c k) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall k (f :: k) (i :: k -> Type) m c (k :: Natural) x.
Rep (NARKInstanceProof f i m c k) x -> NARKInstanceProof f i m c k
forall k (f :: k) (i :: k -> Type) m c (k :: Natural) x.
NARKInstanceProof f i m c k -> Rep (NARKInstanceProof f i m c k) x
$cfrom :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural) x.
NARKInstanceProof f i m c k -> Rep (NARKInstanceProof f i m c k) x
from :: forall x.
NARKInstanceProof f i m c k -> Rep (NARKInstanceProof f i m c k) x
$cto :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural) x.
Rep (NARKInstanceProof f i m c k) x -> NARKInstanceProof f i m c k
to :: forall x.
Rep (NARKInstanceProof f i m c k) x -> NARKInstanceProof f i m c k
Generic, NARKInstanceProof f i m c k -> ()
(NARKInstanceProof f i m c k -> ())
-> NFData (NARKInstanceProof f i m c k)
forall a. (a -> ()) -> NFData a
forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(NFData c, NFData m, NFData (i f)) =>
NARKInstanceProof f i m c k -> ()
$crnf :: forall k (f :: k) (i :: k -> Type) m c (k :: Natural).
(NFData c, NFData m, NFData (i f)) =>
NARKInstanceProof f i m c k -> ()
rnf :: NARKInstanceProof f i m c k -> ()
NFData)

narkInstanceProof :: forall f i p m c d k a .
    ( SpecialSoundProtocol f i p m c d k a
    , Ring f
    , HomomorphicCommit m c
    , RandomOracle (i f) f
    , RandomOracle c f
    , KnownNat k
    ) => FiatShamir (CommitOpen a) -> i f -> p f -> NARKInstanceProof f i m c k
narkInstanceProof :: forall {k1} f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k :: Natural) a.
(SpecialSoundProtocol f i p m c d k a, Ring f,
 HomomorphicCommit m c, RandomOracle (i f) f, RandomOracle c f,
 KnownNat k) =>
FiatShamir (CommitOpen a)
-> i f -> p f -> NARKInstanceProof f i m c k
narkInstanceProof FiatShamir (CommitOpen a)
a i f
pi0 p f
w = i f -> NARKProof m c k -> NARKInstanceProof f i m c k
forall {k} (f :: k) (i :: k -> Type) m c (k :: Natural).
i f -> NARKProof m c k -> NARKInstanceProof f i m c k
NARKInstanceProof (forall {k} {k1} f (i :: Type -> Type) (p :: Type -> Type) m
       (c :: k) (d :: k1) (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> i f
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k2 :: Natural) a.
SpecialSoundProtocol f i p m c d k2 a =>
a -> i f -> p f -> i f
input @f @i @p @(Vector k (m, c)) @c @d @1 FiatShamir (CommitOpen a)
a i f
pi0 p f
w) (forall {k1} f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k :: Natural) a.
(SpecialSoundProtocol f i p m c d k a, Ring f,
 HomomorphicCommit m c, RandomOracle (i f) f, RandomOracle c f,
 KnownNat k) =>
FiatShamir (CommitOpen a) -> i f -> p f -> NARKProof m c k
forall f (i :: Type -> Type) (p :: Type -> Type) m c (d :: k1)
       (k :: Natural) a.
(SpecialSoundProtocol f i p m c d k a, Ring f,
 HomomorphicCommit m c, RandomOracle (i f) f, RandomOracle c f,
 KnownNat k) =>
FiatShamir (CommitOpen a) -> i f -> p f -> NARKProof m c k
narkProof @_ @_ @_ @_ @_ @d FiatShamir (CommitOpen a)
a i f
pi0 p f
w)