create powdr book

README.md

@@ -43,52 +43,6 @@ The assembly language is designed to be extensible. This means that it does not
 native instruction. Instead, all instructions are user-defined and because of that,
 it is easy to adapt *powdr* assembly to any VM.
 
-## How to run the Rust-RISCV example
-
-```sh
-# Install the riscv target for the rust compiler
-rustup target add riscv32imc-unknown-none-elf
-# Run the compiler. It will generate files in /tmp/.
-# -i specifies the prover witness input (see below)
-cargo run --release rust riscv/tests/riscv_data/sum.rs -o /tmp -f -i 10,2,4,6 
-```
-
-The following example Rust file verifies that a supplied list of integers sums up to a specified value.
-Note that this is the full and only input file you need for the whole process!
-
-```rust
-#![no_std]
-
-extern crate alloc;
-use alloc::vec::Vec;
-
-use runtime::get_prover_input;
-
-#[no_mangle]
-pub fn main() {
-    // This is the sum claimed by the prover.
-    let proposed_sum = get_prover_input(0);
-    // The number of integers we want to sum.
-    let len = get_prover_input(1) as usize;
-    // Read the numbers from the prover and store them
-    // in a vector.
-    let data: Vec<_> = (2..(len + 2))
-        .map(|idx| get_prover_input(idx as u32))
-        .collect();
-    // Compute the sum.
-    let sum: u32 = data.iter().sum();
-    // Check that our sum matches the prover's.
-    assert_eq!(sum, proposed_sum);
-}
-```
-
-The function `get_prover_input` reads a number from the list supplied with `-i`.
-
-This is just a first mechanism to provide access to the outside world.
-The plan is to be able to call arbitrary user-defined `ffi` functions that will translate to prover queries,
-and can then ask for e.g. the value of a storage slot at a certain address or the
-root hash of a merkle tree.
-
 ### Notes on Efficiency
 
 Currently, the code is extremely wasteful. It generates many unnecessary columns.

book/.gitignore

@@ -0,0 +1 @@
+book

book/README.md

@@ -0,0 +1,14 @@
+# the powdr book
+
+This is the powdr book.
+
+## Contributing
+
+To serve the book:
+
+```
+cargo install mdbook
+mdbook serve
+```
+
+Then put changes in the `src` folder.

book/book.toml

@@ -0,0 +1,6 @@
+[book]
+authors = ["schaeff"]
+language = "en"
+multilingual = false
+src = "src"
+title = "powdr"

book/src/README.md

@@ -0,0 +1,21 @@
+# Introduction
+
+**powdr** is a compiler stack to build zkVMs.
+It is ideal for implementing existing VMs or experimenting with new designs with minimal boilerplate.
+
+* Domain specific languages are used to specify the VM and its underlying constraints, not low level Rust code
+* Automated witness generation
+* Support for multiple provers as well as aggregation schemes
+* Support for hand-optimized co-processors when performance is critical
+* Built in Rust 🦀
+
+## Contributing
+
+powdr is free and open source. You can find the source code on
+[GitHub](https://github.com/powdr-labs/powdr) and issues and feature requests can be posted on
+the [GitHub issue tracker](https://github.com/powdr-labs/powdr/issues).
+
+## License
+
+The powdr source and documentation are released under
+the [MIT License](https://opensource.org/license/mit/).

book/src/SUMMARY.md

@@ -0,0 +1,23 @@
+# Summary
+
+[Introduction](./README.md)
+
+# Getting Started
+- [Installation](./installation.md)
+- [Hello World](./hello_world.md)
+
+# Reference Guide
+- [asm](./asm/README.md)
+    - [Machines](./asm/machines.md)
+    - [Registers](./asm/registers.md)
+    - [Instructions](./asm/instructions.md)
+    - [Functions](./asm/functions.md)
+- [PIL](./pil/README.md)
+    - [Fixed Columns](./pil/fixed_columns.md)
+- [frontends](./frontends/README.md)
+    - [RISCV](./frontends/riscv.md)
+    - [Valida](./frontends/valida.md)
+    - [EVM](./frontends/evm.md)
+- [Backends](./frontends/README.md)
+    - [Halo2](./backends/halo2.md)
+    - [eSTARK](./backends/estark.md)

book/src/asm/README.md

@@ -0,0 +1,3 @@
+# asm
+
+powdr asm is the higher level of abstraction in powdr. It allows defining Instruction Set Architectures (ISA) using dynamic and static machines.

book/src/asm/functions.md

@@ -0,0 +1,74 @@
+# Functions
+
+Machine functions are the entry points to this machine. They can be called from another machine or from the outside.
+
+For static machines, functions simply indicate which columns should be exposed as inputs and outputs. They do not contain statements, since the business logic of all functions in the static machine is defined directly in constraints. We refer to the previous example [here](./machines.md#static-machines).
+
+From now on, we describe functions in dynamic machines with the example of this simple machine:
+
+```
+{{#include ../../../test_data/asm/book/function.asm:all}}
+```
+
+## Function inputs and outputs
+
+> For dynamic machines, function inputs and outputs are not supported yet
+
+## Expressions
+
+### Field element literals
+
+Field element literals are signed elements of the prime field.
+
+```
+{{#include ../../../test_data/asm/book/function.asm:literals}}
+```
+
+### Registers
+
+Registers can be used as expressions, with the exception of assignment registers.
+```
+{{#include ../../../test_data/asm/book/function.asm:read_register}}
+```
+
+### Instructions
+
+Instructions which return outputs can be used as expressions.
+```
+{{#include ../../../test_data/asm/book/function.asm:instruction}}
+```
+
+## Statements
+
+### Labels
+
+Labels allow referring to a location in a function by name.
+
+```
+{{#include ../../../test_data/asm/book/function.asm:label}}
+```
+
+### Assignments
+
+Assignments allow setting the value of a write register to the value of an expression using an assignment register.
+
+```
+{{#include ../../../test_data/asm/book/function.asm:instruction}}
+```
+
+One important current requirement is for the assignment register of the assignment to be compatible with that of the expression. This is especially relevant for instructions: the assignment register of the instruction output must match that of the assignment. In this example, we use `Y` in the assignment as the output of `square` is `Y`:
+
+```
+{{#include ../../../test_data/asm/book/function.asm:square}}
+```
+
+
+> Specifying the assignment register of the assignment is currently required even in cases where it could be inferred.
+
+### Instructions
+
+Instructions which do not return outputs can be used as statements.
+
+```
+{{#include ../../../test_data/asm/book/function.asm:instruction_statement}}
+```

book/src/asm/instructions.md

@@ -0,0 +1,30 @@
+# Instructions
+
+Instructions are declared as part of a powdr asm machine. Their inputs and outputs are [assignment registers](./registers.md) as well as labels. Once defined, they can be called by any function of this machine.
+
+# Local instructions
+
+A local instruction is the simplest type of instruction. It is called local because its behavior is defined using constraints over columns of the machine it is defined in.
+
+```
+instr add X, Y -> Z {
+    X + Y = Z
+}
+```
+
+Instructions feature:
+- a name
+- some inputs
+- some outputs
+- a set of PIL constraints to activate when the instruction is called
+
+# External instructions
+
+An external instruction points to a function inside a submachine of this machine. When it is called, a call is made to the submachine function. An example of an external instruction is the following:
+
+```
+instr assert_zero X = my_submachine.assert_zero // where `assert_zero` is a function defined in `my_submachine`
+```
+
+Note that external instruction cannot link to functions of the same machine: they delegate computation to a submachine.
+

book/src/asm/machines.md

@@ -0,0 +1,56 @@
+# Machines
+
+Machines are the first main concept in powdr asm. They can currently be of two types: dynamic or static.
+
+## Dynamic machines
+
+Dynamic machines are defined by:
+- a degree
+- a set of registers, including a program counter
+- an instruction set
+- some constraints
+- a set of functions
+- a set of submachines
+
+> Dynamic machines are currently limited to having a single function called `main`
+
+An example of a simple dynamic machine is the following:
+
+```
+{{#include ../../../test_data/asm/book/hello_world.asm}}
+```
+
+## Static machines
+
+Static machines are a lower-level type of machine. They do not have registers, and instead rely on simple committed and fixed columns. They are used to implement hand-optimized computation.
+
+They are defined by:
+- a degree
+- a latch, used to identify rows at which the machine can be accessed from the outside
+- a set of functions
+
+> Currently, the latch must be a fixed column named `latch`
+
+An example of a simple static machine is the following:
+
+```
+{{#include ../../../test_data/asm/book/simple_static.asm}}
+```
+
+For more details on the constraints, check out the [pil](../pil) part of this book. Simply note that the parameters of the function are columns declared within the constraints block.
+
+## Submachines
+
+Machines can have submachines which they access by defining [external instructions](./instructions.md). They are declared like so:
+
+```
+machine MySubmachine {
+    ...
+}
+
+machine MyMachine {
+    MySubmachine my_submachine;
+}
+```
+
+> Currently only dynamic machines can have submachines, and these must be static

book/src/asm/registers.md

@@ -0,0 +1,40 @@
+# Registers
+
+Registers are central to a machine. powdr supports a few types of registers:
+
+## Program counter
+
+Each machine can have at most one program counter. In the absence of a program counter, the machine is considered static, and no other register can be declared. The program counter is defined like so:
+
+```
+reg pc[@pc]
+```
+
+At each step execution step, the program counter points to the ROM line to execute.
+The program counter behaves like a [write register](#write-registers), with the exception that its value is incremented by default after each step.
+
+## Write registers
+
+Write registers are the default type for registers. They are declared like so:
+
+```
+{{#include ../../../test_data/asm/book/write_register.asm:declaration}}
+```
+
+They hold a field element, are initialised at 0 at the beginning of a function and keep their value by default. They can be read from and written to.
+
+```
+{{#include ../../../test_data/asm/book/write_register.asm:component}}
+```
+
+## Assignment registers
+
+Assignment registers are transient to an execution step: their value is not persisted across steps. They are required in order to pass inputs and receive outputs from instructions, as well as in assignments.
+For example, if we want to assert that write register `A` is `0`, we can use the following instruction:
+```
+{{#include ../../../test_data/asm/book/assert_write_register.asm:component}}
+```
+However, if we want the instruction to accept any write register as input, we use an assignment register.
+```
+{{#include ../../../test_data/asm/book/assert_assignment_register.asm:component}}
+```

book/src/backends/estark.md

@@ -0,0 +1,3 @@
+# eSTARK
+
+Integrated support for [eSTARK](https://eprint.iacr.org/2023/474) with the goldilocks field is under development.

book/src/backends/halo2.md

@@ -0,0 +1,3 @@
+# Halo2
+
+powdr supports the [PSE fork of halo2](https://github.com/privacy-scaling-explorations/halo2) with the bn254 field.

book/src/frontends/README.md

@@ -0,0 +1,3 @@
+# Frontends
+
+While any front end can be implemented in powdr asm, powdr comes built-in with several front-ends for popular instruction set architectures.

book/src/frontends/evm.md

@@ -0,0 +1,3 @@
+# EVM
+
+An EVM frontend for powdr is under development. If you are interested, feel free to reach out on matrix!