From a8aebdb8482f43b6c20d4f168fadf6f992f94e73 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 21 Mar 2023 12:23:37 +0700 Subject: [PATCH 1/5] [move-only] circuit::table_layouter: Move TableLayouter, SimpleTableLayouter --- halo2_proofs/src/circuit.rs | 9 +- .../src/circuit/floor_planner/single_pass.rs | 85 +------------- halo2_proofs/src/circuit/floor_planner/v1.rs | 6 +- halo2_proofs/src/circuit/layouter.rs | 20 +--- halo2_proofs/src/circuit/table_layouter.rs | 107 ++++++++++++++++++ 5 files changed, 120 insertions(+), 107 deletions(-) create mode 100644 halo2_proofs/src/circuit/table_layouter.rs diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index eba2ecd68e..1cdd6b360c 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -13,6 +13,9 @@ pub mod floor_planner; pub use floor_planner::single_pass::SimpleFloorPlanner; pub mod layouter; +pub mod table_layouter; + +pub use table_layouter::TableLayouter; /// A chip implements a set of instructions that can be used by gadgets. /// @@ -365,11 +368,11 @@ impl<'r, F: Field> Region<'r, F> { /// A lookup table in the circuit. #[derive(Debug)] pub struct Table<'r, F: Field> { - table: &'r mut dyn layouter::TableLayouter, + table: &'r mut dyn TableLayouter, } -impl<'r, F: Field> From<&'r mut dyn layouter::TableLayouter> for Table<'r, F> { - fn from(table: &'r mut dyn layouter::TableLayouter) -> Self { +impl<'r, F: Field> From<&'r mut dyn TableLayouter> for Table<'r, F> { + fn from(table: &'r mut dyn TableLayouter) -> Self { Table { table } } } diff --git a/halo2_proofs/src/circuit/floor_planner/single_pass.rs b/halo2_proofs/src/circuit/floor_planner/single_pass.rs index 349373759c..2767854908 100644 --- a/halo2_proofs/src/circuit/floor_planner/single_pass.rs +++ b/halo2_proofs/src/circuit/floor_planner/single_pass.rs @@ -7,8 +7,9 @@ use ff::Field; use crate::{ circuit::{ - layouter::{RegionColumn, RegionLayouter, RegionShape, TableLayouter}, - Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value, + layouter::{RegionColumn, RegionLayouter, RegionShape}, + table_layouter::SimpleTableLayouter, + Cell, Layouter, Region, RegionIndex, RegionStart, Table, TableLayouter, Value, }, plonk::{ Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance, @@ -378,86 +379,6 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> RegionLayouter } } -/// The default value to fill a table column with. -/// -/// - The outer `Option` tracks whether the value in row 0 of the table column has been -/// assigned yet. This will always be `Some` once a valid table has been completely -/// assigned. -/// - The inner `Value` tracks whether the underlying `Assignment` is evaluating -/// witnesses or not. -type DefaultTableValue = Option>>; - -pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment + 'a> { - cs: &'a mut CS, - 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, Vec)>, -} - -impl<'r, 'a, F: Field, CS: Assignment + 'a> fmt::Debug for SimpleTableLayouter<'r, 'a, F, CS> { - fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.debug_struct("SimpleTableLayouter") - .field("used_columns", &self.used_columns) - .field("default_and_assigned", &self.default_and_assigned) - .finish() - } -} - -impl<'r, 'a, F: Field, CS: Assignment + 'a> SimpleTableLayouter<'r, 'a, F, CS> { - pub(crate) fn new(cs: &'a mut CS, used_columns: &'r [TableColumn]) -> Self { - SimpleTableLayouter { - cs, - used_columns, - default_and_assigned: HashMap::default(), - } - } -} - -impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter - for SimpleTableLayouter<'r, 'a, F, CS> -{ - fn assign_cell<'v>( - &'v mut self, - annotation: &'v (dyn Fn() -> String + 'v), - column: TableColumn, - offset: usize, - to: &'v mut (dyn FnMut() -> Value> + 'v), - ) -> Result<(), Error> { - if self.used_columns.contains(&column) { - return Err(Error::Synthesis); // TODO better error - } - - let entry = self.default_and_assigned.entry(column).or_default(); - - let mut value = Value::unknown(); - self.cs.assign_fixed( - annotation, - column.inner(), - offset, // tables are always assigned starting at row 0 - || { - let res = to(); - value = res; - res - }, - )?; - - match (entry.0.is_none(), offset) { - // Use the value at offset 0 as the default value for this table column. - (true, 0) => entry.0 = Some(value), - // Since there is already an existing default value for this table column, - // the caller should not be attempting to assign another value at offset 0. - (false, 0) => return Err(Error::Synthesis), // TODO better error - _ => (), - } - if entry.1.len() <= offset { - entry.1.resize(offset + 1, false); - } - entry.1[offset] = true; - - Ok(()) - } -} - #[cfg(test)] mod tests { use pasta_curves::vesta; diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index fe24d10eda..7b1de78cbc 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -4,9 +4,9 @@ use ff::Field; use crate::{ circuit::{ - floor_planner::single_pass::SimpleTableLayouter, - layouter::{RegionColumn, RegionLayouter, RegionShape, TableLayouter}, - Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value, + layouter::{RegionColumn, RegionLayouter, RegionShape}, + table_layouter::SimpleTableLayouter, + Cell, Layouter, Region, RegionIndex, RegionStart, Table, TableLayouter, Value, }, plonk::{ Advice, Any, Assigned, Assignment, Circuit, Column, Error, Fixed, FloorPlanner, Instance, diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index 695c450432..a2d8188303 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -7,7 +7,7 @@ use std::fmt; use ff::Field; use super::{Cell, RegionIndex, Value}; -use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector, TableColumn}; +use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector}; /// Helper trait for implementing a custom [`Layouter`]. /// @@ -109,24 +109,6 @@ pub trait RegionLayouter: fmt::Debug { fn constrain_equal(&mut self, left: Cell, right: Cell) -> Result<(), Error>; } -/// Helper trait for implementing a custom [`Layouter`]. -/// -/// This trait is used for implementing table assignments. -/// -/// [`Layouter`]: super::Layouter -pub trait TableLayouter: fmt::Debug { - /// Assigns a fixed value to a table cell. - /// - /// Returns an error if the table cell has already been assigned to. - fn assign_cell<'v>( - &'v mut self, - annotation: &'v (dyn Fn() -> String + 'v), - column: TableColumn, - offset: usize, - to: &'v mut (dyn FnMut() -> Value> + 'v), - ) -> Result<(), Error>; -} - /// The shape of a region. For a region at a certain index, we track /// the set of columns it uses as well as the number of rows it uses. #[derive(Clone, Debug)] diff --git a/halo2_proofs/src/circuit/table_layouter.rs b/halo2_proofs/src/circuit/table_layouter.rs new file mode 100644 index 0000000000..ecf1688016 --- /dev/null +++ b/halo2_proofs/src/circuit/table_layouter.rs @@ -0,0 +1,107 @@ +//! Implementations of common table layouters. + +use std::{collections::HashMap, fmt}; + +use ff::Field; + +use crate::plonk::{Assigned, Assignment, Error, TableColumn}; + +use super::Value; + +/// Helper trait for implementing a custom [`Layouter`]. +/// +/// This trait is used for implementing table assignments. +/// +/// [`Layouter`]: super::Layouter +pub trait TableLayouter: std::fmt::Debug { + /// Assigns a fixed value to a table cell. + /// + /// Returns an error if the table cell has already been assigned to. + fn assign_cell<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: TableColumn, + offset: usize, + to: &'v mut (dyn FnMut() -> Value> + 'v), + ) -> Result<(), Error>; +} + +/// The default value to fill a table column with. +/// +/// - The outer `Option` tracks whether the value in row 0 of the table column has been +/// assigned yet. This will always be `Some` once a valid table has been completely +/// assigned. +/// - The inner `Value` tracks whether the underlying `Assignment` is evaluating +/// witnesses or not. +type DefaultTableValue = Option>>; + +pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment + 'a> { + cs: &'a mut CS, + 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, Vec)>, +} + +impl<'r, 'a, F: Field, CS: Assignment + 'a> fmt::Debug for SimpleTableLayouter<'r, 'a, F, CS> { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + f.debug_struct("SimpleTableLayouter") + .field("used_columns", &self.used_columns) + .field("default_and_assigned", &self.default_and_assigned) + .finish() + } +} + +impl<'r, 'a, F: Field, CS: Assignment + 'a> SimpleTableLayouter<'r, 'a, F, CS> { + pub(crate) fn new(cs: &'a mut CS, used_columns: &'r [TableColumn]) -> Self { + SimpleTableLayouter { + cs, + used_columns, + default_and_assigned: HashMap::default(), + } + } +} + +impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter + for SimpleTableLayouter<'r, 'a, F, CS> +{ + fn assign_cell<'v>( + &'v mut self, + annotation: &'v (dyn Fn() -> String + 'v), + column: TableColumn, + offset: usize, + to: &'v mut (dyn FnMut() -> Value> + 'v), + ) -> Result<(), Error> { + if self.used_columns.contains(&column) { + return Err(Error::Synthesis); // TODO better error + } + + let entry = self.default_and_assigned.entry(column).or_default(); + + let mut value = Value::unknown(); + self.cs.assign_fixed( + annotation, + column.inner(), + offset, // tables are always assigned starting at row 0 + || { + let res = to(); + value = res; + res + }, + )?; + + match (entry.0.is_none(), offset) { + // Use the value at offset 0 as the default value for this table column. + (true, 0) => entry.0 = Some(value), + // Since there is already an existing default value for this table column, + // the caller should not be attempting to assign another value at offset 0. + (false, 0) => return Err(Error::Synthesis), // TODO better error + _ => (), + } + if entry.1.len() <= offset { + entry.1.resize(offset + 1, false); + } + entry.1[offset] = true; + + Ok(()) + } +} From 327b47524c187a676bda0043748052c3de0444e1 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 21 Mar 2023 12:30:55 +0700 Subject: [PATCH 2/5] table_layouter::compute_table_lengths: Extract helper function --- .../src/circuit/floor_planner/single_pass.rs | 21 ++----------------- halo2_proofs/src/circuit/floor_planner/v1.rs | 21 ++----------------- halo2_proofs/src/circuit/table_layouter.rs | 21 +++++++++++++++++++ 3 files changed, 25 insertions(+), 38 deletions(-) diff --git a/halo2_proofs/src/circuit/floor_planner/single_pass.rs b/halo2_proofs/src/circuit/floor_planner/single_pass.rs index 2767854908..968c3726cc 100644 --- a/halo2_proofs/src/circuit/floor_planner/single_pass.rs +++ b/halo2_proofs/src/circuit/floor_planner/single_pass.rs @@ -8,7 +8,7 @@ use ff::Field; use crate::{ circuit::{ layouter::{RegionColumn, RegionLayouter, RegionShape}, - table_layouter::SimpleTableLayouter, + table_layouter::{compute_table_lengths, SimpleTableLayouter}, Cell, Layouter, Region, RegionIndex, RegionStart, Table, TableLayouter, Value, }, plonk::{ @@ -166,24 +166,7 @@ impl<'a, F: Field, CS: Assignment + 'a> Layouter for SingleChipLayouter<'a // Check that all table columns have the same length `first_unused`, // and all cells up to that length are assigned. - let first_unused = { - match default_and_assigned - .values() - .map(|(_, assigned)| { - if assigned.iter().all(|b| *b) { - Some(assigned.len()) - } else { - None - } - }) - .reduce(|acc, item| match (acc, item) { - (Some(a), Some(b)) if a == b => Some(a), - _ => None, - }) { - Some(Some(len)) => len, - _ => return Err(Error::Synthesis), // TODO better error - } - }; + let first_unused = compute_table_lengths(&default_and_assigned)?; // Record these columns so that we can prevent them from being used again. for column in default_and_assigned.keys() { diff --git a/halo2_proofs/src/circuit/floor_planner/v1.rs b/halo2_proofs/src/circuit/floor_planner/v1.rs index 7b1de78cbc..42f197ca37 100644 --- a/halo2_proofs/src/circuit/floor_planner/v1.rs +++ b/halo2_proofs/src/circuit/floor_planner/v1.rs @@ -5,7 +5,7 @@ use ff::Field; use crate::{ circuit::{ layouter::{RegionColumn, RegionLayouter, RegionShape}, - table_layouter::SimpleTableLayouter, + table_layouter::{compute_table_lengths, SimpleTableLayouter}, Cell, Layouter, Region, RegionIndex, RegionStart, Table, TableLayouter, Value, }, plonk::{ @@ -306,24 +306,7 @@ impl<'p, 'a, F: Field, CS: Assignment + 'a> AssignmentPass<'p, 'a, F, CS> { // Check that all table columns have the same length `first_unused`, // and all cells up to that length are assigned. - let first_unused = { - match default_and_assigned - .values() - .map(|(_, assigned)| { - if assigned.iter().all(|b| *b) { - Some(assigned.len()) - } else { - None - } - }) - .reduce(|acc, item| match (acc, item) { - (Some(a), Some(b)) if a == b => Some(a), - _ => None, - }) { - Some(Some(len)) => len, - _ => return Err(Error::Synthesis), // TODO better error - } - }; + let first_unused = compute_table_lengths(&default_and_assigned)?; // Record these columns so that we can prevent them from being used again. for column in default_and_assigned.keys() { diff --git a/halo2_proofs/src/circuit/table_layouter.rs b/halo2_proofs/src/circuit/table_layouter.rs index ecf1688016..255f2ea9cc 100644 --- a/halo2_proofs/src/circuit/table_layouter.rs +++ b/halo2_proofs/src/circuit/table_layouter.rs @@ -105,3 +105,24 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter Ok(()) } } + +pub(crate) fn compute_table_lengths( + default_and_assigned: &HashMap, Vec)>, +) -> Result { + match default_and_assigned + .values() + .map(|(_, assigned)| { + if assigned.iter().all(|b| *b) { + Some(assigned.len()) + } else { + None + } + }) + .reduce(|acc, item| match (acc, item) { + (Some(a), Some(b)) if a == b => Some(a), + _ => None, + }) { + Some(Some(len)) => Ok(len), + _ => return Err(Error::Synthesis), // TODO better error + } +} From 3f4710892ac2bbcc2c3d5d285499f3a085c72d59 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 21 Mar 2023 14:35:23 +0700 Subject: [PATCH 3/5] plonk::Error: Introduce TableError variant --- halo2_proofs/src/plonk/error.rs | 46 +++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) diff --git a/halo2_proofs/src/plonk/error.rs b/halo2_proofs/src/plonk/error.rs index 527dcdf38d..6e3131e798 100644 --- a/halo2_proofs/src/plonk/error.rs +++ b/halo2_proofs/src/plonk/error.rs @@ -2,6 +2,7 @@ use std::error; use std::fmt; use std::io; +use super::TableColumn; use super::{Any, Column}; /// This is an error that could occur during proving or circuit synthesis. @@ -37,6 +38,8 @@ pub enum Error { /// The instance sets up a copy constraint involving a column that has not been /// included in the permutation. ColumnNotInPermutation(Column), + /// An error relating to a lookup table. + TableError(TableError), } impl From for Error { @@ -79,6 +82,7 @@ impl fmt::Display for Error { "Column {:?} must be included in the permutation. Help: try applying `meta.enable_equalty` on the column", column ), + Error::TableError(error) => write!(f, "{}", error) } } } @@ -91,3 +95,45 @@ impl error::Error for Error { } } } + +/// This is an error that could occur during table synthesis. +#[derive(Debug)] +pub enum TableError { + /// A `TableColumn` has not been assigned. + ColumnNotAssigned(TableColumn), + /// A Table has columns of uneven lengths. + UnevenColumnLengths((TableColumn, usize), (TableColumn, usize)), + /// Attempt to assign a used `TableColumn` + UsedColumn(TableColumn), + /// Attempt to overwrite a default value + OverwriteDefault(TableColumn, String, String), +} + +impl fmt::Display for TableError { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + match self { + TableError::ColumnNotAssigned(col) => { + write!( + f, + "{:?} not fully assigned. Help: assign a value at offset 0.", + col + ) + } + TableError::UnevenColumnLengths((col, col_len), (table, table_len)) => write!( + f, + "{:?} has length {} while {:?} has length {}", + col, col_len, table, table_len + ), + TableError::UsedColumn(col) => { + write!(f, "{:?} has already been used", col) + } + TableError::OverwriteDefault(col, default, val) => { + write!( + f, + "Attempted to overwrite default value {} with {} in {:?}", + default, val, col + ) + } + } + } +} From c3c57c6e073e9d94ad763af1f114d2abb1275648 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 21 Mar 2023 15:55:12 +0700 Subject: [PATCH 4/5] circuit::table_layouter: Better table errors --- halo2_proofs/src/circuit/table_layouter.rs | 311 +++++++++++++++++++-- halo2_proofs/src/plonk/circuit.rs | 2 +- 2 files changed, 296 insertions(+), 17 deletions(-) diff --git a/halo2_proofs/src/circuit/table_layouter.rs b/halo2_proofs/src/circuit/table_layouter.rs index 255f2ea9cc..f2379f7095 100644 --- a/halo2_proofs/src/circuit/table_layouter.rs +++ b/halo2_proofs/src/circuit/table_layouter.rs @@ -1,10 +1,13 @@ //! Implementations of common table layouters. -use std::{collections::HashMap, fmt}; +use std::{ + collections::HashMap, + fmt::{self, Debug}, +}; use ff::Field; -use crate::plonk::{Assigned, Assignment, Error, TableColumn}; +use crate::plonk::{Assigned, Assignment, Error, TableColumn, TableError}; use super::Value; @@ -72,7 +75,7 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter to: &'v mut (dyn FnMut() -> Value> + 'v), ) -> Result<(), Error> { if self.used_columns.contains(&column) { - return Err(Error::Synthesis); // TODO better error + return Err(Error::TableError(TableError::UsedColumn(column))); } let entry = self.default_and_assigned.entry(column).or_default(); @@ -94,7 +97,13 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter (true, 0) => entry.0 = Some(value), // Since there is already an existing default value for this table column, // the caller should not be attempting to assign another value at offset 0. - (false, 0) => return Err(Error::Synthesis), // TODO better error + (false, 0) => { + return Err(Error::TableError(TableError::OverwriteDefault( + column, + format!("{:?}", entry.0.unwrap()), + format!("{:?}", value), + ))) + } _ => (), } if entry.1.len() <= offset { @@ -106,23 +115,293 @@ impl<'r, 'a, F: Field, CS: Assignment + 'a> TableLayouter } } -pub(crate) fn compute_table_lengths( +pub(crate) fn compute_table_lengths( default_and_assigned: &HashMap, Vec)>, ) -> Result { - match default_and_assigned - .values() - .map(|(_, assigned)| { + let column_lengths: Result, Error> = default_and_assigned + .iter() + .map(|(col, (default_value, assigned))| { + if default_value.is_none() || assigned.is_empty() { + return Err(Error::TableError(TableError::ColumnNotAssigned(*col))); + } if assigned.iter().all(|b| *b) { - Some(assigned.len()) + // All values in the column have been assigned + Ok((col, assigned.len())) + } else { + Err(Error::TableError(TableError::ColumnNotAssigned(*col))) + } + }) + .collect(); + let column_lengths = column_lengths?; + column_lengths + .into_iter() + .try_fold((None, 0), |acc, (col, col_len)| { + if acc.1 == 0 || acc.1 == col_len { + Ok((Some(*col), col_len)) } else { - None + let mut cols = [(*col, col_len), (acc.0.unwrap(), acc.1)]; + cols.sort(); + Err(Error::TableError(TableError::UnevenColumnLengths( + cols[0], cols[1], + ))) } }) - .reduce(|acc, item| match (acc, item) { - (Some(a), Some(b)) if a == b => Some(a), - _ => None, - }) { - Some(Some(len)) => Ok(len), - _ => return Err(Error::Synthesis), // TODO better error + .map(|col_len| col_len.1) +} + +#[cfg(test)] +mod tests { + use pasta_curves::Fp; + + use crate::{ + circuit::{Layouter, SimpleFloorPlanner}, + dev::MockProver, + plonk::{Circuit, ConstraintSystem}, + poly::Rotation, + }; + + use super::*; + + #[test] + fn table_no_default() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + table: TableColumn, + } + + struct FaultyCircuit; + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table = meta.lookup_table_column(); + + meta.lookup(|cells| { + let a = cells.query_advice(a, Rotation::cur()); + vec![(a, table)] + }); + + Self::Config { table } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_table( + || "duplicate assignment", + |mut table| { + table.assign_cell( + || "default", + config.table, + 1, + || Value::known(Fp::zero()), + ) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit, vec![]); + assert_eq!( + format!("{}", prover.unwrap_err()), + "TableColumn { inner: Column { index: 0, column_type: Fixed } } not fully assigned. Help: assign a value at offset 0." + ); + } + + #[test] + fn table_overwrite_default() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + table: TableColumn, + } + + struct FaultyCircuit; + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table = meta.lookup_table_column(); + + meta.lookup(|cells| { + let a = cells.query_advice(a, Rotation::cur()); + vec![(a, table)] + }); + + Self::Config { table } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_table( + || "duplicate assignment", + |mut table| { + table.assign_cell( + || "default", + config.table, + 0, + || Value::known(Fp::zero()), + )?; + table.assign_cell( + || "duplicate", + config.table, + 0, + || Value::known(Fp::zero()), + ) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit, vec![]); + assert_eq!( + format!("{}", prover.unwrap_err()), + "Attempted to overwrite default value Value { inner: Some(Trivial(0x0000000000000000000000000000000000000000000000000000000000000000)) } with Value { inner: Some(Trivial(0x0000000000000000000000000000000000000000000000000000000000000000)) } in TableColumn { inner: Column { index: 0, column_type: Fixed } }" + ); + } + + #[test] + fn table_reuse_column() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + table: TableColumn, + } + + struct FaultyCircuit; + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table = meta.lookup_table_column(); + + meta.lookup(|cells| { + let a = cells.query_advice(a, Rotation::cur()); + vec![(a, table)] + }); + + Self::Config { table } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_table( + || "first assignment", + |mut table| { + table.assign_cell( + || "default", + config.table, + 0, + || Value::known(Fp::zero()), + ) + }, + )?; + + layouter.assign_table( + || "reuse", + |mut table| { + table.assign_cell(|| "reuse", config.table, 1, || Value::known(Fp::zero())) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit, vec![]); + assert_eq!( + format!("{}", prover.unwrap_err()), + "TableColumn { inner: Column { index: 0, column_type: Fixed } } has already been used" + ); + } + + #[test] + fn table_uneven_columns() { + const K: u32 = 4; + + #[derive(Clone)] + struct FaultyCircuitConfig { + table: (TableColumn, TableColumn), + } + + struct FaultyCircuit; + + impl Circuit for FaultyCircuit { + type Config = FaultyCircuitConfig; + + type FloorPlanner = SimpleFloorPlanner; + + fn without_witnesses(&self) -> Self { + Self + } + + fn configure(meta: &mut ConstraintSystem) -> Self::Config { + let a = meta.advice_column(); + let table = (meta.lookup_table_column(), meta.lookup_table_column()); + meta.lookup(|cells| { + let a = cells.query_advice(a, Rotation::cur()); + + vec![(a.clone(), table.0), (a, table.1)] + }); + + Self::Config { table } + } + + fn synthesize( + &self, + config: Self::Config, + mut layouter: impl Layouter, + ) -> Result<(), Error> { + layouter.assign_table( + || "table with uneven columns", + |mut table| { + table.assign_cell(|| "", config.table.0, 0, || Value::known(Fp::zero()))?; + table.assign_cell(|| "", config.table.0, 1, || Value::known(Fp::zero()))?; + + table.assign_cell(|| "", config.table.1, 0, || Value::known(Fp::zero())) + }, + ) + } + } + + let prover = MockProver::run(K, &FaultyCircuit, vec![]); + assert_eq!( + format!("{}", prover.unwrap_err()), + "TableColumn { inner: Column { index: 0, column_type: Fixed } } has length 2 while TableColumn { inner: Column { index: 1, column_type: Fixed } } has length 1" + ); } } diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 334755dded..fb6a8b56ef 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -311,7 +311,7 @@ pub struct InstanceQuery { /// they cannot simultaneously be used as general fixed columns. /// /// [`Layouter::assign_table`]: crate::circuit::Layouter::assign_table -#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)] +#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash, Ord, PartialOrd)] pub struct TableColumn { /// The fixed column that this table column is stored in. /// From 72ce521084de8a1a87361b73040f7e234429efed Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Tue, 4 Apr 2023 09:27:32 +0700 Subject: [PATCH 5/5] circuit.rs: crate visibility modifications from code review Co-authored-by: Daira Hopwood Co-authored-by: ebfull --- halo2_proofs/src/circuit.rs | 2 +- halo2_proofs/src/circuit/layouter.rs | 1 + 2 files changed, 2 insertions(+), 1 deletion(-) diff --git a/halo2_proofs/src/circuit.rs b/halo2_proofs/src/circuit.rs index 1cdd6b360c..0822d8d8aa 100644 --- a/halo2_proofs/src/circuit.rs +++ b/halo2_proofs/src/circuit.rs @@ -13,7 +13,7 @@ pub mod floor_planner; pub use floor_planner::single_pass::SimpleFloorPlanner; pub mod layouter; -pub mod table_layouter; +mod table_layouter; pub use table_layouter::TableLayouter; diff --git a/halo2_proofs/src/circuit/layouter.rs b/halo2_proofs/src/circuit/layouter.rs index a2d8188303..81fa00bee5 100644 --- a/halo2_proofs/src/circuit/layouter.rs +++ b/halo2_proofs/src/circuit/layouter.rs @@ -6,6 +6,7 @@ use std::fmt; use ff::Field; +pub use super::table_layouter::TableLayouter; use super::{Cell, RegionIndex, Value}; use crate::plonk::{Advice, Any, Assigned, Column, Error, Fixed, Instance, Selector};