On this page
A Circom circuit is two programs pretending to be one. The first computes a witness: given the inputs, here are the values of every signal. The second is a set of constraints: polynomial equations the witness must satisfy for a proof to verify. The compiler emits both from the same source, and the arrow you use decides which one a line lands in.
<-- assigns. It tells the witness generator how to compute a value and says nothing to the verifier. <== assigns and constrains: the same computation, plus an equation the proof must satisfy. === constrains without assigning.
An attacker does not run your witness generator. They write their own, fill in whatever values they like, and hand the verifier a proof. The verifier checks the constraints and nothing else. So the whole question of circuit soundness is: for every signal, is the value the honest witness would compute the only value the constraints allow? Every place the answer is “no” is a place the prover gets to choose, and a prover who gets to choose will choose whatever breaks you.
Reading a circuit for soundness means reading it the way the verifier does: ignore every <--, and ask what the equations alone pin down.
The arrow that does nothing
The textbook case is a helper that computes something the constraint system cannot express directly, then forgets to add the constraint that makes the computation honest.
template IsZero() {
signal input in;
signal output out;
signal inv;
inv <-- in != 0 ? 1 / in : 0;
out <== -in * inv + 1;
}Division is not a field operation you can write as a constraint, so inv is assigned with <--. That is fine on its own; the point of <-- is to compute things the constraints will then check. The line that makes this template sound is the one the snippet is missing:
in * out === 0;Without it, read the constraints alone. There is exactly one: out = 1 - in·inv. The prover controls inv. For any non-zero in they can set inv = 0 and get out = 1, claiming a non-zero input is zero. Or set inv to make out any value they like. The witness generator would never do that, but the witness generator is not what the verifier trusts.
With the second constraint, in · out = 0 forces out = 0 whenever in ≠ 0, and out = 1 - in·inv with in = 0 forces out = 1. Two equations, one valid witness. This is the shape of nearly every under-constrained bug: a <-- whose “and now check it” line was never written, or was written for a special case and not the general one.
The reading habit: every <-- needs a partner === (or a later <== that consumes the value in a way that pins it). Find each <--, then find the constraint that would fail if the prover lied about that signal. If you cannot point at it, it does not exist.
Outputs nobody constrained
The second family is an output that is computed but not related to the inputs by any constraint. The template looks complete because every signal is assigned.
template Sum(n) {
signal input a[n];
signal output total;
var acc = 0;
for (var i = 0; i < n; i++) {
acc += a[i];
}
total <-- acc;
}total is assigned with <--. The constraints say nothing about it. A proof for this template proves that the prover knows some inputs, and then asserts an arbitrary total. Change the arrow to <== and the accumulated linear expression becomes a constraint; this one is a one-character fix.
The subtler version is an output constrained to something, but not to the inputs. total <== total_hint where total_hint is itself a <-- value is still unconstrained; the constraint is real but it pins the output to another free variable. Follow the chain until it reaches an input, a constant, or a constrained signal. If it reaches a <-- first, the output is free.
Range checks that are not there
Field arithmetic wraps. Signals live in a prime field of roughly 254 bits, and a signal that you think of as “a byte” or “a balance” is only that if a constraint says so.
template Withdraw() {
signal input balance;
signal input amount;
signal output remaining;
remaining <== balance - amount;
}The constraint is sound as an equation; remaining is exactly balance - amount in the field. The bug is that amount > balance does not fail. It wraps, and remaining becomes a number just under the field modulus, which the calling circuit will happily treat as a very large balance. The fix is a range check on remaining (and usually on amount): decompose into bits, constrain each bit to be 0 or 1, and constrain the bits to sum back to the value. Circom’s standard library has Num2Bits for exactly this. The reading habit: every comparison or subtraction on a value you think of as bounded needs a constraint that actually bounds it. LessThan without a preceding range check on its inputs is the same bug wearing a different name.
Components that are wired to nothing
Larger circuits compose templates as components, and the wiring is where a surprising number of real bugs live.
template Check() {
signal input x;
signal output ok;
component isz = IsZero();
isz.in <== x;
ok <-- isz.out;
}The component is instantiated and its input is constrained. Its output is read with <--, so the ok this template exposes is not constrained to be the component’s out. The prover sets ok freely; the perfectly sound IsZero inside was never connected to anything the verifier checks. A component whose output feeds nothing through a constraint contributes no constraints to the proof about the outside world, however good it is internally.
There is a related mistake that reads as its opposite. A component instantiated and never wired at all (component c = Foo(); with no c.in <==) adds Foo’s internal constraints to the system with free inputs, which is dead weight at best and, if Foo’s outputs are read, a free variable at worst. Both show up as a port that no constraint touches.
What tools can and cannot see
Static analysis is good at exactly the reading described here: it walks each signal, classifies each arrow, and asks whether the constraint graph connects the signal to an output through equations rather than through assignments. Sigvex’s under-constrained-signal detector does that walk per component port, which matters: a template with two independent halves has two outputs, and “the signal reaches an output” is only meaningful if it reaches the right one.
What it cannot do is tell you whether the constraints you did write mean what you intended. in * out === 0 is an equation; whether it is the right equation for IsZero is a question about your specification, and no tool has your specification. The reading habit is the same in both cases, though. Cover every <-- with your hand, read what is left, and ask what a prover who hates you would put in the blanks.