Problem in permutation argument

This commit is contained in:
wborgeaud 2021-07-14 08:14:00 +02:00
parent 5c2c01b1ab
commit c3d53392c4
7 changed files with 284 additions and 10 deletions

View File

@ -296,7 +296,7 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
}
}
fn blind_and_pad(&mut self) {
pub fn blind_and_pad(&mut self) {
let (regular_poly_openings, z_openings) = self.blinding_counts();
info!(
"Adding {} blinding terms for witness polynomials, and {}*2 for Z polynomials",
@ -349,7 +349,7 @@ impl<F: Extendable<D>, const D: usize> CircuitBuilder<F, D> {
}
}
fn constant_polys(
pub fn constant_polys(
&self,
gates: &[PrefixedGate<F, D>],
num_constants: usize,

View File

@ -8,6 +8,7 @@ use crate::fri::FriConfig;
use crate::gates::gate::{GateInstance, PrefixedGate};
use crate::generator::WitnessGenerator;
use crate::polynomial::commitment::ListPolynomialCommitment;
use crate::polynomial::polynomial::PolynomialValues;
use crate::proof::{Hash, HashTarget, Proof};
use crate::prover::prove;
use crate::target::Target;

View File

@ -459,7 +459,7 @@ mod tests {
let config = CircuitConfig::large_config();
let mut builder = CircuitBuilder::<F, D>::new(config);
let mut builder = CircuitBuilder::<F, D>::new(config.clone());
let x = FF::rand();
let y = FF::rand();

View File

@ -20,6 +20,7 @@ use crate::util::{log2_ceil, log2_strict, reverse_bits, reverse_index_bits_in_pl
pub const SALT_SIZE: usize = 2;
pub struct ListPolynomialCommitment<F: Field> {
pub original_values: Vec<PolynomialValues<F>>, // TODO: Remove when debugging is done.
pub polynomials: Vec<PolynomialCoeffs<F>>,
pub merkle_tree: MerkleTree<F>,
pub degree: usize,
@ -41,7 +42,7 @@ impl<F: Field> ListPolynomialCommitment<F> {
"to compute LDE"
);
Self::new_from_data(polynomials, lde_values, degree, rate_bits, blinding)
Self::new_from_data(values, polynomials, lde_values, degree, rate_bits, blinding)
}
/// Creates a list polynomial commitment for the polynomials `polynomials`.
@ -51,15 +52,17 @@ impl<F: Field> ListPolynomialCommitment<F> {
blinding: bool,
) -> Self {
let degree = polynomials[0].len();
let values = polynomials.iter().map(|p| p.clone().fft()).collect();
let lde_values = timed!(
Self::lde_values(&polynomials, rate_bits, blinding),
"to compute LDE"
);
Self::new_from_data(polynomials, lde_values, degree, rate_bits, blinding)
Self::new_from_data(values, polynomials, lde_values, degree, rate_bits, blinding)
}
fn new_from_data(
values: Vec<PolynomialValues<F>>,
polynomials: Vec<PolynomialCoeffs<F>>,
lde_values: Vec<Vec<F>>,
degree: usize,
@ -71,6 +74,7 @@ impl<F: Field> ListPolynomialCommitment<F> {
let merkle_tree = timed!(MerkleTree::new(leaves, false), "to build Merkle tree");
Self {
original_values: values,
polynomials,
merkle_tree,
degree,

View File

@ -1,3 +1,4 @@
use std::collections::HashMap;
use std::time::Instant;
use log::info;
@ -5,6 +6,7 @@ use rayon::prelude::*;
use crate::circuit_data::{CommonCircuitData, ProverOnlyCircuitData};
use crate::field::extension_field::Extendable;
use crate::field::field::Field;
use crate::generator::generate_partial_witness;
use crate::plonk_challenger::Challenger;
use crate::plonk_common::{PlonkPolynomials, ZeroPolyOnCoset};
@ -15,8 +17,10 @@ use crate::timed;
use crate::util::marking::MarkedTargets;
use crate::util::partial_products::partial_products;
use crate::util::{log2_ceil, transpose};
use crate::vanishing_poly::eval_vanishing_poly_base;
use crate::vars::EvaluationVarsBase;
use crate::vanishing_poly::{
eval_vanishing_poly_base, evaluate_gate_constraints, evaluate_gate_constraints_base, yoba,
};
use crate::vars::{EvaluationVars, EvaluationVarsBase};
use crate::witness::{PartialWitness, Witness};
pub(crate) fn prove<F: Extendable<D>, const D: usize>(
@ -116,6 +120,169 @@ pub(crate) fn prove<F: Extendable<D>, const D: usize>(
let alphas = challenger.get_n_challenges(num_challenges);
{
let get_at_index = |comm: &ListPolynomialCommitment<F>, i: usize| -> Vec<F> {
comm.original_values
.iter()
.map(|v| v.values[i])
.collect::<Vec<_>>()
};
let mut nums = HashMap::<F, usize>::new();
let mut dens = HashMap::<F, usize>::new();
let points = F::two_adic_subgroup(common_data.degree_bits);
for i in 0..degree {
let x = points[i];
let local_constants_sigmas = get_at_index(&prover_data.constants_sigmas_commitment, i);
let local_constants = &local_constants_sigmas[common_data.constants_range()];
let s_sigmas = &local_constants_sigmas[common_data.sigmas_range()];
let local_wires = get_at_index(&wires_commitment, i);
let vars = EvaluationVarsBase {
local_constants,
local_wires: &local_wires,
};
let numerator_values = (0..common_data.config.num_routed_wires).for_each(|j| {
let wire_value = vars.local_wires[j];
let k_i = common_data.k_is[j];
let s_id = k_i * x;
*nums
.entry(wire_value + betas[0] * s_id + gammas[0])
.or_default() += 1;
});
let denominator_values = (0..common_data.config.num_routed_wires).for_each(|j| {
let wire_value = vars.local_wires[j];
let s_sigma = s_sigmas[j];
*dens
.entry(wire_value + betas[0] * s_sigma + gammas[0])
.or_default() += 1;
});
}
println!("yo");
for (k, v) in nums.iter() {
if let Some(w) = dens.get(&k) {
if *v != *w {
println!("Bad: {} {} {}", *k, *v, *w);
}
} else {
println!("Bad: {} {}", *k, *v);
}
}
println!("ya");
for (k, v) in dens.iter() {
if let Some(w) = nums.get(&k) {
if *v != *w {
println!("Bad: {} {} {}", *k, *v, *w);
}
} else {
println!("Bad: {} {}", *k, *v);
}
}
println!("yu");
let mut bam = F::ONE;
for (k, v) in nums.iter() {
bam *= k.exp(*v as u64);
}
dbg!(bam);
let mut boom = F::ONE;
for (k, v) in dens.iter() {
boom *= k.exp(*v as u64);
}
dbg!(boom);
}
{
let get_at_index = |comm: &ListPolynomialCommitment<F>, i: usize| -> Vec<F> {
comm.original_values
.iter()
.map(|v| v.values[i])
.collect::<Vec<_>>()
};
let mut nums = vec![F::ONE; common_data.config.num_challenges];
let mut dens = vec![F::ONE; common_data.config.num_challenges];
let points = F::two_adic_subgroup(common_data.degree_bits);
for i in 0..degree {
let x = points[i];
let local_constants_sigmas = get_at_index(&prover_data.constants_sigmas_commitment, i);
let local_constants = &local_constants_sigmas[common_data.constants_range()];
let s_sigmas = &local_constants_sigmas[common_data.sigmas_range()];
let local_wires = get_at_index(&wires_commitment, i);
let vars = EvaluationVarsBase {
local_constants,
local_wires: &local_wires,
};
for ii in 0..common_data.config.num_challenges {
let numerator_values = (0..common_data.config.num_routed_wires)
.map(|j| {
let wire_value = vars.local_wires[j];
let k_i = common_data.k_is[j];
let s_id = k_i * x;
wire_value + betas[ii] * s_id + gammas[ii]
})
.collect::<Vec<_>>();
let denominator_values = (0..common_data.config.num_routed_wires)
.map(|j| {
let wire_value = vars.local_wires[j];
let s_sigma = s_sigmas[j];
wire_value + betas[ii] * s_sigma + gammas[ii]
})
.collect::<Vec<_>>();
nums[ii] *= numerator_values.into_iter().product();
dens[ii] *= denominator_values.into_iter().product();
}
}
dbg!(nums, dens);
}
{
let get_at_index = |comm: &ListPolynomialCommitment<F>, i: usize| -> Vec<F> {
comm.original_values
.iter()
.map(|v| v.values[i])
.collect::<Vec<_>>()
};
let points = F::two_adic_subgroup(common_data.degree_bits);
for i in 0..degree {
let x = points[i];
let i_next = (i + 1) % degree;
let local_constants_sigmas = get_at_index(&prover_data.constants_sigmas_commitment, i);
let local_constants = &local_constants_sigmas[common_data.constants_range()];
let s_sigmas = &local_constants_sigmas[common_data.sigmas_range()];
let local_wires = get_at_index(&wires_commitment, i);
let local_zs_partial_products = get_at_index(&zs_partial_products_commitment, i);
let local_zs = &local_zs_partial_products[common_data.zs_range()];
let next_zs =
&get_at_index(&zs_partial_products_commitment, i_next)[common_data.zs_range()];
let partial_products = &local_zs_partial_products[common_data.partial_products_range()];
debug_assert_eq!(local_wires.len(), common_data.config.num_wires);
debug_assert_eq!(local_zs.len(), num_challenges);
let vars = EvaluationVarsBase {
local_constants,
local_wires: &local_wires,
};
let mut quotient_values = yoba(
common_data,
i,
x,
vars,
local_zs,
next_zs,
partial_products,
s_sigmas,
&betas,
&gammas,
&alphas,
);
assert!(
quotient_values.iter().all(|yy| yy.is_zero()),
"{}-th gate ({}) constraints not satisfied.\n {:?}",
i,
prover_data.gate_instances[i].gate_type.0.id(),
quotient_values
);
}
}
let quotient_polys = timed!(
compute_quotient_polys(
common_data,
@ -136,8 +303,7 @@ pub(crate) fn prove<F: Extendable<D>, const D: usize>(
.flat_map(|mut quotient_poly| {
quotient_poly.trim();
quotient_poly.pad(quotient_degree).expect(
"The quotient polynomial doesn't have the right degree. \
This may be because the `Z`s polynomials are still too high degree.",
"Quotient has failed, the vanishing polynomial is not divisible by `Z_H",
);
// Split t into degree-n chunks.
quotient_poly.chunks(degree)

View File

@ -321,6 +321,7 @@ mod tests {
#[test]
fn test_recursive_verifier() {
env_logger::init();
type F = CrandallField;
type FF = QuarticCrandallField;
const D: usize = 4;

View File

@ -5,7 +5,7 @@ use crate::field::extension_field::Extendable;
use crate::field::field::Field;
use crate::gates::gate::{Gate, GateRef, PrefixedGate};
use crate::plonk_common;
use crate::plonk_common::{eval_l_1_recursively, ZeroPolyOnCoset};
use crate::plonk_common::{eval_l_1, eval_l_1_recursively, ZeroPolyOnCoset};
use crate::target::Target;
use crate::util::marking::MarkedTargets;
use crate::util::partial_products::{check_partial_products, check_partial_products_recursively};
@ -185,6 +185,108 @@ pub(crate) fn eval_vanishing_poly_base<F: Extendable<D>, const D: usize>(
plonk_common::reduce_with_powers_multi(&vanishing_terms, alphas)
}
pub(crate) fn yoba<F: Extendable<D>, const D: usize>(
common_data: &CommonCircuitData<F, D>,
index: usize,
x: F,
vars: EvaluationVarsBase<F>,
local_zs: &[F],
next_zs: &[F],
partial_products: &[F],
s_sigmas: &[F],
betas: &[F],
gammas: &[F],
alphas: &[F],
) -> Vec<F> {
let max_degree = common_data.quotient_degree_factor;
let (num_prods, final_num_prod) = common_data.num_partial_products;
let constraint_terms =
evaluate_gate_constraints_base(&common_data.gates, common_data.num_gate_constraints, vars);
// The L_1(x) (Z(x) - 1) vanishing terms.
let mut vanishing_z_1_terms = Vec::new();
// The terms checking the partial products.
let mut vanishing_partial_products_terms = Vec::new();
// The Z(x) f'(x) - g'(x) Z(g x) terms.
let mut vanishing_v_shift_terms = Vec::new();
for i in 0..common_data.config.num_challenges {
let z_x = local_zs[i];
let z_gz = next_zs[i];
vanishing_z_1_terms.push(eval_l_1(common_data.degree(), x) * (z_x - F::ONE));
let numerator_values = (0..common_data.config.num_routed_wires)
.map(|j| {
let wire_value = vars.local_wires[j];
let k_i = common_data.k_is[j];
let s_id = k_i * x;
wire_value + betas[i] * s_id + gammas[i]
})
.collect::<Vec<_>>();
let denominator_values = (0..common_data.config.num_routed_wires)
.map(|j| {
let wire_value = vars.local_wires[j];
let s_sigma = s_sigmas[j];
wire_value + betas[i] * s_sigma + gammas[i]
})
.collect::<Vec<_>>();
let quotient_values = (0..common_data.config.num_routed_wires)
.map(|j| numerator_values[j] / denominator_values[j])
.collect::<Vec<_>>();
// The partial products considered for this iteration of `i`.
let current_partial_products = &partial_products[i * num_prods..(i + 1) * num_prods];
// Check the numerator partial products.
let mut partial_product_check =
check_partial_products(&quotient_values, current_partial_products, max_degree);
// The first checks are of the form `q - n/d` which is a rational function not a polynomial.
// We multiply them by `d` to get checks of the form `q*d - n` which low-degree polynomials.
denominator_values
.chunks(max_degree)
.zip(partial_product_check.iter_mut())
.for_each(|(d, q)| {
*q *= d.iter().copied().product();
});
vanishing_partial_products_terms.extend(partial_product_check);
// The quotient final product is the product of the last `final_num_prod` elements.
let quotient: F = current_partial_products[num_prods - final_num_prod..]
.iter()
.copied()
.product();
assert_eq!(
quotient,
numerator_values.iter().copied().product::<F>()
/ denominator_values.iter().copied().product::<F>()
);
vanishing_v_shift_terms.push(quotient * z_x - z_gz);
}
if vanishing_z_1_terms.iter().any(|x| !x.is_zero()) {
dbg!(&vanishing_z_1_terms);
}
if vanishing_partial_products_terms
.iter()
.any(|x| !x.is_zero())
{
dbg!(&vanishing_partial_products_terms);
}
if vanishing_v_shift_terms.iter().any(|x| !x.is_zero()) {
dbg!(&vanishing_v_shift_terms);
}
if constraint_terms.iter().any(|x| !x.is_zero()) {
dbg!(&constraint_terms);
}
[
vanishing_z_1_terms,
vanishing_partial_products_terms,
vanishing_v_shift_terms,
constraint_terms,
]
.concat()
}
/// Evaluates all gate constraints.
///
/// `num_gate_constraints` is the largest number of constraints imposed by any gate. It is not