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