#1 Circom: Introduction

Introduction

In the ZK Book, we explored the conceptual workings of arithmetic circuits. Now, we’ll use Circom to create these circuits, translating R1CS constraints into Circom code. The reader is expected to have understood concepts within the ZK book.

Installing Circom: https://docs.circom.io/getting-started/installation/#installing-dependencies

Example 1

Assume we are trying to create ZK proofs to assess if someone knows the product of two arbitrary numbers: c = a * b

Put another way, for some a and b, we are looking to verify that the user has computed the correct value for c.

Programmatically speaking:

def someVerification(a, b, c):
		res = a * b 
		assert res == c, "invalid calculation"

Consequently, our R1CS system of constraints would comprise of only 1 constraint, like so:

assert c  == a * b

This is how it would look like in Circom:

template SomeCircuit() {
		// inputs
		signal input a;
		signal input b;
		signal input c;
		
		// constraints 
		c  === a * b;
}

component main = SomeCircuit();

Given inputs a, b, c, the circuit verifies that a * b is indeed equal to c.
The circuit serves to verify, not compute, hence the outcome of the operation (c) is a required input.
The === operator serves to define the constraint as previously expressed in R1CS form.
=== behaves like an assertion, so the circuit will not be satisfied if an invalid inputs are supplied.

`template` , `component` , `main`

Templates define a blueprint for circuits, like a class defines the structure for objects in OOP (Object Oriented Programming).
A component is an instantiation of a template, similar to how an object is an instance of a class in OOP.

// create template
template SomeCircuit() {
	
	// .... stuff
}

// instantiate template 
component main = SomeCircuit();

component main = SomeCircuit(), is needed because Circom requires a single top-level component, main, to define the circuit structure that will be compiled.

`signal input`

Signal inputs are values that will be provided from outside the component.
There are immutable and cannot be altered.

By declaring a signal, you're defining an interface for your component that specifies what data it expects to receive.

The finite field of Circom

Circom performs arithmetic in an finite field with an order of 21888242871839275222246405745257275088548364400416034343698204186575808495617, which we will simply call p.

The following should be obvious to the reader:

p under mod p is congruent to 0;
p-1 is the largest integer under mod p

This is important to note, as passing values that are larger than p-1, will result in overflow.

Example 2

Let’s look at a final example to conclude this article.

Consider a circuit that verifies values passed to it are binary, i.e.: 0 or 1.

Given the inputs are x and y, the R1CS system of constraints would be:

(1):  x * (x - 1) = 0
(2):  y * (y - 1) = 0

Recall that R1CS constraints requires that each constraint to have only 1 multiplication operation.

Why x * (x - 1)

*x * (x - 1) = 0 → x(x - 1) = 0*

There are only 2 roots for this polynomial expression, which happen to be real.
I.e., x = 0 or x = 1.

Expressed in Circom

template IsBinary() {
	
		signal input x;
		signal input y;
		
		x * (x - 1) === 0;
		y * (y - 1) === 0;
}

component main = IsBinary();

Alternative expression: using arrays

It is more conventional in Circom to group all the inputs into an array of signals called in. Following convention, we will represent the earlier circuit, like so:

template IsBinary() {

		// array of 2 input signals
		signal input in[2];
		
		in[0] * (in[0] - 1) === 0;
		in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

Arrays are zero-indexed as you would normally expect

In the next article we will cover loops, variables and template parameters.

Exercise

This section introduces common Circom commands. We assume the reader has already installed Circom and required dependencies.

In an empty directory, create a file called SomeCircuit.circom. Copy the code below into the file:

pragma circom 2.1.8;

template SomeCircuit() {
		// inputs
		signal input a;
		signal input b;
		signal input c;
		
		// constraints 
		c  === a * b;
}

component main = SomeCircuit();

This is a simple circuit with only 1 constraint.

1. Compiling circuits

In terminal execute the following command to compile:

circom **somecircuit**.circom --r1cs --sym --wasm
interchange the name of circuit to be compiled as needed

This is the expected output:

Observe that non-linear constraints are listed as 1, indicative of a * b === c

The compiler creates the following:

somecircuit.r1cs file
somecircuit.sym file
somecircuit_js directory

.r1cs file

Circuit's R1CS system of constraints in binary format.
Can be used with different tool stacks to construct proving/verifying statements (e.g. snarkjs, libsnark)

To read the R1CS file, you'll need a SNARK generator like snarkjs. Running cat somecircuit.r1cs will output gibberish.

Running snarkjs r1cs print somecircuit.r1cs, we get the following human-readable output:

[INFO]  snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.a ] * [ main.b ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.c ] = 0

In Circom, arithmetic operations are conducted within a finite field, so 21888242871839275222246405745257275088548364400416034343698204186575808495616 is actually representative of -1.

We can confirm this by checking -1 mod p, on Wolfram: https://www.wolframalpha.com/input?i=-1+mod+21888242871839275222246405745257275088548364400416034343698204186575808495617, where p is the order of Circom’s finite field.

Hence, we can simplify the output to:

[-1 * main.a] * [main.b] - [-1 * main.c] = 0

    [-main.a] * [main.b] - [-main.c] = 0
   
     [main.a] * [main.b] + [-main.c] = 0
    
     **[main.a] * [main.b] = [main.c]**

Again, observe that this matches with the constraint(a * b === c) described in SomeCircuit.circom.

.sym file

The somecircuit.sym file generated is a symbols file required for debugging and printing the constraint system in an annotated mode.

somecircuit_js directory

somecircuit_js directory contains artifacts for witness generation:

somecircuit.wasm
generate_witness.js
witness_calculator.js

By supplying input values for the circuit, these artifacts will calculate the necessary intermediate values and create a witness that can be submitted to a prover.

This is helpful in complex circuits, where there are few independent signals and many dependent ones, saving us from manually calculating all downstream values.

2. Calculating the witness

We start by providing the values for which the witness has to be generated. We do this by creating inputs.json file in the somecircuit_js directory.

Say we want to create a witness for input values a=1, b=2, c=2. The json file would be like so:

inputs.json

{"a": "1","b": "2","c": "2"}

Circom expects strings instead of numbers because JavaScript does not work accurately with integers larger than 253.

Run this command in somecircuit_js directory: node generate_witness.js **somecircuit**.wasm inputs.json witness.wtns.

outputs the computed witness as file witness.wtns.

If we had passed values that did not honor the constraint, a*b === c, e.g. a=1, b=2, c=3, witness_calculator.js would throw an error.

Examine computed witness: `witness.wtns`

If you run cat witness.wtns, the output is gibberish.

This is because witness.wtns is a binary file in a format accepted by snarkjs.

To get the human-readable form, we export it to json via: snarkjs wtns export json witness.wtns

snarkjs ingests witness.wtns file to output witness.json.
first 1 is the constant portion of the witness, which is always 1.
we have that a = 1, b = 2, and c = 2 since our input json was {"a": "1","b": "2","c": "2"}.
computed witness adheres to the R1CS layout of the witness vector: [1, a, b, c]

The reader might wonder why we are missing out, (which typically follows 1 in R1CS form), recall that while the witness vector always begins with 1, out is not mandatory.

Example: IsBinary.circom

Let’s run though a less trivial example, using IsBinary.circom. The form of the constraints should be familiar to the reader given the explanation offered in example 2.

template IsBinary() {

		// array of 2 input signals
		signal input in[2];
		
		in[0] * (in[0] - 1) === 0;
		in[1] * (in[1] - 1) === 0;
}

// instantiate template 
component main = IsBinary();

Compile circuit

circom isbinary.circom --r1cs --sym --wasm
Sanity check on terminal output: non-linear constraints: 2

This makes sense, as our circuit contains two assertions that contain a multiplication of signals.

Next we examine the R1CS file: snarkjs r1cs print isbinary.r1cs

[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[INFO]  snarkJS: [ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

Notice that this large number is slightly different from the -1 mod p coefficient highlighted earlier
I.e.:21888242871839275222246405745257275088548364400416034343698204186575808495616
- Observe the additional digit, 1 at the end
- 21888242871839275222246405745257275088548364400416034343698204186575808495616
- 218882428718392752222464057452572750885483644004160343436982041865758084956161
The reason there is a 1 at the end is due to a flaw in how snarkjs formats the output. It is “trying” to say -1 * 1 but has no space between them.

The correct way to interpret it is as follows:

[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[0] ] * [ main.in[0] ] - [  ] = 0
[ 218882428718392752222464057452572750885483644004160343436982041865758084956161 +main.in[1] ] * [ main.in[1] ] - [  ] = 0

[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (21888242871839275222246405745257275088548364400416034343698204186575808495616)1 +main.in[1] ] * [ main.in[1] ] = 0

[ (-1)1 +main.in[0] ] * [ main.in[0] ] = 0
[ (-1)1 +main.in[1] ] * [ main.in[1] ] = 0

[ main.in[0] - 1] * [ main.in[0] ] = 0
[ main.in[1] - 1] * [ main.in[1] ] = 0

Visually, the output looks like a single number. However, it ought to be treated as the negative coefficient to 1.

Generate the witness

create inputs.json file in ./isbinary_js directory
we will opt to pass values in[0] = 1, in[1] = 0

{"in": ["1","0"]}

Generate witness.wtns: node generate_witness.js isbinary.wasm inputs.json witness.wtns
Now that witness.wtns has been created, export it to json, so we can examine it: snarkjs wtns export json witness.wtns
We would get the following as output, on executing cat witness.json:

[
 "1",  // 1
 "1",  // in[0] 
 "0"   // in[1] 
]

The computed signal match the R1CS layout of the witness vector: [1, in[0], in[1]], as do their respective values.

PreviousFinal - Proving key, Verifier Key Next#2 Circom: Template parameters, Variables, Loops

Last updated 3 months ago

Was this helpful?