Add halo2::dev::circuit_layout behind dev-graph feature flag

This method renders circuits as tables, showing how the various regions
within them have been layed out.
This commit is contained in:
Jack Grigg 2021-01-23 17:54:31 +00:00
parent 7dd6e65a5f
commit 3c1132ec59
5 changed files with 645 additions and 2 deletions

View file

@ -49,9 +49,14 @@ lazy_static = "1.4.0"
static_assertions = "1.1.0"
# Developer tooling dependencies
plotters = { version = "0.3.0", optional = true }
tabbycat = { version = "0.1", features = ["attributes"], optional = true }
[features]
dev-graph = ["tabbycat"]
dev-graph = ["plotters", "tabbycat"]
gadget-traces = ["backtrace"]
sanity-checks = []
[[example]]
name = "circuit-layout"
required-features = ["dev-graph"]

391
examples/circuit-layout.rs Normal file
View file

@ -0,0 +1,391 @@
use halo2::{
arithmetic::FieldExt,
dev::circuit_layout,
pasta::Fp,
plonk::{Advice, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed},
poly::Rotation,
};
use plotters::prelude::*;
use std::marker::PhantomData;
fn main() {
/// This represents an advice column at a certain row in the ConstraintSystem
#[derive(Copy, Clone, Debug)]
pub struct Variable(Column<Advice>, usize);
struct PLONKConfig {
a: Column<Advice>,
b: Column<Advice>,
c: Column<Advice>,
d: Column<Advice>,
e: Column<Advice>,
sa: Column<Fixed>,
sb: Column<Fixed>,
sc: Column<Fixed>,
sm: Column<Fixed>,
sp: Column<Fixed>,
sl: Column<Fixed>,
sl2: Column<Fixed>,
perm: usize,
perm2: usize,
}
trait StandardCS<FF: FieldExt> {
fn raw_multiply<F>(&mut self, f: F) -> Result<(Variable, Variable, Variable), Error>
where
F: FnOnce() -> Result<(FF, FF, FF), Error>;
fn raw_add<F>(&mut self, f: F) -> Result<(Variable, Variable, Variable), Error>
where
F: FnOnce() -> Result<(FF, FF, FF), Error>;
fn copy(&mut self, a: Variable, b: Variable) -> Result<(), Error>;
fn public_input<F>(&mut self, f: F) -> Result<Variable, Error>
where
F: FnOnce() -> Result<FF, Error>;
fn lookup_table(&mut self, values: &[Vec<FF>]) -> Result<(), Error>;
}
struct MyCircuit<F: FieldExt> {
a: Option<F>,
lookup_tables: Vec<Vec<F>>,
}
struct StandardPLONK<'a, F: FieldExt, CS: Assignment<F> + 'a> {
cs: &'a mut CS,
config: PLONKConfig,
current_gate: usize,
_marker: PhantomData<F>,
}
impl<'a, FF: FieldExt, CS: Assignment<FF>> StandardPLONK<'a, FF, CS> {
fn new(cs: &'a mut CS, config: PLONKConfig) -> Self {
StandardPLONK {
cs,
config,
current_gate: 0,
_marker: PhantomData,
}
}
fn enter_region<NR, N>(&mut self, name_fn: N)
where
NR: Into<String>,
N: FnOnce() -> NR,
{
self.cs.enter_region(name_fn);
}
fn exit_region(&mut self) {
self.cs.exit_region();
}
}
impl<'a, FF: FieldExt, CS: Assignment<FF>> StandardCS<FF> for StandardPLONK<'a, FF, CS> {
fn raw_multiply<F>(&mut self, f: F) -> Result<(Variable, Variable, Variable), Error>
where
F: FnOnce() -> Result<(FF, FF, FF), Error>,
{
let index = self.current_gate;
self.current_gate += 1;
let mut value = None;
self.cs.assign_advice(
|| "lhs",
self.config.a,
index,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::SynthesisError)?.0)
},
)?;
self.cs.assign_advice(
|| "lhs^4",
self.config.d,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.0.square().square()),
)?;
self.cs.assign_advice(
|| "rhs",
self.config.b,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.1),
)?;
self.cs.assign_advice(
|| "rhs^4",
self.config.e,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.1.square().square()),
)?;
self.cs.assign_advice(
|| "out",
self.config.c,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.2),
)?;
self.cs
.assign_fixed(|| "a", self.config.sa, index, || Ok(FF::zero()))?;
self.cs
.assign_fixed(|| "b", self.config.sb, index, || Ok(FF::zero()))?;
self.cs
.assign_fixed(|| "c", self.config.sc, index, || Ok(FF::one()))?;
self.cs
.assign_fixed(|| "a * b", self.config.sm, index, || Ok(FF::one()))?;
Ok((
Variable(self.config.a, index),
Variable(self.config.b, index),
Variable(self.config.c, index),
))
}
fn raw_add<F>(&mut self, f: F) -> Result<(Variable, Variable, Variable), Error>
where
F: FnOnce() -> Result<(FF, FF, FF), Error>,
{
let index = self.current_gate;
self.current_gate += 1;
let mut value = None;
self.cs.assign_advice(
|| "lhs",
self.config.a,
index,
|| {
value = Some(f()?);
Ok(value.ok_or(Error::SynthesisError)?.0)
},
)?;
self.cs.assign_advice(
|| "lhs^4",
self.config.d,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.0.square().square()),
)?;
self.cs.assign_advice(
|| "rhs",
self.config.b,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.1),
)?;
self.cs.assign_advice(
|| "rhs^4",
self.config.e,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.1.square().square()),
)?;
self.cs.assign_advice(
|| "out",
self.config.c,
index,
|| Ok(value.ok_or(Error::SynthesisError)?.2),
)?;
self.cs
.assign_fixed(|| "a", self.config.sa, index, || Ok(FF::one()))?;
self.cs
.assign_fixed(|| "b", self.config.sb, index, || Ok(FF::one()))?;
self.cs
.assign_fixed(|| "c", self.config.sc, index, || Ok(FF::one()))?;
self.cs
.assign_fixed(|| "a * b", self.config.sm, index, || Ok(FF::zero()))?;
Ok((
Variable(self.config.a, index),
Variable(self.config.b, index),
Variable(self.config.c, index),
))
}
fn copy(&mut self, left: Variable, right: Variable) -> Result<(), Error> {
let left_column = match left.0 {
x if x == self.config.a => 0,
x if x == self.config.b => 1,
x if x == self.config.c => 2,
_ => unreachable!(),
};
let right_column = match right.0 {
x if x == self.config.a => 0,
x if x == self.config.b => 1,
x if x == self.config.c => 2,
_ => unreachable!(),
};
self.cs
.copy(self.config.perm, left_column, left.1, right_column, right.1)?;
self.cs.copy(
self.config.perm2,
left_column,
left.1,
right_column,
right.1,
)
}
fn public_input<F>(&mut self, f: F) -> Result<Variable, Error>
where
F: FnOnce() -> Result<FF, Error>,
{
let index = self.current_gate;
self.current_gate += 1;
self.cs
.assign_advice(|| "value", self.config.a, index, || f())?;
self.cs
.assign_fixed(|| "public", self.config.sp, index, || Ok(FF::one()))?;
Ok(Variable(self.config.a, index))
}
fn lookup_table(&mut self, values: &[Vec<FF>]) -> Result<(), Error> {
for (&value_0, &value_1) in values[0].iter().zip(values[1].iter()) {
let index = self.current_gate;
self.current_gate += 1;
self.cs
.assign_fixed(|| "table col 1", self.config.sl, index, || Ok(value_0))?;
self.cs
.assign_fixed(|| "table col 2", self.config.sl2, index, || Ok(value_1))?;
}
Ok(())
}
}
impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
type Config = PLONKConfig;
fn configure(meta: &mut ConstraintSystem<F>) -> PLONKConfig {
let e = meta.advice_column();
let a = meta.advice_column();
let b = meta.advice_column();
let sf = meta.fixed_column();
let c = meta.advice_column();
let d = meta.advice_column();
let p = meta.aux_column();
let perm = meta.permutation(&[a, b, c]);
let perm2 = meta.permutation(&[a, b, c]);
let sm = meta.fixed_column();
let sa = meta.fixed_column();
let sb = meta.fixed_column();
let sc = meta.fixed_column();
let sp = meta.fixed_column();
let sl = meta.fixed_column();
let sl2 = meta.fixed_column();
/*
* A B ... sl sl2
* [
* aux 0 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* ... ... ... ... ...
* ... ... ... aux 0
* ... ... ... a a
* ... ... ... a a^2
* ... ... ... 0 0
*
* ]
*/
meta.lookup(&[a.into()], &[sl.into()]);
meta.lookup(&[a.into(), b.into()], &[sl.into(), sl2.into()]);
meta.create_gate("Combined add-mult", |meta| {
let d = meta.query_advice(d, Rotation::next());
let a = meta.query_advice(a, Rotation::cur());
let sf = meta.query_fixed(sf, Rotation::cur());
let e = meta.query_advice(e, Rotation::prev());
let b = meta.query_advice(b, Rotation::cur());
let c = meta.query_advice(c, Rotation::cur());
let sa = meta.query_fixed(sa, Rotation::cur());
let sb = meta.query_fixed(sb, Rotation::cur());
let sc = meta.query_fixed(sc, Rotation::cur());
let sm = meta.query_fixed(sm, Rotation::cur());
a.clone() * sa + b.clone() * sb + a * b * sm + (c * sc * (-F::one())) + sf * (d * e)
});
meta.create_gate("Public input", |meta| {
let a = meta.query_advice(a, Rotation::cur());
let p = meta.query_aux(p, Rotation::cur());
let sp = meta.query_fixed(sp, Rotation::cur());
sp * (a + p * (-F::one()))
});
PLONKConfig {
a,
b,
c,
d,
e,
sa,
sb,
sc,
sm,
sp,
sl,
sl2,
perm,
perm2,
}
}
fn synthesize(
&self,
cs: &mut impl Assignment<F>,
config: PLONKConfig,
) -> Result<(), Error> {
let mut cs = StandardPLONK::new(cs, config);
cs.enter_region(|| "input");
let _ = cs.public_input(|| Ok(F::one() + F::one()))?;
cs.exit_region();
for i in 0..10 {
cs.enter_region(|| format!("region_{}", i));
let mut a_squared = None;
let (a0, _, c0) = cs.raw_multiply(|| {
a_squared = self.a.map(|a| a.square());
Ok((
self.a.ok_or(Error::SynthesisError)?,
self.a.ok_or(Error::SynthesisError)?,
a_squared.ok_or(Error::SynthesisError)?,
))
})?;
let (a1, b1, _) = cs.raw_add(|| {
let fin = a_squared.and_then(|a2| self.a.map(|a| a + a2));
Ok((
self.a.ok_or(Error::SynthesisError)?,
a_squared.ok_or(Error::SynthesisError)?,
fin.ok_or(Error::SynthesisError)?,
))
})?;
cs.copy(a0, a1)?;
cs.copy(b1, c0)?;
cs.exit_region();
}
cs.enter_region(|| "lookup table");
cs.lookup_table(&self.lookup_tables)?;
cs.exit_region();
Ok(())
}
}
let a = Fp::rand();
let a_squared = a * &a;
let aux = Fp::one() + Fp::one();
let lookup_table = vec![aux, a, a, Fp::zero()];
let lookup_table_2 = vec![Fp::zero(), a, a_squared, Fp::zero()];
let circuit: MyCircuit<Fp> = MyCircuit {
a: None,
lookup_tables: vec![lookup_table, lookup_table_2],
};
let root = BitMapBackend::new("example-circuit-layout.png", (1024, 768)).into_drawing_area();
root.fill(&WHITE).unwrap();
let root = root
.titled("Example Circuit Layout", ("sans-serif", 60))
.unwrap();
circuit_layout(&circuit, &root).unwrap();
}

View file

@ -16,7 +16,7 @@ mod graph;
#[cfg(feature = "dev-graph")]
#[cfg_attr(docsrs, doc(cfg(feature = "dev-graph")))]
pub use graph::circuit_dot_graph;
pub use graph::{circuit_dot_graph, layout::circuit_layout};
/// The reasons why a particular circuit is not satisfied.
#[derive(Debug, PartialEq)]

View file

@ -3,6 +3,8 @@ use tabbycat::{AttrList, Edge, GraphBuilder, GraphType, Identity, StmtList};
use crate::plonk::{Advice, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed};
pub mod layout;
/// Builds a dot graph string representing the given circuit.
///
/// The graph is built from calls to [`Layouter::namespace`] both within the circuit, and

245
src/dev/graph/layout.rs Normal file
View file

@ -0,0 +1,245 @@
use ff::Field;
use plotters::{
coord::Shift,
prelude::{DrawingArea, DrawingAreaErrorKind, DrawingBackend},
};
use std::cmp;
use std::collections::HashSet;
use crate::plonk::{Advice, Any, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed};
/// Renders the circuit layout on the given drawing area.
///
/// # Examples
///
/// ```ignore
/// use halo2::dev::circuit_layout;
/// use plotters::prelude::*;
///
/// let drawing_area = BitMapBackend::new("example-circuit-layout.png", (1024, 768))
/// .into_drawing_area();
/// drawing_area.fill(&WHITE).unwrap();
/// let drawing_area = drawing_area
/// .titled("Example Circuit Layout", ("sans-serif", 60))
/// .unwrap();
///
/// let circuit = MyCircuit::default();
/// circuit_layout(&circuit, &drawing_area).unwrap();
/// ```
pub fn circuit_layout<F: Field, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>(
circuit: &ConcreteCircuit,
drawing_area: &DrawingArea<DB, Shift>,
) -> Result<(), DrawingAreaErrorKind<DB::ErrorType>> {
use plotters::coord::types::RangedCoordusize;
use plotters::prelude::*;
// Collect the layout details.
let mut cs = ConstraintSystem::default();
let config = ConcreteCircuit::configure(&mut cs);
let mut layout = Layout::default();
circuit.synthesize(&mut layout, config).unwrap();
// Figure out what order to render the columns in.
// TODO: For now, just render them in the order they were configured.
let total_columns = cs.num_advice_columns + cs.num_aux_columns + cs.num_fixed_columns;
let column_index = |column: &Column<Any>| {
column.index()
+ match column.column_type() {
Any::Advice => 0,
Any::Aux => cs.num_advice_columns,
Any::Fixed => cs.num_advice_columns + cs.num_aux_columns,
}
};
// Prepare the grid layout. We render a red background for advice columns, white for
// aux columns, and blue for fixed columns.
let root =
drawing_area.apply_coord_spec(Cartesian2d::<RangedCoordusize, RangedCoordusize>::new(
0..total_columns,
0..layout.total_rows,
drawing_area.get_pixel_range(),
));
root.draw(&Rectangle::new(
[(0, 0), (total_columns, layout.total_rows)],
ShapeStyle::from(&WHITE).filled(),
))?;
root.draw(&Rectangle::new(
[(0, 0), (cs.num_advice_columns, layout.total_rows)],
ShapeStyle::from(&RED.mix(0.2)).filled(),
))?;
root.draw(&Rectangle::new(
[
(cs.num_advice_columns + cs.num_aux_columns, 0),
(total_columns, layout.total_rows),
],
ShapeStyle::from(&BLUE.mix(0.2)).filled(),
))?;
root.draw(&Rectangle::new(
[(0, 0), (total_columns, layout.total_rows)],
&BLACK,
))?;
let draw_region = |root: &DrawingArea<_, _>, top_left, bottom_right, label| {
root.draw(&Rectangle::new(
[top_left, bottom_right],
ShapeStyle::from(&GREEN.mix(0.2)).filled(),
))?;
root.draw(&Rectangle::new([top_left, bottom_right], &BLACK))?;
root.draw(
&(EmptyElement::at(top_left)
+ Text::new(label, (10, 10), ("sans-serif", 15.0).into_font())),
)
};
// Render the regions!
for region in layout.regions {
if let Some(offset) = region.offset {
// Sort the region's columns according to the defined ordering.
let mut columns: Vec<_> = region.columns.into_iter().collect();
columns.sort_unstable_by(|a, b| column_index(a).cmp(&column_index(b)));
// Render contiguous parts of the same region as a single box.
let mut width = None;
for column in columns {
let column = column_index(&column);
match width {
Some((start, end)) if end == column => width = Some((start, end + 1)),
Some((start, end)) => {
draw_region(
&root,
(start, offset),
(end, offset + region.rows),
region.name.clone(),
)?;
width = Some((column, column + 1));
}
None => width = Some((column, column + 1)),
}
}
// Render the last part of the region.
if let Some((start, end)) = width {
draw_region(
&root,
(start, offset),
(end, offset + region.rows),
region.name.clone(),
)?;
}
}
}
Ok(())
}
#[derive(Debug)]
struct Region {
/// The name of the region. Not required to be unique.
name: String,
/// The columns used by this region.
columns: HashSet<Column<Any>>,
/// The row that this region starts on, if known.
offset: Option<usize>,
/// The number of rows that this region takes up.
rows: usize,
}
#[derive(Default)]
struct Layout {
regions: Vec<Region>,
current_region: Option<usize>,
total_rows: usize,
}
impl Layout {
fn update(&mut self, column: Column<Any>, row: usize) {
self.total_rows = cmp::max(self.total_rows, row + 1);
// TODO: Track assignments outside regions?
if let Some(region) = self.current_region {
let region = &mut self.regions[region];
region.columns.insert(column);
let offset = region.offset.unwrap_or(row);
region.rows = cmp::max(region.rows, row - offset + 1);
region.offset = Some(offset);
}
}
}
impl<F: Field> Assignment<F> for Layout {
fn enter_region<NR, N>(&mut self, name_fn: N)
where
NR: Into<String>,
N: FnOnce() -> NR,
{
assert!(self.current_region.is_none());
self.current_region = Some(self.regions.len());
self.regions.push(Region {
name: name_fn().into(),
columns: HashSet::default(),
offset: None,
rows: 0,
})
}
fn exit_region(&mut self) {
assert!(self.current_region.is_some());
self.current_region = None;
}
fn assign_advice<V, A, AR>(
&mut self,
_: A,
column: Column<Advice>,
row: usize,
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<F, Error>,
A: FnOnce() -> AR,
AR: Into<String>,
{
self.update(column.into(), row);
Ok(())
}
fn assign_fixed<V, A, AR>(
&mut self,
_: A,
column: Column<Fixed>,
row: usize,
_: V,
) -> Result<(), Error>
where
V: FnOnce() -> Result<F, Error>,
A: FnOnce() -> AR,
AR: Into<String>,
{
self.update(column.into(), row);
Ok(())
}
fn copy(
&mut self,
_: usize,
_: usize,
_: usize,
_: usize,
_: usize,
) -> Result<(), crate::plonk::Error> {
// Do nothing; we don't care about permutations in this context.
Ok(())
}
fn push_namespace<NR, N>(&mut self, _: N)
where
NR: Into<String>,
N: FnOnce() -> NR,
{
// Do nothing; we don't care about namespaces in this context.
}
fn pop_namespace(&mut self, _: Option<String>) {
// Do nothing; we don't care about namespaces in this context.
}
}