circom/README.md
README.mdRaw
1# Circom
2
3Circom is a language designed to write arithmetic circuits that can be used in zero knowledge proofs.
4
5In particular, it is designed to work in [zksnarks JavaScript library](https://github.com/iden3/zksnark).
6
7
8## Usage
9
10### Tutorial
11
12A good starting point [is this tutorial](https://github.com/iden3/circom/blob/master/TUTORIAL.md)
13
14Also this [video](https://www.youtube.com/watch?v=-9TJa1hVsKA) is a good starting point.
15
16### First circuit
17
18Creation of a circuit. This is an example of a NAND door:
19
20```
21template NAND() {
22 signal private input a;
23 signal input b;
24 signal output out;
25
26 out <== 1 - a*b;
27 a*(a-1) === 0;
28 b*(b-1) === 0;
29}
30
31component main = NAND();
32```
33
34The language uses mainly JavaScript/C syntax together with 5 extra operators to define the following constraints:
35
36`<==` , `==>` : These two operators are used to connect signals and at the same time imply a constraint.
37
38As it is shown in the above example, a value is assigned to `out` and a constraint is also generated. The assigned value must be of the form a*b+c where a,b and c are linear combinations of the signals.
39
40`<--` , `-->` : These operators assign values to signals but do not generate any constraints. This allows to assign to a signal any value involving strange operations like shifts, divisions, modulo operations, etc. In general, these operators are used together with a `===` operator in order to force the constraint.
41
42`===` : This operator defines a constraint. The constraint must be simplificable to a constraint of the form `a*b+c=0`, where `a`, `b` and `c` are linear combinations of the signals.
43
44In the above example, both inputs are forced to be binary by adding the constraints `a*(a-1)===0` and `b*(b-1) === 0`.
45
46### Compilation the circuit
47
48First of all, the compiler must be installed by typing:
49
50```
51npm install -g circom
52````
53
54The circuit is compiled with the following command:
55
56```
57circom mycircuit.circom -o mycircuit.json
58```
59
60The resulting output ( `mycircuit.json` ) can be used in the [zksnarks JavaScript library](https://github.com/iden3/zksnark).
61
62In this library one can do the trusted setup, create the proofs and verify them.
63
64### Number to binary
65
66In many situations, one has to convert an input to its binary representation. Therefore, the circuits can be written this way:
67
68```
69template Num2Bits(n) {
70 signal input in;
71 signal output out[n];
72 var lc1=0;
73
74 for (var i = 0; i<n; i++) {
75 out[i] <-- (in >> i) & 1;
76 out[i] * (out[i] -1 ) === 0;
77 lc1 += out[i] * 2**i;
78 }
79
80 lc1 === in;
81}
82
83component main = Num2Bits(8)
84```
85
86First of all, note that templates can have parameters. This allows to create libraries with templates that generate circuits in parametric ways. In this case, the circuit has an output of 8 signals, but one can easily instantiate any circuit with any number of outputs.
87
88The inputs and outputs are defined as arrays. The programm allows multidimensional arrays for signals and variables.
89
90Then, the values are assigned to each of the signals. In this case, the values are assigned without the constraint using the shift and & operators:
91`out[i] <-- (in >> i) & 1;`
92
93Afterwards, the constraints need to be defined. In this case, there is a big constraint of the form:
94
95```
96in === out[0]*2**0 + out[1]*2**1 + out[2]*2**2 + ... + out[n-1]*2**(n-1)
97```
98
99We do this by using a variable `lc1` and adding each signal multiplied by its coefficient.
100This variable does not hold a value at compilation time, but it holds a linear combination and it is used in the last constraint:
101
102```
103lc1 === in;
104```
105
106The last step is to force each output to be binary. This is done by adding the following constraint to each output:
107
108```
109out[i] * (out[i] -1 ) === 0;
110```
111
112### A binary adder
113
114Let's now create a 32bits adder.
115
116This operation could be done directly by adding a simple constraint `out === in1 + in2`,
117but doing this the operation would not be module `2**32` but `r`, where `r`is the range of the elliptic curve. In the case of the zCash current implementation of zkSNARKs this number is typically some prime close to 2**253.
118
119So, the strategy we will follow will be to first convert a number to binary, then do the addition using the binary representation like in regular electronic circuits, and finally change it back to a number.
120
121To do this, we create 3 files: `bitify.circom`, `binsum.circom` and `sum_test.circom`.
122
123bitify.circom:
124```
125template Num2Bits(n) {
126 signal input in;
127 signal output out[n];
128 var lc1=0;
129
130 for (var i = 0; i<n; i++) {
131 out[i] <-- (in >> i) & 1;
132 out[i] * (out[i] -1 ) === 0;
133 lc1 += out[i] * 2**i;
134 }
135
136 lc1 === in;
137
138}
139
140template Bits2Num(n) {
141 signal input in[n];
142 signal output out;
143 var lc1=0;
144
145 for (var i = 0; i<n; i++) {
146 lc1 += in[i] * 2**i;
147 }
148
149 lc1 ==> out;
150}
151
152```
153
154binsum.circom
155```
156/*
157
158Binary sum
159==========
160
161This component creates a binary sum componet of ops operands and n bits each operand.
162
163e is number of carries and it depends on the number of operands in the input.
164
165Main Constraint:
166 in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1) +
167 + in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1) +
168 + ..
169 + in[ops-1][0] * 2^0 + in[ops-1][1] * 2^1 + ..... + in[ops-1][n-1] * 2^(n-1) +
170 ===
171 out[0] * 2^0 + out[1] * 2^1 + + out[n+e-1] *2(n+e-1)
172
173To waranty binary outputs:
174
175 out[0] * (out[0] - 1) === 0
176 out[1] * (out[0] - 1) === 0
177 .
178 .
179 .
180 out[n+e-1] * (out[n+e-1] - 1) === 0
181
182 */
183
184
185/* This function calculates the number of extra bits in the output to do the full sum. */
186
187function nbits(a) {
188 var n = 1;
189 var r = 0;
190 while (n-1<a) {
191 r++;
192 n *= 2;
193 }
194 return r;
195}
196
197
198template BinSum(n, ops) {
199 var nout = nbits((2**n -1)*ops);
200 signal input in[ops][n];
201 signal output out[nout];
202
203 var lin = 0;
204 var lout = 0;
205
206 var k;
207 var j;
208
209 for (k=0; k<n; k++) {
210 for (j=0; j<ops; j++) {
211 lin += in[j][k] * 2**k;
212 }
213 }
214
215 for (k=0; k<nout; k++) {
216 out[k] <-- (lin >> k) & 1;
217
218 // Ensure out is binary
219 out[k] * (out[k] - 1) === 0;
220
221 lout += out[k] * 2**k;
222 }
223
224 // Ensure the sum
225
226 lin === lout;
227}
228```
229
230sumtest.circom:
231```
232include "bitify.circom"
233include "binsum.circom"
234
235template Adder() {
236 signal private input a;
237 signal input b;
238 signal output out;
239
240 component n2ba = Num2Bits(32);
241 component n2bb = Num2Bits(32);
242 component sum = BinSum(32,2);
243 component b2n = Bits2Num(32);
244
245 n2ba.in <== a;
246 n2bb.in <== b;
247
248 for (var i=0; i<32; i++) {
249 sum.in[0][i] <== n2ba.out[i];
250 sum.in[1][i] <== n2bb.out[i];
251 b2n.in[i] <== sum.out[i];
252 }
253
254 out <== b2n.out;
255}
256
257component main = Adder();
258```
259
260In this example we have shown how to design a top-down circuit with many subcircuits and how to connect them together. One can also see that auxiliary functions to do specific computations can be created.
261
262
263### More examples.
264
265You can find more examples in this library of basic circits [circomlib](https://github.com/iden3/circomlib)
266
267
268## License
269
270Circom is part of the iden3 project copyright 2018 0KIMS association and published with GPL-3 license. Please check the COPYING file for more details.
271
272
273