|
1 | | -<p align="center"> |
2 | | -<a href="https://www.adjoint.io"> |
3 | | - <img width="250" src="./.assets/adjoint.png" alt="Adjoint Logo" /> |
4 | | -</a> |
5 | | -</p> |
6 | | - |
7 | | -[](https://circleci.com/gh/adjoint-io/arithmetic-circuits) |
8 | | - |
9 | 1 | # Arithmetic Circuits |
10 | 2 |
|
11 | | -An *arithmetic circuit* is a low-level representation of a program that consists |
12 | | -of gates computing arithmetic operations of addition and multiplication, with |
13 | | -wires connecting the gates. |
14 | | - |
15 | | -This form allows us to express arbitrarily complex programs with a set of |
16 | | -*private inputs* and *public inputs* whose execution can be publicly verified |
17 | | -without revealing the private inputs. This construction relies on recent |
18 | | -advances in zero-knowledge proving systems: |
19 | | - |
20 | | -* Groth16 ([G16](https://eprint.iacr.org/2016/260.pdf)) |
21 | | -* Groth-Maller ([GM17](https://eprint.iacr.org/2017/540.pdf)) |
22 | | -* Pinnochio ([PGHR13](https://eprint.iacr.org/2013/279.pdf)) |
23 | | -* Bulletproofs ([BBBPWM17](https://web.stanford.edu/~buenz/pubs/bulletproofs.pdf)) |
24 | | -* Sonic ([MBKM19](https://eprint.iacr.org/2019/099)) |
25 | | - |
26 | | -This library presents a low-level interface for building zkSNARK proving systems |
27 | | -from higher-level compilers. This system depends on the following cryptographic |
28 | | -dependenices. |
29 | | - |
30 | | -* [pairing](https://www.github.com/adjoint-io/pairing) - Optimised bilinear |
31 | | - pairings over elliptic curves |
32 | | -* [galois-field](https://www.github.com/adjoint-io/galois-field) - Finite field |
33 | | - arithmetic |
34 | | -* [galois-fft](https://www.github.com/adjoint-io/galois-fft) - Finite field |
35 | | - polynomial arithmetic based on fast Fourier transforms |
36 | | -* [elliptic-curve](https://www.github.com/adjoint-io/elliptic-curve) - Elliptic |
37 | | - curve operations |
38 | | -* [bulletproofs](https://www.github.com/adjoint-io/bulletproofs) - Bulletproofs |
39 | | - proof system |
40 | | -* [arithmoi](https://www.github.com/adjoint-io/arithmoi) - Number theory |
41 | | - operations |
42 | | -* [semirings](https://www.github.com/adjoint-io/semirings) - Algebraic semirings |
43 | | -* [poly](https://www.github.com/adjoint-io/poly) - Efficient polynomial |
44 | | - arithmetic |
45 | | - |
46 | | -## Theory |
47 | | - |
48 | | -### Towers of Finite Fields |
49 | | - |
50 | | -This library can build proof systems polymorphically over a variety of pairing |
51 | | -friendly curves. By default we use the [BN254](https://github.com/adjoint-io/elliptic-curve/blob/master/src/Data/Curve/Weierstrass/BN254.hs) |
52 | | -with an efficient implementation of the optimal Ate pairing. |
53 | | - |
54 | | -The Barreto-Naehrig (BN) family of curves achieve high security and efficiency |
55 | | -with pairings due to an optimum embedding degree and high 2-adicity. We have |
56 | | -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/> |
57 | | -as: |
58 | | - |
59 | | -* <img src="/tex/f041cced24931de6e6fbe77cf7fdc920.svg?invert_in_darkmode&sanitize=true" align=middle width=221.83192679999993pt height=26.76175259999998pt/> |
60 | | -* <img src="/tex/c0ea121dfdf29950f20f29c86635f197.svg?invert_in_darkmode&sanitize=true" align=middle width=221.77679534999993pt height=26.76175259999998pt/> |
61 | | -* <img src="/tex/71d71cc186d8238f79d664af6a48289f.svg?invert_in_darkmode&sanitize=true" align=middle width=184.01870685pt height=21.18721440000001pt/> |
62 | | - |
63 | | -The tower of finite fields we work with is defined as: |
64 | | - |
65 | | -* <img src="/tex/66eff114f6c4385dd25cca62457ad776.svg?invert_in_darkmode&sanitize=true" align=middle width=134.80114229999998pt height=26.76175259999998pt/> |
66 | | -* <img src="/tex/661afe19025c1f97ae61a41f91d325e9.svg?invert_in_darkmode&sanitize=true" align=middle width=181.79879189999997pt height=26.76175259999998pt/> |
67 | | -* <img src="/tex/ad84179c73fb68d93d2a147cce2cb19c.svg?invert_in_darkmode&sanitize=true" align=middle width=152.75024985pt height=26.76175259999998pt/> |
68 | | - |
69 | | -### Arithmetic circuits |
70 | | - |
71 | | -<p align="center"> |
72 | | -<img src="./.assets/circuit.png" alt="Arithmetic Circuit" height=300 align="left" /> |
73 | | -</p> |
74 | | - |
75 | | -An arithmetic circuit over a finite field is a directed acyclic graph with gates |
76 | | -as vertices and wires and edges. It consists of a list of multiplication gates |
77 | | -together with a set of linear consistency equations relating the inputs and |
78 | | -outputs of the gates. |
79 | | - |
80 | | -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/> |
81 | | -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 |
82 | | -value of the inputs that pass through wires to gates are only manipulated according to arithmetic operations + or x (allowing |
83 | | -constant gates). |
84 | | - |
85 | | -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 |
86 | | -<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 |
87 | | -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 |
88 | | -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/>. |
89 | | - |
90 | | - |
91 | | -### Quadratic Arithmetic Programs (QAP) |
92 | | - |
93 | | -QAPs are encodings of arithmetic circuits that allow the prover to construct a |
94 | | -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 |
95 | | -circuit <img src="/tex/9b325b9e31e85137d1de765f43c0f8bc.svg?invert_in_darkmode&sanitize=true" align=middle width=12.92464304999999pt height=22.465723500000017pt/>. |
96 | | - |
97 | | -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 |
98 | | -<img src="/tex/a420c52aa24a502d60aef830b3b45f9f.svg?invert_in_darkmode&sanitize=true" align=middle width=28.57312259999999pt height=24.65753399999998pt/>: |
99 | | - |
100 | | -<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/> |
101 | | - |
102 | | -and a target polynomial <img src="/tex/083da1124b81d709f20f2575ae9138c3.svg?invert_in_darkmode&sanitize=true" align=middle width=34.06973294999999pt height=24.65753399999998pt/>. |
103 | | - |
104 | | -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 |
105 | | -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: |
106 | | - |
107 | | -<img src="/tex/d6b98fe1452c7c16cfd1ad84a2e7331b.svg?invert_in_darkmode&sanitize=true" align=middle width=613.0190187pt height=26.438629799999987pt/> |
108 | | - |
109 | | -Logical circuits can be written in terms of the addition, multiplication and |
110 | | -negation operations. |
111 | | - |
112 | | -* <img src="/tex/cc073b29543f2694def1c15e2d40cb07.svg?invert_in_darkmode&sanitize=true" align=middle width=110.71153004999998pt height=24.65753399999998pt/> |
113 | | -* <img src="/tex/bf01d477a12bededfd9d65617fedacc9.svg?invert_in_darkmode&sanitize=true" align=middle width=117.37814879999999pt height=24.65753399999998pt/> |
114 | | -* <img src="/tex/e5079841837a9e98336245a5ecdb2538.svg?invert_in_darkmode&sanitize=true" align=middle width=151.35072315pt height=24.65753399999998pt/> |
115 | | -* <img src="/tex/065fdfe9ba3a8e9e839cea21d15eb1cd.svg?invert_in_darkmode&sanitize=true" align=middle width=221.2135992pt height=24.65753399999998pt/> |
116 | | -* <img src="/tex/85a105718538df533c60d0d34caeac95.svg?invert_in_darkmode&sanitize=true" align=middle width=187.1858703pt height=24.65753399999998pt/> |
117 | | - |
118 | | -## DSL and Circuit Builder Monad |
119 | | - |
120 | | -Any arithmetic circuit can be built using a domain specific language to |
121 | | -construct circuits that lives inside [Lang.hs](src/Circuit/Lang.hs). |
122 | | - |
123 | | -```haskell ignore |
124 | | -type ExprM f a = State (ArithCircuit f, Int) a |
125 | | -execCircuitBuilder :: ExprM f a -> ArithCircuit f |
126 | | -``` |
127 | | - |
128 | | -```haskell ignore |
129 | | --- | Binary arithmetic operations |
130 | | -add, sub, mul :: Expr Wire f f -> Expr Wire f f -> Expr Wire f f |
131 | | -``` |
132 | | - |
133 | | -```haskell ignore |
134 | | --- | Binary logic operations |
135 | | --- Have to use underscore or similar to avoid shadowing @and@ and @or@ |
136 | | --- from Prelude/Protolude. |
137 | | -and_, or_, xor_ :: Expr Wire f Bool -> Expr Wire f Bool -> Expr Wire f Bool |
138 | | -``` |
139 | | - |
140 | | -```haskell ignore |
141 | | --- | Negate expression |
142 | | -not_ :: Expr Wire f Bool -> Expr Wire f Bool |
143 | | -``` |
144 | | - |
145 | | -```haskell ignore |
146 | | --- | Compare two expressions |
147 | | -eq :: Expr Wire f f -> Expr Wire f f -> Expr Wire f Bool |
148 | | -``` |
149 | | - |
150 | | -```haskell ignore |
151 | | --- | Convert wire to expression |
152 | | -deref :: Wire -> Expr Wire f f |
153 | | -``` |
154 | | - |
155 | | -```haskell ignore |
156 | | --- | Return compilation of expression into an intermediate wire |
157 | | -e :: Num f => Expr Wire f f -> ExprM f Wire |
158 | | -``` |
159 | | - |
160 | | -```haskell ignore |
161 | | --- | Conditional statement on expressions |
162 | | -cond :: Expr Wire f Bool -> Expr Wire f ty -> Expr Wire f ty -> Expr Wire f ty |
163 | | -``` |
164 | | - |
165 | | -```haskell ignore |
166 | | --- | Return compilation of expression into an output wire |
167 | | -ret :: Num f => Expr Wire f f -> ExprM f Wire |
168 | | -``` |
169 | | - |
170 | | -The following program represents the image of the |
171 | | -arithmetic circuit [above](#arithmetic-circuits-1). |
172 | | - |
173 | | -```haskell ignore |
174 | | -program :: ArithCircuit Fr |
175 | | -program = execCircuitBuilder (do |
176 | | - i0 <- fmap deref input |
177 | | - i1 <- fmap deref input |
178 | | - i2 <- fmap deref input |
179 | | - let r0 = mul i0 i1 |
180 | | - r1 = mul r0 (add i0 i2) |
181 | | - ret r1) |
182 | | -``` |
183 | | - |
184 | | -The output of an arithmetic circuit can be converted to a DOT graph and save it |
185 | | -as SVG. |
186 | | - |
187 | | -```haskell ignore |
188 | | -dotOutput :: Text |
189 | | -dotOutput = arithCircuitToDot (execCircuitBuilder program) |
190 | | -``` |
191 | | - |
192 | | -<p> |
193 | | - <img src=".assets/arithmetic-circuit-example.svg" width="250"/> |
194 | | -</p> |
195 | | - |
196 | | - |
197 | | -## Example |
198 | | - |
199 | | -We'll keep taking the program constructed with our DSL as example and will |
200 | | -use the library [pairing](https://www.github.com/adjoint-io/pairing) that |
201 | | -provides a field of points of the BN254 curve and precomputes primitive roots of |
202 | | -unity for binary powers that divide <img src="/tex/580e7a6446bf50562e34247c545883a2.svg?invert_in_darkmode&sanitize=true" align=middle width=36.18335654999999pt height=21.18721440000001pt/>. |
203 | | - |
204 | | -```haskell |
205 | | -import Protolude |
206 | | - |
207 | | -import qualified Data.Map as Map |
208 | | -import Data.Pairing.BN254 (Fr, getRootOfUnity) |
209 | | - |
210 | | -import Circuit.Arithmetic |
211 | | -import Circuit.Expr |
212 | | -import Circuit.Lang |
213 | | -import Fresh (evalFresh, fresh) |
214 | | -import QAP |
215 | | - |
216 | | -program :: ArithCircuit Fr |
217 | | -program = execCircuitBuilder (do |
218 | | - i0 <- fmap deref input |
219 | | - i1 <- fmap deref input |
220 | | - i2 <- fmap deref input |
221 | | - let r0 = mul i0 i1 |
222 | | - r1 = mul r0 (add i0 i2) |
223 | | - ret r1) |
224 | | -``` |
225 | | - |
226 | | -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 |
227 | | -<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 |
228 | | -allow the prover to construct a proof of a valid assignment. |
229 | | - |
230 | | -We also need to give values to the three input wires to this arithmetic circuit. |
231 | | - |
232 | | -```haskell |
233 | | -roots :: [[Fr]] |
234 | | -roots = evalFresh (generateRoots (fmap (fromIntegral . (+ 1)) fresh) program) |
235 | | - |
236 | | -qap :: QAP Fr |
237 | | -qap = arithCircuitToQAPFFT getRootOfUnity roots program |
238 | | - |
239 | | -inputs :: Map.Map Int Fr |
240 | | -inputs = Map.fromList [(0, 7), (1, 5), (2, 4)] |
241 | | -``` |
242 | | - |
243 | | -A prover can now generate a valid assignment. |
244 | | - |
245 | | -```haskell |
246 | | -assignment :: QapSet Fr |
247 | | -assignment = generateAssignment program inputs |
248 | | -``` |
249 | | - |
250 | | -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. |
251 | | - |
252 | | -```haskell |
253 | | -main :: IO () |
254 | | -main = do |
255 | | - if verifyAssignment qap assignment |
256 | | - then putText "Valid assignment" |
257 | | - else putText "Invalid assignment" |
258 | | -``` |
259 | | - |
260 | | -See [Example.hs](./Example.hs). |
261 | | - |
262 | | -## Disclaimer |
263 | | - |
264 | | -This is experimental code meant for research-grade projects only. Please do not |
265 | | -use this code in production until it has matured significantly. |
| 3 | +A Haskell library for building ZK programs |
266 | 4 |
|
267 | | -## License |
| 5 | +## Contents |
| 6 | +- High level expression language DSL for writing ZK programs |
| 7 | +- Low level arithmetic circuit DSL |
| 8 | +- Efficient constraint solver for arbitrary circuits |
| 9 | +- Binary codecs for core types (R1CS, witness, etc) which are compatible with the Circom toolchain |
| 10 | +- Witness generator which is WASM compatible with Circom witness generator binaries. |
268 | 11 |
|
269 | | -``` |
270 | | -Copyright (c) 2017-2020 Adjoint Inc. |
| 12 | +## Examples |
| 13 | +There are examples in `test` directory. See the sudoky verifier for the most complete example. |
271 | 14 |
|
272 | | -Permission is hereby granted, free of charge, to any person obtaining a copy |
273 | | -of this software and associated documentation files (the "Software"), to deal |
274 | | -in the Software without restriction, including without limitation the rights |
275 | | -to use, copy, modify, merge, publish, distribute, sublicense, and/or sell |
276 | | -copies of the Software, and to permit persons to whom the Software is |
277 | | -furnished to do so, subject to the following conditions: |
| 15 | +### Note about WASM target |
| 16 | +Circom is a language/compiler which has been widely adopted by developers building ZK programs. As such, many proving frameworks (e.g. arkworks, snarkjs, nova) have integrations with Circom that expect a certain binary serialization format for the r1cs and witness data. The Circom compiler also emits a witness calculator in the form of a WASM binary, which is meant to be embedded in a host environment (e.g. the browser, a rust program, etc). In the `circom-compat` library in this repo, we give the scaffolding that you need in order to produce this binary via GHC's WASM backend. You can see an example of how to use there [here](https://github.com/l-adic/factors) |
278 | 17 |
|
279 | | -The above copyright notice and this permission notice shall be included in all |
280 | | -copies or substantial portions of the Software. |
281 | 18 |
|
282 | | -THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, |
283 | | -EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF |
284 | | -MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. |
285 | | -IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, |
286 | | -DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR |
287 | | -OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE |
288 | | -OR OTHER DEALINGS IN THE SOFTWARE. |
289 | | -``` |
| 19 | +### Attributions |
| 20 | +This work started as a fork from the original [arithmetic-circuits](https://github.com/sdiehl/arithmetic-circuits) library which is no longer developed. Since there is currently no hope for merging changes upstream and GitHub forks have limited PM functionality, this repo has been severed. All good ideas surrounding the low-level circuit DSL come from those effors, and the supporting libs created by those original authors (e.g. galois-fields lib) are heavily used. You can find their original README in the `docs` folder. Much credit goes to them, in the event they revive the original libraries then PRs will be made. |
0 commit comments