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

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 files
  • 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
  • riscv-asm — Compiles riscv assembly to powdr assembly and then to PIL and generates fixed and witness columns
  • prove —
  • setup —
  • reformat — Parses and prints the PIL file on stdout
  • optimize-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 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). Assumes queries to have the form ("input", )

    Default value: ``

  • -f, --force — Force overwriting of PIL output file

    Default value: false

  • -p, --prove-with <PROVE_WITH> — Generate a proof with a given backend

    Possible values: estark, pil-stark-cli

  • --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

  • -j, --just-execute — Just execute in the RISCV/Powdr executor

    Default 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 use

    Default 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 files

    Default value: .

  • -f, --force — Force overwriting of files in output directory

    Default value: false

  • -p, --prove-with <PROVE_WITH> — Generate a proof with a given backend

    Possible values: estark, pil-stark-cli

  • --coprocessors <COPROCESSORS> — Comma-separated list of coprocessors

  • -j, --just-execute — Just execute in the RISCV/Powdr executor

    Default 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 use

    Default 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 files

    Default value: .

  • -f, --force — Force overwriting of files in output directory

    Default value: false

  • -p, --prove-with <PROVE_WITH> — Generate a proof with a given backend

    Possible values: estark, pil-stark-cli

  • --coprocessors <COPROCESSORS> — Comma-separated list of coprocessors

  • -j, --just-execute — Just execute in the RISCV/Powdr executor

    Default 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 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, 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 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, 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 use

    Default 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:

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:

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:

  1. Create an empty PIL file
  2. Start from the main AIR. If it defines a degree, let main_degree be that value. If it does not, let main_degree be 1024.
  3. For each AIR
    1. Create a new namespace in the PIL file
    2. 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 to main_degree
    3. Add the constraints to the namespace
    4. 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.