Inclusion arguments

For most of the programs used in the zkEVM’s Prover, the values recorded in the columns of execution traces are field elements. In many cases, there may be a need to restrict the sizes of these values to only a certain number of bits. For example the variate with uint32 type, needs restricting the range from 0 to $2^{32}-1$. It is therefore necessary to devise a good control strategy for handling both underflows and overflows. This document introduces the addition of 2-byte numbers as the scene using Inclusion arguments.

Verify addition of 2-byte numbers

The addition of uint16 type is a common data type in programming. It can be constrained as the below trace table:

The constraint is: $$\mathrm{a}+\mathrm{b}+(1-\mathrm{RESET})\cdot \mathrm{prevCarry}=\mathrm{carry}\cdot 2^8+\mathrm{add}$$ We use $\mathrm{prevCarry}$ as the carry in and $\mathrm{Carry}$ as the carry out. becasue the lowest endian byte of uint16 not use $\mathrm{prevCarry}$, we use $\mathrm{Reset}$ as the flag of the lowest endian byte.

The snippet of PIL code as follows:

namespace TwoByteAdd(%N);

pol constant RESET;
pol commit a, b;
pol commit carry , prevCarry , add;

prevCarry ' = carry;
a + b + (1-RESET)*prevCarry = carry*2**8 + add;

The above equation (1) only constrains the coerectness of addition, but not constrains the columns of $\mathrm{a}$ , $\mathrm{b}$ is 8-bits integer which range form 0 to 255. It also not constrains the columns of $\mathrm{prevCarry}$, $\mathrm{Carry}$, $\mathrm{Reset}$ is 1-bit bool type.

An inclusion argument is used for this purpose.

Inclusion argument

Given two vectors, $(\mathrm{a}=(a_1,...,a_n)\in {\mathbb{F}}_p^n)$ and $\mathrm{b}=(b_1,...,b_m)\in {\mathbb{F}}_p^m$, it is said that:

$\mathrm{a}$ is contained in $\mathrm{b}$ if $\forall i\in [n],\exists j\in [m]$ such that ${\mathrm{a}}_i={\mathrm{b}}_j$.

In other words, if one thinks of $\mathrm{a}$ and $\mathrm{b}$ as multisets and reduce them to sets (by removing the multiplicity), then $\mathrm{a}$ is contained in $\mathrm{b}$ if $\mathrm{a}$ is a subset of $\mathrm{b}$.

A protocol ($\mathcal{P}$,$\mathcal{V}$) is an inclusion argument if the protocol can be used by $\mathcal{P}$ to prove to $\mathcal{V}$ that one vector is contained in another vector.

In the PIL context, the implemented inclusion argument is the same as the Plookup method provided in GW20, also discussed here

An inclusion argument is invoked in PIL with the in keyword.

Specifically, given two columns $\mathrm{a}$ and $\mathrm{b}$, we can declare an inclusion argument between them using the syntax: {$\mathrm{a}$} in {$\mathrm{b}$}.

Generalized inclusion arguments

In PIL we can also write inclusion arguments not only over single columns but over multiple columns. That is, given two subsets of committed columns ${\mathrm{a}}_1,\cdots ,{\mathrm{a}}_m$ and ${\mathrm{b}}_1,\cdots ,{\mathrm{b}}_m$ of some program(s) we can write as,

{${\mathrm{a}}_1,\cdots ,{\mathrm{a}}_{\mathrm{m}}$} in {${\mathrm{b}}_1,\cdots ,{\mathrm{b}}_{\mathrm{m}}$}

A natural application for this generalization shows that a set of columns that a program repeatedly computes, probably with the same pair of inputs/outputs. Following on with the previous “2-byte addition” program example, one can construct five new constant polynomials; BYTE_A, BYTE_B, BIT_PRECARRY,BIT_CARRY and BYTE_ADD; containing all possible byte additions.

The execution trace of these polynomials can be constructed as follows, the total number of rows is $2^8\cdot 2^8\cdot 2$ = 131072:

Recall that there is no need to enforce constraints between these polynomials since they are constant and therefore, publicly known. An inclusion argument can be utilized and thus ensure a sound description of the “2-byte addition” program. The inclusion constraint is not only ensuring that all the values are single bytes, but also that the addition is correctly computed. The input is combination of five variables : BYTE_A, BYTE_B, BIT_PRECARRY,BIT_CARRY and BYTE_ADD and it must be found in the lookup table.

In addition, recall that we only have to take into account prevCarry whenever Reset is 0. PIL is flexible enough to consider this kind of situation involving Plookups. To introduce this requirement, the inclusion check can be implemented as follows:

include "config.pil"; 

namespace TwoByteAdd(%N);

pol constant BYTE_A, BYTE_B, BYTE_PREVCARRY, BYTE_CARRY , BYTE_ADD; 
pol constant RESET;
pol commit a, b;
pol commit carry, prevCarry, add;

prevCarry' = carry;

{a, b, (1 - RESET)*prevCarry, carry, add} in {BYTE_A, BYTE_B, BYTE_PREVCARRY, BYTE_CARRY, BYTE_ADD};