2021-04-19 06:25:32 -07:00
|
|
|
extern crate halo2;
|
|
|
|
|
|
|
|
use std::marker::PhantomData;
|
|
|
|
|
|
|
|
use halo2::{
|
|
|
|
arithmetic::FieldExt,
|
2021-06-21 11:10:59 -07:00
|
|
|
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
|
2021-07-08 11:47:51 -07:00
|
|
|
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
|
2021-04-19 06:25:32 -07:00
|
|
|
poly::Rotation,
|
|
|
|
};
|
|
|
|
|
2021-04-27 19:47:26 -07:00
|
|
|
// ANCHOR: field-instructions
|
2021-04-19 06:25:32 -07:00
|
|
|
/// A variable representing a number.
|
|
|
|
#[derive(Clone)]
|
|
|
|
struct Number<F: FieldExt> {
|
|
|
|
cell: Cell,
|
|
|
|
value: Option<F>,
|
|
|
|
}
|
|
|
|
|
|
|
|
trait FieldInstructions<F: FieldExt>: AddInstructions<F> + MulInstructions<F> {
|
|
|
|
/// Variable representing a number.
|
|
|
|
type Num;
|
|
|
|
|
|
|
|
/// Loads a number into the circuit as a private input.
|
|
|
|
fn load_private(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Option<F>,
|
|
|
|
) -> Result<<Self as FieldInstructions<F>>::Num, Error>;
|
|
|
|
|
|
|
|
/// Returns `d = (a + b) * c`.
|
|
|
|
fn add_and_mul(
|
|
|
|
&self,
|
|
|
|
layouter: &mut impl Layouter<F>,
|
|
|
|
a: <Self as FieldInstructions<F>>::Num,
|
|
|
|
b: <Self as FieldInstructions<F>>::Num,
|
|
|
|
c: <Self as FieldInstructions<F>>::Num,
|
|
|
|
) -> Result<<Self as FieldInstructions<F>>::Num, Error>;
|
|
|
|
|
|
|
|
/// Exposes a number as a public input to the circuit.
|
|
|
|
fn expose_public(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
num: <Self as FieldInstructions<F>>::Num,
|
2021-07-08 14:22:16 -07:00
|
|
|
row: usize,
|
2021-04-19 06:25:32 -07:00
|
|
|
) -> Result<(), Error>;
|
|
|
|
}
|
|
|
|
// ANCHOR_END: field-instructions
|
|
|
|
|
|
|
|
// ANCHOR: add-instructions
|
|
|
|
trait AddInstructions<F: FieldExt>: Chip<F> {
|
|
|
|
/// Variable representing a number.
|
|
|
|
type Num;
|
|
|
|
|
|
|
|
/// Returns `c = a + b`.
|
|
|
|
fn add(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error>;
|
|
|
|
}
|
|
|
|
// ANCHOR_END: add-instructions
|
|
|
|
|
|
|
|
// ANCHOR: mul-instructions
|
|
|
|
trait MulInstructions<F: FieldExt>: Chip<F> {
|
|
|
|
/// Variable representing a number.
|
|
|
|
type Num;
|
|
|
|
|
|
|
|
/// Returns `c = a * b`.
|
|
|
|
fn mul(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error>;
|
|
|
|
}
|
|
|
|
// ANCHOR_END: mul-instructions
|
|
|
|
|
|
|
|
// ANCHOR: field-config
|
|
|
|
// The top-level config that provides all necessary columns and permutations
|
|
|
|
// for the other configs.
|
|
|
|
#[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],
|
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
/// Public inputs
|
|
|
|
instance: Column<Instance>,
|
2021-04-19 06:25:32 -07:00
|
|
|
|
2021-04-27 19:47:26 -07:00
|
|
|
add_config: AddConfig,
|
|
|
|
mul_config: MulConfig,
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
// ANCHOR END: field-config
|
|
|
|
|
|
|
|
// ANCHOR: add-config
|
|
|
|
#[derive(Clone, Debug)]
|
|
|
|
struct AddConfig {
|
|
|
|
advice: [Column<Advice>; 2],
|
|
|
|
s_add: Selector,
|
|
|
|
}
|
|
|
|
// ANCHOR_END: add-config
|
|
|
|
|
|
|
|
// ANCHOR: mul-config
|
|
|
|
#[derive(Clone, Debug)]
|
|
|
|
struct MulConfig {
|
|
|
|
advice: [Column<Advice>; 2],
|
|
|
|
s_mul: Selector,
|
|
|
|
}
|
|
|
|
// ANCHOR END: mul-config
|
|
|
|
|
|
|
|
// ANCHOR: field-chip
|
|
|
|
/// The top-level chip that will implement the `FieldInstructions`.
|
|
|
|
struct FieldChip<F: FieldExt> {
|
2021-04-27 19:47:26 -07:00
|
|
|
config: FieldConfig,
|
2021-04-19 06:25:32 -07:00
|
|
|
_marker: PhantomData<F>,
|
|
|
|
}
|
|
|
|
// ANCHOR_END: field-chip
|
|
|
|
|
|
|
|
// ANCHOR: add-chip
|
|
|
|
struct AddChip<F: FieldExt> {
|
2021-04-27 19:47:26 -07:00
|
|
|
config: AddConfig,
|
2021-04-19 06:25:32 -07:00
|
|
|
_marker: PhantomData<F>,
|
|
|
|
}
|
|
|
|
// ANCHOR END: add-chip
|
|
|
|
|
|
|
|
// ANCHOR: mul-chip
|
|
|
|
struct MulChip<F: FieldExt> {
|
2021-04-27 19:47:26 -07:00
|
|
|
config: MulConfig,
|
2021-04-19 06:25:32 -07:00
|
|
|
_marker: PhantomData<F>,
|
|
|
|
}
|
|
|
|
// ANCHOR_END: mul-chip
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
// ANCHOR: add-chip-trait-impl
|
2021-04-19 06:25:32 -07:00
|
|
|
impl<F: FieldExt> Chip<F> for AddChip<F> {
|
2021-04-27 19:47:26 -07:00
|
|
|
type Config = AddConfig;
|
2021-04-19 06:25:32 -07:00
|
|
|
type Loaded = ();
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
fn config(&self) -> &Self::Config {
|
|
|
|
&self.config
|
|
|
|
}
|
|
|
|
|
|
|
|
fn loaded(&self) -> &Self::Loaded {
|
|
|
|
&()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR END: add-chip-trait-impl
|
|
|
|
|
|
|
|
// ANCHOR: add-chip-impl
|
|
|
|
impl<F: FieldExt> AddChip<F> {
|
|
|
|
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
|
2021-04-19 06:25:32 -07:00
|
|
|
Self {
|
|
|
|
config,
|
|
|
|
_marker: PhantomData,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
fn configure(
|
|
|
|
meta: &mut ConstraintSystem<F>,
|
2021-04-21 15:58:44 -07:00
|
|
|
advice: [Column<Advice>; 2],
|
|
|
|
) -> <Self as Chip<F>>::Config {
|
2021-04-19 06:25:32 -07:00
|
|
|
let s_add = meta.selector();
|
|
|
|
|
|
|
|
// Define our addition gate!
|
|
|
|
meta.create_gate("add", |meta| {
|
2021-04-21 15:58:44 -07:00
|
|
|
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());
|
2021-06-04 08:18:51 -07:00
|
|
|
let s_add = meta.query_selector(s_add);
|
2021-05-27 06:44:02 -07:00
|
|
|
|
|
|
|
vec![s_add * (lhs + rhs + out * -F::one())]
|
2021-04-19 06:25:32 -07:00
|
|
|
});
|
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
AddConfig { advice, s_add }
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR END: add-chip-impl
|
|
|
|
|
|
|
|
// ANCHOR: add-instructions-impl
|
|
|
|
impl<F: FieldExt> AddInstructions<F> for FieldChip<F> {
|
|
|
|
type Num = Number<F>;
|
|
|
|
fn add(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config().add_config.clone();
|
|
|
|
|
2021-04-19 06:25:32 -07:00
|
|
|
let add_chip = AddChip::<F>::construct(config, ());
|
|
|
|
add_chip.add(layouter, a, b)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<F: FieldExt> AddInstructions<F> for AddChip<F> {
|
|
|
|
type Num = Number<F>;
|
|
|
|
|
|
|
|
fn add(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
mut layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config();
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
let mut out = None;
|
|
|
|
layouter.assign_region(
|
|
|
|
|| "add",
|
|
|
|
|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_add.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),
|
|
|
|
)?;
|
2021-07-08 11:47:51 -07:00
|
|
|
region.constrain_equal(a.cell, lhs)?;
|
|
|
|
region.constrain_equal(b.cell, rhs)?;
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// 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())
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR END: add-instructions-impl
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
// ANCHOR: mul-chip-trait-impl
|
2021-04-19 06:25:32 -07:00
|
|
|
impl<F: FieldExt> Chip<F> for MulChip<F> {
|
2021-04-27 19:47:26 -07:00
|
|
|
type Config = MulConfig;
|
2021-04-19 06:25:32 -07:00
|
|
|
type Loaded = ();
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
fn config(&self) -> &Self::Config {
|
|
|
|
&self.config
|
|
|
|
}
|
|
|
|
|
|
|
|
fn loaded(&self) -> &Self::Loaded {
|
|
|
|
&()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR END: mul-chip-trait-impl
|
|
|
|
|
|
|
|
// ANCHOR: mul-chip-impl
|
|
|
|
impl<F: FieldExt> MulChip<F> {
|
|
|
|
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
|
2021-04-19 06:25:32 -07:00
|
|
|
Self {
|
|
|
|
config,
|
|
|
|
_marker: PhantomData,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
fn configure(
|
|
|
|
meta: &mut ConstraintSystem<F>,
|
2021-04-21 15:58:44 -07:00
|
|
|
advice: [Column<Advice>; 2],
|
|
|
|
) -> <Self as Chip<F>>::Config {
|
2021-07-08 11:47:51 -07:00
|
|
|
for column in &advice {
|
|
|
|
meta.enable_equality((*column).into());
|
|
|
|
}
|
2021-04-19 06:25:32 -07:00
|
|
|
let s_mul = 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.
|
2021-04-21 15:58:44 -07:00
|
|
|
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());
|
2021-06-04 08:18:51 -07:00
|
|
|
let s_mul = meta.query_selector(s_mul);
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// The polynomial expression 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.
|
2021-05-27 06:44:02 -07:00
|
|
|
vec![s_mul * (lhs * rhs + out * -F::one())]
|
2021-04-19 06:25:32 -07:00
|
|
|
});
|
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
MulConfig { advice, s_mul }
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
}
|
2021-04-21 15:58:44 -07:00
|
|
|
// ANCHOR_END: mul-chip-impl
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// ANCHOR: mul-instructions-impl
|
|
|
|
impl<F: FieldExt> MulInstructions<F> for FieldChip<F> {
|
|
|
|
type Num = Number<F>;
|
|
|
|
fn mul(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config().mul_config.clone();
|
2021-04-19 06:25:32 -07:00
|
|
|
let mul_chip = MulChip::<F>::construct(config, ());
|
|
|
|
mul_chip.mul(layouter, a, b)
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
impl<F: FieldExt> MulInstructions<F> for MulChip<F> {
|
|
|
|
type Num = Number<F>;
|
|
|
|
|
|
|
|
fn mul(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
mut layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
a: Self::Num,
|
|
|
|
b: Self::Num,
|
|
|
|
) -> Result<Self::Num, Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config();
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
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),
|
|
|
|
)?;
|
2021-07-08 11:47:51 -07:00
|
|
|
region.constrain_equal(a.cell, lhs)?;
|
|
|
|
region.constrain_equal(b.cell, rhs)?;
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// 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())
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR END: mul-instructions-impl
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
// ANCHOR: field-chip-trait-impl
|
2021-04-19 06:25:32 -07:00
|
|
|
impl<F: FieldExt> Chip<F> for FieldChip<F> {
|
2021-04-27 19:47:26 -07:00
|
|
|
type Config = FieldConfig;
|
2021-04-19 06:25:32 -07:00
|
|
|
type Loaded = ();
|
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
fn config(&self) -> &Self::Config {
|
|
|
|
&self.config
|
|
|
|
}
|
|
|
|
|
|
|
|
fn loaded(&self) -> &Self::Loaded {
|
|
|
|
&()
|
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR_END: field-chip-trait-impl
|
|
|
|
|
|
|
|
// ANCHOR: field-chip-impl
|
|
|
|
impl<F: FieldExt> FieldChip<F> {
|
|
|
|
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
|
2021-04-19 06:25:32 -07:00
|
|
|
Self {
|
|
|
|
config,
|
|
|
|
_marker: PhantomData,
|
|
|
|
}
|
|
|
|
}
|
|
|
|
|
|
|
|
fn configure(
|
|
|
|
meta: &mut ConstraintSystem<F>,
|
2021-04-21 15:58:44 -07:00
|
|
|
advice: [Column<Advice>; 2],
|
|
|
|
instance: Column<Instance>,
|
|
|
|
) -> <Self as Chip<F>>::Config {
|
2021-07-08 11:47:51 -07:00
|
|
|
let add_config = AddChip::configure(meta, advice);
|
|
|
|
let mul_config = MulChip::configure(meta, advice);
|
2021-04-19 06:25:32 -07:00
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
meta.enable_equality(instance.into());
|
|
|
|
|
2021-04-27 19:47:26 -07:00
|
|
|
FieldConfig {
|
2021-04-21 15:58:44 -07:00
|
|
|
advice,
|
2021-07-08 14:22:16 -07:00
|
|
|
instance,
|
2021-04-21 15:58:44 -07:00
|
|
|
add_config,
|
|
|
|
mul_config,
|
2021-04-27 19:47:26 -07:00
|
|
|
}
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR_END: field-chip-impl
|
|
|
|
|
|
|
|
// ANCHOR: field-instructions-impl
|
|
|
|
impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
|
|
|
|
type Num = Number<F>;
|
|
|
|
|
|
|
|
fn load_private(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
mut layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
value: Option<F>,
|
|
|
|
) -> Result<<Self as FieldInstructions<F>>::Num, Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config();
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
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())
|
|
|
|
}
|
|
|
|
|
|
|
|
/// Returns `d = (a + b) * c`.
|
|
|
|
fn add_and_mul(
|
|
|
|
&self,
|
|
|
|
layouter: &mut impl Layouter<F>,
|
|
|
|
a: <Self as FieldInstructions<F>>::Num,
|
|
|
|
b: <Self as FieldInstructions<F>>::Num,
|
|
|
|
c: <Self as FieldInstructions<F>>::Num,
|
|
|
|
) -> Result<<Self as FieldInstructions<F>>::Num, Error> {
|
2021-04-21 15:58:44 -07:00
|
|
|
let ab = self.add(layouter.namespace(|| "a + b"), a, b)?;
|
|
|
|
self.mul(layouter.namespace(|| "(a + b) * c"), ab, c)
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
|
|
|
|
fn expose_public(
|
|
|
|
&self,
|
2021-04-21 15:58:44 -07:00
|
|
|
mut layouter: impl Layouter<F>,
|
2021-04-19 06:25:32 -07:00
|
|
|
num: <Self as FieldInstructions<F>>::Num,
|
2021-07-08 14:22:16 -07:00
|
|
|
row: usize,
|
2021-04-19 06:25:32 -07:00
|
|
|
) -> Result<(), Error> {
|
2021-04-27 19:47:26 -07:00
|
|
|
let config = self.config();
|
2021-04-19 06:25:32 -07:00
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
layouter.constrain_instance(num.cell, config.instance, row)
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR_END: field-instructions-impl
|
|
|
|
|
|
|
|
// ANCHOR: 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.
|
2021-06-21 11:10:59 -07:00
|
|
|
#[derive(Default)]
|
2021-04-19 06:25:32 -07:00
|
|
|
struct MyCircuit<F: FieldExt> {
|
|
|
|
a: Option<F>,
|
|
|
|
b: Option<F>,
|
|
|
|
c: 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.
|
2021-04-27 19:47:26 -07:00
|
|
|
type Config = FieldConfig;
|
2021-06-21 11:10:59 -07:00
|
|
|
type FloorPlanner = SimpleFloorPlanner;
|
|
|
|
|
|
|
|
fn without_witnesses(&self) -> Self {
|
|
|
|
Self::default()
|
|
|
|
}
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
|
|
|
|
// We create the two advice columns that FieldChip uses for I/O.
|
2021-04-21 15:58:44 -07:00
|
|
|
let advice = [meta.advice_column(), meta.advice_column()];
|
2021-04-19 06:25:32 -07:00
|
|
|
|
2021-04-21 15:58:44 -07:00
|
|
|
// We also need an instance column to store public inputs.
|
|
|
|
let instance = meta.instance_column();
|
2021-04-19 06:25:32 -07:00
|
|
|
|
2021-04-27 19:47:26 -07:00
|
|
|
FieldChip::configure(meta, advice, instance)
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
|
2021-06-21 11:10:59 -07:00
|
|
|
fn synthesize(
|
|
|
|
&self,
|
|
|
|
config: Self::Config,
|
|
|
|
mut layouter: impl Layouter<F>,
|
|
|
|
) -> Result<(), Error> {
|
2021-04-19 06:25:32 -07:00
|
|
|
let field_chip = FieldChip::<F>::construct(config, ());
|
|
|
|
|
|
|
|
// Load our private values into the circuit.
|
2021-04-21 15:58:44 -07:00
|
|
|
let a = field_chip.load_private(layouter.namespace(|| "load a"), self.a)?;
|
|
|
|
let b = field_chip.load_private(layouter.namespace(|| "load b"), self.b)?;
|
|
|
|
let c = field_chip.load_private(layouter.namespace(|| "load c"), self.c)?;
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// Use `add_and_mul` to get `d = (a + b) * c`.
|
|
|
|
let d = field_chip.add_and_mul(&mut layouter, a, b, c)?;
|
|
|
|
|
|
|
|
// Expose the result as a public input to the circuit.
|
2021-07-08 14:22:16 -07:00
|
|
|
field_chip.expose_public(layouter.namespace(|| "expose d"), d, 0)
|
2021-04-19 06:25:32 -07:00
|
|
|
}
|
|
|
|
}
|
|
|
|
// ANCHOR_END: circuit
|
|
|
|
|
2021-04-25 17:53:43 -07:00
|
|
|
#[allow(clippy::many_single_char_names)]
|
2021-04-19 06:25:32 -07:00
|
|
|
fn main() {
|
|
|
|
use halo2::{dev::MockProver, pasta::Fp};
|
|
|
|
|
|
|
|
// ANCHOR: test-circuit
|
|
|
|
// 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.
|
2021-07-08 11:47:51 -07:00
|
|
|
let k = 4;
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// Prepare the private and public inputs to the circuit!
|
|
|
|
let a = Fp::rand();
|
|
|
|
let b = Fp::rand();
|
|
|
|
let c = Fp::rand();
|
|
|
|
let d = (a + b) * c;
|
|
|
|
|
|
|
|
// Instantiate the circuit with the private inputs.
|
|
|
|
let circuit = MyCircuit {
|
|
|
|
a: Some(a),
|
|
|
|
b: Some(b),
|
|
|
|
c: Some(c),
|
|
|
|
};
|
|
|
|
|
2021-07-08 14:22:16 -07:00
|
|
|
// Arrange the public input. We expose the multiplication result in row 0
|
2021-04-19 06:25:32 -07:00
|
|
|
// of the instance column, so we position it there in our public inputs.
|
2021-07-14 08:47:53 -07:00
|
|
|
let mut public_inputs = vec![d];
|
2021-04-19 06:25:32 -07:00
|
|
|
|
|
|
|
// 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!
|
2021-07-08 14:22:16 -07:00
|
|
|
public_inputs[0] += Fp::one();
|
2021-04-19 06:25:32 -07:00
|
|
|
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
|
2021-07-08 14:22:16 -07:00
|
|
|
assert!(prover.verify().is_err());
|
2021-04-19 06:25:32 -07:00
|
|
|
// ANCHOR_END: test-circuit
|
|
|
|
}
|