Language Implementation

This is a high-level overview of the implementation.

Parser

The parser is split into 3 modules:

  • a scanner built using the Logos lexer-generator tool
  • an LR(1) parser generated by the LALRPOP parser-generator framework
  • an AST for representing the parsed AIR description

IR

The IR is where semantic checking is done and where optimizations will be done in the future.

A directed acyclic graph called AlgebraicGraph is responsible for efficiently representing all boundary and integrity constraints, identifying their domain (i.e. the rows they should be applied to), identifying their trace segment (main or auxiliary), and computing their degrees.

Building the graph

While building the graph, the IR associates the following information with each constraint:

  • For integrity constraints, identifies the trace segment and the type of the integrity constraint (transition or validity) based on the constraint expression.
    • Constraints referencing the auxiliary trace columns or using random values are identified as constraints against the auxiliary trace (trace segment 1). All other constraints are identified as constraints against the main trace (trace segment 0).
    • Constraints referencing the "next" indicator are identified as transition constraints. All other constraints are identified as validity constraints.
  • For boundary constraints, identifies the trace segment and constraint domain (first or last row) based on the trace column and the boundary to which the constraint is applied.

Error checking

Currently, error checking in the IR covers the following cases

Identifiers

  • Prevent duplicate identifier declarations.
  • Prevent usage of undeclared identifiers.

Periodic columns

  • Ensure the cycle length of periodic columns is valid (greater than the minimum and a power of two).

Boundary constraints

  • Prevent multiple constraints against the same column at the same boundary.
  • Ensure boundary constraint expressions contain valid identifier references by:
    • Preventing periodic columns from being used by boundary constraints.
    • Ensuring valid indices for vector accesses (e.g. for public inputs, random values, vector constants or vector variables) or matrix accesses (e.g. for matrix constants or matrix variables).
    • Ensuring valid identifier types for vector and matrix accesses.

Integrity constraints

  • Ensure integrity constraints contain valid identifier references by:
    • Preventing public inputs from being used.
    • Preventing "next" indicators from being applied to anything other than trace columns.
    • Ensuring valid indices for vector accesses (e.g. for public inputs, random values, vector constants or vector variables) or matrix accesses (e.g. for matrix constants or matrix variables).
    • Ensuring valid identifier types for vector and matrix accesses.

Winterfell Codegen

The codegen/winterfell crate provides a code generator for a Rust implementation of the Winterfell prover's Air trait from an instance of an AirScript IR.

AirScript Core

The air-script-core crate contains commonly used constants and structs used by the other crates.