#5 Circom: Witness, Proof generation and Verification

Recap: Signal operators

=== : used to constraint two signals
←— : used to assign a value to a signal
<== : assign and constraint (combines the above two operators)

Example

template Main() {
  // inputs 
  signal input a;
  signal input b;
 
  // intermediate 
  signal x;
  signal y;

	// assignments
  x <-- a + 3;

	// constraints
  a === b;
  x === a + 3;
  y <== a + 3;  

}

x <-- a + 3 : x is assigned the value of input signal a incremented by 3.
x === a + 3 : x is constrained against the value of input signal a incremented by 3.
y <== a + 3 : y is assigned & constrained against the value of input signal a incremented by 3.

Essentially, the two operations with x can be simplified to one operation as seen with y.

Use `<==` with intermediate signals

In the previous article, we use a combination of <-- and === to introduce our intermediate signal prod. We could have simply used a single <== operator:

template Mul3() {
		// input signals
		signal input a;
		signal input b;
		signal input c;
		signal input res;
		
		// intermediate signal: declaration
		signal prod;
		
		// quadratic constraints
		prod <== a * b;		
		 res === prod * c;
}

The <== operator does two operations under the hood:

assign prod the value of a * b,
constraint prod against said value.

The question we left the reader with was: ‘Why constraint prod === a * b? Why is assignment alone insufficient?’.

To answer this question we first explore what happens to circuits during and after compilation.

Witness, Proof generation and Verification

Let’s examine how a proof is generated and verified using the example above:

template Mul3() {
		// input signals
		signal input a;
		signal input b;
		signal input c;
		signal input res;
		
		// intermediate signal: declaration
		signal prod;
		
		// quadratic constraints
		prod <== a * b;		
		 res === prod * c;
}

The process of compiling this circuit creates a number of artifacts that are meant to help with:

Witness generation
Low-level representation of constraints

Witness generator

The artifacts pertaining to witness generation assists with calculating intermediate signals from the primary inputs (signal inputs).
This is helpful since the prover expects a witness as input. Meaning to say, we are expected to supply the intermediate signal values as well.

Hence, we see that the witness generator accounts for operations involving <-- .

Low-level representation of constraints

This is to be fed into a zkSNARK generator like snarkjs, to generate a prover and verifier.
The prover component can be integrated with some web app, while the verifying component could be integrated into a smart contract or server.
~~Since the compiler places restrictions on how the~~ === ~~and~~ <== ~~can be used, the resulting system of constraints are of R1CS form.~~

Example illustration

The prover expects inputs values in-line with the dimensions of the witness vector; intermediate signals and all.
From this, it generates a proof.
The verifier serves to confirm if the proof provided to it is valid or not.

Consequently, an attacker has two channels of attack:

Supply the prover with tailored witness values, to generate a valid proof
Attack the verifier directly by supplying it with a tailored proof

Now let’s review and answer the original question in the next section.

Why assign and constraint `prod`?

Why is prod <== a * b necessary, and prod <-- a * b insufficient?

Using only <-- will leave the prover vulnerable to be exploited via tailored witness values. It will produce seemingly valid proofs without checking to ensure prod is constrained. Similarly, the verifier will accept these proofs.

Let us illustrate this:

Witness generation remains unchanged
System of constraints changes; prod === a * b is dropped

This means that when we feed the constraints generated on compilation to a zkSNARK generator, the generated prover and verifier will not ensure that prod is equivalent to a * b.

prover expects prod to be supplied together with the other witness values,
prover will not check that prod honours the relationship prod = a * b;
prove will only generate a proof based on res === prod * c;
verifier will only check that proofs honour the constraint res === prod * c;

In short, the circuit only verifies that res === prod * c. This is why it is crucial to assign and constraint intermediate signals. Else, the outcome is an under-constrained circuit.

Remember, while the compiler produces witness generator artifacts for our convenience, it does not mean an attacker must use it. An attacker could pass tailored values to the prover, especially if its under-constrained. We will illustrate this in the exercise section.

It is crucial to understand that we can pass any values we want to a prover. The prover will only check that those inputs honour defined constraints and generate a proof. The prover has no concept of witness generation.

Takeaway: use `<==` when assigning to intermediate signals

using only <-- with intermediate signals is dangerous, because there is no constraint that ‘protects’ the assignment.
hence, the common use of <== in circuit definitions.

That leaves us with a final question; when should we be using <-- all by its lonesome?

When to use assignment operator: `<—-`

Let’s say you want to verify that you know some values x1, x2, x3, x4, out, such that, out = [(x1 + x2) / x3] - x4. How would this circuit be constructed?

Since constraints must be constructed as quadratic expressions, we need to breakdown the equation into intermediate parts. Like so:

y1 = x1 + x2
y2 = y1 / x3
out = y2 - x4

This is how the circuit would look like:

template Main() {
    // input signals
    signal input x1;
    signal input x2;
    signal input x3;
    signal input x4;
    signal output out;

    // intermediate signals
    signal y1;
    signal y2;

    // calc. intermediate values 
    y2 <-- y1 / x3;

    // constraints can only have quadratic expressions
    // can only use + or * or -
    y1 <== x1 + x2;
    y1 === y2 * x3;
    out <== y2 - x4;
  
}

component main = Main();

division is non-quadratic; cannot be used in constraint definition.
cannot express the y2 = y1 / x3 as a constraint in Circom

Therefore, we compute the values of the intermediate signals separately, before defining the constraints.

y2 = y1 / x3 is expressed in two parts:

y2 <-- y1 / x3;
y1 === y2 * x3;

At this point, you should have gotten a good understanding of using <== and <-- . Other common places you will notice and be expected to use <== is with components and output signals.

Output signals (signal output out) would be new to the reader. We will cover this in the next article.

Exercise

This exercise will serve to illustrate the folly of using <-- alone, without constraining the intermediate signal.

In an empty directory create negative.circom, with the following code:

pragma circom 2.1.8;

template Mul3() {
		// input signals
		signal input a;
		signal input b;
		signal input c;
		signal input res;
		
		// intermediate signal: declaration
		signal prod;
		
		// quadratic constraints
		prod <-- a * b;		
		 res === prod * c;
}

component main = Mul3();

Compile the circuit

circom negative.circom --r1cs --sym --wasm
Sanity check on terminal output: non-linear constraints: 1

Examine the R1CS file

snarkjs r1cs print negative.r1cs

snarkJS: [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.prod ] * [ main.c ] - [ 21888242871839275222246405745257275088548364400416034343698204186575808495616main.res ] = 0

There is only 1 constraint in this circuit, which is correctly reflected on compilation and in the R1CS file.

Generate the witness

create inputs.json file in ./negative_js directory
values passed will be as below

inputs.json

{"a": "1","b": "2","c": "3", "res": "6"}

run: node generate_witness.js **negative**.wasm inputs.json witness.wtns
export to json: snarkjs wtns export json witness.wtns
cat witness.json should output:

[
 "1",    // 1
 "3",    // c
 "6",    // res
 "2"     // prod
]

The reader will observe in the layout of the witness, that intermediate signals are included, and come after input signals.

However, the first two input signals, a and b have been omitted. This is because they are not involved in any constraint definition, and therefore have no place in the witness vector.

Verify witness.wtns against the circuit: snarkjs wtns check negative.r1cs witness.wtns

this checks that the witness produced honors the systems of constraints
think of this as a proxy means to check if a computed witness would create a valid proof

The witness clears. Now let’s see how to create a tailored witness that would be accepted just the same.

Exploiting the circuit

First we re-compile our circuit with the following command: circom negative.circom --r1cs --sym --wasm --O0

We add the --O0 flag, to instruct the compiler to avoid simplifying the circuit on compilation. This will surface both a and b in the witness. See constraint simplification for more info.

Generate the witness

create inputs.json file in ./negative_js directory
values passed will be as below

{"a": "1","b": "2","c": "3", "res": "6"}

run: node generate_witness.js **negative**.wasm inputs.json witness.wtns
export to json: snarkjs wtns export json witness.wtns
cat witness.json, should output:

[
 "1",    // 1
 "1",    // **a**
 "2",    // **b**
 "3",    // c
 "6",    // res
 "2"     // prod
]

Input signals a and b are now present in the witness. This is the consequence of using the --O0 flag.

Creating an exploit witness

We are going to show that as long res = prod * c, the values of a and b do not matter.

To that end, we will create a malicious witness by altering witness.wtns.

While it would be preferable to alter witness.json to produce the required witness.wtns, neither Circom nor snarkjs have the necessary APIs. Hence, the following grease-monkey approach.

Create view.js in the same directory as witness.wtns with the following code:

const fs = require('fs');
const path = require('path');

const witnessPath = path.join(__dirname, 'witness.wtns');

try {
    const witness = fs.readFileSync(witnessPath);
    
    let data_arr = new Uint8Array(witness);
    console.dir(data_arr, {'maxArrayLength': null});
  
} catch (error) {

    console.error(`Error reading witness file: ${error.message}`);
}

Running view.js will give us the following output in terminal:

Observe that the values of our witness are laid out in the same sequential order as witness.json.

Modify witness values

Overwrite witness.wtns where the values for signals a, b are stored, with arbitrary values.
Create edit.js file in the same directory:

edit.js

const fs = require('fs');
const path = require('path');

// Use path.join to create a full path to the witness.wtns file
const witnessPath = path.join(__dirname, 'witness.wtns');

try {
    const witness = fs.readFileSync(witnessPath);
    
    let data_arr = new Uint8Array(witness);

    console.log("Before");
    console.dir(data_arr, {'maxArrayLength': null});

    data_arr[108] = 42;  // `a`
    data_arr[140] = 69;  // `b`

    console.log("After");
    console.dir(data_arr, {'maxArrayLength': null});
		
    // create exploit witness 
    const exploitWitnessPath = path.join(__dirname, 'exploit_witness.wtns');
    fs.writeFileSync(exploitWitnessPath, data_arr);

} catch (error) {

    console.error(`Error reading witness file: ${error.message}`);
}