{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeOperators       #-}

{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# HLINT ignore "Redundant ^." #-}

module ZkFold.Base.Protocol.IVC.AccumulatorScheme where

import           Control.Lens                               ((^.))
import           Data.Constraint                            (withDict)
import           Data.Constraint.Nat                        (plusMinusInverse1)
import           Data.Functor.Rep                           (Representable (..))
import           Data.Zip                                   (Zip (..))
import           GHC.IsList                                 (IsList (..))
import           Prelude                                    (fmap, ($), (.), (<$>))
import qualified Prelude                                    as P

import           ZkFold.Base.Algebra.Basic.Class
import           ZkFold.Base.Algebra.Basic.Number
import qualified ZkFold.Base.Algebra.Polynomials.Univariate as PU
import           ZkFold.Base.Data.Vector                    (Vector, init, mapWithIx, tail, unsafeToVector)
import           ZkFold.Base.Protocol.IVC.Accumulator
import           ZkFold.Base.Protocol.IVC.AlgebraicMap      (algebraicMap)
import           ZkFold.Base.Protocol.IVC.Commit            (HomomorphicCommit (..))
import           ZkFold.Base.Protocol.IVC.FiatShamir        (transcript)
import           ZkFold.Base.Protocol.IVC.NARK              (NARKInstanceProof (..), NARKProof (..))
import           ZkFold.Base.Protocol.IVC.Oracle            (HashAlgorithm, RandomOracle (..))
import           ZkFold.Base.Protocol.IVC.Predicate         (Predicate)

-- | Accumulator scheme for V_NARK as described in Chapter 3.4 of the Protostar paper
data AccumulatorScheme d k i c f = AccumulatorScheme
  {
    forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
AccumulatorScheme d k i c f
-> Accumulator k i c f
-> NARKInstanceProof k i c f
-> (Accumulator k i c f, Vector (d - 1) (c f))
prover   ::
               Accumulator k i c f                          -- accumulator
            -> NARKInstanceProof k i c f                    -- instance-proof pair (pi, π)
            -> (Accumulator k i c f, Vector (d-1) (c f))    -- updated accumulator and accumulation proof

  , 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 :: i f                                         -- Public input
            -> Vector k (c f)                               -- NARK proof π.x
            -> AccumulatorInstance k i c f                  -- accumulator instance acc.x
            -> Vector (d-1) (c f)                           -- accumulation proof E_j
            -> AccumulatorInstance k i c f                  -- updated accumulator instance acc'.x

  , forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
AccumulatorScheme d k i c f
-> Accumulator k i c f -> (Vector k (c f), c f)
decider  ::
               Accumulator k i c f                          -- final accumulator
            -> (Vector k (c f), c f)                        -- returns zeros if the final accumulator is valid
  }

accumulatorScheme :: forall algo d k a i p c 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 (PU.PolyVec f (d+1))
    , Scale f (c f)
    )
    => Predicate a i p
    -> AccumulatorScheme d k i c f
accumulatorScheme :: forall {k} (algo :: k) (d :: Natural) (k :: 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 k i c f
accumulatorScheme Predicate a i p
phi =
  let
      prover :: Accumulator k i c f
-> NARKInstanceProof k i c f
-> (Accumulator k i c f, Vector (d - 1) (c f))
prover Accumulator k i c f
acc (NARKInstanceProof i f
pubi (NARKProof Vector k (c f)
pi_x Vector k [f]
pi_w)) =
        let
            r_0 :: f
            r_0 :: f
r_0 = 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 i f
pubi

            -- Fig. 3, step 1
            r_i :: Vector (k-1) f
            r_i :: Vector (k - 1) f
r_i = forall (algo :: k) (k2 :: Natural) (c :: Type -> Type) f.
(HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (c f) f) =>
f -> Vector k2 (c f) -> Vector (k2 - 1) f
forall {k1} (algo :: k1) (k2 :: Natural) (c :: Type -> Type) f.
(HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (c f) f) =>
f -> Vector k2 (c f) -> Vector (k2 - 1) f
transcript @algo f
r_0 Vector k (c f)
pi_x

            -- Fig. 3, step 2

            -- X + mu as a univariate polynomial
            polyMu :: PU.PolyVec f (d+1)
            polyMu :: PolyVec f (d + 1)
polyMu = f -> f -> PolyVec f (d + 1)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
PU.polyVecLinear f
forall a. MultiplicativeMonoid a => a
one (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting f (AccumulatorInstance k i c f) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance k i c f) f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
mu)

            -- X * pi + pi' as a list of univariate polynomials
            polyPi :: i (PU.PolyVec f (d+1))
            polyPi :: i (PolyVec f (d + 1))
polyPi = (f -> f -> PolyVec f (d + 1))
-> i f -> i f -> i (PolyVec f (d + 1))
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 (forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
PU.polyVecLinear @f) i f
pubi (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting (i f) (AccumulatorInstance k i c f) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance k i c f) (i f)
forall (k :: Natural) (i1 :: Type -> Type) (c :: Type -> Type) f1
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance k i1 c f1
-> f2 (AccumulatorInstance k i2 c f1)
pi)

            -- X * mi + mi'
            polyW :: Vector k [PU.PolyVec f (d+1)]
            polyW :: Vector k [PolyVec f (d + 1)]
polyW = ([f] -> [f] -> [PolyVec f (d + 1)])
-> Vector k [f] -> Vector k [f] -> Vector k [PolyVec f (d + 1)]
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith ((f -> f -> PolyVec f (d + 1)) -> [f] -> [f] -> [PolyVec f (d + 1)]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
PU.polyVecLinear @f)) Vector k [f]
pi_w (Accumulator k i c f
accAccumulator k i c f
-> Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k [f1] -> f2 (Vector k [f1]))
-> Accumulator k i c f1 -> f2 (Accumulator k i c f1)
w)

            -- X * ri + ri'
            polyR :: Vector (k-1) (PU.PolyVec f (d+1))
            polyR :: Vector (k - 1) (PolyVec f (d + 1))
polyR = (f -> f -> PolyVec f (d + 1))
-> Vector (k - 1) f
-> Vector (k - 1) f
-> Vector (k - 1) (PolyVec f (d + 1))
forall a b c.
(a -> b -> c)
-> Vector (k - 1) a -> Vector (k - 1) b -> Vector (k - 1) c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith ((f -> f -> PolyVec f (d + 1)) -> f -> f -> PolyVec f (d + 1)
forall a b c. (a -> b -> c) -> b -> a -> c
P.flip f -> f -> PolyVec f (d + 1)
forall c (size :: Natural).
(Ring c, KnownNat size) =>
c -> c -> PolyVec c size
PU.polyVecLinear) (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
r) Vector (k - 1) f
r_i

            -- The @l x d+1@ matrix of coefficients as a vector of @l@ univariate degree-@d@ polynomials
            --
            e_uni :: [Vector (d+1) f]
            e_uni :: [Vector (d + 1) f]
e_uni = [f] -> Vector (d + 1) f
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ([f] -> Vector (d + 1) f)
-> (PolyVec f (d + 1) -> [f])
-> PolyVec f (d + 1)
-> Vector (d + 1) f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PolyVec f (d + 1) -> [f]
PolyVec f (d + 1) -> [Item (PolyVec f (d + 1))]
forall l. IsList l => l -> [Item l]
toList (PolyVec f (d + 1) -> Vector (d + 1) f)
-> [PolyVec f (d + 1)] -> [Vector (d + 1) f]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f 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 (PolyVec f (d + 1))
polyPi Vector k [PolyVec f (d + 1)]
polyW Vector (k - 1) (PolyVec f (d + 1))
polyR PolyVec f (d + 1)
polyMu

            -- e_all are coefficients of degree-j homogenous polynomials where j is from the range [0, d]
            e_all :: Vector (d+1) [f]
            e_all :: Vector (d + 1) [f]
e_all = (Rep (Vector (d + 1)) -> [f]) -> Vector (d + 1) [f]
forall a. (Rep (Vector (d + 1)) -> a) -> Vector (d + 1) a
forall (f :: Type -> Type) a.
Representable f =>
(Rep f -> a) -> f a
tabulate (\Rep (Vector (d + 1))
i -> (Vector (d + 1) f -> f) -> [Vector (d + 1) f] -> [f]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (Vector (d + 1) f -> Rep (Vector (d + 1)) -> f
forall a. Vector (d + 1) a -> Rep (Vector (d + 1)) -> a
forall (f :: Type -> Type) a. Representable f => f a -> Rep f -> a
`index` Rep (Vector (d + 1))
i) [Vector (d + 1) f]
e_uni)

            -- e_j are coefficients of degree-j homogenous polynomials where j is from the range [1, d - 1]
            e_j :: Vector (d-1) [f]
            e_j :: Vector (d - 1) [f]
e_j = Dict (((d + 1) - 1) ~ d)
-> ((((d + 1) - 1) ~ d) => Vector (d - 1) [f])
-> Vector (d - 1) [f]
forall (c :: Constraint) e r. HasDict c e => e -> (c => r) -> r
withDict (forall (n :: Natural) (m :: Natural). Dict (((m + n) - n) ~ m)
plusMinusInverse1 @1 @d) (((((d + 1) - 1) ~ d) => Vector (d - 1) [f]) -> Vector (d - 1) [f])
-> ((((d + 1) - 1) ~ d) => Vector (d - 1) [f])
-> Vector (d - 1) [f]
forall a b. (a -> b) -> a -> b
$ Vector d [f] -> Vector (d - 1) [f]
forall (size :: Natural) a. Vector size a -> Vector (size - 1) a
tail (Vector d [f] -> Vector (d - 1) [f])
-> Vector d [f] -> Vector (d - 1) [f]
forall a b. (a -> b) -> a -> b
$ Vector (d + 1) [f] -> Vector ((d + 1) - 1) [f]
forall (size :: Natural) a. Vector size a -> Vector (size - 1) a
init Vector (d + 1) [f]
e_all

            -- Fig. 3, step 3
            pf :: Vector (d - 1) (c f)
pf = [f] -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit ([f] -> c f) -> Vector (d - 1) [f] -> Vector (d - 1) (c f)
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
<$> Vector (d - 1) [f]
e_j

            -- Fig. 3, step 4
            alpha :: f
            alpha :: f
alpha = 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 (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
x, i f
pubi, Vector k (c f)
pi_x, Vector (d - 1) (c f)
pf)

            -- Fig. 3, steps 5, 6
            mu' :: f
mu'   = f
alpha f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
+ Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting f (AccumulatorInstance k i c f) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance k i c f) f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
mu
            pi'' :: i f
pi''  = (f -> f -> f) -> i f -> i f -> i f
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 f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
(+) ((f -> f) -> i f -> i f
forall a b. (a -> b) -> i a -> i b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (f -> f -> f
forall a. MultiplicativeSemigroup a => a -> a -> a
* f
alpha) i f
pubi) (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting (i f) (AccumulatorInstance k i c f) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance k i c f) (i f)
forall (k :: Natural) (i1 :: Type -> Type) (c :: Type -> Type) f1
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance k i1 c f1
-> f2 (AccumulatorInstance k i2 c f1)
pi)
            ri'' :: Vector (k - 1) f
ri''  = f -> Vector (k - 1) f -> Vector (k - 1) f
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector (k - 1) f
r_i  Vector (k - 1) f -> Vector (k - 1) f -> Vector (k - 1) f
forall a. AdditiveSemigroup a => a -> a -> a
+ Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
r
            ci'' :: Vector k (c f)
ci''  = f -> Vector k (c f) -> Vector k (c f)
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector k (c f)
pi_x Vector k (c f) -> Vector k (c f) -> Vector k (c f)
forall a. AdditiveSemigroup a => a -> a -> a
+ Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting
     (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
-> Vector k (c f)
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k (c f1) -> f2 (Vector k (c f1)))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
c
            m_i'' :: Vector k [f]
m_i'' = ([f] -> [f] -> [f]) -> Vector k [f] -> Vector k [f] -> Vector k [f]
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith [f] -> [f] -> [f]
forall a. AdditiveSemigroup a => a -> a -> a
(+) (f -> Vector k [f] -> Vector k [f]
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector k [f]
pi_w) (Accumulator k i c f
accAccumulator k i c f
-> Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k [f1] -> f2 (Vector k [f1]))
-> Accumulator k i c f1 -> f2 (Accumulator k i c f1)
w)

            -- Fig. 3, step 7
            eCapital' :: c f
eCapital' = Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting (c f) (AccumulatorInstance k i c f) (c f) -> c f
forall s a. s -> Getting a s a -> a
^.Getting (c f) (AccumulatorInstance k i c f) (c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(c f1 -> f2 (c f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
e c f -> c f -> c f
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector (d - 1) (c f) -> c f
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((Natural -> c f -> c f)
-> Vector (d - 1) (c f) -> Vector (d - 1) (c f)
forall (n :: Natural) a b.
KnownNat n =>
(Natural -> a -> b) -> Vector n a -> Vector n b
mapWithIx (\Natural
i c f
a -> f -> c f -> c f
forall b a. Scale b a => b -> a -> a
scale (f
alpha f -> Natural -> f
forall a b. Exponent a b => a -> b -> a
^ (Natural
iNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
1)) c f
a) Vector (d - 1) (c f)
pf)
        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 (i f
-> Vector k (c f)
-> Vector (k - 1) f
-> c f
-> f
-> AccumulatorInstance k i c f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f.
i f
-> Vector k (c f)
-> Vector (k - 1) f
-> c f
-> f
-> AccumulatorInstance k i c f
AccumulatorInstance i f
pi'' Vector k (c f)
ci'' Vector (k - 1) f
ri'' c f
eCapital' f
mu') Vector k [f]
m_i'', Vector (d - 1) (c f)
pf)

      verifier :: i f
-> Vector k (c f)
-> AccumulatorInstance k i c f
-> Vector (d - 1) (c f)
-> AccumulatorInstance k i c f
verifier i f
pubi Vector k (c f)
pi_x AccumulatorInstance k i c f
acc Vector (d - 1) (c f)
pf =
        let
            r_0 :: f
            r_0 :: f
r_0 = 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 i f
pubi

            -- Fig. 4, step 1
            r_i :: Vector (k-1) f
            r_i :: Vector (k - 1) f
r_i = forall (algo :: k) (k2 :: Natural) (c :: Type -> Type) f.
(HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (c f) f) =>
f -> Vector k2 (c f) -> Vector (k2 - 1) f
forall {k1} (algo :: k1) (k2 :: Natural) (c :: Type -> Type) f.
(HashAlgorithm algo f, RandomOracle algo f f,
 RandomOracle algo (c f) f) =>
f -> Vector k2 (c f) -> Vector (k2 - 1) f
transcript @algo f
r_0 Vector k (c f)
pi_x

            -- Fig. 4, step 2
            alpha :: f
            alpha :: f
alpha = 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 i c f
acc, i f
pubi, Vector k (c f)
pi_x, Vector (d - 1) (c f)
pf)

            -- Fig. 4, steps 3-4
            mu' :: f
mu'  = f
alpha f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
+ AccumulatorInstance k i c f
accAccumulatorInstance k i c f
-> Getting f (AccumulatorInstance k i c f) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance k i c f) f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
mu
            pi'' :: i f
pi'' = (f -> f -> f) -> i f -> i f -> i f
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 f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
(+) ((f -> f) -> i f -> i f
forall a b. (a -> b) -> i a -> i b
forall (f :: Type -> Type) a b. Functor f => (a -> b) -> f a -> f b
fmap (f -> f -> f
forall a. MultiplicativeSemigroup a => a -> a -> a
* f
alpha) i f
pubi) (AccumulatorInstance k i c f
accAccumulatorInstance k i c f
-> Getting (i f) (AccumulatorInstance k i c f) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance k i c f) (i f)
forall (k :: Natural) (i1 :: Type -> Type) (c :: Type -> Type) f1
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance k i1 c f1
-> f2 (AccumulatorInstance k i2 c f1)
pi)
            ri'' :: Vector (k - 1) f
ri'' = (f -> f -> f)
-> Vector (k - 1) f -> Vector (k - 1) f -> Vector (k - 1) f
forall a b c.
(a -> b -> c)
-> Vector (k - 1) a -> Vector (k - 1) b -> Vector (k - 1) c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
(+) (f -> Vector (k - 1) f -> Vector (k - 1) f
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector (k - 1) f
r_i)     (AccumulatorInstance k i c f
accAccumulatorInstance k i c f
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
r)
            ci'' :: Vector k (c f)
ci'' = (c f -> c f -> c f)
-> Vector k (c f) -> Vector k (c f) -> Vector k (c f)
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith c f -> c f -> c f
forall a. AdditiveSemigroup a => a -> a -> a
(+) (f -> Vector k (c f) -> Vector k (c f)
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector k (c f)
pi_x)    (AccumulatorInstance k i c f
accAccumulatorInstance k i c f
-> Getting
     (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
-> Vector k (c f)
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k (c f1) -> f2 (Vector k (c f1)))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
c)

            -- Fig 4, step 5
            e' :: c f
e' = AccumulatorInstance k i c f
accAccumulatorInstance k i c f
-> Getting (c f) (AccumulatorInstance k i c f) (c f) -> c f
forall s a. s -> Getting a s a -> a
^.Getting (c f) (AccumulatorInstance k i c f) (c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(c f1 -> f2 (c f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
e c f -> c f -> c f
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector (d - 1) (c f) -> c f
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((Natural -> c f -> c f)
-> Vector (d - 1) (c f) -> Vector (d - 1) (c f)
forall (n :: Natural) a b.
KnownNat n =>
(Natural -> a -> b) -> Vector n a -> Vector n b
mapWithIx (\Natural
i c f
a -> f -> c f -> c f
forall b a. Scale b a => b -> a -> a
scale (f
alpha f -> Natural -> f
forall a b. Exponent a b => a -> b -> a
^ (Natural
iNatural -> Natural -> Natural
forall a. AdditiveSemigroup a => a -> a -> a
+Natural
1)) c f
a) Vector (d - 1) (c f)
pf)
        in
            AccumulatorInstance { _pi :: i f
_pi = i f
pi'', _c :: Vector k (c f)
_c = Vector k (c f)
ci'', _r :: Vector (k - 1) f
_r = Vector (k - 1) f
ri'', _e :: c f
_e = c f
e', _mu :: f
_mu = f
mu' }

      decider :: Accumulator k i c f -> (Vector k (c f), c f)
decider Accumulator k i c f
acc =
        let
            -- Fig. 5, step 1
            commitsDiff :: Vector k (c f)
commitsDiff = (c f -> [f] -> c f)
-> Vector k (c f) -> Vector k [f] -> Vector k (c f)
forall a b c.
(a -> b -> c) -> Vector k a -> Vector k b -> Vector k c
forall (f :: Type -> Type) a b c.
Zip f =>
(a -> b -> c) -> f a -> f b -> f c
zipWith (\c f
cm [f]
m_acc -> c f
cm c f -> c f -> c f
forall a. AdditiveGroup a => a -> a -> a
- [f] -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit [f]
m_acc) (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting
     (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
-> Vector k (c f)
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector k (c f)) (AccumulatorInstance k i c f) (Vector k (c f))
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k (c f1) -> f2 (Vector k (c f1)))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
c) (Accumulator k i c f
accAccumulator k i c f
-> Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k [f1] -> f2 (Vector k [f1]))
-> Accumulator k i c f1 -> f2 (Accumulator k i c f1)
w)

            -- Fig. 5, step 2
            err :: [f]
            err :: [f]
err = 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 (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting (i f) (AccumulatorInstance k i c f) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance k i c f) (i f)
forall (k :: Natural) (i1 :: Type -> Type) (c :: Type -> Type) f1
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance k i1 c f1
-> f2 (AccumulatorInstance k i2 c f1)
pi) (Accumulator k i c f
accAccumulator k i c f
-> Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator k i c f) (Vector k [f])
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k [f1] -> f2 (Vector k [f1]))
-> Accumulator k i c f1 -> f2 (Accumulator k i c f1)
w) (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance k i c f) (Vector (k - 1) f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
r) (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting f (AccumulatorInstance k i c f) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance k i c f) f
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
mu)


            -- Fig. 5, step 3
            eDiff :: c f
eDiff = (Accumulator k i c f
accAccumulator 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) (i1 :: Type -> Type) (c1 :: Type -> Type) f1
       (i2 :: Type -> Type) (c2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(AccumulatorInstance k i1 c1 f1
 -> f2 (AccumulatorInstance k i2 c2 f1))
-> Accumulator k i1 c1 f1 -> f2 (Accumulator k i2 c2 f1)
xAccumulatorInstance k i c f
-> Getting (c f) (AccumulatorInstance k i c f) (c f) -> c f
forall s a. s -> Getting a s a -> a
^.Getting (c f) (AccumulatorInstance k i c f) (c f)
forall (k :: Natural) (i :: Type -> Type) (c :: Type -> Type) f1
       (f2 :: Type -> Type).
Functor f2 =>
(c f1 -> f2 (c f1))
-> AccumulatorInstance k i c f1
-> f2 (AccumulatorInstance k i c f1)
e) c f -> c f -> c f
forall a. AdditiveGroup a => a -> a -> a
- [f] -> c f
forall a c. HomomorphicCommit a c => a -> c
hcommit [f]
err
        in
            (Vector k (c f)
commitsDiff, c f
eDiff)

  in
      (Accumulator k i c f
 -> NARKInstanceProof k i c f
 -> (Accumulator k i c f, Vector (d - 1) (c f)))
-> (i f
    -> Vector k (c f)
    -> AccumulatorInstance k i c f
    -> Vector (d - 1) (c f)
    -> AccumulatorInstance k i c f)
-> (Accumulator k i c f -> (Vector k (c f), c f))
-> AccumulatorScheme d k i c f
forall (d :: Natural) (k :: Natural) (i :: Type -> Type)
       (c :: Type -> Type) f.
(Accumulator k i c f
 -> NARKInstanceProof k i c f
 -> (Accumulator k i c f, Vector (d - 1) (c f)))
-> (i f
    -> Vector k (c f)
    -> AccumulatorInstance k i c f
    -> Vector (d - 1) (c f)
    -> AccumulatorInstance k i c f)
-> (Accumulator k i c f -> (Vector k (c f), c f))
-> AccumulatorScheme d k i c f
AccumulatorScheme Accumulator k i c f
-> NARKInstanceProof k i c f
-> (Accumulator k i c f, Vector (d - 1) (c f))
prover i f
-> Vector k (c f)
-> AccumulatorInstance k i c f
-> Vector (d - 1) (c f)
-> AccumulatorInstance k i c f
verifier Accumulator k i c f -> (Vector k (c f), c f)
decider