Skip to content

Commit

Permalink
feat: pick changes about mod circuit and mod dev
Browse files Browse the repository at this point in the history
  • Loading branch information
han0110 committed Aug 29, 2023
1 parent 132641c commit 05ab478
Show file tree
Hide file tree
Showing 15 changed files with 1,268 additions and 388 deletions.
3 changes: 3 additions & 0 deletions halo2_proofs/Cargo.toml
Original file line number Diff line number Diff line change
Expand Up @@ -63,6 +63,9 @@ maybe-rayon = { version = "0.1.0", default-features = false }
plotters = { version = "0.3.0", default-features = false, optional = true }
tabbycat = { version = "0.1", features = ["attributes"], optional = true }

# Legacy circuit compatibility
halo2_legacy_pdqsort = { version = "0.1.0", optional = true }

[dev-dependencies]
assert_matches = "1.5"
criterion = "0.3"
Expand Down
23 changes: 19 additions & 4 deletions halo2_proofs/src/circuit.rs
Original file line number Diff line number Diff line change
Expand Up @@ -13,9 +13,11 @@ pub use value::Value;

pub mod floor_planner;
pub use floor_planner::single_pass::SimpleFloorPlanner;
pub use floor_planner::single_pass::SimpleTableLayouter;

pub mod layouter;
mod table_layouter;

pub use table_layouter::{SimpleTableLayouter, TableLayouter};

/// A chip implements a set of instructions that can be used by gadgets.
///
Expand Down Expand Up @@ -314,6 +316,19 @@ impl<'r, F: Field> Region<'r, F> {
})
}

/// Returns the value of the instance column's cell at absolute location `row`.
///
/// This method is only provided for convenience; it does not create any constraints.
/// Callers still need to use [`Self::assign_advice_from_instance`] to constrain the
/// instance values in their circuit.
pub fn instance_value(
&mut self,
instance: Column<Instance>,
row: usize,
) -> Result<Value<F>, Error> {
self.region.instance_value(instance, row)
}

/// Assign a fixed value.
///
/// Even though `to` has `FnMut` bounds, it is guaranteed to be called at most once.
Expand Down Expand Up @@ -369,11 +384,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 }
}
}
Expand Down
110 changes: 10 additions & 100 deletions halo2_proofs/src/circuit/floor_planner/single_pass.rs
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@ use ff::Field;
use crate::{
circuit::{
layouter::{RegionColumn, RegionLayouter, RegionShape, SyncDeps, TableLayouter},
table_layouter::{compute_table_lengths, SimpleTableLayouter},
Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value,
},
plonk::{
Expand Down Expand Up @@ -167,24 +168,7 @@ impl<'a, F: Field, CS: Assignment<F> + 'a + SyncDeps> Layouter<F>

// 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() {
Expand Down Expand Up @@ -346,6 +330,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a + SyncDeps> RegionLayouter<F>
Ok((cell, value))
}

fn instance_value(
&mut self,
instance: Column<Instance>,
row: usize,
) -> Result<Value<F>, Error> {
self.layouter.cs.query_instance(instance, row)
}

fn assign_fixed<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
Expand Down Expand Up @@ -384,88 +376,6 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + 'a + SyncDeps> 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>>>;

/// A table layouter that can be used to assign values to a table.
pub 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 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> {
/// Returns a new SimpleTableLayouter
pub 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 halo2curves::pasta::vesta;
Expand Down
29 changes: 10 additions & 19 deletions halo2_proofs/src/circuit/floor_planner/v1.rs
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ use ff::Field;

use crate::{
circuit::{
floor_planner::single_pass::SimpleTableLayouter,
layouter::{RegionColumn, RegionLayouter, RegionShape, SyncDeps, TableLayouter},
table_layouter::{compute_table_lengths, SimpleTableLayouter},
Cell, Layouter, Region, RegionIndex, RegionStart, Table, Value,
},
plonk::{
Expand Down Expand Up @@ -313,24 +313,7 @@ impl<'p, 'a, F: Field, CS: Assignment<F> + SyncDeps> AssignmentPass<'p, 'a, F, C

// 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() {
Expand Down Expand Up @@ -455,6 +438,14 @@ impl<'r, 'a, F: Field, CS: Assignment<F> + SyncDeps> RegionLayouter<F> for V1Reg
Ok((cell, value))
}

fn instance_value(
&mut self,
instance: Column<Instance>,
row: usize,
) -> Result<Value<F>, Error> {
self.plan.cs.query_instance(instance, row)
}

fn assign_fixed<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
Expand Down
21 changes: 19 additions & 2 deletions halo2_proofs/src/circuit/floor_planner/v1/strategy.rs
Original file line number Diff line number Diff line change
Expand Up @@ -199,7 +199,7 @@ pub fn slot_in_biggest_advice_first(
region_shapes: Vec<RegionShape>,
) -> (Vec<RegionStart>, CircuitAllocations) {
let mut sorted_regions: Vec<_> = region_shapes.into_iter().collect();
sorted_regions.sort_unstable_by_key(|shape| {
let sort_key = |shape: &RegionShape| {
// Count the number of advice columns
let advice_cols = shape
.columns()
Expand All @@ -211,7 +211,24 @@ pub fn slot_in_biggest_advice_first(
.count();
// Sort by advice area (since this has the most contention).
advice_cols * shape.row_count()
});
};

// This used to incorrectly use `sort_unstable_by_key` with non-unique keys, which gave
// output that differed between 32-bit and 64-bit platforms, and potentially between Rust
// versions.
// We now use `sort_by_cached_key` with non-unique keys, and rely on `region_shapes`
// being sorted by region index (which we also rely on below to return `RegionStart`s
// in the correct order).
#[cfg(not(feature = "floor-planner-v1-legacy-pdqsort"))]
sorted_regions.sort_by_cached_key(sort_key);

// To preserve compatibility, when the "floor-planner-v1-legacy-pdqsort" feature is enabled,
// we use a copy of the pdqsort implementation from the Rust 1.56.1 standard library, fixed
// to its behaviour on 64-bit platforms.
// https://github.com/rust-lang/rust/blob/1.56.1/library/core/src/slice/mod.rs#L2365-L2402
#[cfg(feature = "floor-planner-v1-legacy-pdqsort")]
halo2_legacy_pdqsort::sort::quicksort(&mut sorted_regions, |a, b| sort_key(a).lt(&sort_key(b)));

sorted_regions.reverse();

// Lay out the sorted regions.
Expand Down
36 changes: 16 additions & 20 deletions halo2_proofs/src/circuit/layouter.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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, TableColumn};

Expand Down Expand Up @@ -98,7 +99,8 @@ pub trait RegionLayouter<F: Field>: fmt::Debug + SyncDeps {
/// Assign the value of the instance column's cell at absolute location
/// `row` to the column `advice` at `offset` within this region.
///
/// Returns the advice cell, and its value if known.
/// Returns the advice cell that has been equality-constrained to the
/// instance cell, and its value if known.
fn assign_advice_from_instance<'v>(
&mut self,
annotation: &'v (dyn Fn() -> String + 'v),
Expand All @@ -108,7 +110,11 @@ pub trait RegionLayouter<F: Field>: fmt::Debug + SyncDeps {
offset: usize,
) -> Result<(Cell, Value<F>), Error>;

/// Assign a fixed value
/// Returns the value of the instance column's cell at absolute location `row`.
fn instance_value(&mut self, instance: Column<Instance>, row: usize)
-> Result<Value<F>, Error>;

/// Assigns a fixed value
fn assign_fixed<'v>(
&'v mut self,
annotation: &'v (dyn Fn() -> String + 'v),
Expand All @@ -128,24 +134,6 @@ pub trait RegionLayouter<F: Field>: fmt::Debug + SyncDeps {
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)]
Expand Down Expand Up @@ -282,6 +270,14 @@ impl<F: Field> RegionLayouter<F> for RegionShape {
))
}

fn instance_value(
&mut self,
_instance: Column<Instance>,
_row: usize,
) -> Result<Value<F>, Error> {
Ok(Value::unknown())
}

fn assign_fixed<'v>(
&'v mut self,
_: &'v (dyn Fn() -> String + 'v),
Expand Down
Loading

0 comments on commit 05ab478

Please sign in to comment.