arnaucube
arnaucube/circomPublic Self-hosted repository
circom/TUTORIAL.md
TUTORIAL.mdRaw
  1# circom and snarkjs tutorial
  2
  3This tutorial will guide you in creating your first zero-knowledge SNARK circuit. It will take you through the various techniques to write circuits and show you how to create and verify proofs off-chain and on-chain on Ethereum.
  4
  5## 1. Installing the tools
  6
  7### 1.1 Pre-requisites
  8
  9If you don't have it installed yet, you need to install `Node.js`.
 10
 11The last stable version of `Node.js` (or 8.12.0) works just fine, but if you install the latest current version `Node.js` (10.12.0) you will see a significant increase in performance. This is because last versions of node includes Big Integer Libraries nativelly. The `snarkjs` library makes use of this feature if available, and this improves the performance x10 (!).
 12
 13### 1.2 Install **circom** and **snarkjs**
 14
 15Run:
 16
 17```sh
 18npm install -g circom
 19npm install -g circom_runtime
 20npm install -g snarkjs
 21```
 22
 23
 24## 2. Working with a circuit
 25
 26Let's create a circuit that will allow you to prove that you are able to factor a number!
 27
 28### 2.1 Create a circuit in a new directory
 29
 301. Create an empty directory called `factor` where you will put all the files that you will use in this tutorial.
 31```
 32mkdir factor
 33cd factor
 34```
 35
 36
 37> In a real circuit, you will probably want to create a `git` repository with a `circuits` directory and a `test` directory with all your tests, and the needed scripts to build all the circuits.
 38
 392. Create a new file named `circuit.circom` with the following content:
 40
 41```
 42template Multiplier() {
 43    signal private input a;
 44    signal private input b;
 45    signal output c;
 46
 47    c <== a*b;
 48}
 49
 50component main = Multiplier();
 51```
 52
 53This circuit has 2 private input signals named `a` and `b` and one output named `c`.
 54
 55The only thing that the circuit does is forcing the signal `c` to be the value of `a*b`
 56
 57After declaring the `Multiplier` template, we instantiate it with a component named`main`.
 58
 59Note: When compiling a circuit, a component named `main` must always exist.
 60
 61### 2.2 Compile the circuit
 62
 63We are now ready to compile the circuit. Run the following command:
 64
 65```sh
 66circom circuit.circom --r1cs --wasm --sym
 67```
 68
 69The `--r1cs` option will generate `circuit.r1cs` (the r1cs constraint system of the circuit in binary format).
 70
 71The `--wasm` option will generate `circuit.wasm` (the wasm code to generate the witness).
 72
 73The `--sym` option will generate `circuit.sym` (a symbols file required for debugging or if you want to print the constraint system in an annotated mode).
 74
 75
 76## 3. Taking the compiled circuit to *snarkjs*
 77
 78Now that the circuit is compiled, we will continue with `snarkjs`.
 79Please note that you can always access the help of `snarkjs` by typing:
 80
 81```sh
 82snarkjs --help
 83```
 84
 85### 3.1 View information and stats regarding a circuit
 86
 87To show general statistics of this circuit, you can run:
 88
 89```sh
 90snarkjs info -r circuit.r1cs
 91```
 92
 93You can also print the constraints of the circuit by running:
 94
 95```sh
 96snarkjs printconstraints -r circuit.r1cs -s circuit.sym
 97```
 98
 99
100### 3.2 Setting up using *snarkjs*
101
102
103Ok, let's run a setup for our circuit:
104
105```sh
106snarkjs setup
107```
108
109> By default `snarkjs` will look for and use `circuit.r1cs`.  You can always specify a different circuit file by adding `-r <circuit R1CS file name>`
110
111The output of the setup will in the form of 2 files: `proving_key.json` and `verification_key.json`
112
113### 3.3. Calculating a witness
114
115Before creating any proof, we need to calculate all the signals of the circuit that match (all) the constrains of the circuit.
116
117`circom` generates a wasm module that calculates those for you.  You need to provide a file with the inputs and it will execute the circuit and calculate all the intermediate signals and the output. This set of signals is the *witness*.
118
119The zero knowledge proofs prove that you know a set of signals (witness) that match all the constraints, without revealing any of the signals except the public inputs plus the outputs.
120
121For example, imagine you want to prove you are able to factor 33. It means that you know two numbers `a` and `b` and when you multiply them, it results in 33.
122
123> Of course you can always use one and the same number as `a` or `b`.  We  will deal with this problem later.
124
125So you want to prove that you know 3 and 11.
126
127Let's create a file named `input.json`
128
129```json
130{"a": 3, "b": 11}
131```
132
133Now let's calculate the witness:
134
135```sh
136snarkjs calculatewitness --wasm circuit.wasm --input input.json --witness witness.json
137```
138
139`calcwit` is part of the circom_runtime package and it's just a wrapper in JS to call the wasm module.
140
141You can use `circom_runtime` from your own project to calulate the witness.
142
143You may want to take a look at `witness.json` file with all the signals.
144
145### Create the proof
146
147Now that we have the witness generated, we can create the proof.
148
149```sh
150snarkjs proof
151```
152
153This command will use the `proving_key.json` and the `witness.json` files by default to generate `proof.json` and `public.json`
154
155The `proof.json` file will contain the actual proof.  And the `public.json` file will contain just the values of the public inputs and the outputs.
156
157
158### Verifying the proof
159
160To verify the proof run:
161
162```sh
163snarkjs verify
164```
165
166This command will use `verification_key.json`, `proof.json` and `public.json` to verify that is valid.
167
168Here we are verifying that we know a witness that the public inputs and the outputs matches the ones in the `public.json` file.
169
170
171If the proof is ok, you will see `OK` or `INVALID` if not ok.
172
173### Generate the solidity verifier
174
175```sh
176snarkjs generateverifier
177```
178
179This command will take the `verification_key.json` and generate solidity code in `verifier.sol` file.
180
181You can take the code in `verifier.sol` and cut and paste it in remix.
182
183This code contains two contracts: Pairings and Verifier.  You only need to deploy the `Verifier` contract.
184
185> You may want to use a test net like Rinkeby, Kovan or Ropsten.  You can also use the Javascript VM, but in some browsers, the verification takes long and it may hang the page.
186
187
188### Verifying the proof on-chain
189
190The verifier contract deployed in the last step has a `view` function called `verifyProof`.
191
192This function will return true if the proof and the inputs are valid.
193
194To facilitate the call, you can use snarkjs to generate the parameters of the call by typing:
195
196```sh
197snarkjs generatecall
198```
199
200Just cut and paste the output to the parameters field of the `verifyProof` method in Remix.
201
202If every thing works ok, this method should return true.
203
204If you change any bit in the parameters, the result will be verifiably false.
205
206
207## Bonus track
208
209We can fix the circuit to not accept one as any of the values by adding some extra constraints.
210
211Here the trick is that we use the property that 0 has no inverse.  So `(a-1)` should not have an inverse.
212
213That means that `(a-1)*inv = 1` will be inpossible to match if `a` is 1.
214
215We just calculate inv by `1/(a-1)`
216
217So let's modify the circuit:
218
219```
220template Multiplier() {
221    signal private input a;
222    signal private input b;
223    signal output c;
224    signal inva;
225    signal invb;
226
227    inva <-- 1/(a-1);
228    (a-1)*inva === 1;
229
230    invb <-- 1/(b-1);
231    (b-1)*invb === 1;
232
233    c <== a*b;
234}
235
236component main = Multiplier();
237```
238
239A nice thing of the circom language is that you can split a <== into two independent actions: <-- and ===
240
241The <-- and --> operators assign a value to a signal without creating any constraints.
242
243The === operator adds a constraint without assigning any value to any signal.
244
245The circuit also has another problem: the operation works in Zr, so we need to guarantee the multiplication does not overflow. This can be done by converting the inputs to binary and checking the ranges, but we will reserve it for future tutorials.
246
247## Where to go from here:
248
249You may want to read the [README](https://github.com/iden3/circom)  to learn more features about circom.
250
251You can also check a library with many basic circuits lib binarizations, comparators, eddsa, hashes, merkle trees etc [here](https://github.com/iden3/circomlib) (Work in progress).
252
253
254Or a exponentiation in the Baby Jub curve [here](https://github.com/iden3/circomlib) (Work in progress).
255
256
257# Final note
258
259There is nothing worse for a dev than working with a buggy compiler.  This is a very early stage of the compiler, so there are many bugs and lots of work needs to be done. Please have it present if you are doing anything serious with it.
260
261And please contact us for any isue you have. In general, a github issue with a small piece of code with the bug is very useful to us.
262
263Enjoy zero knowledge proving!