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
.. is used to define ranges used in constraint descriptions.
[ 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)

Slice expressions may be used in constraint descriptions to create sub-arrays from arrays. The syntax for slice expressions is array_name[start_index..end_index], where start_index is inclusive and end_index is exclusive.

Requirements for slice expressions:

Both start_index and end_index must be non-negative constants integer literals or named constant of scalar type.
start_index must be less than or equal to end_index.
nested slices are only supported through evaluator calls.

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

AirScript by Miden