This is a study note of Cairo whitepaper. The main purpose of Cairo is to enable the generation of proofs of the integrity of general computation. The withepaper covers its CPU architecture and a set of polynomial equations that validate the execution of Cairo program.
Cryptographic proof systems for computational integrity are protocols that have two desired features: zero-knowledge for privacy and succinct verfication for efficency.
Cairo is a programming language that describes a computation and its execution generates a proof of integrity for the computation. Most of the existing proof systems represent the computation being proven in terms of polynomial equations over a finite field – so called “arithmetization” process. Current arithmetization representations include arithmetic circuits, Quadratic Span Programs (R1CS), and Algebraic Intermediate Representions (AIR). These representations are complicated and often result in unnecessary computation for branching and looping operations.
One solution could be a compiler that compiles the computational code into a list of polynomial equations. ZKPDL, Pinocchio, TinyRAM and xJsnark are some examples. The process is simpler but they suffered from the inefficiencies mentioned above.
The Cairo approach learns from the CPU and the von Neumann architecture: using a single universal system of polynomial equations representing the execution of an arbitrary computer program. It was used by vnTinyRAM system. Cairo is the first STARK von Neumann architecture. Its features are:
- The instruction set (algebraic RISC) is expressive and efficent. All instructions can be encoded using 15 flags and 3 integers.
- Predefined complex operations are implemented as a set of equations using efficient builtins.
- It is practical. Cairo supports conditional branches, memory, function calls, and recursion.
- It uses a read-only random-access memory.
- It uses permutation range-checks.
- the nondeterministic von Neumann architecture can prove multiple different programs in one proof where only the program hash is known to the verifier.
2 Design Principles
The Cairo framework is used to convince the verifier that a certain program ran successfully with some given output. It provdes a layer of abstraction around STARK protocol that simplifies the way the computation is described. Cairo uses an assembly language to describe the Algebraic Intermediate Representation (AIR). An AIR can be thought of as a list of polynomial constraints (equations) operating on trace, the **witness. The trace is a two-dimensioinal table of field elements. A STARK proof proves that there exists a trace satisfying the contraints.