zec
/
halo2
mirror of https://github.com/zcash/halo2.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

[move-only] circuit::table_layouter: Move TableLayouter, SimpleTableLayouter

This commit is contained in:
therealyingtong 2023-03-21 12:23:37 +07:00
parent 2633567840
commit a8aebdb848
5 changed files with 120 additions and 107 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
halo2_proofs/src/circuit.rs
View File

@ -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<F>,
table: &'r mut dyn TableLayouter<F>,
}
impl<'r, F: Field> From<&'r mut dyn layouter::TableLayouter<F>> for Table<'r, F> {
fn from(table: &'r mut dyn layouter::TableLayouter<F>) -> Self {
impl<'r, F: Field> From<&'r mut dyn TableLayouter<F>> for Table<'r, F> {
fn from(table: &'r mut dyn TableLayouter<F>) -> Self {
Table { table }
}
}

85
halo2_proofs/src/circuit/floor_planner/single_pass.rs
View File

@ -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<F> + 'a> RegionLayouter<F>
}
}
/// 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<F> = Option<Value<Assigned<F>>>;
pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment<F> + '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<TableColumn, (DefaultTableValue<F>, Vec<bool>)>,
}
impl<'r, 'a, F: Field, CS: Assignment<F> + '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<F> + '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<F> + 'a> TableLayouter<F>
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<Assigned<F>> + '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;

6
halo2_proofs/src/circuit/floor_planner/v1.rs
View File

@ -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,

20
halo2_proofs/src/circuit/layouter.rs
View File

@ -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<F: Field>: 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<F: Field>: 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<Assigned<F>> + '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)]

107
halo2_proofs/src/circuit/table_layouter.rs Normal file
View File

@ -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<F: Field>: 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<Assigned<F>> + '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<F> = Option<Value<Assigned<F>>>;
pub(crate) struct SimpleTableLayouter<'r, 'a, F: Field, CS: Assignment<F> + '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<TableColumn, (DefaultTableValue<F>, Vec<bool>)>,
}
impl<'r, 'a, F: Field, CS: Assignment<F> + '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<F> + '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<F> + 'a> TableLayouter<F>
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<Assigned<F>> + '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(())
}
}