Winter AIR

This crate contains components needed to describe arbitrary computations in a STARK-specific format.

Arithmetization

Before we can generate proofs attesting that some computations were executed correctly, we need to reduce these computations to algebraic statements involving a set of bounded-degree polynomials. This step is usually called arithmetization. For basics of AIR arithmetization please refer to the excellent posts from StarkWare:

• Arithmetization I
• Arithmetization II
• StarkDEX Deep Dive: the STARK Core Engine

Coming up with efficient arithmetizations for computations is highly non-trivial, and describing arithmetizations could be tedious and error-prone. Air trait aims to help with the latter, which, hopefully, also makes the former a little simpler.

To define AIR for a given computation, you'll need to implement the Air trait which involves the following:

1. Define base field for your computation via the BaseField associated type (see math crate for available field options).
2. Define a set of public inputs which are required for your computation via the PublicInputs associated type.
3. Implement Air::new() function. As a part of this function you should create a AirContext struct which takes degrees for all transition constraints as one of the constructor parameters.
4. Implement context() method which should return a reference to the AirContext struct created in Air::new() function.
5. Implement evaluate_transition() method which should evaluate transition constraints over a given evaluation frame.
6. Implement get_assertions() method which should return a vector of assertions for a given instance of your computation.
7. If your computation requires periodic values, you can also override the default get_periodic_column_values() method.

For more information, take a look at the definition at the Air trait and check out examples crate which illustrates how to implement the trait for a several different computations.

Transition constraints

Transition constraints define algebraic relations between two consecutive steps of a computation. In Winterfell, transition constraints are evaluated inside evaluate_transition() function which takes the following parameters:

• frame: &EvaluationFrame<FieldElement>, which contains vectors with current and next states of the computation.
• periodic_values: &[FieldElement], when periodic columns are defined for a computation, this will contain values of periodic columns at the current step of the computation. Otherwise, this will be an empty slice.
• result: &mut [FieldElement], this is the slice where constraint evaluation results should be written to.

The constraints are considered to be satisfied if and only if, after the function returns, the result slice contains all zeros. In general, it is important for the transition constraint evaluation function to work as follows:

• For all valid transitions between consecutive computation steps, transition constraints should evaluation to all zeros.
• For any invalid transition, at least one constraint must evaluate to a non-zero value.

Keep in mind is that since transition constraints define algebraic relations, they should be described using only algebraic operations: additions, subtractions, and multiplications (divisions can be emulated using inverse of multiplication).

Constraint degrees

One of the main factors impacting proof generation time and proof size is the maximum degree of transition constraints. The higher is this degree, the larger our blowup factor needs to be. Usually, we want to keep this degree as low as possible - e.g. under 4 or 8. To accurately describe degrees of your transition constraints, keep the following in mind:

• All trace columns have degree 1.
• When multiplying trace columns together, the degree increases by 1. For example, if our constraint involves multiplication of two columns, the degree of this constraint will be 2. We can describe this constraint using TransitionConstraintDegree struct as follows: TransitionConstraintDegree::new(2).
• Degrees of periodic columns depend on the length of their cycles, but in most cases, these degrees are very close to 1.
• To describe a degree of a constraint involving multiplication of trace columns and periodic columns, use the with_cycles() constructor of TransitionConstraintDegree struct. For example, if our constraint involves multiplication of one trace column and one periodic column with a cycle of 32 steps, the degree can be described as: TransitionConstraintDegree::with_cycles(1, vec![32]).

In general, multiplications should be used judiciously - though, there are ways to ease this restriction a bit (check out mulfib8 example).

Trace assertions

Assertions are used to specify that a valid execution trace of a computation must contain certain values in certain cells. They are frequently used to tie public inputs to a specific execution trace, but can be used to constrain a computation in other ways as well. Internally within Winterfell, assertions are converted into boundary constraints.

To define assertions for your computation, you'll need to implement get_assertions() function of the Air trait. Every computation must have at least one assertion. Assertions can be of the following types:

• A single assertion - such assertion specifies that a single cell of an execution trace must be equal to a specific value. For example: value in column 0, step 0, must be equal to 1.
• A periodic assertion - such assertion specifies that values in a given column at specified intervals should be equal to some values. For example: values in column 0, steps 0, 8, 16, 24 etc. must be equal to 2.
• A sequence assertion - such assertion specifies that values in a given column at specific intervals must be equal to a sequence of provided values. For example: values in column 0, step 0 must be equal to 1, step 8 must be equal to 2, step 16 must be equal to 3 etc.

For more information on how to define assertions see the assertions module and check out the examples in the examples crate.

Periodic values

Sometimes, it may be useful to define a column in an execution trace which contains a set of repeating values. For example, let's say we have a column which contains value 1 on every 4th step, and 0 otherwise. Such a column can be described with a simple periodic sequence of [1, 0, 0, 0].

To define such columns for your computation, you can override get_periodic_column_values() method of the Air trait. The values of the periodic columns at a given step of the computation will be supplied to the evaluate_transition() method via the periodic_values parameter.

Randomized AIR

Randomized AIR is a powerful extension of AIR which enables, among other things, multiset and permutation checks similar to the ones available in PLONKish systems. These, in turn, allow efficient descriptions of "non-local" constraints which can be used to build such components as efficient range checks, random access memory, and many others.

With Randomized AIR, construction of the execution trace is split into multiple stages. During the first stage, the main trace segment is built in a manner similar to how the trace is built for regular AIR. In the subsequent stages, auxiliary trace segment is built. When building the auxiliary trace segment, the prover has access to extra randomness sent by the verifier (in the non-interactive version of the protocol, this randomness is derived from the previous trace segment commitments).

To describe Randomized AIR, you will need to do the following when implementing the Air trait:

• The AirContext struct returned from Air::context() method must be instantiated using AirContext::new_multi_segment() constructor. When building AIR context in this way, you will need to provide a TraceLayout which describes the shape of a multi-segment execution trace.
• Override Air::evaluate_aux_transition() method. This method is similar to the Air::evaluate_transition() method but it also accepts two extra parameters: aux_evaluation_frame and aux_rand_elements. These parameters are needed for evaluating transition constraints over the auxiliary trace segment.
• Override Air::get_aux_assertions() method. This method is similar to the Air::get_assertions() method, but it should return assertions against columns of the auxiliary trace segment.

Protocol parameters

ProofOptions struct defines a set of options which are used during STARK proof generation and verification. These options have a direct impact on the security of the generated proofs as well as the proof generation time. Specifically, security of STARK proofs depends on:

1. Hash function - proof security is limited by the collision resistance of the hash function used by the protocol. For example, if a hash function with 128-bit collision resistance is used, security of a STARK proof cannot exceed 128 bits.
2. Finite field - proof security is limited by the finite field used by the protocol. This means, that for small fields (e.g. smaller than ~128 bits), field extensions must be used to achieve adequate security. And even for ~128 bit fields, to achieve security over 100 bits, a field extension may be required.
3. Number of queries - higher values increase proof security, but also increase proof size.
4. Blowup factor - higher values increase proof security, but also increase proof generation time and proof size. However, higher blowup factors require fewer queries for the same security level. Thus, it is frequently possible to increase blowup factor and at the same time decrease the number of queries in such a way that the proofs become smaller.
5. Grinding factor - higher values increase proof security, but also may increase proof generation time.

See options.rs for more info on currently available options and their meaning. Additionally, security level of a proof can be estimated using Proof::security_level() function.

Crate features

This crate can be compiled with the following features:

• std - enabled by default and relies on the Rust standard library.
• no_std - does not rely on the Rust standard library and enables compilation to WebAssembly.

To compile with no_std, disable default features via --no-default-features flag.

License

This project is MIT licensed.