diff --git a/symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs b/symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs index 541d3895d..9a27cc897 100644 --- a/symbolic-base/src/ZkFold/Base/Algebra/Basic/Class.hs +++ b/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 diff --git a/symbolic-base/src/ZkFold/Base/Data/Orphans.hs b/symbolic-base/src/ZkFold/Base/Data/Orphans.hs new file mode 100644 index 000000000..d6a2c2031 --- /dev/null +++ b/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) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC.hs new file mode 100644 index 000000000..b12ab6351 --- /dev/null +++ b/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 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Accumulator.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Accumulator.hs new file mode 100644 index 000000000..d7cf3bb2d --- /dev/null +++ b/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 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/AccumulatorScheme.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/AccumulatorScheme.hs new file mode 100644 index 000000000..ef5bfd19c --- /dev/null +++ b/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 diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/AlgebraicMap.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/AlgebraicMap.hs new file mode 100644 index 000000000..ce8c36f84 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/AlgebraicMap.hs @@ -0,0 +1,81 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.AlgebraicMap (algebraicMap) where + +import Data.ByteString (ByteString) +import Data.Functor.Rep (Representable (..)) +import Data.List (foldl') +import Data.Map.Strict (Map, keys) +import qualified Data.Map.Strict as M +import Prelude (fmap, zip, ($), (.), (<$>)) +import qualified Prelude as P + +import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Algebra.Basic.Number +import qualified ZkFold.Base.Algebra.Polynomials.Multivariate as PM +import ZkFold.Base.Algebra.Polynomials.Multivariate +import qualified ZkFold.Base.Data.Vector as V +import ZkFold.Base.Data.Vector (Vector) +import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..)) +import ZkFold.Symbolic.Compiler +import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal +import ZkFold.Symbolic.Data.Eq + +-- | Algebraic map of @a@. +-- It calculates a system of equations defining @a@ in some way. +-- The inputs are polymorphic in a ring element @f@. +-- The main application is to define the verifier's algebraic map in the NARK protocol. +-- +algebraicMap :: forall d k a i p 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 Predicate {..} pi pm _ pad = padDecomposition pad f_sps_uni + where + sys :: [PM.Poly a (SysVar i) Natural] + sys = M.elems (acSystem predicateCircuit) + + witness :: Map ByteString f + witness = M.fromList $ zip (keys $ acWitness predicateCircuit) (V.head pm) + + varMap :: SysVar i -> f + varMap (InVar inV) = index pi inV + varMap (NewVar newV) = M.findWithDefault zero newV witness + + f_sps :: Vector (d+1) [PM.Poly a (SysVar i) Natural] + f_sps = degreeDecomposition @d $ sys + + f_sps_uni :: Vector (d+1) [f] + f_sps_uni = fmap (PM.evalPolynomial PM.evalMonomial varMap) <$> f_sps + +padDecomposition :: forall d f . + ( MultiplicativeMonoid f + , AdditiveMonoid f + , KnownNat (d+1) + ) => f -> V.Vector (d+1) [f] -> [f] +padDecomposition pad = foldl' (P.zipWith (+)) (P.repeat zero) . V.mapWithIx (\j p -> ((pad ^ (d -! j)) * ) <$> p) + where + d = value @(d+1) -! 1 + +-- | Decomposes an algebraic map into homogenous degree-j maps for j from 0 to @d@ +-- +degreeDecomposition :: forall d f v . KnownNat (d+1) => [Poly f v Natural] -> V.Vector (d+1) [Poly f v Natural] +degreeDecomposition lmap = tabulate (degree_j . toConstant) + where + degree_j :: Natural -> [Poly f v Natural] + degree_j j = P.fmap (leaveDeg j) lmap + + leaveDeg :: Natural -> PM.Poly f v Natural -> PM.Poly f v Natural + leaveDeg j (PM.P monomials) = PM.P $ P.filter (\(_, m) -> deg m == j) monomials + +deg :: PM.Mono v Natural -> Natural +deg (PM.M m) = sum m diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs new file mode 100644 index 000000000..cfa084d40 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Commit.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module ZkFold.Base.Protocol.IVC.Commit (Commit (..), HomomorphicCommit (..), PedersonSetup (..)) where + +import Data.Functor.Constant (Constant (..)) +import Data.Zip (Zip (..)) +import Prelude hiding (Num (..), sum, take, zipWith) +import System.Random (Random (..), mkStdGen) + +import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Algebra.Basic.Number +import ZkFold.Base.Algebra.EllipticCurve.Class +import ZkFold.Base.Data.Vector (Vector, unsafeToVector) +import ZkFold.Base.Protocol.IVC.Oracle +import ZkFold.Prelude (take) + +-- | Commit to the object @a@ with commitment key @ck@ and results of type @f@ +-- +class Commit algo a f where + commit :: a -> f + +instance RandomOracle algo a x => Commit algo a x where + commit = oracle @algo + +-- | Homomorphic commitment scheme, i.e. (hcommit x) * (hcommit y) == hcommit (x + y) +-- +class AdditiveGroup c => HomomorphicCommit a c where + hcommit :: a -> c + +class PedersonSetup s c where + groupElements :: s c + +type PedersonSetupMaxSize = 100 + +instance (EllipticCurve curve, Random (ScalarField curve)) => PedersonSetup [] (Point curve) where + groupElements = + -- TODO: This is just for testing purposes! Not to be used in production + let x = fst $ random $ mkStdGen 0 :: ScalarField curve + in take (value @PedersonSetupMaxSize) $ iterate (mul x) gen + +instance (KnownNat n, EllipticCurve curve, Random (ScalarField curve), n <= PedersonSetupMaxSize) => PedersonSetup (Vector n) (Point curve) where + groupElements = + -- TODO: This is just for testing purposes! Not to be used in production + unsafeToVector $ take (value @n) $ groupElements @[] + +instance (PedersonSetup s (Point curve), Functor s) => PedersonSetup s (Constant (Point curve) a) where + groupElements = Constant <$> groupElements @s + +instance (PedersonSetup s c, Zip s, Foldable s, Scale f c, AdditiveGroup c) => HomomorphicCommit (s f) c where + hcommit v = sum $ zipWith scale v groupElements diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/CommitOpen.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/CommitOpen.hs new file mode 100644 index 000000000..bd10da54b --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/CommitOpen.hs @@ -0,0 +1,25 @@ +module ZkFold.Base.Protocol.IVC.CommitOpen where + +import Data.Zip (zipWith) +import Prelude hiding (Num (..), length, pi, tail, zipWith, (&&)) + +import ZkFold.Base.Algebra.Basic.Class (AdditiveGroup (..)) +import ZkFold.Base.Data.Vector (Vector) +import ZkFold.Base.Protocol.IVC.Commit (HomomorphicCommit (hcommit)) +import ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..)) + +type CommitOpen k i p c m o f = SpecialSoundProtocol k i p (m, c f) (Vector k (c f), o) f + +commitOpen :: HomomorphicCommit m (c f) => SpecialSoundProtocol k i p m o f -> CommitOpen k i p c m o f +commitOpen SpecialSoundProtocol {..} = + let + prover' pi0 w r i = + let m = prover pi0 w r i + in (m, hcommit m) + + verifier' pi pms rs = + let ms = fmap fst pms + cs = fmap snd pms + in (zipWith (-) (fmap hcommit ms) cs, verifier pi ms rs) + in + SpecialSoundProtocol input prover' verifier' diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/FiatShamir.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/FiatShamir.hs new file mode 100644 index 000000000..1a08c751e --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/FiatShamir.hs @@ -0,0 +1,48 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.FiatShamir where + +import Data.Constraint (withDict) +import Data.Constraint.Nat (plusMinusInverse1) +import Prelude hiding (Bool (..), Eq (..), init, length, pi, scanl, unzip) + +import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (-)) +import ZkFold.Base.Data.Vector (Vector, init, item, scanl, unfold) +import ZkFold.Base.Protocol.IVC.CommitOpen +import ZkFold.Base.Protocol.IVC.Oracle (HashAlgorithm, RandomOracle (..)) +import ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..)) + +type FiatShamir k i p c m o f = SpecialSoundProtocol 1 i p (Vector k (m, c f)) (Vector k (c f), o) f + +-- The transcript of the Fiat-Shamired protocol (ignoring the last round) +transcript :: forall algo k c f . + ( HashAlgorithm algo f + , RandomOracle algo f f + , RandomOracle algo (c f) f + ) => f -> Vector k (c f) -> Vector (k-1) f +transcript r0 cs = withDict (plusMinusInverse1 @1 @k) $ init $ init $ scanl (curry (oracle @algo)) r0 cs + +fiatShamir :: forall algo k i p c m o f . + ( KnownNat k + , HashAlgorithm algo f + , RandomOracle algo f f + , RandomOracle algo (i f) f + , RandomOracle algo (c f) f + ) => CommitOpen k i p c m o f -> FiatShamir k i p c m o f +fiatShamir SpecialSoundProtocol {..} = + let + prover' pi0 w _ _ = + let r0 = oracle @algo pi0 + f (r, k) = + let (m', c') = prover pi0 w r k + in ((m', c'), (oracle @algo (r, c'), k + 1)) + in unfold f (r0, 1) + + verifier' pi pms' _ = + let pms = item pms' + r0 = oracle @algo pi :: f + rs = transcript @algo r0 $ fmap snd pms + in verifier pi pms rs + in + SpecialSoundProtocol input prover' verifier' diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Internal.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Internal.hs new file mode 100644 index 000000000..d0e5f24ec --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Internal.hs @@ -0,0 +1,184 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeOperators #-} + +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Redundant ^." #-} + +module ZkFold.Base.Protocol.IVC.Internal where + +import Control.DeepSeq (NFData) +import Control.Lens ((^.)) +import Control.Lens.Combinators (makeLenses) +import Data.Functor.Rep (Representable (..)) +import Data.Type.Equality (type (~)) +import Data.Zip (Zip (..), unzip) +import GHC.Generics (Generic, U1, (:*:)) +import Prelude (Show, const, ($)) + +import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (+)) +import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec) +import ZkFold.Base.Data.Vector (Vector, singleton) +import ZkFold.Base.Protocol.IVC.Accumulator hiding (pi) +import qualified ZkFold.Base.Protocol.IVC.AccumulatorScheme as Acc +import ZkFold.Base.Protocol.IVC.AccumulatorScheme (AccumulatorScheme, accumulatorScheme) +import ZkFold.Base.Protocol.IVC.Commit (HomomorphicCommit) +import ZkFold.Base.Protocol.IVC.CommitOpen +import ZkFold.Base.Protocol.IVC.FiatShamir +import ZkFold.Base.Protocol.IVC.NARK (NARKInstanceProof (..), NARKProof (..)) +import ZkFold.Base.Protocol.IVC.Oracle +import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..), predicate) +import ZkFold.Base.Protocol.IVC.RecursiveFunction +import ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..), specialSoundProtocol, + specialSoundProtocol') +import ZkFold.Base.Protocol.IVC.StepFunction (StepFunction) +import ZkFold.Symbolic.Compiler (ArithmeticCircuit) +import ZkFold.Symbolic.Data.FieldElement (FieldElement) +import ZkFold.Symbolic.Interpreter (Interpreter) + +-- | The recursion circuit satisfiability proof. +data IVCProof k c f + = IVCProof + { _proofX :: Vector k (c f) + -- ^ The commitment to the witness of the recursion circuit satisfiability proof. + , _proofW :: Vector k [f] + -- ^ The witness of the recursion circuit satisfiability proof. + } deriving (GHC.Generics.Generic, Show, NFData) + +makeLenses ''IVCProof + +noIVCProof :: forall k c f . + ( KnownNat k + , AdditiveMonoid (c f) + , AdditiveMonoid f + ) => IVCProof k c f +noIVCProof = IVCProof (tabulate $ const zero) (tabulate $ const zero) + +-- | The current result of recursion together with the first iteration flag, +-- the corresponding accumulator, and the recursion circuit satisfiability proof. +data IVCResult k i c f + = IVCResult + { _z :: i f + , _acc :: Accumulator k (RecursiveI i) c f + , _proof :: IVCProof k c f + } deriving (GHC.Generics.Generic, Show, NFData) + +makeLenses ''IVCResult + +type IVCAssumptions ctx0 ctx1 algo d k a i p c f = + ( RecursivePredicateAssumptions algo d k a i p c + , KnownNat (d+1) + , k ~ 1 + , Zip i + , Field f + , HashAlgorithm algo f + , RandomOracle algo f f + , RandomOracle algo (i f) f + , RandomOracle algo (c f) f + , HomomorphicCommit [f] (c f) + , Scale a f + , Scale a (PolyVec f (d+1)) + , Scale f (c f) + , ctx0 ~ Interpreter a + , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0 + , ctx1 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1 + , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx1) ctx1 + ) + +-- | Create the first IVC result +-- +-- It differs from the rest of the iterations as we don't have anything accumulated just yet. +ivcSetup :: forall ctx0 ctx1 algo d k a i p c . IVCAssumptions ctx0 ctx1 algo d k a i p c a + => StepFunction a i p + -> i a + -> p a + -> IVCResult k i c a +ivcSetup f z0 witness = + let + p :: Predicate a i p + p = predicate f + + z1 :: i a + z1 = predicateEval p z0 witness + + pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c) + pRec = recursivePredicate @algo $ recursiveFunction @algo f + in + IVCResult z1 (emptyAccumulator @d pRec) noIVCProof + +ivcProve :: forall ctx0 ctx1 algo d k a i p c . IVCAssumptions ctx0 ctx1 algo d k a i p c a + => StepFunction a i p + -> IVCResult k i c a + -> p a + -> IVCResult k i c a +ivcProve f res witness = + let + p :: Predicate a i p + p = predicate f + + z' :: i a + z' = predicateEval p (res^.z) witness + + pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c) + pRec = recursivePredicate @algo $ recursiveFunction @algo f + + input :: RecursiveI i a + input = RecursiveI (res^.z) (oracle @algo $ res^.acc^.x) + + messages :: Vector k [a] + messages = res^.proof^.proofW + + commits :: Vector k (c a) + commits = res^.proof^.proofX + + narkIP :: NARKInstanceProof k (RecursiveI i) c a + narkIP = NARKInstanceProof input (NARKProof commits messages) + + accScheme :: AccumulatorScheme d k (RecursiveI i) c a + accScheme = accumulatorScheme @algo @d pRec + + (acc', pf) = Acc.prover accScheme (res^.acc) narkIP + + payload :: RecursiveP d k i p c a + payload = RecursiveP witness commits (res^.acc^.x) one pf + + protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [a] [a] a + protocol = fiatShamir @algo $ commitOpen $ specialSoundProtocol @d pRec + + (messages', commits') = unzip $ prover protocol input payload zero 0 + + ivcProof :: IVCProof k c a + ivcProof = IVCProof commits' messages' + in + IVCResult z' acc' ivcProof + +ivcVerify :: forall ctx0 ctx1 algo d k a i p c f . IVCAssumptions ctx0 ctx1 algo d k a i p c f + => StepFunction a i p + -> IVCResult k i c f + -> ((Vector k (c f), [f]), (Vector k (c f), c f)) +ivcVerify f res = + let + pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c) + pRec = recursivePredicate @algo $ recursiveFunction @algo f + + input :: RecursiveI i f + input = RecursiveI (res^.z) (oracle @algo $ res^.acc^.x) + + messages :: Vector k [f] + messages = res^.proof^.proofW + + commits :: Vector k (c f) + commits = res^.proof^.proofX + + accScheme :: AccumulatorScheme d k (RecursiveI i) c f + accScheme = accumulatorScheme @algo @d pRec + + protocol :: FiatShamir k (RecursiveI i) (RecursiveP d k i p c) c [f] [f] f + protocol = fiatShamir @algo $ commitOpen $ specialSoundProtocol' @d pRec + in + ( verifier protocol input (singleton $ zip messages commits) zero + , Acc.decider accScheme (res^.acc) + ) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/NARK.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/NARK.hs new file mode 100644 index 000000000..4d8f77c99 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/NARK.hs @@ -0,0 +1,41 @@ +{-# LANGUAGE DeriveAnyClass #-} + +module ZkFold.Base.Protocol.IVC.NARK where + +import Control.DeepSeq (NFData (..)) +import Data.Zip (unzip) +import GHC.Generics +import Prelude hiding (head, length, pi, unzip) + +import ZkFold.Base.Algebra.Basic.Class (Ring, zero) +import ZkFold.Base.Data.Vector (Vector) +import ZkFold.Base.Protocol.IVC.FiatShamir (FiatShamir) +import ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol (..)) + +-- Page 18, section 3.4, The accumulation predicate +-- +data NARKProof k c f + = NARKProof + { narkCommits :: Vector k (c f) -- Commits [C_i] ∈ C^k + , narkWitness :: Vector k [f] -- prover messages in the special-sound protocol [m_i] + } + deriving (Show, Generic, NFData) + +narkProof :: Ring f + => FiatShamir k i p c [f] o f + -> i f + -> p f + -> NARKProof k c f +narkProof a pi0 w = + let (narkWitness, narkCommits) = unzip $ prover a pi0 w zero 0 + in NARKProof {..} + +data NARKInstanceProof k i c f = NARKInstanceProof (i f) (NARKProof k c f) + deriving (Show, Generic, NFData) + +narkInstanceProof :: Ring f + => FiatShamir k i p c [f] o f + -> i f + -> p f + -> NARKInstanceProof k i c f +narkInstanceProof a pi0 w = NARKInstanceProof (input a pi0 w) (narkProof a pi0 w) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Oracle.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Oracle.hs new file mode 100644 index 000000000..d90646d52 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Oracle.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +module ZkFold.Base.Protocol.IVC.Oracle where + +import qualified Data.Vector as V +import GHC.Generics +import Prelude (map, (.)) +import qualified Prelude as P + +import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Symbolic.Algorithms.Hash.MiMC (mimcHashN) +import ZkFold.Symbolic.Algorithms.Hash.MiMC.Constants (mimcConstants) + +-- TODO: add more specific instances for efficiency + +class HashAlgorithm algo a where + hash :: [a] -> a + +data MiMCHash +instance Ring a => HashAlgorithm MiMCHash a where + hash = mimcHashN @a mimcConstants zero + +class RandomOracle algo x a where + oracle :: x -> a + default oracle :: (Generic x, RandomOracle' algo (Rep x) a) => x -> a + oracle = oracle' @algo . from + +instance (FromConstant P.Integer a, HashAlgorithm algo a) => RandomOracle algo P.Integer a where + oracle = oracle @algo @a . fromConstant + +instance HashAlgorithm algo a => RandomOracle algo a a where + oracle x = hash @algo [x] + +instance HashAlgorithm algo a => RandomOracle algo (a, a) a where + oracle (x, y) = hash @algo [x, y] + +instance HashAlgorithm algo a => RandomOracle algo [a] a where + oracle = hash @algo + +instance (HashAlgorithm algo b, RandomOracle algo a b) => RandomOracle algo [a] b where + oracle = hash @algo . map (oracle @algo) + +instance (HashAlgorithm algo b, RandomOracle algo a b) => RandomOracle algo (V.Vector a) b where + oracle = (oracle @algo) . V.toList + +instance {-# OVERLAPPABLE #-} (Generic x, RandomOracle' algo (Rep x) a) => RandomOracle algo x a + +class RandomOracle' algo f a where + oracle' :: f x -> a + +-- TODO: fix this instance +instance (RandomOracle' algo f b, RandomOracle' algo g b, HashAlgorithm algo b, Ring b) => RandomOracle' algo (f :+: g) b where + oracle' (L1 x) = hash @algo [zero, oracle' @algo x] + oracle' (R1 x) = oracle' @algo x + +instance (RandomOracle' algo f a, RandomOracle' algo g a, HashAlgorithm algo a) => RandomOracle' algo (f :*: g) a where + oracle' (x :*: y) = + let z1 = oracle' @algo x :: a + z2 = oracle' @algo y :: a + in hash @algo [z1, z2] + +instance RandomOracle algo c a => RandomOracle' algo (Rec0 c) a where + oracle' (K1 x) = oracle @algo x + +-- | Handling constructors with no fields. +instance {-# OVERLAPPING #-} + Ring a => RandomOracle' algo (M1 C ('MetaCons conName fixity selectors) U1) a where + oracle' _ = zero + +instance RandomOracle' algo f a => RandomOracle' algo (M1 c m f) a where + oracle' (M1 x) = oracle' @algo x diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/Predicate.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Predicate.hs new file mode 100644 index 000000000..c29bb3dca --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/Predicate.hs @@ -0,0 +1,49 @@ +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.Predicate where + +import Data.Binary (Binary) +import GHC.Generics (U1 (..), (:*:) (..)) +import Prelude hiding (Num (..), drop, head, replicate, take, zipWith) + +import ZkFold.Base.Data.Package (packed, unpacked) +import ZkFold.Base.Protocol.IVC.StepFunction (FunctorAssumptions, StepFunction, StepFunctionAssumptions) +import ZkFold.Symbolic.Class +import ZkFold.Symbolic.Compiler (ArithmeticCircuit, compileWith, guessOutput, hlmap) +import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) +import ZkFold.Symbolic.Interpreter (Interpreter (..)) + +type PredicateCircuit a i p = ArithmeticCircuit a (i :*: p) i U1 + +data Predicate a i p = Predicate + { predicateEval :: i a -> p a -> i a + , predicateCircuit :: PredicateCircuit a i p + } + +type PredicateAssumptions a i p = + ( Arithmetic a + , Binary a + , FunctorAssumptions i + , FunctorAssumptions p + ) + +predicate :: forall a i p . PredicateAssumptions a i p + => StepFunction a i p -> Predicate a i p +predicate func = + let + func' :: forall f ctx . StepFunctionAssumptions a f ctx => ctx i -> ctx p -> ctx i + func' x' u' = + let + x = FieldElement <$> unpacked x' + u = FieldElement <$> unpacked u' + in + packed . fmap fromFieldElement $ func x u + + predicateEval :: i a -> p a -> i a + predicateEval x u = runInterpreter $ func' (Interpreter x) (Interpreter u) + + predicateCircuit :: PredicateCircuit a i p + predicateCircuit = + hlmap (U1 :*:) $ + compileWith @a guessOutput (\(i :*: p) U1 -> (U1 :*: U1 :*: U1, i :*: p :*: U1)) func' + in Predicate {..} diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/RecursiveFunction.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/RecursiveFunction.hs new file mode 100644 index 000000000..00e61cce4 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/RecursiveFunction.hs @@ -0,0 +1,165 @@ +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE UndecidableInstances #-} + +{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-} + +{-# HLINT ignore "Redundant ^." #-} + +module ZkFold.Base.Protocol.IVC.RecursiveFunction where + +import Control.DeepSeq (NFData) +import Data.Distributive (Distributive (..)) +import Data.Functor.Rep (Representable (..), collectRep, distributeRep) +import Data.These (These (..)) +import Data.Zip (Semialign (..), Zip (..)) +import GHC.Generics (Generic, Generic1, U1 (..), (:*:) (..)) +import Prelude (Foldable, Functor, Show, Traversable, fmap, type (~), ($), + (.), (<$>)) + +import ZkFold.Base.Algebra.Basic.Class (Scale, zero) +import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (+), type (-)) +import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec) +import ZkFold.Base.Data.Orphans () +import ZkFold.Base.Data.Package (packed, unpacked) +import ZkFold.Base.Data.Vector (Vector) +import ZkFold.Base.Protocol.IVC.Accumulator hiding (pi, x) +import ZkFold.Base.Protocol.IVC.AccumulatorScheme (AccumulatorScheme (..), accumulatorScheme) +import ZkFold.Base.Protocol.IVC.Commit (HomomorphicCommit) +import ZkFold.Base.Protocol.IVC.Oracle +import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..), PredicateAssumptions, PredicateCircuit, + predicate) +import ZkFold.Base.Protocol.IVC.StepFunction (FunctorAssumptions, StepFunction, StepFunctionAssumptions) +import ZkFold.Symbolic.Compiler (ArithmeticCircuit, compileWith, guessOutput, hlmap) +import ZkFold.Symbolic.Data.Bool (Bool (..)) +import ZkFold.Symbolic.Data.Class (SymbolicData (..)) +import ZkFold.Symbolic.Data.Conditional (bool) +import ZkFold.Symbolic.Data.FieldElement (FieldElement (FieldElement), fromFieldElement) +import ZkFold.Symbolic.Data.Input (SymbolicInput) +import ZkFold.Symbolic.Interpreter (Interpreter (..)) + +-- | Public input to the recursive function +data RecursiveI i f = RecursiveI (i f) f + deriving (Generic, Generic1, Show, NFData, Functor, Foldable, Traversable) + +instance Semialign i => Semialign (RecursiveI i) where + alignWith f (RecursiveI x h) (RecursiveI y h') = RecursiveI (alignWith f x y) (f (These h h')) + +instance Zip i => Zip (RecursiveI i) where + zipWith f (RecursiveI x h) (RecursiveI y h') = RecursiveI (zipWith f x y) (f h h') + +instance Representable i => Distributive (RecursiveI i) where + distribute = distributeRep + collect = collectRep + +instance Representable i => Representable (RecursiveI i) + +instance (HashAlgorithm algo f, RandomOracle algo f f, RandomOracle algo (i f) f) => RandomOracle algo (RecursiveI i f) f + +instance (SymbolicData f, SymbolicData (i f), Context f ~ Context (i f), Support f ~ Support (i f)) => SymbolicData (RecursiveI i f) + +instance (SymbolicInput f, SymbolicInput (i f), Context f ~ Context (i f)) => SymbolicInput (RecursiveI i f) + +-- | Payload to the recursive function +data RecursiveP d k i p c f = RecursiveP (p f) (Vector k (c f)) (AccumulatorInstance k (RecursiveI i) c f) f (Vector (d-1) (c f)) + deriving (Generic, Generic1, Functor, Foldable, Traversable) + +instance (KnownNat (d-1), KnownNat (k-1), KnownNat k, Representable i, Representable p, Representable c) => Distributive (RecursiveP d k i p c) where + distribute = distributeRep + collect = collectRep + +instance (KnownNat (d-1), KnownNat (k-1), KnownNat k, Representable i, Representable p, Representable c) => Representable (RecursiveP d k i p c) + +type RecursiveFunctionAssumptions algo d a i c f ctx = + ( StepFunctionAssumptions a f ctx + , HashAlgorithm algo f + , RandomOracle algo f f + , RandomOracle algo (i f) f + , RandomOracle algo (c f) f + , HomomorphicCommit [f] (c f) + , Scale a f + , Scale a (PolyVec f (d+1)) + , Scale f (c f) + ) + +type RecursiveFunction algo d k a i p c = forall f ctx . RecursiveFunctionAssumptions algo d a i c f ctx + => RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f + +-- | Transform a step function into a recursive function +recursiveFunction :: forall algo d k a i p c . + ( PredicateAssumptions a i p + , FunctorAssumptions c + , KnownNat (d-1) + , KnownNat (d+1) + , KnownNat (k-1) + , KnownNat k + , Zip i + ) => StepFunction a i p -> RecursiveFunction algo d k a i p c +recursiveFunction func = + let + -- A helper function to derive the accumulator scheme + func' :: forall ctx f . StepFunctionAssumptions a f ctx => RecursiveI i f -> RecursiveP d k i p c f -> RecursiveI i f + func' (RecursiveI x h) (RecursiveP u _ _ _ _) = RecursiveI (func x u) h + + -- A helper predicate to derive the accumulator scheme + pRec :: Predicate a (RecursiveI i) (RecursiveP d k i p c) + pRec = predicate func' + + funcRecursive :: forall ctx f . RecursiveFunctionAssumptions algo d a i c f ctx + => RecursiveI i f + -> RecursiveP d k i p c f + -> RecursiveI i f + funcRecursive z@(RecursiveI x _) (RecursiveP u piX accX flag pf) = + let + accScheme :: AccumulatorScheme d k (RecursiveI i) c f + accScheme = accumulatorScheme @algo pRec + + x' :: i f + x' = func x u + + accX' :: AccumulatorInstance k (RecursiveI i) c f + accX' = verifier accScheme z piX accX pf + + h :: f + h = bool zero (oracle @algo accX') $ Bool $ fromFieldElement flag + in + RecursiveI x' h + + in funcRecursive + +-------------------------------------------------------------------------------- + +type RecursivePredicateAssumptions algo d k a i p c = + ( KnownNat (d-1) + , KnownNat (k-1) + , KnownNat k + , PredicateAssumptions a i p + , FunctorAssumptions c + ) + +recursivePredicate :: forall algo d k a i p c ctx0 ctx1 . + ( RecursivePredicateAssumptions algo d k a i p c + , ctx0 ~ Interpreter a + , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx0) ctx0 + , ctx1 ~ ArithmeticCircuit a (RecursiveI i :*: RecursiveP d k i p c) U1 + , RecursiveFunctionAssumptions algo d a i c (FieldElement ctx1) ctx1 + ) => RecursiveFunction algo d k a i p c -> Predicate a (RecursiveI i) (RecursiveP d k i p c) +recursivePredicate func = + let + func' :: forall f ctx . RecursiveFunctionAssumptions algo d a i c f ctx + => ctx (RecursiveI i) -> ctx (RecursiveP d k i p c) -> ctx (RecursiveI i) + func' x' u' = + let + x = FieldElement <$> unpacked x' + u = FieldElement <$> unpacked u' + in + packed . fmap fromFieldElement $ func x u + + predicateEval :: (RecursiveI i) a -> (RecursiveP d k i p c) a -> (RecursiveI i) a + predicateEval z u = runInterpreter $ func' (Interpreter z) (Interpreter u) + + predicateCircuit :: PredicateCircuit a (RecursiveI i) (RecursiveP d k i p c) + predicateCircuit = + hlmap (U1 :*:) $ + compileWith @a guessOutput (\(i :*: p) U1 -> (U1 :*: U1 :*: U1, i :*: p :*: U1)) func' + in Predicate {..} diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/SpecialSound.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/SpecialSound.hs new file mode 100644 index 000000000..d5046cb41 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/SpecialSound.hs @@ -0,0 +1,77 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.SpecialSound where + +import Data.Functor.Rep (Representable (..)) +import Data.Map.Strict (elems) +import GHC.Generics ((:*:) (..)) +import Prelude (undefined, ($)) + +import ZkFold.Base.Algebra.Basic.Class +import ZkFold.Base.Algebra.Basic.Number +import ZkFold.Base.Data.Vector (Vector) +import qualified ZkFold.Base.Protocol.IVC.AlgebraicMap as AM +import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..)) +import ZkFold.Symbolic.Class +import ZkFold.Symbolic.Compiler + +{-- | Section 3.1 + +The protocol Πsps has 3 essential parameters k, d, l ∈ N, meaning that Πsps is a (2k − 1)- +move protocol with verifier degree d and output length l (i.e. the verifier checks l degree +d algebraic equations). In each round i (1 ≤ i ≤ k), the prover Psps(pi, w, [mj , rj], j=1 to i-1) +generates the next message mi on input the public input pi, the witness w, and the current +transcript [mj , rj], j=1 to i-1, and sends mi to the verifier; the verifier replies with a random +challenge ri ∈ F. After the final message mk, the verifier computes the algebraic map Vsps +and checks that the output is a zero vector of length l. + +--} + +data SpecialSoundProtocol k i p m o f = SpecialSoundProtocol + { + input :: + i f -- ^ previous public input + -> p f -- ^ witness + -> i f -- ^ public input + + , prover :: + i f -- ^ previous public input + -> p f -- ^ witness + -> f -- ^ current random challenge + -> Natural -- ^ round number (starting from 1) + -> m -- ^ prover message + + , verifier :: + i f -- ^ public input + -> Vector k m -- ^ prover messages + -> Vector (k-1) f -- ^ random challenges + -> o -- ^ verifier output + } + +specialSoundProtocol :: forall d a i p . + ( KnownNat (d+1) + , Arithmetic a + , Representable i + , Representable p + ) => Predicate a i p -> SpecialSoundProtocol 1 i p [a] [a] a +specialSoundProtocol phi@Predicate {..} = + let + prover pi0 w _ _ = elems $ witnessGenerator predicateCircuit (pi0 :*: w) (predicateEval pi0 w) + + verifier pi pm ts = AM.algebraicMap @d phi pi pm ts one + in + SpecialSoundProtocol predicateEval prover verifier + +specialSoundProtocol' :: forall d a i p f . + ( KnownNat (d+1) + , Representable i + , Ring f + , Scale a f + ) => Predicate a i p -> SpecialSoundProtocol 1 i p [f] [f] f +specialSoundProtocol' phi = + let + verifier pi pm ts = AM.algebraicMap @d phi pi pm ts one + in + SpecialSoundProtocol undefined undefined verifier + diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/StepFunction.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/StepFunction.hs new file mode 100644 index 000000000..029327aa7 --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/StepFunction.hs @@ -0,0 +1,28 @@ +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.StepFunction where + +import Control.DeepSeq (NFData) +import Data.Binary (Binary) +import Data.Functor.Rep (Representable (..)) +import Prelude hiding (Num (..), drop, head, replicate, take, zipWith) + +import ZkFold.Symbolic.Class +import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) + +type FunctorAssumptions f = + ( Representable f + , Traversable f + , NFData (Rep f) + , Binary (Rep f) + , Ord (Rep f) + ) + +type StepFunctionAssumptions a f ctx = + ( Symbolic ctx + , BaseField ctx ~ a + , FieldElement ctx ~ f + ) + +type StepFunction a i p = forall f ctx . StepFunctionAssumptions a f ctx + => i f -> p f -> i f diff --git a/symbolic-base/src/ZkFold/Base/Protocol/IVC/VerifierCircuit.hs b/symbolic-base/src/ZkFold/Base/Protocol/IVC/VerifierCircuit.hs new file mode 100644 index 000000000..960e1aacc --- /dev/null +++ b/symbolic-base/src/ZkFold/Base/Protocol/IVC/VerifierCircuit.hs @@ -0,0 +1,70 @@ +{-# LANGUAGE AllowAmbiguousTypes #-} +{-# LANGUAGE TypeOperators #-} + +module ZkFold.Base.Protocol.IVC.VerifierCircuit where + +-- import GHC.Generics (Par1 (..), U1 (..), type (:.:) (..), (:*:) (..)) +-- import Prelude hiding (Num (..), drop, head, replicate, take, zipWith) + +-- import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (+), type (-)) +-- import ZkFold.Base.Data.ByteString (Binary) +-- import ZkFold.Base.Data.Vector (Vector) +-- import ZkFold.Base.Protocol.IVC.Commit (HomomorphicCommit) +-- import ZkFold.Base.Protocol.IVC.CommitOpen (CommitOpen (..)) +-- import ZkFold.Base.Protocol.IVC.FiatShamir (FiatShamir (..)) +-- import ZkFold.Base.Protocol.IVC.Internal (IVCResult, ivcVerify, RecursiveI, RecursiveP) +-- import ZkFold.Base.Protocol.IVC.Oracle (HashAlgorithm) +-- import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..), predicate) +-- import ZkFold.Symbolic.Class +-- import ZkFold.Symbolic.Compiler +-- import ZkFold.Symbolic.Data.Class (SymbolicData (..)) +-- import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) +-- import ZkFold.Symbolic.Data.Input (SymbolicInput) +-- import ZkFold.Base.Protocol.IVC.SpecialSound (SpecialSoundProtocol(..)) + +-- -- | Takes a function `f` and returns a circuit `C` with input `y` and witness `w`. +-- -- The circuit is such that `C(y, w) = 0` implies that `y = x(n)` for some positive `n` where +-- -- `x(k+1) = f(x(k), u(k))` for all `k` and some `u`. +-- ivcVerifierCircuit :: forall f i p m c d k a payload input output nx nu ctx algo . +-- ( f ~ FieldElement ctx +-- , i ~ Vector nx +-- , p ~ Vector nu +-- , m ~ [f] +-- , c ~ f +-- , HashAlgorithm algo f +-- , HomomorphicCommit m c +-- , KnownNat (d - 1) +-- , KnownNat (d + 1) +-- , KnownNat k +-- , KnownNat (k - 1) +-- , Binary a +-- , Arithmetic a +-- , KnownNat nx +-- , KnownNat nu +-- , ctx ~ ArithmeticCircuit a payload input +-- , SymbolicInput (IVCResult f i m c k) +-- , Context (IVCResult f i m c k) ~ ctx +-- -- , payload ~ (Payload (IVCResult f i m c k) :*: U1) +-- -- , input ~ (Layout (IVCResult f i m c k) :*: U1) +-- -- , output ~ (((Par1 :*: (Vector nx :.: Par1)) :*: ((Vector (k - 1) :.: Par1) :*: ((Vector k :.: Par1) :*: Par1))) :*: ((Vector k :.: Par1) :*: Par1)) +-- ) => (forall ctx' . Symbolic ctx' => Vector nx (FieldElement ctx') -> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')) +-- -> ArithmeticCircuit a payload input output +-- ivcVerifierCircuit func = +-- let +-- -- Protostar IVC takes an arithmetizable function as input. +-- p :: Predicate a (Vector nx) (Vector nu) +-- p = predicate func + +-- -- The Fiat-Shamired commit-open special-sound protocol for the arithmetizable function +-- fs :: FiatShamir algo (CommitOpen (Predicate a (Vector nx) (Vector nu))) +-- fs = FiatShamir (CommitOpen p) + +-- -- The verification function for the IVC result object +-- vf :: IVCResult f i m c k +-- -> (VerifierOutput f (RecursiveI i c k) (RecursiveP i p c d k) (Vector k (m, c)) c d 1 (FiatShamir algo (CommitOpen (Predicate a (Vector nx) (Vector nu)))), (Vector k c, c)) +-- vf = ivcVerify @f @i @p @m @c @d @k p + +-- -- -- TODO: the circuit functors must be adjusted for better usability +-- -- circuit = compile @a $ ivcVerify @f @i @p @m @c @d @k p +-- circuit = undefined +-- in circuit diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar.hs deleted file mode 100644 index fa1251f52..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar.hs +++ /dev/null @@ -1,3 +0,0 @@ -module ZkFold.Base.Protocol.Protostar (module P) where - -import ZkFold.Base.Protocol.Protostar.IVC as P diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Accumulator.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Accumulator.hs deleted file mode 100644 index 6a6be2af7..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Accumulator.hs +++ /dev/null @@ -1,74 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE TemplateHaskell #-} -{-# LANGUAGE TypeOperators #-} - -module ZkFold.Base.Protocol.Protostar.Accumulator where - -import Control.DeepSeq (NFData (..)) -import Control.Lens ((^.)) -import Control.Lens.Combinators (makeLenses) -import Data.Functor.Rep (Representable (..)) -import GHC.Generics -import Prelude hiding (length, pi) - -import ZkFold.Base.Algebra.Basic.Class (zero) -import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, type (-)) -import ZkFold.Base.Data.Vector (Vector) -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 (FiatShamir)) - --- Page 19, Accumulator instance -data AccumulatorInstance f i c k - = AccumulatorInstance - { _pi :: i f -- pi ∈ M^{l_in} in the paper - , _c :: Vector k c -- [C_i] ∈ C^k in the paper - , _r :: Vector (k-1) f -- [r_i] ∈ F^{k-1} in the paper - , _e :: c -- E ∈ C in the paper - , _mu :: f -- μ ∈ F in the paper - } - deriving (Show, Generic, NFData) - -makeLenses ''AccumulatorInstance - --- 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 f i m c k - = Accumulator - { _x :: AccumulatorInstance f i c k - , _w :: Vector k m - } - deriving (Show, Generic, NFData) - -makeLenses ''Accumulator - -emptyAccumulator :: forall f i m c (d :: Natural) k a . - ( Representable i - , m ~ [f] - , HomomorphicCommit m c - , KnownNat (k-1) - , KnownNat k - , AlgebraicMap f i d a - ) => FiatShamir (CommitOpen a) -> Accumulator f i m c k -emptyAccumulator (FiatShamir (CommitOpen sps)) = - let accW = tabulate (const zero) - aiC = fmap hcommit accW - aiR = tabulate (const zero) - aiMu = zero - aiPI = tabulate (const zero) - aiE = hcommit $ algebraicMap @_ @_ @d sps aiPI accW aiR aiMu - accX = AccumulatorInstance { _pi = aiPI, _c = aiC, _r = aiR, _e = aiE, _mu = aiMu } - in Accumulator accX accW - -emptyAccumulatorInstance :: forall f i m c (d :: Natural) k a . - ( Representable i - , m ~ [f] - , HomomorphicCommit m c - , KnownNat (k-1) - , KnownNat k - , AlgebraicMap f i d a - ) => FiatShamir (CommitOpen a) -> AccumulatorInstance f i c k -emptyAccumulatorInstance fs = emptyAccumulator @_ @_ @_ @_ @d fs ^. x diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AccumulatorScheme.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AccumulatorScheme.hs deleted file mode 100644 index fd73b4a7b..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AccumulatorScheme.hs +++ /dev/null @@ -1,160 +0,0 @@ -{-# 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 sps)) acc (NARKInstanceProof pubi (NARKProof pi_x pi_w)) = - (Accumulator (AccumulatorInstance pi'' ci'' ri'' eCapital' mu') m_i'', pf) - where - r_0 :: f - r_0 = oracle pubi - - -- Fig. 3, step 1 - r_i :: Vector (k-1) f - r_i = transcriptFiatShamir 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 sps 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 (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) - - - verifier pubi c_i acc acc' pf = (muDiff, piDiff, riDiff, ciDiff, eDiff) - where - -- Fig. 4, step 1 - r_i :: Vector (k-1) f - r_i = unsafeToVector $ P.tail $ P.tail $ P.scanl (P.curry oracle) (oracle pubi) $ toList c_i - - -- Fig. 4, step 2 - alpha :: f - alpha = oracle (acc, pubi, c_i, pf) - - -- Fig. 4, step 3 - mu' = alpha + acc^.mu - pi'' = zipWith (+) (fmap (* alpha) pubi) (acc^.pi) - ri'' = zipWith (+) (scale alpha r_i) (acc^.r) - ci'' = zipWith (+) (scale alpha c_i) (acc^.c) - - -- Fig 4, step 4 - muDiff = acc'^.mu - mu' - piDiff = zipWith (-) (acc'^.pi) pi'' - riDiff = zipWith (-) (acc'^.r) ri'' - ciDiff = acc'^.c - ci'' - - -- Fig 4, step 5 - eDiff = acc'^.e - (acc^.e + sum (mapWithIx (\i a -> scale (alpha ^ (i+1)) a) pf)) - - decider (FiatShamir (CommitOpen sps)) acc = (commitsDiff, eDiff) - where - -- 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 sps (acc^.x^.pi) (acc^.w) (acc^.x^.r) (acc^.x^.mu) - - - -- Fig. 5, step 3 - eDiff = (acc^.x^.e) - hcommit err diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AlgebraicMap.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AlgebraicMap.hs deleted file mode 100644 index 683ed7b25..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/AlgebraicMap.hs +++ /dev/null @@ -1,90 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.AlgebraicMap where - -import Data.ByteString (ByteString) -import Data.Functor.Rep (Representable (..)) -import Data.List (foldl') -import Data.Map.Strict (Map, keys) -import qualified Data.Map.Strict as M -import Prelude (fmap, zip, ($), (.), (<$>)) -import qualified Prelude as P - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number -import qualified ZkFold.Base.Algebra.Polynomials.Multivariate as PM -import ZkFold.Base.Algebra.Polynomials.Multivariate -import qualified ZkFold.Base.Data.Vector as V -import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.ArithmetizableFunction (ArithmetizableFunction (..)) -import ZkFold.Symbolic.Class -import ZkFold.Symbolic.Compiler -import ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal -import ZkFold.Symbolic.Data.Eq - --- | Algebraic map of @a@. --- It calculates a system of equations defining @a@ in some way. --- The inputs are polymorphic in a ring element @f@. --- The main application is to define the verifier's algebraic map in the NARK protocol. --- -class (Ring f) => AlgebraicMap f i (d :: Natural) a where - -- | the algebraic map Vsps computed by the NARK verifier. - algebraicMap :: a - -> i f -- ^ public input - -> Vector k [f] -- ^ NARK proof witness (the list of prover messages) - -> Vector (k-1) f -- ^ Verifier random challenges - -> f -- ^ Slack variable for padding - -> [f] - -instance - ( Ring f - , Representable i - , KnownNat (d + 1) - , Arithmetic a - , Scale a f - ) => AlgebraicMap f i d (ArithmetizableFunction a i p) where - -- We can use the polynomial system from the circuit as a base for Vsps. - -- - algebraicMap ArithmetizableFunction {..} pi pm _ pad = padDecomposition pad f_sps_uni - where - sys :: [PM.Poly a (SysVar i) Natural] - sys = M.elems (acSystem afCircuit) - - witness :: Map ByteString f - witness = M.fromList $ zip (keys $ acWitness afCircuit) (V.head pm) - - varMap :: SysVar i -> f - varMap (InVar inV) = index pi inV - varMap (NewVar newV) = M.findWithDefault zero newV witness - - f_sps :: Vector (d+1) [PM.Poly a (SysVar i) Natural] - f_sps = degreeDecomposition @_ @d $ sys - - f_sps_uni :: Vector (d+1) [f] - f_sps_uni = fmap (PM.evalPolynomial PM.evalMonomial varMap) <$> f_sps - - -padDecomposition :: forall f n . - ( MultiplicativeMonoid f - , AdditiveMonoid f - , KnownNat n - ) => f -> V.Vector n [f] -> [f] -padDecomposition pad = foldl' (P.zipWith (+)) (P.repeat zero) . V.mapWithIx (\j p -> ((pad ^ (d -! j)) * ) <$> p) - where - d = value @n -! 1 - --- | Decomposes an algebraic map into homogenous degree-j maps for j from 0 to @d@ --- -degreeDecomposition :: forall f d v . KnownNat (d + 1) => [Poly f v Natural] -> V.Vector (d + 1) [Poly f v Natural] -degreeDecomposition lmap = tabulate (degree_j . toConstant) - where - degree_j :: Natural -> [Poly f v Natural] - degree_j j = P.fmap (leaveDeg j) lmap - - leaveDeg :: Natural -> PM.Poly f v Natural -> PM.Poly f v Natural - leaveDeg j (PM.P monomials) = PM.P $ P.filter (\(_, m) -> deg m == j) monomials - -deg :: PM.Mono v Natural -> Natural -deg (PM.M m) = sum m diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/ArithmetizableFunction.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/ArithmetizableFunction.hs deleted file mode 100644 index 59b9277db..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/ArithmetizableFunction.hs +++ /dev/null @@ -1,12 +0,0 @@ -{-# LANGUAGE TypeOperators #-} - -module ZkFold.Base.Protocol.Protostar.ArithmetizableFunction where - -import GHC.Generics (U1 (..), (:*:) (..)) - -import ZkFold.Symbolic.Compiler - -data ArithmetizableFunction a i p = ArithmetizableFunction - { afEval :: i a -> p a -> i a - , afCircuit :: ArithmeticCircuit a (i :*: p) i U1 - } diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs deleted file mode 100644 index 901255792..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Commit.hs +++ /dev/null @@ -1,52 +0,0 @@ -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.Commit (Commit (..), HomomorphicCommit (..), PedersonSetup (..)) where - -import Data.Zip (zipWith) -import GHC.IsList (IsList (..)) -import Prelude hiding (Num (..), sum, take, zipWith) -import System.Random (Random (..), mkStdGen) - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Field (Zp) -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 -import ZkFold.Base.Algebra.EllipticCurve.Class -import ZkFold.Base.Algebra.EllipticCurve.Ed25519 -import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.Oracle -import ZkFold.Prelude (take) - --- | Commit to the object @a@ with commitment key @ck@ and results of type @f@ --- -class Commit a f where - commit :: a -> f - -instance RandomOracle a x => Commit a x where - commit = oracle - --- | Homomorphic commitment scheme, i.e. (hcommit x) * (hcommit y) == hcommit (x + y) --- -class AdditiveGroup c => HomomorphicCommit a c where - hcommit :: a -> c - -class PedersonSetup n c where - groupElements :: Vector n c - -instance KnownNat n => PedersonSetup n (Point BLS12_381_G1) where - groupElements = - -- TODO: This is just for testing purposes! Not to be used in production - let x = fst $ random $ mkStdGen 0 :: Zp BLS12_381_Scalar - in fromList $ take (value @n) $ iterate (scale x) pointGen - -instance KnownNat n => PedersonSetup n (Point Ed25519) where - groupElements = - -- TODO: This is just for testing purposes! Not to be used in production - let x = fst $ random $ mkStdGen 0 :: ScalarField Ed25519 - in fromList $ take (value @n) $ iterate (scale x) pointGen - -instance (PedersonSetup n c, Scale f c, AdditiveGroup c) => HomomorphicCommit (Vector n f) c where - hcommit v = sum $ zipWith scale v groupElements - -instance (PedersonSetup 100 c, Scale f c, AdditiveGroup c) => HomomorphicCommit [f] c where - hcommit v = sum $ zipWith scale v (toList $ groupElements @100) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/CommitOpen.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/CommitOpen.hs deleted file mode 100644 index 8c26efa23..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/CommitOpen.hs +++ /dev/null @@ -1,35 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.CommitOpen where - -import Data.Zip (zipWith) -import Prelude hiding (Num (..), length, pi, tail, zipWith, (&&)) - -import ZkFold.Base.Algebra.Basic.Class (AdditiveGroup (..)) -import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit (hcommit)) -import ZkFold.Base.Protocol.Protostar.Oracle -import ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..)) - -newtype CommitOpen a = CommitOpen a - -instance RandomOracle a b => RandomOracle (CommitOpen a) b where - oracle (CommitOpen a) = oracle a - -instance - ( SpecialSoundProtocol f i p m c d k a - , HomomorphicCommit m c - ) => SpecialSoundProtocol f i p (m, c) c d k (CommitOpen a) where - type VerifierOutput f i p (m, c) c d k (CommitOpen a) = (Vector k c, VerifierOutput f i p m c d k a) - - input (CommitOpen a) = input @_ @_ @_ @m @c @d @k a - - prover (CommitOpen a) pi0 w r i = - let m = prover @f @i @_ @m @c @d @k a pi0 w r i - in (m, hcommit m) - - verifier (CommitOpen a) pi pms rs = - let ms = fmap fst pms - cs = fmap snd pms - in (zipWith (-) (fmap hcommit ms) cs, verifier @f @_ @p @m @c @d @k a pi ms rs) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/FiatShamir.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/FiatShamir.hs deleted file mode 100644 index 9154f6ef6..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/FiatShamir.hs +++ /dev/null @@ -1,49 +0,0 @@ -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.FiatShamir where - -import Data.Constraint (withDict) -import Data.Constraint.Nat (plusMinusInverse1) -import GHC.Generics (Generic) -import Prelude hiding (Bool (..), Eq (..), init, length, pi, scanl, unzip) - -import ZkFold.Base.Algebra.Basic.Class (Ring) -import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (-)) -import ZkFold.Base.Data.Vector (Vector, init, item, scanl, unfold) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit) -import ZkFold.Base.Protocol.Protostar.CommitOpen -import ZkFold.Base.Protocol.Protostar.Oracle (RandomOracle (..)) -import ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..)) - -newtype FiatShamir a = FiatShamir a - deriving Generic - --- The transcript of the Fiat-Shamired protocol (ignoring the last round) -transcriptFiatShamir :: forall f c k . (Ring f, RandomOracle f f, RandomOracle c f) => f -> Vector k c -> Vector (k-1) f -transcriptFiatShamir r0 cs = withDict (plusMinusInverse1 @1 @k) $ init $ init $ scanl (curry (oracle @(f, c))) r0 cs - -instance - ( SpecialSoundProtocol f i p m c d k a - , Ring f - , HomomorphicCommit m c - , RandomOracle (i f) f - , RandomOracle c f - , KnownNat k - ) => SpecialSoundProtocol f i p (Vector k (m, c)) c d 1 (FiatShamir (CommitOpen a)) where - type VerifierOutput f i p (Vector k (m, c)) c d 1 (FiatShamir (CommitOpen a)) = VerifierOutput f i p (m, c) c d k (CommitOpen a) - - input (FiatShamir a) = input @_ @_ @_ @(m, c) @c @d @k a - - prover (FiatShamir a) pi0 w _ _ = - let r0 = oracle pi0 - f (r, k) = - let (m', c') = prover @f @i @_ @(m, c) @c @d @k a pi0 w r k - in ((m', c'), (oracle (r, c'), k + 1)) - in unfold f (r0, 1) - - verifier (FiatShamir a) pi pms' _ = - let pms = item pms' - r0 = oracle pi :: f - rs = transcriptFiatShamir r0 $ fmap snd pms - in verifier @f @i @p @(m, c) @c @d @k a pi pms rs diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/IVC.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/IVC.hs deleted file mode 100644 index 6e313e33f..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/IVC.hs +++ /dev/null @@ -1,105 +0,0 @@ -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE TypeOperators #-} - -module ZkFold.Base.Protocol.Protostar.IVC where - -import Control.DeepSeq (NFData) -import Control.Lens ((^.)) -import Data.Functor.Rep (Representable (..)) -import Data.Type.Equality (type (~)) -import GHC.Generics (Generic) -import Prelude (const, ($)) -import qualified Prelude as P - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number (KnownNat, Natural, type (-)) -import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.Accumulator hiding (pi) -import qualified ZkFold.Base.Protocol.Protostar.AccumulatorScheme as Acc -import ZkFold.Base.Protocol.Protostar.AlgebraicMap (AlgebraicMap) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit) -import ZkFold.Base.Protocol.Protostar.CommitOpen -import ZkFold.Base.Protocol.Protostar.FiatShamir -import ZkFold.Base.Protocol.Protostar.NARK (NARKInstanceProof (..), NARKProof (..), - narkInstanceProof) -import ZkFold.Base.Protocol.Protostar.Oracle -import ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..)) - -data IVCProof f i m c d k - = IVCProof - { ivcpAccumulatorInstance :: AccumulatorInstance f i c k - , ivcpAccumulationProof :: Vector (d-1) c - } deriving (GHC.Generics.Generic) - -deriving instance (P.Show f, P.Show (i f), P.Show m, P.Show c) => P.Show (IVCProof f i m c d k) -deriving instance (NFData f, NFData (i f), NFData m, NFData c) => NFData (IVCProof f i m c d k) - -noIVCProof :: forall f i m c d k a . - ( Representable i - , m ~ [f] - , HomomorphicCommit m c - , KnownNat (d-1) - , KnownNat (k-1) - , KnownNat k - , AlgebraicMap f i d a - ) => FiatShamir (CommitOpen a) -> IVCProof f i m c d k -noIVCProof ac = IVCProof (emptyAccumulatorInstance @_ @_ @_ @_ @d ac) (tabulate $ const zero) - --- | The final result of recursion and the final accumulator. --- Accumulation decider is an arithmetizable function which can be called on the final accumulator. --- -data IVCResult f i m c d k - = IVCResult - { ivcInstance :: i f - , ivcCommits :: Vector k c - , ivcAccumulator :: Accumulator f i m c k - , ivcProof :: IVCProof f i m c d k - } deriving (GHC.Generics.Generic) - -deriving instance (P.Show f, P.Show (i f), P.Show m, P.Show c) => P.Show (IVCResult f i m c d k) -deriving instance (NFData f, NFData (i f), NFData m, NFData c) => NFData (IVCResult f i m c d k) - -ivcInitialize :: forall f i m c (d :: Natural) k a . - ( Representable i - , m ~ [f] - , HomomorphicCommit m c - , KnownNat (d-1) - , KnownNat (k-1) - , KnownNat k - , AlgebraicMap f i d a - ) => FiatShamir (CommitOpen a) -> i f -> IVCResult f i m c d k -ivcInitialize ac pi0 = IVCResult pi0 (tabulate $ const zero) (emptyAccumulator @_ @_ @_ @_ @d ac) (noIVCProof ac) - -ivcIterate :: forall f i p m c (d :: Natural) k a . - ( SpecialSoundProtocol f i p m c d k a - , Ring f - , HomomorphicCommit m c - , RandomOracle (i f) f - , RandomOracle c f - , KnownNat k - , Acc.AccumulatorScheme f i m c d k (FiatShamir (CommitOpen a)) - ) => FiatShamir (CommitOpen a) -> IVCResult f i m c d k -> p f -> IVCResult f i m c d k -ivcIterate fs (IVCResult pi0 _ acc0 _) witness = - let - narkIP@(NARKInstanceProof pi (NARKProof cs _)) = narkInstanceProof @_ @_ @_ @_ @_ @d fs pi0 witness - (acc, pf) = Acc.prover fs acc0 narkIP - proof = IVCProof (acc0^.x) pf - in - IVCResult pi cs acc proof - -ivcVerify :: forall f i m c d k a . - ( Acc.AccumulatorScheme f i m c d k a - ) => a -> IVCResult f i m c d k -> ((f, i f, Vector (k-1) f, Vector k c, c), (Vector k c, c)) -ivcVerify a IVCResult {..} = - let - pi = ivcInstance - cs = ivcCommits - acc = ivcAccumulator - IVCProof {..} = ivcProof - accX = acc^.x - accX0 = ivcpAccumulatorInstance - pf = ivcpAccumulationProof - in - ( Acc.verifier @f @i @m @c @d @k @a pi cs accX0 accX pf - , Acc.decider @f @i @m @c @d @k @a a acc - ) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/NARK.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/NARK.hs deleted file mode 100644 index 14d9ac32f..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/NARK.hs +++ /dev/null @@ -1,52 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE DeriveAnyClass #-} - -module ZkFold.Base.Protocol.Protostar.NARK where - -import Control.DeepSeq (NFData (..)) -import Data.Zip (unzip) -import GHC.Generics -import Prelude hiding (head, length, pi, unzip) - -import ZkFold.Base.Algebra.Basic.Class (Ring) -import ZkFold.Base.Algebra.Basic.Number (KnownNat) -import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit) -import ZkFold.Base.Protocol.Protostar.CommitOpen (CommitOpen (..)) -import ZkFold.Base.Protocol.Protostar.FiatShamir (FiatShamir) -import ZkFold.Base.Protocol.Protostar.Oracle (RandomOracle (..)) -import ZkFold.Base.Protocol.Protostar.SpecialSound (SpecialSoundProtocol (..)) - --- Page 18, section 3.4, The accumulation predicate --- -data NARKProof m c k - = NARKProof - { narkCommits :: Vector k c -- Commits [C_i] ∈ C^k - , narkWitness :: Vector k m -- prover messages in the special-sound protocol [m_i] - } - deriving (Show, Generic, NFData) - -narkProof :: forall f i p m c d k a . - ( SpecialSoundProtocol f i p m c d k a - , Ring f - , HomomorphicCommit m c - , RandomOracle (i f) f - , RandomOracle c f - , KnownNat k - ) => FiatShamir (CommitOpen a) -> i f -> p f -> NARKProof m c k -narkProof a pi0 w = - let (ms, cs) = unzip $ prover @f @i @_ @_ @c @d @1 a pi0 w (oracle pi0) 0 - in NARKProof cs ms - -data NARKInstanceProof f i m c k = NARKInstanceProof (i f) (NARKProof m c k) - deriving (Show, Generic, NFData) - -narkInstanceProof :: forall f i p m c d k a . - ( SpecialSoundProtocol f i p m c d k a - , Ring f - , HomomorphicCommit m c - , RandomOracle (i f) f - , RandomOracle c f - , KnownNat k - ) => FiatShamir (CommitOpen a) -> i f -> p f -> NARKInstanceProof f i m c k -narkInstanceProof a pi0 w = NARKInstanceProof (input @f @i @p @(Vector k (m, c)) @c @d @1 a pi0 w) (narkProof @_ @_ @_ @_ @_ @d a pi0 w) diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Oracle.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Oracle.hs deleted file mode 100644 index 099a389bd..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/Oracle.hs +++ /dev/null @@ -1,67 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE NoOverloadedStrings #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.Oracle where - -import Data.Char (ord) -import Data.Proxy (Proxy (..)) -import qualified Data.Vector as V -import GHC.Generics -import GHC.TypeLits -import Prelude (foldl, ($), (.), (<$>)) -import qualified Prelude as P - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Symbolic.Algorithms.Hash.MiMC (mimcHash2) -import ZkFold.Symbolic.Algorithms.Hash.MiMC.Constants (mimcConstants) - -class RandomOracle a b where - oracle :: a -> b - default oracle :: (Generic a, RandomOracle' (Rep a) b) => a -> b - oracle = oracle' . from - -instance (Ring a, FromConstant P.Integer a) => RandomOracle P.Integer a where - oracle = oracle @a . fromConstant - -instance Ring a => RandomOracle a a where - oracle a = mimcHash2 mimcConstants a zero zero - -instance (Ring b, RandomOracle a b) => RandomOracle [a] b where - oracle = foldl (\acc x -> let y = oracle x in y * acc + y) zero - -instance (Ring b, RandomOracle a b) => RandomOracle (V.Vector a) b where - oracle = foldl (\acc x -> let y = oracle x in y * acc + y) zero - -instance {-# OVERLAPPABLE #-} (Generic a, RandomOracle' (Rep a) b) => RandomOracle a b where - -class RandomOracle' f b where - oracle' :: f a -> b - -instance (RandomOracle' f b, RandomOracle' g b) => RandomOracle' (f :+: g) b where - oracle' (L1 x) = oracle' x - oracle' (R1 x) = oracle' x - --- TODO: it is not secure if we know the preimage of 0 or (-1). -instance (RandomOracle' f b, RandomOracle' g b, Ring b) => RandomOracle' (f :*: g) b where - oracle' (x :*: y) = - let z1 = oracle' x - z2 = oracle' y - in z1 * z2 + z1 - -instance RandomOracle c b => RandomOracle' (K1 i c) b where - oracle' (K1 x) = oracle x - --- | Handling constructors with no fields. --- The oracle will be based on the constructor's name --- -instance {-# OVERLAPPING #-} - ( KnownSymbol conName - , Ring a - , FromConstant Natural a - ) => RandomOracle' (M1 C ('MetaCons conName fixity selectors) U1) a where - oracle' _ = oracle @[a] $ (fromConstant @Natural . P.fromIntegral . ord) <$> symbolVal (Proxy @conName) - -instance RandomOracle' f b => RandomOracle' (M1 c m f) b where - oracle' (M1 x) = oracle' x diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/RecursiveCircuit.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/RecursiveCircuit.hs deleted file mode 100644 index 936949d5b..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/RecursiveCircuit.hs +++ /dev/null @@ -1,86 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE TypeOperators #-} - -module ZkFold.Base.Protocol.Protostar.RecursiveCircuit where - -import GHC.Generics (Par1 (..), U1 (..), type (:.:) (..), (:*:) (..)) -import Prelude hiding (Num (..), drop, head, replicate, take, - zipWith) - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (+), type (-), value) -import ZkFold.Base.Data.ByteString (Binary) -import ZkFold.Base.Data.Vector (Vector, unsafeToVector) -import ZkFold.Base.Protocol.Protostar.ArithmetizableFunction (ArithmetizableFunction (ArithmetizableFunction)) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit) -import ZkFold.Base.Protocol.Protostar.CommitOpen (CommitOpen (..)) -import ZkFold.Base.Protocol.Protostar.FiatShamir (FiatShamir (..)) -import ZkFold.Base.Protocol.Protostar.IVC (IVCResult, ivcVerify) -import ZkFold.Prelude (replicate) -import ZkFold.Symbolic.Class -import ZkFold.Symbolic.Compiler -import ZkFold.Symbolic.Data.Class (SymbolicData (..)) -import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) -import ZkFold.Symbolic.Data.Input (SymbolicInput) -import ZkFold.Symbolic.Interpreter (Interpreter (..)) - --- | Takes a function `f` and returns a circuit `C` with input `y` and witness `w`. --- The circuit is such that `C(y, w) = 0` implies that `y = x(n)` for some positive `n` where --- `x(k+1) = f(x(k), u(k))` for all `k` and some `u`. -protostar :: forall f i m c d k a payload input output nx nu ctx . - ( f ~ FieldElement ctx - , i ~ Vector nx - , m ~ [f] - , c ~ f - , HomomorphicCommit m c - , KnownNat (d - 1) - , KnownNat (d + 1) - , KnownNat k - , KnownNat (k - 1) - , Binary a - , Arithmetic a - , KnownNat nx - , KnownNat nu - , ctx ~ ArithmeticCircuit a payload input - , SymbolicInput (IVCResult f i m c d k) - , Context (IVCResult f i m c d k) ~ ctx - , payload ~ (Payload (IVCResult f i m c d k) :*: U1) - , input ~ (Layout (IVCResult f i m c d k) :*: U1) - , output ~ (((Par1 :*: (Vector nx :.: Par1)) :*: ((Vector (k - 1) :.: Par1) :*: ((Vector k :.: Par1) :*: Par1))) :*: ((Vector k :.: Par1) :*: Par1)) - ) => (forall ctx' . Symbolic ctx' => Vector nx (FieldElement ctx') -> Vector nu (FieldElement ctx') -> Vector nx (FieldElement ctx')) - -> ArithmeticCircuit a payload input output -protostar func = - let - -- The numeric interpretation of the function `f`. - stepFunction :: Vector nx a -> Vector nu a -> Vector nx a - stepFunction x' u' = - let x = fromConstant <$> x' :: Vector nx (FieldElement (Interpreter a)) - u = fromConstant <$> u' :: Vector nu (FieldElement (Interpreter a)) - in unPar1 . runInterpreter . fromFieldElement <$> func x u - - -- The step circuit for the recursion implements the function `F(x, u, y) = f(x, u) - y`. - -- Here `x` and `u` are the private inputs and `y` is the public input. - stepCircuit :: ArithmeticCircuit a (Vector nx :*: Vector nu) (Vector nx) U1 - stepCircuit = - hpmap (\(x :*: u) -> Comp1 (Par1 <$> x) :*: Comp1 (Par1 <$> u)) $ - hlmap (\x -> U1 :*: Comp1 (Par1 <$> x)) $ - compileWith @a guessOutput (\(x :*: u) U1 -> - ( Comp1 (unsafeToVector $ replicate (value @nx) U1) :*: Comp1 (unsafeToVector $ replicate (value @nx) U1) :*: U1 - , x :*: u :*: U1) - ) func - - -- Protostar IVC takes an arithmetizable function as input. - af :: ArithmetizableFunction a (Vector nx) (Vector nu) - af = ArithmetizableFunction stepFunction stepCircuit - - -- The Fiat-Shamired commit-open special-sound protocol for the arithmetizable function - fs :: FiatShamir (CommitOpen (ArithmetizableFunction a (Vector nx) (Vector nu))) - fs = FiatShamir (CommitOpen af) - - -- The verification function for the IVC result object - vf :: IVCResult f i m c d k -> ((f, i f, Vector (k-1) f, Vector k c, c), (Vector k c, c)) - vf = ivcVerify @f @i @m @c @d @k fs - - -- -- TODO: the circuit functors must be adjusted for better usability - circuit = compile @a vf - in circuit diff --git a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/SpecialSound.hs b/symbolic-base/src/ZkFold/Base/Protocol/Protostar/SpecialSound.hs deleted file mode 100644 index f3dce5bdf..000000000 --- a/symbolic-base/src/ZkFold/Base/Protocol/Protostar/SpecialSound.hs +++ /dev/null @@ -1,63 +0,0 @@ -{-# LANGUAGE AllowAmbiguousTypes #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module ZkFold.Base.Protocol.Protostar.SpecialSound where - -import Data.Functor.Rep (Representable (..)) -import Data.Map.Strict (elems) -import GHC.Generics ((:*:) (..)) -import Prelude (($)) - -import ZkFold.Base.Algebra.Basic.Class -import ZkFold.Base.Algebra.Basic.Number -import ZkFold.Base.Data.Vector (Vector) -import qualified ZkFold.Base.Protocol.Protostar.AlgebraicMap as AM -import ZkFold.Base.Protocol.Protostar.ArithmetizableFunction (ArithmetizableFunction (..)) -import ZkFold.Symbolic.Class -import ZkFold.Symbolic.Compiler - -{-- | Section 3.1 - -The protocol Πsps has 3 essential parameters k, d, l ∈ N, meaning that Πsps is a (2k − 1)- -move protocol with verifier degree d and output length l (i.e. the verifier checks l degree -d algebraic equations). In each round i (1 ≤ i ≤ k), the prover Psps(pi, w, [mj , rj], j=1 to i-1) -generates the next message mi on input the public input pi, the witness w, and the current -transcript [mj , rj], j=1 to i-1, and sends mi to the verifier; the verifier replies with a random -challenge ri ∈ F. After the final message mk, the verifier computes the algebraic map Vsps -and checks that the output is a zero vector of length l. - ---} -class SpecialSoundProtocol f i p m c d k a where - type VerifierOutput f i p m c d k a - - input :: a - -> i f -- ^ previous public input - -> p f -- ^ witness - -> i f -- ^ public input - - prover :: a - -> i f -- ^ previous public input - -> p f -- ^ witness - -> f -- ^ current random challenge - -> Natural -- ^ round number (starting from 1) - -> m -- ^ prover message - - verifier :: a - -> i f -- ^ public input - -> Vector k m -- ^ prover messages - -> Vector (k-1) f -- ^ random challenges - -> VerifierOutput f i p m c d k a -- ^ verifier output - -instance (Arithmetic a, Representable i, Representable p, KnownNat (d + 1)) - => SpecialSoundProtocol a i p [a] c d 1 (ArithmetizableFunction a i p) where - type VerifierOutput a i p [a] c d 1 (ArithmetizableFunction a i p) = [a] - - input ArithmetizableFunction {..} = afEval - - -- | Just return the witness values on the previous public input - prover ArithmetizableFunction {..} pi0 w _ _ = elems $ witnessGenerator afCircuit (pi0 :*: w) (afEval pi0 w) - - -- | Evaluate the algebraic map on public inputs and prover messages - -- - verifier af pi pm ts = AM.algebraicMap @_ @_ @d af pi pm ts one diff --git a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs index 66252af01..2b8e2b28f 100644 --- a/symbolic-base/src/ZkFold/Symbolic/Data/List.hs +++ b/symbolic-base/src/ZkFold/Symbolic/Data/List.hs @@ -29,30 +29,22 @@ import ZkFold.Symbolic.Data.Payloaded (Payloaded (Payloaded)) import ZkFold.Symbolic.Data.UInt (UInt) import ZkFold.Symbolic.MonadCircuit -data ListItem x a = ListItem - { tailHash :: Layout x a - , headLayout :: Layout x a - , headPayload :: Payload x a +data ListItem l p a = ListItem + { tailHash :: l a + , headLayout :: l a + , headPayload :: p a } - deriving (Generic1) + deriving (Functor, Generic1) -deriving instance - (Functor (Layout x), Functor (Payload x)) => - Functor (ListItem x) - -instance - (Representable (Layout x), Representable (Payload x)) => - Distributive (ListItem x) where +instance (Representable l, Representable p) => Distributive (ListItem l p) where distribute = distributeRep -instance - (Representable (Layout x), Representable (Payload x)) => - Representable (ListItem x) +instance (Representable l, Representable p) => Representable (ListItem l p) data List c x = List { lHash :: c (Layout x) , lSize :: c Par1 - , lWitness :: Payloaded (Infinite :.: ListItem x) c + , lWitness :: Payloaded (Infinite :.: ListItem (Layout x) (Payload x)) c } deriving (Generic) diff --git a/symbolic-base/symbolic-base.cabal b/symbolic-base/symbolic-base.cabal index 8ad30575e..2c7226e1c 100644 --- a/symbolic-base/symbolic-base.cabal +++ b/symbolic-base/symbolic-base.cabal @@ -115,6 +115,7 @@ library ZkFold.Base.Data.HFunctor ZkFold.Base.Data.List.Infinite ZkFold.Base.Data.Matrix + ZkFold.Base.Data.Orphans ZkFold.Base.Data.Package ZkFold.Base.Data.Product ZkFold.Base.Data.Sparse.Matrix @@ -122,6 +123,21 @@ library ZkFold.Base.Data.Type ZkFold.Base.Data.Utils ZkFold.Base.Data.Vector + ZkFold.Base.Protocol.IVC + ZkFold.Base.Protocol.IVC.Accumulator + ZkFold.Base.Protocol.IVC.AccumulatorScheme + ZkFold.Base.Protocol.IVC.AlgebraicMap + ZkFold.Base.Protocol.IVC.CommitOpen + ZkFold.Base.Protocol.IVC.Commit + ZkFold.Base.Protocol.IVC.FiatShamir + ZkFold.Base.Protocol.IVC.Internal + ZkFold.Base.Protocol.IVC.NARK + ZkFold.Base.Protocol.IVC.Oracle + ZkFold.Base.Protocol.IVC.Predicate + ZkFold.Base.Protocol.IVC.RecursiveFunction + ZkFold.Base.Protocol.IVC.SpecialSound + ZkFold.Base.Protocol.IVC.StepFunction + ZkFold.Base.Protocol.IVC.VerifierCircuit ZkFold.Base.Protocol.KZG ZkFold.Base.Protocol.Plonk ZkFold.Base.Protocol.Plonk.Prover @@ -145,19 +161,6 @@ library ZkFold.Base.Protocol.Plonkup.Verifier.Commitments ZkFold.Base.Protocol.Plonkup.Verifier.Setup ZkFold.Base.Protocol.Plonkup.Witness - ZkFold.Base.Protocol.Protostar - ZkFold.Base.Protocol.Protostar.Accumulator - ZkFold.Base.Protocol.Protostar.AccumulatorScheme - ZkFold.Base.Protocol.Protostar.AlgebraicMap - ZkFold.Base.Protocol.Protostar.ArithmetizableFunction - ZkFold.Base.Protocol.Protostar.CommitOpen - ZkFold.Base.Protocol.Protostar.Commit - ZkFold.Base.Protocol.Protostar.FiatShamir - ZkFold.Base.Protocol.Protostar.IVC - ZkFold.Base.Protocol.Protostar.NARK - ZkFold.Base.Protocol.Protostar.Oracle - ZkFold.Base.Protocol.Protostar.RecursiveCircuit - ZkFold.Base.Protocol.Protostar.SpecialSound ZkFold.Base.Protocol.NonInteractiveProof ZkFold.Base.Protocol.NonInteractiveProof.Internal ZkFold.Base.Protocol.NonInteractiveProof.Prover @@ -231,6 +234,7 @@ library swagger2 , text , these < 1.3, + transformers , type-errors < 0.2.1, vector < 0.14, vector-binary-instances < 0.3, @@ -261,12 +265,12 @@ test-suite symbolic-base-test Tests.GroebnerBasis Tests.Group Tests.Hash + Tests.IVC Tests.List Tests.NonInteractiveProof Tests.Pairing Tests.Permutations Tests.Plonkup - Tests.Protostar Tests.RSA Tests.SHA2 Tests.UInt @@ -292,6 +296,7 @@ test-suite symbolic-base-test RSA < 1.1, split < 0.2.6, symbolic-base , + transformers , vector , vector-algorithms , aeson diff --git a/symbolic-base/test/Main.hs b/symbolic-base/test/Main.hs index ecb60b636..90906bb53 100644 --- a/symbolic-base/test/Main.hs +++ b/symbolic-base/test/Main.hs @@ -13,12 +13,12 @@ import Tests.Field (specField) import Tests.GroebnerBasis (specGroebner) import Tests.Group (specAdditiveGroup) import Tests.Hash (specHash) +import Tests.IVC (specIVC) import Tests.List (specList) import Tests.NonInteractiveProof (specNonInteractiveProof) import Tests.Pairing (specPairing) import Tests.Permutations (specPermutations) import Tests.Plonkup (specPlonkup) -import Tests.Protostar (specProtostar) import Tests.RSA (specRSA) import Tests.SHA2 (specSHA2, specSHA2Natural) import Tests.UInt (specUInt) @@ -57,7 +57,7 @@ main = do -- Protocols specPlonkup specNonInteractiveProof - specProtostar + specIVC -- Cryptography specSHA2Natural diff --git a/symbolic-base/test/Tests/IVC.hs b/symbolic-base/test/Tests/IVC.hs new file mode 100644 index 000000000..98e3bcdae --- /dev/null +++ b/symbolic-base/test/Tests/IVC.hs @@ -0,0 +1,142 @@ +{-# LANGUAGE TypeOperators #-} + +module Tests.IVC (specIVC) where + +import Data.Functor.Constant (Constant) +import GHC.Generics (U1 (..), type (:*:) (..)) +import GHC.IsList (IsList (..)) +import Prelude hiding (Num (..), pi, replicate, sum, (+)) +import Test.Hspec (describe, hspec, it) +import Test.QuickCheck (arbitrary, generate, property, withMaxSuccess) + +import ZkFold.Base.Algebra.Basic.Class (FromConstant (..), one, zero) +import ZkFold.Base.Algebra.Basic.Field (Zp) +import ZkFold.Base.Algebra.Basic.Number (Natural, type (-)) +import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_G1, BLS12_381_Scalar) +import ZkFold.Base.Algebra.EllipticCurve.Class (Point) +import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec, evalPolyVec) +import ZkFold.Base.Data.Vector (Vector (..), item, singleton, unsafeToVector) +import ZkFold.Base.Protocol.IVC.Accumulator (Accumulator (..), AccumulatorInstance (..), + emptyAccumulator) +import ZkFold.Base.Protocol.IVC.AccumulatorScheme as Acc +import ZkFold.Base.Protocol.IVC.AlgebraicMap (algebraicMap) +import ZkFold.Base.Protocol.IVC.CommitOpen (commitOpen) +import ZkFold.Base.Protocol.IVC.FiatShamir (FiatShamir, fiatShamir) +import ZkFold.Base.Protocol.IVC.NARK (NARKInstanceProof (..), NARKProof (..), narkInstanceProof) +import ZkFold.Base.Protocol.IVC.Oracle (MiMCHash) +import ZkFold.Base.Protocol.IVC.Predicate (Predicate (..), predicate) +import ZkFold.Base.Protocol.IVC.SpecialSound (specialSoundProtocol) +import ZkFold.Prelude (replicate) +import ZkFold.Symbolic.Class (BaseField, Symbolic) +import ZkFold.Symbolic.Compiler (ArithmeticCircuit, acSizeN) +import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) + +type F = Zp BLS12_381_Scalar +type C = Constant (Point BLS12_381_G1) +type I = Vector 1 +type P = U1 +type K = 1 +type AC = ArithmeticCircuit F (Vector 1 :*: U1) (Vector 1) U1 +type PHI = Predicate F I P +type SPS = FiatShamir 1 I P C [F] [F] F +type D = 2 +type PARDEG = 5 +type PAR = PolyVec F PARDEG + +testFunction :: forall ctx . (Symbolic ctx, FromConstant F (BaseField ctx)) + => PAR -> Vector 1 (FieldElement ctx) -> U1 (FieldElement ctx) -> Vector 1 (FieldElement ctx) +testFunction p x _ = + let p' = fromList $ map fromConstant $ toList p :: PolyVec (FieldElement ctx) PARDEG + in singleton $ evalPolyVec p' $ item x + +testPredicateCircuit :: PAR -> AC +testPredicateCircuit p = predicateCircuit @F @I @P $ testPredicate p + +testPredicate :: PAR -> PHI +testPredicate p = predicate $ testFunction p + +testSPS :: PHI -> SPS +testSPS = fiatShamir @MiMCHash . commitOpen . specialSoundProtocol @D + +initAccumulator :: PHI -> Accumulator K I C F +initAccumulator = emptyAccumulator @D + +initAccumulatorInstance :: PHI -> AccumulatorInstance K I C F +initAccumulatorInstance phi = + let Accumulator ai _ = initAccumulator phi + in ai + +testPublicInput0 :: I F +testPublicInput0 = singleton $ fromConstant @Natural 42 + +testInstanceProofPair :: PHI -> NARKInstanceProof K I C F +testInstanceProofPair phi = narkInstanceProof (testSPS phi) testPublicInput0 U1 + +testMessages :: PHI -> Vector K [F] +testMessages phi = + let NARKInstanceProof _ (NARKProof _ ms) = testInstanceProofPair phi + in ms + +testNarkProof :: PHI -> Vector K (C F) +testNarkProof phi = + let NARKInstanceProof _ (NARKProof cs _) = testInstanceProofPair phi + in cs + +testPublicInput :: PHI -> I F +testPublicInput phi = + let NARKInstanceProof pi _ = testInstanceProofPair phi + in pi + +testAccumulatorScheme :: PHI -> AccumulatorScheme D 1 I C F +testAccumulatorScheme = accumulatorScheme @MiMCHash + +testAccumulator :: PHI -> Accumulator K I C F +testAccumulator phi = + let s = testAccumulatorScheme phi + in fst $ prover s (initAccumulator phi) $ testInstanceProofPair phi + +testAccumulatorInstance :: PHI -> AccumulatorInstance K I C F +testAccumulatorInstance phi = + let Accumulator ai _ = testAccumulator phi + in ai + +testAccumulationProof :: PHI -> Vector (D - 1) (C F) +testAccumulationProof phi = + let s = testAccumulatorScheme phi + in snd $ prover s (initAccumulator phi) $ testInstanceProofPair phi + +testDeciderResult :: PHI -> (Vector K (C F), C F) +testDeciderResult phi = + let s = testAccumulatorScheme phi + in decider s $ testAccumulator phi + +testVerifierResult :: PHI -> AccumulatorInstance K I C F +testVerifierResult phi = + let s = testAccumulatorScheme phi + in verifier s (testPublicInput phi) (testNarkProof phi) (initAccumulatorInstance phi) (testAccumulationProof phi) + +specAlgebraicMap :: IO () +specAlgebraicMap = hspec $ do + describe "Algebraic map specification" $ do + describe "Algebraic map" $ do + it "must output zeros on the public input and testMessages" $ do + withMaxSuccess 10 $ property $ + \p -> algebraicMap @D (testPredicate p) (testPublicInput $ testPredicate p) (testMessages $ testPredicate p) (unsafeToVector []) one + == replicate (acSizeN $ testPredicateCircuit p) zero + +specAccumulatorScheme :: IO () +specAccumulatorScheme = hspec $ do + describe "Accumulator scheme specification" $ do + describe "decider" $ do + it "must output zeros" $ do + withMaxSuccess 10 $ property $ \p -> testDeciderResult (testPredicate p) == (singleton zero, zero) + describe "verifier" $ do + it "must output zeros" $ do + withMaxSuccess 10 $ property $ \p -> testVerifierResult (testPredicate p) == testAccumulatorInstance (testPredicate p) + +specIVC :: IO () +specIVC = do + p <- generate arbitrary :: IO PAR + print $ "Recursion circuit size: " ++ show (acSizeN $ testPredicateCircuit p) + specAlgebraicMap + specAccumulatorScheme diff --git a/symbolic-base/test/Tests/List.hs b/symbolic-base/test/Tests/List.hs index 884b11bb5..25336c7b3 100644 --- a/symbolic-base/test/Tests/List.hs +++ b/symbolic-base/test/Tests/List.hs @@ -16,11 +16,11 @@ import ZkFold.Base.Algebra.Basic.Class (one) import ZkFold.Base.Algebra.Basic.Field (Zp) import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar) import ZkFold.Symbolic.Class (Arithmetic, Symbolic) -import ZkFold.Symbolic.Compiler (compile, eval1) +import ZkFold.Symbolic.Compiler (acOutput, compile, eval1) import ZkFold.Symbolic.Data.Bool (Bool) import ZkFold.Symbolic.Data.Eq ((==)) import ZkFold.Symbolic.Data.FieldElement (FieldElement) -import ZkFold.Symbolic.Data.List (emptyList, head, tail, (.:)) +import ZkFold.Symbolic.Data.List (List, emptyList, head, tail, (.:)) headTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c headTest x y = head (x .: y .: emptyList) == x @@ -28,8 +28,13 @@ headTest x y = head (x .: y .: emptyList) == x tailTest :: Symbolic c => FieldElement c -> FieldElement c -> Bool c tailTest x y = head (tail (x .: y .: emptyList)) == y +headFun :: Symbolic c => List c (FieldElement c) -> FieldElement c +headFun = head + specList' :: forall a. (Arbitrary a, Arithmetic a, Binary a, Show a) => IO () specList' = hspec $ describe "List spec" $ do + let _headChecks = -- compile-time test + acOutput (compile @a headFun) prop "Head works fine" $ \x y -> eval1 (compile @a headTest) (U1 :*: U1 :*: U1) (Par1 x :*: Par1 y :*: U1) Haskell.== one diff --git a/symbolic-base/test/Tests/Protostar.hs b/symbolic-base/test/Tests/Protostar.hs deleted file mode 100644 index ddcbf14c8..000000000 --- a/symbolic-base/test/Tests/Protostar.hs +++ /dev/null @@ -1,139 +0,0 @@ -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - -module Tests.Protostar (specProtostar) where - -import GHC.Generics (Par1 (..), U1 (..), type (:*:) (..), - type (:.:) (..)) -import GHC.IsList (IsList (..)) -import Prelude hiding (Num (..), pi, replicate, sum, (+)) -import Test.Hspec (describe, hspec, it) -import Test.QuickCheck (property, withMaxSuccess) - -import ZkFold.Base.Algebra.Basic.Class (FromConstant (..), one, zero) -import ZkFold.Base.Algebra.Basic.Field (Zp) -import ZkFold.Base.Algebra.Basic.Number (Natural, type (-)) -import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_G1, BLS12_381_Scalar) -import ZkFold.Base.Algebra.EllipticCurve.Class (Point) -import ZkFold.Base.Algebra.Polynomials.Univariate (PolyVec, evalPolyVec) -import ZkFold.Base.Data.Vector (Vector (..), item, singleton, unsafeToVector) -import ZkFold.Base.Protocol.Protostar.Accumulator (Accumulator (..), AccumulatorInstance (..), - emptyAccumulator) -import ZkFold.Base.Protocol.Protostar.AccumulatorScheme as Acc -import ZkFold.Base.Protocol.Protostar.AlgebraicMap (AlgebraicMap (..)) -import ZkFold.Base.Protocol.Protostar.ArithmetizableFunction (ArithmetizableFunction (..)) -import ZkFold.Base.Protocol.Protostar.CommitOpen (CommitOpen (..)) -import ZkFold.Base.Protocol.Protostar.FiatShamir (FiatShamir (..)) -import ZkFold.Base.Protocol.Protostar.NARK (NARKInstanceProof (..), NARKProof (..), - narkInstanceProof) -import ZkFold.Prelude (replicate) -import ZkFold.Symbolic.Class (Symbolic) -import ZkFold.Symbolic.Compiler (ArithmeticCircuit, acSizeN, compileWith, - guessOutput, hlmap, hpmap) -import ZkFold.Symbolic.Data.FieldElement (FieldElement (..)) - -type F = Zp BLS12_381_Scalar -type G = Point BLS12_381_G1 -type I = Vector 1 -type M = [F] -type K = 1 -type AC = ArithmeticCircuit F (Vector 1 :*: U1) (Vector 1) U1 -type AF = ArithmetizableFunction F I U1 -type SPS = FiatShamir (CommitOpen AF) -type D = 2 -type PARDEG = 5 -type PAR = PolyVec F PARDEG - -testFunction :: forall ctx . (Symbolic ctx, FromConstant F (FieldElement ctx)) - => PAR -> Vector 1 (FieldElement ctx) -> Vector 1 (FieldElement ctx) -testFunction p x = - let p' = fromList $ map fromConstant $ toList p :: PolyVec (FieldElement ctx) PARDEG - in singleton $ evalPolyVec p' $ item x - -testFunction' :: PAR -> Vector 1 F -> Vector 1 F -testFunction' p x = - let p' = fromList $ toList p :: PolyVec F PARDEG - in singleton $ evalPolyVec p' $ item x - -testCircuit :: PAR -> AC -testCircuit p = - hpmap (\(x :*: U1) -> Comp1 (Par1 <$> x) :*: U1) $ - hlmap (\x -> U1 :*: Comp1 (Par1 <$> x)) $ - compileWith @F guessOutput (\x U1 -> (Comp1 (singleton U1) :*: U1, x)) $ testFunction p - -testArithmetizableFunction :: PAR -> ArithmetizableFunction F I U1 -testArithmetizableFunction p = ArithmetizableFunction (\x _ -> testFunction' p x) (testCircuit p) - -testSPS :: PAR -> SPS -testSPS = FiatShamir . CommitOpen . testArithmetizableFunction - -initAccumulator :: SPS -> Accumulator F I M G K -initAccumulator = emptyAccumulator @_ @_ @_ @_ @D - -initAccumulatorInstance :: SPS -> AccumulatorInstance F I G K -initAccumulatorInstance sps = - let Accumulator ai _ = initAccumulator sps - in ai - -testPublicInput0 :: I F -testPublicInput0 = singleton $ fromConstant @Natural 42 - -testInstanceProofPair :: SPS -> NARKInstanceProof F I M G K -testInstanceProofPair sps = narkInstanceProof @_ @_ @_ @_ @_ @D sps testPublicInput0 U1 - -testMessages :: SPS -> Vector K M -testMessages sps = - let NARKInstanceProof _ (NARKProof _ ms) = testInstanceProofPair sps - in ms - -testNarkProof :: SPS -> Vector K G -testNarkProof sps = - let NARKInstanceProof _ (NARKProof cs _) = testInstanceProofPair sps - in cs - -testPublicInput :: SPS -> I F -testPublicInput sps = - let NARKInstanceProof pi _ = testInstanceProofPair sps - in pi - -testAccumulator :: SPS -> Accumulator F I M G K -testAccumulator sps = fst $ Acc.prover @F @I @M @G @D @K sps (initAccumulator sps) $ testInstanceProofPair sps - -testAccumulatorInstance :: SPS -> AccumulatorInstance F I G K -testAccumulatorInstance sps = - let Accumulator ai _ = testAccumulator sps - in ai - -testAccumulationProof :: SPS -> Vector (D - 1) G -testAccumulationProof sps = snd $ Acc.prover sps (initAccumulator sps) $ testInstanceProofPair sps - -testDeciderResult :: SPS -> (Vector K G, G) -testDeciderResult sps = decider @F @I @M @G @D @K sps $ testAccumulator sps - -testVerifierResult :: SPS -> (F, I F, Vector (K-1) F, Vector K G, G) -testVerifierResult sps = Acc.verifier @F @I @M @G @D @K @SPS - (testPublicInput sps) (testNarkProof sps) (initAccumulatorInstance sps) (testAccumulatorInstance sps) (testAccumulationProof sps) - -specAlgebraicMap :: IO () -specAlgebraicMap = hspec $ do - describe "Algebraic map specification" $ do - describe "Algebraic map" $ do - it "must output zeros on the public input and testMessages" $ do - property $ - \p -> algebraicMap @_ @_ @D (testArithmetizableFunction p) (testPublicInput $ testSPS p) (testMessages $ testSPS p) (unsafeToVector []) one - == replicate (acSizeN $ testCircuit p) zero - -specAccumulatorScheme :: IO () -specAccumulatorScheme = hspec $ do - describe "Accumulator scheme specification" $ do - describe "decider" $ do - it "must output zeros" $ do - withMaxSuccess 10 $ property $ \p -> testDeciderResult (testSPS p) == (singleton zero, zero) - describe "verifier" $ do - it "must output zeros" $ do - withMaxSuccess 10 $ property $ \p -> testVerifierResult (testSPS p) == (zero, singleton zero, unsafeToVector [], singleton zero, zero) - -specProtostar :: IO () -specProtostar = do - specAlgebraicMap - specAccumulatorScheme diff --git a/symbolic-examples/src/Examples/Commitment.hs b/symbolic-examples/src/Examples/Commitment.hs index 323403d48..158fa3225 100644 --- a/symbolic-examples/src/Examples/Commitment.hs +++ b/symbolic-examples/src/Examples/Commitment.hs @@ -4,8 +4,8 @@ module Examples.Commitment ( import ZkFold.Base.Algebra.EllipticCurve.Class import ZkFold.Base.Data.Vector (Vector) -import ZkFold.Base.Protocol.Protostar.Commit (HomomorphicCommit (..)) -import ZkFold.Symbolic.Data.Ed25519 +import ZkFold.Base.Protocol.IVC.Commit (HomomorphicCommit (..)) +import ZkFold.Symbolic.Data.Ed25519 (AcEd25519) exampleCommitment :: HomomorphicCommit (Vector 1 (ScalarField (AcEd25519 c))) (Point (AcEd25519 c))