arithmetic-circuits (empty) → 0.2.0
raw patch · 21 files changed
+3376/−0 lines, 21 filesdep +MonadRandomdep +QuickCheckdep +aeson
Dependencies added: MonadRandom, QuickCheck, aeson, arithmetic-circuits, base, bulletproofs, containers, criterion, elliptic-curve, filepath, galois-fft, galois-field, markdown-unlit, pairing, poly, process-extras, protolude, quickcheck-instances, semirings, tasty, tasty-discover, tasty-hunit, tasty-quickcheck, text, vector, wl-pprint-text
Files
- ChangeLog.md +9/−0
- LICENSE +21/−0
- README.lhs +291/−0
- README.md +287/−0
- arithmetic-circuits.cabal +185/−0
- bench/Circuit.hs +37/−0
- bench/Main.hs +16/−0
- src/Circuit.hs +10/−0
- src/Circuit/Affine.hs +125/−0
- src/Circuit/Arithmetic.hs +243/−0
- src/Circuit/Bulletproofs.hs +554/−0
- src/Circuit/Dot.hs +79/−0
- src/Circuit/Expr.hs +332/−0
- src/Circuit/Lang.hs +78/−0
- src/Fresh.hs +20/−0
- src/QAP.hs +618/−0
- test/Main.hs +1/−0
- test/Test/Circuit/Affine.hs +62/−0
- test/Test/Circuit/Arithmetic.hs +209/−0
- test/Test/Circuit/Expr.hs +96/−0
- test/Test/QAP.hs +103/−0
+ ChangeLog.md view
@@ -0,0 +1,9 @@+# Change log for arithmetic-circuits++## 0.2.0++* Added JSON serialisation for arithmetic circuits.++## 0.1.0++* Initial release.
+ LICENSE view
@@ -0,0 +1,21 @@+MIT License++Copyright (c) 2019 Adjoint++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.
+ README.lhs view
@@ -0,0 +1,291 @@+<p align="center">+<a href="https://www.adjoint.io">+ <img width="250" src="./.assets/adjoint.png" alt="Adjoint Logo" />+</a>+</p>++[](https://circleci.com/gh/adjoint-io/arithmetic-circuits)++# Arithmetic Circuits++An *arithmetic circuit* is a low-level representation of a program that consists+of gates computing arithmetic operations of addition and multiplication, with+wires connecting the gates.++This form allows us to express arbitrarily complex programs with a set of+*private inputs* and *public inputs* whose execution can be publicly verified+without revealing the private inputs. This construction relies on recent+advances in zero-knowledge proving systems:++* Groth16 ([G16](https://eprint.iacr.org/2016/260.pdf))+* Groth-Maller ([GM17](https://eprint.iacr.org/2017/540.pdf))+* Pinnochio ([PGHR13](https://eprint.iacr.org/2013/279.pdf))+* Bulletproofs ([BBBPWM17](https://web.stanford.edu/~buenz/pubs/bulletproofs.pdf))+* Sonic ([MBKM19](https://eprint.iacr.org/2019/099))++This library presents a low-level interface for building zkSNARK proving systems+from higher-level compilers. This system depends on the following cryptographic+dependenices.++* [pairing](https://www.github.com/adjoint-io/pairing) - Optimised bilinear+ pairings over elliptic curves+* [galois-field](https://www.github.com/adjoint-io/galois-field) - Finite field+ arithmetic+* [galois-fft](https://www.github.com/adjoint-io/galois-fft) - Finite field+ polynomial arithmetic based on fast Fourier transforms+* [elliptic-curve](https://www.github.com/adjoint-io/elliptic-curve) - Elliptic+ curve operations+* [bulletproofs](https://www.github.com/adjoint-io/bulletproofs) - Bulletproofs+ proof system+* [arithmoi](https://www.github.com/adjoint-io/arithmoi) - Number theory+ operations+* [semirings](https://www.github.com/adjoint-io/semirings) - Algebraic semirings+* [poly](https://www.github.com/adjoint-io/poly) - Efficient polynomial+ arithmetic++## Theory++### Towers of Finite Fields++This library can build proof systems polymorphically over a variety of pairing+friendly curves. By default we use the [BN254](https://github.com/adjoint-io/elliptic-curve/blob/master/src/Data/Curve/Weierstrass/BN254.hs)+with an efficient implementation of the optimal Ate pairing.++The Barreto-Naehrig (BN) family of curves achieve high security and efficiency+with pairings due to an optimum embedding degree and high 2-adicity. We have+implemented the optimal Ate pairing over the BN254 curve we define $q$ and $r$+as:++* $q = 36t^4 + 36t^3 + 24t^2 + 6t + 1$+* $r = 36t^4 + 36t^3 + 18t^2 + 6t + 1$+* $t = 4965661367192848881$++The tower of finite fields we work with is defined as:++* $\mathbb{F}_{q^2} = \mathbb{F}_q[u]/u^2 + 1$+* $\mathbb{F}_{q^6} = \mathbb{F}_{q^2}[v]/v^3 - (9 + u)$+* $\mathbb{F}_{q^{12}} = \mathbb{F}_{q^6}[w]/w^2 - v$++### Arithmetic circuits++<p align="center">+<img src="./.assets/circuit.png" alt="Arithmetic Circuit" height=300 align="left" />+</p>++An arithmetic circuit over a finite field is a directed acyclic graph with gates+as vertices and wires and edges. It consists of a list of multiplication gates+together with a set of linear consistency equations relating the inputs and+outputs of the gates.++Let $\mathbb{F}$ be a finite field and $C: \mathbb{F}^n \times \mathbb{F}^h \rightarrow \mathbb{F}^l$ a map that takes $n+h$+arguments as inputs from $\mathbb{F}$ and outputs l elements in $\mathbb{F}$. 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 $n$, $h$, $l$ respectively denote the input, witness and output size and+$N = (n+h)+l$ be the number of all inputs and outputs of the circuit+A tuple $(a_1, ..., a_N) \in \mathbb{F}^N$, is said to be a valid+assignment for an arithmetic circuit C if $C(a_1,...,a_{n+h}) = (a_{n+h+1}, ..., a_N)$.+++### Quadratic Arithmetic Programs (QAP)++QAPs are encodings of arithmetic circuits that allow the prover to construct a+proof of knowledge of a valid assignment $(a_1,...,a_N) \in \mathbb{F}^N$ for a given+circuit $C$.++A quadratic arithmetic program (QAP) $Q(C)$ contains three sets of polynomials in+$\mathbb{F}[x]$:++$$+A=\{A_k(x) : k \in \{0..m\}\}$, $B=\{B_k(x) : k \in \{0..m\}\}$, $C=\{C_k(x) : k \in \{0..m\}\}$+$$++and a target polynomial $T(x)$.++In this setting, an assignment $(a_1,...,a_N)$ is valid for a circuit $C$ if and+only if the target polynomial $T(x)$ divides the polynomial:++$$+P(x) = (A_0(x) + \sum_{k=1}^m a_k A_k(x)) (B_0(x) + \sum_{k=1}^m a_k B_k(x)) - (C_0(x) + \sum_{k=1}^m a_k C_k(x))$+$$++Logical circuits can be written in terms of the addition, multiplication and+negation operations.++* $\text{AND}(a,b) = ab$+* $\text{NOT}(a) = 1 - a$+* $\text{NAND}(a,b) = 1 - ab$+* $\text{NOR}(a,b) = 1 - (1 - a)(1 - b)$+* $\text{XOR}(a,b) = (a+b) - 2ab$++## 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)+```++<p>+ <img src=".assets/arithmetic-circuit-example.svg" width="250"/>+</p>+++## Example++We'll keep taking the program constructed with our DSL as example and will+use the library [pairing](https://www.github.com/adjoint-io/pairing) that+provides a field of points of the BN254 curve and precomputes primitive roots of+unity for binary powers that divide $r - 1$.++```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 $T(x)$ and+$P(x)$ 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 $P(x)$ by $T(x)$ 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.+```
+ README.md view
@@ -0,0 +1,287 @@+<p align="center">+<a href="https://www.adjoint.io">+ <img width="250" src="./.assets/adjoint.png" alt="Adjoint Logo" />+</a>+</p>++[](https://circleci.com/gh/adjoint-io/arithmetic-circuits)++# Arithmetic Circuits++An *arithmetic circuit* is a low-level representation of a program that consists+of gates computing arithmetic operations of addition and multiplication, with+wires connecting the gates.++This form allows us to express arbitrarily complex programs with a set of+*private inputs* and *public inputs* whose execution can be publicly verified+without revealing the private inputs. This construction relies on recent+advances in zero-knowledge proving systems:++* Groth16 ([G16](https://eprint.iacr.org/2016/260.pdf))+* Groth-Maller ([GM17](https://eprint.iacr.org/2017/540.pdf))+* Pinnochio ([PGHR13](https://eprint.iacr.org/2013/279.pdf))+* Bulletproofs ([BBBPWM17](https://web.stanford.edu/~buenz/pubs/bulletproofs.pdf))+* Sonic ([MBKM19](https://eprint.iacr.org/2019/099))++This library presents a low-level interface for building zkSNARK proving systems+from higher-level compilers. This system depends on the following cryptographic+dependenices.++* [pairing](https://www.github.com/adjoint-io/pairing) - Optimised bilinear+ pairings over elliptic curves+* [galois-field](https://www.github.com/adjoint-io/galois-field) - Finite field+ arithmetic+* [galois-fft](https://www.github.com/adjoint-io/galois-fft) - Finite field+ polynomial arithmetic based on fast Fourier transforms+* [elliptic-curve](https://www.github.com/adjoint-io/elliptic-curve) - Elliptic+ curve operations+* [bulletproofs](https://www.github.com/adjoint-io/bulletproofs) - Bulletproofs+ proof system+* [arithmoi](https://www.github.com/adjoint-io/arithmoi) - Number theory+ operations+* [semirings](https://www.github.com/adjoint-io/semirings) - Algebraic semirings+* [poly](https://www.github.com/adjoint-io/poly) - Efficient polynomial+ arithmetic++## Theory++### Towers of Finite Fields++This library can build proof systems polymorphically over a variety of pairing+friendly curves. By default we use the [BN254](https://github.com/adjoint-io/elliptic-curve/blob/master/src/Data/Curve/Weierstrass/BN254.hs)+with an efficient implementation of the optimal Ate pairing.++The Barreto-Naehrig (BN) family of curves achieve high security and efficiency+with pairings due to an optimum embedding degree and high 2-adicity. We have+implemented the optimal Ate pairing over the BN254 curve we define <img src="/tex/d5c18a8ca1894fd3a7d25f242cbe8890.svg?invert_in_darkmode&sanitize=true" align=middle width=7.928106449999989pt height=14.15524440000002pt/> and <img src="/tex/89f2e0d2d24bcf44db73aab8fc03252c.svg?invert_in_darkmode&sanitize=true" align=middle width=7.87295519999999pt height=14.15524440000002pt/>+as:++* <img src="/tex/f041cced24931de6e6fbe77cf7fdc920.svg?invert_in_darkmode&sanitize=true" align=middle width=221.83192679999993pt height=26.76175259999998pt/>+* <img src="/tex/c0ea121dfdf29950f20f29c86635f197.svg?invert_in_darkmode&sanitize=true" align=middle width=221.77679534999993pt height=26.76175259999998pt/>+* <img src="/tex/71d71cc186d8238f79d664af6a48289f.svg?invert_in_darkmode&sanitize=true" align=middle width=184.01870685pt height=21.18721440000001pt/>++The tower of finite fields we work with is defined as:++* <img src="/tex/66eff114f6c4385dd25cca62457ad776.svg?invert_in_darkmode&sanitize=true" align=middle width=134.80114229999998pt height=26.76175259999998pt/>+* <img src="/tex/661afe19025c1f97ae61a41f91d325e9.svg?invert_in_darkmode&sanitize=true" align=middle width=181.79879189999997pt height=26.76175259999998pt/>+* <img src="/tex/ad84179c73fb68d93d2a147cce2cb19c.svg?invert_in_darkmode&sanitize=true" align=middle width=152.75024985pt height=26.76175259999998pt/>++### Arithmetic circuits++<p align="center">+<img src="./.assets/circuit.png" alt="Arithmetic Circuit" height=300 align="left" />+</p>++An arithmetic circuit over a finite field is a directed acyclic graph with gates+as vertices and wires and edges. It consists of a list of multiplication gates+together with a set of linear consistency equations relating the inputs and+outputs of the gates.++Let <img src="/tex/2d4c6ac334688c42fb4089749e372345.svg?invert_in_darkmode&sanitize=true" align=middle width=10.045686749999991pt height=22.648391699999998pt/> be a finite field and <img src="/tex/c8a92e9bd23d2e4841e72114a69462d7.svg?invert_in_darkmode&sanitize=true" align=middle width=124.1115777pt height=27.91243950000002pt/> a map that takes <img src="/tex/5e27bca98285ab8eccf4d53506baeaec.svg?invert_in_darkmode&sanitize=true" align=middle width=39.42918209999999pt height=22.831056599999986pt/>+arguments as inputs from <img src="/tex/2d4c6ac334688c42fb4089749e372345.svg?invert_in_darkmode&sanitize=true" align=middle width=10.045686749999991pt height=22.648391699999998pt/> and outputs l elements in <img src="/tex/2d4c6ac334688c42fb4089749e372345.svg?invert_in_darkmode&sanitize=true" align=middle width=10.045686749999991pt height=22.648391699999998pt/>. 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 <img src="/tex/55a049b8f161ae7cfeb0197d75aff967.svg?invert_in_darkmode&sanitize=true" align=middle width=9.86687624999999pt height=14.15524440000002pt/>, <img src="/tex/2ad9d098b937e46f9f58968551adac57.svg?invert_in_darkmode&sanitize=true" align=middle width=9.47111549999999pt height=22.831056599999986pt/>, <img src="/tex/2f2322dff5bde89c37bcae4116fe20a8.svg?invert_in_darkmode&sanitize=true" align=middle width=5.2283516999999895pt height=22.831056599999986pt/> respectively denote the input, witness and output size and+<img src="/tex/dc35769e37858254d0d77fab2d83bcf4.svg?invert_in_darkmode&sanitize=true" align=middle width=114.45175665pt height=24.65753399999998pt/> be the number of all inputs and outputs of the circuit+A tuple <img src="/tex/2c4cf6568afbabb029a579215dfa6e3e.svg?invert_in_darkmode&sanitize=true" align=middle width=120.09967859999999pt height=27.6567522pt/>, is said to be a valid+assignment for an arithmetic circuit C if <img src="/tex/86c8263cd0afa711b888c85bcb5b03a3.svg?invert_in_darkmode&sanitize=true" align=middle width=241.74771059999995pt height=24.65753399999998pt/>.+++### Quadratic Arithmetic Programs (QAP)++QAPs are encodings of arithmetic circuits that allow the prover to construct a+proof of knowledge of a valid assignment <img src="/tex/6e1ad13b9c0521871bb453942700c519.svg?invert_in_darkmode&sanitize=true" align=middle width=120.09967859999999pt height=27.6567522pt/> for a given+circuit <img src="/tex/9b325b9e31e85137d1de765f43c0f8bc.svg?invert_in_darkmode&sanitize=true" align=middle width=12.92464304999999pt height=22.465723500000017pt/>.++A quadratic arithmetic program (QAP) <img src="/tex/9000cff3d46536c190fabb076ebe7cbb.svg?invert_in_darkmode&sanitize=true" align=middle width=38.70549539999999pt height=24.65753399999998pt/> contains three sets of polynomials in+<img src="/tex/a420c52aa24a502d60aef830b3b45f9f.svg?invert_in_darkmode&sanitize=true" align=middle width=28.57312259999999pt height=24.65753399999998pt/>:++<img src="/tex/cf792d8b490521d817a643a4adea6f28.svg?invert_in_darkmode&sanitize=true" align=middle width=184.37011065pt height=24.65753399999998pt/>, <img src="/tex/258504deb4909bd9a3058fffbdb20262.svg?invert_in_darkmode&sanitize=true" align=middle width=185.47456784999997pt height=24.65753399999998pt/>, <img src="/tex/36b962f85e4e4de2a88919a5e00acbe1.svg?invert_in_darkmode&sanitize=true" align=middle width=184.38600014999997pt height=24.65753399999998pt/>++and a target polynomial <img src="/tex/083da1124b81d709f20f2575ae9138c3.svg?invert_in_darkmode&sanitize=true" align=middle width=34.06973294999999pt height=24.65753399999998pt/>.++In this setting, an assignment <img src="/tex/d1dd493c98f06e9ef29b5fdc411e29f8.svg?invert_in_darkmode&sanitize=true" align=middle width=78.31669229999999pt height=24.65753399999998pt/> is valid for a circuit <img src="/tex/9b325b9e31e85137d1de765f43c0f8bc.svg?invert_in_darkmode&sanitize=true" align=middle width=12.92464304999999pt height=22.465723500000017pt/> if and+only if the target polynomial <img src="/tex/083da1124b81d709f20f2575ae9138c3.svg?invert_in_darkmode&sanitize=true" align=middle width=34.06973294999999pt height=24.65753399999998pt/> divides the polynomial:++<img src="/tex/d6b98fe1452c7c16cfd1ad84a2e7331b.svg?invert_in_darkmode&sanitize=true" align=middle width=613.0190187pt height=26.438629799999987pt/>++Logical circuits can be written in terms of the addition, multiplication and+negation operations.++* <img src="/tex/cc073b29543f2694def1c15e2d40cb07.svg?invert_in_darkmode&sanitize=true" align=middle width=110.71153004999998pt height=24.65753399999998pt/>+* <img src="/tex/bf01d477a12bededfd9d65617fedacc9.svg?invert_in_darkmode&sanitize=true" align=middle width=117.37814879999999pt height=24.65753399999998pt/>+* <img src="/tex/e5079841837a9e98336245a5ecdb2538.svg?invert_in_darkmode&sanitize=true" align=middle width=151.35072315pt height=24.65753399999998pt/>+* <img src="/tex/065fdfe9ba3a8e9e839cea21d15eb1cd.svg?invert_in_darkmode&sanitize=true" align=middle width=221.2135992pt height=24.65753399999998pt/>+* <img src="/tex/85a105718538df533c60d0d34caeac95.svg?invert_in_darkmode&sanitize=true" align=middle width=187.1858703pt height=24.65753399999998pt/>++## 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)+```++<p>+ <img src=".assets/arithmetic-circuit-example.svg" width="250"/>+</p>+++## Example++We'll keep taking the program constructed with our DSL as example and will+use the library [pairing](https://www.github.com/adjoint-io/pairing) that+provides a field of points of the BN254 curve and precomputes primitive roots of+unity for binary powers that divide <img src="/tex/580e7a6446bf50562e34247c545883a2.svg?invert_in_darkmode&sanitize=true" align=middle width=36.18335654999999pt height=21.18721440000001pt/>.++```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 <img src="/tex/083da1124b81d709f20f2575ae9138c3.svg?invert_in_darkmode&sanitize=true" align=middle width=34.06973294999999pt height=24.65753399999998pt/> and+<img src="/tex/52be0087c9da1f0683ccc50761e8bcab.svg?invert_in_darkmode&sanitize=true" align=middle width=35.01719264999999pt height=24.65753399999998pt/> 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 <img src="/tex/52be0087c9da1f0683ccc50761e8bcab.svg?invert_in_darkmode&sanitize=true" align=middle width=35.01719264999999pt height=24.65753399999998pt/> by <img src="/tex/083da1124b81d709f20f2575ae9138c3.svg?invert_in_darkmode&sanitize=true" align=middle width=34.06973294999999pt height=24.65753399999998pt/> 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.+```
+ arithmetic-circuits.cabal view
@@ -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
+ bench/Circuit.hs view
@@ -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+ ]+
+ bench/Main.hs view
@@ -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+ ]
+ src/Circuit.hs view
@@ -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
+ src/Circuit/Affine.hs view
@@ -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
+ src/Circuit/Arithmetic.hs view
@@ -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)
+ src/Circuit/Bulletproofs.hs view
@@ -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+ }
+ src/Circuit/Dot.hs view
@@ -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")++
+ src/Circuit/Expr.hs view
@@ -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)
+ src/Circuit/Lang.hs view
@@ -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
+ src/Fresh.hs view
@@ -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
+ src/QAP.hs view
@@ -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
+ test/Main.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}
+ test/Test/Circuit/Affine.hs view
@@ -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
+ test/Test/Circuit/Arithmetic.hs view
@@ -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
+ test/Test/Circuit/Expr.hs view
@@ -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))
+ test/Test/QAP.hs view
@@ -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