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