Use lookup mod in plonk::prover and plonk::verifier

This commit is contained in:
therealyingtong 2020-12-02 03:00:59 +08:00
parent 19c1b20063
commit 0c81e9adab
7 changed files with 181 additions and 46 deletions

View file

@ -53,6 +53,7 @@ pub struct Proof<C: CurveAffine> {
advice_commitments: Vec<C>,
h_commitments: Vec<C>,
permutations: Option<permutation::Proof<C>>,
lookups: Vec<lookup::Proof<C>>,
advice_evals: Vec<C::Scalar>,
aux_evals: Vec<C::Scalar>,
fixed_evals: Vec<C::Scalar>,

View file

@ -4,7 +4,7 @@ use ff::Field;
use std::collections::BTreeMap;
use std::convert::TryFrom;
use super::{permutation, Error};
use super::{lookup, permutation, Error};
use crate::poly::Rotation;
/// A column type
@ -313,6 +313,10 @@ pub struct ConstraintSystem<F> {
// Vector of permutation arguments, where each corresponds to a sequence of columns
// that are involved in a permutation argument.
pub(crate) permutations: Vec<permutation::Argument>,
// Vector of lookup arguments, where each corresponds to a sequence of
// input columns and a sequence of table columns involved in the lookup.
pub(crate) lookups: Vec<lookup::Argument>,
}
impl<F: Field> Default for ConstraintSystem<F> {
@ -330,6 +334,7 @@ impl<F: Field> Default for ConstraintSystem<F> {
aux_queries: Vec::new(),
rotations,
permutations: Vec::new(),
lookups: Vec::new(),
}
}
}

View file

@ -1,7 +1,7 @@
use super::circuit::{Any, Column};
use crate::arithmetic::CurveAffine;
mod prover;
pub(crate) mod prover;
mod verifier;
#[derive(Clone, Debug)]

View file

@ -1,6 +1,6 @@
use super::super::{
circuit::{Advice, Any, Aux, Column, Fixed},
ChallengeX, Error, ProvingKey,
ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX, Error, ProvingKey,
};
use super::{Argument, Proof};
use crate::{
@ -41,8 +41,8 @@ pub(crate) struct Product<C: CurveAffine> {
#[derive(Clone, Debug)]
pub(crate) struct Committed<C: CurveAffine> {
permuted: Permuted<C>,
product: Product<C>,
pub permuted: Permuted<C>,
pub product: Product<C>,
}
pub(crate) struct Constructed<C: CurveAffine> {
@ -85,7 +85,7 @@ impl Argument {
pk: &ProvingKey<C>,
params: &Params<C>,
domain: &EvaluationDomain<C::Scalar>,
theta: C::Scalar,
theta: ChallengeTheta<C::Scalar>,
advice_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
fixed_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
aux_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
@ -105,7 +105,7 @@ impl Argument {
// Compressed version of input columns
let compressed_input_value = unpermuted_input_values
.iter()
.fold(domain.empty_lagrange(), |acc, input| acc * theta + input);
.fold(domain.empty_lagrange(), |acc, input| acc * *theta + input);
// Values of table columns involved in the lookup
let unpermuted_table_values: Vec<Polynomial<C::Scalar, LagrangeCoeff>> = self
@ -121,7 +121,7 @@ impl Argument {
// Compressed version of table columns
let compressed_table_value = unpermuted_table_values
.iter()
.fold(domain.empty_lagrange(), |acc, table| acc * theta + table);
.fold(domain.empty_lagrange(), |acc, table| acc * *theta + table);
// Permute compressed (InputColumn, TableColumn) pair
let (permuted_input_value, permuted_table_value) =
@ -192,9 +192,9 @@ impl Argument {
permuted: &Permuted<C>,
pk: &ProvingKey<C>,
params: &Params<C>,
theta: C::Scalar,
beta: C::Scalar,
gamma: C::Scalar,
theta: ChallengeTheta<C::Scalar>,
beta: ChallengeBeta<C::Scalar>,
gamma: ChallengeGamma<C::Scalar>,
advice_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
fixed_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
aux_values: &[Polynomial<C::Scalar, LagrangeCoeff>],
@ -240,8 +240,8 @@ impl Argument {
.zip(permuted.permuted_input_value[start..].iter())
.zip(permuted.permuted_table_value[start..].iter())
{
*lookup_product *= &(beta + permuted_input_value);
*lookup_product *= &(gamma + permuted_table_value);
*lookup_product *= &(*beta + permuted_input_value);
*lookup_product *= &(*gamma + permuted_table_value);
}
});
@ -382,10 +382,10 @@ impl<C: CurveAffine> Committed<C> {
pub(in crate::plonk) fn construct<'a>(
self,
pk: &'a ProvingKey<C>,
theta: C::Scalar,
beta: C::Scalar,
gamma: C::Scalar,
argument: Argument,
theta: ChallengeTheta<C::Scalar>,
beta: ChallengeBeta<C::Scalar>,
gamma: ChallengeGamma<C::Scalar>,
argument: &'a Argument,
advice_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
fixed_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
aux_cosets: &'a [Polynomial<C::Scalar, ExtendedLagrangeCoeff>],
@ -458,8 +458,8 @@ impl<C: CurveAffine> Committed<C> {
.zip(permuted.permuted_input_coset[start..].iter())
.zip(permuted.permuted_table_coset[start..].iter())
{
*left *= &(*permuted_input + &beta);
*left *= &(*permuted_table + &gamma);
*left *= &(*permuted_input + &(*beta));
*left *= &(*permuted_table + &(*gamma));
}
});
@ -473,7 +473,7 @@ impl<C: CurveAffine> Committed<C> {
parallelize(&mut input_terms, |input_term, start| {
for (input_term, input) in input_term.iter_mut().zip(input[start..].iter())
{
*input_term *= &theta;
*input_term *= &(*theta);
*input_term += input;
}
});
@ -486,7 +486,7 @@ impl<C: CurveAffine> Committed<C> {
parallelize(&mut table_terms, |table_term, start| {
for (table_term, table) in table_term.iter_mut().zip(table[start..].iter())
{
*table_term *= &theta;
*table_term *= &(*theta);
*table_term += table;
}
});
@ -499,8 +499,8 @@ impl<C: CurveAffine> Committed<C> {
.zip(input_terms[start..].iter())
.zip(table_terms[start..].iter())
{
*right *= &(*input_term + &beta);
*right *= &(*table_term + &gamma);
*right *= &(*input_term + &(*beta));
*right *= &(*table_term + &(*gamma));
}
});

View file

@ -41,7 +41,7 @@ impl<C: CurveAffine> Proof<C> {
&'a self,
vk: &'a VerifyingKey<C>,
l_0: C::Scalar,
argument: Argument,
argument: &'a Argument,
theta: ChallengeTheta<C::Scalar>,
beta: ChallengeBeta<C::Scalar>,
gamma: ChallengeGamma<C::Scalar>,
@ -106,13 +106,13 @@ impl<C: CurveAffine> Proof<C> {
))
}
pub(crate) fn evals(&self) -> impl Iterator<Item = C::Scalar> {
pub(crate) fn evals(&self) -> impl Iterator<Item = &C::Scalar> {
iter::empty()
.chain(Some(self.product_eval))
.chain(Some(self.product_inv_eval))
.chain(Some(self.permuted_input_eval))
.chain(Some(self.permuted_input_inv_eval))
.chain(Some(self.permuted_table_eval))
.chain(Some(&self.product_eval))
.chain(Some(&self.product_inv_eval))
.chain(Some(&self.permuted_input_eval))
.chain(Some(&self.permuted_input_inv_eval))
.chain(Some(&self.permuted_table_eval))
}
pub(in crate::plonk) fn queries<'a>(

View file

@ -3,8 +3,8 @@ use std::iter;
use super::{
circuit::{Advice, Assignment, Circuit, Column, ConstraintSystem, Fixed},
permutation, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX, ChallengeY, Error,
Proof, ProvingKey,
lookup, permutation, ChallengeBeta, ChallengeGamma, ChallengeTheta, ChallengeX, ChallengeY,
Error, Proof, ProvingKey,
};
use crate::arithmetic::{eval_polynomial, Curve, CurveAffine, FieldExt};
use crate::poly::{
@ -172,6 +172,28 @@ impl<C: CurveAffine> Proof<C> {
// Sample theta challenge for keeping lookup columns linearly independent
let theta = ChallengeTheta::<C::Scalar>::get(&mut transcript);
// Construct permuted values for each lookup
let lookups_permuted = pk
.vk
.cs
.lookups
.iter()
.map(|lookup| {
lookup
.commit_permuted(
&pk,
&params,
&domain,
theta,
&witness.advice,
&pk.fixed_values,
&aux,
&mut transcript,
)
.unwrap()
})
.collect::<Vec<_>>();
// Sample beta challenge
let beta = ChallengeBeta::get(&mut transcript);
@ -192,6 +214,40 @@ impl<C: CurveAffine> Proof<C> {
None
};
// Construct products for each lookup
let lookups_products = pk
.vk
.cs
.lookups
.iter()
.zip(lookups_permuted.iter())
.map(|(lookup, permuted)| {
lookup
.commit_product(
permuted,
&pk,
&params,
theta,
beta,
gamma,
&witness.advice,
&pk.fixed_values,
&aux,
&mut transcript,
)
.unwrap()
})
.collect::<Vec<_>>();
let lookups = lookups_permuted
.iter()
.zip(lookups_products.iter())
.map(|(permuted, product)| lookup::prover::Committed {
permuted: permuted.clone(),
product: product.clone(),
})
.collect::<Vec<_>>();
// Obtain challenge for keeping all separate gates linearly independent
let y = ChallengeY::<C::Scalar>::get(&mut transcript);
@ -202,6 +258,25 @@ impl<C: CurveAffine> Proof<C> {
.map(|(p, expressions)| (Some(p), Some(expressions)))
.unwrap_or_default();
// Evaluate the h(X) polynomial's constraint system expressions for the lookup constraints, if any.
let (lookups, lookup_expressions): (Vec<_>, Vec<_>) = lookups
.into_iter()
.zip(pk.vk.cs.lookups.iter())
.map(|(p, argument)| {
p.construct(
pk,
theta,
beta,
gamma,
argument,
&advice_cosets,
&pk.fixed_cosets,
&aux_cosets,
)
.unwrap()
})
.unzip();
// Evaluate the h(X) polynomial's constraint system expressions for the constraints provided
let h_poly = iter::empty()
// Custom constraints
@ -217,6 +292,8 @@ impl<C: CurveAffine> Proof<C> {
}))
// Permutation constraints, if any.
.chain(permutation_expressions.into_iter().flatten())
// Lookup constraints, if any.
.chain(lookup_expressions.into_iter().flatten())
.fold(domain.empty_extended(), |h_poly, v| h_poly * *y + &v);
// Divide by t(X) = X^{params.n} - 1.
@ -296,6 +373,12 @@ impl<C: CurveAffine> Proof<C> {
// Evaluate the permutations, if any, at omega^i x.
let permutations = permutations.map(|p| p.evaluate(pk, x, &mut transcript));
// Evaluate the lookups, if any, at omega^i x.
let lookups = lookups
.into_iter()
.map(|p| p.evaluate(pk, x, &mut transcript))
.collect::<Vec<_>>();
let instances =
iter::empty()
.chain(pk.vk.cs.advice_queries.iter().enumerate().map(
@ -339,13 +422,15 @@ impl<C: CurveAffine> Proof<C> {
let multiopening = multiopen::Proof::create(
params,
&mut transcript,
instances.chain(
permutations
.as_ref()
.map(|p| p.open(pk, x))
.into_iter()
.flatten(),
),
instances
.chain(
permutations
.as_ref()
.map(|p| p.open(pk, x))
.into_iter()
.flatten(),
)
.chain(lookups.iter().map(|p| p.open(pk, x)).into_iter().flatten()),
)
.map_err(|_| Error::OpeningError)?;
@ -353,6 +438,7 @@ impl<C: CurveAffine> Proof<C> {
advice_commitments,
h_commitments,
permutations: permutations.map(|p| p.build()),
lookups: lookups.into_iter().map(|p| p.build()).collect::<Vec<_>>(),
advice_evals,
fixed_evals,
aux_evals,

View file

@ -51,6 +51,11 @@ impl<'a, C: CurveAffine> Proof<C> {
// Sample theta challenge for keeping lookup columns linearly independent
let theta = ChallengeTheta::get(&mut transcript);
// Hash each lookup permuted commitment
for lookup in &self.lookups {
lookup.absorb_permuted_commitments(&mut transcript)?;
}
// Sample beta challenge
let beta = ChallengeBeta::get(&mut transcript);
@ -62,6 +67,11 @@ impl<'a, C: CurveAffine> Proof<C> {
p.absorb_commitments(&mut transcript)?;
}
// Hash each lookup product commitment
for lookup in &self.lookups {
lookup.absorb_product_commitment(&mut transcript)?;
}
// Sample y challenge, which keeps the gates linearly independent.
let y = ChallengeY::get(&mut transcript);
@ -93,6 +103,7 @@ impl<'a, C: CurveAffine> Proof<C> {
.into_iter()
.flatten(),
)
.chain(self.lookups.iter().map(|p| p.evals()).into_iter().flatten())
{
transcript.absorb_scalar(*eval);
}
@ -142,13 +153,21 @@ impl<'a, C: CurveAffine> Proof<C> {
.verify(
params,
&mut transcript,
queries.chain(
self.permutations
.as_ref()
.map(|p| p.queries(vk, x))
.into_iter()
.flatten(),
),
queries
.chain(
self.permutations
.as_ref()
.map(|p| p.queries(vk, x))
.into_iter()
.flatten(),
)
.chain(
self.lookups
.iter()
.map(|p| p.queries(vk, x))
.into_iter()
.flatten(),
),
msm,
)
.map_err(|_| Error::OpeningError)
@ -180,6 +199,10 @@ impl<'a, C: CurveAffine> Proof<C> {
.map(|p| p.check_lengths(vk))
.transpose()?;
if self.lookups.len() != vk.cs.lookups.len() {
return Err(Error::IncompatibleParams);
}
// TODO: check h_commitments
if self.advice_commitments.len() != vk.cs.num_advice_columns {
@ -230,6 +253,26 @@ impl<'a, C: CurveAffine> Proof<C> {
.into_iter()
.flatten(),
)
.chain(
self.lookups
.iter()
.zip(vk.cs.lookups.iter())
.map(|(p, argument)| {
p.expressions(
vk,
l_0,
argument,
theta,
beta,
gamma,
&self.advice_evals,
&self.fixed_evals,
&self.aux_evals,
)
})
.into_iter()
.flatten(),
)
.fold(C::Scalar::zero(), |h_eval, v| h_eval * &y + &v);
// Compute h(x) from the prover