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

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

module ZkFold.Base.Protocol.Protostar.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.Protostar.Accumulator
import           ZkFold.Base.Protocol.Protostar.AlgebraicMap (AlgebraicMap (..))
import           ZkFold.Base.Protocol.Protostar.Commit       (HomomorphicCommit (..))
import           ZkFold.Base.Protocol.Protostar.CommitOpen   (CommitOpen (..))
import           ZkFold.Base.Protocol.Protostar.FiatShamir   (FiatShamir (..), transcriptFiatShamir)
import           ZkFold.Base.Protocol.Protostar.NARK         (NARKInstanceProof (..), NARKProof (..))
import           ZkFold.Base.Protocol.Protostar.Oracle       (RandomOracle (..))

-- | Accumulator scheme for V_NARK as described in Chapter 3.4 of the Protostar paper
--
-- TODO: define the initial accumulator
--
class AccumulatorScheme f i m c d k a where
  prover   :: a
           -> Accumulator f i m c k                      -- accumulator
           -> NARKInstanceProof f i m c k                -- instance-proof pair (pi, π)
           -> (Accumulator f i m c k, Vector (d - 1) c)  -- updated accumulator and accumulation proof

  verifier :: i f                                        -- Public input
           -> Vector k c                                 -- NARK proof π.x
           -> AccumulatorInstance f i c k                -- accumulator instance acc.x
           -> AccumulatorInstance f i c k                -- updated accumulator instance acc'.x
           -> Vector (d - 1) c                           -- accumulation proof E_j
           -> (f, i f, Vector (k-1) f, Vector k c, c)    -- returns zeros if the accumulation proof is correct

  decider  :: a
           -> Accumulator f i m c k                      -- final accumulator
           -> (Vector k c, c)                            -- returns zeros if the final accumulator is valid

instance
    ( AlgebraicMap f i d a
    , AlgebraicMap (PU.PolyVec f (d + 1)) i d a
    , Ring f
    , Zip i
    , KnownNat (d - 1)
    , KnownNat (d + 1)
    , Scale f c
    , HomomorphicCommit [f] c
    , RandomOracle (i f) f    -- Random oracle for compressing public input
    , RandomOracle c f        -- Random oracle ρ_NARK
    , KnownNat k
    ) => AccumulatorScheme f i [f] c d k (FiatShamir (CommitOpen a)) where
  prover :: FiatShamir (CommitOpen a)
-> Accumulator f i [f] c k
-> NARKInstanceProof f i [f] c k
-> (Accumulator f i [f] c k, Vector (d - 1) c)
prover (FiatShamir (CommitOpen a
sps)) Accumulator f i [f] c k
acc (NARKInstanceProof i f
pubi (NARKProof Vector k c
pi_x Vector k [f]
pi_w)) =
        (AccumulatorInstance f i c k
-> Vector k [f] -> Accumulator f i [f] c k
forall f (i :: Type -> Type) m c (k :: Natural).
AccumulatorInstance f i c k -> Vector k m -> Accumulator f i m c k
Accumulator (i f
-> Vector k c
-> Vector (k - 1) f
-> c
-> f
-> AccumulatorInstance f i c k
forall f (i :: Type -> Type) c (k :: Natural).
i f
-> Vector k c
-> Vector (k - 1) f
-> c
-> f
-> AccumulatorInstance f i c k
AccumulatorInstance i f
pi'' Vector k c
ci'' Vector (k - 1) f
ri'' c
eCapital' f
mu') Vector k [f]
m_i'', Vector (d - 1) c
pf)
      where
          r_0 :: f
          r_0 :: f
r_0 = i f -> f
forall a b. RandomOracle a b => a -> b
oracle i f
pubi

          -- Fig. 3, step 1
          r_i :: Vector (k-1) f
          r_i :: Vector (k - 1) f
r_i = f -> Vector k c -> Vector (k - 1) f
forall f c (k :: Natural).
(Ring f, RandomOracle f f, RandomOracle c f) =>
f -> Vector k c -> Vector (k - 1) f
transcriptFiatShamir f
r_0 Vector k c
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting f (AccumulatorInstance f i c k) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance f i c k) f
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting (i f) (AccumulatorInstance f i c k) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance f i c k) (i f)
forall f1 (i1 :: Type -> Type) c (k :: Natural)
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance f1 i1 c k
-> f2 (AccumulatorInstance f1 i2 c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
forall f1 (i :: Type -> Type) m1 c (k :: Natural) m2
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k m1 -> f2 (Vector k m2))
-> Accumulator f1 i m1 c k -> f2 (Accumulator f1 i m2 c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
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 f (i :: Type -> Type) (d :: Natural) a (k :: Natural).
AlgebraicMap f i d a =>
a -> i f -> Vector k [f] -> Vector (k - 1) f -> f -> [f]
algebraicMap @_ @_ @d a
sps 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
pf = [f] -> c
forall a c. HomomorphicCommit a c => a -> c
hcommit ([f] -> c) -> Vector (d - 1) [f] -> Vector (d - 1) c
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 = (AccumulatorInstance f i c k, i f, Vector k c, Vector (d - 1) c)
-> f
forall a b. RandomOracle a b => a -> b
oracle (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
x, i f
pubi, Vector k c
pi_x, Vector (d - 1) c
pf)

          -- Fig. 3, steps 5, 6
          mu' :: f
mu'   = f
alpha f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
+ Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting f (AccumulatorInstance f i c k) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance f i c k) f
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting (i f) (AccumulatorInstance f i c k) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance f i c k) (i f)
forall f1 (i1 :: Type -> Type) c (k :: Natural)
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance f1 i1 c k
-> f2 (AccumulatorInstance f1 i2 c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
r
          ci'' :: Vector k c
ci''  = f -> Vector k c -> Vector k c
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector k c
pi_x Vector k c -> Vector k c -> Vector k c
forall a. AdditiveSemigroup a => a -> a -> a
+ Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
-> Vector k c
forall s a. s -> Getting a s a -> a
^.Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k c -> f2 (Vector k c))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
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 f i [f] c k
accAccumulator f i [f] c k
-> Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
forall f1 (i :: Type -> Type) m1 c (k :: Natural) m2
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k m1 -> f2 (Vector k m2))
-> Accumulator f1 i m1 c k -> f2 (Accumulator f1 i m2 c k)
w)

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


  verifier :: i f
-> Vector k c
-> AccumulatorInstance f i c k
-> AccumulatorInstance f i c k
-> Vector (d - 1) c
-> (f, i f, Vector (k - 1) f, Vector k c, c)
verifier i f
pubi Vector k c
c_i AccumulatorInstance f i c k
acc AccumulatorInstance f i c k
acc' Vector (d - 1) c
pf = (f
muDiff, i f
piDiff, Vector (k - 1) f
riDiff, Vector k c
ciDiff, c
eDiff)
      where
          -- Fig. 4, step 1
          r_i :: Vector (k-1) f
          r_i :: Vector (k - 1) f
r_i = [f] -> Vector (k - 1) f
forall (size :: Natural) a. [a] -> Vector size a
unsafeToVector ([f] -> Vector (k - 1) f) -> [f] -> Vector (k - 1) f
forall a b. (a -> b) -> a -> b
$ [f] -> [f]
forall a. HasCallStack => [a] -> [a]
P.tail ([f] -> [f]) -> [f] -> [f]
forall a b. (a -> b) -> a -> b
$ [f] -> [f]
forall a. HasCallStack => [a] -> [a]
P.tail ([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]
P.scanl (((f, c) -> f) -> f -> c -> f
forall a b c. ((a, b) -> c) -> a -> b -> c
P.curry (f, c) -> f
forall a b. RandomOracle a b => a -> b
oracle) (i f -> f
forall a b. RandomOracle a b => a -> b
oracle i f
pubi) ([c] -> [f]) -> [c] -> [f]
forall a b. (a -> b) -> a -> b
$ Vector k c -> [Item (Vector k c)]
forall l. IsList l => l -> [Item l]
toList Vector k c
c_i

          -- Fig. 4, step 2
          alpha :: f
          alpha :: f
alpha = (AccumulatorInstance f i c k, i f, Vector k c, Vector (d - 1) c)
-> f
forall a b. RandomOracle a b => a -> b
oracle (AccumulatorInstance f i c k
acc, i f
pubi, Vector k c
c_i, Vector (d - 1) c
pf)

          -- Fig. 4, step 3
          mu' :: f
mu'  = f
alpha f -> f -> f
forall a. AdditiveSemigroup a => a -> a -> a
+ AccumulatorInstance f i c k
accAccumulatorInstance f i c k
-> Getting f (AccumulatorInstance f i c k) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance f i c k) f
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
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 f i c k
accAccumulatorInstance f i c k
-> Getting (i f) (AccumulatorInstance f i c k) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance f i c k) (i f)
forall f1 (i1 :: Type -> Type) c (k :: Natural)
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance f1 i1 c k
-> f2 (AccumulatorInstance f1 i2 c k)
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 f i c k
accAccumulatorInstance f i c k
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
r)
          ci'' :: Vector k c
ci'' = (c -> c -> c) -> Vector k c -> Vector k c -> Vector k c
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 -> c -> c
forall a. AdditiveSemigroup a => a -> a -> a
(+) (f -> Vector k c -> Vector k c
forall b a. Scale b a => b -> a -> a
scale f
alpha Vector k c
c_i)  (AccumulatorInstance f i c k
accAccumulatorInstance f i c k
-> Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
-> Vector k c
forall s a. s -> Getting a s a -> a
^.Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k c -> f2 (Vector k c))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
c)

          -- Fig 4, step 4
          muDiff :: f
muDiff = AccumulatorInstance f i c k
acc'AccumulatorInstance f i c k
-> Getting f (AccumulatorInstance f i c k) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance f i c k) f
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
mu f -> f -> f
forall a. AdditiveGroup a => a -> a -> a
- f
mu'
          piDiff :: i f
piDiff = (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 (-) (AccumulatorInstance f i c k
acc'AccumulatorInstance f i c k
-> Getting (i f) (AccumulatorInstance f i c k) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance f i c k) (i f)
forall f1 (i1 :: Type -> Type) c (k :: Natural)
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance f1 i1 c k
-> f2 (AccumulatorInstance f1 i2 c k)
pi) i f
pi''
          riDiff :: Vector (k - 1) f
riDiff = (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 (-) (AccumulatorInstance f i c k
acc'AccumulatorInstance f i c k
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
r)  Vector (k - 1) f
ri''
          ciDiff :: Vector k c
ciDiff = AccumulatorInstance f i c k
acc'AccumulatorInstance f i c k
-> Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
-> Vector k c
forall s a. s -> Getting a s a -> a
^.Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k c -> f2 (Vector k c))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
c  Vector k c -> Vector k c -> Vector k c
forall a. AdditiveGroup a => a -> a -> a
- Vector k c
ci''

          -- Fig 4, step 5
          eDiff :: c
eDiff = AccumulatorInstance f i c k
acc'AccumulatorInstance f i c k
-> Getting c (AccumulatorInstance f i c k) c -> c
forall s a. s -> Getting a s a -> a
^.Getting c (AccumulatorInstance f i c k) c
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(c -> f2 c)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
e c -> c -> c
forall a. AdditiveGroup a => a -> a -> a
- (AccumulatorInstance f i c k
accAccumulatorInstance f i c k
-> Getting c (AccumulatorInstance f i c k) c -> c
forall s a. s -> Getting a s a -> a
^.Getting c (AccumulatorInstance f i c k) c
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(c -> f2 c)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
e c -> c -> c
forall a. AdditiveSemigroup a => a -> a -> a
+ Vector (d - 1) c -> c
forall (t :: Type -> Type) a.
(Foldable t, AdditiveMonoid a) =>
t a -> a
sum ((Natural -> c -> c) -> Vector (d - 1) c -> Vector (d - 1) c
forall (n :: Natural) a b.
KnownNat n =>
(Natural -> a -> b) -> Vector n a -> Vector n b
mapWithIx (\Natural
i c
a -> f -> c -> c
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
a) Vector (d - 1) c
pf))

  decider :: FiatShamir (CommitOpen a)
-> Accumulator f i [f] c k -> (Vector k c, c)
decider (FiatShamir (CommitOpen a
sps)) Accumulator f i [f] c k
acc = (Vector k c
commitsDiff, c
eDiff)
      where
          -- Fig. 5, step 1
          commitsDiff :: Vector k c
commitsDiff = (c -> [f] -> c) -> Vector k c -> Vector k [f] -> Vector k c
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
cm [f]
m_acc -> c
cm c -> c -> c
forall a. AdditiveGroup a => a -> a -> a
- [f] -> c
forall a c. HomomorphicCommit a c => a -> c
hcommit [f]
m_acc) (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
-> Vector k c
forall s a. s -> Getting a s a -> a
^.Getting (Vector k c) (AccumulatorInstance f i c k) (Vector k c)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k c -> f2 (Vector k c))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
c) (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
forall f1 (i :: Type -> Type) m1 c (k :: Natural) m2
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k m1 -> f2 (Vector k m2))
-> Accumulator f1 i m1 c k -> f2 (Accumulator f1 i m2 c k)
w)

          -- Fig. 5, step 2
          err :: [f]
          err :: [f]
err = forall f (i :: Type -> Type) (d :: Natural) a (k :: Natural).
AlgebraicMap f i d a =>
a -> i f -> Vector k [f] -> Vector (k - 1) f -> f -> [f]
algebraicMap @_ @_ @d a
sps (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting (i f) (AccumulatorInstance f i c k) (i f) -> i f
forall s a. s -> Getting a s a -> a
^.Getting (i f) (AccumulatorInstance f i c k) (i f)
forall f1 (i1 :: Type -> Type) c (k :: Natural)
       (i2 :: Type -> Type) (f2 :: Type -> Type).
Functor f2 =>
(i1 f1 -> f2 (i2 f1))
-> AccumulatorInstance f1 i1 c k
-> f2 (AccumulatorInstance f1 i2 c k)
pi) (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
-> Vector k [f]
forall s a. s -> Getting a s a -> a
^.Getting (Vector k [f]) (Accumulator f i [f] c k) (Vector k [f])
forall f1 (i :: Type -> Type) m1 c (k :: Natural) m2
       (f2 :: Type -> Type).
Functor f2 =>
(Vector k m1 -> f2 (Vector k m2))
-> Accumulator f1 i m1 c k -> f2 (Accumulator f1 i m2 c k)
w) (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting
     (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
-> Vector (k - 1) f
forall s a. s -> Getting a s a -> a
^.Getting
  (Vector (k - 1) f) (AccumulatorInstance f i c k) (Vector (k - 1) f)
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(Vector (k - 1) f1 -> f2 (Vector (k - 1) f1))
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
r) (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting f (AccumulatorInstance f i c k) f -> f
forall s a. s -> Getting a s a -> a
^.Getting f (AccumulatorInstance f i c k) f
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(f1 -> f2 f1)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
mu)


          -- Fig. 5, step 3
          eDiff :: c
eDiff = (Accumulator f i [f] c k
accAccumulator f i [f] c k
-> Getting
     (AccumulatorInstance f i c k)
     (Accumulator f i [f] c k)
     (AccumulatorInstance f i c k)
-> AccumulatorInstance f i c k
forall s a. s -> Getting a s a -> a
^.Getting
  (AccumulatorInstance f i c k)
  (Accumulator f i [f] c k)
  (AccumulatorInstance f i c k)
forall f1 (i1 :: Type -> Type) m c1 (k :: Natural) f2
       (i2 :: Type -> Type) c2 (f3 :: Type -> Type).
Functor f3 =>
(AccumulatorInstance f1 i1 c1 k
 -> f3 (AccumulatorInstance f2 i2 c2 k))
-> Accumulator f1 i1 m c1 k -> f3 (Accumulator f2 i2 m c2 k)
xAccumulatorInstance f i c k
-> Getting c (AccumulatorInstance f i c k) c -> c
forall s a. s -> Getting a s a -> a
^.Getting c (AccumulatorInstance f i c k) c
forall f1 (i :: Type -> Type) c (k :: Natural)
       (f2 :: Type -> Type).
Functor f2 =>
(c -> f2 c)
-> AccumulatorInstance f1 i c k
-> f2 (AccumulatorInstance f1 i c k)
e) c -> c -> c
forall a. AdditiveGroup a => a -> a -> a
- [f] -> c
forall a c. HomomorphicCommit a c => a -> c
hcommit [f]
err