diff --git a/Cargo.toml b/Cargo.toml index 8d00e9f..e8ccfdb 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -41,3 +41,6 @@ ff = "0.8" metrics = "=0.13.0-alpha.11" num_cpus = "1.13" rand = "0.7" + +[features] +sanity-checks = [] diff --git a/src/plonk/lookup/prover.rs b/src/plonk/lookup/prover.rs index 25f807d..5c32256 100644 --- a/src/plonk/lookup/prover.rs +++ b/src/plonk/lookup/prover.rs @@ -12,7 +12,7 @@ use crate::{ transcript::{Hasher, Transcript}, }; use ff::Field; -use std::collections::BTreeMap; +use std::{collections::BTreeMap, convert::TryFrom, iter}; #[derive(Clone, Debug)] pub(crate) struct Permuted { @@ -372,6 +372,171 @@ impl Argument { } } +impl Committed { + /// Given a Lookup with input columns, table columns, permuted input + /// column, permuted table column, and grand product polynomial, this + /// method constructs constraints that must hold between these values. + /// This method returns the constraints as a vector of polynomials in + /// the extended evaluation domain. + pub(in crate::plonk) fn construct<'a>( + self, + pk: &'a ProvingKey, + theta: C::Scalar, + beta: C::Scalar, + gamma: C::Scalar, + argument: Argument, + advice_cosets: &'a [Polynomial], + fixed_cosets: &'a [Polynomial], + aux_cosets: &'a [Polynomial], + ) -> Result< + ( + Constructed, + impl Iterator> + 'a, + ), + Error, + > { + let permuted = self.permuted; + let product = self.product; + let unpermuted_input_cosets: Vec> = argument + .input_columns + .iter() + .map(|&input| match input.column_type() { + Any::Advice => advice_cosets[pk + .vk + .cs + .get_advice_query_index(Column::::try_from(input).unwrap(), 0)] + .clone(), + Any::Fixed => fixed_cosets[pk + .vk + .cs + .get_fixed_query_index(Column::::try_from(input).unwrap(), 0)] + .clone(), + Any::Aux => aux_cosets[pk + .vk + .cs + .get_aux_query_index(Column::::try_from(input).unwrap(), 0)] + .clone(), + }) + .collect(); + + let unpermuted_table_cosets: Vec> = argument + .table_columns + .iter() + .map(|&table| match table.column_type() { + Any::Advice => advice_cosets[pk + .vk + .cs + .get_advice_query_index(Column::::try_from(table).unwrap(), 0)] + .clone(), + Any::Fixed => fixed_cosets[pk + .vk + .cs + .get_fixed_query_index(Column::::try_from(table).unwrap(), 0)] + .clone(), + Any::Aux => aux_cosets[pk + .vk + .cs + .get_aux_query_index(Column::::try_from(table).unwrap(), 0)] + .clone(), + }) + .collect(); + + let expressions = iter::empty() + // l_0(X) * (1 - z'(X)) = 0 + .chain(Some( + Polynomial::one_minus(product.product_coset.clone()) * &pk.l0, + )) + // z'(X) (a'(X) + \beta) (s'(X) + \gamma) + // - z'(\omega^{-1} X) (a_1(X) + \theta a_2(X) + ... + \beta) (s_1(X) + \theta s_2(X) + ... + \gamma) + .chain({ + // z'(X) (a'(X) + \beta) (s'(X) + \gamma) + let mut left = product.product_coset.clone(); + parallelize(&mut left, |left, start| { + for ((left, permuted_input), permuted_table) in left + .iter_mut() + .zip(permuted.permuted_input_coset[start..].iter()) + .zip(permuted.permuted_table_coset[start..].iter()) + { + *left *= &(*permuted_input + &beta); + *left *= &(*permuted_table + &gamma); + } + }); + + // z'(\omega^{-1} X) (a_1(X) + \theta a_2(X) + ... + \beta) (s_1(X) + \theta s_2(X) + ... + \gamma) + let mut right = product.product_inv_coset; + let mut input_terms = pk.vk.domain.empty_extended(); + + // Compress the unpermuted input columns + for input in unpermuted_input_cosets.iter() { + // (a_1(X) + \theta a_2(X) + ...) + parallelize(&mut input_terms, |input_term, start| { + for (input_term, input) in input_term.iter_mut().zip(input[start..].iter()) + { + *input_term *= θ + *input_term += input; + } + }); + } + + let mut table_terms = pk.vk.domain.empty_extended(); + // Compress the unpermuted table columns + for table in unpermuted_table_cosets.iter() { + // (s_1(X) + \theta s_2(X) + ...) + parallelize(&mut table_terms, |table_term, start| { + for (table_term, table) in table_term.iter_mut().zip(table[start..].iter()) + { + *table_term *= θ + *table_term += table; + } + }); + } + + // Add \beta and \gamma offsets + parallelize(&mut right, |right, start| { + for ((right, input_term), table_term) in right + .iter_mut() + .zip(input_terms[start..].iter()) + .zip(table_terms[start..].iter()) + { + *right *= &(*input_term + &beta); + *right *= &(*table_term + &gamma); + } + }); + + Some(left - &right) + }) + // Check that the first values in the permuted input column and permuted + // fixed column are the same. + // l_0(X) * (a'(X) - s'(X)) = 0 + .chain(Some( + (permuted.permuted_input_coset.clone() - &permuted.permuted_table_coset) * &pk.l0, + )) + // Check that each value in the permuted lookup input column is either + // equal to the value above it, or the value at the same index in the + // permuted table column. + // (a′(X)−s′(X))⋅(a′(X)−a′(\omega{-1} X)) = 0 + .chain(Some( + (permuted.permuted_input_coset.clone() - &permuted.permuted_table_coset) + * &(permuted.permuted_input_coset.clone() - &permuted.permuted_input_inv_coset), + )); + + Ok(( + Constructed { + permuted_input_poly: permuted.permuted_input_poly, + permuted_input_blind: permuted.permuted_input_blind, + permuted_input_commitment: permuted.permuted_input_commitment, + permuted_table_poly: permuted.permuted_table_poly, + permuted_table_blind: permuted.permuted_table_blind, + permuted_table_commitment: permuted.permuted_table_commitment, + product_poly: product.product_poly, + product_blind: product.product_blind, + product_commitment: product.product_commitment, + }, + expressions, + )) + } +} + /// Given a column of input values A and a column of table values S, /// this method permutes A and S to produce A' and S', such that: /// - like values in A' are vertically adjacent to each other; and