# 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](https://eprint.iacr.org/2019/953)** 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](#Why-do-we-need-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](http://learn.0xparc.org/materials/halo2/learning-group-1/halo2-api)*

#### 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](https://zcash.github.io/halo2/background/fields.html#roots-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](#What's-Layouter?).

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](http://learn.0xparc.org/materials/halo2/learning-group-1/halo2-api)*

**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](http://learn.0xparc.org/materials/halo2/learning-group-1/halo2-api)*
* **Copy constraint**
Also called equality constraint, which enforces that the two cells contain the same value. It's represented by [permutation argument ](https://zcash.github.io/halo2/design/proving-system/permutation.html)of Plonk
*Copy constriant example
Copy constraint from [Halo2 API & Building a Basic Fibonacci Circuit](http://learn.0xparc.org/materials/halo2/learning-group-1/halo2-api)*

* **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](https://zcash.github.io/halo2/design/proving-system/lookup.html) in Halo 2
Used for range checks, bitwise operation, hash functions etc.


*Range check lookup table from [Halo 2 - with PSE](https://www.youtube.com/watch?v=ihPcnctm4q4&t=836s) 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](#Why-do-we-need-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: 2^k^ ), 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](#When-things-go-wrong,how-bugs-happen-in-the-cirucit?)

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](https://github.com/rairyx/Halo2-Fibonacci) for Fibonacci circuit, forked from original [Fibonacci example](https://github.com/zcash/halo2) 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](https://github.com/zcash/pasta) in ZCash Halo2 implementation
* Columns: encoded by a Lagrange polynomial over the powers of an n^th^ [roots of unity](https://zcash.github.io/halo2/background/fields.html#roots-of-unity)
* Rows: correspond to roots of unity, number of rows is power of 2, limited by the multiplicative subgroup size, 2^n^xT=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](https://zcash.github.io/halo2/design/proving-system/permutation.html)
* [Lookup argument](https://zcash.github.io/halo2/design/proving-system/lookup.html)

### Polynomial commitment scheme
Commit the constraints to polynomials based on [inner product argument](https://zcash.github.io/halo2/background/pc-ipa.html) in ZCash Halo2 implementation
* [Cell assignment commitment](https://zcash.github.io/halo2/design/proving-system/circuit-commitments.html#committing-to-the-circuit-assignments): 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](https://zcash.github.io/halo2/design/proving-system/circuit-commitments.html#committing-to-the-lookup-permutations): commit the lookup table to a polynomial
* [Permutation argument commitment](https://zcash.github.io/halo2/design/proving-system/circuit-commitments.html#committing-to-the-equality-constraint-permutation): commit permutation argument to a polynomial

* [Vanishing argument](https://zcash.github.io/halo2/design/proving-system/vanishing.html): 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](https://zcash.github.io/halo2/design/proving-system/multipoint-opening.html#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](https://zcash.github.io/halo2/background/recursion.html))
* Run inner product argument to implement recursive proof

## Resources and reference
* ZCash Halo2 book
https://zcash.github.io/halo2/index.html
* ZCash Halo2 repository
https://github.com/zcash/halo2
* 0xparc Halo2 learning group
http://learn.0xparc.org/materials/halo2/learning-group-1/introduction
* Halo 2 - with PSE, Present by CC Liang
https://www.youtube.com/watch?v=ihPcnctm4q4&t=836s
Little Things I’ve Learned in Developing Halo2 Circuits by Chih-Cheng Liang
https://www.youtube.com/watch?v=wSfkpJDq8AI&t=1101s
* Original Fibonnaci example
https://github.com/therealyingtong/halo2-hope