### 4 releases (breaking)

Uses new Rust 2021

0.4.0 | Apr 29, 2022 |
---|---|

0.3.0 | Jan 5, 2022 |

0.2.0 | Aug 24, 2021 |

0.1.0 | Aug 4, 2021 |

#**6** in #air

**1,082** downloads per month

Used in **8** crates
(3 directly)

**MIT**license

705KB

11K
SLoC

# 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:

Coming up with efficient arithmetizations for computations is highly non-trivial, and describing arithmetizations could be tedious and error-prone.

trait aims to help with the latter, which, hopefully, also makes the former a little simpler.`Air`

To define AIR for a given computation, you'll need to implement the

trait which involves the following:`Air`

- Define base field for your computation via the

associated type (see math crate for available field options).`BaseField` - Define a set of public inputs which are required for your computation via the

associated type.`PublicInputs` - Implement

function. As a part of this function you should create a`Air`new`::``(``)`

struct which takes degrees for all transition constraints as one of the constructor parameters.`AirContext` - Implement

method which should return a reference to the`context``(``)`

struct created in`AirContext`

function.`Air`new`::``(``)` - Implement

method which should evaluate transition constraints over a given evaluation frame.`evaluate_transition``(``)` - Implement

method which should return a vector of assertions for a given instance of your computation.`get_assertions``(``)` - If your computation requires periodic values, you can also override the default

method.`get_periodic_column_values``(``)`

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

function which takes the following parameters:`evaluate_transition``(``)`

**frame**:

, which contains vectors with current and next states of the computation.`&``EvaluationFrame``<`FieldElement`>`**periodic_values**:

, 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.`&``[`FieldElement`]`**result**:

, this is the slice where constraint evaluation results should be written to.`&``mut``[`FieldElement`]`

The constraints are considered to be satisfied if and only if, after the function returns, the

slice contains all zeros. In general, it is important for the transition constraint evaluation function to work as follows:`result`

- 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

. For example, if our constraint involves multiplication of two columns, the degree of this constraint will be`1`

. We can describe this constraint using`2`

struct as follows:`TransitionConstraintDegree`

.`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

constructor of`with_cycles``(``)`

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`

.`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

function of the `get_assertions``(``)`

trait. Every computation must have at least one assertion. Assertions can be of the following types:`Air`

- 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

method of the `get_periodic_column_values``(``)`

trait. The values of the periodic columns at a given step of the computation will be supplied to the `Air`

method via the `evaluate_transition``(``)`

parameter.`periodic_values`

### 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 segments* are built. When building auxiliary trace segments, 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). Currently, the number of auxiliary trace segments is limited to one.

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

trait:`Air`

- The

struct returned from`AirContext`

method must be instantiated using`Air`context`::``(``)`

constructor. When building AIR context in this way, you will need to provide a`AirContext`new_multi_segment`::``(``)`

which describes the shape of a multi-segment execution trace.`TraceLayout` - Override

method. This method is similar to the`Air`evaluate_aux_transition`::``(``)`

method but it also accepts two extra parameters:`Air`evaluate_transition`::``(``)`

and`aux_evaluation_frame`

. These parameters are needed for evaluating transition constraints over the auxiliary trace segments.`aux_rand_elements` - Override

method. This method is similar to the`Air`get_aux_assertions`::``(``)`

method, but it should return assertions against columns of the auxiliary trace segments.`Air`get_assertions`::``(``)`

## Protocol parameters

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:`ProofOptions`

- 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.
- 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.
- Number of queries - higher values increase proof security, but also increase proof size.
- 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.
- 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

function.`StarkProof ::`security_level

`(`

`)`

## Crate features

This crate can be compiled with the following features:

- enabled by default and relies on the Rust standard library.`std`

- does not rely on the Rust standard library and enables compilation to WebAssembly.`no_std`

To compile with

, disable default features via `no_std`

flag.`--no-default-features`

## License

This project is MIT licensed.

#### Dependencies

~2.5MB

~47K SLoC