{-# LANGUAGE AllowAmbiguousTypes #-}

module ZkFold.Base.Protocol.ARK.Protostar.Accumulator where

import           Prelude                         hiding (length)

import           ZkFold.Base.Algebra.Basic.Class

data AccumulatorInstance f c = AccumulatorInstance {
      forall f c. AccumulatorInstance f c -> f
accPublicInput :: f
    , forall f c. AccumulatorInstance f c -> [c]
accCommits     :: [c]
    , forall f c. AccumulatorInstance f c -> [f]
accChallenges  :: [f]
    , forall f c. AccumulatorInstance f c -> c
accError       :: c
    , forall f c. AccumulatorInstance f c -> f
accMu          :: f
}

newtype AccumulatorWitness m = AccumulatorWitness { forall m. AccumulatorWitness m -> [m]
accMessages :: [m] }

data Accumulator f c m = Accumulator (AccumulatorInstance f c) (AccumulatorWitness m)

data NARKInstance f c = NARKInstance {
      forall f c. NARKInstance f c -> f
narkPublicInput :: f
    , forall f c. NARKInstance f c -> [c]
narkCommits     :: [c]
}

newtype NARKWitness m = NARKWitness { forall m. NARKWitness m -> [m]
narkMessages :: [m] }

data NARKPair pi f c m = NARKPair (NARKInstance f c) (NARKWitness m)

toAccumulatorInstance :: (FiniteField f, AdditiveGroup c) => (f -> c -> f) -> NARKInstance f c -> AccumulatorInstance f c
toAccumulatorInstance :: forall f c.
(FiniteField f, AdditiveGroup c) =>
(f -> c -> f) -> NARKInstance f c -> AccumulatorInstance f c
toAccumulatorInstance f -> c -> f
oracle (NARKInstance f
i [c]
cs) =
      let r0 :: f
r0 = f -> c -> f
oracle f
i c
forall a. AdditiveMonoid a => a
zero
          f :: [f] -> c -> [f]
f acc :: [f]
acc@(f
r:[f]
_) c
c = f -> c -> f
oracle f
r c
c f -> [f] -> [f]
forall a. a -> [a] -> [a]
: [f]
acc
          f []        c
_ = [Char] -> [f]
forall a. HasCallStack => [Char] -> a
error [Char]
"Invalid accumulator instance"
          rs :: [f]
rs = [f] -> [f]
forall a. HasCallStack => [a] -> [a]
init ([f] -> [f]) -> [f] -> [f]
forall a b. (a -> b) -> a -> b
$ [f] -> [f]
forall a. [a] -> [a]
reverse ([f] -> [f]) -> [f] -> [f]
forall a b. (a -> b) -> a -> b
$ ([f] -> c -> [f]) -> [f] -> [c] -> [f]
forall b a. (b -> a -> b) -> b -> [a] -> b
forall (t :: Type -> Type) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl [f] -> c -> [f]
f [f
r0] [c]
cs
      in f -> [c] -> [f] -> c -> f -> AccumulatorInstance f c
forall f c. f -> [c] -> [f] -> c -> f -> AccumulatorInstance f c
AccumulatorInstance f
i [c]
cs [f]
rs c
forall a. AdditiveMonoid a => a
zero f
forall a. MultiplicativeMonoid a => a
one

toAccumulatorWitness :: NARKWitness m -> AccumulatorWitness m
toAccumulatorWitness :: forall m. NARKWitness m -> AccumulatorWitness m
toAccumulatorWitness (NARKWitness [m]
ms) = [m] -> AccumulatorWitness m
forall m. [m] -> AccumulatorWitness m
AccumulatorWitness [m]
ms

toAccumulator :: (FiniteField f, AdditiveGroup c) => (f -> c -> f) -> NARKPair pi f c m -> Accumulator f c m
toAccumulator :: forall {k} f c (pi :: k) m.
(FiniteField f, AdditiveGroup c) =>
(f -> c -> f) -> NARKPair pi f c m -> Accumulator f c m
toAccumulator f -> c -> f
oracle (NARKPair NARKInstance f c
i NARKWitness m
w) = AccumulatorInstance f c
-> AccumulatorWitness m -> Accumulator f c m
forall f c m.
AccumulatorInstance f c
-> AccumulatorWitness m -> Accumulator f c m
Accumulator ((f -> c -> f) -> NARKInstance f c -> AccumulatorInstance f c
forall f c.
(FiniteField f, AdditiveGroup c) =>
(f -> c -> f) -> NARKInstance f c -> AccumulatorInstance f c
toAccumulatorInstance f -> c -> f
oracle NARKInstance f c
i) (NARKWitness m -> AccumulatorWitness m
forall m. NARKWitness m -> AccumulatorWitness m
toAccumulatorWitness NARKWitness m
w)