{-# 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)