Skip to content

Commit

Permalink
A/B polynomial evaluations in CRS are checked against the same comput…
Browse files Browse the repository at this point in the history 
…ed using the powers of tau
  • Loading branch information
@swasilyev
swasilyev committed Feb 3, 2020
1 parent 0338019 commit 3610163
Showing 1 changed file with 68 additions and 24 deletions.
92 changes: 68 additions & 24 deletions src/groth16/mod.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -548,9 +548,8 @@ impl<E: Engine> ExtendedParameters<E> {
// - bases
pub fn verify<C: Circuit<E>>(&self, circuit: C) -> Result<(), SynthesisError> {

// Convert the circuit in R1CS to the QAP in Lagrange base in the roots of unity.
// As the check is given in monomial base, later the polynomials are interpolated with iFFT.
// The additional input and constraints are Groth16/bellman specific, see the code in generator or prover.
// Convert the circuit in R1CS to the QAP in Lagrange base in the roots of unity
// The additional input and constraints are Groth16/bellman specific, see the code in generator or prover

This comment has been minimized.

Sign in to view

Copy link
@mmaker

mmaker Apr 30, 2020

There's a dot missing at the end of all these sentences (the rest of the file always puts them).
You might want to add it for coherence!

let mut assembly = KeypairAssembly {
num_inputs: 0,
Expand All @@ -576,9 +575,38 @@ impl<E: Engine> ExtendedParameters<E> {
assembly.enforce(|| "", |lc| lc + Variable(Index::Input(i)), |lc| lc, |lc| lc);
}



// Convert the QAP polynomials to monomial base and evaluate them in tau in the exponent

This comment has been minimized.

Sign in to view

Copy link
@mmaker

mmaker Apr 30, 2020

what does it mean "monomial base"? Also, there's a pronoun/article missing before "monomial base"

This comment has been minimized.

Sign in to view

Copy link
@swasilyev

swasilyev May 4, 2020

Author Collaborator

I use the term "monomial base" to highlight that the poly is presented using its coefficients (= coordinate vector in the usual basis 1, x, ..., x^n, that i call "monomial", not sure if it requires an article) as opposed to its evaluations in the roots of unity, which i call Lagrange.

This comment has been minimized.

Sign in to view

Copy link
@burdges

burdges May 4, 2020

"monomial basis"

This comment has been minimized.

Sign in to view

Copy link
@swasilyev

swasilyev May 4, 2020

Author Collaborator

"monomial basis"

the?

This comment has been minimized.

Sign in to view

Copy link
@burdges

burdges May 4, 2020

Yes a or the
// Polynomials corresponding to the (public) inputs go first
// These evaluations are used twice:
// 1. ai and ci in G1 and bi in G2 are used in sections 4 and 5 of the Fuchsbauer's check
// 2. ai in G1 and bi in G1 and G2 to validate evaluations provided by bellman CRS that are actually used by the prover

let mut a_g1 = vec![E::G1::zero(); assembly.num_inputs + assembly.num_aux];
let mut b_g1 = vec![E::G1::zero(); assembly.num_inputs + assembly.num_aux];
let mut b_g2 = vec![E::G2::zero(); assembly.num_inputs + assembly.num_aux];
let mut c_g1 = vec![E::G1::zero(); assembly.num_inputs + assembly.num_aux];
for ((((((ai_g1, bi_g1), bi_g2), ci_g1), a_coeffs), b_coeffs), c_coeffs) in a_g1.iter_mut()
.zip(b_g1.iter_mut())
.zip(b_g2.iter_mut())
.zip(c_g1.iter_mut())
.zip(assembly.at_inputs.iter().chain(assembly.at_aux.iter()))
.zip(assembly.bt_inputs.iter().chain(assembly.bt_aux.iter()))
.zip(assembly.ct_inputs.iter().chain(assembly.ct_aux.iter()))
{
*ai_g1 = eval1::<E>(a_coeffs, &self.taus_g1, assembly.num_constraints)?;
*bi_g1 = eval1::<E>(b_coeffs, &self.taus_g1, assembly.num_constraints)?;
*bi_g2 = eval2::<E>(b_coeffs, &self.taus_g2, assembly.num_constraints)?;
*ci_g1 = eval1::<E>(c_coeffs, &self.taus_g1, assembly.num_constraints)?;
}


//TODO: sizes
assert_eq!(self.params.l.len(), assembly.num_aux);

// https://eprint.iacr.org/2017/587, p. 26

This comment has been minimized.

Sign in to view

Copy link
@mmaker

mmaker Apr 30, 2020

I would personally put a more informative description, like:
«The following corresponds to the CRS verification procedure in https://eprint.iacr.org/2017/587, p. 26.»

I would also change the comments below from "// 1" to "// CRS check 1", and so on.

// 1
// P1 != 0
if self.g1.is_zero() {
Expand Down Expand Up @@ -642,26 +670,24 @@ impl<E: Engine> ExtendedParameters<E> {
if E::pairing(self.g1, self.params.vk.delta_g2) != E::pairing(self.params.vk.delta_g1, self.g2) {
return Err(SynthesisError::MalformedCrs);
}
//
for (((li, ai), bi), ci) in self.params.l.iter()
.zip(assembly.at_aux.iter())
.zip(assembly.bt_aux.iter())
.zip(assembly.ct_aux.iter())

for (((li, ai_g1), bi_g2), ci_g1) in self.params.l.iter()
.zip(a_g1.iter().skip(assembly.num_inputs))
.zip(b_g2.iter().skip(assembly.num_inputs))
.zip(c_g1.iter().skip(assembly.num_inputs))
{
let lhs = E::pairing(li.clone(), self.params.vk.delta_g2);
let eval_a = eval1::<E>(ai, &self.taus_g1, assembly.num_constraints)?;
let eval_b = eval2::<E>(bi, &self.taus_g2, assembly.num_constraints)?;
let eval_c = eval1::<E>(ci, &self.taus_g1, assembly.num_constraints)?;
let mut rhs = E::pairing(eval_a, self.params.vk.beta_g2);
rhs.mul_assign(&E::pairing(self.params.vk.alpha_g1, eval_b));
rhs.mul_assign(&E::pairing(eval_c, self.g2));
let mut rhs = E::pairing(ai_g1.clone(), self.params.vk.beta_g2);
rhs.mul_assign(&E::pairing(self.params.vk.alpha_g1, bi_g2.clone()));
rhs.mul_assign(&E::pairing(ci_g1.clone(), self.g2));
if lhs != rhs {
return Err(SynthesisError::MalformedCrs);
}
}

// 5
// z (aka t in Groth16/bellman) is the vanishing polynomial of the domain. In our case z = x^m - 1
// btw, there's a typo un Fuc19, as z should have degree d-1 in his notation

This comment has been minimized.

Sign in to view

Copy link
@mmaker

mmaker Apr 30, 2020 •
edited
Loading

In definition 3.3 I see that Z is defined really for having degree d? It's difficult to think it's a typo repeated a couple times

This comment has been minimized.

Sign in to view

Copy link
@swasilyev

swasilyev May 4, 2020 •
edited
Loading

Author Collaborator

Def. 3.3 in Fuc19 is correct. So we have domain size = vanishing poly z degree = d; a,b,c then have degree d-1 and the quotient h -- d-2. And this is consistent with the check input on page 26. The typo is in the last check in section 4: in the rhs there is a poly of degree d-1. This sum should really be ... \sum_{k=0}^{d}z_k pk_{H, k}. Then we need to know pk_{H, k} for k = d that is not present in the CRS as defined. So i claim there should be an additional power of tau added to CRS

This comment has been minimized.

Sign in to view

Copy link
@swasilyev

swasilyev May 11, 2020

Author Collaborator

The typo is in the last check in section 4
On p. 26
let mut z = self.taum_g1.into_projective();
let g1 = self.taus_g1[0].into_projective();
z.sub_assign(&g1);
Expand All @@ -671,23 +697,41 @@ impl<E: Engine> ExtendedParameters<E> {
}
}

for (((ici, ai), bi), ci) in self.params.vk.ic.iter()
.zip(assembly.at_inputs.iter())
.zip(assembly.bt_inputs.iter())
.zip(assembly.ct_inputs.iter())
for (((ici, ai_g1), bi_g2), ci_g1) in self.params.vk.ic.iter()
.zip(a_g1.iter())
.zip(b_g2.iter())
.zip(c_g1.iter())
{
let lhs = E::pairing(ici.clone(), self.params.vk.gamma_g2);
let eval_a = eval1::<E>(ai, &self.taus_g1, assembly.num_constraints)?;
let eval_b = eval2::<E>(bi, &self.taus_g2, assembly.num_constraints)?;
let eval_c = eval1::<E>(ci, &self.taus_g1, assembly.num_constraints)?;
let mut rhs = E::pairing(eval_a, self.params.vk.beta_g2);
rhs.mul_assign(&E::pairing(self.params.vk.alpha_g1, eval_b));
rhs.mul_assign(&E::pairing(eval_c, self.g2));
let mut rhs = E::pairing(ai_g1.clone(), self.params.vk.beta_g2);
rhs.mul_assign(&E::pairing(self.params.vk.alpha_g1, bi_g2.clone()));
rhs.mul_assign(&E::pairing(ci_g1.clone(), self.g2));
if lhs != rhs {
return Err(SynthesisError::MalformedCrs);
}
}

// Check that QAP polynomial evaluations given in the CRS coincide with those computed above

// assert_eq!(self.params.a.len(), assembly.num_inputs + assembly.num_aux);
// assert_eq!(self.params.b_g1.l en(), assembly.num_inputs + assembly.num_aux);
// assert_eq!(self.params.b_g2.len(), assembly.num_inputs + assembly.num_aux);

// TODO: filter zero evaluations at the very beginning
for (((((ai_g1, bi_g1), bi_g2), crs_ai_g1), crs_bi_g1), crs_bi_g2) in a_g1.iter().filter(|e| !e.is_zero())

This comment has been minimized.

Sign in to view

Copy link
@mmaker

mmaker Apr 30, 2020

I don't understand why you filter a_g1, b_g1, b_g2 by not being zero. If there's one that gives zero all items will be misaligned won't they? also I don't find it in the subversion check

This comment has been minimized.

Sign in to view

Copy link
@swasilyev

swasilyev May 4, 2020 •
edited
Loading

Author Collaborator

So did i when found it in original bellman: https://github.com/zkcrypto/bellman/blob/0aab37f418c7258db66165ee8553d7e6373db058/src/groth16/generator.rs#L458

I thought that, being evaluations of polynomials at a random point, these guys shouldn't really be zero. But some of them actually are. In QAP they represent quite valid R1CS constraints of the form A * B = C, where one of the linear combinations A, B, or C is 0. One example is "is zero" constraint: x * 1 = 0. Also bellman adds redundant constraints itself here: https://github.com/zkcrypto/bellman/blob/0aab37f418c7258db66165ee8553d7e6373db058/src/groth16/generator.rs#L188-L192 (Zexe afair doen't do that, see zkcrypto#36)
And finally, as we force the domain size to be a power of 2, and the number of constraints = the size of domain, we have additional 0 * 0 = 0 constraints.

We have an R1CS sat problem AxoBx=Cx where x is a wire vector of size M (we don't distinguish witness/input here), matrices A, B and C are then DxM, so we interpolate column-wise to get 3*M polys of degree D-1. While having fully unconstrainted wires doesn't make sense, a wire that has constraints only, say, in A and B, but not in C is a valid case.
.zip(b_g1.iter().filter(|e| !e.is_zero()))
.zip(b_g2.iter().filter(|e| !e.is_zero()))
.zip(self.params.a.iter())
.zip(self.params.b_g1.iter())
.zip(self.params.b_g2.iter())
{
if ai_g1.into_affine() != *crs_ai_g1
|| bi_g1.into_affine() != *crs_bi_g1
|| bi_g2.into_affine() != *crs_bi_g2 {
return Err(SynthesisError::MalformedCrs);
}
}

Ok(())
}
}
Expand Down

0 comments on commit 3610163

Please sign in to comment.