Compiler and Composability in ZKP
On Friday July 15th, we hosted four experts from Polygon Miden, O(1) Labs, Risc0, and Circom to share their insights on ZKP compiler and composability. Here are the popular topics and highlights we picked from the talks.
The recording can be found on our YouTube channel here: https://www.youtube.com/watch?v=zRngElDdUNE. You can join our ZKP discussion Telegram group chat here: https://t.me/+Uh9eaB-LYP84YTgx.
Bobbin Threadbare: Feeding program source code to ZK VMs
Any computations can be represented as circuit computations with signal propagation or machine computations through transition function. ZK Virtual Machine obtains better performance through machine computations.
A regular virtual machine is composed of the initial state, programs, and final state. A zero-knowledge virtual machine has in addition a witness as an input and a generated proof as an output. The witness is known only to the prover and the proof is assumed to be fast to verify.
There are four approaches to provide a program to the VM: public memory, bootloading, codeword commitment, and MAST root.
The Public Memory approach takes in instructions as public inputs and uses a program counter (PC) to compute the instructions in the memory.
Bootloader approach takes in the hash of the program as public inputs and the instructions as the witness. The bootloader in the VM sets the instructions from witness to the memory which inverts the input hash in the VM.
Codeword approach takes the instruction as the witness and stores them in the Read-Only Memory (ROM) to compute the instructions. The instructions are also sent as a codeword commitment to add onto the Merkle tree proof in the output.
MAST stands for Merkelized abstract syntax tree. All programs can be reduced to a single hash as the root of the MAST. Every internal node is a MAST of a smaller program, for example, leaves of a program MAST are linear programs with no control flow. The MAST approach takes the program root as the public inputs and instructions as the witness. The VM uses a decoder to compute the instructions.
Why do we choose one over the other? Each approach has different prover cost, verifier cost, decoding complexity, and program hiding. The pros and cons are shown in the graph.
Brian Retford: Towards a Unified Compilation Framework for Zero Knowledge
Risc0 is a ZK VM that implements the RISC-V instruction set and can run generic programs. For example, we can write a Rust program, compile it in LLVM-IR into an ELF file and load into the RISC-V VM with the public memory model.
Computationally intensive domain specific workloads may be computed via CPUs, GPUs and ASICs. The workload may have a limited core set of operations, and therefore is not generalized. For example, AI workloads mostly have convolutions and matrix multiplications, and ZK workloads have NTTs and elliptic curve operations. The more narrow a computation domain is, the quicker we can transition into GPUs and ASICs. AI has taken a long path to reach ASIC. ZK is still early to reach ASIC, while bitcoin mining has quickly reached ASIC due to its simple set of operations.
The framework approach is not very scalable. It heavily relies on the specific hardware target and could pollute the framework. For example, the first version of Tensorflow could only work with CUDA because it uses CUDA’s memory loading primitives and cannot run on AMD problems well. The problem lies on the software level, and a more generalized and scalable approach is needed.
A potential solution is the compiler approach, which gains popularity among developers over time. The programmer writes in Python or other frameworks and uses a high level script like JAX, PlaidML and Tensorscript. The EDSL resembles a host language and limits the scope of computation so that compilers can lay out the operations on a wide variety of hardwares. The EDSL and compiler approach can let developers write the program once and run anywhere.
ZK computation can also take the framework or the EDSL and compiler approach. For example, the ZPrize competition uses a lot of the same flavor as CUDNN & framework based approach. On the other hand, Leo, Miden, Cirgen, etc. are helping shift towards the compiler approach.
We want to reach “write once run anywhere” with better standard tools. Multi-Level IR (MLIR) turns dense vertical computing space to be approachable via the compilation approach. For example, some large console manufacturers are rumored to have more than 10 custom chips with MLIR based compiler stacks.
Izaak Meckler: Composability and Recursion in SnarkyJS
The goal of a ZK programming system should be easy to learn, develop, easy to integrate with other parts of an application, and performant. In the ZK landscape, we have VM-based systems and circuit-based systems. Within each category, there are ones compiled from new languages, such as Cairo for VM-based systems and Aleo and zinc for circuit-based systems, and from existing languages, such as Risc0 for VM-based systems and SnarkyJS and Arkworks for circuit-based systems.
SnarkyJS builds a framework for writing ZK applications with Typescript and based on its Kimchi SNARK over Pasta curves. It can run easily in the browser and works well with Mina, a Layer 1 chain based on ZK-SNARKs.
SnarkyJS takes advantage of using Typescript as many developers already know it well and it has a solid compiler. The support system for the Typescript development community is also great with toolings. It can also run in the browser out of the box.
Composability separates systems into independent parts and may generally be accomplished through functions and classes. SnarkyJS uses recursion in addition for composability.
Let’s example composability via recursion in detail. Using the game mastermind as an example, the player is guessing the codeword from the code master in rounds. When the game finishes after rounds of guesses and hints, they can commit the game to the chain to finalize the prize. This can be scaled horizontally if there are 10 games that use zk-rollup to compress them into one proof. The batch commit records the games while reducing the gas costs.
The code in Typescript is rather straightforward: the proofs are private inputs and can use “verify” on it to check the state of the game up to the current state.
Composability via recursion is useful towards privacy in a multi-party setting with private data. It also supports scalability to sync the states between systems.
Albert Rubio: Circom 2.0: A Scalable Circuit Compiler
When defining circuits for SNARKs, we start from a computation to an arithmetic circuit and then we use the constraints of the circuit and provide solutions. We send the constraints and witness to the SnarkJS to obtain the prover and verifier. We need a language to define the circuits and a compiler to create the constraints and witness.
Circom fits in the puzzle as the language and compiler. Circom is open source and fully written in Rust. It was mainly developed by Albert’s group at UCM and has a large developer community now.
The aim of a Circom program is to provide a symbolic description of the circuit and provide an efficient way to compute the witness. Circom allows developers to design arithmetic circuits at low level like electronic circuits. All constraints have to be explicitly added by the programmers and may only be simplified by the compiler.
The Circomlib provides implementations of useful circuits including binary transformers and operations, comparators, hash functions (MiMC, Pedersen, sha256), elliptic curves (twisted Edwards, Montgomery), and Sparse Merkle Trees. They may be used as primitive templates and can build up complex computations.
The compiler may generate hundreds of millions of constraints which are excessive to efficiently compute and store. Most zk-SNARK systems have an upper bound of 2²⁷ constraints per system. Luckily, many of the constraints may be eliminated. Circom simplifies the constraints while not modifying the behavior of the circuit.
Circom uses linear constraint simplifications to apply clustering and parallelize the simplification. It is implemented through Gauss-Jordan elimination and the process iterates until no linear constraints are left. This approach can reduce up to 80% of the constraints, which can mean a reduction from 650 million to 130 million constraints.
The simplification is a new form of code optimization. Circom simplification can be applied independently to R1CS produced by other languages and is more powerful than in Zokrates.
We host monthly panel discussions and publish research blogs. If you want to share your ideas, or seek advice, review, or co-publish, feel free to contact us at hello@delendum.xyz.
