changed 2 years ago  
Published Linked with GitHub

Endeavor into Halo2

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

How does proving system work?

Prover wants to prove a statement, the statement can be represented by a constraint C(x, w) where there is a public input x and a private input w that they know that C(x, w) = 0 which makes the statement holds.
The relation (valid value combination) bewteen x and w is the constraint
The expression of the constraint in a proof system is called circuit

The representation that we use to express circuits for a particular proof system is called arithmetization

There is a setup phase which generates proving key and verification key
Prover turns the statement into constraints which are represented in arithmetization, generates the proof with a proving key. Verifier verifys the proof with the verifying key and outputs true or false

What's Halo2?

Halo2 is a proving system based on Plonkish arithmetization, which is an improvement on Plonk proving system with custom gates and lookup tables

Halo2 arithmetization (how statement/computation is represented?)

Halo2 arithmetization( expression of circuit) is represented by a grid/matrix with number of columns and rows

A computation is flattened into an area/region containing a number of columns and rows on the matrix, the initial value and intermediate value and output value of the computation are filled in the cells of that area, constraints are applied on these cells (i.e. the value filled in the cell that satisfies the constriant), this region can be positioned anywhere in the matrix

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

Columns

  • Instance columns contains public inputs, that are shared between the the prover and verifier
  • Advice columns are where the prover assigns private values, that the verifier learns zero knowledge about.
  • 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 constraint.

Rows:

The number of rows is power of two, limited by the field size. It corresponds to the nth root of unity in Plonkish arithmetization. Constraints applies to all the rows, which can be enabled/disabled by the selector columns

Cells:
Filled in finite field element, also called computation trace.

You can use as many columns as you want, but the number of rows is limited, but be aware more columns and rows costs more in proving(proof size and time) and verification time. That's why you need to optimize the arithmetization, one way to optimize is using layouter which will be covered in the later section.

The following is the representation of the Fibonnaci series circuit, in this representation, the computation is flatten into a rectangular area of 4 columns and number of rows, each row represents a computation step in which a0 and a1 are the previous two items in the Fibonnaci serie and a2 is computed by a0 + a1, a constraint a2 = a0 + a1 is satisfied, 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 serie (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 set of constraints controlled by a set of selector columns that are designed to be used together

  • Standard gate: field multiplication and division

  • Custom gate: specialized operations
    Example: Fibonacci series
    Note the gate is applied on every row when the selector is enabled.

    Fibonnaci gate from Halo2 API & Building a Basic Fibonacci Circuit

  • Copy constraint
    Also called equality constraint, which enforces that the two cells contain the same value. It's represented by permutation argument of Plonk
    Copy constriant example

    Copy constraint from Halo2 API & Building a Basic Fibonacci Circuit

  • Lookup table
    Defined by tuples of input expressions and a table of pre-computed values represents a relationship in which every tuple of input expression must equal to some expression in the set of table columns, they are not easily or expensive expressed by multiplication and addition operations. It's represented by lookup argument in Halo 2
    Used for range checks, bitwise operation, hash functions etc.

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

Chip:

  • A higher level API that provides efficient pre-built implementations of particular functionality. characteristics of auditability, efficiency, modularity, and expressiveness.
  • Examples: Hash function, scalar multiplication, pairing check

Gadget

  • Higher level interface/API to chip that abstracts away from chips extraneous detail
    provide modular and reusable abstractions for circuit programming at a higher level
  • Examples: ECC gadget ( Elliptic curve operations), Sinsemilla hash function

How to write a circuit in Halo2?

I'm using Fibonnaci circuit as an example, the circuit is to prove given the first two numbers are 1 (private input), the 10th number of Fibonacci sequence is 55, which is the public input of the circuit

1 Configure the chip

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

  • advice_column: Create a advice column
  • instance_column: Create an instance column
  • enable_equality: Enforce equality over cells in this column
  • create_gate: Creates a new gate which contains constraints
​struct Config {
​   //column a0
​   elem_1: Column<Advice>,
​   //column a1
​   elem_2: Column<Advice>,
​   //column a2
​   elem_3: Column<Advice>,
​   //slector column s 
​   q_fib: Selector,
​   //instance column for the last item "55"
​   instance: Column<Instance>,
}

impl Config {
​   fn configure<F: Field>(
​       cs: &mut ConstraintSystem<F>
​   ) -> Self {
​       let elem_1 = cs.advice_column();
​       //enable copy constraint for column a0 
​       cs.enable_equality(elem_1);
​       let elem_2 = cs.advice_column();
​       //enable copy constraint for column a1 
​       cs.enable_equality(elem_2);
​       let elem_3 = cs.advice_column();
​       let instance = cs.instance_column();  
​       //enable copy constraint for column a2 
​       cs.enable_equality(elem_3);
​       //enable copy constraint for instance column, the last item "55"
​       cs.enable_equality(instance);

​       let q_fib = cs.selector();
​       //creates a gate called "fibonacci"   
​       cs.create_gate("fibonacci", |virtual_cells| {
​           // Query a selector at the current position
​           let q_fib = virtual_cells.query_selector(q_fib);
​           // Query an advice column at current position
​           let elem_1 = virtual_cells.query_advice(elem_1, Rotation::cur());
​           let elem_2 = virtual_cells.query_advice(elem_2, Rotation::cur());
​           let elem_3 = virtual_cells.query_advice(elem_3, Rotation::cur());
​       // this gate constaints one constraint: s * (elem_1 + elem_2 - elem_3) = 0
​           vec![
​              
​               q_fib * (elem_1 + elem_2 - elem_3),
​           ]
​       });

​       Self { elem_1, elem_2, elem_3, q_fib, instance }
​   }

Configure funciton of Fibonacci chip

2 Layout the gates, assign cells and cell values

Assign the region for the gates of a chip, fill in the cells of the gate and implement chip functions

What's Layouter?

Imagin you are putting the gates on the matrix, you need a strategy to decide where to layout the gates on the matrix, so the circuit is best optimised (smaller proof size and shorter proving/verifying time), the tool is called layouter, the most common layouter is 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 assigement of gates preserving the relative offset(positions) within the region.

  • Assign the first row of Fibonacci circuit
fn init<F: Field>(
​       &self,
​       mut layouter: impl Layouter<F>,
​       elem_1: Value<F>,
​       elem_2: Value<F>,
​   ) -> Result<(
​       AssignedCell<F, F>, // elem_2
​       AssignedCell<F, F> // elem_3
​   ), Error> {
​       layouter.assign_region(|| "init Fibonacci", |mut region| {
​           let offset = 0;

​           // Enable q_fib
​           self.q_fib.enable(&mut region, offset)?;

​           // Assign elem_1
​           region.assign_advice(|| "elem_1", self.elem_1, offset, || elem_1)?;

​           // Assign elem_2
​           let elem_2 = region.assign_advice(|| "elem_2", self.elem_2, offset, || elem_2)?;
​          // let elem_3 = elem_1;
​           let elem_3 = elem_1 + elem_2.value_field().evaluate();
​           // Assign elem_3
​           let elem_3 = region.assign_advice(|| "elem_3", self.elem_3, offset, || elem_3)?;

​           Ok((
​               elem_2,
​               elem_3
​           ))

​       })
​   }
  • Assign the next row:
fn assign<F: Field>(
        &self,
        mut layouter: impl Layouter<F>,
        elem_2: &AssignedCell<F, F>,
        elem_3: &AssignedCell<F, F>,
    ) -> Result<(
        AssignedCell<F, F>, // elem_2
        AssignedCell<F, F> // elem_3
    ), Error> {
        layouter.assign_region(|| "next row", |mut region| {
            let offset = 0;

            // Enable q_fib
            self.q_fib.enable(&mut region, offset)?;

            // Copy elem_1 (which is the previous elem_2)
            let elem_1 = elem_2.copy_advice(|| "copy elem_2 into current elem_1", &mut region, self.elem_1, offset)?;

            // Copy elem_2 (which is the previous elem_3)
            let elem_2 = elem_3.copy_advice(|| "copy elem_3 into current elem_2", &mut region, self.elem_2, offset)?;
            let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate();
            //comment next line makes constaint not satified 
           // let elem_3 = elem_1.value_field().evaluate() + elem_2.value_field().evaluate() + elem_2.value_field().evaluate();
            // Assign elem_3
            let elem_3 = region.assign_advice(|| "elem_3", self.elem_3, offset, || elem_3)?;
            
           
            Ok((
                elem_2,
                elem_3
            ))

        })
    }
  • Constraint output( last item of the Fibonnaci serie) to be equal as instance
fn expose_public<F:Field>(
​       &self,
​       mut layouter: impl Layouter<F>,
​       cell: &AssignedCell<F,F>,
​       row: usize,
​   ) -> Result<(), Error> {
​       
​       layouter.constrain_instance(cell.cell(), self.instance, row)


​   }

API function for copy constraint

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

3 Build the circuit

Implement the Circuit trait

  • Configure function configures the circuit. Configure function can include multiple chips configuration, Configure happens in the key generation of prover and proving
  • Synthesize function does the computation by feeding the cells of gates with initial value, intermediate values and output values and putting all the gates together
struct MyCircuit<F: Field> {
        elem_1: Value<F>, // 1
        elem_2: Value<F>, // 1
      
    }

impl<F: Field> Circuit<F> for MyCircuit<F> {
        type Config = Config;

        type FloorPlanner = SimpleFloorPlanner;

        fn without_witnesses(&self) -> Self {
            Self::default()
        }

        fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
            Self::Config::configure(meta)
        }

        fn synthesize(&self, config: Self::Config, mut layouter: impl Layouter<F>) -> Result<(), Error> {
            // elem_2 = 1, elem_3 = 2
            let (mut elem_2, mut elem_3) = config.init(layouter.namespace(|| "init"), self.elem_1, self.elem_2)?;

            for _i in 3..10 {
             let (_, new_elem_3) = config.assign(layouter.namespace(|| "next row"), &elem_2, &elem_3)?;
             elem_2 = elem_3; 
             elem_3 = new_elem_3; 
         
            }
            config.expose_public(layouter, &elem_3, 0)?;
            Ok(())
        }
    }

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<F>>), receives a number k which is the maximum degree of polynomials( which determines the number of rows: 2k ), the circuit being verified and a vector of vector of instance value (public inputs) for all the gates,
Internally MockProver::run calls configure and synthesize of the circuit, collects constraint information in a structure and assigns the witness (private and public input) 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 satified
When any constraint is not satisfied, mock prover would output error with the exact constraint. But be aware if the constraint is missing or disabled by mistake, mock prover would still pass, which is a bug in the circuit. See section 6

fn test_fib() {
​    
​       let circuit = MyCircuit {

​           elem_1: Value::known(Fp::one()),
​           elem_2: Value::known(Fp::one()),
​       };
​       let instance = Fp::from(55);
​       let mut public_input = vec![instance];
​       let prover = MockProver::run(5, &circuit, vec![public_input]).unwrap();
​       
​       prover.assert_satisfied();
​   }

5 Circuit Visualization

  • Circuit layout
    halo2_proofs::dev::CircuitLayout::default() generates circuit layout
  • Circuit structure
    halo2_proofs::dev::circuit_dot_graph generate the DOT graph string for circuit structure
  • Has to run test with –all-features
    has to be wrapped in the test #[cfg(feature = “test-dev-graph”)]
#[test]
    #[cfg(feature = "dev-graph")]
    #[test]
    fn print_fibo() {
        use plotters::prelude::*;
        let root = BitMapBackend::new("fib-layout.png", (1024, 3096)).into_drawing_area();
        root.fill(&WHITE).unwrap();
        let root = root.titled("Fib Layout", ("sans-serif", 60)).unwrap();


        let circuit = MyCircuit {

            elem_1: Value::known(Fp::one()),
            elem_2: Value::known(Fp::one()),
       
        };
        halo2_proofs::dev::CircuitLayout::default()
            .render(5, &circuit, &root)
            .unwrap();

        let dot_string = halo2_proofs::dev::circuit_dot_graph(&circuit);    
        print!("{}", dot_string);
    }

Note there are 2 regions: "init" and "next row", the selector is in the purple column

6 When things go wrong, how bugs happen in the circuit

Mock prover outputs error when constraint not satisfied

  • Change 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)

  • Change 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();

  • Change cell rows
    change config.expose_public(layouter, &elem_3, 0)? to config.expose_public(layouter, &elem_3, 1)?

Missing constaint, mock prover won't output error

When constraint is not satisfied, Mock prover can detect it. But when a constraint is missinng, mock prover won't find it, the MockProver::run would pass Ok, creating a bug in the circuit

  • Missing instance(public input) constraint
    e.g.

    Remove config.expose_public(layouter, &elem_3, 0)? and change initial cell value elem_1 to 2

  • Missing selector
    Remove self.q_fib.enable(&mut region, offset)? and config.expose_public(layouter, &elem_3, 0)?, 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();

What would happen? Mockprover.prove would pass, because the gate is not enabled, even there is an error of the circuit (invalid elem_3 value assigment ), the computatiton will still pass proof verification, although the Fibonacci serie computed is wrong

Source code for Fibonacci circuit, forked from original Fibonacci example by Yingtong Lai

How does things work behind the scene?

I'm not a cryptographer, the following is it's my high-level and over simplified understanding of the cryptography making Halo2 work behind the scene

Plonkish arithmetization

  • Finite field: field of an elliptic curve group, Pallas/Vesta curve in ZCash Halo2 implementation
  • Columns: encoded by a Lagrange polynomial over the powers of an nth roots of unity
  • Rows: correspond to roots of unity, number of rows is power of 2, limited by the multiplicative subgroup size, 2nxT=p-1
  • Cells: Element of finite field, 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

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

  • Cell assignment commitment: commit cell assignments to polynomials. The advice column commitments are computed by the prover and stored in the proof, while the fixed and instance columns commitment are computed both by the prover and verifier

  • Lookup argument commitment: commit the lookup table to a polynomial

  • Permutation argument commitment: commit permutation argument to a polynomial

  • Vanishing argument: Construct 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 reference

Select a repo