Trait LiftedAir 

pub trait LiftedAir<F, EF>: Sync + BaseAir<F>
where
    F: Field,
{
    // Required methods
    fn num_randomness(&self) -> usize;
    fn aux_width(&self) -> usize;
    fn num_aux_values(&self) -> usize;
    fn num_var_len_public_inputs(&self) -> usize;
    fn eval<AB>(&self, builder: &mut AB)
       where AB: LiftedAirBuilder<F = F>;

    // Provided methods
    fn periodic_columns(&self) -> Vec<Vec<F>> { ... }
    fn periodic_columns_matrix(&self) -> Option<DenseMatrix<F>> { ... }
    fn reduced_aux_values(
        &self,
        _aux_values: &[EF],
        _challenges: &[EF],
        _public_values: &[F],
        _var_len_public_inputs: &[&[F]],
    ) -> Result<ReducedAuxValues<EF>, Box<dyn Error + Sync + Send>>
       where EF: ExtensionField<F> { ... }
    fn air_layout(&self) -> AirLayout { ... }
    fn validate(&self) -> Result<(), AirValidationError> { ... }
    fn log_quotient_degree(&self) -> usize
       where Self: Sized { ... }
    fn constraint_degree(&self) -> usize
       where Self: Sized { ... }
    fn is_valid_builder<AB>(
        &self,
        builder: &AB,
    ) -> Result<(), AirValidationError>
       where AB: LiftedAirBuilder<F = F> { ... }
}

Super-trait for AIR definitions used by the lifted STARK prover/verifier.

Inherits from upstream traits for width and public values. Adds Miden-specific auxiliary trace support and periodic column data. Every LiftedAir must provide an auxiliary trace (even if it is a minimal 1-column dummy).

Type Parameters

• F: Base field
• EF: Extension field (for aux trace challenges and aux values)

Required Methods

fn num_randomness(&self) -> usize

Number of extension-field challenges required for the auxiliary trace.

fn aux_width(&self) -> usize

Number of extension-field columns in the auxiliary trace.

fn num_aux_values(&self) -> usize

Number of extension-field aux values committed to the Fiat-Shamir transcript.

These are the values returned by AuxBuilder::build_aux_trace alongside the aux trace matrix. Their count may differ from aux_width (the number of aux trace columns).

These values are exposed to AIR constraints as permutation values via PermutationAirBuilder::permutation_values.

fn num_var_len_public_inputs(&self) -> usize

Number of variable-length public inputs this AIR expects.

Each input is a slice of base-field elements that reduced_aux_values reduces to a single value. The prover validates that witnesses provide exactly this many slices.

Implementors of reduced_aux_values should verify that var_len_public_inputs contains exactly this many slices, returning [ReductionError] otherwise.

fn eval<AB>(&self, builder: &mut AB)

where AB: LiftedAirBuilder<F = F>,

Evaluate all AIR constraints using the provided builder.

Provided Methods

fn periodic_columns(&self) -> Vec<Vec<F>>

Return the periodic table data: a list of columns, each a Vec<F> of evaluations.

Each inner Vec<F> represents one periodic column. Its length is the period of that column, and the entries are the evaluations over a subgroup of that order.

Default: no periodic columns.

fn periodic_columns_matrix(&self) -> Option<DenseMatrix<F>>

Return a matrix with all periodic columns extended to a common height.

Columns with smaller periods are repeated cyclically to fill the extended domain. Returns None if there are no periodic columns.

fn reduced_aux_values( &self, _aux_values: &[EF], _challenges: &[EF], _public_values: &[F], _var_len_public_inputs: &[&[F]], ) -> Result<ReducedAuxValues<EF>, Box<dyn Error + Sync + Send>>

where EF: ExtensionField<F>,

Reduce this AIR’s aux values to a [ReducedAuxValues] contribution.

Called by the verifier (with concrete field values, not symbolic expressions) to compute each AIR’s contribution to the global cross-AIR bus identity check. The verifier accumulates contributions across all AIRs and checks that the combined result is identity (prod=1, sum=0).

Arguments

• aux_values: prover-supplied aux values (from the proof)
• challenges: extension-field challenges (same as used for aux trace building)
• public_values: this AIR’s public values (base field)
• var_len_public_inputs: reducible inputs for the cross-AIR identity check

Errors

The verifier validates instance dimensions (public values length, var-len public inputs count) before calling this method, so implementations can assume correct input counts. However, the length of each individual var-len slice is not validated upfront — implementations that index into these slices must check lengths themselves or use the Result return type to report errors.

Default: returns identity (correct for AIRs without buses).

fn air_layout(&self) -> AirLayout

Return the [AirLayout] describing this AIR’s dimensions.

This is the single source of truth for building symbolic or layout builders. preprocessed_width is always 0 because lifted AIRs forbid preprocessed traces.

fn validate(&self) -> Result<(), AirValidationError>

Validate that this AIR satisfies the LiftedAir contract.

The lifted STARK protocol relies on several structural properties of the AIR that can be checked statically (i.e. without a witness). This method verifies the subset that is machine-checkable; the full list of trust assumptions is documented in the module docs of p3-miden-lifted-stark. Both the prover and verifier call this before proceeding, so a malformed AIR is caught early.

Checked properties

• No preprocessed trace — the lifted STARK protocol does not support preprocessed (fixed) columns; their presence is an error.
• Positive auxiliary width — every lifted AIR must declare at least one auxiliary column (aux_width() > 0).
• Well-formed periodic columns — each periodic column must be non-empty and have a power-of-two length.

fn log_quotient_degree(&self) -> usize

where Self: Sized,

Log₂ of the number of quotient chunks, inferred from symbolic constraint analysis.

Evaluates the AIR on a SymbolicAirBuilder to determine the maximum constraint degree M, then returns log2_ceil(M - 1) (padded so M ≥ 2).

Uses SymbolicAirBuilder<F> (i.e. EF = F) which is sufficient for degree computation since extension-field operations have the same degree structure.

Why M − 1 chunks?

Let N be the trace height (so trace columns are polynomials of degree < N). Symbolic evaluation assigns each constraint a degree multiple M, meaning the resulting numerator polynomial C(X) has degree bounded by roughly M·(N − 1).

In a STARK, the constraint numerator is divisible by the trace vanishing polynomial Z_H(X) = Xᴺ − 1, so the quotient polynomial Q(X) = C(X) / Z_H(X) has

deg(Q) ≤ deg(C) − N ≤ M·(N − 1) − N < (M − 1)·N.

We commit to Q(X) by splitting it into D chunks of degree < N. The bound above shows that D = M − 1 chunks suffice; we then round D up to a power of two and return log2(D).

We clamp M ≥ 2 so that D ≥ 1. If M = 1 then deg(C) < N, and divisibility by Z_H would force C(X) to be the zero polynomial (i.e. the constraint carries no information about the trace).

fn constraint_degree(&self) -> usize

where Self: Sized,

Number of quotient chunks: 2^log_quotient_degree().

fn is_valid_builder<AB>(&self, builder: &AB) -> Result<(), AirValidationError>

where AB: LiftedAirBuilder<F = F>,

Check that a builder’s dimensions match this AIR.

Verifies every data-carrying accessor on LiftedAirBuilder: main trace, preprocessed trace, aux trace, public values, randomness, aux values, and periodic values.

This guards the invariant that makes eval panic-free: if the symbolic evaluation in log_quotient_degree succeeds and this check passes, then eval() cannot panic from out-of-bounds access on the builder’s accessors.

Dyn Compatibility

This trait is not dyn compatible.

In older versions of Rust, dyn compatibility was called "object safety", so this trait is not object safe.

Implementors

impl<EF: ExtensionField<Felt>> LiftedAir<Felt, EF> for ProcessorAir