Skip to content

Commit

Permalink
move CairoVM related doc into separate section
Browse files Browse the repository at this point in the history
  • Loading branch information
@mellowcroc
mellowcroc committed Sep 23, 2024
1 parent e01ff2f commit 0c4c49f
Show file tree
Hide file tree
Showing 2 changed files with 82 additions and 79 deletions.
82 changes: 3 additions & 79 deletions src/cairo/bootloader.md
View file
Original file line number Diff line number Diff line change
@@ -1,86 +1,10 @@
# Bootloader

The bootloader is a Cairo program that can prove the execution of multiple Cairo programs by simply running the programs inside the bootloader. Since the Cairo program to be proved can be any arbitrary program, it can also be a Cairo verifier program, which means that the bootloader also supports creating a proof that proves the validity of a bootloader proof. Building on this concept, the bootloader allows creating a proof of nested Cairo programs, or a tree-like structure made up of Cairo programs and bootloader proofs.
The primary purpose of the bootloader is to reduce the size of the public inputs, which includes the instructions of the program that is being proven. Since this can become a bottleneck once a program becomes big enough, the idea is to create a program of constant size that executes the big program and outputs only the hash of its instructions, which can be externally verified. Using the bootloader, we can also do the following: 1. sequentially run multiple programs, and 2. recursively verify bootloader proofs inside the bootloader.

If this sounds too abstract, don't worry--this doc will attempt to explain in detail how the bootloader works and the two use cases mentioned above. (Note: this is based on the [Cairo v0.13.1 version of the bootloader](https://github.com/starkware-libs/cairo-lang/tree/v0.13.1/src/starkware/cairo/bootloaders))
Note: this doc is based on the [Cairo v0.13.1 version of the bootloader](https://github.com/starkware-libs/cairo-lang/tree/v0.13.1/src/starkware/cairo/bootloaders)

## A short primer on how CairoVM works

Before diving into the details about the bootloader, let’s go over how CairoVM works. CairoVM is a virtual machine that can execute a Cairo program (technically, a Cairo program compiled to a Cairo-specific set of instructions) and in the end produce a memory vector and execution trace table that is populated throughout the execution of the program.

More specifically, the generated memory can be thought of as a vector that is divided into segments that have different functionalities (e.g. program instructions, execution, output). The execution trace is a table with 3 columns each representing a register value and rows that each represent the value of the registers over the execution of the program. This means that the number of rows is equal to the number of steps that the CairoVM runs, given that 1 step equals 1 instruction call.

<div style="text-align: center;">
<img src="cairo_vm.png" alt="CairoVM execution structure" width="80%">
</div>

Note: the execution segment can be thought of as values that are written to the stack while running a program. Since the memory values can only be written once in CairoVM, the stack values are all written to this segment.

Using these results of the CairoVM execution, the Stone prover can create a proof that proves the following (very roughly speaking):

- there exists a valid execution trace of n steps on the CairoVM
- which starts with a given set of initial register values
- which ends with a given set of final register values
- for some memory which satisfies certain constraints (e.g. read-only, continuous, consistent with the public memory portion)

### Builtins

Builtins are pre-allocated memory cells that can be used for certain commonly-used “builtin” functions. As of Cairo v0.13.1, these builtins are currently supported:

- Output
- Pedersen
- Range check
- Bitwise
- Elliptic curve operation
- Keccak
- Poseidon
- Range check (96 bits)

Each builtin will have a separate segment in the memory vector and depending on the builtin, you can just input the values you want to run the builtin on or additionally use the output of the builtin.

For example, to use the range-check builtin you can just input the values you want to range-check in a certain memory segment and the CairoVM will create the necessary constraints for you.

For a Pedersen builtin, on the other hand, for each builtin use, you can input two values and read the next cell as output since the VM provides a guarantee that the next cell will contain the correct output (i.e. the Pedersen hash of the two input values).

<div style="text-align: center;">
<img src="builtin_memory_layout.png" alt="Builtin memory layout" width="80%">
</div>

In order to run a program that uses one of these builtins, we need to specify a specific layout to CairoVM that supports the builtins that the program uses. Below is a subset of layouts that are currently supported by the CairoVM. (Check this [code](https://github.com/lambdaclass/cairo-vm/blob/main/vm/src/types/instance_definitions/builtins_instance_def.rs) for the updated, comprehensive list)

| | small | recursive | dex | recursive_with_poseidon | starknet | starknet_with_keccak |
| ----------- | :---: | :-------: | :-: | :---------------------: | :------: | :------------------: |
| output | O | O | O | O | O | O |
| pedersen | O | O | O | O | O | O |
| range_check | O | O | O | O | O | O |
| bitwise | | O | | O | O | O |
| ecdsa | | | O | | O | O |
| poseidon | | | | O | O | O |
| ec_op | | | | | O | O |
| keccak | | | | | | O |

### Hints

Hints are non-deterministic computation (i.e. code that is run outside of the VM to populate values that are validated inside the VM)

For example, when computing the square root of an integer in a prime field, directly computing this using constraints is expensive. So instead, we can use hint to calculate the square root and create a constraint inside the VM that checks that the power of the given square root is equal to the original value.

So given a computation $x=\sqrt{y}$, compute $y$ using a hint and create a constraint: $y=x*x$

$x$ from the perspective of the VM is a wild guess, but the constraint makes sure that it’s valid.

In Cairo 0 language, you can run a hint by embedding a block of Python code. Below is an example of computing a square root of 25.

```python
[ap] = 25, ap++;
%{
import math
memory[ap] = int(math.sqrt(memory[ap - 1]))
%}
[ap - 1] = [ap] * [ap], ap++;
```

When compiling this Cairo 0 program into CASM, the compiler stores this Python code as a string and specifies that this hint should be run before running the ensuing instruction. In this case, the hint should be run before the `[ap - 1] = [ap] * [ap], ap++;` instruction.
Please refer to the [CairoVM doc](./cairo_vm.md) for an overview of how CairoVM works.

## How the "simple bootloader" works

Expand Down
79 changes: 79 additions & 0 deletions src/cairo/cairo_vm.md
View file
Original file line number Diff line number Diff line change
@@ -0,0 +1,79 @@
# CairoVM

Cairo compiles down to CairoVM and in the end produce a memory vector and execution trace table that is populated throughout the execution of the program.

More specifically, the fully assigned memory can be thought of as a vector that is divided into segments that have different functionalities (e.g. program instructions, execution, output). The execution trace is a table with 3 columns each representing a register value and rows that each represent the value of the registers over the execution of the program.

<div style="text-align: center;">
<img src="cairo_vm.png" alt="CairoVM execution structure" width="80%">
</div>

Note: the execution segment can be thought of as values that are written to the memory when running a program. Since the memory values can only be written once in CairoVM, Cairo programs keep track of the next available memory cell with a "allocation pointer" register (similar to a bump allocator in conventional terms).

Using these results of the CairoVM execution, the Stone prover can create a proof that proves the following (very roughly speaking):

- there exists a valid execution trace of n steps on the CairoVM
- which starts with a given set of initial register values
- which ends with a given set of final register values
- for some memory which satisfies certain constraints (e.g. read-only, continuous, consistent with the public memory portion)

## Builtins

Builtins can be understood as memory-mapped peripherals, i.e. pre-allocated memory cells that can be used for certain commonly-used functions.

As of Cairo v0.13.1, these builtins are currently supported:

- Output
- Pedersen
- Range check (128 bits)
- Bitwise
- Elliptic curve operation
- Keccak
- Poseidon
- Range check (96 bits)

Each builtin is assigned a separate segment in the memory vector. The VM will write the builtin inputs to memory cells in the segment and retrieve the builtin outputs by reading memory cells from the segment.

For the range-check builtin, the CairoVM simply writes the value to be range checked into the next unused cell in the range-check segment. This segment guarantees that every memory cell in the range [X, Y).

For a Pedersen builtin, on the other hand, for each builtin use, you can input two values and read the next cell as output since the VM provides a guarantee that the next cell will contain the correct output (i.e. the Pedersen hash of the two input values).

<div style="text-align: center;">
<img src="builtin_memory_layout.png" alt="Builtin memory layout" width="80%">
</div>

In order to run a program that uses one of these builtins, we need to specify a specific layout to CairoVM that supports the builtins that the program uses. Below is a subset of layouts that are currently supported by the CairoVM. (Check this [code](https://github.com/lambdaclass/cairo-vm/blob/main/vm/src/types/instance_definitions/builtins_instance_def.rs) for the updated, comprehensive list)

| | small | recursive | dex | recursive_with_poseidon | starknet | starknet_with_keccak |
| ----------- | :---: | :-------: | :-: | :---------------------: | :------: | :------------------: |
| output | O | O | O | O | O | O |
| pedersen | O | O | O | O | O | O |
| range_check | O | O | O | O | O | O |
| bitwise | | O | | O | O | O |
| ecdsa | | | O | | O | O |
| poseidon | | | | O | O | O |
| ec_op | | | | | O | O |
| keccak | | | | | | O |

## Hints

Hints are non-deterministic computation (i.e. code that is run outside of the VM to populate values that are validated inside the VM)

For example, when computing the square root of an integer in a prime field, directly computing this using constraints is expensive. So instead, we can use hint to calculate the square root and create a constraint inside the VM that checks that the power of the given square root is equal to the original value.

So given a computation $x=\sqrt{y}$, compute $y$ using a hint and create a constraint: $y=x*x$

$x$ from the perspective of the VM is a wild guess, but the constraint makes sure that it’s valid.

In Cairo 0 language, you can run a hint by embedding a block of Python code. Below is an example of computing a square root of 25.

```python
[ap] = 25, ap++;
%{
import math
memory[ap] = int(math.sqrt(memory[ap - 1]))
%}
[ap - 1] = [ap] * [ap], ap++;
```

When compiling this Cairo 0 program into CASM, the compiler stores this Python code as a string and specifies that this hint should be run before running the ensuing instruction. In this case, the hint should be run before the `[ap - 1] = [ap] * [ap], ap++;` instruction.

0 comments on commit 0c4c49f

Please sign in to comment.