Circom

tl;dr: My current sense: circom is still in its early days. First, it lacks an ability to write correctness tests natively in its own language (as opposed to JavaScript testing frameworks). Second, it gives no mechanism for developers to ascertain soundness of their templates. (In its defense, the only such mechanism is a formal verification framework.) Third, it has not been designed for safety (e.g., weird comparison semantics; a lack of types, at least initially; no testing framework in its own language).

Gotchas

• Cannot test correctness of your circom code without special tools like circom_tester or circom_kit
  • e.g., does my witness generation logic produce a satisfying assignment?
• Impossible to test soundness of your circom code
  • e.g., does this malicious assignment pass my constraints?
  • just try and write such a test for the IsZero template
• Comparison operators (<, >, >=, <=) on var’s treat $\Zp$ values as signed.
  • This will daze and confuse you, at best.
  • At worst, it’ll cause soundness issues.
• Cannot declare a constant (e.g., var MAX_LEN = 32;) and then declare an array of that size (e.g., var array[MAX_LEN];)
• Cannot out-of-the-box test that $\ell$ bits “fit” into a $\Zp$ field element, where $p$ is circom’s chosen prime
  • Even worse, you may not even understand why it’s often necessary to ensure this!
  • This can create soundness issues (e.g., the LessThan template in circomlib is hardcoded for BN254’s prime $p$, but what if the chosen $p$ is much smaller?)
  • Fortunately, there are ways to do it manually.
• The LessThan(N) template is not (always) sound when its inputs are >N bits: beware and read this!
• circomlib doesn’t use safety features like tags or buses

Notes

As put by Palladino¹:

The main challenges [in] Circom is understanding when you are writing constraint-generation code, and when you are writing witness-generation code, and tracking what values are known at compile-time versus only known at runtime. […] Keeping in mind the difference between constraint and witness generation times can guard you against underconstrained computation bugs.

Terminology

• witness generation: computation of hints a.k.a. “witness data” that aids in satisfying the constraints encoded in a circom template
  • can be sped up with parallel keyword
• variables
  • circom docs say: “variables are identifiers that hold non-signal data and are mutable.”
  • but, a more accurate mental model, AFAICT, is that they are compile-time symbolic expressions (e.g., often they are used to symbolically-store a linear combination of signals at compile time; see the Num2Bits example)
• functions: reusable pieces of code used only during witness generation
• signals
  • input signals; i.e.,:
    • part of the NP relation’s statement or witness
    • you cannot do s <== expression for signal input s; only for signal s.
  • output signals
  • intermediate signals (computed via witness generation)
• template: a family of circuits, parameterized by one or more values known at compile-time (think C++ templates)
  • template parameters
• components
  • anonymous components
• assignment
• constraints

Operators

Source here.

• a \ b computes the $\lfloor a / b\rfloor$ division quotient as if dividing natural numbers (i.e., s.t. $a=b q + r$ and $0 \le r < b$, when viewed as natural numbers)
• a % b similarly computes the remainder $r$
• all other binary operators perform arithmetic modulo the R1CS prime $p$, as one would expect, except for the comparison operators, as already mentioned in the gotcha’s above

Signals

Input signals versus output signals.

Marking a signal in a template as input or output defines a “function-like” interface for the template.

This allows for a nicer calling syntax that avoids explicitly instantiating a template via the component keyword. (See anonymous components in the circom docs.)

The main component

An example:

pragma circom 2.0.0;

template Multiplier2() {
   signal input in1;
   signal input in2;
   signal output out <== in1 * in2;
}

component main { public [in1, in2] } = Multiplier2();

As emphasized in the circom docs: “all output signals of the main component are public (and cannot be made private)”.

In contrast, “the input signals of the main component are private if not stated otherwise using the keyword public as above”

Variables: var versus signal

Initially, var seemed like it was just a “compile-time derivable linear combination of signals” (including the trivial one like var = some_signal; or var = SomeTemplateCall(N)(in);).

A good example of this is in the Num2Bits template.

But you can also put (compile-time) constants or any other compile-time expression.

Most importantly, in circom, compile-time constants/values stored in var’s are stored as $\Z_p$ scalar field elements! So if you add or multiply too much, you will “wrap around”: e.g., $p/2 + p/2 = p = 0$.

Comparison operators (<, >, >=, <=) on var’s

Even more importantly, circom treats these $\Zp$ values inside vars as signed integers when doing comparisons! This will trip you up!

• Everything in $v\in [0, p/2]$ is treated as positive; so, as expected, its actual value is $\bar{v} = v \in [0,p/2]$.
• But: everything in $v\in [p/2 + 1, p)$ is treated as negative, which is unexpected: its actual value, from the point of view of the comparison operator, is $\bar{v} = v - p \in [-(p/2 - 1), -1])$.

See here for details.

Witness generation versus constraints

Find a more natural circuit that showcases this difference. Not IsZero().

As explained by Palladino¹:

When writing a circuit you’re writing two different programs, that belong to two different programming paradigms, in a single one.

The most important thing to know: when (not) to use <--.

Tags

Tags seem very useful for safety. An article by Hess² explains them well. Unfortunately, nobody seems to use them.

e.g., the output signal out of the IsZero template could be tagged as binary to indicate that the returned output is either 0 or 1.

I found Circom’s docs confusing because they make it seem like binary is a language-reserved tag with this actual meaning. (e.g., “This tag means that each signal in the array is always expected to be 0 or 1, in order to compute the corresponding number correctly.”) But it is not: there are no “reserved” circom tags.

The code below would propagate the binary tag to the a signal:

signal a <=== IsZero()(10);

Tags can have compile-time values:

“Valued tags behave like parameters which means that they can only be assigned to values known at compilation time.”

e.g., a template’s compile time parameter can be used to tag its output signal’s max bit length:

template Bits2Num(n) {
    signal input {binary} in[n];
    signal output {maxbit} out;
    var num = 0;

    var pow_2 = 1;
    for (var i = 0; i < n; i++) {
        num += in[i] * pow_2;
        pow_2 = pow2 + pow_2;
    }
    out.maxbit = n;

    num ==> out;
}

This suggests max lengths of strings could be tags.

Buses

Very useful for readable, maintainable code. And therefore, for safety. See here.

Buses, combined with tags should offer a decent amount of type-safety in circom. (Yet nobody seems to use buses either.)

For example, an elliptic curve point can be represented as:

bus Point() {
    signal x;
    signal y;
}

You can even tag buses: e.g., an Edwards Point() vs. a Montgomery one! So, you can have templates that work like this:

template Edwards2Montgomery () {
  input  Point() { edwards_point    } in;
  output Point() { montgomery_point } out;

  out.x <–- (1 + in.y) / (1 - in.y);
  out.y <–- out.x / in.x;

  out.x * (1 - in.y) === (1 + in.y);
  out.y * in.x === out.x;
}

Or, you can even tag signals in buses:

bus Book () {
  signal {maxvalue} title[50];
  signal {maxvalue} author[50];
  signal {maxvalue} sold_copies;
  signal {maxvalue} year;
};

Buses can be nested (but not recursed):

bus Date() {
    signal day;
    signal month;
    signal year;
}

bus Person() {
    signal name[50];
    Date() birthday;
}

Buses can be parameterized by compile-time constants:

bus Vector(N) {
    signal v[N];
}

bus Matrix(NUM_ROWS, NUM_COLS) {
	Vector(NUM_ROWS) column[NUM_COLS];
}

Assert

The assert keyword is particularly “interesting.” I think I’m gonna stay away from it.

Quoting from here, it is supposed to add constraints:

// 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);

But I don’t think that’s true, from looking at the circom docs and from here or here: it does not add constraints.

Non-trivial examples

IsZero() template

This is a template that outputs 1 when the input signal is 0 and outputs 0 otherwise.

It should be the most trivial thing to implement, no? Yet it turns out that, while checking whether something is zero is trivial (i.e., something === 0), assigning a signal with the truth value of something === 0 is not as trivial… (This is because the only operations in circom are equality checks, addition and multiplication.)

This example will also illustrate the difference between witness generation versus constraining.

template IsZero() {
  signal input in;
  signal output out;
  signal inv;

  inv <-- in != 0 ? 1/in : 0;   // W1 (witgen one)

  out <== -in * inv + 1;  // C1 (constraint one)
  in * out === 0;         // C2 (constraint two)
}

How does it work? Here’s a simple analysis:

• When in is 0, then:
  • out <== -in * inv + 1 (C1) implies out <== 0 * inv + 1.
  • Which implies out <== 1, ensuring the desired behaviour.
  • Q: But then inv does not even matter for this case? Which is why it is assigned 0? But why 0? It could be assigned anything it seems.
• When in is not 0, then:
  • in * out === 0 (C2) implies out === 0.
  • As a result, out <== -in * inv + 1 (C1) implies 0 <== -in * inv + 1
  • Which implies in * inv === 1
  • Which can be satisfied, since the witness generation can compute an inverse via the inv <-- in != 0 ? 1/in : 0 line.

Observation: I find the explanation in circom’s docs a bit confusing, perhaps even in a dangerous way. It says: “If in is 0, then […]. Otherwise, in * inv is always 1, then out is 0.” This could be interpreted to suggest that circom enforces that inv be correctly computed as the inverse of in. Which is not the case. It’s not that circom guarantees in * inv will be always 1; it’s that when in is not zero, the only way to satisfy the C1 and C2 constraints is to correctly compute the correct inverse inv of in (via the witness generation code at W1)

In a way, this rather-elegant IsZero() template perfectly illustrates how non-intuitive circom can be when it comes to efficiently-programming ZK relations.

Num2Bits(N) template

Let’s also consider the Num2Bits() example from circom’s docs, which returns the $n$-bit binary representation of its input.

This example illustrates:

• template parameters (e.g., n)
• variables versus signals
• witness generation versus constraining

template Num2Bits(N) {
    signal input num;
    signal output {binary} bits[N];

    // Asserts that 2^N - 1 fits in a scalar
    _ = assert_bits_fit_scalar(N);

    // incrementally-updated to eventually store the symbolic expression:
    //
    //   bits[0] * 1 + bits[1] * 2 + bits[2] * 2^2 + ... + bits[N-1] * (2^(N-1))
    //
    var acc = 0;

    // stores increasing powers of two: 2^0, 2^1, 2^2, ...
    var pow2 = 1;

    for (var i = 0; i < N; i++) {
        bits[i] <-- (num >> i) & 1;    // extracts `num`'s ith bit
        bits[i] * (bits[i] - 1) === 0; // constrains bits[i] to be a bit

        // appends `+ bits[i] * 2^i` as a term to the symbolic expression in
        // `acc`, setting it to \prod_{i = 0}^{N-1} bits[i] * 2^{i+1}
        acc += bits[i] * pow2;

        // set to 2^{i+1}
        pow2 = pow2 + pow2;
    }

    // since acc stores the symbolic expression from above, this constrains
    // that the `bits` are indeed the binary representation of `num`
    num === acc;
}

It was actually ChatGPT who helped me understand that acc merely stores a symbolic expression that is derivable at compile-time (see here), because circom docs, IMHO, do a poor job at clarifying the distinction between circom signals and circom variables.

LessThan(N) template

The LessThan(N) implementation here is the same as in circom, except for a few things. It takes its inputs as two separate inputs signals lhs and rhs, as opposed to an array in[2] containing both. It leverages tags. It properly asserts that $2^{N+1}$ fits in a scalar via assert_bits_fit_scalar (defined later).

/**
 * Outputs a truth bit for whether lhs < rhs when viewed as N-bit
 * *unsigned* integers.
 *
 * @preconditions
 *
 * @input   lhs    the left-hand side input < 2^N
 * @input   rhs    the right-hand side input < 2^N
 *
 * @output  out {binary}    a bit indicating whether lhs < rhs when viewed as integers
 *
 * @notes
 *   The old LessThan(N) template was (unfortunately) hard-coded for the scalar field
 *   of BN254, where scalars are \le (p - 1) and where 2^253 < p < 2^254.
 *
 *   The choice of N <= 252 ensures that the maximum value assigned to `bits`
 *   below is (2^N - 1) + 2^N = 2^{N+1} - 1 = 2^253 - 1, and thus does not
 *   exceed p-1.
 *
 *   (If N were <= 253, then this maximum value would have been 2^254 - 1
 *    which would be larger than p-1 and would thus not fit in a signal.)
 */
template LessThan(N) {
    signal input lhs;
    signal input rhs;

    // We have to make sure 1 << N (which is N+1 bits wide) fits in the scalar 
    // field. Otherwise, we lose soundness.
    _ = assert_bits_fit_scalar(N+1);

    // (N+1)-bit representation of m = lhs + 1 << N - rhs
    //                               = lhs + 2^N    - rhs
    //                               <= (2^N - 1) + 2^N - 0 <= 2^{N+1} - 1
    // e.g., for N = 3
    //  lhs   = 100
    //        >
    //  rhs   = 001
    //  m     = lhs + 1 << N - rhs
    //        = 100 + 1000   - 001
    //        = 1100 - 001
    //        = 1011
    //        = *___
    //
    // e.g., flipping over
    //  lhs   = 001
    //        <
    //  rhs   = 100
    //  m     = lhs + 1 << N - rhs
    //        = 001 + 1000   - 100
    //        = 1001 - 100
    //        = 0101
    //        = *___
    signal {binary} bits[N + 1] <== Num2Bits(N + 1)(lhs + (1 << N) - rhs);

    // if lhs < rhs, then:
    //   bits[N], the N'th bit toggled above by adding 2^N, becomes 0 => assign 1 to `out`
    // else:
    //   bits[N], the N'th bit toggled above by adding 2^N, remains 1 => assign 0 to `out`
    //
    signal output {binary} out <== 1 - bits[N];

    // Mark remaining signals as intentionally-unused & avoid unnecessary compiler warnings
    for(var i = 0; i < N; i++) {
        _ <== bits[i];
    }
}

Never use LessThan for range checks

The LessThan template is often insecurely used for range checks. e.g., developers write code like this to ensure that an input is $(N-1)$ bits wide:

signal is_in_range <== LessThan(N)(x, 2**(N-1));
is_in_range === 1;

Unfortunately, this is completely broken³. A malicious prover can feed in: \begin{align} x = p - 2^{N-1} \end{align} where $p$ is the circom scalar field order.

You can see why this fails by running those values through the code. We start with: \begin{align} \mathsf{lhs} &= p - 2^{N-1}\\
\mathsf{rhs} &= 2^{N-1} \end{align} Therefore, \begin{align} \mathsf{bits} &= \mathsf{lhs} + (1 \ll N) - \mathsf{rhs} \bmod p\\
&= (p - 2^{N-1}) + 2^N - 2^{N-1} \bmod p\\
&= 2^N + (p - 2^{N-1}) - 2^{N-1} \bmod p\\
&= 2^N + p - 2\cdot 2^{N-1} \bmod p\\
&= 2^N + p - 2^N \bmod p\\
&= 2^N - 2^N \bmod p\\
&= 0 \bmod p \end{align} Recall that LessThan(N) takes bits[N], flips it and returns it as the output signal. So, in this case, it would incorrectly output 1.

The fix? If you want to do $(N-1)$-bit range checks, use _ <== Num2Bits(N-1)(x). But, if you don’t know what you’re doing, use my variant of Num2Bits, which enforces that 2^{N-1} “fits” in the field. Otherwise, circomlib has aliasing issues⁴. (Don’t even get me started.)

This kind of attack has been described before, but only at a high-level.

Apparently, LessThan was designed with signed-integer semantics in mind, just like the comparison operators. In this sense, the attack from above is not considered problematic by many folks. In theory… In practice, I think most circom developers are not aware of the intended semantics, since those semantics are not even documented in circomlib. Furthermore, even though circom has security features like tags and buses that could prevent developers from misusing LessThan, those features are unfortunately not (yet) leveraged in circomlib’s master branch. (There is a circomlib2 branch that uses tags though; although I doubt most devs know about it.)

DivRem() template

It’s surprisingly tricky to implement a basic “division with remainder” in circom because emulating integer division in a finite field is rife with dangers. For example:

Normally, for any $a,b\in \N$, Euclid’s division theorem says there exist unique $q,r\in\N$ s.t.: \begin{align} a = q\cdot b + r\\
0\le r < b \end{align}

Now, suppose we are implementing a circom template that checks $a,b,q,r$ for the properties above via:

a === b * q + r;
_ <== Num2Bits(M)(r);
is_valid_remainder <== LessThan(M)(r, b); // assume b < 2^M
is_valid_remainder === 1;

Are we good? Is this enough to guarantee uniqueness of $q$ and $r$?

Nope!

AFAICT, some online resources are wrong on this, suggesting that simply checking $r < b$ is enough.

If the field were $\F_{13}$, then dividing $a=10$ by $b=3$ we would have two solutions: \begin{align} q = 3 \wedge r = 1\Rightarrow (q \cdot b + r) \bmod {13} = (3\cdot 3 + 1) \bmod {13}= 10 \bmod {13} = a \end{align} But also: \begin{align} q = 7 \wedge r = 2\Rightarrow (q \cdot b + r) \bmod {13} = (7\cdot 3 + 2) \bmod {13} = 23 \bmod {13} = 10 \bmod {13} = a \end{align}

To fix this, we actually have to check that quotient $q$ is bounded too. There may be several ways of doing this, some more efficient than others.

Below, I describe an approach that, assuming $0\le a < 2^N$ and $0 < b < 2^M$ simply checks if $q < 2^N$. This guarantees soundness as long as $2^M(2^N + 1) \le p$, because:

• We know that $a < 2^N$ and $b < 2^M$.
• We will check that $a \equiv q b + r \pmod p$
• We will check that $0 \le r < b$
• We will check that $0 \le q < 2^N$
• We are good as long as $qb + r < p$ for all such $(b,q,r)$
  • i.e., the Euclidean division check mod $p$ from above will hold over the integers
• From above, we can bound $q b + r < 2^{N + M} + 2^M$
• So, as long as $2^{N + M} + 2^M \le p$, we are good
• Equivalently, as long as $2^M(2^N + 1) \le p$, we are good

The code below leverages tags. It also uses assert_bits_fit_scalar (defined later) and LessThan. To understand the code better, see it directly in circom-stdlib⁵.

template DivRem() {
    signal input {maxbits} a;
    signal input {nonzero, maxbits} b;
    signal output {maxbits} q <-- a \ b;    // maxbits enforced below
    signal output {maxbits} r <-- a % b;    // maxbits enforced below

    var N = a.maxbits;
    var M = b.maxbits;

    // We only need to test 2^M(2^N + 1) <= p, but no easy way to in circom.
    // Instead, we can test that a slighlty larger 2^{M + N + 1} < p.
    // We do lose the ability of using this with higher (N, M), but that's okay.
    _ = assert_bits_fit_scalar(N + M +1);

    // Check Euclidean division theorem, including r \in [0, b)
    a === q * b + r;
    
    // We can assume b < 2^M, because it is tagged.
    // But, for the remainder r, we have to enforce it:
    // (Of course, r may is a bit smaller than M bits, because r < b)
    r.maxbits = M;
    _ <== Num2Bits(M)(r);
    
    // We know that r, b < 2^M => can safely call LessThan(M)
    signal valid_remainder <== LessThan(M)(r, b);
    valid_remainder === 1;
    
    // Check that q is bounded, otherwise we are in trouble
    q.maxbits = N;
    _ <== Num2Bits(N)(q);
}

You can see an implementation of a related template that computes just the remainder $r$, when a bound on $a$ is known, here.

assert_bits_fit_scalar(N) compile-time check

circomlib templates often hardcode the maximum # of bits that can fit into a $\Zp$ scalar by assuming $p$ to be the order of the BN254 curve.

This is not just silly as it may break applications deployed for different curves with higher $p$.

But it is also insecure for applications deployed with smaller $p$ than what the circomlib template asserts (e.g., what if somebody develops for Goldilocks with $p \approx 2^{64}$?). If so, templates like Num2Bits would have serious soundness issues!

It would be better if we could check that any N-bit number “fits” in circom’s configured $\Zp$ scalar type.

We do this via assert_bits_fit_scalar(N) below, inspired by the maxbits() check in the costa-group fork of circomlib.

/**
 * Computes the maximum bit-width $b$ such that an *unsigned* $2^b - 1$ value can
 * be always stored in a circom scalar in $\mathbb{Z}_p$, without it wrapping around
 * after being reduced modulo $p$.
 *
 * Leverages the fact that circom comparison operators treat scalars in $[0, p/2]$
 * as positive, while every $v \in (p/2, p)$ is treated as negative (i.e., as 
 * $v - p$ instead of as $v$).
 */
function MAX_BITS() {
    var n = 1;
    var b = 1;

    while (2 * n > n) {
        n = n * 2;
        b = b + 1;
    }

    return b;
}

/**
 * Utility method used to make sure an N-bit *unsigned* number will fit in a scalar,
 * for the curently-selected circom scalar field.
 */
function assert_bits_fit_scalar(N) {
    var max_bits = MAX_BITS();
    log("N: ", N);
    log("MAX_BITS(): ", max_bits);

    assert(N <= max_bits);

    return 0; // circom needs you to return smth!
}

TODOs

Assert template parameters are not larger than field order

How do we assert non-overflows on variables like? What if they exceed the field size?

var MAX_QUOTIENT = (3 * MAX_ENCODED_LEN) \ 4;

CalculateTotal

Why do people add constraints to implement sums? Why don’t they just use a var? (e.g., here)

Conclusion

circom is an amazing tools for implementing ZK relations that (obviously) makes the developer’s job 10,000x easier than writing R1CS constraints directly.

I am still trying to understand the many pitfalls developers can fall into when writing circom code, most importantly, under-constraining bugs.

Looking forward to looking at NoirLang to see if it makes it easier to distinguish between constraints and witness generation?

Awesome list

Libraries

• iden3/circomlib, standard library from iden3
• costa-group/circomlib, a modified circomlib that leverages tags (see diffs)
• zkFHE/circomlib-fhe
• nullity00/circom-circuits
• Trees in circom
• ABDK libraries for circom

SoK

• zksecurity/zkbugs
• 0xPARC/zk-bug-tracker
• nullity00/zk-security-reviews
• pluto/circom-correctly-constrained
• Best Practices for Large circuits

Security list

Coda⁶

• Veridise/coda
• ZK DSL that allows developer to specify functional correctness theorems about the circuits they write
• Compiles to R1CS
• Somewhat-automated-but-not-fully: generates intermediate lemmas that have to be manually proved in Coq/Rocq

Unclear whether/how it handles witness generation.

Unclear how mature this is.

The --inspect option in circom itself

• Helps find (some?) underconstraining bugs
  • How? Unclear.
• Most important thing: marking unused signals via _ <== unused_signal to avoid false positives
• See example here
• See circom docs here

circomspect⁷

• Like circom --inspect above, but does more checks
• It’s called a “linter”, but does not seem to actually lint like cargo fmt would

zkFuzz

• zkFuzz

circomscribe⁸

• Allows you to paste in circom code and see what constraints are generated, in a developer friendly way.
• Likely does not scale to big circuits, due to cognitive overload.
• Available to use for free here.
• Does not seem to be open source

Ecne⁹

• Helps “verify that certain sets of R1CS constraints uniquely identify functions”
• Takes as input just the .r1cs file (e.g., see here)

A bit confusing: is Ecne trying to solve two problems at the same time? First, incorrect compilation from circom to R1CS. Second, identify missed constraints in circom by looking directly at the compiled R1CS? A bit awkward. Confusingly, its stated goal is “to make it easier to convert functions into R1CS form”, which presumably circom already solves?

Picus¹⁰

• Detects under-constraining bugs: i.e., “a circuit is underconstrained if the equations do not specify a function.”
  • Not sure how useful this is in reality.
  • While it seems very useful to know that a template is a function, it says nothing about it being the right function.
• It is open-source

Others

Exercises:

• ZK exercises

Testing frameworks:

• erhant/circomkit

Audits:

• zkEmail audit, by MatterLabs

References

For cited works and other resources¹¹$^,$¹²$^,$⁹$^,$¹³$^,$¹⁴, see below 👇👇