{-# LANGUAGE DeriveAnyClass #-}

module ZkFold.Base.Protocol.IVC.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, zero)
import           ZkFold.Base.Data.Vector               (Vector)
import           ZkFold.Base.Protocol.IVC.FiatShamir   (FiatShamir)
import           ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..))

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

narkProof :: Ring f
    => FiatShamir k i p c [f] o f
    -> i f
    -> p f
    -> NARKProof k c f
narkProof :: forall f (k :: Natural) (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type) o.
Ring f =>
FiatShamir k i p c [f] o f -> i f -> p f -> NARKProof k c f
narkProof FiatShamir k i p c [f] o f
a i f
pi0 p f
w =
    let (Vector k [f]
narkWitness, Vector k (c f)
narkCommits) = Vector k ([f], c f) -> (Vector k [f], Vector k (c f))
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 ([f], c f) -> (Vector k [f], Vector k (c f)))
-> Vector k ([f], c f) -> (Vector k [f], Vector k (c f))
forall a b. (a -> b) -> a -> b
$ FiatShamir k i p c [f] o f
-> i f -> p f -> f -> Natural -> Vector k ([f], c f)
forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
SpecialSoundProtocol k i p m o f -> i f -> p f -> f -> Natural -> m
prover FiatShamir k i p c [f] o f
a i f
pi0 p f
w f
forall a. AdditiveMonoid a => a
zero Natural
0
    in NARKProof {Vector k (c f)
Vector k [f]
narkCommits :: Vector k (c f)
narkWitness :: Vector k [f]
narkWitness :: Vector k [f]
narkCommits :: Vector k (c f)
..}

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

narkInstanceProof :: Ring f
    => FiatShamir k i p c [f] o f
    -> i f
    -> p f
    -> NARKInstanceProof k i c f
narkInstanceProof :: forall f (k :: Natural) (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type) o.
Ring f =>
FiatShamir k i p c [f] o f
-> i f -> p f -> NARKInstanceProof k i c f
narkInstanceProof FiatShamir k i p c [f] o f
a i f
pi0 p f
w = i f -> NARKProof k c f -> NARKInstanceProof k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
i f -> NARKProof k c f -> NARKInstanceProof k i c f
NARKInstanceProof (FiatShamir k i p c [f] o f -> i f -> p f -> i f
forall (k :: Natural) (i :: Type -> Type) (p :: Type -> Type) m o
       f.
SpecialSoundProtocol k i p m o f -> i f -> p f -> i f
input FiatShamir k i p c [f] o f
a i f
pi0 p f
w) (FiatShamir k i p c [f] o f -> i f -> p f -> NARKProof k c f
forall f (k :: Natural) (i :: Type -> Type) (p :: Type -> Type)
       (c :: Type -> Type) o.
Ring f =>
FiatShamir k i p c [f] o f -> i f -> p f -> NARKProof k c f
narkProof FiatShamir k i p c [f] o f
a i f
pi0 p f
w)