this operator describes computation only performed by an honest prover. This is called witness computation and is not performed by the verifier. As a result, the verifier can't trust that this computation will be performed correctly (not all provers are honest), and has to introduce constraints making sure that all witness computation was done correctly. If at any point, you use this operator, make sure you have accompanying constraints verifying this computation. Your system is not sound otherwise.
===
this operator describes the constraints, which is the only computation performed by the verifier. Verifier is given access to an array of signals which were set by the prover using some witness computation, and now the verifier checks if this array constitutes a valid proof. In the Num2Bits example, the verifier can't trust that signal vector bits[i] was set correctly by the prover. Hence, it is checking that they are indeed all bits. Similarly, it can't be sure that bits[i] actually corresponds to the bits of input in. So, there is an additional constraint at the end of this function, making sure that the linear combination of bits (basically shifting each bit in its right place) is indeed equal to in. The constraint statements can only take the following form: (linear combination of signals) === (linear combination of signals) (linear combination of signals) + constant , where a linear combination of signals is simply c_1 w_1 + c_2 w_2 + ... + c_n w_n, where c_i's are constants known at compile time and w_i's are signals. You can check arbitrary computations with these quadratic constraints.
<==
this operator is basically syntactic sugar for <-- followed by ===. You should always use this operator when the statement is quadratic (as defined above). It does not introduce soundness issues because whatever the prover is computing, the verifier is computing it as well.
var
serves two purposes: (i) helps in performing witness computation, and (ii) helps to accumulate a linear combination. For instance, in Num2Bits, you can't write out the linear combination sum_of_bits directly without var as it is tedious and its number of terms depend on the template parameter b.
template: try to use existing templates as much as possible. These are already sound, so you can use them without worrying about constraining any witnesses. While using them, it is also a good exercise to try to understand why they are complete and sound.
=== is clearly harder to work with than <-- which allows arbitrary statements, but note that === has to do something simpler than <-- in most cases. It only has to verify that the computation was done correctly, while <-- has to do the computation. A naive (and sound) way of verifying is to just do the entire computation and check if the output matches. If you are finding it hard to come up with clever way of verifying, you can always use this approach. Quadratic statements are expressive enough to do arbitrary computation, and an example of how you can do degree-3 computation is as follows:
// check if c = a^3
signal input a;
signal output c;
// introduce a signal to store your intermediate results
// use the safe operator <== that automatically adds constraints for you
signal b <== a * a;
c <== a * b;
An example of being clever about verification is Num2Bits. The statement bits[i] <-- (in >> i) & 1 corresponds to a high-degree arithmetic circuit, which will be quite expensive to compute using quadratic statements. Instead, the template introduces very simple constraints that verify this computation. In general, Num2Bits is a good template to look at for ideas.
Eventually, think that this program will be split into two parts. All computation with <-- will be run by the prover, and all computation with === will be run by the verifier (along with the relevant var statements). You can always assume that the verifier computation will happen as-is, but a sound proof system will never assume that the prover did its computation correctly.
<--
this operator describes computation only performed by an honest prover. This is called witness computation and is not performed by the verifier. As a result, the verifier can't trust that this computation will be performed correctly (not all provers are honest), and has to introduce constraints making sure that all witness computation was done correctly. If at any point, you use this operator, make sure you have accompanying constraints verifying this computation. Your system is not sound otherwise.
===
this operator describes the constraints, which is the only computation performed by the verifier. Verifier is given access to an array of signals which were set by the prover using some witness computation, and now the verifier checks if this array constitutes a valid proof. In the Num2Bits example, the verifier can't trust that signal vector bits[i] was set correctly by the prover. Hence, it is checking that they are indeed all bits. Similarly, it can't be sure that bits[i] actually corresponds to the bits of input in. So, there is an additional constraint at the end of this function, making sure that the linear combination of bits (basically shifting each bit in its right place) is indeed equal to in. The constraint statements can only take the following form: (linear combination of signals) === (linear combination of signals) (linear combination of signals) + constant , where a linear combination of signals is simply c_1 w_1 + c_2 w_2 + ... + c_n w_n, where c_i's are constants known at compile time and w_i's are signals. You can check arbitrary computations with these quadratic constraints.
<==
this operator is basically syntactic sugar for <-- followed by ===. You should always use this operator when the statement is quadratic (as defined above). It does not introduce soundness issues because whatever the prover is computing, the verifier is computing it as well.
var
serves two purposes: (i) helps in performing witness computation, and (ii) helps to accumulate a linear combination. For instance, in Num2Bits, you can't write out the linear combination sum_of_bits directly without var as it is tedious and its number of terms depend on the template parameter b.
template: try to use existing templates as much as possible. These are already sound, so you can use them without worrying about constraining any witnesses. While using them, it is also a good exercise to try to understand why they are complete and sound.
=== is clearly harder to work with than <-- which allows arbitrary statements, but note that === has to do something simpler than <-- in most cases. It only has to verify that the computation was done correctly, while <-- has to do the computation. A naive (and sound) way of verifying is to just do the entire computation and check if the output matches. If you are finding it hard to come up with clever way of verifying, you can always use this approach. Quadratic statements are expressive enough to do arbitrary computation, and an example of how you can do degree-3 computation is as follows:
An example of being clever about verification is Num2Bits. The statement bits[i] <-- (in >> i) & 1 corresponds to a high-degree arithmetic circuit, which will be quite expensive to compute using quadratic statements. Instead, the template introduces very simple constraints that verify this computation. In general, Num2Bits is a good template to look at for ideas.
Eventually, think that this program will be split into two parts. All computation with <-- will be run by the prover, and all computation with === will be run by the verifier (along with the relevant var statements). You can always assume that the verifier computation will happen as-is, but a sound proof system will never assume that the prover did its computation correctly.