Introduction

0xMiden 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 the main trace 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],)

• Buses: Users can declare buses which serve as communication channels between chiplets. They can be one of 2 types:

  • multiset: simple multi-set based bus.
  • logup: more complex LogUp based bus. (e.g. multiset p,, or logup q,)

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

• Integrity Constraints: Users can enforce integrity constraints on main trace columns and buses using trace columns, periodic columns, 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:
  • multi-table constraints.
  • type system.
• 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.
• additional language targets for simplifying verifier implementations:
  • Plonky3 AirBuilder.
  • JSON-based constraint syntax.
• formal verification

Language Description

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

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 or a bus, 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 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, b],
}

integrity_constraints {
  enf b' = b * 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 alphanumeric 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).
• 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 buses, 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 alphanumeric characters and underscores.
• Start with a letter.
• End with a newline.

Besides the name declaration, library modules may 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.

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.

The main declarations define the shape of the main execution trace 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 variable $main and the index of the column in the trace.

A trace_columns section with a main declaration is required for an AIR defined in AirScript to be valid.

The following is a valid trace_columns source section:

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

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]).

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 public 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.

Buses (buses)

A buses section contains declarations for buses used in the description and evaluation of integrity constraints.

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

buses {
    multiset p,
    logup q,
}

In the above example, we declare two buses: p of type multiset, and q of type logup. They respectively correspond to a multiset-based bus and a LogUp-based bus, that expand to different constraints. More information on bus types can be found in the buses section.

Constraint description sections

Boundary constraints (boundary_constraints)

The boundary_constraints section consists of expressions describing the expected value of columns in the main trace or for the buses 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 to which it is applied.

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

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, the null identifier in the case of buses, and any of the available operations.
5. end with a ; and 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],
}

public_inputs {
    <omitted for brevity>
}

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

integrity_constraints {
    <omitted for brevity>
}

Public inputs

Boundary constraints can access public input 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.

Example of bus boundary constraints with public inputs

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

def BoundaryConstraintsExample

trace_columns {
    main: [a, b],
}

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

buses {
    multiset p,
    logup q,
}

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 bus constraints that specify that buses must be empty at the beginning and the end of the execution trace
    enf p.first = null;
    enf p.last = null;
    enf q.first = null;
    enf q.last = null;
}

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],
}

public_inputs {
    <omitted for brevity>
}

boundary_constraints {
    # this is a constraint that uses intermediate variables.
    let x = 3
    let y = 4
    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.

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, bus operations and any of the available operations.
3. end with a ; and 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 trace:

def IntegrityConstraintsExample

trace_columns {
    main: [a, b],
}

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;
}

Periodic columns

Integrity constraints can access the value of any periodic column in the current row.

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.

Example of integrity constraints with periodic columns

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

def IntegrityConstraintsExample

trace_columns {
    main: [a, b],
}

public_inputs {
    <omitted for brevity>
}

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

boundary_constraints {
    <omitted for brevity>
}

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

Buses

Integrity constraints can constrain insertions and removal of elements into / from a given bus. The bus must first be declared in the buses source section. More information on bus types and the associated constraints can be found in the buses section.

Example of integrity constraints with buses

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

def IntegrityConstraintsExample

trace_columns {
    main: [a, s],
}

public_inputs {
    <omitted for brevity>
}

buses {
    multiset p,
}

boundary_constraints {
    <omitted for brevity>
}

integrity_constraints {
    # this is a bus constraint, inserting a into the bus p while s = 1
    p.insert(a) when s;
}

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],
}

public_inputs {
    <omitted for brevity>
}

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

boundary_constraints {
    <omitted for brevity>
}

integrity_constraints {
    # this is a main constraint that uses intermediate variables.
    let x = a + 2
    let y = b + 5
    enf b' = 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],
}

public_inputs {
    stack_inputs: [16],
}

boundary_constraints {
    let x = stack_inputs[0] + stack_inputs[1];
    let y = [stack_inputs[2], stack_inputs[3]];
    enf a.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.

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]) {}

Evaluator name must:

• Be a string consisting of alphanumeric 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 trace segment 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).

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

Buses

A bus is a construct which aims to simplify description of non-local constraints defined via multiset or LogUp checks.

Bus types

• Multiset (multiset): Multiset-based buses can represent constraints which specify values that must have been inserted or removed from a column, in no particular order. Miden VM - Multiset Checks Incremental Multiset Hash Functions and Their Application to Memory Integrity Checking - Clarke et al. MIT CSAIL (2018)

• LogUp (logup): LogUp-based buses are more complex than multiset buses, and can encode the multiplicity of an element: an element can be inserted or removed multiple times. Miden VM - LogUp: multivariate lookups with logarithmic derivatives Multivariate lookups based on logarithmic derivatives - Ulrich Haböck, Orbis Labs, Polygon Labs

Defining buses

See the declaring buses for more details.

buses {
    multiset p,
    logup q,
}

Bus boundary constraints

In the boundary constraints section, we can constrain the initial and final state of the bus. Currently, only constraining a bus to be empty (with the null keyword) is supported.

boundary_constraints {
    enf p.first = null;
    enf p.last = null;
}

The above example states that the bus p should be empty at the beginning and end of the trace.

Bus integrity constraints

In the integrity constraints section, we can insert and remove elements (as tuples of felts) into and from a bus. In the following examples, p and q are respectively multiset and LogUp based buses.

integrity_constraints {
    p.insert(a) when s1;
    p.remove(a, b) when 1 - s2;
}

Here, s1 and 1 - s2 are binary selectors: the element is inserted or removed when the corresponding selector's value is 1.

The global resulting constraint on the column of the bus is the following, where ${\alpha }_i$ corresponds to the i-th random value provided by the verifier:

$$p\prime \cdot (({\alpha }_0+{\alpha }_1\cdot a+{\alpha }_2\cdot b)\cdot (1-s2)+s2)=p\cdot (({\alpha }_0+{\alpha }_1\cdot a)\cdot s1+1-s1))$$

integrity_constraints {
    q.remove(e, f, g) when s;
    q.insert(a, b, c) with d;
}

Similarly to the previous example elements can be inserted or removed from q with binary selectors. However, as it is a LogUp-based bus, it is also possible to add and remove elements with a given scalar multiplicity with the with keyword (here, d does not have to be binary).

The global resulting constraint on the column of the bus is the following, where ${\alpha }_i$ corresponds to the i-th random value provided by the verifier:

$$q\prime +\frac{s}{{\alpha }_0+{\alpha }_1\cdot e+{\alpha }_2\cdot f+{\alpha }_3\cdot g}=q+\frac{d}{{\alpha }_0+{\alpha }_1\cdot a+{\alpha }_2\cdot b+{\alpha }_3\cdot c}$$

If we respectively note $v_{+}={\alpha }_0+{\alpha }_1\cdot a+{\alpha }_2\cdot b+{\alpha }_3\cdot c$ and $v_{-}={\alpha }_0+{\alpha }_1\cdot e+{\alpha }_2\cdot f+{\alpha }_3\cdot g$ the tuples inserted into and removed from the bus, the equation can be rewritten:

$$(q\prime -q)\cdot v_{+}\cdot v_{-}=s\cdot v_{+}+d\cdot v_{-}$$

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.

const Y = [
    [1, 2],
    [3, 4],
    [5, 6]
];
const X = [1, 2];
let c = [sum([x * y for (x, y) in (X, row_y)]) for row_y in Y];

List comprehensions can be nested. The above example creates a new vector c where each element is the sum of the products of corresponding elements in X and each row of Y. The outer list comprehension iterates over each row of Y, while the inner list comprehension iterates over each element in X and the current row of Y.

# The following will result in a parsing error:
let c = [[x * y for (x, y) in (X, row_y)] for row_y in Y];

List comprehensions can only have a scalar expression as their body. This means that the comprehension must always result in a vector of scalars. If the body of the comprehension is not a scalar expression, it will throw an error, like in the example above: notice that we removed the sum function from the body of the comprehension, which makes the outer comprehension's body a vector instead of a scalar expression. This is not valid syntax currently and will throw a parsing error.

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;
}

when keyword

The when keyword can be used to apply a binary selector to constraints where only one of the two branches is specified, the other being a no-op.

Its usage in the case of bus operations is handled separately, as defined in buses.md.

In the case of conditional constraints and conditional evaluators, constraint when selector is equivalent to:

enf match {
    case selector: constraint
    case !selector: 1 // this is a no_op
};

Examples:

A bus operation with a binary selector:

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

buses {
    multiset p,
}

integrity_constraints {
    enf s^2 = s;
    p.insert(a, b) when s;
}

A conditional constraint:

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

integrity_constraints {
    enf s^2 = s;
    enf c' = a + b when s;
}

A conditional evaluator:

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

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

integrity_constraints {
    enf s^2 = s;
    enf foo([a, b, c]) when s;
}

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],
}

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

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

buses {
    logup: q,
}

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 bus q to be initially empty
    enf q.first = null;
}

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;

    # insert p to the q bus when s = 1
    q.insert(p) when s;
}

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 / bus 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 / bus at the last row of the trace. It may only be used when defining boundary constraints.
  • null: used to specify an empty value for a bus. 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.
• for: used to specify the bound variable in a list comprehensions.
• in: used to specify the iterable in a list comprehension.
• insert: used to insert a tuple to a bus. It may only be used when defining integrity constraints.
• 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.
• remove: used to remove a tuple from a bus. It may only be used when defining integrity constraints.
• 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.
• use: used to import evaluators from library AirScript modules.
• when: used to specify a binary selector. It may only be used when defining integrity constraints:
  • bus integrity constraints.
  • conditional constraints and conditional evaluators.
• with: used to specify multiplicity in a LogUp bus operations, . It may only be used when defining integrity constraints.
• $main: used to access columns in the main execution trace by index.

Backends

AirScript currently comes bundled with two backends:

• Winterfell backend which outputs Air trait implementation for the Winterfell prover (Rust).

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

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