zkProverPolygon Labs

Description

zkProver is a STARKShort for "scalable transparent argument of knowledge", a STARK is a type of zero-knowledge proof that resolves one of the primary weaknesses of ZK-SNARKs, its reliance on a "trusted setup”. STARKs also come with much simpler cryptographic assumptions, avoiding the need for elliptic curves, pairings, and the knowledge-of-exponent assumption and instead relying purely on hashes and information theory. This means that they are secure even against attackers with quantum computers. proving system designed to implement the zkEVM component of Polygon zkEVM. It proves the execution of EVM transactions in a zkVMA special type of zk proving system that proves the correctness of state transitions of a virtual machine. Computation is represented by a program in a specific instruction language, it can have private and public inputs and public outputs. Most of zkVMs are STARKs. running on zkASM ISAInstruction Set Architecture of a virutal machine describes its computational model, including the available instructions, registers, data types, etc.. zkProver allows recursive STARK aggregation as well as the final wrap in a Fflonk SNARKShort for "succinct non-interactive argument of knowledge", a SNARK is a widely used type of zero-knowledge proof that is short and fast to verify. Different kinds of SNARKs are usually systematized by proof size, verification time, and type of setup. The most famous SNARKs are Groth16, PLONK/Marlin, Bulletproofs, and STARKs. for efficient onchain verification. zkProver onchain verifierAn entity in a ZK-Rollup, often a smart contract, that verifies zero-knowledge proofs submitted by a prover. targets 128 bits of security.

Proof systemThe infrastructure that allows projects to verify their state transitions. It is composed by onchain verifiers and offchain provers. The main two flavors are optimistic and ZK proof systems, but they can be combined in a hybrid model. In general though, if a system is able to accept state roots optimistically, even if it has a ZK component, it is considered an optimistic proof system.

zkProver toolkit introduces two new domain specific languages: zkASM and PIL. zkASM is the instruction language of the internal zkVM, and the execution of EVM transactions is proven with a specific zkASM program called ROM. PIL is a language for creating circuits, conceptually similar to circom.

zkProver is based on eSTARK paper, meaning that it implements a FRIA proximity test method that is used to determine whether a set of points is mostly on a polynomial with a degree less than a specified value. It resembles the FFT but the arithmetic complexity of its prover is strictly linear and that of the verifier is strictly logarithmic.-based STARK with AIRAlgebraic intermediate representation (AIR) is a type of arithmetization commonly used in zkVMs. It represents a trace of zkVM state transitions with low degree polynomial constraints that enforce the correct relation between previous and current states of the computation. Several variations of AIR are used in practice, with slight differences among them. arithmetizationA part of zk proving system, a process that transforms the computation to be proven into a set of polynomials with particular properties. extended with additional arguments. It also provides tools to automatically generate circom arithmetic circuits for verifying the STARK proof, which plays an essential role in proof compression and recursive proving.

Polynomial Identity Language (PIL)

The polynomial constraints that define circuits within zkProver are specified using a language called polynomial identity language (PIL). PIL supports complicated and powerful polynomial constraints, like permutation, inclusion and connection arguments. PIL was designed to be applicable in other zk tools as well. The next iteration of PIL called PIL2 could be found here.

State machine

zkProver state machine (zkVM) consists of 13 separate state machines specified in PIL, including main SM, arithmetic SM, binary SM, etc. Each state machine creates its own execution trace, which is connected to the rest using connection argument. The state machine has access to EVM state trie, EVM memory and the ROM program that implements verification of EVM transactions in zkASM language.

Recursion circuits

Proving architecture of zkProver consists of several stages. Compression stage reduces the size of STARK proofs of zkEVM batch execution for efficiency of further computations. Normalization stage prepares for aggregation by correctly aligning public inputs across several batches. Aggregation stage repeatedly joins pairs of STARK proofs to produce a single proof of multiple zkEVM batches. Final STARK stage changes the field over which the proof is generated to prepare for the SNARK wrap. Finally, SNARK stage produces a Fflonk proof to be posted onchain.

Each recursion step uses a circom R1CS arithmetic circuitA computation model often used in ZK-SNARKs, represents a sequential application of + and * to initial inputs and some intermediate computational results to get a single numerical outcome. to verify input PIL-STARK proofs (see here). The proof of verification is a PIL-STARK that is generated on the Plonkish arithmetization of this circom circuitA program written for the purpose of being proven within a proving system. A circuit is a mathematical representation of the computation to be executed, arithmetic circuits and zkVM execution trace are examples of circuits. Circuits can be written in different languages, ranging from low-level to high-level..