extern crate halo2;
use std::marker::PhantomData;
use halo2::{
arithmetic::FieldExt,
circuit::{Cell, Chip, Layouter, Region, SimpleFloorPlanner},
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Instance, Selector},
poly::Rotation,
};
#[derive(Clone)]
struct Number<F: FieldExt> {
cell: Cell,
value: Option<F>,
}
trait FieldInstructions<F: FieldExt>: AddInstructions<F> + MulInstructions<F> {
type Num;
fn load_private(
&self,
layouter: impl Layouter<F>,
a: Option<F>,
) -> Result<<Self as FieldInstructions<F>>::Num, Error>;
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>;
fn expose_public(
&self,
layouter: impl Layouter<F>,
num: <Self as FieldInstructions<F>>::Num,
row: usize,
) -> Result<(), Error>;
}
trait AddInstructions<F: FieldExt>: Chip<F> {
type Num;
fn add(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error>;
}
trait MulInstructions<F: FieldExt>: Chip<F> {
type Num;
fn mul(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error>;
}
#[derive(Clone, Debug)]
struct FieldConfig {
advice: [Column<Advice>; 2],
instance: Column<Instance>,
add_config: AddConfig,
mul_config: MulConfig,
}
#[derive(Clone, Debug)]
struct AddConfig {
advice: [Column<Advice>; 2],
s_add: Selector,
}
#[derive(Clone, Debug)]
struct MulConfig {
advice: [Column<Advice>; 2],
s_mul: Selector,
}
struct FieldChip<F: FieldExt> {
config: FieldConfig,
_marker: PhantomData<F>,
}
struct AddChip<F: FieldExt> {
config: AddConfig,
_marker: PhantomData<F>,
}
struct MulChip<F: FieldExt> {
config: MulConfig,
_marker: PhantomData<F>,
}
impl<F: FieldExt> Chip<F> for AddChip<F> {
type Config = AddConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
impl<F: FieldExt> AddChip<F> {
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
) -> <Self as Chip<F>>::Config {
let s_add = meta.selector();
meta.create_gate("add", |meta| {
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_add = meta.query_selector(s_add);
vec![s_add * (lhs + rhs - out)]
});
AddConfig { advice, s_add }
}
}
impl<F: FieldExt> AddInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn add(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config().add_config.clone();
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,
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(
|| "add",
|mut region: Region<'_, F>| {
config.s_add.enable(&mut region, 0)?;
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(a.cell, lhs)?;
region.constrain_equal(b.cell, rhs)?;
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),
)?;
out = Some(Number { cell, value });
Ok(())
},
)?;
Ok(out.unwrap())
}
}
impl<F: FieldExt> Chip<F> for MulChip<F> {
type Config = MulConfig;
type Loaded = ();
fn config(&self) -> &Self::Config {
&self.config
}
fn loaded(&self) -> &Self::Loaded {
&()
}
}
impl<F: FieldExt> MulChip<F> {
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
) -> <Self as Chip<F>>::Config {
for column in &advice {
meta.enable_equality((*column).into());
}
let s_mul = meta.selector();
meta.create_gate("mul", |meta| {
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);
vec![s_mul * (lhs * rhs - out)]
});
MulConfig { advice, s_mul }
}
}
impl<F: FieldExt> MulInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn mul(
&self,
layouter: impl Layouter<F>,
a: Self::Num,
b: Self::Num,
) -> Result<Self::Num, Error> {
let config = self.config().mul_config.clone();
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,
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>| {
config.s_mul.enable(&mut region, 0)?;
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(a.cell, lhs)?;
region.constrain_equal(b.cell, rhs)?;
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),
)?;
out = Some(Number { cell, value });
Ok(())
},
)?;
Ok(out.unwrap())
}
}
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 {
&()
}
}
impl<F: FieldExt> FieldChip<F> {
fn construct(config: <Self as Chip<F>>::Config, _loaded: <Self as Chip<F>>::Loaded) -> Self {
Self {
config,
_marker: PhantomData,
}
}
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
instance: Column<Instance>,
) -> <Self as Chip<F>>::Config {
let add_config = AddChip::configure(meta, advice);
let mul_config = MulChip::configure(meta, advice);
meta.enable_equality(instance.into());
FieldConfig {
advice,
instance,
add_config,
mul_config,
}
}
}
impl<F: FieldExt> FieldInstructions<F> for FieldChip<F> {
type Num = Number<F>;
fn load_private(
&self,
mut layouter: impl Layouter<F>,
value: Option<F>,
) -> Result<<Self as FieldInstructions<F>>::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 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> {
let ab = self.add(layouter.namespace(|| "a + b"), a, b)?;
self.mul(layouter.namespace(|| "(a + b) * c"), ab, c)
}
fn expose_public(
&self,
mut layouter: impl Layouter<F>,
num: <Self as FieldInstructions<F>>::Num,
row: usize,
) -> Result<(), Error> {
let config = self.config();
layouter.constrain_instance(num.cell, config.instance, row)
}
}
#[derive(Default)]
struct MyCircuit<F: FieldExt> {
a: Option<F>,
b: Option<F>,
c: Option<F>,
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
type Config = FieldConfig;
type FloorPlanner = SimpleFloorPlanner;
fn without_witnesses(&self) -> Self {
Self::default()
}
fn configure(meta: &mut ConstraintSystem<F>) -> Self::Config {
let advice = [meta.advice_column(), meta.advice_column()];
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, ());
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)?;
let d = field_chip.add_and_mul(&mut layouter, a, b, c)?;
field_chip.expose_public(layouter.namespace(|| "expose d"), d, 0)
}
}
#[allow(clippy::many_single_char_names)]
fn main() {
use halo2::{dev::MockProver, pasta::Fp};
let k = 4;
let a = Fp::rand();
let b = Fp::rand();
let c = Fp::rand();
let d = (a + b) * c;
let circuit = MyCircuit {
a: Some(a),
b: Some(b),
c: Some(c),
};
let mut public_inputs = vec![d];
let prover = MockProver::run(k, &circuit, vec![public_inputs.clone()]).unwrap();
assert_eq!(prover.verify(), Ok(()));
public_inputs[0] += Fp::one();
let prover = MockProver::run(k, &circuit, vec![public_inputs]).unwrap();
assert!(prover.verify().is_err());
}