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
16 changes: 7 additions & 9 deletions docs/docs/vm-fundamentals/intro.md
Original file line number Diff line number Diff line change
Expand Up @@ -10,7 +10,7 @@ First, let us clarify what is a Virtual Machine (VM)? A VM is **a digital versi

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.

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. Also, the Cairo VM is able to generate cryptographic proofs, these proofs are be posted on a settlement layer such as Ethereum, offering Starknet the same level of security as the underlying layer
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. Also, the Cairo VM is able to generate cryptographic proofs, these proofs will be posted on a settlement layer such as Ethereum, offering Starknet the same level of security as the underlying layer.

## VM Layout

Expand All @@ -20,7 +20,7 @@ The Cairo Virtual Machine optimizes its operations around a unique structure of

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:
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.

### Pointers

Expand All @@ -29,7 +29,7 @@ Allocation Pointer (ap) identifies the first free memory cell not yet used by th

### Memory

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.
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 memory model is particularly efficient for proof generation, as it requires fewer trace cells per memory access.
TAdev0 marked this conversation as resolved.
Show resolved Hide resolved

Cairo's memory model also introduces the idea of "public memory," a crucial feature for validating data integrity between the prover and verifier. This feature enables the prover to prove that specific memory cells contain certain values without exposing the entire memory's content.

Expand All @@ -41,11 +41,11 @@ Cairo's instruction set is designed to facilitate the verification of computatio

### Assert Statements

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++`; 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++`. This is crucial for the generation of proofs, however, proofs cannot be partially correct, they can be generated or not
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++`; 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++`.

### Pointer Management

The incrementing of the allocation pointer (ap++) is an important standalone operation in many Cairo instructions. It readies the virtual machine to utilize the next cell in memory for future operations, thereby ensuring a seamless flow of computation.
The increment of the allocation pointer (ap++) is an important standalone operation in many Cairo instructions. It prepares the virtual machine to utilize the next cell in memory for future operations, thereby ensuring a seamless flow of computation.

### Control Flow Instructions

Expand All @@ -64,8 +64,6 @@ In addition to fundamental arithmetic and control flow operations, Cairo provide

Builtins in Cairo are predefined and optimized low-level execution units that are added to the Cairo CPU board to perform predefined calculations that are expensive to perform in Cairo. Communication between the CPU and embedded functionalities occurs through memory-mapped I/O. Each builtin is assigned a contiguous region of memory and applies specific restrictions on the data found in that area.

TAdev0 marked this conversation as resolved.
Show resolved Hide resolved
This builtins are: output, Pedersen, range_check, ecdsa and bitwise. Each of this would be onboard in the specific section for builtins in this documentation.

## 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, not needed 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.
Expand All @@ -74,13 +72,13 @@ Hints are written in Python in the Cairo VM currently in production, providing a

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. To incorporate a hint, simply write Python code inside the `%{ ... %}` markers, this feature allows programmers to leverage Python's extensive functionalities within Cairo programs, enhancing their capability to manage complex computations efficiently and securely.

Hints in Cairo are useful when the cost of verifying a computed value is cheaper than finding the value itself, they are particularly valuable for solving equations or optimizing computational tasks. When considering hints, you should evaluate the properties of the inputs you will provide, the inequalities that define them, and the tools and builtins already available in Cairo.
Hints in Cairo are useful when the cost of verifying a computed value is cheaper than finding the value itself, they are particularly valuable for solving equations or optimizing computational tasks.

## Cairo Runner

The Cairo Runner, a specialized computer program, executes compiled Cairo programs. Unlike conventional programs, these include nondeterministic code due to Cairo's acceptance of nondeterminism. For instance, when computing the square root of a number, the Cairo Runner considers both possible outcomes (+Y and -Y). It then selects the solution that aligns with the following program instructions.

The output of the Cairo Runner comprises two main parts: an accepting input for the Cairo nondeterministic machine and an accepting input for the Cairo deterministic machine, which serves as the witness for the nondeterministic machine. Additionally, the Runner may return a failure if the execution results in a contradiction or if it cannot compute the value of a memory cell due to insufficient hints.
The output of the Cairo Runner comprises two main parts: an accepting input for the Cairo nondeterministic machine and a corresponding input for the Cairo deterministic machine, which serves as the witness for the nondeterministic machine. Additionally, the Runner may return a failure if the execution results in a contradiction or if it cannot compute the value of a memory cell due to insufficient hints.

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.

Expand Down