Add bootloader docs #7

mellowcroc · 2024-09-16T04:28:12Z

No description provided.

mimoo

Looks great!

rot256

Consider more explicitly stating when "we" are the VM and when "we" are the programmer.

Consider splitting into multiple sections: we might want to expand / reference the internals of the CairoVM later.

The illustrations are very useful!

rot256 · 2024-09-20T10:13:38Z

src/cairo/bootloader.md

@@ -1 +1,199 @@
 # 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 bootloader is a Cairo program that can prove the execution of multiple Cairo programs by simply running the programs inside the bootloader.

This seems a little cyclic.

AFAIK the primary purpose of the bootloader is to reduce the size of the public inputs: unlike a preprocessing SNARK the STARK takes the program instructions as public input.

Hence, for long programs, the bootloader serves to reduce the size of the public inputs and by extension the verifiers running time: effectively it turns the STARK into a preprocessing SNARK with the index being a hash of the program.

As a side-effect:

You can also have the bootloader execute one program after the other.

It makes recursion easier as the program executed at any node of the tree is the same: the bootloader.

rot256 · 2024-09-20T10:20:24Z

src/cairo/bootloader.md

+## 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)


Consider moving this to a separate section on the CairoVM

rot256 · 2024-09-20T10:22:08Z

src/cairo/bootloader.md

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


I guess the technical term is a "bump allocator"

rot256 · 2024-09-20T10:24:15Z

src/cairo/bootloader.md

+### 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           |


I would have a separate section on CairoVM builtins.

rot256 · 2024-09-20T10:24:31Z

src/cairo/bootloader.md

+### 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.


Again a separate section.

rot256 · 2024-09-20T11:37:30Z

src/cairo/iteratively_creating_proofs.png

rot256 · 2024-09-20T11:37:51Z

src/cairo/output_structure.png

rot256 · 2024-09-20T11:37:56Z

src/cairo/perfect_loop.png

rot256 · 2024-09-20T11:38:07Z

src/cairo/simple_bootloader_memory_layout.png

rot256 · 2024-09-20T11:38:29Z

src/cairo/simple_bootloader_output_memory_layout.png

mellowcroc self-assigned this Sep 16, 2024

mellowcroc force-pushed the add-bootloader-docs branch 2 times, most recently from e4009be to 7e4f0ce Compare September 16, 2024 11:36

add bootloader docs

a8c1d30

mellowcroc force-pushed the add-bootloader-docs branch from 7e4f0ce to a8c1d30 Compare September 16, 2024 11:37

rot256 self-requested a review September 16, 2024 11:38

mellowcroc requested a review from mimoo September 19, 2024 15:43

mimoo approved these changes Sep 19, 2024

View reviewed changes

mimoo merged commit e01ff2f into main Sep 19, 2024
1 check passed

rot256 reviewed Sep 20, 2024

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Add bootloader docs #7

Add bootloader docs #7

mellowcroc commented Sep 16, 2024

mimoo left a comment

rot256 left a comment

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

rot256 Sep 20, 2024

		@@ -1 +1,199 @@
		# 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.

Add bootloader docs #7

Add bootloader docs #7

Conversation

mellowcroc commented Sep 16, 2024

mimoo left a comment

Choose a reason for hiding this comment

rot256 left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment