|
| 1 | +An 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. |
| 2 | + |
| 3 | +Currently, all modules must be located in a single directory, but in the future this limitation will be removed. |
| 4 | + |
| 5 | +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. |
| 6 | + |
| 7 | +<center> |
| 8 | + |
| 9 | +| Section | Root module | Library module | |
| 10 | +| ------------------------------------------------------------------------------------- | :---------: | :---------------: | |
| 11 | +| [constants](type-declarations.md#constants-const) | optional | optional | |
| 12 | +| [trace columns](type-declarations.md#execution-trace-trace_columns) | required | not allowed | |
| 13 | +| [public inputs](type-declarations.md#public-inputs-public_inputs) | required | not allowed | |
| 14 | +| [periodic columns](type-declarations.md#periodic-columns-periodic_columns) | optional | optional | |
| 15 | +| [random values](type-declarations.md#random-values-random_values) | optional | not allowed | |
| 16 | +| [boundary constraints](constraints.md#boundary-constraints-boundary_constraints) | required | not allowed | |
| 17 | +| [integrity constraints](constraints.md#integrity-constraints-integrity_constraints) | required | not allowed | |
| 18 | +| [evaluators](evaluators.md) | optional | optional | |
| 19 | + |
| 20 | +</center> |
| 21 | + |
| 22 | +!!! note |
| 23 | + Constants and evaluators are not really distinct sections but rather a set of declarations which can be done in-between any other sections. |
| 24 | + |
| 25 | +### Root module |
| 26 | + |
| 27 | +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: |
| 28 | + |
| 29 | +``` |
| 30 | +def ExampleAir |
| 31 | +``` |
| 32 | + |
| 33 | +where the name of the module must: |
| 34 | + |
| 35 | +- Be a string consisting of alpha-numeric characters and underscores. |
| 36 | +- Start with a letter. |
| 37 | +- End with a newline. |
| 38 | + |
| 39 | +Besides the name declaration, a root module must: |
| 40 | + |
| 41 | +- Describe the shape of the execution trace (done via the *trace columns* section). |
| 42 | + - 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). |
| 43 | +- Describe the shape of the public inputs (done via the *public inputs* section). |
| 44 | +- Describe the boundary constraints placed against the execution trace (done via the *boundary constraints* section). |
| 45 | +- Describe the integrity constraints placed against the execution trace (done via the *integrity constraints* section). |
| 46 | + |
| 47 | +To aid with boundary and integrity constraint descriptions, a root module may also contain definitions of constants, evaluators, and periodic columns. |
| 48 | + |
| 49 | +### Library modules |
| 50 | + |
| 51 | +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: |
| 52 | + |
| 53 | +``` |
| 54 | +mod example_module |
| 55 | +``` |
| 56 | + |
| 57 | +where the name of the module must: |
| 58 | + |
| 59 | +- 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). |
| 60 | +- Be a string consisting of alpha-numeric characters and underscores. |
| 61 | +- Start with a letter. |
| 62 | +- End with a newline. |
| 63 | + |
| 64 | +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. |
| 65 | + |
| 66 | +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. |
| 67 | + |
| 68 | +## Importing evaluators |
| 69 | + |
| 70 | +A module can import constants and evaluators from library modules via a `use` statement. For example: |
| 71 | + |
| 72 | +``` |
| 73 | +use my_module::my_evaluator |
| 74 | +use my_module::my_constant |
| 75 | +``` |
| 76 | + |
| 77 | +where: |
| 78 | + |
| 79 | +- `my_module` is a library module located in the same directory as the importing module. |
| 80 | +- `my_evaluator` and `my_constant` is an evaluator and a constant defined in `my_module`. |
| 81 | + |
| 82 | +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. |
| 83 | + |
| 84 | +To import multiple evaluators and constants, multiple `use` statements must be used: |
| 85 | + |
| 86 | +``` |
| 87 | +use my_module::foo |
| 88 | +use my_module::bar |
| 89 | +use my_other_module::baz |
| 90 | +``` |
| 91 | + |
| 92 | +!!! note |
| 93 | + `use` statements can appear anywhere in the module file. |
0 commit comments