From a845b81f10c21ffa19d8c5d7fdbfe2d3572555f3 Mon Sep 17 00:00:00 2001 From: therealyingtong Date: Mon, 26 Sep 2022 20:06:37 +0800 Subject: [PATCH] Introduce multiset equality argument --- halo2_proofs/src/plonk.rs | 1 + halo2_proofs/src/plonk/circuit.rs | 44 +- halo2_proofs/src/plonk/multiset_equality.rs | 69 +++ .../src/plonk/multiset_equality/prover.rs | 393 ++++++++++++++++++ .../src/plonk/multiset_equality/verifier.rs | 139 +++++++ halo2_proofs/src/plonk/prover.rs | 175 +++++--- halo2_proofs/src/plonk/verifier.rs | 166 +++++--- 7 files changed, 884 insertions(+), 103 deletions(-) create mode 100644 halo2_proofs/src/plonk/multiset_equality.rs create mode 100644 halo2_proofs/src/plonk/multiset_equality/prover.rs create mode 100644 halo2_proofs/src/plonk/multiset_equality/verifier.rs diff --git a/halo2_proofs/src/plonk.rs b/halo2_proofs/src/plonk.rs index e96cf3fe..f85cdba6 100644 --- a/halo2_proofs/src/plonk.rs +++ b/halo2_proofs/src/plonk.rs @@ -20,6 +20,7 @@ mod circuit; mod error; mod keygen; mod lookup; +mod multiset_equality; pub(crate) mod permutation; mod vanishing; diff --git a/halo2_proofs/src/plonk/circuit.rs b/halo2_proofs/src/plonk/circuit.rs index 334755dd..fc4af3da 100644 --- a/halo2_proofs/src/plonk/circuit.rs +++ b/halo2_proofs/src/plonk/circuit.rs @@ -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 { // 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>, + // 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>, @@ -1007,6 +1012,7 @@ impl Default for ConstraintSystem { 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 ConstraintSystem { 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, Expression)>, + ) -> 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 ConstraintSystem { .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( diff --git a/halo2_proofs/src/plonk/multiset_equality.rs b/halo2_proofs/src/plonk/multiset_equality.rs new file mode 100644 index 00000000..405cd4c6 --- /dev/null +++ b/halo2_proofs/src/plonk/multiset_equality.rs @@ -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 { + pub original_expressions: Vec>, + pub permuted_expressions: Vec>, +} + +impl Argument { + /// Constructs a new multiset equality argument. + /// + /// `multiset_map` is a sequence of `(original, permuted)` tuples. + pub fn new(multiset_map: Vec<(Expression, Expression)>) -> 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, + ) + } +} diff --git a/halo2_proofs/src/plonk/multiset_equality/prover.rs b/halo2_proofs/src/plonk/multiset_equality/prover.rs new file mode 100644 index 00000000..ba07a42d --- /dev/null +++ b/halo2_proofs/src/plonk/multiset_equality/prover.rs @@ -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 { + original_cosets_compressed: poly::Ast, + original_compressed: Polynomial, + permuted_cosets_compressed: poly::Ast, + permuted_compressed: Polynomial, +} + +#[derive(Debug)] +pub(in crate::plonk) struct Committed { + compressed: Compressed, + product_poly: Polynomial, + product_coset: poly::AstLeaf, + product_blind: Blind, +} + +#[derive(Debug)] +pub(in crate::plonk) struct Constructed { + product_poly: Polynomial, + product_blind: Blind, +} + +pub(in crate::plonk) struct Evaluated { + constructed: Constructed, +} + +impl Argument { + #[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, + value_evaluator: &poly::Evaluator, + theta: ChallengeTheta, + advice_values: &'a [poly::AstLeaf], + fixed_values: &'a [poly::AstLeaf], + instance_values: &'a [poly::AstLeaf], + advice_cosets: &'a [poly::AstLeaf], + fixed_cosets: &'a [poly::AstLeaf], + instance_cosets: &'a [poly::AstLeaf], + ) -> Compressed + where + C: CurveAffine, + C::Curve: Mul + MulAssign, + { + // Closure to get values of expressions and compress them + let compress_expressions = |expressions: &[Expression]| { + // 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 Compressed { + pub(in crate::plonk) fn commit_product< + E: EncodedChallenge, + R: RngCore, + T: TranscriptWrite, + >( + self, + pk: &ProvingKey, + params: &Params, + beta: ChallengeBeta, + evaluator: &mut poly::Evaluator, + mut rng: R, + transcript: &mut T, + ) -> Result, 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::>(); + 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:: { + compressed: self, + product_poly: z, + product_coset, + product_blind, + }) + } +} + +impl<'a, C: CurveAffine, Ev: Copy + Send + Sync + 'a> Committed { + /// 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, + l0: poly::AstLeaf, + l_blind: poly::AstLeaf, + l_last: poly::AstLeaf, + ) -> ( + Constructed, + impl Iterator> + '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 Constructed { + pub(in crate::plonk) fn evaluate, T: TranscriptWrite>( + self, + pk: &ProvingKey, + x: ChallengeX, + transcript: &mut T, + ) -> Result, 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 Evaluated { + pub(in crate::plonk) fn open<'a>( + &'a self, + pk: &'a ProvingKey, + x: ChallengeX, + ) -> impl Iterator> + 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, + })) + } +} diff --git a/halo2_proofs/src/plonk/multiset_equality/verifier.rs b/halo2_proofs/src/plonk/multiset_equality/verifier.rs new file mode 100644 index 00000000..01bfd962 --- /dev/null +++ b/halo2_proofs/src/plonk/multiset_equality/verifier.rs @@ -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 { + product_commitment: C, +} + +pub struct Evaluated { + committed: Committed, + product_eval: C::Scalar, + product_next_eval: C::Scalar, +} + +impl Argument { + pub(in crate::plonk) fn read_product_commitment< + C: CurveAffine, + E: EncodedChallenge, + T: TranscriptRead, + >( + self, + transcript: &mut T, + ) -> Result, Error> { + let product_commitment = transcript.read_point()?; + + Ok(Committed { product_commitment }) + } +} + +impl Committed { + pub(crate) fn evaluate, T: TranscriptRead>( + self, + transcript: &mut T, + ) -> Result, Error> { + let product_eval = transcript.read_scalar()?; + let product_next_eval = transcript.read_scalar()?; + + Ok(Evaluated { + committed: self, + product_eval, + product_next_eval, + }) + } +} + +impl Evaluated { + #[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, + theta: ChallengeTheta, + beta: ChallengeBeta, + advice_evals: &[C::Scalar], + fixed_evals: &[C::Scalar], + instance_evals: &[C::Scalar], + ) -> impl Iterator + 'a { + let active_rows = C::Scalar::one() - (l_last + l_blind); + + let product_expression = || { + let compress_expressions = |expressions: &[Expression]| { + 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, + x: ChallengeX, + ) -> impl Iterator> + 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, + ))) + } +} diff --git a/halo2_proofs/src/plonk/prover.rs b/halo2_proofs/src/plonk/prover.rs index e54f2129..0e5b4b37 100644 --- a/halo2_proofs/src/plonk/prover.rs +++ b/halo2_proofs/src/plonk/prover.rs @@ -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::>() + }, + ); + let lookups: Vec>> = instance_values .iter() .zip(instance_cosets.iter()) @@ -480,6 +508,27 @@ pub fn create_proof< }) .collect::, _>>()?; + // Commit to multiset equality arguments. + let multisets: Vec>> = multisets + .map(|multisets| -> Result, _> { + // 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::, _>>() + }) + .collect::, _>>()?; + + // Commit to lookups. let lookups: Vec>> = lookups .into_iter() .map(|lookups| -> Result, _> { @@ -529,6 +578,17 @@ pub fn create_proof< }) .unzip(); + let (multisets, multiset_expressions): (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>) = 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::, _>>()?; + // Evaluate the multisets, if any, at omega^i x. + let multisets: Vec>> = multisets + .into_iter() + .map(|multisets| -> Result, _> { + multisets + .into_iter() + .map(|p| p.evaluate(pk, x, transcript)) + .collect::, _>>() + }) + .collect::, _>>()?; + // Evaluate the lookups, if any, at omega^i x. let lookups: Vec>> = lookups .into_iter() @@ -674,52 +751,54 @@ pub fn create_proof< }) .collect::, _>>()?; - 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) } diff --git a/halo2_proofs/src/plonk/verifier.rs b/halo2_proofs/src/plonk/verifier.rs index f141ebaf..3bc11a2f 100644 --- a/halo2_proofs/src/plonk/verifier.rs +++ b/halo2_proofs/src/plonk/verifier.rs @@ -149,6 +149,17 @@ pub fn verify_proof< }) .collect::, _>>()?; + let multisets_committed = (0..num_proofs) + .map(|_| -> Result, _> { + // Hash each multiset product commitment + vk.cs + .multisets + .iter() + .map(|argument| argument.clone().read_product_commitment(transcript)) + .collect::, _>>() + }) + .collect::, _>>()?; + let lookups_committed = lookups_permuted .into_iter() .map(|lookups| { @@ -189,6 +200,16 @@ pub fn verify_proof< .map(|permutation| permutation.evaluate(transcript)) .collect::, _>>()?; + let multisets_evaluated = multisets_committed + .into_iter() + .map(|multisets| -> Result, _> { + multisets + .into_iter() + .map(|multiset| multiset.evaluate(transcript)) + .collect::, _>>() + }) + .collect::, _>>()?; + let lookups_evaluated = lookups_committed .into_iter() .map(|lookups| -> Result, _> { @@ -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()