A Brief Taxonomy of Circuit Compilation Strategies

Oct 12th, 2022
Christopher Goes

Thanks to Bobbin Threadbare, Alex Ozdemir, Daniel Lubarov, and Ventali Tan for helpful suggestions. This article is based on the talk given by Christopher Goes at Delendum ZKP Panel Series (direct link).

Table of Content

Motivation Question

The motivating question in defensive ZKP compiler pipeline design is:

If most general-purpose applications of ZKPs will require general-purpose programmable privacy, what compiler stack can allow developers to safely write programs and also produce efficient outputs?

This is the motivating question simply because the things that are many are the programs. Eventually, we’ll have a few proof systems and maybe a few different compiler stacks and those might have some bugs and we’ll need to iron out those bugs and formally verify those parts - but the proof systems and compiler stacks will be relatively small in number compared to the actual programs.

Consider comparable examples, such as the Ethereum Virtual Machine (EVM) and the Solidity compiler. Early on in the history of the EVM and Solidity, the EVM and the Solidity compiler both had a lot of bugs, and often, bugs in programs were if not equally likely then at least non-trivially likely to be due to a bug in the compiler or in the EVM as opposed to a bug in the program caused by a developer not thinking about their model or writing the Solidity code correctly. But, over time, as the EVM and Solidity “solidified” and became better understood and more formally modeled in different ways, the frequency of those bugs has declined, in the case of the EVM perhaps to zero and in the case of Solidity to a very low number and to mostly minor ones. Now most of the problems, if you go on Rekt, most bugs nowadays are not bugs in the Solidity compiler or bugs in the EVM but rather bugs in code written by developers - sometimes mistakes caused by the model of the program itself being unclear or wrong (with respect to what the developer probably intended), sometimes mistakes in the use of the Solidity language to express that model, but in both cases the result of an incongruity at the developer level. If you’re interested in preventing bugs, you have to focus on this layer because most of the bugs are written by developers.

This holds doubly so for programs involving zero-knowledge proof systems (ZKPs) and privacy, because most developers aren’t going to be intricately familiar with the implementation details of zero-knowledge proof systems, and if the compilation stack requires that they understand these details in order to write programs safely, their programs are going to have a lot of bugs. It’s really hard to understand cryptography, especially if you don’t have a deep background in it and especially if you’re writing a complex application at the same time. Of course, if you have a very safe compiler stack but it’s not fast enough and the performance costs are too high for actual applications, no one will be any safer because no one will use it. So, the question can be rephrased a wee bit: what compiler stacks can provide the most protection to developers, while also being efficient enough that they will actually be used?

General Constraints

There are some different constraints in circuit / ZKP compiler design than in the design of ordinary compilers. For one, there are some very specific “threshold latency constraints”, where execution times under a few seconds will be fine but execution times over that will render many applications impossible. In most cases, at least if you want privacy, users have to be creating the proofs, and when users are creating the proofs there’s a really big user experience difference between 3 seconds latency and 9 seconds latency, even though this is only a constant factor of 3.

With normal compilers, you might be able to tolerate such small factor differences in the interest of making it easier to write programs (see: Javascript) - if you’re running a spreadsheet tax calculation program, for example, a difference of a factor of 3 may not actually matter that much - the person would just do something else while the program is running as long as they aren’t running it too frequently. With normal compilers you also tend to care about user interaction latency, which has deep implications in compiler design. For example, it means that languages with automatic memory management tend to do incremental garbage collection, which limits garbage collector latency, as opposed to simpler garbage collection algorithms which can cause unpredictable latency spikes. This doesn’t apply when writing circuits to be used in ZKP systems, because all of the interactions are non-interactive with respect to one individual program - the compiler should instead optimize for making the total prover execution time as low as possible.

Another class of parties who could potentially write bugs are the circuit compiler developers - us! - so it behooves the ecosystem to come up with at least some reusable complements of the compiler stack that can be shared by multiple parties and jointly verified. To that end, the subsequent parts of this post craft a high-level taxonomy of current approaches to circuit compilation and describe their trade-offs.

This taxonomy categorizes compilation approaches in three broad classes, which are defined and analyzed in order:

  1. DSL approach
  2. ISA/VM approach
  3. Direct approach

DSL Approach

The first approach and the approach that quite logically the ecosystem started with is herein termed the “DSL approach”. DSL stands for “domain-specific language”, and the DSL approach is to take something like R1CS or PLONK or AIR and build a language on top of it, crafting abstractions iteratively in order to simplify the job of the programmer. DSL instructions in this sort of a system typically act like constraint-writing macros - some variables can be tracked, there’s some sort of simplified compilation going on, but there’s no intermediate instruction set or abstract machine, and instructions in the DSL translate pretty directly to constraints. Examples of this approach include:

Note that Noir is backend-agnostic. It compiles down to an abstract IR which can then be compiled down to R1CS or Plonkish languages. Likewise, Leo does compile to an IR, called Aleo Instructions, which is an assembly-language-like language that you can use directly for fine-grained control of the constraints.

While these languages are quite different, written with different syntaxes and targeting different proof systems, they are all following the same kind of general approach of starting with a low-level constraint system and iteratively adding abstractions on top.

Advantages of the DSL approach:

Disadvantages of the DSL approach:

One challenge of the DSL approach is that each DSL needs a compiler. Such compilers are hard to build. The burden of building a new compiler from scratch just to test out a new idea for a DSL makes it infeasible to explore a large number of DSL designs.

One idea to decrease the cost of building such compilers is to design compiler infrastructure for compiling to circuits. The infrastructure can implement common optimizations, transformation algorithms, and abstractions. These are provided as a library that makes it easy to build new compilers. CirC is a compiler infrastructure for existentially quantified circuits, which capture the computation model of ZKP/MPC/FHE/SMT/ILP.

ISA/VM Approach

The next compilation approach is termed ISA (instruction set architecture) / VM (virtual machine) compilation. This approach is more involved. ISA/VM compilation requires clearly defining an intermediate virtual machine and instruction set architecture which then intermediates in the compilation pipeline between the high-level languages in which developers are writing programs and the low-level zero-knowledge proof systems with which proofs are being made. Although it is possible to write VM instructions directly, in this approach it is generally assumed that developers won’t (and these VMs are not optimized for developer ergonomics).

This can be done with an existing instruction set. For example, the Risc0 team has done this with the RISC-V microarchitecture - originally designed for CPUs with no thought given to ZKP systems - but Risc0 has written a STARK prover and verifier for RISC-V which is compatible with the existing specification of the RISC-V ISA.

This can also be done with a custom-built VM and instruction set designed specifically to be efficient for a particular proof system, and potentially for recursive verification in the VM or some other specific application you might want to support efficiently. For example, the Cairo VM and the Miden VM are designed to be more efficient to prove and verify in a STARK than an architecture such as RISC-V (which was not designed for this) might be, and the Triton VM has been designed specifically to make recursive proof verification in the VM relatively inexpensive.

All of these approaches use one circuit for all programs, and support many higher-level languages - the higher-level languages just need to compile to the specified instruction set - and most of these examples are von Neumann architecture-style machines - so there’s a stack, operations on the stack, some form of memory, storage, I/O, and maybe some co-processors or built-in operations. Note that RISC-V, Cairo are not stack machines (RISK-V is a register machine and Cairo is a memory machine), and Miden VM is not von Neumann architecture.

Advantages of the ISA/VM approach:

Disadvantages of the ISA/VM approach:

Direct Approach

The third approach, for lack of a better word, is just referred to here as direct. The basic idea here is to somehow directly compile higher-level programs to circuits. These higher-level programs could be functional, based on the lambda calculus, or some kind of imperative language, but the direct approach involves transforming this high-level language directly to a circuit without an intermediate instruction set.

The best candidate for this sort of translation, at least for functional languages, is based on a paper called “Compiling to Categories” by Conal Elliot, which works by taking the kind of simple lambda calculus core that you can translate a functional language to, translating the semantics of lambda calculus operations to the semantics of a category, translating the categorical semantics into the category of polynomial operations, then translating the polynomial operations into a specific circuit. You can find a more detailed description in the GEB project repository here.

Similar to the DSL approach, with the direct approach each program generates a unique circuit. Other kinds of direct compilation may be possible - arguably, there’s a sort of continuum of DSLs where they approach higher and higher-level semantics and get more and more like this kind of direct compilation.

Advantages of direct compilation:

Disadvantages of direct compilation:


So many compiler options! It’s all a little exhausting - and prompts the question: what might be expected to happen, and where, accordingly, can efforts best be spent right now?

The three approaches outlined here have different trade-offs, particularly in terms of potential performance, low-level control, degree of abstraction, and difficulty of creating appropriate tooling. Due to these trade-offs, we’re likely to see a hybridization of approaches, where critical functions and gadgets (e.g. hash functions, Merkle proof verification, signature checks, recursive verification, other cryptography) are written directly in lower-level DSLs (1) or even in raw constraints, but these will be provided in standard libraries and then tied together with “business logic” written by developers in a higher-level language compiled using either the ISA/VM (2) or direct compilation (3) approaches.

Hybridization is likely because it gives you the best of both worlds - you can spend your “optimisation time” (the time of people writing hand-optimized circuits) on the critical “hot spots” of your code which really need to be optimized and whose performance mostly determines the overall performance of your program, and use a less efficient but more general compilation pipeline for custom per-program “business logic” written by regular developers.

This is also similar to the structure of cryptographic systems today - if you look at how people implement cryptographic protocols, there’s usually hardware support (after standardization) for specific optimized primitives (hash functions, encryption algorithms), which are tied together in protocols themselves written in higher-level languages which are easier to develop in and reason about.

Finally, a minor exhortation: agreement on and convergence to specific standard primitives and intermediate interfaces can help facilitate deduplication of work across the ecosystem and an easier learning environment for developers. A good example of a moderately successful standardization effort in the space already is the IBC protocol, which is now being adopted by many different chains and ecosystems.

For zero-knowledge related standards effort, zkInterface is a standard tool for zero-knowledge interoperability between different ZK DSLs, gadget libraries, and proving systems. Anoma is trying to help a little bit in this direction with VampIR proof-system-agnostic intermediate polynomial representation, Delendum is also exploring practical approaches for composition and conversion across different proving systems — and we’d be very happy to collaborate or learn about other standards efforts.

If you are interested in working together on this subject, please consider applying to our fellowship program. If you’re interested in further discussions on this topic, please consider joining our group chat or reach out to us at research@delendum.xyz.