Introduction

Polygon Miden's AirScript is designed to make it simple to describe AIR constraints and generate efficient and accurate constraint evaluation code in the required target language. The code for AirScript can be found here.

Current Version

Currently, AirScript is on version 0.3, which includes about 95% of features needed to describe Miden VM constraints, and supports generation of constraint evaluation code for the following backends:

AirScript includes the following features:

• Trace Columns: Users can declare trace columns for main and auxiliary traces as individual columns or groups of columns (e.g. main: [a, b, c[3], d], where a, b, and d are single columns and c refers to a group of 3 columns)

• Public Inputs: Users can declare public inputs where each public input is a named vector (e.g. stack_inputs: [16],)

• Periodic Columns: Users can declare periodic columns (e.g. k0: [1, 0, 0, 0],)

• Random Values: Users can define random values provided by the verifier (e.g. alphas: [x, y[14], z], or rand: [16],)

• Boundary Constraints: Users can enforce boundary constraints on main and auxiliary trace columns using public inputs, random values, constants and variables.

• Integrity Constraints: Users can enforce integrity constraints on main and auxiliary trace columns using trace columns, periodic columns, random values, constants and variables.

• Constants: Users can declare module level constants. Constants can be scalars, vectors or matrices. (e.g. const A = 123;, const B = [1, 2, 3];, const C = [[1, 2, 3], [4, 5, 6]];)

• Variables: Local variables can be declared for use in defining boundary and integrity constraints. Variables can be scalars, vectors or matrices built from expressions (e.g. let x = k * c[1];', let y = [k * c[1], l * c[2], m * c[3]]; or let z = [[k * c[1], l * c[2]], [m * c[3], n * c[4]]];)

• Evaluators: Users can declare evaluator functions to group multiple related integrity constraints together. Evaluators can be declared locally or imported from other modules. This helps increase modularity and readability of AirScript code.

The language also includes some convenience syntax to make writing constraints easier. This includes:

• List comprehension - e.g., let x = [k * c for (k, c) in (k, c[1..4])];.
• List folding - e.g., let y = sum([k * c for (k, c) in (k, c[1..4])]);.
• Constraint comprehension - e.g., enf x^2 = x for x in a;.
• Conditional constraints - which enable convenient syntax for turning constraints on or off based on selector values.

CLI

There is a command-line interface available for emitting constraint evaluation code in Rust or Miden assembly. There are also several example .air files written in AirScript which can be found in the examples/ directory.

To use the CLI, first run:

cargo build --release

Then, run the airc target with the transpile option. For example:

./target/release/airc transpile examples/example.air

This will output constraint evaluation code targeted for the Winterfell prover.

You can use the help option to see other available options.

./target/release/airc transpile --help

Future Work

The following changes are some of the improvements under consideration for future releases.

• more advanced language functionality for better ergonomics and modularity, such as:
  • support for functions.
  • specialized expressions for multiset checks.
• optimizations, such as:
  • constant folding.
  • removing unnecessary nodes from the AlgebraicGraph of boundary and integrity constraints.
  • combining integrity constraints with mutually exclusive selectors to reduce the total number of constraints.
  • Optimizing constraint evaluation logic for Miden assembly backend.
• additional language targets for simplifying verifier implementations:
  • Solidity.
• formal verification

Language Description

• Syntax overview
• Code organization
• Type declarations
• Constraint descriptions
• Variables
• Evaluators
• Convenience syntax
• AirScript Example
• Keywords
• Appendix

Syntax Overview

This page specifies the basic syntax and types.

Delimiters and special characters

• : is used as a delimiter when declaring source sections and types
• . is used to access a boundary on a trace column, e.g. a.first or a.last
• [ and ] are used for defining arrays in type declarations and for indexing in constraint descriptions
• , is used as a delimiter for defining arrays in type declarations, as well as a separator in when declaring source sections
• ; is used as a statement terminator in constraint descriptions and variable declarations
• $ is used to access random values or built-in variables by their identifier. For example, the column at index i in the main execution trace can be accessed by $main[i].

Identifiers

Valid identifiers are strings that start with a letter a-z or A-Z followed by any combination of letters, digits 0-9 or an underscore _.

Numbers

The only supported numbers are integers, and all integers are parsed as u64. Using a number larger than 2^64 - 1 will result in a ParseError.

Operations

The following operations are supported in constraint descriptions with the specified syntax:

• Equality (a = b)
• Addition (a + b)
• Subtraction (a - b)
• Multiplication (a * b)
• Exponentiation by a constant integer x (a^x)

The following operations are not supported:

• Negation
• Division
• Inversion

Parentheses and complex expressions

Parentheses (( and )) are supported and can be included in any expression except exponentiation, where complex expressions are not allowed.

The following is allowed:

a * (b + c)

The following is not allowed:

a^(2 + 3)

Section-specific accessors

These accessors may only be used in the specified source section in which they are described below.

Boundary constraints

The following accessors may only be applied to trace columns when they are in boundary constraint definitions.

• First boundary (.first): accesses the trace column's value in the first row. It is only supported in boundary constraint descriptions
• Last boundary (.last): accesses the trace column's value in the last row. It is only supported in boundary constraint descriptions

The following accessor may only be applied to public inputs declared in public_inputs when they are referenced in boundary constraint definitions.

• Indexing (input_name[i]): public inputs may be accessed by using the indexing operator on the declared identifier name with an index value that is less than the declared size of its array.

Here is an example of usage of first and last boundaries and a public input within a boundary constraint:

trace_columns {
    main: [a],
}

public_inputs {
    stack_inputs: [4],
    stack_outputs: [4],
}

boundary_constraints {
    enf a.first = stack_inputs[0];
    enf a.last = stack_outputs[0];
}

Integrity constraints

The following accessor may only be applied to trace columns when they are referenced in integrity constraint definitions.

• Next Row (a'): ' is a postfix operator that indicates the value of the specified trace column in the next row. It is only supported in integrity constraint descriptions.

Here is an example of usage of the Next Row operator within an integrity constraint:

trace_columns {
  main: [a],
  aux: [p],
}

integrity_constraints {
  enf p' = p * a;
}

Code organization

AirScript project can consist of one or more modules, each module located in a separate file with a .air extension. For projects consisting of multiple modules, one module must be declared as the root module, and all other modules must be declared as library modules.

Currently, all modules must be located in a single directory, but in the future this limitation will be removed.

All modules must start with a module name declaration followed by a set of source sections. These sections describe both the metadata and constraint evaluation logic for the AIR. Depending on the module type, some source sections may be required, be optional, or may not be allowed. The table below summarizes this information.

Note that constants and evaluators are not really distinct sections but rather a set of declarations which can be done in-between any other sections.

Root module

A root module defines an entrypoint into an AirScript project. It must start with a name declaration which consists of a def keyword followed by the name of the AIR project. For example:

def ExampleAir

where the name of the module must:

• Be a string consisting of alpha-numeric characters and underscores.
• Start with a letter.
• End with a newline.

Besides the name declaration, a root module must:

• Describe the shape of the execution trace (done via the trace columns section).
  • If the trace consists of more than one segment (e.g., main and auxiliary segments), describe random values available to the prover after each segment commitment (done via the random values section).
• Describe the shape of the public inputs (done via the public inputs section).
• Describe the boundary constraints placed against the execution trace (done via the boundary constraints section).
• Describe the integrity constraints placed against the execution trace (done via the integrity constraints section).

To aid with boundary and integrity constraint descriptions, a root module may also contain definitions of constants, evaluators, and periodic columns.

Library modules

Library modules can be used to split integrity constraint descriptions across multiple files. A library module must start with a name declaration which consists of a mod keyword followed by the name of the module. For example:

mod example_module

where the name of the module must:

• Be the same as the name of the file in which the library module is defined (e.g., the above module must be located in example_module.air file).
• Be a string consisting of alpha-numeric characters and underscores.
• Start with a letter.
• End with a newline.

Besides the name declaration, library modules my contain definitions of constants, evaluators, and periodic columns. Constants and evaluators defined in a library module may be imported by a root or other library modules.

Library modules inherit random value declarations of the root module. That is, evaluators defined in a library module can reference random values declared in the root module.

Importing evaluators

A module can import constants and evaluators from library modules via a use statement. For example:

use my_module::my_evaluator
use my_module::my_constant

where:

• my_module is a library module located in the same directory as the importing module.
• my_evaluator and my_constant is an evaluator and a constant defined in my_module.

Once an evaluator or a constant is imported, it can be used in the same way as evaluators and constants defined in the importing module.

To import multiple evaluators and constants, multiple use statements must be used:

use my_module::foo
use my_module::bar
use my_other_module::baz

use statements can appear anywhere in the module file.

Type declaration sections

Constants (const)

Constants can be optionally declared with the const keyword at the top of an AirScript module just below the declaration of the module name. They can be scalars, vectors or matrices. Constant names must contain only uppercase letters.

Each constant is defined by an identifier and a value in the following format:

const FOO = 123;
const BAR = [1, 2, 3];
const BAZ = [[1, 2, 3], [4, 5, 6]];

In the above example, FOO is a constant of type scalar with value 123, BAR is a constant of type vector with value [1, 2, 3], and BAZ is a constant of type matrix with value [[1, 2, 3], [4, 5, 6]].

Execution trace (trace_columns)

A trace_columns section contains declarations for main trace columns or aux (auxiliary) trace columns.

The main and aux declarations define the shape of the main and auxiliary execution traces respectively and define identifiers which can be used to refer to each of the columns or a group of columns in that trace. The columns can also be referred using the built-in variables $main and $aux and the index of the column in the respective trace.

A trace_columns section with a main declaration is required for an AIR defined in AirScript to be valid. The aux declaration is optional, but if it is defined then it must follow the main declaration.

The following is a valid trace_columns source section:

trace_columns {
    main: [a, b, c[3], d]
    aux: [e, f]
}

In the above example, the main execution trace for the AIR has 6 columns with 4 column bindings, where the identifiers a, b, and d are each bound to a single column and c refers to a group of 3 columns. Single columns can be referenced using their identifiers (e.g. a, b and d) and columns in a group (e.g. c) can be referenced using the identifier c and the index of the column within the group c (c[0], c[1] and c[2]). Similarly, the auxiliary execution trace has 2 columns which can be referenced by e and f.

Public inputs (public_inputs)

A public_inputs section contains declarations for public inputs. Currently, each public input must be provided as a vector of a fixed size, but there is no limit to how many of them can be declared within the public_inputs section.

Public inputs are required. There must be at least one pubic input declared.

Each public input is described by an identifier and an array length (n) in the following format:

identifier: [n]

The following is an example of a valid public_inputs source section:

public_inputs {
    program_hash: [4],
    stack_inputs: [16],
    stack_outputs: [16],
}

In the above example, the public input program_hash is an array of length 4. stack_inputs and stack_outputs are both arrays of length 16.

Public inputs can be referenced by boundary constraints by using the identifier and an index. For example, the 3rd element of the program_hash declared above would be referenced as program_hash[2].

Periodic Columns (periodic_columns)

A periodic_columns section contains declarations for periodic columns used in the description and evaluation of integrity constraints. Each periodic column declares an array of periodic values which can then be referenced by the declared identifier.

There is no limit to how many of them can be declared within the periodic_columns section.

Periodic columns are optional. It is equally valid to define an empty periodic_columns section or to omit the periodic_columns section declaration entirely.

Each periodic column is described by an identifier and an array of integers in the following format. These integers are the periodic values.

identifier: [i, j, k, n],

The length of each of the array must be a power of two which is greater than or equal to 2.

The following is an example of a valid periodic_columns source section:

periodic_columns {
    k0: [0, 0, 0, 1],
    k1: [1, 1, 1, 1, 1, 1, 1, 0],
}

In the above example, k0 declares a periodic column with a cycle of length 4, and k1 declares a periodic column with a cycle of length 8.

Periodic columns can be referenced by integrity constraints by using the column's identifier.

When constraints are evaluated, these periodic values always refer to the value of the column in the current row. For example, when evaluating an integrity constraint such as enf k0 * a = 0, k0 would be evaluated as 0 in rows 0, 1, 2 of the trace and as 1 in row 3, and then the cycle would repeat. Attempting to refer to the "next" row of a periodic column, such as by k0', is invalid and will cause a ParseError.

Random values (random_values)

A random_values section contains declarations for random values provided by the verifier. Random values can be accessed by the named identifier for the whole array or by named bindings to single or grouped random values within the array.

Random values are optional. However if the section is declared then it cannot be empty and it can only contain a single declaration.

The following is an example of a valid random_values source section:

random_values {
    rand: [4],
}

In the above example, rand is a random value array of length 4. Random values can be accessed using $ followed by the name of the array and the index of the value. For example, $rand[2] would refer to the third random value in the array.

The following is an example of a valid random_values section with named bindings to particular random values and groups of random values:

random_values {
    rand: [a, b, c[2]],
}

In the above example, rand is a random value array of length 4 and a and b are individual random value bindings and c is a binding referring to a group of 2 random values. In this case, random values can be accessed similarly (e.g. $rand[2]) or using named bindings (e.g. a or c[0]). Here, $rand[2] and c[0] refer to the same random value.

Constraint description sections

Boundary constraints (boundary_constraints)

The boundary_constraints section consists of expressions describing the expected value of columns in the main or auxiliary traces at the specified boundary. Column boundaries can be selected using boundary accessors. Valid boundary accessors are .first, which selects the first cell of the column to which it is applied, and .last, which selects the last cell of the column column to which it is applied.

Boundary constraints are required. The boundary_constraints section must be defined and contain at least one boundary constraint.

Boundary constraints that are defined against auxiliary columns or that use random values from the built-in $rand array will be identified as auxiliary constraints.

A boundary constraint definition must:

1. start with a block indentation and the enf keyword to indicate that the constraint must be enforced.
2. continue by specifying a column identifier with a boundary accessor, e.g. a.first or a.last.
3. continue with =
4. continue with a right-hand-side "value" expression that evaluates to the required value of the specified column at the specified boundary. The expression may include numbers, named constants, variables, public inputs, random values, and any of the available operations.
5. end with a newline.

Simple example of boundary constraints

The following is a simple example of a valid boundary_constraints source section:

def BoundaryConstraintsExample

trace_columns {
    main: [a]
    aux: [p]
}

public_inputs {
    <omitted for brevity>
}

boundary_constraints {
    # these are main constraints.
    enf a.first = 0
    enf a.last = 10

    # these are auxiliary constraints, since they are defined against auxiliary trace columns.
    enf p.first = 1
    enf p.last = 1
}

integrity_constraints {
    <omitted for brevity>
}

Public inputs and random values

Boundary constraints can access public input values and random values provided by the verifier in their value expressions.

To use public inputs, the public input must be declared in the public_inputs source section. They can be accessed using array indexing syntax, as described by the accessor syntax rules.

To use random values, they must be declared in the random_values source section. Random values are defined by an identifier which is bound to a fixed-length array (e.g. rand: [16]), but it is additionally possible to bind identifiers to specific random values or groups of values (e.g. rand: [a, b[14], c]). Random values can be accessed by using $ followed by the array identifier and the index of the value (e.g. $rand[10]) or by using the name of the bound random value or group along with the index of the value within the group (e.g. a or b[5]), as described by the accessor syntax rules.

Example of boundary constraints with public inputs and random values

The following is an example of a valid boundary_constraints source section that uses public inputs and random values:

def BoundaryConstraintsExample

trace_columns {
    main: [a, b]
    aux: [p0, p1]
}

public_inputs {
    stack_inputs: [16]
    stack_outputs: [16]
}

boundary_constraints {
    # these are main constraints that use public input values.
    enf a.first = stack_inputs[0]
    enf a.last = stack_outputs[0]

    # these are auxiliary constraints that use public input values.
    enf p0.first = stack_inputs[1]
    enf p0.last = stack_outputs[1]

    # these are auxiliary constraints that use random values from the verifier.
    enf b.first = a + $rand[0]
    enf p1.first = (stack_inputs[2] + $rand[0]) * (stack_inputs[3] + $rand[1])
}

integrity_constraints {
    <omitted for brevity>
}

Intermediate variables

Boundary constraints can use intermediate variables to express more complex constraints. Intermediate variables are declared using the let keyword, as described in the variables section.

Example of boundary constraints with intermediate variables

The following is an example of a valid boundary_constraints source section that uses intermediate variables:

def BoundaryConstraintsExample

trace_columns {
    main: [a, b]
    aux: [p0, p1]
}

public_inputs {
    <omitted for brevity>
}

boundary_constraints {
    # this is an auxiliary constraint that uses intermediate variables.
    let x = $rand[0]
    let y = $rand[1]
    enf p1.first = x * y
}

integrity_constraints {
    <omitted for brevity>
}

Integrity constraints (integrity_constraints)

The integrity_constraints section consists of expressions describing constraints that must be true at each row of the execution trace in order for the proof to be valid.

Integrity constraints are required. The integrity_constraints section must be defined and contain at least one integrity constraint.

Integrity constraints that are defined against auxiliary columns or that use random values from the built-in $rand array will be identified as auxiliary constraints.

An integrity constraint definition must:

1. start with a block indentation and the enf keyword to indicate that the constraint must be enforced.
2. continue with an equality expression that describes the constraint. The expression may include numbers, constants, variables, trace columns, periodic columns, random values, and any of the available operations.
3. end with a newline.

Current and next rows

Integrity constraints have access to values in the "current" row of the trace to which the constraint is being applied, as well as the "next" row of the trace. The value of a trace column in the next row is specified with the ' postfix operator, as described by the accessor syntax rules.

Simple example of integrity constraints

The following is a simple example of a valid integrity_constraints source section using values from the current and next rows of the main and auxiliary traces:

def IntegrityConstraintsExample

trace_columns {
    main: [a, b],
    aux: [p],
}

public_inputs {
    <omitted for brevity>
}

boundary_constraints {
    <omitted for brevity>
}

integrity_constraints {
    # these are main constraints. they both express the same constraint.
    enf a' = a + 1;
    enf b' - b - 1 = 0;

    # this is an auxiliary constraint, since it uses an auxiliary trace column.
    enf p = p' * a;
}

Periodic columns and random values

Integrity constraints can access the value of any periodic column in the current row, as well as random values provided by the verifier.

To use periodic column values, the periodic column must be declared in the periodic_columns source section. The value in the current row can then be accessed by using the defined identifier of the periodic column.

Random values can be accessed by using array indexing syntax on the $rand built-in, as described by the accessor syntax rules.

Example of integrity constraints with periodic columns and random values

The following is an example of a valid integrity_constraints source section that uses periodic columns and random values:

def IntegrityConstraintsExample

trace_columns {
    main: [a, b],
    aux: [p0, p1],
}

public_inputs {
    <omitted for brevity>
}

periodic_columns {
    k: [1, 1, 1, 0],
}

random_values {
    rand: [16],
}

boundary_constraints {
    <omitted for brevity>
}

integrity_constraints {
    # this is a main constraint that uses a periodic column.
    enf a' = k * a;

    # this is an auxiliary constraint that uses a periodic column.
    enf p0' = k * p0;

    # these are auxiliary constraints that use random values from the verifier.
    enf b = a + $rand[0];
    enf p1 = k * (a + $rand[0]) * (b + $rand[1]);
}

Intermediate variables

Integrity constraints can use intermediate variables to express more complex constraints. Intermediate variables are declared using the let keyword, as described in the variables section.

Example of integrity constraints with intermediate variables

The following is an example of a valid integrity_constraints source section that uses intermediate variables:

def IntegrityConstraintsExample

trace_columns {
    main: [a, b]
    aux: [p0, p1]
}

public_inputs {
    <omitted for brevity>
}

random_values {
    rand: [16]
}

periodic_columns {
    k: [1, 1, 1, 0]
}

boundary_constraints {
    <omitted for brevity>
}

integrity_constraints {
    # this is an auxiliary constraint that uses intermediate variables.
    let x = a + $rand[0]
    let y = b + $rand[1]
    enf p1 = k * x * y
}

Local Variables and Built-in Variables

This section describes the syntax for declaring local variables and built-in variables.

Variables

In AirScript, variables can be declared in boundary_constraints and integrity_constraints sections and can contain any expression that would be valid within that source section. Variables can be of type scalar, vector or matrix. In the example below, x is a variable of type scalar, y is a variable of type vector and z is a variable of type matrix.

def VariablesExample

const A = 1;
const B = 2;

trace_columns {
    main: [a, b, c, d],
    aux: [e, f],
}

public_inputs {
    stack_inputs: [16],
}

random_values {
    rand: [16],
}

boundary_constraints {
    let x = stack_inputs[0] + stack_inputs[1]   ;
    let y = [$rand[0], $rand[1]]  ;
    enf e.first = x + y[0] + y[1];
}

integrity_constraints {
    let z = [
        [a + b, c + d],
        [A * a, B * b]
    ];
    enf a' = z[0][0] + z[0][1] + z[1][0] + z[1][1];
}

Syntax restriction for local variables

Currently, it is not possible to:

1. Create matrices containing both arrays and references to arrays.

   Example:

   ...
   boundary_constraints {
       let a = [[1,2], [3,4]];  # <-- this is allowed
       let b = [1, 2];
       let c = [a[1], b];  # <-- this is allowed
       let d = [b, [3, 4]];  # <-- this is not allowed, because `d` consists of array `[3, 4]` and reference to array `b`
       enf ...
   ...
   }
   

2. Create variables with list comprehension for which the source array is a inlined vector, a matrix row, or a range in matrix row.

   Example:

   ...
   integrity_constraints {
       let a = [[1, 2], [3, 4]];
       let b = [5, 6];
       let c = 7;
       let d = [e for e in [8, 9, 10]];  # <-- source array is an inlined vector
       let f = [g for g in a[1]];  # <-- source is a matrix row
       let h = [i for i in a[0][0..2]];  # <-- source is a range in matrix row
       enf ...
   ...
   }
   

Built-in variables

Built-in variables are identified by the starting character $. There are two built-in variables:

$main

$main is used to access columns in the main execution trace.

These columns may be accessed by using the indexing operator on $main. For example, $main[i] provides the (i+1)th column in the main execution trace.

Columns using the $main built-in may only be accessed within source sections for integrity constraints, i.e. the integrity_constraints section.

$aux

$aux is used to access columns in the auxiliary execution trace.

These columns may be accessed by using the indexing operator on $aux. For example, $aux[i] provides the (i+1)th column in the auxiliary execution trace.

Columns using the $aux built-in may only be accessed within source sections for integrity constraints, i.e. the integrity_constraints section.

Evaluators

Evaluators are sets of constraints logically grouped together. The primary purpose of evaluators is to increase modularity and readability of AirScript code.

Defining evaluators

An evaluator consists of a declaration which specifies evaluator metadata and a body which contains descriptions of integrity constraints.

Evaluator declaration starts with the ev keyword, followed by the name of the evaluator, parameter declarations, and a code block surrounded by braces. For example:

ev foo([a, b, c], [p]) {}

Evaluator name must:

• Be a string consisting of alpha-numeric characters and underscores.
• Start with a letter.
• Be unique among the evaluators declared in and imported by a module.

Evaluator parameters define an evaluator's view into the execution trace. Specifically, they define the set of columns in the main and the auxiliary trace segments the evaluator can access. For example, the evaluator declared above can access 3 columns of the main trace segment (which can be referenced as a, b, and c), and 1 column in the auxiliary trace segment (which can be referenced as p).

If an evaluator needs to access only the main trace segment, we can omit the parameters for the auxiliary trace segment. For example:

ev bar([a, b, c]) {}

If, however, an evaluator needs to access only the auxiliary trace segments, we must define the main trace segment parameters as an empty set like so:

ev baz([], [p]) {}

An evaluator body must contain at least one integrity constraint. For example:

ev foo([a, b]) {
    enf a' = a + b
}

In general, an evaluator body may contain any set of expressions allowed in the integrity constraints section subject to the following caveats:

• Evaluators can access only the trace columns defined via its parameters.
• Evaluators can access only constants and periodic columns defined in the same module.
• Evaluators can access random values defined in the root module.

Evaluators can be declared anywhere in a module, but usually are declared towards the end of the module.

Using evaluators

An evaluator defined in a module or imported from a different module can be invoked via the enf keyword. For example (public inputs and boundary constraints omitted for brevity):

trace_columns {
    main: [a, b],
}

integrity_constraints {
    enf foo([a, b]);
}

ev foo([x, y]) {
    enf x' = x + y;
}

In the above example, evaluator foo is invoked using trace columns a and b, but notice that within the evaluator we refer to these columns by different names (specifically, x and y respectively). The above example is equivalent to:

trace_columns {
    main: [a, b],
}

integrity_constraints {
    enf a' = a + b;
}

That is, we can think of evaluators as being inlined at their call sites.

Evaluators can be invoked multiple times. For example:

trace_columns {
    main: [a, b, c],
}

integrity_constraints {
    enf foo([a, b]);
    enf foo([c, a]);
}

ev foo([x, y]) {
    enf x' = x + y;
}

This is equivalent to:

trace_columns {
    main: [a, b, c],
}

integrity_constraints {
    enf a' = a + b;
    enf c' = c + a;
}

Evaluators can also invoke other evaluators. For example:

trace_columns {
    main: [a, b],
}

integrity_constraints {
    enf foo([a, b]);
}

ev foo([x, y]) {
    enf x' = x + y;
    enf bar([y, x]);
}

ev bar([x, y]) {
    enf x' = x * y;
}

The above is equivalent to:

trace_columns {
    main: [a, b],
}

integrity_constraints {
    enf a' = a + b;
    enf b' = b * a;
}

Using in conditional constraints

Evaluators can also be used in conditional constraints. The combination of evaluator and selector syntax is especially powerful as it enables describing complex constraints in a simple and modular way.

Convenience syntax

To make writing constraints easier, AirScript provides a number of syntactic conveniences. These are described in this section.

List comprehension

List comprehension provides a simple way to create new vectors. It is similar to the list comprehension syntax in Python. The following examples show how to use list comprehension in AirScript.

let x = [a * 2 for a in b];

This will create a new vector with the same length as b and the value of each element will be twice that of the corresponding element in b.

let x = [a + b for (a, b) in (c, d)];

This will create a new vector with the same length as c and d and the value of each element will be the sum of the corresponding elements in c and d. This will throw an error if c and d vectors are of unequal lengths.

let x = [2^i * a for (i, a) in (0..5, b)];

Ranges can also be used as iterables, which makes it easy to refer to an element and its index at the same time. This will create a new vector with length 5 and each element will be the corresponding element in b multiplied by 2 raised to the power of the element's index. This will throw an error if b is not of length 5.

const MAX = 5;
let x = [2^i * a for (i, a) in (0..MAX, b)];

Ranges are defined with each bound being either an integer literal, or a named constant of type scalar.

let x = [m + n + o for (m, n, o) in (a, 0..5, c[0..5])];

Slices can also be used as iterables. This will create a new vector with length 5 and each element will be the sum of the corresponding elements in a, the range 0 to 5, and the first 5 elements of c. This will throw an error if a is not of length 5 or if c is of length less than 5.

List folding

List folding provides syntactic convenience for folding vectors into expressions. It is similar to the list folding syntax in Python. List folding can be applied to vectors, list comprehension or identifiers referring to vectors and list comprehension. The following examples show how to use list folding in AirScript.

trace_columns {
    main: [a[5], b, c],
}

integrity_constraints {
    let x = sum(a);
    let y = sum([a[0], a[1], a[2], a[3], a[4]]);
    let z = sum([a * 2 for a in a]);
}

In the above, x and y both represent the sum of all trace column values in the trace column group a. z represents the sum of all trace column values in the trace column group a multiplied by 2.

trace_columns {
    main: [a[5], b, c],
}

integrity_constraints {
    let x = prod(a);
    let y = prod([a[0], a[1], a[2], a[3], a[4]]);
    let z = prod([a + 2 for a in a]);
}

In the above, x and y both represent the product of all trace column values in the trace column group a. z represents the product of all trace column values in the trace column group a added by 2.

Constraint comprehension

Constraint comprehension provides a way to enforce the same constraint on multiple values. Conceptually, it is very similar to the list comprehension described above. For example:

trace_columns {
    main: [a[5], b, c],
}

integrity_constraints {
    enf v^2 = v for v in a;
}

The above will enforce $a_i^2=a_i$ constraint for all columns in the trace column group a. Semantically, this is equivalent to:

trace_columns {
    main: [a[5], b, c],
}

integrity_constraints {
    enf a[0]^2 = a[0];
    enf a[1]^2 = a[1];
    enf a[2]^2 = a[2];
    enf a[3]^2 = a[3];
    enf a[4]^2 = a[4];
}

Similar to list comprehension, constraints in constraint comprehension can involve values from multiple lists. For example:

trace_columns {
    main: [a[5], b[5]],
}

integrity_constraints {
    enf x' = i * y for (x, y, i) in (a, b, 0..5);
}

The above will enforce that $a_i^{\prime }=i\cdot b_i$ for $i\in [0,5)$. If the length of either a or b is not 5, this will throw an error.

Conditional constraints

Frequently, we may want to enforce constraints based on some selectors. For example, let's say our trace has 4 columns: a, b, c, and s, and we want to enforce that $c^{\prime }=a+b$ when $s=1$ and $c^{\prime }=a\cdot c$ when $s=0$. We can write these constraints directly like so:

trace_columns {
    main: [a, b, c, s],
}

integrity_constraints {
    enf s^2 = s;
    enf c' = s * (a + b) + (1 - s) * (a * b);
}

Notice that we also need to enforce $s^2=s$ to ensure that column $s$ can contain only binary values.

While the above approach works, it gets more and more difficult to manage as selectors and constraints get more complicated. To simplify describing constraints for this use case, AirScript introduces enf match statement. The above constraints can be described using enf match statement as follows:

trace_columns {
    main: [a, b, c, s],
}

integrity_constraints {
    enf s^2 = s;
    enf match {
        case s: c' = a + b
        case !s: c' = a * c
    };
}

In the above, the syntax of each "option" is case <selector expression>: <constraint>, where selector expression consists of values composed using binary operands and logical operators !, &, and |. AirScript reduces logical operations to their equivalent algebraic operations as follows:

• !a reduces to $1-a$.
• a & b reduces to $a\cdot b$.
• a | b reduces to $a+b-a\cdot b$.

The example below illustrates how these operators can be used to build more complex selectors:

trace_columns {
    main: [a, b, c, s0, s1],
}

integrity_constraints {
    enf s0^2 = s0;
    enf s1^2 = s1;
    enf match {
        case s0 & s1:   c' = a + b
        case s0 & !s1:  c' = a * c
        case !s0 & s1:  c' = a - b
        case !s0 & !s1: c' = c
    };
}

AirScript makes the following assumptions about selector expressions, which are not yet enforced by the language:

1. All selector expressions are based on binary values. To enforce these, we must manually add constraints of the form $x^2=x$ for all values involved in selector expressions.
2. All selector expressions are mutually exclusive. That is, for a given set of inputs, only one of the selector expressions in an enf match statement can evaluate to $1$, and all other selectors must evaluate to $0$. Note: it is OK if all selector expressions evaluate to $0$.

Conditional evaluators

In addition to applying selectors to individual constraints, we can apply them to evaluators. For example:

trace_columns {
    main: [a, b, c, s],
}

integrity_constraints {
    enf s^2 = s;
    enf match {
        case s: foo([a, b, c])
        case !s: bar([a, b, c])
    };
}

ev foo([a, b, c]) {
    enf c' = a + b;
}

ev bar([a, b, c]) {
    enf c' = a * b;
}

The above is equivalent to the first example in this section. However, the real power of combining evaluators and conditional constraints comes from two aspects:

1. Evaluators can be imported from other modules. Thus, the logic of defining constraints, and then selecting which one is applied in a given case can be cleanly separated.
2. Evaluators can contain multiple constraints. In such cases, selector expressions would be applied to all constraints of an evaluator.

The example below illustrates the latter point.

trace_columns {
    main: [a, b, c, s],
}

integrity_constraints {
    enf s^2 = s;
    enf match {
        case s: foo([a, b, c])
        case !s: bar([a, b, c])
    };
}

ev foo([a, b, c]) {
    enf a' = a * 2;
    enf b' = b + 1;
    enf c' = a + b;
}

ev bar([a, b, c]) {
    enf a' = a + 1;
    enf b' = b * 3;
    enf c' = a * b;
}

Example AIR in AirScript

This is an example AIR definition in AirScript that includes all existing AirScript syntax. It is intended to be syntactically demonstrative rather than meaningful.

def ExampleAir

trace_columns {
    main: [s, a, b, c],
    aux: [p],
}

public_inputs {
    stack_inputs: [16],
    stack_outputs: [16],
}

periodic_columns {
    k0: [1, 1, 1, 1, 1, 1, 1, 0],
}

boundary_constraints {
    # define boundary constraints against the main trace at the first row of the trace.
    enf a.first = stack_inputs[0];
    enf b.first = stack_inputs[1];
    enf c.first = stack_inputs[2];

    # define boundary constraints against the main trace at the last row of the trace.
    enf a.last = stack_outputs[0];
    enf b.last = stack_outputs[1];
    enf c.last = stack_outputs[2];

    # set the first row of the auxiliary column p to 1
    enf p.first = 1;
}

integrity_constraints {
    # the selector must be binary.
    enf s^2 = s;

    # selector should stay the same for all rows of an 8-row cycle.
    enf k0 * (s' - s) = 0;

    # c = a + b when s = 0.
    enf (1 - s) * (c - a - b) = 0;

    # c = a * b when s = 1.
    enf s * (c - a * b) = 0;

    # the auxiliary column contains the product of values of c offset by a random value.
    enf p' = p * (c + $rand[0]);
}

Keywords

AirScript defines the following keywords:

• boundary_constraints: used to declare the source section where the boundary constraints are described.
  • first: used to access the value of a trace column at the first row of the trace. It may only be used when defining boundary constraints.
  • last: used to access the value of a trace column at the last row of the trace. It may only be used when defining boundary constraints.
• case: used to declare arms of conditional constraints.
• const: used to declare constants.
• def: used to define the name of a root AirScript module.
• enf: used to describe a single constraint.
  • enf match: used to describe conditional constraints.
• ev: used to declare a transition constraint evaluator.
• integrity_constraints: used to declare the source section where the integrity constraints are described.
• let: used to declare intermediate variables in the boundary_constraints or integrity_constraints source sections.
• mod: used to define a name of a library AirScript module.
• periodic_columns: used to declare the source section where the periodic columns are declared. They may only be referenced when defining integrity constraints.
• prod: used to fold a list into a single value by multiplying all of the values in the list together.
• public_inputs: used to declare the source section where the public inputs are declared. They may only be referenced when defining boundary constraints.
• random_values: used to declare the source section where the random values are described.
• sum: used to fold a list into a single value by summing all of the values in the list.
• trace_columns: used to declare the source section where the execution trace is described. They may only be referenced when defining integrity constraints.
  • main: used to declare the main execution trace.
  • aux: used to declare the auxiliary execution trace.
• use: used to import evaluators from library AirScript modules.
• $<identifier>: used to access random values provided by the verifier.
• $main: used to access columns in the main execution trace by index.
• $aux: used to access columns in the auxiliary execution trace by index.

Appendix

This appendix contains additional information about some concepts that are not covered in the main documentation.

Main vs. auxiliary execution trace segments (main and aux)

With Randomized AIRs, the construction of the execution trace can be split into multiple rounds, with the verifier providing new randomness between rounds. In the first round, before any random values are available, the Prover builds the first segment of the execution trace, which we refer to as the main trace (using Winterfell terminology). Additional trace segments can be built after the prover has committed to the first execution trace segment. When building auxiliary trace segments, the prover has access to the extra randomness sent by the verifier (in the non-interactive version of the protocol, this randomness is derived from the previous trace segment commitments). We refer to these as auxiliary trace segments (using Winterfell terminology again), and we call the first one the aux segment in AirScript and throughout this documentation.

Miden VM only makes use of one auxiliary trace segment, and in Winterfell the number of auxiliary trace segments is currently limited to one. Therefore, AirScript currently only supports the main execution trace called main and a single auxiliary trace segment called aux.

Backends

AirScript currently comes bundled with two backends:

• Winterfell backend which outputs Air trait implementation for the Winterfell prover (Rust).
• Miden assembly backend which outputs constraint evaluation code for the Miden VM recursive verifier.

These backends can be used programmatically as crates. They can also be used via AirScript CLI by specifying --target flag.

For example, the following will output Winterfell Air trait implementation for AIR constraints described in example.air file:

./target/release/airc transpile examples/example.air --target winterfell

While the following will output constraint evaluation code for the same constraints in Miden assembly.

./target/release/airc transpile examples/example.air --target masm

In both cases we assumed that the CLI has been compiled as described here.