# #5 Circom: Witness, Proof generation and Verification

## Recap: Signal operators

* <mark style="color:red;">`===`</mark> : used to constraint two signals
* <mark style="color:red;">`←—`</mark> : used to assign a value to a signal
* <mark style="color:red;">`<==`</mark> : assign and constraint (combines the above two operators)

#### Example

```jsx
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;  

}
```

* <mark style="color:red;">`x <-- a + 3`</mark> : `x` is **assigned** the value of input signal `a` incremented by 3.
* <mark style="color:red;">`x === a + 3`</mark> : `x` is **constrained** against the value of input signal `a` incremented by 3.
* <mark style="color:red;">`y <== a + 3`</mark> : `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 <mark style="color:red;">`<==`</mark> with intermediate signals

In the previous article, we use a combination of <mark style="color:red;">`<--`</mark> and <mark style="color:red;">`===`</mark> to introduce our intermediate signal `prod`. We could have simply used a single <mark style="color:red;">`<==`</mark> operator:

```jsx
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 <mark style="color:red;">`<==`</mark> operator does two operations under the hood:

1. assign <mark style="color:red;">`prod`</mark> the value of <mark style="color:red;">`a * b`</mark>,
2. constraint <mark style="color:red;">`prod`</mark> against said value.

The question we left the reader with was: \
‘*Why constraint <mark style="color:red;">`prod === a * b`</mark>?  Why is assignment alone insufficient?*’. <br>

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:

```jsx
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:

1. Witness generation
2. Low-level representation of constraints

<figure><img src="/files/TBt0sphmJGYw2947DZJ2" alt="" width="517"><figcaption></figcaption></figure>

### **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&#x20;**<mark style="color:red;">**`<--`**</mark>**&#x20;.**

### **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

<figure><img src="/files/QrMgpjXmZlNdlgbdiFH8" alt="" width="563"><figcaption></figcaption></figure>

* 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:**

1. Supply the prover with tailored witness values, to generate a valid proof
2. 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** <mark style="color:red;">`prod`</mark>?

Why is <mark style="color:red;">`prod <== a * b`</mark> necessary, and <mark style="color:red;">`prod <-- a * b`</mark> insufficient?

Using only <mark style="color:red;">`<--`</mark> 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:

<figure><img src="/files/ZEHRacOhKenTUOEPg6DG" alt="" width="524"><figcaption></figcaption></figure>

* Witness generation remains unchanged
* System of constraints changes; <mark style="color:red;">`prod === a * b`</mark> 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 <mark style="color:red;">`prod`</mark> to be supplied together with the other witness values,
* prover will not check that <mark style="color:red;">`prod`</mark> honours the relationship <mark style="color:red;">`prod = a * b;`</mark>
* prove will only generate a proof based on <mark style="color:red;">`res === prod * c;`</mark>
* verifier will only check that proofs honour the constraint <mark style="color:red;">`res === prod * c;`</mark>

In short, the circuit only verifies that <mark style="color:red;">`res === prod * c`</mark>. 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&#x20;**<mark style="color:red;">**`<==`**</mark>**&#x20;when assigning to intermediate signals**

* using only <mark style="color:red;">`<--`</mark> with intermediate signals is dangerous, because there is no constraint that ‘protects’ the assignment.
* hence, the common use of <mark style="color:red;">`<==`</mark> in circuit definitions.

That leaves us with a final question; when should we be using <mark style="color:red;">`<--`</mark> all by its lonesome?

## When to use assignment operator: <mark style="color:red;">`<—-`</mark>

Let’s say you want to verify that you know some values x1, x2, x3, x4, out, such that, <mark style="color:red;">`out = [(x1 + x2) / x3] - x4`</mark>. 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:

```rust
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 <mark style="color:red;">`y2 = y1 / x3`</mark> as a constraint in Circom

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

<mark style="color:red;">`y2 = y1 / x3`</mark> is expressed in two parts:

* <mark style="color:red;">`y2 <-- y1 / x3;`</mark>
* <mark style="color:red;">`y1 === y2 * x3;`</mark>

At this point, you should have gotten a good understanding of using <mark style="color:red;">`<==`</mark> and <mark style="color:red;">`<--`</mark> . \
Other common places you will notice and be expected to use <mark style="color:red;">`<==`</mark> is with **components** and **output signals.**

Output signals (<mark style="color:red;">`signal output out`</mark>) 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 <mark style="color:red;">`<--`</mark> alone, without constraining the intermediate signal.

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

```jsx
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`**

<figure><img src="/files/3IWi414Ed4i4NM0Tfetj" alt=""><figcaption></figcaption></figure>

```jsx
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

{% code title="inputs.json" %}

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

{% endcode %}

* 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:

```jsx
[
 "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

<figure><img src="/files/PoLr5niclPfInUf2NAU1" alt=""><figcaption></figcaption></figure>

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](https://docs.circom.io/circom-language/circom-insight/simplification/) for more info.

**Generate the witness**

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

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

* run: <mark style="color:red;">`node generate_witness.js **negative**.wasm inputs.json witness.wtns`</mark>
* export to json: <mark style="color:red;">`snarkjs wtns export json witness.wtns`</mark>
* <mark style="color:red;">`cat witness.json`</mark>, should output:

```jsx
[
 "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 <mark style="color:red;">`res = prod * c`</mark>, the values of <mark style="color:red;">`a`</mark> and <mark style="color:red;">`b`</mark> do not matter.

To that end, we will create a malicious witness by altering <mark style="color:red;">`witness.wtns`</mark>.

While it would be preferable to alter <mark style="color:red;">`witness.json`</mark> to produce the required <mark style="color:red;">`witness.wtns`</mark>, 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:**

```jsx
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:**

<figure><img src="/files/1jqc5iUqrwW9ls9c2xyo" alt=""><figcaption></figcaption></figure>

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

<figure><img src="/files/dgjK5z6WiTLwTwmBfpQH" alt=""><figcaption></figcaption></figure>

#### 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:

{% code title="edit.js" %}

```jsx
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}`);
}
```

{% endcode %}

The After output should be like so:

<figure><img src="/files/9xMehNgLkvGHlzzFtaoS" alt=""><figcaption></figcaption></figure>

Observe that only signals `a`, `b` are modified; the rest remain unchanged.

**Verify&#x20;**<mark style="color:red;">**`exploit_witness.wtns`**</mark>**&#x20;against the circuit:**

* <mark style="color:red;">`snarkjs wtns check negative.r1cs exploit_witness.wtns`</mark>

<figure><img src="/files/Q1edxAGSxLUNcx26mEn6" alt=""><figcaption></figcaption></figure>

This indicates that the exploit witness will be accepted, even though <mark style="color:red;">`prod`</mark> is not the resulting product of <mark style="color:red;">`a`</mark> and <mark style="color:red;">`b`</mark>.

This should be instructive in educating the reader the importance of assigning and constraining (<mark style="color:red;">`<==`</mark>) intermediate variables.


---

# Agent Instructions: Querying This Documentation

If you need additional information that is not directly available in this page, you can query the documentation dynamically by asking a question.

Perform an HTTP GET request on the current page URL with the `ask` query parameter:

```
GET https://calnix.gitbook.io/zk-notes/circom/5-circom-witness-proof-generation-and-verification.md?ask=<question>
```

The question should be specific, self-contained, and written in natural language.
The response will contain a direct answer to the question and relevant excerpts and sources from the documentation.

Use this mechanism when the answer is not explicitly present in the current page, you need clarification or additional context, or you want to retrieve related documentation sections.