Circuits
Last updated
Last updated
So far we have covered how to define the starting equation, the columns that are required to represent it, how to wrap all that up in a chip struct, and also define a composer trait on top of that chip as a sort of API for using gates under the chosen equation. Fantastic! Now that we have all that, how do we actually create a single circuit under that structural scaffolding we built?
Let's first clarify what we mean by a circuit here. Of course a zk circuit is some arrangement of addition and multiplication gates (connected via copy constraints, and using public inputs to reveal wire values) that should represent some computation of interest, and we are going to want to create a proof that we filled out the wires of such a circuit in a valid manner, revealing only wire values we want. But the TutorialCircuit
we want to build in the code isn't quite that.
The struct we will build in the code will just contain some info we need to create our proof. The structure of our zk circuit will be defined somewhere else, so things that go in the circuit struct we build are things like input values, a lookup table, or the size of the circuit. I recognise that this item being called Circuit
is going to be slightly misleading in that regard, but that's just how the repo works.
For example, in the image above we are going to have 2 input values x
and y
(no indication of whether they are public or private here), and a constant value constant
. The input values are contained in a Value
, which allows both known and unknown values (an unknown value is essentially an Option with None) - this is desired because the actual values aren't needed to create the verifying key.
Another example: let's imagine you want to prove that some value x
to the power k
is y
. Then in the circuit struct you would put x
and k
, but there aren't any other input values you need to put in this struct. You can handle the output value by constraining the final power to be equal to the first entry in the public input column, and insert the claimed value there.
One way to think of this Circuit
struct is as the piece that contains all the data that you will need to actually fill out your circuit. Taking the last example, you only need the values x
and k
, but you don't need any other wire values of the circuit as they can all be calculated by the ones in the Circuit struct
Note: in order to know what your circuit struct should contain, you need to know what the zk circuit you want to build looks like. This doesn't mean you need to know where every gate is, but you should know the rough structure and the inputs or constants required for it.
Now that we have implemented the circuit struct, we are going to want to implement the circuit trait on it to give us the core functionality we expect.
The first function is explained succinctly in the comment above it (note that witness means an advice column value, essentially a wire value of our gates). Let's dive into the second function a little, configure
.
In this function, we will take the columns we defined in the config earlier and 'set' them as the correct column type. More importantly, we will also enforce that the columns interact as we wanted them to based on the starting equation we chose.
You can see in the above code that we define our columns in the way we set earlier and with the same nomenclature. Another thing we do is to enable equality or constant assignments that respectively allow us to enforce equality over cells in the column, and to allow cells to be used for global constant assignments.
The other important aspect to focus on is of course the create_gate
function we apply. You may have guessed, but this is where we are enforcing the columns to respect the equation we chose at the beginning. You should be able to see pretty clearly here the relationship between the equation and the columns.
Note: You may have noticed that the equation in the image doesn't actually include the public input PI. We decided to add the public input functionality via a gate instead for no particular reason other than to show you that there are often multiple ways to achieve the same functionality, each with different tradeoffs.
We come to the third function in the circuit trait, and this is the juicy part - it's where we will actually define what our zk circuit looks like, i.e. where all the addition & multiplication gates are and how they are linked. This will require a bit more work to wrap your head around, so maybe try to keep distractions at bay for a bit.
When you start implementing this function, you should already know roughly what your circuit should look like in a physical or structural sense. For example, the tutorial circuit we want to represent is drawn below.
Pretty straightforward, right? We need 3 multiplication gates and an addition gate. We also need to do some copy constraints to ensure that the outputs of certain gates are the same as the inputs of their corresponding gates. For example, the output of the first multiplication gate needs to be the same as one of the inputs to the third multiplication. We draw these wires as continuous but the way the proof system works is that each gate is separate and you can connect wires with copy constraints. Moreover, we need to ensure that both entries to the first multiplication gate are the same.
Question: can you find a more efficient way to implement the above circuit? You should be able to remove one of the gates. (as you progress in your zk circuit journey, making more efficient implementations is going to be one of the core skills you develop)
Note that with this drawing we have also determined what our circuit struct could contain. Now to actually implement it!
We create the chip struct using the provided config, and then we initialise some of the intermediate values for convenience. Next we insert the first multiplication gate using the raw_multiply
function we defined earlier.
Recall that this function returns three cells, hence the let
definition. The function that is entered as an input to the multiplication function is written to ensure it does what we wanted it to do. It creates x
squared, and then assigns the values x
and x
squared as we should expect. Finally, we include a copy constraint to ensure the inputs to this gate were both the same as we claimed they would be. Surprisingly straightforward actually.
Please take this opportunity to connect up what you learnt previously. Can you see how we are defining a function to go into the raw_multiplication
function we defined earlier to create the functionality we want? The function inserted here returns three field values, each wrapped in a Cell
, and assign_region
in the multiplication function uses this function to allocate values to particular cells and return them.
We just need to repeat this general process for the other gates, including copy constraints and exposing public values. We will leave this for you in the lab.