Halo2 Essentials

This page is to serve as a reminder for the core things regarding how the Halo2 proof system works that you need to know.

Circuit creation

EF's Halo2 implementation allows you to create and connect gates to form an arithmetic computation. For example, standard plonk gives you an addition gate and a multiplication gate, each with 2 inputs and one output. You can place as many of these around as you like and connect them how you like. When you make the proof you can reveal any wire values you please and keep hidden wire values you please as well

__________ADD IMAGE***********

When placing and connecting gates this is of course done with an aim in mind, i.e. you want the computation to represent something useful. For example, if you factored one of the numbers in the RSA challenge that has an associated reward, then your circuit would consist of one multiplication gate and nothing else, where you would reveal the output of the multiplication gate to be the RSA number people wanted factorised (of course you would keep the inputs of the gate private because revealing them would allow somebody else to claim that they solved the factorisation problem)

Empty circuit

Once you have designed your circuit, you can then assign values to the wires and fill out the circuit so that you have a fully worked computation (i.e. every wire will have a valid value)

Key generation

You can then generate verifying and proving keys (actually the verifying key can be generated from the empty circuit too). The verifying key will be used by verifiers to check your proof (when you check a proof you need to know what the computation that is claimed to have been done correctly was), and the proving key will be used to make the proof (it contains private info and therefore shouldn't be shared).

Proof generation

Now you can use the proving key to create the proof!

Proof verification

Anybody with the proof and the verifying key (or knowledge of what the circuit should be, because then they can just create the verifying key themselves) can check the validity of the proof and therefore of your claim!

Lies (simplifications)

Here we want to highlight what was oversimplified in our description. We spoke of placing gates. In actual fact, the gates are just a pedagogically useful way to interpret the maths. Instead of a gate, what we have is an equation we want to satisfy.

$$l + r - o = 0$$

​For example, the above equation can be viewed as an addition gate by letting l represent the left input wire, r the right input wire, and o the output of the gate. We can add more nuance in what we can do by adding a selector like so:

$$l\cdot s_l + r\cdot s_r - o = 0.$$

​Now we can turn on or off our left or right wires using the selector values s_i. For example if s_l=1 and s_r=0 then we essentially have a gate that just inputs a value. Notice that we can set these scalar values to anything we like though, giving us some flexibility.

These selector values also allow us to put an equation representing an addition gate and a multiplication gate together and using the selectors to decide when it should be addition or multiplication. The original plonk paper comes with this equation:

$$l\cdot s_l + r\cdot s_r + (l\cdot r)\cdot s_m - o\cdot s_o + s_c + PI = 0.$$

​Note that s_c represents the input of a constant value (this value is essentially fixed and never changes, so if there is a common circuit that everybody may use like a transaction circuit then this value never changes). PI represents a public input, meaning that each time you make a proof of this circuit you can make this value whatever you like.

Can you figure out how to set the selectors above to turn the equation into a multiplication gate or an addition gate?

Now for the structure of the main equation. Since we place gates around in the circuit, this means we have multiple copies of the main equation, one for each gate. We structure this in the proof system by just building a table, adding a new row for each gate you add to the circuit (you never directly interact with this table when using halo2, it is handled for you). Connecting wires between gates is done by more data outside of this table.

For example if you have an output and input wire, let's say they are called o_3 and i_7, that you want to connect, we can write down a pair (o)3, i_7) (actually we don't write down the pair ourselves, we just tell the proof system what wires we want connected). Then we can collect a bunch of these pairs, and then when we make the proof the system will handle everything for us.

EF's Halo2

In EF's Halo2 implementation, you can actually decide what the main equation is yourself. This gives users the adaptability to ensure that when they use the proof system it is optimised. This includes removing gates that aren't needed, but also adding in uncommon gates that may be relevant to their use case. There is a limit to this though, once you add too many variables in the equation the proof system slows down, 100 is likely way too many.

Combining equations

Actually in this implementation you will be able to make things called 'chips' that each have their own equation that is different. You can combine these chips into a single proof even though their equation is different - this of course gives a lot of flexibility to its users, but it comes with the handicap of learning how to do so correctly.