Skip to content

Commit

Permalink
Add halo2::plonk::circuit::TableColumn struct
Browse files Browse the repository at this point in the history
This type is required by the `ConstraintSystem::lookup` API, and cannot
be converted into a `Column<Fixed>` via the public API, forcing chip
developers to use `Layouter::assign_table` API to load tables. This is
a safety feature, as lookup table rows need to be default-value-filled
by the layouter (or else the table would have an implicit default value
of all-zeroes which could introduce soundness bugs into circuits).
  • Loading branch information
str4d committed Jul 27, 2021
1 parent b21ab75 commit e855ac6
Show file tree
Hide file tree
Showing 7 changed files with 61 additions and 32 deletions.
8 changes: 4 additions & 4 deletions examples/circuit-layout.rs
Original file line number Diff line number Diff line change
Expand Up @@ -3,7 +3,7 @@ use halo2::{
circuit::{Cell, Layouter, Region, SimpleFloorPlanner},
dev::CircuitLayout,
pasta::Fp,
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed},
plonk::{Advice, Circuit, Column, ConstraintSystem, Error, Fixed, TableColumn},
poly::Rotation,
};
use plotters::prelude::*;
Expand All @@ -27,7 +27,7 @@ fn main() {
sb: Column<Fixed>,
sc: Column<Fixed>,
sm: Column<Fixed>,
sl: Column<Fixed>,
sl: TableColumn,
}

trait StandardCs<FF: FieldExt> {
Expand Down Expand Up @@ -171,7 +171,7 @@ fn main() {
layouter: &mut impl Layouter<FF>,
values: &[FF],
) -> Result<(), Error> {
layouter.assign_region(
layouter.assign_table(
|| "",
|mut region| {
for (index, &value) in values.iter().enumerate() {
Expand Down Expand Up @@ -211,7 +211,7 @@ fn main() {
let sa = meta.fixed_column();
let sb = meta.fixed_column();
let sc = meta.fixed_column();
let sl = meta.fixed_column();
let sl = meta.lookup_table_column();

/*
* A B ... sl
Expand Down
7 changes: 2 additions & 5 deletions src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ use ff::Field;

use crate::{
arithmetic::FieldExt,
plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector},
plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn},
};

pub mod floor_planner;
Expand Down Expand Up @@ -245,9 +245,6 @@ impl<'r, F: Field> Region<'r, F> {
}

/// A lookup table in the circuit.
///
/// TODO: Add wrapper type to `ConstraintSystem` to allow us to only deal with lookup
/// columns here.
#[derive(Debug)]
pub struct Table<'r, F: Field> {
table: &'r mut dyn layouter::TableLayouter<F>,
Expand All @@ -266,7 +263,7 @@ impl<'r, F: Field> Table<'r, F> {
pub fn assign_fixed<'v, V, VR, A, AR>(
&'v mut self,
annotation: A,
column: Column<Fixed>,
column: TableColumn,
offset: usize,
mut to: V,
) -> Result<(), Error>
Expand Down
17 changes: 8 additions & 9 deletions src/circuit/floor_planner/single_pass.rs
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ use crate::{
},
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
Selector,
Selector, TableColumn,
},
};

Expand Down Expand Up @@ -45,7 +45,7 @@ pub struct SingleChipLayouter<'a, F: Field, CS: Assignment<F> + 'a> {
/// Stores the first empty row for each column.
columns: HashMap<RegionColumn, usize>,
/// Stores the table fixed columns.
table_columns: Vec<Column<Fixed>>,
table_columns: Vec<TableColumn>,
_marker: PhantomData<F>,
}

Expand Down Expand Up @@ -193,7 +193,7 @@ impl<'a, F: Field, CS: Assignment<F> + 'a> Layouter<F> for SingleChipLayouter<'a
// at least one cell in each column, and in that case we checked
// that all cells up to first_unused were assigned.
self.cs
.fill_from_row(col, first_unused, default_val.unwrap())?;
.fill_from_row(col.inner(), first_unused, default_val.unwrap())?;
}

Ok(result)
Expand Down Expand Up @@ -372,10 +372,9 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> RegionLayouter<F>

pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment<F> + 'a> {
cs: &'a mut CS,
used_columns: &'r [Column<Fixed>],
used_columns: &'r [TableColumn],
// maps from a fixed column to a pair (default value, vector saying which rows are assigned)
pub(crate) default_and_assigned:
HashMap<Column<Fixed>, (Option<Option<Assigned<F>>>, Vec<bool>)>,
pub(crate) default_and_assigned: HashMap<TableColumn, (Option<Option<Assigned<F>>>, Vec<bool>)>,
}

impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for SimpleTableLayouter<'r, 'a, F, CS> {
Expand All @@ -387,7 +386,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for SimpleTableLayoute
}

impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> SimpleTableLayouter<'r, 'a, F, CS> {
pub(crate) fn new(cs: &'a mut CS, used_columns: &'r [Column<Fixed>]) -> Self {
pub(crate) fn new(cs: &'a mut CS, used_columns: &'r [TableColumn]) -> Self {
SimpleTableLayouter {
cs,
used_columns,
Expand All @@ -402,7 +401,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> TableLayouter<F>
fn assign_fixed<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
column: TableColumn,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
) -> Result<(), Error> {
Expand All @@ -415,7 +414,7 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a> TableLayouter<F>
let mut value = None;
self.cs.assign_fixed(
annotation,
column,
column.inner(),
offset, // tables are always assigned starting at row 0
|| {
let res = to();
Expand Down
6 changes: 3 additions & 3 deletions src/circuit/floor_planner/v1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ use crate::{
},
plonk::{
Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance,
Selector,
Selector, TableColumn,
},
};

Expand All @@ -34,7 +34,7 @@ struct V1Plan<'a, F: Field, CS: Assignment<F> + 'a> {
/// Stores the constants to be assigned, and the cells to which they are copied.
constants: Vec<(Assigned<F>, Cell)>,
/// Stores the table fixed columns.
table_columns: Vec<Column<Fixed>>,
table_columns: Vec<TableColumn>,
}

impl<'a, F: Field, CS: Assignment<F> + 'a> fmt::Debug for V1Plan<'a, F, CS> {
Expand Down Expand Up @@ -334,7 +334,7 @@ impl<'p, 'a, F: Field, CS: Assignment<F> + 'a> AssignmentPass<'p, 'a, F, CS> {
// that all cells up to first_unused were assigned.
self.plan
.cs
.fill_from_row(col, first_unused, default_val.unwrap())?;
.fill_from_row(col.inner(), first_unused, default_val.unwrap())?;
}

Ok(result)
Expand Down
5 changes: 2 additions & 3 deletions src/circuit/layouter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,7 @@ use std::fmt;
use ff::Field;

use super::{Cell, RegionIndex};
use crate::plonk::Assigned;
use crate::plonk::{Advice, Any, Column, Error, Fixed, Instance, Selector};
use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn};

/// Helper trait for implementing a custom [`Layouter`].
///
Expand Down Expand Up @@ -115,7 +114,7 @@ pub trait TableLayouter<F: Field>: fmt::Debug {
fn assign_fixed<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
column: Column<Fixed>,
column: TableColumn,
offset: usize,
to: &'v mut (dyn FnMut() -> Result<Assigned<F>, Error> + 'v),
) -> Result<(), Error>;
Expand Down
43 changes: 39 additions & 4 deletions src/plonk/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -245,6 +245,34 @@ impl Selector {
}
}

/// A fixed column of a lookup table.
///
/// A lookup table can be loaded into this column via [`Layouter::assign_table`]. Columns
/// can currently only contain a single table, but they may be used in multiple lookup
/// arguments via [`ConstraintSystem::lookup`].
///
/// Lookup table columns are always "encumbered" by the lookup arguments they are used in;
/// they cannot simultaneously be used as general fixed columns.
///
/// [`Layouter::assign_table`]: crate::circuit::Layouter::assign_table
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct TableColumn {
/// The fixed column that this table column is stored in.
///
/// # Security
///
/// This inner column MUST NOT be exposed in the public API, or else chip developers
/// can load lookup tables into their circuits without default-value-filling the
/// columns, which can cause soundness bugs.
inner: Column<Fixed>,
}

impl TableColumn {
pub(crate) fn inner(&self) -> Column<Fixed> {
self.inner
}
}

/// A value assigned to a cell within a circuit.
///
/// Stored as a fraction, so the backend can use batch inversion.
Expand Down Expand Up @@ -994,13 +1022,13 @@ impl<F: Field> ConstraintSystem<F> {
self.permutation.add_column(column);
}

/// Add a lookup argument for some input expressions and table expressions.
/// Add a lookup argument for some input expressions and table columns.
///
/// `table_map` returns a map between input expressions and the table expressions
/// `table_map` returns a map between input expressions and the table columns
/// they need to match.
pub fn lookup(
&mut self,
table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, Column<Fixed>)>,
table_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, TableColumn)>,
) -> usize {
let mut cells = VirtualCells::new(self);
let table_map = table_map(&mut cells)
Expand All @@ -1010,7 +1038,7 @@ impl<F: Field> ConstraintSystem<F> {
panic!("expression containing simple selector supplied to lookup argument");
}

let table = cells.query_fixed(table, Rotation::cur());
let table = cells.query_fixed(table.inner(), Rotation::cur());

(input, table)
})
Expand Down Expand Up @@ -1310,6 +1338,13 @@ impl<F: Field> ConstraintSystem<F> {
Selector(index, false)
}

/// Allocates a new fixed column that can be used in a lookup table.
pub fn lookup_table_column(&mut self) -> TableColumn {
TableColumn {
inner: self.fixed_column(),
}
}

/// Allocate a new fixed column
pub fn fixed_column(&mut self) -> Column<Fixed> {
let tmp = Column {
Expand Down
7 changes: 3 additions & 4 deletions tests/plonk_api.rs
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ use halo2::dev::MockProver;
use halo2::pasta::{Eq, EqAffine, Fp};
use halo2::plonk::{
create_proof, keygen_pk, keygen_vk, verify_proof, Advice, Circuit, Column, ConstraintSystem,
Error, Fixed, VerifyingKey,
Error, Fixed, TableColumn, VerifyingKey,
};
use halo2::poly::{commitment::Params, Rotation};
use halo2::transcript::{Blake2bRead, Blake2bWrite, Challenge255};
Expand Down Expand Up @@ -37,7 +37,7 @@ fn plonk_api() {
sc: Column<Fixed>,
sm: Column<Fixed>,
sp: Column<Fixed>,
sl: Column<Fixed>,
sl: TableColumn,
}

trait StandardCs<FF: FieldExt> {
Expand Down Expand Up @@ -270,7 +270,7 @@ fn plonk_api() {
let sb = meta.fixed_column();
let sc = meta.fixed_column();
let sp = meta.fixed_column();
let sl = meta.fixed_column();
let sl = meta.lookup_table_column();

/*
* A B ... sl
Expand Down Expand Up @@ -332,7 +332,6 @@ fn plonk_api() {
meta.enable_equality(sb.into());
meta.enable_equality(sc.into());
meta.enable_equality(sp.into());
meta.enable_equality(sl.into());

PlonkConfig {
a,
Expand Down

0 comments on commit e855ac6

Please sign in to comment.