Merge pull request #208 from zcash/selector-type

Add a Selector type
This commit is contained in:
str4d 2021-02-26 05:01:32 +13:00 committed by GitHub
commit ecfd1dea91
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 92 additions and 11 deletions

View File

@ -7,7 +7,8 @@ use halo2::{
circuit::{layouter::SingleChip, Cell, Chip, Layouter},
dev::VerifyFailure,
plonk::{
Advice, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed, Instance, Permutation,
Advice, Assignment, Circuit, Column, ConstraintSystem, Error, Instance, Permutation,
Selector,
},
poly::Rotation,
};
@ -63,10 +64,10 @@ struct FieldConfig {
// any constraints on cells where `NumericInstructions::mul` is not being used.
// This is important when building larger circuits, where columns are used by
// multiple sets of instructions.
s_mul: Column<Fixed>,
s_mul: Selector,
// The selector for the public-input gate, which uses one of the advice columns.
s_pub: Column<Fixed>,
s_pub: Selector,
}
impl<F: FieldExt> FieldChip<F> {
@ -82,8 +83,8 @@ impl<F: FieldExt> FieldChip<F> {
.map(|column| (*column).into())
.collect::<Vec<_>>(),
);
let s_mul = meta.fixed_column();
let s_pub = meta.fixed_column();
let s_mul = meta.selector();
let s_pub = meta.selector();
// Define our multiplication gate!
meta.create_gate("mul", |meta| {
@ -102,7 +103,7 @@ impl<F: FieldExt> FieldChip<F> {
let lhs = meta.query_advice(advice[0], Rotation::cur());
let rhs = meta.query_advice(advice[1], Rotation::cur());
let out = meta.query_advice(advice[0], Rotation::next());
let s_mul = meta.query_fixed(s_mul, Rotation::cur());
let s_mul = meta.query_selector(s_mul, Rotation::cur());
// The polynomial expression returned from `create_gate` will be
// constrained by the proving system to equal zero. Our expression
@ -118,7 +119,7 @@ impl<F: FieldExt> FieldChip<F> {
// column for exposing numbers as public inputs.
let a = meta.query_advice(advice[1], Rotation::cur());
let p = meta.query_instance(instance, Rotation::cur());
let s = meta.query_fixed(s_pub, Rotation::cur());
let s = meta.query_selector(s_pub, Rotation::cur());
// We simply constrain the advice cell to be equal to the instance cell,
// when the selector is enabled.
@ -195,7 +196,7 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
// We only want to use a single multiplication gate in this region,
// so we enable it at region offset 0; this means it will constrain
// cells at offsets 0 and 1.
region.assign_fixed(|| "example mul", config.s_mul, 0, || Ok(F::one()))?;
config.s_mul.enable(&mut region, 0)?;
// The inputs we've been given could be located anywhere in the circuit,
// but we can only rely on relative offsets inside this region. So we
@ -241,7 +242,7 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
|| "expose public",
|mut region| {
// Enable the public-input gate.
region.assign_fixed(|| "public result", config.s_pub, 0, || Ok(F::one()))?;
config.s_pub.enable(&mut region, 0)?;
// Load the output into the correct advice column.
let out = region.assign_advice(

View File

@ -7,8 +7,11 @@ use std::{
};
use super::{lookup, permutation, Error};
use crate::arithmetic::FieldExt;
use crate::poly::Rotation;
use crate::{
arithmetic::FieldExt,
circuit::{Chip, Region},
poly::Rotation,
};
/// A column type
pub trait ColumnType: 'static + Sized + std::fmt::Debug {}
@ -127,6 +130,71 @@ impl TryFrom<Column<Any>> for Column<Instance> {
}
}
/// A selector, representing a fixed boolean value per row of the circuit.
///
/// Selectors can be used to conditionally enable (portions of) gates:
/// ```
/// use halo2::poly::Rotation;
/// # use halo2::pasta::Fp;
/// # use halo2::plonk::ConstraintSystem;
///
/// # let mut meta = ConstraintSystem::<Fp>::default();
/// let a = meta.advice_column();
/// let b = meta.advice_column();
/// let s = meta.selector();
///
/// meta.create_gate("foo", |meta| {
/// let a = meta.query_advice(a, Rotation::prev());
/// let b = meta.query_advice(b, Rotation::cur());
/// let s = meta.query_selector(s, Rotation::cur());
///
/// // On rows where the selector is enabled, a is constrained to equal b.
/// // On rows where the selector is disabled, a and b can take any value.
/// s * (a - b)
/// });
/// ```
///
/// Selectors are disabled on all rows by default, and must be explicitly enabled on each
/// row when required:
/// ```
/// use halo2::{circuit::{Chip, Layouter}, plonk::{Advice, Column, Error, Selector}};
/// # use ff::Field;
/// # use halo2::plonk::Fixed;
///
/// struct Config {
/// a: Column<Advice>,
/// b: Column<Advice>,
/// s: Selector,
/// }
///
/// fn circuit_logic<C: Chip>(mut layouter: impl Layouter<C>) -> Result<(), Error> {
/// let config = layouter.config().clone();
/// # let config: Config = todo!();
/// layouter.assign_region(|| "bar", |mut region| {
/// region.assign_advice(|| "a", config.a, 0, || Ok(C::Field::one()))?;
/// region.assign_advice(|| "a", config.b, 1, || Ok(C::Field::one()))?;
/// config.s.enable(&mut region, 1)
/// })?;
/// Ok(())
/// }
/// ```
#[derive(Clone, Copy, Debug)]
pub struct Selector(Column<Fixed>);
impl Selector {
/// Enable this selector at the given offset within the given region.
pub fn enable<C: Chip>(&self, region: &mut Region<C>, offset: usize) -> Result<(), Error> {
// TODO: Ensure that the default for a selector's cells is always zero, if we
// alter the proving system to change the global default.
// TODO: Add Region::enable_selector method to allow the layouter to control the
// selector's assignment.
// https://github.com/zcash/halo2/issues/116
region
.assign_fixed(|| "", self.0, offset, || Ok(C::Field::one()))
.map(|_| ())
}
}
/// A permutation.
#[derive(Clone, Debug)]
pub struct Permutation {
@ -507,6 +575,11 @@ impl<F: Field> ConstraintSystem<F> {
index
}
/// Query a selector at a relative position.
pub fn query_selector(&mut self, selector: Selector, at: Rotation) -> Expression<F> {
Expression::Fixed(self.query_fixed_index(selector.0, at))
}
fn query_fixed_index(&mut self, column: Column<Fixed>, at: Rotation) -> usize {
// Return existing query, if it exists
for (index, fixed_query) in self.fixed_queries.iter().enumerate() {
@ -642,6 +715,13 @@ impl<F: Field> ConstraintSystem<F> {
self.gates.push((name, poly));
}
/// Allocate a new selector.
pub fn selector(&mut self) -> Selector {
// TODO: Track selectors separately, and combine selectors where possible.
// https://github.com/zcash/halo2/issues/116
Selector(self.fixed_column())
}
/// Allocate a new fixed column
pub fn fixed_column(&mut self) -> Column<Fixed> {
let tmp = Column {