Introduction
powdr is a modular compiler stack to build zkVMs. It is ideal for implementing existing VMs and experimenting with new designs with minimal boilerplate.
- Domain specific languages are used to specify the VM and its underlying constraints, not low level Rust code
- Automated witness generation
- Support for multiple provers as well as aggregation schemes
- Support for hand-optimized co-processors when performance is critical
- Built in Rust 🦀
Contributing
powdr is free and open source. You can find the source code on GitHub. Issues and feature requests can be posted on the GitHub issue tracker.
License
The powdr source and documentation are released under the MIT License.
Installation
The only way to install powdr currently is to build it from source.
Prerequisites
You will need the Rust compiler and Cargo, the Rust package manager.
The easiest way to install both is with rustup.rs
.
On Windows, you will also need a recent version of Visual Studio, installed with the "Desktop Development With C++" Workloads option.
Building
Using a single Cargo command:
cargo install --git https://github.com/powdr-labs/powdr 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 --path ./powdr_cli
Hello World
Let's write a minimal VM and generate a SNARK!
machine HelloWorld {
degree 8;
// this simple machine does not have submachines
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg A;
instr incr X -> Y {
Y = X + 1
}
instr decr X -> Y {
Y = X - 1
}
instr assert_zero X {
X = 0
}
// the main function assigns the first prover input to A, increments it, decrements it, and loops forever
function main {
A <=X= ${ ("input", 0) };
A <== incr(A);
A <== decr(A);
assert_zero A;
return;
}
}
Then let's generate a proof of execution for the valid prover input 0
(since for 0 + 1 - 1 == 0
)
powdr pil hello_world.asm --field bn254 --force --inputs 0 --prove-with halo2
We observe that a proof was created at proof.bin
.
Now let's try for the invalid input 1
powdr pil hello_world.asm --field bn254 --force --inputs 1 --prove-with halo2
We observe that witness generation fails, and no proof is created.
Command-Line Help for powdr
This document contains the help content for the powdr
command-line program.
Command Overview:
powdr
↴powdr pil
↴powdr rust
↴powdr riscv-asm
↴powdr prove
↴powdr setup
↴powdr reformat
↴powdr optimize-pil
↴
powdr
Usage: powdr [COMMAND]
Subcommands:
pil
— Runs compilation and witness generation for .pil and .asm files. First converts .asm files to .pil, if needed. Then converts the .pil file to json and generates fixed and witness column data filesrust
— Compiles (no-std) rust code to riscv assembly, then to powdr assembly and finally to PIL and generates fixed and witness columns. Needsrustup target add riscv32imac-unknown-none-elf
riscv-asm
— Compiles riscv assembly to powdr assembly and then to PIL and generates fixed and witness columnsprove
—setup
—reformat
— Parses and prints the PIL file on stdoutoptimize-pil
— Optimizes the PIL file and outputs it on stdout
Options:
--markdown-help
powdr pil
Runs compilation and witness generation for .pil and .asm files. First converts .asm files to .pil, if needed. Then converts the .pil file to json and generates fixed and witness column data files
Usage: powdr pil [OPTIONS] <FILE>
Arguments:
<FILE>
— Input file
Options:
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
-
-o
,--output-directory <OUTPUT_DIRECTORY>
— Output directory for the PIL file, json file and fixed and witness column dataDefault 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). Assumes queries to have the form ("input",) Default value: ``
-
-f
,--force
— Force overwriting of PIL output fileDefault value:
false
-
-p
,--prove-with <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estark
,pil-stark-cli
-
--export-csv
— Generate a CSV file containing the fixed and witness column values. Useful for debugging purposesDefault value:
false
-
--csv-mode <CSV_MODE>
— How to render field elements in the csv fileDefault value:
hex
Possible values:
i
,ui
,hex
-
-j
,--just-execute
— Just execute in the RISCV/Powdr executorDefault value:
false
powdr rust
Compiles (no-std) rust code to riscv assembly, then to powdr assembly and finally to PIL and generates fixed and witness columns. Needs rustup target add riscv32imac-unknown-none-elf
Usage: powdr rust [OPTIONS] <FILE>
Arguments:
<FILE>
— Input file (rust source file) or directory (containing a crate)
Options:
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
-
-i
,--inputs <INPUTS>
— Comma-separated list of free inputs (numbers)Default value: ``
-
-o
,--output-directory <OUTPUT_DIRECTORY>
— Directory for output filesDefault value:
.
-
-f
,--force
— Force overwriting of files in output directoryDefault value:
false
-
-p
,--prove-with <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estark
,pil-stark-cli
-
--coprocessors <COPROCESSORS>
— Comma-separated list of coprocessors -
-j
,--just-execute
— Just execute in the RISCV/Powdr executorDefault value:
false
powdr riscv-asm
Compiles riscv assembly to powdr assembly and then to PIL and generates fixed and witness columns
Usage: powdr riscv-asm [OPTIONS] <FILES>...
Arguments:
<FILES>
— Input files
Options:
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
-
-i
,--inputs <INPUTS>
— Comma-separated list of free inputs (numbers)Default value: ``
-
-o
,--output-directory <OUTPUT_DIRECTORY>
— Directory for output filesDefault value:
.
-
-f
,--force
— Force overwriting of files in output directoryDefault value:
false
-
-p
,--prove-with <PROVE_WITH>
— Generate a proof with a given backendPossible values:
estark
,pil-stark-cli
-
--coprocessors <COPROCESSORS>
— Comma-separated list of coprocessors -
-j
,--just-execute
— Just execute in the RISCV/Powdr executorDefault value:
false
powdr prove
Usage: powdr prove [OPTIONS] --backend <BACKEND> <FILE>
Arguments:
<FILE>
— Input PIL file
Options:
-
-d
,--dir <DIR>
— Directory to find the committed and fixed valuesDefault value:
.
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
-
-b
,--backend <BACKEND>
— Generate a proof with a given backendPossible values:
estark
,pil-stark-cli
-
--proof <PROOF>
— File containing previously generated proof for aggregation -
--params <PARAMS>
— File containing previously generated setup parameters
powdr setup
Usage: powdr setup [OPTIONS] --backend <BACKEND> <SIZE>
Arguments:
<SIZE>
— Size of the parameters
Options:
-
-d
,--dir <DIR>
— Directory to output the generated parametersDefault value:
.
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
-
-b
,--backend <BACKEND>
— Generate a proof with a given backendPossible values:
estark
,pil-stark-cli
powdr reformat
Parses and prints the PIL file on stdout
Usage: powdr reformat <FILE>
Arguments:
<FILE>
— Input file
powdr optimize-pil
Optimizes the PIL file and outputs it on stdout
Usage: powdr optimize-pil [OPTIONS] <FILE>
Arguments:
<FILE>
— Input file
Options:
-
--field <FIELD>
— The field to useDefault value:
gl
Possible values:
gl
,bn254
This document was generated automatically by
clap-markdown
.
asm
powdr-asm is the higher level of abstraction in powdr. It allows defining Instruction Set Architectures (ISA) using virtual and constrained machines.
Modules
powdr exposes a module system to help organise and reuse code.
use my_module::Other as LocalOther;
// we can define a module at `./submodule.asm`
mod submodule;
// we can define a module at `./submodule_in_folder/mod.asm`
mod submodule_in_folder;
use submodule::Other as SubmoduleOther;
use submodule_in_folder::Other as FolderSubmoduleOther;
machine Main {
// use a machine from another module by relative path
my_module::Other a;
// use a machine from another module using a local binding
LocalOther b;
// use a machine from another module defined in a different file
SubmoduleOther c;
// use a machine from another module defined in a different directory
FolderSubmoduleOther c;
reg pc[@pc];
instr nothing = a.nothing
instr also_nothing = b.nothing
instr still_nothing = c.nothing
function main {
nothing;
also_nothing;
still_nothing;
return;
}
}
mod my_module {
machine Other(latch, operation_id) {
operation nothing<0>;
col fixed latch = [1]*;
col fixed operation_id = [0]*;
}
}
Note that a module can't be called std
, as this name is reserved for an upcoming powdr standard library.
Machines
Machines are the first main concept in powdr-asm. They can currently be of two types: virtual or constrained.
Virtual machines
Dynamic machines are defined by:
- a degree, indicating the number of execution steps
- a set of registers, including a program counter
- an instruction set
- a set of powdr-pil statements
- a set of functions
- a set of submachines
An example of a simple dynamic machine is the following:
machine HelloWorld {
degree 8;
// this simple machine does not have submachines
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg A;
instr incr X -> Y {
Y = X + 1
}
instr decr X -> Y {
Y = X - 1
}
instr assert_zero X {
X = 0
}
// the main function assigns the first prover input to A, increments it, decrements it, and loops forever
function main {
A <=X= ${ ("input", 0) };
A <== incr(A);
A <== decr(A);
assert_zero A;
return;
}
}
Constrained machines
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:
- a degree, indicating the number of execution steps
- a set of operations
- an
operation_identifier
column, used to make constraints conditional over which function is called. It can be omitted with_
if the machine has at most one operation. - a
latch
column, used to identify rows at which the machine can be accessed from the outside (where the inputs and outputs are passed). It can be omitted if the machine has no operations. - a set of submachines
- a set of links
An example of a simple constrained machine is the following:
machine SimpleStatic(latch, operation_id) {
degree 8;
operation power_4<0> x -> y;
col fixed operation_id = [0]*;
col fixed latch = [0, 0, 0, 1]*;
col witness x;
col witness y;
// initialise y to x at the beginning of each block
latch * (y' - x') = 0;
// x is unconstrained at the beginning of the block
// x is constant within a block
(1 - latch) * (x' - x) = 0;
// y is multiplied by x at each row
(1 - latch) * (y' - x * y) = 0;
}
For more details on the 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.
Submachines
Machines can have submachines which they access by defining external instructions or links. They are declared as follows:
machine MySubmachine {
...
}
machine MyMachine {
MySubmachine my_submachine;
}
Registers
Registers are central to a machine. powdr supports a few types of registers:
Program counter
Each machine can have at most one program counter. In the absence of a program counter, the machine is considered static, and no other register can be declared. The program counter is defined as follows:
reg pc[@pc]
At each step execution step, the program counter points to the function line to execute. The program counter behaves like a write register, with the exception that its value is incremented by default after each step.
Write registers
Write registers are the default type for registers. They are declared as follows:
reg A;
They hold a field element, are initialized as 0 at the beginning of a function and keep their value by default. They can be read from and written to.
// write to A
A <=X= 1;
// A is 1
// read from A
B <=X= A;
// A is still 1
Assignment registers
Assignment registers are transient to an execution step: their value is not persisted across steps. They are required in order to pass inputs and receive outputs from instructions, as well as in assignments.
For example, if we want to assert that write register A
is 0
, we can use the following instruction:
reg pc[@pc];
reg A;
instr assert_A_is_zero {
A = 0
}
function main {
assert_A_is_zero;
return;
}
However, if we want the instruction to accept any write register as input, we use an assignment register.
reg pc[@pc];
reg X[<=];
reg A;
instr assert_zero X {
X = 0
}
function main {
assert_zero A;
return;
}
Read-only registers
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
Functions are the entry points to a virtual machine. They can be called from another machine or from the outside.
In this section, we describe functions with this simple virtual machine:
machine Machine {
degree 256;
reg pc[@pc];
reg X[<=];
reg Y[<=];
reg Z[<=];
reg CNT;
reg A;
reg B;
// an instruction to assert that a number is zero
instr assert_zero X {
X = 0
}
// an instruction to jump to a label
instr jmp l: label {
pc' = l
}
// an instruction to jump to a label iff `X` is `0`, otherwise continue
instr jmpz X, l: label {
pc' = XIsZero * l + (1 - XIsZero) * (pc + 1)
}
// an instruction to return the square of an input as well as its double
instr square_and_double X -> Y, Z {
Y = X * X,
Z = 2 * X
}
function main {
// initialise `A` to 2
A <=X= 2;
// initialise `CNT` to `3`
CNT <=X= 3;
start::
// if `CNT` is `0`, jump to `end`
jmpz CNT, end;
// decrement `CNT`
CNT <=X= CNT - 1;
// get the square and the double of `A`
A, B <== square_and_double(A);
// jump back to `start`
jmp start;
end::
// check that `A == ((2**2)**2)**2`
assert_zero A - ((2**2)**2)**2;
// check that `B == ((2**2)**2)*2`
assert_zero B - ((2**2)**2)*2;
return;
}
// some superpowers on `X` to allow us to check if it's 0
col witness XInv;
col witness XIsZero;
XIsZero = 1 - X * XInv;
XIsZero * X = 0;
XIsZero * (1 - XIsZero) = 0;
}
Function inputs and outputs
Function inputs and outputs are not supported yet
Statements
Labels
Labels allow referring to a location in a function by name.
start::
Assignments
Assignments allow setting the values of some write registers to the values of some expressions expression using assignment registers.
CNT <=X= 3;
If the 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
Instructions which do not return outputs can be used as statements.
assert_zero A - ((2**2)**2)**2;
Expressions
Field element literals
Field element literals are signed elements of the prime field.
CNT <=X= 3;
Registers and columns
Registers can be used as expressions, with the exception of assignment registers.
CNT <=X= CNT - 1;
Instructions
Instructions which return outputs can be used as expressions.
A, B <== square_and_double(A);
Instructions
Instructions are declared as part of a powdr virtual machine. Their inputs and outputs are assignment registers as well as labels. Once defined, they can be called by any function in this machine.
Local instructions
A local instruction is the simplest type of instruction. It is called local because its behavior is defined using constraints over registers and columns of the machine it is defined in.
instr add X, Y -> Z {
X + Y = Z
}
Instructions feature:
- a name
- some inputs
- some outputs
- a set of powdr-pil constraints to activate when the instruction is called
External instructions
An external instruction delegates calls to a function inside a submachine of this machine. When it is called, a call is made to the submachine function. An example of an external instruction is the following:
instr assert_zero X = my_submachine.assert_zero // where `assert_zero` is a function defined in `my_submachine`
Note that external instructions cannot currently link to functions of the same machine: they delegate computation to a submachine.
Operations
Operations enable a constrained machine to expose behavior to the outside.
machine Arith(latch, operation_id) {
operation add<0> a, b -> c;
operation sub<1> a, b -> c;
col witness operation_id;
col fixed latch = [1]*;
col witness a;
col witness b;
col witness c;
c = (1 - operation_id) * (a + b) + operation_id * (a - b);
}
They are defined by:
- a value for the operation id. When calling this operation, the operation id of this machine is set to this value.
- parameters in the form of columns defined in the current machine
The actual behavior of the operation is defined freely as constraints.
Links
Links enable a constrained machine to call into another machine.
machine Main(latch, operation_id) {
Arith adder;
operation main<0> x, y -> z;
// - on every row (the boolean flag is `1`)
// - constrain the values of `x`, `y`, and `z` so that `z = adder.add(x, y)`
// TODO: uncomment the link once witness generation supports it
// link 1 x, y -> z = adder.add;
col fixed operation_id = [0]*;
col fixed latch = [1]*;
col witness x;
col witness y;
col witness z;
}
They are defined by:
- a boolean flag which must be on for the link to be active
- parameters to pass to the other machine, in the form of columns defined in the current machine
- an operation or function of the machine which is called
PIL
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.
Declarations
Powdr-pil allows the same syntax to declare various kinds of symbols. This includes constants, fixed columns, witness columns and even macros. It deduces the symbol kind by its type 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.
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 the
way the symbol is used:
- symbols without a value are witness columns,
- symbols evaluating to a number are constants,
- symbols defined as a function with a single parameter are fixed columns and
- everything else is a "generic symbol" that is not a column.
Examples:
#![allow(unused)] fn main() { // This defines a constant let rows = 2**16; // This defines a fixed column that contains the row number in each row. let step = |i| i; // Here, we have a witness column. let x; // This functions returns the square of its input (classified as a fixed column). let square = |x| x*x; // A recursive function, taking a function and an integer as parameter let sum = |f, i| match i { 0 => f(0), _ => f(i) + sum(f, i - 1) }; // The same function as "square" above, but employing a trick to avoid it // being classified as a column. let square_non_column = (|| |x| x*x)(); }
Expressions
Depending on the context, powdr allows more or less features for expressions.
Inside values for declarations, you can use a very flexible language which includes many different operators, function calls, lambda functions, tuple types, statement blocks, match statements and others.
In statements and expressions that are required to evaluate to polynomial identities, only a much more restrictive language can be used. Expressions in that language are caleld Algebraic Expressions. While you can use the full language everywhere, in the context of a polynomial identity, the result after function evaluation and constant propagation has to be an algebraic expression.
Generic Expressions
The expression language allows the following operators, in order of increased precedence:
- lambda functions:
|params| body
. Examples:|i| i
(the identity),|a, b| a + b
(sum) ||
- logical or&&
- logical and<
,<=
,==
,!=
,>=
,>
- comparisons|
- bitwise or^
- bitwise xor&
- bitwise and<<
,>>
- left and right shift+
,-
- addition and subtraction (binary operator)*
,/
,%
- multiplication, division and modulo**
- exponentiation-
,!
- numerical and logical negation (unary operators, prefix)'
- "next row" operator (suffix)[]
,()
- array index access and function calls
Elementary expressions are
- number literals (integers)
- string literals, written in double quotes, e.g.
"hello"
- array literals written in square brackets, e.g.
[1, 2, 3]
- tuples, having at least two elements, e.g.
(1, "abc")
- match expressions (see below).
Parentheses are allowed at any point to force precedence.
Match Expressions
Match expressions take the form match <value> { <pattern 1> => <value 1>, <pattern 2> => <value 2>, _ => <default value> }
,
with an arbitrary number of match arms.
The semantics are that the first match arm where the pattern equals the value after the match
keyword is evaluated.
The "default" arm with the pattern _
matches all values.
Example:
let fib = |i| match i {
0 => 1,
1 => 1,
_ => fib(i - 2) + fib(i - 1),
};
Algebraic Expressions
For identities (or functions called from identities), the expression syntax is limited: After evaluating function calls and performing constant propagation, the resulting expression has to be an "algebraic expression". These are restricted in the following way:
- You can freely use the operators
+
,-
,*
. - The operator
**
must have a number as exponent. - The operator
[i]
must have a column name on the left-hand side and the index must be a number. - The operator
'
must have a column or[i]
on the left-hand-side. - No other operators are allowed.
Arbitrary parentheses are allowed.
Fixed columns
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.
Values with repetitions
powdr-pil supports a basic language to define the value of constant columns using:
- arrays, for example
[1, 2, 3]
- repetition, for example
[1, 2]*
- concatenation, for example
[1, 2] + [3, 4]
These mechanisms can be combined, as long as a single repetition is used per column definition.
// valid, as for a given total length, only one column fits this definition for a given `N`
col fixed A = [1, 2] + [3, 4]* + [5];
// invalid, as many columns fit this definition
// col fixed A = [1, 2]* + [3, 4]*
Mappings
A column can be seen as a mapping from integers to field elements. In this context, different functions are supported:
col fixed B(i) { i + 1 };
col fixed C(i) {match i {
0 => 1,
_ => 0
}};
Note that conversion from integer to field element is currently implicit, as seen in the first example above.
Frontends
While any frontend VM can be implemented in powdr-asm, powdr comes with several frontends for popular instruction set architectures.
RISCV
A RISCV frontend for powdr is already available.
How to run the Rust-RISCV example
# Install the riscv target for the rust compiler
rustup target add riscv32imac-unknown-none-elf
# Run the compiler. It will generate files in /tmp/.
# -i specifies the prover witness input (see below)
powdr rust riscv/tests/riscv_data/sum.rs -o /tmp -f -i 10,2,4,6
The following example Rust file verifies that a supplied list of integers sums up to a specified value. Note that this is the full and only input file you need for the whole process!
#![no_std] extern crate alloc; use alloc::vec::Vec; use runtime::get_prover_input; #[no_mangle] pub fn main() { // This is the sum claimed by the prover. let proposed_sum = get_prover_input(0); // The number of integers we want to sum. let len = get_prover_input(1) as usize; // Read the numbers from the prover and store them // in a vector. let data: Vec<_> = (2..(len + 2)) .map(|idx| get_prover_input(idx as u32)) .collect(); // Compute the sum. let sum: u32 = data.iter().sum(); // Check that our sum matches the prover's. assert_eq!(sum, proposed_sum); }
The function get_prover_input
reads a number from the list supplied with -i
.
This is just a first mechanism to provide access to the outside world.
The plan is to be able to call arbitrary user-defined ffi
functions that will translate to prover queries,
and can then ask for e.g. the value of a storage slot at a certain address or the root hash of a Merkle tree.
Valida
A Valida front end for powdr is under development. If you are interested, feel free to reach out!
EVM
An EVM frontend for powdr is under development. If you are interested, feel free to reach out!
Backends
powdr aims to have full flexibility when it comes to generating proofs and comes with a few built-in backends to get started with zkVMs.
Halo2
powdr supports the PSE fork of halo2 with the bn254 field.
eSTARK
powdr supports the eSTARK proof system with the Goldilocks field, implemented by the starky library from eigen-zkvm.
Architecture
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 ├──────►
│ │ │ │
│ │ │ │
└────────────┘ └──────────┘
Compiler
In this section, we explain how the powdr compiler reduces a program made of virtual and constrained machines to a set of AIRs.
Virtual machine reduction
The first step is to reduce virtual machines to constrained machines. This step is run on all machines and does not affect constrained machines. As a result of this step, for each machine:
- Local instructions are reduced to constraints
- External instructions are reduced to links
- Functions are reduced to operations
Block enforcement
Block enforcement applies on constrained machines. It makes sure that the operation_id
is constant within each machine block.
AIR generation
At this point, all machines contain only:
- an optional degree
- constraints
- links to other machines
- operations
Let's define AIR as a data structure with only these elements.
Starting from the main machine's type, we create a tree of AIR objects by traversing its submachines, recursively instantiating each machine as an AIR. Let's define the AIR tree as the resulting tree.
Linker
A linker is used to turn an AIR tree into a single PIL file. The linking process operates in the following way:
- Create an empty PIL file
- Start from the main AIR. If it defines a degree, let
main_degree
be that value. If it does not, letmain_degree
be1024
. - For each AIR
- Create a new namespace in the PIL file
- If a degree is defined, check that it equals
main_degree
and error out if it does not. If no degree is defined, set the degree tomain_degree
- Add the constraints to the namespace
- Turn the links into lookups and add them to the namespace
The result is a monolithic AIR where:
- each machine instance is a namespace
- all namespaces have the same degree
- links between instances are encoded as lookup identities
More flexible approaches to the linking process will be explored in the future, such as allowing for machine instances of different degrees.