TL;DR
Cairo is the first production-grade platform for generating STARK proofs for general computation. It is Turing Complete, and highly efficient. Everything we’ve been building — starting with our Reddit Bake-off submission — is written in Cairo, including all our upcoming deployments: DeversiFi, Immutable, and dYdX.
Whatever your computation and storage needs are, if you want massive scale at low gas cost on Ethereum, Cairo can be of use. Over the coming quarters we’ll start offering Cairo developer tools; till then we invite you to come talk to us about building your application together.
Background
The Great Reddit Scaling Bake-off was a significant milestone for us at StarkWare. Not so much because of what we achieved — 300,000 transactions in a single STARK proof — but rather because of how we achieved it. The Reddit Bake-off was the first time we deployed Cairo, our production-grade Turing-complete¹ platform for producing STARK proofs for general computation, to Ethereum Mainnet. Our upcoming Mainnet deployments will all be Cairo-based, including:
- StarkEx 2.0 for DeversiFi (spot trading)
- The StarkEx system powering ImmutableX, the Non-Fungible Token (NFT) trading system for Immutable/Gods Unchained
- The StarkEx system for dYdX’s Perpetual Contracts
This post: (i) explains the need for Cairo, (ii) describes its novelty, capabilities and scaling efficiency and (iii) discusses the next steps on our roadmap for sharing the Cairo toolchain with the developer community.
The Need: Production-Grade Turing-Complete STARKs
We’ve focused on solving scaling problems since our incorporation in 2018, starting with Ethereum’s. We realized early on that Validity Proofs are a powerful scaling solution, and that STARKs are uniquely positioned to solve scalability for general computation. Recall the general concept: an off-chain Prover which processes large computations (like large batches of transactions), and produces exponentially smaller validity proofs, which are in turn verified on-chain.
Each of our partners has a unique computation that they need to offload to Layer-2 (L-2). DeversiFi supports spot trading. Immutable supports minting and trading of NFTs, and dYdX executes about Perpetual Contracts. Creating a custom “hand-written” STARK system² for each such project would be time consuming, much like building a dedicated “ASIC” for each computation. Thus, it was clear to us that to scale our business and to support high feature velocity, a production-grade Turing-complete STARK L-2 system is called for, and so we developed Cairo. Cairo stands for CPU Algebraic Intermediate Representation (AIR), and includes a single AIR that verifies the instruction set of this “CPU”.
The Solution: Cairo — One AIR to Rule Them All
Cairo joins a respectable list of toolchains that build scalable and/or zero knowledge (ZK) proofs for general computation. All previous systems deployed on testnets or mainnet can be classified as “libraries for writing circuits”³. These can also be thought of as the equivalent of toolchains for creating an “ASIC” for a particular computation. Cairo is a fundamentally different beast. The introduction of Cairo can be thought of as the transition from “ASIC” to “CPU”.
Cairo is the first production-grade proof system implementing a Turing Complete von Neumann Architecture: each Cairo program P resides in the virtual machine’s memory, alongside the data D processed by it. Cairo comes with a single AIR (and thus a single Verifier — in a smart contract, WebAssembly, etc.) that can verify any Cairo program. Namely, the Cairo AIR verifies the computational integrity of executing P on D, and the correctness of the post-execution state of the system.
With Cairo, new business logic doesn’t require a new smart contract, it only requires a different Cairo program. Consequently, the business logic and the proof system are clearly demarcated.
A single AIR to rule them all has a profound implication: one could use a single proof to assert the integrity of a bunch of different program executions. For example, a VeeDo-based sealed-bid auction, the minting of a batch of Gods Unchained cards, and another batch of dYdX trades, could all be proved valid in a single proof! We call this functionality a Generic Proving Service (GPS), and you’ll hear more about this shortly.
The Cairo Language
Cairo programs are written in an assembly-like programming language (called, well, Cairo) that has the following features: memory, function calls, recursion, and branching conditions. It also uses Prover-side “hints” to create shortcuts and enable certain computations. When we say that Cairo is production-grade we refer not just to our upcoming Mainnet deployments — we refer to the powerful development environment we’ve built for it, including a compiler from the Cairo language to Cairo byte code, a virtual machine that simulates Cairo executions, a debugger, IDE integration, and the above-mentioned single Verifier smart contract written in Solidity.
We will soon publish a whitepaper with details about the design philosophy of Cairo, alongside a full specification of this novel programming language. And, in the coming months, we’ll start releasing tools for writing, debugging and running Cairo programs (sign up for updates).
Cairo’s Efficiency and Safety
Efficiency and safety can be considered in the context of the math involved (AIR), or the engineering implementation (Verifier smart contract, for Ethereum) — Cairo helps on both fronts.
Cairo’s AIR is relatively simple, which leads to efficiency and low amortized costs for both the on-chain Verifier and the off-chain proving service. It also leads to increased security, because auditing a single simple AIR is safer than auditing multiple complicated application-specific AIRs.
Consequently, with Cairo, we can rely on a single Verifier smart contract; there is no longer a need to deploy a Verifier for every application used. Note the security implications of this property: a single set of audits for this one contract protects any application from the proof system risk, leaving them to audit only the business logic. As for the business logic, it is much easier to understand and audit code for correctness than it is to comprehend application-specific AIR.
To appreciate the concrete efficiency of Cairo as measured on real use cases, let’s look at two examples:
DeversiFi:
The StarkEx system currently powering DeversiFi 2.0 on Ethereum Mainnet is an “ASIC” STARK system. We implemented the same StarkEx over Cairo, ran it over testnet, and compared the two systems. As is often the case, CPUs are slower than ASICs. But in our case, due to some powerful Cairo optimizations, the difference is negligible:
- The Cairo Prover is 30% slower than the current “ASIC” implementation
- The Verifier consumes only 3% more gas
Reddit Bake-off:
Alongside the rest of the ecosystem, we sprinted to complete the Great Reddit Scaling Bake-off. Thanks to Cairo:
- We got there with unprecedented efficiency: Our ability to batch all 300K tx into a single proof, including aggregated call data (representing per batch only modified accounts rather than each and every tx) — these were a direct result of the programmability of Cairo, and the ease with which algorithmic optimizations can be harvested. We completed the whole thing in 6:03 minutes.
Worth noting: Higher-level programming enables easily adding optimizations, which often outweigh the CPU “penalty” mentioned above. Thus, in many cases the Cairo implementation may end up having better performance than what would have otherwise been practically achieved using a tailored AIR. - We got there fast: Few noticed that our single proof was submitted to Mainnet on July 15th, two weeks before the deadline of a six week sprint. This is an indication of the wonders Cairo can do for feature velocity.
The Road Ahead
We plan to make Cairo and GPS capabilities — developed by us and others — available to the broader developer community. We intend to offer powerful developer tools. We plan to develop compilers from Higher-Level languages to Cairo. We will make our cloud-based production environment available to the long tail of developers. This will take considerable effort and resources — Cairo won’t be built in a day. Instead, we will introduce new generations of Cairo at a regular cadence, which will offer enhanced functionality, better performance and powerful optimizations.
Currently we’re dog-fooding Cairo and improving it on a weekly basis, together with our partners DeversiFi, Immutable, and dYdX. If you want to build over Ethereum today, and are held up by scale and rising gas prices, if you want to build a real business that requires a production-grade toolchain with high feature velocity, do reach out to us.
Twitter: StarkWare, email: info@starkware.co
Thanks to Bobbin Threadbare and Georgios Konstantopoulos for insightful comments on a draft of this post.
Lior Goldberg, Shahar Papini, Michael Riabzev, and Eli Ben-Sasson
¹ We use the term in its colloquial meaning, as covering all real world general purpose computations.
² More accurately, what differs among different applications is the Algebraic Intermediate Representation (AIR), which is the STARK analog of the arithmetic circuits and R1CS systems used in SNARKs.
³ As categorized by the comprehensive zkp.science
