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### Number to binary
 41
 42In many situations, we have to convert an input to it's binary representation.  We would write a circuit this way:
 43
 44```
 45template Num2Bits(n) {
 46    signal input in;
 47    signal output out[n];
 48    var lc1=0;
 49
 50    for (var i = 0; i<n; i++) {
 51        out[i] <-- (in >> i) & 1;
 52        out[i] * (out[i] -1 ) === 0;
 53        lc1 += out[i] * 2**i;
 54    }
 55
 56    lc1 === in;
 57}
 58
 59component main = Num2Bits(8)
 60```
 61
 62The 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.
 63
 64Then we define the inputs and the outputs. We see that we can work with arrays. The program allows multidimension arrays for signals and variables.
 65
 66Then 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:
 67`out[i] <-- (in >> i) & 1;`
 68
 69But we need to define also the constrains.  In this case there is a big constrain of the form:
 70
 71```
 72in === out[0]*2**0  + out[1]*2**1 + out[2]*2**2  ....
 73```
 74
 75We do this by using a variable `lc1` and adding each signal multiplied by his coefficient.
 76
 77This variable does not hold a value in compilation time, but it holds a linear combination.  and it is used in the last constrain:
 78
 79```
 80lc1 === in;
 81```
 82
 83Finally we also have to force each output to be binary.
 84
 85We do this by adding this constrain for each output:
 86
 87```
 88out[i] * (out[i] -1 ) === 0;
 89```
 90
 91### A Binary adder.
 92Lets now create a 32bits adder.
 93
 94The 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.
 95
 96We 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
 97
 98With 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.
 99
100To do this, we will create 3 files named: `bitify.circom` `binsum.circom` and `sum_test.circom`
101
102bitify.circom:
103```
104template Num2Bits(n) {
105    signal input in;
106    signal output out[n];
107    var lc1=0;
108
109    for (var i = 0; i<n; i++) {
110        out[i] <-- (in >> i) & 1;
111        out[i] * (out[i] -1 ) === 0;
112        lc1 += out[i] * 2**i;
113    }
114
115    lc1 === in;
116
117}
118
119template Bits2Num(n) {
120    signal input in[n];
121    signal output out;
122    var lc1=0;
123
124    for (var i = 0; i<n; i++) {
125        lc1 += in[i] * 2**i;
126    }
127
128    lc1 ==> out;
129}
130
131```
132
133binsum.circom
134```
135/*
136
137Binary Sum
138==========
139
140This component creates a binary sum componet of ops operands and n bits each operand.
141
142e is Number of carries: Depends on the number of operands in the input.
143
144Main Constrain:
145   in[0][0]     * 2^0  +  in[0][1]     * 2^1  + ..... + in[0][n-1]    * 2^(n-1)  +
146 + in[1][0]     * 2^0  +  in[1][1]     * 2^1  + ..... + in[1][n-1]    * 2^(n-1)  +
147 + ..
148 + in[ops-1][0] * 2^0  +  in[ops-1][1] * 2^1  + ..... + in[ops-1][n-1] * 2^(n-1)  +
149 ===
150   out[0] * 2^0  + out[1] * 2^1 +   + out[n+e-1] *2(n+e-1)
151
152To waranty binary outputs:
153
154    out[0]     * (out[0] - 1) === 0
155    out[1]     * (out[0] - 1) === 0
156    .
157    .
158    .
159    out[n+e-1] * (out[n+e-1] - 1) == 0
160
161 */
162
163
164/*
165    This function calculates the number of extra bits in the output to do the full sum.
166 */
167
168function nbits(a) {
169    var n = 1;
170    var r = 0;
171    while (n-1<a) {
172        r++;
173        n *= 2;
174    }
175    return r;
176}
177
178
179template BinSum(n, ops) {
180    var nout = nbits((2**n -1)*ops);
181    signal input in[ops][n];
182    signal output out[nout];
183
184    var lin = 0;
185    var lout = 0;
186
187    var k;
188    var j;
189
190    for (k=0; k<n; k++) {
191        for (j=0; j<ops; j++) {
192            lin += in[j][k] * 2**k;
193        }
194    }
195
196    for (k=0; k<nout; k++) {
197        out[k] <-- (lin >> k) & 1;
198
199        // Ensure out is binary
200        out[k] * (out[k] - 1) === 0;
201
202        lout += out[k] * 2**k;
203    }
204
205    // Ensure the sum;
206
207    lin === lout;
208}
209```
210
211sumtest.circom:
212```
213include "bitify.circom"
214include "binsum.circom"
215
216template Adder() {
217    signal private input a;
218    signal input b;
219    signal output out;
220
221    component n2ba = Num2Bits(32);
222    component n2bb = Num2Bits(32);
223    component sum = BinSum(32,2);
224    component b2n = Bits2Num(32);
225
226    n2ba.in <== a;
227    n2bb.in <== b;
228
229    for (var i=0; i<32; i++) {
230        sum.in[0][i] <== n2ba.out[i];
231        sum.in[1][i] <== n2bb.out[i];
232        b2n.in[i] <== sum.out[i];
233    }
234
235    out <== b2n.out;
236}
237
238component main = Adder();
239```
240
241In this example we can see how we can design a top dow circuit with many subcircuits and how we connect them together.
242
243We also see the option to create auxilary functions to do specific computations.
244
245
246## License
247
248circon is part of the iden3 project copyright 2018 0kims association and published with GPL-3 license, please check the COPYING file for more details.
249
250
251