Merge branch 'main' into secp256k1-merge

symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs

@@ -8,6 +8,7 @@ module ZkFold.Base.Algebra.Basic.Class where
 
 import           Data.Bool                        (bool)
 import           Data.Foldable                    (foldl')
+import           Data.Functor.Constant            (Constant (..))
 import           Data.Kind                        (Type)
 import           GHC.Natural                      (naturalFromInteger)
 import           Prelude                          hiding (Num (..), div, divMod, length, mod, negate, product,
@@ -285,7 +286,6 @@ class Semiring a => SemiEuclidean a where
     mod :: a -> a -> a
     mod n d = Haskell.snd $ divMod n d
 
-
 {- | Class of rings with both 0, 1 and additive inverses. The following should hold:
 
 [Left distributivity] @a * (b - c) == a * b - a * c@
@@ -691,7 +691,55 @@ instance Semiring a => Semiring (p -> a)
 
 instance Ring a => Ring (p -> a)
 
----------------------------------------------------------------------------------
+--------------------------------------------------------------------------------
+
+instance {-# OVERLAPPING #-} FromConstant (Constant a f) (Constant a f)
+
+instance FromConstant a b => FromConstant a (Constant b f) where
+    fromConstant = Constant . fromConstant
+
+instance Scale b a => Scale b (Constant a f) where
+    scale c (Constant x) = Constant (scale c x)
+
+instance (MultiplicativeSemigroup a, Scale (Constant a f) (Constant a f)) => MultiplicativeSemigroup (Constant a f) where
+    Constant x * Constant y = Constant (x * y)
+
+instance Exponent a b => Exponent (Constant a f) b where
+    Constant x ^ y = Constant (x ^ y)
+
+instance (MultiplicativeMonoid a, Scale (Constant a f) (Constant a f)) => MultiplicativeMonoid (Constant a f) where
+    one = Constant one
+
+instance (MultiplicativeGroup a, Scale (Constant a f) (Constant a f)) => MultiplicativeGroup (Constant a f) where
+    Constant x / Constant y = Constant (x / y)
+
+    invert (Constant x) = Constant (invert x)
+
+instance AdditiveSemigroup a => AdditiveSemigroup (Constant a f) where
+    Constant x + Constant y = Constant (x + y)
+
+instance AdditiveMonoid a => AdditiveMonoid (Constant a f) where
+    zero = Constant zero
+
+instance AdditiveGroup a => AdditiveGroup (Constant a f) where
+    Constant x - Constant y = Constant (x - y)
+
+    negate (Constant x) = Constant (negate x)
+
+instance (Semiring a, Scale (Constant a f) (Constant a f)) => Semiring (Constant a f)
+
+instance (SemiEuclidean a, Scale (Constant a f) (Constant a f)) => SemiEuclidean (Constant a f) where
+    divMod (Constant x) (Constant y) = (Constant q, Constant r)
+      where
+        (q, r) = divMod x y
+
+    div (Constant x) (Constant y) = Constant (div x y)
+
+    mod (Constant x) (Constant y) = Constant (mod x y)
+
+instance (Ring a, Scale (Constant a f) (Constant a f)) => Ring (Constant a f)
+
+--------------------------------------------------------------------------------
 
 instance Finite a => Finite (Maybe a) where
     type Order (Maybe a) = Order a

symbolic-base/src/ZkFold/Base/Data/Orphans.hs

@@ -0,0 +1,16 @@
+{-# LANGUAGE DerivingStrategies   #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+{-# OPTIONS_GHC -Wno-orphans #-}
+
+module ZkFold.Base.Data.Orphans where
+
+import           Control.DeepSeq  (NFData)
+import           Data.Binary      (Binary)
+import           Data.Functor.Rep (Representable (..), WrappedRep (..))
+import           Prelude          (Eq, Ord)
+
+deriving newtype instance NFData (Rep f) => NFData (WrappedRep f)
+deriving newtype instance Binary (Rep f) => Binary (WrappedRep f)
+deriving instance Eq (Rep f) => Eq (WrappedRep f)
+deriving instance Ord (Rep f) => Ord (WrappedRep f)

symbolic-base/src/ZkFold/Base/Protocol/IVC.hs

@@ -0,0 +1,3 @@
+module ZkFold.Base.Protocol.IVC (module Protostar) where
+
+import           ZkFold.Base.Protocol.IVC.Internal as Protostar

symbolic-base/src/ZkFold/Base/Protocol/IVC/Accumulator.hs

@@ -0,0 +1,100 @@
+{-# LANGUAGE AllowAmbiguousTypes  #-}
+{-# LANGUAGE DeriveAnyClass       #-}
+{-# LANGUAGE TemplateHaskell      #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module ZkFold.Base.Protocol.IVC.Accumulator where
+
+import           Control.DeepSeq                       (NFData (..))
+import           Control.Lens                          ((^.))
+import           Control.Lens.Combinators              (makeLenses)
+import           Data.Distributive                     (Distributive (..))
+import           Data.Functor.Rep                      (Representable (..), collectRep, distributeRep)
+import           GHC.Generics
+import           Prelude                               hiding (length, pi)
+
+import           ZkFold.Base.Algebra.Basic.Class       (Ring, Scale, zero)
+import           ZkFold.Base.Algebra.Basic.Number      (KnownNat, type (+), type (-))
+import           ZkFold.Base.Data.Vector               (Vector)
+import           ZkFold.Base.Protocol.IVC.AlgebraicMap (algebraicMap)
+import           ZkFold.Base.Protocol.IVC.Commit       (HomomorphicCommit (..))
+import           ZkFold.Base.Protocol.IVC.Oracle       (HashAlgorithm, RandomOracle)
+import           ZkFold.Base.Protocol.IVC.Predicate    (Predicate)
+import           ZkFold.Symbolic.Data.Class            (SymbolicData (..))
+
+-- Page 19, Accumulator instance
+data AccumulatorInstance k i c f
+    = AccumulatorInstance
+        { _pi :: i f             -- pi ∈ M^{l_in} in the paper
+        , _c  :: Vector k (c f)  -- [C_i] ∈ C^k in the paper
+        , _r  :: Vector (k-1) f  -- [r_i] ∈ F^{k-1} in the paper
+        , _e  :: c f             -- E ∈ C in the paper
+        , _mu :: f               -- μ ∈ F in the paper
+        }
+    deriving (Show, Eq, Generic, Generic1, NFData, Functor, Foldable, Traversable)
+
+makeLenses ''AccumulatorInstance
+
+instance (Representable i, Representable c, KnownNat k, KnownNat (k-1)) => Distributive (AccumulatorInstance k i c) where
+    distribute = distributeRep
+    collect = collectRep
+
+instance (Representable i, Representable c, KnownNat k, KnownNat (k-1)) => Representable (AccumulatorInstance k i c)
+
+instance (HashAlgorithm algo f, RandomOracle algo f f, RandomOracle algo (i f) f, RandomOracle algo (c f) f)
+    => RandomOracle algo (AccumulatorInstance k i c f) f
+
+instance
+    ( KnownNat (k-1)
+    , KnownNat k
+    , SymbolicData f
+    , SymbolicData (i f)
+    , SymbolicData (c f)
+    , Context f ~ Context (c f)
+    , Context f ~ Context (i f)
+    , Support f ~ Support (c f)
+    , Support f ~ Support (i f)
+    ) => SymbolicData (AccumulatorInstance k i c f)
+
+-- Page 19, Accumulator
+-- @acc.x@ (accumulator instance) from the paper corresponds to _x
+-- @acc.w@ (accumulator witness) from the paper corresponds to _w
+data Accumulator k i c f
+    = Accumulator
+        { _x :: AccumulatorInstance k i c f
+        , _w :: Vector k [f]
+        }
+    deriving (Show, Generic, NFData)
+
+makeLenses ''Accumulator
+
+emptyAccumulator :: forall d k a i p c f .
+    ( KnownNat (d+1)
+    , KnownNat (k-1)
+    , KnownNat k
+    , Representable i
+    , HomomorphicCommit [f] (c f)
+    , Ring f
+    , Scale a f
+    ) => Predicate a i p -> Accumulator k i c f
+emptyAccumulator phi =
+    let accW  = tabulate (const zero)
+        aiC   = fmap hcommit accW
+        aiR   = tabulate (const zero)
+        aiMu  = zero
+        aiPI  = tabulate (const zero)
+        aiE   = hcommit $ algebraicMap @d phi aiPI accW aiR aiMu
+        accX = AccumulatorInstance { _pi = aiPI, _c = aiC, _r = aiR, _e = aiE, _mu = aiMu }
+    in Accumulator accX accW
+
+emptyAccumulatorInstance :: forall d k a i p c f .
+    ( KnownNat (d+1)
+    , KnownNat (k-1)
+    , KnownNat k
+    , Representable i
+    , HomomorphicCommit [f] (c f)
+    , Ring f
+    , Scale a f
+    ) => Predicate a i p -> AccumulatorInstance k i c f
+emptyAccumulatorInstance phi = emptyAccumulator @d phi ^. x

symbolic-base/src/ZkFold/Base/Protocol/IVC/AccumulatorScheme.hs

@@ -0,0 +1,167 @@
+{-# 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
+  {
+    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
+
+  , 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
+
+  , 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 phi =
+  let
+      prover acc (NARKInstanceProof pubi (NARKProof pi_x pi_w)) =
+        let
+            r_0 :: f
+            r_0 = oracle @algo pubi
+
+            -- Fig. 3, step 1
+            r_i :: Vector (k-1) f
+            r_i = transcript @algo r_0 pi_x
+
+            -- Fig. 3, step 2
+
+            -- X + mu as a univariate polynomial
+            polyMu :: PU.PolyVec f (d+1)
+            polyMu = PU.polyVecLinear one (acc^.x^.mu)
+
+            -- X * pi + pi' as a list of univariate polynomials
+            polyPi :: i (PU.PolyVec f (d+1))
+            polyPi = zipWith (PU.polyVecLinear @f) pubi (acc^.x^.pi)
+
+            -- X * mi + mi'
+            polyW :: Vector k [PU.PolyVec f (d+1)]
+            polyW = zipWith (zipWith (PU.polyVecLinear @f)) pi_w (acc^.w)
+
+            -- X * ri + ri'
+            polyR :: Vector (k-1) (PU.PolyVec f (d+1))
+            polyR = zipWith (P.flip PU.polyVecLinear) (acc^.x^.r) 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 = unsafeToVector . toList <$> algebraicMap @d phi polyPi polyW polyR 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 = tabulate (\i -> fmap (`index` i) 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 = withDict (plusMinusInverse1 @1 @d) $ tail $ init e_all
+
+            -- Fig. 3, step 3
+            pf = hcommit <$> e_j
+
+            -- Fig. 3, step 4
+            alpha :: f
+            alpha = oracle @algo (acc^.x, pubi, pi_x, pf)
+
+            -- Fig. 3, steps 5, 6
+            mu'   = alpha + acc^.x^.mu
+            pi''  = zipWith (+) (fmap (* alpha) pubi) (acc^.x^.pi)
+            ri''  = scale alpha r_i  + acc^.x^.r
+            ci''  = scale alpha pi_x + acc^.x^.c
+            m_i'' = zipWith (+) (scale alpha pi_w) (acc^.w)
+
+            -- Fig. 3, step 7
+            eCapital' = acc^.x^.e + sum (mapWithIx (\i a -> scale (alpha ^ (i+1)) a) pf)
+        in
+            (Accumulator (AccumulatorInstance pi'' ci'' ri'' eCapital' mu') m_i'', pf)
+
+      verifier pubi pi_x acc pf =
+        let
+            r_0 :: f
+            r_0 = oracle @algo pubi
+
+            -- Fig. 4, step 1
+            r_i :: Vector (k-1) f
+            r_i = transcript @algo r_0 pi_x
+
+            -- Fig. 4, step 2
+            alpha :: f
+            alpha = oracle @algo (acc, pubi, pi_x, pf)
+
+            -- Fig. 4, steps 3-4
+            mu'  = alpha + acc^.mu
+            pi'' = zipWith (+) (fmap (* alpha) pubi) (acc^.pi)
+            ri'' = zipWith (+) (scale alpha r_i)     (acc^.r)
+            ci'' = zipWith (+) (scale alpha pi_x)    (acc^.c)
+
+            -- Fig 4, step 5
+            e' = acc^.e + sum (mapWithIx (\i a -> scale (alpha ^ (i+1)) a) pf)
+        in
+            AccumulatorInstance { _pi = pi'', _c = ci'', _r = ri'', _e = e', _mu = mu' }
+
+      decider acc =
+        let
+            -- Fig. 5, step 1
+            commitsDiff = zipWith (\cm m_acc -> cm - hcommit m_acc) (acc^.x^.c) (acc^.w)
+
+            -- Fig. 5, step 2
+            err :: [f]
+            err = algebraicMap @d phi (acc^.x^.pi) (acc^.w) (acc^.x^.r) (acc^.x^.mu)
+
+
+            -- Fig. 5, step 3
+            eDiff = (acc^.x^.e) - hcommit err
+        in
+            (commitsDiff, eDiff)
+
+  in
+      AccumulatorScheme prover verifier decider