Groth16 circuits useful examples:

1. RC4 circuit;

2. SHA256 circuit;

3. PoSt circuit;

Common principles:

Before creating a circuit it is desirable to have reference implementation of finite computation that is going to be used with SNARK system. In case of arbitrary crypto-algorithm, say hash function, you can always have test vectors - mapping between input and output (preimage → hash value) that can be used for checking correctness. Having that, while creating a circuit, you base your implementation on already available and well-tested gadgets from bellperson / bellman library and tries to achieve similarity with reference implementation by comparing the test vectors.

A good way is to start implementing circuit using TestConstraintSystem, which has a good indicator of circuit correctness - by evaluating result of is_satisfied() method. Most likely, such circuit will work while actual proving. Also it is useful to compare packed results of computation with the inputs generated by compute_multipacking() function.

Generally, once synthesizing the circuit has been debugged / implemented with TestConstraintSystem, it is necessary to take a look at propagating None values after moving code to synthesize method of the circuit implementation. I may not work with TestConstraintSystem which doesn’t ignore SynthesizeError errors, but they are ignored with KeypairAssembly used internally in while generating global parameters. It allows generating parameters for circuits with undefined values of variables - as actual values do not matter in this case, while only relationship between variables (constraints) - e.g. shape of constraints system produced by the circuit matters.

MalformedVerifyingKey error obtained while proof verification means that number of expected public inputs (set of field elements) is not valid. So first step in debugging that is trying to identify how many field elements is required and then provide valid logic of their generation based on input available for verifier.

When it is necessary to enforce some value included in the public inputs (e.g. when we want to enable verifier to submit the expected result of some computation enforced in the circuit) we can use inputize function. Then while proof verification make sure that this public input is included into the output vector of scalars.

Q&A

1. What is a namespace in a ConstraintSystem

Jake: Its just an abstraction for better separation of variables

2. What is a MultiEq? And why it is used somehow instead of regular ConstraintSystem?

Jake: Its an additional implementation of ConstraintSystem with optimisations for UInt32 additions

3. How to convert UInt32 value to usize/u32 from Rust standard library?

Jake: A good way to do that is following (it also handles None case)

let mut value = 0usize;
for (i, bit) in value.into_bits().iter().enumerate() {
    if let Some(true) = bit.get_value() {
        value += 1 << i;
    }
}

4. How synthesizing should work with the blank circuits (while generating global parameters in particular)?

Jake: during key generation each SynthesizeError due to a None value will be ignored. The only thing that matters is the number of variables used in the circuit and the relationships between those variables (constraints), so circuits instantiated with propagated None values must be working when they are used for generation global parameters

5. What approach to use while enforcing operations that do not have gadgets for constraining? Currently, I do following - try to constrain such operations as much as possible using available gadgets

Jake: Some operations like indexing arrays using constant variables or rotation/shifts in sha256 indeed do not required to be enforced. It is because they are just “constant” references to previously assigned (existing) variables. Otherwise, generally If operation requires allocating new variable in CS, it needs to be enforced. An example is indexing array using variable provided as input (pick gadget).