In this continuation of our series on zkMIPS, we explore the specific proving process that verifies the correct execution of MIPS programs off-chain. Here, we cover the structured steps involved in segmenting the program, the modular proof structure, and the cryptographic proofs employed.
Without getting into the complex details of input standards, the initial step involves compiling the original program, which is potentially written in various high-level languages, into MIPS assembly code. This standardizes the input for subsequent segmentation and modular processing, tailored specifically for the zkMIPS architecture. Following the compilation, zkMIPS divides the MIPS program into segments, thereby simplifying the complex proving tasks and allowing for parallel processing. Each segment is further subdivided into four module tables that categorize the instructions. This organization isolates and independently verifies different types of operations.
Within these module tables, zkMIPS utilizes STARK proofs to independently confirm that each instruction is executed correctly, adhering to the program's logic. The core of the process involves encoding verification steps and program values as polynomials - specifically, constraint polynomials for the verification steps and witness polynomials for the program values. The entire algorithm execution is expressed as a single polynomial through a thoughtful composition of these polynomials. The validity of this composed polynomial is assessed using the FRI protocol, which checks whether the polynomial has the appropriate degree. A structured evaluation using FRI ensure that the program's execution is correct , matching the witness and constraint polynomials effectively.
Following this modular proving, the architecture utilizes a sophisticated cross lookup scheme to ensure that all instructions of a segment are correctly accounted for within its module tables, validating the structural integrity of each segment's proof. The chosen lookup scheme is the logUp protocol, written as a STARK. Furthermore, the lookup enhances the system’s ability to manage and verify complex operations that are not directly polynomial in nature (such as logic operations), facilitating the implementation of proofs for different operational types. The correct sequence of segments is recursively verified using a PLONK proof, ensuring that the overall program execution matches the intended logic and sequence. This step confirms the continuity and sequential integrity of the program.
To enhance on-chain verifiability, particularly for platforms like Ethereum, a final Groth16 proof is optionally generated. This proof system optimizes the proofs to ensure they are compatible and efficient for blockchain integration.
The proof steps are all implemented using the Plonky2 library, which is designed to write both STARK and PLONK proofs efficiently.
