zkMIPS: Step by Step

Proofs of Knowledge in Verifiable Computation

Proofs of knowledge in verifiable computation involve a Prover that performs a computation and produces a proof to show this computation was correctly executed, both of which are sent to the Verifier.

The proof should be short or “succinct” so that the Verifier has minimal work to do. This is however at the cost of putting the burden on the Prover.

Proofs of knowledge within blockchains are 1) succinct 2) non-interactive (between the Prover and Verifier) 3) ZK (this is optional). Common computational problems that are usually proven are [3]:

  1. Transition functions for L2s – as seen in zkRollups.

  2. The execution of smart contracts – as seen in zkEVMs. Smart contracts are typically written in Solidity and the EVM verifies the execution of the contract.

  3. The execution of off-chain programs – as seen in zkVMs. In ZKM’s case, an off-chain MIPS program is given and zkMIPS verifies the execution of that program on-chain.

zkMIPS in Verifiable Computation

zkMIPS verifies the correctness of the execution of a MIPS program in the form of a proof. This is equivalent to the sequence of overall CPU states that represent a program’s execution.

In zkMIPS, the computational problem that we want to verify is the program. The solution comes in the form of an execution trace.

An execution trace is a complete record of the computation executed from running the program. The execution trace is commonly represented through a trace record, where each column is a list representing the states of a fixed CPU variable and the rows showing each step of the computation [1].

The program is verified by checking whether each row of the execution trace matches the respective instruction of a program.

A solution to this is to simply rerun the program. The problem is that this is not succinct. Similar to what we’ve discussed with the trivial proofs in proofs of knowledge, the state sequences would be too large for the smart contract to verify [2].

Techniques For Succinct zkMIPS Proving

The following sections describe techniques that zkMIPS uses for improving the succinctness during the proof generation process. This includes arithmetization, FRI, method continuation, lookups and polynomial commitments.

More details can be found in “Getting to Know zkMIPS Proving Architecture” written by ZKM Researcher Lucas Fraga and the zkMIPS whitepaper written by the ZKM research team.

How can we complete the verification of a MIPS program more efficiently?

With succinct proofs, we can verify a program in a time that is polynomial on the logarithm of the size of the program. For example, a program of size n can be verified in around a time that is polynomial on log(n).

To enable greater succinctness, zkMIPS uses 2 main methods:

  1. Compressing the number of verification steps

  2. Moving the verification complexity from the Verifier to the Prover (hence there is a sophisticated Prover and a simple Verifier).

Arithmetization

In moving the verification complexity to the Prover, we can use polynomials. Using arithmetization, we can represent the entire trace record as a single polynomial.

The constraints (verification steps) and witnesses (the values in each step) can be encoded as polynomials. The constraint and witness polynomials can be combined together to form a single composition polynomial.

In the above diagram, the MIPS instructions and registers are encoded as polynomials. Constraints are applied in each row of the trace table. Each row is then converted into a constraint polynomial.

We can now:

  1. Combine the different steps of the program and compress them

  2. Combine the constraint and witness polynomials into a single function where the result should still be a polynomial if the constraint and witness polynomials match.

The program is verified through polynomial evaluations on the composition polynomial. What specific evaluations should be performed on the composition polynomial?

FRI Protocol

The FRI protocol is one such method for determining this, specifically used to verify whether the composition polynomial has a proper degree.

The way the composition polynomial is defined guarantees that, if it is indeed a polynomial, the witness and constraints must match, and the program and its execution trace as a result are compatible. This is sufficient enough to verify the program.

There are, however, problems to creating a composition polynomial for the entire program:

  1. The polynomial input to FRI can be as large as the MIPS program

  2. FRI proofs are heavily based on hash functions, which are expensive to compute on-chain

Using FRI alone is not succinct enough for on-chain verification.

Lookup Protocols

A lookup protocol shows that a target table is contained in a reference table, i.e., that the segment is contained in the modular tables.

The lookup protocol, if successful, shows that every entry in the original set of internal CPU states appears in the table of one of the operation groups. The lookup proof will be equivalent to the FRI-based continuation proof.

Lookups are used because:

  1. They are another technique to improve succinct proving by decreasing the proof size

  2. Some operations (e.g., logic operations) cannot easily be expressed as polynomials

Different tables are created for different types of operations and table lookups are used to show the original segment table corresponds to the smaller operation tables proved with FRI. Different programs will also produce different tables. The entries of the tables and lookups into the tables are encoded as polynomials.

In zkMIPS, the segment polynomials are broken down into four main modular tables: arithmetic, logic, memory and control. FRI is used to prove each operation group in parallel and joins them together in a lookup protocol.

There are two types of tables used:

  • Target table – a table representing the entire segment

  • Reference table – a table combining all four modular tables

Continuation

To counter the computational expense of creating a single composition polynomial, method continuation can be used by breaking down the witness and constraint polynomials into pieces.

This process includes:

  1. Dividing the program into smaller segments

  2. Proving each of the segments in parallel

  3. Running the FRI protocol for each segment

  4. Combining all segments proofs to get a program proof

We will end up with one FRI proof for each segment. The continuation protocol will show that the FRI proofs continue onto one another, which is done recursively until there is one single continuation proof. The final proof will be around the size of one segment proof and is sufficient enough to prove the correctness of the entire program.

Because the resulting continuation proof is FRI-based, it is not adequate for on-chain computation. We can further improve the succinctness by using lookups.

Polynomial Commitments

Polynomial commitments are used to further decrease the overall final proof size and proving time by adjusting the FRI-produced proofs.

Using polynomial commitments, larger proofs can be produced faster and smaller proofs can be produced slower. The last continuation proof uses slow and small commitments (to decrease the final proof size) before being converted into Groth16. The other FRI-based phases use fast and large commitments.

Another note about polynomial commitments: zkMIPS uses Merkle trees to commit to all possible evaluations of certain polynomials in a given domain. The Verifier can use the Merkle root to query the polynomial evaluation from the Prover [1] and check certain polynomial properties using the queried values.

zkMIPS Step-by-Step Process

Proof Generation & Verification with zkMIPS – Step-By-Step Overview

zkMIPS is ZKM’s general-purpose zkVM verifying on-chain that a MIPS program was correctly executed off-chain. zkMIPS is based on MIPS32 microarchitecture.

zkMIPS is composed of: a sophisticated prover, a simple verifier and an equivalent verifier smart contract [2].

Components:

  • MIPS Compiler

  • ELF Loader

  • MIPS VM

  • Prover

  • Verifier Contract

Steps I-III describe program execution in zkMIPS.

Steps IV 1-6 describe the proof generation in zkMIPS.

Step V describes the proof verification in zkMIPS.

  1. MIPS Compiler

A program written in Go or Rust is compiled into a MIPS ELF binary file using the MIPS Compiler. The ELF file is the executable format for the MIPS instruction set.

  1. ELF Loader

The MIPS ELF binary file is loaded into the MIPS VM using the ELF Loader.

  1. MIPS VM

The MIPS VM runs the program and generates an execution trace for the Prover.

Any high-level language can compile down to MIPS. We get a sequence of the MIPS instructions as a result.

For example for row i, the described data operation is addition. In the instruction, the value in register 5 (13) is added to the value in register 6 (21). The result of the computation is stored in register 7 (34). For row i+1, the described data operation is addition (using an immediate operand). In the instruction, the value in register 5 (21) moves to register 6.

After each instruction is executed (left side table), we will get a value for each register. After going through all the instructions, we will get the trace table (right side table).

  1. Prover

The Prover executes the MIPS program and uses the execution trace to generate a proof.

As part of the Prover, the following are steps in the proof generation process:

  1. The program and trace are divided into segments.

After getting the trace table, the first step of continuation can be applied by splitting the table into segments. Segments are small sequential executions from the program execution.

  1. The segments are divided into modules. The instructions of each segment are divided into groups of four module tables: arithmetic, logic, memory and control.

Modules are smaller non-sequential executions from the segments.

Each instruction, depending on the category it falls under, will be divided into its corresponding table. For example, instructions with the add operation (rows i - i+3) are placed in the arithmetic table.

  1. STARK – The modules are proven independently and in parallel with FRI. These proofs are FRI-based modular proofs.

Each module execution that combines all segment instructions is independently proved using STARK proofs. In this layer, arithmetic, memory, logic and control proofs are generated. Traces proved in this layer are referred to as module traces.

  1. LogUp (STARK) – The modular proofs from the previous step are combined into one single proof for each segment using the LogUp lookup protocol. These segment proofs are LogUp proofs written using Starky.

LogUp is the lookup scheme used by zkMIPS to prove that the program instructions were correctly verified in their own specific modules.

Traces proved in this layer are referred to as segment traces. Segment proofs can be produced before module proofs, and as a result, this layer can run in parallel with the previously described layer [1].

  1. PLONK – All segment proofs from the previous layer are recursively combined using the continuation protocol into one single continuation proof. This proves the correctness of the entire program trace. The continuation proofs are written using Plonky.

  2. Groth16 – The Groth16 proving system is used to enable on-chain computation by converting the proof to an EVM-friendly format. The continuation proof is converted into an on-chain Groth16 (SNARK-based) proof.

This enables the final proof to be verified on L1. Groth16 uses bilinear functions over elliptic curves that are natively implemented in EVM which also enables zkMIPS to verify the proof faster on-chain.

The final proof is the zkMIPS proof representing the proof of the correct execution of the program.

  1. Verifier Contract

After generating the zkMIPS proof, the verifier contract verifies the proof on-chain.

zkMIPS implements a Plonky2 verifier in Gnark for the proof verification.

High Level Overview

The following is a high-level overview of the interactions involved:

  1. End User Action – the end user wants to prove the correct execution of a program. Some examples include proving the correctness of blockchain transactions, validating new rollup states, verifying smart contract function calls, etc.

  2. Program Execution – the program runs in zkMIPS’ execution environment.

  3. Proof Generation – a proof for the program’s correct execution is generated by zkMIPS and can be outsourced to ZKM’s Prover Service.

  4. Proof Verification – once the zkMIPS proof is generated, a verifier contract will be run on a destination chain to verify the proof.

  5. Settlement – in the case of proving the correctness of blockchain transactions, once the proof is verified on-chain, the transaction is considered to be settled.

Example – Asset Transfer with Entangled Rollups

The L2s in the Universal L2 structure serve as interoperability mechanisms to facilitate cross-chain transfers without the implementation of a bridge.

In this example, 100 USDT is sent from the source chain (ETH L1) to the destination chain (AVA L1). A proof that the 100 USDT was burned on the L2 (ETH UL2) is generated off-chain. The proof is verified by a verification contract on the destination chain. Once verified, the user will receive 100 USDT on AVA L1.

Last updated