diff --git a/.github/workflows/deploy-book.yml b/.github/workflows/deploy-book.yml new file mode 100644 index 000000000..454d28db6 --- /dev/null +++ b/.github/workflows/deploy-book.yml @@ -0,0 +1,43 @@ +# adapted from https://github.com/rust-lang/mdBook/wiki/Automated-Deployment%3A-GitHub-Actions#GitHub-Pages-Deploy + +name: Deploy book +on: + push: + branches: + - main + +jobs: + deploy: + runs-on: ubuntu-latest + permissions: + contents: write # To push a branch + pull-requests: write # To create a PR from that branch + steps: + - uses: actions/checkout@v3 + with: + fetch-depth: 0 + - name: Install latest mdbook + run: | + tag=$(curl 'https://api.github.com/repos/rust-lang/mdbook/releases/latest' | jq -r '.tag_name') + url="https://github.com/rust-lang/mdbook/releases/download/${tag}/mdbook-${tag}-x86_64-unknown-linux-gnu.tar.gz" + mkdir mdbook + curl -sSL $url | tar -xz --directory=./mdbook + echo `pwd`/mdbook >> $GITHUB_PATH + - name: Deploy GitHub Pages + run: | + # generate cli docs and inject them into the book + cargo run --package powdr_cli -- --markdown-help > book/src/cli/README.md + # build the book + cd book + mdbook build + git worktree add gh-pages + git config user.name "Deploy from CI" + git config user.email "" + cd gh-pages + # Delete the ref to avoid keeping history. + git update-ref -d refs/heads/gh-pages + rm -rf * + mv ../book/* . + git add . + git commit -m "Deploy $GITHUB_SHA to gh-pages" + git push --force --set-upstream origin gh-pages \ No newline at end of file diff --git a/README.md b/README.md index 8f9f10b30..413d74ef5 100644 --- a/README.md +++ b/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. diff --git a/book/.gitignore b/book/.gitignore new file mode 100644 index 000000000..7585238ef --- /dev/null +++ b/book/.gitignore @@ -0,0 +1 @@ +book diff --git a/book/README.md b/book/README.md new file mode 100644 index 000000000..6fb9f4927 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/book/book.toml b/book/book.toml new file mode 100644 index 000000000..6803379f8 --- /dev/null +++ b/book/book.toml @@ -0,0 +1,6 @@ +[book] +authors = ["schaeff"] +language = "en" +multilingual = false +src = "src" +title = "powdr" diff --git a/book/src/README.md b/book/src/README.md new file mode 100644 index 000000000..cf4d53264 --- /dev/null +++ b/book/src/README.md @@ -0,0 +1,21 @@ +# Introduction + +**powdr** is a modular compiler stack to build zkVMs. +It is ideal for implementing existing VMs and 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). 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/). \ No newline at end of file diff --git a/book/src/SUMMARY.md b/book/src/SUMMARY.md new file mode 100644 index 000000000..fb8e02d2b --- /dev/null +++ b/book/src/SUMMARY.md @@ -0,0 +1,26 @@ +# Summary + +[Introduction](./README.md) + +# Getting Started +- [Installation](./installation.md) +- [Hello World](./hello_world.md) + +# Reference Guide +- [CLI](./cli/README.md) +- [asm](./asm/README.md) + - [Machines](./asm/machines.md) + - [Registers](./asm/registers.md) + - [Functions](./asm/functions.md) + - [Expressions](./asm/expressions.md) + - [Instructions](./asm/instructions.md) +- [PIL](./pil/README.md) + - [Fixed Columns](./pil/fixed_columns.md) + - [Macros](./pil/macros.md) +- [Frontends](./frontends/README.md) + - [RISCV](./frontends/riscv.md) + - [Valida](./frontends/valida.md) + - [EVM](./frontends/evm.md) +- [Backends](./backends/README.md) + - [Halo2](./backends/halo2.md) + - [eSTARK](./backends/estark.md) diff --git a/book/src/asm/README.md b/book/src/asm/README.md new file mode 100644 index 000000000..c319567af --- /dev/null +++ b/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. \ No newline at end of file diff --git a/book/src/asm/expressions.md b/book/src/asm/expressions.md new file mode 100644 index 000000000..932aa7222 --- /dev/null +++ b/book/src/asm/expressions.md @@ -0,0 +1,23 @@ +# Expressions + +## Field element literals + +Field element literals are signed elements of the prime field. + +``` +{{#include ../../../test_data/asm/book/function.asm:literals}} +``` + +## Registers and columns + +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}} +``` \ No newline at end of file diff --git a/book/src/asm/functions.md b/book/src/asm/functions.md new file mode 100644 index 000000000..59814f1dd --- /dev/null +++ b/book/src/asm/functions.md @@ -0,0 +1,49 @@ +# Functions + +Machine functions are the entry points to a 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 a static machine is defined directly in constraints. We refer to the previous example [here](./machines.md#static-machines). + +In the rest of this section, 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 + +## 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](#expressions) using an assignment register. + +``` +{{#include ../../../test_data/asm/book/function.asm:instruction}} +``` + +One important 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. That restriction may be lifted in the future. + +### Instructions + +Instructions which do not return outputs can be used as statements. + +``` +{{#include ../../../test_data/asm/book/function.asm:instruction_statement}} +``` \ No newline at end of file diff --git a/book/src/asm/instructions.md b/book/src/asm/instructions.md new file mode 100644 index 000000000..029e2ce28 --- /dev/null +++ b/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 registers and 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 delegates calls 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 instructions cannot link to functions of the same machine: they delegate computation to a submachine. + diff --git a/book/src/asm/machines.md b/book/src/asm/machines.md new file mode 100644 index 000000000..3423c7077 --- /dev/null +++ b/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, indicating the number of execution steps +- a set of registers, including a program counter +- an instruction set +- 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, indicating the number of execution steps +- a latch, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed) +- 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) section of this book. 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 as follows: + +``` +machine MySubmachine { + ... +} + +machine MyMachine { + MySubmachine my_submachine; +} +``` + +> Currently only dynamic machines can have submachines, and these must be static \ No newline at end of file diff --git a/book/src/asm/registers.md b/book/src/asm/registers.md new file mode 100644 index 000000000..a2d381d0c --- /dev/null +++ b/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 as follows: + +``` +reg pc[@pc] +``` + +At each step execution step, the program counter points to the [function](./functions.md) 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 as follows: + +``` +{{#include ../../../test_data/asm/book/write_register.asm:declaration}} +``` + +They hold a field element, are initialized as 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}} +``` \ No newline at end of file diff --git a/book/src/backends/README.md b/book/src/backends/README.md new file mode 100644 index 000000000..0d89303de --- /dev/null +++ b/book/src/backends/README.md @@ -0,0 +1,3 @@ +# Backends + +powdr aims to have full flexibility when it comes to generating proofs and comes with a few built-in backends to get started with zkVMs. \ No newline at end of file diff --git a/book/src/backends/estark.md b/book/src/backends/estark.md new file mode 100644 index 000000000..3b19c8d4b --- /dev/null +++ b/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. \ No newline at end of file diff --git a/book/src/backends/halo2.md b/book/src/backends/halo2.md new file mode 100644 index 000000000..7de2b9fe4 --- /dev/null +++ b/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. \ No newline at end of file diff --git a/book/src/cli/.gitignore b/book/src/cli/.gitignore new file mode 100644 index 000000000..42061c01a --- /dev/null +++ b/book/src/cli/.gitignore @@ -0,0 +1 @@ +README.md \ No newline at end of file diff --git a/book/src/frontends/README.md b/book/src/frontends/README.md new file mode 100644 index 000000000..751e0c259 --- /dev/null +++ b/book/src/frontends/README.md @@ -0,0 +1,3 @@ +# Frontends + +While any frontend VM can be implemented in powdr asm, powdr comes with several frontends for popular instruction set architectures. diff --git a/book/src/frontends/evm.md b/book/src/frontends/evm.md new file mode 100644 index 000000000..ebe0a77a2 --- /dev/null +++ b/book/src/frontends/evm.md @@ -0,0 +1,3 @@ +# EVM + +An [EVM](https://ethereum.org/en/developers/docs/evm/) frontend for powdr is under development. If you are interested, feel free to [reach out](https://matrix.to/#/#powdr:matrix.org)! \ No newline at end of file diff --git a/book/src/frontends/riscv.md b/book/src/frontends/riscv.md new file mode 100644 index 000000000..62691d9a6 --- /dev/null +++ b/book/src/frontends/riscv.md @@ -0,0 +1,48 @@ +# RISCV + +A [RISCV](https://riscv.org/technical/specifications/) frontend for powdr is already available. + +## 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) +powdr 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. \ No newline at end of file diff --git a/book/src/frontends/valida.md b/book/src/frontends/valida.md new file mode 100644 index 000000000..8242391bb --- /dev/null +++ b/book/src/frontends/valida.md @@ -0,0 +1,3 @@ +# Valida + +A [Valida](https://github.com/valida-xyz/valida-compiler/issues/2) front end for powdr is under development. If you are interested, feel free to [reach out](https://matrix.to/#/#powdr:matrix.org)! \ No newline at end of file diff --git a/book/src/hello_world.md b/book/src/hello_world.md new file mode 100644 index 000000000..3c4a4562b --- /dev/null +++ b/book/src/hello_world.md @@ -0,0 +1,22 @@ +# Hello World + +Let's write [a minimal VM](https://github.com/powdr-labs/powdr/blob/main/test_data/asm/book/hello_world.asm) and generate a SNARK! + +``` +{{#include ../../test_data/asm/book/hello_world.asm}} +``` + +Then let's generate a proof of execution for the valid prover input `0` (since for `0 + 1 - 1 == 0`) + +```console +powdr pil hello_world.asm --field bn254 --force --inputs 0 --prove-with halo2 +``` + +We observe that a proof was created at `proof.bin`. +Now let's try for the invalid input `1` + +```console +powdr pil hello_world.asm --field bn254 --force --inputs 1 --prove-with halo2 +``` + +We observe that witness generation fails, and no proof is created. \ No newline at end of file diff --git a/book/src/installation.md b/book/src/installation.md new file mode 100644 index 000000000..cc52aca9b --- /dev/null +++ b/book/src/installation.md @@ -0,0 +1,29 @@ +# Installation + +The only way to install powdr currently is to build it from source. + +## Prerequisites + +You will need the [Rust](https://rust-lang.org) compiler and Cargo, the Rust package manager. +The easiest way to install both is with [`rustup.rs`](https://rustup.rs/). + +On Windows, you will also need a recent version of [Visual Studio](https://visualstudio.microsoft.com/downloads/), +installed with the "Desktop Development With C++" Workloads option. + +## Building + +Using a single Cargo command: + +```sh +cargo install --git https://github.com/powdr-labs/powdr powdr_cli +``` + +Or, by manually building from a local copy of the [powdr repository](https://github.com/powdr-labs/powdr): + +```sh +# clone the repository +git clone https://github.com/powdr-labs/powdr.git +cd powdr +# install powdr_cli +cargo install --path ./powdr_cli +``` diff --git a/book/src/pil/README.md b/book/src/pil/README.md new file mode 100644 index 000000000..61cf50b13 --- /dev/null +++ b/book/src/pil/README.md @@ -0,0 +1,3 @@ +# PIL + +powdr PIL is the lower level of abstraction in powdr. It is strongly inspired by and compatible with [Polygon zkEVM PIL](https://github.com/0xPolygonHermez/pilcom/). We refer to the [Polygon zkEVM PIL documentation](https://zkevm.polygon.technology/PIL/introduction) and document deviations from the original design here. \ No newline at end of file diff --git a/book/src/pil/fixed_columns.md b/book/src/pil/fixed_columns.md new file mode 100644 index 000000000..1ae6b3794 --- /dev/null +++ b/book/src/pil/fixed_columns.md @@ -0,0 +1,34 @@ +# Fixed columns + +powdr PIL requires the definition of fixed columns at the time of declaration. + +For example: + +``` +{{#include ../../../test_data/pil/fixed_columns.pil:declare_and_define}} +``` + +A number of mechanisms are supported to declare fixed columns. Let `N` be the total length of the column we're defining. + +## Values with repetitions + +powdr PIL supports a basic language to define the value of constant columns using: +- arrays, for example `[1, 2, 3]` +- repetition, for example `[1, 2]*` +- concatenation, for example `[1, 2] + [3, 4]` + +These mechanisms can be combined, as long as a single repetition is used per column definition. + +``` +{{#include ../../../test_data/pil/fixed_columns.pil:repetitions}} +``` + +## Mappings + +A column can be seen as a mapping from integers to field elements. In this context, different functions are supported: + +``` +{{#include ../../../test_data/pil/fixed_columns.pil:mapping}} +``` + +> Note that conversion from integer to field element is currently implicit, as seen in the first example above. \ No newline at end of file diff --git a/book/src/pil/macros.md b/book/src/pil/macros.md new file mode 100644 index 000000000..2ea986395 --- /dev/null +++ b/book/src/pil/macros.md @@ -0,0 +1,34 @@ +# Macros + +powdr PIL exposes a macro system which can generate arbitrary powdr PIL code. + +## Definition + +Let's define some macros which generate powdr PIL expressions: + +``` +{{#include ../../../test_data/pil/fib_macro.pil:expression_macro_definitions}} +``` + +In particular, we can generate constraints inside macros: + +``` +{{#include ../../../test_data/pil/fib_macro.pil:constraint_macro_definitions}} +``` + +## Usage + +> Macros currently have global scope + +Usage of the defined macros happens as expected in powdr PIL code: + +``` +{{#include ../../../test_data/pil/fib_macro.pil:expression_macro_usage}} +``` + +Generating constraints: + +``` +{{#include ../../../test_data/pil/fib_macro.pil:constraint_macro_usage}} +``` + diff --git a/book/src/powdr_logo_pink.png b/book/src/powdr_logo_pink.png new file mode 100644 index 000000000..4cd39d3f8 Binary files /dev/null and b/book/src/powdr_logo_pink.png differ diff --git a/book/theme/favicon.png b/book/theme/favicon.png new file mode 100644 index 000000000..4cd39d3f8 Binary files /dev/null and b/book/theme/favicon.png differ diff --git a/book/theme/favicon.svg b/book/theme/favicon.svg new file mode 100644 index 000000000..aa7906a2b --- /dev/null +++ b/book/theme/favicon.svg @@ -0,0 +1,14 @@ + + + + + + + + + + + + + + diff --git a/compiler/tests/asm.rs b/compiler/tests/asm.rs index 4068a8fc3..595fe5419 100644 --- a/compiler/tests/asm.rs +++ b/compiler/tests/asm.rs @@ -85,3 +85,24 @@ fn full_pil_constant() { verify_asm::(f, Default::default()); gen_proof(f, Default::default()); } + +#[test] +fn book() { + for f in fs::read_dir("../test_data/asm/book/").unwrap() { + let f = f.unwrap().path(); + let f = f.strip_prefix("../test_data/asm/").unwrap(); + // passing 0 to all tests currently works as they either take no prover input or 0 works + let i = [0]; + + verify_asm::(f.to_str().unwrap(), slice_to_vec(&i)); + gen_proof(f.to_str().unwrap(), slice_to_vec(&i)); + } +} + +#[test] +#[should_panic = "Witness generation failed."] +fn hello_world_asm_fail() { + let f = "book/hello_world.asm"; + let i = [1]; + verify_asm::(f, slice_to_vec(&i)); +} diff --git a/compiler/tests/pil.rs b/compiler/tests/pil.rs index 7748f22ae..ad4a97f8a 100644 --- a/compiler/tests/pil.rs +++ b/compiler/tests/pil.rs @@ -132,3 +132,8 @@ fn test_single_line_blocks() { fn test_two_block_machine_functions() { verify_pil("two_block_machine_functions.pil", None); } + +#[test] +fn test_fixed_columns() { + verify_pil("fixed_columns.pil", None); +} diff --git a/powdr_cli/Cargo.toml b/powdr_cli/Cargo.toml index 834847661..6b1075f6d 100644 --- a/powdr_cli/Cargo.toml +++ b/powdr_cli/Cargo.toml @@ -19,6 +19,7 @@ halo2 = { path = "../halo2", optional = true } backend = { path = "../backend" } pilopt = { path = "../pilopt" } strum = { version = "0.24.1", features = ["derive"] } +clap-markdown = "0.1.3" [dev-dependencies] tempfile = "3.6" diff --git a/powdr_cli/src/main.rs b/powdr_cli/src/main.rs index 37e767fab..21f39c2c1 100644 --- a/powdr_cli/src/main.rs +++ b/powdr_cli/src/main.rs @@ -2,13 +2,13 @@ mod util; -use clap::{Parser, Subcommand}; +use clap::{CommandFactory, Parser, Subcommand}; use compiler::{compile_pil_or_asm, Backend}; use env_logger::{Builder, Target}; use log::LevelFilter; use number::{Bn254Field, FieldElement, GoldilocksField}; use riscv::{compile_riscv_asm, compile_rust}; -use std::io::BufWriter; +use std::io::{self, BufWriter}; use std::{borrow::Cow, collections::HashSet, fs, io::Write, path::Path}; use strum::{Display, EnumString, EnumVariantNames}; @@ -34,10 +34,13 @@ pub enum CsvRenderMode { } #[derive(Parser)] -#[command(author, version, about, long_about = None)] +#[command(name = "powdr", author, version, about, long_about = None)] struct Cli { + #[arg(long, hide = true)] + markdown_help: bool, + #[command(subcommand)] - command: Commands, + command: Option, } #[derive(Subcommand)] @@ -233,7 +236,7 @@ fn split_inputs(inputs: &str) -> Vec { .collect() } -fn main() { +fn main() -> Result<(), io::Error> { let mut builder = Builder::new(); builder .filter_level(LevelFilter::Info) @@ -242,8 +245,17 @@ fn main() { .format(|buf, record| writeln!(buf, "{}", record.args())) .init(); - let command = Cli::parse().command; - run_command(command); + let args = Cli::parse(); + + if args.markdown_help { + clap_markdown::print_help_markdown::(); + Ok(()) + } else if let Some(command) = args.command { + run_command(command); + Ok(()) + } else { + Cli::command().print_help() + } } fn run_command(command: Commands) { @@ -524,7 +536,6 @@ fn optimize_and_output(file: &str) { mod test { use backend::Backend; - use tempfile; use crate::{run_command, Commands, CsvRenderMode, FieldArgument}; #[test] diff --git a/test_data/asm/book/assert_assignment_register.asm b/test_data/asm/book/assert_assignment_register.asm new file mode 100644 index 000000000..6887ef7bc --- /dev/null +++ b/test_data/asm/book/assert_assignment_register.asm @@ -0,0 +1,23 @@ +machine Machine { + + degree 8; + + // ANCHOR: component +reg pc[@pc]; +reg X[<=]; +reg A; + +instr assert_zero X { + X = 0 +} + +function main { + assert_zero A; + loop; +} + // ANCHOR_END: component + + instr loop { + pc' = pc + } +} \ No newline at end of file diff --git a/test_data/asm/book/assert_write_register.asm b/test_data/asm/book/assert_write_register.asm new file mode 100644 index 000000000..5a32d2295 --- /dev/null +++ b/test_data/asm/book/assert_write_register.asm @@ -0,0 +1,22 @@ +machine Machine { + + degree 8; + + // ANCHOR: component +reg pc[@pc]; +reg A; + +instr assert_A_is_zero { + A = 0 +} + +function main { + assert_A_is_zero; + loop; +} + // ANCHOR_END: component + + instr loop { + pc' = pc + } +} \ No newline at end of file diff --git a/test_data/asm/book/function.asm b/test_data/asm/book/function.asm new file mode 100644 index 000000000..64ed7c58e --- /dev/null +++ b/test_data/asm/book/function.asm @@ -0,0 +1,81 @@ +/* ANCHOR: all */ + +machine Machine { + + degree 256; + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg CNT; + reg A; + + // an instruction to assert that a number is zero + instr assert_zero X { + X = 0 + } + + // an instruction to jump to a label + instr jmp l: label { + pc' = l + } + + // an instruction to jump to a label iff `X` is `0`, otherwise continue + instr jmpz X, l: label { + pc' = XIsZero * l + (1 - XIsZero) * (pc + 1) + } + + // an instruction to return the square of an input + // ANCHOR: square + instr square X -> Y { + Y = X * X + } + // ANCHOR_END: square + + function main { + // initialise `A` to 2 + A <=X= 2; + // initialise `CNT` to `3` + // ANCHOR: literals + CNT <=X= 3; + // ANCHOR_END: literals + // ANCHOR: label + start:: + // ANCHOR_END: label + // if `CNT` is `0`, jump to `end` + jmpz CNT, end; + // decrement `CNT` + // ANCHOR: read_register + CNT <=X= CNT - 1; + // ANCHOR_END: read_register + // square `A` + // ANCHOR: instruction + A <=Y= square(A); + // ANCHOR_END: instruction + // jump back to `start` + jmp start; + end:: + // check that `A == ((2**2)**2)**2` + // ANCHOR: instruction_statement + assert_zero A - ((2**2)**2)**2; + // ANCHOR_END: instruction_statement + // loop forever + loop; + } + + // an instruction to loop forever + instr loop { + pc' = pc + } + + // some superpowers on `X` to allow us to check if it's 0 + constraints { + col witness XInv; + col witness XIsZero; + XIsZero = 1 - X * XInv; + XIsZero * X = 0; + XIsZero * (1 - XIsZero) = 0; + } +} + +/* ANCHOR_END: all */ \ No newline at end of file diff --git a/test_data/asm/book/hello_world.asm b/test_data/asm/book/hello_world.asm new file mode 100644 index 000000000..9868140b5 --- /dev/null +++ b/test_data/asm/book/hello_world.asm @@ -0,0 +1,41 @@ +machine HelloWorld { + + degree 8; + + // this simple machine does not have submachines + + reg pc[@pc]; + reg X[<=]; + reg Y[<=]; + reg A; + + instr incr X -> Y { + Y = X + 1 + } + + instr decr X -> Y { + Y = X - 1 + } + + // an instruction to loop forever, as we must fill the whole execution trace + instr loop { + pc' = pc + } + + instr assert_zero X { + X = 0 + } + + constraints { + // in this machine, we do not add more constraints + } + + // the main function assigns the first prover input to A, increments it, decrements it, and loops forever + function main { + A <=X= ${ ("input", 0) }; + A <=Y= incr(A); + A <=Y= decr(A); + assert_zero A; + loop; + } +} \ No newline at end of file diff --git a/test_data/asm/book/simple_static.asm b/test_data/asm/book/simple_static.asm new file mode 100644 index 000000000..75feadb11 --- /dev/null +++ b/test_data/asm/book/simple_static.asm @@ -0,0 +1,22 @@ +machine SimpleStatic { + + degree 8; + + function power_4 x -> y { + } + + constraints { + col fixed latch = [0, 0, 0, 1]*; + col witness x; + col witness y; + + // initialise y to x at the beginning of each block + latch * (y' - x') = 0; + // x is unconstrained at the beginning of the block + + // x is constant within a block + (1 - latch) * (x' - x) = 0; + // y is multiplied by x at each row + (1 - latch) * (y' - x * y) = 0; + } +} \ No newline at end of file diff --git a/test_data/asm/book/write_register.asm b/test_data/asm/book/write_register.asm new file mode 100644 index 000000000..2815b4ec7 --- /dev/null +++ b/test_data/asm/book/write_register.asm @@ -0,0 +1,29 @@ +machine Machine { + + degree 8; + + reg pc[@pc]; + reg X[<=]; +// ANCHOR: declaration +reg A; +// ANCHOR_END: declaration + reg B; + + function main { +// ANCHOR: component +// write to A +A <=X= 1; +// A is 1 + +// read from A +B <=X= A; +// A is still 1 +// ANCHOR_END: component + + loop; + } + + instr loop { + pc' = pc + } +} \ No newline at end of file diff --git a/test_data/pil/fib_macro.pil b/test_data/pil/fib_macro.pil index cf19bbb6b..f17f40e4f 100644 --- a/test_data/pil/fib_macro.pil +++ b/test_data/pil/fib_macro.pil @@ -4,24 +4,31 @@ namespace Fibonacci(%N); constant %last_row = %N - 1; macro bool(X) { X * (1 - X) = 0; }; - macro is_nonzero(X) { match X { 0 => 0, _ => 1, } }; - macro is_zero(X) { 1 - is_nonzero(X) }; - macro is_equal(A, B) { is_zero(A - B) }; - macro is_one(X) { is_equal(X, 1) }; - macro ite(C, A, B) { is_nonzero(C) * A + is_zero(C) * B}; +// ANCHOR: expression_macro_definitions +macro is_nonzero(X) { match X { 0 => 0, _ => 1, } }; +macro is_zero(X) { 1 - is_nonzero(X) }; +macro is_equal(A, B) { is_zero(A - B) }; +macro is_one(X) { is_equal(X, 1) }; +macro ite(C, A, B) { is_nonzero(C) * A + is_zero(C) * B}; +macro one_hot(i, index) { ite(is_equal(i, index), 1, 0) }; +// ANCHOR_END: expression_macro_definitions - macro one_hot(i, index) { ite(is_equal(i, index), 1, 0) }; - - pol constant ISLAST(i) { one_hot(i, %last_row) }; +// ANCHOR: expression_macro_usage +pol constant ISLAST(i) { one_hot(i, %last_row) }; +// ANCHOR_END: expression_macro_usage pol commit x, y; - macro constrain_equal_expr(A, B) { A - B }; - macro force_equal_on_last_row(poly, value) { ISLAST * constrain_equal_expr(poly, value) = 0; }; +// ANCHOR: constraint_macro_definitions +macro constrain_equal_expr(A, B) { A - B }; +macro force_equal_on_last_row(poly, value) { ISLAST * constrain_equal_expr(poly, value) = 0; }; +// ANCHOR_END: constraint_macro_definitions // TODO would be easier if we could use "'" as an operator, // then we could write a "force_equal_on_first_row" macro, // and the macro would add a "'" to the parameter. - force_equal_on_last_row(x', 1); +// ANCHOR: constraint_macro_usage +force_equal_on_last_row(x', 1); +// ANCHOR_END: constraint_macro_usage force_equal_on_last_row(y', 1); macro on_regular_row(cond) { (1 - ISLAST) * cond = 0; }; diff --git a/test_data/pil/fixed_columns.pil b/test_data/pil/fixed_columns.pil new file mode 100644 index 000000000..1fac84ee5 --- /dev/null +++ b/test_data/pil/fixed_columns.pil @@ -0,0 +1,23 @@ +namespace Main(8); + +// ANCHOR: declare_and_define +col fixed ONES = [1]*; // this is valid +// col fixed ONES; // this is invalid +// ANCHOR_END: declare_and_define + +// ANCHOR: repetitions +// valid, as for a given total length, only one column fits this definition for a given `N` +col fixed A = [1, 2] + [3, 4]* + [5]; + +// invalid, as many columns fit this definition +// col fixed A = [1, 2]* + [3, 4]* +// ANCHOR_END: repetitions + +// ANCHOR: mapping +col fixed B(i) { i + 1 }; + +col fixed C(i) {match i { + 0 => 1, + _ => 0 +}}; +// ANCHOR_END: mapping \ No newline at end of file