Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

doc: annotated guide to correctly constraining and optimizing circom #2

Merged
merged 4 commits into from
Oct 2, 2024
Merged

doc: annotated guide to correctly constraining and optimizing circom #2

Changes from all commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
058ee33
doc: notes on circom constraint basics and <-- operator
thor314 Oct 1, 2024
c43a1bb
notes on further resources added
thor314 Oct 1, 2024
f99557a
polish
thor314 Oct 1, 2024
73af2c7
polish
thor314 Oct 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
201 changes: 173 additions & 28 deletions README.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,31 +2,21 @@
A succinct reference to correctly constraining circuits
</h1>

<!-- <div align="center"> -->
<!-- <a href="https://github.com/pluto/circom-correctly-constrained/graphs/contributors"> -->
<!-- <img src="https://img.shields.io/github/contributors/pluto/circom-correctly-constrained?style=flat-square&logo=github&logoColor=8b949e&labelColor=282f3b&color=32c955" alt="Contributors" /> -->
<!-- </a> -->
<!-- <a href="https://github.com/pluto/circom-correctly-constrained/actions/workflows/circom.yaml"> -->
<!-- <img src="https://img.shields.io/badge/tests-passing-32c955?style=flat-square&logo=github-actions&logoColor=8b949e&labelColor=282f3b" alt="Tests" /> -->
<!-- </a> -->
<!-- <a href="https://github.com/pluto/circom-correctly-constrained/actions/workflows/lint.yaml"> -->
<!-- <img src="https://img.shields.io/badge/lint-passing-32c955?style=flat-square&logo=github-actions&logoColor=8b949e&labelColor=282f3b" alt="Lint" /> -->
<!-- </a> -->
<!-- </div> -->

## Overview
This repo is a reference on correctly testing and constraining circom circuits, with example workflows and reference patterns.

TLDR: use `circom --inspect $circuit_path` and `circomspect $circuit_path` for automated circuit underconstraint static analysis, and `circomkit` for testing.

Skim down to "Everything you should know..." for a primer for circom authors on constraining and optimizing circuits.

## Recommended Tools

### [circom docs: --inspect option](https://docs.circom.io/circom-language/code-quality/inspect/)
The circom compiler has an option to look for underconstrained templates and unused signals. It requires little setup, beyond specifying a main component.

The linked documentation is one of the better guides I've seen on how to guide the compiler how to properly constrain circuits, or else tell the compiler that a signal is unimportant to constrain.

Usage:
#### Example
```sh
# with UnusedSignalMultiplier as main
❯ mkdir target
Expand Down Expand Up @@ -61,19 +51,21 @@ warning[CA01]: In template "UnderconstrainedMultiplier1()": Local signal a does
```

### [circomspect static analyzer and linter for circom](https://github.com/trailofbits/circomspect)
`circomspect` is a static analyzer and linter for Circom.
`circomspect` is a static analyzer and linter for Circom, similar to `circom --inspect`, but with a greater area of checks, and more verbose error logs.

- install: `cargo install circomspect`
- run: `circomspect $CIRCUIT_PATH`
- e.g.: `circomspect circuits/multiplier.circom`. `circomspect` will flag underconstrained templates, but will not flag the overconstrained circuit.

`circomspect` seems powerful and straightforward to use, requiring very little extra context for the developer to use the tool.
`circomspect` is powerful and straightforward to use, requiring very little extra context for the developer to use the tool.

More about `circomspect` by Trail of Bits, in a few blog posts. These blog posts briefly describe the tool and a few of the passes performed by `circomspect`. They are summaries of the `circomspect` in context, but not important for using the tool.
More about `circomspect` by Trail of Bits, in a few blog posts. These blog posts briefly describe the tool and a few of the passes performed by `circomspect`. They are summaries of the `circomspect` in context, but are inessential for using the tool.
- [ToB blog: it pays to be circomspect](https://blog.trailofbits.com/2022/09/15/it-pays-to-be-circomspect/)
- [ToB blog: circomspect has more passes](https://blog.trailofbits.com/2023/03/21/circomspect-static-analyzer-circom-more-passes/)

It would be good if there were CI to run circomspect, but that does not currently seem to be available. There is no fast way to install circomspect, so it would be slightly costly to run in CI today.

#### Example
Circomspect produces the following output on `multiplier.circom`:
```sh
❯ circomspect circuits/multiplier.circom
Expand Down Expand Up @@ -149,7 +141,7 @@ circomspect: 7 issues found.
```

### [circomkit circom testing suite](https://github.com/erhant/circomkit)
A typescript-based suite of testing tools for circom. The circomkit readme does a better job of summarizing the tool than I could here.
A typescript-based suite of testing tools for circom. The circomkit README does a better job of summarizing the tool than I could here.

Circomkit theoretically could be used to [test passing and failing witnesses](https://github.com/erhant/circomkit?tab=readme-ov-file#witness-tester) for circuits, though this seems inelegant as provided, and seems really only designed for one-off soundness checks.

Expand All @@ -159,12 +151,12 @@ See the [short circomkit usage example in this repo](https://github.com/pluto/ci
The following tools were examined and found eclipsed in utility by other tools (circomscribe), failed to build (picus), or exceedingly complex to understand [(circom-mutator)](https://github.com/aviggiano/circom-mutator).

### [zksecurity circomscribe - demo playground, visualize constraints ](https://www.circomscribe.dev/)
Circomscribe is the circom compiler, run in WASM in the browser in an online playground tool. The tool emits information about the circom compilation process. This is a clunky workflow, copy pasting code into a browser.
Circomscribe is the circom compiler, run in WASM in the browser in an online playground tool. The tool emits information about the circom compilation process. This is a clunky workflow, pasting code into a browser.

The main context where this tool could be useful would be to see explicitly what constraints are produced by circom snippet, which could be useful for obtaining greater granularity of depth. This tool would be annoying to use if the template had more than one or two dependency templates.

Run on each of the multipliers in `circuits/multiplier.circom`, Circomscribe produces the following outputs. Note that the underconstrained circuits each only have 1 line of constraint rather than 2.
```ts
Run on each of the multipliers in `circuits/multiplier.circom`, Circomscribe produces the following outputs. Note that the underconstrained circuits each only have 1 line of constraint, rather than 2.
```sh
(- 1 * Multiplier.a )*(Multiplier.b ) = - 1 * Multiplier.intermediary
- 1 * Multiplier.c + Multiplier.intermediary = 0

Expand All @@ -189,14 +181,167 @@ I tried a few things including restarting my Docker daemon, then attempting a bu

It could be worthwhile to come back and try to get this tool to work, but it's hard to say whether the tool is actually user-ready.

## more reading about underconstrained circuits
- [circom constraining docs](https://docs.circom.io/circom-language/constraint-generation/)
- [veridise blog: circom pairing](https://medium.com/veridise/circom-pairing-a-million-dollar-zk-bug-caught-early-c5624b278f25)
- [dacian: exploiting under-constrained zk circuits](https://dacian.me/exploiting-under-constrained-zk-circuits)
- [blockdev: tips for safe circom circuits](https://hackmd.io/@blockdev/Bk_-jRkXa)
- [circom101 book by erhant, author of circomkit](https://github.com/erhant/circom101/tree/main)
- [0xparc: circom workshop series](https://learn.0xparc.org/materials/circom/learning-group-1/intro-zkp)
- [paper by veridise on underconstrained circuits](https://eprint.iacr.org/2023/512.pdf)
### Backlog list of further tools to examine
- [Ecne - an engine for verifying R1CS soundness](https://github.com/franklynwang/EcneProject)

## Everything you should know about correctly assigning constraints

### The basics
Circom allows the developer to specify constraints in two ways:
```rust
// 1. equality constraint operators: ===, <==, ==>
signal_b <== signal_or_var_a;
// the above line is equivalent to the following two lines:
signal_b <-- signal_or_var_a; // assigns, but does not constrain
signal_b === signal_or_var_a;

// 2. the assert keyword
// if all values are known at compile-time the assertion is checked then
// otherwise, the assertion creates a constraint.
assert(a <= b);
assert(a * a == b);
```

Recall that, due to the construction of the R1CS circuit layout, Circom cannot express greater-than-quadratic constraints:
- this is fine: `assert(a*a == b)`
- this is a cubic constraint (no go): `assert(a*a*a == b)

so we may express higher degree constraints as such:
```rust
a2 <== a*a;
a2*a === b; // equivalently, assert(a2*a == b);
```

### When may a developer choose to use `<--` assignment over `<==`?
> assigning a value to a signal using <-- and --> is considered dangerous and should, in general, be combined with adding constraints with \=\=\=, which describe by means of constraints which the assigned values are.
> https://docs.circom.io/circom-language/constraint-generation/

As stated in the circom docs, generally avoid using `<--`, at least until an optimization code pass. The operator may save a few gates, but risks underconstraining the circuit. A developer may incorrectly use `<--` to allow assignment for would-be non-quadratic assignments; this is a [footgun](https://en.wiktionary.org/wiki/footgun).

Use of `<--` allows the developer to reason extra constraints out of their circuits, thereby improving proving times. When optimizing code with `<--`, use tools like `circom --inspect` (which searches the codebase for `<--` that can be transformed into `<==`) and `circomspect` to check for correctly constrained circuits.

Documentation as to how to correctly use `<--` is sparse, but as best as this author can infer, there are essentially two reasons to use assignment without assertion:
1. **avoid unnecessary constraints on intermediate calculations**
2. **defer constraint checks to a final value assertion**
3. **check a more general constraint**

Two examples applying `<--` are given in the [circom documentation](https://docs.circom.io/circom-language/basic-operators/#examples-using-operators-from-the-circom-library).

#### Circom docs example 1: avoid unnecessary constraints on intermediate calculations
```rust
pragma circom 2.0.0;

template IsZero() {
signal input in;
signal output out;
signal inv;
// avoid unnecessary constraint on intermediate signal inv
// recall: / is multiplication by the inverse modulo p
inv <-- in!=0 ? 1/in : 0;
out <== -in*inv +1;
in*out === 0;
}
component main {public [in]}= IsZero();
```

> This template checks if the input signal `in` is `0`. In case it is, the value of output signal`out` is `1`. `0`, otherwise. Note here that we use the intermediate signal `inv` to compute the inverse of the value of `in` or `0` if it does not exist. If `in`is 0, then `in*inv` is 0, and the value of `out` is `1`. Otherwise, `in*inv` is always `1`, then `out` is `0`.

That is, this template computes the function:
$$\text{out} =\cases{1 &\text{if in = 0}\\ 0 & \text{if in $\ne$ 0 }}$$
Which can be expressed in two constraints; assigning a value to `out` from the value of `in`, and checking that the value assigned matches the function described above.

The value of `inv` is an intermediate calculation, and does not require a constraint.

#### Circom docs example 2: check a more general constraint, and defer constraint checks
```rust
pragma circom 2.0.0;

template Num2Bits(n) {
signal input in;
signal output out[n];
var lc1=0;
var e2=1;
for (var i = 0; i<n; i++) {
// check a more general constraint than assignment
// namely that out[i] is binary
out[i] <-- (in >> i) & 1;
out[i] * (out[i] -1 ) === 0;

lc1 += out[i] * e2;
e2 = e2+e2;
}
// deferred constraint check of out
// checks the value assignments of out, as lc1 is computed from out
lc1 === in;
}
component main {public [in]}= Num2Bits(3);
```

> This templates returns a n-dimensional array with the value of `in` in binary. Line 7 uses the right shift `>>` and operator `&` to obtain at each iteration the `i` component of the array. Finally, line 12 adds the constraint `lc1 = in` to guarantee that the conversion is well done.

That is, the constraints for this template can be specified more succinctly than simply checking for assignment. The circomlib implementation checks that:
- `out[i]` is binary (this could be stated even more succinctly with the `binary` tag in circom 2.1.0)
- `out`'s assignments are accumulated in var `lc1`, which is value-checked at template's end.

#### Example 3: further examples
```rust
template QuadraticIntermediate() {
// Intermediate calculations
signal input x;
signal output y; // = x*x+x+1
signal squareX;

squareX <-- x * x;
y <== squareX + x + 1; // includes check that x*x == squareX
}

// By comparison, this template DOES require an intermediate constraint
// to avoid enforcing non-linear constraints.
template CubicIntermediate() {
signal input x;
signal output y; // = x*x*x + x + 1
signal sqX;

// sqX <-- x * x; // leads to non-linear constraint in final line
sqX <== x * x;
y <== sqX * x + x + 1;
}

template IsEven() {
signal input bigNumber;
signal output isEven;
signal remainder;

// assign the intermediate value without constraint:
remainder <-- bigNumber % 2;
// enforce the constraint we actually want to check:
isEven <== 1 - remainder;
}
```

### Common mistakes in underconstraining circuits
I was originally going to close with a section on common oversights in underconstrained circuits, but other resources have already done this well. I direct the reader toward the [0xPARC ZK bug tracker](https://github.com/0xPARC/zk-bug-tracker) in particular, an index of zk bugs in discovered in the wild, and a list of common oversights in constraining circuits, and Erhant's [circom101 book](https://circom.erhant.me/), which provides further examples of optimized and constrained circuits.

## Further Reading
The following resources may provide further direction in writing correctly constrained Circom.

### Recommended short reading
- [0xPARC ZK bug tracker](https://github.com/0xPARC/zk-bug-tracker) - a list of bugs and exploits found in zk applications. The list of [common vulnerabilities](https://github.com/0xPARC/zk-bug-tracker?tab=readme-ov-file#common-vulnerabilities-1) is particularly worth reviewing.
- [Circom constraint generation docs](https://docs.circom.io/circom-language/constraint-generation/) - an introduction to how constraints are generated; overlaps with the *basics* section given above.
- [Circom Anonymous Component documentation](https://docs.circom.io/circom-language/anonymous-components-and-tuples) - Circom 2.1.0 introduced anonymous components. While not directly related to circuit constraints, anonymous components allow for significantly more concise and expressive syntax in declaring components, reducing risk of developer error (i.e. the developer may incur less brain damage from writing Circom, the author recommends this)

### Recommended longer reading
- [circom101 book by erhant, author of circomkit](https://circom.erhant.me/) - Erhant's book is good supplementary material for the circom documentation, and details the implementation of several optimized circom templates.
- [0xPARC: circom workshop series](https://learn.0xparc.org/materials/circom/learning-group-1/intro-zkp) - a series of videos on zero knowledge generally, and circom in particular

### Also reviewed in preparation for this post
To save the reader some time in exploring resources, these posts were reviewed in preparation for this post and are briefly summarized for completeness, but are not recommended reading.

- [dacian: exploiting under-constrained zk circuits](https://dacian.me/exploiting-under-constrained-zk-circuits) - a walkthrough of correctly constraining a circom template that a value is not prime. Examples provided for:
- asserting inputs values are not equal to one
- range checking for to prevent multiplication overflow
- [veridise blog: circom pairing](https://medium.com/veridise/circom-pairing-a-million-dollar-zk-bug-caught-early-c5624b278f25) - somewhat in the weeds audit by Veridise found a bug in the `circom-pairing` library. The bug involves somewhat in-the-weeds elliptic curve cryptography trivia; namely than the output of a custom comparator, `BigLessThan`, is unconstrained, allowing for inputs to `CoreVerifyPubkeyG1` to accept inputs larger than the curve prime `q`. I didn't take anything away from this post.
- [blockdev: tips for safe circom circuits](https://hackmd.io/@blockdev/Bk_-jRkXa) - a high level notes pass on circom circuits

## License

Expand Down