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
 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