Trait winter_prover::Air[−][src]

pub trait Air: Send + Sync {
    type BaseElement: StarkField;
    type PublicInputs: Serializable;

Show 26 methods    fn new(
        trace_info: TraceInfo, 
        pub_inputs: Self::PublicInputs, 
        options: ProofOptions
    ) -> Self;

    fn context(&self) -> &AirContext<Self::BaseElement>;

    fn evaluate_transition<E>(
        &self, 
        frame: &EvaluationFrame<E>, 
        periodic_values: &[E], 
        result: &mut [E]
    )
    where
        E: FieldElement<BaseField = Self::BaseElement>;

    fn get_assertions(&self) -> Vec<Assertion<Self::BaseElement>, Global>;

    fn get_periodic_column_values(
        &self
    ) -> Vec<Vec<Self::BaseElement, Global>, Global> { ... }

    fn get_periodic_column_polys(
        &self
    ) -> Vec<Vec<Self::BaseElement, Global>, Global> { ... }

    fn get_transition_constraints<E>(
        &self, 
        coefficients: &[(E, E)]
    ) -> Vec<TransitionConstraintGroup<E>, Global>
    where
        E: FieldElement<BaseField = Self::BaseElement>,
    { ... }

    fn get_boundary_constraints<E>(
        &self, 
        coefficients: &[(E, E)]
    ) -> Vec<BoundaryConstraintGroup<Self::BaseElement, E>, Global>
    where
        E: FieldElement<BaseField = Self::BaseElement>,
    { ... }

    fn options(&self) -> &ProofOptions { ... }

    fn trace_info(&self) -> &TraceInfo { ... }

    fn trace_length(&self) -> usize { ... }

    fn trace_width(&self) -> usize { ... }

    fn trace_poly_degree(&self) -> usize { ... }

    fn trace_domain_generator(&self) -> Self::BaseElement { ... }

    fn ce_blowup_factor(&self) -> usize { ... }

    fn ce_domain_size(&self) -> usize { ... }

    fn composition_degree(&self) -> usize { ... }

    fn lde_blowup_factor(&self) -> usize { ... }

    fn lde_domain_size(&self) -> usize { ... }

    fn lde_domain_generator(&self) -> Self::BaseElement { ... }

    fn domain_offset(&self) -> Self::BaseElement { ... }

    fn transition_constraint_degrees(&self) -> &[TransitionConstraintDegree] { ... }

    fn num_transition_constraints(&self) -> usize { ... }

    fn transition_constraint_divisor(
        &self
    ) -> ConstraintDivisor<Self::BaseElement> { ... }

    fn get_constraint_composition_coefficients<E, H>(
        &self, 
        public_coin: &mut RandomCoin<Self::BaseElement, H>
    ) -> Result<ConstraintCompositionCoefficients<E>, RandomCoinError>
    where
        E: FieldElement<BaseField = Self::BaseElement>,
        H: Hasher,
    { ... }

    fn get_deep_composition_coefficients<E, H>(
        &self, 
        public_coin: &mut RandomCoin<Self::BaseElement, H>
    ) -> Result<DeepCompositionCoefficients<E>, RandomCoinError>
    where
        E: FieldElement<BaseField = Self::BaseElement>,
        H: Hasher,
    { ... }

}
Expand description

Describes algebraic intermediate representation of a computation.

To describe 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 Air::BaseElement associated type (see math::fields for available field options).
  2. Define a set of public inputs which are required for your computation via the Air::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 Air::context() method which should return a reference to the AirContext struct created in Air::new() function.
  5. Implement Air::evaluate_transition() method which should evaluate transition constraints over a given evaluation frame.
  6. Implement Air::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 Air::get_periodic_column_values() method.

Transition constraints

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

  • EvaluationFrame which contains vectors with current and next states of the computation.
  • A list of 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 list.
  • A mutable result slice. This is the slice where constraint evaluations should be written to. The length of this slice will be equal to the number of transition constraints defined for the computation.

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.

Note: 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 registers have degree 1.
  • When multiplying trace registers together, the degree increases by 1. For example, if our constraint involves multiplication of two registers, 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 registers and periodic columns, use the TransitionConstraintDegree::with_cycles() constructor. For example, if our constraint involves multiplication of one trace register 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 at the expense of wider execution trace.

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 Air::get_assertions() function which should return a vector of Assertion structs. 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 register 0, at step 0, must be equal to 1.
  • A periodic assertion - such assertion specifies that values in a given register at specified intervals should be equal to some value. For example: values in register 0, at steps 0, 8, 16, 24 etc. must be equal to 2.
  • A sequence assertion - such assertion specifies that values in a given register at specific intervals must be equal to a sequence of provided values. For example: values in register 0, at step 0 must be equal to 1, at step 8 must be equal to 2, at step 16 must be equal to 3 etc.

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 register 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 Air::get_periodic_column_values() method. The values of the periodic columns at a given step of the computation will be supplied to the Air::evaluate_transition() method via the periodic_values parameter.

Associated Types

Base field for the computation described by this AIR. STARK protocol for this computation may be executed in the base field, or in an extension of the base fields as specified by ProofOptions struct.

A type defining shape of public inputs for the computation described by this protocol. This could be any type as long as it can be serialized into a sequence of bytes.

Required methods

Returns new instance of AIR for this computation instantiated from the provided parameters, which have the following meaning:

  • trace_info contains information about a concrete execution trace of the computation described by this AIR, including trace width, trace length length, and optionally, additional custom parameters in meta field.
  • public_inputs specifies public inputs for this instance of the computation.
  • options defines proof generation options such as blowup factor, hash function etc. these options define security level of the proof and influence proof generation time.

Returns context for this instance of the computation.

Evaluates transition constraints over the specified evaluation frame.

The evaluations should be written into the results slice in the same order as the the order of transition constraint degree descriptors used to instantiate AirContext for this AIR. Thus, the length of the result slice will equal to the number of transition constraints defined for this computation.

Returns a set of assertions against a concrete execution trace of this computation.

Provided methods

Returns values for all periodic columns used in the computation.

These values will be used to compute column values at specific states of the computation and passed in to the evaluate_transition() method as periodic_values parameter.

The default implementation of this method returns an empty vector. For computations which rely on periodic columns, this method should be overridden in the specialized implementation. Number of values for each periodic column must be a power of two.

Returns polynomial for all periodic columns.

These polynomials are interpolated from the values returned from the get_periodic_column_values() method.

Groups transition constraints together by their degree.

This function also assigns coefficients to each constraint. These coefficients will be used to compute a random linear combination of transition constraints evaluations during constraint merging performed by TransitionConstraintGroup::merge_evaluations() function.

Convert assertions returned from get_assertions() method into boundary constraints.

This function also assign coefficients to each constraint, and group the constraints by denominator. The coefficients will be used to compute random linear combination of boundary constraints during constraint merging.

Returns options which specify STARK protocol parameters for an instance of the computation described by this AIR.

Returns info of the execution trace for an instance of the computation described by this AIR.

Returns length of the execution trace for an instance of the computation described by this AIR.

Returns width of the execution trace for an instance of the computation described by this AIR.

This is guaranteed to be between 1 and 255.

Returns degree of trace polynomials for an instance of the computation described by this AIR.

The degree is always trace_length - 1.

Returns the generator of the trace domain for an instance of the computation described by this AIR.

The generator is the $n$th root of unity where $n$ is the length of the execution trace.

Returns constraint evaluation domain blowup factor for the computation described by this AIR.

The blowup factor is defined as the smallest power of two greater than or equal to the hightest transition constraint degree. For example, if the hightest transition constraint degree = 3, ce_blowup_factor will be set to 4.

ce_blowup_factor is guaranteed to be smaller than or equal to the lde_blowup_factor.

Returns size of the constraint evaluation domain.

This is guaranteed to be a power of two, and is equal to trace_length * ce_blowup_factor.

Returns the degree to which all constraint polynomials are normalized before they are composed together.

This degree is one less than the size of constraint evaluation domain.

Returns low-degree extension domain blowup factor for the computation described by this AIR. This is guaranteed to be a power of two, and is always either equal to or greater than ce_blowup_factor.

Returns the size of the low-degree extension domain.

This is guaranteed to be a power of two, and is equal to trace_length * lde_blowup_factor.

Returns the generator of the low-degree extension domain for an instance of the computation described by this AIR.

The generator is the $n$th root of unity where $n$ is the size of the low-degree extension domain.

Returns the offset by which the domain for low-degree extension is shifted in relation to the execution trace domain.

Returns a list of transition constraint degree description for an instance of the computation described by this AIR.

This list will be identical to the list passed into the AirContext::new() method as the transition_constraint_degrees parameter.

Returns the number of transition constraints for an instance of the computation described by this AIR.

The number of transition constraints is defined by the number of transition constraint degree descriptors.

Returns a divisor for transition constraints.

All transition constraints have the same divisor which has the form: $$ z(x) = \frac{x^n - 1}{x - g^{n - 1}} $$ where: $n$ is the length of the execution trace and $g$ is the generator of the trace domain.

This divisor specifies that transition constraints must hold on all steps of the execution trace except for the last one.

Returns coefficients needed for random linear combination during construction of constraint composition polynomial.

Returns coefficients needed for random linear combinations during construction of DEEP composition polynomial.

Implementors