Pil Stark

Simply put, PIL-STARK is a special STARK that enables:

• The state machine prover (SM-prover) to generate STARK proofs for any state machine written in PIL.
• The state machine verifier (SM-verifier) to verify STARK proofs generated by the prover.

Hence there is a PIL-STARK component in the SM-prover which is the generator of a STARK proof, and another PIL-STARK component in the SM-verifier which is the actual verifier of the STARK proof.

Since the SM-prover and the SM-verifier, who are separate and independent entities, require certain PIL-STARK parameters prior to proving and verification, the system needs some preprocessing phase. Call this phase, the setup phase.

The PIL-STARK proof-verification process therefore consists of three (3) phases, the setup, the proving, and the verification. These are outlined below.

PIL-STARK setup phase

The setup phase can be considered to have three 'components', the $\texttt{PILCOM}$, the setup $\texttt{executor}$ and the $\texttt{PIL-STARK setup}$.

Compilation with PILCOM

As part of PIL-STARK's preprocessing phase, a novel PIL compiler, called $\texttt{PILCOM}$, is used for compiling a $\texttt{.pil}$ file into a parsed $\texttt{.json}$ file.

The compilation of the $\texttt{.pil}$ file into a parsed $\texttt{.json}$ file is the first step in this phase of the PIL-STARK proof-verification process.

Setup executor

The $\texttt{setup executor}$ takes as input the PIL $\texttt{.json}$ file from $\texttt{PILCOM}$ and computes evaluations of the state machine's constant polynomials. For each state machine, described by the $\texttt{.pil}$ file compiled with $\texttt{PILCOM}$, the execution process is carried out only once.

PIL-STARK setup

The PIL-STARK setup takes the PIL $\texttt{.json}$ file from $\texttt{PILCOM}$, the evaluations of the constant polynomials from the $\texttt{setup}$ $\texttt{executor}$, and the STARK configuration information in the form of a $\texttt{starkstruct.json}$ file as inputs. It then creates a Merkle tree with the evaluations of all the constant polynomials, called the $\texttt{constTree}$

It outputs PIL-STARK parameters; the $\texttt{constTree}$ which is a Merkle tree of evaluations of the constant polynomials, the $\texttt{starkInfo}$ which is a STARK-specific information, and the $\texttt{constRoot}$ which is the root of the $\texttt{constTree}$.

Overall, the setup phase of PIL-STARK takes the $\texttt{.pil}$ file describing the state machine and STARK-specific parameters as inputs. Its outputs are the evaluations of the constant polynomials, the $\texttt{constTree}$, the $\texttt{starkInfo}$, the $\texttt{constRoot}$, as well as the PIL $\texttt{.json}$ file from $\texttt{PILCOM}$.

We emphasise that the setup phase of PIL-STARK is run only once for a particular $\texttt{.pil}$ file describing the state machine. A change in the $\texttt{.pil}$ file means a fresh setup needs to be executed.

PIL-STARK proving phase

The proving phase consists of two main components:

• the $\texttt{SM-prover}$ $\texttt{executor}$.
• the PIL-STARK proof $\texttt{Generator}$.

SM-prover's executor

The executor in the SM-prover's takes as inputs; the PIL $\texttt{.json}$ file from $\texttt{PILCOM}$ and another $\texttt{.json}$ file of inputs, called $\texttt{input.json}$ . In the case of our mFibonacci SM, the inputs in $\texttt{input.json}$ includes the initial values of the registries $\texttt{A}$ and $\texttt{B}$.

The SM-prover's executor builds the values of polynomials that are to be committed. Its output is the evaluations of the committed polynomials, per proof. These evaluations of committed polynomials are actually the SM's execution trace.

Note that the input values in the $\texttt{input.json}$ file can be varied without altering the actual state machine. The reason the state machine remains intact is due to fact that the $\texttt{.pil}$ file, that was initially compiled in the setup phase, is not affected by any change in the input values of the SM-prover's executor.

However, with every set of inputs, the SM-prover's executor computes corresponding evaluations of the committed polynomials to be used in generating the respective STARK proof. In other words, each new set of inputs determines a new set of evaluations, which in turn determines the STARK proof generated by the PIL-STARK Generator.

PIL-STARK proof generator

This STARK Proof Generator takes the evaluations of the committed polynomials from the SM-prover's executor, the evaluations of the constant polynomials from the setup phase, together with the $\texttt{constTree}$ and the $\texttt{starkInfo}$ as inputs.

This is where the evaluations of the committed polynomials, from the SM-prover's executor, are Merkelized. And all elements of the ultimate STARK proof are generated, these include; the witness and the required openings of the committed polynomials.

The output of the STARK Proof Generator is a $\texttt{STARK}$ $\texttt{proof}$ and the $\texttt{publics}$, which are values to be publicised.

For the PIL-STARK proving phase as a whole, also as depicted in Figure 9 below:

• there are five (5) inputs; the $\texttt{input.json}$ file, the PIL $\texttt{.json}$ file from $\texttt{PILCOM}$, the evaluations of the constant polynomials from the setup phase, as well as the $\texttt{constTree}$ and the $\texttt{starkInfo}$.
• and there are two (2) outputs; a $\texttt{STARK}$ $\texttt{proof}$ and the $\texttt{publics}$.

PIL-STARK verification phase

The verification phase is constituted by the PIL-STARK verifier.

As it is common practice amongst zero-knowledge proof-verification systems, the size of the verifier's inputs is very small compared to that of the prover's inputs. For example, while the proving phase takes the whole $\texttt{constTree}$ as one of its inputs, the verifier takes the $\texttt{constRoot}$ instead.

The $\texttt{STARK}$ $\texttt{proof}$ and the $\texttt{publics}$ from the prover, together with the $\texttt{starkInfo}$ and the $\texttt{constRoot}$ from the setup phase are the inputs for the verifier.

And the verifier's output is either an $\texttt{Accept}$ if the proof is accepted, or a $\texttt{Reject}$ if the proof is rejected.

PIL-STARK is, all-in-all, a specific implementation of a STARK that can be used as a generic tool for proving state machines' polynomial identities.

The actual implementation of PIL-STARK uses recursion. That is, hundreds of STARK proofs are proved with another STARK proof, and these STARK proofs of other STARK proofs are also proved with a single STARK proof. This achieves exponential scalability than it would otherwise be possible.

The code for implementing PIL-STARK is found in the zkEVM repository here.