Skip to content
This repository has been archived by the owner on Mar 15, 2024. It is now read-only.

Commit

Permalink
Changes after feedback
Browse files Browse the repository at this point in the history
  • Loading branch information
druiz0992 committed Apr 30, 2019
1 parent 4443570 commit 4decd7c
Show file tree
Hide file tree
Showing 28 changed files with 2,071 additions and 1,962 deletions.
2 changes: 1 addition & 1 deletion config/iden3_docmap.py
Expand Up @@ -440,7 +440,7 @@

iden3_repo = [ iden3js_docs, goiden3_docs, tx_forwarder_docs,
circom_docs, circomlib_docs, websnark_docs,
discovery_node_docs, citrus_docs, snarkjs_docs, notifications_server_docs,
discovery_node_docs, snarkjs_docs, notifications_server_docs,
wasmbuilder_docs, research_docs ]

iden3_docs = [ iden3_devel_docs, iden3_tech_docs, iden3_publications_docs]
Expand Down
2 changes: 1 addition & 1 deletion source/devel/centralized_login.rst
Expand Up @@ -2,7 +2,7 @@


##############################################
Centralized Login
Centralized Login Use Case
##############################################

.. topic:: Overview
Expand Down
242 changes: 121 additions & 121 deletions source/iden3_repos/circom/README.rst
Expand Up @@ -32,17 +32,17 @@ Creation of a circuit. This is an example of a NAND door:

::

template NAND() {
signal private input a;
signal input b;
signal output out;
template NAND() {
signal private input a;
signal input b;
signal output out;

out <== 1 - a*b;
a*(a-1) === 0;
b*(b-1) === 0;
}
out <== 1 - a*b;
a*(a-1) === 0;
b*(b-1) === 0;
}

component main = NAND();
component main = NAND();

The language uses mainly JavaScript/C syntax together with 5 extra
operators to define the following constraints:
Expand All @@ -52,7 +52,7 @@ at the same time imply a constraint.

As 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.
a*b+c where a,b and c are linear combinations of the signals.

``<--`` , ``-->`` : These operators assign values to signals but do not
generate any constraints. This allows to assign to a signal any value
Expand All @@ -74,13 +74,13 @@ First of all, the compiler must be installed by typing:

::

npm install -g circom
npm install -g circom

The circuit is compiled with the following command:

::

circom mycircuit.circom -o mycircuit.json
circom mycircuit.circom -o mycircuit.json

The resulting output ( ``mycircuit.json`` ) can be used in the `zksnarks
JavaScript library <https://github.com/iden3/zksnark>`__.
Expand All @@ -96,21 +96,21 @@ representation. Therefore, the circuits can be written this way:

::

template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;

for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * 2**i;
}
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * 2**i;
}

lc1 === in;
}
lc1 === in;
}

component main = Num2Bits(8)
component main = Num2Bits(8)

First of all, note that templates can have parameters. This allows to
create libraries with templates that generate circuits in parametric
Expand All @@ -129,7 +129,7 @@ big constraint of the form:

::

in === out[0]*2**0 + out[1]*2**1 + out[2]*2**2 + ... + out[n-1]*2**(n-1)
in === out[0]*2**0 + out[1]*2**1 + out[2]*2**2 + ... + out[n-1]*2**(n-1)

We do this by using a variable ``lc1`` and adding each signal multiplied
by its coefficient. This variable does not hold a value at compilation
Expand All @@ -138,25 +138,25 @@ constraint:

::

lc1 === in;
lc1 === in;

The last step is to force each output to be binary. This is done by
adding the following constraint to each output:

::

out[i] * (out[i] -1 ) === 0;
out[i] * (out[i] -1 ) === 0;

A binary adder
~~~~~~~~~~~~~~

Let's now create a 32bits adder.
Lets now create a 32bits adder.

This operation could be done directly by adding a simple constraint
``out === in1 + in2``, but 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.
typically some prime close to 2**253.

So, the strategy we will follow will be to first convert a number to
binary, then do the addition using the binary representation like in
Expand All @@ -169,140 +169,140 @@ bitify.circom:

::

template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;

for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * 2**i;
}
for (var i = 0; i<n; i++) {
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;
lc1 += out[i] * 2**i;
}

lc1 === in;
lc1 === in;

}
}

template Bits2Num(n) {
signal input in[n];
signal output out;
var lc1=0;
template Bits2Num(n) {
signal input in[n];
signal output out;
var lc1=0;

for (var i = 0; i<n; i++) {
lc1 += in[i] * 2**i;
}
for (var i = 0; i<n; i++) {
lc1 += in[i] * 2**i;
}

lc1 ==> out;
}
lc1 ==> out;
}

binsum.circom

::

/*
/*

Binary sum
==========
Binary sum
==========

This component creates a binary sum componet of ops operands and n bits each operand.
This component creates a binary sum componet of ops operands and n bits each operand.

e is number of carries and it depends on the number of operands in the input.
e is number of carries and it depends on the number of operands in the input.

Main Constraint:
in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1) +
+ in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1) +
+ ..
+ in[ops-1][0] * 2^0 + in[ops-1][1] * 2^1 + ..... + in[ops-1][n-1] * 2^(n-1) +
===
out[0] * 2^0 + out[1] * 2^1 + + out[n+e-1] *2(n+e-1)
Main Constraint:
in[0][0] * 2^0 + in[0][1] * 2^1 + ..... + in[0][n-1] * 2^(n-1) +
+ in[1][0] * 2^0 + in[1][1] * 2^1 + ..... + in[1][n-1] * 2^(n-1) +
+ ..
+ in[ops-1][0] * 2^0 + in[ops-1][1] * 2^1 + ..... + in[ops-1][n-1] * 2^(n-1) +
===
out[0] * 2^0 + out[1] * 2^1 + + out[n+e-1] *2(n+e-1)

To waranty binary outputs:
To waranty binary outputs:

out[0] * (out[0] - 1) === 0
out[1] * (out[0] - 1) === 0
.
.
.
out[n+e-1] * (out[n+e-1] - 1) == 0
out[0] * (out[0] - 1) === 0
out[1] * (out[0] - 1) === 0
.
.
.
out[n+e-1] * (out[n+e-1] - 1) == 0

*/
*/


/* This function calculates the number of extra bits in the output to do the full sum. */
/* This function calculates the number of extra bits in the output to do the full sum. */

function nbits(a) {
var n = 1;
var r = 0;
while (n-1<a) {
r++;
n *= 2;
}
return r;
}
function nbits(a) {
var n = 1;
var r = 0;
while (n-1<a) {
r++;
n *= 2;
}
return r;
}


template BinSum(n, ops) {
var nout = nbits((2**n -1)*ops);
signal input in[ops][n];
signal output out[nout];
template BinSum(n, ops) {
var nout = nbits((2**n -1)*ops);
signal input in[ops][n];
signal output out[nout];

var lin = 0;
var lout = 0;
var lin = 0;
var lout = 0;

var k;
var j;
var k;
var j;

for (k=0; k<n; k++) {
for (j=0; j<ops; j++) {
lin += in[j][k] * 2**k;
}
}
for (k=0; k<n; k++) {
for (j=0; j<ops; j++) {
lin += in[j][k] * 2**k;
}
}

for (k=0; k<nout; k++) {
out[k] <-- (lin >> k) & 1;
for (k=0; k<nout; k++) {
out[k] <-- (lin >> k) & 1;

// Ensure out is binary
out[k] * (out[k] - 1) === 0;
// Ensure out is binary
out[k] * (out[k] - 1) === 0;

lout += out[k] * 2**k;
}
lout += out[k] * 2**k;
}

// Ensure the sum
// Ensure the sum

lin === lout;
}
lin === lout;
}

sumtest.circom:

::

include "bitify.circom"
include "binsum.circom"
include "bitify.circom"
include "binsum.circom"

template Adder() {
signal private input a;
signal input b;
signal output out;
template Adder() {
signal private input a;
signal input b;
signal output out;

component n2ba = Num2Bits(32);
component n2bb = Num2Bits(32);
component sum = BinSum(32,2);
component b2n = Bits2Num(32);
component n2ba = Num2Bits(32);
component n2bb = Num2Bits(32);
component sum = BinSum(32,2);
component b2n = Bits2Num(32);

n2ba.in <== a;
n2bb.in <== b;
n2ba.in <== a;
n2bb.in <== b;

for (var i=0; i<32; i++) {
sum.in[0][i] <== n2ba.out[i];
sum.in[1][i] <== n2bb.out[i];
b2n.in[i] <== sum.out[i];
}
for (var i=0; i<32; i++) {
sum.in[0][i] <== n2ba.out[i];
sum.in[1][i] <== n2bb.out[i];
b2n.in[i] <== sum.out[i];
}

out <== b2n.out;
}
out <== b2n.out;
}

component main = Adder();
component main = Adder();

In 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
Expand Down

0 comments on commit 4decd7c

Please sign in to comment.