Understanding the implementation of the $f (ζ) = Z_{H} (ζ) t (ζ)$ check

Unlike the latest version of vanilla $P l o n K$ 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 $f (ζ) = Z_{H} (ζ) t (ζ)$ . 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 $f (z)$ is computed on the prover side (or the commitment of $f$ 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:

$- 1 \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) β \cdot σ [6] (x)$

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

the two sides of the coin: $z (ζ) \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot zkpm (ζ) \cdot α^{PERM0} (w [0] (ζ) + β \cdot shift [0] (ζ) + γ) (w [1] (ζ) + β \cdot shift [1] (ζ) + γ) (w [2] (ζ) + β \cdot shift [2] (ζ) + γ) (w [3] (ζ) + β \cdot shift [3] (ζ) + γ) (w [4] (ζ) + β \cdot shift [4] (ζ) + γ) (w [5] (ζ) + β \cdot shift [5] (ζ) + γ) (w [6] (ζ) + β \cdot shift [6] (ζ) + γ)$ with $shift [0] = 1$
and $- 1 \cdot \cdot \cdot \cdot \cdot \cdot \cdot \cdot z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) (w [6] (ζ) + β \cdot σ [6] (ζ) + γ)$
the initialization: $(z (ζ) - 1) \cdot L_{1} (ζ) \cdot α^{PERM1}$
and the end of the accumulator: $(z (ζ) - 1) \cdot L_{n - k} (ζ) \cdot α^{PERM2}$

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 $f (ζ) = Z_{H} (ζ) t (ζ)$ we’ll actually have to check something like this (I colored the missing parts on the left-hand side of the equation):

$f (ζ) + pub (ζ) + z (ζ) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + βζ + γ) \cdot (w [1] (ζ) + β \cdot shift [0] (ζ) + γ) \cdot (w [2] (ζ) + β \cdot shift [1] (ζ) + γ) \cdot (w [3] (ζ) + β \cdot shift [2] (ζ) + γ) \cdot (w [4] (ζ) + β \cdot shift [3] (ζ) + γ) \cdot (w [5] (ζ) + β \cdot shift [4] (ζ) + γ) \cdot (w [6] (ζ) + β \cdot shift [5] (ζ) + γ) - z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot \cdot (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) \cdot \cdot (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) \cdot \cdot (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) \cdot \cdot (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) \cdot \cdot (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) \cdot \cdot (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) \cdot \cdot (w [6] (ζ) + γ) + (z (ζ) - 1) \cdot L_{1} (ζ) \cdot α^{PERM1} + (z (ζ) - 1) \cdot L_{n - k} (ζ) \cdot α^{PERM2} = t (ζ) (ζ^{n} - 1)$

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:

$f (ζ) + pub (ζ) + z (ζ) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + β \cdot shift [0] ζ + γ) \cdot (w [1] (ζ) + β \cdot shift [1] ζ + γ) \cdot (w [2] (ζ) + β \cdot shift [2] ζ + γ) \cdot (w [3] (ζ) + β \cdot shift [3] ζ + γ) \cdot (w [4] (ζ) + β \cdot shift [4] ζ + γ) \cdot (w [5] (ζ) + β \cdot shift [5] ζ + γ) \cdot (w [6] (ζ) + β \cdot shift [6] ζ + γ) - z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot \cdot (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) \cdot (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) \cdot (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) \cdot (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) \cdot (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) \cdot (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) \cdot (w [6] (ζ) + γ) - t (ζ) (ζ^{n} - 1) = (1 - z (ζ)) L_{1} (ζ) α^{PERM1} + (1 - z (ζ)) L_{n - k} (ζ) α^{PERM2}$

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

$f (ζ) + + - - = pub (ζ) z (ζ) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + β \cdot shift [0] ζ + γ) \cdot (w [1] (ζ) + β \cdot shift [1] ζ + γ) \cdot (w [2] (ζ) + β \cdot shift [2] ζ + γ) \cdot (w [3] (ζ) + β \cdot shift [3] ζ + γ) \cdot (w [4] (ζ) + β \cdot shift [4] ζ + γ) \cdot (w [5] (ζ) + β \cdot shift [5] ζ + γ) \cdot (w [6] (ζ) + β \cdot shift [6] ζ + γ) + z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) \cdot (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) \cdot (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) \cdot (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) \cdot (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) \cdot (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) \cdot (w [6] (ζ) + γ) + t (ζ) (ζ^{n} - 1) (1 - z (ζ)) [\frac{( ζ ^{n} - 1 )}{n ( ζ - 1 )} α^{PERM1} + \frac{ω ^{n - k} ( ζ ^{n} - 1 )}{n ( ζ - ω ^{n - k} )} α^{PERM2}]$

finally we extract some terms from the lagrange basis:

$[f (ζ) + pub (ζ) + z (ζ) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + β \cdot shift [0] ζ + γ) \cdot (w [1] (ζ) + β \cdot shift [1] ζ + γ) \cdot (w [2] (ζ) + β \cdot shift [2] ζ + γ) \cdot (w [3] (ζ) + β \cdot shift [3] ζ + γ) \cdot (w [4] (ζ) + β \cdot shift [4] ζ + γ) \cdot (w [5] (ζ) + β \cdot shift [5] ζ + γ) \cdot (w [6] (ζ) + β \cdot shift [6] ζ + γ) + - z (ζ ω) \cdot zkpm (ζ) \cdot α^{PERM0} \cdot (w [0] (ζ) + β \cdot σ [0] (ζ) + γ) \cdot (w [1] (ζ) + β \cdot σ [1] (ζ) + γ) \cdot (w [2] (ζ) + β \cdot σ [2] (ζ) + γ) \cdot (w [3] (ζ) + β \cdot σ [3] (ζ) + γ) \cdot (w [4] (ζ) + β \cdot σ [4] (ζ) + γ) \cdot (w [5] (ζ) + β \cdot σ [5] (ζ) + γ) \cdot (w [6] (ζ) + γ) - t (ζ) (ζ^{n} - 1)] \cdot (ζ - 1) (ζ - ω^{n - k}) = (1 - z (ζ)) [\frac{( ζ ^{n} - 1 ) ( ζ - ω ^{n - k} )}{n} α^{PERM1} + \frac{ω ^{n - k} ( ζ ^{n} - 1 ) ( ζ - 1 )}{n} α^{PERM2}]$

with $α^{PERM0} = α^{17}, α^{PERM1} = α^{18}, α^{PERM2} = α^{19}$

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

Also, about the code:

the division by $n$ in the $α^{PERM1}$ and the $α^{PERM2}$ terms is missing (why?)
the multiplication by $w^{n - k}$ in the $α^{PERM2}$ term is missing (why?)

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

What about $t$ ?

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

#![allow(unused)]
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:

$perm (x) = - a^{PERM0} \cdot zkpl (x) \cdot [z (x) \cdot (w [0] (x) + γ + x \cdot β \cdot shift [0]) \cdot (w [1] (x) + γ + x \cdot β \cdot shift [1]) \cdot \dots z (x \cdot w) \cdot (w [0] (x) + γ + σ [0] \cdot β) \cdot (w [1] (x) + γ + σ [1] \cdot β) \cdot \dots]$

and bnd is:

$bnd (x) = a^{PERM1} \cdot \frac{z ( x ) - 1}{x - 1} + a^{PERM2} \cdot \frac{z ( x ) - 1}{x - sid [ n - k ]}$

you can see that some terms are missing in bnd, specifically the numerator $x^{n} - 1$ . 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 $Z_{H} (x) = x^{n} - 1$ .

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

Mina book

Understanding the implementation of the f(ζ)=ZH​(ζ)t(ζ) check

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

What about t?

Understanding the implementation of the $f (ζ) = Z_{H} (ζ) t (ζ)$ check

What about $t$ ?