GitHub

A succinct reference to correctly constraining circuits

Table of Contents

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

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.

Example

# with UnusedSignalMultiplier as main
❯ mkdir target
❯ circom --inspect circuits/multiplier.circom -o target
warning[CA01]: In template "UnusedSignalMultiplier()": Local signal unused does not appear in any constraint
# with UnderconstrainedMultiplier2 as main
warning[T3002]: Consider using <== instead of <-- to add the corresponding constraint.
 The constraint representing the assignment satisfies the R1CS format and can be added to the constraint system.
   ┌─ "circuits/multiplier.circom":45:5
   │
45 │     c <-- intermediary;
   │     ^^^^^^^^^^^^^^^^^^ found here
   │
   = call trace:
     ->UnderconstrainedMultiplier2
warning[CA01]: In template "UnderconstrainedMultiplier2()": Local signal c does not appear in any constraint
# with UnderconstrainedMultiplier1 as main
warning[T3002]: Consider using <== instead of <-- to add the corresponding constraint.
 The constraint representing the assignment satisfies the R1CS format and can be added to the constraint system.
   ┌─ "circuits/multiplier.circom":33:5
   │
33 │     intermediary <-- a * b;
   │     ^^^^^^^^^^^^^^^^^^^^^^ found here
   │
   = call trace:
     ->UnderconstrainedMultiplier1
warning[CA01]: In template "UnderconstrainedMultiplier1()": Local signal a does not appear in any constraint

circomspect 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 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 are inessential for using the tool.

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:

❯ circomspect circuits/multiplier.circom
circomspect: analyzing template 'Multiplier'
circomspect: analyzing template 'OverconstrainedMultiplier'
circomspect: analyzing template 'UnderconstrainedMultiplier1'
warning: Using the signal assignment operator `<--` is not necessary here.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:33:5
   │
33 │     intermediary <-- a * b;
   │     ^^^^^^^^^^^^^^^^^^^^^^ The expression assigned to `intermediary` is quadratic.
   │
   = Consider rewriting the statement using the constraint assignment operator `<==`.
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#unnecessary-signal-assignment.
warning: Intermediate signals should typically occur in at least two separate constraints.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:31:5
   │
31 │     signal intermediary;
   │     ^^^^^^^^^^^^^^^^^^^ The intermediate signal `intermediary` is declared here.
   ·
34 │     c <== intermediary;
   │     ------------------ The intermediate signal `intermediary` is constrained here.
   │
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#under-constrained-signal.
circomspect: analyzing template 'UnderconstrainedMultiplier2'
warning: Using the signal assignment operator `<--` is not necessary here.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:45:5
   │
45 │     c <-- intermediary;
   │     ^^^^^^^^^^^^^^^^^^ The expression assigned to `c` is quadratic.
   │
   = Consider rewriting the statement using the constraint assignment operator `<==`.
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#unnecessary-signal-assignment.
warning: The signal `c` is not constrained by the template.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:41:5
   │
41 │     signal output c;
   │     ^^^^^^^^^^^^^^^ This signal does not occur in a constraint.
warning: Intermediate signals should typically occur in at least two separate constraints.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:42:5
   │
42 │     signal intermediary;
   │     ^^^^^^^^^^^^^^^^^^^ The intermediate signal `intermediary` is declared here.
43 │
44 │     intermediary <== a * b;
   │     ---------------------- The intermediate signal `intermediary` is constrained here.
   │
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#under-constrained-signal.
circomspect: analyzing template 'UnusedSignalMultiplier'
warning: The signal `unused` is not used by the template.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:54:5
   │
54 │     signal unused;
   │     ^^^^^^^^^^^^^ This signal is unused and could be removed.
   │
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#unused-variable-or-parameter.
warning: Intermediate signals should typically occur in at least two separate constraints.
   ┌─ /home/thor/tmp/circom-correctly-constrained/circuits/multiplier.circom:54:5
   │
54 │     signal unused;
   │     ^^^^^^^^^^^^^ The intermediate signal `unused` is declared here.
   │
   = For more details, see https://github.com/trailofbits/circomspect/blob/main/doc/analysis_passes.md#under-constrained-signal.
circomspect: 7 issues found.

circomkit circom testing suite

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 for circuits, though this seems inelegant as provided, and seems really only designed for one-off soundness checks.

See the short circomkit usage example in this repo for a demonstration of circomkit, or circomkit-examples for further examples.

Not recommended

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).

zksecurity circomscribe - demo playground, visualize constraints

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.

(- 1 * Multiplier.a )*(Multiplier.b ) = - 1 * Multiplier.intermediary
- 1 * Multiplier.c + Multiplier.intermediary = 0
(- 1 * OverconstrainedMultiplier.a )*(OverconstrainedMultiplier.b ) = - 1 * OverconstrainedMultiplier.intermediary
- 1 * OverconstrainedMultiplier.c + OverconstrainedMultiplier.intermediary = 0
- 1 * UnderconstrainedMultiplier1.c + UnderconstrainedMultiplier1.intermediary = 0
(- 1 * UnderconstrainedMultiplier2.a )*(UnderconstrainedMultiplier2.b ) = - 1 * UnderconstrainedMultiplier2.intermediary

Circomscribe's announcement blog post briefly introduces the tool.

Picus QED uniqueness property underconstraint checker

Picus is a tool by Veridise for checking under-constrained signals of circuits. I couldn't install Picus (in a half hour of trying). The docker build script fails for me with error:

ERROR: failed to solve: process "/bin/bash -c raco make picus.rkt" did not complete successfully: failed to create endpoint m4k1rddek6olk2zpiynatvsz5 on network bridge: failed to add the host (veth7b01635) <=> sandbox (veth4ac65fd) pair interfaces: operation not supported

I tried a few things including restarting my Docker daemon, then attempting a build from scratch by installing z3 and cvc5, but these took too long, so I'm moving on after leaving an issue. Just kidding, they disabled issues for their repo, big oof.

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.

Backlog list of further tools to examine

Everything you should know about correctly assigning constraints

The basics

Circom allows the developer to specify constraints in two ways:

// 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(aaa == b)

so we may express higher degree constraints as such:

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.

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.

Circom docs example 1: avoid unnecessary constraints on intermediate calculations

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 signalout 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 inis 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

Read the original on github.com ↗