A simple example
Let's start with a simple circuit, to introduce you to the common APIs and how they are used. The circuit will take a public input , and will prove knowledge of two private inputs and such that
Define instructions
Firstly, we need to define the instructions that our circuit will rely on. Instructions are the boundary between high-level gadgets and the low-level circuit operations. Instructions may be as coarse or as granular as desired, but in practice you want to strike a balance between an instruction being large enough to effectively optimize its implementation, and small enough that it is meaningfully reusable.
For our circuit, we will use three instructions:
- Load a private number into the circuit.
- Multiply two numbers.
- Expose a number as a public input to the circuit.
We also need a type for a variable representing a number. Instruction interfaces provide associated types for their inputs and outputs, to allow the implementations to represent these in a way that makes the most sense for their optimization goals.
trait NumericInstructions<F: FieldExt>: Chip<F> {
/// Variable representing a number.
type Num;
/// Loads a number into the circuit as a private input.
fn load_private(&self, layouter: impl Layouter<F>, a: Option<F>) -> Result<Self::Num, Error>;
/// Returns `c = a * b`.
fn mul(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error>;
/// Exposes a number as a public input to the circuit.
fn expose_public(&self, layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error>;
}
Define a chip implementation
For our circuit, we will build a chip that provides the above numeric instructions for a finite field.
/// The chip that will implement our instructions! Chips store their own
/// config, as well as type markers if necessary.
struct FieldChip<F: FieldExt> {
config: FieldConfig,
_marker: PhantomData<F>,
}
Every chip needs to implement the Chip trait. This defines the properties of the chip
that a Layouter may rely on when synthesizing a circuit, as well as enabling any initial
state that the chip requires to be loaded into the circuit.
impl<F: FieldExt> Chip<F> for FieldChip<F> {
type Config = FieldConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
Configure the chip
The chip needs to be configured with the columns, permutations, and gates that will be required to implement all of the desired instructions.
/// Chip state is stored in a config struct. This is generated by the chip
/// during configuration, and then stored inside the chip.
#[derive(Clone, Debug)]
struct FieldConfig {
/// For this chip, we will use two advice columns to implement our instructions.
/// These are also the columns through which we communicate with other parts of
/// the circuit.
advice: [Column<Advice>; 2],
// We need to create a permutation between our advice columns. This allows us to
// copy numbers within these columns from arbitrary rows, which we can use to load
// inputs into our instruction regions.
perm: Permutation,
// We need a selector to enable the multiplication gate, so that we aren't placing
// any constraints on cells where `NumericInstructions::mul` is not being used.
// This is important when building larger circuits, where columns are used by
// multiple sets of instructions.
s_mul: Selector,
// The selector for the public-input gate, which uses one of the advice columns.
s_pub: Selector,
}
impl<F: FieldExt> FieldChip<F> {
fn construct(config: <Self as Chip<F>>::Config) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
) -> <Self as Chip<F>>::Config {
let perm = Permutation::new(
meta,
&advice
.iter()
.map(|column| (*column).into())
.collect::<Vec<_>>(),
);
let s_mul = meta.selector();
let s_pub = meta.selector();
// Define our multiplication gate!
meta.create_gate("mul", |meta| {
// To implement multiplication, we need three advice cells and a selector
// cell. We arrange them like so:
//
// | a0 | a1 | s_mul |
// |-----|-----|-------|
// | lhs | rhs | s_mul |
// | out | | |
//
// Gates may refer to any relative offsets we want, but each distinct
// offset adds a cost to the proof. The most common offsets are 0 (the
// current row), 1 (the next row), and -1 (the previous row), for which
// `Rotation` has specific constructors.
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_selector(s_mul);
// Finally, we return the polynomial expressions that constrain this gate.
// For our multiplication gate, we only need a single polynomial constraint.
//
// The polynomial expressions returned from `create_gate` will be
// constrained by the proving system to equal zero. Our expression
// has the following properties:
// - When s_mul = 0, any value is allowed in lhs, rhs, and out.
// - When s_mul != 0, this constrains lhs * rhs = out.
vec![s_mul * (lhs * rhs + out * -F::one())]
});
// Define our public-input gate!
meta.create_gate("public input", |meta| {
// We choose somewhat-arbitrarily that we will use the second advice
// column for exposing numbers as public inputs.
let a = meta.query_advice(advice[1], Rotation::cur());
let p = meta.query_instance(instance, Rotation::cur());
let s = meta.query_selector(s_pub);
// We simply constrain the advice cell to be equal to the instance cell,
// when the selector is enabled.
vec![s * (p + a * -F::one())]
});
FieldConfig {
advice,
perm,
s_mul,
s_pub,
}
}
}
Implement chip traits
/// A variable representing a number.
#[derive(Clone)]
struct Number<F: FieldExt> {
cell: Cell,
value: Option<F>,
}
impl<F: FieldExt> NumericInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Option<F>,
) -> Result<Self::Num, Error> {
let config = self.config();
let mut num = None;
layouter.assign_region(
|| "load private",
|mut region| {
let cell = region.assign_advice(
|| "private input",
config.advice[0],
0,
|| value.ok_or(Error::SynthesisError),
)?;
num = Some(Number { cell, value });
Ok(())
},
)?;
Ok(num.unwrap())
}
fn mul(
&self,
mut layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config();
let mut out = None;
layouter.assign_region(
|| "mul",
|mut region: Region<'_, F>| {
// We only want to use a single multiplication gate in this region,
// so we enable it at region offset 0; this means it will constrain
// cells at offsets 0 and 1.
config.s_mul.enable(&mut region, 0)?;
// The inputs we've been given could be located anywhere in the circuit,
// but we can only rely on relative offsets inside this region. So we
// assign new cells inside the region and constrain them to have the
// same values as the inputs.
let lhs = region.assign_advice(
|| "lhs",
config.advice[0],
0,
|| a.value.ok_or(Error::SynthesisError),
)?;
let rhs = region.assign_advice(
|| "rhs",
config.advice[1],
0,
|| b.value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.perm, a.cell, lhs)?;
region.constrain_equal(&config.perm, b.cell, rhs)?;
// Now we can assign the multiplication result into the output position.
let value = a.value.and_then(|a| b.value.map(|b| a * b));
let cell = region.assign_advice(
|| "lhs * rhs",
config.advice[0],
1,
|| value.ok_or(Error::SynthesisError),
)?;
// Finally, we return a variable representing the output,
// to be used in another part of the circuit.
out = Some(Number { cell, value });
Ok(())
},
)?;
Ok(out.unwrap())
}
fn expose_public(&self, mut layouter: impl Layouter<F>, num: Self::Num) -> Result<(), Error> {
let config = self.config();
layouter.assign_region(
|| "expose public",
|mut region: Region<'_, F>| {
// Enable the public-input gate.
config.s_pub.enable(&mut region, 0)?;
// Load the output into the correct advice column.
let out = region.assign_advice(
|| "public advice",
config.advice[1],
0,
|| num.value.ok_or(Error::SynthesisError),
)?;
region.constrain_equal(&config.perm, num.cell, out)?;
// We don't assign to the instance column inside the circuit;
// the mapping of public inputs to cells is provided to the prover.
Ok(())
},
)
}
}
Build the circuit
Now that we have the instructions we need, and a chip that implements them, we can finally build our circuit!
/// The full circuit implementation.
///
/// In this struct we store the private input variables. We use `Option<F>` because
/// they won't have any value during key generation. During proving, if any of these
/// were `None` we would get an error.
#[derive(Default)]
struct MyCircuit<F: FieldExt> {
a: Option<F>,
b: Option<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
// Since we are using a single chip for everything, we can just reuse its config.
type Config = FieldConfig;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
// We create the two advice columns that FieldChip uses for I/O.
let advice = [meta.advice_column(), meta.advice_column()];
// We also need an instance column to store public inputs.
let instance = meta.instance_column();
FieldChip::configure(meta, advice, instance)
}
fn synthesize(
&self,
config: Self::Config,
mut layouter: impl Layouter<F>,
) -> Result<(), Error> {
let field_chip = FieldChip::<F>::construct(config);
// Load our private values into the circuit.
let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;
// We only have access to plain multiplication.
// We could implement our circuit as:
// asq = a*a
// bsq = b*b
// c = asq*bsq
//
// but it's more efficient to implement it as:
// ab = a*b
// c = ab^2
let ab = field_chip.mul(layouter.namespace(|| "a * b"), a, b)?;
let c = field_chip.mul(layouter.namespace(|| "ab * ab"), ab.clone(), ab)?;
// Expose the result as a public input to the circuit.
field_chip.expose_public(layouter.namespace(|| "expose c"), c)
}
}
Testing the circuit
halo2::dev::MockProver can be used to test that the circuit is working correctly. The
private and public inputs to the circuit are constructed as we will do to create a proof,
but by passing them to MockProver::run we get an object that can test every constraint
in the circuit, and tell us exactly what is failing (if anything).
// The number of rows in our circuit cannot exceed 2^k. Since our example
// circuit is very small, we can pick a very small value here.
let k = 3;
// Prepare the private and public inputs to the circuit!
let a = Fp::from(2);
let b = Fp::from(3);
let c = a.square() * b.square();
// Instantiate the circuit with the private inputs.
let circuit = MyCircuit {
a: Some(a),
b: Some(b),
};
// Arrange the public input. We expose the multiplication result in row 6
// of the instance column, so we position it there in our public inputs.
let mut public_inputs = vec![Fp::zero(); 1 << k];
public_inputs[6] = c;
// Given the correct public input, our circuit will verify.
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
assert_eq!(prover.verify(), Ok(()));
// If we try some other public input, the proof will fail!
public_inputs[6] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
assert_eq!(
prover.verify(),
Err(vec![VerifyFailure::Constraint {
constraint: ((1, "public input").into(), 0, "").into(),
row: 6,
}])
);
Full example
You can find the source code for this example here.