ToolszkEVMSpecIndex

Simple Example

This document explains the fundamentals of Polynomial Identity Language with the help of a simple multiplier program. PIL was designed with the aim to simplify

This document explains the fundamentals of Polynomial Identity Language with the help of a simple multiplier program.

PIL was designed with the aim to simplify the proving and verification of execution correctness. Given that PIL is geared towards modularity, each PIL code has to stipulate a unique identifier for each program. It therefore has an effective syntax that is easy to learn.

In the nutshell, a typical PIL code states the program identifier, the parameters used in the program's computations as well as constraints these parameters must satisfy.

Key features

A PIL code starts with the program's namespace\texttt{namespace} which is a reserved keyword used to identify the program being executed and to frame the scope of the program definition.

The namespace\texttt{namespace} has to be instantiated with a unique name together with an argument representing the length\texttt{length} of the program, which is the maximum number of rows in any execution trace of the program.

In a PIL code, one should define the polynomials\texttt{polynomials} used by its program and the constraints\texttt{constraints} among the defined polynomials. Polynomials are identified by the keyword pol\texttt{pol}.

As opposed to constant\texttt{constant} polynomials which are preprocessed for a given program, committed\texttt{committed} polynomials are allowed to change from one execution to the next. Constant polynomials are considered public as they are known by all parties, while committed polynomials are in most cases, only known by one party (usually the proving party).

The keyword commit\texttt{commit} allows the compiler to identify the corresponding polynomial as committed.

Multiplier program in PIL

Let us create a simple PIL program that models the computation of the product of two integers. Consider a program that, at each step, takes two input numbers and multiplies them.

Such a program is commonly referred to as the Multiplier\text{Multiplier} program, and it can be modelled by using 3 polynomials;

freeIn1, freeIn2  and  out\mathtt{freeIn1},\ \mathtt{freeIn2}\ \text{ and }\ \mathtt{out}

where freeIn1\mathtt{freeIn1} and freeIn2\mathtt{freeIn2} are "free" inputs and out\mathtt{out} is the output. The term “free" refers to the fact the values are arbitrarily chosen and they do not strictly depend on any previously computed values.

The corresponding execution trace would be correct if the values in the output out\mathtt{out} column satisfy the following identity:

out = freeIn1  freeIn2.(Eqn. 1)\mathtt{out}\ =\ \mathtt{freeIn1}\ *\ \mathtt{freeIn2}. \tag{Eqn. 1}

See the execution trace of the Multiplier program in the table below:

rowfreeIn1freeIn2out  1428  2313  3090  47321  54416  65630   \begin{aligned} \begin{array}{|l|c|c|c|c|c|c|c|}\hline \texttt{row} & \mathtt{freeIn1} & \mathtt{freeIn2} & \texttt{out} \\ \hline \ \text{ 1} & \texttt{4} & \texttt{2} & \texttt{8} \\ \hline \ \text{ 2} & \texttt{3} & \texttt{1} & \texttt{3} \\ \hline \ \text{ 3} & \texttt{0} & \texttt{9} & \texttt{0} \\ \hline \ \text{ 4} & \texttt{7} & \texttt{3} & \texttt{21} \\ \hline \ \text{ 5} & \texttt{4} & \texttt{4} & \texttt{16} \\ \hline \ \text{ 6} & \texttt{5} & \texttt{6} & \texttt{30} \\ \hline \text{ } \ \vdots & \vdots & \vdots & \vdots \\ \hline \end{array} \end{aligned}

Since the above identity, labelled Eqn. 1\text{Eqn. 1}, is satisfied in each of the rows of the execution trace, it means that the output column is filled with correct values.

In the language of proof/verification systems concerned with proving and verifying the correctness of the execution trace, the two inputs freeIn1\mathtt{freeIn1} and freeIn2\mathtt{freeIn2} together with the output out\mathtt{out} are referred to as polynomials\text{polynomials}.

So, the values in each column of the execution trace actually represents or describes a particular polynomial. Such polynomials can be computed by interpolation\text{interpolation}.

The PIL code for the above Multiplier program is as follows.

namespace Multiplier(2**10);

// Polynomials
pol commit freeIn1;
pol commit freeIn2;
pol commit out;

// Constraints
out = freeIn1*freeIn2;

In the above figure, the namespace given to the Multiplier program is Multiplier\texttt{Multiplier}, and its specified length is 2102^{10}.

In the zkEVM context, these polynomials would be committed by the Main state machine for verification, they appear in the PIL code as pol commit.

Optimized Multiplier program

The above design of the Multiplier program, as represented by its execution trace, does not scale easily to more complex operations. The number of polynomials (or number of columns) grows linearly with the number of operations that needs to be performed.

For example, if we were to design a Multiplier program that computes 2102^{10} operation, the above design would require 2102^{10} committed polynomials, which is far from being practical.

Here's a more practical design, which reduces the 2102^{10} committed polynomials to only 3 polynomials;

  1. The freeIn\texttt{freeIn} polynomial which records, as a column in the execution trace, each input one at a time.

  2. The RESET\texttt{RESET} polynomial (column) which flags the starting row of each operation by evaluating to 11 in each odd row and 00 otherwise.

  3. The out\texttt{out} polynomial which holds the result of the operation as before.

See the below table for the corresponding execution trace:

rowfreeInRESETout  1410  2204  3318  4103  5913  6009  7010    \begin{aligned} \begin{array}{|l|c|c|c|c|}\hline \texttt{row} & \mathtt{freeIn} & \mathtt{RESET} & \texttt{out} \\ \hline \ \text{ 1} & \texttt{4} & \texttt{1} & \texttt{0} \\ \hline \ \text{ 2} & \texttt{2} & \texttt{0} & \texttt{4} \\ \hline \ \text{ 3} & \texttt{3} & \texttt{1} & \texttt{8} \\ \hline \ \text{ 4} & \texttt{1} & \texttt{0} & \texttt{3} \\ \hline \ \text{ 5} & \texttt{9} & \texttt{1} & \texttt{3} \\ \hline \ \text{ 6} & \texttt{0} & \texttt{0} & \texttt{9} \\ \hline \ \text{ 7} & \texttt{0} & \texttt{1} & \texttt{0} \\ \hline \text{ }\ \text{ } \vdots & \vdots & \vdots & \vdots \\ \hline \end{array} \end{aligned}

Observe how each column of the execution trace records the "state" in each row.

  • row 1\texttt{row 1} : The freeIn\texttt{freeIn} column records the first input 44 of the operation, hence RESET\texttt{RESET} reflects a 11, while out\texttt{out} records 00 as its default initial value.

  • row 2\texttt{row 2} : The freeIn\texttt{freeIn} column records the second input 22 of the operation, RESET\texttt{RESET} reflects a 00 because the operation has started in the previous row, and now out\texttt{out} records the value 44 which is the first input to the operation.

  • row 3\texttt{row 3} : The freeIn\texttt{freeIn} column now records the first input 33 of the second operation (for the sake of simplicity, the same multiplication operation is used again), RESET\texttt{RESET} reflects a 11 because a fresh operation has begun in this row, and then out\texttt{out} records the output value 88 of the operation that started in row 1\texttt{row 1}.

  • row 4\texttt{row 4} : Similarly, the freeIn\texttt{freeIn} column records the second input 11 of the operation, RESET\texttt{RESET} reflects a 00 to indicate the current operation has started in the previous row, and then out\texttt{out} records the value 33 which is the first input to the current operation.

The same pattern is followed in the subsequent rows of the execution trace, for the three columns; freeIn\texttt{freeIn}, RESET\texttt{RESET} and out\texttt{out}.

Constraints

In order to express the values of the out\texttt{out} polynomial in terms of the values of freeIn\texttt{freeIn} and RESET\texttt{RESET} per row, we observe the following;

  • Whenever RESET\texttt{RESET} equals 11 (i.e., in every row 2i-1\texttt{row 2i-1}), the next value of the out\texttt{out} polynomial, denoted by out\texttt{out}', equals the value of current freeIn\texttt{freeIn} value. That is,

    out=RESETfreeIn(Eqn. 2) \texttt{out}' = \texttt{RESET} * \texttt{freeIn} \qquad\qquad\qquad\qquad \tag{Eqn. 2}
  • Whenever RESET\texttt{RESET} equals 00 (i.e., in every row 2i\texttt{row 2i}), the next value out\texttt{out}' is the product of the current and the previous values of freeIn\texttt{freeIn}. That is,

    out=freeInrow 2ifreeInrow 2i-1(Eqn. 3) \texttt{out}' = \texttt{freeIn}_{\texttt{row 2i}} * \texttt{freeIn}_{\texttt{row 2i-1}} \quad\quad \tag{Eqn. 3}

    which is the value of the out\texttt{out} polynomial in row 2i+1\texttt{row 2i+1}.

    But, whenever RESET\texttt{RESET} equals 00 (for every row 2i\texttt{row 2i}), we have out=freeInrow 2i-1\texttt{out} = \texttt{freeIn}_{\texttt{row 2i-1}}. Hence Eqn. 3\text{Eqn. 3} can be rewritten as,

    out=freeInout(Eqn. 4) \texttt{out}' = \texttt{freeIn} * \texttt{out} \qquad\qquad\qquad\qquad\quad \tag{Eqn. 4}

    Or equivalently, for every row 2i\texttt{row 2i}, the next output value out\texttt{out}' can be expressed as:

    out=(1RESET)(freeInout)(Eqn. 5) \texttt{out}' = (1 - \texttt{RESET}) (\texttt{freeIn} * \texttt{out})\quad\quad\quad \tag{Eqn. 5}

    Putting Eqn. 2\text{Eqn. 2} and Eqn. 5\text{Eqn. 5} together yields the following constraint:

    out=RESETfreeIn + (1RESET)(freeInout)(Eqn. 6) \texttt{out}' = \texttt{RESET} * \texttt{freeIn}\ +\ (1 - \texttt{RESET}) (\texttt{freeIn} * \texttt{out})\quad \tag{Eqn. 6}

    Therefore, the PIL code for an optimized Multiplier SM can be written as follows,

    namespace Multiplier(2**10);
    
    // Constant Polynomials
    pol constant RESET;
    
    // Committed Polynomials
    pol commit freeIn;
    pol commit out;
    
    // Constraints
    out' = RESET*freeIn + (1-RESET)*(out*freeIn);

    Observe that the RESET\texttt{RESET} polynomial is constant\texttt{constant} because it does not change from one execution to the next. In an actual implementation of the Multiplier program, RESET\texttt{RESET} would be among the preprocessed polynomials.

Edit on GitHub

Last updated on