Composition of proofs
Composition of Proofs refers to using different proving systems, one after the other, so as to generate the final validity proof. In the case of zkEVM, STARK is used as the first proving system, which produces a STARK proof attesting to correctness of a deterministic computation. The main idea with composition is to delegate verification of the STARK proof to a verification circuit . As described in the PIL-STARK section of this document, the basic verification of a STARK proof is performed by a Verifier entity which takes as inputs; the Proof, the Publics, and some other Verifier parameters. In this case, if the Prover can provide a proof , of correct execution of the verification circuit, then it should be sufficient for verifying the original STARK. As shown in the figure below, the Verifier entity just verifies the proof of the STARK verification circuit. The main advantage of this composition is that is smaller and faster to verify than .
Recursion of proofs
Recursion of proofs is carried out in two phases; setup phase and proving phase. Setup phase consists of an alternating set of two sub-processes: converting a STARK proof to a Verifier circuit and converting a Verifier circuit to a STARK proof. Prover phase is responsible for the actual recursive generation of STARK proofs. The STARK Prover uses the required inputs to generate a STARK proof, and this STARK proof, along with the requisite public values, is used as input by the next STARK Prover.Setup phase
This phase takes advantage of the fact that Verifiers are much more efficient than Provers. The design idea is to create a cascade of Verifier circuits, where at each step a lot more efficiently verifiable proof is recursively created. The process therefore consists of an alternating series of two sub-processes; converting a STARK proof into a Verifier circuit, and converting a Verifier circuit into a STARK proof, denoted by S2C and C2S, respectively.
STARK-to-CIRCUIT or S2C Sub-process
Suppose the first STARK, denoted by , is described with the parameters;pil, constants and starkinfo.
is automatically translated into its Verifier circuit, denoted by .
The translation from a STARK to its Verifier circuit, herein dubbed S2C as its shorthand, is performed during the setup phase.
In other words, the R1CS description of the STARK Verifier circuit can be preprocessed prior to the computation of STARK proof.
CIRCOM is used as an intermediate representation language for the description of circuits. More details on how the CIRCOM is utilized is discussed in the Setup S2C section.
CIRCUIT-to-STARK or C2S Sub-process
The circuit definition in the form of R1CS is taken and automatically translated into a new STARK definition. In this C2S sub-process, a circuit Verifier is translated into a STARK proof. That is, a newpil description, new constants and a starkinfo.
This translation, is herein referred to as C2S (short for CIRCUIT-to-STARK).
Following our example, the newly generated STARK is denoted as and it is essentially a PlonKish arithmetization of with some custom gates of the verification circuit.
See the Setup C2S section for more details.
Concluding the setup phase
It is worth mentioning that these recursion steps can be applied as many times as desired, while taking into account the fact that each step will compress the proof, making it more efficient to be verified but at the expense of increased Prover complexity. Finally, we remark that several artifacts for generating each STARK Prover are generated during the setup phase. See the Setup S2C and Setup C2S subsections for more information about these artifacts.Proving phase
The first proof is generated by providing the first STARK Prover with the proper inputs and public values. The output proof is then passed as input to the next STARK Prover, together with public inputs. This process is recursively repeated. In the below figure, it is shown how in essence a chain of recursive STARK Provers work.
Aggregation
In addition to Composition and Recursion, the zkProver architecture also allows for Aggregation while generating the proofs. Aggregation is a type of proof composition in which multiple valid proofs can be collated and proved to be valid by using one proof, called the Aggregated proof. Validating such an Aggregated Proof is equivalent to validating all the collated proofs. The below figure shows an example of aggregation with binary aggregators.