Merge pull request #193 from zkFold/vks4git/protostar

Vks4git/protostar

bench/BenchDiv.hs

@@ -0,0 +1,102 @@
+{-# LANGUAGE AllowAmbiguousTypes          #-}
+{-# LANGUAGE DeriveAnyClass               #-}
+{-# LANGUAGE NoGeneralisedNewtypeDeriving #-}
+{-# LANGUAGE ScopedTypeVariables          #-}
+{-# LANGUAGE TypeApplications             #-}
+{-# LANGUAGE TypeOperators                #-}
+{-# OPTIONS_GHC -freduction-depth=0 #-}
+
+module Main where
+
+import           Control.DeepSeq                             (force)
+import           Control.Exception                           (evaluate)
+import qualified Data.Map                                    as M
+import           Data.Time.Clock                             (getCurrentTime)
+import           Prelude                                     hiding (divMod, not, sum, (&&), (*), (+), (-), (/), (^),
+                                                              (||))
+import           System.Random                               (randomIO)
+import           Test.Tasty.Bench
+
+import           ZkFold.Base.Algebra.Basic.Class
+import           ZkFold.Base.Algebra.Basic.Field
+import           ZkFold.Base.Algebra.Basic.Number
+import           ZkFold.Base.Algebra.EllipticCurve.BLS12_381
+import           ZkFold.Base.Data.Vector
+import           ZkFold.Symbolic.Compiler
+import           ZkFold.Symbolic.Data.Combinators
+import           ZkFold.Symbolic.Data.UInt
+
+evalUInt :: forall a n . UInt n ArithmeticCircuit a -> Vector (NumberOfRegisters a n) a
+evalUInt (UInt xs) = eval xs M.empty
+
+-- | Generate random addition circuit of given size
+--
+divisionCircuit
+    :: forall n p r
+    .  KnownNat n
+    => PrimeField (Zp p)
+    => r ~ NumberOfRegisters (Zp p) n
+    => KnownNat r
+    => KnownNat (r - 1)
+    => KnownNat (r + r)
+    => 1 + (r - 1) ~ r
+    => 1 <= r
+    => IO (UInt n ArithmeticCircuit (Zp p), UInt n ArithmeticCircuit (Zp p))
+divisionCircuit = do
+    x <- randomIO
+    y <- randomIO
+    let acX = fromConstant (x :: Integer) :: UInt n ArithmeticCircuit (Zp p)
+        acY = fromConstant (y :: Integer) :: UInt n ArithmeticCircuit (Zp p)
+
+        acZ = acX `divMod` acY
+
+    evaluate . force $ acZ
+
+benchOps
+    :: forall n p r
+    .  KnownNat n
+    => PrimeField (Zp p)
+    => r ~ NumberOfRegisters (Zp p) n
+    => KnownNat r
+    => KnownNat (r - 1)
+    => KnownNat (r + r)
+    => 1 + (r - 1) ~ r
+    => 1 <= r
+    => Benchmark
+benchOps = env (divisionCircuit @n @p) $ \ ~ac ->
+    bench ("Dividing UInts of size " <> show (value @n)) $ nf (\(a, b) -> (evalUInt a, evalUInt b)) ac
+
+main :: IO ()
+main = do
+  getCurrentTime >>= print
+  (UInt ac32q, UInt ac32r)  <- divisionCircuit @32 @BLS12_381_Scalar
+  getCurrentTime >>= print
+  (UInt ac64q,  UInt ac64r)  <- divisionCircuit @64 @BLS12_381_Scalar
+  getCurrentTime >>= print
+  (UInt ac128q, UInt ac128r) <- divisionCircuit @128 @BLS12_381_Scalar
+  getCurrentTime >>= print
+
+  putStrLn "Sizes"
+
+  print $ (acSizeM ac32q, acSizeM ac32r)
+  getCurrentTime >>= print
+  print $ (acSizeM ac64q, acSizeM ac64r)
+  getCurrentTime >>= print
+  print $ (acSizeM ac128q, acSizeM ac128r)
+  getCurrentTime >>= print
+
+  putStrLn "Evaluation"
+
+  print $ (exec ac32q, exec ac32r)
+  getCurrentTime >>= print
+  print $ (exec ac64q, exec ac64r)
+  getCurrentTime >>= print
+  print $ (exec ac128q, exec ac128r)
+  getCurrentTime >>= print
+
+  defaultMain
+      [ benchOps @32 @BLS12_381_Scalar
+      , benchOps @64 @BLS12_381_Scalar
+      , benchOps @128 @BLS12_381_Scalar
+      ]
+

src/ZkFold/Base/Algebra/Basic/Class.hs

@@ -7,9 +7,9 @@
 module ZkFold.Base.Algebra.Basic.Class where
 
 import           Data.Bool                        (bool)
+import           Data.Foldable                    (foldl')
 import           Data.Kind                        (Type)
 import           GHC.Natural                      (naturalFromInteger)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), div, divMod, length, mod, negate, product,
                                                    replicate, sum, (/), (^))
 import qualified Prelude                          as Haskell
@@ -99,6 +99,7 @@ class (MultiplicativeSemigroup a, Exponent a Natural) => MultiplicativeMonoid a
     -- [Right identity] @x * one == x@
     one :: a
 
+{-# INLINE natPow #-}
 natPow :: MultiplicativeMonoid a => a -> Natural -> a
 -- | A default implementation for natural exponentiation. Uses only @('*')@ and
 -- @'one'@ so doesn't loop via an @'Exponent' Natural a@ instance.
@@ -109,10 +110,10 @@ natPow a n = product $ zipWith f (binaryExpansion n) (iterate (\x -> x * x) a)
     f _ _ = error "^: This should never happen."
 
 product :: (Foldable t, MultiplicativeMonoid a) => t a -> a
-product = foldl (*) one
+product = foldl' (*) one
 
 multiExp :: (MultiplicativeMonoid a, Exponent a b, Foldable t) => a -> t b -> a
-multiExp a = foldl (\x y -> x * (a ^ y)) one
+multiExp a = foldl' (\x y -> x * (a ^ y)) one
 
 {- | A class for monoid actions where multiplicative notation is the most
 natural (including multiplication by constant itself).

src/ZkFold/Base/Algebra/Basic/Field.hs

@@ -22,7 +22,6 @@ import           Data.Bool                                  (bool)
 import qualified Data.Vector                                as V
 import           GHC.Generics                               (Generic)
 import           GHC.TypeLits                               (Symbol)
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Fractional (..), Num (..), div, length, (^))
 import qualified Prelude                                    as Haskell
 import           System.Random                              (Random (..), RandomGen, mkStdGen, uniformR)
@@ -38,12 +37,15 @@ import           ZkFold.Base.Data.ByteString
 newtype Zp (p :: Natural) = Zp Integer
     deriving (Generic, NFData)
 
+{-# INLINE fromZp #-}
 fromZp :: Zp p -> Natural
 fromZp (Zp a) = fromIntegral a
 
+{-# INLINE residue #-}
 residue :: forall p . KnownNat p => Integer -> Integer
 residue = (`Haskell.mod` fromIntegral (value @p))
 
+{-# INLINE toZp #-}
 toZp :: forall p . KnownNat p => Integer -> Zp p
 toZp = Zp . residue @p
 

src/ZkFold/Base/Algebra/Basic/Number.hs

@@ -4,7 +4,22 @@
 {-# LANGUAGE TypeOperators        #-}
 {-# LANGUAGE UndecidableInstances #-}
 
-module ZkFold.Base.Algebra.Basic.Number (KnownNat, Prime, KnownPrime, IsPrime, Log2, Mod, Div, value, type (<=), type (*), type (+), type (-), type (^)) where
+module ZkFold.Base.Algebra.Basic.Number
+    ( Natural
+    , KnownNat
+    , Prime
+    , KnownPrime
+    , IsPrime
+    , Log2
+    , Mod
+    , Div
+    , value
+    , type (<=)
+    , type (*)
+    , type (+)
+    , type (-)
+    , type (^)
+    ) where
 
 import           Data.Kind      (Constraint)
 import           Data.Type.Bool (If, type (&&))

src/ZkFold/Base/Algebra/Basic/Permutations.hs

@@ -14,7 +14,6 @@ module ZkFold.Base.Algebra.Basic.Permutations (
 import           Data.Map                         (Map, elems, empty, singleton, union)
 import           Data.Maybe                       (fromJust)
 import qualified Data.Vector                      as V
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), drop, length, mod, (!!))
 import qualified Prelude                          as P
 import           Test.QuickCheck                  (Arbitrary (..))

src/ZkFold/Base/Algebra/EllipticCurve/BLS12_381.hs

@@ -11,7 +11,6 @@ import           Data.Bits
 import           Data.Foldable
 import           Data.List                                  (unfoldr)
 import           Data.Word
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), (/), (^))
 import qualified Prelude                                    as Haskell
 

src/ZkFold/Base/Algebra/Polynomials/Multivariate/Polynomial.hs

@@ -38,9 +38,14 @@ newtype Poly c i j = P [(c, Mono i j)]
 polynomial :: Polynomial c i j => [(c, Mono i j)] -> Poly c i j
 polynomial = foldr (\(c, m) x -> if c == zero then x else P [(c, m)] + x) zero
 
-evalPolynomial :: forall c i j b .
-    Algebra c b =>
-    ((i -> b) -> Mono i j -> b) -> (i -> b) -> Poly c i j -> b
+evalPolynomial
+    :: forall c i j b
+     . AdditiveMonoid b
+    => Scale c b
+    => ((i -> b) -> Mono i j -> b)
+    -> (i -> b)
+    -> Poly c i j
+    -> b
 evalPolynomial e f (P p) = foldr (\(c, m) x -> x + scale c (e f m)) zero p
 
 variables :: forall c .

src/ZkFold/Base/Algebra/Polynomials/Univariate.hs

@@ -40,7 +40,6 @@ module ZkFold.Base.Algebra.Polynomials.Univariate
 import           Control.DeepSeq                  (NFData (..))
 import qualified Data.Vector                      as V
 import           GHC.Generics                     (Generic)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (Num (..), drop, length, product, replicate, sum, take, (/),
                                                    (^))
 import qualified Prelude                          as P

src/ZkFold/Base/Data/Vector.hs

@@ -14,7 +14,6 @@ import           Data.List.Split                  (chunksOf)
 import           Data.These                       (These (..))
 import           Data.Zip                         (Semialign (..), Zip (..))
 import           GHC.Generics                     (Generic)
-import           Numeric.Natural                  (Natural)
 import           Prelude                          hiding (drop, head, length, mod, replicate, sum, tail, take, zip,
                                                    zipWith, (*))
 import qualified Prelude                          as P
@@ -41,6 +40,9 @@ toVector as
 unsafeToVector :: forall size a . [a] -> Vector size a
 unsafeToVector = Vector
 
+generate :: forall size a . KnownNat size => (Natural -> a) -> Vector size a
+generate f = Vector $ f <$> [0 .. value @size -! 1]
+
 unfold :: forall size a b. KnownNat size => (b -> (a, b)) -> b -> Vector size a
 unfold f = Vector . ZP.take (value @size) . List.unfoldr (Just . f)
 

src/ZkFold/Base/Protocol/ARK/Plonk.hs

@@ -15,7 +15,6 @@ import           Data.Maybe                                 (fromJust)
 import qualified Data.Vector                                as V
 import           GHC.Generics                               (Par1)
 import           GHC.IsList                                 (IsList (..))
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), div, drop, length, replicate, sum, take,
                                                              (!!), (/), (^))
 import qualified Prelude                                    as P hiding (length)

src/ZkFold/Base/Protocol/ARK/Plonk/Internal.hs

@@ -8,7 +8,6 @@ import           Data.Bool                                  (bool)
 import qualified Data.Map                                   as Map
 import qualified Data.Vector                                as V
 import           GHC.IsList                                 (IsList (..))
-import           Numeric.Natural                            (Natural)
 import           Prelude                                    hiding (Num (..), drop, length, sum, take, (!!), (/), (^))
 import           System.Random                              (RandomGen, mkStdGen, uniformR)
 import           Test.QuickCheck                            (Arbitrary (..), Gen, shuffle)

src/ZkFold/Base/Protocol/ARK/Plonk/Relation.hs

@@ -6,7 +6,6 @@ module ZkFold.Base.Protocol.ARK.Plonk.Relation where
 import           Data.Map                                     (Map, elems, (!))
 import           GHC.Generics                                 (Par1)
 import           GHC.IsList                                   (IsList (..))
-import           Numeric.Natural                              (Natural)
 import           Prelude                                      hiding (Num (..), drop, length, replicate, sum, take,
                                                                (!!), (/), (^))
 
@@ -37,7 +36,6 @@ toPlonkRelation :: forall n l a .
     => KnownNat l
     => Arithmetic a
     => Scale a a
-    => FromConstant a a
     => Vector l Natural
     -> ArithmeticCircuit a Par1
     -> Maybe (PlonkRelation n l a)

src/ZkFold/Base/Protocol/ARK/Protostar.hs

@@ -1 +1,71 @@
+{-# LANGUAGE DeriveAnyClass #-}
+
 module ZkFold.Base.Protocol.ARK.Protostar where
+
+
+import           Control.DeepSeq                                     (NFData)
+import           Data.Map.Strict                                     (Map)
+import qualified Data.Map.Strict                                     as M
+import           GHC.Generics                                        (Generic)
+import           Prelude                                             (($), (==))
+import qualified Prelude                                             as P
+
+import           ZkFold.Base.Algebra.Basic.Number
+import qualified ZkFold.Base.Data.Vector                             as V
+import           ZkFold.Base.Data.Vector                             (Vector)
+import           ZkFold.Base.Protocol.ARK.Protostar.SpecialSound
+import           ZkFold.Symbolic.Compiler.ArithmeticCircuit.Internal
+
+{--
+
+1. Compress verification checks (Section 3.5; )
+2. Commit (Section 3.2; ZkFold.Base.Protocol.ARK.Protostar.CommitOpen)
+3. Fiat-Shamir transform (Section 3.3; ZkFold.Base.Protocol.ARK.Protostar.FiatShamir)
+   A technique for taking an interactive proof of knowledge and creating a digital signature based on it.
+   This way, some fact (for example, knowledge of a certain secret number) can be publicly proven without revealing underlying information.
+4. Accumulation scheme (Section 3.4; ZkFold.Base.Protocol.ARK.Protostar.AccumulatorScheme)
+5. Obtain the IVC scheme (Theorem 1 from “Proof-Carrying Data Without Succinct Arguments”; )
+
+--}
+--
+--
+-- To complete the protocol:
+-- 1. Finish AccumulatorScheme -- and Lookup
+-- 2. Implement IVC scheme
+-- 3. Put it all together
+-- 4. Input and output == AC
+
+
+-- | A data for recurcive computations.
+-- @circuit@ is an Arithmetic circuit with @n@ inputs and @n@ outputs applied to itself (i.e. outputs are fed as inputs at the next iteration) @iterations@ times.
+--
+data RecursiveCircuit n a
+    = RecursiveCircuit
+        { iterations :: Natural
+        , circuit    :: ArithmeticCircuit a (Vector n)
+        } deriving (Generic, NFData)
+
+instance Arithmetic a => SpecialSoundProtocol a (RecursiveCircuit n a) where
+    type Witness a (RecursiveCircuit n a) = Map Natural a
+    type Input a (RecursiveCircuit n a) = Vector n a
+    type ProverMessage a (RecursiveCircuit n a) = Vector n a
+    type VerifierMessage a (RecursiveCircuit n a) = Vector n a
+    type Degree (RecursiveCircuit n a) = 2
+
+    -- One round for Plonk
+    rounds = P.const 1
+
+    outputLength (RecursiveCircuit _ c) = P.fromIntegral $ M.size $ constraintSystem c
+
+    -- The transcript will be empty at this point, it is a one-round protocol
+    --
+    prover rc _ i _ = eval (circuit rc) (M.fromList $ P.zip [1..] (V.fromVector i))
+
+    -- We can use the polynomial system from the circuit, no need to build it from scratch
+    --
+    algebraicMap rc _ _ _ = M.elems $ constraintSystem (circuit rc)
+
+    -- The transcript is only one prover message since this is a one-round protocol
+    --
+    verifier rc i pm _ = eval (circuit rc) (M.fromList $ P.zip [1..] (V.fromVector i)) == P.head pm
+