Understanding the implementation of the check

Unlike the latest version of vanilla that implements the final check using a polynomial opening (via Maller’s optimization), we implement it manually. (That is to say, Izaak implemented Maller’s optimization for 5-wires.)

But the check is not exactly . This note describes how and why the implementation deviates a little.

What’s f and what’s missing in the final equation?

If you look at how the evaluation of is computed on the prover side (or the commitment of is computed on the verifier side), you can see that f is missing two things:

  • the public input part
  • some terms in the permutation

What is it missing in the permutation part? Let’s look more closely. This is what we have:

In comparison, here is the list of the stuff we needed to have:

  1. the two sides of the coin: with
  2. and
  3. the initialization:
  4. and the end of the accumulator:

You can read more about why it looks like that in this post.

We can see clearly that the permutation stuff we have in f is clearly lacking. It’s just the subtraction part (equation 2), and even that is missing some terms. It is missing exactly this:

So at the end, when we have to check for the identity we’ll actually have to check something like this (I colored the missing parts on the left hand side of the equation):

This is not exactly what happens in the code. But if we move things around a bit, we end up with what’s implemented. I highlight what changes in each steps. First, we just move things around:

here are the actual lagrange basis calculated with the formula here, oh and we actually use in the code, not , so let’s change that as well:

finally we extract some terms from the lagrange basis:


Why do we do things this way? Most likely to reduce

Also, about the code:

  • the division by in the and the terms is missing (why?)
  • the multiplication by in the term is missing (why?)

As these terms are constants, and do not prevent the division by to form , also omits them. In other word, they cancel one another.

What about ?

In verifier.rs you can see the following code (cleaned to remove anything not important)

fn main() {
// compute the witness polynomials $w_0, \cdots, w_14$ and the permutation polynomial $z$ in evaluation forms on different domains
let lagrange = index.cs.evaluate(&w, &z);

// compute parts of the permutation stuff that is included in t
let (perm, bnd) = index.cs.perm_quot(&lagrange, &oracles, &z, &alpha[range::PERM])?;

// divide contributions with vanishing polynomial
let (mut t, res) = (perm + some_other_stuff).divide_by_vanishing_poly()

// add the other permutation stuff
t += &bnd;

// t is evaluated at zeta and sent...

Notice that bnd is not divided by the vanishing polynomial. Also what’s perm? Let’s answer the latter TESTREMOVEME:

and bnd is:

you can see that some terms are missing in bnd, specifically the numerator . Well, it would have been cancelled by the division by the vanishing polynomial, and this is the reason why we didn’t divide that term by .

Also, note that the same constant terms that were missing in are missing in .