1# circon
  2
  3Circon is a language designed to write aritmetic circuits to be used in zero knowlage proof.
  4
  5Concretly it is designed to work in convination with [zksnarks javascript library](https://github.com/iden3/zksnark)
  6
  7
  8## Usage
  9
 10### First circuit
 11
 12Create a circuit. This is a simple example for 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 is mainly a javascript/c syntax but with extra 5 operators in order to define the constrains:
 29
 30`<==` , `==>`  This operator is used to connect signals. This operator also implies a constrain.
 31
 32As you can see in the example above, `out` is assigned a value and a constrain is also generated.  The assigned value must be of the form a*b+c where a,b and c are linear convinations of the signals.
 33
 34`<--` , `-->` This operators assign values to a signals but does not generate any constrain. This allow to assign any value to a signal including extrange operations like shifhts, modules, divisiones, etc.  Generally this operator goes together wit a `===` operator in order to force the constrain.
 35
 36`===` This operator defines a constrain. The constrain must be simplificable to the form a*b+c=0 where a,b and c are linear convinations.
 37
 38In the example above, we force the two inputs to be binary by adding the constrain `a*(a-1)===0` and `b*(b-1) === 0`
 39
 40### Compile the circui
 41
 42To compile the circuit, you first install the compiler:
 43
 44```
 45npm install -g circom
 46````
 47
 48Then just run
 49
 50```
 51circom -s mycircuit.circom -o mycircuit.json
 52```
 53
 54The resulting output ( `mycircuit.json` ) can be used with the [zksnarks javascript library](https://github.com/iden3/zksnark)
 55
 56In that library you will be able to do the trusted setup, create the proofs and verify them.
 57
 58### Number to binary
 59
 60In many situations, we have to convert an input to it's binary representation.  We would write a circuit 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
 80The first thing we observe in this example is that templates can have parameters. This allows to create libraries with templates that generate circuits in a parametric ways. In this case, we are using a circuit with an output of 8 signals, but you can instantiate easily any circuit with any number of outputs.
 81
 82Then we define the inputs and the outputs. We see that we can work with arrays. The program allows multidimension arrays for signals and variables.
 83
 84Then we need to assign the values to the different signals. In this case, we assign the value without the constrain by using the shift and & operators:
 85`out[i] <-- (in >> i) & 1;`
 86
 87But we need to define also the constrains.  In this case there is a big constrain of the form:
 88
 89```
 90in === out[0]*2**0  + out[1]*2**1 + out[2]*2**2  ....
 91```
 92
 93We do this by using a variable `lc1` and adding each signal multiplied by his coefficient.
 94
 95This variable does not hold a value in compilation time, but it holds a linear combination.  and it is used in the last constrain:
 96
 97```
 98lc1 === in;
 99```
100
101Finally we also have to force each output to be binary.
102
103We do this by adding this constrain for each output:
104
105```
106out[i] * (out[i] -1 ) === 0;
107```
108
109### A Binary adder.
110Lets now create a 32bits adder.
111
112The strategy will be to first convert the number to binary, do the addition in the binary space and then finally convert it back to a number.
113
114We could do it directly by adding a simple constrain where out === in1 + in2, but if we do this the operation will not be module 2**32 but `r` where r is the range of the elliptic curve. In the case of regular zkSnarks typically is some prime number close to 2**253
115
116With this example we also demostrate the normal patter of binarize a number, work in binary (reguular electronic circuit), and then convert the result back to a number.
117
118To do this, we will create 3 files named: `bitify.circom` `binsum.circom` and `sum_test.circom`
119
120bitify.circom:
121```
122template Num2Bits(n) {
123    signal input in;
124    signal output out[n];
125    var lc1=0;
126
127    for (var i = 0; i<n; i++) {
128        out[i] <-- (in >> i) & 1;
129        out[i] * (out[i] -1 ) === 0;
130        lc1 += out[i] * 2**i;
131    }
132
133    lc1 === in;
134
135}
136
137template Bits2Num(n) {
138    signal input in[n];
139    signal output out;
140    var lc1=0;
141
142    for (var i = 0; i<n; i++) {
143        lc1 += in[i] * 2**i;
144    }
145
146    lc1 ==> out;
147}
148
149```
150
151binsum.circom
152```
153/*
154
155Binary Sum
156==========
157
158This component creates a binary sum componet of ops operands and n bits each operand.
159
160e is Number of carries: Depends on the number of operands in the input.
161
162Main Constrain:
163   in[0][0]     * 2^0  +  in[0][1]     * 2^1  + ..... + in[0][n-1]    * 2^(n-1)  +
164 + in[1][0]     * 2^0  +  in[1][1]     * 2^1  + ..... + in[1][n-1]    * 2^(n-1)  +
165 + ..
166 + in[ops-1][0] * 2^0  +  in[ops-1][1] * 2^1  + ..... + in[ops-1][n-1] * 2^(n-1)  +
167 ===
168   out[0] * 2^0  + out[1] * 2^1 +   + out[n+e-1] *2(n+e-1)
169
170To waranty binary outputs:
171
172    out[0]     * (out[0] - 1) === 0
173    out[1]     * (out[0] - 1) === 0
174    .
175    .
176    .
177    out[n+e-1] * (out[n+e-1] - 1) == 0
178
179 */
180
181
182/*
183    This function calculates the number of extra bits in the output to do the full sum.
184 */
185
186function nbits(a) {
187    var n = 1;
188    var r = 0;
189    while (n-1<a) {
190        r++;
191        n *= 2;
192    }
193    return r;
194}
195
196
197template BinSum(n, ops) {
198    var nout = nbits((2**n -1)*ops);
199    signal input in[ops][n];
200    signal output out[nout];
201
202    var lin = 0;
203    var lout = 0;
204
205    var k;
206    var j;
207
208    for (k=0; k<n; k++) {
209        for (j=0; j<ops; j++) {
210            lin += in[j][k] * 2**k;
211        }
212    }
213
214    for (k=0; k<nout; k++) {
215        out[k] <-- (lin >> k) & 1;
216
217        // Ensure out is binary
218        out[k] * (out[k] - 1) === 0;
219
220        lout += out[k] * 2**k;
221    }
222
223    // Ensure the sum;
224
225    lin === lout;
226}
227```
228
229sumtest.circom:
230```
231include "bitify.circom"
232include "binsum.circom"
233
234template Adder() {
235    signal private input a;
236    signal input b;
237    signal output out;
238
239    component n2ba = Num2Bits(32);
240    component n2bb = Num2Bits(32);
241    component sum = BinSum(32,2);
242    component b2n = Bits2Num(32);
243
244    n2ba.in <== a;
245    n2bb.in <== b;
246
247    for (var i=0; i<32; i++) {
248        sum.in[0][i] <== n2ba.out[i];
249        sum.in[1][i] <== n2bb.out[i];
250        b2n.in[i] <== sum.out[i];
251    }
252
253    out <== b2n.out;
254}
255
256component main = Adder();
257```
258
259In this example we can see how we can design a top dow circuit with many subcircuits and how we connect them together.
260
261We also see the option to create auxilary functions to do specific computations.
262
263
264## License
265
266circon is part of the iden3 project copyright 2018 0kims association and published with GPL-3 license, please check the COPYING file for more details.
267
268
269