Document not found (404)
+This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +This URL is invalid, sorry. Please use the navigation bar or search to continue.
+ +In this section, we explain how the powdr compiler reduces a program made of virtual and constrained machines to a set of AIRs.
+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:
+Block enforcement applies on constrained machines. It makes sure that the operation_id is constant within each machine block.
At this point, all machines contain only:
+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.
+ +powdr applies a number of steps in order to reduce a powdr-asm program into PIL.
+We provide a high level overview of these steps.
+ ┌────────────┐ ┌──────────┐
+ │ │ │ │
+ powdr-asm │ │ AIR graph │ │ PIL
+───────────►│ compiler ├───────────┤ linker ├──────►
+ │ │ │ │
+ │ │ │ │
+ └────────────┘ └──────────┘
+A linker is used to turn an AIR tree into a single PIL file. +The linking process operates in the following way:
+optional_main_degree be its optional degree.optional_main_degreeThe result is a monolithic AIR where:
+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 PIL-expression.
+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 with degree: 4 {
+ // 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;
+ }
+}
+Field element literals are signed elements of the prime field.
+ CNT <=X= 3;
+Registers can be used as expressions, with the exception of assignment registers.
+ CNT <=X= CNT - 1;
+Instructions which return outputs can be used as expressions.
+ A, B <== square_and_double(A);
+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 with degree: 16 {
+ 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 are not supported yet
+
Labels allow referring to a location in a function by name.
+ start:
+Assignments allow setting the values of some write registers to the values of some expressions expression using assignment registers.
+ CNT <=X= 3;
+If the right-hand 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 which do not return outputs can be used as statements.
+ assert_zero A - ((2**2)**2)**2;
+powdr-asm is the higher level of abstraction in powdr. It allows defining Instruction Set Architectures (ISA) using virtual and constrained machines.
+ +Instructions are declared as part of a powdr virtual machine. +Once defined, they can be called by any function in this machine. +An instruction is composed of:
+A local instruction is the simplest type of instruction. +It is called local because its behavior is defined by a set of constraints over registers and columns of the machine it is defined in.
+instr add X, Y -> Z {
+ X + Y = Z
+}
+Instructions may also delegate all or part of their implementation to functions/operations in submachines.
+Each link in an instruction defines the inputs and outputs of a call to a specific function/operation in a submachine.
Assume we have a submachine with a single operation add:
machine SubMachine with
+ latch: latch,
+ operation_id: 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 instruction calling into this operation can be declared as follows:
+ SubMachine submachine;
+
+ instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
+In the previous example, only assignment registers (instruction inputs and outputs) were used to call the submachine.
+The following example shows more complex usage of link calls:
machine Main with degree: 32 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg Z[<=];
+ reg A;
+ reg B;
+ reg C;
+
+ SubMachine submachine;
+
+ instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
+ instr add_to_A X, Y link => A' = submachine.add(X, Y);// - output to a regular register
+ instr addAB -> X link => X = submachine.add(A, B); // - inputs from regular registers
+ instr addAB_to_C link => C' = submachine.add(A, B); // - inputs and output from regular registers
+ instr addAB_to_A link => A' = submachine.add(A, B); // - reusing an input register as output
+ instr sub X, Y -> Z link => X = submachine.add(Y, Z); // - swapping input/output
+ // expressions can also be used as call parameters
+ instr add5 X -> Z link => Z = submachine.add(X, 3+2); // - literal expression as argument
+ col fixed STEP(i) { i };
+ instr add_current_time_step X -> Z link => Z = submachine.add(X, STEP);// - machine columns can be referenced
+ let arr = [1,2,3,4,5]; // - functions can be used
+ instr add_arr_sum X -> Z link => Z = submachine.add(X, std::array::sum(arr));
+
+ 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 (STEP column)
+ A <== add_current_time_step(42);
+ B <== add_current_time_step(42);
+ assert_eq B - A, 1;
+
+ return;
+ }
+}
+A single instruction can activate multiple links, and may also include a set of constraints.
+Furthermore, each link can be activated conditionally, based on a given boolean flag:
machine Main with degree: 16 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg Z[<=];
+ reg W[<=];
+ reg A;
+ col witness B;
+ col witness C;
+
+ SubMachine submachine;
+
+ // multiple links can be activated by a single instruction,
+ // witness columns can be used for temporary values,
+ // and additional constraints can be used
+ instr double_then_mul X, Y -> Z
+ link => B = submachine.add(X, X)
+ link => C = submachine.add(Y, Y)
+ {
+ Z = B * C
+ }
+
+ // links activated conditional on a boolean flag
+ instr add_or_sub W, X, Y -> Z
+ link if W => Z = submachine.add(X, Y)
+ link if (1 - W) => Z = submachine.sub(X, Y);
+
+ instr assert_eq X, Y { X = Y }
+
+ function main {
+ A <== double_then_mul(3, 2);
+ assert_eq A, 24;
+
+ A <== add_or_sub(1, 3, 2);
+ assert_eq A, 5;
+ A <== add_or_sub(0, 3, 2);
+ assert_eq A, 1;
+
+ return;
+ }
+}
+++ +Note that links cannot currently call functions from the same machine: they delegate computation to a submachine.
+
Links enable a constrained machine to call into another machine. +They are defined by a call to an operation, where inputs and outputs are expressions. +An optional boolean flag restricts the rows in which the link is active. +Links without a boolean flag are active in every row.
+machine Add4 with
+ latch: latch,
+ operation_id: operation_id
+{
+ Add adder;
+
+ operation add4<0> x, y, z, w -> r;
+
+ // Links without a flag are active on every row.
+ // - constrain the values of `x`, `y`, and `n` so that `n = adder.add(x, y)`
+ link => n = adder.add(x, y);
+ // - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
+ link => m = adder.add(z, w);
+ // - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
+ link => r = adder.add(m, n);
+
+ 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 with
+ latch: 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;
+}
+If a boolean flag is given, the link is only active in rows where the flag evaluates to 1.
+Whenever a link is active, the columns mapped as inputs and outputs are constrained by the operation implementation.
+The following example demonstrates how to use links with flags.
col fixed odd_row = [0,1]*;
+
+link if odd_row => z = submachine.foo(x, y); // active on odd rows only
+link if (1 - odd_row) => z = submachine.bar(x, y); // active on even rows only
+Machines are the first main concept in powdr-asm. They can currently be of two types: virtual or constrained.
+Dynamic machines are defined by:
+An example of a simple dynamic machine is the following:
+machine HelloWorld with 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 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:
+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.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.An example of a simple constrained machine is the following:
+machine SimpleStatic with
+ degree: 8,
+ latch: latch,
+ operation_id: operation_id
+{
+ 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 powdr-pil statements, check out the pil section of this book. Note that the parameters of the operation are columns defined in powdr-pil statements.
+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;
+}
+Machines can also receive submachines as construction parameters. +A machine passed in as an argument can be accessed in the same way as locally declared submachines:
+machine MachineWithParam(subm: MySubmachine) {
+ // `subm` can be accessed as a submachine
+ ...
+}
+
+machine MyMachine {
+ MySubmachine my_submachine;
+ // `my_submachine` is passed to `another_submachine` as a construction argument
+ MachineWithParam another_submachine(my_submachine);
+}
+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 with degree: 8 {
+ // 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 d;
+
+ reg pc[@pc];
+
+ instr nothing link => a.nothing();
+ instr also_nothing link => b.nothing();
+ instr still_nothing link => c.nothing();
+ instr nothing_again link => d.nothing();
+
+ function main {
+ nothing;
+ also_nothing;
+ still_nothing;
+ nothing_again;
+ return;
+ }
+}
+
+mod my_module {
+ machine Other with
+ latch: latch,
+ operation_id: 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 the powdr standard library.
Similar to Rust, any reference that cannot be resolved is looked up once more in std::prelude.
+This module exposes basic types and values such as Option, true and false.
+This means that you can use Option anywhere without prefix.
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 with
+ latch: 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 with
+ latch: latch,
+ operation_id: 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.
+ +Registers are central to a machine. powdr supports a few types of registers:
+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 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 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;
+}
+Read-only 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.
+++ +Read-only registers are only mentioned for completeness here and are currently only used inside the compiler. We advise against using them.
+
powdr supports the eSTARK proof system with the Goldilocks field, +implemented by the starky library from eigen-zkvm.
+ +powdr supports the PSE fork of halo2 with the bn254 field.
+ +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.
+ +powdrThis document contains the help content for the powdr command-line program.
Command Overview:
+powdr↴powdr pil↴powdr prove↴powdr verify↴powdr verification-key↴powdr export-verifier↴powdr setup↴powdr reformat↴powdr optimize-pil↴powdrpowdr CLI to compile powdr-asm and powdr-pil programs
+Usage: powdr [OPTIONS] [COMMAND]
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 filesprove —verify —verification-key —export-verifier —setup —reformat — Parses and prints the PIL file on stdoutoptimize-pil — Optimizes the PIL file and outputs it on stdout--log-level <LOG_LEVEL> — Set log filter value [ off, error, warn, info, debug, trace ]
Default value: INFO
powdr pilRuns 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>
<FILE> — Input file--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-o, --output-directory <OUTPUT_DIRECTORY> — Output directory for the PIL file, json file and fixed and witness column data
Default value: .
-w, --witness-values <WITNESS_VALUES> — Path to a CSV file containing externally computed witness values
-i, --inputs <INPUTS> — Comma-separated list of free inputs (numbers)
Default value: ``
+-f, --force — Force overwriting of PIL output file
Default value: false
--pilo — Whether to output the pilo PIL object
Default value: false
-p, --prove-with <PROVE_WITH> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--params <PARAMS> — File containing previously generated setup parameters
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--export-csv — Generate a CSV file containing the fixed and witness column values. Useful for debugging purposes
Default value: false
--csv-mode <CSV_MODE> — How to render field elements in the csv file
Default value: hex
Possible values: i, ui, hex
powdr proveUsage: powdr prove [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the committed and fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--proof <PROOF> — File containing previously generated proof for aggregation
--vkey <VKEY> — File containing previously generated verification key
--vkey-app <VKEY_APP> — File containing the verification key of a proof to be verified recursively
--params <PARAMS> — File containing previously generated setup parameters
powdr verifyUsage: powdr verify [OPTIONS] --backend <BACKEND> --proof <PROOF> --vkey <VKEY> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--proof <PROOF> — File containing the proof
--publics <PUBLICS> — Comma-separated list of public inputs (numbers)
Default value: ``
+--vkey <VKEY> — File containing the verification key
--params <PARAMS> — File containing the params
powdr verification-keyUsage: powdr verification-key [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Chosen backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--params <PARAMS> — File containing previously generated setup parameters. This will be needed for SNARK verification keys but not for STARK
--vkey-app <VKEY_APP> — File containing the verification key of a proof to be verified recursively
powdr export-verifierUsage: powdr export-verifier [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Chosen backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--params <PARAMS> — File containing previously generated setup parameters. This will be needed for SNARK verification keys but not for STARK
--vkey <VKEY> — File containing previously generated verification key
powdr setupUsage: powdr setup [OPTIONS] --backend <BACKEND> <SIZE>
<SIZE> — Size of the parameters-d, --dir <DIR> — Directory to output the generated parameters
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
powdr reformatParses and prints the PIL file on stdout
+Usage: powdr reformat <FILE>
<FILE> — Input filepowdr optimize-pilOptimizes the PIL file and outputs it on stdout
+Usage: powdr optimize-pil [OPTIONS] <FILE>
<FILE> — Input file--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
+This document was generated automatically by
+clap-markdown.
+
Besides the Hello World examples, you are encouraged to check out these more +complex and real-world use cases:
+ + +While any frontend VM can be implemented in powdr-asm, powdr comes with several frontends for popular instruction set architectures.
+ +A RISCV frontend for powdr is already available.
+# Install the riscv target for the rust compiler
+rustup target add riscv32imac-unknown-none-elf
+# Run the powdr-rs compiler. It will generate files in ./output/
+powdr-rs compile riscv/tests/riscv_data/sum -o output
+# Run powdr to compile powdr-asm to powdr-PIL and generate the witness
+# -i specifies the prover witness input (see below)
+powdr pil output/sum.asm -o output -f -i 10,2,4,6
+The example Rust code verifies that a supplied list of integers sums up to a specified value.
+{{#include ../../../riscv/tests/riscv_data/sum/src/lib.rs}}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.
ZK-continuations can be used to make proofs for unbounded execution traces of
+Rust programs, where the trace is split into many different chunks. A proof
+is computed for each chunk, and all proofs can be combined with
+recursion/aggregation until a single proof remains.
For the details of how memory is handled in the ZK-continuations case please +see this.
+powdr-rs has experimental support to ZK-continuations, which can be used as follows.
Let's use as example test many chunks from the riscv crate:
{{#include ../../../riscv/tests/riscv_data/many_chunks/src/lib.rs}}First we need to compile the Rust code to powdr-asm:
+powdr-rs compile riscv/tests/riscv_data/many_chunks
+Now we can use podwr's RISCV executor to estimate how many cycles are needed:
+powdr-rs execute many_chunks.asm
+...
+Execution trace length: 750329
+By default, powdr-RISCV uses chunks of length 2^18. That means we will need at +least 3 chunks.
+For the continuations case, the compiled assembly code looks different because
+of the external memory commitments, so we need to recompile using the
+--continuations flag:
powdr-rs compile riscv/tests/riscv_data/many_chunks --continuations
+We can now execute the program with continuations enabled:
+powdr-rs -- execute many_chunks.asm --continuations
+The output now is longer:
+Running chunk 0...
+Building bootloader inputs for chunk 0...
+26 unique memory accesses over 2 accessed pages: {31, 32}
+Estimating the shutdown routine to use 1362 rows.
+Bootloader inputs length: 1285
+Simulating chunk execution...
+Initial memory root hash: 44cd91c12033ad4c6a6b19793b73f1a66d99a0e0bf63494c12ceb1f451ec9452
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 260782
+Validating chunk...
+Bootloader used 3134 rows.
+ => 257648 / 262144 (98%) of rows are used for the actual computation!
+Proved 257647 rows.
+
+Running chunk 1...
+Building bootloader inputs for chunk 1...
+0 unique memory accesses over 0 accessed pages: {}
+Estimating the shutdown routine to use 42 rows.
+Bootloader inputs length: 83
+Simulating chunk execution...
+Initial memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 262102
+Validating chunk...
+Bootloader used 62 rows.
+ => 262040 / 262144 (99%) of rows are used for the actual computation!
+Proved 262039 rows.
+
+Running chunk 2...
+Building bootloader inputs for chunk 2...
+2 unique memory accesses over 1 accessed pages: {31}
+Estimating the shutdown routine to use 702 rows.
+Bootloader inputs length: 684
+Simulating chunk execution...
+Initial memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 232057
+Validating chunk...
+Bootloader used 1610 rows.
+ => 259832 / 262144 (99%) of rows are used for the actual computation!
+Done!
+The step above is informational, but for the proofs we also need the full witness:
+powdr-rs execute many_chunks.asm --witness
+The witnesses are written in ./chunk_0/commits.bin, ./chunk_1/commits.bin
+and ./chunk_2/commits.bin.
Now that we have the witnesses for all chunks we can use powdr (instead of
+powdr-rs) to compute proofs for each chunk:
powdr prove many_chunks.asm -d chunk_0 --backend estark-dump
+powdr prove many_chunks.asm -d chunk_1 --backend estark-dump
+powdr prove many_chunks.asm -d chunk_2 --backend estark-dump
+These proofs are mock proofs for the sake of the example, but any backend +should work here.
+After generating real proofs, each specific proof system can be used for the +recursion/aggregation parts. A follow-up tutorial on that is coming soon.
+ +Let's write a minimal VM and generate a proof!
+machine HelloWorld with 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;
+ }
+}
+Let's generate a proof of execution for the valid prover input 0 (since 0 + 1 - 1 == 0)
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2
+We observe that several artifacts are created in the current directory:
+hello_world.pil: the compiled PIL file.hello_world_opt.pil: the optimized PIL file.hello_world_constants.bin: the computed fixed columns which only have to be computed once per PIL file.hello_world_commits.bin: the computed witness which needs to be computed for each proof.hello_world_proof.bin: the ZK proof!++Note that the output directory can be specified with option
+-o|--output, and.is used by default.
Now let's try for the invalid input 1:
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 1 --prove-with halo2
+In this case witness generation fails, and no proof is created.
+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 verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --params "params.bin"
+++The command above can read previously generated constants from the directory +specified via
+-d|--dir, where.is used by default. If the constants are not present +it computes them before generating the verification key.
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.
+
Another aspect that was omitted in this example is the fact that this proof +uses a Poseidon transcript and cannot be verified in a cheap way on Ethereum, +even though we can verify it efficiently via powdr. +There are two ways to enable verification on Ethereum:
+This example is a variation of the previous Hello World, +targeting verification on Ethereum. In this example we will cover how to +generate proofs directly using a Keccak transcript instead of the Poseidon +transcript of the previous example, which will enable us to verify proofs +onchain. There are almost no differences from the CLI perspective.
+machine HelloWorld with 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;
+ }
+}
+Since the following command creates a proof, a Solidity verifier, and verifies
+the proof on the EVM, we need to have solc available in the system. One easy
+way to install it is by using svm.
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "snark_single" -f --params params.bin
+The extra parameter --backend-options snark_single tells powdr to produce a single
+SNARK that uses Keccak. The option -f forces overwriting the compiled files
+that have been generated before, which is useful if you are running the examples
+on the same directory as the previous example.
When the a proof is generated, it is verified on a simulated EVM transaction as well!
+Verifying SNARK in the EVM...
+We can observe again that a proof was created at hello_world_proof.bin.
Now we can generate a Solidity verifier, using the same setup (params) as the
+previous example:
powdr export-verifier test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_single" --params params.bin
+A Solidity file verifier.sol is generated. You can verify the same proof that
+we just generated by passing it to the contract together with the public inputs
+(which we have not used so far).
++ +Note that the more complex your VM is, the larger the verifier contract will be. In some cases, it might exceed Ethereum's contract size limit. You can mitigate that by using proof recursion on proofs that use Poseidon transcripts. See the next section for details.
+
This example is yet another variation of the previous Hello World on Ethereum +example, still targeting verification on Ethereum but supporting more complex +VMs. As noted in the previous section, complex VMs can lead to large +Solidity verifiers that exceed the contract size limit on Ethereum. One +solution to that problem is to create proofs using the Poseidon transcript, as +we did in the first example, and then use proof +recursion to create a proof that we know we will be able to verify on Ethereum.
+A recursive SNARK works by generating a proof for a circuit that verifies
+another proof. The circuit we are using here to prove our initial proof
+recursively is PSE's snark-verifier. This circuit is large enough
+to be able to prove complex programs that were proven initial with the Poseidon
+transcript, like our first example. Because of that our aggregation setup
+params and verification key are going to be larger than before and take
+longer to compute. The good news are that (i) we can use a pre-computed setup
+from a previous ceremony, and (ii) the verification key only has to be computed
+once per program.
First, we need a setup of "size" 2^22. This is the maximum execution trace length of the recursion circuit.
+You can generate it using the command line below, or download a pre-computed +one here.
+This will take a couple minutes if you decide to compute it yourself:
+powdr setup 4194304 --backend halo2 --field bn254
+We can re-use the new large params.bin for both initial and recursive proofs.
+Let's start by re-computing our Poseidon proof like in the first example,
+but using our new setup file:
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "poseidon" -f --params params.bin
+This generates the initial proof hello_world_proof.bin.
+We'll also need a verification key:
powdr verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "poseidon" --params params.bin
+Let's verify the proof with our fresh verification key to make sure we're on the right track:
+powdr verify test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "poseidon" --params params.bin --vkey vkey.bin --proof hello_world_proof.bin
+In order to avoid confusion between the application's artifacts +that we've just generated and the recursion one we're going to generate +later, let's rename them:
+mv vkey.bin vkey_app.bin
+mv hello_world_proof.bin hello_world_proof_app.bin
+We can now generate a verification key for the Halo2 circuit that verifies our proofs recursively. This might take up to a minute.
+powdr verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey-app vkey_app.bin
+++Note that this verification key can only be used to verify recursive proofs that verify other proofs using the application's key
+vkey_app.bin.
We can now generate the recursive proof (can take 3 or more minutes and use 28gb RAM):
+powdr prove test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin --vkey-app vkey_app.bin --proof hello_world_proof_app.bin
+We have a proof! Note that the proof contents have two fields, proof and
+publics. The proof object contains the binary encoding of the proof
+points, and the publics object contains the public accumulator limbs that we
+need in order to verify the recursive proof.
We can now verify the proof, using the publics object as input (your numbers will likely be different):
powdr verify test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin --proof hello_world_proof_aggr.bin --publics "269487626280642378794,9378970522278219882,62304027188881225691,811176493438944,234778270138968319485,3212529982775999134,171155758373806079356,207910400337448,188563849779606300850,155626297629081952942,194348356185923309508,433061951018270,34598221006207900280,283775241405787955338,79508596887913496910,354189825580534"
+Since the goal of the recursive proof was to be able to verify it on Ethereum, let's do that!
+powdr export-verifier test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin
+A Solidity verifier is created in verifier.sol. The contract expects an array of the accumulators' limbs followed by a tightly packed proof, where each accumulator limb uses 32 bytes, and there is no function signature.
Note that this verifier can be used to verify any recursive proof that verifies exactly one Poseidon proof of the given circuit.
+ +powdr is a modular compiler stack to build zkVMs. +It is ideal for implementing existing VMs and experimenting with new designs with minimal boilerplate.
+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.
+The powdr source and documentation are released under the MIT License.
+ +The only way to install powdr currently is to build it from source.
+There are two binaries, powdr and powdr-rs.
The former can compile powdr-asm files to powdr-PIL, as well as generate +witnesses and proofs.
+The latter compiles Rust crates to powdr-asm via RISCV, and can execute +powdr-asm code with given inputs.
+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 estark-polygon, you also need the following
+runtime dependencies installed on the system:
gccnlohmann-json3-devYou will also need the following build time dependencies:
+makepkg-configlibpqxx-dev (Ubuntu) | libpqxx (Arch Linux)nasmUsing a single Cargo command (enable the Halo2 backend to use it with the cli):
+cargo install --git https://github.com/powdr-labs/powdr --features halo2 powdr-cli
+Or, by manually building from a local copy of the powdr repository:
+# clone the repository
+git clone https://github.com/powdr-labs/powdr.git
+cd powdr
+# install powdr-cli
+cargo install --features halo2 --path ./cli
+Using a single Cargo command:
+cargo install --git https://github.com/powdr-labs/powdr powdr-rs-cli
+Or, by manually building from a local copy of the powdr repository:
+# clone the repository
+git clone https://github.com/powdr-labs/powdr.git
+cd powdr
+# install powdr-rs-cli
+cargo install --path ./cli-rs
+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.
+let<T> std::array::len: T[] -> intReturns the length of an array as an integer.
+Example:
+let x = [1, 2, 3];
+let l = std::array::len(x); // returns 3let std::check::panic: string -> !Aborts evaluation and prints its argument as error message as a +side-effect 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 prover-internal consistency.
Example:
+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);
+ };let<T: FromLiteral> std::convert::fe: T -> feThis function is meant to be used on int, but also works on fe for convenience.
It converts a non-negative 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.
+let<T: FromLiteral> std::convert::int: T -> intThis 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.
+let<T: FromLiteral> std::convert::expr: T -> exprThis 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.
+let std::debug::print: string -> Constr[]This function takes a string and prints it on the standard output during evaluation, as a side-effect 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.
let std::field::modulus: -> intReturns the current field's modulus as an integer.
+Example:
+// Inside a machine
+if std::field::modulus() != 2**64 - 2**32 + 1 {
+ panic!("This machine can only be used with the Goldilocks field.")
+} else {
+ []
+};let std::prover::eval: expr -> feEvaluates 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:
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;
+
+}}let std::prelude::challenge: int, int -> exprConstructs 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.
+let std::prover::degree: -> intReturns the current number of rows / the length of the witness columns, also +known as the degree.
+let std::prover::set_hint: expr, (int -> std::prover::Query) -> ()This function can be used to set a "query function" for a witness column. +Query functions are used during witness generation and allow witness column cells +to receive a value even though they are not uniquely constrained by the constraints.
+The first argument must be a witness column and the function can only be called +once per witness column.
+There are some types that are not proper built-in types (in the sense that they are not treated +specially in the type system), but they are defined in the +standard library and are referenced by built-in functions.
+The type Constr or more specifically, std::prelude::Constr is the type of a constraint.
+Expressions at statement level are required to evaluate either to Constr or Constr[].
It is defined as follows:
+enum Constr {
+ /// A polynomial identity.
+ Identity(expr, expr),
+ /// A lookup constraint with selectors.
+ Lookup((Option<expr>, Option<expr>), (expr, expr)[]),
+ /// A permutation constraint with selectors.
+ Permutation((Option<expr>, Option<expr>), (expr, expr)[]),
+ /// A connection constraint (copy constraint).
+ Connection((expr, expr)[])
+}The operator = can be applied on two expr values and results in a Constr::Identity.
The type implements no traits and allows no operators.
+The following operators are supported by powdr-pil 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
+Powdr-pil allows the same syntax to declare various kinds of symbols. This includes +constants, fixed columns, witness columns and even higher-order 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 (higher-order) +functions that can transform expressions. The kind of symbol is deduced by its type and whether +it is has a value:
+col or col[k].col (or col[k]) are fixed columns (or arrays of fixed columns).inter (or inter[k]) are intermediate columns (or arrays of intermediate columns).Examples:
+ // 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 = 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;Name lookup is performed as follows:
+Lookup is performed starting from the current namespace, going up to the root component by component
+where the first match is used. If all lookups fail, a last attempt is done
+inside the std::prelude namespace.
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.
+The expression language allows the following operators, in order of increased precedence:
+|params| body. Examples: |i| i (the identity), |a, b| a + b (sum)|| - logical or&& - logical and<, <=, ==, !=, >=, > - comparisons and = - identity operator| - 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 callsElementary expressions are
+"hello"[1, 2, 3](1, "abc")Parentheses are allowed at any point to force precedence.
+The only way to declare a function in pil is by assigning a lambda function to a symbol.
+Example:
+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:
+let x: int -> int = |i| i + 1;It is possible to use patterns in the function parameters:
+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.
+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:
+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:
+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:
+let constrain_to_bool: expr -> Constr = |x| x * (x - 1) = 0;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:
+let fib = |i| match i {
+ 0 => 1,
+ 1 => 1,
+ _ => fib(i - 2) + fib(i - 1),
+};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:
+let is_seven = |i| if i == 7 { 1 } else { 0 };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:
++, -,*.** must have a number as exponent.[i] must have a column name on the left-hand side and the index must be a number.' must have a column or [i] on the left-hand-side.Arbitrary parentheses are allowed.
+The following example illustrates how you can still use the generic language:
+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 sub-expression `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);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:
+// 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 bool_constraint: expr -> Constr = |x| x * (x - 1) = 0;powdr-pil 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.
powdr-pil supports a basic language to define the value of constant columns using:
+[1, 2, 3][1, 2]*[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]*
+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
+}};
+powdr-pil 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.
+ +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 identifier x, matches anything and assigns the value to the new local variable of that namek - for a literal number k, matches the exact number, either as an int or a fe-k - for a literal number k, matches the exact negated number, either as an int or a fe"text" - for a string literal, matches the exact string literal as a string(a, b, c) - for a tuple, matches a tuple-typed 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 of a and ends in b, c. The omitted part can be empty.X::Y(a, b) - for an enum variant X::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:
+// This pattern de-structures 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 non-empty 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.
+
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:
+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:
+[..].Variable patterns and _ are always irrefutable.
The powdr-pil language has the following types:
+boolint (integer)fe (field element)stringexpr (expression)! ("bottom" or "unreachable" type)++In addition, there are the
+colandintertypes, but they are special in that +they are only used for declaring columns, but cannot appear as the type of an expression. +See Declaring and Referencing Columns for details.
Powdr-pil performs Hindley-Milner 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 built-in 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.
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.
let<T: FromLiteral + Add> add_one: T -> T = |i| i + 1;A symbol declared to have type col or inter (or col[k] / inter[k]) is a bit special:
These symbols represent columns in the arithmetization and the types of values that can be assigned to +such symbols and the references to the symbols are different from their declared type.
+If you assign a value to a col symbol, that value is expected to have type int -> fe or int -> int (or an array thereof).
+This allows the simple declaration of a fixed 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 non-negative and less than
+the field modulus.
Symbols of declared type col are fixed (those with value) or witness columns (those without value).
A symbol of declared type inter is an intermediate column. You can assign it a value of type expr.
+The idea of an intermediate column is that it is an algebraic expression of other columns that you do
+not want to compute multiple times.
++Note that if you use
+let x: expr = a * b;, the symbolxis just a name in the PIL environment, +this will not create an intermediate column. The difference betweeninterandexprin this case +is that if you uselet x: inter = ..., the expression might not be inlined into constraints (depending on the backend), +while if you uselet x: expr = ..., it will always be inlined.
If you reference a symbol of declared type inter or col, the type of the reference is expr (or 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 built-in 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.
+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 ==, !=.
Type name: bool
Booleans are the results of comparisons. They allow the following operators:
+&&: logical conjunction||: logical disjunction!: logical negationShort-circuiting is not performed when evaluating boolean operators.
+This means that (1 == 1) || std::check::panic("reason") will cause a panic abort.
Type name: int
Integers in powdr-pil 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 non-negative 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&: bit-wise conjunction|: bit-wise disjunction^: bit-wise exclusive or<<: bit-wise shift left, the shift amount needs to be non-negative and fit 32 bits, otherwise a runtime error is triggered>>: bit-wise shift right, the shift amount needs to be non-negative and fit 32 bits, otherwise a runtime error is triggeredThe exponentiation operator on field elements requires a non-negative 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 thanType 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 multiplicationThere is also an exponentiation operator ** on field elements. It requires the exponent
+to be a non-negative 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 comparisonSince 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.
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 concatenationType 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.
+Type name: _[]
Arrays are statically or dynamically-sized collections of elements each of the same type
+denoted for example as int[] (a dynamically-sized 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 built-in 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 dynamically-sized arrays, which means that it does not compare the sizes of statically-sized array types.
+Arrays allow the following operators:
++: array concatenation_[]: array index access, the index needs to be a non-negative integer that is less than the length of the array, otherwise a runtime error is triggeredType 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 evaluationPowdr-pil is usually side-effect free, but there are some built-in functions that have
+side-effects:
+These are std::debug::print and std::check::panic and all functions that call them.
+Expressions are eagerly evaluated from left to right.
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:
+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 onceThe operator = on expressions constructs a constraint (see [../builtins#Constr]).
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.
Enums are user-defined 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:
+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:
+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.
+ +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/powdr-labs/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::number::buffered_write_file;
+use powdr::Bn254Field;
+use powdr::Pipeline;
+
+use std::path::Path;
+
+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, None)
+ .compute_proof()
+ .unwrap();
+
+ // Step-by-step case
+
+ // First we create the universal setup of size 8
+ buffered_write_file(Path::new("params.bin"), |writer| {
+ BackendType::Halo2
+ .factory::<Bn254Field>()
+ .generate_setup(8, writer)
+ .unwrap()
+ })
+ .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, None)
+ .with_setup_file(Some("params.bin".into()));
+
+ // Create the verification key
+ buffered_write_file(Path::new("vkey.bin"), |w| {
+ pipeline.export_verification_key(w).unwrap()
+ })
+ .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, None)
+ .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();
+}powdr is a modular compiler stack to build zkVMs. +It is ideal for implementing existing VMs and experimenting with new designs with minimal boilerplate.
+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.
+The powdr source and documentation are released under the MIT License.
+The only way to install powdr currently is to build it from source.
+There are two binaries, powdr and powdr-rs.
The former can compile powdr-asm files to powdr-PIL, as well as generate +witnesses and proofs.
+The latter compiles Rust crates to powdr-asm via RISCV, and can execute +powdr-asm code with given inputs.
+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 estark-polygon, you also need the following
+runtime dependencies installed on the system:
gccnlohmann-json3-devYou will also need the following build time dependencies:
+makepkg-configlibpqxx-dev (Ubuntu) | libpqxx (Arch Linux)nasmUsing a single Cargo command (enable the Halo2 backend to use it with the cli):
+cargo install --git https://github.com/powdr-labs/powdr --features halo2 powdr-cli
+Or, by manually building from a local copy of the powdr repository:
+# clone the repository
+git clone https://github.com/powdr-labs/powdr.git
+cd powdr
+# install powdr-cli
+cargo install --features halo2 --path ./cli
+Using a single Cargo command:
+cargo install --git https://github.com/powdr-labs/powdr powdr-rs-cli
+Or, by manually building from a local copy of the powdr repository:
+# clone the repository
+git clone https://github.com/powdr-labs/powdr.git
+cd powdr
+# install powdr-rs-cli
+cargo install --path ./cli-rs
+Let's write a minimal VM and generate a proof!
+machine HelloWorld with 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;
+ }
+}
+Let's generate a proof of execution for the valid prover input 0 (since 0 + 1 - 1 == 0)
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2
+We observe that several artifacts are created in the current directory:
+hello_world.pil: the compiled PIL file.hello_world_opt.pil: the optimized PIL file.hello_world_constants.bin: the computed fixed columns which only have to be computed once per PIL file.hello_world_commits.bin: the computed witness which needs to be computed for each proof.hello_world_proof.bin: the ZK proof!++Note that the output directory can be specified with option
+-o|--output, and.is used by default.
Now let's try for the invalid input 1:
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 1 --prove-with halo2
+In this case witness generation fails, and no proof is created.
+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 verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --params "params.bin"
+++The command above can read previously generated constants from the directory +specified via
+-d|--dir, where.is used by default. If the constants are not present +it computes them before generating the verification key.
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.
+
Another aspect that was omitted in this example is the fact that this proof +uses a Poseidon transcript and cannot be verified in a cheap way on Ethereum, +even though we can verify it efficiently via powdr. +There are two ways to enable verification on Ethereum:
+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/powdr-labs/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::number::buffered_write_file;
+use powdr::Bn254Field;
+use powdr::Pipeline;
+
+use std::path::Path;
+
+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, None)
+ .compute_proof()
+ .unwrap();
+
+ // Step-by-step case
+
+ // First we create the universal setup of size 8
+ buffered_write_file(Path::new("params.bin"), |writer| {
+ BackendType::Halo2
+ .factory::<Bn254Field>()
+ .generate_setup(8, writer)
+ .unwrap()
+ })
+ .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, None)
+ .with_setup_file(Some("params.bin".into()));
+
+ // Create the verification key
+ buffered_write_file(Path::new("vkey.bin"), |w| {
+ pipeline.export_verification_key(w).unwrap()
+ })
+ .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, None)
+ .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();
+}This example is a variation of the previous Hello World, +targeting verification on Ethereum. In this example we will cover how to +generate proofs directly using a Keccak transcript instead of the Poseidon +transcript of the previous example, which will enable us to verify proofs +onchain. There are almost no differences from the CLI perspective.
+machine HelloWorld with 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;
+ }
+}
+Since the following command creates a proof, a Solidity verifier, and verifies
+the proof on the EVM, we need to have solc available in the system. One easy
+way to install it is by using svm.
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "snark_single" -f --params params.bin
+The extra parameter --backend-options snark_single tells powdr to produce a single
+SNARK that uses Keccak. The option -f forces overwriting the compiled files
+that have been generated before, which is useful if you are running the examples
+on the same directory as the previous example.
When the a proof is generated, it is verified on a simulated EVM transaction as well!
+Verifying SNARK in the EVM...
+We can observe again that a proof was created at hello_world_proof.bin.
Now we can generate a Solidity verifier, using the same setup (params) as the
+previous example:
powdr export-verifier test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_single" --params params.bin
+A Solidity file verifier.sol is generated. You can verify the same proof that
+we just generated by passing it to the contract together with the public inputs
+(which we have not used so far).
++Note that the more complex your VM is, the larger the verifier contract will be. In some cases, it might exceed Ethereum's contract size limit. You can mitigate that by using proof recursion on proofs that use Poseidon transcripts. See the next section for details.
+
This example is yet another variation of the previous Hello World on Ethereum +example, still targeting verification on Ethereum but supporting more complex +VMs. As noted in the previous section, complex VMs can lead to large +Solidity verifiers that exceed the contract size limit on Ethereum. One +solution to that problem is to create proofs using the Poseidon transcript, as +we did in the first example, and then use proof +recursion to create a proof that we know we will be able to verify on Ethereum.
+A recursive SNARK works by generating a proof for a circuit that verifies
+another proof. The circuit we are using here to prove our initial proof
+recursively is PSE's snark-verifier. This circuit is large enough
+to be able to prove complex programs that were proven initial with the Poseidon
+transcript, like our first example. Because of that our aggregation setup
+params and verification key are going to be larger than before and take
+longer to compute. The good news are that (i) we can use a pre-computed setup
+from a previous ceremony, and (ii) the verification key only has to be computed
+once per program.
First, we need a setup of "size" 2^22. This is the maximum execution trace length of the recursion circuit.
+You can generate it using the command line below, or download a pre-computed +one here.
+This will take a couple minutes if you decide to compute it yourself:
+powdr setup 4194304 --backend halo2 --field bn254
+We can re-use the new large params.bin for both initial and recursive proofs.
+Let's start by re-computing our Poseidon proof like in the first example,
+but using our new setup file:
powdr pil test_data/asm/book/hello_world.asm --field bn254 --inputs 0 --prove-with halo2 --backend-options "poseidon" -f --params params.bin
+This generates the initial proof hello_world_proof.bin.
+We'll also need a verification key:
powdr verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "poseidon" --params params.bin
+Let's verify the proof with our fresh verification key to make sure we're on the right track:
+powdr verify test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "poseidon" --params params.bin --vkey vkey.bin --proof hello_world_proof.bin
+In order to avoid confusion between the application's artifacts +that we've just generated and the recursion one we're going to generate +later, let's rename them:
+mv vkey.bin vkey_app.bin
+mv hello_world_proof.bin hello_world_proof_app.bin
+We can now generate a verification key for the Halo2 circuit that verifies our proofs recursively. This might take up to a minute.
+powdr verification-key test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey-app vkey_app.bin
+++Note that this verification key can only be used to verify recursive proofs that verify other proofs using the application's key
+vkey_app.bin.
We can now generate the recursive proof (can take 3 or more minutes and use 28gb RAM):
+powdr prove test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin --vkey-app vkey_app.bin --proof hello_world_proof_app.bin
+We have a proof! Note that the proof contents have two fields, proof and
+publics. The proof object contains the binary encoding of the proof
+points, and the publics object contains the public accumulator limbs that we
+need in order to verify the recursive proof.
We can now verify the proof, using the publics object as input (your numbers will likely be different):
powdr verify test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin --proof hello_world_proof_aggr.bin --publics "269487626280642378794,9378970522278219882,62304027188881225691,811176493438944,234778270138968319485,3212529982775999134,171155758373806079356,207910400337448,188563849779606300850,155626297629081952942,194348356185923309508,433061951018270,34598221006207900280,283775241405787955338,79508596887913496910,354189825580534"
+Since the goal of the recursive proof was to be able to verify it on Ethereum, let's do that!
+powdr export-verifier test_data/asm/book/hello_world.asm --field bn254 --backend halo2 --backend-options "snark_aggr" --params params.bin --vkey vkey.bin
+A Solidity verifier is created in verifier.sol. The contract expects an array of the accumulators' limbs followed by a tightly packed proof, where each accumulator limb uses 32 bytes, and there is no function signature.
Note that this verifier can be used to verify any recursive proof that verifies exactly one Poseidon proof of the given circuit.
+Besides the Hello World examples, you are encouraged to check out these more +complex and real-world use cases:
+Public values are a small but important part of verifying ZK proofs. Often, a +verifier is interested inputs and/or outputs to a public function.
+In the toy example below the prover can show that they know the square root of +a public value that is published with the proof.
+machine Square with degree: 8 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg A;
+
+ // Expose the register value of A in the last time step
+ public N = A(7);
+
+ instr square X -> Y {
+ Y = X * X
+ }
+
+ function main {
+ A <=X= ${ std::prover::Query::Input(0) };
+ A <== square(A);
+ }
+}
+This example uses a small VM with jump and a square instructions. The
+program reads the private input from the prover, squares it, and enters an
+infinite loop to ensure that all the remaining rows are filled with the result of A^2.
+Since the length of our execution trace is fixed and equals 8, we can tag the
+8-th row of A (A[7]) as the publicly exposed number.
Let's run all steps needed to generate and verify a proof that 32 = 9:
+powdr setup 8 --backend halo2 --field bn254
+powdr pil test_data/asm/sqrt_with_public.asm --field bn254 -i 3
+powdr verification-key test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin
+powdr prove test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin --vkey vkey.bin
+powdr verify test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin --vkey vkey.bin --proof sqrt_with_public_proof.bin --publics 9
+powdrThis document contains the help content for the powdr command-line program.
Command Overview:
+powdr↴powdr pil↴powdr prove↴powdr verify↴powdr verification-key↴powdr export-verifier↴powdr setup↴powdr reformat↴powdr optimize-pil↴powdrpowdr CLI to compile powdr-asm and powdr-pil programs
+Usage: powdr [OPTIONS] [COMMAND]
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 filesprove —verify —verification-key —export-verifier —setup —reformat — Parses and prints the PIL file on stdoutoptimize-pil — Optimizes the PIL file and outputs it on stdout--log-level <LOG_LEVEL> — Set log filter value [ off, error, warn, info, debug, trace ]
Default value: INFO
powdr pilRuns 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>
<FILE> — Input file--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-o, --output-directory <OUTPUT_DIRECTORY> — Output directory for the PIL file, json file and fixed and witness column data
Default value: .
-w, --witness-values <WITNESS_VALUES> — Path to a CSV file containing externally computed witness values
-i, --inputs <INPUTS> — Comma-separated list of free inputs (numbers)
Default value: ``
+-f, --force — Force overwriting of PIL output file
Default value: false
--pilo — Whether to output the pilo PIL object
Default value: false
-p, --prove-with <PROVE_WITH> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--params <PARAMS> — File containing previously generated setup parameters
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--export-csv — Generate a CSV file containing the fixed and witness column values. Useful for debugging purposes
Default value: false
--csv-mode <CSV_MODE> — How to render field elements in the csv file
Default value: hex
Possible values: i, ui, hex
powdr proveUsage: powdr prove [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the committed and fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--proof <PROOF> — File containing previously generated proof for aggregation
--vkey <VKEY> — File containing previously generated verification key
--vkey-app <VKEY_APP> — File containing the verification key of a proof to be verified recursively
--params <PARAMS> — File containing previously generated setup parameters
powdr verifyUsage: powdr verify [OPTIONS] --backend <BACKEND> --proof <PROOF> --vkey <VKEY> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--proof <PROOF> — File containing the proof
--publics <PUBLICS> — Comma-separated list of public inputs (numbers)
Default value: ``
+--vkey <VKEY> — File containing the verification key
--params <PARAMS> — File containing the params
powdr verification-keyUsage: powdr verification-key [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Chosen backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--params <PARAMS> — File containing previously generated setup parameters. This will be needed for SNARK verification keys but not for STARK
--vkey-app <VKEY_APP> — File containing the verification key of a proof to be verified recursively
powdr export-verifierUsage: powdr export-verifier [OPTIONS] --backend <BACKEND> <FILE>
<FILE> — Input PIL file-d, --dir <DIR> — Directory to find the fixed values
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Chosen backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
--backend-options <BACKEND_OPTIONS> — Backend options. Halo2: "poseidon", "snark_single" or "snark_aggr". EStark and PilStarkCLI: "stark_gl", "stark_bn" or "snark_bn"
--params <PARAMS> — File containing previously generated setup parameters. This will be needed for SNARK verification keys but not for STARK
--vkey <VKEY> — File containing previously generated verification key
powdr setupUsage: powdr setup [OPTIONS] --backend <BACKEND> <SIZE>
<SIZE> — Size of the parameters-d, --dir <DIR> — Directory to output the generated parameters
Default value: .
--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
-b, --backend <BACKEND> — Generate a proof with a given backend
Possible values: estark-starky, estark-starky-composite, estark-dump, estark-dump-composite
powdr reformatParses and prints the PIL file on stdout
+Usage: powdr reformat <FILE>
<FILE> — Input filepowdr optimize-pilOptimizes the PIL file and outputs it on stdout
+Usage: powdr optimize-pil [OPTIONS] <FILE>
<FILE> — Input file--field <FIELD> — The field to use
Default value: gl
Possible values: gl, bn254
+This document was generated automatically by
+clap-markdown.
+
powdr-asm is the higher level of abstraction in powdr. It allows defining Instruction Set Architectures (ISA) using virtual and constrained machines.
+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 with degree: 8 {
+ // 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 d;
+
+ reg pc[@pc];
+
+ instr nothing link => a.nothing();
+ instr also_nothing link => b.nothing();
+ instr still_nothing link => c.nothing();
+ instr nothing_again link => d.nothing();
+
+ function main {
+ nothing;
+ also_nothing;
+ still_nothing;
+ nothing_again;
+ return;
+ }
+}
+
+mod my_module {
+ machine Other with
+ latch: latch,
+ operation_id: 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 the powdr standard library.
Similar to Rust, any reference that cannot be resolved is looked up once more in std::prelude.
+This module exposes basic types and values such as Option, true and false.
+This means that you can use Option anywhere without prefix.
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 PIL-expression.
+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 with degree: 4 {
+ // 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 are the first main concept in powdr-asm. They can currently be of two types: virtual or constrained.
+Dynamic machines are defined by:
+An example of a simple dynamic machine is the following:
+machine HelloWorld with 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 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:
+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.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.An example of a simple constrained machine is the following:
+machine SimpleStatic with
+ degree: 8,
+ latch: latch,
+ operation_id: operation_id
+{
+ 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 powdr-pil statements, check out the pil section of this book. Note that the parameters of the operation are columns defined in powdr-pil statements.
+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;
+}
+Machines can also receive submachines as construction parameters. +A machine passed in as an argument can be accessed in the same way as locally declared submachines:
+machine MachineWithParam(subm: MySubmachine) {
+ // `subm` can be accessed as a submachine
+ ...
+}
+
+machine MyMachine {
+ MySubmachine my_submachine;
+ // `my_submachine` is passed to `another_submachine` as a construction argument
+ MachineWithParam another_submachine(my_submachine);
+}
+Registers are central to a machine. powdr supports a few types of registers:
+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 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 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;
+}
+Read-only 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.
+++Read-only registers are only mentioned for completeness here and are currently only used inside the compiler. We advise against using them.
+
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 with degree: 16 {
+ 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 are not supported yet
+
Labels allow referring to a location in a function by name.
+ start:
+Assignments allow setting the values of some write registers to the values of some expressions expression using assignment registers.
+ CNT <=X= 3;
+If the right-hand 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 which do not return outputs can be used as statements.
+ assert_zero A - ((2**2)**2)**2;
+Field element literals are signed elements of the prime field.
+ CNT <=X= 3;
+Registers can be used as expressions, with the exception of assignment registers.
+ CNT <=X= CNT - 1;
+Instructions which return outputs can be used as expressions.
+ A, B <== square_and_double(A);
+Instructions are declared as part of a powdr virtual machine. +Once defined, they can be called by any function in this machine. +An instruction is composed of:
+A local instruction is the simplest type of instruction. +It is called local because its behavior is defined by a set of constraints over registers and columns of the machine it is defined in.
+instr add X, Y -> Z {
+ X + Y = Z
+}
+Instructions may also delegate all or part of their implementation to functions/operations in submachines.
+Each link in an instruction defines the inputs and outputs of a call to a specific function/operation in a submachine.
Assume we have a submachine with a single operation add:
machine SubMachine with
+ latch: latch,
+ operation_id: 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 instruction calling into this operation can be declared as follows:
+ SubMachine submachine;
+
+ instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
+In the previous example, only assignment registers (instruction inputs and outputs) were used to call the submachine.
+The following example shows more complex usage of link calls:
machine Main with degree: 32 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg Z[<=];
+ reg A;
+ reg B;
+ reg C;
+
+ SubMachine submachine;
+
+ instr add X, Y -> Z link => Z = submachine.add(X, Y); // - trivial usage: only instruction inputs/outputs used in the call
+ instr add_to_A X, Y link => A' = submachine.add(X, Y);// - output to a regular register
+ instr addAB -> X link => X = submachine.add(A, B); // - inputs from regular registers
+ instr addAB_to_C link => C' = submachine.add(A, B); // - inputs and output from regular registers
+ instr addAB_to_A link => A' = submachine.add(A, B); // - reusing an input register as output
+ instr sub X, Y -> Z link => X = submachine.add(Y, Z); // - swapping input/output
+ // expressions can also be used as call parameters
+ instr add5 X -> Z link => Z = submachine.add(X, 3+2); // - literal expression as argument
+ col fixed STEP(i) { i };
+ instr add_current_time_step X -> Z link => Z = submachine.add(X, STEP);// - machine columns can be referenced
+ let arr = [1,2,3,4,5]; // - functions can be used
+ instr add_arr_sum X -> Z link => Z = submachine.add(X, std::array::sum(arr));
+
+ 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 (STEP column)
+ A <== add_current_time_step(42);
+ B <== add_current_time_step(42);
+ assert_eq B - A, 1;
+
+ return;
+ }
+}
+A single instruction can activate multiple links, and may also include a set of constraints.
+Furthermore, each link can be activated conditionally, based on a given boolean flag:
machine Main with degree: 16 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg Z[<=];
+ reg W[<=];
+ reg A;
+ col witness B;
+ col witness C;
+
+ SubMachine submachine;
+
+ // multiple links can be activated by a single instruction,
+ // witness columns can be used for temporary values,
+ // and additional constraints can be used
+ instr double_then_mul X, Y -> Z
+ link => B = submachine.add(X, X)
+ link => C = submachine.add(Y, Y)
+ {
+ Z = B * C
+ }
+
+ // links activated conditional on a boolean flag
+ instr add_or_sub W, X, Y -> Z
+ link if W => Z = submachine.add(X, Y)
+ link if (1 - W) => Z = submachine.sub(X, Y);
+
+ instr assert_eq X, Y { X = Y }
+
+ function main {
+ A <== double_then_mul(3, 2);
+ assert_eq A, 24;
+
+ A <== add_or_sub(1, 3, 2);
+ assert_eq A, 5;
+ A <== add_or_sub(0, 3, 2);
+ assert_eq A, 1;
+
+ return;
+ }
+}
+++Note that links cannot currently call functions from the same machine: they delegate computation to a submachine.
+
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 with
+ latch: 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 with
+ latch: latch,
+ operation_id: 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 enable a constrained machine to call into another machine. +They are defined by a call to an operation, where inputs and outputs are expressions. +An optional boolean flag restricts the rows in which the link is active. +Links without a boolean flag are active in every row.
+machine Add4 with
+ latch: latch,
+ operation_id: operation_id
+{
+ Add adder;
+
+ operation add4<0> x, y, z, w -> r;
+
+ // Links without a flag are active on every row.
+ // - constrain the values of `x`, `y`, and `n` so that `n = adder.add(x, y)`
+ link => n = adder.add(x, y);
+ // - constrain the values of `z`, `w`, and `m` so that `m = adder.add(z, w)`
+ link => m = adder.add(z, w);
+ // - constrain the values of `m`, `n` and `r` so that `r = adder.add(m,n)`
+ link => r = adder.add(m, n);
+
+ 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 with
+ latch: 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;
+}
+If a boolean flag is given, the link is only active in rows where the flag evaluates to 1.
+Whenever a link is active, the columns mapped as inputs and outputs are constrained by the operation implementation.
+The following example demonstrates how to use links with flags.
col fixed odd_row = [0,1]*;
+
+link if odd_row => z = submachine.foo(x, y); // active on odd rows only
+link if (1 - odd_row) => z = submachine.bar(x, y); // active on even rows only
+powdr-pil 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.
+Powdr-pil allows the same syntax to declare various kinds of symbols. This includes +constants, fixed columns, witness columns and even higher-order 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 (higher-order) +functions that can transform expressions. The kind of symbol is deduced by its type and whether +it is has a value:
+col or col[k].col (or col[k]) are fixed columns (or arrays of fixed columns).inter (or inter[k]) are intermediate columns (or arrays of intermediate columns).Examples:
+ // 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 = 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;Name lookup is performed as follows:
+Lookup is performed starting from the current namespace, going up to the root component by component
+where the first match is used. If all lookups fail, a last attempt is done
+inside the std::prelude namespace.
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.
+The expression language allows the following operators, in order of increased precedence:
+|params| body. Examples: |i| i (the identity), |a, b| a + b (sum)|| - logical or&& - logical and<, <=, ==, !=, >=, > - comparisons and = - identity operator| - 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 callsElementary expressions are
+"hello"[1, 2, 3](1, "abc")Parentheses are allowed at any point to force precedence.
+The only way to declare a function in pil is by assigning a lambda function to a symbol.
+Example:
+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:
+let x: int -> int = |i| i + 1;It is possible to use patterns in the function parameters:
+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.
+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:
+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:
+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:
+let constrain_to_bool: expr -> Constr = |x| x * (x - 1) = 0;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:
+let fib = |i| match i {
+ 0 => 1,
+ 1 => 1,
+ _ => fib(i - 2) + fib(i - 1),
+};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:
+let is_seven = |i| if i == 7 { 1 } else { 0 };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:
++, -,*.** must have a number as exponent.[i] must have a column name on the left-hand side and the index must be a number.' must have a column or [i] on the left-hand-side.Arbitrary parentheses are allowed.
+The following example illustrates how you can still use the generic language:
+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 sub-expression `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);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:
+// 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 bool_constraint: expr -> Constr = |x| x * (x - 1) = 0;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 identifier x, matches anything and assigns the value to the new local variable of that namek - for a literal number k, matches the exact number, either as an int or a fe-k - for a literal number k, matches the exact negated number, either as an int or a fe"text" - for a string literal, matches the exact string literal as a string(a, b, c) - for a tuple, matches a tuple-typed 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 of a and ends in b, c. The omitted part can be empty.X::Y(a, b) - for an enum variant X::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:
+// This pattern de-structures 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 non-empty 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.
+
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:
+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:
+[..].Variable patterns and _ are always irrefutable.
The powdr-pil language has the following types:
+boolint (integer)fe (field element)stringexpr (expression)! ("bottom" or "unreachable" type)++In addition, there are the
+colandintertypes, but they are special in that +they are only used for declaring columns, but cannot appear as the type of an expression. +See Declaring and Referencing Columns for details.
Powdr-pil performs Hindley-Milner 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 built-in 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.
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.
let<T: FromLiteral + Add> add_one: T -> T = |i| i + 1;A symbol declared to have type col or inter (or col[k] / inter[k]) is a bit special:
These symbols represent columns in the arithmetization and the types of values that can be assigned to +such symbols and the references to the symbols are different from their declared type.
+If you assign a value to a col symbol, that value is expected to have type int -> fe or int -> int (or an array thereof).
+This allows the simple declaration of a fixed 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 non-negative and less than
+the field modulus.
Symbols of declared type col are fixed (those with value) or witness columns (those without value).
A symbol of declared type inter is an intermediate column. You can assign it a value of type expr.
+The idea of an intermediate column is that it is an algebraic expression of other columns that you do
+not want to compute multiple times.
++Note that if you use
+let x: expr = a * b;, the symbolxis just a name in the PIL environment, +this will not create an intermediate column. The difference betweeninterandexprin this case +is that if you uselet x: inter = ..., the expression might not be inlined into constraints (depending on the backend), +while if you uselet x: expr = ..., it will always be inlined.
If you reference a symbol of declared type inter or col, the type of the reference is expr (or 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 built-in 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.
+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 ==, !=.
Type name: bool
Booleans are the results of comparisons. They allow the following operators:
+&&: logical conjunction||: logical disjunction!: logical negationShort-circuiting is not performed when evaluating boolean operators.
+This means that (1 == 1) || std::check::panic("reason") will cause a panic abort.
Type name: int
Integers in powdr-pil 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 non-negative 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&: bit-wise conjunction|: bit-wise disjunction^: bit-wise exclusive or<<: bit-wise shift left, the shift amount needs to be non-negative and fit 32 bits, otherwise a runtime error is triggered>>: bit-wise shift right, the shift amount needs to be non-negative and fit 32 bits, otherwise a runtime error is triggeredThe exponentiation operator on field elements requires a non-negative 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 thanType 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 multiplicationThere is also an exponentiation operator ** on field elements. It requires the exponent
+to be a non-negative 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 comparisonSince 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.
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 concatenationType 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.
+Type name: _[]
Arrays are statically or dynamically-sized collections of elements each of the same type
+denoted for example as int[] (a dynamically-sized 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 built-in 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 dynamically-sized arrays, which means that it does not compare the sizes of statically-sized array types.
+Arrays allow the following operators:
++: array concatenation_[]: array index access, the index needs to be a non-negative integer that is less than the length of the array, otherwise a runtime error is triggeredType 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 evaluationPowdr-pil is usually side-effect free, but there are some built-in functions that have
+side-effects:
+These are std::debug::print and std::check::panic and all functions that call them.
+Expressions are eagerly evaluated from left to right.
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:
+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 onceThe operator = on expressions constructs a constraint (see [../builtins#Constr]).
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.
Enums are user-defined 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:
+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:
+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.
+powdr-pil 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.
powdr-pil supports a basic language to define the value of constant columns using:
+[1, 2, 3][1, 2]*[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]*
+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
+}};
+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.
+let<T> std::array::len: T[] -> intReturns the length of an array as an integer.
+Example:
+let x = [1, 2, 3];
+let l = std::array::len(x); // returns 3let std::check::panic: string -> !Aborts evaluation and prints its argument as error message as a +side-effect 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 prover-internal consistency.
Example:
+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);
+ };let<T: FromLiteral> std::convert::fe: T -> feThis function is meant to be used on int, but also works on fe for convenience.
It converts a non-negative 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.
+let<T: FromLiteral> std::convert::int: T -> intThis 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.
+let<T: FromLiteral> std::convert::expr: T -> exprThis 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.
+let std::debug::print: string -> Constr[]This function takes a string and prints it on the standard output during evaluation, as a side-effect 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.
let std::field::modulus: -> intReturns the current field's modulus as an integer.
+Example:
+// Inside a machine
+if std::field::modulus() != 2**64 - 2**32 + 1 {
+ panic!("This machine can only be used with the Goldilocks field.")
+} else {
+ []
+};let std::prover::eval: expr -> feEvaluates 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:
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;
+
+}}let std::prelude::challenge: int, int -> exprConstructs 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.
+let std::prover::degree: -> intReturns the current number of rows / the length of the witness columns, also +known as the degree.
+let std::prover::set_hint: expr, (int -> std::prover::Query) -> ()This function can be used to set a "query function" for a witness column. +Query functions are used during witness generation and allow witness column cells +to receive a value even though they are not uniquely constrained by the constraints.
+The first argument must be a witness column and the function can only be called +once per witness column.
+There are some types that are not proper built-in types (in the sense that they are not treated +specially in the type system), but they are defined in the +standard library and are referenced by built-in functions.
+The type Constr or more specifically, std::prelude::Constr is the type of a constraint.
+Expressions at statement level are required to evaluate either to Constr or Constr[].
It is defined as follows:
+enum Constr {
+ /// A polynomial identity.
+ Identity(expr, expr),
+ /// A lookup constraint with selectors.
+ Lookup((Option<expr>, Option<expr>), (expr, expr)[]),
+ /// A permutation constraint with selectors.
+ Permutation((Option<expr>, Option<expr>), (expr, expr)[]),
+ /// A connection constraint (copy constraint).
+ Connection((expr, expr)[])
+}The operator = can be applied on two expr values and results in a Constr::Identity.
The type implements no traits and allows no operators.
+The following operators are supported by powdr-pil 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
+While any frontend VM can be implemented in powdr-asm, powdr comes with several frontends for popular instruction set architectures.
+A RISCV frontend for powdr is already available.
+# Install the riscv target for the rust compiler
+rustup target add riscv32imac-unknown-none-elf
+# Run the powdr-rs compiler. It will generate files in ./output/
+powdr-rs compile riscv/tests/riscv_data/sum -o output
+# Run powdr to compile powdr-asm to powdr-PIL and generate the witness
+# -i specifies the prover witness input (see below)
+powdr pil output/sum.asm -o output -f -i 10,2,4,6
+The example Rust code verifies that a supplied list of integers sums up to a specified value.
+{{#include ../../../riscv/tests/riscv_data/sum/src/lib.rs}}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.
ZK-continuations can be used to make proofs for unbounded execution traces of
+Rust programs, where the trace is split into many different chunks. A proof
+is computed for each chunk, and all proofs can be combined with
+recursion/aggregation until a single proof remains.
For the details of how memory is handled in the ZK-continuations case please +see this.
+powdr-rs has experimental support to ZK-continuations, which can be used as follows.
Let's use as example test many chunks from the riscv crate:
{{#include ../../../riscv/tests/riscv_data/many_chunks/src/lib.rs}}First we need to compile the Rust code to powdr-asm:
+powdr-rs compile riscv/tests/riscv_data/many_chunks
+Now we can use podwr's RISCV executor to estimate how many cycles are needed:
+powdr-rs execute many_chunks.asm
+...
+Execution trace length: 750329
+By default, powdr-RISCV uses chunks of length 2^18. That means we will need at +least 3 chunks.
+For the continuations case, the compiled assembly code looks different because
+of the external memory commitments, so we need to recompile using the
+--continuations flag:
powdr-rs compile riscv/tests/riscv_data/many_chunks --continuations
+We can now execute the program with continuations enabled:
+powdr-rs -- execute many_chunks.asm --continuations
+The output now is longer:
+Running chunk 0...
+Building bootloader inputs for chunk 0...
+26 unique memory accesses over 2 accessed pages: {31, 32}
+Estimating the shutdown routine to use 1362 rows.
+Bootloader inputs length: 1285
+Simulating chunk execution...
+Initial memory root hash: 44cd91c12033ad4c6a6b19793b73f1a66d99a0e0bf63494c12ceb1f451ec9452
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 260782
+Validating chunk...
+Bootloader used 3134 rows.
+ => 257648 / 262144 (98%) of rows are used for the actual computation!
+Proved 257647 rows.
+
+Running chunk 1...
+Building bootloader inputs for chunk 1...
+0 unique memory accesses over 0 accessed pages: {}
+Estimating the shutdown routine to use 42 rows.
+Bootloader inputs length: 83
+Simulating chunk execution...
+Initial memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 262102
+Validating chunk...
+Bootloader used 62 rows.
+ => 262040 / 262144 (99%) of rows are used for the actual computation!
+Proved 262039 rows.
+
+Running chunk 2...
+Building bootloader inputs for chunk 2...
+2 unique memory accesses over 1 accessed pages: {31}
+Estimating the shutdown routine to use 702 rows.
+Bootloader inputs length: 684
+Simulating chunk execution...
+Initial memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Final memory root hash: e6a6fd63d864c734d6a4df4988f733738790262af9c7b014a1c036679baf1125
+Chunk trace length: 232057
+Validating chunk...
+Bootloader used 1610 rows.
+ => 259832 / 262144 (99%) of rows are used for the actual computation!
+Done!
+The step above is informational, but for the proofs we also need the full witness:
+powdr-rs execute many_chunks.asm --witness
+The witnesses are written in ./chunk_0/commits.bin, ./chunk_1/commits.bin
+and ./chunk_2/commits.bin.
Now that we have the witnesses for all chunks we can use powdr (instead of
+powdr-rs) to compute proofs for each chunk:
powdr prove many_chunks.asm -d chunk_0 --backend estark-dump
+powdr prove many_chunks.asm -d chunk_1 --backend estark-dump
+powdr prove many_chunks.asm -d chunk_2 --backend estark-dump
+These proofs are mock proofs for the sake of the example, but any backend +should work here.
+After generating real proofs, each specific proof system can be used for the +recursion/aggregation parts. A follow-up tutorial on that is coming soon.
+A Valida front end for powdr is under development. If you are interested, feel free to reach out!
+An EVM frontend for powdr is under development. If you are interested, feel free to reach out!
+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.
+powdr supports the PSE fork of halo2 with the bn254 field.
+powdr supports the eSTARK proof system with the Goldilocks field, +implemented by the starky library from eigen-zkvm.
+powdr applies a number of steps in order to reduce a powdr-asm program into PIL.
+We provide a high level overview of these steps.
+ ┌────────────┐ ┌──────────┐
+ │ │ │ │
+ powdr-asm │ │ AIR graph │ │ PIL
+───────────►│ compiler ├───────────┤ linker ├──────►
+ │ │ │ │
+ │ │ │ │
+ └────────────┘ └──────────┘
+In this section, we explain how the powdr compiler reduces a program made of virtual and constrained machines to a set of AIRs.
+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:
+Block enforcement applies on constrained machines. It makes sure that the operation_id is constant within each machine block.
At this point, all machines contain only:
+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.
+A linker is used to turn an AIR tree into a single PIL file. +The linking process operates in the following way:
+optional_main_degree be its optional degree.optional_main_degreeThe result is a monolithic AIR where:
+Public values are a small but important part of verifying ZK proofs. Often, a +verifier is interested inputs and/or outputs to a public function.
+In the toy example below the prover can show that they know the square root of +a public value that is published with the proof.
+machine Square with degree: 8 {
+ reg pc[@pc];
+ reg X[<=];
+ reg Y[<=];
+ reg A;
+
+ // Expose the register value of A in the last time step
+ public N = A(7);
+
+ instr square X -> Y {
+ Y = X * X
+ }
+
+ function main {
+ A <=X= ${ std::prover::Query::Input(0) };
+ A <== square(A);
+ }
+}
+This example uses a small VM with jump and a square instructions. The
+program reads the private input from the prover, squares it, and enters an
+infinite loop to ensure that all the remaining rows are filled with the result of A^2.
+Since the length of our execution trace is fixed and equals 8, we can tag the
+8-th row of A (A[7]) as the publicly exposed number.
Let's run all steps needed to generate and verify a proof that 32 = 9:
+powdr setup 8 --backend halo2 --field bn254
+powdr pil test_data/asm/sqrt_with_public.asm --field bn254 -i 3
+powdr verification-key test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin
+powdr prove test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin --vkey vkey.bin
+powdr verify test_data/asm/sqrt_with_public.asm --field bn254 --backend halo2 --params params.bin --vkey vkey.bin --proof sqrt_with_public_proof.bin --publics 9
+