Why circom IsZero needs in*out === 0: `<--` is not a constraint, so out can be forged

Question that trips up circom beginners: in circomlib's IsZero, why is the third line needed?

signal inv;
inv <-- in != 0 ? 1/in : 0;   // witness computation only
out <== -in*inv + 1;          // constraint
in*out === 0;                 // constraint

Answer: <-- emits *no constraint*. It only tells the witness generator how to compute a value; a malicious prover can supply any inv they like. So when reasoning about soundness, mentally delete every <-- line and look at what remains. Without in*out === 0, the only constraint is out === -in*inv + 1, which a prover satisfies with in = 1, inv = -1, out = 2. The circuit then "proves" that a nonzero input is zero-ish, and any downstream logic gated on out is broken. That is an under-constrained circuit — the classic circom vulnerability class.

in*out === 0 closes the hole: if in != 0 it forces out == 0, and combined with the first constraint that pins inv to 1/in.

Practical heuristics: - Read circuits twice: once as witness generation, once as constraints only. Only the second reading is what the proof enforces. - Every intermediate signal introduced typically needs one additional constraint to be pinned down. IsZero adds a third signal (inv), hence needs a second constraint. - out * (out - 1) === 0 is not needed here because the two existing constraints already determine out uniquely; adding it costs a constraint without buying soundness.

Removing constraints reduces proving cost but the thing you lose is *soundness*, not completeness — a prover can then prove false statements.

Source: adapted from a Stack Exchange answer by 0xSanson (question by kitakita), https://ethereum.stackexchange.com/questions/167316/how-to-determine-if-a-constraint-in-a-circom-circuit-is-necessary — CC BY-SA 4.0