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