Introduction

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

Current Version

Currently, AirScript is on version 0.2, which supports a simple syntax for describing air constraints and generation of Rust code targeting the Winterfell prover.

The language is based on this discussion, and includes features to write ~90% of the constraints required for Miden albeit with some limitations.

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

The language also includes some convenience syntax like list comprehension and list folding to make writing constraints easier. (e.g. let x = [k * c for (k, c) in (k, c[1..4])], let y = sum([k * c for (k, c) in (k, c[1..4])]))

The language will be specified in detail in the rest of this book.

CLI

There is a command-line interface available for transpiling AirScript files to Rust. 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 and specify your input file with -i. For example:

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

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:
  • python-style list comprehension (and other "convenience" syntax)
  • modules and imports
  • support for functions
  • support for evaluators
  • support for selectors
• 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:
  • Solidity
  • Miden Assembly
• formal verification

Language Description

• Syntax overview
• File structure
• Type declarations
• Variables
• Convenience syntax
• Constraint descriptions
• 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
• $ 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

File Structure

An AIR Script file consists of a name definition and several source sections which contain declarations and constraints. The declarations describe the shape of the execution trace to which constraints are applied and the public inputs, and periodic columns that are used for computing those constraints. The constraints describe boundary and integrity constraints which must hold for an execution trace and set of public inputs in order for them to be valid (i.e. in order for a valid proof to be generated or verification to pass).

AIR name definition

An AirScript file starts with a definition of the name of the AIR module, such as:

def ExampleAir

It must:

• Begin with the def keyword, with no indentation.
• Continue with a string that does not begin with a number.
• End with a newline.

Constant declarations

Constants can be declared using the const keyword, followed by an identifier with uppercase letters only, an = sign and a value. For example:

const FOO = 42

Constants are conventionally declared at the top of the module just after Air name definition section. Constants may be used in any boundary_constraints or integrity_constraints sections.

Source sections

All source sections must:

• Begin with a valid source section keyword, followed by : and a newline.
• Have all contents in an indented block.

This is an example of a well-formed source section:

# source section keyword
trace_columns:
    # indented content block
    main: [a, b, c, d]
    aux: [x, y, z]

Valid keywords for type declaration sections are the following:

• trace_columns
• public_inputs
• periodic_columns
• random_values

Valid keywords for constraint description sections are the following:

• boundary_constraints
• integrity_constraints

By convention, type declaration sections precede constraint description sections, although this is not a requirement of the language.

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.

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.

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.

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 binding a. z represents the sum of all trace column values in the trace column binding 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 binding a. z represents the product of all trace column values in the trace column binding a added by 2.

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]

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>

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

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.
• const: used to declare constants.
• def: used to define the name of an AirScript module.
• enf: used to describe a single constraint.
• 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.
• 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.
• $<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.

Language Implementation

This is a high-level overview of the implementation.

Parser

The parser is split into 3 modules:

• a scanner built using the Logos lexer-generator tool
• an LR(1) parser generated by the LALRPOP parser-generator framework
• an AST for representing the parsed AIR description

IR

The IR is where semantic checking is done and where optimizations will be done in the future.

A directed acyclic graph called AlgebraicGraph is responsible for efficiently representing all boundary and integrity constraints, identifying their domain (i.e. the rows they should be applied to), identifying their trace segment (main or auxiliary), and computing their degrees.

Building the graph

While building the graph, the IR associates the following information with each constraint:

• For integrity constraints, identifies the trace segment and the type of the integrity constraint (transition or validity) based on the constraint expression.
  • Constraints referencing the auxiliary trace columns or using random values are identified as constraints against the auxiliary trace (trace segment 1). All other constraints are identified as constraints against the main trace (trace segment 0).
  • Constraints referencing the "next" indicator are identified as transition constraints. All other constraints are identified as validity constraints.
• For boundary constraints, identifies the trace segment and constraint domain (first or last row) based on the trace column and the boundary to which the constraint is applied.

Error checking

Currently, error checking in the IR covers the following cases

Identifiers

• Prevent duplicate identifier declarations.
• Prevent usage of undeclared identifiers.

Periodic columns

• Ensure the cycle length of periodic columns is valid (greater than the minimum and a power of two).

Boundary constraints

• Prevent multiple constraints against the same column at the same boundary.
• Ensure boundary constraint expressions contain valid identifier references by:
  • Preventing periodic columns from being used by boundary constraints.
  • Ensuring valid indices for vector accesses (e.g. for public inputs, random values, vector constants or vector variables) or matrix accesses (e.g. for matrix constants or matrix variables).
  • Ensuring valid identifier types for vector and matrix accesses.

Integrity constraints

• Ensure integrity constraints contain valid identifier references by:
  • Preventing public inputs from being used.
  • Preventing "next" indicators from being applied to anything other than trace columns.
  • Ensuring valid indices for vector accesses (e.g. for public inputs, random values, vector constants or vector variables) or matrix accesses (e.g. for matrix constants or matrix variables).
  • Ensuring valid identifier types for vector and matrix accesses.

Winterfell Codegen

The codegen/winterfell crate provides a code generator for a Rust implementation of the Winterfell prover's Air trait from an instance of an AirScript IR.

AirScript Core

The air-script-core crate contains commonly used constants and structs used by the other crates.