iden3 / circom

zkSnark circuit compiler
GNU General Public License v3.0
1.28k stars 244 forks source link

Question about constraints and expression order impact #183

Closed a6-dou closed 1 year ago

a6-dou commented 1 year ago

Does it matter if we write assignment expression first then constrain or doing the inverse?

In documentation at this line it's stated that:

Constraint generation can be combined with signal assignment with the operator <== with the signal to be assigned on the left hand side of the operator.

out <== 1 - a*b;

Which is equivalent to:

out === 1 – a*b;
out <-- 1 - a*b;

what's the difference between

out === 1 – a*b;
out <-- 1 - a*b;

and

out <-- 1 - a*b;
out === 1 – a*b;

making the calculation expression first before the checking the constraints is same doing the inverse? i believe both expressions and constraints are treated separately but just wanted to confirm if it's the same or not.

Thanks!

alrubio commented 1 year ago

Hi, in fact out <== 1 - a*b;

is equivalent to:

out <-- 1 - ab; out === 1 – ab;

although the second option generates and additional check in the witness generation code (wasm or C), because 1) the use of <== produces a contraint in the system and an assignment in the witness generation code 2) the use of <-- produces an assignment in the witness generation code 3) the use of === produces a contraint in the system and an equality check assertion in the witness generation code (in the place it is in the circom code).

For this reason, currently the order maters and is always better to use <==. After your comment, we are planing to add the equality assertion checks at the end of the code generated for the template instead of at the place they appear in the circom code. Then the place where the === are used in the circom code will become irrelevant. Until then it matters and using out === 1 – ab; out <-- 1 - ab; may raise an exception in the witness generation since at the point we have === the signal out has the default value 0.

As a general rule, never use <--. Only use it when you cannot do it with <== or using existing templates, and then add constraints with === that ensure that the value you have given with <-- is the right one to get the outputs of the template. Adding no constraint means that any value for the signal is valid in your system. Hope it's clear.

a6-dou commented 1 year ago

make sense thanks!