We are interested in practical automated verification techniques for ZK circuits that are being built for production use cases in the near future (3-6mo).

Robust auditing and verification processes are especially important for ZK circuits because it can be impossible to tell whether or not a missing constraint in a circuit has been exploited in production.

In zkSNARK circuits that exist in production today, a circuit is represented as a set of “R1CS constraints”—essentially, degree 2 equations over variables that are elements in a prime field. A zkSNARK proof is a proof of knowledge of a satisfying assignment (witness) to this set of equations. We designate a subset of these variables as “input” variables, and a disjoint subset as “output” variables.

The goal of the ZK circuit developer is to construct a set of constraints such that satisfaction of constraints implies a specific relationship between the input variables and output variables—i.e., satisfying the constraints tells you that f(inputs) = outputs for a function f. For example, for the function y = f(x) = x^3 + x - 5, we might write the following set of constraints:

interm1 = x * x
interm2 = interm1 * x
interm3 = interm2 + x
y = interm3 - 5

It is easy to see in this case that satisfying these equations is “equivalent” to having executed the function f on a value x.

However, for more complex functions, the equations and the function definition might not line up as cleanly. Our ultimate goal is to prove the equivalence of constraints and a function specification. We are looking to award grants to proving engineers or anyone with expertise in verification methods who may be interested in working on the project directions below.

Of the approaches we have tried so far, the Ecne tool by Franklyn Wang (more details) is currently the most promising, and is able to verify witness uniqueness for most of circomlib as well as several of our more complex ECC circuits. We expect however that there is a lot we have not yet tried—for example, we haven’t even started to touch more generic solvers.

Problems

What properties do we want to verify?

We are interested in verifying a few different claims about the constraints set IR. It’s probably easier to verify certain IRs than it is to verify others, and it seems like we prefer to verify the low-level constraint IR rather than other representations of human-written programs; for these reasons, we are mostly looking at the R1CS intermediate representation.

In order of strength:

• Uniqueness of witness. Mathematically stated: given a system of polynomial equations (R1CS constraints) over a set of variables, when a specific subset of these variables are fixed, is there at most one solution for the remaining variables that satisfies the equations?
  • The reason we care about this is that we want our constraint sets to be properly determined—satisfying the constraints is equivalent to executing a well-defined function at all.
  • Theoretically, one could imagine ZK circuits which don’t admit a unique witness, but for which there is still only a single output variable set admitted for every input. Perhaps there are even clever optimizations you can do if you allow this. But so far we have never encountered this case in constructing any circuits, nor have we encountered this “in the wild.”
  • Currently, the ecne project aims to do this.
• Specific mathematical relationships between certain variables. This is stronger than simply proving uniqueness of witness: here, we want to prove things like “given satisfaction of these constraints, the evaluation of a polynomial with coefficients {x_i} evaluated at X is always equal to the evaluation of a polynomial with coefficients {y_i} evaluated at X.”
• Equivalence of a constraint set and a function spec. This is probably the strongest notion of verification. It’s basically the above bullet point, but for the full relationship we want to prove between input and output variables.
• Equivalence of different sets of constraint equations (i.e. optimized and unoptimized circuits, or different arithmetizations). Different proving systems have different IRs, depending on the proving system’s arithmetization scheme. Also, optimized constraint sets may be harder to verify than unoptimized constraint sets. Still, at the end of the day, most IRs generally involve polynomial equations over finite fields. But in dealing with PIL or UltraPLONK constraints (such as PLOOKUP) we may have to add in new methods.
  • Being able to prove equivalence of constraints sets means that we may be able to turn one set of constraints into another that is easier to verify.
  • Ecne currently has a simple deoptimization process that makes some optimized circuits easier to verify.

What objects and processes do we want to verify/audit?

• Circuit building blocks (”components” or “templates” in circom). These are reusable building blocks, such as IsZero (output is 1 if input is 0, else 0), Num2Bits (output is an array of bits equal to bitstring representation of input), ECDSAPrivToPub (output is an ECDSA public key corresponding to an input interpreted as an ECDSA private key). These reusable building blocks are composed to build larger programs.
  • Usually, we compile these templates to R1CS, then verify claims on the R1CS.
• Entire compiled circuits. Almost by definition, this is at least as hard as verifying the building blocks that a circuit is built from. Even if we know that building blocks of a circuit in higher-level code are all “correct,” there is still the question of what happens to these building blocks when the whole circuit is compiled (especially under optimization).
  • We compile a circuit to R1CS, and verify that R1CS.
  • At low levels of optimization, verifying a claim on a circuit building block may help to verify the full circuit, as we can search for sub-constraint-sets within the full R1CS and abstract them away given our prior knowledge.
• Compilation and decompilation; compiler optimization and deoptimization. If we know that compilation is correct, then we can verify a constraint set at a lower level of optimization. Alternatively, we can “de-optimize” an optimized circuit to make it easy to verify. Verification of compilation may also help us feel better about verification of correctness of circuit building blocks implying correctness of full circuits.
  • This may require verifying circuit compiler code, or verifying various transformations applied during optimization/deoptimization.