When we compute a ZK circuit we are not just executing some code, but proving that we have executed the code correctly.
Take a program that computes x + y = z. It’s not enough for a ZK program to simply output z, the program also needs to prove that x + y was executed correctly to arrive at the value z.
Producing the proof requires establishing constraints.
In other words, circuits are comprised of constrained functions–meaning ZK programs that generate proofs based on a set of constraints.
So why then, would you need a function with no constraints–an unconstrained function? You might think unconstrained functions would be unsafe, given their name–like taking the guardrails off of a ZK circuit. And you’d be right!
Circuit code without constraints can be “proven” to create any outcome! Rather than creating a proof that deterministically proves the validity of a piece of code, unconstrained functions allow you to execute code that would otherwise be very expensive or difficult to compute inside the circuit.
But being able to execute logic outside of a circuit is critical for both circuit performance and constructing proofs on information that is external to a circuit.
When to use
Generally, we want to use unconstrained functions whenever there’s something that’s easy to verify but hard to compute within the circuit.
An unconstrained function simply executes code as you would expect in a normal programming execution environment.
In this post we want to make sure that developers who are tapping into the performance benefits of unconstrained functions aren’t incorrectly implementing unconstrained functions in a way that leads to worse security for their programs. Incorrect usage of unconstrained functions could lead to bugs, and zk development overall is a newer, scarier paradigm. We want to make it easy for developers to use Noir to write performant and secure ZK programs, and unconstrained functions can help them optimize their circuits when implemented correctly.
Simple division
Assuming proving divisions in ZK is costly while proving multiplications is easy, and we want to prove the computation of 100 / 5.
Proving 100 / 5 = x directly in ZK would be inefficient:
Instead, we might use unconstrained functions to optimize our circuits. A more optimized approach would involve:
1. Computing 100 / 5 = x in an unconstrained manner
2. Proving x * 5 = 100 in ZK
Here’s a way to optimize the same division operation:
Cautious readers however might notice both the code excerpts above yield approximately the same number of constraints in Noir’s abstract circuit intermediate representation (ACIR) given the optimization is simple enough to implement in Noir’s compiler.
The key intuition here is that in a ZK execution environment, proving multiplications is cheaper than proving divisions.
Given all Noir programs compile to an intermediate representation called the Abstract Circuit Intermediate Representation (ACIR), we can judge circuit optimization on both ACIR opcodes and the ultimate number of backend circuit gates.
This simple division case has 2 ACIR opcodes and 7 final backend circuit gates. The unoptimized version where we check assert(x == 20) has 3 ACIR opcodes and 8 final backend circuit sizes. Our optimization reduced the final backend size by one gate. Given this is a super simple example, let’s dive into a more complex case where the optimizations are more meaningful.
A more complex example
Colin Nielsen, developer in the Noir community wrote the following code for converting unsigned integers (uints) to u8 arrays, without the use of unconstrained functions.
Here’s the unoptimized code:
This code has 91 total ACIR opcodes and a circuit size of 3,619. A lot of the operations in this function are already optimized away by the compiler (e.g., all the bitshifts turn into divisions by constants).
However, we can save a bunch of gates by casting to u8 a bit earlier. This automatically truncates the bitshifted value to fit in a u8, which allows us to remove the XOR against 0xff.
This is what the slightly-optimized code looks like:
ACIR opcodes generated: 75
Backend circuit size: 3,143
Already, this saves us ~480 gates in total, but we can do better.
This code is all constrained, so we’re proving every step of the calculation using num. But in fact, we don’t actually care about how we make the calculation, just that the computation is correct.
This is where unconstrained functions come in.
Optimizing with unconstrained functions
It turns out that truncating a u72 into a u8 is hard to do inside of a SNARK. Each time we do this operation to truncate down into u8, we lay down 4 ACIR opcodes, which get converted into multiple gates.
It’s actually much easier to calculate num from out, rather than the other way around. All we need to do is multiply each element of out by a constant and add them all together, both of which are relatively easy operations to do inside of a SNARK.
So, instead of truncating u72 into u8, we can run u72_to_u8 as unconstrained function code in order to calculate out. Then, we can use that result in our constrained function and assert that if we were to do the reverse calculation, we’d get back num.
An example of what this looks like is below:
Total ACIR opcodes generated: 78
Backend circuit size: 2,902
This usage of unconstrained functions ends up optimizing our circuit even further and taking off another ~250 gates from our circuit!
We’ve ended up with more ACIR opcodes than before, but these are easier for the backend to prove (resulting in fewer gates overall). This is the beauty of using unconstrained functions – optimizing code that’s easy to verify but hard to compute within the circuit.
Put differently, unconstrained functions allow you to reformulate certain pieces of code that are easier to check than to execute directly in a ZK circuit.
Resources
For more on unconstrained functions, see this post by Tom French in the official Noir docs: https://noir-lang.org/language_concepts/unconstrained/
Are you a developer interested in getting started with Noir?
Jump into the noir-starter Github repo and when you’re ready apply for a Grant–we’re currently supporting Noir use-cases through the end of 2023.
