Thanks Chingiz Mardanov, George Kobakhidze, Yingtong Lai and Halo2 team for suggestions and feedback
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
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( 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
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:
Gadget
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
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 columninstance_column
: Create an instance columnenable_equality
: Enforce equality over cells in this columncreate_gate
: Creates a new gate which contains constraintsstruct 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
Assign the region for the gates of a chip, fill in the cells of the gate and implement chip functions
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.
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.
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
))
})
}
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
))
})
}
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)
}
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
Configure
function configures the circuit. Configure
function can include multiple chips configuration, Configure happens in the key generation of prover and provingSynthesize
function does the computation by feeding the cells of gates with initial value, intermediate values and output values and putting all the gates togetherstruct 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(())
}
}
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();
}
#[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
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)?
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
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
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