+
+
+
+
+
+
+
+
+ 
+
+
+
+
+
and 
+as:
+
+* 
+* 
+* 
+
+The tower of finite fields we work with is defined as:
+
+* 
+* 
+* 
+
+### Arithmetic circuits
+
+
+
+
be a finite field and 
a map that takes 
+arguments as inputs from and outputs l elements in . The function C is an arithmetic circuit if the
+value of the inputs that pass through wires to gates are only manipulated according to arithmetic operations + or x (allowing
+constant gates).
+
+Let 
, 
, 
respectively denote the input, witness and output size and
+
be the number of all inputs and outputs of the circuit
+A tuple 
, is said to be a valid
+assignment for an arithmetic circuit C if 
.
+
+
+### Quadratic Arithmetic Programs (QAP)
+
+QAPs are encodings of arithmetic circuits that allow the prover to construct a
+proof of knowledge of a valid assignment 
for a given
+circuit 
.
+
+A quadratic arithmetic program (QAP) 
contains three sets of polynomials in
+
:
+
+
, 
, 
+
+and a target polynomial 
.
+
+In this setting, an assignment 
is valid for a circuit if and
+only if the target polynomial divides the polynomial:
+
+
+
+Logical circuits can be written in terms of the addition, multiplication and
+negation operations.
+
+* 
+* 
+* 
+* 
+* 
+
+## DSL and Circuit Builder Monad
+
+Any arithmetic circuit can be built using a domain specific language to
+construct circuits that lives inside [Lang.hs](src/Circuit/Lang.hs).
+
+```haskell ignore
+type ExprM f a = State (ArithCircuit f, Int) a
+execCircuitBuilder :: ExprM f a -> ArithCircuit f
+```
+
+```haskell ignore
+-- | Binary arithmetic operations
+add, sub, mul :: Expr Wire f f -> Expr Wire f f -> Expr Wire f f
+```
+
+```haskell ignore
+-- | Binary logic operations
+-- Have to use underscore or similar to avoid shadowing @and@ and @or@
+-- from Prelude/Protolude.
+and_, or_, xor_ :: Expr Wire f Bool -> Expr Wire f Bool -> Expr Wire f Bool
+```
+
+```haskell ignore
+-- | Negate expression
+not_ :: Expr Wire f Bool -> Expr Wire f Bool
+```
+
+```haskell ignore
+-- | Compare two expressions
+eq :: Expr Wire f f -> Expr Wire f f -> Expr Wire f Bool
+```
+
+```haskell ignore
+-- | Convert wire to expression
+deref :: Wire -> Expr Wire f f
+```
+
+```haskell ignore
+-- | Return compilation of expression into an intermediate wire
+e :: Num f => Expr Wire f f -> ExprM f Wire
+```
+
+```haskell ignore
+-- | Conditional statement on expressions
+cond :: Expr Wire f Bool -> Expr Wire f ty -> Expr Wire f ty -> Expr Wire f ty
+```
+
+```haskell ignore
+-- | Return compilation of expression into an output wire
+ret :: Num f => Expr Wire f f -> ExprM f Wire
+```
+
+The following program represents the image of the
+arithmetic circuit [above](#arithmetic-circuits-1).
+
+```haskell ignore
+program :: ArithCircuit Fr
+program = execCircuitBuilder (do
+ i0 <- fmap deref input
+ i1 <- fmap deref input
+ i2 <- fmap deref input
+ let r0 = mul i0 i1
+ r1 = mul r0 (add i0 i2)
+ ret r1)
+```
+
+The output of an arithmetic circuit can be converted to a DOT graph and save it
+as SVG.
+
+```haskell ignore
+dotOutput :: Text
+dotOutput = arithCircuitToDot (execCircuitBuilder program)
+```
+
+
+
+
.
+
+```haskell
+import Protolude
+
+import qualified Data.Map as Map
+import Data.Pairing.BN254 (Fr, getRootOfUnity)
+
+import Circuit.Arithmetic
+import Circuit.Expr
+import Circuit.Lang
+import Fresh (evalFresh, fresh)
+import QAP
+
+program :: ArithCircuit Fr
+program = execCircuitBuilder (do
+ i0 <- fmap deref input
+ i1 <- fmap deref input
+ i2 <- fmap deref input
+ let r0 = mul i0 i1
+ r1 = mul r0 (add i0 i2)
+ ret r1)
+```
+
+We need to generate the roots of the circuit to construct polynomials and
+
that satisfy the divisibility property and encode the circuit to a QAP to
+allow the prover to construct a proof of a valid assignment.
+
+We also need to give values to the three input wires to this arithmetic circuit.
+
+```haskell
+roots :: [[Fr]]
+roots = evalFresh (generateRoots (fmap (fromIntegral . (+ 1)) fresh) program)
+
+qap :: QAP Fr
+qap = arithCircuitToQAPFFT getRootOfUnity roots program
+
+inputs :: Map.Map Int Fr
+inputs = Map.fromList [(0, 7), (1, 5), (2, 4)]
+```
+
+A prover can now generate a valid assignment.
+
+```haskell
+assignment :: QapSet Fr
+assignment = generateAssignment program inputs
+```
+
+The verifier can check the divisibility property of by for the given circuit.
+
+```haskell
+main :: IO ()
+main = do
+ if verifyAssignment qap assignment
+ then putText "Valid assignment"
+ else putText "Invalid assignment"
+```
+
+## Disclaimer
+
+This is experimental code meant for research-grade projects only. Please do not
+use this code in production until it has matured significantly.
+
+## License
+
+```
+Copyright (c) 2017-2020 Adjoint Inc.
+
+Permission is hereby granted, free of charge, to any person obtaining a copy
+of this software and associated documentation files (the "Software"), to deal
+in the Software without restriction, including without limitation the rights
+to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
+copies of the Software, and to permit persons to whom the Software is
+furnished to do so, subject to the following conditions:
+
+The above copyright notice and this permission notice shall be included in all
+copies or substantial portions of the Software.
+
+THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
+EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF
+MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT.
+IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM,
+DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR
+OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
+OR OTHER DEALINGS IN THE SOFTWARE.
+```
diff --git a/arithmetic-circuits.cabal b/arithmetic-circuits.cabal
new file mode 100644
--- /dev/null
+++ b/arithmetic-circuits.cabal
@@ -0,0 +1,185 @@
+cabal-version: 1.12
+
+-- This file has been generated from package.yaml by hpack version 0.31.2.
+--
+-- see: https://github.com/sol/hpack
+--
+-- hash: 82f266d078e820121bdc6466a5f276447fbe15dfb72a701071b2a43f1c5e2e63
+
+name: arithmetic-circuits
+version: 0.2.0
+synopsis: Arithmetic circuits for zkSNARKs
+description: Arithmetic circuits for zkSNARKs
+category: Cryptography
+homepage: https://github.com/adjoint-io/arithmetic-circuits#readme
+bug-reports: https://github.com/adjoint-io/arithmetic-circuits/issues
+maintainer: Adjoint Inc (info@adjoint.io)
+license: MIT
+license-file: LICENSE
+build-type: Simple
+extra-source-files:
+ README.md
+ ChangeLog.md
+
+source-repository head
+ type: git
+ location: https://github.com/adjoint-io/arithmetic-circuits
+
+library
+ exposed-modules:
+ Circuit
+ Circuit.Affine
+ Circuit.Arithmetic
+ Circuit.Bulletproofs
+ Circuit.Dot
+ Circuit.Expr
+ Circuit.Lang
+ Fresh
+ QAP
+
+ other-modules: Paths_arithmetic_circuits
+ hs-source-dirs: src
+ default-extensions:
+ NoImplicitPrelude
+ GADTs
+ LambdaCase
+ OverloadedStrings
+
+ ghc-options: -freverse-errors -O2 -Wall
+ build-depends:
+ aeson >=1.4 && <1.5
+ , base >=4.10 && <5
+ , bulletproofs >=1.1.0 && <1.2
+ , containers >=0.6.0 && <0.7
+ , elliptic-curve >=0.3 && <0.4
+ , filepath >=1.4.2 && <1.5
+ , galois-fft >=0.1.0 && <0.2
+ , galois-field >=1.0.0 && <2.0.0
+ , MonadRandom >=0.5.1 && <0.6
+ , poly >=0.3.2 && <0.4
+ , process-extras >=0.7.4 && <0.8
+ , protolude >=0.2 && <0.3
+ , semirings >=0.5.0 && <0.6
+ , text >=1.2.3 && <1.3
+ , vector >=0.12 && <0.13
+ , wl-pprint-text >=1.2.0 && <1.3
+
+ default-language: Haskell2010
+
+test-suite circuit-tests
+ type: exitcode-stdio-1.0
+ main-is: Main.hs
+ other-modules:
+ Paths_arithmetic_circuits
+ Test.Circuit.Affine
+ Test.Circuit.Arithmetic
+ Test.Circuit.Expr
+ Test.QAP
+
+ hs-source-dirs: test
+ default-extensions:
+ NoImplicitPrelude
+ GADTs
+ LambdaCase
+ OverloadedStrings
+
+ ghc-options: -freverse-errors -O2 -Wall -main-is Main
+ build-depends:
+ aeson >=1.4 && <1.5
+ , arithmetic-circuits
+ , base >=4.10 && <5
+ , bulletproofs >=1.1.0 && <1.2
+ , containers >=0.6.0 && <0.7
+ , elliptic-curve >=0.3 && <0.4
+ , filepath >=1.4.2 && <1.5
+ , galois-fft >=0.1.0 && <0.2
+ , galois-field >=1.0.0 && <2.0.0
+ , MonadRandom >=0.5.1 && <0.6
+ , pairing >=1.0 && <1.1
+ , poly >=0.3.2 && <0.4
+ , process-extras >=0.7.4 && <0.8
+ , protolude >=0.2 && <0.3
+ , QuickCheck >=2.12 && <2.14
+ , quickcheck-instances >=0.3 && <0.4
+ , semirings >=0.5.0 && <0.6
+ , tasty >=1.2 && <1.3
+ , tasty-discover >=4.2 && <4.3
+ , tasty-hunit >=0.10 && <0.11
+ , tasty-quickcheck >=0.10 && <0.11
+ , text >=1.2.3 && <1.3
+ , vector >=0.12 && <0.13
+ , wl-pprint-text >=1.2.0 && <1.3
+
+ default-language: Haskell2010
+
+test-suite readme-test
+ type: exitcode-stdio-1.0
+ main-is: README.lhs
+ other-modules: Paths_arithmetic_circuits
+ default-extensions:
+ NoImplicitPrelude
+ GADTs
+ LambdaCase
+ OverloadedStrings
+
+ ghc-options: -freverse-errors -O2 -Wall -pgmL markdown-unlit
+ build-depends:
+ aeson >=1.4 && <1.5
+ , arithmetic-circuits
+ , base >=4.10 && <5
+ , bulletproofs >=1.1.0 && <1.2
+ , containers >=0.6.0 && <0.7
+ , elliptic-curve >=0.3 && <0.4
+ , filepath >=1.4.2 && <1.5
+ , galois-fft >=0.1.0 && <0.2
+ , galois-field >=1.0.0 && <2.0.0
+ , markdown-unlit >=0.5 && <0.6
+ , MonadRandom >=0.5.1 && <0.6
+ , pairing >=1.0 && <1.1
+ , poly >=0.3.2 && <0.4
+ , process-extras >=0.7.4 && <0.8
+ , protolude >=0.2 && <0.3
+ , semirings >=0.5.0 && <0.6
+ , text >=1.2.3 && <1.3
+ , vector >=0.12 && <0.13
+ , wl-pprint-text >=1.2.0 && <1.3
+
+ default-language: Haskell2010
+
+benchmark circuit-benchmarks
+ type: exitcode-stdio-1.0
+ main-is: Main.hs
+ other-modules:
+ Circuit
+ Paths_arithmetic_circuits
+
+ hs-source-dirs: bench
+ default-extensions:
+ NoImplicitPrelude
+ GADTs
+ LambdaCase
+ OverloadedStrings
+
+ ghc-options: -freverse-errors -O2 -Wall -main-is Main
+ build-depends:
+ aeson >=1.4 && <1.5
+ , arithmetic-circuits
+ , base >=4.10 && <5
+ , bulletproofs >=1.1.0 && <1.2
+ , containers >=0.6.0 && <0.7
+ , criterion >=1.5 && <1.6
+ , elliptic-curve >=0.3 && <0.4
+ , filepath >=1.4.2 && <1.5
+ , galois-fft >=0.1.0 && <0.2
+ , galois-field >=1.0.0 && <2.0.0
+ , MonadRandom >=0.5.1 && <0.6
+ , pairing >=1.0 && <1.1
+ , poly >=0.3.2 && <0.4
+ , process-extras >=0.7.4 && <0.8
+ , protolude >=0.2 && <0.3
+ , semirings >=0.5.0 && <0.6
+ , text >=1.2.3 && <1.3
+ , vector >=0.12 && <0.13
+ , wl-pprint-text >=1.2.0 && <1.3
+
+ default-language: Haskell2010
diff --git a/bench/Circuit.hs b/bench/Circuit.hs
new file mode 100644
--- /dev/null
+++ b/bench/Circuit.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+module Circuit (benchmarks) where
+
+import Protolude
+
+import Circuit.Affine
+import Circuit.Arithmetic
+import Criterion.Main
+import Data.Curve.Weierstrass.BN254 (Fr)
+import qualified Data.Map as Map
+import Data.Pairing.BN254 (getRootOfUnity)
+import Fresh
+import QAP
+
+
+program :: ArithCircuit Fr
+program = ArithCircuit
+ [ Mul (Var (InputWire 0)) (Var (InputWire 1)) (IntermediateWire 0)
+ , Mul (Var (IntermediateWire 0))(Add (Var (InputWire 0)) (Var (InputWire 2))) (OutputWire 0)
+ ]
+
+input :: Map.Map Int Fr
+input = Map.fromList [(0, 7), (1, 5), (2, 4)]
+
+benchmarks :: [Benchmark]
+benchmarks
+ = [ bench "evaluating circuit"
+ $ whnf (evalArithCircuit lookupAtWire updateAtWire program) (initialQapSet input)
+ , bench "creating QAP (no interpolation)"
+ $ nf (\c -> arithCircuitToGenQAP (evalFresh $ generateRoots (fromIntegral <$> fresh) c) c) program
+ , bench "creating QAP (fast interpolation)"
+ $ nf (\c -> arithCircuitToQAPFFT getRootOfUnity (evalFresh $ generateRoots (fromIntegral <$> fresh) c) c) program
+ , bench "creating QAP (slow interpolation)"
+ $ nf (\c -> arithCircuitToQAP (evalFresh $ generateRoots (fromIntegral <$> fresh) c) c) program
+ ]
+
diff --git a/bench/Main.hs b/bench/Main.hs
new file mode 100644
--- /dev/null
+++ b/bench/Main.hs
@@ -0,0 +1,16 @@
+{-# LANGUAGE NoImplicitPrelude #-}
+
+-- To get the benchmarking data, run "stack bench".
+
+module Main where
+
+import Protolude
+
+import Criterion.Main
+
+import qualified Circuit
+
+main :: IO ()
+main = defaultMain
+ [ bgroup "Circuit to QAP translation" Circuit.benchmarks
+ ]
diff --git a/src/Circuit.hs b/src/Circuit.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit.hs
@@ -0,0 +1,10 @@
+module Circuit
+ ( module Circuit.Arithmetic,
+ module Circuit.Lang,
+ module Circuit.Expr,
+ )
+where
+
+import Circuit.Arithmetic
+import Circuit.Expr
+import Circuit.Lang
diff --git a/src/Circuit/Affine.hs b/src/Circuit/Affine.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Affine.hs
@@ -0,0 +1,125 @@
+{-# LANGUAGE DeriveAnyClass, DeriveGeneric, LambdaCase, StrictData #-}
+
+-- | Definition of arithmetic circuits that only contain addition,
+-- scalar multiplications and constant gates, along with its direct
+-- evaluation and translation into affine maps.
+module Circuit.Affine
+ ( AffineCircuit (..),
+ collectInputsAffine,
+ mapVarsAffine,
+ evalAffineCircuit,
+ affineCircuitToAffineMap,
+ evalAffineMap,
+ dotProduct,
+ )
+where
+
+import Data.Aeson (FromJSON, ToJSON)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Protolude
+import Text.PrettyPrint.Leijen.Text (Doc, Pretty(..), parens, text,
+ (<+>))
+
+-- | Arithmetic circuits without multiplication, i.e. circuits
+-- describe affine transformations.
+data AffineCircuit i f
+ = Add (AffineCircuit i f) (AffineCircuit i f)
+ | ScalarMul f (AffineCircuit i f)
+ | ConstGate f
+ | Var i
+ deriving (Read, Eq, Show, Generic, NFData, FromJSON, ToJSON)
+
+collectInputsAffine :: Ord i => AffineCircuit i f -> [i]
+collectInputsAffine = \case
+ Add l r -> collectInputsAffine l ++ collectInputsAffine r
+ ScalarMul _ x -> collectInputsAffine x
+ ConstGate _ -> []
+ Var i -> [i]
+
+instance (Pretty i, Show f) => Pretty (AffineCircuit i f) where
+ pretty = prettyPrec 0
+ where
+ prettyPrec :: (Pretty i, Show f) => Int -> AffineCircuit i f -> Doc
+ prettyPrec p e =
+ case e of
+ Var v ->
+ pretty v
+ ConstGate f ->
+ text $ show f
+ ScalarMul f e1 ->
+ text (show f) <+> text "*" <+> parensPrec 7 p (prettyPrec p e1)
+ Add e1 e2 ->
+ parensPrec 6 p $
+ prettyPrec 6 e1
+ <+> text "+"
+ <+> prettyPrec 6 e2
+
+parensPrec :: Int -> Int -> Doc -> Doc
+parensPrec opPrec p = if p > opPrec then parens else identity
+
+-- | Apply mapping to variable names, i.e. rename variables. (Ideally
+-- the mapping is injective.)
+mapVarsAffine :: (i -> j) -> AffineCircuit i f -> AffineCircuit j f
+mapVarsAffine f = \case
+ Add l r -> Add (mapVarsAffine f l) (mapVarsAffine f r)
+ ScalarMul s expr -> ScalarMul s $ mapVarsAffine f expr
+ ConstGate c -> ConstGate c
+ Var i -> Var $ f i
+
+-- | Evaluate the arithmetic circuit without mul-gates on the given
+-- input. Variable map is assumed to have all the variables referred
+-- to in the circuit. Failed lookups are currently treated as 0.
+evalAffineCircuit ::
+ Num f =>
+ -- | lookup function for variable mapping
+ (i -> vars -> Maybe f) ->
+ -- | variables
+ vars ->
+ -- | circuit to evaluate
+ AffineCircuit i f ->
+ f
+evalAffineCircuit lookupVar vars = \case
+ ConstGate f -> f
+ Var i -> fromMaybe 0 $ lookupVar i vars
+ Add l r -> evalAffineCircuit lookupVar vars l + evalAffineCircuit lookupVar vars r
+ ScalarMul scalar expr -> evalAffineCircuit lookupVar vars expr * scalar
+
+-- | Convert non-mul circuit to a vector representing the evaluation
+-- function. We use a @Map@ to represent the potentially sparse vector.
+affineCircuitToAffineMap ::
+ (Num f, Ord i) =>
+ -- | circuit to translate
+ AffineCircuit i f ->
+ -- | constant part and non-constant part
+ (f, Map i f)
+affineCircuitToAffineMap = \case
+ Var i -> (0, Map.singleton i 1)
+ Add l r -> (constLeft + constRight, Map.unionWith (+) vecLeft vecRight)
+ where
+ (constLeft, vecLeft) = affineCircuitToAffineMap l
+ (constRight, vecRight) = affineCircuitToAffineMap r
+ ScalarMul scalar expr -> (scalar * constExpr, fmap (scalar *) vecExpr)
+ where
+ (constExpr, vecExpr) = affineCircuitToAffineMap expr
+ ConstGate f -> (f, Map.empty)
+
+-- | Evaluating the affine map representing the arithmetic circuit
+-- without mul-gates against inputs. If the input map does not have a
+-- variable that is referred to in the affine map, then it is treated
+-- as a 0.
+evalAffineMap ::
+ (Num f, Ord i) =>
+ -- | program split into constant and non-constant part
+ (f, Map i f) ->
+ -- | input variables
+ Map i f ->
+ f
+evalAffineMap (constPart, linearPart) input =
+ constPart + dotProduct linearPart input
+
+dotProduct :: (Num f, Ord i) => Map i f -> Map i f -> f
+dotProduct inp comp =
+ sum
+ . Map.elems
+ $ Map.mapWithKey (\ix c -> c * Map.findWithDefault 0 ix inp) comp
diff --git a/src/Circuit/Arithmetic.hs b/src/Circuit/Arithmetic.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Arithmetic.hs
@@ -0,0 +1,243 @@
+{-# LANGUAGE DeriveAnyClass, DeriveGeneric, LambdaCase, ScopedTypeVariables,
+ StrictData #-}
+
+-- | Definition of arithmetic circuits: one with a single
+-- multiplication gate with affine inputs and another variant with an
+-- arbitrary number of such gates.
+module Circuit.Arithmetic
+ ( Gate (..),
+ mapVarsGate,
+ collectInputsGate,
+ outputWires,
+ ArithCircuit (..),
+ fetchVars,
+ generateRoots,
+ validArithCircuit,
+ Wire (..),
+ evalGate,
+ evalArithCircuit,
+ unsplit,
+ )
+where
+
+import Circuit.Affine (AffineCircuit(..), collectInputsAffine,
+ evalAffineCircuit, mapVarsAffine)
+import Data.Aeson (FromJSON, ToJSON)
+import Protolude
+import Text.PrettyPrint.Leijen.Text as PP (Pretty(..), hsep, list, parens, text,
+ vcat)
+
+-- | Wires are can be labeled in the ways given in this data type
+data Wire
+ = InputWire Int
+ | IntermediateWire Int
+ | OutputWire Int
+ deriving (Show, Eq, Ord, Generic, NFData, ToJSON, FromJSON)
+
+instance Pretty Wire where
+ pretty (InputWire v) = text "input_" <> pretty v
+ pretty (IntermediateWire v) = text "imm_" <> pretty v
+ pretty (OutputWire v) = text "output_" <> pretty v
+
+-- | An arithmetic circuit with a single multiplication gate.
+data Gate i f
+ = Mul
+ { mulLeft :: AffineCircuit i f,
+ mulRight :: AffineCircuit i f,
+ mulOutput :: i
+ }
+ | Equal
+ { eqInput :: i,
+ eqMagic :: i,
+ eqOutput :: i
+ }
+ | Split
+ { splitInput :: i,
+ splitOutputs :: [i]
+ }
+ deriving (Show, Eq, Generic, NFData, FromJSON, ToJSON)
+
+collectInputsGate :: Ord i => Gate i f -> [i]
+collectInputsGate = \case
+ Mul l r _ -> collectInputsAffine l ++ collectInputsAffine r
+ _ -> panic "collectInputsGate: only supports mul gates"
+
+-- | List output wires of a gate
+outputWires :: Gate i f -> [i]
+outputWires = \case
+ Mul _ _ out -> [out]
+ Equal _ _ out -> [out]
+ Split _ outs -> outs
+
+instance (Pretty i, Show f) => Pretty (Gate i f) where
+ pretty (Mul l r o) =
+ hsep
+ [ pretty o,
+ text ":=",
+ parens (pretty l),
+ text "*",
+ parens (pretty r)
+ ]
+ pretty (Equal i _ o) =
+ hsep
+ [ pretty o,
+ text ":=",
+ pretty i,
+ text "== 0 ? 0 : 1"
+ ]
+ pretty (Split inp outputs) =
+ hsep
+ [ PP.list (map pretty outputs),
+ text ":=",
+ text "split",
+ pretty inp
+ ]
+
+-- | Apply mapping to variable names, i.e. rename variables. (Ideally
+-- the mapping is injective.)
+mapVarsGate :: (i -> j) -> Gate i f -> Gate j f
+mapVarsGate f = \case
+ Mul l r o -> Mul (mapVarsAffine f l) (mapVarsAffine f r) (f o)
+ Equal i j o -> Equal (f i) (f j) (f o)
+ Split i os -> Split (f i) (fmap f os)
+
+-- | Evaluate a single gate
+evalGate ::
+ (Bits f, Fractional f) =>
+ -- | lookup a value at a wire
+ (i -> vars -> Maybe f) ->
+ -- | update a value at a wire
+ (i -> f -> vars -> vars) ->
+ -- | context before evaluation
+ vars ->
+ -- | gate
+ Gate i f ->
+ -- | context after evaluation
+ vars
+evalGate lookupVar updateVar vars gate =
+ case gate of
+ Mul l r outputWire ->
+ let lval = evalAffineCircuit lookupVar vars l
+ rval = evalAffineCircuit lookupVar vars r
+ res = lval * rval
+ in updateVar outputWire res vars
+ Equal i m outputWire ->
+ case lookupVar i vars of
+ Nothing ->
+ panic "evalGate: the impossible happened"
+ Just inp ->
+ let res = if inp == 0 then 0 else 1
+ mid = if inp == 0 then 0 else recip inp
+ in updateVar outputWire res $
+ updateVar m mid vars
+ Split i os ->
+ case lookupVar i vars of
+ Nothing ->
+ panic "evalGate: the impossible happened"
+ Just inp ->
+ let bool2val True = 1
+ bool2val False = 0
+ setWire (ix, oldEnv) currentOut =
+ ( ix + 1,
+ updateVar currentOut (bool2val $ testBit inp ix) oldEnv
+ )
+ in snd . foldl setWire (0, vars) $ os
+
+-- | A circuit is a list of multiplication gates along with their
+-- output wire labels (which can be intermediate or actual outputs).
+newtype ArithCircuit f = ArithCircuit [Gate Wire f]
+ deriving (Eq, Show, Generic, NFData, FromJSON, ToJSON)
+
+instance Show f => Pretty (ArithCircuit f) where
+ pretty (ArithCircuit gs) = vcat . map pretty $ gs
+
+-- | Check whether an arithmetic circuit does not refer to
+-- intermediate wires before they are defined and whether output wires
+-- are not used as input wires.
+validArithCircuit ::
+ ArithCircuit f -> Bool
+validArithCircuit (ArithCircuit gates) =
+ noRefsToUndefinedWires
+ where
+ noRefsToUndefinedWires =
+ fst $
+ foldl
+ ( \(res, definedWires) gate ->
+ ( res
+ && all isNotInput (outputWires gate)
+ && all (validWire definedWires) (fetchVarsGate gate),
+ outputWires gate ++ definedWires
+ )
+ )
+ (True, [])
+ gates
+ isNotInput (InputWire _) = False
+ isNotInput (OutputWire _) = True
+ isNotInput (IntermediateWire _) = True
+ validWire _ (InputWire _) = True
+ validWire _ (OutputWire _) = False
+ validWire definedWires i@(IntermediateWire _) = i `elem` definedWires
+ fetchVarsGate (Mul l r _) = fetchVars l ++ fetchVars r
+ fetchVarsGate (Equal i _ _) = [i] -- we can ignore the magic
+ -- variable "m", as it is filled
+ -- in when evaluating the circuit
+ fetchVarsGate (Split i _) = [i]
+
+fetchVars :: AffineCircuit Wire f -> [Wire]
+fetchVars (Var i) = [i]
+fetchVars (ConstGate _) = []
+fetchVars (ScalarMul _ c) = fetchVars c
+fetchVars (Add l r) = fetchVars l ++ fetchVars r
+
+-- | Generate enough roots for a circuit
+generateRoots ::
+ Applicative m =>
+ m f ->
+ ArithCircuit f ->
+ m [[f]]
+generateRoots _ (ArithCircuit []) =
+ pure []
+generateRoots takeRoot (ArithCircuit (gate : gates)) =
+ case gate of
+ Mul {} ->
+ (\r rs -> [r] : rs)
+ <$> takeRoot
+ <*> generateRoots takeRoot (ArithCircuit gates)
+ Equal {} ->
+ (\r0 r1 rs -> [r0, r1] : rs)
+ <$> takeRoot
+ <*> takeRoot
+ <*> generateRoots takeRoot (ArithCircuit gates)
+ Split _ outputs ->
+ (\r0 rOutputs rRest -> (r0 : rOutputs) : rRest)
+ <$> takeRoot
+ <*> traverse (const takeRoot) outputs
+ <*> generateRoots takeRoot (ArithCircuit gates)
+
+-- | Evaluate an arithmetic circuit on a given environment containing
+-- the inputs. Outputs the entire environment (outputs, intermediate
+-- values and inputs).
+evalArithCircuit ::
+ forall f vars.
+ (Bits f, Fractional f) =>
+ -- | lookup a value at a wire
+ (Wire -> vars -> Maybe f) ->
+ -- | update a value at a wire
+ (Wire -> f -> vars -> vars) ->
+ -- | circuit to evaluate
+ ArithCircuit f ->
+ -- | input variables
+ vars ->
+ -- | input and output variables
+ vars
+evalArithCircuit lookupVar updateVar (ArithCircuit gates) vars =
+ foldl' (evalGate lookupVar updateVar) vars gates
+
+-- | Turn a binary expansion back into a single value.
+unsplit ::
+ Num f =>
+ -- | (binary) wires containing a binary expansion,
+ -- small-endian
+ [Wire] ->
+ AffineCircuit Wire f
+unsplit = snd . foldl (\(ix, rest) wire -> (ix + (1 :: Integer), Add rest (ScalarMul (2 ^ ix) (Var wire)))) (0, ConstGate 0)
diff --git a/src/Circuit/Bulletproofs.hs b/src/Circuit/Bulletproofs.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Bulletproofs.hs
@@ -0,0 +1,554 @@
+{-# LANGUAGE DeriveAnyClass, DeriveGeneric, LambdaCase,
+ RecordWildCards, ScopedTypeVariables, ViewPatterns #-}
+
+-- | Translate arithmetic circuits into a Hadamard product equation
+-- and linear constraints.
+module Circuit.Bulletproofs
+ ( setupProof,
+ SetupProof (..),
+ AltArithCircuit,
+ LinearConstraint (..),
+ GateConstraint (..),
+ rewire,
+ rewireCircuit,
+ circuitToConstraints,
+ transformInputs,
+ evalCircuit,
+ computeBulletproofsAssignment,
+ )
+where
+
+import qualified Bulletproofs.ArithmeticCircuit as Bulletproofs
+import Bulletproofs.Utils (commit)
+import Circuit.Affine (AffineCircuit(..),
+ affineCircuitToAffineMap,
+ dotProduct,
+ evalAffineCircuit)
+import Circuit.Arithmetic (ArithCircuit(..), Gate(..),
+ Wire(..), collectInputsGate,
+ mapVarsGate, outputWires)
+import Control.Monad.Random (MonadRandom, getRandomR)
+import Data.Aeson (FromJSON, ToJSON)
+import Data.Curve.Weierstrass.SECP256K1 (Fr, PA)
+import qualified Data.Map as Map
+import Protolude
+import Text.PrettyPrint.Leijen.Text as PP (Pretty(..), enclose,
+ lbracket, rbracket,
+ text, vcat, (<+>))
+
+newtype AltArithCircuit f = AltArithCircuit [Gate AltWire f]
+ deriving (Show, Generic, NFData, FromJSON, ToJSON)
+
+instance (Pretty f, Show f) => Pretty (AltArithCircuit f) where
+ pretty (AltArithCircuit l) = pretty l
+
+-- | Use different wire type as required for the constraints generated
+-- in this module.
+rewireCircuit :: ArithCircuit f -> AltArithCircuit f
+rewireCircuit (ArithCircuit oldGates) = AltArithCircuit newGates
+ where
+ newGates = map (mapVarsGate (rewire maxMid)) oldGates
+ getMid (IntermediateWire x) = x
+ getMid _ = 0
+ maxMid :: Int
+ maxMid = maximumSafe . map getMid . concatMap outputWires $ oldGates
+
+-- | Replace all input wires v_i with a mul-gate (v_i * 1). This means
+-- that when we translate it to linear constraints, the weights matrix
+-- for V will always be of rank m, where m is the number of input
+-- wires, as is required by the Bulletproof protocol.
+transformInputs :: forall f. Num f => AltArithCircuit f -> AltArithCircuit f
+transformInputs (AltArithCircuit oldGates) = AltArithCircuit newGates
+ where
+ newGates :: [Gate AltWire f]
+ newGates = inputGates ++ map rewireInput oldGates
+ maxInp :: Int
+ maxInp = maximumSafe . mapMaybe getInp . concatMap collectInputsGate $ oldGates
+ getInp (InWire x) = Just x
+ getInp _ = Nothing
+ maxOutp :: Int
+ maxOutp = maximumSafe . mapMaybe getOutp . concatMap outputWires $ oldGates
+ getOutp (OutWire x) = Just x
+ getOutp _ = Nothing
+ inputGates :: [Gate AltWire f]
+ inputGates = map inputGate [0 .. maxInp]
+ inputGate :: Int -> Gate AltWire f
+ inputGate i = Mul (Var (InWire i)) (ConstGate 1) (OutWire (maxOutp + 1 + i))
+ rewireInput :: Gate AltWire f -> Gate AltWire f
+ rewireInput =
+ mapVarsGate
+ ( \case
+ InWire i -> OutWire (maxOutp + 1 + i)
+ w -> w
+ )
+
+maximumSafe :: (Num f, Ord f) => [f] -> f
+maximumSafe [] = 0
+maximumSafe ls = maximum ls
+
+rewire :: Int -> Wire -> AltWire
+rewire _maxMid (InputWire i) = InWire i
+rewire maxMid (OutputWire i) = OutWire (i + maxMid + 1)
+rewire _maxMid (IntermediateWire i) = OutWire i
+
+-- | Distinguish between left/right/out and in wires.
+data AltWire
+ = LeftWire Int
+ | RightWire Int
+ | OutWire Int
+ | InWire Int
+ deriving (Show, Eq, Ord, Generic, NFData, FromJSON, ToJSON)
+
+instance Pretty AltWire where
+ pretty (LeftWire v) = text "left_" <> pretty v
+ pretty (RightWire v) = text "right_" <> pretty v
+ pretty (OutWire v) = text "out_" <> pretty v
+ pretty (InWire v) = text "in_" <> pretty v
+
+getAltWireNumber :: AltWire -> Int
+getAltWireNumber = \case
+ LeftWire i -> i
+ RightWire i -> i
+ OutWire i -> i
+ InWire i -> i
+
+-- Should we unify this type with the assignments, a la QapSet?
+data LinearConstraint f
+ = LinearConstraint
+ { -- | wL
+ lcWeightsLeft :: Map Int f,
+ -- | wR
+ lcWeightsRight :: Map Int f,
+ -- | wO
+ lcWeightsOut :: Map Int f,
+ -- | wV
+ lcWeightsIn :: Map Int f,
+ -- | c
+ lcConstant :: f
+ }
+ deriving (Show, Generic, FromJSON, ToJSON)
+
+instance Pretty f => Pretty (LinearConstraint f) where
+ pretty (LinearConstraint left right out lIn cnst) =
+ vcat
+ [ text "lc left:" <+> pretty (ppMap left),
+ text "lc right:" <+> pretty (ppMap right),
+ text "lc out:" <+> pretty (ppMap out),
+ text "lc in:" <+> pretty (ppMap lIn),
+ text "lc constant:" <+> pretty cnst
+ ]
+ where
+ ppMap =
+ vcat
+ . map (\(ix, x) -> enclose lbracket rbracket (pretty ix) <+> pretty x)
+ . Map.toList
+
+data MulConstraint i
+ = MulConstraint
+ { -- | pointer to aLi
+ mcLeft :: i,
+ -- | pointer to aRi
+ mcRight :: i,
+ -- | pointer to aOi
+ mcOut :: i
+ }
+ deriving (Show, Generic, FromJSON, ToJSON)
+
+instance Pretty i => Pretty (MulConstraint i) where
+ pretty (MulConstraint left right out) =
+ vcat
+ [ text "mc left:" <+> pretty left,
+ text "mc right:" <+> pretty right,
+ text "mc out:" <+> pretty out
+ ]
+
+data GateConstraint i f
+ = GateConstraint
+ { gcLinearConstraintLeft :: LinearConstraint f,
+ gcLinearConstraintRight :: LinearConstraint f,
+ gcMulConstraint :: MulConstraint i
+ }
+ deriving (Show, Generic, FromJSON, ToJSON)
+
+instance (Pretty i, Pretty f) => Pretty (GateConstraint i f) where
+ pretty (GateConstraint left right mul) =
+ vcat
+ [ text "linear constraint left:" <+> pretty left,
+ text "linear constraint right:" <+> pretty right,
+ text "mul constraint:" <+> pretty mul
+ ]
+
+-- | Map AltWire f is isomorphic to Assignment f, assuming the lengths
+-- are correct. We can think of @Map Int f@ as a (potentially) sparse
+-- vector.
+data Assignment f
+ = Assignment
+ { -- | length is number of gates
+ assignmentLeft :: Map Int f,
+ -- | length is number of gates
+ assignmentRight :: Map Int f,
+ -- | length is number of gates
+ assignmentOut :: Map Int f,
+ -- | length is number of inputs
+ assignmentIn :: Map Int f
+ }
+ deriving (Show, Generic, FromJSON, ToJSON)
+
+assignmentToMap :: Assignment f -> Map AltWire f
+assignmentToMap Assignment {..} =
+ Map.unions
+ [ Map.mapKeys LeftWire assignmentLeft,
+ Map.mapKeys RightWire assignmentRight,
+ Map.mapKeys OutWire assignmentOut,
+ Map.mapKeys InWire assignmentIn
+ ]
+
+mapToAssignment :: Map AltWire f -> Assignment f
+mapToAssignment wireMap = Assignment
+ { assignmentLeft =
+ Map.mapKeys getAltWireNumber . Map.filterWithKey isLeftWire $ wireMap,
+ assignmentRight =
+ Map.mapKeys getAltWireNumber . Map.filterWithKey isRightWire $ wireMap,
+ assignmentOut =
+ Map.mapKeys getAltWireNumber . Map.filterWithKey isOutWire $ wireMap,
+ assignmentIn =
+ Map.mapKeys getAltWireNumber . Map.filterWithKey isInWire $ wireMap
+ }
+
+linearConstraintToAffineMap :: LinearConstraint f -> (f, Map AltWire f)
+linearConstraintToAffineMap LinearConstraint {..} =
+ ( lcConstant,
+ Map.unions
+ [ Map.mapKeys LeftWire lcWeightsLeft,
+ Map.mapKeys RightWire lcWeightsRight,
+ Map.mapKeys OutWire lcWeightsOut,
+ Map.mapKeys InWire lcWeightsIn
+ ]
+ )
+
+affineMapToLinearConstraint :: Num f => (f, Map AltWire f) -> LinearConstraint f
+affineMapToLinearConstraint (constant, wireMap) = LinearConstraint
+ { lcWeightsLeft =
+ fmap negate . Map.mapKeys getAltWireNumber . Map.filterWithKey isLeftWire $ wireMap,
+ lcWeightsRight =
+ fmap negate . Map.mapKeys getAltWireNumber . Map.filterWithKey isRightWire $ wireMap,
+ lcWeightsOut =
+ fmap negate . Map.mapKeys getAltWireNumber . Map.filterWithKey isOutWire $ wireMap,
+ lcWeightsIn =
+ Map.mapKeys getAltWireNumber . Map.filterWithKey isInWire $ wireMap,
+ lcConstant =
+ constant
+ }
+
+updateConstraint :: f -> LinearConstraint f -> AltWire -> LinearConstraint f
+updateConstraint x lc = \case
+ LeftWire i -> lc {lcWeightsLeft = Map.insert i x $ lcWeightsLeft lc}
+ RightWire i -> lc {lcWeightsRight = Map.insert i x $ lcWeightsRight lc}
+ OutWire i -> lc {lcWeightsOut = Map.insert i x $ lcWeightsOut lc}
+ InWire i -> lc {lcWeightsIn = Map.insert i x $ lcWeightsIn lc}
+
+isLeftWire :: AltWire -> f -> Bool
+isLeftWire (LeftWire _) _ = True
+isLeftWire _ _ = False
+
+isRightWire :: AltWire -> f -> Bool
+isRightWire (RightWire _) _ = True
+isRightWire _ _ = False
+
+isOutWire :: AltWire -> f -> Bool
+isOutWire (OutWire _) _ = True
+isOutWire _ _ = False
+
+isInWire :: AltWire -> f -> Bool
+isInWire (InWire _) _ = True
+isInWire _ _ = False
+
+lookupWire :: AltWire -> Assignment f -> Maybe f
+lookupWire w Assignment {..} = case w of
+ LeftWire i -> Map.lookup i assignmentLeft
+ RightWire i -> Map.lookup i assignmentRight
+ OutWire i -> Map.lookup i assignmentOut
+ InWire i -> Map.lookup i assignmentIn
+
+updateWire :: AltWire -> f -> Assignment f -> Assignment f
+updateWire (LeftWire i) x assign =
+ assign {assignmentLeft = Map.insert i x (assignmentLeft assign)}
+updateWire (RightWire i) x assign =
+ assign {assignmentRight = Map.insert i x (assignmentRight assign)}
+updateWire (OutWire i) x assign =
+ assign {assignmentOut = Map.insert i x (assignmentOut assign)}
+updateWire (InWire i) x assign =
+ assign {assignmentIn = Map.insert i x (assignmentIn assign)}
+
+inputToAssignment :: Map Int f -> Assignment f
+inputToAssignment inps = Assignment
+ { assignmentLeft = Map.empty,
+ assignmentRight = Map.empty,
+ assignmentOut = Map.empty,
+ assignmentIn = inps
+ }
+
+-- This is slightly different from ArithmeticCircuit.evalGate in that
+-- this one also assigns values to the left and right wires.
+evalGate ::
+ (Num f) =>
+ -- | initial context
+ Assignment f ->
+ -- | gate
+ Gate AltWire f ->
+ -- | context after evaluation
+ Assignment f
+evalGate vars (Mul lhs rhs (OutWire gateNumber)) =
+ let lval = evalAffineCircuit lookupWire vars lhs
+ rval = evalAffineCircuit lookupWire vars rhs
+ res = lval * rval
+ in updateWire (LeftWire gateNumber) lval
+ $ updateWire (RightWire gateNumber) rval
+ $ updateWire (OutWire gateNumber) res vars
+evalGate _ _ = panic "evalGate: gate malformed"
+
+evalCircuit ::
+ Num f =>
+ -- | circuit to evaluate
+ AltArithCircuit f ->
+ -- | initial context (containing input variables)
+ Assignment f ->
+ -- | input and output variables
+ Assignment f
+evalCircuit (AltArithCircuit gates) vars =
+ foldl' evalGate vars gates
+
+checkConstraints :: (Num f, Eq f) => GateConstraint AltWire f -> Assignment f -> Bool
+checkConstraints (GateConstraint constraintL constraintR constraintMul) assign =
+ and
+ [ checkLinearConstraint constraintL assign,
+ checkLinearConstraint constraintR assign,
+ checkMulConstraint constraintMul assign
+ ]
+
+checkLinearConstraint ::
+ (Num f, Eq f) =>
+ LinearConstraint f ->
+ Assignment f ->
+ Bool
+checkLinearConstraint LinearConstraint {..} Assignment {..} =
+ lcWeightsLeft `dotProduct` assignmentLeft
+ + lcWeightsRight `dotProduct` assignmentRight
+ + lcWeightsOut `dotProduct` assignmentOut
+ == lcWeightsIn `dotProduct` assignmentIn + lcConstant
+
+checkMulConstraint ::
+ (Num f, Eq f) =>
+ MulConstraint AltWire ->
+ Assignment f ->
+ Bool
+checkMulConstraint (MulConstraint l r o) vars = fromMaybe False $ do
+ lval <- lookupWire l vars
+ rval <- lookupWire r vars
+ oval <- lookupWire o vars
+ pure $ lval * rval == oval
+
+-- | Generate constraints for a single multiplication gate
+gateToConstraints :: Num f => Gate AltWire f -> GateConstraint AltWire f
+gateToConstraints (Mul lhs rhs (OutWire gateNumber)) =
+ let affineMapLeft = affineCircuitToAffineMap lhs
+ affineMapRight = affineCircuitToAffineMap rhs
+ in GateConstraint
+ { gcLinearConstraintLeft =
+ updateConstraint 1 (affineMapToLinearConstraint affineMapLeft) (LeftWire gateNumber),
+ gcLinearConstraintRight =
+ updateConstraint 1 (affineMapToLinearConstraint affineMapRight) (RightWire gateNumber),
+ gcMulConstraint =
+ MulConstraint (LeftWire gateNumber) (RightWire gateNumber) (OutWire gateNumber)
+ }
+gateToConstraints _ = panic "gateToConstraints: gate malformed"
+
+-- spits out constraints "in reverse"
+circuitToConstraints :: Num f => AltArithCircuit f -> [GateConstraint AltWire f]
+circuitToConstraints (AltArithCircuit gates) =
+ foldl' (\cs gate -> gateToConstraints gate : cs) [] gates
+
+-- XXX: migrate example out of core library before release
+
+---------------------------------------------------------
+-- Example of an arithmetic circuit with a single gate
+---------------------------------------------------------
+
+-- (v0 + v1) * (v2 + 10)
+exampleGate :: Num f => Gate AltWire f
+exampleGate = Mul
+ { mulLeft = Add (Var $ InWire 0) (Var $ InWire 1),
+ mulRight = Add (Var $ InWire 2) (ConstGate 10),
+ mulOutput = OutWire 0
+ }
+
+exampleEqns :: Num f => LinearConstraint f
+exampleEqns = LinearConstraint
+ { lcWeightsLeft = Map.fromList [(0, 1)],
+ lcWeightsRight = Map.fromList [(0, 0)],
+ lcWeightsOut = Map.fromList [(0, 0)],
+ lcWeightsIn = Map.fromList [(0, 1)],
+ lcConstant = 5
+ }
+
+exampleAssignment :: Num f => [f] -> Assignment f
+exampleAssignment [v0, v1, v2] = Assignment
+ { assignmentLeft = Map.fromList [(0, v0 + v1)],
+ assignmentRight = Map.fromList [(0, v2 + 10)],
+ assignmentOut = Map.fromList [(0, (v0 + v1) * (v2 + 10))],
+ assignmentIn = Map.fromList [(0, v0), (1, v1), (2, v2)]
+ }
+exampleAssignment _ = panic "Invalid inputs for this example"
+
+---------------------------------------------------------
+-- Example of an arithmetic circuit with multiple gates
+-- (Example from BCC 16. Appendix A. Efficient zero-knowledge
+-- arguments for arithmetic circuits in the discrete log setting.)
+---------------------------------------------------------
+
+exampleMultiGates :: Num f => [Gate AltWire f]
+exampleMultiGates =
+ [ Mul
+ { mulLeft = Var $ InWire 0,
+ mulRight = Var $ InWire 1,
+ mulOutput = OutWire 0
+ },
+ Mul
+ { mulLeft = Var $ InWire 2,
+ mulRight = Var $ InWire 3,
+ mulOutput = OutWire 1
+ },
+ Mul
+ { mulLeft = Var $ InWire 4,
+ mulRight = Var $ InWire 5,
+ mulOutput = OutWire 2
+ },
+ Mul
+ { mulLeft = Var $ OutWire 0,
+ mulRight = Var $ OutWire 1,
+ mulOutput = OutWire 3
+ },
+ Mul
+ { mulLeft = ScalarMul 4 (Var $ OutWire 2),
+ mulRight = Add (ScalarMul 4 (Var $ OutWire 2)) (Var $ OutWire 3),
+ mulOutput = OutWire 4
+ },
+ Mul
+ { mulLeft = Var $ OutWire 3,
+ mulRight = Add (ScalarMul 4 (Var $ OutWire 2)) (Var $ OutWire 3),
+ mulOutput = OutWire 5
+ }
+ ]
+
+exampleMultiAssignmentInitial :: [f] -> Assignment f
+exampleMultiAssignmentInitial vs = Assignment
+ { assignmentLeft = Map.empty,
+ assignmentRight = Map.empty,
+ assignmentOut = Map.empty,
+ assignmentIn = Map.fromList (zip [0 ..] vs)
+ }
+
+--------------------------------------------------------
+-- Bulletproofs arithmetic circuits conversion utils
+--------------------------------------------------------
+
+altToBulletproofsAssignment :: Num f => Int -> Assignment f -> Bulletproofs.Assignment f
+altToBulletproofsAssignment n Assignment {..} =
+ Bulletproofs.Assignment aL aR aO
+ where
+ aL = (\i -> fromMaybe 0 (Map.lookup i assignmentLeft)) <$> [0 .. n - 1]
+ aR = (\i -> fromMaybe 0 (Map.lookup i assignmentRight)) <$> [0 .. n - 1]
+ aO = (\i -> fromMaybe 0 (Map.lookup i assignmentOut)) <$> [0 .. n - 1]
+
+altToBulletproofsCircuit :: forall f. Num f => AltArithCircuit f -> Bulletproofs.ArithCircuit f
+altToBulletproofsCircuit (circuitToConstraints -> constraints) =
+ Bulletproofs.ArithCircuit
+ { weights = Bulletproofs.GateWeights wL wR wO,
+ commitmentWeights = wV,
+ cs = cs
+ }
+ where
+ wL = foldl' (buildMatrix lcWeightsLeft (numberOfGates - 1)) [] constraints
+ wR = foldl' (buildMatrix lcWeightsRight (numberOfGates - 1)) [] constraints
+ wO = foldl' (buildMatrix lcWeightsOut (numberOfGates - 1)) [] constraints
+ wV = foldl' (buildMatrix lcWeightsIn (m - 1)) [] constraints
+ cs = foldl' (buildVector lcConstant) [] constraints
+ numberOfGates = length constraints
+ m = foldl' countWeigths 0 constraints
+ buildVector :: (LinearConstraint f -> f) -> [f] -> GateConstraint AltWire f -> [f]
+ buildVector f acc c = lConstraints : rConstraints : acc
+ where
+ lConstraints = f $ gcLinearConstraintLeft c
+ rConstraints = f $ gcLinearConstraintRight c
+ buildMatrix :: (LinearConstraint f -> Map Int f) -> Int -> [[f]] -> GateConstraint AltWire f -> [[f]]
+ buildMatrix f n acc c = lConstraintsList : rConstraintsList : acc
+ where
+ lConstraints = f $ gcLinearConstraintLeft c
+ lConstraintsList = (\i -> fromMaybe 0 (Map.lookup i lConstraints)) <$> [0 .. n]
+ rConstraints = f $ gcLinearConstraintRight c
+ rConstraintsList = (\i -> fromMaybe 0 (Map.lookup i rConstraints)) <$> [0 .. n]
+
+countWeigths :: Int -> GateConstraint AltWire f -> Int
+countWeigths acc c =
+ acc
+ + Map.size (lcWeightsIn $ gcLinearConstraintLeft c)
+ + Map.size (lcWeightsIn $ gcLinearConstraintRight c)
+
+calculateMatrixSizes :: (Num f) => AltArithCircuit f -> (Int, Int)
+calculateMatrixSizes altCircuit = (m, n)
+ where
+ constraints = circuitToConstraints altCircuit
+ n = fromIntegral $ length constraints
+ m = foldl' countWeigths 0 constraints
+
+data SetupProof f p
+ = SetupProof
+ { assignment :: Bulletproofs.Assignment f,
+ pedersens :: Pedersens f p,
+ circuit :: Bulletproofs.ArithCircuit f,
+ witness :: Bulletproofs.ArithWitness f p,
+ n :: Int,
+ m :: Int
+ }
+ deriving (Show, Generic, NFData)
+
+data Pedersens f p
+ = Pedersens
+ { vs :: [f],
+ vBlindings :: [f],
+ vCommitments :: [p]
+ }
+ deriving (Show, Generic, NFData)
+
+computePedersens :: (MonadRandom m) => Int -> Int -> m (Pedersens Fr PA)
+computePedersens n m = do
+ vs <- replicateM m (fromInteger <$> getRandomR (0, 2 ^ n - 1))
+ vBlindings <- replicateM m (fromInteger <$> getRandomR (0, 2 ^ n - 1))
+ let vCommitments = zipWith commit vs vBlindings
+ pure Pedersens
+ { vs = vs,
+ vBlindings = vBlindings,
+ vCommitments = vCommitments
+ }
+
+computeBulletproofsAssignment :: AltArithCircuit Fr -> [Fr] -> Int -> Bulletproofs.Assignment Fr
+computeBulletproofsAssignment altCircuit vs n =
+ altToBulletproofsAssignment (fromIntegral n) altAssignment
+ where
+ altAssignment = evalCircuit altCircuit (exampleMultiAssignmentInitial vs)
+
+setupProof :: (MonadRandom m) => AltArithCircuit Fr -> m (SetupProof Fr PA)
+setupProof (transformInputs -> altCircuit) = do
+ let (m, n) = calculateMatrixSizes altCircuit
+ bulletproofsCircuit = altToBulletproofsCircuit altCircuit
+ pedersens@Pedersens {..} <- computePedersens n m
+ let assignment = computeBulletproofsAssignment altCircuit vs n
+ let arithWitness = Bulletproofs.ArithWitness assignment vCommitments vBlindings
+ pure SetupProof
+ { assignment = assignment,
+ pedersens = pedersens,
+ circuit = bulletproofsCircuit,
+ witness = arithWitness,
+ n = n,
+ m = m
+ }
diff --git a/src/Circuit/Dot.hs b/src/Circuit/Dot.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Dot.hs
@@ -0,0 +1,79 @@
+-- | Visualise circuits using Graphviz
+module Circuit.Dot
+ ( arithCircuitToDot
+ , dotWriteSVG
+ ) where
+
+import Protolude
+
+import qualified Data.Text as Text
+import System.FilePath (replaceExtension)
+import System.Process.Text (readProcessWithExitCode)
+import Text.PrettyPrint.Leijen.Text (Pretty(..))
+
+import Circuit.Affine ()
+import Circuit.Arithmetic (ArithCircuit(..), Gate(..), Wire(..), fetchVars)
+
+arithCircuitToDot
+ :: (Show f) => ArithCircuit f -> Text
+arithCircuitToDot (ArithCircuit gates)
+ = Text.unlines . wrapInDigraph . concatMap graphGate $ gates
+ where
+ wrapInDigraph x = ["digraph g {"] ++ x ++ ["}"]
+
+ dotWire :: Wire -> Text
+ dotWire = show . pretty
+
+ dotArrow :: Text -> Text -> Text
+ dotArrow s t = s <> " -> " <> t
+
+ dotArrowLabel :: Text -> Text -> Text -> Text
+ dotArrowLabel s t lbl = dotArrow s t <> " [label=\"" <> lbl <> "\"]"
+
+ labelNode lblId lbl = lblId <> " [label=\"" <> lbl <> "\"]"
+
+ pointNode lblId = lblId <> " [shape=point]"
+
+ graphGate :: Show f => Gate Wire f -> [Text]
+ graphGate (Mul lhs rhs output)
+ = [ labelNode gateLabel "*"
+ , labelNode lhsLabel (show $ pretty lhs)
+ , dotArrow lhsLabel gateLabel
+ , labelNode rhsLabel (show $ pretty rhs)
+ , dotArrow rhsLabel gateLabel
+ ] ++ inputs lhs lhsLabel
+ ++ inputs rhs rhsLabel
+ where
+ lhsLabel = dotWire output <> "lhs"
+ rhsLabel = dotWire output <> "rhs"
+ gateLabel = dotWire output
+ inputs circuit tgt
+ = map ((\src -> dotArrowLabel src tgt (show $ pretty src))
+ . dotWire)
+ $ fetchVars circuit
+ graphGate (Equal i m output)
+ = [ labelNode gateLabel "= 0 ? 0 : 1"
+ , dotArrowLabel (dotWire i) gateLabel (dotWire i)
+ , dotArrowLabel (dotWire m) gateLabel (dotWire m)
+ ]
+ where
+ gateLabel = dotWire output
+ graphGate (Split i outputs)
+ = [ labelNode gateLabel "split"
+ , dotArrowLabel (dotWire i) gateLabel (dotWire i)
+ ] ++ map (pointNode . dotWire) outputs
+ ++ map (\output -> dotArrow gateLabel (dotWire output)) outputs
+ where
+ gateLabel = Text.concat . fmap dotWire $ outputs
+
+
+callDot :: Text -> IO Text
+callDot g = do
+ (_, out, err) <- readProcessWithExitCode "dot" ["-Tsvg"] g
+ if err == "" then pure out else panic err
+
+
+dotWriteSVG :: FilePath -> Text -> IO ()
+dotWriteSVG path = callDot >=> writeFile (replaceExtension path ".svg")
+
+
diff --git a/src/Circuit/Expr.hs b/src/Circuit/Expr.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Expr.hs
@@ -0,0 +1,332 @@
+{-# LANGUAGE StandaloneDeriving #-}
+
+module Circuit.Expr
+ ( UnOp (..),
+ BinOp (..),
+ Expr (..),
+ ExprM,
+ compile,
+ emit,
+ imm,
+ addVar,
+ addWire,
+ freshInput,
+ freshOutput,
+ rotateList,
+ runCircuitBuilder,
+ evalCircuitBuilder,
+ execCircuitBuilder,
+ exprToArithCircuit,
+ evalExpr,
+ truncRotate,
+ )
+where
+
+import Circuit.Affine
+import Circuit.Arithmetic
+import Protolude
+import Text.PrettyPrint.Leijen.Text hiding ((<$>))
+
+data UnOp f a where
+ UNeg :: UnOp f f
+ UNot :: UnOp f Bool
+ -- | # truncate bits, # rotate bits
+ URot :: Int -> Int -> UnOp f f
+
+data BinOp f a where
+ BAdd :: BinOp f f
+ BSub :: BinOp f f
+ BMul :: BinOp f f
+ BAnd :: BinOp f Bool
+ BOr :: BinOp f Bool
+ BXor :: BinOp f Bool
+
+opPrecedence :: BinOp f a -> Int
+opPrecedence BOr = 5
+opPrecedence BXor = 5
+opPrecedence BAnd = 5
+opPrecedence BSub = 6
+opPrecedence BAdd = 6
+opPrecedence BMul = 7
+
+-- | Expression data type of (arithmetic) expressions over a field @f@
+-- with variable names/indices coming from @i@.
+data Expr i f ty where
+ EConst :: f -> Expr i f f
+ EConstBool :: Bool -> Expr i f Bool
+ EVar :: i -> Expr i f f
+ EVarBool :: i -> Expr i f Bool
+ EUnOp :: UnOp f ty -> Expr i f ty -> Expr i f ty
+ EBinOp :: BinOp f ty -> Expr i f ty -> Expr i f ty -> Expr i f ty
+ EIf :: Expr i f Bool -> Expr i f ty -> Expr i f ty -> Expr i f ty
+ EEq :: Expr i f f -> Expr i f f -> Expr i f Bool
+
+deriving instance (Show i, Show f) => Show (Expr i f ty)
+
+deriving instance (Show f) => Show (BinOp f a)
+
+deriving instance (Show f) => Show (UnOp f a)
+
+instance Pretty (BinOp f a) where
+ pretty op = case op of
+ BAdd -> text "+"
+ BSub -> text "-"
+ BMul -> text "*"
+ BAnd -> text "&&"
+ BOr -> text "||"
+ BXor -> text "xor"
+
+instance Pretty (UnOp f a) where
+ pretty op = case op of
+ UNeg -> text "neg"
+ UNot -> text "!"
+ URot truncBits rotBits -> text "rot(" <> pretty truncBits <> text "," <> pretty rotBits <> ")"
+
+instance (Pretty f, Pretty i, Pretty ty) => Pretty (Expr i f ty) where
+ pretty = prettyPrec 0
+ where
+ prettyPrec :: (Pretty f, Pretty i, Pretty ty) => Int -> Expr i f ty -> Doc
+ prettyPrec p e =
+ case e of
+ EVar v ->
+ pretty v
+ EVarBool v ->
+ pretty v
+ EConst l ->
+ pretty l
+ EConstBool b ->
+ pretty b
+ -- TODO correct precedence
+ EUnOp op e1 -> parens (pretty op <+> pretty e1)
+ EBinOp op e1 e2 ->
+ parensPrec (opPrecedence op) p $
+ prettyPrec (opPrecedence op) e1
+ <+> pretty op
+ <+> prettyPrec (opPrecedence op) e2
+ EIf b true false ->
+ parensPrec 4 p (text "if" <+> pretty b <+> text "then" <+> pretty true <+> text "else" <+> pretty false)
+ -- TODO correct precedence
+ EEq l r ->
+ parensPrec 1 p (pretty l) <+> text "=" <+> parensPrec 1 p (pretty r)
+
+parensPrec :: Int -> Int -> Doc -> Doc
+parensPrec opPrec p = if p > opPrec then parens else identity
+
+-------------------------------------------------------------------------------
+-- Evaluator
+-------------------------------------------------------------------------------
+
+-- | Truncate a number to the given number of bits and perform a right
+-- rotation (assuming small-endianness) within the truncation.
+truncRotate ::
+ (Bits f) =>
+ -- | number of bits to truncate to
+ Int ->
+ -- | number of bits to rotate by
+ Int ->
+ f ->
+ f
+truncRotate nbits nrots x =
+ foldr
+ ( \ix rest ->
+ if testBit x ix
+ then setBit rest ((ix + nrots) `mod` nbits)
+ else rest
+ )
+ zeroBits
+ [0 .. nbits - 1]
+
+-- | Evaluate arithmetic expressions directly, given an environment
+evalExpr ::
+ (Bits f, Num f) =>
+ -- | variable lookup
+ (i -> vars -> Maybe f) ->
+ -- | expression to evaluate
+ Expr i f ty ->
+ -- | input values
+ vars ->
+ -- | resulting value
+ ty
+evalExpr lookupVar expr vars = case expr of
+ EConst f -> f
+ EConstBool b -> b
+ EVar i -> case lookupVar i vars of
+ Just v -> v
+ Nothing -> panic "TODO: incorrect var lookup"
+ EVarBool i -> case lookupVar i vars of
+ Just v -> v == 1
+ Nothing -> panic "TODO: incorrect var lookup"
+ EUnOp UNeg e1 ->
+ negate $ evalExpr lookupVar e1 vars
+ EUnOp UNot e1 ->
+ not $ evalExpr lookupVar e1 vars
+ EUnOp (URot truncBits rotBits) e1 ->
+ truncRotate truncBits rotBits $ evalExpr lookupVar e1 vars
+ EBinOp op e1 e2 ->
+ (evalExpr lookupVar e1 vars) `apply` (evalExpr lookupVar e2 vars)
+ where
+ apply = case op of
+ BAdd -> (+)
+ BSub -> (-)
+ BMul -> (*)
+ BAnd -> (&&)
+ BOr -> (||)
+ BXor -> \x y -> (x || y) && not (x && y)
+ EIf b true false ->
+ if evalExpr lookupVar b vars
+ then evalExpr lookupVar true vars
+ else evalExpr lookupVar false vars
+ EEq lhs rhs -> evalExpr lookupVar lhs vars == evalExpr lookupVar rhs vars
+
+-------------------------------------------------------------------------------
+-- Circuit Builder
+-------------------------------------------------------------------------------
+
+type ExprM f a = State (ArithCircuit f, Int) a
+
+execCircuitBuilder :: ExprM f a -> ArithCircuit f
+execCircuitBuilder m = reverseCircuit $ fst $ execState m (ArithCircuit [], 0)
+ where
+ reverseCircuit = \(ArithCircuit cs) -> ArithCircuit $ reverse cs
+
+evalCircuitBuilder :: ExprM f a -> a
+evalCircuitBuilder = fst . runCircuitBuilder
+
+runCircuitBuilder :: ExprM f a -> (a, ArithCircuit f)
+runCircuitBuilder m = second (reverseCircuit . fst) $ runState m (ArithCircuit [], 0)
+ where
+ reverseCircuit = \(ArithCircuit cs) -> ArithCircuit $ reverse cs
+
+fresh :: ExprM f Int
+fresh = do
+ v <- gets snd
+ modify (second (+ 1))
+ pure v
+
+-- | Fresh intermediate variables
+imm :: ExprM f Wire
+imm = IntermediateWire <$> fresh
+
+-- | Fresh input variables
+freshInput :: ExprM f Wire
+freshInput = InputWire <$> fresh
+
+-- | Fresh output variables
+freshOutput :: ExprM f Wire
+freshOutput = OutputWire <$> fresh
+
+-- | Multiply two wires or affine circuits to an intermediate variable
+mulToImm :: Either Wire (AffineCircuit Wire f) -> Either Wire (AffineCircuit Wire f) -> ExprM f Wire
+mulToImm l r = do
+ o <- imm
+ emit $ Mul (addVar l) (addVar r) o
+ pure o
+
+-- | Add a Mul and its output to the ArithCircuit
+emit :: Gate Wire f -> ExprM f ()
+emit c = modify $ first (\(ArithCircuit cs) -> ArithCircuit (c : cs))
+
+-- | Rotate a list to the right
+rotateList :: Int -> [a] -> [a]
+rotateList steps x = take (length x) $ drop steps $ cycle x
+
+-- | Turn a wire into an affine circuit, or leave it be
+addVar :: Either Wire (AffineCircuit Wire f) -> AffineCircuit Wire f
+addVar (Left w) = Var w
+addVar (Right c) = c
+
+-- | Turn an affine circuit into a wire, or leave it be
+addWire :: Num f => Either Wire (AffineCircuit Wire f) -> ExprM f Wire
+addWire (Left w) = pure w
+addWire (Right c) = do
+ mulOut <- imm
+ emit $ Mul (ConstGate 1) c mulOut
+ pure mulOut
+
+compile :: Num f => Expr Wire f ty -> ExprM f (Either Wire (AffineCircuit Wire f))
+compile expr = case expr of
+ EConst n -> pure . Right $ ConstGate n
+ EConstBool b -> pure . Right $ ConstGate (if b then 1 else 0)
+ EVar v -> pure . Left $ v
+ EVarBool v -> pure . Left $ v
+ EUnOp op e1 -> do
+ e1Out <- compile e1
+ case op of
+ UNeg -> pure . Right $ ScalarMul (-1) (addVar e1Out)
+ UNot -> pure . Right $ Add (ConstGate 1) (ScalarMul (-1) (addVar e1Out))
+ URot truncBits rotBits -> do
+ inp <- addWire e1Out
+ outputs <- replicateM truncBits imm
+ emit $ Split inp outputs
+ pure . Right $ unsplit (rotateList rotBits outputs)
+ EBinOp op e1 e2 -> do
+ e1Out <- addVar <$> compile e1
+ e2Out <- addVar <$> compile e2
+ case op of
+ BAdd -> pure . Right $ Add e1Out e2Out
+ BMul -> do
+ tmp1 <- mulToImm (Right e1Out) (Right e2Out)
+ pure . Left $ tmp1
+ -- SUB(x, y) = x + (-y)
+ BSub -> pure . Right $ Add e1Out (ScalarMul (-1) e2Out)
+ BAnd -> do
+ tmp1 <- mulToImm (Right e1Out) (Right e2Out)
+ pure . Left $ tmp1
+ BOr -> do
+ -- OR(input1, input2) = (input1 + input2) - (input1 * input2)
+ tmp1 <- imm
+ emit $ Mul e1Out e2Out tmp1
+ pure . Right $ Add (Add e1Out e2Out) (ScalarMul (-1) (Var tmp1))
+ BXor -> do
+ -- XOR(input1, input2) = (input1 + input2) - 2 * (input1 * input2)
+ tmp1 <- imm
+ emit $ Mul e1Out e2Out tmp1
+ pure . Right $ Add (Add e1Out e2Out) (ScalarMul (-2) (Var tmp1))
+ -- IF(cond, true, false) = (cond*true) + ((!cond) * false)
+ EIf cond true false -> do
+ condOut <- addVar <$> compile cond
+ trueOut <- addVar <$> compile true
+ falseOut <- addVar <$> compile false
+ tmp1 <- imm
+ tmp2 <- imm
+ emit $ Mul condOut trueOut tmp1
+ emit $ Mul (Add (ConstGate 1) (ScalarMul (-1) condOut)) falseOut tmp2
+ pure . Right $ Add (Var tmp1) (Var tmp2)
+ -- EQ(lhs, rhs) = (lhs - rhs == 1)
+ EEq lhs rhs -> do
+ lhsSubRhs <- compile (EBinOp BSub lhs rhs)
+ eqInWire <- addWire lhsSubRhs
+ eqFreeWire <- imm
+ eqOutWire <- imm
+ emit $ Equal eqInWire eqFreeWire eqOutWire
+ -- eqOutWire == 0 if lhs == rhs, so we need to return 1 -
+ -- neqOutWire instead.
+ pure . Right $ Add (ConstGate 1) (ScalarMul (-1) (Var eqOutWire))
+
+-- | Translate an arithmetic expression to an arithmetic circuit
+exprToArithCircuit ::
+ Num f =>
+ -- | expression to compile
+ Expr Int f ty ->
+ -- | Wire to assign the output of the expression to
+ Wire ->
+ ExprM f ()
+exprToArithCircuit expr output =
+ exprToArithCircuit' (mapVarsExpr InputWire expr) output
+
+exprToArithCircuit' :: Num f => Expr Wire f ty -> Wire -> ExprM f ()
+exprToArithCircuit' expr output = do
+ exprOut <- compile expr
+ emit $ Mul (ConstGate 1) (addVar exprOut) output
+
+-- | Apply function to variable names.
+mapVarsExpr :: (i -> j) -> Expr i f ty -> Expr j f ty
+mapVarsExpr f expr = case expr of
+ EVar i -> EVar $ f i
+ EVarBool i -> EVarBool $ f i
+ EConst v -> EConst v
+ EConstBool b -> EConstBool b
+ EBinOp op e1 e2 -> EBinOp op (mapVarsExpr f e1) (mapVarsExpr f e2)
+ EUnOp op e1 -> EUnOp op (mapVarsExpr f e1)
+ EIf b tr fl -> EIf (mapVarsExpr f b) (mapVarsExpr f tr) (mapVarsExpr f fl)
+ EEq lhs rhs -> EEq (mapVarsExpr f lhs) (mapVarsExpr f rhs)
diff --git a/src/Circuit/Lang.hs b/src/Circuit/Lang.hs
new file mode 100644
--- /dev/null
+++ b/src/Circuit/Lang.hs
@@ -0,0 +1,78 @@
+-- | Surface language
+module Circuit.Lang
+ ( c
+ , add
+ , sub
+ , mul
+ , and_
+ , or_
+ , xor_
+ , not_
+ , eq
+ , deref
+ , e
+ , cond
+ , ret
+ , input
+ ) where
+
+import Protolude
+
+import Circuit.Affine (AffineCircuit(..))
+import Circuit.Arithmetic (Gate(..), Wire(..))
+import Circuit.Expr
+
+-- | Convert constant to expression
+c :: f -> Expr Wire f f
+c = EConst
+
+-- | Binary arithmetic operations on expressions
+add, sub, mul :: Expr Wire f f -> Expr Wire f f -> Expr Wire f f
+add = EBinOp BAdd
+sub = EBinOp BSub
+mul = EBinOp BMul
+
+-- | Binary logic operations on expressions
+-- Have to use underscore or similar to avoid shadowing @and@ and @or@
+-- from Prelude/Protolude.
+and_, or_, xor_ :: Expr Wire f Bool -> Expr Wire f Bool -> Expr Wire f Bool
+and_ = EBinOp BAnd
+or_ = EBinOp BOr
+xor_ = EBinOp BXor
+
+-- | Negate expression
+not_ :: Expr Wire f Bool -> Expr Wire f Bool
+not_ = EUnOp UNot
+
+-- | Compare two expressions
+eq :: Expr Wire f f -> Expr Wire f f -> Expr Wire f Bool
+eq = EEq
+
+-- | Convert wire to expression
+deref :: Wire -> Expr Wire f f
+deref = EVar
+
+-- | Return compilation of expression into an intermediate wire
+e :: Num f => Expr Wire f f -> ExprM f Wire
+e = compileWithWire imm
+
+-- | Conditional statement on expressions
+cond :: Expr Wire f Bool -> Expr Wire f ty -> Expr Wire f ty -> Expr Wire f ty
+cond = EIf
+
+-- | Return compilation of expression into an output wire
+ret :: Num f => Expr Wire f f -> ExprM f Wire
+ret = compileWithWire freshOutput
+
+compileWithWire :: Num f => ExprM f Wire -> Expr Wire f f -> ExprM f Wire
+compileWithWire freshWire expr = do
+ compileOut <- compile expr
+ case compileOut of
+ Left wire -> pure wire
+ Right circ -> do
+ wire <- freshWire
+ emit $ Mul (ConstGate 1) circ wire
+ pure wire
+
+input :: ExprM f Wire
+input = freshInput
diff --git a/src/Fresh.hs b/src/Fresh.hs
new file mode 100644
--- /dev/null
+++ b/src/Fresh.hs
@@ -0,0 +1,20 @@
+module Fresh
+ ( fresh
+ , evalFresh
+ , Fresh
+ , FreshT
+ ) where
+
+import Protolude
+
+type FreshT m a = StateT Int m a
+type Fresh a = FreshT Identity a
+
+evalFresh :: Fresh a -> a
+evalFresh act = runIdentity $ evalStateT act 0
+
+fresh :: Fresh Int
+fresh = do
+ v <- get
+ modify (+ 1)
+ pure v
diff --git a/src/QAP.hs b/src/QAP.hs
new file mode 100644
--- /dev/null
+++ b/src/QAP.hs
@@ -0,0 +1,618 @@
+{-# OPTIONS -fno-warn-orphans #-}
+
+{-# LANGUAGE DeriveAnyClass, DeriveFoldable, DeriveFunctor, DeriveGeneric,
+ FlexibleInstances, ParallelListComp, RecordWildCards,
+ ScopedTypeVariables, TupleSections #-}
+
+-- | Definitions of quadratic arithmetic programs, along with their
+-- assignment verification functions and the translations from single
+-- multiplication- or equality-gates into QAPs and arithmetic circuits
+-- into QAPs.
+module QAP
+ ( QapSet(..)
+ , QAP(..)
+ , updateAtWire
+ , lookupAtWire
+ , cnstInpQapSet
+ , sumQapSet
+ , sumQapSetCnstInp
+ , sumQapSetMidOut
+ , foldQapSet
+ , combineWithDefaults
+ , combineInputsWithDefaults
+ , combineNonInputsWithDefaults
+ , verifyAssignment
+ , verificationWitness
+ , verificationWitnessZk
+ , gateToQAP
+ , gateToGenQAP
+ , qapSetToMap
+ , initialQapSet
+ , generateAssignmentGate
+ , generateAssignment
+ , addMissingZeroes
+ , arithCircuitToGenQAP
+ , arithCircuitToQAP
+ , arithCircuitToQAPFFT
+ , createPolynomials
+ , createPolynomialsFFT
+ ) where
+
+import Protolude hiding (quot, quotRem)
+
+import Data.Aeson (FromJSON, ToJSON)
+import Data.Aeson.Types
+import Data.Foldable (foldr1)
+import Data.Map (Map, fromList, mapKeys)
+import qualified Data.Map as Map
+import qualified Data.Map.Merge.Lazy as Merge
+
+import Data.Euclidean (Euclidean(..))
+import Data.Field (Field)
+import Data.Field.Galois (GaloisField, Prime, pow)
+import Data.Poly
+import qualified Data.Vector as V
+import Text.PrettyPrint.Leijen.Text (Pretty(..), enclose, indent,
+ lbracket, rbracket, text, vcat,
+ (<+>))
+
+import Circuit.Affine (affineCircuitToAffineMap)
+import Circuit.Arithmetic (ArithCircuit(..), Gate(..), Wire(..),
+ evalArithCircuit, evalGate)
+import qualified FFT
+
+-- | The sets of polynomials/constants as they occur in QAPs, grouped
+-- into their constant, input, output and intermediate parts.
+data QapSet f = QapSet
+ { qapSetConstant :: f
+ , qapSetInput :: Map Int f
+ , qapSetIntermediate :: Map Int f
+ , qapSetOutput :: Map Int f
+ } deriving (Show, Eq, Functor, Foldable, Generic, NFData, ToJSON, FromJSON)
+
+-- | Quadratic arithmetic program
+data QAP f = QAP
+ { qapInputsLeft :: QapSet (VPoly f)
+ , qapInputsRight :: QapSet (VPoly f)
+ , qapOutputs :: QapSet (VPoly f)
+ , qapTarget :: VPoly f
+ } deriving (Show, Eq, Generic, NFData, ToJSON, FromJSON)
+
+-- Orphan instances for VPoly
+instance (ToJSON f, Generic f) => ToJSON (VPoly f) where
+ toJSON = toJSON . unPoly
+instance (FromJSON f, Generic f, Eq f, Num f) => FromJSON (VPoly f) where
+ parseJSON v = toPoly <$> parseJSON v
+
+instance ToJSON (Prime n)
+instance FromJSON (Prime n)
+
+-- | Generalised quadratic arithmetic program: instead of @Poly@, allow
+-- any functor.
+data GenQAP p f = GenQAP
+ { genQapInputsLeft :: QapSet (p f)
+ , genQapInputsRight :: QapSet (p f)
+ , genQapOutputs :: QapSet (p f)
+ , genQapTarget :: p f
+ } deriving (Show, Eq, Generic, NFData, ToJSON, FromJSON)
+
+-- Note that we could get "sequence" from the Traversable instance of
+-- lists if we had an Applicative/Monad instance of QapSet. There do
+-- not seem to be sensible instances of those classes for QapSet.
+sequenceQapSet :: [QapSet f] -> QapSet [f]
+sequenceQapSet qapSets = QapSet constants inputs mids outputs
+ where
+ constants = map qapSetConstant qapSets
+ inputs = Map.unionsWith (<>) . fmap (fmap pure) $ map qapSetInput qapSets
+ mids = Map.unionsWith (<>) . fmap (fmap pure) $ map qapSetIntermediate qapSets
+ outputs = Map.unionsWith (<>) . fmap (fmap pure) $ map qapSetOutput qapSets
+
+-- | Create QapSet with only a constant value and empty maps for the
+-- rest.
+constantQapSet :: g -> QapSet g
+constantQapSet g = QapSet
+ { qapSetConstant = g
+ , qapSetInput = Map.empty
+ , qapSetIntermediate = Map.empty
+ , qapSetOutput = Map.empty
+ }
+
+cnstInpQapSet :: g -> Map Int g -> QapSet g
+cnstInpQapSet g inp = QapSet
+ { qapSetConstant = g
+ , qapSetInput = inp
+ , qapSetIntermediate = Map.empty
+ , qapSetOutput = Map.empty
+ }
+-- | Sum all the values contained in a QapSet.
+sumQapSet :: Monoid g => QapSet g -> g
+sumQapSet = fold
+
+-- | Sum only over constant and input values
+sumQapSetCnstInp :: Monoid g => QapSet g -> g
+sumQapSetCnstInp (QapSet cnst inp _ _)
+ = cnst <> fold inp
+
+-- | Sum only over intermediate and output values
+sumQapSetMidOut :: Monoid g => QapSet g -> g
+sumQapSetMidOut (QapSet _ _ mid out)
+ = fold mid <> fold out
+
+instance Pretty (Ratio Integer) where
+ pretty = text . show
+
+instance Pretty f => Pretty (QapSet f) where
+ pretty (QapSet constant inps mids outps)
+ = vcat
+ [ text "constant:" <+> pretty constant
+ , text "inputs:"
+ , indent 2 $ ppMap inps
+ , text "outputs:"
+ , indent 2 $ ppMap outps
+ , text "intermediates:"
+ , indent 2 $ ppMap mids
+ ]
+ where
+ ppMap
+ = vcat
+ . map (\(ix, x) -> enclose lbracket rbracket (pretty ix) <+> pretty x)
+ . Map.toList
+
+combineWithDefaults
+ :: (a -> b -> c) -- ^ function to combine the values with
+ -> a -- ^ default left value
+ -> b -- ^ default right value
+ -> QapSet a -- ^ left QapSet
+ -> QapSet b -- ^ right QapSet
+ -> QapSet c
+combineWithDefaults f defaultA defaultB (QapSet cA inpA midA outpA) (QapSet cB inpB midB outpB)
+ = QapSet
+ { qapSetConstant = f cA cB
+ , qapSetInput = combineMaps inpA inpB
+ , qapSetIntermediate = combineMaps midA midB
+ , qapSetOutput = combineMaps outpA outpB
+ }
+ where
+ combineMaps = Merge.merge missingRight missingLeft matching
+ missingLeft = Merge.mapMissing $ const $ f defaultA
+ missingRight = Merge.mapMissing $ const $ flip f defaultB
+ matching = Merge.zipWithMatched $ const f
+
+combineInputsWithDefaults
+ :: (a -> b -> c) -- ^ function to combine the values with
+ -> a -- ^ default left value
+ -> b -- ^ default right value
+ -> QapSet a -- ^ left QapSet
+ -> QapSet b -- ^ right QapSet
+ -> QapSet c
+combineInputsWithDefaults f defaultA defaultB (QapSet cA inpA _ _) (QapSet cB inpB _ _)
+ = QapSet
+ { qapSetConstant = f cA cB
+ , qapSetInput = combineMaps inpA inpB
+ , qapSetIntermediate = mempty
+ , qapSetOutput = mempty
+ }
+ where
+ combineMaps = Merge.merge missingRight missingLeft matching
+ missingLeft = Merge.mapMissing $ const $ f defaultA
+ missingRight = Merge.mapMissing $ const $ flip f defaultB
+ matching = Merge.zipWithMatched $ const f
+
+combineNonInputsWithDefaults
+ :: (a -> b -> c) -- ^ function to combine the values with
+ -> a -- ^ default left value
+ -> b -- ^ default right value
+ -> c -- ^ default constant
+ -> QapSet a -- ^ left QapSet
+ -> QapSet b -- ^ right QapSet
+ -> QapSet c
+combineNonInputsWithDefaults f defaultA defaultB defaultC (QapSet _ _ midA outpA) (QapSet _ _ midB outpB)
+ = QapSet
+ { qapSetConstant = defaultC
+ , qapSetInput = mempty
+ , qapSetIntermediate = combineMaps midA midB
+ , qapSetOutput = combineMaps outpA outpB
+ }
+ where
+ combineMaps = Merge.merge missingRight missingLeft matching
+ missingLeft = Merge.mapMissing $ const $ f defaultA
+ missingRight = Merge.mapMissing $ const $ flip f defaultB
+ matching = Merge.zipWithMatched $ const f
+
+-- | Fold over a QapSet with an operation that is assumed to be
+-- commutative.
+foldQapSet
+ :: (a -> a -> a) -- ^ *commutative* binary operation
+ -> QapSet a -- ^ QapSet to fold over
+ -> a
+foldQapSet = foldr1
+
+-- Alternative to @sequenceGenQap@
+createMapGenQap :: Ord k => [GenQAP ((,) k) k] -> GenQAP (Map k) k
+createMapGenQap genQaps = GenQAP inpLefts inpRights outputs targets
+ where
+ inpLefts = fmap Map.fromList . sequenceQapSet . map genQapInputsLeft $ genQaps
+ inpRights = fmap Map.fromList . sequenceQapSet . map genQapInputsRight $ genQaps
+ outputs = fmap Map.fromList . sequenceQapSet . map genQapOutputs $ genQaps
+ targets = Map.fromList . map genQapTarget $ genQaps
+
+instance (Eq f, Num f, Pretty f, Show f) => Pretty (QAP f) where
+ pretty (QAP inpsLeft inpsRight outps target)
+ = vcat
+ [ text "QAP:"
+ , text "inputs left:"
+ , indent 2 . text . show $ inpsLeft
+ , text "inputs right:"
+ , indent 2 . text . show $ inpsRight
+ , text "outputs:"
+ , indent 2 . text . show $ outps
+ , text "target: " <> text (show target)
+ ]
+
+instance (Pretty f, Pretty (p f)) => Pretty (GenQAP p f) where
+ pretty (GenQAP inpsLeft inpsRight outps target)
+ = vcat
+ [ text "QAP:"
+ , text "inputs left:"
+ , indent 2 $ pretty inpsLeft
+ , text "inputs right:"
+ , indent 2 $ pretty inpsRight
+ , text "outputs:"
+ , indent 2 $ pretty outps
+ , text "target: " <> pretty target
+ ]
+
+instance Functor p => Functor (GenQAP p) where
+ fmap f (GenQAP inpLeft inpRight outp target)
+ = GenQAP (fmap (fmap f) inpLeft)
+ (fmap (fmap f) inpRight)
+ (fmap (fmap f) outp)
+ (fmap f target)
+
+-- | Verify whether an assignment of variables is consistent with the
+-- given QAP
+verifyAssignment
+ :: (Eq f, Field f, Num f)
+ => QAP f -- ^ circuit whose evaluation we want to verify
+ -> QapSet f -- ^ vector containing the inputs, outputs and
+ -- intermediate values (outputs of all the mul-gates)
+ -> Bool
+verifyAssignment qap assignment = isJust $ verificationWitness qap assignment
+
+-- | Produce the polynomial witnessing the validity of given
+-- assignment against the given QAP. Will return @Nothing@ if the
+-- assignment is not valid.
+--
+-- In Pinocchio's terminology: this produces the h(x) such that p(x) =
+-- h(x) * t(x) where t(x) is the target polynomial and p(x) is the
+-- left input polynomials times the right input polynomials minus the
+-- output polynomials.
+verificationWitness
+ :: forall f . (Eq f, Field f, Num f)
+ => QAP f -- ^ circuit whose evaluation we want to verify
+ -> QapSet f -- ^ vector containing the inputs, outputs and
+ -- intermediate values (outputs of all the mul-gates)
+ -> Maybe (VPoly f)
+verificationWitness = verificationWitnessZk 0 0 0
+
+verificationWitnessZk
+ :: (Eq f, Field f, Num f)
+ => f
+ -> f
+ -> f
+ -> QAP f -- ^ circuit whose evaluation we want to verify
+ -> QapSet f -- ^ vector containing the inputs, outputs and
+ -- intermediate values (outputs of all the mul-gates)
+ -> Maybe (VPoly f)
+verificationWitnessZk delta1 delta2 delta3 QAP {..} assignment
+ = if remainder == 0
+ then Just quotient
+ else Nothing
+ where
+ scaleWithAssignment x = combineWithDefaults (\a b -> monomial 0 b * a) 0 0 x assignment
+ leftInputPoly
+ = (monomial 0 delta1 * qapTarget)
+ + sumQap (scaleWithAssignment qapInputsLeft)
+ rightInputPoly
+ = (monomial 0 delta2 * qapTarget)
+ + sumQap (scaleWithAssignment qapInputsRight)
+ outputPoly
+ = (monomial 0 delta3 * qapTarget)
+ + sumQap (scaleWithAssignment qapOutputs)
+ sumQap = foldQapSet (+)
+ inputOutputPoly
+ = (leftInputPoly * rightInputPoly) - outputPoly
+ (quotient, remainder) = quotRem inputOutputPoly qapTarget
+
+-- | Lookup the value at the given wire label in the
+-- @QapSet@.
+lookupAtWire :: Wire -> QapSet a -> Maybe a
+lookupAtWire (InputWire ix) QapSet { qapSetInput = inps }
+ = Map.lookup ix inps
+lookupAtWire (IntermediateWire ix) QapSet { qapSetIntermediate = mids }
+ = Map.lookup ix mids
+lookupAtWire (OutputWire ix) QapSet { qapSetOutput = outps }
+ = Map.lookup ix outps
+
+-- | Update the value at the given wire label in the
+-- @QapSet@. (Partial function at the moment.)
+updateAtWire :: Wire -> a -> QapSet a -> QapSet a
+updateAtWire (InputWire ix) a qs@QapSet { qapSetInput = inps }
+ = qs { qapSetInput = Map.insert ix a inps }
+updateAtWire (IntermediateWire ix) a qs@QapSet { qapSetIntermediate = mids }
+ = qs { qapSetIntermediate = Map.insert ix a mids }
+updateAtWire (OutputWire ix) a qs@QapSet { qapSetOutput = outps }
+ = qs { qapSetOutput = Map.insert ix a outps }
+
+-- | Update at multiple wires
+updateAtWires :: [(Wire, a)] -> QapSet a -> QapSet a
+updateAtWires wireVals vars
+ = foldl' (\rest (wire, val) -> updateAtWire wire val rest) vars wireVals
+
+-- | Convert a single multiplication- or equality-gate into a QAP
+gateToQAP
+ :: GaloisField k
+ => (Int -> k)
+ -> [k] -- ^ arbitrarily chosen roots
+ -> Gate Wire k -- ^ circuit to encode as a QAP
+ -> QAP k
+gateToQAP primRoots roots
+ = createPolynomialsFFT primRoots . addMissingZeroes roots . createMapGenQap . gateToGenQAP roots
+
+-- | Convert a single multiplication gate (with affine circuits for
+-- inputs) into a GenQAP
+gateToGenQAP
+ :: (GaloisField k)
+ => [k] -- ^ arbitrarily chosen roots
+ -> Gate Wire k -- ^ circuit to encode as a QAP
+ -> [GenQAP ((,) k) k]
+gateToGenQAP [root] (Mul l r wire)
+ = pure
+ . addOutputVals
+ . addInputVals
+ $ GenQAP
+ { genQapInputsLeft = constantQapSet (root, leftInputConst)
+ , genQapInputsRight = constantQapSet (root, rightInputConst)
+ , genQapOutputs = constantQapSet (root, 0)
+ , genQapTarget = (root, 0)
+ }
+ where
+ (leftInputConst, leftInputVector) = affineCircuitToAffineMap l
+ (rightInputConst, rightInputVector) = affineCircuitToAffineMap r
+
+ addInputVals (GenQAP left right out t)
+ = GenQAP (Map.foldrWithKey updateAtWire left $ fmap (root,) leftInputVector)
+ (Map.foldrWithKey updateAtWire right $ fmap (root,) rightInputVector)
+ out
+ t
+
+ addOutputVals (GenQAP left right out t)
+ = GenQAP left
+ right
+ (updateAtWire wire (root, 1) out)
+ t
+gateToGenQAP [root0,root1] (Equal i m outputWire)
+ = [qap0, qap1]
+ where
+ qap0 = GenQAP
+ { genQapInputsLeft
+ = updateAtWires [ (i, (root0, 1))
+ , (m, (root0, 0))
+ , (outputWire, (root0, 0))
+ ]
+ $ constantQapSet (root0, 0)
+ , genQapInputsRight
+ = updateAtWires [ (i, (root0, 0))
+ , (m, (root0, 1))
+ , (outputWire, (root0, 0))
+ ]
+ $ constantQapSet (root0, 0)
+ , genQapOutputs
+ = updateAtWires [ (i, (root0, 0))
+ , (m, (root0, 0))
+ , (outputWire, (root0, 1))
+ ]
+ $ constantQapSet (root0, 0)
+ , genQapTarget
+ = (root0, 0)
+ }
+ qap1 = GenQAP
+ { genQapInputsLeft
+ = updateAtWires [ (i, (root1, 0))
+ , (m, (root1, 0))
+ , (outputWire, (root1, -1))
+ ]
+ $ constantQapSet (root1, 1)
+ , genQapInputsRight
+ = updateAtWires [ (i, (root1, 1))
+ , (m, (root1, 0))
+ , (outputWire, (root1, 0))
+ ]
+ $ constantQapSet (root1, 0)
+ , genQapOutputs
+ = updateAtWires [ (i, (root1, 0))
+ , (m, (root1, 0))
+ , (outputWire, (root1, 0))
+ ]
+ $ constantQapSet (root1, 0)
+ , genQapTarget
+ = (root1, 0)
+ }
+gateToGenQAP (root:roots) (Split inp outputs)
+ = if length roots /= length outputs
+ then panic "gateToGenQAP: wrong number of roots supplied"
+ else qap0:zipWith qaps roots outputs
+ where
+ qap0 = GenQAP
+ { genQapInputsLeft
+ = updateAtWires ((inp, (root, 0)):zipWith (\output i -> (output, (root, 2 `pow` i))) outputs [0 :: Integer ..])
+ $ constantQapSet (root, 0)
+ , genQapInputsRight
+ = updateAtWires [(inp, (root, 0))]
+ $ constantQapSet (root, 1)
+ , genQapOutputs
+ = updateAtWires [(inp, (root, 1))]
+ $ constantQapSet (root, 0)
+ , genQapTarget
+ = (root, 0)
+ }
+ qaps r outp = GenQAP
+ { genQapInputsLeft
+ = updateAtWire outp (r, 1)
+ $ constantQapSet (r, 0)
+ , genQapInputsRight
+ = updateAtWire outp (r, -1)
+ $ constantQapSet (r, 1)
+ , genQapOutputs
+ = updateAtWire outp (r, 0)
+ $ constantQapSet (r, 0)
+ , genQapTarget
+ = (r, 0)
+ }
+gateToGenQAP _ _ = panic "gateToGenQAP: wrong number of roots supplied"
+
+-- | For the left input/right input/output polynomials: turn list of
+-- coordinates into a polynomial that interpolates the
+-- coordinates. For the target polynomial: define it as the product of
+-- all monics t_g(x) := x - r_g where r_g is the root corresponding to
+-- the gate g.
+
+
+-- | Naive construction of polynomials using Lagrange interpolation
+-- This has terrible complexity at the moment.
+-- Use the FFT-based approach if possible.
+createPolynomials :: forall k. (GaloisField k) => GenQAP (Map k) k -> QAP k
+createPolynomials (GenQAP inpLeft inpRight outp targetRoots)
+ = QAP
+ { qapInputsLeft = fmap (lagrangeInterpolate . Map.toList) inpLeft
+ , qapInputsRight = fmap (lagrangeInterpolate . Map.toList) inpRight
+ , qapOutputs = fmap (lagrangeInterpolate . Map.toList) outp
+ , qapTarget = foldl' (*) (monomial 0 1) . map ((\root -> toPoly $ V.fromList [-root, 1]) . fst) . Map.toList $ targetRoots
+ }
+ where
+ lagrangeInterpolate :: [(k, k)] -> VPoly k
+ lagrangeInterpolate xys = sum
+ [ scale 0 f (roots `quot` root x)
+ | f <- zipWith (/) ys phis
+ | x <- xs
+ ]
+ where
+ xs, ys :: [k]
+ (xs,ys) = foldr (\(a, b) ~(as,bs) -> (a:as,b:bs)) ([],[]) xys
+ phis :: [k]
+ phis = map (eval (deriv roots)) xs
+ roots :: VPoly k
+ roots = foldl' (\acc xi -> acc * root xi) 1 xs -- (X - x_0) * ... * (X - x_{n-1})
+ root xi = toPoly . V.fromList $ [-xi, 1] -- (X - x_i)
+
+-- | Create polynomials using FFT-based polynomial operations instead
+-- of naive.
+createPolynomialsFFT
+ :: GaloisField k
+ => (Int -> k) -- ^ function that gives us the primitive 2^k-th root
+ -- of unity
+ -> GenQAP (Map k) k -- ^ GenQAP containing the coordinates we want
+ -- to interpolate
+ -> QAP k
+createPolynomialsFFT primRoots (GenQAP inpLeft inpRight outp targetRoots)
+ = QAP
+ { qapInputsLeft = fmap (FFT.interpolate primRoots . Map.elems) inpLeft
+ , qapInputsRight = fmap (FFT.interpolate primRoots . Map.elems) inpRight
+ , qapOutputs = fmap (FFT.interpolate primRoots . Map.elems) outp
+ , qapTarget = FFT.fftTargetPoly primRoots (Map.size targetRoots)
+ }
+
+
+-- | Convert an arithmetic circuit into a GenQAP: perform every step
+-- of the QAP translation except the final interpolation step.
+arithCircuitToGenQAP
+ :: GaloisField k
+ => [[k]] -- ^ arbitrarily chosen roots, one for each gate
+ -> ArithCircuit k -- ^ circuit to encode as a QAP
+ -> GenQAP (Map k) k
+arithCircuitToGenQAP rootsPerGate (ArithCircuit gates)
+ = addMissingZeroes (concat rootsPerGate)
+ . createMapGenQap
+ . concat
+ $ zipWith gateToGenQAP rootsPerGate gates
+
+-- | Convert an arithmetic circuit into a QAP
+arithCircuitToQAP
+ :: GaloisField k
+ => [[k]] -- ^ arbitrarily chosen roots, one for each gate
+ -> ArithCircuit k -- ^ circuit to encode as a QAP
+ -> QAP k
+arithCircuitToQAP roots circuit =
+ createPolynomials
+ $ arithCircuitToGenQAP roots circuit
+
+-- | Convert an arithmetic circuit into a QAP
+arithCircuitToQAPFFT
+ :: GaloisField k
+ => (Int -> k) -- ^ function that gives us the primitive 2^k-th root
+ -- of unity
+ -> [[k]] -- ^ arbitrarily chosen roots, one for each gate
+ -> ArithCircuit k -- ^ circuit to encode as a QAP
+ -> QAP k
+arithCircuitToQAPFFT primRoots roots circuit =
+ createPolynomialsFFT primRoots
+ $ arithCircuitToGenQAP roots circuit
+-- | Add zeroes for those roots that are missing, to prevent the
+-- values in the GenQAP to be too sparse. (We can be sparse in wire
+-- values, but not in values at roots, otherwise the interpolation
+-- step is incorrect.)
+addMissingZeroes
+ :: forall f . (Ord f, Num f)
+ => [f] -> GenQAP (Map f) f -> GenQAP (Map f) f
+addMissingZeroes allRoots (GenQAP inpLeft inpRight outp t)
+ = GenQAP (fmap (`Map.union` allZeroes) inpLeft)
+ (fmap (`Map.union` allZeroes) inpRight)
+ (fmap (`Map.union` allZeroes) outp)
+ (t `Map.union` allZeroes)
+ where
+ allZeroes :: Map f f
+ allZeroes = Map.fromList . map (,0) $ allRoots
+
+-- | Generate a valid assignment for a single gate.
+generateAssignmentGate
+ :: (Bits f, Fractional f)
+ => Gate Wire f -- ^ program
+ -> Map Int f -- ^ inputs
+ -> QapSet f
+generateAssignmentGate program inps
+ = evalGate
+ lookupAtWire
+ updateAtWire
+ (initialQapSet inps)
+ program
+
+initialQapSet
+ :: Num f
+ => Map Int f -- ^ inputs
+ -> QapSet f
+initialQapSet inputs = QapSet 1 inputs Map.empty Map.empty
+
+generateAssignment
+ :: forall f . (Bits f, Fractional f)
+ => ArithCircuit f -- ^ program
+ -> Map Int f -- ^ inputs
+ -> QapSet f
+generateAssignment circuit inputs
+ = evalArithCircuit lookupAtWire updateAtWire circuit $ initialQapSet inputs
+
+qapSetToMap :: QapSet g -> Map Int g
+qapSetToMap QapSet{..}
+ = fromList [(0, qapSetConstant)]
+ <> mapKeys ((+) 1) qapSetInput
+ <> mapKeys ((+) (1 + numOfInputs)) qapSetIntermediate
+ <> mapKeys ((+) (1 + numOfInputs + numOfInterms)) qapSetOutput
+ where
+ numOfInputs = maxKey qapSetInput
+ numOfInterms = maxKey qapSetIntermediate
+
+ maxKey :: Map Int a -> Int
+ maxKey = maximumSafe . Map.keys
+
+ maximumSafe :: (Num a, Ord a) => [a] -> a
+ maximumSafe [] = 0
+ maximumSafe ls = maximum ls + 1
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}
diff --git a/test/Test/Circuit/Affine.hs b/test/Test/Circuit/Affine.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Circuit/Affine.hs
@@ -0,0 +1,62 @@
+module Test.Circuit.Affine where
+
+import Circuit.Affine
+import qualified Data.Map as Map
+import Protolude
+import Test.Tasty.QuickCheck
+
+-------------------------------------------------------------------------------
+-- Generators
+-------------------------------------------------------------------------------
+
+arbAffineCircuit ::
+ Arbitrary f =>
+ Int ->
+ Int ->
+ Gen (AffineCircuit Int f)
+arbAffineCircuit numVars size
+ | size <= 0 =
+ oneof $
+ [ ConstGate <$> arbitrary
+ ]
+ ++ if numVars > 0
+ then [Var <$> choose (0, numVars - 1)]
+ else []
+ | size > 0 =
+ oneof
+ [ ScalarMul <$> arbitrary <*> arbAffineCircuit numVars (size - 1),
+ Add <$> arbAffineCircuit numVars (size - 1)
+ <*> arbAffineCircuit numVars (size - 1)
+ ]
+
+arbInputVector :: Arbitrary f => Int -> Gen (Map Int f)
+arbInputVector numVars = Map.fromList . zip [0 ..] <$> vector numVars
+
+-- | The input vector has to have the correct length, so we want to
+-- generate the program and the test input simultaneously.
+data AffineCircuitWithInputs f = AffineCircuitWithInputs (AffineCircuit Int f) [Map Int f]
+ deriving (Show)
+
+instance Arbitrary f => Arbitrary (AffineCircuitWithInputs f) where
+ arbitrary = do
+ numVars <- abs <$> arbitrary
+ program <- scale (`div` 7) $ sized (arbAffineCircuit numVars)
+ inputs <- vectorOf 10 $ arbInputVector numVars
+ pure $ AffineCircuitWithInputs program inputs
+
+-------------------------------------------------------------------------------
+-- Tests
+-------------------------------------------------------------------------------
+
+-- | Check that evaluating the vector representation of the circuit
+-- yields the same results as evaluating the circuit "directly". Field
+-- is instantiated as being the rationals for testing. It later should
+-- probably be something like Pairing.Fr.Fr.
+prop_affineCircuitToAffineMap ::
+ AffineCircuitWithInputs Rational -> Bool
+prop_affineCircuitToAffineMap (AffineCircuitWithInputs program inputs) =
+ all testInput inputs
+ where
+ testInput input =
+ evalAffineCircuit Map.lookup input program
+ == evalAffineMap (affineCircuitToAffineMap program) input
diff --git a/test/Test/Circuit/Arithmetic.hs b/test/Test/Circuit/Arithmetic.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Circuit/Arithmetic.hs
@@ -0,0 +1,209 @@
+{-# LANGUAGE DeriveAnyClass, DeriveGeneric, TupleSections #-}
+
+module Test.Circuit.Arithmetic where
+
+import Circuit.Affine
+import Circuit.Arithmetic
+import Data.Curve.Weierstrass.BN254 (Fr)
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Data.Pairing.BN254 (getRootOfUnity)
+import Fresh
+import Protolude
+import QAP
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+
+-------------------------------------------------------------------------------
+-- Test values
+-------------------------------------------------------------------------------
+
+testEqualCircuit :: ArithCircuit Fr
+testEqualCircuit = ArithCircuit [Equal (InputWire 0) (IntermediateWire 0) (OutputWire 0)]
+
+testInputMap :: Fr -> Map Int Fr
+testInputMap = Map.singleton 0
+
+testSplitUnsplitCircuit :: Int -> ArithCircuit Fr
+testSplitUnsplitCircuit nbits =
+ ArithCircuit
+ [ Split (InputWire 0) midWires,
+ Mul (ConstGate 1) (unsplit midWires) (OutputWire 0)
+ ]
+ where
+ midWires = fmap IntermediateWire [0 .. nbits - 1]
+
+-------------------------------------------------------------------------------
+-- Generators
+-------------------------------------------------------------------------------
+
+arbVars :: Int -> [Int] -> [Gen (AffineCircuit Wire f)]
+arbVars numInps mids =
+ varInps numInps ++ varMids mids
+ where
+ varInps size
+ | size <= 0 = []
+ | otherwise = [Var . InputWire <$> choose (0, numInps - 1)]
+ varMids [] = []
+ varMids ms@(_ : _) = [Var . IntermediateWire <$> elements ms]
+
+arbAffineCircuitWithMids ::
+ Arbitrary f =>
+ Int ->
+ [Int] ->
+ Int ->
+ Gen (AffineCircuit Wire f)
+arbAffineCircuitWithMids numInps mids size
+ | size <= 0 =
+ oneof $ [ConstGate <$> arbitrary] ++ arbVars numInps mids
+ | size > 0 =
+ oneof
+ [ ScalarMul <$> arbitrary <*> arbAffineCircuitWithMids numInps mids (size - 1),
+ Add <$> arbAffineCircuitWithMids numInps mids (size - 1)
+ <*> arbAffineCircuitWithMids numInps mids (size - 1)
+ ]
+
+arbInputVector :: (Arbitrary f) => Int -> Gen (Map Int f)
+arbInputVector numVars = Map.fromList . zip [0 ..] <$> vector numVars
+
+arbArithCircuit ::
+ Arbitrary f =>
+ -- | distribution of frequency of mul/equal/split
+ -- gates, respectively
+ (Int, Int, Int) ->
+ Int ->
+ Int ->
+ Gen (ArithCircuit f)
+arbArithCircuit (distMul, distEqual, distSplit) numInps size
+ | size <= 0 =
+ pure $ ArithCircuit []
+ | size > 0 =
+ do
+ ArithCircuit gates <- arbArithCircuit (distMul, distEqual, distSplit) numInps (size - 1)
+ let mids = [i | IntermediateWire i <- concatMap outputWires gates]
+ frequency . catMaybes $
+ [ (distMul,) <$> mulGate gates mids,
+ (distEqual,) <$> equalGate gates mids,
+ (distSplit,) <$> splitGate gates mids
+ ]
+ where
+ mulGate gates mids =
+ Just $ do
+ lhs <- arbAffineCircuitWithMids numInps mids 1
+ rhs <- arbAffineCircuitWithMids numInps mids 1
+ let outWire = case mids of
+ [] -> 0
+ ms@(_ : _) -> maximum ms + 1
+ gate = Mul lhs rhs (IntermediateWire outWire)
+ pure . ArithCircuit $ gates ++ [gate]
+ equalGate _ [] =
+ Nothing
+ equalGate gates mids@(_ : _) =
+ Just $ do
+ inp <- elements mids
+ let outWire =
+ case mids of
+ [] -> 0
+ ms@(_ : _) -> maximum ms + 1
+ gate =
+ Equal
+ (IntermediateWire inp)
+ (IntermediateWire outWire)
+ (IntermediateWire $ outWire + 1)
+ pure . ArithCircuit $ gates ++ [gate]
+ splitGate _ [] =
+ Nothing
+ splitGate gates mids@(_ : _) =
+ Just $ do
+ inp <- IntermediateWire <$> elements mids
+ let firstOutWire =
+ case mids of
+ [] -> 0
+ ms@(_ : _) -> maximum ms + 1
+ nbits = 256
+ outWires = fmap IntermediateWire [firstOutWire .. firstOutWire + nbits - 1]
+ gate = Split inp outWires
+ pure . ArithCircuit $ gates ++ [gate]
+
+-- | The input vector has to have the correct length, so we want to
+-- generate the program and the test input simultaneously.
+data ArithCircuitWithInputs f = ArithCircuitWithInputs (ArithCircuit f) [Map Int f]
+ deriving (Show, Generic, NFData)
+
+instance (Arbitrary f, Num f) => Arbitrary (ArithCircuitWithInputs f) where
+ arbitrary = do
+ numVars <- abs <$> arbitrary `suchThat` (> 0)
+ program <- sized (arbArithCircuit (50, 10, 1) numVars)
+ inputs <- vectorOf 5 $ arbInputVector numVars
+ pure $ ArithCircuitWithInputs program inputs
+
+data ArithCircuitWithInput f = ArithCircuitWithInput (ArithCircuit f) (Map Int f)
+ deriving (Show, Generic, NFData)
+
+instance (Arbitrary f, Num f) => Arbitrary (ArithCircuitWithInput f) where
+ arbitrary = do
+ numVars <- abs <$> arbitrary `suchThat` (> 0)
+ program <- sized (arbArithCircuit (50, 10, 1) numVars)
+ input <- arbInputVector numVars
+ pure $ ArithCircuitWithInput program input
+
+-------------------------------------------------------------------------------
+-- Tests
+-------------------------------------------------------------------------------
+
+unit_eqGate ::
+ Assertion
+unit_eqGate =
+ do
+ testEvalWith 0 @?= Just 0
+ testEvalWith 1 @?= Just 1
+ testEvalWith 2 @?= Just 1
+ testEvalWith 3 @?= Just 1
+ where
+ testEvalWith n =
+ lookupAtWire (OutputWire 0) $
+ evalArithCircuit
+ lookupAtWire
+ updateAtWire
+ testEqualCircuit
+ (initialQapSet $ testInputMap n)
+
+unit_splitUnsplit :: Assertion
+unit_splitUnsplit =
+ mapM_ (\n -> testSplitUnsplit n @?= Just n) (fmap fromIntegral [0 .. 2 ^ nbits - 1])
+ where
+ nbits = 16
+ testSplitUnsplit n =
+ lookupAtWire (OutputWire 0) $
+ evalArithCircuit
+ lookupAtWire
+ updateAtWire
+ (testSplitUnsplitCircuit nbits)
+ (initialQapSet $ testInputMap n)
+
+prop_arithCircuitValid :: ArithCircuitWithInputs Fr -> Bool
+prop_arithCircuitValid (ArithCircuitWithInputs program _) =
+ validArithCircuit program
+
+prop_arithCircuitToQAP_slow :: ArithCircuitWithInputs Fr -> Property
+prop_arithCircuitToQAP_slow (ArithCircuitWithInputs program inputs) =
+ withMaxSuccess 10 $
+ case program of
+ ArithCircuit [] -> True
+ ArithCircuit (_ : _) -> all testInput inputs
+ where
+ roots = evalFresh $ generateRoots (fromIntegral . (+ 1) <$> fresh) program
+ qap = arithCircuitToQAP roots program
+ testInput input =
+ verifyAssignment qap $ generateAssignment program input
+
+prop_arithCircuitToQAP_fft :: ArithCircuitWithInputs Fr -> Property
+prop_arithCircuitToQAP_fft (ArithCircuitWithInputs program inputs) =
+ withMaxSuccess 10 $
+ case program of
+ ArithCircuit [] -> True
+ ArithCircuit (_ : _) -> all testInput inputs
+ where
+ roots = evalFresh $ generateRoots (fromIntegral . (+ 1) <$> fresh) program
+ qap = createPolynomialsFFT getRootOfUnity $ arithCircuitToGenQAP roots program
+ testInput input = verifyAssignment qap $ generateAssignment program input
diff --git a/test/Test/Circuit/Expr.hs b/test/Test/Circuit/Expr.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/Circuit/Expr.hs
@@ -0,0 +1,96 @@
+module Test.Circuit.Expr where
+
+import Circuit.Arithmetic
+import Circuit.Expr
+import Data.Curve.Weierstrass.BN254 (Fr)
+import qualified Data.Map as Map
+import Fresh
+import Protolude
+import QAP
+import Test.Circuit.Affine
+import Test.Tasty.QuickCheck
+
+-------------------------------------------------------------------------------
+-- Generators
+-------------------------------------------------------------------------------
+
+arbExprBool :: Arbitrary f => Int -> Int -> Gen (Expr Int f Bool)
+arbExprBool numVars size
+ | size <= 0 = oneof $ [EConstBool <$> arbitrary] ++ if numVars > 0
+ then []
+ else []
+ | size > 0 = oneof
+ [ EBinOp BAnd <$> arbExprBool numVars (size - 1) <*> arbExprBool
+ numVars
+ (size - 1)
+ , EBinOp BOr <$> arbExprBool numVars (size - 1) <*> arbExprBool numVars
+ (size - 1)
+ , EUnOp UNot <$> arbExprBool numVars (size - 1)
+ , EEq <$> arbExpr numVars (size - 1)
+ <*> arbExpr numVars (size - 1)
+ ]
+
+arbExpr :: Arbitrary f => Int -> Int -> Gen (Expr Int f f)
+arbExpr numVars size
+ | size <= 0 = oneof $ [EConst <$> arbitrary] ++ if numVars > 0
+ then [EVar <$> choose (0, numVars - 1)]
+ else []
+ | size > 0 = oneof
+ [ EBinOp BAdd <$> arbExpr numVars (size - 1) <*> arbExpr numVars (size - 1)
+ , EBinOp BSub <$> arbExpr numVars (size - 1) <*> arbExpr numVars (size - 1)
+ , EBinOp BMul <$> arbExpr numVars (size - 1) <*> arbExpr numVars (size - 1)
+ , EUnOp UNeg <$> arbExpr numVars (size - 1)
+ , EIf
+ <$> arbExprBool numVars (size - 1)
+ <*> arbExpr numVars (size - 1)
+ <*> arbExpr numVars (size - 1)
+ ]
+
+
+data ExprWithInputs f = ExprWithInputs (Expr Int f f) [Map Int f]
+ deriving Show
+
+
+instance Arbitrary f => Arbitrary (ExprWithInputs f) where
+ arbitrary = do
+ numVars <- abs <$> arbitrary
+ program <- scale (`div` 10) $ sized (arbExpr numVars)
+ inputs <- vectorOf 5 $ arbInputVector numVars
+ pure $ ExprWithInputs program inputs
+
+-------------------------------------------------------------------------------
+-- Tests
+-------------------------------------------------------------------------------
+
+
+-- | Check whether exprToArithCircuit produces valid circuits
+prop_compiledCircuitValid :: ExprWithInputs Fr -> Bool
+prop_compiledCircuitValid (ExprWithInputs expr _) =
+ validArithCircuit (execCircuitBuilder $ exprToArithCircuit expr (OutputWire 0))
+
+-- | Check whether exprToArithCircuit produces circuits that have valid assignments to the qap
+prop_compiledQAPValid :: ExprWithInputs Fr -> Property
+prop_compiledQAPValid (ExprWithInputs expr inputs) = withMaxSuccess 50
+ $ all testInput inputs
+ where
+ circuit = (execCircuitBuilder $ exprToArithCircuit expr (OutputWire 0))
+ roots :: ArithCircuit Fr -> [[Fr]]
+ roots = evalFresh . generateRoots (fromIntegral <$> fresh)
+ qap = arithCircuitToQAP (roots circuit) circuit
+ assignment input = generateAssignment circuit input
+ testInput = verifyAssignment qap . assignment
+
+-- | Check whether evaluating an expression and
+-- evaluating the arithmetic circuit translation produces the same
+-- result
+prop_evalEqArithEval :: ExprWithInputs Fr -> Bool
+prop_evalEqArithEval (ExprWithInputs expr inputs) = all testInput inputs
+ where
+ testInput input = exprResult input == arithResult input
+ exprResult input = evalExpr (Map.lookup) expr input
+ arithResult input = arithOutput input Map.! (OutputWire 0)
+ arithOutput input = evalArithCircuit (Map.lookup)
+ (Map.insert)
+ circuit
+ (Map.mapKeys InputWire input)
+ circuit = (execCircuitBuilder $ exprToArithCircuit expr (OutputWire 0))
diff --git a/test/Test/QAP.hs b/test/Test/QAP.hs
new file mode 100644
--- /dev/null
+++ b/test/Test/QAP.hs
@@ -0,0 +1,103 @@
+module Test.QAP where
+
+import Protolude
+
+import Data.Map (Map)
+import qualified Data.Map as Map
+import Test.Tasty.HUnit
+import Test.Tasty.QuickCheck
+
+import Circuit.Affine
+import Circuit.Arithmetic
+import Data.Pairing.BN254 (Fr, getRootOfUnity)
+import QAP
+
+import Test.Circuit.Affine (arbAffineCircuit, arbInputVector)
+
+-------------------------------------------------------------------------------
+-- Generators
+-------------------------------------------------------------------------------
+
+arbGate
+ :: Arbitrary f
+ => Int -> Gen (Gate Wire f)
+arbGate numVars
+ = oneof
+ [ Mul <$> (mapVarsAffine InputWire <$> sized (arbAffineCircuit numVars))
+ <*> (mapVarsAffine InputWire <$> sized (arbAffineCircuit numVars))
+ <*> pure (OutputWire 0)
+ , Equal <$> (InputWire <$> choose (0, numVars - 1))
+ <*> pure (IntermediateWire 0)
+ <*> pure (OutputWire 0)
+ ]
+
+data GateWithInputs f = GateWithInputs (Gate Wire f) [Map Int f]
+ deriving Show
+
+instance Arbitrary f => Arbitrary (GateWithInputs f) where
+ arbitrary = do
+ numVars <- (+1) . abs <$> arbitrary
+ program <- scale (`div` 7) $ arbGate numVars
+ inputs <- vectorOf 10 (arbInputVector numVars)
+ pure $ GateWithInputs program inputs
+
+-------------------------------------------------------------------------------
+-- Test values
+-------------------------------------------------------------------------------
+
+testArithCircuit :: ArithCircuit Fr
+testArithCircuit
+ = ArithCircuit
+ [ Mul (Var (InputWire 0)) (Var (InputWire 1)) (IntermediateWire 0)
+ , Mul (Var (InputWire 2)) (Var (InputWire 3)) (IntermediateWire 1)
+ , Mul (Add (ConstGate 10) (Var (IntermediateWire 0))) (Var (IntermediateWire 1)) (OutputWire 0)
+ ]
+
+testVarsArithCircuit :: Map Int Fr
+testVarsArithCircuit
+ = Map.fromList [ (0, 2)
+ , (1, 3)
+ , (2, 4)
+ , (3, 5)
+ ]
+
+-------------------------------------------------------------------------------
+-- Tests
+-------------------------------------------------------------------------------
+
+unit_arithCircuitToQapCorrect :: Assertion
+unit_arithCircuitToQapCorrect
+ = assertBool "Verifying assignment against QAP of circuit failed"
+ $ verifyAssignment qap assignment
+ where
+ roots = [[7],[8],[9]]
+ qap = arithCircuitToQAP roots testArithCircuit
+ assignment = generateAssignment testArithCircuit testVarsArithCircuit
+
+unit_arithCircuitToQapNoFalsePositive :: Assertion
+unit_arithCircuitToQapNoFalsePositive
+ = assertBool "Verifying whether verification fails on faulty assignment"
+ $ not $ verifyAssignment qap invalidAssignment
+ where
+ roots = [[7],[8],[9]]
+ qap = arithCircuitToQAP roots testArithCircuit
+ invalidAssignment
+ = QapSet
+ { qapSetConstant = 1
+ , qapSetInput = Map.fromList [(0,2),(1,3),(2,4),(3,5)]
+ , qapSetIntermediate = Map.fromList [(0,7),(1,20)]
+ , qapSetOutput = Map.fromList [(0,320)]
+ }
+
+prop_gateToQapCorrect
+ :: GateWithInputs Fr -> Bool
+prop_gateToQapCorrect (GateWithInputs program inputs)
+ = all testInput inputs
+ where
+ roots = case program of
+ Mul {} -> [1]
+ Equal {} -> [1,2]
+ _ -> panic "Invalid roots"
+ qap = gateToQAP getRootOfUnity roots program
+ assignment input = generateAssignmentGate program input
+ testInput = verifyAssignment qap . assignment