-
Notifications
You must be signed in to change notification settings - Fork 19
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
Merge pull request #69 from 0xPolygonMiden/finalize-v01
Finalize v0.1
- Loading branch information
Showing
23 changed files
with
229 additions
and
37 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
|
@@ -3,5 +3,5 @@ members = [ | |
"air-script", | ||
"parser", | ||
"ir", | ||
"codegen-winter" | ||
"codegen/winterfell" | ||
] |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,20 +1,31 @@ | ||
# AirScript | ||
|
||
A domain specific language to write AIR constraints for the [Miden VM](https://github.com/maticnetwork/miden/). | ||
A domain-specific language for expressing AIR constraints for STARKs, especially for STARK-based virtual machines like [Miden VM](https://github.com/maticnetwork/miden/). | ||
|
||
NOTE: This project is in the initial stages of development. | ||
An in-depth description of AirScript is available in the full AirScript [documentation](https://0xpolygonmiden.github.io/air-script/). | ||
|
||
**WARNING**: This project is in an alpha stage. It has not been audited and may contain bugs and security flaws. This implementation is NOT ready for production use. | ||
|
||
## Overview | ||
|
||
AirScript is a domain specific language for writing AIR constraints for the STARK proving system. The primary goals of AirScript is to enable writing and auditing AIR constraints without the need to learn a specific programming language (e.g., Rust). The secondary goal is to perform automated optimizations of constraints and to output constraint evaluator code to multiple backends (e.g., Rust, Miden assembly, Solidity etc.). | ||
AirScript is a domain-specific language for writing AIR constraints for the STARK proving system. The primary goal of AirScript is to enable writing and auditing AIR constraints without the need to learn a specific programming language (e.g., Rust). The secondary goal is to perform automated optimizations of constraints and to output constraint evaluator code in multiple target languages (e.g., Rust, Miden assembly, Solidity etc.). | ||
|
||
## Project Structure | ||
|
||
The project is organized into several crates like so: | ||
| Crate | Description | | ||
The project is organized into several crates as follows: | ||
| Crate | Description | | ||
| ---------------------- | ----------- | | ||
| [Parser](parser) | Contains parser for the AirScript. The parser is used to parse the constraints written in AirScript into an AST. | | ||
| [Parser](parser) | Contains the parser for AirScript. The parser is used to parse the constraints written in AirScript into an AST. | | ||
| [IR](ir) | Contains the IR for AirScript, `AirIR`. `AirIR` is initialized with an AirScript AST, which it converts to an internal representation that can be optimized and used to generate code in multiple target languages. | | ||
| [Winterfell code generator](codegen/winterfell/) | Contains a code generator targeting the [Winterfell prover](https://github.com/novifinancial/winterfell) Rust library. The Winterfell code generator converts a provided AirScript `AirIR` into Rust code that represents the AIR as a new custom struct that implements Winterfell's `Air` trait. | | ||
|
||
## References | ||
1. [Lalrpop](https://github.com/lalrpop/lalrpop/): Rust parser generator framework. | ||
2. [Logos](https://github.com/maciejhirsz/logos/): Library to help in creating a lexer. | ||
|
||
1. [Logos](https://github.com/maciejhirsz/logos/): Library for generating fast lexers in Rust. | ||
1. [LALRPOP](https://github.com/lalrpop/lalrpop/): LR(1) Rust parser generator framework. | ||
1. [Codegen](https://github.com/carllerche/codegen): Library for generating Rust code. | ||
1. [mdBook](https://github.com/rust-lang/mdBook): Utility for creating online documentation books. | ||
|
||
## License | ||
|
||
This project is [MIT licensed](./LICENSE). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,57 @@ | ||
# AirScript Compiler | ||
|
||
This crate aggregates all components of the AirScript compiler into a single place. Specifically, it re-exports functionality from the [parser](../parser/), [ir](../ir/), and [winterfell code generator](../codegen/winterfell/) crates. Additionally, when compiled as an executable, this crate can be used via a [CLI](#command-line-interface-cli) to transpile AIRs defined in AirScript to a specified target language. | ||
|
||
## Basic Usage | ||
|
||
An in-depth description of AirScript is available in the full AirScript [documentation](https://0xpolygonmiden.github.io/air-script/). | ||
|
||
The compiler has three stages, which can be imported and used independently or together. | ||
|
||
1. [Parser](../parser/): scans and parses AirScript files and builds an AST | ||
2. [IR](../ir/): produces an intermediate representation from an AirScript AST | ||
3. [Code generation](../codegen/): translate an `AirIR` into a specific target language | ||
- [Winterfell Code Generator](../codegen/winterfell/): generates Rust code targeting the [Winterfell prover](https://github.com/novifinancial/winterfell). | ||
|
||
Example usage: | ||
|
||
```Rust | ||
use air_script::{parse, AirIR, CodeGenerator}; | ||
|
||
// parse the source string to a Result containing the AST or an Error | ||
let ast = parse(source.as_str()).expect("Parsing failed"); | ||
|
||
// process the AST to get a Result containing the AirIR or an Error | ||
let ir = AirIR::from_source(&ast).expect("AIR is invalid"); | ||
|
||
// generate Rust code targeting the Winterfell prover | ||
let rust_code = CodeGenerator::new(&ir); | ||
``` | ||
|
||
There are several example `.air` files written in AirScript which can be found in the `examples/` directory. | ||
|
||
To run the full transpilation pipeline, the CLI can be used for convenience. | ||
|
||
## Command-Line Interface (CLI) | ||
|
||
There is a command-line interface available for transpiling AirScript files. Currently, the only available target is Rust code for use with the [Winterfell](https://github.com/novifinancial/winterfell) STARK prover library. | ||
|
||
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/system.air | ||
``` | ||
|
||
When no output destination is specified, the output file will use the path and name of the input file, replacing the `.air` extension with `.rs`. For the above example, `examples/system.rs` will contain the generated output. | ||
|
||
You can use the `help` option to see other available options. | ||
|
||
``` | ||
./target/release/airc transpile --help | ||
``` |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,11 @@ | ||
// EXPORTS | ||
// ================================================================================================ | ||
|
||
/// AirScript parse method to generate an AST from AirScript source files | ||
pub use parser::parse; | ||
|
||
/// AirScript intermediate representation | ||
pub use ir::AirIR; | ||
|
||
/// Code generation targeting Rust for the Winterfell prover | ||
pub use codegen_winter::CodeGenerator; |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,8 @@ | ||
[package] | ||
name = "air-codegen-winter" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
[dependencies] | ||
codegen = "0.2.0" | ||
ir = {package = "air-ir", path="../../ir", version="0.1.0" } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,44 @@ | ||
# Winterfell Code Generator | ||
|
||
This crate contains a code generator targeting the [Winterfell prover](https://github.com/novifinancial/winterfell) Rust library. | ||
|
||
The purpose of this code generator is to convert a provided `AirIR` representation of an AIR into a custom Rust struct that implements Winterfell's `Air` trait. The generated code can be used instead of writing a custom Winterfell `Air` implementation directly in Rust. | ||
|
||
## Generating the Winterfell Rust Code | ||
|
||
Generate Rust code from an `AirIR` (AirScript's intermediate representation) by instantiating a new `CodeGenerator` with an AirScript AST (the output of the AirScript parser) and then calling `generate`. The `generate` method will return the Rust code implementation as a `String`. | ||
|
||
Instantiating the `CodeGenerator` will add the required Winterfell imports, create a custom `struct` using the name defined for the AIR, then implement the Winterfell `Air` trait for the custom `struct`. | ||
|
||
Example usage: | ||
|
||
```Rust | ||
// parse the source string to a Result containing the AST or an Error | ||
let ast = parse(source.as_str()).expect("Parsing failed"); | ||
|
||
// process the AST to get a Result containing the AirIR or an Error | ||
let ir = AirIR::from_source(&ast).expect("AIR is invalid"); | ||
|
||
// generate Rust code targeting the Winterfell prover | ||
let rust_code = CodeGenerator::new(&ir); | ||
``` | ||
|
||
## Generated Winterfell Rust Code | ||
|
||
The following code is generated for the Winterfell `Air` trait implementation: | ||
|
||
- declaration and implementation of a `PublicInputs` struct. | ||
- custom struct declaration and implementation, using the defined name of the AIR from the original AirScript file | ||
- implementation of Winterfell `Air` trait: | ||
- constraint-related declarations as part of the `AirContext` creation in the `new` method: | ||
- the number of boundary constraints for the main trace | ||
- the number of boundary constraints for the auxiliary trace | ||
- the order and degrees of the transition constraints for the main trace | ||
- the order and degrees of the transition constraints for the auxiliary trace | ||
- getters for: | ||
- periodic column values (`get_periodic_column_values`) | ||
- main trace boundary constraints (`get_assertions`) | ||
- auxiliary trace boundary constraints (`get_aux_assertions`) | ||
- transition constraint evaluation code for: | ||
- main trace transition constraints (`evaluate_transition`) | ||
- auxiliary trace transition constraints (`evaluate_aux_transition`) |
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
File renamed without changes.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,9 @@ | ||
# AirScript docs | ||
|
||
This crate contains source files and assets for [AirScript documentation](https://0xpolygonmiden.github.io/air-script/). | ||
|
||
All doc files are written in Markdown and are converted into an online book using the [mdBook](https://github.com/rust-lang/mdBook) utility. | ||
|
||
## License | ||
|
||
This project is [MIT licensed](../LICENSE). |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,7 @@ | ||
[package] | ||
name = "ir" | ||
version = "0.0.1" | ||
name = "air-ir" | ||
version = "0.1.0" | ||
edition = "2021" | ||
|
||
[dependencies] | ||
parser = { package = "parser", path = "../parser", version = "0.0.1" } | ||
parser = { package = "air-parser", path = "../parser", version = "0.1.0" } |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,33 @@ | ||
# Intermediate Representation (IR) | ||
|
||
This crate contains the intermediate representation for AirScript, `AirIR`. | ||
|
||
The purpose of the `AirIR` is to provide a simple and accurate representation of an AIR that allows for optimization and translation to constraint evaluator code in a variety of target languages. | ||
|
||
## Generating the AirIR | ||
|
||
Generate an `AirIR` from an AirScript AST (the output of the AirScript parser) using the `from_source` method. The `from_source` method will return a new `AirIR` or an `Error` of type `SemanticError` if it encounters any errors while processing the AST. | ||
|
||
The `from_source` method will first iterate through the source sections that contain declarations to build a symbol table with trace columns, public inputs, and periodic columns. It will return a `SemanticError` if it encounters a duplicate, incorrect, or missing declaration. Once the symbol table is built, the constraints in the `boundary_constraints` and `transition_constraints` sections of the AST are processed. Finally, `from_source` returns a Result containing the `AirIR` or a `SemanticError`. | ||
|
||
Example usage: | ||
|
||
```Rust | ||
// parse the source string to a Result containing the AST or an Error | ||
let ast = parse(source.as_str()).expect("Parsing failed"); | ||
|
||
// process the AST to get a Result containing the AirIR or an Error | ||
let ir = AirIR::from_source(&ast) | ||
``` | ||
|
||
## AirIR | ||
|
||
Although generation of an `AirIR` uses a symbol table while processing the source AST, the internal representation only consists of the following: | ||
|
||
- **Name** of the AIR definition represented by the `AirIR`. | ||
- **Public inputs**, represented by a vector that maps an identifier to a size for each public input that was declared. (Currently, public inputs can only be declared as fixed-size arrays.) | ||
- **Periodic columns**, represented by an ordered vector that contains each periodic column's repeating pattern (as a vector). | ||
- **Boundary constraints**, stored as mappings from trace column indices to expressions, with a separate mapping for each boundary (first and last) of each trace segment (main and auxiliary). | ||
- **Transition constraints**, represented by the combination of: | ||
- a directed acyclic graph (DAG) without duplicate nodes. | ||
- a vector of `NodeIndex` for each of the main and auxiliary trace segments, which contains the node index in the graph where each of the respective trace segment's constraints starts. |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters