Endeavors into the zero-knowledge Halo2 proving system

Consensys Diligence explains the Halo2 zero-knowledge prover and highlights bugs that can affect security of Halo2 circuits.

How does a proving system work?

In a proving system, a party (“the prover”) wants to prove a statement—for example, the result of a particular computation. The statement can be represented by a constraint C(x, w) where x is a public input and w is a private input; the private input w is called a “witness”, and the prover’s aim is to show prove knowledge of a witness w such that  C(x, w) = 0 (meaning the statement holds). 

The relation specifying valid value combinations between x and w for a statement is the constraint, while the expression of the constraint in a proof system is called a circuit. The representation that we use to express circuits for a particular proof system is called an arithmetization. 

There is a setup phase which generates a proving key and a verification key to be used by the prover and the verifier, respectively. The prover turns the statement into constraints which are represented in arithmetization, and generates the proof with a proving key. The verifier verifies the proof with the verifying key and outputs true or false depending on whether the statement is valid or not. 

The proof is described as a Succinct Non-Interactive Argument of Knowledge (SNARK), and allows the prover to convince a verifier that it knows a witness that makes  the statement true. If the proof reveals no other information asides from the prover’s knowledge of a valid witness w for a statement C (x,w), it is described as “zero-knowledge”; hence, the term zkSNARK (Zero-Knowledge Non-Interactive Succinct Argument of Knowledge). 

What is Halo2?

Halo2 is a proving system based on Plonkish arithmetization, with elements inspired by UltraPLONK (an improvement on the PLONK proving system with support for custom gates and lookup tables). Besides its use in ZCash, Halo2 has been used by teams such as Protocol Labs, the Ethereum Foundation’s Privacy and Scaling Explorations (PSE) team, Scroll, and Taiko, making it one of the more popular zkSNARK constructions today.

Halo2 arithmetization: How is a statement/computation represented? 

An arithmetization in Halo2 (the expression of a circuit) is represented by a grid/matrix with a number of columns and rows. Arithmetization is what makes it possible to prove computational statements (using mathematical tools) without forcing a verifier to evaluate the statement itself. 

A computation is flattened into an area/region containing a number of columns and rows on the matrix, with the initial value, intermediate values, and output value of a computation filling up the cells in that area. Constraints are applied on these cells—that is, the value filled in the cell must satisfy a specified constraint—and this region can be positioned anywhere in the matrix.

Columns in Halo2 arithmetization from Halo2 API & Building a Basic Fibonacci Circuit

Components of Halo2 arithmetization

Columns 

  • Instance columns contain public inputs that are known to both the prover and verifier (or, more broadly, inputs shared between the prover and verifier). 
  • Advice columns contain the witness values (i.e., the prover’s private inputs to the circuit); in a zkSNARK construction, the verifier extracts no knowledge about these values. 
  • Fixed columns contain constants used by every proof that are fixed in the circuit. 
  • Selector columns are special cases of fixed columns that can be used to selectively enable certain constraints.

Rows

The number of rows in the matrix is typically a power of two, limited by the size of the finite field F; it corresponds to the nth root of unity in Plonkish arithmetization. Constraints apply to all the rows, but can be enabled/disabled by selectors defined in selector columns. 

Cells

Cells in the matrix are filled with elements from the chosen finite field; a matrix/grid with cells filled in is called a computation trace. The values of cells will correspond to the public inputs and witness values.

Note that you can use as many columns as you want in a circuit (though the number of rows is limited); but, be aware that more columns and rows will result in larger proofs and increase proof generation and verification times. That’s why you need to optimize the arithmetization, and one way to optimize is using layouter (covered in the later section).

The following table is the representation of a circuit for calculating numbers in the Fibonnaci series. In this representation, the computation is flattened into a rectangular area of 4 rows; each row in the grid represents a computation step where a0 and a1 are the two previous items in the Fibonnaci series and a2 is computed by adding a0 and a1 (a0 + a1)such that the constraint a2 = a0 + a1 is satisfied. Some other details to note:

  • a0, a1, a2 are the advice columns (witness of the constraint) 
  • On each row a selector column s is enabled to apply the constraint
  • a2 is the nth item of the Fibonnaci series (n >= 2), while a0 and a1 on row 0 are the first two items


Arithmetization of Fibonacci circuit from Halo2 API & Building a Basic Fibonacci Circuit

Gate

A gate is a set of constraints controlled by a set of selector columns to be used together. Halo2 provides two types of gates:

  • Standard gate: A standard gate supports general arithmetic, such as field multiplication and division
  • Custom gate: A custom gate is more expressive and capable of supporting specialized operations in a circuit; an example of a custom gate is shown in the Fibonacci circuit below (note that the gate is applied on every row when the selector is enabled)

    Custom gate example from Halo2 API & Building a Basic Fibonacci Circuit

Copy constraint

A copy constraint (also called an equality constraint) enforces that the two cells of a matrix contain the same value. Copy constraints in Halo2 are represented by the permutation argument from PLONK. An example of a copy constraint is described below:
Copy constraint example from Halo2 API & Building a Basic Fibonacci Circuit

Lookup table

A lookup table is defined by tuples of input expressions and a table of pre-computed values representing a relationship in which every tuple of an input expression must be equal to some expression in the set of table columns. Lookup tables are used for  operations not easily expressed by multiplication and addition; in Halo2, lookup tables are represented by lookup arguments and used for complex circuit operations like range checks, bitwise operations, and hash functions. 

Range check lookup table from Halo 2 - with PSE by Chih-Cheng Liang

Chip

A chip is a higher level API that provides efficient pre-built implementations of a particular functionality, with the goal of improving auditability, efficiency, modularity, and expressiveness of circuit implementations. Some examples of functionality that can be implemented in Halo2 using chips include cryptographic hash functions, scalar multiplications, and pairing checks. 

Gadget

A gadget is a higher level interface/API that provides a familiar and convenient means of accessing a chip’s features while abstracting away (extraneous) details of chips’ low-level implementation. Gadgets provide modular and reusable abstractions for circuit programming at a higher level and are useful for implementing Elliptic curve operations, Sinsemilla hash functions, and other functionalities in Halo2 circuits. 

How to write a circuit in Halo2

We’ll be using the Fibonnaci circuit (source code for Fibonacci circuit, forked from original Fibonacci example by Yingtong Lai) as an example to explain how to implement a Halo2 circuit that produces a SNARK proof. Here, the prover’s goal is to prove a statement (represented by the circuit) that given the first two numbers of a Fibonnaci sequence are 1 (representing the private input), the 10th number of the Fibonacci sequence is 55 (representing the public input to the circuit). 

Step 1: Configure the chip

Chip configuration starts by defining columns (advice, instance, selector columns etc.), and copy constraints, and creating custom gates and lookup tables. There are a few APIs from Halo2’s ConstraintSystem for doing this:

  • advice_column: Creates a advice column
  • instance_column: Creates an instance column
  • enable_equality: Enforces equality over cells in this column
  • create_gate: Creates a new gate which contains constraints

Configure function of Fibonacci chip

Step 2: Layout the gates, assign cells and cell values

In this step, we assign the region for the gates of a chip, fill in the cells of the gate and implement chip functions. Below is an explanation of some concepts relevant to this part of building the circuit (layouter and region):

What is Layouter?

Imagine you are putting the gates on the matrix, you need a strategy to decide where to lay out the gates on the matrix, so the circuit is best optimized (smaller proof size and shorter proving/verifying time). The tool for doing this in Halo2 is called layouter, with the most common layouter being the SimpleFloorPlanner.

Why do we need region?

Region is used by the layouter to optimize the global layout and reasoning about local position (offset) of the gate. Region is a block of assignment of gates preserving the relative offset (positions) within the region.

Step 2 (i): Assign the first row of Fibonacci circuit

Step 2 (ii): Assign the next row

Step 2 (iii): Constrain the output (last item of the Fibonacci sequence) to be equal to the instance value

  API functions for implementing copy constraints

  • AssignedCell.copy_advice: Copy the value of a cell to a given advice cell and constrain them to be equal using permutation argument.
  • region.assign_advice_from_instance: Copy the value of an instance cell to an advice cell and use it within the region
  • Layouter.constrain_instance: Constrains the value of a cell to be equal to an instance value

Step 3: Build the circuit

     Implement the circuit trait

  • Configure function configures the circuit. Configure function can include multiple chips’ configuration and happens in the key generation of prover and proving
  • Synthesize function does the computation by filling the cells of gates with initial values, intermediate values and output values and putting all the gates together

Step 4: Run mock prover to verify the proof and test if the constraints are satisfied

Mock prover is a tool to debug a circuit and to verify the constraints are satisfied.
MockProver::run(k: u32, circuit: &ConcreteCircuit, instance: Vec<Vec>)receives a number k which is the maximum degree of polynomials (and determines the number of rows: 2k ), the circuit being verified,and a vector of instance values (public inputs) for all gates in the circuit. 

Internally MockProver::run calls configure and synthesize of the circuit, collects constraint information in a structure and assigns the witness (both private and public inputs) to the structure “in the clear”, while real prover needs to generate proving key (the encoded information of constraint without witness assignments), then creates the proof with proving key and witness at proving time that will be verified by the verifier with verifying key and public input

prover.assert_satisfied() verifies if the constraints are satisfied any constraint is not satisfied, mock prover would output an error with the exact constraint. But be aware that if the constraint is missing or disabled by mistake, mock prover would still pass; this is a bug in the circuit (see section 6 for details). 

Step 5: Circuit visualization

  • Circuit layout: halo2_proofs::dev::CircuitLayout::default() generates circuit layout
  • Circuit structure: halo2_proofs::dev::circuit_dot_graph generates the DOT graph string for circuit structure and has to run test with –all-features and wrapped in the test #[cfg(feature = “test-dev-graph”)]

Note there are 2 regions: “init” and “next row”; the selector is in the purple column

How can bugs happen in Halo2 circuits?

Before writing circuits in Halo2, it is important to know various edge cases that may occur. Each edge case represents a bug in the circuit and may affect security/soundness guarantees of a particular circuit. Below are some examples (referencing the Fibonnaci circuit described previously):   

Mock prover outputs error when a constraint is not satisfied

  • Change in the initial cell value (i.e. elem_1) or instance value (e.g., change let instance = Fp::from(55)to let instance = Fp::from(57)in the Fibonacci circuit. 
  • Change in the assignment of cells (e.g., change let elem_3 =elem_1.value_field().evaluate() +elem_2.value_field().evaluate(); to let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate() + elem_2.value_field().evaluate();in the Fibonacci circuit) 
  • Change in cell rows (e.g., change config.expose_public(layouter, &elem_3, 0)? To config.expose_public(layouter, &elem_3, 1)? in Fibonacci circuit. 

Mock prover won’t output error due to missing constraint

When a constraint is not satisfied, mock prover can detect it. But when a constraint is missing, mock prover won’t find it; thus, the MockProver::run would pass successfully (even if a particular constraint is missing), creating a bug in the circuit. Below are some examples:

  • Missing constraint on instance (public input) value (e.g., remove config.expose_public(layouter, &elem_3, 0)? and change initial cell value (elem_1) to 2 in the Fibonacci circuit)
  • Missing constraint on selectors (e.g., remove self.q_fib.enable(&mut region, offset)? and config.expose_public(layouter, &elem_3, 0)? and change let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate(); to let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate() + elem_2.value_field().evaluate(); in the Fibonacci circuit)
What would happen? 

Mockprover.prove would pass, because the gate is not enabled, even if there is an error in the circuit (invalid elem_3 value assignment ); also, the proof generated by the circuit will pass proof verification, although the Fibonacci sequence computed by the prover is wrong. 

How do things work behind the scenes in Halo2?

I’m not a cryptographer, and the following is  my high-level and oversimplified understanding of the cryptography making Halo2 work under the hood. 

Plonkish arithmetization

  • Finite fields: Field of an elliptic curve group (Pallas/Vesta curve in ZCash Halo2 implementation)
  • Columns: Columns are defined by a Lagrange polynomial over the powers of an nth roots of unity
  • Rows: Rows in Plonkish arithmetization correspond to roots of unity; the number of rows is a power of 2, limited by the multiplicative subgroup size, 2^n x T = p-1
  • Cells: Cells are elements of a finite field and represent evaluation/commitment of polynomial on the roots of unity; scalar field element of Vesta curve (base field element of Pallas curve) in ZCash Halo2 implementation
  • Permutation argument
  • Lookup argument

Polynomial commitment scheme

Commits the constraints to polynomials based on inner product argument in ZCash Halo2 implementation:

  • Cell assignment commitment: Commits cell assignments to polynomials. The advice column commitments are computed by the prover and stored in the proof, while the fixed and instance column commitments are computed both by the prover and verifier. 
  • Lookup argument commitment: Commits the lookup table to a polynomial
  • Permutation argument commitment: Commits a permutation argument to a polynomial
  • Vanishing argument: Constructs the vanishing argument (polynomial) to constrain all circuit relations to zero including standard and custom gates, lookup argument and permutation argument’s degree. 
  • Evaluate the above polynomials at all necessary points
  • Multipoint opening argument: Construct the multipoint opening argument (polynomial) to check that all evaluations are consistent with their respective commitments
  • Run inner product argument to create a polynomial opening proof for the multipoint opening argument, the size of which is the log(N) of the original polynomial’s dimension N

Accumulation scheme (recursion)

  • Run inner product argument to implement recursive proof

Resources and References

Original Fibonnaci example**https://github.com/therealyingtong/halo2-hope

Thanks Chingiz Mardanov, George Kobakhidze, Yingtong Lai and Halo2 team for suggestions and feedback

All posts chevronRight icon

`