Trait winter_prover::Air
source · pub trait Air: Send + Sync {
type BaseField: StarkField + ExtensibleField<2> + ExtensibleField<3>;
type PublicInputs: Serializable;
Show 26 methods
fn new(
trace_info: TraceInfo,
pub_inputs: Self::PublicInputs,
options: ProofOptions
) -> Self;
fn context(&self) -> &AirContext<Self::BaseField>;
fn evaluate_transition<E>(
&self,
frame: &EvaluationFrame<E>,
periodic_values: &[E],
result: &mut [E]
)
where
E: FieldElement<BaseField = Self::BaseField>;
fn get_assertions(&self) -> Vec<Assertion<Self::BaseField>, Global>;
fn evaluate_aux_transition<F, E>(
&self,
main_frame: &EvaluationFrame<F>,
aux_frame: &EvaluationFrame<E>,
periodic_values: &[F],
aux_rand_elements: &AuxTraceRandElements<E>,
result: &mut [E]
)
where
F: FieldElement<BaseField = Self::BaseField>,
E: FieldElement<BaseField = Self::BaseField> + ExtensionOf<F>,
{ ... }
fn get_aux_assertions<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>
) -> Vec<Assertion<E>, Global>
where
E: FieldElement<BaseField = Self::BaseField>,
{ ... }
fn get_periodic_column_values(
&self
) -> Vec<Vec<Self::BaseField, Global>, Global> { ... }
fn get_periodic_column_polys(
&self
) -> Vec<Vec<Self::BaseField, Global>, Global> { ... }
fn get_transition_constraints<E>(
&self,
composition_coefficients: &[(E, E)]
) -> TransitionConstraints<E>
where
E: FieldElement<BaseField = Self::BaseField>,
{ ... }
fn get_boundary_constraints<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>,
composition_coefficients: &[(E, E)]
) -> BoundaryConstraints<E>
where
E: FieldElement<BaseField = Self::BaseField>,
{ ... }
fn options(&self) -> &ProofOptions { ... }
fn trace_info(&self) -> &TraceInfo { ... }
fn trace_length(&self) -> usize { ... }
fn trace_layout(&self) -> &TraceLayout { ... }
fn trace_poly_degree(&self) -> usize { ... }
fn trace_domain_generator(&self) -> Self::BaseField { ... }
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::BaseField { ... }
fn domain_offset(&self) -> Self::BaseField { ... }
fn get_aux_trace_segment_random_elements<E, H>(
&self,
aux_segment_idx: usize,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<Vec<E, Global>, RandomCoinError>
where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
{ ... }
fn get_constraint_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<ConstraintCompositionCoefficients<E>, RandomCoinError>
where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
{ ... }
fn get_deep_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<DeepCompositionCoefficients<E>, RandomCoinError>
where
E: FieldElement<BaseField = Self::BaseField>,
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:
- Define base field for your computation via the Air::BaseField associated type (see math::fields for available field options).
- Define a set of public inputs which are required for your computation via the Air::PublicInputs associated type.
- 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.
- Implement Air::context() method which should return a reference to the AirContext struct created in Air::new() function.
- Implement Air::evaluate_transition() method which should evaluate transition constraints over a given evaluation frame.
- Implement Air::get_assertions() method which should return a vector of assertions for a given instance of your computation.
- If your computation requires periodic values, you can also override the default Air::get_periodic_column_values() method.
If your computation uses Randomized AIR, you will also need to override Air::evaluate_aux_transition() and Air::get_aux_assertions() methods.
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 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 be2
. 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 TransitionConstraintDegree::with_cycles() constructor. 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 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 column 0, at 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 value. For example: values in column 0, at 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, 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 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
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.
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 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
andaux_rand_elements
. These parameters are needed for evaluating transition constraints over the auxiliary trace segments. - 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 segments.
Required Associated Types
sourcetype BaseField: StarkField + ExtensibleField<2> + ExtensibleField<3>
type BaseField: StarkField + ExtensibleField<2> + ExtensibleField<3>
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.
sourcetype PublicInputs: Serializable
type PublicInputs: Serializable
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
sourcefn new(
trace_info: TraceInfo,
pub_inputs: Self::PublicInputs,
options: ProofOptions
) -> Self
fn new(
trace_info: TraceInfo,
pub_inputs: Self::PublicInputs,
options: ProofOptions
) -> Self
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 inmeta
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.
sourcefn context(&self) -> &AirContext<Self::BaseField>
fn context(&self) -> &AirContext<Self::BaseField>
Returns context for this instance of the computation.
sourcefn evaluate_transition<E>(
&self,
frame: &EvaluationFrame<E>,
periodic_values: &[E],
result: &mut [E]
)where
E: FieldElement<BaseField = Self::BaseField>,
fn evaluate_transition<E>(
&self,
frame: &EvaluationFrame<E>,
periodic_values: &[E],
result: &mut [E]
)where
E: FieldElement<BaseField = Self::BaseField>,
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.
We define type E
separately from Self::BaseField
to allow evaluation of constraints
over the out-of-domain evaluation frame, which may be defined over an extension field
(when extension fields are used).
Provided Methods
sourcefn evaluate_aux_transition<F, E>(
&self,
main_frame: &EvaluationFrame<F>,
aux_frame: &EvaluationFrame<E>,
periodic_values: &[F],
aux_rand_elements: &AuxTraceRandElements<E>,
result: &mut [E]
)where
F: FieldElement<BaseField = Self::BaseField>,
E: FieldElement<BaseField = Self::BaseField> + ExtensionOf<F>,
fn evaluate_aux_transition<F, E>(
&self,
main_frame: &EvaluationFrame<F>,
aux_frame: &EvaluationFrame<E>,
periodic_values: &[F],
aux_rand_elements: &AuxTraceRandElements<E>,
result: &mut [E]
)where
F: FieldElement<BaseField = Self::BaseField>,
E: FieldElement<BaseField = Self::BaseField> + ExtensionOf<F>,
Evaluates transition constraints over the specified evaluation frames for the main and auxiliary trace segments.
The evaluations should be written into the results
slice in the same order as the order
of auxiliary transition constraint degree descriptors used to instantiate AirContext for
this AIR. Thus, the length of the result
slice will equal to the number of auxiliary
transition constraints defined for this computation.
The default implementation of this function panics. It must be overridden for AIRs describing computations which require multiple trace segments.
The types for main and auxiliary trace evaluation frames are defined as follows:
- When the entire protocol is executed in a prime field, types
F
andE
are the same, and thus, both the main and the auxiliary trace frames are defined over the base field. - When the protocol is executed in an extension field, the main trace frame is defined over the base field, while the auxiliary trace frame is defined over the extension field.
We define type F
separately from Self::BaseField
to allow evaluation of constraints
over the out-of-domain evaluation frame, which may be defined over an extension field
(when extension fields are used). The type bounds specified for this function allow the
following:
F
andE
could be the same StarkField or extensions of the same StarkField.F
andE
could be the same field, because a field is always an extension of itself.- If
F
andE
are different, thenE
must be an extension ofF
.
sourcefn get_aux_assertions<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>
) -> Vec<Assertion<E>, Global>where
E: FieldElement<BaseField = Self::BaseField>,
fn get_aux_assertions<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>
) -> Vec<Assertion<E>, Global>where
E: FieldElement<BaseField = Self::BaseField>,
Returns a set of assertions placed against auxiliary trace segments.
The default implementation of this function returns an empty vector. It should be overridden only if the computation relies on auxiliary trace segments. In such a case, the vector returned from this function must contain at least one assertion.
The column index for assertions is expected to be zero-based across all auxiliary trace segments. That is, assertion against column 0, is an assertion against the first column of the auxiliary trace segments.
When the protocol is executed using an extension field, auxiliary assertions are defined over the extension field. This is in contrast with the assertions returned from get_assertions() function, which always returns assertions defined over the base field of the protocol.
sourcefn get_periodic_column_values(
&self
) -> Vec<Vec<Self::BaseField, Global>, Global>
fn get_periodic_column_values(
&self
) -> Vec<Vec<Self::BaseField, Global>, Global>
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.
sourcefn get_periodic_column_polys(&self) -> Vec<Vec<Self::BaseField, Global>, Global>
fn get_periodic_column_polys(&self) -> Vec<Vec<Self::BaseField, Global>, Global>
Returns polynomial for all periodic columns.
These polynomials are interpolated from the values returned from the get_periodic_column_values() method.
sourcefn get_transition_constraints<E>(
&self,
composition_coefficients: &[(E, E)]
) -> TransitionConstraints<E>where
E: FieldElement<BaseField = Self::BaseField>,
fn get_transition_constraints<E>(
&self,
composition_coefficients: &[(E, E)]
) -> TransitionConstraints<E>where
E: FieldElement<BaseField = Self::BaseField>,
Groups transition constraints together by their degree.
This function also assigns composition 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.
sourcefn get_boundary_constraints<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>,
composition_coefficients: &[(E, E)]
) -> BoundaryConstraints<E>where
E: FieldElement<BaseField = Self::BaseField>,
fn get_boundary_constraints<E>(
&self,
aux_rand_elements: &AuxTraceRandElements<E>,
composition_coefficients: &[(E, E)]
) -> BoundaryConstraints<E>where
E: FieldElement<BaseField = Self::BaseField>,
Convert assertions returned from get_assertions() and get_aux_assertions() methods into boundary constraints.
This function also assigns composition coefficients to each constraint, and groups the constraints by their divisors. The coefficients will be used to compute random linear combination of boundary constraints during constraint merging.
sourcefn options(&self) -> &ProofOptions
fn options(&self) -> &ProofOptions
Returns options which specify STARK protocol parameters for an instance of the computation described by this AIR.
sourcefn trace_info(&self) -> &TraceInfo
fn trace_info(&self) -> &TraceInfo
Returns info of the execution trace for an instance of the computation described by this AIR.
sourcefn trace_length(&self) -> usize
fn trace_length(&self) -> usize
Returns length of the execution trace for an instance of the computation described by this AIR.
sourcefn trace_layout(&self) -> &TraceLayout
fn trace_layout(&self) -> &TraceLayout
Returns a description of how execution trace columns are arranged into segments for an instance of a computation described by this AIR.
sourcefn trace_poly_degree(&self) -> usize
fn trace_poly_degree(&self) -> usize
Returns degree of trace polynomials for an instance of the computation described by this AIR.
The degree is always trace_length
- 1.
sourcefn trace_domain_generator(&self) -> Self::BaseField
fn trace_domain_generator(&self) -> Self::BaseField
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.
sourcefn ce_blowup_factor(&self) -> usize
fn ce_blowup_factor(&self) -> usize
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
.
sourcefn ce_domain_size(&self) -> usize
fn ce_domain_size(&self) -> usize
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
.
sourcefn composition_degree(&self) -> usize
fn composition_degree(&self) -> usize
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.
sourcefn lde_blowup_factor(&self) -> usize
fn lde_blowup_factor(&self) -> usize
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.
sourcefn lde_domain_size(&self) -> usize
fn lde_domain_size(&self) -> usize
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
.
sourcefn lde_domain_generator(&self) -> Self::BaseField
fn lde_domain_generator(&self) -> Self::BaseField
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.
sourcefn domain_offset(&self) -> Self::BaseField
fn domain_offset(&self) -> Self::BaseField
Returns the offset by which the domain for low-degree extension is shifted in relation to the execution trace domain.
sourcefn get_aux_trace_segment_random_elements<E, H>(
&self,
aux_segment_idx: usize,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<Vec<E, Global>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
fn get_aux_trace_segment_random_elements<E, H>(
&self,
aux_segment_idx: usize,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<Vec<E, Global>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
Returns a vector of field elements required for construction of an auxiliary trace segment with the specified index.
The elements are drawn uniformly at random from the provided public coin.
sourcefn get_constraint_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<ConstraintCompositionCoefficients<E>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
fn get_constraint_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<ConstraintCompositionCoefficients<E>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
Returns coefficients needed for random linear combination during construction of constraint composition polynomial.
sourcefn get_deep_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<DeepCompositionCoefficients<E>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
fn get_deep_composition_coefficients<E, H>(
&self,
public_coin: &mut RandomCoin<Self::BaseField, H>
) -> Result<DeepCompositionCoefficients<E>, RandomCoinError>where
E: FieldElement<BaseField = Self::BaseField>,
H: Hasher,
Returns coefficients needed for random linear combinations during construction of DEEP composition polynomial.