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 handoptimized coprocessors when performance is critical
 Built in Rust 🦀
Contributing
powdr is free and open source. You can find the source code on GitHub. Issues and feature requests can be posted on the GitHub issue tracker.
License
The powdr source and documentation are released under the MIT License.
Installation
The only way to install powdr currently is to build it from source.
Prerequisites
You will need the Rust compiler and Cargo, the Rust package manager.
The easiest way to install both is with rustup.rs
.
On Windows, you will also need a recent version of Visual Studio, installed with the "Desktop Development With C++" Workloads option.
If you want to enable feature estarkpolygon
, you also need the following
runtime dependencies installed on the system:
gcc
nlohmannjson3dev
You will also need the following build time dependencies:
make
pkgconfig
libpqxxdev
(Ubuntu) libpqxx
(Arch Linux)nasm
Building
Using a single Cargo command (enable the Halo2 backend to use it with the cli):
cargo install git https://github.com/powdrlabs/powdr features halo2 powdrcli
Or, by manually building from a local copy of the powdr repository:
# clone the repository
git clone https://github.com/powdrlabs/powdr.git
cd powdr
# install powdrcli
cargo install features halo2 path ./cli
Hello World
Let's write a minimal VM and generate a SNARK!
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
}
instr assert_zero X {
X = 0
}
// the main function assigns the first prover input to A, increments it, decrements it, and loops forever
function main {
A <=X= ${ std::prover::Query::Input(0) };
A <== incr(A);
A <== decr(A);
assert_zero A;
return;
}
}
Then let's generate a proof of execution for the valid prover input 0
(since for 0 + 1  1 == 0
)
powdr pil test_data/asm/book/hello_world.asm field bn254 inputs 0 provewith halo2
We observe that a proof was created at hello_world_proof.bin
.
Now let's try for the invalid input 1
powdr pil test_data/asm/book/hello_world.asm field bn254 inputs 1 provewith halo2
We observe that witness generation fails, and no proof is created.
Setup & Verification
The example above omits some important steps in proof generation: Setup and
Verification key generation. Some proof systems, such as Halo2 (and other
SNARKs), require a Setup to be performed before the proof. Such Setup can be
specific to the program or universal, where its artifact is a binary usually
called parameters
or params
. STARKs do not require a previous Setup.
Another step required before the proof is computed is key generation. A
proving key
and a verification key
are generated taking into account the
constraints and potentially Setup parameters. The proving key
is used by the
prover to generate the proof, and the verification key is used by the verifier
to verify such proof. A single verification key can be used to verify any
number of different proofs for a given program.
Therefore, when computing a proof, it is important that the Setup parameters and the verification key are also available as artifacts.
Below we reproduce the same proof as in the example above, keeping the artifacts needed for verification:
First we run the Setup, where the number given must match the degree
of our
source file (degree 8
). The command below generates file params.bin
.
powdr setup 8 backend halo2 field bn254
We can now compute the verification key, output in vkey.bin
:
powdr verificationkey test_data/asm/book/hello_world.asm field bn254 backend halo2 params "params.bin"
The next command compiles and optimizes the given source, generating the file
hello_world_opt.pil
. It also computes both the fixed data and the witness
needed for the proof, stored respectively in hello_world_constants.bin
and
hello_world_commits.bin
.
powdr pil test_data/asm/book/hello_world.asm field bn254 force inputs 0
We can now generate the proof:
powdr prove test_data/asm/book/hello_world.asm field bn254 backend halo2 params "params.bin" vkey "vkey.bin"
The proof can be verified by anyone via:
powdr verify test_data/asm/book/hello_world.asm field bn254 backend halo2 vkey "vkey.bin" params "params.bin" proof "hello_world_proof.bin"
Note that CLI proof verification works analogously for eSTARK, without the setup step and using the Goldilocks field instead of Bn254.
Using powdr as a library
Besides the CLI, powdr can also be used as a Rust library. The powdr crate exposes internal crates and data structures needed to compile code, generate witnesses, and compute proofs.
Add powdr
to your crate's dependencies:
[dependencies]
powdr = { git = "https://github.com/powdrlabs/powdr", branch = "main" }
The following Rust code has the same workflow as our previous "Hello World" example. The full project can be found here, and as an example in the powdr crate. To run the example in the powdr repository, run:
cargo run example powdr_crate_usage
You can also enable logs to know what is happening internally:
RUST_LOG=info cargo run example powdr_crate_usage
use powdr::backend::BackendType; use powdr::pipeline::util::write_or_panic; use powdr::Bn254Field; use powdr::Pipeline; use std::fs; use std::io::BufWriter; fn main() { env_logger::init(); // Straightforward case let _proof = Pipeline::<Bn254Field>::default() .from_file("test_data/asm/book/hello_world.asm".into()) .with_prover_inputs(vec![0.into()]) .with_backend(BackendType::Halo2) .compute_proof() .unwrap(); // Stepbystep case // First we create the universal setup of size 8 let params_file = BufWriter::new(fs::File::create("params.bin").unwrap()); write_or_panic(params_file, writer { BackendType::Halo2 .factory::<Bn254Field>() .generate_setup(8, writer) .unwrap() }); // Configure a pipeline let mut pipeline = Pipeline::<Bn254Field>::default() .from_file("test_data/asm/book/hello_world.asm".into()) .with_prover_inputs(vec![0.into()]) .with_backend(BackendType::Halo2) .with_setup_file(Some("params.bin".into())); // Create the verification key let vkey_file = BufWriter::new(fs::File::create("vkey.bin").unwrap()); write_or_panic(vkey_file, w pipeline.export_verification_key(w)).unwrap(); // Add the verification key to a fresh pipeline and create a proof let mut pipeline_fresh = pipeline.clone().with_vkey_file(Some("vkey.bin".into())); let proof = pipeline_fresh.compute_proof().unwrap(); // Create yet another fresh pipeline only for proof verification let mut pipeline = pipeline .with_backend(BackendType::Halo2) .with_setup_file(Some("params.bin".into())) .with_vkey_file(Some("vkey.bin".into())); // Verify a proof created by a different Pipeline pipeline.verify(proof, &[vec![]]).unwrap(); }
CommandLine Help for powdr
This document contains the help content for the powdr
commandline program.
Command Overview:
powdr
↴powdr pil
↴powdr rust
↴powdr riscvasm
↴powdr prove
↴powdr verify
↴powdr verificationkey
↴powdr setup
↴powdr reformat
↴powdr optimizepil
↴
powdr
powdr CLI
Usage: powdr [OPTIONS] [COMMAND]
Subcommands:
pil
— Runs compilation and witness generation for .pil and .asm files. First converts .asm files to .pil, if needed. Then converts the .pil file to json and generates fixed and witness column data filesrust
— Compiles (nostd) rust code to riscv assembly, then to powdr assembly and finally to PIL and generates fixed and witness columns. Needsrustup target add riscv32imacunknownnoneelf
riscvasm
— Compiles riscv assembly to powdr assembly and then to PIL and generates fixed and witness columnsprove
—verify
—verificationkey
—setup
—reformat
— Parses and prints the PIL file on stdoutoptimizepil
— Optimizes the PIL file and outputs it on stdout
Options:

markdownhelp
Possible values:
true
,false

loglevel <LOG_LEVEL>
— Set log filter value [ off, error, warn, info, debug, trace ]Default value:
INFO
powdr pil
Runs compilation and witness generation for .pil and .asm files. First converts .asm files to .pil, if needed. Then converts the .pil file to json and generates fixed and witness column data files
Usage: powdr pil [OPTIONS] <FILE>
Arguments:
<FILE>
— Input file
Options:

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

o
,outputdirectory <OUTPUT_DIRECTORY>
— Output directory for the PIL file, json file and fixed and witness column dataDefault value:
.

w
,witnessvalues <WITNESS_VALUES>
— Path to a CSV file containing externally computed witness values 
i
,inputs <INPUTS>
— Commaseparated list of free inputs (numbers)Default value: ``

f
,force
— Force overwriting of PIL output fileDefault value:
false
Possible values:
true
,false

pilo
— Whether to output the pilo PIL objectDefault value:
false
Possible values:
true
,false

p
,provewith <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump

exportcsv
— Generate a CSV file containing the fixed and witness column values. Useful for debugging purposesDefault value:
false
Possible values:
true
,false

csvmode <CSV_MODE>
— How to render field elements in the csv fileDefault value:
hex
Possible values:
i
,ui
,hex

j
,justexecute
— Just execute in the RISCV/Powdr executorDefault value:
false
Possible values:
true
,false

c
,continuations
— Run a long execution in chunks (Experimental and not sound!)Default value:
false
Possible values:
true
,false
powdr rust
Compiles (nostd) rust code to riscv assembly, then to powdr assembly and finally to PIL and generates fixed and witness columns. Needs rustup target add riscv32imacunknownnoneelf
Usage: powdr rust [OPTIONS] <FILE>
Arguments:
<FILE>
— input rust code, points to a crate dir or its Cargo.toml file
Options:

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

i
,inputs <INPUTS>
— Commaseparated list of free inputs (numbers)Default value: ``

o
,outputdirectory <OUTPUT_DIRECTORY>
— Directory for output filesDefault value:
.

f
,force
— Force overwriting of files in output directoryDefault value:
false
Possible values:
true
,false

pilo
— Whether to output the pilo PIL objectDefault value:
false
Possible values:
true
,false

p
,provewith <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump

exportcsv
— Generate a CSV file containing the fixed and witness column values. Useful for debugging purposesDefault value:
false
Possible values:
true
,false

csvmode <CSV_MODE>
— How to render field elements in the csv fileDefault value:
hex
Possible values:
i
,ui
,hex

coprocessors <COPROCESSORS>
— Commaseparated list of coprocessors 
j
,justexecute
— Just execute in the RISCV/Powdr executorDefault value:
false
Possible values:
true
,false

c
,continuations
— Run a long execution in chunks (Experimental and not sound!)Default value:
false
Possible values:
true
,false
powdr riscvasm
Compiles riscv assembly to powdr assembly and then to PIL and generates fixed and witness columns
Usage: powdr riscvasm [OPTIONS] <FILES>...
Arguments:
<FILES>
— Input files
Options:

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

i
,inputs <INPUTS>
— Commaseparated list of free inputs (numbers)Default value: ``

o
,outputdirectory <OUTPUT_DIRECTORY>
— Directory for output filesDefault value:
.

f
,force
— Force overwriting of files in output directoryDefault value:
false
Possible values:
true
,false

pilo
— Whether to output the pilo PIL objectDefault value:
false
Possible values:
true
,false

p
,provewith <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump

exportcsv
— Generate a CSV file containing the fixed and witness column values. Useful for debugging purposesDefault value:
false
Possible values:
true
,false

csvmode <CSV_MODE>
— How to render field elements in the csv fileDefault value:
hex
Possible values:
i
,ui
,hex

coprocessors <COPROCESSORS>
— Commaseparated list of coprocessors 
j
,justexecute
— Just execute in the RISCV/Powdr executorDefault value:
false
Possible values:
true
,false

c
,continuations
— Run a long execution in chunks (Experimental and not sound!)Default value:
false
Possible values:
true
,false
powdr prove
Usage: powdr prove [OPTIONS] backend <BACKEND> <FILE>
Arguments:
<FILE>
— Input PIL file
Options:

d
,dir <DIR>
— Directory to find the committed and fixed valuesDefault value:
.

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

b
,backend <BACKEND>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump

proof <PROOF>
— File containing previously generated proof for aggregation 
vkey <VKEY>
— File containing previously generated verification key 
params <PARAMS>
— File containing previously generated setup parameters
powdr verify
Usage: powdr verify [OPTIONS] backend <BACKEND> proof <PROOF> vkey <VKEY> <FILE>
Arguments:
<FILE>
— Input PIL file
Options:

d
,dir <DIR>
— Directory to find the fixed valuesDefault value:
.

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

b
,backend <BACKEND>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump

proof <PROOF>
— File containing the proof 
publics <PUBLICS>
— Commaseparated list of public inputs (numbers)Default value: ``

vkey <VKEY>
— File containing the verification ley 
params <PARAMS>
— File containing the params
powdr verificationkey
Usage: powdr verificationkey [OPTIONS] backend <BACKEND> <FILE>
Arguments:
<FILE>
— Input PIL file
Options:

d
,dir <DIR>
— Directory to find the fixed valuesDefault value:
.

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

b
,backend <BACKEND>
— Chosen backendPossible values:
estarkstarky
,estarkdump

params <PARAMS>
— File containing previously generated setup parameters. This will be needed for SNARK verification keys but not for STARK
powdr setup
Usage: powdr setup [OPTIONS] backend <BACKEND> <SIZE>
Arguments:
<SIZE>
— Size of the parameters
Options:

d
,dir <DIR>
— Directory to output the generated parametersDefault value:
.

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254

b
,backend <BACKEND>
— Generate a proof with a given backendPossible values:
estarkstarky
,estarkdump
powdr reformat
Parses and prints the PIL file on stdout
Usage: powdr reformat <FILE>
Arguments:
<FILE>
— Input file
powdr optimizepil
Optimizes the PIL file and outputs it on stdout
Usage: powdr optimizepil [OPTIONS] <FILE>
Arguments:
<FILE>
— Input file
Options:

field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
This document was generated automatically by
clapmarkdown
.
asm
powdrasm is the higher level of abstraction in powdr. It allows defining Instruction Set Architectures (ISA) using virtual and constrained machines.
Modules
powdr exposes a module system to help organise and reuse code.
use my_module::Other as LocalOther;
// we can define a module at `./submodule.asm`
mod submodule;
// we can define a module at `./submodule_in_folder/mod.asm`
mod submodule_in_folder;
use submodule::Other as SubmoduleOther;
use submodule_in_folder::Other as FolderSubmoduleOther;
let zero: int = 0;
// we can also define modules inline
mod utils {
// Each module has a fresh symbol list. Every external symbol needs to be imported,
// even from the parent module.
use super::zero;
let one = zero + 1;
}
machine Main {
// use a machine from another module by relative path
my_module::Other a;
// use a machine from another module using a local binding
LocalOther b;
// use a machine from another module defined in a different file
SubmoduleOther c;
// use a machine from another module defined in a different directory
FolderSubmoduleOther c;
reg pc[@pc];
instr nothing = a.nothing;
instr also_nothing = b.nothing;
instr still_nothing = c.nothing;
function main {
nothing;
also_nothing;
still_nothing;
return;
}
}
mod my_module {
machine Other(latch, operation_id) {
operation nothing<0>;
col fixed latch = [1]*;
col fixed operation_id = [0]*;
}
}
Note that a module can't be called std
, as this name is reserved for an upcoming powdr standard library.
Declarations
Symbols can be defined via let <name> = <value>;
, or via let <name>: <type> = <value>;
if you want to
specify the type explicitly. The value is an arbitrary PILexpression.
For details, see the Declarations section in the PIL part.
Other symbols available in the current module can be accessed by name, but it is also possible to specify
full relative paths in the form of e.g. super::super::module_name::symbol
.
Here are some examples of how to define and use symbols:
mod utils {
// This defines a function by means of a lambda expression that
// computes the sum of an array of values. We fully specify its type.
let sum: int, int[] > int = len, arr match len {
0 => 0,
_ => arr[len  1] + sum(len  1, arr)
};
// A simple function that returns the input incremented by one,
// as an expression.
let incremented: expr > expr = x x + 1;
// This is a function that takes an expression as input and returns
// a constraint enforcing this expression increments by a certain value
// between rows.
// The type will be inferred here because `'` is only valid on `expr`.
let constrain_incremented_by = x, inc x' = x + inc;
}
machine Main {
// Machines create local scopes in the way functions create local scopes:
//  all symbols in the machine's module are available without prefix,
//  new symbols can be defined but are only available inside the machine.
reg A;
reg pc[@pc];
// This defines a witness column,
let x;
// and now we force it to stay unchanged.
utils::constrain_incremented_by(x, 0);
// We define an instruction that uses a complicated way to increment a register.
instr incr_a { A = utils::incremented(A) }
function main {
return;
}
}
Machines
Machines are the first main concept in powdrasm. They can currently be of two types: virtual or constrained.
Virtual 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
 a set of powdrpil statements
 a set of functions
 a set of submachines
An example of a simple dynamic machine is the following:
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
}
instr assert_zero X {
X = 0
}
// the main function assigns the first prover input to A, increments it, decrements it, and loops forever
function main {
A <=X= ${ std::prover::Query::Input(0) };
A <== incr(A);
A <== decr(A);
assert_zero A;
return;
}
}
Constrained machines
Constrained machines are a lowerlevel type of machine. They do not have registers, and instead rely on simple committed and fixed columns. They are used to implement handoptimized computation.
They are defined by:
 a degree, indicating the number of execution steps
 a set of operations
 an
operation_identifier
column, used to make constraints conditional over which function is called. It can be omitted with_
if the machine has at most one operation.  a
latch
column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations.  a set of submachines
 a set of links
An example of a simple constrained machine is the following:
machine SimpleStatic(latch, operation_id) {
degree 8;
operation power_4<0> x > y;
col fixed operation_id = [0]*;
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;
}
For more details on the powdrpil statements, check out the pil section of this book. Note that the parameters of the operation are columns defined in powdrpil statements.
Submachines
Machines can have submachines which they access by defining external instructions or links. They are declared as follows:
machine MySubmachine {
...
}
machine MyMachine {
MySubmachine my_submachine;
}
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 line to execute. The program counter behaves like a write register, 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:
reg A;
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.
// write to A
A <=X= 1;
// A is 1
// read from A
B <=X= A;
// A is still 1
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:
reg pc[@pc];
reg A;
instr assert_A_is_zero {
A = 0
}
function main {
assert_A_is_zero;
return;
}
However, if we want the instruction to accept any write register as input, we use an assignment register.
reg pc[@pc];
reg X[<=];
reg A;
instr assert_zero X {
X = 0
}
function main {
assert_zero A;
return;
}
Readonly registers
Readonly registers are used for function inputs. However, powdr creates them automatically based on functions arguments, so that they do not need to be declared explicitly.
Readonly registers are only mentioned for completeness here and are currently only used inside the compiler. We advise against using them.
Functions
Functions are the entry points to a virtual machine. They can be called from another machine or from the outside.
In this section, we describe functions with this simple virtual machine:
machine Machine {
degree 256;
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg Z[<=];
reg CNT;
reg A;
reg B;
// 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 as well as its double
instr square_and_double X > Y, Z {
Y = X * X,
Z = 2 * X
}
function main {
// initialise `A` to 2
A <=X= 2;
// initialise `CNT` to `3`
CNT <=X= 3;
start:
// if `CNT` is `0`, jump to `end`
jmpz CNT, end;
// decrement `CNT`
CNT <=X= CNT  1;
// get the square and the double of `A`
A, B <== square_and_double(A);
// jump back to `start`
jmp start;
end:
// check that `A == ((2**2)**2)**2`
assert_zero A  ((2**2)**2)**2;
// check that `B == ((2**2)**2)*2`
assert_zero B  ((2**2)**2)*2;
return;
}
// some superpowers on `X` to allow us to check if it's 0
col witness XInv;
col witness XIsZero;
XIsZero = 1  X * XInv;
XIsZero * X = 0;
XIsZero * (1  XIsZero) = 0;
}
Function inputs and outputs
Function inputs and outputs are not supported yet
Statements
Labels
Labels allow referring to a location in a function by name.
start:
Assignments
Assignments allow setting the values of some write registers to the values of some expressions expression using assignment registers.
CNT <=X= 3;
If the righthand side of the assignment is an instruction, assignment registers can be inferred and are optional:
A, B <== square_and_double(A);
This will be inferred to be the same as A, B <=Y, Z= square_and_double(A);
from the definition of the instruction:
instr square_and_double X > Y, Z {
Y = X * X,
Z = 2 * X
}
Instructions
Instructions which do not return outputs can be used as statements.
assert_zero A  ((2**2)**2)**2;
Expressions
Field element literals
Field element literals are signed elements of the prime field.
CNT <=X= 3;
Registers and columns
Registers can be used as expressions, with the exception of assignment registers.
CNT <=X= CNT  1;
Instructions
Instructions which return outputs can be used as expressions.
A, B <== square_and_double(A);
Instructions
Instructions are declared as part of a powdr virtual machine. Their inputs and outputs are assignment registers as well as labels. Once defined, they can be called by any function in 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 powdrpil constraints to activate when the instruction is called
External instructions
An external instruction delegates its implementation to a function/operation from a submachine. When called, the inputs and outputs of the declared instruction are mapped into a call to the submachine function.
Assume we have a submachine with a single operation add
:
machine SubMachine(latch, operation_id) {
col witness operation_id;
col fixed latch = [1]*;
operation add<0> x, y > z;
col witness x;
col witness y;
col witness z;
z = y + x;
}
An external instruction calling into this operation can be declared as follows:
SubMachine submachine;
instr add X, Y > Z = submachine.add; //  trivial usage, equivalent to:
// instr add X, Y > Z = submachine.add X, Y > Z;
The lefthand side of the definition declares the local instruction and which assignment registers are used in its inputs and outputs. It describes how the instruction is used. The righthand side of the definition specifies the call to the external operation, with its inputs and outputs. All assignment registers on the lefthand side must be used in the call to the external operation.
In the previous example, parameters of the instruction match exactly with how the target operation should be called, and the righthand parameters can thus be omitted. The following example shows more complex usages of external instructions:
machine Main {
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg Z[<=];
reg A;
reg B;
reg C;
SubMachine submachine;
instr add X, Y > Z = submachine.add; //  trivial usage, equivalent to:
// instr add X, Y > Z = submachine.add X, Y > Z;
instr add_to_A X, Y = submachine.add X, Y > A';//  output to a regular register
instr addAB > X = submachine.add A, B > X; //  inputs from regular registers
instr addAB_to_C = submachine.add A, B > C'; //  inputs and output from regular registers
instr addAB_to_A = submachine.add A, B > A'; //  reusing an input register as output
instr sub X, Y > Z = submachine.add Y, Z > X; //  swapping input/output
// any expression can be used in the external call
instr add5 X > Z = submachine.add X, 3+2 > Z; //  literal expression as argument
col fixed STEP(i) { i };
instr add_current_time_step X > Z = submachine.add X, STEP > Z;//  columns can be referenced
let arr = [1,2,3,4,5]; //  functions can be used
instr add_arr_sum X > Z = submachine.add X, std::array::sum(arr) > Z;
instr assert_eq X, Y { X = Y }
function main {
A <== add(2, 3);
assert_eq A, 5;
add_to_A 6, 7;
assert_eq A, 13;
A <== sub(6, 5);
assert_eq A, 1;
B <=X= 20;
C <== addAB();
assert_eq C, 21;
A <=X= 2;
B <=X= 3;
addAB_to_C;
assert_eq C, 5;
A <=X= 33;
B <=X= 44;
addAB_to_A;
assert_eq A, 77;
A <== add5(2);
assert_eq A, 7;
A <== add_arr_sum(3);
assert_eq A, 18;
// Note that the result of this operation depends on when it executed
A <== add_current_time_step(42);
B <== add_current_time_step(42);
assert_eq B  A, 1;
return;
}
}
Note that external instructions cannot currently link to functions of the same machine: they delegate computation to a submachine.
Operations
Operations enable a constrained machine to expose behavior to the outside. If a machine has a single operation, it can simply be declared with its name and parameters:
machine Add(latch, _) {
// operation name, with column names as inputs and outputs
operation add a, b > c;
col fixed latch = [1]*;
col witness a;
col witness b;
col witness c;
// constraint "implementing" the operation
c = a + b;
}
The parameters of the operation (inputs and outputs) must be columns declared in the machine.
If a machine exposes more than one operation, the machine itself needs an operation id column (op_id
in the following).
Then, each operation needs to be declared with its own unique operation id:
// machine declaration must include an operation id column name
machine AddSub(latch, op_id) {
// each operation has its own unique operation id
operation add<0> a, b > c;
operation sub<1> a, b > c;
col fixed latch = [1]*;
// it also needs to be declared as a column
col witness op_id;
col witness a;
col witness b;
col witness c;
// constraint "implementing" both operations, depending on `op_id`
c = (1  op_id) * (a + b) + op_id * (a  b);
}
The actual behavior of an operation is defined by the machine constraints on the columns used as inputs and outputs.
Links
Links enable a constrained machine to call into another machine. They are defined by a boolean flag and a call to the operation, where inputs and outputs are expressions.
machine Add4(latch, operation_id) {
Add adder;
operation add4<0> x, y, z, w > r;
//  on every row (the boolean flag is `1`)
//  constrain the values of `x`, `y`, and `n` so that `n = adder.add(x, y)`
link 1 => adder.add x, y > n;
//  constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
link 1 => adder.add z, w > m;
//  constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
link 1 => adder.add m, n > r;
col fixed operation_id = [0]*;
col fixed latch = [1]*;
col witness x;
col witness y;
col witness z;
col witness w;
col witness r;
col witness m;
col witness n;
}
machine Add(latch, _) {
// operation name, with column names as inputs and outputs
operation add a, b > c;
col fixed latch = [1]*;
col witness a;
col witness b;
col witness c;
// constraint "implementing" the operation
c = a + b;
}
A link is only active in rows where the boolean flag is 1
(all lines in the above example).
Whenever it is active, the columns mapped as inputs and outputs are constrained by the operation implementation.
PIL
powdrpil is the lower level of abstraction in powdr. It is strongly inspired by Polygon zkEVM PIL. We refer to the Polygon zkEVM PIL documentation and document deviations from the original design here.
Declarations
Powdrpil allows the same syntax to declare various kinds of symbols. This includes constants, fixed columns, witness columns and even higherorder functions. It deduces the symbol kind from the type of the symbol and the way the symbol is used.
Symbols can be declared using let <name>;
and they can be declared and defined
using let <name> = <value>;
, where <value>
is an expression. The type of the symbol
can be explicitly specified using let <name>: <type>;
and let <name>: <type> = <value>;
.
Symbols with a generic type can be defined using let<TV1, TV1, ..> <name>: <type> = <value>;
,
where the TV
are newly created type variables that can be used in the type.
This syntax can be used for constants, fixed columns, witness columns and even (higherorder) functions that can transform expressions. The kind of symbol is deduced by its type and the way the symbol is used:
 Symbols without a value are witness columns or arrays of witness columns. Their type can be omitted. If it is given, it must be
col
orcol[k]
.  Symbols defined with a value and type
col
(orcol[k]
) are fixed columns (or arrays of fixed columns).  Symbols defined with a value and type
expr
(orexpr[k]
) are intermediate columns (or arrays of intermediate columns).  Everything else is a "generic symbol" that is not a column.
Examples:
#![allow(unused)] fn main() { // This defines a integer constant. We can omit the type when it is used // somewhere that constrains its type. Since it is not used below, // we have to specify `: int` (another option would be `fe`, field element). let rows: int = 2**16; // This defines a fixed column that contains the row number in each row. // Only symbols whose type is "col" are considered fixed columns. let step: col = i i; // Here, we have a witness column, the do not need an explicit `: col`. let x; // This functions defines a fixed column where each cell contains the // square of its row number. let square: col = x x*x; // This is a generic function that computes the sum of an array // given its length. // It is not stored as a column. // If it is used in a constraint, it has to be evaulated, while // columns must be used symbolically. let<T: Add + FromLiteral> sum: T[], int > T = a, len match len { 0 => 0, _ => sum(a, len  1) + a[len  1], }; // This is a constraint that uses the `sum` function: sum([x, step], 2) = 0; }
Expressions
Depending on the context, powdr allows more or less features for expressions.
Inside values for declarations, you can use a very flexible language which includes many different operators, function calls, lambda functions, tuple types, statement blocks, match statements and others.
In statements and expressions that are required to evaluate to constraints / polynomial identities, only a much more restrictive language can be used. Expressions in that language are called Algebraic Expressions. While you can use the full language everywhere, in the context of a constraint, the result after function evaluation and constant propagation has to be an algebraic expression.
Generic Expressions
The expression language allows the following operators, in order of increased precedence:
 lambda functions:
params body
. Examples:i i
(the identity),a, b a + b
(sum) 
 logical or&&
 logical and<
,<=
,==
,!=
,>=
,>
 comparisons
 bitwise or^
 bitwise xor&
 bitwise and<<
,>>
 left and right shift+
,
 addition and subtraction (binary operator)*
,/
,%
 multiplication, division and modulo**
 exponentiation
,!
 numerical and logical negation (unary operators, prefix)'
 "next row" operator (suffix)[]
,()
 array index access and function calls
Elementary expressions are
 number literals (integers)
 string literals, written in double quotes, e.g.
"hello"
 array literals written in square brackets, e.g.
[1, 2, 3]
 tuples, having at least two elements, e.g.
(1, "abc")
 statement blocks (see below)
 match expressions (see below).
 if expressions (see below).
Parentheses are allowed at any point to force precedence.
Lambda Functions
The only way to declare a function in pil is by assigning a lambda function to a symbol.
Example:
#![allow(unused)] fn main() { let x = i i + 1; }
If you want to specify the types of parameters or return values explicitly, you have to do it on the symbol, you cannot do it on the parameters:
#![allow(unused)] fn main() { let x: int > int = i i + 1; }
It is possible to use patterns in the function parameters:
#![allow(unused)] fn main() { let y: (int, int), int > int = (i, j), _ i + j; }
If you use patterns, they have to be irrefutable, which means that the pattern has to be able to match any value of the given type.
Statement Blocks
A {
}
delimited block can be used everywhere where an expression is expected.
It has the form { <statement> ; <statement> ; ... ; <expression> }
,
i.e. a sequence of statements followed by an expression.
The statements can either be expressions (f();
, only inside constr
functions)
or let statements: let x = ...;
/ let x;
The value of the statement block is the value of the final expression.
Example:
#![allow(unused)] fn main() { let plus_one_squared = x { let y = x + 1; y * y }; }
Let statements with value can be used everywhere, they just bind an expression to a local variable and allow to avoid repeating the expression. You can use patterns for the left hand side of let statements to destructure values.
Example:
#![allow(unused)] fn main() { let f = i (i / 2, i % 2); let (quot, rem) = f(7); }
The second let statement will create two local variables x
and y
. You can also ignore values using
the _
pattern element. For details, please see the patterns section.
Let statements without value (let x;
) create a new witness column and are only allowed inside constr
functions.
Similarly, an expression at statement level (e.g. x * (x  1) = 0;
) can be used to create new constraints that are added to the global constraint set
and this can only be done inside a constr
functions.
Note that you can always create constraints and return them from a function, even in pure function.
Example:
#![allow(unused)] fn main() { let constrain_to_bool: expr > constr = x { x * (x  1) = 0 }; }
Match Expressions
Match expressions take the form match <value> { <pattern 1> => <value 1>, <pattern 2> => <value 2>, _ => <default value> }
,
with an arbitrary number of match arms.
The semantics are that the first match arm where the pattern equals the value after the match
keyword is evaluated.
Patterns can be used to destructure more complex data types and to capture values inside new local variables. For more details, please see the patterns section.
Example:
#![allow(unused)] fn main() { let fib = i match i { 0 => 1, 1 => 1, _ => fib(i  2) + fib(i  1), }; }
If Expressions
If expressions take the form if <condition> { <true value> } else { <false value> }
, where the "else" part is not optional.
If the condition evaluates to true
, then <true value>
is evaluated, otherwise <false value>
is.
Example:
#![allow(unused)] fn main() { let is_seven = i if i == 7 { 1 } else { 0 }; }
Algebraic Expressions
For constraints (or functions called at a place where a constraint is expected), the expression syntax is limited: After evaluating function calls and performing constant propagation, the resulting expression has to be an "algebraic expression". These are restricted in the following way:
 You can freely use the operators
+
,
,*
.  The operator
**
must have a number as exponent.  The operator
[i]
must have a column name on the lefthand side and the index must be a number.  The operator
'
must have a column or[i]
on the lefthandside.  No other operators are allowed.
Arbitrary parentheses are allowed.
The following example illustrates how you can still use the generic language:
#![allow(unused)] fn main() { namespace Main(16); // Returns folder(...folder(folder(0, f(0)), f(1)) ..., f(length  1)) // This is a generic function. let<T1, T2> fold: int, (int > T1), T2, (T2, T1 > T2) > T2 = length, f, initial, folder match length { 0 => initial, _ => folder(fold(length  1, f, initial, folder), f(length  1)) }; // returns f(0) + f(1) + ... + f(length  1) let sum = length, f fold(length, f, 0, acc, e acc + e); // This function takes an algebraic expression (a column or expression // involving columns) and returns an identity that forces this expression // to equal 20. Note that `=` is not an assignment but creates an identity constraint. let equals_twenty: expr > constr = x x = 20; // This declares an array of 16 witness columns. col witness wit[16]; // This expression has to evaluate to an identity, but we can still use // higher order functions and all the flexibility of the language. // The subexpression `sum(16, i wit[i])` evaluates to the algebraic // expression "wit[0] + wit[1] + ... + wit[15]", which is then // turned into the identity by `equals_twenty` // wit[0] + wit[1] + ... + wit[15] = 20. equals_twenty(sum(16, i wit[i])); // We constrained the sum to equal twenty, but there is no unique solution // to that constraint. In order to fully constrain the system, we need to // add something more: The first fifteen columns should all be one. // returns [f(0), f(1), ..., f(length  1)] let make_array = length, f fold(length, f, [], acc, e acc + [e]); // If an expression evaluates to an array of constraints, all the // constraints in the array are added to the system. make_array(15, i wit[i] = 1); }
Constr and Query Functions
Every function in PIL is either a pure, a constr
or a query
function. They are denoted by
... ...
constr ... ...
query ... ...
Inside constr
functions, it is possible to create new witness columns
and add constraints to the set of constraints (see the Statement Blocks section for details).
Inside query
functions, it is possible to evaluate the value of a column on the "current" row
using the std::prover::eval
function.
Both actions require a certain context to be available, which is not the case for example when the values of a fixed column are computed.
A query
function can only be used in the query or hint part of a witness column while constr
functions
can only be evaluated in the constraint part of a namespace or machine.
You can define and call new constr
functions inside a constr
function and you can call and define
new query
functions inside query
functions, but as soon as you enter a pure function, this is not possible any more.
Examples:
#![allow(unused)] fn main() { // This function creates and returns a new witness column. let new_wit = constr  { let x; x }; // Queries the current value of a column and returns its square. let square_of = query x { let v = std::prover::eval(x); v * v }; // Creates a new witness column, constrains it to be boolean and returns it. let new_bool = constr x { let x = new_wit(); x * (x  1) = 0; x }; // This is a pure function that only returns a constraint, but does not add it // to the global set of constraints. let constrain_to_bool: expr > constr = x x * (x  1) = 0; }
Patterns
Patterns are a way to destructure or match certain values. They are valid in match
arms,
function parameters or left hand sides of let statements in blocks.
A pattern is built up in from the following components:
_
 the "catch all" pattern that matches anythingx
 for an identifierx
, matches anything and assigns the value to the new local variable of that namek
 for a literal numberk
, matches the exact number, either as anint
or afe
k
 for a literal numberk
, matches the exact negated number, either as anint
or afe
"text"
 for a string literal, matches the exact string literal as astring
(a, b, c)
 for a tuple, matches a tupletyped value if all the components match[a, b, c
]  for an array, matches array values of exactly the same length if all the components match[a, .., b, c]
 matches an array that has an initial segment ofa
and ends inb, c
. The omitted part can be empty.X::Y(a, b)
 for an enum variantX::Y
, matches that enum variant if all the enum fields match.
Patterns can be nested, which means that the components of tuple and array patterns are themselves patterns.
Some examples:
#![allow(unused)] fn main() { // This pattern destructures the first function parameter. let f: (int, int), int > int = (a, b), c (a + c, b); // Matches a tuple, ignores the second component. let (x, _) = f((6, 7), 3); // The match statement typically uses patterns to check for certain values // but it can also destructure and create new local variables valid inside // the match arm. let t = match (x, f((1, x), 2)) { (0, _) => 0, (1, _) => 7, (_, y) => y, _ => 9 }; let head: int[] > int = x match x { // Matches the first element of a nonempty array and binds it to a local variable. [a, ..] => a, [] => std::check::panic("Called 'head' on empty array."), }; }
Note that PIL does not check that patterns in a match expression are exhaustive.
(Ir)refutability
A pattern is refutable if there is a value of the correct type that the pattern does not match.
An example is the pattern 7
since it does not match all integers, or the patten [x, ..]
, because it
does not match the empty array.
Refutable patterns are fine in match arms, because if the pattern does not match, the evaluator will just continue trying the next match arm, but they are disallowed in let statements and in function parameters, because there we do not have the option of "trying the next arm".
Example:
#![allow(unused)] fn main() { let f: int > int[] = i match i { // This is a refutable pattern, but it is fine // because we will try the next match arm. 0 => [], _ => f(i  1) + [i], }; // This pattern does not match all `int[]`, because it requires a length // of at least one. let [x, ..] = f(8); }
The following patterns are refutable:
 all integer literal patterns
 all string literal patterns
 enum variant patterns
 tuple patterns that have refutable components
 array patterns that are not
[..]
.
Variable patterns and _
are always irrefutable.
Types
The powdrpil language has the following types:
bool
int
(integer)fe
(field element)string
 tuple
 array
 function type
expr
(expression)constr
(constraint)!
("bottom" or "unreachable" type) enum types
The
col
type is special in that it is only used for declaring columns, but cannot appear as the type of an expression. See Declaring and Referencing Columns for details.
Powdrpil performs HindleyMilner type inference. This means that, similar to Rust, the type of a symbol does not always have to be specified. The compiler will try to find a type for every symbol depending both on the value assigned to the symbol and on the context the symbol is used in. It is an error if the type is not uniquely determined.
Symbols can have a generic type, but in those cases, you have to explicitly specify the generic type. Such declarations can require type variables to satisfy certain trait bounds. Currently, only builtin traits are supported (see the next section).
Literal numbers do not have a specific type, they can be either int
, fe
or expr
(the types that
implement the FromLiteral
trait), and their type can also stay generic until evaluation.
Example
The following snippet defines a function that takes a value of a generic type and returns the value incremented by one.
The type bounds on the generic type are FromLiteral
and Add
. The type checker will complain if we do not specify
the type bounds. The bound Add
is required because we use the +
operator in the function and FromLiteral
is needed
because we use the literal 1
as a value of that type.
#![allow(unused)] fn main() { let<T: FromLiteral + Add> add_one: T > T = i i + 1; }
Declaring and Referencing Columns
A symbol declared to have type col
(or col[k]
) is a bit special:
If you assign it a value, that value is expected to have type int > fe
or int > int
(or an array thereof).
This allows the simple declaration of a column let byte: col = i i & 0xff;
without complicated conversions.
The integer value is converted to a field element during evaluation, but it has to be nonnegative and less than
the field modulus.
If you reference such a symbol, the type of the reference is expr
.
A byte constraint is as easy as { X } in { byte }
, since the expected types in plookup columns is expr
.
The downside is that you cannot evaluate columns as functions. If you want to do that, you either have to assign
a copy to an int > int
symbol: let byte_f: int > int = i i & 0xff; let byte: col = byte_f;
.
Or you can use the builtin function std::prover::eval
if you want to do that inside a prover query or hint.
All other symbols use their declared type both for their value and for references to these symbols.
Builtin Traits
FromLiteral
:
Implemented by int
, fe
, expr
. The type of a number literal needs to implement FromLiteral
.
Add
: Implemented by int
, fe
, expr
, T[]
, string
. Used by <T: Add> +: T, T > T
(binary plus).
Sub
:
Implemented by int
, fe
, expr
. Used by <T: Sub> : T, T > T
(binary minus).
Neg
:
Implemented by int
, fe
, expr
. Used by <T: Neg> : T > T
(unary minus).
Mul
:
Implemented by int
, fe
, expr
. Used by <T: Mul> *: T, T > T
(binary multiplication).
Pow
:
Implemented by int
, fe
, expr
, Used by <T: Pow> **: T, int > T
(exponentiation).
Ord
:
Implemented by int
. Used by <T: Ord> op: T, T, > bool
for op
being one of <
, >
, <=
, >=
.
Eq
:
Implemented by int
, fe
, expr
. Used by <T: Eq> op: T, T > bool
for op
being one of ==
, !=
.
List of Types
Bool
Type name: bool
Booleans are the results of comparisons. They allow the following operators:
&&
: logical conjunction
: logical disjunction!
: logical negation
Shortcircuiting is not performed when evaluating boolean operators.
This means that (1 == 1)  std::check::panic("reason")
will cause a panic abort.
Integer
Type name: int
Integers in powdrpil have unlimited size. Array index requires an integer and row indices (for example the input to a fixed column defined through a function) are also integers.
Integer implements FromLiteral
, which means that literal numbers can be used in contexts where int
is expected.
Integers allow the following operators, whose result is always an integer:
+
: addition
: subtraction (also unary negation)*
: multiplication/
: integer division rounding towards zero, division by zero results in a runtime error**
: exponentiation, the exponent needs to be nonnegative and fit 32 bits, otherwise a runtime error is triggered%
: remainder after division, (for signed arguments,p % q == sgn(p) * abs(p) % abs(q)
), remainder by zero results in a runtime error&
: bitwise conjunction
: bitwise disjunction^
: bitwise exclusive or<<
: bitwise shift left, the shift amount needs to be nonnegative and fit 32 bits, otherwise a runtime error is triggered>>
: bitwise shift right, the shift amount needs to be nonnegative and fit 32 bits, otherwise a runtime error is triggered
The exponentiation operator on field elements requires a nonnegative integer as exponent.
It has the signature **: fe, int > fe
.
In addition, the following comparison operators are allowed, the result is a boolean:
<
: less than<=
: less or equal==
: equal!=
: not equal>=
: greater or equal>
: greater than
Field Element
Type name: fe
Field elements are elements of a particular but unspecified prime field. The exact field is
chosen when powdr is run. The modulus of that field can be accessed via std::field::modulus()
.
Field elements are the values stored in (fixed and witness) columns. Arithmetic inside constraints (algebraic expressions) is also always finite field arithmetic.
The type fe
implements FromLiteral
, which means that literal numbers can be used in contexts where fe
is expected.
If the literal number is not less than the field modulus, a runtime error is caused.
Field elements allow the following operators, where the result is always a field element:
+
: finite field addition
: finite field subtraction (also unary negation)*
: finite field multiplication
There is also an exponentiation operator **
on field elements. It requires the exponent
to be a nonnegative integer and thus has the signature **: fe, int > fe
. If the exponent is negative, a runtime error is triggered. 0**0
is defined as 1
.
The following comparison operators exist for field elements, whose result is a boolean:
==
: equality comparison!=
: inequality comparison
Since finite fields do not have an inherent order as integers do, if you want to
compare them using <
, you have to first convert them to integers.
String
Type name: string
String literals are written as "string content"
. They are mainly used for debugging or
documentation purposes, since they cannot occur in constraints.
They allow the following operators:
+
: string concatenation
Tuple
Type name: (..., ..., ...)
Tuples are complex types that are composed from other types, either zero or two or more. There is no tuple type with a single element ((int)
is the same as int
).
The empty tuple type is written as ()
.
Examples include (int, int)
(a pair of integers) and ((fe[], int), ())
(a tuple consisting of a tuple that contains an array of field elements and an integer
and an empty tuple).
Tuples values are constructed using parentheses: (1, 2)
constructs the tuple that consists of
a one and a two.
Tuples do not allow any operators.
Array
Type name: _[]
Arrays are statically or dynamicallysized collections of elements each of the same type
denoted for example as int[]
(a dynamicallysized array of integers) or int[2]
(an array of integers with static size two).
Array values can be constructed inline using [1, 2]
(the array containing the
two elements one and two).
The builtin function std::array::len
can be used to retrieve the length of an array (statically or dynamically sized)
and the elements of an array a
can be accessed using a[0]
, a[1]
, etc.
The type checker currently only knows dynamicallysized arrays, which means that it does not compare the sizes of staticallysized array types.
Arrays allow the following operators:
+
: array concatenation_[]
: array index access, the index needs to be a nonnegative integer that is less than the length of the array, otherwise a runtime error is triggered
Function
Type name: T1, T2, ..., Tn > T0
Function type names are for example denoted as int, fe > int
or > int
.
Note that (int, fe) > int
is a function that takes a single tuple as parameter
while int, fe > int
takes two parameters of type integer and field element.
Functions can be constructed using the lambda expression notation.
For example x, y x + y
returns a function that performs addition.
The lambda expression  7
is a function that returns a constant (has no parameters).
Lambda functions can capture anything in their environment and thus form closures.
Functions allow the following operators:
_(...)
: function evaluation
Powdrpil is usually sideeffect free, but there are some builtin functions that have
sideeffects:
These are std::debug::print
and std::check::panic
and all functions that call them.
Expressions are eagerly evaluated from left to right.
Expression
Type name: expr
Expressions are the elements of the algebraic expressions used in constraints.
References to columns have type expr
and expr
also implements FromLiteral
,
which means that literal numbers can be used in contexts where expr
is expected.
Example:
#![allow(unused)] fn main() { let x: col; let y: col; let f: > expr =  x + y; let g =  7; f() = g(); }
The first two lines define the witness columns x
and y
.
The next two lines define the utility functions f
and g
.
The function f
adds the two columns x
and y
symbolically  it essentially returns the expression x + y
.
The last line is at statement level and it is expected that it evaluates to a constraint, in this case, a polynomial identity.
Because of that, g
is inferred to have type > expr
, which is compatible with the literal 7
.
Since expressions are built from abstract column references, applying operators does not perform any operations but instead constructs an abstract expression structure / syntax tree.
Expressions allow the following operators, which always construct new expressions:
+
: additive combination of expressions
: subtractive combination of expressions (also unary negation)*
: multiplicative combination of expressions**
: exponential combination of an expression with an integer constant'
: reference to the next row of a column, can only be applied directly to columns and only once
The operator =
on expressions constructs a constraint (see below);
Constraints
Type name: constr
Any evaluation of an expression at statement level needs to result in a constraint, or in an array of constraints.
Generally, constraints include polynomial identities, plookups, permutations and connection identities.
The only constraint currently constructible in the powdrpil language are polynomial identities.
These can be constructed from expressions by applying the =
operator as in x = 7
.
Constraints do not allow any operators.
Bottom Type
Type name: !
The bottom type essentially is the return type of a function that never returns, which currently only happens
if you call the panic
function. The bottom type is compatible with any other type, which means
that you can call the panic
function in any context.
Enum Types
Enums are userdefined types that can hold different named alternatives plus data. An enum type has a (namespaced) name that uniquely identifies it and is also used to reference the type.
Enums are declared in the following way:
#![allow(unused)] fn main() { enum EnumName { Variant1, Variant2(), Variant3(int), Variant4(int, int[], EnumName), } }
The variants must have unique names inside the enum and they can optionally take additional data. Each variant declares a type constructor function that can be used to create a value of the enum:
#![allow(unused)] fn main() { let a = EnumName::Variant1; let b = EnumName::Variant2(); let c = EnumName::Variant3(3); let d = EnumName::Variant4(1, [2, 3], EnumName::Variant1); }
Recursive enums are allowed.
Enums do not allow any operators.
Fixed columns
powdrpil requires the definition of fixed columns at the time of declaration.
For example:
col fixed ONES = [1]*; // this is valid
// col fixed ONES; // this is invalid
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
powdrpil 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.
// 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]*
Mappings
A column can be seen as a mapping from integers to field elements. In this context, different functions are supported:
col fixed B(i) { i + 1 };
col fixed C(i) {match i {
0 => 1,
_ => 0
}};
Builtins
Functions
The following functions are built into the compiler. They need to be defined to be accessible, but their assigned value is ignored and the compiler replaces it with the following.
Array length
#![allow(unused)] fn main() { let<T> std::array::len: T[] > int }
Returns the length of an array as an integer.
Example:
#![allow(unused)] fn main() { let x = [1, 2, 3]; let l = std::array::len(x); // returns 3 }
Panic
#![allow(unused)] fn main() { let std::check::panic: string > ! }
Aborts evaluation and prints its argument as error message as a sideeffect of its evaluation.
Since panic
does not generate a constraint, it cannot be used
for correctness checks. The verifier only checks constraints / identities and
thus ignores anything that could lead to a panic. Panic should only
be used to check proverinternal consistency.
Example:
#![allow(unused)] fn main() { let secp256k1_inverse = x if x == std::convert::fe(0) { panic!("Tried to compute the inverse of zero.") } else { std::math::ff::inverse(x, secp256k1_modulus); }; }
Conversions
#![allow(unused)] fn main() { let<T: FromLiteral> std::convert::fe: T > fe }
This function is meant to be used on int
, but also works on fe
for convenience.
It converts a nonnegative integer less than the field modulus to a field element. Causes a type error in all other cases.
If the argument is already a field element, it is returned without modification.
#![allow(unused)] fn main() { let<T: FromLiteral> std::convert::int: T > int }
This function is meant to be used on fe
, but also works on int
for convenience.
It converts a field element to an integer.
If the argument is already an integer, it is returned without modification.
#![allow(unused)] fn main() { let<T: FromLiteral> std::convert::expr: T > expr }
This function is meant to be used on int
, but also works on fe
and expr
for convenience.
It converts an integer to an expr.
If the argument is already an expr, it is returned without modification.
Printing
#![allow(unused)] fn main() { let std::debug::print: string > constr[] }
This function takes a string and prints it on the standard output during evaluation, as a sideeffect of its evaluation.
This function should only be used for debugging purposes.
Note that the function does not append a newline at the end.
It returns an empty constr
array so that it can be used at statement level where
constraints are expected.
Modulus
#![allow(unused)] fn main() { let std::field::modulus: > int }
Returns the current field's modulus as an integer.
Example:
#![allow(unused)] fn main() { // Inside a machine if std::field::modulus() != 2**64  2**32 + 1 { panic!("This machine can only be used with the Goldilocks field.") } else { [] }; }
Evaluate
#![allow(unused)] fn main() { let std::prover::eval: expr > fe }
Evaluates a column (potentially with '
applied) on the current row.
This function can only be used for prover queries or hints and it only
works on columns (and those with '
applied). This means you cannot use
std::prover::eval(x + 1)
.
In the following example, the column x
is evaluated in a prover
hint that returns the square root of a number.
Example:
#![allow(unused)] fn main() { machine Sqrt { let sqrt_hint: fe > fe = x match x { // Code to compute the square root of x goes here. }; col witness x; col witness y(i) query std::prover::Query::Hint(sqrt_hint(std::prover::eval(x))); y * y = x; }} }
Challenges
#![allow(unused)] fn main() { let std::prover::challenge: int, int > expr }
Constructs a challenge object, essentially asking the verifier for a random number.
The first argument is the proof stage and the second is the identifier of the challenge.
If you want two challenges to be different, you have to choose different IDs.
Operators
The following operators are supported by powdrpil with their respective signatures.
let<T: Add> +: T, T > T
let<T: Sub> : T, T > T
let<T: Neg> : T > T
let<T: Mul> *: T, T > T
let /: int, int > int
let %: int, int > int
let<T: Pow> **: T, int > T
let <<: int, int > int
let >>: int, int > int
let &: int, int > int
let : int, int > int
let ^: int, int > int
let<T: Ord> <: T, T > bool
let<T: Ord> <=: T, T > bool
let<T: Ord> >: T, T > bool
let<T: Ord> >=: T, T > bool
let<T: Ord> <: T, T > bool
let<T: Eq> ==: T, T > bool
let<T: Eq> !=: T, T > bool
let =: expr, expr > constr
let ': expr > expr
let : bool, bool > bool
let &&: bool, bool > bool
let !: bool > bool
Frontends
While any frontend VM can be implemented in powdrasm, powdr comes with several frontends for popular instruction set architectures.
RISCV
A RISCV frontend for powdr is already available.
How to run the RustRISCV example
# Install the riscv target for the rust compiler
rustup target add riscv32imacunknownnoneelf
# Run the compiler. It will generate files in /tmp/.
# i specifies the prover witness input (see below)
powdr rust riscv/tests/riscv_data/sum o /tmp f i 10,2,4,6
The example Rust code verifies that a supplied list of integers sums up to a specified value.
#![no_std] extern crate alloc; use alloc::vec::Vec; use powdr_riscv_runtime::input::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 userdefined 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.
Valida
A Valida front end for powdr is under development. If you are interested, feel free to reach out!
EVM
An EVM frontend for powdr is under development. If you are interested, feel free to reach out!
Backends
powdr aims to have full flexibility when it comes to generating proofs and comes with a few builtin backends to get started with zkVMs.
Halo2
powdr supports the PSE fork of halo2 with the bn254 field.
eSTARK
powdr supports the eSTARK proof system with the Goldilocks field, implemented by the starky library from eigenzkvm.
Architecture
powdr applies a number of steps in order to reduce a powdrasm program into PIL.
We provide a high level overview of these steps.
┌────────────┐ ┌──────────┐
│ │ │ │
powdrasm │ │ AIR graph │ │ PIL
───────────►│ compiler ├───────────┤ linker ├──────►
│ │ │ │
│ │ │ │
└────────────┘ └──────────┘
Compiler
In this section, we explain how the powdr compiler reduces a program made of virtual and constrained machines to a set of AIRs.
Virtual machine reduction
The first step is to reduce virtual machines to constrained machines. This step is run on all machines and does not affect constrained machines. As a result of this step, for each machine:
 Local instructions are reduced to constraints
 External instructions are reduced to links
 Functions are reduced to operations
Block enforcement
Block enforcement applies on constrained machines. It makes sure that the operation_id
is constant within each machine block.
AIR generation
At this point, all machines contain only:
 an optional degree
 constraints
 links to other machines
 operations
Let's define AIR as a data structure with only these elements.
Starting from the main machine's type, we create a tree of AIR objects by traversing its submachines, recursively instantiating each machine as an AIR. Let's define the AIR tree as the resulting tree.
Linker
A linker is used to turn an AIR tree into a single PIL file. The linking process operates in the following way:
 Create an empty PIL file
 Start from the main AIR. If it defines a degree, let
main_degree
be that value. If it does not, letmain_degree
be1024
.  For each AIR
 Create a new namespace in the PIL file
 If a degree is defined, check that it equals
main_degree
and error out if it does not. If no degree is defined, set the degree tomain_degree
 Add the constraints to the namespace
 Turn the links into lookups and add them to the namespace
The result is a monolithic AIR where:
 each machine instance is a namespace
 all namespaces have the same degree
 links between instances are encoded as lookup identities
More flexible approaches to the linking process will be explored in the future, such as allowing for machine instances of different degrees.