PLONK

PLONK is a popular cryptographic proving system within the Zero Knowledge (ZK) community due to its efficiency and flexibility. It enables the verification of complex computations executed by untrusted parties through the transformation of programs into circuit representations. The system relies on a process called arithmetization, which converts logical circuits into polynomial representations. The main idea behind arithmetization is to express the computation as a set of polynomial equations. The solutions to these equations correspond to the outputs of the circuit. In this section, we will delve into the mechanics of how arithmetization works in PLONK, as well as the protocol used to generate and verify proofs.

The paper can be found here

Notation

We use the following notation.

The symbol denotes a finite field. It is fixed all along. The symbol denotes a primitive root of unity in .

All polynomials have coefficients in and the variable is usually denoted by . We denote polynomials by single letters like . We only denote them as when we want to emphasize the fact that it is a polynomial in , or we need that to explicitly define a polynomial from another one. For example when composing a polynomial with the polynomial , the result being denoted by . The symbol is not used to denote derivatives.

When interpolating at a domain , the symbols denote the Lagrange basis. That is is the polynomial such that for all , and that .

If is a matrix, then denotes the value at the row and column .

The ideas and components

Programs. Our toy example

For better clarity, we'll be using the following toy program throughout this recap.

INPUT:
  x

PRIVATE INPUT:
  e

OUTPUT:
  e * x + x - 1

The observer would have noticed that this program could also be written as , which is more sensible. But the way it is written now serves us to better explain the arithmetization of PLONK. So we'll stick to it.

The idea here is that the verifier holds some value , say . He gives it to the prover. She executes the program using her own chosen value , and sends the output value, say , along with a proof demonstrating correct execution of the program and obtaining the correct output.

In the context of PLONK, both the inputs and outputs of the program are considered public inputs. This may sound odd, but it is because these are the inputs to the verification algorithm. This is the algorithm that takes, in this case, the tuple and outputs Accept if the toy program was executed with input , some private value not revealed to the verifier, and out came . Otherwise it outputs Reject.

PLONK can be used to delegate program executions to untrusted parties, but it can also be used as a proof of knowledge. Our program could be used by a prover to demostrate that she knows the multiplicative inverse of some value in the finite field without revealing it. She would do it by sending the verifier the tuple , where is the proof of the execution of our toy program.

In our toy example this is pointless because inverting field elements is easily performed by any verifier. But change our program to the following and you get proofs of knowledge of the preimage of SHA256 digests.

PRIVATE INPUT:
  e

OUTPUT:
  SHA256(e)

Here there's no input aside from the prover's private input. As we mentioned, the output of the program is then part of the inputs to the verification algorithm. Which in this case just takes .

PLONK Arithmetization

This is the process that takes the circuit of a particular program and produces a set of mathematical tools that can be used to generate and verify proofs of execution. The end result will be a set of eight polynomials. To compute them we need first to define two matrices. We call them the matrix and the matrix. The polynomials and the matrices depend only on the program and not on any particular execution of it. So they can be computed once and used for every execution instance. To understand what they are useful for, we need to start from execution traces.

Circuits and execution traces

See the program as a sequence of gates that have left operand, a right operand and an output. The two most basic gates are multiplication and addition gates. In our example, one way of seeing our toy program is as a composition of three gates.

Gate 1: left: e, right: x, output: u = e * x Gate 2: left: u, right: x, output: v = e + x Gate 3: left: v, right: 1, output: w = v - 1

On executing the circuit, all these variables will take a concrete value. All that information can be put in table form. It will be a matrix with all left, right and output values of all the gates. One row per gate. We call the columns of this matrix . Let's build them for and . We get , and . So the first matrix is:

ABC
236
639
9-8

The last gate subtracts a constant value that is part of the program and is not a variable. So it actually has only one input instead of two. And the output is the result of subtracting to it. That's why it is handled a bit different from the second gate. The symbol "-" in the column is a consequence of that. With that we mean "any value" because it won't change the result. In the next section we'll see how we implement that. Here we'll use this notation when any value can be put there. In case we have to choose some, we'll default to .

What we got is a valid execution trace. Not all matrices of that shape will be the trace of an execution. The matrices and will be the tool we need to distinguish between valid and invalid execution traces.

The matrix

As we said, it only depends on the program itself and not on any particular evaluation of it. It has one row for each gate and its columns are called . They encode the type of gate of the rows and are designed to satisfy the following.

Claim: if columns correspond to a valid evaluation of the circuit then for all the following equality holds

This is better seen with examples. A multiplication gate is represented by the row:

001-10

And the row in the trace matrix that corresponds to the execution of that gate is

ABC
236

The equation in the claim for that row is that , which equals . The next is an addition gate. This is represented by the row

110-10

The corresponding row in the trace matrix its

ABC
639

And the equation of the claim is , which adds up to . Our last row is the gate that adds a constant. Addition by constant C can be represented by the row

100-1C

In our case . The corresponding row in the execution trace is

ABC
9-8

And the equation of the claim is . This is also zero.

Putting it altogether, the full matrix is

001-10
110-10
100-1-1

And we saw that the claim is true for our particular execution:

Not important to our example, but multiplication by constant C can be represented by:

C00-10

As you might have already noticed, there are several ways of representing the same gate in some cases. We'll exploit this in a moment.

The matrix

The claim in the previous section is clearly not an "if and only if" statement because the following trace columns do satisfy the equations but do not correspond to a valid execution:

ABC
236
000
20-19

The matrix encodes the carry of the results from one gate to the right or left operand of a subsequent one. These are called wirings. Like the matrix, it's independent of the particular evaluation. It consists of indices for all input and intermediate variables. In this case that matrix is:

LRO
012
213
3-4

Here is the index of , is the index of , is the index of , is the index of and is the index of the output . Now we can update the claim to have an "if and only if" statement.

Claim: Let be a matrix with columns . It correspond to a valid evaluation of the circuit if and only if a) for all the following equality holds b) for all such that we have .

So now our malformed example does not pass the second check.

Custom gates

Our matrices are fine now. But they can be optimized. Let's do that to showcase this flexibility of PLONK and also reduce the size of our example.

PLONK has the flexibility to construct more sophisticated gates as combinations of the five columns. And therefore the same program can be expressed in multiple ways. In our case all three gates can actually be merged into a single custom gate. The matrix ends up being a single row.

111-11

and also the matrix

LRO
012

The trace matrix for this representation is just

ABC
238

And we check that it satisfies the equation

Of course, we can't always squash an entire program into a single gate.

Public inputs

Aside from the gates that execute the program operations, additional rows must be incorporated into these matrices. This is due to the fact that the prover must demonstrate not only that she executed the program, but also that she used the appropriate inputs. Furthermore, the proof must include an assertion of the output value. As a result, a few extra rows are necessary. In our case these are the first two and the last one. The original one sits now in the third row.

-10003
-10008
111-11
1-1000

And this is the updated matrix

LRO
0--
1--
203
13-

The first row is there to force the variable with index to take the value . Similarly the second row forces variable with index to take the value . These two will be the public inputs of the verifier. The last row checks that the output of the program is the claimed one.

And the trace matrix is now

ABC
3--
8--
238
88-

With these extra rows, equations add up to zero only for valid executions of the program with input and output .

An astute observer would notice that by incorporating these new rows, the matrix is no longer independent of the specific evaluation. This is because the first two rows of the column contain concrete values that are specific to a particular execution instance. To maintain independence, we can remove these values and consider them as part of an extra one-column matrix called (stands for Public Input). This column has zeros in all rows not related to public inputs. We put zeros in the columns. The responsibility of filling in the matrix is of the prover and verifier. In our example it is

3
8
0
0

And the final matrix is

-10000
-10000
111-11
1-1000

We ended up with two matrices that depend only on the program, and . And two matrices that depend on a particular evaluation, namely the and matrices. The updated version of the claim is the following:

Claim: Let be a matrix with columns . It corresponds to a evaluation of the circuit if and only if a) for all the following equality holds b) for all such that we have .

From matrices to polynomials

In the previous section we showed how the arithmetization process works in PLONK. For a program with public inputs and gates, we constructed two matrices and , of sizes and that satisfy the following. Let

Claim: Let be a matrix with columns and a matrix. They correspond to a valid execution instance with public input given by if and only if a) for all the following equality holds b) for all such that we have , c) for all .

Polynomials enter now to squash most of these equations. We will traduce the set of all equations in conditions (a) and (b) to just a few equations on polynomials.

Let be a primitive -th root of unity and let . Let be the polynomials of degree at most that interpolate the columns at the domain . This means for example that for all . And similarly for all the other columns.

With this, condition (a) of the claim is equivalent to for all in .This is just by definition of the polynomials. But in polynomials land this is also equivalent to (a) there exists a polynomial such that , where is the polynomial .

To reduce condition (b) to polynomial equations we need to introduce the concept of permutation. A permutation is a rearrangement of a set. Usually denoted . For finite sets it is a map from a set to itself that takes all values. In our case the set will be the set of all pairs The matrix induces a permutation of this set where is equal to the indices of the next occurrence of the value at position . If already at the last occurrence, go to the first one. By next we mean the following occurrence as if the columns were stacked on each other. Let's see how this works in the example circuit. Recall is

LRO
0--
1--
203
13-

The permutation in this case is the map , , , , , , . For the positions with - values doesn't really matter right now.

It's not hard to see that condition (b) is equivalent to: for all , .

A little less obvious is that this condition is in turn equivalent to checking whether the following sets and are equal The proof this equivalence is straightforward. Give it a try!

In our example the sets in question are respectively and

You can check these sets coincide by inspection. Recall our trace matrix is

ABC
3--
8--
238
88-

Checking equality of these sets is something that can be reduced to polynomial equations. It is a very nice method that PLONK uses. To understand it better let's start with a simpler case.

Equality of sets

Suppose we have two sets of two field elements in . And we are interested in checking whether they are equal.

One thing we could do is compute and and compare them. If the sets are equal, then those elements are necessarily equal.

But the converse is not true. For example the sets and both have as the result of the product of their elements. But they are not equal. So this is not good to check equality.

Polynomials come to rescue here. What we can do instead is consider the following sets of polynomials , . Sets and are equal if and only if sets and are equal. This is because equality of polynomials boils down to equality of their coefficients. But the difference with and is that now the approach of multiplying the elements works. That is, and are equal if and only if . This is not entirely evident but follows from a property that polynomials have, called unique factorization. Here the important fact is that linear polynomials act as sort of prime factors. Anyway, you can take that for granted. The last part of this trick is to use the Schwartz-Zippel lemma and go back to the land of field elements. That means, if for some random element we have , then with overwhelming probability the equality holds.

Putting this altogether, if for some random element we have , then the sets and are equal. Of course this also holds for sets with more than two elements. Let's write that down.

Fact: Let and be sets of field elements. If for some random the following equality holds then with overwhelming probability is equal to .

And here comes the trick that reduces this check to polynomial equations. Let be a domain of the form for some primitive -th root of unity . Let and be respectively the polynomials that interpolate the following values at .

Then equals if and only if there exists a polynomial such that for all .

Let's see why. Suppose that equals . Construct as the polynomial that interpolates the following values in the same domain as and . That works. Conversely, suppose such a polynomial exists. By evaluating the equation at and using recursion we get that . Moreover, evaluating it at we obtain that The second equality holds because since it is a -th root of unity. Expanding with the values of and one obtains that equals . Which is what we wanted.

In summary. We proved the following:

Fact: Let and be sets of field elements. Let be a random field element. Let be a primitive -th root of unity and . Let and be respectively the polynomials that interpolate the values and at . If there exists a polynomial such that for all , then with overwhelming probability the sets and are equal.

Sets of tuples

In the previous section we saw how to check whether two sets of field elements are equal using polynomial equations. To be able to use it in our context we need to extend it to sets of tuples of field elements. This is pretty straightforward.

Let's start with the easy case. Let and be two sets of pairs of field elements. That is for all . The trick is very similar to the previous section.

Just as before, by looking at coefficients we can see that the sets and are equal if and only if and are equal. And notice that these are sets of polynomials, we got rid of the tuples! And now the situation is very similar to the previous section. We have that and are equal if and only if the product of their elements coincide. This is true also because polynomials in two variables are a unique factorization domain. So as before, we can use the Schwartz-Zippel lemma. Precisely, if for random , the elements and coincide, then and are equal with overwhelming probability.

Here is the statement for sets of more than two pairs of field elements.

Fact: Let and be sets of pairs of field elements. So that and the same for . Let be a random field elements. Let be a -th root of unity and . Let and be respectively the polynomials that interpolate the values and at . If there exists a polynomial such that for all , then with overwhelming probability the sets and are equal.

Going back to our case

Recall we want to rephrase condition (b) in terms of polynomials. We have already seen that condition (b) is equivalent to and being equal, where and

We cannot directly use the facts of the previous sections because our sets are not sets of field elements. Nor are they sets of pairs of field elements. They are sets of pairs with some indexes in the first coordinate and a field element in the second one. So the solution is to convert them to sets of pairs of field elements and apply the result of the previous section. So how do we map an element of the form to something of the form with and field elements? The second coordinate is trivial, we can just leave as it is and take . For the indexes pair there are multiple ways. The important thing to achieve here is that different pairs get mapped to different field elements. Recall that ranges from to and ranges from to . One way is to take a -th primitive root of unity and define . Putting it altogether, we are mapping the pair to the pair , which is a pair of field elements. Now we can consider the sets and We have that condition (b) is equivalent to and being equal.

Applying the method of the previous section to these sets, we obtain the following.

Fact: Let be a -th root of unity and and random field elements. Let . Let and be the polynomials that interpolate, respectively, the following values at : and Suppose there exists a polynomial such that for all . Then the sets and are equal with overwhelming probability.

One last minute definitions. Notice that is a primitive -th root of unity. Let .

Define to be the interpolation at of Similarly define and to be the interpolation at of the sets of values These will be useful during the protocol to work with such polynomials and the above equations.

A more compact form

The last fact is equivalent the following. There's no new idea here, just a more compact form of the same thing that allows the polynomial to be of degree at most .

Fact: Let be a -th root of unity. Let . Let and be two field elements such that for all . Let and be random field elements. Let and be the polynomials that interpolate, respectively, the following values at : and Suppose there exists a polynomial such that for all . Then the sets and are equal with overwhelming probability.

Common preprocessed input

We have arrived at the eight polynomials we mentioned at the beginning:

These are what's called the common preprocessed input.

Wrapping up the whole thing

Let's try to wrap up what we have so far. We started from a program. We saw that it can be seen as a sequence of gates with left, right and output values. That's called a circuit. From this two matrices and can be computed that capture the gates logic.

Executing the circuit leaves us with matrices and , called the trace matrix and the public input matrix, respectively. Everything we want to prove boils down to check that such matrices are valid. And we have the following result.

Fact: Let be a matrix with columns and a matrix. They correspond to a valid execution instance with public input given by if and only if a) for all the following equality holds b) for all such that we have , c) for all .

Then we constructed polynomials , , off the matrices and . They are the result of interpolating at a domain for some -th primitive root of unity and a few random values. And also constructed polynomials off the matrices and . Loosely speaking, the above fact can be reformulated in terms of polynomial equations as follows.

Fact: Let . Let be a matrix with columns and a matrix. They correspond to a valid execution instance with public input given by if and only if

a) There is a polynomial such that the following equality holds

b) There are polynomials , such that and , where

You might be wondering where the polynomials came from. Recall that for a polynomial , we have for all if and only if for some polynomial .

Finally both conditions (a) and (b) are equivalent to a single equation (c) if we let more randomness to come into play. This is:

(c) Let be a random field element. There is a polynomial such that

This last step is not obvious. You can check the paper to see the proof. Anyway, this is the equation you'll recognize below in the description of the protocol.

Randomness is a delicate matter and an important part of the protocol is where it comes from, who chooses it and when they choose it. Check out the protocol to see how it works.

Protocol

Details and tricks

Polynomial commitment scheme

A polynomial commitment scheme (PCS) is a cryptographic tool that allows one party to commit to a polynomial, and later prove properties of that polynomial. This commitment polynomial hides the original polynomial's coefficients and can be publicly shared without revealing any information about the original polynomial. Later, the party can use the commitment to prove certain properties of the polynomial, such as that it satisfies certain constraints or that it evaluates to a certain value at a specific point.

In the implementation section we'll explain the inner workings of the Kate-Zaverucha-Goldberg scheme, a popular PCS chosen in Lambdaworks for PLONK.

For the moment we only need the following about it:

It consists of a finite group and the following algorithms:

  • Commit(): This algorithm takes a polynomial and produces an element of the group . It is called the commitment of and is denoted by . It is homomorphic in the sense that . The former sum being addition of polynomials. The latter is addition in the group .
  • Open(,): It takes a polynomial and a field element and produces an element of the group . This element is called an opening proof for . It is the proof that evaluated at gives .
  • Verify(, , , ): It takes group elements and , and also field elements and . With overwhelming probability it outputs Accept if and Reject otherwise.

Blindings

As you will see in the protocol, the prover reveals the value taken by a bunch of the polynomials at a random . In order for the protocol to be Honest Verifier Zero Knowledge, these polynomials need to be blinded. This is a process that makes the values of these polynomials at seemingly random by forcing them to be of certain degree. Here's how it works.

Let's take for example the polynomial the prover constructs. This is the interpolation of the first column of the trace matrix at the domain . This matrix has all of the left operands of all the gates. The prover wishes to keep them secret. Say the trace matrix has rows. And so is . The invariant that the prover cannot violate is that must take the value , for all . This is what the interpolation polynomial satisfies. And is the unique such polynomial of degree at most with such property. But for higher degrees, there are many such polynomials.

The blinding process takes and a desired degree , and produces a new polynomial of degree exactly . This new polynomial satisfies that for all . But outside differs from .

This may seem hard but it's actually very simple. Let be the polynomial . If , with , then sample random values and define

The reason why this does the job is that for all . Therefore the added term vanishes at and leaves the values of at unchanged.

Linearization trick

This is an optimization in PLONK to reduce the number of checks of the verifier.

One of the main checks in PLONK boils down to check that , with some polynomial that looks like , and so on. In particular the verifier needs to get the value from somewhere.

For the sake of simplicity, in this section assume is exactly . Secret to the prover here are only . The polynomials and are known also to the verifier. The verifier will already have the commitments and . So the prover could send just , along with their opening proofs and let the verifier compute by himself and . Then with all these values the verifier could compute . And also use his commitments to validate the opening proofs of and .

This has the problem that computing and is expensive. The prover can instead save the verifier this by sending also along with opening proofs. Since the verifier will have the commitments and beforehand, he can check that the prover is not cheating and cheaply be convinced that the claimed values are actually and . This is much better. It involves the check of four opening proofs and the computation of off the values received from the prover. But it can be further improved as follows.

As before, the prover sends along with their opening proofs. She constructs the polynomial . She sends the value along with an opening proof of it. Notice that the value of is exactly . The verifier can compute by himself as . The verifier has everything to check all three openings and get convinced that the claimed value is true. And this value is actually . So this means no more work for the verifier. And the whole thing got reduced to three openings.

This is called the linearization trick. The polynomial is called the linearization of .

Setup

There's a one time setup phase to compute some values common to any execution and proof of the particular circuit. Precisely, the following commitments are computed and published.

Proving algorithm

Next we describe the proving algorithm for a program of size . That includes public inputs. Let be a primitive -th root of unity. Let . Define .

Assume the eight polynomials of common preprocessed input are already given.

The prover computes the trace matrix as described in the first sections. That means, with the first rows corresponding to the public inputs. It should be a matrix.

Round 1

Add to the transcript the following:

Compute polynomials as the interpolation polynomials of the columns of at the domain . Sample random Let

Compute and add them to the transcript.

Round 2

Sample from the transcript.

Let and define recursively for .

Compute the polynomial as the interpolation polynomial at the domain of the values .

Sample random values and let .

Compute and add it to the transcript.

Round 3

Sample from the transcript.

Let be the interpolation of the public input matrix at the domain .

Let

and define . Compute such that . Write with and polynomials of degree at most .

Sample random and define

Compute and add them to the transcript.

Round 4

Sample from the transcript.

Compute and add them to the transcript.

Round 5

Sample from the transcript.

Let

Define

The subscript stands for "non constant", as is the part of the linearization of that has non constant factors. The subscript "partial" indicates that it is a partial evaluation of at . Partial meaning that only some power of ar replaced by the powers of . So in particular .

Let be the opening proof at of the polynomial defined as

Let be the opening proof at of the polynomial .

Compute and .

Proof

The proof is:

Verification algorithm

Transcript initialization

The first step is to initialize the transcript in the same way the prover did, adding to it the following elements.

Extraction of values and commitments

Challenges

Firstly, the verifier needs to compute all the challenges. For that, he follows these steps:

  • Add to the transcript.
  • Sample two challenges .
  • Add to the transcript.
  • Sample a challenge .
  • Add to the transcript.
  • Sample a challenge .
  • Add to the transcript.
  • Sample a challenge .

Compute

Also he needs compute a few values off all these data. First, he computes the matrix with the public inputs and outputs. He needs to compute , where is the interpolation of at the domain . But he doesn't need to compute . He can instead compute as where is the number of public inputs and is the Lagrange basis at the domain .

Compute claimed values and

He computes

This is the constant part of the linearization of . So adding it to what the prover claims to be , he obtains

With respect to , this is actually already .

Compute and

He computes these off the commitments in the proof as follows

For , first compute

Then .

Compute claimed value and

Compute as

Also, the commitment of the polynomial is

Proof check

Now the verifier has all the necessary values to proceed with the checks.

  • Check that equals .
  • Verify the opening of at . That is, check that outputs Accept.
  • Verify the opening of at . That is, check the validity of the proof using the commitment and the value . That is, check that outputs Accept.

If all checks pass, he outputs Accept. Otherwise outputs Reject.

Implementation

In this section we discuss the implementation details of the PLONK algorithm. We use the notation and terminology of the protocol and recap sections.

At the moment our API supports the backend of PLONK. That is, all the setup, prove and verify algorithms. We temporarily rely on external sources for the definition of a circuit and the creation of the and matrices, as well as the execution of it to obtain the trace matrix . We mainly use gnark temporarily for that purpose.

So to generate proofs and validate them, we need to feed the algorithms with precomputed values of the , and matrices, and the primitive root of unity .

Let us see our API on a test circuit that provides all these values. The program in this case is the one that takes an input , a private input and computes . As in the toy example of the recap, the output of the program is added to the public inputs and the circuit actually asserts that the output is the claimed value. So more precisely, the prover will generate a proof for the statement ASSERT(x*e+5==y), where both are public inputs.

Usage

Here is the happy path.

#![allow(unused)]
fn main() {
// This is the common preprocessed input for
// the test circuit ( ASSERT(x * e + 5 == y) )
let common_preprocessed_input = test_common_preprocessed_input_2();

// Input
let x = FieldElement::from(2_u64);

// Private input
let e = FieldElement::from(3_u64);

let y, witness = test_witness_2(x, e);

let srs = test_srs(common_preprocessed_input.n);
let kzg = KZG::new(srs);

let verifying_key = setup(&common_preprocessed_input, &kzg);

let random_generator = TestRandomFieldGenerator {};
let prover = Prover::new(kzg.clone(), random_generator);

let public_input = vec![x.clone(), y];

let proof = prover.prove(
    &witness,
    &public_input,
    &common_preprocessed_input,
    &verifying_key,
);

let verifier = Verifier::new(kzg);
assert!(verifier.verify(
    &proof,
    &public_input,
    &common_preprocessed_input,
    &verifying_key
));
}

Let's brake it down. The helper function test_common_preprocessed_input_2() returns an instance of the following struct for the particular test circuit:

#![allow(unused)]
fn main() {
pub struct CommonPreprocessedInput<F: IsField> {
    pub n: usize,
    pub domain: Vec<FieldElement<F>>,
    pub omega: FieldElement<F>,
    pub k1: FieldElement<F>,

    pub ql: Polynomial<FieldElement<F>>,
    pub qr: Polynomial<FieldElement<F>>,
    pub qo: Polynomial<FieldElement<F>>,
    pub qm: Polynomial<FieldElement<F>>,
    pub qc: Polynomial<FieldElement<F>>,

    pub s1: Polynomial<FieldElement<F>>,
    pub s2: Polynomial<FieldElement<F>>,
    pub s3: Polynomial<FieldElement<F>>,

    pub s1_lagrange: Vec<FieldElement<F>>,
    pub s2_lagrange: Vec<FieldElement<F>>,
    pub s3_lagrange: Vec<FieldElement<F>>,
}
}

Apart from the eight polynomials in the canonical basis, we store also here the number of constraints , the domain , the primitive -th of unity and the element . The element will be . For convenience, we also store the polynomials in Lagrange form.

The following lines define the particular values of the program input and the private input .

#![allow(unused)]
fn main() {
// Input
let x = FieldElement::from(2_u64);

// Private input
let e = FieldElement::from(3_u64);
let y, witness = test_witness_2(x, e);
}

The function test_witness_2(x, e) returns an instance of the following struct, that holds the polynomials that interpolate the columns of the trace matrix .

#![allow(unused)]
fn main() {
pub struct Witness<F: IsField> {
    pub a: Vec<FieldElement<F>>,
    pub b: Vec<FieldElement<F>>,
    pub c: Vec<FieldElement<F>>,
}
}

Next the commitment scheme KZG (Kate-Zaverucha-Goldberg) is instantiated.

#![allow(unused)]
fn main() {
let srs = test_srs(common_preprocessed_input.n);
let kzg = KZG::new(srs);
}

The setup function performs the setup phase. It only needs the common preprocessed input and the commitment scheme.

#![allow(unused)]
fn main() {
let verifying_key = setup(&common_preprocessed_input, &kzg);
}

It outputs an instance of the struct VerificationKey.

#![allow(unused)]
fn main() {
pub struct VerificationKey<G1Point> {
    pub qm_1: G1Point,
    pub ql_1: G1Point,
    pub qr_1: G1Point,
    pub qo_1: G1Point,
    pub qc_1: G1Point,

    pub s1_1: G1Point,
    pub s2_1: G1Point,
    pub s3_1: G1Point,
}
}

It stores the commitments of the eight polynomials of the common preprocessed input. The suffix _1 means it is a commitment. It comes from the notation , where is a polynomial.

Then a prover is instantiated

#![allow(unused)]
fn main() {
let random_generator = TestRandomFieldGenerator {};
let prover = Prover::new(kzg.clone(), random_generator);
}

The prover is an instance of the struct Prover:

#![allow(unused)]
fn main() {
pub struct Prover<F, CS, R>
where
  F:  IsField,
  CS: IsCommitmentScheme<F>,
  R:  IsRandomFieldElementGenerator<F>
  {
    commitment_scheme: CS,
    random_generator: R,
    phantom: PhantomData<F>,
}
}

It stores an instance of a commitment scheme and a random field element generator needed for blinding polynomials.

Then the public input is defined. As we mentioned in the recap, the public input contains the output of the program.

#![allow(unused)]
fn main() {
let public_input = vec![x.clone(), y];
}

We then generate a proof using the prover's method prove

#![allow(unused)]
fn main() {
let proof = prover.prove(
    &witness,
    &public_input,
    &common_preprocessed_input,
    &verifying_key,
);
}

The output is an instance of the struct Proof.

#![allow(unused)]
fn main() {
pub struct Proof<F: IsField, CS: IsCommitmentScheme<F>> {
    // Round 1.
    /// Commitment to the wire polynomial `a(x)`
    pub a_1: CS::Commitment,
    /// Commitment to the wire polynomial `b(x)`
    pub b_1: CS::Commitment,
    /// Commitment to the wire polynomial `c(x)`
    pub c_1: CS::Commitment,

    // Round 2.
    /// Commitment to the copy constraints polynomial `z(x)`
    pub z_1: CS::Commitment,

    // Round 3.
    /// Commitment to the low part of the quotient polynomial t(X)
    pub t_lo_1: CS::Commitment,
    /// Commitment to the middle part of the quotient polynomial t(X)
    pub t_mid_1: CS::Commitment,
    /// Commitment to the high part of the quotient polynomial t(X)
    pub t_hi_1: CS::Commitment,

    // Round 4.
    /// Value of `a(ζ)`.
    pub a_zeta: FieldElement<F>,
    /// Value of `b(ζ)`.
    pub b_zeta: FieldElement<F>,
    /// Value of `c(ζ)`.
    pub c_zeta: FieldElement<F>,
    /// Value of `S_σ1(ζ)`.
    pub s1_zeta: FieldElement<F>,
    /// Value of `S_σ2(ζ)`.
    pub s2_zeta: FieldElement<F>,
    /// Value of `z(ζω)`.
    pub z_zeta_omega: FieldElement<F>,

    // Round 5
    /// Value of `p_non_constant(ζ)`.
    pub p_non_constant_zeta: FieldElement<F>,
    ///  Value of `t(ζ)`.
    pub t_zeta: FieldElement<F>,
    /// Batch opening proof for all the evaluations at ζ
    pub w_zeta_1: CS::Commitment,
    /// Single opening proof for `z(ζω)`.
    pub w_zeta_omega_1: CS::Commitment,
}
}

Finally, we instantiate a verifier.

#![allow(unused)]
fn main() {
let verifier = Verifier::new(kzg);
}

It's an instance of Verifier:

#![allow(unused)]
fn main() {
struct Verifier<F: IsField, CS: IsCommitmentScheme<F>> {
    commitment_scheme: CS,
    phantom: PhantomData<F>,
}
}

Finally, we call the verifier's method verify that outputs a bool.

#![allow(unused)]
fn main() {
assert!(verifier.verify(
    &proof,
    &public_input,
    &common_preprocessed_input,
    &verifying_key
));
}

Padding

All the matrices are padded with dummy rows so that their length is a power of two. To be able to interpolate their columns, we need a primitive root of unity of that order. Given the particular field used in our implementation, that means that the maximum possible size for a circuit is .

The entries of the dummy rows are filled in with zeroes in the , and matrices. The matrix needs to be consistent with the matrix. Therefore it is filled with the value of the variable with index .

Some other rows in the matrix have also dummy values. These are the rows corresponding to the and columns of the public input rows. In the recap we denoted them with the empty - symbol. They are filled in with the same logic as the padding rows, as well as the corresponding values in the matrix.

Implementation details

The implementation pretty much follows the rounds as are described in the protocol section. There are a few details that are worth mentioning.

Commitment Scheme

The commitment scheme we use is the Kate-Zaverucha-Goldberg scheme with the BLS 12 381 curve and the ate pairing. It can be found in the commitments module of the lambdaworks_crypto package.

The order of the cyclic subgroup is

0x73eda753299d7d483339d80809a1d80553bda402fffe5bfeffffffff00000001

The maximum power of two that divides is . Therefore, that is the maximum possible order for a primitive root of unity in with order a power of two.

Fiat-Shamir

Transcript strategy

Here we describe our implementation of the transcript used for the Fiat-Shamir heuristic.

A Transcript exposes two methods: append and challenge.

The method append adds a message to the transcript by updating the internal state of the hasher with the raw bytes of the message.

The method challenge returns the result of the hasher using the current internal state of the hasher. It subsequently resets the hasher and updates the internal state with the last result.

Here is an example of this process:

  1. Start a fresh transcript.
  2. Call append and pass message_1.
  3. Call append and pass message_2.
  4. The internal state of the hasher at this point is message_2 || message_1.
  5. Call challenge. The output is Hash(message_2 || message_1).
  6. Call append and pass message_3.
  7. Call challenge. The output is Hash(message_3 || Hash(message_2 || message_1)).
  8. Call append and pass message_4.

The internal state of the hasher at the end of this exercise is message_4 || Hash(message_3 || Hash(message_2 || message_1))

The underlying hasher function we use is h=sha3.

Field elements

The result of every challenge is a -bit string, which is interpreted as an integer in big-endian order. A field element is constructed out of it by taking modulo the field order. The prime field used in this implementation has a -bit order. Therefore some field elements are more probable to occur than others because they have more representatives as 256-bit integers.

Strong Fiat-Shamir

The first messages added to the transcript are all commitments of the polynomials of the common preprocessed input and the values of the public inputs. This prevents a known vulnerability called "weak Fiat-Shamir". Check out the following resources to learn more about it.

Circuit API

In this section, we'll discuss how to build your own constraint system to prove the execution of a particular program.

Simple Example

Let's take the following simple program as an example. We have two public inputs: x and y. We want to prove to a verifier that we know a private input e such that x * e = y. You can achieve this by building the following constraint system:

use lambdaworks_plonk::constraint_system::ConstraintSystem;
use lambdaworks_math::elliptic_curve::short_weierstrass::curves::bls12_381::default_types::FrField;

fn main() {
    let system = &mut ConstraintSystem::<FrField>::new();
    let x = system.new_public_input();
    let y = system.new_public_input();
    let e = system.new_variable();

    let z = system.mul(&x, &e);
    
    // This constraint system asserts that x * e == y
    system.assert_eq(&y, &z);
}

This code creates a constraint system over the field of the BLS12381 curve. Then, it creates three variables: two public inputs x and y, and a private variable e. Note that every variable is private except for the public inputs. Finally, it adds the constraints that represent a multiplication and an assertion.

Before generating proofs for this system, we need to run a setup and obtain a verifying key:

#![allow(unused)]
fn main() {
let common = CommonPreprocessedInput::from_constraint_system(&system, &ORDER_R_MINUS_1_ROOT_UNITY);
let srs = test_srs(common.n);
let kzg = KZG::new(srs); // The commitment scheme for plonk.
let vk = setup(&common, &kzg);
}

Now we can generate proofs for our system. We just need to specify the public inputs and obtain a witness that is a solution for our constraint system:

#![allow(unused)]
fn main() {
let inputs = HashMap::from([(x, FieldElement::from(4)), (e, FieldElement::from(3))]);
let assignments = system.solve(inputs).unwrap();
let witness = Witness::new(assignments, &system);
}

Once you have all these ingredients, you can call the prover:

#![allow(unused)]
fn main() {
let public_inputs = system.public_input_values(&assignments);
let prover = Prover::new(kzg.clone(), TestRandomFieldGenerator {});
let proof = prover.prove(&witness, &public_inputs, &common, &vk);
}

and verify:

#![allow(unused)]
fn main() {
let verifier = Verifier::new(kzg);
assert!(verifier.verify(&proof, &public_inputs, &common, &vk));
}

Building Complex Systems

Some operations are common, and it makes sense to wrap the set of constraints that do these operations in a function and use it several times. Lambdaworks comes with a collection of functions to help you build your own constraint systems, such as conditionals, inverses, and hash functions.

However, if you have an operation that does not come with Lambdaworks, you can easily extend Lambdaworks functionality. Suppose that the exponentiation operation is something common in your program. You can write the square and multiply algorithm and put it inside a function:

#![allow(unused)]
fn main() {
pub fn pow(
    system: &mut ConstraintSystem<FrField>,
    base: Variable,
    exponent: Variable,
) -> Variable {
    let exponent_bits = system.new_u32(&exponent);
    let mut result = system.new_constant(FieldElement::one());

    for i in 0..32 {
        if i != 0 {
            result = system.mul(&result, &result);
        }
        let result_times_base = system.mul(&result, &base);
        result = system.if_else(&exponent_bits[i], &result_times_base, &result);
    }
    result
}
}

This function can then be used to modify our simple program from the previous section. The following circuit checks that the prover knows e such that pow(x, e) = y:

use lambdaworks_plonk::constraint_system::ConstraintSystem;
use lambdaworks_math::elliptic_curve::short_weierstrass::curves::bls12_381::default_types::FrField;

fn main() {
    let system = &mut ConstraintSystem::<FrField>::new();
    let x = system.new_public_input();
    let y = system.new_public_input();
    let e = system.new_variable();

    let z = pow(system, &x, &e);
    system.assert_eq(&y, &z);
}

You can keep composing these functions in order to create more complex systems.