Introduction
This book is a course on Halo2 development and PlonKish arithmetization in general. The intended audience is Rust developers who have a vague understanding of succinct proofs in general, but no specific knowledge of Halo2, PlonK or developing circuits for zkSNARKs.
The book was created as a collaboration between ZKSecurity and the Zircuit development team. All material, full code examples and the book's source, are available on GitHub.
Chapter 0: Halo World
More boilerplate than Java.
Setup
For this we are going to need Rust 1.67.0 for this:
$ rustup default 1.67.0
To follow along, create a new Rust project:
$ cargo init --bin halo-hero
And populate Cargo.toml as follows:
[package]
name = "halo-hero"
version = "0.1.0"
edition = "2021"
[dependencies]
ff = "0.13"
rand = "0.8"
rand_chacha = "0.3.1"
halo2_proofs = { git = "https://github.com/privacy-scaling-explorations/halo2", tag = "v0.3.0" }
A few notes on the dependencies, there are two:
ffprovides finite field arithmetic traits.halo2_proofsis the Halo2 library we will use, duh.
There is a sea of different versions of Halo2 out there:
- The original Halo2 by the Zcash foundation: it does not support KZG.
- The Privacy Scaling Explorations (PSE) fork which adds KZG support.
- The Scroll fork which forked from PSE.
- The Axiom fork which forked from PSE.
- And more...
However, you write circuits in the same way for all of them.
How To Do Nothing
Let's start by taking a look at the simplest possible circuit: one that does nothing.
Unfortunately, this still requires quite a bit of boilerplate, here is a minimal example:
use std::marker::PhantomData;
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner},
dev::MockProver,
plonk::{self, Circuit, ConstraintSystem},
};
use ff::Field;
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
}
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit { _ph: PhantomData }
}
#[allow(unused_variables)]
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
TestConfig { _ph: PhantomData }
}
#[allow(unused_variables)]
fn synthesize(
&self,
config: Self::Config,
layouter: impl Layouter<F>,
) -> Result<(), plonk::Error> {
Ok(())
}
}
fn main() {
use halo2_proofs::halo2curves::bn256::Fr;
let circuit = TestCircuit::<Fr> { _ph: PhantomData };
let prover = MockProver::run(8, &circuit, vec![]).unwrap();
prover.verify().unwrap();
}We will cover the different parts of this code in more detail in the next chapters.
For now we will just make a few observations:
-
The
Circuit<F>trait represents a "top-level" circuit which may be proved or verified. -
The
Circuit<F>trait is generic over the finite fieldFfor which the circuit is defined.
In the example above, we implementCircuit<F>for everyTestCircuit<F>. -
You might not always be able to make your circuit generic over every field because it relies on field-specific properties. Perhaps the field needs to be of a certain size, or you might need the ability to convert an integer to a field element -- which requires
F: PrimeField.
In practice, every circuit is over a prime field :) -
The
Circuit<F>trait has two associated types:ConfigandFloorPlanner.
The floor planner is not that important, but we will touch on it in the next chapter. -
The
without_witnessesfunction is used by the verifier to create an instance of the circuit without any witness data. This is required to compute the verification key, which would otherwise require the verifier to know a witness for the circuit in order to generate the verification key required to check the SNARK -- which would partly defeat the purpose.
All of this brings us to the two most central concepts in Halo2.
In Halo2, there are two steps in creating a circuit:
Configuration
This is implemented by the configure function.
The high-level task of configuration is to define the available collection of gates in the circuit.
Because Halo2 circuits are much more flexible than traditional arithmetic circuits,
consisting of only addition and multiplication gates,
we need to define the gates that we will use somewhere.
This is done in the configure function.
The resulting Config can then be used to create instances of the gates (or gadgets) in the circuit.
We will cover this in more detail in the next chapter.
Synthesis
After the configuration step, the circuit is synthesized.
This is implemented by the synthesize function.
After defining the gates, we need to create a circuit out of them.
This is done in the synthesize function.
Which, not surprisingly, takes the Config produced by the configure function.
It also takes a Layouter which is used to store the state of the circuit as it is being built.
Finally, the layouter is then responsible for, well, laying out the circuit in some "physical" space
which we will cover in a lot more detail in the next chapter.
Chapter 1: Endless Spreadsheets
Less circuit, more Excel.
Configuration
To get going, we start by adding two columns to the circuit during configuration:
#![allow(unused)] fn main() { fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config { let q_enable = meta.complex_selector(); let advice = meta.advice_column(); }
Each column comes along with a type, in the case above:
advice: an "advice" column which the prover can assign values to freely.q_enable: a "selector" column, used to turn gates on and off.
It contains constants (that the prover can't change).
This can be visualized as a "spreadsheet" with two columns (and an infinite number of rows):
The circuit is defined by fixing certain cells in this "spreadsheet" and the prover gets to fill in the rest of the spreadsheet. If we stop here, we have a spreadsheet where:
- The first column is completely unconstrained.
- The second column is a column of constant zeros.
For this to do anything useful, we need to define some gates. Gates in Halo2 is kind of a misnomer - it's more useful to think of them as constraints over the cells in this "spreadsheet": to enforce relationships between the cells (e.g. constraint the first column).
So here is a very simple example of a gate:
#![allow(unused)] fn main() { fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config { let q_enable = meta.complex_selector(); let advice = meta.advice_column(); // 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))] }); }
This enforces a global constraint on the cells in the spreadsheet, i.e. every row of the spreadsheet:
- The
advicecell in the current row:meta.query_advice(advice, Rotation::cur()) - Minus the
advicecell in the next row:meta.query_advice(advice, Rotation::next()) - Plus one:
Expression::Constant(F::ONE) - Times the
q_enable"selector":meta.query_selector(q_enable)
Must be zero. Like this:
In other words:
- If
q_enable = 1, thennext = curr + 1. - If
q_enable = 0, thennextcan be anything.
This is why we need "selector" columns: to turn gates off.
If we did not multiply by a selector (e.g. q_enable) the gate would always be on and the prover would have to satisfy every gate for every row.
By turning selectors on/off we can "program" the spreadsheet to enforce different constraints over different rows -- that's the job of the synthesize step in Halo2.
Observe that at the next row, the current row is the next row of the previous row:
This means that enabling this gate over a sequence of rows will enforce that the advice column contains a sequence
(e, e+1, e+2, ...).
We will do that in the next section.
Key takeaway: the goal of "configuration" is to define this spreadsheet and the gates (constraints) that act on it. The goal of synthesis will be to fill in the spreadsheet.
The ability to refer to the "next" cell in a column is readily applied in Halo2 circuit design, when the same function needs to be applied over and over again to an input. A classical example is a hash function where the gate might constrain a single round of the hash function.
Synthesize
Creating Regions
A set of consecutive rows are called a region in Halo2. The way they work is as follows:
- You ask Halo2 to create a region.
- You can then refer to the cells in the region relative to its start.
Creating regions and assigning cells in them is exactly the job of the synthesize step in Halo2.
The smallest possible region is a single row, the largest is the entire spreadsheet.
In this example, we will have just a single region.
We create this region using layouter.assign_region.
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "steps",
|mut region| {A couple of natural questions about regions:
For usability.
In fact, you could create your circuit by just having a single giant region which contains the entire spreadsheet. However, this would be very cumbersome to work with, you would have to refer to cells by their absolute position in the spreadsheet and manage all the indexing yourself. With regions, you can break the spreadsheet into smaller logical pieces, reuse them and give them names for easier debugging etc.
That's easy actually: Halo2 (more specifically the "layouter") decides that for you.
You can only refer to cells in the region relative to the region's start,
which means Halo2 may place the "region" (some subset of rows) anywhere in the spreadsheet.
In practice, it will place the region starting at the next available row in the spreadsheet.
It figures it out automatically: the number of rows in the region is the largest relative offset you use in the region. i.e. if you refer to the 5th row in a region, Halo2 knows that the region has at least 5 rows.
Assigning Cells in a Region
We now have a region.
Time to occupy the cells in it, but first:
where should the values come from?
i.e. where do we get the values that the prover should fill the advice column with?
In other ZK-words, where is the witness?
We feed the witness into synthesize by adding a member to the circuit struct:
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
values: Value<Vec<F>>,
}A natural question arises: what the heck is a Value?
A Value<T> is a glorified Option<T>, nothing more.
It exists to contain values that only the prover knows (the witness), i.e.
- For the verifier the
ValueisValue::unknown() - For the prover it is
Value::known(some_witness).
When creating a proof you assign the Values in the circuit struct with the witness
and run synthesis.
Synthesis then assigns the values in the spreadsheet according to the Values in the circuit struct.
In the case above, the Value contains the witness for the advice column: some vector of field elements.
Naturally we must update the without_witnesses function from the circuit to return a Value::unknown():
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
values: Value::unknown(),
}
}Okay back to filling out our new region, this looks as follows:
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(())
}If we assume that:
self.values = Value::known(vec![1, 2, 3, 4, 5, 6])The assignment is as follows:
Exercises
The full code is at the end.
Exercise:
- Implement the
mainfunction to create a (valid)TestCircuitinstance - Call
proveon theTestCircuitinstance.
Exercise:
- Try filling in an invalid value in the
advicecolumn: e.g.[1, 2, 3, 4, 5, 5]. - Does it fail?
Exercise:
Create a circuit which computes the Fibonacci sequence, i.e. enforces next = curr + prev.
- Add a Fibonacci gate or change the existing gate to enforce this relation.
- Create valid witness assignments for the circuit: change how
valuesis assigned in theTestCircuitstruct.
use std::marker::PhantomData;
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Expression, Selector},
poly::Rotation,
};
use ff::Field;
const STEPS: usize = 5;
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
values: Value<Vec<F>>,
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
q_enable: Selector,
advice: Column<Advice>,
}
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
values: Value::unknown(),
}
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_enable = meta.complex_selector();
let advice = meta.advice_column();
// 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))]
});
TestConfig {
_ph: PhantomData,
q_enable,
advice,
}
}
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(())
}
}Regions in Halo2
Okay, circuits have chips, right?, oh! and regions!
Up until this point we have had a single large region, although this is a useful technique because it allows easy "repeating" computation by referring to neighboring cells, it would be a hard way to build circuits in general: normally, we like to compartmentalize and compose smaller things into larger things. Whether in software engineering or hardware design, this is a common pattern, and Halo2 circuit development is no different.
Using (multiple) regions will allow us to create distinct "logical" units that we can compose. In fact, what people usually refer to as a "gate" in regular circuits (think addition/multiplication gates) are in fact more analogous to regions with certain gates enabled in Halo2. This will enable us to create more complex circuits in a more modular way by building up a library of "gadgets" which we can compose to obtain more and more complex behavior.
Another Gate
Okay, new gate time...
Change the configure function into:
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_enable = meta.complex_selector();
let advice = meta.advice_column();
// define a new gate:
meta.create_gate("vertical-mul", |meta| {
let w0 = meta.query_advice(advice, Rotation(0));
let w1 = meta.query_advice(advice, Rotation(1));
let w3 = meta.query_advice(advice, Rotation(2));
let q_enable = meta.query_selector(q_enable);
vec![q_enable * (w0 * w1 - w3)]
});
TestConfig {
_ph: PhantomData,
q_mul: q_enable,
advice,
}
}What does the "vertical-mul" gate do?
Hint:
- Rotation(0) = Rotation::cur()
- Rotation(1) = Rotation::next()
- Rotation(2) = The Next Next Row
To ease the creation of the multiplication gate, we will add a function that allocates a new separate region for a multiplication gate:
impl<F: Field> TestCircuit<F> {
/// This region occupies 3 rows.
fn mul(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
let v0 = lhs.value().cloned();
let v1 = rhs.value().cloned();
let v2 =
v0 //
.and_then(|v0| v1.and_then(|v1| Value::known(v0 * v1)));
let w0 = region.assign_advice(
|| "assign w0", //
config.advice,
0,
|| v0,
)?;
let w1 = region.assign_advice(
|| "assign w1", //
config.advice,
1,
|| v1,
)?;
let w2 = region.assign_advice(
|| "assign w2", //
config.advice,
2,
|| v2,
)?;
// turn on the gate
config.q_mul.enable(&mut region, 0)?;
Ok(w2)
},
)
}
}This function:
- Takes two assigned cells.
- Assigns the
offset = 0cell to the value of thelhscell. - Assigns the
offset = 1cell to the value of therhscell. - Assigns the
offset = 2cell to the product of the two inputs. - Turns on the
vertical-mulgate.
Finally, it returns the offset = 2 cell: the product of the two inputs.
This code is not safe (yet)! Can you see why?
We will get to that when we explore equality constraints.
In order to use this function, we will also need some way to create assigned cells. To do this we create a function which allocates a small (1 row) region, enables no gates and simply returns the cell:
#![allow(unused)] fn main() { impl<F: Field> TestCircuit<F> { /// This region occupies 1 row. fn unconstrained( config: &<Self as Circuit<F>>::Config, layouter: &mut impl Layouter<F>, value: Value<F>, ) -> Result<AssignedCell<F, F>, Error> { layouter.assign_region( || "free variable", |mut region| { region.assign_advice( || "assign w0", // config.advice, 0, || value, ) }, ) } } }
With this we can start writing circuits in style:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
// create a new free variable
let a = TestCircuit::<F>::unconstrained(
&config, //
&mut layouter,
self.secret.clone(),
)?;
// do a few multiplications
let a2 = TestCircuit::<F>::mul(
&config, //
&mut layouter,
a.clone(),
a.clone(),
)?;
let a3 = TestCircuit::<F>::mul(
&config, //
&mut layouter,
a2.clone(),
a.clone(),
)?;
let _a5 = TestCircuit::<F>::mul(
&config, //
&mut layouter,
a3.clone(),
a2.clone(),
)?;
Ok(())
}So far this circuit is not that useful: we are not checking the result of the multiplications against anything. We will get to that in the next couple of sections.
The Issue
As hinted at in the warning, this code is not safe!
The problem is that equality is not enforced between:
- The assigned cells
lhs/rhs - The assigned cells
w0/w1
A malicious prover could set w0 and w1 to arbitrary values
not related to the inputs of lhs and rhs.
To fix this, we are going to need equality constraints, which we will explore in the next section.
Exercises
Exercise: Implement the attack described above:
assign w0 and w1 to arbitrary values not related to the inputs of lhs and rhs.
Verify that the circuit accepts this malicious assignment.
Equality Constraints
So like =A4 in Excel? Yes exactly.
Equality Constraints
Equality constraints allow us to enforce that two arbitrary cells in the spreadsheet are equal.
Fixing The Soundness Issue
We are going to use these to fix the issue in the previous section:
enforcing that w0 and w1 are equal to lhs and rhs respectively.
In order to enforce equality between cells,
we need to enable equality constraints on the columns we want to enforce equality on.
In our example we only have a single advice column:
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// let q_enable = meta.fixed_column();
let q_enable = meta.complex_selector();
let advice = meta.advice_column();
// enable equality constraints
meta.enable_equality(advice);And we need to add equality constraints between the cells when we assign regions:
/// This region occupies 3 rows.
fn mul(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
let w0 = lhs.value().cloned();
let w1 = rhs.value().cloned();
let w2 =
w0 //
.and_then(|w0| w1.and_then(|w1| Value::known(w0 * w1)));
let w0 = region.assign_advice(|| "assign w0", config.advice, 0, || w0)?;
let w1 = region.assign_advice(|| "assign w1", config.advice, 1, || w1)?;
let w2 = region.assign_advice(|| "assign w2", config.advice, 2, || w2)?;
config.q_enable.enable(&mut region, 0)?;
// enforce equality between the w0/w1 cells and the lhs/rhs cells
region.constrain_equal(w0.cell(), lhs.cell())?;
region.constrain_equal(w1.cell(), rhs.cell())?;
Ok(w2)
},
)
}Because manually assigning a value from another cell, only to then enforce equality to the same cell, is very common, cumbersome and error-prone, Halo2 provides a handy function which "copies" one cell to another:
// enforce equality between the w0/w1 cells and the lhs/rhs cells
let _w0 = lhs.copy_advice(|| "assign w0", &mut region, config.advice, 0)?;
let _w1 = rhs.copy_advice(|| "assign w1", &mut region, config.advice, 1)?;
let w2 = region.assign_advice(|| "assign w2", config.advice, 2, || w2)?;
config.q_enable.enable(&mut region, 0)?;It's simply syntactic sugar for the above code.
Exercises
The full code is available at the bottom of the page.
Exercise: Try reimplementing the attack from the previous section.
Does the circuit reject the assignment now?
use std::marker::PhantomData;
use halo2_proofs::{
circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Selector},
poly::Rotation,
};
use ff::Field;
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
secret: Value<F>,
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
q_enable: Selector,
advice: Column<Advice>,
}
impl<F: Field> TestCircuit<F> {
// ANCHOR: mul
/// This region occupies 3 rows.
fn mul(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
let w0 = lhs.value().cloned();
let w1 = rhs.value().cloned();
let w2 =
w0 //
.and_then(|w0| w1.and_then(|w1| Value::known(w0 * w1)));
let w0 = region.assign_advice(|| "assign w0", config.advice, 0, || w0)?;
let w1 = region.assign_advice(|| "assign w1", config.advice, 1, || w1)?;
let w2 = region.assign_advice(|| "assign w2", config.advice, 2, || w2)?;
config.q_enable.enable(&mut region, 0)?;
// ANCHOR: enforce_equality
// enforce equality between the w0/w1 cells and the lhs/rhs cells
region.constrain_equal(w0.cell(), lhs.cell())?;
region.constrain_equal(w1.cell(), rhs.cell())?;
// ANCHOR_END: enforce_equality
Ok(w2)
},
)
}
// ANCHOR_END: mul
/// This region occupies 3 rows.
#[rustfmt::skip]
fn mul_sugar(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
let w0 = lhs.value().cloned();
let w1 = rhs.value().cloned();
let w2 =
w0 //
.and_then(|w0| w1.and_then(|w1| Value::known(w0 * w1)));
// ANCHOR: copy
// enforce equality between the w0/w1 cells and the lhs/rhs cells
let _w0 = lhs.copy_advice(|| "assign w0", &mut region, config.advice, 0)?;
let _w1 = rhs.copy_advice(|| "assign w1", &mut region, config.advice, 1)?;
let w2 = region.assign_advice(|| "assign w2", config.advice, 2, || w2)?;
config.q_enable.enable(&mut region, 0)?;
// ANCHOR_END: copy
Ok(w2)
},
)
}
/// This region occupies 1 row.
fn free(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
value: Value<F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "free variable",
|mut region| {
let w0 = value;
let w0 = region.assign_advice(|| "assign w0", config.advice, 0, || w0)?;
Ok(w0)
},
)
}
}
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
secret: Value::unknown(),
}
}
// ANCHOR: enable_equality
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// let q_enable = meta.fixed_column();
let q_enable = meta.complex_selector();
let advice = meta.advice_column();
// enable equality constraints
meta.enable_equality(advice);
// ANCHOR_END: enable_equality
// ANCHOR: new_gate
// define a new gate:
//
// Advice
// | w0 |
// | w1 |
// | w0 * w1 |
meta.create_gate("vertical-mul", |meta| {
let w0 = meta.query_advice(advice, Rotation(0));
let w1 = meta.query_advice(advice, Rotation(1));
let w3 = meta.query_advice(advice, Rotation(2));
let q_enable = meta.query_selector(q_enable);
vec![q_enable * (w0 * w1 - w3)]
});
// ANCHOR: new_gate
TestConfig {
_ph: PhantomData,
q_enable,
advice,
}
}
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let a = TestCircuit::<F>::free(&config, &mut layouter, self.secret.clone())?;
// do a few multiplications
let a2 = TestCircuit::<F>::mul(&config, &mut layouter, a.clone(), a.clone())?;
let a3 = TestCircuit::<F>::mul(&config, &mut layouter, a2.clone(), a.clone())?;
let _a5 = TestCircuit::<F>::mul(&config, &mut layouter, a3.clone(), a2.clone())?;
Ok(())
}
}
fn main() {
use halo2_proofs::halo2curves::bn256::Fr;
// run the MockProver
let circuit = TestCircuit::<Fr> {
_ph: PhantomData,
secret: Value::known(Fr::from(1337u64)),
};
let prover = MockProver::run(8, &circuit, vec![]).unwrap();
prover.verify().unwrap();
}Fixed Columns
Fixing cells in the spreadsheet.
It is very useful to be able to fix certain cells in the spreadsheet to a constant value.
This is the goal of the Column::Fixed column type which,
as the name suggests, is a column containing values fixed by the verifier which the prover cannot change.
We have in fact already encountered this column type, albeit under a different name:
selector columns, e.g. q_enable, are fixed columns with a fixed value of 0 or 1.
The Column::Fixed column type is more general, allowing any fixed value.
Constants in Gates
So now let us use this to enable checks against constants. One way to use fixed columns is to "program" gates, the simplest example of this is a gate which checks a cell against a constant.
To do so, we introduce a new selector, a new fixed column and a gate to match:
// selector for the fixed column
let q_fixed = meta.complex_selector();
// add a new fixed column
let fixed = meta.fixed_column();
meta.create_gate("equal-constant", |meta| {
let w0 = meta.query_advice(advice, Rotation::cur());
let c1 = meta.query_fixed(fixed, Rotation::cur());
let q_fixed = meta.query_selector(q_fixed);
vec![q_fixed * (w0 - c1)]
});Here, q_fixed * (w0 - c1) is zero iff:
q_fixedis zero, in which case the gate is disabled.w0is equal to the cellc1in the fixed column.
To use this gate we use an equality constraint to enforce that w0 matches the AssignedCell, assign the constant and turn on the gate:
/// This region occupies 1 row.
fn fixed(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
value: F,
variable: AssignedCell<F, F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "fixed",
|mut region| {
variable.copy_advice(
|| "assign variable", //
&mut region,
config.advice,
0,
)?;
region.assign_fixed(
|| "assign constant",
config.fixed, //
0,
|| Value::known(value),
)?;
// turn the gate on
config.q_fixed.enable(&mut region, 0)?;
Ok(())
},
)
}With this new gate, we can finally enforce some non-trivial constraints:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let a = TestCircuit::<F>::free(&config, &mut layouter, self.secret.clone())?;
// a2 = a * a = a^2
let a2 = TestCircuit::<F>::mul(
&config,
&mut layouter, //
a.clone(),
a.clone(),
)?;
// a3 = a2 * a = a^3
let a3 = TestCircuit::<F>::mul(
&config,
&mut layouter, //
a2.clone(),
a.clone(),
)?;
// a5 = a3 * a2 = a^5
let a5 = TestCircuit::<F>::mul(
&config,
&mut layouter, //
a3.clone(),
a2.clone(),
)?;
// fix the value 1337
TestCircuit::<F>::fixed(
&config,
&mut layouter, //
F::from_u128(4272253717090457),
a5,
)?;
Ok(())
}We will see much more complex examples of "programming" gates in subsequent sections. Namely, in the exercises of the "chips" section.
Constants in Equality Constraints
Another, less common, use of fixed columns is to enforce equality between a cell and a constant by enabling equality constraints on a fixed column. Using this strategy, we do not need a separate gate, we simply define a fixed column and enable equality constraints on it:
// add a new fixed column
let fixed = meta.fixed_column();
// turn on equality constraints for the fixed column
meta.enable_constant(fixed);We can then use this by assigning the desired constant to the fixed column and enforcing equality using region.constrain_equal:
/// This region occupies 1 row.
fn fixed(
config: &<Self as Circuit<F>>::Config,
layouter: &mut impl Layouter<F>,
value: F,
variable: AssignedCell<F, F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "fixed",
|mut region| {
// add the value to the fixed column
// if the same constant is used multiple times,
// we could optimize this by caching the cell
let fixed_cell = region.assign_fixed(
|| "assign fixed",
config.fixed,
0,
|| Value::known(value),
)?;
region.constrain_equal(variable.cell(), fixed_cell.cell())?;
Ok(())
},
)
}Chips in Halo2
You would not implement every method on the same class, would you?
So far, we have created multiple regions.
We have created regions for addition and multiplication.
We have been stringing them together having a grand old time.
But things are getting a bit unwieldy:
every method has been implemented on the TestCircuit struct.
Like writing Java with only a single class...
Throwing everything into the same struct
also hinders reusability: nobody else can use the nice gadgets that we have created,
without buying the whole TestCircuit struct.
We need to find a way to make our gadgets more modular.
The pattern we introduce here is that of "chips".
There is nothing special about a chip, it is just a way to structure our circuits. Like a class in object-oriented programming, a chip is a way to group related functionality together. Like a library.
I think we are also ready to graduate to multiple advice columns :)
An Arithmetic Chip
So let's dive into it.
We will create an ArithmeticChip that will implement a small library of arithmetic operations:
#[derive(Clone, Debug)]
struct ArithmeticChip<F: Field> {
_ph: PhantomData<F>,
q_mul: Selector,
q_add: Selector,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
}As you can see, the chip has:
- A selector
q_multo enable the multiplication gate. - A selector
q_addto enable the addition gate. - An advice column
w0to store the first "input". - An advice column
w1to store the second "input". - An advice column
w2to store the "output".
An instance of the ArithmeticChip can be created at configuration time for the circuit:
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
secret: Value::unknown(),
}
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// define advice columns
let w0 = meta.advice_column();
let w1 = meta.advice_column();
let w2 = meta.advice_column();
// enable equality constraints
meta.enable_equality(w0);
meta.enable_equality(w1);
meta.enable_equality(w2);
let arithmetic_chip = ArithmeticChip::configure(meta, w0, w1, w2);
TestConfig {
_ph: PhantomData,
arithmetic_chip,
w0,
w1,
w2,
}
}Which in turn will invoke a method called configure on the ArithmeticChip.
We will get to that in a bit.
A natural question at this point arises:
Namely, why not define the Advice columns inside ArithmeticChip::configure?
The answer is that we could do so, but that it is often useful for different chips to share the same columns.
This is because introducing new columns is relatively expensive:
it increases the size of the proof and the verification time.
Of course Selector columns are usually chip-specific:
sharing them would cause different chips to interfere with each other.
Configuration of the ArithmeticChip should be relatively straightforward to the reader by now:
impl<F: Field> ArithmeticChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
) -> Self {
let q_mul = meta.complex_selector();
let q_add = meta.complex_selector();
// define an addition gate:
meta.create_gate("add", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let w1 = meta.query_advice(w1, Rotation::cur());
let w2 = meta.query_advice(w2, Rotation::cur());
let q_add = meta.query_selector(q_add);
vec![q_add * (w0 + w1 - w2)]
});
// define a multiplication gate:
meta.create_gate("mul", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let w1 = meta.query_advice(w1, Rotation::cur());
let w2 = meta.query_advice(w2, Rotation::cur());
let q_mul = meta.query_selector(q_mul);
vec![q_mul * (w0 * w1 - w2)]
});
Self {
_ph: PhantomData,
q_mul,
q_add,
w0,
w1,
w2,
}
}The only difference from previous examples is that the inputs/outputs are now stored next to each other in the Advice columns,
rather than stacked on top of each other in the same column.
At this point we are ready to add some methods to our ArithmeticChip to create regions for addition and multiplication:
fn add(
&self,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "add",
|mut region| {
// enable the addition gate
self.q_add.enable(&mut region, 0)?;
// compute cell values
let w0 = lhs.value().cloned();
let w1 = rhs.value().cloned();
let w2 = w0.and_then(|w0| w1.and_then(|w1| Value::known(w0 + w1)));
// assign the values to the cells
let w0 = region.assign_advice(|| "assign w0", self.w0, 0, || w0)?;
let w1 = region.assign_advice(|| "assign w1", self.w1, 0, || w1)?;
let w2 = region.assign_advice(|| "assign w2", self.w2, 0, || w2)?;
// constrain the inputs
region.constrain_equal(w0.cell(), lhs.cell())?;
region.constrain_equal(w1.cell(), rhs.cell())?;
Ok(w2)
},
)
} fn mul(
&self,
layouter: &mut impl Layouter<F>,
lhs: AssignedCell<F, F>,
rhs: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
// enable the multiplication gate
self.q_mul.enable(&mut region, 0)?;
// compute cell values
let w0 = lhs.value().cloned();
let w1 = rhs.value().cloned();
let w2 = w0.and_then(|w0| w1.and_then(|w1| Value::known(w0 * w1)));
// assign the values to the cells
let w0 = region.assign_advice(|| "assign w0", self.w0, 0, || w0)?;
let w1 = region.assign_advice(|| "assign w1", self.w1, 0, || w1)?;
let w2 = region.assign_advice(|| "assign w2", self.w2, 0, || w2)?;
// constrain the inputs
region.constrain_equal(w0.cell(), lhs.cell())?;
region.constrain_equal(w1.cell(), rhs.cell())?;
Ok(w2)
},
)
}This is essentially just refactoring the code we saw in the previous sections.
Finally, we can use the ArithmeticChip in the TestCircuit during synthesize:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let a1 = config
.arithmetic_chip
.free(&mut layouter, self.secret.clone())?;
let a2 = config
.arithmetic_chip
.mul(&mut layouter, a1.clone(), a1.clone())?;
let a3 = config
.arithmetic_chip
.add(&mut layouter, a1.clone(), a2.clone())?;
Ok(())
}That's pretty much chips in a nutshell: they are simply a collection of functionality, with convenient methods to create regions. In the exercises we explore how to use a more complex chip along with custom types.
Exercises
So the arithmetic chip we have so far is nice and all, but pretty limited/inefficient. A common optimization in PlonKish (e.g. Halo2) is to have a single arithmetic super gate, that can do:
- Addition
- Multiplication
- Bit range checks
- Constant equality checks
- And more!
While also allowing free multiplication/addition by constants.
This allows PlonK to recoup some of the "linear combination is free" advantages exhibited by alternative arithmetizations like R1CS (like Marlin or Groth16). Such a general arithmetic gate looks as follows:
\[ \text{c0} \cdot \text{w0} + \text{c1} \cdot \text{w1} + \text{c2} \cdot \text{w2} + \text{cm} \cdot (\text{w0} \cdot \text{w1}) + \text{cc} = 0 \]
Where:
cmis the multiplication constant (Column<Fixed>)c0,c1,c2are linear constants (Column<Fixed>)ccis an additive constant (Column<Fixed>)w0,w1,w2are the advice cells (Column<Advice>)
Update the ArithmeticChip to use the new gate for both addition/multiplication.
This requires introducing a number of new fixed columns.
Where do you think these should be defined?
Use the same gate to implement a function fixing a cell to a constant:
Create a function which takes a field element and returns an assigned cell which must be equal to the field element.
One of the main motivations for the new gate was to reduce the cost of multiplication/addition by constants.
To achieve this we introduce a new struct, called Variable:
#[derive(Clone, Debug)]
struct Variable<F: Field> {
mul: F,
add: F,
val: AssignedCell<F, F>,
}
impl<F: Field> Variable<F> {
fn value(&self) -> Value<F> {
self.val.value().map(|v| self.mul * v + self.add)
}
}The value of a Variable is mul * val + add where mul and add are fixed field elements and val is a cell of Column<Advice>. This is useful because we can add/multiply by constants without introducing new regions, simply by changing the mul and add constants:
impl<F: Field> Add<F> for Variable<F> {
type Output = Self;
fn add(self, rhs: F) -> Self {
Self {
mul: self.mul,
add: self.add + rhs,
val: self.val,
}
}
}
impl<F: Field> Mul<F> for Variable<F> {
type Output = Self;
fn mul(self, rhs: F) -> Self {
Self {
mul: self.mul * rhs,
add: self.add * rhs,
val: self.val,
}
}
}Update the ArithmeticChip to use the new Variable struct for addition/multiplication:
accounting for the new multiplicative and additive constants.
Hint
Hint
Multiplication is a bit tricky, you need to expand the expression:
\[ (\text{mul}_1 \cdot \text{val}_1 + \text{add}_1) \cdot (\text{mul}_2 \cdot \text{val}_2 + \text{add}_2) \]
Then set c0, c1, c2, cm, cc appropriately to account for the cross terms. Good luck!
This gate can also be used to do other things, e.g. create a fresh variable restricted to a single bit (the prover must assign the variable either 0 or 1):
/// Allocate a bit-constrained variable.
fn bit(
&self,
layouter: &mut impl Layouter<F>,
value: Value<bool>,
) -> Result<Variable<F>, Error> {Solution
use std::{
marker::PhantomData,
ops::{Add, Mul},
};
use halo2_proofs::{
circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
plonk::{
Advice,
Circuit,
Column,
ConstraintSystem, //
Error,
Expression,
Fixed,
Selector,
},
poly::Rotation,
};
use ff::{Field, PrimeField};
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
secret: Value<F>,
}
// ANCHOR: variable
#[derive(Clone, Debug)]
struct Variable<F: Field> {
mul: F,
add: F,
val: AssignedCell<F, F>,
}
impl<F: Field> Variable<F> {
fn value(&self) -> Value<F> {
self.val.value().map(|v| self.mul * v + self.add)
}
}
// ANCHOR_END: variable
// ANCHOR: add-mul-const
impl<F: Field> Add<F> for Variable<F> {
type Output = Self;
fn add(self, rhs: F) -> Self {
Self {
mul: self.mul,
add: self.add + rhs,
val: self.val,
}
}
}
impl<F: Field> Mul<F> for Variable<F> {
type Output = Self;
fn mul(self, rhs: F) -> Self {
Self {
mul: self.mul * rhs,
add: self.add * rhs,
val: self.val,
}
}
}
// ANCHOR_END: add-mul-const
#[derive(Clone, Debug)]
struct ArithmeticChip<F: Field> {
_ph: PhantomData<F>,
q_arith: Selector,
cm: Column<Fixed>,
c0: Column<Fixed>,
c1: Column<Fixed>,
c2: Column<Fixed>,
cc: Column<Fixed>,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
}
impl<F: Field> ArithmeticChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
c0: Column<Fixed>,
c1: Column<Fixed>,
c2: Column<Fixed>,
cm: Column<Fixed>,
cc: Column<Fixed>,
) -> Self {
let q_arith = meta.complex_selector();
// define arithmetic gate
meta.create_gate("arith", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let w1 = meta.query_advice(w1, Rotation::cur());
let w2 = meta.query_advice(w2, Rotation::cur());
let c0 = meta.query_fixed(c0, Rotation::cur());
let c1 = meta.query_fixed(c1, Rotation::cur());
let c2 = meta.query_fixed(c2, Rotation::cur());
let cm = meta.query_fixed(cm, Rotation::cur());
let cc = meta.query_fixed(cc, Rotation::cur());
let q_arith = meta.query_selector(q_arith);
// define the arithmetic expression
//
// w0 * c0 + w1 * c1 + w2 * c2 + cm * (w0 * w1) + cc
let expr = Expression::Constant(F::ZERO);
let expr = expr + c0 * w0.clone();
let expr = expr + c1 * w1.clone();
let expr = expr + c2 * w2.clone();
let expr = expr + cm * (w0 * w1);
let expr = expr + cc;
vec![q_arith * expr]
});
Self {
_ph: PhantomData,
q_arith,
cm,
c0,
c1,
c2,
cc,
w0,
w1,
w2,
}
}
/// Multiply two variables
fn mul(
&self,
layouter: &mut impl Layouter<F>,
lhs: Variable<F>,
rhs: Variable<F>,
) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
// (c0 * w0 + cc1) * (c1 * w1 + cc2)
// c0 * c1 * (w0 * w1) + c0 * cc2 * w0 + c1 * cc1 * w1 + cc1 * cc2
lhs.val.copy_advice(|| "lhs", &mut region, self.w0, 0)?;
rhs.val.copy_advice(|| "rhs", &mut region, self.w1, 0)?;
let val =
region.assign_advice(|| "res", self.w2, 0, || lhs.value() * rhs.value())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(lhs.mul * rhs.add))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(rhs.mul * lhs.add))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(lhs.add * rhs.add))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(lhs.mul * rhs.mul))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
/// Add two variables
fn add(
&self,
layouter: &mut impl Layouter<F>,
lhs: Variable<F>,
rhs: Variable<F>,
) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "add",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
lhs.val.copy_advice(|| "lhs", &mut region, self.w0, 0)?;
rhs.val.copy_advice(|| "rhs", &mut region, self.w1, 0)?;
let val =
region.assign_advice(|| "res", self.w2, 0, || lhs.value() + rhs.value())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(lhs.mul))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(rhs.mul))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(lhs.add + rhs.add))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
/// Allocate a free variable.
fn free(&self, layouter: &mut impl Layouter<F>, value: Value<F>) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "free",
|mut region| {
// no need to turn on anything
let val = region.assign_advice(|| "free", self.w0, 0, || value)?;
region.assign_advice(|| "junk1", self.w1, 0, || Value::known(F::ZERO))?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
/// Assert equal
fn eq_consant(
&self,
layouter: &mut impl Layouter<F>,
constant: F,
variable: Variable<F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "eq_constant",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
variable
.val
.copy_advice(|| "val", &mut region, self.w0, 0)?;
let delta = variable.add - constant;
region.assign_advice(|| "junk1", self.w1, 0, || Value::known(F::ZERO))?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(variable.mul))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(delta))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(())
},
)
}
// ANCHOR: bit
/// Allocate a bit-constrained variable.
fn bit(
&self,
layouter: &mut impl Layouter<F>,
value: Value<bool>,
) -> Result<Variable<F>, Error> {
// ANCHOR_END: bit
layouter.assign_region(
|| "bit",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
// (v1 - 1) * v1 = v1^2 - v1
let w0 = region.assign_advice(
|| "bit0",
self.w0,
0,
|| value.map(|b| if b { F::ONE } else { F::ZERO }),
)?;
let w1 = region.assign_advice(
|| "bit1",
self.w1,
0,
|| value.map(|b| if b { F::ONE } else { F::ZERO }),
)?;
region.assign_advice(|| "junk", self.w2, 0, || Value::known(F::ZERO))?;
region.constrain_equal(w0.cell(), w1.cell())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c1", self.c0, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "c2", self.c0, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ONE))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val: w0,
})
},
)
}
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
arithmetic_chip: ArithmeticChip<F>,
}
impl<F: PrimeField> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
secret: Value::unknown(),
}
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// let q_enable = meta.fixed_column();
let w0 = meta.advice_column();
let w1 = meta.advice_column();
let w2 = meta.advice_column();
let c0 = meta.fixed_column();
let c1 = meta.fixed_column();
let c2 = meta.fixed_column();
let cc = meta.fixed_column();
let cm = meta.fixed_column();
// enable equality constraints
meta.enable_equality(w0);
meta.enable_equality(w1);
meta.enable_equality(w2);
let arithmetic_chip = ArithmeticChip::configure(meta, w0, w1, w2, c0, c1, c2, cc, cm);
TestConfig {
_ph: PhantomData,
arithmetic_chip,
}
}
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let a1 = config
.arithmetic_chip
.free(&mut layouter, self.secret.clone())?;
let a2 = config
.arithmetic_chip
.add(&mut layouter, a1.clone(), a1.clone())?;
let a3 = config
.arithmetic_chip
.mul(&mut layouter, a1.clone(), a2.clone())?;
config
.arithmetic_chip
.eq_consant(&mut layouter, F::from_u128(1337 * (1337 + 1337)), a3)?;
Ok(())
}
}
fn main() {
use halo2_proofs::halo2curves::bn256::Fr;
// run the MockProver
let circuit = TestCircuit::<Fr> {
_ph: PhantomData,
secret: Value::known(Fr::from(1337u64)),
};
let prover = MockProver::run(8, &circuit, vec![]).unwrap();
prover.verify().unwrap();
}Instances
Instance, public input, statement, whatever.
So far, every circuit we have defined has been specific to a statement we wanted the prover to satisfy. This would be of no use for, e.g. a zk-rollup / validium. We would need a separate circuit for every state transition: in a zk-rollup the circuit shows that a transition between commitments to two adjacent states is valid, without public inputs we would need a separate circuit for every such pair of commitments. Ouch. This in turn would require the verifier to regenerate the verification key for every such new circuit, a very expensive operation, which would defeat the purpose of zk-rollups / validiums: that verification is faster than execution.
The solution is Instance columns.
You can think of instances/public inputs as parameterizing the circuit:
for every assignment (known to the verifier) the prover can be asked to provide a witness.
In other, computer science, words:
the SNARK proves satisfiability of some NP relation \( \mathcal{R} \):
\[
\mathcal{R}(\mathsf{x}, \mathsf{w}) = 1
\]
Where \( \mathsf{x} \), the statement, is known to both parties and \( \mathsf{w} \), the witness (advice column assignments), is known only to the prover.
So far we have always had \( \mathsf{x} \) be the empty string.
Instances
An Instance column is just a regular column, like an advice column,
but the values in the instance column are provided/known to the verifier;
as opposed to the Advice column, which are only known to the prover.
Because Instance columns themselves are pretty simple,
we are going to visit some additional techniques in the examples below:
as a bit of a throwback to the very first circuit we defined,
we will define a circuit that takes an index and returns the fibonacci number at that index.
This means that the circuit must be able to accommodate a variable number of "steps" in the fibonacci sequence.
Our circuit will have 5 columns:
-
fib: anAdvicecolumn which will contain the fibonacci sequence. -
flag: anAdvicecolumn which will contain a "flag" for the gate.
More details on this later. -
index: anAdvicecolumn which will contain the index of the fibonacci number. -
q_step: this is theSelectorcolumn which turns on the sole gate: the "fibonacci" gate. -
instance:Instancecolumn which will contain the index of the fibonacci number we want.
Looks like this:
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let fib = meta.advice_column();
let flag = meta.advice_column();
let index = meta.advice_column();
let q_fib = meta.complex_selector();
let instance = meta.instance_column();
meta.enable_equality(fib);
meta.enable_equality(instance);
meta.enable_equality(index);The Fibonacci Gate
There is a single gate in this circuit, the "fibonacci" gate. This gate is by far the most complex gate we have defined so far, so hold on to your hats:
meta.create_gate("fibonacci", |meta| {
// selector
let enable = meta.query_selector(q_fib);
// index in the Fibonacci sequence
let idx0 = meta.query_advice(index, Rotation(0));
let idx1 = meta.query_advice(index, Rotation(1));
// fibonacci sequence
let w0 = meta.query_advice(fib, Rotation(0));
let w1 = meta.query_advice(fib, Rotation(1));
let w2 = meta.query_advice(fib, Rotation(2));
// indicator
let bit = meta.query_advice(flag, Rotation(0));
let not_bit = Expression::Constant(F::ONE) - bit.clone();
vec![
// it's a bit (strictly speaking, this is redundant)
enable.clone() * bit.clone() * not_bit.clone(),
// apply the Fibonacci rule
enable.clone() * bit.clone() * (w0.clone() + w1.clone() - w2.clone()),
enable.clone()
* bit.clone()
* (idx1.clone() - idx0.clone() - Expression::Constant(F::ONE)),
// OR, maintain the value / index
enable.clone() * not_bit.clone() * (w1.clone() - w2.clone()),
enable.clone() * not_bit.clone() * (idx1.clone() - idx0.clone()),
]
});The layout of the gate is as follows:
This is a gate that essentially allows the prover to choose between two smaller gates:
- Force
bitto be either 0 or 1. - If
bit = 1: calculate the next fibonacci number.w2 = w0 + w1idx1 = idx0 + 1
- If
bit = 0: do nothing.w2 = w0idx1 = idx0
The motivation for this gate is that we want to be able to calculate the fibonacci number at any index:
by setting the bit to 0, the prover can choose to stop progressing the fibonacci sequence once it reaches the desired index.
An alternative way to implement this gate would be to use a dynamic lookup, but we have not covered these yet, stay tuned.
Observe that the gate has a comment about the first constraint being redundant. Why is this?
The Fibonacci Circuit
The circuit is simply turning on the "fibonacci" gate for some number of rows. We save the cells from all these assignments, finally we export the initial state and the final state as instances.
We will break it down in the next section, but here it is in all its glory:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let instances = layouter.assign_region(
|| "fibonacci-steps",
|mut region| {
// apply the "step" gate STEPS = 5 times
let mut fib_cells = Vec::new();
let mut flg_cells = Vec::new();
let mut idx_cells = Vec::new();
for i in 0..STEPS {
// turn on the gate
config.q_fib.enable(&mut region, i)?;
// assign the fibonacci value
fib_cells.push(region.assign_advice(
|| "assign-fib",
config.fib,
i,
|| self.fib_seq.as_ref().map(|v| v[i]),
)?);
// assign the flag
flg_cells.push(region.assign_advice(
|| "assign-bit",
config.flag,
i,
|| {
self.flg_seq
.as_ref()
.map(|v| if v[i] { F::ONE } else { F::ZERO })
},
)?);
// assign the index
idx_cells.push(region.assign_advice(
|| "assign-idx",
config.index,
i,
|| self.idx_seq.as_ref().map(|v| F::from_u128(v[i] as u128)),
)?);
}
// assign the last index
idx_cells.push(region.assign_advice(
|| "assign-fib",
config.index,
STEPS,
|| {
self.idx_seq
.as_ref()
.map(|v| F::from_u128(v[STEPS] as u128))
},
)?);
// assign the last two fibonacci values
fib_cells.push(region.assign_advice(
|| "assign-fib",
config.fib,
STEPS,
|| self.fib_seq.as_ref().map(|v| v[STEPS]),
)?);
fib_cells.push(region.assign_advice(
|| "assign-fib",
config.fib,
STEPS + 1,
|| self.fib_seq.as_ref().map(|v| v[STEPS + 1]),
)?);
// sanity check
assert_eq!(flg_cells.len(), STEPS);
assert_eq!(idx_cells.len(), STEPS + 1);
assert_eq!(fib_cells.len(), STEPS + 2);
// enforce instances
Ok([
fib_cells[0].cell(), // start fib0
fib_cells[1].cell(), // start fib1
idx_cells[0].cell(), // start idx0
fib_cells.last().unwrap().cell(), // end fib
idx_cells.last().unwrap().cell(), // end idx
])
},
)?;
for (i, cell) in instances.into_iter().enumerate() {
layouter.constrain_instance(cell, config.instance, i)?;
}
Ok(())
}Most of the code is very reminiscent of the circuit we explored in the "Endless Spreadsheets" section very early on.
One small difference is that we save the assigned cells,
e.g. saving the assigned cells of the fib column in the fib_cells vector:
fib_cells.push(region.assign_advice(
|| "assign-fib",
config.fib,
i,
|| self.fib_seq.as_ref().map(|v| v[i]),
)?);Then at the end return some cells from the region:
Ok([
fib_cells[0].cell(), // start fib0
fib_cells[1].cell(), // start fib1
idx_cells[0].cell(), // start idx0
fib_cells.last().unwrap().cell(), // end fib
idx_cells.last().unwrap().cell(), // end idx
])Namely:
- The first two cells of the
fibcolumn (first two fibonacci numbers). - The initial index of the first fibonacci number, i.e. 0.
- The final cell of the
fibcolumn. - The final index of the last fibonacci number.
We then enforce that the instance column is equal to these cells:
for (i, cell) in instances.into_iter().enumerate() {
layouter.constrain_instance(cell, config.instance, i)?;
}This, in a nutshell, is how we use instances.
The Witness Generation
Let's briefly look at how the prover generates the witness for this circuit:
let fib_steps = 20; // the number of Fibonacci steps we want to prove
let fib_start0 = Fr::from(1u64); // first Fibonacci number
let fib_start1 = Fr::from(1u64); // second Fibonacci number
// generate a witness
let mut flg_seq = vec![];
let mut idx_seq = vec![0];
let mut fib_seq = vec![fib_start0, fib_start1];
for idx in 1..=STEPS {
if idx <= fib_steps {
// generate the Fibonacci sequence
let f0 = fib_seq[fib_seq.len() - 2];
let f1 = fib_seq[fib_seq.len() - 1];
flg_seq.push(true);
fib_seq.push(f0 + f1);
idx_seq.push(idx);
} else {
// pad the sequences
flg_seq.push(false);
fib_seq.push(*fib_seq.last().unwrap());
idx_seq.push(*idx_seq.last().unwrap());
}
}
// create the circuit
let circuit = TestCircuit::<Fr> {
_ph: PhantomData,
fib_seq: Value::known(fib_seq.clone()),
flg_seq: Value::known(flg_seq.clone()),
idx_seq: Value::known(idx_seq.clone()),
};In other words, the prover progresses the fibonacci sequence until
idx > fib_steps at which point the prover sets the flag bit to 0
and adds padding until the end of the region.
The Verifier
The only change to the MockProver is that we need to provide the instances:
// run the MockProver
let fib_result = fib_seq.last().unwrap().clone();
let prover = MockProver::run(
10,
&circuit,
vec![vec![
fib_start0, // first Fibonacci number
fib_start1, // second Fibonacci number
Fr::from_u128(0 as u128), // start index
fib_result, // claimed result
Fr::from_u128(fib_steps as u128), // after this number of steps
]],
)
.unwrap();
prover.verify().unwrap();The instances taken by the verifier is a Vec<Vec<F>>.
This is to support multiple Instance columns: one vector of values per column.
Static Lookups
Let's write some circuits weird machines
In this installment, we will introduce the concept of lookups.
Rather than trotting through yet another example with range checks, we will explore lookups by creating a "circuit" that can (very efficiently) match regular expressions. Regular expression matching has been used in projects such as zk-email, although the approach outlined here is more efficient than that of zk-email owing to the power of Halo2.
You might be thinking that regular expressions are relatively inefficient to check using a circuit over a finite field, and you would be right. Fortunately, lookups enable us to implement this kind of very non-field-friendly functionality in an efficient way. It might also sound complicated, but in fact, the whole (barebones) circuit fits in just over 200 lines of code.
Brief Detour: Regular Expressions
Some people, when confronted with a problem, think "I know, I'll use regular expressions.".
Now they have two problems.
-- Jamie Zawinski
The particular regular expression we will match is a+b+c, meaning:
- One or more
as. - Followed by one or more
bs. - Followed by a single
c.
For example, it would match:
aaabbcabc
But not:
aaabbbbbbcaaac
For us, the convenient way to view a regular expression is
as a "Non-Deterministic Finite Automaton" (NFA).
You can visualize this as a directed graph where each node is a state
and every edge is labeled with a character.
You are allowed to move between states if the next character in the string matches the edge label.
For instance, for our regular expression a+b+c, an NFA would look like this:
Meaning:
- You start in a state
ST_A. - In this state
ST_A, you can either:- Move to
ST_Aif the next character isa. - Move to
ST_Bif the next character isa.
- Move to
- In state
ST_B, you can either:- Move to
ST_Bif the next character isb. - Move to
ST_Cif the next character isb.
- Move to
- In state
ST_C, you can:- Only move to
ST_DONEif the next character isc.
- Only move to
For instance, if the string we are matching is aaabbc,
we would move through the states like this:
ST_A -> ST_A -> ST_A -> ST_B -> ST_B -> ST_C -> ST_DONE
Conversely, if you have the string aaabbb,
you would get stuck in state ST_B after the third b and not be able to move to ST_C.
We can represent this "NFA" as a table of valid state transitions:
| State | Character | Next State |
|---|---|---|
| ST_A | a | ST_A |
| ST_A | a | ST_B |
| ST_B | b | ST_B |
| ST_B | b | ST_C |
| ST_C | c | ST_DONE |
In Rust we could encode this table as follows:
const ST_A: usize = 1;
const ST_B: usize = 2;
const ST_C: usize = 3;
// start and done states
const ST_START: usize = ST_A;
const ST_DONE: usize = 4;
// end of file marker:
// "dummy padding character"
const EOF: usize = 0xFFFF;
// conversion of the regular expression: a+b+c
const REGEX: [(usize, usize, Option<char>); 6] = [
(ST_A, ST_A, Some('a')), // you can stay in ST_A by reading 'a'
(ST_A, ST_B, Some('a')), // or move to ST_B by reading 'a'
(ST_B, ST_B, Some('b')), // you can stay in ST_B by reading 'b'
(ST_B, ST_C, Some('b')), // or move to ST_C by reading 'b'
(ST_C, ST_DONE, Some('c')), // you can move to ST_DONE by reading 'c'
(ST_DONE, ST_DONE, None), // you can stay in ST_DONE by reading EOF
];The "values" of the states (e.g. const ST_A: usize = 1) are just arbitrary distinct integers.
We introduce a special EOF character which we will use to "pad" the end of the string:
our circuit has a fixed size, but we want it to accommodate strings of different lengths.
We also add another transition ST_DONE -> ST_DONE for the EOF character:
you can stay in the ST_DONE state forever by consuming the special EOF padding character.
If you are still confused, it simply means that we are now matching strings like:
aaabbc<EOF><EOF><EOF>...<EOF>
Of some fixed length, where <EOF> is a special character.
In this example, we will just match the regular expression, but in general you want to do something more interesting with the result or restrict the string being matched.
For instance, in zk-email it is used to extract the sender's address from an email after verifying a DKIM signature on the email: in this case the string being matched comes with a digital signature (an RSA signature).
In our case, the string ends up in a column and it is trivial to use it for further processing, like hashing it to check a digital signature on it.
Configuration
In order for us to match against the regular expression, we will have the prover supply a table of transitions, we will then look up each transition in a fixed table of valid state transitions. We need two gates:
-
A gate to force the current state to be a fixed value: this is used at the start and end, to ensure that the prover starts in the
ST_Astate and ends in theST_DONEstate. -
A gate to check the transition is valid: this is used to check each transition in the table.
Our configuration step looks as follows:
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_regex = meta.complex_selector();
let q_match = meta.complex_selector();
let st = meta.advice_column();
let ch = meta.advice_column();
let fix_st = meta.fixed_column();
let tbl_st_cur = meta.lookup_table_column();
let tbl_st_nxt = meta.lookup_table_column();
let tbl_ch = meta.lookup_table_column();
The new thing to notice is the meta.lookup_table_column() function calls:
these introduce a new column on which we can lookup rows.
In our case, the lookup table will have three columns:
- The current state (e.g.
ST_B). - The next state (e.g.
ST_C). - The character being consumed (e.g.
b).
Gate: Fix
Let us start with the gate that can force the current state to be a fixed value, to the reader, there should be no surprises here:
meta.create_gate("fix-st", |meta| {
let st = meta.query_advice(st, Rotation::cur());
let fix_st = meta.query_fixed(fix_st, Rotation::cur());
let en = meta.query_selector(q_match);
vec![en * (st - fix_st)]
});It simply:
- Reads the current state,
st. - Reads the fixed state,
fix_st. - Forces
st = fix_stifq_match = 1.
Gate: Transition
The new magic is happening in the "transition" gate:
meta.lookup("transition-st", |meta| {
let st_cur = meta.query_advice(st, Rotation::cur());
let st_nxt = meta.query_advice(st, Rotation::next());
let ch = meta.query_advice(ch, Rotation::cur());
let en = meta.query_selector(q_regex);
vec![
(en.clone() * st_cur, tbl_st_cur),
(en.clone() * st_nxt, tbl_st_nxt),
(en.clone() * ch, tbl_ch),
]
});Let's break it down:
- It reads the current state,
st_cur, from thest(state column). - It reads the next state,
st_nxt, from thest(state column). - It reads the next character,
ch, from thech(character column).
The layout looks like this:
It then multiplies them all by the selector q_regex, meaning:
- If
q_regex = 0, then the lookup checks:(0, 0, 0)in(tbl_st_cur, st_nxt, tbl_ch).
- If
q_regex = 1, then the lookup checks:(st_cur, st_nxt, ch)in(tbl_st_cur, st_nxt, tbl_ch).
This 3-tuple is looked up in our table of valid state transitions.
Synthesize
With our gates and lookup table in place, we can now synthesize the circuit.
Assign Table
Let us now take a look at how we populate the table of valid state transitions:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
// assign the transition table
layouter.assign_table(
|| "table",
|mut table| {
// convert the numbers to field elements
let mut transitions: Vec<(F, F, F)> = vec![
// (0, 0, 0) is in the table to account for q_regex = 0
(F::ZERO, F::ZERO, F::ZERO),
];
for tx in REGEX.iter() {
let (st_cur, st_nxt, ch) = tx;
transitions.push((
F::from(*st_cur as u64),
F::from(*st_nxt as u64),
ch.map(|c| F::from(c as u64)).unwrap_or(F::from(EOF as u64)),
));
}
// assign the table
for (offset, (st_cur, st_nxt, char)) in transitions //
.into_iter()
.enumerate()
{
table.assign_cell(
|| format!("st_cur"),
config.tbl_st_cur,
offset,
|| Value::known(st_cur),
)?;
table.assign_cell(
|| format!("st_nxt"),
config.tbl_st_nxt,
offset,
|| Value::known(st_nxt),
)?;
table.assign_cell(
|| format!("char"),
config.tbl_ch,
offset,
|| Value::known(char),
)?;
}
Ok(())
},
)?;Take a second to look at this code. It's mostly self-explanatory, but let's go through it:
- We use
layouter.assign_tableto get a closure with aTableargument. - We convert the
REGEXtable into tuples of field elements:
- We encode the state as a field element.
- We encode each (e.g. ASCII) character as a field element in the obvious way.
- We encode
EOFas some arbitrary value outside the range of valid characters.
- This is then stored in
transitionsas a vector of such tuples. - Finally, we assign the vector of tuples to the table using
table.assign_cell.
Start Constraint
At the first row of our region, we will need to force the state to be ST_A (aka. ST_START).
This is done by assigning the fixed column fix_st to be ST_A and turning on the q_match selector:
layouter.assign_region(
|| "regex",
|mut region| {
// at offset 0, the state is ST_START
region.assign_fixed(
|| "initial state",
config.fix_st,
0,
|| Value::known(F::from(ST_START as u64)),
)?;
config.q_match.enable(&mut region, 0)?;Nothing new here, we saw similar code in the section of Column<Fixed>.
Assign Transitions
The meat of the circuit is in the region where we assign the sequence of states we are transitioning through, as well as the sequence of characters we are consuming:
// assign each step
for i in 0..MAX_STR_LEN {
// enable the regex automaton
config.q_regex.enable(&mut region, i)?;
// state
region.assign_advice(
|| "st",
config.st,
i,
|| {
self.sts.as_ref().map(|s| {
F::from(
s.get(i) //
.cloned()
.unwrap_or(ST_DONE)
as u64,
)
})
},
)?;
// character
region.assign_advice(
|| "ch",
config.ch,
i,
|| {
self.str.as_ref().map(|s| {
s.chars()
.nth(i)
.map(|c| F::from(c as u64))
.unwrap_or(F::from(EOF as u64))
})
},
)?;
}End Constraint
At the end, similar to the start, we need to ensure that the state is ST_DONE:
// at offset MAX_STR_LEN, the state is ST_START
region.assign_advice(
|| "st",
config.st,
MAX_STR_LEN,
|| Value::known(F::from(ST_DONE as u64)),
)?;
region.assign_fixed(
|| "final state",
config.fix_st,
MAX_STR_LEN,
|| Value::known(F::from(ST_DONE as u64)),
)?;
config.q_match.enable(&mut region, MAX_STR_LEN)?;
Ok(())
},
)?;Exercises
The full code is at the end.
Hint
Hint
You do not need to change the circuit, only the REGEX constant.
However, this exercise is slightly more complicated than it seems at first:
we must somehow be able to transition from matching as without consuming an a
(in case there are zero a).
Create a circuit which computes a single round of AES encryption.
You may ignore the key schedule.
Hint
Hint
Use four separate lookup tables to represent:
- The S-box. A table with 256 entries.
- The GF(2^8) addition (XOR). A table with 256x256 entries.
- A "multiplication by 2" in GF(2^8) table. A table with 256 entries.
- A "multiplication by 3" in GF(2^8) table. A table with 256 entries.
Hint
Hint
The above is dominated by the XOR table, which is a 256x256 table. To avoid this massive table we can use the fact that XOR acts component-wise on the bits of the input:
\[ (l_1, l_2) \oplus (r_1, r_2) = (l_1 \oplus r_1, l_2 \oplus r_2) \]
Therefore, we can replace a single lookup in a 256x256 table with two lookups in 16x16 tables.
Create a circuit which takes an AES ciphertext as public input (instance) and a key as private input (witness) and checks that the ciphertext decrypts to a known plaintext.
use std::marker::PhantomData;
use halo2_proofs::{
circuit::{Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
plonk::{
Advice,
Circuit,
Column, //
ConstraintSystem,
Error,
Fixed,
Selector,
TableColumn,
},
poly::Rotation,
};
use ff::{Field, PrimeField};
// ANCHOR: regex
const ST_A: usize = 1;
const ST_B: usize = 2;
const ST_C: usize = 3;
// start and done states
const ST_START: usize = ST_A;
const ST_DONE: usize = 4;
// end of file marker:
// "dummy padding character"
const EOF: usize = 0xFFFF;
// conversion of the regular expression: a+b+c
const REGEX: [(usize, usize, Option<char>); 6] = [
(ST_A, ST_A, Some('a')), // you can stay in ST_A by reading 'a'
(ST_A, ST_B, Some('a')), // or move to ST_B by reading 'a'
(ST_B, ST_B, Some('b')), // you can stay in ST_B by reading 'b'
(ST_B, ST_C, Some('b')), // or move to ST_C by reading 'b'
(ST_C, ST_DONE, Some('c')), // you can move to ST_DONE by reading 'c'
(ST_DONE, ST_DONE, None), // you can stay in ST_DONE by reading EOF
];
// ANCHOR_END: regex
const MAX_STR_LEN: usize = 20;
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
str: Value<String>,
sts: Value<Vec<usize>>,
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
q_match: Selector,
q_regex: Selector, // enable the regex gate
st: Column<Advice>, // current state of automaton
ch: Column<Advice>, // current character
tbl_st_cur: TableColumn,
tbl_st_nxt: TableColumn,
tbl_ch: TableColumn,
fix_st: Column<Fixed>,
}
impl<F: PrimeField> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
str: Value::unknown(), // the string
sts: Value::unknown(), // state of the automaton
}
}
// ANCHOR: columns
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let q_regex = meta.complex_selector();
let q_match = meta.complex_selector();
let st = meta.advice_column();
let ch = meta.advice_column();
let fix_st = meta.fixed_column();
let tbl_st_cur = meta.lookup_table_column();
let tbl_st_nxt = meta.lookup_table_column();
let tbl_ch = meta.lookup_table_column();
// ANCHOR_END: columns
// ANCHOR: fix
meta.create_gate("fix-st", |meta| {
let st = meta.query_advice(st, Rotation::cur());
let fix_st = meta.query_fixed(fix_st, Rotation::cur());
let en = meta.query_selector(q_match);
vec![en * (st - fix_st)]
});
// ANCHOR_END: fix
// ANCHOR: lookup
meta.lookup("transition-st", |meta| {
let st_cur = meta.query_advice(st, Rotation::cur());
let st_nxt = meta.query_advice(st, Rotation::next());
let ch = meta.query_advice(ch, Rotation::cur());
let en = meta.query_selector(q_regex);
vec![
(en.clone() * st_cur, tbl_st_cur),
(en.clone() * st_nxt, tbl_st_nxt),
(en.clone() * ch, tbl_ch),
]
});
// ANCHOR_END: lookup
TestConfig {
_ph: PhantomData,
q_regex,
st,
ch,
tbl_st_cur,
tbl_st_nxt,
tbl_ch,
fix_st,
q_match,
}
}
// ANCHOR: assign_table
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
// assign the transition table
layouter.assign_table(
|| "table",
|mut table| {
// convert the numbers to field elements
let mut transitions: Vec<(F, F, F)> = vec![
// (0, 0, 0) is in the table to account for q_regex = 0
(F::ZERO, F::ZERO, F::ZERO),
];
for tx in REGEX.iter() {
let (st_cur, st_nxt, ch) = tx;
transitions.push((
F::from(*st_cur as u64),
F::from(*st_nxt as u64),
ch.map(|c| F::from(c as u64)).unwrap_or(F::from(EOF as u64)),
));
}
// assign the table
for (offset, (st_cur, st_nxt, char)) in transitions //
.into_iter()
.enumerate()
{
table.assign_cell(
|| format!("st_cur"),
config.tbl_st_cur,
offset,
|| Value::known(st_cur),
)?;
table.assign_cell(
|| format!("st_nxt"),
config.tbl_st_nxt,
offset,
|| Value::known(st_nxt),
)?;
table.assign_cell(
|| format!("char"),
config.tbl_ch,
offset,
|| Value::known(char),
)?;
}
Ok(())
},
)?;
// ANCHOR_END: assign_table
// ANCHOR: region_start
layouter.assign_region(
|| "regex",
|mut region| {
// at offset 0, the state is ST_START
region.assign_fixed(
|| "initial state",
config.fix_st,
0,
|| Value::known(F::from(ST_START as u64)),
)?;
config.q_match.enable(&mut region, 0)?;
// ANCHOR_END: region_start
// ANCHOR: region_steps
// assign each step
for i in 0..MAX_STR_LEN {
// enable the regex automaton
config.q_regex.enable(&mut region, i)?;
// state
region.assign_advice(
|| "st",
config.st,
i,
|| {
self.sts.as_ref().map(|s| {
F::from(
s.get(i) //
.cloned()
.unwrap_or(ST_DONE)
as u64,
)
})
},
)?;
// character
region.assign_advice(
|| "ch",
config.ch,
i,
|| {
self.str.as_ref().map(|s| {
s.chars()
.nth(i)
.map(|c| F::from(c as u64))
.unwrap_or(F::from(EOF as u64))
})
},
)?;
}
// ANCHOR_END: region_steps
// ANCHOR: region_end
// at offset MAX_STR_LEN, the state is ST_START
region.assign_advice(
|| "st",
config.st,
MAX_STR_LEN,
|| Value::known(F::from(ST_DONE as u64)),
)?;
region.assign_fixed(
|| "final state",
config.fix_st,
MAX_STR_LEN,
|| Value::known(F::from(ST_DONE as u64)),
)?;
config.q_match.enable(&mut region, MAX_STR_LEN)?;
Ok(())
},
)?;
// ANCHOR_END: region_end
Ok(())
}
}
fn main() {
use halo2_proofs::halo2curves::bn256::Fr;
// run the MockProver
let circuit = TestCircuit::<Fr> {
_ph: PhantomData,
// the string to match
str: Value::known("aaabbbc".to_string()),
// manually create a trace of the state transitions
sts: Value::known(vec![
ST_A, // ST_A -a-> ST_A (START)
ST_A, // ST_A -a-> ST_A
ST_A, // ST_A -a-> ST_A
ST_B, // ST_A -a-> ST_B
ST_B, // ST_B -b-> ST_B
ST_B, // ST_B -b-> ST_B
ST_C, // ST_B -b-> ST_C
ST_DONE, // ST_C -c-> ST_DONE
]),
};
let prover = MockProver::run(8, &circuit, vec![]).unwrap();
prover.verify().unwrap();
}Dynamic Lookups
"No, no!" said the Queen. "Sentence first—verdict afterwards."
Dynamic Lookups
The previous section introduced the concept of lookups. Namely static lookups, in which the values to look up are fixed at circuit generation time and the only freedom afforded to the prover is to choose the entries to look up. This is fine if you know all the values you want to look up at compile time and the set is small enough (e.g. the XOR table of 8-bit values). But what if you don't? Or maybe the table would be too large to encode explicitly?
In this section we will introduce the concept of dynamic lookups.
It is a natural extension of the static lookups we have seen so far:
rather than looking up rows in Constant columns we will look up rows in Advice columns.
Such dynamic lookups are widely used in machine emulation, let us start by getting a grasp of why such lookups are useful.
Motivation
The instruction set architecture (ISA) of a CPU defines the set of potential instructions that the processor can execute.
This set can be rather large, for example the x86-64 ISA has over 1000 instructions,
for the EVM (Ethereum Virtual Machine) this number is a more modest 140 instructions but includes very complex operations like KECCAK256.
A naive approach to implementing a CPU in a zkSNARK would be to create a circuit for each instruction,
then run every possible instruction in parallel and multiplex the result.
This requires executing every possible instruction at every cycle of the CPU.
Without lookups, this is essentially what people did in the early days of zkSNARKs for machine emulation,
which in turn restricted the size and complexity of the ISA that could be emulated.
Dynamic lookups allow us to avoid this naive approach as follows:
- We can create a table for each instruction. The table simply contains inputs/outputs for the instruction,
for instance a table for the
ADDinstruction would contain rows of the form:
$$(a, b, a + b)$$
- When emulating the CPU, we can then do a lookup in each table to retrieve the result for every possible instruction and then multiplex the results.
The key insight is that we need only a single row in the table for the instruction we are actually executing: all the other lookups can be "nopped out" and the result of the lookup is ignored. If every instruction previously required a separate circuit with \( m \) gates and we have \( n \) instructions, the dynamic lookup approach requires only \( n \) tables with \( m \) rows each whereas the original approach would require \( n \cdot m \) gates.
Example: Conditional Hashing
The example that we are going to explore is a gate that conditionally hashes a value, i.e.
$$ \mathsf{ConditionalHash}(x, b) = \begin{cases} \mathsf{Hash}(x) & \text{if } b = 1 \\ 0 & \text{if } b = 0 \\ \end{cases} $$
The goal is to only "pay" for the hash operation if \( b = 1 \): there will be some a priori bound on the maximum number of hash operations that can be performed, but we don't know ahead of time where / how many of these operations will be performed. We want to incur a cost that is proportional to this upper bound.
A Naive Approach
Before we proceed, let us consider a naive approach to this problem, without dynamic lookups. The baseline solution to this problem would be to create a circuit that hashes the value unconditionally, then use a multiplexer to select the output of the hash operation if the condition is true:
$$ \mathsf{ConditionalHash}(x, b) = \mathsf{Hash}(x) \cdot b $$
As hinted above, the issue with this approach is that the hash operation is always performed, even if the condition is false: we need to generate a circuit for \( \mathsf{Hash}(x) \) and assign the witness, even when \( b = 0 \). So if, for instance, you have a CPU which may compute a hash at every cycle, the circuit of the CPU would have to include the hash operation at every cycle even if the hash is not computed (e.g. if a simple arithmetic operation is performed instead).
In the EVM, the hash might be keccak256 and the condition might be the result of a comparison between the current instruction and the KECCAK256 opcode.
But in order to keep things simple, we will use a simplified and round-reduced variant of the "Poseidon" hash function instead. This variant is not secure for cryptographic use!
The Poseidon Hash Function
The simplified Poseidon used in this example is not secure for cryptographic use!
It's a round-reduced variant with the same round function for all rounds.
Our simplified Poseidon hash function has a state width of 3 field elements and 8 rounds, we split the state into two parts: the "RATE" and the "CAPACITY" part:
#![allow(unused)] fn main() { const ROUNDS: usize = 8; const WIDTH: usize = 3; const CAPACITY: usize = 1; const RATE: usize = WIDTH - CAPACITY; }
The CAPACITY part is the "internal state" of the hash function, while the message to be hashed is added to the "RATE" part.
As mentioned above there are 8 rounds in the hash function, each round consists of the following operations:
-
AddRoundConstant: $$(x, y, z) \mapsto (x + a, y + b, z + c)$$ Where a, b, c are constants (and different each round).
-
SBox: $$ (x, y, z) \mapsto (x^5, y^5, z^5) $$ The exponent 5 is chosen such that the map is a permutation.
-
Mix: $$ (x, y, z) \mapsto M (x, y, z) $$ Where M is a 3x3 matrix (the same for all rounds).
To hash a message \( (x, y) \) we initialize the state with \( (x, y, 0) \) and then apply the 8 rounds.
The hash digest is the first element of the final state:
$$ \mathsf{Hash}(x, y) = \mathsf{output} \text{ where } (\mathsf{output}, ?, ?) = \mathsf{PoseidonPermutation}(x, y, 0) $$
The Poseidon Table
We are going to have a table which contains every invocation of the Poseidon hash function and all their intermediate rounds. The table will contain the following columns:
// a simplified version of Poseidon permutation
#[derive(Debug, Clone)]
struct PoseidonTable<F: Field + Clone> {
matrix: [[F; WIDTH]; WIDTH],
round_constants: [[F; WIDTH]; ROUNDS],
flag_start: Column<Fixed>, // start of permutation
flag_round: Column<Fixed>, // apply round
flag_final: Column<Fixed>, // end of permutation
inp1: Column<Advice>,
inp2: Column<Advice>,
rndc: [Column<Fixed>; WIDTH],
cols: [Column<Advice>; WIDTH],
_ph: PhantomData<F>,
}Some explanation is in order:
matrixis the fixed matrix M from theMixoperation.round_constantsare the constants a, b, c from theAddRoundConstantoperation.flag_startis a flag that indicates the start of a new hash invocation.flag_roundis a flag that indicates that the Poseidon round should be applied.flag_finalis a flag that indicates that the result is ready.inp1is the first input to the Poseidon hash function.inp2is the second input to the Poseidon hash function.rndca set of fixed columns containing the round constants.colsa set of advice columns storing the state of the Poseidon hash function.
As a table we are going to fill it out like this:
| flag_start | flag_round | flag_final | inp1 | inp2 | rndc1 | rndc2 | rndc3 | col1 | col2 | col3 |
|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 1 | 0 | x | y | a1 | b1 | c1 | x | y | 0 |
| 0 | 1 | 0 | x | y | a2 | b2 | c2 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a3 | b3 | c3 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a4 | b4 | c4 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a5 | b5 | c5 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a6 | b6 | c6 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a7 | b7 | c7 | ... | ... | ... |
| 0 | 1 | 0 | x | y | a8 | b8 | c8 | ... | ... | ... |
| 0 | 0 | 1 | x | y | ... | ... | ... | hash | ... | ... |
Constraining the Poseidon Table
There are two types of constraints that we need to add to the Poseidon table:
- The
flag_startconstraint: This resets the state to the input values of the hash function. - The
flag_roundconstraint: This applies the Poseidon round to the state.
Let's take a look at each in turn:
The Start Constraint
The start constraint in its totality is as follows:
meta.create_gate("start", |meta| {
let flag_start = meta.query_fixed(flag_start, Rotation::cur());
let inp1 = meta.query_advice(inp1, Rotation::cur());
let inp2 = meta.query_advice(inp2, Rotation::cur());
let col1 = meta.query_advice(cols[0], Rotation::cur());
let col2 = meta.query_advice(cols[1], Rotation::cur());
let col3 = meta.query_advice(cols[2], Rotation::cur());
vec![
flag_start.clone() * (inp1 - col1), // col1 = inp1
flag_start.clone() * (inp2 - col2), // col2 = inp2
flag_start.clone() * col3, // col3 = 0
]
});What this enforces is:
inp1.cur() = col[0].cur(): load the first input into the first element of the state.inp2.cur() = col[1].cur(): load the second input into the second element of the state.col[2].cur() = 0: set the third element of the state to 0.
These constraints are enforced when flag_start is set to 1.
It corresponds to a row of this form:
| flag_start | flag_round | flag_final | inp1 | inp2 | rndc1 | rndc2 | rndc3 | col1 | col2 | col3 |
|---|---|---|---|---|---|---|---|---|---|---|
| 1 | ... | .. | x | y | ... | ... | ... | x | y | 0 |
The Round Constraint
The round constraint is substantially more complex than the start constraint. It is likely the most complex gate you have encountered so far. It applies an entire round of the Poseidon hash function to the state, including the addition of the round constants, the SBox, and the full matrix operation.
So let's break it down into parts.
We start by "reading" the cells of the current row and the next:
meta.create_gate("round", |meta| {
let flag_round = meta.query_fixed(flag_round, Rotation::cur());
let rndc = [
meta.query_fixed(rndc[0], Rotation::cur()),
meta.query_fixed(rndc[1], Rotation::cur()),
meta.query_fixed(rndc[2], Rotation::cur()),
];
let cols_cur = [
meta.query_advice(cols[0], Rotation::cur()),
meta.query_advice(cols[1], Rotation::cur()),
meta.query_advice(cols[2], Rotation::cur()),
];
let cols_nxt = [
meta.query_advice(cols[0], Rotation::next()),
meta.query_advice(cols[1], Rotation::next()),
meta.query_advice(cols[2], Rotation::next()),
];
let inp_cur = [
meta.query_advice(inp1, Rotation::cur()),
meta.query_advice(inp2, Rotation::cur()),
];
let inp_nxt = [
meta.query_advice(inp1, Rotation::next()),
meta.query_advice(inp2, Rotation::next()),
];We then add the round constants to the state:
// add round constants
let cols_arc = [
cols_cur[0].clone() + rndc[0].clone(), //
cols_cur[1].clone() + rndc[1].clone(), //
cols_cur[2].clone() + rndc[2].clone(), //
];Note that this results in an array of Expressions: in what follows we are essentially composing constraints
as if we were applying functions to concrete values.
We now apply the SBox to the elements of the state:
// apply sbox: this is pretty inefficient, the degree of the gate is high
assert_eq!(POWER, 5);
fn sbox<F: Field>(x: Expression<F>) -> Expression<F> {
x.clone() * x.clone() * x.clone() * x.clone() * x.clone()
}
let cols_sbox = [
sbox(cols_arc[0].clone()),
sbox(cols_arc[1].clone()),
sbox(cols_arc[2].clone()),
];Finally, we apply the matrix operation to the state (consisting of Expressions):
// apply matrix
let cols_mat: [Expression<F>; WIDTH] = [
Expression::Constant(F::ZERO)
+ cols_sbox[0].clone() * matrix[0][0]
+ cols_sbox[1].clone() * matrix[0][1]
+ cols_sbox[2].clone() * matrix[0][2],
Expression::Constant(F::ZERO)
+ cols_sbox[0].clone() * matrix[1][0]
+ cols_sbox[1].clone() * matrix[1][1]
+ cols_sbox[2].clone() * matrix[1][2],
Expression::Constant(F::ZERO)
+ cols_sbox[0].clone() * matrix[2][0]
+ cols_sbox[1].clone() * matrix[2][1]
+ cols_sbox[2].clone() * matrix[2][2],
];Finally we enforce that the next row is the result of applying this complex transformation to the current row:
// enforce that the next state is the round applied to the current state.
vec![
// round application
flag_round.clone() * (cols_mat[0].clone() - cols_nxt[0].clone()), // inp1 = col1
flag_round.clone() * (cols_mat[1].clone() - cols_nxt[1].clone()), // inp2 = col2
flag_round.clone() * (cols_mat[2].clone() - cols_nxt[2].clone()), // 0 = col3
// maintain input
flag_round.clone() * (inp_cur[0].clone() - inp_nxt[0].clone()), // inp1 = inp1
flag_round.clone() * (inp_cur[1].clone() - inp_nxt[1].clone()), // inp2 = inp2
]
});Overall, this corresponds to a row of the form:
| flag_start | flag_round | flag_final | inp1 | inp2 | rndc1 | rndc2 | rndc3 | col1 | col2 | col3 |
|---|---|---|---|---|---|---|---|---|---|---|
| 0 | 1 | 0 | x | y | a1 | b1 | c1 | x' | y' | z' |
Where:
$$(x', y', z') = \text{PoseidonRound}(\mathsf{st} = (x, y, z), \mathsf{rndc} = (a1, b1, c1)) $$
Filling in the Poseidon Table
To aid in the construction of the Poseidon table, we can define a simple helper function that fills in a single row:
fn assign_row(
&self,
idx: usize,
reg: &mut Region<'_, F>,
flag_start: bool,
flag_round: bool,
flag_final: bool,
rndc: [F; 3],
cols: [F; 3],
inp: [F; 2],
) -> Result<(), plonk::Error> {
reg.assign_fixed(
|| "flag_start",
self.flag_start,
idx,
|| Value::known(if flag_start { F::ONE } else { F::ZERO }),
)?;
reg.assign_fixed(
|| "flag_round",
self.flag_round,
idx,
|| Value::known(if flag_round { F::ONE } else { F::ZERO }),
)?;
reg.assign_fixed(
|| "flag_final",
self.flag_final,
idx,
|| Value::known(if flag_final { F::ONE } else { F::ZERO }),
)?;
reg.assign_fixed(|| "rndc0", self.rndc[0], idx, || Value::known(rndc[0]))?;
reg.assign_fixed(|| "rndc1", self.rndc[1], idx, || Value::known(rndc[1]))?;
reg.assign_fixed(|| "rndc2", self.rndc[2], idx, || Value::known(rndc[2]))?;
reg.assign_advice(|| "cols", self.cols[0], idx, || Value::known(cols[0]))?;
reg.assign_advice(|| "cols", self.cols[1], idx, || Value::known(cols[1]))?;
reg.assign_advice(|| "cols", self.cols[2], idx, || Value::known(cols[2]))?;
reg.assign_advice(|| "inp1", self.inp1, idx, || Value::known(inp[0]))?;
reg.assign_advice(|| "inp2", self.inp2, idx, || Value::known(inp[1]))?;
Ok(())
}To assign the entire table we create a function which takes a list of pairs of elements to be hashed and fills the table accordingly. All it does is hash each pair, round-by-round and fill in the rows of the table sequentially. There is one special row however: the first row is the all-zero row (all the flags are set to 0 as well), this is to enable the lookup of a "dummy" value whenever the Poseidon gate is disabled.
fn populate(
&self,
layouter: &mut impl Layouter<F>,
inputs: Vec<(F, F)>,
) -> Result<(), plonk::Error> {
// ensure padded
assert_eq!(inputs.len(), MAX_OPS_POSEIDON);
// assign poseidon table
layouter.assign_region(
|| "poseidon",
|mut reg| {
let mut st = [F::ZERO; WIDTH];
let mut inp = [F::ZERO; 2];
let mut nxt = 0;
// zero row
{
self.assign_row(
nxt,
&mut reg,
false,
false,
false,
[F::ZERO, F::ZERO, F::ZERO],
[F::ZERO, F::ZERO, F::ZERO],
[F::ZERO, F::ZERO],
)?;
nxt += 1;
}
for op in 0..MAX_OPS_POSEIDON {
// apply rounds
for r in 0..ROUNDS {
// load input
if r == 0 {
inp = [inputs[op].0, inputs[op].1];
st[0] = inp[0];
st[1] = inp[1];
st[2] = F::ZERO;
}
self.assign_row(
nxt,
&mut reg,
r == 0,
r > 0,
false,
self.round_constants[r],
st,
inp,
)?;
// apply poseidon round (out of circuit)
st = poseidon_round(&self.matrix, &self.round_constants[r], st);
// next row
nxt += 1;
}
// output
self.assign_row(
nxt,
&mut reg,
false,
false,
true,
[F::ZERO, F::ZERO, F::ZERO],
st,
inp,
)?;
nxt += 1;
}
Ok(())
},
)?;
Ok(())
}Note that when generating the verification key, this function will be run on junk values:
the inputs are completely arbitrary and the state of the Poseidon hash function does not matter.
The flags and round constants are fixed however.
The Poseidon Chip
At this point we have a table, guaranteed to contain correct invocations of the Poseidon hash function. Now we need to create a chip that can look up the entries (input/output pairs) in the table dynamically so we can "use the hash function" in a circuit.
Configuration
Towards this end, we define a chip responsible for looking up the Poseidon table:
#[derive(Clone, Debug)]
pub struct PoseidonChip<F: Field> {
inputs: RefCell<Vec<(F, F)>>,
sel: Selector,
tbl: PoseidonTable<F>,
in1: Column<Advice>,
in2: Column<Advice>,
out: Column<Advice>,
on: Column<Advice>,
}The fields are mostly self-explanatory, but here is a brief overview:
-
inputsis a simple way for us to collect all the inputs to the Poseidon hash function we encounter during witness generation. Whenever we are asked to hash a pair of values \( (x, y) \), we simply hash them out-of-circuit \( \mathsf{Hash}(x, y) \) then we add them to this list. -
selis just a selector to turn on this chip at the current offset. -
tblis the Poseidon table we constructed earlier. -
in1andin2are the inputs to the Poseidon hash function. -
outis the output of the Poseidon hash function. -
onis the flag that determines whether the Poseidon chip is enabled or not. Unlike a selector, which is constant, this can be toggled on and off dynamically (it's anAdvicecolumn).
The gates of the Poseidon chip are where the magic happens:
impl<F: Field> PoseidonChip<F> {
fn configure(meta: &mut ConstraintSystem<F>) -> Self {
let sel = meta.complex_selector();
let in1 = meta.advice_column();
let in2 = meta.advice_column();
let out = meta.advice_column();
let on = meta.advice_column();
let tbl = PoseidonTable::new(meta);
meta.enable_equality(in1);
meta.enable_equality(in2);
meta.enable_equality(out);
meta.enable_equality(on);
meta.create_gate("bit", |meta| {
let on = meta.query_advice(on, Rotation::cur());
let sel = meta.query_selector(sel);
vec![
sel * on.clone() * (on.clone() - Expression::Constant(F::ONE)), //
]
});
meta.lookup_any("poseidon_lookup", |cells| {
let on = cells.query_advice(on, Rotation::cur());
let sel = cells.query_selector(sel);
let in1 = cells.query_advice(in1, Rotation::cur());
let in2 = cells.query_advice(in2, Rotation::cur());
let out = cells.query_advice(out, Rotation::cur());
let do_lookup = on * sel;
let table = tbl.table_expr(cells);
// (1, in1, in2, out) in PoseidonTable
vec![
(do_lookup.clone() * Expression::Constant(F::ONE), table.flag),
(do_lookup.clone() * in1.clone(), table.inp1),
(do_lookup.clone() * in2.clone(), table.inp2),
(do_lookup.clone() * out.clone(), table.out),
]
});
Self {
sel,
tbl,
in1,
in2,
out,
on,
inputs: RefCell::new(Vec::new()),
}
}The first constraint is pretty simple: it simply enforces that on is a boolean value whenever sel is set to 1.
The poseidon_lookup "lookup_any" constraint is where the actual lookup happens:
- We read
onat the current offset. - We read
selat the current offset. - We read
in1at the current offset. - We read
in2at the current offset. - We read
outat the current offset.
We then define do_lookup = sel * on, which means that:
$$ \text{do_lookup} = 1 \iff \text{sel} = 1 \land \text{on} = 1 $$
This dynamic value will be used to turn the lookup "on" and "off".
In order for us to access the Poseidon table, we need to gain access to its columns,
to do this we follow the approach of PSE and create a little helper which reads the column expressions.
This is done by let table = tbl.table_expr(cells); and
inside table_expr we simply query the columns at the current offset and return the resulting expressions:
fn table_expr(&self, meta: &mut VirtualCells<F>) -> PoseidonExprs<F> {
PoseidonExprs {
flag: meta.query_any(self.flag_final, Rotation::cur()),
inp1: meta.query_any(self.inp1, Rotation::cur()),
inp2: meta.query_any(self.inp2, Rotation::cur()),
out: meta.query_any(self.cols[0], Rotation::cur()),
}
}With that out of the way, we can now define the actual lookup:
when do_lookup = 1 the lookup requires that the row (1, inp1, inp2, out) is in the columns (flag_final, inp1, inp2, col1) of the Poseidon table.
In other words: the inputs/output pair is from a row which has been marked by flag_final = 1 i.e. for which the Poseidon hash function has been completely evaluated.
If we did not include flag_final in the lookup, the prover would be able to lookup any row in the table,
not just the ones corresponding to the full evaluation of the Poseidon hash function.
For instance, he could lookup the first row of a Poseidon application:
| flag_start | flag_round | flag_final | inp1 | inp2 | rndc1 | rndc2 | rndc3 | col1 | col2 | col3 |
|---|---|---|---|---|---|---|---|---|---|---|
| 1 | 1 | 0 | x | y | a1 | b1 | c1 | x | y | 0 |
This row does not represent a complete hash computation, but only the initial state. The prover could then claim that this initial state is the result of the hash function, which would yield trivial collisions: \( \mathsf{Hash}(x, y) = x = \mathsf{Hash}(x, y') \) for any \( y' \).
The flag flag_final is used to mark results "ready for consumption" avoiding this issue.
Synthesizing
What remains is to use our new Poseidon chip in a circuit. To do this we define a function which creates a new region and assigns the output appropriately:
fn hash(
&self,
layouter: &mut impl Layouter<F>,
on: AssignedCell<F, F>,
in1: AssignedCell<F, F>,
in2: AssignedCell<F, F>,
) -> Result<AssignedCell<F, F>, plonk::Error> {
// store inputs
in1.value().and_then(|in1| {
in2.value()
.map(|in2| self.inputs.borrow_mut().push((*in1, *in2)))
});
layouter.assign_region(
|| "poseidon",
|mut reg| {
self.sel.enable(&mut reg, 0)?;
on.copy_advice(|| "on", &mut reg, self.on, 0)?;
in1.copy_advice(|| "in1", &mut reg, self.in1, 0)?;
in2.copy_advice(|| "in2", &mut reg, self.in2, 0)?;
let hsh = in1
.value()
.and_then(|in1| in2.value().map(|in2| self.tbl.hash(*in1, *in2)));
// if on = 0, hsh = 0
let hsh = on.value().and_then(|on| hsh.map(|hsh| hsh * on));
let out = reg.assign_advice(|| "out", self.out, 0, || hsh)?;
Ok(out)
},
)
}The hash function stores the inputs into inputs,
computes the Poseidon hash function out-of-circuit,
and assigns the inputs/output pairs of the Poseidon chip.
Finally, we turn on the selector sel for the Poseidon chip (lookup).
This constrains the inputs/output pair to be in the Poseidon table,
which will only be the case if the Poseidon hash function was correctly evaluated out-of-circuit.
After the last hash invocation, we need to finalize the Poseidon chip:
fn finalize(self, layouter: &mut impl Layouter<F>) -> Result<(), plonk::Error> {
let mut inputs = self.inputs.borrow().clone();
while inputs.len() < MAX_OPS_POSEIDON {
inputs.push((F::ZERO, F::ZERO));
}
self.tbl.populate(layouter, inputs)
}Which simply pads the inputs vector with dummy values to hash, before populating the Poseidon table.
The overall use of the Poseidon chip is as follows:
impl<F: Field> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit { _ph: PhantomData }
}
#[allow(unused_variables)]
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let poseidon = PoseidonChip::configure(meta);
let free = meta.advice_column();
meta.enable_equality(free);
TestConfig { poseidon, free }
}
#[allow(unused_variables)]
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), plonk::Error> {
let hashes = vec![(F::ZERO, F::ZERO); MAX_OPS_POSEIDON];
let in1 = layouter.assign_region(
|| "free1",
|mut region| {
region.assign_advice(
|| "free", //
config.free,
0,
|| Value::known(F::ONE),
)
},
)?;
let in2 = layouter.assign_region(
|| "free2",
|mut region| {
region.assign_advice(
|| "free", //
config.free,
0,
|| Value::known(F::ONE),
)
},
)?;
let on = layouter.assign_region(
|| "free3",
|mut region| {
region.assign_advice(
|| "free", //
config.free,
0,
|| Value::known(F::ONE),
)
},
)?;
// populate poseidon
let out = config.poseidon.hash(&mut layouter, on, in1, in2)?;
println!("hash done: {:?}", out);
config.poseidon.finalize(&mut layouter)?;
Ok(())
}
}Which should be familiar by now:
- We create three free variables
in1,in2, andon. - We hash the inputs using the Poseidon chip.
- We finalize the Poseidon chip.
Of course in a real application, the variables in1, in2, and on would likely be constrained by other parts of the circuit.
Exercises
When opening leaves in a Merkle tree, you will often end up computing the same hash multiple times. For instance, consider the tree below:
And suppose we want to open leaf D and C.
Verifying the inclusion proof of C requires computing:
- \( \mathsf{Hash}(C, D) \)
- \( \mathsf{Hash}(A, B) \)
And opening D requires computing the same hashes:
- \( \mathsf{Hash}(C, D) \)
- \( \mathsf{Hash}(A, B) \)
Even in the case where C and F are opened, the hash \( \mathsf{Hash}(A, B) \) is still computed twice...
Would it not be nice if we could only compute each hash once inside the circuit?
Well that is actually pretty easy given what we have learned so far.
Exercise: Optimize your Merkle tree chip to only compute each hash once, deduplicating identical hashes.
Exercise: Implement an "conditional AES" circuit, where the AES encryption is only performed if a condition is true:
$$ \mathsf{ConditionalAES}(b, k, x) = \begin{cases} \mathsf{AES128}(k, x) & \text{if } b = 1 \\ x & \text{if } b = 0 \end{cases} $$
This requires combining static and dynamic lookups.
Hint
Hint
You can either combine the table for the AES rounds with the key schedule table, or do lookups across the two dynamic tables. The first is the easier option.
Challenges
"And what is the use of a book," thought Alice, "without pictures or conversations?"
Because of how PlonK works, it is trivial to add multiple "rounds of interaction" in which the prover commits to some values, the verifier sends a challenge and the prover commits to some more values, etc. This back and forth can be repeated essentially for as many rounds as you like, Halo2 (as implemented) supports three such "phases" of interaction.
Sticking with the spreadsheet analogy, you can think of the "phases" as the prover and verifier passing the spreadsheet back and forth while taking turns to fill in values: first the prover fills out some columns in the spreadsheet, then the verifier fills out some columns, then the prover fills out some more columns, etc.
Configuration of Challenges
In Halo2, the "challenges" are used by allocating a Challenge
which acts very similarly to the columns we have seen so far:
You can think of Challenge as a column where every row contains the same random challenge value.
They are allocated with a "Phase" using challenge_usable_after:
let alpha = meta.challenge_usable_after(FirstPhase);In the example above, we are asking for a challenge that is usable after the first phase of the interaction.
The first phase is the "default": it is the implicit phase that we have been using to allocate all the Advice columns so far:
it is the first time the prover gets to fill in values in the spreadsheet.
This means that only after assigning values to these Advice columns,
does the prover learn the challenge value (the random value assigned to alpha):
so the first phase values cannot depend on the challenge alpha in our example.
Stop and think.
Does it make sense to have other column types, besides Advice, in any other phases?
Before we continue with the challenges, a natural question is:
how do we assign Advice columns after the challenge?
In other words, how do we allow the prover to "respond" to the challenge alpha?
It's straightforward: you simply use meta.advice_column_in(SecondPhase)
instead of meta.advice_column() when allocating the column.
let w0_phase2 = meta.advice_column_in(SecondPhase);These later phase advice columns act just like the first phase advice columns we have seen so far.
As an example, let us create a very simple chip which simply enforces that an advice cell takes the value of the challenge alpha.
In that case, configuration should look something like this:
#[derive(Clone, Debug)]
struct ChallengeChip<F: Field> {
q_enable: Selector,
challenge: Challenge,
advice: Column<Advice>,
_ph: PhantomData<F>,
}
impl<F: Field> ChallengeChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>, //
challenge: Challenge,
w0: Column<Advice>,
) -> Self {
let q_challenge = meta.selector();
meta.create_gate("eq_challenge", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let chal = meta.query_challenge(challenge);
let q_challenge = meta.query_selector(q_challenge);
vec![q_challenge * (w0 - chal)]
});
Self {
q_enable: q_challenge,
challenge,
advice: w0,
_ph: PhantomData,
}
}
}This chip takes a Challenge and an Advice column and enforces that the advice column is equal to the challenge.
For this to work the Advice column must be allocated in a phase after the challenge,
in our case, the SecondPhase:
impl<F: PrimeField> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit { _ph: PhantomData }
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// let q_enable = meta.fixed_column();
let w0 = meta.advice_column();
// enable equality constraints
meta.enable_equality(w0);
let alpha = meta.challenge_usable_after(FirstPhase);
let w0_phase2 = meta.advice_column_in(SecondPhase);
meta.enable_equality(w0_phase2);
TestConfig {
challenge_chip: ChallengeChip::configure(meta, alpha, w0_phase2),
_ph: PhantomData,
}
}
...Synthesis of Challenges
So far the prover has had complete knowledge of every value in the circuit from the beginning of proving: synthesize was able to assign all values in one pass over the circuit.
This now has to change.
We will need to do multiple passes over the circuit. The reason is that the prover cannot know the challenge value until after the first phase. So we need to do:
- A pass over the circuit, assigning all the
FirstPhaseadvice columns. - Obtain the first challenge value (
alphain our example). - Then do another pass over the circuit, assigning all the
SecondPhaseadvice columns which might depend on the challenge value. - Obtain the second challenge value.
- etc.
Luckily, we already have a nice way to "partially" assign the witness of a circuit:
remember that Value is a sum type that can be either Value::known or Value::unknown.
This is used to access the value of a challenge during synthesis:
the layouter is given a method get_challenge which takes a Challenge and returns a Value,
if the challenge is available during this pass the value will be Value::known otherwise it will be Value::unknown.
#![allow(unused)] fn main() { let chal = layouter.get_challenge(self.challenge); }
This allows us to compute Values for the second phase:
these will be Value::unknown during the first pass and Value::known during the second pass.
For instance:
#![allow(unused)] fn main() { let some_witness = chal.map(|chal| { // do something with the challenge ... }) }
In this case, some_witness will be a Value::known during the second pass and a Value::unknown during the first pass
since chal is a Value::unknown (the Value equivalent of None).
impl<F: Field> ChallengeChip<F> {
fn challenge(
&self, //
layouter: &mut impl Layouter<F>,
) -> Result<AssignedCell<F, F>, Error> {
let chal = layouter.get_challenge(self.challenge);
layouter.assign_region(
|| "challenge",
|mut region| region.assign_advice(|| "chl", self.advice, 0, || chal),
)
}
}When we use it during synthesis, we can now access the challenge value:
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let chal: AssignedCell<F, F> = config.challenge_chip.challenge(&mut layouter)?;
Ok(())
}Exercise
So far, so simple. Now let's see what challenges can do for us: we will use them to create a circuit which efficiently verifies Sudoku solutions and we will use (two copies) of the Arithmetic chip we developed earlier.
Hint
Hint
To verify that every row/column/diagonal/3x3 square must contain exactly one of each number 1-9, you can use the following trick:
Use the fact that for a set \( C \) if you define the polynomials: \[ f(X) = \prod_{i=1}^9 (X - i) \] \[ g(X) = \prod_{c \in C} (X - c) \]
Then \[ C = \{ 1, 2, 3, 4, 5, 6, 7, 8, 9 \} \iff f(X) = g(X) \] You can then check \(f(X) = g(X) \) by evaluating the polynomials at a random challenge \( \alpha \) and enforcing \( f(\alpha) = g(\alpha) \)
#[derive(Clone, Debug)]
struct ChallengeChip<F: Field> {
q_enable: Selector,
challenge: Challenge,
advice: Column<Advice>,
_ph: PhantomData<F>,
}
impl<F: Field> ChallengeChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>, //
challenge: Challenge,
w0: Column<Advice>,
) -> Self {
let q_challenge = meta.selector();
meta.create_gate("eq_challenge", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let chal = meta.query_challenge(challenge);
let q_challenge = meta.query_selector(q_challenge);
vec![q_challenge * (w0 - chal)]
});
Self {
q_enable: q_challenge,
challenge,
advice: w0,
_ph: PhantomData,
}
}
fn challenge(
&self, //
layouter: &mut impl Layouter<F>,
) -> Result<Variable<F>, Error> {
let chal = layouter.get_challenge(self.challenge);
layouter.assign_region(
|| "challenge",
|mut region| {
self.q_enable.enable(&mut region, 0)?;
let val = region.assign_advice(|| "w0", self.advice, 0, || chal)?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
}Solutions
Full solution:
use std::{
marker::PhantomData,
ops::{Add, Mul, Neg, Sub},
};
use halo2_proofs::{
circuit::{AssignedCell, Layouter, SimpleFloorPlanner, Value},
dev::MockProver,
plonk::{
Advice,
Challenge,
Circuit,
Column, //
ConstraintSystem,
Error,
Expression,
FirstPhase,
Fixed,
SecondPhase,
Selector,
},
poly::Rotation,
};
use ff::{Field, PrimeField};
const DIM: usize = 9;
const SQR: usize = 3;
// Sudoku puzzle to solve
const SUDOKU: [[u8; DIM]; DIM] = [
[5, 3, 0, 0, 7, 0, 0, 0, 0],
[6, 0, 0, 1, 9, 5, 0, 0, 0],
[0, 9, 8, 0, 0, 0, 0, 6, 0],
[8, 0, 0, 0, 6, 0, 0, 0, 3],
[4, 0, 0, 8, 0, 3, 0, 0, 1],
[7, 0, 0, 0, 2, 0, 0, 0, 6],
[0, 6, 0, 0, 0, 0, 2, 8, 0],
[0, 0, 0, 4, 1, 9, 0, 0, 5],
[0, 0, 0, 0, 8, 0, 0, 7, 9],
];
struct TestCircuit<F: Field> {
_ph: PhantomData<F>,
suduko: [[u8; DIM]; DIM],
solution: Value<[[u8; DIM]; DIM]>,
}
#[derive(Clone, Debug)]
struct Variable<F: Field> {
mul: F,
add: F,
val: AssignedCell<F, F>,
}
impl<F: Field> Variable<F> {
fn value(&self) -> Value<F> {
self.val.value().map(|v| self.mul * v + self.add)
}
}
impl<F: Field> Neg for Variable<F> {
type Output = Self;
fn neg(self) -> Self {
Self {
mul: -self.mul,
add: -self.add,
val: self.val,
}
}
}
impl<F: Field> Sub<F> for Variable<F> {
type Output = Self;
fn sub(self, rhs: F) -> Self {
Self {
mul: self.mul,
add: self.add - rhs,
val: self.val,
}
}
}
impl<F: Field> Add<F> for Variable<F> {
type Output = Self;
fn add(self, rhs: F) -> Self {
Self {
mul: self.mul,
add: self.add + rhs,
val: self.val,
}
}
}
impl<F: Field> Mul<F> for Variable<F> {
type Output = Self;
fn mul(self, rhs: F) -> Self {
Self {
mul: self.mul * rhs,
add: self.add * rhs,
val: self.val,
}
}
}
// ANCHOR: challenge_chip
#[derive(Clone, Debug)]
struct ChallengeChip<F: Field> {
q_enable: Selector,
challenge: Challenge,
advice: Column<Advice>,
_ph: PhantomData<F>,
}
impl<F: Field> ChallengeChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>, //
challenge: Challenge,
w0: Column<Advice>,
) -> Self {
let q_challenge = meta.selector();
meta.create_gate("eq_challenge", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let chal = meta.query_challenge(challenge);
let q_challenge = meta.query_selector(q_challenge);
vec![q_challenge * (w0 - chal)]
});
Self {
q_enable: q_challenge,
challenge,
advice: w0,
_ph: PhantomData,
}
}
fn challenge(
&self, //
layouter: &mut impl Layouter<F>,
) -> Result<Variable<F>, Error> {
let chal = layouter.get_challenge(self.challenge);
layouter.assign_region(
|| "challenge",
|mut region| {
self.q_enable.enable(&mut region, 0)?;
let val = region.assign_advice(|| "w0", self.advice, 0, || chal)?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
}
// ANCHOR_END: challenge_chip
#[derive(Clone, Debug)]
struct ArithmeticChip<F: Field> {
_ph: PhantomData<F>,
q_arith: Selector,
cm: Column<Fixed>,
c0: Column<Fixed>,
c1: Column<Fixed>,
c2: Column<Fixed>,
cc: Column<Fixed>,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
}
impl<F: Field> ArithmeticChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>,
w0: Column<Advice>,
w1: Column<Advice>,
w2: Column<Advice>,
c0: Column<Fixed>,
c1: Column<Fixed>,
c2: Column<Fixed>,
cm: Column<Fixed>,
cc: Column<Fixed>,
) -> Self {
let q_arith = meta.complex_selector();
// define arithmetic gate
meta.create_gate("arith", |meta| {
let w0 = meta.query_advice(w0, Rotation::cur());
let w1 = meta.query_advice(w1, Rotation::cur());
let w2 = meta.query_advice(w2, Rotation::cur());
let c0 = meta.query_fixed(c0, Rotation::cur());
let c1 = meta.query_fixed(c1, Rotation::cur());
let c2 = meta.query_fixed(c2, Rotation::cur());
let cm = meta.query_fixed(cm, Rotation::cur());
let cc = meta.query_fixed(cc, Rotation::cur());
let q_arith = meta.query_selector(q_arith);
// define the arithmetic expression
//
// w0 * c0 + w1 * c1 + w2 * c2 + cm * (w0 * w1) + cc
let expr = Expression::Constant(F::ZERO);
let expr = expr + c0 * w0.clone();
let expr = expr + c1 * w1.clone();
let expr = expr + c2 * w2.clone();
let expr = expr + cm * (w0 * w1);
let expr = expr + cc;
vec![q_arith * expr]
});
Self {
_ph: PhantomData,
q_arith,
cm,
c0,
c1,
c2,
cc,
w0,
w1,
w2,
}
}
/// Multiply two variables
fn mul(
&self,
layouter: &mut impl Layouter<F>,
lhs: &Variable<F>,
rhs: &Variable<F>,
) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "mul",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
// (c0 * w0 + cc1) * (c1 * w1 + cc2)
// c0 * c1 * (w0 * w1) + c0 * cc2 * w0 + c1 * cc1 * w1 + cc1 * cc2
lhs.val.copy_advice(|| "lhs", &mut region, self.w0, 0)?;
rhs.val.copy_advice(|| "rhs", &mut region, self.w1, 0)?;
let val =
region.assign_advice(|| "res", self.w2, 0, || lhs.value() * rhs.value())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(lhs.mul * rhs.add))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(rhs.mul * lhs.add))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(lhs.add * rhs.add))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(lhs.mul * rhs.mul))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
/// Add two variables
fn add(
&self,
layouter: &mut impl Layouter<F>,
lhs: &Variable<F>,
rhs: &Variable<F>,
) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "add",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
lhs.val.copy_advice(|| "lhs", &mut region, self.w0, 0)?;
rhs.val.copy_advice(|| "rhs", &mut region, self.w1, 0)?;
let val =
region.assign_advice(|| "res", self.w2, 0, || lhs.value() + rhs.value())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(lhs.mul))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(rhs.mul))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(lhs.add + rhs.add))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
fn sub(
&self,
layouter: &mut impl Layouter<F>,
lhs: &Variable<F>,
rhs: &Variable<F>,
) -> Result<Variable<F>, Error> {
let minus = -rhs.clone();
self.add(layouter, lhs, &minus)
}
/// Allocate a free variable.
fn free(&self, layouter: &mut impl Layouter<F>, value: Value<F>) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "free",
|mut region| {
// no need to turn on anything
let val = region.assign_advice(|| "free", self.w0, 0, || value)?;
region.assign_advice(|| "junk1", self.w1, 0, || Value::known(F::ZERO))?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
fn constant(&self, layouter: &mut impl Layouter<F>, constant: F) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "constant",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
let val = region.assign_advice(|| "val", self.w0, 0, || Value::known(constant))?;
region.assign_advice(|| "junk1", self.w1, 0, || Value::known(F::ZERO))?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(F::ONE))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(-constant))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val,
})
},
)
}
fn eq(
&self,
layouter: &mut impl Layouter<F>,
lhs: &Variable<F>,
rhs: &Variable<F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "eq",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
lhs.val.copy_advice(|| "lhs", &mut region, self.w0, 0)?;
rhs.val.copy_advice(|| "rhs", &mut region, self.w1, 0)?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
let delta = lhs.add - rhs.add;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(lhs.mul))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(-rhs.mul))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(delta))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(())
},
)
}
/// Assert equal
fn eq_consant(
&self,
layouter: &mut impl Layouter<F>,
constant: F,
variable: Variable<F>,
) -> Result<(), Error> {
layouter.assign_region(
|| "eq_constant",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
variable
.val
.copy_advice(|| "val", &mut region, self.w0, 0)?;
let delta = variable.add - constant;
region.assign_advice(|| "junk1", self.w1, 0, || Value::known(F::ZERO))?;
region.assign_advice(|| "junk2", self.w2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(variable.mul))?;
region.assign_fixed(|| "c1", self.c1, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c2", self.c2, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(delta))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ZERO))?;
Ok(())
},
)
}
/// Allocate a bit-constrained variable.
fn bit(
&self,
layouter: &mut impl Layouter<F>,
value: Value<bool>,
) -> Result<Variable<F>, Error> {
layouter.assign_region(
|| "bit",
|mut region| {
// turn on the arithmetic gate
self.q_arith.enable(&mut region, 0)?;
// (v1 - 1) * v1 = v1^2 - v1
let w0 = region.assign_advice(
|| "bit0",
self.w0,
0,
|| value.map(|b| if b { F::ONE } else { F::ZERO }),
)?;
let w1 = region.assign_advice(
|| "bit1",
self.w1,
0,
|| value.map(|b| if b { F::ONE } else { F::ZERO }),
)?;
region.assign_advice(|| "junk", self.w2, 0, || Value::known(F::ZERO))?;
region.constrain_equal(w0.cell(), w1.cell())?;
region.assign_fixed(|| "c0", self.c0, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "c1", self.c0, 0, || Value::known(-F::ONE))?;
region.assign_fixed(|| "c2", self.c0, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cc", self.cc, 0, || Value::known(F::ZERO))?;
region.assign_fixed(|| "cm", self.cm, 0, || Value::known(F::ONE))?;
Ok(Variable {
mul: F::ONE,
add: F::ZERO,
val: w0,
})
},
)
}
}
#[derive(Clone, Debug)]
struct TestConfig<F: Field + Clone> {
_ph: PhantomData<F>,
phase1_chip: ArithmeticChip<F>,
phase2_chip: ArithmeticChip<F>,
challenge_chip: ChallengeChip<F>,
}
impl<F: PrimeField> Circuit<F> for TestCircuit<F> {
type Config = TestConfig<F>;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
TestCircuit {
_ph: PhantomData,
solution: Value::unknown(),
suduko: SUDOKU,
}
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// let q_enable = meta.fixed_column();
let w0 = meta.advice_column();
let w1 = meta.advice_column();
let w2 = meta.advice_column();
let c0 = meta.fixed_column();
let c1 = meta.fixed_column();
let c2 = meta.fixed_column();
let cc = meta.fixed_column();
let cm = meta.fixed_column();
// enable equality constraints
meta.enable_equality(w0);
meta.enable_equality(w1);
meta.enable_equality(w2);
// ANCHOR: challenge_alloc
let alpha = meta.challenge_usable_after(FirstPhase);
// ANCHOR_END: challenge_alloc
let phase1_chip = ArithmeticChip::configure(meta, w0, w1, w2, c0, c1, c2, cc, cm);
// ANCHOR: phase2_alloc
let w0_phase2 = meta.advice_column_in(SecondPhase);
let w1_phase2 = meta.advice_column_in(SecondPhase);
let w2_phase2 = meta.advice_column_in(SecondPhase);
// ANCHOR_END: phase2_alloc
meta.enable_equality(w0_phase2);
meta.enable_equality(w1_phase2);
meta.enable_equality(w2_phase2);
let phase2_chip =
ArithmeticChip::configure(meta, w0_phase2, w1_phase2, w2_phase2, c0, c1, c2, cc, cm);
let challenge_chip = ChallengeChip::configure(meta, alpha, w0_phase2);
TestConfig {
_ph: PhantomData,
phase1_chip,
phase2_chip,
challenge_chip,
}
}
fn synthesize(
&self,
config: Self::Config, //
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
// load/fix the suduko
let mut cells = vec![];
for i in 0..DIM {
let mut row = vec![];
for j in 0..DIM {
let cell = match self.suduko[i][j] {
0 => config.phase1_chip.free(
&mut layouter,
self.solution.map(|sol| F::from_u128(sol[i][j] as u128)),
),
fixed => config
.phase1_chip
.constant(&mut layouter, F::from_u128(fixed as u128)),
}?;
row.push(cell);
}
cells.push(row)
}
// distinct constraints
let mut distinct = vec![];
// row constraints
for row in 0..DIM {
distinct.push(
cells[row]
.iter()
.map(|cell| cell.clone())
.collect::<Vec<_>>(),
);
}
// column constraints
for col in 0..DIM {
distinct.push(cells.iter().map(|row| row[col].clone()).collect::<Vec<_>>());
}
// block constraints
for i in 0..DIM / SQR {
for j in 0..DIM / SQR {
let row = i * SQR;
let col = j * SQR;
let mut block = vec![];
for ii in 0..SQR {
for jj in 0..SQR {
block.push(cells[row + ii][col + jj].clone());
}
}
distinct.push(block);
}
}
assert_eq!(distinct.len(), 9 + 9 + 9);
// next phase
let alpha = config.challenge_chip.challenge(&mut layouter)?;
// allowed set of entries
let mut numbers = vec![];
for num in 1..=DIM {
numbers.push(
config
.phase2_chip
.constant(&mut layouter, F::from_u128(num as u128))?,
);
}
// eval the vanish poly over the numbers
let eval_known = eval_vanish(&mut layouter, &config.phase2_chip, &alpha, &numbers)?;
// eval the vanish poly over the distinct cells and check against eval_known
for dist in distinct.iter() {
let eval_check = eval_vanish(&mut layouter, &config.phase2_chip, &alpha, &dist)?;
config
.phase2_chip
.eq(&mut layouter, &eval_known, &eval_check)?;
}
Ok(())
}
}
fn eval_vanish<F: PrimeField>(
layouter: &mut impl Layouter<F>,
chip: &ArithmeticChip<F>,
alpha: &Variable<F>,
terms: &[Variable<F>],
) -> Result<Variable<F>, Error> {
let mut poly = chip.constant(layouter, F::ONE)?;
for term in terms.iter() {
let mono = chip.sub(layouter, term, alpha)?;
poly = chip.mul(layouter, &poly, &mono)?;
}
Ok(poly)
}
fn main() {
use halo2_proofs::halo2curves::bn256::Fr;
// our sudoku solution
const SOLUTION: [[u8; DIM]; DIM] = [
[5, 3, 4, 6, 7, 8, 9, 1, 2],
[6, 7, 2, 1, 9, 5, 3, 4, 8],
[1, 9, 8, 3, 4, 2, 5, 6, 7],
[8, 5, 9, 7, 6, 1, 4, 2, 3],
[4, 2, 6, 8, 5, 3, 7, 9, 1],
[7, 1, 3, 9, 2, 4, 8, 5, 6],
[9, 6, 1, 5, 3, 7, 2, 8, 4],
[2, 8, 7, 4, 1, 9, 6, 3, 5],
[3, 4, 5, 2, 8, 6, 1, 7, 9],
];
// run the MockProver
let circuit = TestCircuit::<Fr> {
_ph: PhantomData,
solution: Value::known(SOLUTION),
suduko: SUDOKU,
};
let prover = MockProver::run(10, &circuit, vec![]).unwrap();
prover.verify().unwrap();
}Bonus: Circuit Architecture
We have seen a number of different techniques.
These exercises will help you explore when to use which technique.
Exercise: Optimizing multi-MSM.
Suppose the prover wants to demonstrate that he knows the discrete logarithm of points \( c_1, c_2, c_3 \) with respect to a set of base points \( \vec{G} \) of length \( n \).
$$ \begin{aligned} c_1 &= \langle \vec{w_1}, \vec{G} \rangle \\ c_2 &= \langle \vec{w_2}, \vec{G} \rangle \\ c_3 &= \langle \vec{w_3}, \vec{G} \rangle \\ \end{aligned} $$
Doing this naively would require three multi-scalar multiplications of length \( n \). However, there is a better way: this can be achieved with only one multi-scalar multiplication of length \( n \) and two scalar multiplications of length \( 1 \).
Architect a circuit which achieves this.
Exercise: The string machine.
We want to design a circuit for efficiently proving different string operations:
- Checking equality.
- String concatenation.
- Computing the length of a string.
- Substring extraction.
We want to support strings of variable length.
Help design chips for these operations.
- How should strings be represented / stored?
- Design a gate for checking equality of two strings.
- Design a gate for concatenating two strings.
- Design a gate for computing the length of a string.
- Design a gate for extracting a substring.
- How could you combine this with our regular expression matching circuit?
Hint
Hint
Use a challenge to compute fingerprints of each string.
Add a gate to ensure that the fingerprints are correctly computed.
Exercise: Battle Ships
Would it be cool if you could play Battle Ships over the internet without a trusted third party?
Design a circuit which allows two players to play Battle Ships: the idea is that the state of the game is stored in a commitment (e.g. a Poseidon hash) and the players take turns querying the state of the board.
At a high level, the circuit proves:
- That the assigment of ships to the board is valid
e.g. not overlapping and every ship is of the correct length. - The position queried by the other player is a hit or a miss.
The questions to ponder are:
- What public inputs are needed?
- How can you represent the board?
- How can you represent the ships?
- How do you prove that the ships are placed correctly?
- How do you prove that the position queried is a hit or a miss?