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

Merge a845b81f10 into 7df93fd855

This commit is contained in:
ying tong 2024-03-04 16:25:12 +05:30 committed by GitHub
parent 7df93fd855 a845b81f10
commit dd1ffe93dd
No known key found for this signature in database
GPG Key ID: B5690EEEBB952194
7 changed files with 884 additions and 103 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
halo2_proofs/src/plonk.rs
View File

@ -20,6 +20,7 @@ mod circuit;
mod error;
mod keygen;
mod lookup;
mod multiset_equality;
pub(crate) mod permutation;
mod vanishing;

44
halo2_proofs/src/plonk/circuit.rs
View File

@ -6,7 +6,7 @@ use std::{
ops::{Neg, Sub},
};
use super::{lookup, permutation, Assigned, Error};
use super::{lookup, multiset_equality, permutation, Assigned, Error};
use crate::{
circuit::{Layouter, Region, Value},
poly::Rotation,
@ -954,6 +954,11 @@ pub struct ConstraintSystem<F: Field> {
// Permutation argument for performing equality constraints
pub(crate) permutation: permutation::Argument,
// Vector of multiset equality arguments, where each corresponds to a
// sequence of unpermuted expressions and a sequence of permuted
// expressions involved in the multiset equality.
pub(crate) multisets: Vec<multiset_equality::Argument<F>>,
// Vector of lookup arguments, where each corresponds to a sequence of
// input expressions and a sequence of table expressions involved in the lookup.
pub(crate) lookups: Vec<lookup::Argument<F>>,
@ -1007,6 +1012,7 @@ impl<F: Field> Default for ConstraintSystem<F> {
num_advice_queries: Vec::new(),
instance_queries: Vec::new(),
permutation: permutation::Argument::new(),
multisets: Vec::new(),
lookups: Vec::new(),
constants: vec![],
minimum_degree: None,
@ -1054,6 +1060,32 @@ impl<F: Field> ConstraintSystem<F> {
self.permutation.add_column(column);
}
/// Add a multiset equality argument for some unpermuted expressions and
/// permuted expressions.
///
/// `multiset_map` returns a map between unpermuted expressions and the
/// permuted expfressions they need to match.
pub fn multiset_equality(
&mut self,
multiset_map: impl FnOnce(&mut VirtualCells<'_, F>) -> Vec<(Expression<F>, Expression<F>)>,
) -> usize {
let mut cells = VirtualCells::new(self);
let multiset_map = multiset_map(&mut cells);
for (original, permuted) in multiset_map.iter() {
if original.contains_simple_selector() || permuted.contains_simple_selector() {
panic!(
"expression containing simple selector supplied to multiset equality argument"
);
}
}
let index = self.multisets.len();
self.multisets
.push(multiset_equality::Argument::new(multiset_map));
index
}
/// Add a lookup argument for some input expressions and table columns.
///
/// `table_map` returns a map between input expressions and the table columns
@ -1416,6 +1448,16 @@ impl<F: Field> ConstraintSystem<F> {
.unwrap_or(1),
);
// Account for the multiset equality argument.
degree = std::cmp::max(
degree,
self.multisets
.iter()
.map(|l| l.required_degree())
.max()
.unwrap_or(1),
);
// Account for each gate to ensure our quotient polynomial is the
// correct degree and that our extended domain is the right size.
degree = std::cmp::max(

69
halo2_proofs/src/plonk/multiset_equality.rs Normal file
View File

@ -0,0 +1,69 @@
use ff::Field;
use super::Expression;
pub(crate) mod prover;
pub(crate) mod verifier;
#[derive(Clone, Debug)]
pub(crate) struct Argument<F: Field> {
pub original_expressions: Vec<Expression<F>>,
pub permuted_expressions: Vec<Expression<F>>,
}
impl<F: Field> Argument<F> {
/// Constructs a new multiset equality argument.
///
/// `multiset_map` is a sequence of `(original, permuted)` tuples.
pub fn new(multiset_map: Vec<(Expression<F>, Expression<F>)>) -> Self {
let (original_expressions, permuted_expressions) = multiset_map.into_iter().unzip();
Argument {
original_expressions,
permuted_expressions,
}
}
pub(crate) fn required_degree(&self) -> usize {
assert_eq!(
self.original_expressions.len(),
self.permuted_expressions.len()
);
// The first value in the permutation poly should be one.
// degree 2:
// l_0(X) * (1 - z(X)) = 0
//
// The "last" value in the permutation poly should be a boolean, for
// completeness and soundness.
// degree 3:
// l_last(X) * (z(X)^2 - z(X)) = 0
//
// Enable the permutation argument for only the rows involved.
// degree (2 + original_degree) or (2 + permuted_degree) or 3,
// whichever is larger:
// (1 - (l_last(X) + l_blind(X))) * (
// z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
// ) = 0
//
let mut original_degree = 1;
for expr in self.original_expressions.iter() {
original_degree = std::cmp::max(original_degree, expr.degree());
}
let mut permuted_degree = 1;
for expr in self.permuted_expressions.iter() {
permuted_degree = std::cmp::max(permuted_degree, expr.degree());
}
// In practice because original_degree and permuted_degree are initialized to
// one, the latter half of this max() invocation is at least 3 always,
// rendering this call pointless except to be explicit in case we change
// the initialization of original_degree/permuted_degree in the future.
std::cmp::max(
// (1 - (l_last + l_blind)) z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
2 + original_degree,
// (1 - (l_last + l_blind)) z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
2 + original_degree,
)
}
}

393
halo2_proofs/src/plonk/multiset_equality/prover.rs Normal file
View File

@ -0,0 +1,393 @@
use std::ops::{Mul, MulAssign};
use ff::{BatchInvert, Field};
use group::Curve;
use pasta_curves::arithmetic::{CurveAffine, FieldExt};
use rand_core::RngCore;
use super::Argument;
use crate::{
arithmetic::{eval_polynomial, parallelize},
plonk::{ChallengeBeta, ChallengeTheta, ChallengeX, Error, Expression, ProvingKey},
poly::{
self,
commitment::{Blind, Params},
multiopen::ProverQuery,
Coeff, EvaluationDomain, ExtendedLagrangeCoeff, LagrangeCoeff, Polynomial, Rotation,
},
transcript::{EncodedChallenge, TranscriptWrite},
};
#[derive(Debug)]
pub(in crate::plonk) struct Compressed<C: CurveAffine, Ev> {
original_cosets_compressed: poly::Ast<Ev, C::Scalar, ExtendedLagrangeCoeff>,
original_compressed: Polynomial<C::Scalar, LagrangeCoeff>,
permuted_cosets_compressed: poly::Ast<Ev, C::Scalar, ExtendedLagrangeCoeff>,
permuted_compressed: Polynomial<C::Scalar, LagrangeCoeff>,
}
#[derive(Debug)]
pub(in crate::plonk) struct Committed<C: CurveAffine, Ev> {
compressed: Compressed<C, Ev>,
product_poly: Polynomial<C::Scalar, Coeff>,
product_coset: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
product_blind: Blind<C::Scalar>,
}
#[derive(Debug)]
pub(in crate::plonk) struct Constructed<C: CurveAffine> {
product_poly: Polynomial<C::Scalar, Coeff>,
product_blind: Blind<C::Scalar>,
}
pub(in crate::plonk) struct Evaluated<C: CurveAffine> {
constructed: Constructed<C>,
}
impl<F: FieldExt> Argument<F> {
#[allow(clippy::too_many_arguments)]
pub(in crate::plonk) fn compress_expressions<
'a,
C,
Ev: Copy + Send + Sync,
Ec: Copy + Send + Sync,
>(
&self,
domain: &EvaluationDomain<C::Scalar>,
value_evaluator: &poly::Evaluator<Ev, C::Scalar, LagrangeCoeff>,
theta: ChallengeTheta<C>,
advice_values: &'a [poly::AstLeaf<Ev, LagrangeCoeff>],
fixed_values: &'a [poly::AstLeaf<Ev, LagrangeCoeff>],
instance_values: &'a [poly::AstLeaf<Ev, LagrangeCoeff>],
advice_cosets: &'a [poly::AstLeaf<Ec, ExtendedLagrangeCoeff>],
fixed_cosets: &'a [poly::AstLeaf<Ec, ExtendedLagrangeCoeff>],
instance_cosets: &'a [poly::AstLeaf<Ec, ExtendedLagrangeCoeff>],
) -> Compressed<C, Ec>
where
C: CurveAffine<ScalarExt = F>,
C::Curve: Mul<F, Output = C::Curve> + MulAssign<F>,
{
// Closure to get values of expressions and compress them
let compress_expressions = |expressions: &[Expression<C::Scalar>]| {
// Values of expressions
let expression_values: Vec<_> = expressions
.iter()
.map(|expression| {
expression.evaluate(
&|scalar| poly::Ast::ConstantTerm(scalar),
&|_| panic!("virtual selectors are removed during optimization"),
&|query| {
fixed_values[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|query| {
advice_values[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|query| {
instance_values[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|a| -a,
&|a, b| a + b,
&|a, b| a * b,
&|a, scalar| a * scalar,
)
})
.collect();
let cosets: Vec<_> = expressions
.iter()
.map(|expression| {
expression.evaluate(
&|scalar| poly::Ast::ConstantTerm(scalar),
&|_| panic!("virtual selectors are removed during optimization"),
&|query| {
fixed_cosets[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|query| {
advice_cosets[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|query| {
instance_cosets[query.column_index]
.with_rotation(query.rotation)
.into()
},
&|a| -a,
&|a, b| a + b,
&|a, b| a * b,
&|a, scalar| a * scalar,
)
})
.collect();
// Compressed version of expressions
let compressed_expressions = expression_values.iter().fold(
poly::Ast::ConstantTerm(C::Scalar::zero()),
|acc, expression| &(acc * *theta) + expression,
);
// Compressed version of cosets
let compressed_cosets = cosets.iter().fold(
poly::Ast::<_, _, ExtendedLagrangeCoeff>::ConstantTerm(C::Scalar::zero()),
|acc, eval| acc * poly::Ast::ConstantTerm(*theta) + eval.clone(),
);
(
compressed_cosets,
value_evaluator.evaluate(&compressed_expressions, domain),
)
};
let (original_cosets_compressed, original_compressed) =
compress_expressions(&self.original_expressions);
let (permuted_cosets_compressed, permuted_compressed) =
compress_expressions(&self.permuted_expressions);
Compressed {
original_cosets_compressed,
original_compressed,
permuted_cosets_compressed,
permuted_compressed,
}
}
}
impl<C: CurveAffine, Ev> Compressed<C, Ev> {
pub(in crate::plonk) fn commit_product<
E: EncodedChallenge<C>,
R: RngCore,
T: TranscriptWrite<C, E>,
>(
self,
pk: &ProvingKey<C>,
params: &Params<C>,
beta: ChallengeBeta<C>,
evaluator: &mut poly::Evaluator<Ev, C::Scalar, ExtendedLagrangeCoeff>,
mut rng: R,
transcript: &mut T,
) -> Result<Committed<C, Ev>, Error> {
let blinding_factors = pk.vk.cs.blinding_factors();
// Goal is to compute the products of fractions
//
// Numerator: (\theta^{m-1} a_0(\omega^i) + \theta^{m-2} a_1(\omega^i) + ... + \theta a_{m-2}(\omega^i) + a_{m-1}(\omega^i) + \beta)
// Denominator: (\theta^{m-1} a'_0(\omega^i) + \theta^{m-2} a'_1(\omega^i) + ... + \theta a'_{m-2}(\omega^i) + a'_{m-1}(\omega^i) + \beta)
//
// where a(X) is the compression of the original expressions in this multiset equality check,
// a'(X) is the compression of the permuted expressions,
// and i is the ith row of the expression.
let mut product = vec![C::Scalar::zero(); params.n as usize];
// Denominator uses the permuted expression
parallelize(&mut product, |product, start| {
for (product, permuted_value) in product
.iter_mut()
.zip(self.permuted_compressed[start..].iter())
{
*product = *beta + permuted_value;
}
});
// Batch invert to obtain the denominators for the product
// polynomials
product.iter_mut().batch_invert();
// Finish the computation of the entire fraction by computing the numerators
// (\theta^{m-1} a_0(\omega^i) + \theta^{m-2} a_1(\omega^i) + ... + \theta a_{m-2}(\omega^i) + a_{m-1}(\omega^i) + \beta)
parallelize(&mut product, |product, start| {
for (product, original_value) in product
.iter_mut()
.zip(self.original_compressed[start..].iter())
{
*product *= &(*beta + original_value);
}
});
// The product vector is a vector of products of fractions of the form
//
// Numerator: (\theta^{m-1} a_0(\omega^i) + \theta^{m-2} a_1(\omega^i) + ... + \theta a_{m-2}(\omega^i) + a_{m-1}(\omega^i) + \beta)
// Denominator: (\theta^{m-1} a'_0(\omega^i) + \theta^{m-2} a'_1(\omega^i) + ... + \theta a'_{m-2}(\omega^i) + a'_{m-1}(\omega^i) + \beta)
//
// where there are m original expressions and m permuted expressions,
// a_j(\omega^i)'s are the original expressions,
// a'_j(\omega^i)'s are the original expressions,
// and i is the ith row of the expression.
// Compute the evaluations of the lookup product polynomial
// over our domain, starting with z[0] = 1
let z = std::iter::once(C::Scalar::one())
.chain(product)
.scan(C::Scalar::one(), |state, cur| {
*state *= &cur;
Some(*state)
})
// Take all rows including the "last" row which should
// be a boolean (and ideally 1, else soundness is broken)
.take(params.n as usize - blinding_factors)
// Chain random blinding factors.
.chain((0..blinding_factors).map(|_| C::Scalar::random(&mut rng)))
.collect::<Vec<_>>();
assert_eq!(z.len(), params.n as usize);
let z = pk.vk.domain.lagrange_from_vec(z);
#[cfg(feature = "sanity-checks")]
// This test works only with intermediate representations in this method.
// It can be used for debugging purposes.
{
// While in Lagrange basis, check that product is correctly constructed
let u = (params.n as usize) - (blinding_factors + 1);
// l_0(X) * (1 - z(X)) = 0
assert_eq!(z[0], C::Scalar::one());
// z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
for i in 0..u {
let mut left = z[i + 1];
let permuted_value = &self.permuted_compressed[i];
left *= &(*beta + permuted_value);
let mut right = z[i];
let original_value = self.original_compressed[i];
right *= &(*beta + original_value);
assert_eq!(left, right);
}
// l_last(X) * (z(X)^2 - z(X)) = 0
// Assertion will fail only when soundness is broken, in which
// case this z[u] value will be zero. (bad!)
assert_eq!(z[u], C::Scalar::one());
}
let product_blind = Blind(C::Scalar::random(rng));
let product_commitment = params.commit_lagrange(&z, product_blind).to_affine();
let z = pk.vk.domain.lagrange_to_coeff(z);
let product_coset = evaluator.register_poly(pk.vk.domain.coeff_to_extended(z.clone()));
// Hash product commitment
transcript.write_point(product_commitment)?;
Ok(Committed::<C, _> {
compressed: self,
product_poly: z,
product_coset,
product_blind,
})
}
}
impl<'a, C: CurveAffine, Ev: Copy + Send + Sync + 'a> Committed<C, Ev> {
/// Given a Multiset equality argument with unpermuted expressions,
/// permuted expressions, and grand product polynomial, this method
/// constructs constraints that must hold between these values.
/// This method returns the constraints as a vector of ASTs for polynomials in
/// the extended evaluation domain.
pub(in crate::plonk) fn construct(
self,
beta: ChallengeBeta<C>,
l0: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
l_blind: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
l_last: poly::AstLeaf<Ev, ExtendedLagrangeCoeff>,
) -> (
Constructed<C>,
impl Iterator<Item = poly::Ast<Ev, C::Scalar, ExtendedLagrangeCoeff>> + 'a,
) {
let compressed = self.compressed;
let active_rows = poly::Ast::one() - (poly::Ast::from(l_last) + l_blind);
let beta = poly::Ast::ConstantTerm(*beta);
let expressions = std::iter::empty()
// l_0(X) * (1 - z(X)) = 0
.chain(Some((poly::Ast::one() - self.product_coset) * l0))
// l_last(X) * (z(X)^2 - z(X)) = 0
.chain(Some(
(poly::Ast::from(self.product_coset) * self.product_coset - self.product_coset)
* l_last,
))
// (1 - (l_last(X) + l_blind(X))) * (
// z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
// ) = 0
.chain({
// z(\omega X) (a'(X) + \beta)
let left: poly::Ast<_, _, _> = poly::Ast::<_, C::Scalar, _>::from(
self.product_coset.with_rotation(Rotation::next()),
) * (compressed.permuted_cosets_compressed
+ beta.clone());
// z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
let right: poly::Ast<_, _, _> = poly::Ast::from(self.product_coset)
* (&compressed.original_cosets_compressed + &beta);
Some((left - right) * active_rows)
});
(
Constructed {
product_poly: self.product_poly,
product_blind: self.product_blind,
},
expressions,
)
}
}
impl<C: CurveAffine> Constructed<C> {
pub(in crate::plonk) fn evaluate<E: EncodedChallenge<C>, T: TranscriptWrite<C, E>>(
self,
pk: &ProvingKey<C>,
x: ChallengeX<C>,
transcript: &mut T,
) -> Result<Evaluated<C>, Error> {
let domain = &pk.vk.domain;
let x_next = domain.rotate_omega(*x, Rotation::next());
let product_eval = eval_polynomial(&self.product_poly, *x);
let product_next_eval = eval_polynomial(&self.product_poly, x_next);
// Hash each advice evaluation
for eval in std::iter::empty()
.chain(Some(product_eval))
.chain(Some(product_next_eval))
{
transcript.write_scalar(eval)?;
}
Ok(Evaluated { constructed: self })
}
}
impl<C: CurveAffine> Evaluated<C> {
pub(in crate::plonk) fn open<'a>(
&'a self,
pk: &'a ProvingKey<C>,
x: ChallengeX<C>,
) -> impl Iterator<Item = ProverQuery<'a, C>> + Clone {
let x_next = pk.vk.domain.rotate_omega(*x, Rotation::next());
std::iter::empty()
// Open multiset argument product commitments at x
.chain(Some(ProverQuery {
point: *x,
poly: &self.constructed.product_poly,
blind: self.constructed.product_blind,
}))
// Open multiset argument product commitments at x_next
.chain(Some(ProverQuery {
point: x_next,
poly: &self.constructed.product_poly,
blind: self.constructed.product_blind,
}))
}
}

139
halo2_proofs/src/plonk/multiset_equality/verifier.rs Normal file
View File

@ -0,0 +1,139 @@
use std::iter;
use super::super::{circuit::Expression, ChallengeBeta, ChallengeTheta, ChallengeX};
use super::Argument;
use crate::{
arithmetic::{CurveAffine, FieldExt},
plonk::{Error, VerifyingKey},
poly::{multiopen::VerifierQuery, Rotation},
transcript::{EncodedChallenge, TranscriptRead},
};
use ff::Field;
pub struct Committed<C: CurveAffine> {
product_commitment: C,
}
pub struct Evaluated<C: CurveAffine> {
committed: Committed<C>,
product_eval: C::Scalar,
product_next_eval: C::Scalar,
}
impl<F: FieldExt> Argument<F> {
pub(in crate::plonk) fn read_product_commitment<
C: CurveAffine,
E: EncodedChallenge<C>,
T: TranscriptRead<C, E>,
>(
self,
transcript: &mut T,
) -> Result<Committed<C>, Error> {
let product_commitment = transcript.read_point()?;
Ok(Committed { product_commitment })
}
}
impl<C: CurveAffine> Committed<C> {
pub(crate) fn evaluate<E: EncodedChallenge<C>, T: TranscriptRead<C, E>>(
self,
transcript: &mut T,
) -> Result<Evaluated<C>, Error> {
let product_eval = transcript.read_scalar()?;
let product_next_eval = transcript.read_scalar()?;
Ok(Evaluated {
committed: self,
product_eval,
product_next_eval,
})
}
}
impl<C: CurveAffine> Evaluated<C> {
#[allow(clippy::too_many_arguments)]
pub(in crate::plonk) fn expressions<'a>(
&'a self,
l_0: C::Scalar,
l_last: C::Scalar,
l_blind: C::Scalar,
argument: &'a Argument<C::Scalar>,
theta: ChallengeTheta<C>,
beta: ChallengeBeta<C>,
advice_evals: &[C::Scalar],
fixed_evals: &[C::Scalar],
instance_evals: &[C::Scalar],
) -> impl Iterator<Item = C::Scalar> + 'a {
let active_rows = C::Scalar::one() - (l_last + l_blind);
let product_expression = || {
let compress_expressions = |expressions: &[Expression<C::Scalar>]| {
expressions
.iter()
.map(|expression| {
expression.evaluate(
&|scalar| scalar,
&|_| panic!("virtual selectors are removed during optimization"),
&|query| fixed_evals[query.index],
&|query| advice_evals[query.index],
&|query| instance_evals[query.index],
&|a| -a,
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * &scalar,
)
})
.fold(C::Scalar::zero(), |acc, eval| acc * &*theta + &eval)
};
// z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
let left = self.product_next_eval
* &(compress_expressions(&argument.permuted_expressions) + &*beta);
let right = self.product_eval
* &(compress_expressions(&argument.original_expressions) + &*beta);
(left - &right) * &active_rows
};
std::iter::empty()
.chain(
// l_0(X) * (1 - z(X)) = 0
Some(l_0 * &(C::Scalar::one() - &self.product_eval)),
)
.chain(
// l_last(X) * (z(X)^2 - z(X)) = 0
Some(l_last * &(self.product_eval.square() - &self.product_eval)),
)
.chain(
// (1 - (l_last(X) + l_blind(X))) * (
// z(\omega X) (\theta^{m-1} a'_0(X) + ... + a'_{m-1}(X) + \beta)
// - z(X) (\theta^{m-1} a_0(X) + ... + a_{m-1}(X) + \beta)
// ) = 0
Some(product_expression()),
)
}
pub(in crate::plonk) fn queries<'r, 'params: 'r>(
&'r self,
vk: &'r VerifyingKey<C>,
x: ChallengeX<C>,
) -> impl Iterator<Item = VerifierQuery<'r, 'params, C>> + Clone {
let x_next = vk.domain.rotate_omega(*x, Rotation::next());
iter::empty()
// Open multiset product commitment at x
.chain(Some(VerifierQuery::new_commitment(
&self.committed.product_commitment,
*x,
self.product_eval,
)))
// Open multiset product commitment at \omega x
.chain(Some(VerifierQuery::new_commitment(
&self.committed.product_commitment,
x_next,
self.product_next_eval,
)))
}
}

175
halo2_proofs/src/plonk/prover.rs
View File

@ -15,7 +15,7 @@ use super::{
use crate::{
arithmetic::{eval_polynomial, CurveAffine},
circuit::Value,
plonk::Assigned,
plonk::{multiset_equality, Assigned},
poly::{
self,
commitment::{Blind, Params},
@ -420,6 +420,34 @@ pub fn create_proof<
// Sample theta challenge for keeping lookup columns linearly independent
let theta: ChallengeTheta<_> = transcript.squeeze_challenge_scalar();
let multisets = instance_values
.iter()
.zip(instance_cosets.iter())
.zip(advice_values.iter())
.zip(advice_cosets.iter())
.map(
|(((instance_values, instance_cosets), advice_values), advice_cosets)| -> Vec<_> {
pk.vk
.cs
.multisets
.iter()
.map(|multiset| {
multiset.compress_expressions(
domain,
&value_evaluator,
theta,
advice_values,
&fixed_values,
instance_values,
advice_cosets,
&fixed_cosets,
instance_cosets,
)
})
.collect::<Vec<_>>()
},
);
let lookups: Vec<Vec<lookup::prover::Permuted<C, _>>> = instance_values
.iter()
.zip(instance_cosets.iter())
@ -480,6 +508,27 @@ pub fn create_proof<
})
.collect::<Result<Vec<_>, _>>()?;
// Commit to multiset equality arguments.
let multisets: Vec<Vec<multiset_equality::prover::Committed<C, _>>> = multisets
.map(|multisets| -> Result<Vec<_>, _> {
// Construct and commit to products for each multiset
multisets
.into_iter()
.map(|multiset| {
multiset.commit_product(
pk,
params,
beta,
&mut coset_evaluator,
&mut rng,
transcript,
)
})
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;
// Commit to lookups.
let lookups: Vec<Vec<lookup::prover::Committed<C, _>>> = lookups
.into_iter()
.map(|lookups| -> Result<Vec<_>, _> {
@ -529,6 +578,17 @@ pub fn create_proof<
})
.unzip();
let (multisets, multiset_expressions): (Vec<Vec<_>>, Vec<Vec<_>>) = multisets
.into_iter()
.map(|multisets| {
// Evaluate the h(X) polynomial's constraint system expressions for the multiset argument constraints, if any.
multisets
.into_iter()
.map(|p| p.construct(beta, l0, l_blind, l_last))
.unzip()
})
.unzip();
let (lookups, lookup_expressions): (Vec<Vec<_>>, Vec<Vec<_>>) = lookups
.into_iter()
.map(|lookups| {
@ -544,9 +604,13 @@ pub fn create_proof<
.iter()
.zip(instance_cosets.iter())
.zip(permutation_expressions.into_iter())
.zip(multiset_expressions)
.zip(lookup_expressions.into_iter())
.flat_map(
|(((advice_cosets, instance_cosets), permutation_expressions), lookup_expressions)| {
|(
(((advice_cosets, instance_cosets), permutation_expressions), multiset_expressions),
lookup_expressions,
)| {
let fixed_cosets = &fixed_cosets;
iter::empty()
// Custom constraints
@ -579,6 +643,8 @@ pub fn create_proof<
}))
// Permutation constraints, if any.
.chain(permutation_expressions.into_iter())
// Multiset constraints, if any.
.chain(multiset_expressions.into_iter().flatten())
// Lookup constraints, if any.
.chain(lookup_expressions.into_iter().flatten())
},
@ -663,6 +729,17 @@ pub fn create_proof<
.map(|permutation| -> Result<_, _> { permutation.evaluate(pk, x, transcript) })
.collect::<Result<Vec<_>, _>>()?;
// Evaluate the multisets, if any, at omega^i x.
let multisets: Vec<Vec<multiset_equality::prover::Evaluated<C>>> = multisets
.into_iter()
.map(|multisets| -> Result<Vec<_>, _> {
multisets
.into_iter()
.map(|p| p.evaluate(pk, x, transcript))
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;
// Evaluate the lookups, if any, at omega^i x.
let lookups: Vec<Vec<lookup::prover::Evaluated<C>>> = lookups
.into_iter()
@ -674,52 +751,54 @@ pub fn create_proof<
})
.collect::<Result<Vec<_>, _>>()?;
let instances = instance
.iter()
.zip(advice.iter())
.zip(permutations.iter())
.zip(lookups.iter())
.flat_map(|(((instance, advice), permutation), lookups)| {
iter::empty()
.chain(
pk.vk
.cs
.instance_queries
.iter()
.map(move |&(column, at)| ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &instance.instance_polys[column.index()],
blind: Blind::default(),
}),
)
.chain(
pk.vk
.cs
.advice_queries
.iter()
.map(move |&(column, at)| ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &advice.advice_polys[column.index()],
blind: advice.advice_blinds[column.index()],
}),
)
.chain(permutation.open(pk, x))
.chain(lookups.iter().flat_map(move |p| p.open(pk, x)).into_iter())
})
.chain(
pk.vk
.cs
.fixed_queries
.iter()
.map(|&(column, at)| ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &pk.fixed_polys[column.index()],
blind: Blind::default(),
}),
)
.chain(pk.permutation.open(x))
// We query the h(X) polynomial at x
.chain(vanishing.open(x));
let instances =
instance
.iter()
.zip(advice.iter())
.zip(permutations.iter())
.zip(multisets.iter())
.zip(lookups.iter())
.flat_map(
|((((instance, advice), permutation), multisets), lookups)| {
iter::empty()
.chain(pk.vk.cs.instance_queries.iter().map(move |&(column, at)| {
ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &instance.instance_polys[column.index()],
blind: Blind::default(),
}
}))
.chain(pk.vk.cs.advice_queries.iter().map(move |&(column, at)| {
ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &advice.advice_polys[column.index()],
blind: advice.advice_blinds[column.index()],
}
}))
.chain(permutation.open(pk, x))
.chain(
multisets
.iter()
.flat_map(move |p| p.open(pk, x))
.into_iter(),
)
.chain(lookups.iter().flat_map(move |p| p.open(pk, x)).into_iter())
},
)
.chain(
pk.vk
.cs
.fixed_queries
.iter()
.map(|&(column, at)| ProverQuery {
point: domain.rotate_omega(*x, at),
poly: &pk.fixed_polys[column.index()],
blind: Blind::default(),
}),
)
.chain(pk.permutation.open(x))
// We query the h(X) polynomial at x
.chain(vanishing.open(x));
multiopen::create_proof(params, rng, transcript, instances).map_err(|_| Error::Opening)
}

166
halo2_proofs/src/plonk/verifier.rs
View File

@ -149,6 +149,17 @@ pub fn verify_proof<
})
.collect::<Result<Vec<_>, _>>()?;
let multisets_committed = (0..num_proofs)
.map(|_| -> Result<Vec<_>, _> {
// Hash each multiset product commitment
vk.cs
.multisets
.iter()
.map(|argument| argument.clone().read_product_commitment(transcript))
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;
let lookups_committed = lookups_permuted
.into_iter()
.map(|lookups| {
@ -189,6 +200,16 @@ pub fn verify_proof<
.map(|permutation| permutation.evaluate(transcript))
.collect::<Result<Vec<_>, _>>()?;
let multisets_evaluated = multisets_committed
.into_iter()
.map(|multisets| -> Result<Vec<_>, _> {
multisets
.into_iter()
.map(|multiset| multiset.evaluate(transcript))
.collect::<Result<Vec<_>, _>>()
})
.collect::<Result<Vec<_>, _>>()?;
let lookups_evaluated = lookups_committed
.into_iter()
.map(|lookups| -> Result<Vec<_>, _> {
@ -221,61 +242,85 @@ pub fn verify_proof<
.iter()
.zip(instance_evals.iter())
.zip(permutations_evaluated.iter())
.zip(multisets_evaluated.iter())
.zip(lookups_evaluated.iter())
.flat_map(|(((advice_evals, instance_evals), permutation), lookups)| {
let fixed_evals = &fixed_evals;
std::iter::empty()
// Evaluate the circuit using the custom gates provided
.chain(vk.cs.gates.iter().flat_map(move |gate| {
gate.polynomials().iter().map(move |poly| {
poly.evaluate(
&|scalar| scalar,
&|_| panic!("virtual selectors are removed during optimization"),
&|query| fixed_evals[query.index],
&|query| advice_evals[query.index],
&|query| instance_evals[query.index],
&|a| -a,
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * &scalar,
)
})
}))
.chain(permutation.expressions(
vk,
&vk.cs.permutation,
&permutations_common,
advice_evals,
fixed_evals,
instance_evals,
l_0,
l_last,
l_blind,
beta,
gamma,
x,
))
.chain(
lookups
.iter()
.zip(vk.cs.lookups.iter())
.flat_map(move |(p, argument)| {
p.expressions(
l_0,
l_last,
l_blind,
argument,
theta,
beta,
gamma,
advice_evals,
fixed_evals,
instance_evals,
.flat_map(
|((((advice_evals, instance_evals), permutation), multisets), lookups)| {
let fixed_evals = &fixed_evals;
std::iter::empty()
// Evaluate the circuit using the custom gates provided
.chain(vk.cs.gates.iter().flat_map(move |gate| {
gate.polynomials().iter().map(move |poly| {
poly.evaluate(
&|scalar| scalar,
&|_| {
panic!("virtual selectors are removed during optimization")
},
&|query| fixed_evals[query.index],
&|query| advice_evals[query.index],
&|query| instance_evals[query.index],
&|a| -a,
&|a, b| a + &b,
&|a, b| a * &b,
&|a, scalar| a * &scalar,
)
})
.into_iter(),
)
});
}))
.chain(permutation.expressions(
vk,
&vk.cs.permutation,
&permutations_common,
advice_evals,
fixed_evals,
instance_evals,
l_0,
l_last,
l_blind,
beta,
gamma,
x,
))
.chain(
multisets
.iter()
.zip(vk.cs.multisets.iter())
.flat_map(move |(p, argument)| {
p.expressions(
l_0,
l_last,
l_blind,
argument,
theta,
beta,
advice_evals,
fixed_evals,
instance_evals,
)
})
.into_iter(),
)
.chain(
lookups
.iter()
.zip(vk.cs.lookups.iter())
.flat_map(move |(p, argument)| {
p.expressions(
l_0,
l_last,
l_blind,
argument,
theta,
beta,
gamma,
advice_evals,
fixed_evals,
instance_evals,
)
})
.into_iter(),
)
},
);
vanishing.verify(params, expressions, y, xn)
};
@ -286,12 +331,19 @@ pub fn verify_proof<
.zip(advice_commitments.iter())
.zip(advice_evals.iter())
.zip(permutations_evaluated.iter())
.zip(multisets_evaluated.iter())
.zip(lookups_evaluated.iter())
.flat_map(
|(
(
(((instance_commitments, instance_evals), advice_commitments), advice_evals),
permutation,
(
(
((instance_commitments, instance_evals), advice_commitments),
advice_evals,
),
permutation,
),
multisets,
),
lookups,
)| {
@ -315,6 +367,12 @@ pub fn verify_proof<
},
))
.chain(permutation.queries(vk, x))
.chain(
multisets
.iter()
.flat_map(move |p| p.queries(vk, x))
.into_iter(),
)
.chain(
lookups
.iter()