Merge pull request #185 from daira/aux-to-instance

Rename "auxiliary column" to "instance column" in the book and in code
This commit is contained in:
Daira Hopwood 2021-02-15 15:42:54 +00:00 committed by GitHub
commit 22297bbc89
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
15 changed files with 237 additions and 221 deletions

View File

@ -15,8 +15,10 @@ A UPA circuit depends on a ***configuration***:
* A finite field $\mathbb{F}$, where cell values (for a given statement and witness) will be
elements of $\mathbb{F}$.
* The number of columns in the matrix, and a specification of each column as being
***fixed***, ***advice***, or ***auxiliary***. Fixed columns are fixed by the circuit;
advice columns correspond to witness values; and auxiliary columns are used for public inputs.
***fixed***, ***advice***, or ***instance***. Fixed columns are fixed by the circuit;
advice columns correspond to witness values; and instance columns are normally used for
public inputs (technically, they can be used for any elements shared between the prover
and verifier).
* A subset of the columns that can participate in equality constraints.

View File

@ -1,7 +1,7 @@
# Chips
In order to combine functionality from several cores, we use a ***chip***. To implement a
chip, we define a set of fixed, advice, and auxiliary columns, and then specify how they
chip, we define a set of fixed, advice, and instance columns, and then specify how they
should be distributed between cores.
In the simplest case, each core will use columns disjoint from the other cores. However, it

View File

@ -4,13 +4,13 @@
At the start of proof creation, the prover has a table of cell assignments that it claims
satisfy the constraint system. The table has $n = 2^k$ rows, and is broken into advice,
auxiliary, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th row of
instance, and fixed columns. We define $F_{i,j}$ as the assignment in the $j$th row of
the $i$th fixed column. Without loss of generality, we'll similarly define $A_{i,j}$ to
represent the advice and auxiliary assignments.
represent the advice and instance assignments.
> We separate fixed columns here because they are provided by the verifier, whereas the
> advice and auxiliary columns are provided by the prover. In practice, the commitments to
> auxiliary and fixed columns are computed by both the prover and verifier, and only the
> advice and instance columns are provided by the prover. In practice, the commitments to
> instance and fixed columns are computed by both the prover and verifier, and only the
> advice commitments are stored in the proof.
To commit to these assignments, we construct Lagrange polynomials of degree $n - 1$ for

View File

@ -36,7 +36,7 @@ Halo 2's polynomial commitment scheme differs from Appendix A.2 of BCMS20 in two
1. Step 8 of the $\text{Open}$ algorithm computes a "non-hiding" commitment $C'$ prior to
the inner product argument, which opens to the same value as $C$ but is a commitment to
a randomly-drawn polynomial. The remainder of the protocol involves no blinding. By
contrast, in Halo 2 we blind every single commitment that we make (even for auxiliary
contrast, in Halo 2 we blind every single commitment that we make (even for instance
and fixed polynomials, though using a blinding factor of 1 for the fixed polynomials);
this makes the protocol simpler to reason about. As a consequence of this, the verifier
needs to handle the cumulative blinding factor at the end of the protocol, and so there

View File

@ -255,7 +255,7 @@ fn main() {
let sf = meta.fixed_column();
let c = meta.advice_column();
let d = meta.advice_column();
let p = meta.aux_column();
let p = meta.instance_column();
let perm = meta.permutation(&[a, b, c]);
let perm2 = meta.permutation(&[a, b, c]);
@ -269,19 +269,18 @@ fn main() {
let sl2 = meta.fixed_column();
/*
* A B ... sl sl2
* A B ... sl sl2
* [
* aux 0 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* ... ... ... ... ...
* ... ... ... aux 0
* ... ... ... a a
* ... ... ... a a^2
* ... ... ... 0 0
*
* instance 0 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* ... ... ... ... ...
* ... ... ... instance 0
* ... ... ... a a
* ... ... ... a a^2
* ... ... ... 0 0
* ]
*/
meta.lookup(&[a.into()], &[sl.into()]);
@ -305,7 +304,7 @@ fn main() {
meta.create_gate("Public input", |meta| {
let a = meta.query_advice(a, Rotation::cur());
let p = meta.query_aux(p, Rotation::cur());
let p = meta.query_instance(p, Rotation::cur());
let sp = meta.query_fixed(sp, Rotation::cur());
sp * (a + p * (-F::one()))
@ -374,8 +373,8 @@ fn main() {
let a = Fp::rand();
let a_squared = a * a;
let aux = Fp::one() + Fp::one();
let lookup_table = vec![aux, a, a, Fp::zero()];
let instance = Fp::one() + Fp::one();
let lookup_table = vec![instance, a, a, Fp::zero()];
let lookup_table_2 = vec![Fp::zero(), a, a_squared, Fp::zero()];
let circuit: MyCircuit<Fp> = MyCircuit {

View File

@ -194,7 +194,7 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
let a = meta.advice_column();
let b = meta.advice_column();
let c = meta.advice_column();
let p = meta.aux_column();
let p = meta.instance_column();
let perm = meta.permutation(&[a, b, c]);
@ -219,7 +219,7 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
meta.create_gate("Public input", |meta| {
let a = meta.query_advice(a, Rotation::cur());
let p = meta.query_aux(p, Rotation::cur());
let p = meta.query_instance(p, Rotation::cur());
let sp = meta.query_fixed(sp, Rotation::cur());
sp * (a + p * (-F::one()))

View File

@ -6,7 +6,7 @@ use halo2::{
arithmetic::FieldExt,
circuit::{layouter::SingleChip, Cell, Chip, Layouter, Permutation},
dev::VerifyFailure,
plonk::{Advice, Assignment, Aux, Circuit, Column, ConstraintSystem, Error, Fixed},
plonk::{Advice, Assignment, Circuit, Column, ConstraintSystem, Error, Fixed, Instance},
poly::Rotation,
};
@ -71,7 +71,7 @@ impl<F: FieldExt> FieldChip<F> {
fn configure(
meta: &mut ConstraintSystem<F>,
advice: [Column<Advice>; 2],
aux: Column<Aux>,
instance: Column<Instance>,
) -> FieldConfig {
let perm = Permutation::new(meta, &advice);
let s_mul = meta.fixed_column();
@ -109,10 +109,10 @@ impl<F: FieldExt> FieldChip<F> {
// We choose somewhat-arbitrarily that we will use the second advice
// column for exposing numbers as public inputs.
let a = meta.query_advice(advice[1], Rotation::cur());
let p = meta.query_aux(aux, Rotation::cur());
let p = meta.query_instance(instance, Rotation::cur());
let s = meta.query_fixed(s_pub, Rotation::cur());
// We simply constrain the advice cell to be equal to the aux cell,
// We simply constrain the advice cell to be equal to the instance cell,
// when the selector is enabled.
s * (p + a * -F::one())
});
@ -243,7 +243,7 @@ impl<F: FieldExt> NumericInstructions for FieldChip<F> {
)?;
region.constrain_equal(&config.perm, num.cell, out)?;
// We don't assign to the auxiliary column inside the circuit;
// We don't assign to the instance column inside the circuit;
// the mapping of public inputs to cells is provided to the prover.
Ok(())
},
@ -271,10 +271,10 @@ impl<F: FieldExt> Circuit<F> for MyCircuit<F> {
// We create the two advice columns that FieldChip uses for I/O.
let advice = [meta.advice_column(), meta.advice_column()];
// We also need an auxiliary column to store public inputs.
let aux = meta.aux_column();
// We also need an instance column to store public inputs.
let instance = meta.instance_column();
FieldChip::configure(meta, advice, aux)
FieldChip::configure(meta, advice, instance)
}
fn synthesize(&self, cs: &mut impl Assignment<F>, config: Self::Config) -> Result<(), Error> {
@ -322,7 +322,7 @@ fn main() {
};
// Arrange the public input. We expose the multiplication result in row 6
// of the aux column, so we position it there in our public inputs.
// of the instance column, so we position it there in our public inputs.
let mut public_inputs = vec![Fp::zero(); 1 << k];
public_inputs[6] = c;

View File

@ -130,9 +130,9 @@ pub enum VerifyFailure {
/// };
///
/// // This circuit has no public inputs.
/// let aux = vec![];
/// let instance = vec![];
///
/// let prover = MockProver::<Fp>::run(K, &circuit, aux).unwrap();
/// let prover = MockProver::<Fp>::run(K, &circuit, instance).unwrap();
/// assert_eq!(
/// prover.verify(),
/// Err(VerifyFailure::Gate {
@ -151,8 +151,8 @@ pub struct MockProver<F: Group> {
fixed: Vec<Vec<F>>,
// The advice cells in the circuit, arranged as [column][row].
advice: Vec<Vec<F>>,
// The aux cells in the circuit, arranged as [column][row].
aux: Vec<Vec<F>>,
// The instance cells in the circuit, arranged as [column][row].
instance: Vec<Vec<F>>,
permutations: Vec<permutation::keygen::Assembly>,
}
@ -244,7 +244,7 @@ impl<F: FieldExt> MockProver<F> {
pub fn run<ConcreteCircuit: Circuit<F>>(
k: u32,
circuit: &ConcreteCircuit,
aux: Vec<Vec<F>>,
instance: Vec<Vec<F>>,
) -> Result<Self, Error> {
let n = 1 << k;
@ -264,7 +264,7 @@ impl<F: FieldExt> MockProver<F> {
cs,
fixed,
advice,
aux,
instance,
permutations,
};
@ -298,7 +298,7 @@ impl<F: FieldExt> MockProver<F> {
if gate.evaluate(
&load(n, row, &self.cs.fixed_queries, &self.fixed),
&load(n, row, &self.cs.advice_queries, &self.advice),
&load(n, row, &self.cs.aux_queries, &self.aux),
&load(n, row, &self.cs.instance_queries, &self.instance),
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * scalar,
@ -319,7 +319,7 @@ impl<F: FieldExt> MockProver<F> {
let load = |column: &Column<Any>, row| match column.column_type() {
Any::Fixed => self.fixed[column.index()][row as usize],
Any::Advice => self.advice[column.index()][row as usize],
Any::Aux => self.aux[column.index()][row as usize],
Any::Instance => self.instance[column.index()][row as usize],
};
let inputs: Vec<_> = lookup

View File

@ -45,18 +45,18 @@ pub fn circuit_layout<F: Field, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>
// Figure out what order to render the columns in.
// TODO: For now, just render them in the order they were configured.
let total_columns = cs.num_advice_columns + cs.num_aux_columns + cs.num_fixed_columns;
let total_columns = cs.num_advice_columns + cs.num_instance_columns + cs.num_fixed_columns;
let column_index = |column: &Column<Any>| {
column.index()
+ match column.column_type() {
Any::Advice => 0,
Any::Aux => cs.num_advice_columns,
Any::Fixed => cs.num_advice_columns + cs.num_aux_columns,
Any::Instance => cs.num_advice_columns,
Any::Fixed => cs.num_advice_columns + cs.num_instance_columns,
}
};
// Prepare the grid layout. We render a red background for advice columns, white for
// aux columns, and blue for fixed columns.
// instance columns, and blue for fixed columns.
let root =
drawing_area.apply_coord_spec(Cartesian2d::<RangedCoordusize, RangedCoordusize>::new(
0..total_columns,
@ -73,7 +73,7 @@ pub fn circuit_layout<F: Field, ConcreteCircuit: Circuit<F>, DB: DrawingBackend>
))?;
root.draw(&Rectangle::new(
[
(cs.num_advice_columns + cs.num_aux_columns, 0),
(cs.num_advice_columns + cs.num_instance_columns, 0),
(total_columns, layout.total_rows),
],
ShapeStyle::from(&BLUE.mix(0.2)).filled(),

View File

@ -394,7 +394,7 @@ fn test_proving() {
let sf = meta.fixed_column();
let c = meta.advice_column();
let d = meta.advice_column();
let p = meta.aux_column();
let p = meta.instance_column();
let perm = meta.permutation(&[a, b, c]);
let perm2 = meta.permutation(&[a, b, c]);
@ -408,19 +408,18 @@ fn test_proving() {
let sl2 = meta.fixed_column();
/*
* A B ... sl sl2
* A B ... sl sl2
* [
* aux 0 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* ... ... ... ... ...
* ... ... ... aux 0
* ... ... ... a a
* ... ... ... a a^2
* ... ... ... 0 0
*
* instance 0 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* a a ... 0 0
* a a^2 ... 0 0
* ... ... ... ... ...
* ... ... ... instance 0
* ... ... ... a a
* ... ... ... a a^2
* ... ... ... 0 0
* ]
*/
meta.lookup(&[a.into()], &[sl.into()]);
@ -444,7 +443,7 @@ fn test_proving() {
meta.create_gate("Public input", |meta| {
let a = meta.query_advice(a, Rotation::cur());
let p = meta.query_aux(p, Rotation::cur());
let p = meta.query_instance(p, Rotation::cur());
let sp = meta.query_fixed(sp, Rotation::cur());
sp * (a + p * (-F::one()))
@ -507,8 +506,8 @@ fn test_proving() {
let a = Fp::rand();
let a_squared = a * &a;
let aux = Fp::one() + Fp::one();
let lookup_table = vec![aux, a, a, Fp::zero()];
let instance = Fp::one() + Fp::one();
let lookup_table = vec![instance, a, a, Fp::zero()];
let lookup_table_2 = vec![Fp::zero(), a, a_squared, Fp::zero()];
let empty_circuit: MyCircuit<Fp> = MyCircuit {
@ -526,7 +525,7 @@ fn test_proving() {
let pk = keygen_pk(&params, vk, &empty_circuit).expect("keygen_pk should not fail");
let mut pubinputs = pk.get_vk().get_domain().empty_lagrange();
pubinputs[0] = aux;
pubinputs[0] = instance;
let pubinput = params
.commit_lagrange(&pubinputs, Blind::default())
.to_affine();

View File

@ -37,24 +37,24 @@ pub struct Advice;
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Fixed;
/// An auxiliary column
/// An instance column
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub struct Aux;
pub struct Instance;
/// An enum over the Advice, Fixed, Aux structs
/// An enum over the Advice, Fixed, Instance structs
#[derive(Clone, Copy, Debug, Eq, PartialEq, Hash)]
pub enum Any {
/// An Advice variant
Advice,
/// A Fixed variant
Fixed,
/// An Auxiliary variant
Aux,
/// An Instance variant
Instance,
}
impl ColumnType for Advice {}
impl ColumnType for Fixed {}
impl ColumnType for Aux {}
impl ColumnType for Instance {}
impl ColumnType for Any {}
impl From<Column<Advice>> for Column<Any> {
@ -75,11 +75,11 @@ impl From<Column<Fixed>> for Column<Any> {
}
}
impl From<Column<Aux>> for Column<Any> {
fn from(advice: Column<Aux>) -> Column<Any> {
impl From<Column<Instance>> for Column<Any> {
fn from(advice: Column<Instance>) -> Column<Any> {
Column {
index: advice.index(),
column_type: Any::Aux,
column_type: Any::Instance,
}
}
}
@ -112,16 +112,16 @@ impl TryFrom<Column<Any>> for Column<Fixed> {
}
}
impl TryFrom<Column<Any>> for Column<Aux> {
impl TryFrom<Column<Any>> for Column<Instance> {
type Error = &'static str;
fn try_from(any: Column<Any>) -> Result<Self, Self::Error> {
match any.column_type() {
Any::Aux => Ok(Column {
Any::Instance => Ok(Column {
index: any.index(),
column_type: Aux,
column_type: Instance,
}),
_ => Err("Cannot convert into Column<Aux>"),
_ => Err("Cannot convert into Column<Instance>"),
}
}
}
@ -228,8 +228,8 @@ pub enum Expression<F> {
Fixed(usize),
/// This is an advice (witness) column queried at a certain relative location
Advice(usize),
/// This is an auxiliary (external) column queried at a certain relative location
Aux(usize),
/// This is an instance (external) column queried at a certain relative location
Instance(usize),
/// This is the sum of two polynomials
Sum(Box<Expression<F>>, Box<Expression<F>>),
/// This is the product of two polynomials
@ -245,7 +245,7 @@ impl<F: Field> Expression<F> {
&self,
fixed_column: &impl Fn(usize) -> T,
advice_column: &impl Fn(usize) -> T,
aux_column: &impl Fn(usize) -> T,
instance_column: &impl Fn(usize) -> T,
sum: &impl Fn(T, T) -> T,
product: &impl Fn(T, T) -> T,
scaled: &impl Fn(T, F) -> T,
@ -253,12 +253,12 @@ impl<F: Field> Expression<F> {
match self {
Expression::Fixed(index) => fixed_column(*index),
Expression::Advice(index) => advice_column(*index),
Expression::Aux(index) => aux_column(*index),
Expression::Instance(index) => instance_column(*index),
Expression::Sum(a, b) => {
let a = a.evaluate(
fixed_column,
advice_column,
aux_column,
instance_column,
sum,
product,
scaled,
@ -266,7 +266,7 @@ impl<F: Field> Expression<F> {
let b = b.evaluate(
fixed_column,
advice_column,
aux_column,
instance_column,
sum,
product,
scaled,
@ -277,7 +277,7 @@ impl<F: Field> Expression<F> {
let a = a.evaluate(
fixed_column,
advice_column,
aux_column,
instance_column,
sum,
product,
scaled,
@ -285,7 +285,7 @@ impl<F: Field> Expression<F> {
let b = b.evaluate(
fixed_column,
advice_column,
aux_column,
instance_column,
sum,
product,
scaled,
@ -296,7 +296,7 @@ impl<F: Field> Expression<F> {
let a = a.evaluate(
fixed_column,
advice_column,
aux_column,
instance_column,
sum,
product,
scaled,
@ -311,7 +311,7 @@ impl<F: Field> Expression<F> {
match self {
Expression::Fixed(_) => 1,
Expression::Advice(_) => 1,
Expression::Aux(_) => 1,
Expression::Instance(_) => 1,
Expression::Sum(a, b) => max(a.degree(), b.degree()),
Expression::Product(a, b) => a.degree() + b.degree(),
Expression::Scaled(poly, _) => poly.degree(),
@ -365,10 +365,10 @@ pub(crate) struct PointIndex(pub usize);
pub struct ConstraintSystem<F> {
pub(crate) num_fixed_columns: usize,
pub(crate) num_advice_columns: usize,
pub(crate) num_aux_columns: usize,
pub(crate) num_instance_columns: usize,
pub(crate) gates: Vec<(&'static str, Expression<F>)>,
pub(crate) advice_queries: Vec<(Column<Advice>, Rotation)>,
pub(crate) aux_queries: Vec<(Column<Aux>, Rotation)>,
pub(crate) instance_queries: Vec<(Column<Instance>, Rotation)>,
pub(crate) fixed_queries: Vec<(Column<Fixed>, Rotation)>,
// Vector of permutation arguments, where each corresponds to a sequence of columns
@ -385,11 +385,11 @@ impl<F: Field> Default for ConstraintSystem<F> {
ConstraintSystem {
num_fixed_columns: 0,
num_advice_columns: 0,
num_aux_columns: 0,
num_instance_columns: 0,
gates: vec![],
fixed_queries: Vec::new(),
advice_queries: Vec::new(),
aux_queries: Vec::new(),
instance_queries: Vec::new(),
permutations: Vec::new(),
lookups: Vec::new(),
}
@ -474,31 +474,33 @@ impl<F: Field> ConstraintSystem<F> {
Expression::Advice(self.query_advice_index(column, at))
}
fn query_aux_index(&mut self, column: Column<Aux>, at: Rotation) -> usize {
fn query_instance_index(&mut self, column: Column<Instance>, at: Rotation) -> usize {
// Return existing query, if it exists
for (index, aux_query) in self.aux_queries.iter().enumerate() {
if aux_query == &(column, at) {
for (index, instance_query) in self.instance_queries.iter().enumerate() {
if instance_query == &(column, at) {
return index;
}
}
// Make a new query
let index = self.aux_queries.len();
self.aux_queries.push((column, at));
let index = self.instance_queries.len();
self.instance_queries.push((column, at));
index
}
/// Query an auxiliary column at a relative position
pub fn query_aux(&mut self, column: Column<Aux>, at: Rotation) -> Expression<F> {
Expression::Aux(self.query_aux_index(column, at))
/// Query an instance column at a relative position
pub fn query_instance(&mut self, column: Column<Instance>, at: Rotation) -> Expression<F> {
Expression::Instance(self.query_instance_index(column, at))
}
fn query_any_index(&mut self, column: Column<Any>, at: Rotation) -> usize {
match column.column_type() {
Any::Advice => self.query_advice_index(Column::<Advice>::try_from(column).unwrap(), at),
Any::Fixed => self.query_fixed_index(Column::<Fixed>::try_from(column).unwrap(), at),
Any::Aux => self.query_aux_index(Column::<Aux>::try_from(column).unwrap(), at),
Any::Instance => {
self.query_instance_index(Column::<Instance>::try_from(column).unwrap(), at)
}
}
}
@ -511,9 +513,9 @@ impl<F: Field> ConstraintSystem<F> {
Any::Fixed => Expression::Fixed(
self.query_fixed_index(Column::<Fixed>::try_from(column).unwrap(), at),
),
Any::Aux => {
Expression::Aux(self.query_aux_index(Column::<Aux>::try_from(column).unwrap(), at))
}
Any::Instance => Expression::Instance(
self.query_instance_index(Column::<Instance>::try_from(column).unwrap(), at),
),
}
}
@ -537,14 +539,14 @@ impl<F: Field> ConstraintSystem<F> {
panic!("get_fixed_query_index called for non-existent query");
}
pub(crate) fn get_aux_query_index(&self, column: Column<Aux>, at: Rotation) -> usize {
for (index, aux_query) in self.aux_queries.iter().enumerate() {
if aux_query == &(column, at) {
pub(crate) fn get_instance_query_index(&self, column: Column<Instance>, at: Rotation) -> usize {
for (index, instance_query) in self.instance_queries.iter().enumerate() {
if instance_query == &(column, at) {
return index;
}
}
panic!("get_aux_query_index called for non-existent query");
panic!("get_instance_query_index called for non-existent query");
}
pub(crate) fn get_any_query_index(&self, column: Column<Any>, at: Rotation) -> usize {
@ -555,7 +557,9 @@ impl<F: Field> ConstraintSystem<F> {
Any::Fixed => {
self.get_fixed_query_index(Column::<Fixed>::try_from(column).unwrap(), at)
}
Any::Aux => self.get_aux_query_index(Column::<Aux>::try_from(column).unwrap(), at),
Any::Instance => {
self.get_instance_query_index(Column::<Instance>::try_from(column).unwrap(), at)
}
}
}
@ -585,13 +589,13 @@ impl<F: Field> ConstraintSystem<F> {
tmp
}
/// Allocate a new auxiliary column
pub fn aux_column(&mut self) -> Column<Aux> {
/// Allocate a new instance column
pub fn instance_column(&mut self) -> Column<Instance> {
let tmp = Column {
index: self.num_aux_columns,
column_type: Aux,
index: self.num_instance_columns,
column_type: Instance,
};
self.num_aux_columns += 1;
self.num_instance_columns += 1;
tmp
}
}

View File

@ -75,10 +75,10 @@ impl Argument {
theta: ChallengeTheta<C>,
advice_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
fixed_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
aux_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
instance_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
advice_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
fixed_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
aux_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
instance_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
transcript: &mut T,
) -> Result<Permuted<'a, C>, Error> {
// Closure to get values of columns and compress them
@ -90,7 +90,7 @@ impl Argument {
let (values, cosets) = match column.column_type() {
Any::Advice => (advice_values, advice_cosets),
Any::Fixed => (fixed_values, fixed_cosets),
Any::Aux => (aux_values, aux_cosets),
Any::Instance => (instance_values, instance_cosets),
};
(
&values[column.index()],

View File

@ -107,7 +107,7 @@ impl<C: CurveAffine> Evaluated<C> {
gamma: ChallengeGamma<C>,
advice_evals: &[C::Scalar],
fixed_evals: &[C::Scalar],
aux_evals: &[C::Scalar],
instance_evals: &[C::Scalar],
) -> impl Iterator<Item = C::Scalar> + 'a {
let product_expression = || {
// z'(X) (a'(X) + \beta) (s'(X) + \gamma)
@ -124,7 +124,7 @@ impl<C: CurveAffine> Evaluated<C> {
match column.column_type() {
Any::Advice => advice_evals[index],
Any::Fixed => fixed_evals[index],
Any::Aux => aux_evals[index],
Any::Instance => instance_evals[index],
}
})
.fold(C::Scalar::zero(), |acc, eval| acc * &*theta + &eval)

View File

@ -21,11 +21,11 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
params: &Params<C>,
pk: &ProvingKey<C>,
circuits: &[ConcreteCircuit],
auxs: &[&[Polynomial<C::Scalar, LagrangeCoeff>]],
instances: &[&[Polynomial<C::Scalar, LagrangeCoeff>]],
transcript: &mut T,
) -> Result<(), Error> {
for aux in auxs.iter() {
if aux.len() != pk.vk.cs.num_aux_columns {
for instance in instances.iter() {
if instance.len() != pk.vk.cs.num_instance_columns {
return Err(Error::IncompatibleParams);
}
}
@ -34,32 +34,35 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
let mut meta = ConstraintSystem::default();
let config = ConcreteCircuit::configure(&mut meta);
struct AuxSingle<'a, C: CurveAffine> {
pub aux_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
pub aux_polys: Vec<Polynomial<C::Scalar, Coeff>>,
pub aux_cosets: Vec<Polynomial<C::Scalar, ExtendedLagrangeCoeff>>,
struct InstanceSingle<'a, C: CurveAffine> {
pub instance_values: &'a [Polynomial<C::Scalar, LagrangeCoeff>],
pub instance_polys: Vec<Polynomial<C::Scalar, Coeff>>,
pub instance_cosets: Vec<Polynomial<C::Scalar, ExtendedLagrangeCoeff>>,
}
let aux: Vec<AuxSingle<C>> = auxs
let instance: Vec<InstanceSingle<C>> = instances
.iter()
.map(|aux| -> Result<AuxSingle<C>, Error> {
let aux_commitments_projective: Vec<_> = aux
.map(|instance| -> Result<InstanceSingle<C>, Error> {
let instance_commitments_projective: Vec<_> = instance
.iter()
.map(|poly| params.commit_lagrange(poly, Blind::default()))
.collect();
let mut aux_commitments = vec![C::zero(); aux_commitments_projective.len()];
C::Projective::batch_to_affine(&aux_commitments_projective, &mut aux_commitments);
let aux_commitments = aux_commitments;
drop(aux_commitments_projective);
metrics::counter!("aux_commitments", aux_commitments.len() as u64);
let mut instance_commitments = vec![C::zero(); instance_commitments_projective.len()];
C::Projective::batch_to_affine(
&instance_commitments_projective,
&mut instance_commitments,
);
let instance_commitments = instance_commitments;
drop(instance_commitments_projective);
metrics::counter!("instance_commitments", instance_commitments.len() as u64);
for commitment in &aux_commitments {
for commitment in &instance_commitments {
transcript
.common_point(*commitment)
.map_err(|_| Error::TranscriptError)?;
}
let aux_polys: Vec<_> = aux
let instance_polys: Vec<_> = instance
.iter()
.map(|poly| {
let lagrange_vec = domain.lagrange_from_vec(poly.to_vec());
@ -67,19 +70,19 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
})
.collect();
let aux_cosets: Vec<_> = meta
.aux_queries
let instance_cosets: Vec<_> = meta
.instance_queries
.iter()
.map(|&(column, at)| {
let poly = aux_polys[column.index()].clone();
let poly = instance_polys[column.index()].clone();
domain.coeff_to_extended(poly, at)
})
.collect();
Ok(AuxSingle {
aux_values: *aux,
aux_polys,
aux_cosets,
Ok(InstanceSingle {
instance_values: *instance,
instance_polys,
instance_cosets,
})
})
.collect::<Result<Vec<_>, _>>()?;
@ -238,10 +241,10 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
// Sample theta challenge for keeping lookup columns linearly independent
let theta = ChallengeTheta::get(transcript);
let lookups: Vec<Vec<lookup::prover::Permuted<'_, C>>> = aux
let lookups: Vec<Vec<lookup::prover::Permuted<'_, C>>> = instance
.iter()
.zip(advice.iter())
.map(|(aux, advice)| -> Result<Vec<_>, Error> {
.map(|(instance, advice)| -> Result<Vec<_>, Error> {
// Construct and commit to permuted values for each lookup
pk.vk
.cs
@ -255,10 +258,10 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
theta,
&advice.advice_values,
&pk.fixed_values,
&aux.aux_values,
&instance.instance_values,
&advice.advice_cosets,
&pk.fixed_cosets,
&aux.aux_cosets,
&instance.instance_cosets,
transcript,
)
})
@ -343,18 +346,18 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
let expressions = advice
.iter()
.zip(aux.iter())
.zip(instance.iter())
.zip(permutation_expressions.into_iter())
.zip(lookup_expressions.into_iter())
.flat_map(
|(((advice, aux), permutation_expressions), lookup_expressions)| {
|(((advice, instance), permutation_expressions), lookup_expressions)| {
iter::empty()
// Custom constraints
.chain(meta.gates.iter().map(move |(_, poly)| {
poly.evaluate(
&|index| pk.fixed_cosets[index].clone(),
&|index| advice.advice_cosets[index].clone(),
&|index| aux.aux_cosets[index].clone(),
&|index| instance.instance_cosets[index].clone(),
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * scalar,
@ -372,19 +375,22 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
let x = ChallengeX::get(transcript);
// Compute and hash aux evals for each circuit instance
for aux in aux.iter() {
// Compute and hash instance evals for each circuit instance
for instance in instance.iter() {
// Evaluate polynomials at omega^i x
let aux_evals: Vec<_> = meta
.aux_queries
let instance_evals: Vec<_> = meta
.instance_queries
.iter()
.map(|&(column, at)| {
eval_polynomial(&aux.aux_polys[column.index()], domain.rotate_omega(*x, at))
eval_polynomial(
&instance.instance_polys[column.index()],
domain.rotate_omega(*x, at),
)
})
.collect();
// Hash each aux column evaluation
for eval in aux_evals.iter() {
// Hash each instance column evaluation
for eval in instance_evals.iter() {
transcript
.write_scalar(*eval)
.map_err(|_| Error::TranscriptError)?;
@ -454,21 +460,21 @@ pub fn create_proof<C: CurveAffine, T: TranscriptWrite<C>, ConcreteCircuit: Circ
})
.collect::<Result<Vec<_>, _>>()?;
let instances = aux
let instances = instance
.iter()
.zip(advice.iter())
.zip(permutations.iter())
.zip(lookups.iter())
.flat_map(|(((aux, advice), permutations), lookups)| {
.flat_map(|(((instance, advice), permutations), lookups)| {
iter::empty()
.chain(
pk.vk
.cs
.aux_queries
.instance_queries
.iter()
.map(move |&(column, at)| ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &aux.aux_polys[column.index()],
poly: &instance.instance_polys[column.index()],
blind: Blind::default(),
}),
)

View File

@ -17,21 +17,21 @@ pub fn verify_proof<'a, C: CurveAffine, T: TranscriptRead<C>>(
params: &'a Params<C>,
vk: &VerifyingKey<C>,
msm: MSM<'a, C>,
aux_commitments: &[&[C]],
instance_commitments: &[&[C]],
transcript: &mut T,
) -> Result<Guard<'a, C>, Error> {
// Check that aux_commitments matches the expected number of aux columns
for aux_commitments in aux_commitments.iter() {
if aux_commitments.len() != vk.cs.num_aux_columns {
// Check that instance_commitments matches the expected number of instance columns
for instance_commitments in instance_commitments.iter() {
if instance_commitments.len() != vk.cs.num_instance_columns {
return Err(Error::IncompatibleParams);
}
}
let num_proofs = aux_commitments.len();
let num_proofs = instance_commitments.len();
for aux_commitments in aux_commitments.iter() {
// Hash the aux (external) commitments into the transcript
for commitment in *aux_commitments {
for instance_commitments in instance_commitments.iter() {
// Hash the instance (external) commitments into the transcript
for commitment in *instance_commitments {
transcript
.common_point(*commitment)
.map_err(|_| Error::TranscriptError)?
@ -96,9 +96,10 @@ pub fn verify_proof<'a, C: CurveAffine, T: TranscriptRead<C>>(
// satisfied with high probability.
let x = ChallengeX::get(transcript);
let aux_evals = (0..num_proofs)
let instance_evals = (0..num_proofs)
.map(|_| -> Result<Vec<_>, _> {
read_n_scalars(transcript, vk.cs.aux_queries.len()).map_err(|_| Error::TranscriptError)
read_n_scalars(transcript, vk.cs.instance_queries.len())
.map_err(|_| Error::TranscriptError)
})
.collect::<Result<Vec<_>, _>>()?;
@ -150,76 +151,81 @@ pub fn verify_proof<'a, C: CurveAffine, T: TranscriptRead<C>>(
// Compute the expected value of h(x)
let expressions = advice_evals
.iter()
.zip(aux_evals.iter())
.zip(instance_evals.iter())
.zip(permutations_evaluated.iter())
.zip(lookups_evaluated.iter())
.flat_map(|(((advice_evals, aux_evals), permutations), lookups)| {
let fixed_evals = fixed_evals.clone();
let fixed_evals_copy = fixed_evals.clone();
.flat_map(
|(((advice_evals, instance_evals), permutations), lookups)| {
let fixed_evals = fixed_evals.clone();
let fixed_evals_copy = fixed_evals.clone();
std::iter::empty()
// Evaluate the circuit using the custom gates provided
.chain(vk.cs.gates.iter().map(move |(_, poly)| {
poly.evaluate(
&|index| fixed_evals[index],
&|index| advice_evals[index],
&|index| aux_evals[index],
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * &scalar,
std::iter::empty()
// Evaluate the circuit using the custom gates provided
.chain(vk.cs.gates.iter().map(move |(_, poly)| {
poly.evaluate(
&|index| fixed_evals[index],
&|index| advice_evals[index],
&|index| instance_evals[index],
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * &scalar,
)
}))
.chain(
permutations
.iter()
.zip(vk.cs.permutations.iter())
.flat_map(move |(p, argument)| {
p.expressions(vk, argument, &advice_evals, l_0, beta, gamma, x)
})
.into_iter(),
)
}))
.chain(
permutations
.iter()
.zip(vk.cs.permutations.iter())
.flat_map(move |(p, argument)| {
p.expressions(vk, argument, &advice_evals, l_0, beta, gamma, x)
})
.into_iter(),
)
.chain(
lookups
.iter()
.zip(vk.cs.lookups.iter())
.flat_map(move |(p, argument)| {
p.expressions(
vk,
l_0,
argument,
theta,
beta,
gamma,
&advice_evals,
&fixed_evals_copy,
&aux_evals,
)
})
.into_iter(),
)
});
.chain(
lookups
.iter()
.zip(vk.cs.lookups.iter())
.flat_map(move |(p, argument)| {
p.expressions(
vk,
l_0,
argument,
theta,
beta,
gamma,
&advice_evals,
&fixed_evals_copy,
&instance_evals,
)
})
.into_iter(),
)
},
);
vanishing.verify(expressions, y, xn)?;
}
let queries = aux_commitments
let queries = instance_commitments
.iter()
.zip(aux_evals.iter())
.zip(instance_evals.iter())
.zip(advice_commitments.iter())
.zip(advice_evals.iter())
.zip(permutations_evaluated.iter())
.zip(lookups_evaluated.iter())
.flat_map(
|(
((((aux_commitments, aux_evals), advice_commitments), advice_evals), permutations),
(
(((instance_commitments, instance_evals), advice_commitments), advice_evals),
permutations,
),
lookups,
)| {
iter::empty()
.chain(vk.cs.aux_queries.iter().enumerate().map(
.chain(vk.cs.instance_queries.iter().enumerate().map(
move |(query_index, &(column, at))| VerifierQuery {
point: vk.domain.rotate_omega(*x, at),
commitment: &aux_commitments[column.index()],
eval: aux_evals[query_index],
commitment: &instance_commitments[column.index()],
eval: instance_evals[query_index],
},
))
.chain(vk.cs.advice_queries.iter().enumerate().map(