Skip to content

Commit

Permalink
+ compiler benchmarks + example library
Browse files Browse the repository at this point in the history
  • Loading branch information
@iokasimov @TurtlePU
iokasimov authored and TurtlePU committed Aug 23, 2024
1 parent 64bc5e9 commit 03efaf2
Show file tree
Hide file tree
Showing 39 changed files with 390 additions and 552 deletions.
2 changes: 1 addition & 1 deletion .gitignore
View file
Original file line number Diff line number Diff line change
Expand Up @@ -22,4 +22,4 @@ cabal.project.local~
.HTF/
.ghc.environment.*
compiled_scripts/*
stack.yaml*
stack.yaml*
146 changes: 0 additions & 146 deletions bench/BenchAC.hs
View file

This file was deleted.

45 changes: 45 additions & 0 deletions bench/BenchCompiler.hs
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,45 @@
module Main where

import Control.DeepSeq (NFData, force)
import Control.Monad (return)
import Data.ByteString.Lazy (ByteString)
import Data.Function (($))
import Data.Map (Map, fromAscList)
import Data.Semigroup ((<>))
import Data.String (String, fromString)
import Numeric.Natural (Natural)
import System.IO (IO)
import Test.Tasty.Bench
import Test.Tasty.Golden (goldenVsString)
import Text.Show (show)

import ZkFold.Base.Algebra.Basic.Class (AdditiveMonoid, zero)
import ZkFold.Symbolic.Compiler
import ZkFold.Symbolic.Examples

inputMap :: AdditiveMonoid a => ArithmeticCircuit a o -> Map Natural a
inputMap circuit = fromAscList [ (i, zero) | i <- acInput circuit ]

metrics :: String -> ArithmeticCircuit a o -> ByteString
metrics name circuit =
fromString name
<> "\nNumber of constraints: " <> fromString (show $ acSizeN circuit)
<> "\nNumber of variables: " <> fromString (show $ acSizeM circuit)
<> "\nNumber of range lookups: " <> fromString (show $ acSizeR circuit)

benchmark ::
(NFData a, AdditiveMonoid a, NFData (o Natural)) =>
String -> (() -> ArithmeticCircuit a o) -> Benchmark
benchmark name circuit = bgroup name
[ bench "compilation" $ nf circuit ()
, env (return $ force $ circuit ()) $ \c ->
let input = inputMap c
path = "stats/" <> name
in bgroup "on compilation"
[ bench "evaluation" $ nf (witnessGenerator c) input
, goldenVsString "# of constraints" path $ return (metrics name c)
]
]

main :: IO ()
main = defaultMain [ benchmark n c | (n, ExampleOutput c) <- examples ]
6 changes: 2 additions & 4 deletions bench/BenchPolyMul.hs
View file
Original file line number Diff line number Diff line change
@@ -1,7 +1,5 @@
{-# LANGUAGE DeriveAnyClass #-}
{-# LANGUAGE NoGeneralisedNewtypeDeriving #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}

module Main where

Expand Down
25 changes: 11 additions & 14 deletions examples/Examples/BatchTransfer.hs
View file
Original file line number Diff line number Diff line change
@@ -1,19 +1,16 @@
{-# LANGUAGE TypeApplications #-}
{-# OPTIONS_GHC -freduction-depth=0 #-} -- Avoid reduction overflow error caused by NumberOfRegisters
{-# LANGUAGE TypeOperators #-}

module Examples.BatchTransfer (exampleBatchTransfer) where

import Prelude hiding (Eq (..), Num (..), any, not, (!!), (/), (^),
(||))
import Data.Type.Equality (type (~))

import ZkFold.Symbolic.Cardano.Contracts.BatchTransfer (batchTransfer)
import ZkFold.Symbolic.Cardano.Types
import ZkFold.Symbolic.Compiler (compileIO)
import ZkFold.Base.Data.Vector (Vector)
import ZkFold.Symbolic.Cardano.Contracts.BatchTransfer (Tx, TxOut, batchTransfer)
import ZkFold.Symbolic.Cardano.Types (Bool, ByteString, F)
import ZkFold.Symbolic.Class (Symbolic (BaseField))
import ZkFold.Symbolic.Data.Eq (Eq)

exampleBatchTransfer :: IO ()
exampleBatchTransfer = do
let file = "compiled_scripts/batch-transfer.json"

putStrLn "\nExample: Batch Transfer smart contract\n"

compileIO @F file (batchTransfer @CtxCompilation)
exampleBatchTransfer ::
(Symbolic c, BaseField c ~ F, Eq (Bool c) (TxOut c)) =>
Tx c -> Vector 5 (TxOut c, TxOut c, ByteString 256 c) -> Bool c
exampleBatchTransfer = batchTransfer
75 changes: 32 additions & 43 deletions examples/Examples/ByteString.hs
View file
Original file line number Diff line number Diff line change
@@ -1,49 +1,38 @@
{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeOperators #-}

module Examples.ByteString (
exampleByteStringAnd,
exampleByteStringOr,
exampleByteStringExtend
exampleByteStringExtend,
exampleByteStringAdd,
exampleSHA
) where

import Data.Data (Proxy (Proxy))
import Data.Function (($))
import Data.List ((++))
import Data.String (String)
import GHC.TypeNats (KnownNat, natVal, type (+), type (<=))
import System.IO (IO, putStrLn)
import Text.Show (show)

import ZkFold.Base.Algebra.Basic.Field (Zp)
import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar)
import ZkFold.Symbolic.Compiler (ArithmeticCircuit, compileIO)
import ZkFold.Symbolic.Data.Bool
import ZkFold.Symbolic.Data.ByteString
import ZkFold.Symbolic.Data.Combinators

exampleByteStringAnd :: forall n . (KnownNat n, KnownNat (n + n)) => IO ()
exampleByteStringAnd = makeExample @n "*" "and" (&&)

exampleByteStringOr :: forall n . (KnownNat n, KnownNat (n + n)) => IO ()
exampleByteStringOr = makeExample @n "+" "or" (||)

exampleByteStringExtend :: forall n k . (KnownNat n, KnownNat k, n <= k) => IO ()
exampleByteStringExtend = do
let n = show $ natVal (Proxy @n)
let k = show $ natVal (Proxy @k)
putStrLn $ "\nExample: Extending a bytestring of length " ++ n ++ " to length " ++ k
let file = "compiled_scripts/bytestring" ++ n ++ "_to_" ++ k ++ ".json"
compileIO @(Zp BLS12_381_Scalar) file $ extend @(ByteString n (ArithmeticCircuit (Zp BLS12_381_Scalar))) @(ByteString k (ArithmeticCircuit (Zp BLS12_381_Scalar)))

type Binary a = a -> a -> a

type UBinary n = Binary (ByteString n (ArithmeticCircuit (Zp BLS12_381_Scalar)))

makeExample :: forall n . (KnownNat n, KnownNat (n + n)) => String -> String -> UBinary n -> IO ()
makeExample shortName name op = do
let n = show $ natVal (Proxy @n)
putStrLn $ "\nExample: (" ++ shortName ++ ") operation on ByteString" ++ n
let file = "compiled_scripts/bytestring" ++ n ++ "_" ++ name ++ ".json"
compileIO @(Zp BLS12_381_Scalar) file op
import ZkFold.Base.Algebra.Basic.Class
import ZkFold.Base.Algebra.Basic.Number (KnownNat, type (<=))
import ZkFold.Symbolic.Algorithms.Hash.SHA2 (SHA2, sha2)
import ZkFold.Symbolic.Class (Symbolic)
import ZkFold.Symbolic.Data.Bool (BoolType (..))
import ZkFold.Symbolic.Data.ByteString (ByteString)
import ZkFold.Symbolic.Data.Combinators (Extend (..), Iso (..), RegisterSize (..))
import ZkFold.Symbolic.Data.UInt (UInt)

exampleByteStringAnd ::
(Symbolic c, KnownNat n) => ByteString n c -> ByteString n c -> ByteString n c
exampleByteStringAnd = (&&)

exampleByteStringOr ::
(Symbolic c, KnownNat n) => ByteString n c -> ByteString n c -> ByteString n c
exampleByteStringOr = (||)

exampleByteStringExtend ::
(Symbolic c, KnownNat n, KnownNat k, n <= k) =>
ByteString n c -> ByteString k c
exampleByteStringExtend = extend

exampleByteStringAdd ::
forall c n. (Symbolic c, KnownNat n) => ByteString n c -> ByteString n c -> ByteString n c
exampleByteStringAdd x y = from (from x + from y :: UInt n Auto c)

exampleSHA :: SHA2 "SHA256" c n => ByteString n c -> ByteString 256 c
exampleSHA = sha2 @"SHA256"
28 changes: 7 additions & 21 deletions examples/Examples/Conditional.hs
View file
Original file line number Diff line number Diff line change
@@ -1,24 +1,10 @@
{-# LANGUAGE TypeApplications #-}

module Examples.Conditional (exampleConditional) where

import GHC.Generics (Par1)
import Prelude (IO, putStrLn)

import ZkFold.Base.Algebra.Basic.Field (Zp)
import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar)
import ZkFold.Symbolic.Compiler
import ZkFold.Symbolic.Data.Bool (Bool)
import ZkFold.Symbolic.Data.Conditional (Conditional (..))

type F = Zp BLS12_381_Scalar
type A = ArithmeticCircuit F
type B = Bool A

exampleConditional :: IO ()
exampleConditional = do
let file = "compiled_scripts/conditional.json"

putStrLn "\nExample: conditional\n"
import ZkFold.Symbolic.Class (Symbolic)
import ZkFold.Symbolic.Data.Bool (Bool)
import ZkFold.Symbolic.Data.Conditional (Conditional (..))
import ZkFold.Symbolic.Data.FieldElement (FieldElement)

compileIO @F file (bool @B @(A Par1))
exampleConditional ::
Symbolic c => FieldElement c -> FieldElement c -> Bool c -> FieldElement c
exampleConditional = bool
28 changes: 6 additions & 22 deletions examples/Examples/Eq.hs
View file
Original file line number Diff line number Diff line change
@@ -1,26 +1,10 @@
{-# LANGUAGE TypeApplications #-}

module Examples.Eq (exampleEq) where

import Prelude hiding (Bool, Eq (..), Num (..), Ord (..), any, not, (!!),
(/), (^), (||))

import ZkFold.Base.Algebra.Basic.Field (Zp)
import ZkFold.Base.Algebra.EllipticCurve.BLS12_381 (BLS12_381_Scalar)
import ZkFold.Symbolic.Class (Symbolic)
import ZkFold.Symbolic.Compiler
import ZkFold.Symbolic.Data.Bool (Bool (..))
import ZkFold.Symbolic.Data.Eq (Eq (..))
import ZkFold.Symbolic.Data.FieldElement (FieldElement)
import ZkFold.Symbolic.Class (Symbolic)
import ZkFold.Symbolic.Data.Bool (Bool)
import ZkFold.Symbolic.Data.Eq (Eq (..))
import ZkFold.Symbolic.Data.FieldElement (FieldElement)

-- | (==) operation
eq :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
eq x y = x == y

exampleEq :: IO ()
exampleEq = do
let file = "compiled_scripts/eq.json"

putStrLn "\nExample: (==) operation\n"

compileIO @(Zp BLS12_381_Scalar) file (eq @(ArithmeticCircuit (Zp BLS12_381_Scalar)))
exampleEq :: Symbolic c => FieldElement c -> FieldElement c -> Bool c
exampleEq x y = x == y
Loading

0 comments on commit 03efaf2

Please sign in to comment.