{-# LANGUAGE AllowAmbiguousTypes  #-}
{-# LANGUAGE DeriveAnyClass       #-}
{-# LANGUAGE TemplateHaskell      #-}
{-# LANGUAGE TypeOperators        #-}
{-# LANGUAGE UndecidableInstances #-}

module ZkFold.Base.Protocol.IVC.Accumulator where

import           Control.DeepSeq                       (NFData (..))
import           Control.Lens                          ((^.))
import           Control.Lens.Combinators              (makeLenses)
import           Data.Distributive                     (Distributive (..))
import           Data.Functor.Rep                      (Representable (..), collectRep, distributeRep)
import           GHC.Generics
import           Prelude                               hiding (length, pi)

import           ZkFold.Base.Algebra.Basic.Class       (Ring, Scale, zero)
import           ZkFold.Base.Algebra.Basic.Number      (KnownNat, type (+), type (-))
import           ZkFold.Base.Data.Vector               (Vector)
import           ZkFold.Base.Protocol.IVC.AlgebraicMap (algebraicMap)
import           ZkFold.Base.Protocol.IVC.Commit       (HomomorphicCommit (..))
import           ZkFold.Base.Protocol.IVC.Oracle       (HashAlgorithm, RandomOracle)
import           ZkFold.Base.Protocol.IVC.Predicate    (Predicate)
import           ZkFold.Symbolic.Data.Class            (SymbolicData (..))

-- Page 19, Accumulator instance
data AccumulatorInstance k i c f
    = AccumulatorInstance
        { forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> i f
_pi :: i f             -- pi ∈ M^{l_in} in the paper
        , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> Vector k (c f)
_c  :: Vector k (c f)  -- [C_i] ∈ C^k in the paper
        , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> Vector (k - 1) f
_r  :: Vector (k-1) f  -- [r_i] ∈ F^{k-1} in the paper
        , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> c f
_e  :: c f             -- E ∈ C in the paper
        , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> f
_mu :: f               -- μ ∈ F in the paper
        }
    deriving (Int -> AccumulatorInstance k i c f -> ShowS
[AccumulatorInstance k i c f] -> ShowS
AccumulatorInstance k i c f -> String
(Int -> AccumulatorInstance k i c f -> ShowS)
-> (AccumulatorInstance k i c f -> String)
-> ([AccumulatorInstance k i c f] -> ShowS)
-> Show (AccumulatorInstance k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Int -> AccumulatorInstance k i c f -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[AccumulatorInstance k i c f] -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
AccumulatorInstance 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 -> AccumulatorInstance k i c f -> ShowS
showsPrec :: Int -> AccumulatorInstance k i c f -> ShowS
$cshow :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
AccumulatorInstance k i c f -> String
show :: AccumulatorInstance k i c f -> String
$cshowList :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[AccumulatorInstance k i c f] -> ShowS
showList :: [AccumulatorInstance k i c f] -> ShowS
Show, AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
(AccumulatorInstance k i c f
 -> AccumulatorInstance k i c f -> Bool)
-> (AccumulatorInstance k i c f
    -> AccumulatorInstance k i c f -> Bool)
-> Eq (AccumulatorInstance k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Eq f, Eq (i f), Eq (c f)) =>
AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Eq f, Eq (i f), Eq (c f)) =>
AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
== :: AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
$c/= :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Eq f, Eq (i f), Eq (c f)) =>
AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
/= :: AccumulatorInstance k i c f -> AccumulatorInstance k i c f -> Bool
Eq, (forall x.
 AccumulatorInstance k i c f -> Rep (AccumulatorInstance k i c f) x)
-> (forall x.
    Rep (AccumulatorInstance k i c f) x -> AccumulatorInstance k i c f)
-> Generic (AccumulatorInstance k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (AccumulatorInstance k i c f) x -> AccumulatorInstance k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
AccumulatorInstance k i c f -> Rep (AccumulatorInstance k i c f) x
forall x.
Rep (AccumulatorInstance k i c f) x -> AccumulatorInstance k i c f
forall x.
AccumulatorInstance k i c f -> Rep (AccumulatorInstance 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.
AccumulatorInstance k i c f -> Rep (AccumulatorInstance k i c f) x
from :: forall x.
AccumulatorInstance k i c f -> Rep (AccumulatorInstance k i c f) x
$cto :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (AccumulatorInstance k i c f) x -> AccumulatorInstance k i c f
to :: forall x.
Rep (AccumulatorInstance k i c f) x -> AccumulatorInstance k i c f
Generic, (forall a.
 AccumulatorInstance k i c a -> Rep1 (AccumulatorInstance k i c) a)
-> (forall a.
    Rep1 (AccumulatorInstance k i c) a -> AccumulatorInstance k i c a)
-> Generic1 (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
Rep1 (AccumulatorInstance k i c) a -> AccumulatorInstance k i c a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
AccumulatorInstance k i c a -> Rep1 (AccumulatorInstance k i c) a
forall a.
Rep1 (AccumulatorInstance k i c) a -> AccumulatorInstance k i c a
forall a.
AccumulatorInstance k i c a -> Rep1 (AccumulatorInstance k i c) a
forall k (f :: k -> Type).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
$cfrom1 :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
AccumulatorInstance k i c a -> Rep1 (AccumulatorInstance k i c) a
from1 :: forall a.
AccumulatorInstance k i c a -> Rep1 (AccumulatorInstance k i c) a
$cto1 :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
Rep1 (AccumulatorInstance k i c) a -> AccumulatorInstance k i c a
to1 :: forall a.
Rep1 (AccumulatorInstance k i c) a -> AccumulatorInstance k i c a
Generic1, AccumulatorInstance k i c f -> ()
(AccumulatorInstance k i c f -> ())
-> NFData (AccumulatorInstance k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(NFData f, NFData (i f), NFData (c f)) =>
AccumulatorInstance 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)) =>
AccumulatorInstance k i c f -> ()
rnf :: AccumulatorInstance k i c f -> ()
NFData, (forall a b.
 (a -> b)
 -> AccumulatorInstance k i c a -> AccumulatorInstance k i c b)
-> (forall a b.
    a -> AccumulatorInstance k i c b -> AccumulatorInstance k i c a)
-> Functor (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Functor i, Functor c) =>
a -> AccumulatorInstance k i c b -> AccumulatorInstance k i c a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Functor i, Functor c) =>
(a -> b)
-> AccumulatorInstance k i c a -> AccumulatorInstance k i c b
forall a b.
a -> AccumulatorInstance k i c b -> AccumulatorInstance k i c a
forall a b.
(a -> b)
-> AccumulatorInstance k i c a -> AccumulatorInstance k i c b
forall (f :: Type -> Type).
(forall a b. (a -> b) -> f a -> f b)
-> (forall a b. a -> f b -> f a) -> Functor f
$cfmap :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Functor i, Functor c) =>
(a -> b)
-> AccumulatorInstance k i c a -> AccumulatorInstance k i c b
fmap :: forall a b.
(a -> b)
-> AccumulatorInstance k i c a -> AccumulatorInstance k i c b
$c<$ :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Functor i, Functor c) =>
a -> AccumulatorInstance k i c b -> AccumulatorInstance k i c a
<$ :: forall a b.
a -> AccumulatorInstance k i c b -> AccumulatorInstance k i c a
Functor, (forall m. Monoid m => AccumulatorInstance k i c m -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> AccumulatorInstance k i c a -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> AccumulatorInstance k i c a -> m)
-> (forall a b.
    (a -> b -> b) -> b -> AccumulatorInstance k i c a -> b)
-> (forall a b.
    (a -> b -> b) -> b -> AccumulatorInstance k i c a -> b)
-> (forall b a.
    (b -> a -> b) -> b -> AccumulatorInstance k i c a -> b)
-> (forall b a.
    (b -> a -> b) -> b -> AccumulatorInstance k i c a -> b)
-> (forall a. (a -> a -> a) -> AccumulatorInstance k i c a -> a)
-> (forall a. (a -> a -> a) -> AccumulatorInstance k i c a -> a)
-> (forall a. AccumulatorInstance k i c a -> [a])
-> (forall a. AccumulatorInstance k i c a -> Bool)
-> (forall a. AccumulatorInstance k i c a -> Int)
-> (forall a. Eq a => a -> AccumulatorInstance k i c a -> Bool)
-> (forall a. Ord a => AccumulatorInstance k i c a -> a)
-> (forall a. Ord a => AccumulatorInstance k i c a -> a)
-> (forall a. Num a => AccumulatorInstance k i c a -> a)
-> (forall a. Num a => AccumulatorInstance k i c a -> a)
-> Foldable (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Eq a) =>
a -> AccumulatorInstance k i c a -> Bool
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Num a) =>
AccumulatorInstance k i c a -> a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Ord a) =>
AccumulatorInstance k i c a -> a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) m.
(Foldable i, Foldable c, Monoid m) =>
AccumulatorInstance k i c m -> m
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> Bool
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> Int
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> [a]
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
(a -> a -> a) -> AccumulatorInstance k i c a -> a
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) m a.
(Foldable i, Foldable c, Monoid m) =>
(a -> m) -> AccumulatorInstance k i c a -> m
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) b a.
(Foldable i, Foldable c) =>
(b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Foldable i, Foldable c) =>
(a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
forall a. Eq a => a -> AccumulatorInstance k i c a -> Bool
forall a. Num a => AccumulatorInstance k i c a -> a
forall a. Ord a => AccumulatorInstance k i c a -> a
forall m. Monoid m => AccumulatorInstance k i c m -> m
forall a. AccumulatorInstance k i c a -> Bool
forall a. AccumulatorInstance k i c a -> Int
forall a. AccumulatorInstance k i c a -> [a]
forall a. (a -> a -> a) -> AccumulatorInstance k i c a -> a
forall m a.
Monoid m =>
(a -> m) -> AccumulatorInstance k i c a -> m
forall b a. (b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
forall a b. (a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
forall (t :: Type -> Type).
(forall m. Monoid m => t m -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall m a. Monoid m => (a -> m) -> t a -> m)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall a b. (a -> b -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall b a. (b -> a -> b) -> b -> t a -> b)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. (a -> a -> a) -> t a -> a)
-> (forall a. t a -> [a])
-> (forall a. t a -> Bool)
-> (forall a. t a -> Int)
-> (forall a. Eq a => a -> t a -> Bool)
-> (forall a. Ord a => t a -> a)
-> (forall a. Ord a => t a -> a)
-> (forall a. Num a => t a -> a)
-> (forall a. Num a => t a -> a)
-> Foldable t
$cfold :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) m.
(Foldable i, Foldable c, Monoid m) =>
AccumulatorInstance k i c m -> m
fold :: forall m. Monoid m => AccumulatorInstance k i c m -> m
$cfoldMap :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) m a.
(Foldable i, Foldable c, Monoid m) =>
(a -> m) -> AccumulatorInstance k i c a -> m
foldMap :: forall m a.
Monoid m =>
(a -> m) -> AccumulatorInstance k i c a -> m
$cfoldMap' :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) m a.
(Foldable i, Foldable c, Monoid m) =>
(a -> m) -> AccumulatorInstance k i c a -> m
foldMap' :: forall m a.
Monoid m =>
(a -> m) -> AccumulatorInstance k i c a -> m
$cfoldr :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Foldable i, Foldable c) =>
(a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
foldr :: forall a b. (a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
$cfoldr' :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a b.
(Foldable i, Foldable c) =>
(a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> AccumulatorInstance k i c a -> b
$cfoldl :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) b a.
(Foldable i, Foldable c) =>
(b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
foldl :: forall b a. (b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
$cfoldl' :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) b a.
(Foldable i, Foldable c) =>
(b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> AccumulatorInstance k i c a -> b
$cfoldr1 :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
(a -> a -> a) -> AccumulatorInstance k i c a -> a
foldr1 :: forall a. (a -> a -> a) -> AccumulatorInstance k i c a -> a
$cfoldl1 :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
(a -> a -> a) -> AccumulatorInstance k i c a -> a
foldl1 :: forall a. (a -> a -> a) -> AccumulatorInstance k i c a -> a
$ctoList :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> [a]
toList :: forall a. AccumulatorInstance k i c a -> [a]
$cnull :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> Bool
null :: forall a. AccumulatorInstance k i c a -> Bool
$clength :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c) =>
AccumulatorInstance k i c a -> Int
length :: forall a. AccumulatorInstance k i c a -> Int
$celem :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Eq a) =>
a -> AccumulatorInstance k i c a -> Bool
elem :: forall a. Eq a => a -> AccumulatorInstance k i c a -> Bool
$cmaximum :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Ord a) =>
AccumulatorInstance k i c a -> a
maximum :: forall a. Ord a => AccumulatorInstance k i c a -> a
$cminimum :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Ord a) =>
AccumulatorInstance k i c a -> a
minimum :: forall a. Ord a => AccumulatorInstance k i c a -> a
$csum :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Num a) =>
AccumulatorInstance k i c a -> a
sum :: forall a. Num a => AccumulatorInstance k i c a -> a
$cproduct :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) a.
(Foldable i, Foldable c, Num a) =>
AccumulatorInstance k i c a -> a
product :: forall a. Num a => AccumulatorInstance k i c a -> a
Foldable, Functor (AccumulatorInstance k i c)
Foldable (AccumulatorInstance k i c)
(Functor (AccumulatorInstance k i c),
 Foldable (AccumulatorInstance k i c)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b)
 -> AccumulatorInstance k i c a -> f (AccumulatorInstance k i c b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    AccumulatorInstance k i c (f a) -> f (AccumulatorInstance k i c a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b)
    -> AccumulatorInstance k i c a -> m (AccumulatorInstance k i c b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    AccumulatorInstance k i c (m a) -> m (AccumulatorInstance k i c a))
-> Traversable (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type).
(Traversable i, Traversable c) =>
Functor (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type).
(Traversable i, Traversable c) =>
Foldable (AccumulatorInstance k i c)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (m :: Type -> Type) a.
(Traversable i, Traversable c, Monad m) =>
AccumulatorInstance k i c (m a) -> m (AccumulatorInstance k i c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (f :: Type -> Type) a.
(Traversable i, Traversable c, Applicative f) =>
AccumulatorInstance k i c (f a) -> f (AccumulatorInstance k i c a)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (m :: Type -> Type) a b.
(Traversable i, Traversable c, Monad m) =>
(a -> m b)
-> AccumulatorInstance k i c a -> m (AccumulatorInstance k i c b)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (f :: Type -> Type) a b.
(Traversable i, Traversable c, Applicative f) =>
(a -> f b)
-> AccumulatorInstance k i c a -> f (AccumulatorInstance k i c b)
forall (t :: Type -> Type).
(Functor t, Foldable t) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> t a -> f (t b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    t (f a) -> f (t a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> t a -> m (t b))
-> (forall (m :: Type -> Type) a. Monad m => t (m a) -> m (t a))
-> Traversable t
forall (m :: Type -> Type) a.
Monad m =>
AccumulatorInstance k i c (m a) -> m (AccumulatorInstance k i c a)
forall (f :: Type -> Type) a.
Applicative f =>
AccumulatorInstance k i c (f a) -> f (AccumulatorInstance k i c a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b)
-> AccumulatorInstance k i c a -> m (AccumulatorInstance k i c b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> AccumulatorInstance k i c a -> f (AccumulatorInstance k i c b)
$ctraverse :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (f :: Type -> Type) a b.
(Traversable i, Traversable c, Applicative f) =>
(a -> f b)
-> AccumulatorInstance k i c a -> f (AccumulatorInstance k i c b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b)
-> AccumulatorInstance k i c a -> f (AccumulatorInstance k i c b)
$csequenceA :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (f :: Type -> Type) a.
(Traversable i, Traversable c, Applicative f) =>
AccumulatorInstance k i c (f a) -> f (AccumulatorInstance k i c a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
AccumulatorInstance k i c (f a) -> f (AccumulatorInstance k i c a)
$cmapM :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (m :: Type -> Type) a b.
(Traversable i, Traversable c, Monad m) =>
(a -> m b)
-> AccumulatorInstance k i c a -> m (AccumulatorInstance k i c b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b)
-> AccumulatorInstance k i c a -> m (AccumulatorInstance k i c b)
$csequence :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type)
       (m :: Type -> Type) a.
(Traversable i, Traversable c, Monad m) =>
AccumulatorInstance k i c (m a) -> m (AccumulatorInstance k i c a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
AccumulatorInstance k i c (m a) -> m (AccumulatorInstance k i c a)
Traversable)

makeLenses ''AccumulatorInstance

instance (Representable i, Representable c, KnownNat k, KnownNat (k-1)) => Distributive (AccumulatorInstance k i c) where
    distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (AccumulatorInstance k i c a) -> AccumulatorInstance k i c (f a)
distribute = f (AccumulatorInstance k i c a) -> AccumulatorInstance k i c (f a)
forall (f :: Type -> Type) (w :: Type -> Type) a.
(Representable f, Functor w) =>
w (f a) -> f (w a)
distributeRep
    collect :: forall (f :: Type -> Type) a b.
Functor f =>
(a -> AccumulatorInstance k i c b)
-> f a -> AccumulatorInstance k i c (f b)
collect = (a -> AccumulatorInstance k i c b)
-> f a -> AccumulatorInstance k i c (f b)
forall (f :: Type -> Type) (w :: Type -> Type) a b.
(Representable f, Functor w) =>
(a -> f b) -> w a -> f (w b)
collectRep

instance (Representable i, Representable c, KnownNat k, KnownNat (k-1)) => Representable (AccumulatorInstance k i c)

instance (HashAlgorithm algo f, RandomOracle algo f f, RandomOracle algo (i f) f, RandomOracle algo (c f) f)
    => RandomOracle algo (AccumulatorInstance k i c f) f

instance
    ( KnownNat (k-1)
    , KnownNat k
    , SymbolicData f
    , SymbolicData (i f)
    , SymbolicData (c f)
    , Context f ~ Context (c f)
    , Context f ~ Context (i f)
    , Support f ~ Support (c f)
    , Support f ~ Support (i f)
    ) => SymbolicData (AccumulatorInstance k i c f)

-- Page 19, Accumulator
-- @acc.x@ (accumulator instance) from the paper corresponds to _x
-- @acc.w@ (accumulator witness) from the paper corresponds to _w
data Accumulator k i c f
    = Accumulator
        { forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
Accumulator k i c f -> AccumulatorInstance k i c f
_x :: AccumulatorInstance k i c f
        , forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
Accumulator k i c f -> Vector k [f]
_w :: Vector k [f]
        }
    deriving (Int -> Accumulator k i c f -> ShowS
[Accumulator k i c f] -> ShowS
Accumulator k i c f -> String
(Int -> Accumulator k i c f -> ShowS)
-> (Accumulator k i c f -> String)
-> ([Accumulator k i c f] -> ShowS)
-> Show (Accumulator k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Int -> Accumulator k i c f -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[Accumulator k i c f] -> ShowS
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Accumulator 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 -> Accumulator k i c f -> ShowS
showsPrec :: Int -> Accumulator k i c f -> ShowS
$cshow :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
Accumulator k i c f -> String
show :: Accumulator k i c f -> String
$cshowList :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(Show f, Show (i f), Show (c f)) =>
[Accumulator k i c f] -> ShowS
showList :: [Accumulator k i c f] -> ShowS
Show, (forall x. Accumulator k i c f -> Rep (Accumulator k i c f) x)
-> (forall x. Rep (Accumulator k i c f) x -> Accumulator k i c f)
-> Generic (Accumulator k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (Accumulator k i c f) x -> Accumulator k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Accumulator k i c f -> Rep (Accumulator k i c f) x
forall x. Rep (Accumulator k i c f) x -> Accumulator k i c f
forall x. Accumulator k i c f -> Rep (Accumulator 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.
Accumulator k i c f -> Rep (Accumulator k i c f) x
from :: forall x. Accumulator k i c f -> Rep (Accumulator k i c f) x
$cto :: forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f x.
Rep (Accumulator k i c f) x -> Accumulator k i c f
to :: forall x. Rep (Accumulator k i c f) x -> Accumulator k i c f
Generic, Accumulator k i c f -> ()
(Accumulator k i c f -> ()) -> NFData (Accumulator k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
(NFData f, NFData (i f), NFData (c f)) =>
Accumulator 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)) =>
Accumulator k i c f -> ()
rnf :: Accumulator k i c f -> ()
NFData)

makeLenses ''Accumulator

emptyAccumulator :: forall d k a i p c f .
    ( KnownNat (d+1)
    , KnownNat (k-1)
    , KnownNat k
    , Representable i
    , HomomorphicCommit [f] (c f)
    , Ring f
    , Scale a f
    ) => Predicate a i p -> Accumulator k i c f
emptyAccumulator :: forall (d :: Natural) (k :: Natural) a (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d + 1), KnownNat (k - 1), KnownNat k, Representable i,
 HomomorphicCommit [f] (c f), Ring f, Scale a f) =>
Predicate a i p -> Accumulator k i c f
emptyAccumulator Predicate a i p
phi =
    let accW :: Vector k [f]
accW  = (Rep (Vector k) -> [f]) -> Vector k [f]
forall a. (Rep (Vector k) -> a) -> Vector k a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate ([f] -> Rep (Vector k) -> [f]
forall a b. a -> b -> a
const [f]
forall a. AdditiveMonoid a => a
zero)
        aiC :: Vector k (c f)
aiC   = ([f] -> c f) -> Vector k [f] -> Vector k (c f)
forall a b. (a -> b) -> Vector k a -> Vector k b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap [f] -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit Vector k [f]
accW
        aiR :: Vector (k - 1) f
aiR   = (Rep (Vector (k - 1)) -> f) -> Vector (k - 1) f
forall a. (Rep (Vector (k - 1)) -> a) -> Vector (k - 1) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (f -> Rep (Vector (k - 1)) -> f
forall a b. a -> b -> a
const f
forall a. AdditiveMonoid a => a
zero)
        aiMu :: f
aiMu  = f
forall a. AdditiveMonoid a => a
zero
        aiPI :: i f
aiPI  = (Rep i -> f) -> i f
forall a. (Rep i -> a) -> i a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (f -> Rep i -> f
forall a b. a -> b -> a
const f
forall a. AdditiveMonoid a => a
zero)
        aiE :: c f
aiE   = [f] -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit ([f] -> c f) -> [f] -> c f
forall a b. (a -> b) -> a -> b
$ forall (d :: Natural) (k :: Natural) a (i :: Type -> Type)
       (p :: Type -> Type) f.
(KnownNat (d + 1), Representable i, Ring f, Scale a f) =>
Predicate a i p
-> i f -> Vector k [f] -> Vector (k - 1) f -> f -> [f]
algebraicMap @d Predicate a i p
phi i f
aiPI Vector k [f]
accW Vector (k - 1) f
aiR f
aiMu
        accX :: AccumulatorInstance k i c f
accX = AccumulatorInstance { _pi :: i f
_pi = i f
aiPI, _c :: Vector k (c f)
_c = Vector k (c f)
aiC, _r :: Vector (k - 1) f
_r = Vector (k - 1) f
aiR, _e :: c f
_e = c f
aiE, _mu :: f
_mu = f
aiMu }
    in AccumulatorInstance k i c f -> Vector k [f] -> Accumulator k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
AccumulatorInstance k i c f -> Vector k [f] -> Accumulator k i c f
Accumulator AccumulatorInstance k i c f
accX Vector k [f]
accW

emptyAccumulatorInstance :: forall d k a i p c f .
    ( KnownNat (d+1)
    , KnownNat (k-1)
    , KnownNat k
    , Representable i
    , HomomorphicCommit [f] (c f)
    , Ring f
    , Scale a f
    ) => Predicate a i p -> AccumulatorInstance k i c f
emptyAccumulatorInstance :: forall (d :: Natural) (k :: Natural) a (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d + 1), KnownNat (k - 1), KnownNat k, Representable i,
 HomomorphicCommit [f] (c f), Ring f, Scale a f) =>
Predicate a i p -> AccumulatorInstance k i c f
emptyAccumulatorInstance Predicate a i p
phi = forall (d :: Natural) (k :: Natural) a (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d + 1), KnownNat (k - 1), KnownNat k, Representable i,
 HomomorphicCommit [f] (c f), Ring f, Scale a f) =>
Predicate a i p -> Accumulator k i c f
emptyAccumulator @d Predicate a i p
phi Accumulator k i c f
-> Getting
     (AccumulatorInstance k i c f)
     (Accumulator k i c f)
     (AccumulatorInstance k i c f)
-> AccumulatorInstance k i c f
forall s a. s -> Getting a s a -> a
^. Getting
  (AccumulatorInstance k i c f)
  (Accumulator k i c f)
  (AccumulatorInstance k i c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f
       (i :: Type -> Type) (c :: Type -> Type) (f :: Type -> Type).
Functor f =>
(AccumulatorInstance k i c f -> f (AccumulatorInstance k i c f))
-> Accumulator k i c f -> f (Accumulator k i c f)
x