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:
- Begin with the
defkeyword, with no indentation.
- Continue with a string that does not begin with a number.
- End with a newline.
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
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:
Valid keywords for constraint description sections are the following:
By convention, type declaration sections precede constraint description sections, although this is not a requirement of the language.