Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Docs: Add introduction documentation for cairo vm - Issue #328 #381

Merged
merged 8 commits into from
Jun 12, 2024
71 changes: 69 additions & 2 deletions docs/docs/vm-fundamentals/intro.md
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,73 @@
sidebar_position: -1
---

# Intro
# Introduction to the Cairo Virtual Machine

An introduction to fundamentals. Which core concepts we will be seeing, what are their purpose etc. Maybe a little description of each one.
Welcome to the introductory documentation for the Cairo VM, an essential component of the Starknet network. This documentation is designed to provide developers with a fundamental understanding of the Cairo VM's architecture and capabilities, empowering them to build and optimize applications on Starknet effectively. This documentation will be divided into four main parts, each of which we will briefly describe in this introduction.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

The Cairo Virtual Machine (CVM), at the heart of the Starknet network, is an advanced computational framework specifically designed to execute Casm bytecode generated by the Cairo compiler. Unlike traditional virtual machines constrained by the limitations of the Ethereum Virtual Machine (EVM), the Cairo VM operates under the principles of Validity Proof systems, it doesn't enhance the security of Ethereum but inherits from it thanks to validity proofs.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

## VM Layout

The Cairo Virtual Machine optimizes its operations around a unique structure of registers and memory to facilitate the efficient execution of Casm bytecode. Unlike traditional architectures where registers are separate storage units, in Cairo, these registers are pointers that facilitate access and management of memory during program execution.

coxmars marked this conversation as resolved.
Show resolved Hide resolved
General-Purpose Registers: These are hypothetical in Cairo, where instead of traditional CPU-bound registers all operations are directly performed on memory cells. This approach aligns with Cairo’s optimization strategy which aims to minimize the number of trace cells in the Algebraic Intermediate Representation (AIR). In Cairo, registers such as the Program Counter (pc), Allocation Pointer (ap), and Frame Pointer (fp) do not store data themselves, instead:
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Program Counter (pc): Points to the current instruction in memory that the VM is executing.

Allocation Pointer (ap): Identifies the first free memory cell not yet used by the program, crucial for dynamic memory management.

Frame Pointer (fp): Points to the current frame on the stack, managing the execution context of function calls.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Memory Models: Cairo employs a nondeterministic read-only memory model, unlike typical random-access memory (RAM) used in most computing systems where any memory cell can be read or written at any time, Cairo's memory model only allows memory to be written once and restricts subsequent modifications. In addition, this model is particularly efficient for AIR, as it requires fewer trace cells per memory access, optimizing the proof generation process.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Additionally, Cairo's memory model supports the concept of "public memory," which is essential for verifying the integrity of data between the prover and verifier, likewise, public memory allows the prover to demonstrate that certain memory cells hold specific values without revealing the entire memory content. This feature is crucial for operations like loading bytecode, passing arguments, and returning values from programs, making it both a secure and efficient mechanism for handling data within the Cairo VM.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

## Basic Instructions

Cairo's instruction set is designed to facilitate the verification of computations within its unique programming environment. The foundational aspect of Cairo instructions revolves around assertions of equality, which form the basis of most operations within the virtual machine.

Assert Statements
coxmars marked this conversation as resolved.
Show resolved Hide resolved
A primary form of instruction in Cairo is the assert statement, which verifies that two values or computations are equal. For example, the instruction `[ap] = [ap - 1] * [fp], ap++`, ap++; not only performs multiplication but also asserts that the result is equal to the value at the current free memory cell `[ap]`, before incrementing `[ap]` with `ap++`. Furthermore, this mechanism is essential for ensuring that each step of the computation adheres to expected results, crucial for the integrity of proofs in the Cairo system.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Pointer Management
Incrementing the allocation pointer ap++ is a standard operation accompanying many Cairo instructions. This operation is crucial as it prepares the virtual machine to access the next cell in memory for subsequent operations, maintaining a continuous flow of computation.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Control Flow Instructions
coxmars marked this conversation as resolved.
Show resolved Hide resolved
Conditional and Unconditional Jumps: These instructions manage the flow of execution, allowing the program to branch or loop based on conditions or unconditionally, respectively.

Call and Return Instructions: Similar to functions in traditional programming, these instructions manage the execution of subroutines within Cairo code. The call instruction directs the machine to execute a block of code at another location, and return concludes that execution, resuming control at the point following the original call.
coxmars marked this conversation as resolved.
Show resolved Hide resolved
These control structures are pivotal for creating complex, logical structures within Cairo programs, enabling more dynamic and versatile applications than would be possible with linear execution paths alone.

Advanced Syntax and Operations
Beyond basic arithmetic and control flow, Cairo supports advanced operations and syntactic constructs that enhance the expressiveness and functionality of the code. Instructions can involve complex operations like double dereferencing, which interprets values as addresses, and direct manipulation of values with immediate and offsets to facilitate flexible memory operations.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

## Builtins

Cairo incorporates builtins, which are optimized low-level execution units specifically designed to perform predefined computations, such as hash functions, syscalls, and range checks. Builtins provide a highly efficient means of implementing functions that would otherwise require extensive Cairo instructions, potentially leading to inefficiencies. These builtins function by executing a set of equations specifically tailored to perform and prove specific tasks, aligning them with Cairo’s approach to utilizing Algebraic Intermediate Representation (AIR).
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Instead of adding new instructions to the Cairo instruction set, which could be costly even if not used, builtins interact directly with the VM's memory system. This interaction does not involve special instructions to invoke a builtin; rather, it employs a method known as memory-mapped I/O, where builtins are engaged through reading or writing to specific memory cells affected by the builtin.

The Cairo CPU operates similarly to a traditional CPU but is implemented as an AIR due to it fetches and executes instructions directly from memory, integrating seamlessly with the builtins. This seamless integration enables the Cairo VM to efficiently handle complex computations without the need for burdensome additional instructions in the core set. This architecture ensures that while the Cairo CPU manages general computations, builtins handle specialized tasks, and each set of operations leverages the AIR framework to ensure that the computations are not only efficient but also provable.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

TAdev0 marked this conversation as resolved.
Show resolved Hide resolved
## Hints

Cairo language introduces "prover hints" or simply "hints" which are snippets of code strategically inserted between Cairo instructions to facilitate additional computations necessary for the prover's operations. Unique to the prover's process, these hints can be authored in any programming language, as their execution is not required to be verified, thereby not needing to be included in the proof submitted to the verifier. As a result, when the Cairo Runner encounters a hint before a Cairo instruction, it executes the hint first potentially initializing memory cells before proceeding with the Cairo instruction.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Hints are written in Python in the Cairo VM currently in production, providing a powerful tool for the prover to execute operations invisible to the verifier, hence, this invisibility is crucial as it allows the hint to perform complex tasks without making them part of the program's formal execution trace, thereby not counting towards the total number of execution steps in the Cairo VM. Moreover, while hints offer enhanced capabilities in writing Cairo code, their use within Starknet contracts should be avoided unless the hints are specifically approved or whitelisted by Starknet.

As a consequence, a "hint" in Cairo is a block of any language executed just before the subsequent Cairo instruction, interacting directly with the program’s variables or memory. So, to incorporate a hint, the Python code must be enclosed within %{ and %} markers, this feature allows programmers to leverage Python's extensive functionalities within Cairo programs, enhancing their capability to manage complex computations efficiently and securely.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

## Cairo Runner

The Cairo Runner serves as the practical interface between theoretical computational models and their execution within the Cairo framework because it is a pivotal tool in the transformation of abstract statements into verifiable computations, exemplified by converting a claim such as "the j-th Fibonacci number is y" into inputs that the deterministic and nondeterministic Cairo machines can process. The success of these inputs in the respective machines substantiates the truth of the original statement, leveraging the Cairo AIR and the STARK protocol to demonstrate the validity of these computations.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

As a specialized computer program, the Cairo Runner is responsible for executing compiled Cairo programs, which notably include nondeterministic code, this execution is distinct from that of conventional programs due to Cairo's allowance for nondeterminism. For example, in a scenario where the computation involves finding the square root of a number, the Cairo Runner facilitates the execution by considering both possible solutions (e.g., +Y and -Y) and selecting the one that satisfies the subsequent program instructions.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

This process is supported by "hints," which are special instructions that the Cairo Runner utilizes to resolve nondeterministic outcomes that cannot be directly inferred. These hints, typically written in Python, are crucial for the execution of certain Cairo programs where additional information is necessary to determine the course of execution.

## Resources

In the Cairo Virtual Machine, state transitions, influenced by each instruction, play a crucial role in the VM's operation. Unlike traditional deterministic CPU architectures, Cairo can handle nondeterministic transitions, allowing it to verify a wider range of computational statements efficiently. However, if a valid subsequent state cannot be established leading to what's known as an "execution rejection" the prover cannot generate proof for that program's execution. Therefore, this highlights the importance of stringent resource management within Cairo, ensuring that the VM operates within its limits and maintains the overall stability and security of the Starknet platform.
coxmars marked this conversation as resolved.
Show resolved Hide resolved

Managing resources effectively is essential for preventing scenarios where an execution might be rejected due to the system hitting resource limits or encountering computationally infeasible states. By carefully monitoring and constraining the use of memory, computational steps, and data outputs, the Cairo VM ensures that each program can be executed and verified without risking the overall stability and security of the Starknet platform.
coxmars marked this conversation as resolved.
Show resolved Hide resolved
Loading