# Assigned but not Constrained

{% hint style="info" %}
[**Book an audit with Zokyo**](https://www.zokyo.io/)
{% endhint %}

A very common bug and misunderstanding is the difference between assignments and constraints. For zk circuits, constraints are the mathematical equations that must be satisfied by any given inputs for a proof to be valid. If any of the inputs result in one of the constraint equations to be incorrect, a valid proof is not possible (well, extremely unlikely).

Assignments, on the other hand, simply assign a value to a variable during proof generation. Assignments do not have to be followed for a valid proof to be created. Often times, an assignment can be used, in combination with other constraints, to reduce the total number of constraints used.

Constraints actually add equations to the R1CS file whereas assignments do not.

**Circom Case and Example**

A great example that highlights the difference between assignment and constraint is the `IsZero` circom circuit:

```
pragma circom 2.0.0;

template IsZero() {
    signal input in;
    signal output out;
    signal inv;
    inv <-- in!=0 ? 1/in : 0;
    out <== -in*inv +1;
    in*out === 0;
}

component main {public [in]}= IsZero();
```

In circom, the `<--`, `-->` and `=` operators are assignments, whereas the `<==`, `==>`, and `===` operators are constraints. So, `inv` is assigned `1/in` if `in` is not `0` and is assigned `0` otherwise. This is not a constraint - a prover can assign whatever they want to `inv` as long as it satisfies the constraints. We will see, however, that even if the prover inputs values other than the expected assignment for `inv`, `IsZero` will still be constrained to output `1` if `in == 0` and `0` otherwise.

There are 2 cases to consider, `in` is zero and `in` is nonzero. If `in` is zero, then the first constraint `out <== -in*inv + 1` forces `out == 1`, and the second constraint `in*out === 0` is satisfied. So the circuit acts as expected, no matter what the prover inputs for `inv`. For the case that `in != 0`, then by the second constraint, `out` must be `0`. Therefore the first constraint must force that `-in*inv + 1 == 0`, and so `in*inv == 1`. This effectively constrains `inv` to equal the inverse of `in` as expected. Even though `inv` is assigned at will by the prover, the added constraints force it to actually be the inverse of `in` when `in != 0`. The circuit acts as expected for both cases of `in == 0` and when `in != 0`.

A good question is why don't we remove the first constraint and simplify the code to the following:

```
template IsZero() {
    signal in;
    signal out;
    signal temp;
    temp <-- in!= 0 ? 0 : 1;
    out === temp;
}
```

The problem here is that `temp` is assigned to `in != 0 ? 0 : 1` and not actually constrained. So a trustworthy prover will always run this code and generate successful proofs, but a malicious prover can alter the code to assign anything to `temp`. A malicious prover could copy this circuit and change the `temp` assignment to `temp <-- 1;` so that the circuit always outputs `1`. Their proofs generated from their slightly changed code would successfully pass a verifier built from this example circuit. We need the `out <== -in*temp +1;` constraint to ensure that `temp` is actually the inverse of `in`.

Another good question is why don't we constrain instead of assign: `inv <== in!=0 ? 1/in : 0;`. This is because circom does not support the automatic constraint of a ternary operator. It adds more than one constraint behind the scenes which affects performance. For example, the [Mux1](https://github.com/iden3/circomlib/blob/master/circuits/mux1.circom) circuit is often used in place of the ternary operator, but it adds more than one constraint. So the authors of the `IsZero` circuit have found a creative way to reduce the constraint count.

**Halo2 Case**

This type of bug can easily happen with Halo2 circuits as well - maybe even more likely because assigning is done separately from constraints. In Halo2, often times the constraints are created in a `configure` function, while the assignments are done in an `assign` function. It is easy for developers to see that the circuit is satisfied because the `assign` function correctly gives the desired inputs. However, if the `configure` function is missing a constraint, a malicious prover can fork the code and change the `assign` function to target the missing constraint.

A good example of this bug is from the SHL and SHR opcode circuit for the PSE zkEVM. The opcode circuit takes as input a `shift` variable and a `shf0` variable:

```
let shift = cb.query_word_rlc();
let shf0 = cb.query_cell();
```

Shf0 is assumed to be the first byte of the `shift` variable. There are later constraints added on `shf0` instead of `shift` because it is cheaper constraint-wise to only consider the first byte. However, there was a missing constraint forcing `shf0` to be the first byte of `shift`. It is easy to miss this because `shf0` and `shift` are properly assigned in the assign function:

```
let shf0 = pop1.to_le_bytes()[0];
self.shift.assign(region, offset, Some(pop1.to_le_bytes()))?;
```

The fix was to add a constraint forcing `shf0` to equal the first byte of `shift`.

**Preventative Techniques**

To prevent these types of bugs, it is important to understand the ins and outs of whatever coding language was used to create the circuits. That way one can quickly identify what's constrained and what's assigned. Additionally, it is extremely important to go over each constraint in detail to ensure that the system is constrained to the exact expected behavior. Do not consider assignments when doing this, only the constraints. A great way to ensure your constraints are sufficient is through [formal verification](https://en.wikipedia.org/wiki/Formal_verification). Some tools are currently in the process that will help enable quick formal verification for circom and halo2 circuits.

**References**

1. [Circom Documentation](https://docs.circom.io/circom-language/signals/)
2. [CircomLib IsZero Circuit](https://github.com/iden3/circomlib/blob/cff5ab6288b55ef23602221694a6a38a0239dcc0/circuits/comparators.circom#L24-L34)
3. [PSE zkEVM Shf0 Bug](https://github.com/privacy-scaling-explorations/zkevm-circuits/issues/1124)

This repo was inspired by a few other github repos that also document common vulnerabilities (but for solidity) -

* [(Not So) Smart Contracts](https://github.com/crytic/not-so-smart-contracts)
* [Solidity Security Blog](https://github.com/sigp/solidity-security-blog)
* [List of Security Vulnerabilities](https://github.com/runtimeverification/verified-smart-contracts/wiki/List-of-Security-Vulnerabilities)


---

# 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://zokyo-auditing-tutorials.gitbook.io/zokyo-tutorials/tutorial-16-zero-knowledge-zk/common-vulnerabilities-in-zk-code/assigned-but-not-constrained.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.