# Halo2 - Circuit Implementation
## Halo2 Libraries
The [original Halo2](https://github.com/zcash/halo2) by the Zcash foundation: it does not support KZG.
The Privacy Scaling Explorations ([PSE](https://github.com/privacy-scaling-explorations/halo2)) fork which adds KZG support.
## Halo2 Books
[Zcash/halo2 books](https://zcash.github.io/halo2/)
[zksecurity/halo2 book](https://halo2.zksecurity.xyz/)
## Create a Circuit
[An example code](https://zcash.github.io/halo2/user/simple-example.html)
### `configure` function
The `configure` function sets up the constraints, enabling the use of custom gates (e.g. multiplication and addition gates) within the circuit:
1. Declaring the columns (advice, instance, fixed) and selectors required for the circuit.
2. Defining gates (constraints).
#### Step 1 in `configure`: Declaring the columns
- `Advice` columns: Used for the prover to assign witness values.
- `Instance` column: Used for public inputs or outputs.
- `Fixed` column: Stores constant values.
- `Selector` columns: special Fixed columns (fixed columns with a fixed value of 1 or 0) that can be used to turn gates on and off (enable or disable constraints inside the gates). In the `synthesize` function we will program the selector on or off.
- `meta: &mut ConstraintSystem<F>`: Represents the constraint system for the ZKP circuit. It's where you define and manage constraints.
-- `meta.enable_equality(column)`: Enable the ability to **enforce equality** over cells in this column. This function is included in `meta.enable_constant`.
-- `meta.advice_column()`: Allocate a new advice column
-- `meta.instance_column()`: Allocate a new instance column
-- `meta.fixed_column()`: Allocate a new fixed column
-- `meta.selector()`: Allocate a new (simple) selector.
**An example**
```rust
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let advice = meta.advice_column();
meta.enable_equality(advice);
let q_enable = meta.selector();
...
}
```
#### Step 2 in `configure`: Defining gates (constraints)
- `meta: &mut ConstraintSystem<F>`: Represents the constraint system for the ZKP circuit. It's where you define and manage constraints.
-- `meta.create_gate` Define a gate
-- `meta.query_advice`: Query an advice column at a relative position
-- `meta.query_selector`: Query a selector at the current position.
```rust
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
...
// define a new gate:
// next = curr + 1 if q_enable is 1
meta.create_gate("step", |meta| {
let curr = meta.query_advice(advice, Rotation::cur());
let next = meta.query_advice(advice, Rotation::next());
let q_enable = meta.query_selector(q_enable);
vec![q_enable * (curr - next + Expression::Constant(F::ONE))]
});
}
```
- `curr`: the expression value in the current row of the `advice` column.
- `next`: the expression value in the next row of the `advice` column.
- `Expression::Constant`: a constant expression value.
The constraint is
`q_enable * (curr - next + 1) = 0`
### `synthesize` function
The `synthesize` function
1. assigns values,
2. performs computations by combining the methods provided by chips (modular arithmetic units), and
3. exposes the outputs to compare with the public inputs for verification.
- `layouter`: The circuit layouter for arranging rows and assigning values in the circuit.
- `region`: A region is a contiguous block of rows in the circuit. We can
-- create a region using `layouter.assign_region`
-- assign a (advice) cell using `region.assign_advice`
- enable the selector at offset i using `config.q_enable.enable(&mut region, i)?;`
- Equality Constraints: `region.constrain_equal` and `copy_advice` can be used to enforce equality between cells.
:::info
Regions ensure local isolation, create distinct "logical" units that we can compose. Not only synthesize, but also chip functions (e.g. `mul` and `add` functions) that allocates new separate regions for gates (e.g., multiplication and addition gates, respectively) that utilize the region.
:::
:::info
A common optimization in PlonKish (e.g. Halo2) is to implement:
1. Arithmetic Gates (in `configure`): Include gates for operations like multiplication, addition, etc.
2. Arithmetic Chip: Implements methods for operations like multiplication, addition, etc., tailored for modular arithmetic, and these methods can be invoked within the `synthesize` function.
3. Synthesize: Can utilize the methods provided by the Arithmetic Chip to assign cells and enforce constraints within the circuit.
:::
**Examples**
```rust
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "steps",
|mut region| {
// apply the "step" gate STEPS = 5 times
for i in 0..STEPS {
// assign the witness value to the advice column
region.assign_advice(
|| "assign advice",
config.advice,
i,
|| self.values.as_ref().map(|values| values[i]),
)?;
// turn on the gate
config.q_enable.enable(&mut region, i)?;
}
// assign the final "next" value
region.assign_advice(
|| "assign advice",
config.advice,
STEPS,
|| self.values.as_ref().map(|values| values[STEPS]),
)?;
Ok(())
},
)?;
Ok(())
}
```
```rust
fn mul(
&self,
mut layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config();
layouter.assign_region(
|| "mul",
|mut region: Region<'_, F>| {
// We only want to use a single multiplication gate in this region,
// so we enable it at region offset 0; this means it will constrain
// cells at offsets 0 and 1.
config.s_mul.enable(&mut region, 0)?;
// The inputs we've been given could be located anywhere in the circuit,
// but we can only rely on relative offsets inside this region. So we
// assign new cells inside the region and constrain them to have the
// same values as the inputs.
a.0.copy_advice(|| "lhs", &mut region, config.advice[0], 0)?;
b.0.copy_advice(|| "rhs", &mut region, config.advice[1], 0)?;
// Now we can assign the multiplication result, which is to be assigned
// into the output position.
let value = a.0.value().copied() * b.0.value();
// Finally, we do the assignment to the output, returning a
// variable to be used in another part of the circuit.
region
.assign_advice(|| "lhs * rhs", config.advice[0], 1, || value)
.map(Number)
},
)
}
```
### Lookup
Lookup is useful for range check and bitwise operations.
- A lookup table is a pre-computed table of values.
- A lookup constraint ensures that the values (or tuples of values) computed in a circuit can be found in a pre-computed lookup table,
Suppose the lookup table is:
| number | alphabet | operation |
| -------- | -------- | -------- |
| 0 | a | + |
| 1 | b | - |
| 2 | c | * |
| 3 | d | / |
The lookup constraint can verify if the following tuples belong to the table above:
- (0,a,+), YES!
- c, YES!
- (0,d), NO!
##### Lookup Implementation Steps
**1. Load the table in `synthesize`**
- Create a table using `layouter.assign_table`
- Assigns a fixed value to a table cell using `table.assign_cell`
This following code ([source](https://github.com/zcash/halo2/blob/main/halo2_gadgets/src/utilities/lookup_range_check.rs)) shows how to load a lookup table with a column indexed by `table_idx`. The table contains K-bit values, enabling it to verify whether a given value is a valid K-bit number.
```rust
fn load(&self, layouter: &mut impl Layouter<F>) -> Result<(), Error> {
layouter.assign_table(
|| "table_idx",
|mut table| {
// We generate the row values lazily (we only need them during keygen).
for index in 0..(1 << K) {
table.assign_cell(
|| "table_idx",
self.table_idx,
index,
|| Value::known(F::from(index as u64)),
)?;
}
Ok(())
},
)
}
```
**2. Lookup Gate (Constraint) in `configure`**
- `meta.lookup` returns a map between input expressions and the table columns they need to match.
- Constraint
```
vec![
(q_lookup * input_expression_1, table_column_1),
(q_lookup * input_expression_2, table_column_2),
...
]
```
if `q_lookup = 1`, then the lookup checks:
- `(input_expression_1, input_expression_2, ...)` in `(table_column_1, table_column_2, ...)`
The following code is sourced from [here](https://github.com/zcash/halo2/blob/main/halo2_gadgets/src/utilities/lookup_range_check.rs).
```rust
meta.lookup(|meta| {
let q_lookup = meta.query_selector(config.q_lookup);
let q_running = meta.query_selector(config.q_running);
let z_cur = meta.query_advice(config.running_sum, Rotation::cur());
// In the case of a running sum decomposition, we recover the word from
// the difference of the running sums:
// z_i = 2^{K}⋅z_{i + 1} + a_i
// => a_i = z_i - 2^{K}⋅z_{i + 1}
let running_sum_lookup = {
let running_sum_word = {
let z_next = meta.query_advice(config.running_sum, Rotation::next());
z_cur.clone() - z_next * F::from(1 << K)
};
q_running.clone() * running_sum_word
};
// In the short range check, the word is directly witnessed.
let short_lookup = {
let short_word = z_cur;
let q_short = Expression::Constant(F::ONE) - q_running;
q_short * short_word
};
// Combine the running sum and short lookups:
vec![(
q_lookup * (running_sum_lookup + short_lookup),
config.table_idx,
)]
});
```
## Testing the circuit
Use `halo2_proofs::dev::MockProver`, see [here](https://zcash.github.io/halo2/user/simple-example.html#testing-the-circuit).
:::warning
The public inputs taken by the verifier is a `Vec<Vec<F>>`.
This is to support multiple Instance columns: one vector of values per column.
:::
Sign in with Wallet
Connect another wallet