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

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}

{-# HLINT ignore "Redundant ^." #-}

module ZkFold.Base.Protocol.IVC.RecursiveFunction where

import           Control.DeepSeq                            (NFData)
import           Data.Distributive                          (Distributive (..))
import           Data.Functor.Rep                           (Representable (..), collectRep, distributeRep)
import           Data.These                                 (These (..))
import           Data.Zip                                   (Semialign (..), Zip (..))
import           GHC.Generics                               (Generic, Generic1, U1 (..), (:*:) (..))
import           Prelude                                    (Foldable, Functor, Show, Traversable, fmap, type (~), ($),
                                                             (.), (<$>))

import           ZkFold.Base.Algebra.Basic.Class            (Scale, zero)
import           ZkFold.Base.Algebra.Basic.Number           (KnownNat, type (+), type (-))
import           ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec)
import           ZkFold.Base.Data.Orphans                   ()
import           ZkFold.Base.Data.Package                   (packed, unpacked)
import           ZkFold.Base.Data.Vector                    (Vector)
import           ZkFold.Base.Protocol.IVC.Accumulator       hiding (pi, x)
import           ZkFold.Base.Protocol.IVC.AccumulatorScheme (AccumulatorScheme (..), accumulatorScheme)
import           ZkFold.Base.Protocol.IVC.Commit            (HomomorphicCommit)
import           ZkFold.Base.Protocol.IVC.Oracle
import           ZkFold.Base.Protocol.IVC.Predicate         (Predicate (..), PredicateAssumptions, PredicateCircuit,
                                                             predicate)
import           ZkFold.Base.Protocol.IVC.StepFunction      (FunctorAssumptions, StepFunction, StepFunctionAssumptions)
import           ZkFold.Symbolic.Compiler                   (ArithmeticCircuit, compileWith, guessOutput, hlmap)
import           ZkFold.Symbolic.Data.Bool                  (Bool (..))
import           ZkFold.Symbolic.Data.Class                 (SymbolicData (..))
import           ZkFold.Symbolic.Data.Conditional           (bool)
import           ZkFold.Symbolic.Data.FieldElement          (FieldElement (FieldElement), fromFieldElement)
import           ZkFold.Symbolic.Data.Input                 (SymbolicInput)
import           ZkFold.Symbolic.Interpreter                (Interpreter (..))

-- | Public input to the recursive function
data RecursiveI i f = RecursiveI (i f) f
    deriving ((forall x. RecursiveI i f -> Rep (RecursiveI i f) x)
-> (forall x. Rep (RecursiveI i f) x -> RecursiveI i f)
-> Generic (RecursiveI i f)
forall x. Rep (RecursiveI i f) x -> RecursiveI i f
forall x. RecursiveI i f -> Rep (RecursiveI i f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall (i :: Type -> Type) f x.
Rep (RecursiveI i f) x -> RecursiveI i f
forall (i :: Type -> Type) f x.
RecursiveI i f -> Rep (RecursiveI i f) x
$cfrom :: forall (i :: Type -> Type) f x.
RecursiveI i f -> Rep (RecursiveI i f) x
from :: forall x. RecursiveI i f -> Rep (RecursiveI i f) x
$cto :: forall (i :: Type -> Type) f x.
Rep (RecursiveI i f) x -> RecursiveI i f
to :: forall x. Rep (RecursiveI i f) x -> RecursiveI i f
Generic, (forall a. RecursiveI i a -> Rep1 (RecursiveI i) a)
-> (forall a. Rep1 (RecursiveI i) a -> RecursiveI i a)
-> Generic1 (RecursiveI i)
forall a. Rep1 (RecursiveI i) a -> RecursiveI i a
forall a. RecursiveI i a -> Rep1 (RecursiveI i) a
forall k (f :: k -> Type).
(forall (a :: k). f a -> Rep1 f a)
-> (forall (a :: k). Rep1 f a -> f a) -> Generic1 f
forall (i :: Type -> Type) a.
Rep1 (RecursiveI i) a -> RecursiveI i a
forall (i :: Type -> Type) a.
RecursiveI i a -> Rep1 (RecursiveI i) a
$cfrom1 :: forall (i :: Type -> Type) a.
RecursiveI i a -> Rep1 (RecursiveI i) a
from1 :: forall a. RecursiveI i a -> Rep1 (RecursiveI i) a
$cto1 :: forall (i :: Type -> Type) a.
Rep1 (RecursiveI i) a -> RecursiveI i a
to1 :: forall a. Rep1 (RecursiveI i) a -> RecursiveI i a
Generic1, Int -> RecursiveI i f -> ShowS
[RecursiveI i f] -> ShowS
RecursiveI i f -> String
(Int -> RecursiveI i f -> ShowS)
-> (RecursiveI i f -> String)
-> ([RecursiveI i f] -> ShowS)
-> Show (RecursiveI i f)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
Int -> RecursiveI i f -> ShowS
forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
[RecursiveI i f] -> ShowS
forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
RecursiveI i f -> String
$cshowsPrec :: forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
Int -> RecursiveI i f -> ShowS
showsPrec :: Int -> RecursiveI i f -> ShowS
$cshow :: forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
RecursiveI i f -> String
show :: RecursiveI i f -> String
$cshowList :: forall (i :: Type -> Type) f.
(Show f, Show (i f)) =>
[RecursiveI i f] -> ShowS
showList :: [RecursiveI i f] -> ShowS
Show, RecursiveI i f -> ()
(RecursiveI i f -> ()) -> NFData (RecursiveI i f)
forall a. (a -> ()) -> NFData a
forall (i :: Type -> Type) f.
(NFData f, NFData (i f)) =>
RecursiveI i f -> ()
$crnf :: forall (i :: Type -> Type) f.
(NFData f, NFData (i f)) =>
RecursiveI i f -> ()
rnf :: RecursiveI i f -> ()
NFData, (forall a b. (a -> b) -> RecursiveI i a -> RecursiveI i b)
-> (forall a b. a -> RecursiveI i b -> RecursiveI i a)
-> Functor (RecursiveI i)
forall a b. a -> RecursiveI i b -> RecursiveI i a
forall a b. (a -> b) -> RecursiveI i a -> RecursiveI i b
forall (i :: Type -> Type) a b.
Functor i =>
a -> RecursiveI i b -> RecursiveI i a
forall (i :: Type -> Type) a b.
Functor i =>
(a -> b) -> RecursiveI i a -> RecursiveI i 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 (i :: Type -> Type) a b.
Functor i =>
(a -> b) -> RecursiveI i a -> RecursiveI i b
fmap :: forall a b. (a -> b) -> RecursiveI i a -> RecursiveI i b
$c<$ :: forall (i :: Type -> Type) a b.
Functor i =>
a -> RecursiveI i b -> RecursiveI i a
<$ :: forall a b. a -> RecursiveI i b -> RecursiveI i a
Functor, (forall m. Monoid m => RecursiveI i m -> m)
-> (forall m a. Monoid m => (a -> m) -> RecursiveI i a -> m)
-> (forall m a. Monoid m => (a -> m) -> RecursiveI i a -> m)
-> (forall a b. (a -> b -> b) -> b -> RecursiveI i a -> b)
-> (forall a b. (a -> b -> b) -> b -> RecursiveI i a -> b)
-> (forall b a. (b -> a -> b) -> b -> RecursiveI i a -> b)
-> (forall b a. (b -> a -> b) -> b -> RecursiveI i a -> b)
-> (forall a. (a -> a -> a) -> RecursiveI i a -> a)
-> (forall a. (a -> a -> a) -> RecursiveI i a -> a)
-> (forall a. RecursiveI i a -> [a])
-> (forall a. RecursiveI i a -> Bool)
-> (forall a. RecursiveI i a -> Int)
-> (forall a. Eq a => a -> RecursiveI i a -> Bool)
-> (forall a. Ord a => RecursiveI i a -> a)
-> (forall a. Ord a => RecursiveI i a -> a)
-> (forall a. Num a => RecursiveI i a -> a)
-> (forall a. Num a => RecursiveI i a -> a)
-> Foldable (RecursiveI i)
forall a. Eq a => a -> RecursiveI i a -> Bool
forall a. Num a => RecursiveI i a -> a
forall a. Ord a => RecursiveI i a -> a
forall m. Monoid m => RecursiveI i m -> m
forall a. RecursiveI i a -> Bool
forall a. RecursiveI i a -> Int
forall a. RecursiveI i a -> [a]
forall a. (a -> a -> a) -> RecursiveI i a -> a
forall m a. Monoid m => (a -> m) -> RecursiveI i a -> m
forall b a. (b -> a -> b) -> b -> RecursiveI i a -> b
forall a b. (a -> b -> b) -> b -> RecursiveI i a -> b
forall (i :: Type -> Type) a.
(Foldable i, Eq a) =>
a -> RecursiveI i a -> Bool
forall (i :: Type -> Type) a.
(Foldable i, Num a) =>
RecursiveI i a -> a
forall (i :: Type -> Type) a.
(Foldable i, Ord a) =>
RecursiveI i a -> a
forall (i :: Type -> Type) m.
(Foldable i, Monoid m) =>
RecursiveI i m -> m
forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> Bool
forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> Int
forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> [a]
forall (i :: Type -> Type) a.
Foldable i =>
(a -> a -> a) -> RecursiveI i a -> a
forall (i :: Type -> Type) m a.
(Foldable i, Monoid m) =>
(a -> m) -> RecursiveI i a -> m
forall (i :: Type -> Type) b a.
Foldable i =>
(b -> a -> b) -> b -> RecursiveI i a -> b
forall (i :: Type -> Type) a b.
Foldable i =>
(a -> b -> b) -> b -> RecursiveI i 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 (i :: Type -> Type) m.
(Foldable i, Monoid m) =>
RecursiveI i m -> m
fold :: forall m. Monoid m => RecursiveI i m -> m
$cfoldMap :: forall (i :: Type -> Type) m a.
(Foldable i, Monoid m) =>
(a -> m) -> RecursiveI i a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> RecursiveI i a -> m
$cfoldMap' :: forall (i :: Type -> Type) m a.
(Foldable i, Monoid m) =>
(a -> m) -> RecursiveI i a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> RecursiveI i a -> m
$cfoldr :: forall (i :: Type -> Type) a b.
Foldable i =>
(a -> b -> b) -> b -> RecursiveI i a -> b
foldr :: forall a b. (a -> b -> b) -> b -> RecursiveI i a -> b
$cfoldr' :: forall (i :: Type -> Type) a b.
Foldable i =>
(a -> b -> b) -> b -> RecursiveI i a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> RecursiveI i a -> b
$cfoldl :: forall (i :: Type -> Type) b a.
Foldable i =>
(b -> a -> b) -> b -> RecursiveI i a -> b
foldl :: forall b a. (b -> a -> b) -> b -> RecursiveI i a -> b
$cfoldl' :: forall (i :: Type -> Type) b a.
Foldable i =>
(b -> a -> b) -> b -> RecursiveI i a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> RecursiveI i a -> b
$cfoldr1 :: forall (i :: Type -> Type) a.
Foldable i =>
(a -> a -> a) -> RecursiveI i a -> a
foldr1 :: forall a. (a -> a -> a) -> RecursiveI i a -> a
$cfoldl1 :: forall (i :: Type -> Type) a.
Foldable i =>
(a -> a -> a) -> RecursiveI i a -> a
foldl1 :: forall a. (a -> a -> a) -> RecursiveI i a -> a
$ctoList :: forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> [a]
toList :: forall a. RecursiveI i a -> [a]
$cnull :: forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> Bool
null :: forall a. RecursiveI i a -> Bool
$clength :: forall (i :: Type -> Type) a. Foldable i => RecursiveI i a -> Int
length :: forall a. RecursiveI i a -> Int
$celem :: forall (i :: Type -> Type) a.
(Foldable i, Eq a) =>
a -> RecursiveI i a -> Bool
elem :: forall a. Eq a => a -> RecursiveI i a -> Bool
$cmaximum :: forall (i :: Type -> Type) a.
(Foldable i, Ord a) =>
RecursiveI i a -> a
maximum :: forall a. Ord a => RecursiveI i a -> a
$cminimum :: forall (i :: Type -> Type) a.
(Foldable i, Ord a) =>
RecursiveI i a -> a
minimum :: forall a. Ord a => RecursiveI i a -> a
$csum :: forall (i :: Type -> Type) a.
(Foldable i, Num a) =>
RecursiveI i a -> a
sum :: forall a. Num a => RecursiveI i a -> a
$cproduct :: forall (i :: Type -> Type) a.
(Foldable i, Num a) =>
RecursiveI i a -> a
product :: forall a. Num a => RecursiveI i a -> a
Foldable, Functor (RecursiveI i)
Foldable (RecursiveI i)
(Functor (RecursiveI i), Foldable (RecursiveI i)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> RecursiveI i a -> f (RecursiveI i b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    RecursiveI i (f a) -> f (RecursiveI i a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> RecursiveI i a -> m (RecursiveI i b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    RecursiveI i (m a) -> m (RecursiveI i a))
-> Traversable (RecursiveI i)
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 (i :: Type -> Type). Traversable i => Functor (RecursiveI i)
forall (i :: Type -> Type).
Traversable i =>
Foldable (RecursiveI i)
forall (i :: Type -> Type) (m :: Type -> Type) a.
(Traversable i, Monad m) =>
RecursiveI i (m a) -> m (RecursiveI i a)
forall (i :: Type -> Type) (f :: Type -> Type) a.
(Traversable i, Applicative f) =>
RecursiveI i (f a) -> f (RecursiveI i a)
forall (i :: Type -> Type) (m :: Type -> Type) a b.
(Traversable i, Monad m) =>
(a -> m b) -> RecursiveI i a -> m (RecursiveI i b)
forall (i :: Type -> Type) (f :: Type -> Type) a b.
(Traversable i, Applicative f) =>
(a -> f b) -> RecursiveI i a -> f (RecursiveI i b)
forall (m :: Type -> Type) a.
Monad m =>
RecursiveI i (m a) -> m (RecursiveI i a)
forall (f :: Type -> Type) a.
Applicative f =>
RecursiveI i (f a) -> f (RecursiveI i a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> RecursiveI i a -> m (RecursiveI i b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> RecursiveI i a -> f (RecursiveI i b)
$ctraverse :: forall (i :: Type -> Type) (f :: Type -> Type) a b.
(Traversable i, Applicative f) =>
(a -> f b) -> RecursiveI i a -> f (RecursiveI i b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> RecursiveI i a -> f (RecursiveI i b)
$csequenceA :: forall (i :: Type -> Type) (f :: Type -> Type) a.
(Traversable i, Applicative f) =>
RecursiveI i (f a) -> f (RecursiveI i a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
RecursiveI i (f a) -> f (RecursiveI i a)
$cmapM :: forall (i :: Type -> Type) (m :: Type -> Type) a b.
(Traversable i, Monad m) =>
(a -> m b) -> RecursiveI i a -> m (RecursiveI i b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> RecursiveI i a -> m (RecursiveI i b)
$csequence :: forall (i :: Type -> Type) (m :: Type -> Type) a.
(Traversable i, Monad m) =>
RecursiveI i (m a) -> m (RecursiveI i a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
RecursiveI i (m a) -> m (RecursiveI i a)
Traversable)

instance Semialign i => Semialign (RecursiveI i) where
    alignWith :: forall a b c.
(These a b -> c)
-> RecursiveI i a -> RecursiveI i b -> RecursiveI i c
alignWith These a b -> c
f (RecursiveI i a
x a
h) (RecursiveI i b
y b
h') = i c -> c -> RecursiveI i c
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI ((These a b -> c) -> i a -> i b -> i c
forall a b c. (These a b -> c) -> i a -> i b -> i c
forall (f :: Type -> Type) a b c.
Semialign f =>
(These a b -> c) -> f a -> f b -> f c
alignWith These a b -> c
f i a
x i b
y) (These a b -> c
f (a -> b -> These a b
forall a b. a -> b -> These a b
These a
h b
h'))

instance Zip i => Zip (RecursiveI i) where
    zipWith :: forall a b c.
(a -> b -> c) -> RecursiveI i a -> RecursiveI i b -> RecursiveI i c
zipWith a -> b -> c
f (RecursiveI i a
x a
h) (RecursiveI i b
y b
h') = i c -> c -> RecursiveI i c
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI ((a -> b -> c) -> i a -> i b -> i c
forall a b c. (a -> b -> c) -> i a -> i b -> i c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith a -> b -> c
f i a
x i b
y) (a -> b -> c
f a
h b
h')

instance Representable i => Distributive (RecursiveI i) where
    distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (RecursiveI i a) -> RecursiveI i (f a)
distribute = f (RecursiveI i a) -> RecursiveI i (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 -> RecursiveI i b) -> f a -> RecursiveI i (f b)
collect = (a -> RecursiveI i b) -> f a -> RecursiveI i (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 (RecursiveI i)

instance (HashAlgorithm algo f, RandomOracle algo f f, RandomOracle algo (i f) f) => RandomOracle algo (RecursiveI i f) f

instance (SymbolicData f, SymbolicData (i f), Context f ~ Context (i f), Support f ~ Support (i f)) => SymbolicData (RecursiveI i f)

instance (SymbolicInput f, SymbolicInput (i f), Context f ~ Context (i f)) => SymbolicInput (RecursiveI i f)

-- | Payload to the recursive function
data RecursiveP d k i p c f = RecursiveP (p f) (Vector k (c f)) (AccumulatorInstance k (RecursiveI i) c f) f (Vector (d-1) (c f))
    deriving ((forall x.
 RecursiveP d k i p c f -> Rep (RecursiveP d k i p c f) x)
-> (forall x.
    Rep (RecursiveP d k i p c f) x -> RecursiveP d k i p c f)
-> Generic (RecursiveP d k i p c f)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f x.
Rep (RecursiveP d k i p c f) x -> RecursiveP d k i p c f
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f x.
RecursiveP d k i p c f -> Rep (RecursiveP d k i p c f) x
forall x. Rep (RecursiveP d k i p c f) x -> RecursiveP d k i p c f
forall x. RecursiveP d k i p c f -> Rep (RecursiveP d k i p c f) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
$cfrom :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f x.
RecursiveP d k i p c f -> Rep (RecursiveP d k i p c f) x
from :: forall x. RecursiveP d k i p c f -> Rep (RecursiveP d k i p c f) x
$cto :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) f x.
Rep (RecursiveP d k i p c f) x -> RecursiveP d k i p c f
to :: forall x. Rep (RecursiveP d k i p c f) x -> RecursiveP d k i p c f
Generic, (forall a. RecursiveP d k i p c a -> Rep1 (RecursiveP d k i p c) a)
-> (forall a.
    Rep1 (RecursiveP d k i p c) a -> RecursiveP d k i p c a)
-> Generic1 (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
Rep1 (RecursiveP d k i p c) a -> RecursiveP d k i p c a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
RecursiveP d k i p c a -> Rep1 (RecursiveP d k i p c) a
forall a. Rep1 (RecursiveP d k i p c) a -> RecursiveP d k i p c a
forall a. RecursiveP d k i p c a -> Rep1 (RecursiveP d k i p 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 (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
RecursiveP d k i p c a -> Rep1 (RecursiveP d k i p c) a
from1 :: forall a. RecursiveP d k i p c a -> Rep1 (RecursiveP d k i p c) a
$cto1 :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
Rep1 (RecursiveP d k i p c) a -> RecursiveP d k i p c a
to1 :: forall a. Rep1 (RecursiveP d k i p c) a -> RecursiveP d k i p c a
Generic1, (forall a b.
 (a -> b) -> RecursiveP d k i p c a -> RecursiveP d k i p c b)
-> (forall a b.
    a -> RecursiveP d k i p c b -> RecursiveP d k i p c a)
-> Functor (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Functor p, Functor i, Functor c) =>
a -> RecursiveP d k i p c b -> RecursiveP d k i p c a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Functor p, Functor i, Functor c) =>
(a -> b) -> RecursiveP d k i p c a -> RecursiveP d k i p c b
forall a b. a -> RecursiveP d k i p c b -> RecursiveP d k i p c a
forall a b.
(a -> b) -> RecursiveP d k i p c a -> RecursiveP d k i p 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 (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Functor p, Functor i, Functor c) =>
(a -> b) -> RecursiveP d k i p c a -> RecursiveP d k i p c b
fmap :: forall a b.
(a -> b) -> RecursiveP d k i p c a -> RecursiveP d k i p c b
$c<$ :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Functor p, Functor i, Functor c) =>
a -> RecursiveP d k i p c b -> RecursiveP d k i p c a
<$ :: forall a b. a -> RecursiveP d k i p c b -> RecursiveP d k i p c a
Functor, (forall m. Monoid m => RecursiveP d k i p c m -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> RecursiveP d k i p c a -> m)
-> (forall m a.
    Monoid m =>
    (a -> m) -> RecursiveP d k i p c a -> m)
-> (forall a b. (a -> b -> b) -> b -> RecursiveP d k i p c a -> b)
-> (forall a b. (a -> b -> b) -> b -> RecursiveP d k i p c a -> b)
-> (forall b a. (b -> a -> b) -> b -> RecursiveP d k i p c a -> b)
-> (forall b a. (b -> a -> b) -> b -> RecursiveP d k i p c a -> b)
-> (forall a. (a -> a -> a) -> RecursiveP d k i p c a -> a)
-> (forall a. (a -> a -> a) -> RecursiveP d k i p c a -> a)
-> (forall a. RecursiveP d k i p c a -> [a])
-> (forall a. RecursiveP d k i p c a -> Bool)
-> (forall a. RecursiveP d k i p c a -> Int)
-> (forall a. Eq a => a -> RecursiveP d k i p c a -> Bool)
-> (forall a. Ord a => RecursiveP d k i p c a -> a)
-> (forall a. Ord a => RecursiveP d k i p c a -> a)
-> (forall a. Num a => RecursiveP d k i p c a -> a)
-> (forall a. Num a => RecursiveP d k i p c a -> a)
-> Foldable (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Eq a) =>
a -> RecursiveP d k i p c a -> Bool
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Num a) =>
RecursiveP d k i p c a -> a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Ord a) =>
RecursiveP d k i p c a -> a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m.
(Foldable p, Foldable i, Foldable c, Monoid m) =>
RecursiveP d k i p c m -> m
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> Bool
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> Int
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> [a]
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
(a -> a -> a) -> RecursiveP d k i p c a -> a
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m a.
(Foldable p, Foldable i, Foldable c, Monoid m) =>
(a -> m) -> RecursiveP d k i p c a -> m
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) b a.
(Foldable p, Foldable i, Foldable c) =>
(b -> a -> b) -> b -> RecursiveP d k i p c a -> b
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Foldable p, Foldable i, Foldable c) =>
(a -> b -> b) -> b -> RecursiveP d k i p c a -> b
forall a. Eq a => a -> RecursiveP d k i p c a -> Bool
forall a. Num a => RecursiveP d k i p c a -> a
forall a. Ord a => RecursiveP d k i p c a -> a
forall m. Monoid m => RecursiveP d k i p c m -> m
forall a. RecursiveP d k i p c a -> Bool
forall a. RecursiveP d k i p c a -> Int
forall a. RecursiveP d k i p c a -> [a]
forall a. (a -> a -> a) -> RecursiveP d k i p c a -> a
forall m a. Monoid m => (a -> m) -> RecursiveP d k i p c a -> m
forall b a. (b -> a -> b) -> b -> RecursiveP d k i p c a -> b
forall a b. (a -> b -> b) -> b -> RecursiveP d k i p 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 (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m.
(Foldable p, Foldable i, Foldable c, Monoid m) =>
RecursiveP d k i p c m -> m
fold :: forall m. Monoid m => RecursiveP d k i p c m -> m
$cfoldMap :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m a.
(Foldable p, Foldable i, Foldable c, Monoid m) =>
(a -> m) -> RecursiveP d k i p c a -> m
foldMap :: forall m a. Monoid m => (a -> m) -> RecursiveP d k i p c a -> m
$cfoldMap' :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) m a.
(Foldable p, Foldable i, Foldable c, Monoid m) =>
(a -> m) -> RecursiveP d k i p c a -> m
foldMap' :: forall m a. Monoid m => (a -> m) -> RecursiveP d k i p c a -> m
$cfoldr :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Foldable p, Foldable i, Foldable c) =>
(a -> b -> b) -> b -> RecursiveP d k i p c a -> b
foldr :: forall a b. (a -> b -> b) -> b -> RecursiveP d k i p c a -> b
$cfoldr' :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a b.
(Foldable p, Foldable i, Foldable c) =>
(a -> b -> b) -> b -> RecursiveP d k i p c a -> b
foldr' :: forall a b. (a -> b -> b) -> b -> RecursiveP d k i p c a -> b
$cfoldl :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) b a.
(Foldable p, Foldable i, Foldable c) =>
(b -> a -> b) -> b -> RecursiveP d k i p c a -> b
foldl :: forall b a. (b -> a -> b) -> b -> RecursiveP d k i p c a -> b
$cfoldl' :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) b a.
(Foldable p, Foldable i, Foldable c) =>
(b -> a -> b) -> b -> RecursiveP d k i p c a -> b
foldl' :: forall b a. (b -> a -> b) -> b -> RecursiveP d k i p c a -> b
$cfoldr1 :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
(a -> a -> a) -> RecursiveP d k i p c a -> a
foldr1 :: forall a. (a -> a -> a) -> RecursiveP d k i p c a -> a
$cfoldl1 :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
(a -> a -> a) -> RecursiveP d k i p c a -> a
foldl1 :: forall a. (a -> a -> a) -> RecursiveP d k i p c a -> a
$ctoList :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> [a]
toList :: forall a. RecursiveP d k i p c a -> [a]
$cnull :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> Bool
null :: forall a. RecursiveP d k i p c a -> Bool
$clength :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c) =>
RecursiveP d k i p c a -> Int
length :: forall a. RecursiveP d k i p c a -> Int
$celem :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Eq a) =>
a -> RecursiveP d k i p c a -> Bool
elem :: forall a. Eq a => a -> RecursiveP d k i p c a -> Bool
$cmaximum :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Ord a) =>
RecursiveP d k i p c a -> a
maximum :: forall a. Ord a => RecursiveP d k i p c a -> a
$cminimum :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Ord a) =>
RecursiveP d k i p c a -> a
minimum :: forall a. Ord a => RecursiveP d k i p c a -> a
$csum :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Num a) =>
RecursiveP d k i p c a -> a
sum :: forall a. Num a => RecursiveP d k i p c a -> a
$cproduct :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) a.
(Foldable p, Foldable i, Foldable c, Num a) =>
RecursiveP d k i p c a -> a
product :: forall a. Num a => RecursiveP d k i p c a -> a
Foldable, Functor (RecursiveP d k i p c)
Foldable (RecursiveP d k i p c)
(Functor (RecursiveP d k i p c),
 Foldable (RecursiveP d k i p c)) =>
(forall (f :: Type -> Type) a b.
 Applicative f =>
 (a -> f b) -> RecursiveP d k i p c a -> f (RecursiveP d k i p c b))
-> (forall (f :: Type -> Type) a.
    Applicative f =>
    RecursiveP d k i p c (f a) -> f (RecursiveP d k i p c a))
-> (forall (m :: Type -> Type) a b.
    Monad m =>
    (a -> m b) -> RecursiveP d k i p c a -> m (RecursiveP d k i p c b))
-> (forall (m :: Type -> Type) a.
    Monad m =>
    RecursiveP d k i p c (m a) -> m (RecursiveP d k i p c a))
-> Traversable (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type).
(Traversable p, Traversable i, Traversable c) =>
Functor (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type).
(Traversable p, Traversable i, Traversable c) =>
Foldable (RecursiveP d k i p c)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (m :: Type -> Type) a.
(Traversable p, Traversable i, Traversable c, Monad m) =>
RecursiveP d k i p c (m a) -> m (RecursiveP d k i p c a)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (f :: Type -> Type) a.
(Traversable p, Traversable i, Traversable c, Applicative f) =>
RecursiveP d k i p c (f a) -> f (RecursiveP d k i p c a)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (m :: Type -> Type) a b.
(Traversable p, Traversable i, Traversable c, Monad m) =>
(a -> m b) -> RecursiveP d k i p c a -> m (RecursiveP d k i p c b)
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (f :: Type -> Type) a b.
(Traversable p, Traversable i, Traversable c, Applicative f) =>
(a -> f b) -> RecursiveP d k i p c a -> f (RecursiveP d k i p 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 =>
RecursiveP d k i p c (m a) -> m (RecursiveP d k i p c a)
forall (f :: Type -> Type) a.
Applicative f =>
RecursiveP d k i p c (f a) -> f (RecursiveP d k i p c a)
forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> RecursiveP d k i p c a -> m (RecursiveP d k i p c b)
forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> RecursiveP d k i p c a -> f (RecursiveP d k i p c b)
$ctraverse :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (f :: Type -> Type) a b.
(Traversable p, Traversable i, Traversable c, Applicative f) =>
(a -> f b) -> RecursiveP d k i p c a -> f (RecursiveP d k i p c b)
traverse :: forall (f :: Type -> Type) a b.
Applicative f =>
(a -> f b) -> RecursiveP d k i p c a -> f (RecursiveP d k i p c b)
$csequenceA :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (f :: Type -> Type) a.
(Traversable p, Traversable i, Traversable c, Applicative f) =>
RecursiveP d k i p c (f a) -> f (RecursiveP d k i p c a)
sequenceA :: forall (f :: Type -> Type) a.
Applicative f =>
RecursiveP d k i p c (f a) -> f (RecursiveP d k i p c a)
$cmapM :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (m :: Type -> Type) a b.
(Traversable p, Traversable i, Traversable c, Monad m) =>
(a -> m b) -> RecursiveP d k i p c a -> m (RecursiveP d k i p c b)
mapM :: forall (m :: Type -> Type) a b.
Monad m =>
(a -> m b) -> RecursiveP d k i p c a -> m (RecursiveP d k i p c b)
$csequence :: forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (p :: Type -> Type) (c :: Type -> Type) (m :: Type -> Type) a.
(Traversable p, Traversable i, Traversable c, Monad m) =>
RecursiveP d k i p c (m a) -> m (RecursiveP d k i p c a)
sequence :: forall (m :: Type -> Type) a.
Monad m =>
RecursiveP d k i p c (m a) -> m (RecursiveP d k i p c a)
Traversable)

instance (KnownNat (d-1), KnownNat (k-1), KnownNat k, Representable i, Representable p, Representable c) => Distributive (RecursiveP d k i p c) where
    distribute :: forall (f :: Type -> Type) a.
Functor f =>
f (RecursiveP d k i p c a) -> RecursiveP d k i p c (f a)
distribute = f (RecursiveP d k i p c a) -> RecursiveP d k i p 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 -> RecursiveP d k i p c b) -> f a -> RecursiveP d k i p c (f b)
collect = (a -> RecursiveP d k i p c b) -> f a -> RecursiveP d k i p 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 (KnownNat (d-1), KnownNat (k-1), KnownNat k, Representable i, Representable p, Representable c) => Representable (RecursiveP d k i p c)

type RecursiveFunctionAssumptions algo d a i c f ctx =
    ( StepFunctionAssumptions a f ctx
    , HashAlgorithm algo f
    , RandomOracle algo f f
    , RandomOracle algo (i f) f
    , RandomOracle algo (c f) f
    , HomomorphicCommit [f] (c f)
    , Scale a f
    , Scale a (PolyVec f (d+1))
    , Scale f (c f)
    )

type RecursiveFunction algo d k a i p c = forall f ctx . RecursiveFunctionAssumptions algo d a i c f ctx
    => RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f

-- | Transform a step function into a recursive function
recursiveFunction :: forall algo d k a i p c .
    ( PredicateAssumptions a i p
    , FunctorAssumptions c
    , KnownNat (d-1)
    , KnownNat (d+1)
    , KnownNat (k-1)
    , KnownNat k
    , Zip i
    ) => StepFunction a i p -> RecursiveFunction algo d k a i p c
recursiveFunction :: forall {k} (algo :: k) (d :: Natural) (k :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type).
(PredicateAssumptions a i p, FunctorAssumptions c,
 KnownNat (d - 1), KnownNat (d + 1), KnownNat (k - 1), KnownNat k,
 Zip i) =>
StepFunction a i p -> RecursiveFunction algo d k a i p c
recursiveFunction StepFunction a i p
func =
    let
        -- A helper function to derive the accumulator scheme
        func' :: forall ctx f . StepFunctionAssumptions a f ctx => RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
        func' :: forall (ctx :: (Type -> Type) -> Type) f.
StepFunctionAssumptions a f ctx =>
RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
func' (RecursiveI i f
x f
h) (RecursiveP p f
u Vector k (c f)
_ AccumulatorInstance k (RecursiveI i) c f
_ f
_ Vector (d - 1) (c f)
_) = i f -> f -> RecursiveI i f
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI (i f -> p f -> i f
StepFunction a i p
func i f
x p f
u) f
h

        -- A helper predicate to derive the accumulator scheme
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
        pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec = StepFunction a (RecursiveI i) (RecursiveP d k i p c)
-> Predicate a (RecursiveI i) (RecursiveP d k i p c)
forall a (i :: Type -> Type) (p :: Type -> Type).
PredicateAssumptions a i p =>
StepFunction a i p -> Predicate a i p
predicate RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
StepFunction a (RecursiveI i) (RecursiveP d k i p c)
forall (ctx :: (Type -> Type) -> Type) f.
StepFunctionAssumptions a f ctx =>
RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
func'

        funcRecursive :: forall ctx f . RecursiveFunctionAssumptions algo d a i c f ctx
            => RecursiveI i f
            -> RecursiveP d k i p c f
            -> RecursiveI i f
        funcRecursive :: forall (ctx :: (Type -> Type) -> Type) f.
RecursiveFunctionAssumptions algo d a i c f ctx =>
RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
funcRecursive z :: RecursiveI i f
z@(RecursiveI i f
x f
_) (RecursiveP p f
u Vector k (c f)
piX AccumulatorInstance k (RecursiveI i) c f
accX f
flag Vector (d - 1) (c f)
pf) =
            let
                accScheme :: AccumulatorScheme d k (RecursiveI i) c f
                accScheme :: AccumulatorScheme d k (RecursiveI i) c f
accScheme = forall (algo :: k) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
forall {k1} (algo :: k1) (d :: Natural) (k2 :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type) f.
(KnownNat (d - 1), KnownNat (d + 1), Representable i, Zip i,
 HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (i f) f, RandomOracle algo (c f) f,
 HomomorphicCommit [f] (c f), Field f, Scale a f,
 Scale a (PolyVec f (d + 1)), Scale f (c f)) =>
Predicate a i p -> AccumulatorScheme d k2 i c f
accumulatorScheme @algo Predicate a (RecursiveI i) (RecursiveP d k i p c)
pRec

                x' :: i f
                x' :: i f
x' = i f -> p f -> i f
StepFunction a i p
func i f
x p f
u

                accX' :: AccumulatorInstance k (RecursiveI i) c f
                accX' :: AccumulatorInstance k (RecursiveI i) c f
accX' = AccumulatorScheme d k (RecursiveI i) c f
-> RecursiveI i f
-> Vector k (c f)
-> AccumulatorInstance k (RecursiveI i) c f
-> Vector (d - 1) (c f)
-> AccumulatorInstance k (RecursiveI i) c f
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
AccumulatorScheme d k i c f
-> i f
-> Vector k (c f)
-> AccumulatorInstance k i c f
-> Vector (d - 1) (c f)
-> AccumulatorInstance k i c f
verifier AccumulatorScheme d k (RecursiveI i) c f
accScheme RecursiveI i f
z Vector k (c f)
piX AccumulatorInstance k (RecursiveI i) c f
accX Vector (d - 1) (c f)
pf

                h :: f
                h :: f
h = f -> f -> Bool ctx -> f
forall b a. Conditional b a => a -> a -> b -> a
bool f
forall a. AdditiveMonoid a => a
zero (forall (algo :: k) x a. RandomOracle algo x a => x -> a
forall {k} (algo :: k) x a. RandomOracle algo x a => x -> a
oracle @algo AccumulatorInstance k (RecursiveI i) c f
accX') (Bool ctx -> f) -> Bool ctx -> f
forall a b. (a -> b) -> a -> b
$ ctx Par1 -> Bool ctx
forall (c :: (Type -> Type) -> Type). c Par1 -> Bool c
Bool (ctx Par1 -> Bool ctx) -> ctx Par1 -> Bool ctx
forall a b. (a -> b) -> a -> b
$ FieldElement ctx -> ctx Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement f
FieldElement ctx
flag
            in
                i f -> f -> RecursiveI i f
forall (i :: Type -> Type) f. i f -> f -> RecursiveI i f
RecursiveI i f
x' f
h

    in RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
forall (ctx :: (Type -> Type) -> Type) f.
RecursiveFunctionAssumptions algo d a i c f ctx =>
RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f
funcRecursive

--------------------------------------------------------------------------------

type RecursivePredicateAssumptions algo d k a i p c =
    ( KnownNat (d-1)
    , KnownNat (k-1)
    , KnownNat k
    , PredicateAssumptions a i p
    , FunctorAssumptions c
    )

recursivePredicate :: forall algo d k a i p c ctx0 ctx1 .
    ( RecursivePredicateAssumptions algo d k a i p c
    , ctx0 ~ Interpreter a
    , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0
    , ctx1 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1
    , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx1) ctx1
    ) => RecursiveFunction algo d k a i p c -> Predicate a (RecursiveI i) (RecursiveP d k i p c)
recursivePredicate :: forall {k} (algo :: k) (d :: Natural) (k :: Natural) a
       (i :: Type -> Type) (p :: Type -> Type) (c :: Type -> Type)
       (ctx0 :: (Type -> Type) -> Type) (ctx1 :: (Type -> Type) -> Type).
(RecursivePredicateAssumptions algo d k a i p c,
 ctx0 ~ Interpreter a,
 RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0,
 ctx1
 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1,
 RecursiveFunctionAssumptions
   algo d a i c (FieldElement ctx1) ctx1) =>
RecursiveFunction algo d k a i p c
-> Predicate a (RecursiveI i) (RecursiveP d k i p c)
recursivePredicate RecursiveFunction algo d k a i p c
func =
    let
        func' :: forall f ctx . RecursiveFunctionAssumptions algo d a i c f ctx
            => ctx (RecursiveI i) -> ctx (RecursiveP d k i p c) -> ctx (RecursiveI i)
        func' :: forall f (ctx :: (Type -> Type) -> Type).
RecursiveFunctionAssumptions algo d a i c f ctx =>
ctx (RecursiveI i)
-> ctx (RecursiveP d k i p c) -> ctx (RecursiveI i)
func' ctx (RecursiveI i)
x' ctx (RecursiveP d k i p c)
u' =
            let
                x :: RecursiveI i (FieldElement ctx)
x = ctx Par1 -> FieldElement ctx
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (ctx Par1 -> FieldElement ctx)
-> RecursiveI i (ctx Par1) -> RecursiveI i (FieldElement ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx (RecursiveI i) -> RecursiveI i (ctx Par1)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Package c, Functor f) =>
c f -> f (c Par1)
unpacked ctx (RecursiveI i)
x'
                u :: RecursiveP d k i p c (FieldElement ctx)
u = ctx Par1 -> FieldElement ctx
forall (c :: (Type -> Type) -> Type). c Par1 -> FieldElement c
FieldElement (ctx Par1 -> FieldElement ctx)
-> RecursiveP d k i p c (ctx Par1)
-> RecursiveP d k i p c (FieldElement ctx)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> ctx (RecursiveP d k i p c) -> RecursiveP d k i p c (ctx Par1)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Package c, Functor f) =>
c f -> f (c Par1)
unpacked ctx (RecursiveP d k i p c)
u'
            in
                RecursiveI i (ctx Par1) -> ctx (RecursiveI i)
forall (c :: (Type -> Type) -> Type) (f :: Type -> Type).
(Package c, Foldable f, Functor f) =>
f (c Par1) -> c f
packed (RecursiveI i (ctx Par1) -> ctx (RecursiveI i))
-> (RecursiveI i (FieldElement ctx) -> RecursiveI i (ctx Par1))
-> RecursiveI i (FieldElement ctx)
-> ctx (RecursiveI i)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (FieldElement ctx -> ctx Par1)
-> RecursiveI i (FieldElement ctx) -> RecursiveI i (ctx Par1)
forall a b. (a -> b) -> RecursiveI i a -> RecursiveI i b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap FieldElement ctx -> ctx Par1
forall (c :: (Type -> Type) -> Type). FieldElement c -> c Par1
fromFieldElement (RecursiveI i (FieldElement ctx) -> ctx (RecursiveI i))
-> RecursiveI i (FieldElement ctx) -> ctx (RecursiveI i)
forall a b. (a -> b) -> a -> b
$ RecursiveI i (FieldElement ctx)
-> RecursiveP d k i p c (FieldElement ctx)
-> RecursiveI i (FieldElement ctx)
RecursiveFunction algo d k a i p c
func RecursiveI i (FieldElement ctx)
x RecursiveP d k i p c (FieldElement ctx)
u

        predicateEval :: (RecursiveI i) a -> (RecursiveP d k i p c) a -> (RecursiveI i) a
        predicateEval :: RecursiveI i a -> RecursiveP d k i p c a -> RecursiveI i a
predicateEval RecursiveI i a
z RecursiveP d k i p c a
u = Interpreter a (RecursiveI i) -> RecursiveI i a
forall {k} (a :: k) (f :: k -> Type). Interpreter a f -> f a
runInterpreter (Interpreter a (RecursiveI i) -> RecursiveI i a)
-> Interpreter a (RecursiveI i) -> RecursiveI i a
forall a b. (a -> b) -> a -> b
$ Interpreter a (RecursiveI i)
-> Interpreter a (RecursiveP d k i p c)
-> Interpreter a (RecursiveI i)
forall f (ctx :: (Type -> Type) -> Type).
RecursiveFunctionAssumptions algo d a i c f ctx =>
ctx (RecursiveI i)
-> ctx (RecursiveP d k i p c) -> ctx (RecursiveI i)
func' (RecursiveI i a -> Interpreter a (RecursiveI i)
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter RecursiveI i a
z) (RecursiveP d k i p c a -> Interpreter a (RecursiveP d k i p c)
forall {k} (a :: k) (f :: k -> Type). f a -> Interpreter a f
Interpreter RecursiveP d k i p c a
u)

        predicateCircuit :: PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
        predicateCircuit :: PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
predicateCircuit =
            (forall x. RecursiveI i x -> (:*:) U1 (RecursiveI i) x)
-> ArithmeticCircuit
     a (RecursiveI i :*: RecursiveP d k i p c) (U1 :*: RecursiveI i) U1
-> PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
forall (i :: Type -> Type) (j :: Type -> Type) (o :: Type -> Type)
       a (p :: Type -> Type).
(Representable i, Representable j, Ord (Rep j), Functor o) =>
(forall x. j x -> i x)
-> ArithmeticCircuit a p i o -> ArithmeticCircuit a p j o
hlmap (U1 x
forall k (p :: k). U1 p
U1 U1 x -> RecursiveI i x -> (:*:) U1 (RecursiveI i) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*:) (ArithmeticCircuit
   a (RecursiveI i :*: RecursiveP d k i p c) (U1 :*: RecursiveI i) U1
 -> PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c))
-> ArithmeticCircuit
     a (RecursiveI i :*: RecursiveP d k i p c) (U1 :*: RecursiveI i) U1
-> PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
forall a b. (a -> b) -> a -> b
$
            forall a y (p :: Type -> Type) (i :: Type -> Type)
       (q :: Type -> Type) (j :: Type -> Type) s f
       (c0 :: (Type -> Type) -> Type) (c1 :: (Type -> Type) -> Type).
(CompilesWith c0 s f, c0 ~ ArithmeticCircuit a p i,
 Representable p, Representable i, RestoresFrom c1 y,
 c1 ~ ArithmeticCircuit a q j, Binary a, Binary (Rep p),
 Binary (Rep i), Binary (Rep j), Ord (Rep i), Ord (Rep j),
 Binary (Rep q)) =>
(c0 (Layout f) -> c1 (Layout y))
-> (forall x. p x -> i x -> (Payload s x, Layout s x)) -> f -> y
compileWith @a ArithmeticCircuit
  a
  (RecursiveI i :*: RecursiveP d k i p c)
  U1
  (Layout
     (ArithmeticCircuit
        a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveI i)
      -> ArithmeticCircuit
           a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveP d k i p c)
      -> ArithmeticCircuit
           a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveI i)))
-> ArithmeticCircuit
     a
     (RecursiveI i :*: RecursiveP d k i p c)
     (U1 :*: RecursiveI i)
     (Layout
        (ArithmeticCircuit
           a
           (RecursiveI i :*: RecursiveP d k i p c)
           (U1 :*: RecursiveI i)
           U1))
ArithmeticCircuit
  a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveI i)
-> ArithmeticCircuit
     a (RecursiveI i :*: RecursiveP d k i p c) (U1 :*: RecursiveI i) U1
forall a (p :: Type -> Type) (i :: Type -> Type)
       (o :: Type -> Type).
(Arithmetic a, Binary a, Binary (Rep p), Binary (Rep i),
 Binary (Rep o), Ord (Rep i), Ord (Rep o), NFData (Rep i),
 NFData (Rep o), Representable i, Representable o, Foldable o) =>
ArithmeticCircuit a p i o -> ArithmeticCircuit a p (i :*: o) U1
guessOutput (\(RecursiveI i x
i :*: RecursiveP d k i p c x
p) U1 x
U1 -> (U1 x
forall k (p :: k). U1 p
U1 U1 x -> (:*:) U1 U1 x -> (:*:) U1 (U1 :*: U1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 x
forall k (p :: k). U1 p
U1 U1 x -> U1 x -> (:*:) U1 U1 x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 x
forall k (p :: k). U1 p
U1, RecursiveI i x
i RecursiveI i x
-> (:*:) (RecursiveP d k i p c) U1 x
-> (:*:) (RecursiveI i) (RecursiveP d k i p c :*: U1) x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: RecursiveP d k i p c x
p RecursiveP d k i p c x -> U1 x -> (:*:) (RecursiveP d k i p c) U1 x
forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
f p -> g p -> (:*:) f g p
:*: U1 x
forall k (p :: k). U1 p
U1)) ArithmeticCircuit
  a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveI i)
-> ArithmeticCircuit
     a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveP d k i p c)
-> ArithmeticCircuit
     a (RecursiveI i :*: RecursiveP d k i p c) U1 (RecursiveI i)
forall f (ctx :: (Type -> Type) -> Type).
RecursiveFunctionAssumptions algo d a i c f ctx =>
ctx (RecursiveI i)
-> ctx (RecursiveP d k i p c) -> ctx (RecursiveI i)
func'
    in Predicate {PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
RecursiveI i a -> RecursiveP d k i p c a -> RecursiveI i a
predicateEval :: RecursiveI i a -> RecursiveP d k i p c a -> RecursiveI i a
predicateCircuit :: PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
predicateEval :: RecursiveI i a -> RecursiveP d k i p c a -> RecursiveI i a
predicateCircuit :: PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c)
..}