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.1, which supports a simple syntax for describing air constraints and generation of Rust code targeting the Winterfell prover.
The simplified version of the language is based on this discussion, but only includes the following:
- declaring trace columns for main and auxiliary traces as a vector (e.g.
main: [a, b, c]
but notmain[a, b, c[2]]
) - declaring public inputs where each public input is a named vector (e.g.
stack_inputs: [16]
) - declaring periodic columns
- enforcing boundary constraints for main and auxiliary traces using trace columns, public inputs, and inline scalar constants
- enforcing transition constraints for main and auxiliary traces using trace columns, periodic columns, and inline scalar constants
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:
- modules and imports
- variable declarations (e.g.
let x = k1 * c[1]'
) - named constants (e.g. in a
constants
section), including:- vector constants
- matrix constants
- python-style list comprehension (and other "convenience" syntax)
- support for functions
- support for evaluators
- support for selectors
- optimizations, such as:
- removing unnecessary nodes from the
AlgebraicGraph
of integrity constraints - combining integrity constraints with mutually exclusive selectors to reduce the total number of constraints
- removing unnecessary nodes from the
- additional language targets for simplifying verifier implementations:
- Solidity
- Miden Assembly
- formal verification