p3_air/
air.rs

1use core::ops::{Add, Mul, Sub};
2
3use p3_field::{Algebra, ExtensionField, Field, PrimeCharacteristicRing};
4use p3_matrix::Matrix;
5use p3_matrix::dense::RowMajorMatrix;
6
7/// The underlying structure of an AIR.
8pub trait BaseAir<F>: Sync {
9    /// The number of columns (a.k.a. registers) in this AIR.
10    fn width(&self) -> usize;
11    /// Return an optional preprocessed trace matrix to be included in the prover's trace.
12    fn preprocessed_trace(&self) -> Option<RowMajorMatrix<F>> {
13        None
14    }
15}
16
17/// An extension of `BaseAir` that includes support for public values.
18pub trait BaseAirWithPublicValues<F>: BaseAir<F> {
19    /// Return the number of expected public values.
20    fn num_public_values(&self) -> usize {
21        0
22    }
23}
24
25/// An algebraic intermediate representation (AIR) definition.
26///
27/// Contains an evaluation function for computing the constraints of the AIR.
28/// This function can be applied to an evaluation trace in which case each
29/// constraint will compute a particular value or it can be applied symbolically
30/// with each constraint computing a symbolic expression.
31pub trait Air<AB: AirBuilder>: BaseAir<AB::F> {
32    /// Evaluate all AIR constraints using the provided builder.
33    ///
34    /// The builder provides both the trace on which the constraints
35    /// are evaluated on as well as the method of accumulating the
36    /// constraint evaluations.
37    ///
38    /// # Arguments
39    /// - `builder`: Mutable reference to an `AirBuilder` for defining constraints.
40    fn eval(&self, builder: &mut AB);
41}
42
43/// A builder which contains both a trace on which AIR constraints can be evaluated as well as a method of accumulating the AIR constraint evaluations.
44///
45/// Supports both symbolic cases where the constraints are treated as polynomials and collected into a vector
46/// as well cases where the constraints are evaluated on an evaluation trace and combined using randomness.
47pub trait AirBuilder: Sized {
48    /// Underlying field type.
49    ///
50    /// This should usually implement `Field` but there are a few edge cases (mostly involving `PackedFields`) where
51    /// it may only implement `PrimeCharacteristicRing`.
52    type F: PrimeCharacteristicRing + Sync;
53
54    /// Serves as the output type for an AIR constraint evaluation.
55    type Expr: Algebra<Self::F> + Algebra<Self::Var>;
56
57    /// The type of the variable appearing in the trace matrix.
58    ///
59    /// Serves as the input type for an AIR constraint evaluation.
60    type Var: Into<Self::Expr>
61        + Clone
62        + Send
63        + Sync
64        + Add<Self::F, Output = Self::Expr>
65        + Add<Self::Var, Output = Self::Expr>
66        + Add<Self::Expr, Output = Self::Expr>
67        + Sub<Self::F, Output = Self::Expr>
68        + Sub<Self::Var, Output = Self::Expr>
69        + Sub<Self::Expr, Output = Self::Expr>
70        + Mul<Self::F, Output = Self::Expr>
71        + Mul<Self::Var, Output = Self::Expr>
72        + Mul<Self::Expr, Output = Self::Expr>;
73
74    /// Matrix type holding variables.
75    type M: Matrix<Self::Var>;
76
77    /// Return the matrix representing the main (primary) trace registers.
78    fn main(&self) -> Self::M;
79
80    /// Expression evaluating to 1 on the first row, 0 elsewhere.
81    fn is_first_row(&self) -> Self::Expr;
82
83    /// Expression evaluating to 1 on the last row, 0 elsewhere.
84    fn is_last_row(&self) -> Self::Expr;
85
86    /// Expression evaluating to 1 on all transition rows (not last row), 0 on last row.
87    fn is_transition(&self) -> Self::Expr {
88        self.is_transition_window(2)
89    }
90
91    /// Expression evaluating to 1 on rows except the last `size - 1` rows, 0 otherwise.
92    fn is_transition_window(&self, size: usize) -> Self::Expr;
93
94    /// Returns a sub-builder whose constraints are enforced only when `condition` is nonzero.
95    fn when<I: Into<Self::Expr>>(&mut self, condition: I) -> FilteredAirBuilder<'_, Self> {
96        FilteredAirBuilder {
97            inner: self,
98            condition: condition.into(),
99        }
100    }
101
102    /// Returns a sub-builder whose constraints are enforced only when `x != y`.
103    fn when_ne<I1: Into<Self::Expr>, I2: Into<Self::Expr>>(
104        &mut self,
105        x: I1,
106        y: I2,
107    ) -> FilteredAirBuilder<'_, Self> {
108        self.when(x.into() - y.into())
109    }
110
111    /// Returns a sub-builder whose constraints are enforced only on the first row.
112    fn when_first_row(&mut self) -> FilteredAirBuilder<'_, Self> {
113        self.when(self.is_first_row())
114    }
115
116    /// Returns a sub-builder whose constraints are enforced only on the last row.
117    fn when_last_row(&mut self) -> FilteredAirBuilder<'_, Self> {
118        self.when(self.is_last_row())
119    }
120
121    /// Returns a sub-builder whose constraints are enforced on all rows except the last.
122    fn when_transition(&mut self) -> FilteredAirBuilder<'_, Self> {
123        self.when(self.is_transition())
124    }
125
126    /// Returns a sub-builder whose constraints are enforced on all rows except the last `size - 1`.
127    fn when_transition_window(&mut self, size: usize) -> FilteredAirBuilder<'_, Self> {
128        self.when(self.is_transition_window(size))
129    }
130
131    /// Assert that the given element is zero.
132    ///
133    /// Where possible, batching multiple assert_zero calls
134    /// into a single assert_zeros call will improve performance.
135    fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I);
136
137    /// Assert that every element of a given array is 0.
138    ///
139    /// This should be preferred over calling `assert_zero` multiple times.
140    fn assert_zeros<const N: usize, I: Into<Self::Expr>>(&mut self, array: [I; N]) {
141        for elem in array {
142            self.assert_zero(elem);
143        }
144    }
145
146    /// Assert that a given array consists of only boolean values.
147    fn assert_bools<const N: usize, I: Into<Self::Expr>>(&mut self, array: [I; N]) {
148        let zero_array = array.map(|x| x.into().bool_check());
149        self.assert_zeros(zero_array);
150    }
151
152    /// Assert that `x` element is equal to `1`.
153    fn assert_one<I: Into<Self::Expr>>(&mut self, x: I) {
154        self.assert_zero(x.into() - Self::Expr::ONE);
155    }
156
157    /// Assert that the given elements are equal.
158    fn assert_eq<I1: Into<Self::Expr>, I2: Into<Self::Expr>>(&mut self, x: I1, y: I2) {
159        self.assert_zero(x.into() - y.into());
160    }
161
162    /// Assert that `x` is a boolean, i.e. either `0` or `1`.
163    ///
164    /// Where possible, batching multiple assert_bool calls
165    /// into a single assert_bools call will improve performance.
166    fn assert_bool<I: Into<Self::Expr>>(&mut self, x: I) {
167        self.assert_zero(x.into().bool_check());
168    }
169}
170
171/// Extension trait for `AirBuilder` providing access to public values.
172pub trait AirBuilderWithPublicValues: AirBuilder {
173    /// Type representing a public variable.
174    type PublicVar: Into<Self::Expr> + Copy;
175
176    /// Return the list of public variables.
177    fn public_values(&self) -> &[Self::PublicVar];
178}
179
180/// Trait for `AirBuilder` variants that include preprocessed data columns.
181pub trait PairBuilder: AirBuilder {
182    /// Return a matrix of preprocessed registers.
183    fn preprocessed(&self) -> Self::M;
184}
185
186/// Extension of `AirBuilder` for working over extension fields.
187pub trait ExtensionBuilder: AirBuilder<F: Field> {
188    /// Extension field type.
189    type EF: ExtensionField<Self::F>;
190
191    /// Expression type over extension field elements.
192    type ExprEF: From<Self::Expr> + Algebra<Self::EF>;
193
194    /// Variable type over extension field elements.
195    type VarEF: Into<Self::ExprEF> + Copy + Send + Sync;
196
197    /// Assert that an extension field expression is zero.
198    fn assert_zero_ext<I>(&mut self, x: I)
199    where
200        I: Into<Self::ExprEF>;
201
202    /// Assert that two extension field expressions are equal.
203    fn assert_eq_ext<I1, I2>(&mut self, x: I1, y: I2)
204    where
205        I1: Into<Self::ExprEF>,
206        I2: Into<Self::ExprEF>,
207    {
208        self.assert_zero_ext(x.into() - y.into());
209    }
210
211    /// Assert that an extension field expression is equal to one.
212    fn assert_one_ext<I>(&mut self, x: I)
213    where
214        I: Into<Self::ExprEF>,
215    {
216        self.assert_eq_ext(x, Self::ExprEF::ONE);
217    }
218}
219
220/// Trait for builders supporting permutation arguments (e.g., for lookup constraints).
221pub trait PermutationAirBuilder: ExtensionBuilder {
222    /// Matrix type over extension field variables representing a permutation.
223    type MP: Matrix<Self::VarEF>;
224
225    /// Randomness variable type used in permutation commitments.
226    type RandomVar: Into<Self::ExprEF> + Copy;
227
228    /// Return the matrix representing permutation registers.
229    fn permutation(&self) -> Self::MP;
230
231    /// Return the list of randomness values for permutation argument.
232    fn permutation_randomness(&self) -> &[Self::RandomVar];
233}
234
235/// A wrapper around an [`AirBuilder`] that enforces constraints only when a specified condition is met.
236///
237/// This struct allows selectively applying constraints to certain rows or under certain conditions in the AIR,
238/// without modifying the underlying logic. All constraints asserted through this filtered builder will be
239/// multiplied by the given `condition`, effectively disabling them when `condition` evaluates to zero.
240#[derive(Debug)]
241pub struct FilteredAirBuilder<'a, AB: AirBuilder> {
242    /// Reference to the underlying inner [`AirBuilder`] where constraints are ultimately recorded.
243    pub inner: &'a mut AB,
244
245    /// Condition expression that controls when the constraints are enforced.
246    ///
247    /// If `condition` evaluates to zero, constraints asserted through this builder have no effect.
248    condition: AB::Expr,
249}
250
251impl<AB: AirBuilder> FilteredAirBuilder<'_, AB> {
252    pub fn condition(&self) -> AB::Expr {
253        self.condition.clone()
254    }
255}
256
257impl<AB: AirBuilder> AirBuilder for FilteredAirBuilder<'_, AB> {
258    type F = AB::F;
259    type Expr = AB::Expr;
260    type Var = AB::Var;
261    type M = AB::M;
262
263    fn main(&self) -> Self::M {
264        self.inner.main()
265    }
266
267    fn is_first_row(&self) -> Self::Expr {
268        self.inner.is_first_row()
269    }
270
271    fn is_last_row(&self) -> Self::Expr {
272        self.inner.is_last_row()
273    }
274
275    fn is_transition_window(&self, size: usize) -> Self::Expr {
276        self.inner.is_transition_window(size)
277    }
278
279    fn assert_zero<I: Into<Self::Expr>>(&mut self, x: I) {
280        self.inner.assert_zero(self.condition() * x.into());
281    }
282}
283
284impl<AB: PairBuilder> PairBuilder for FilteredAirBuilder<'_, AB> {
285    fn preprocessed(&self) -> Self::M {
286        self.inner.preprocessed()
287    }
288}
289
290impl<AB: ExtensionBuilder> ExtensionBuilder for FilteredAirBuilder<'_, AB> {
291    type EF = AB::EF;
292    type ExprEF = AB::ExprEF;
293    type VarEF = AB::VarEF;
294
295    fn assert_zero_ext<I>(&mut self, x: I)
296    where
297        I: Into<Self::ExprEF>,
298    {
299        let ext_x = x.into();
300        let condition: Self::ExprEF = self.condition().into();
301
302        self.inner.assert_zero_ext(ext_x * condition);
303    }
304}
305
306impl<AB: PermutationAirBuilder> PermutationAirBuilder for FilteredAirBuilder<'_, AB> {
307    type MP = AB::MP;
308
309    type RandomVar = AB::RandomVar;
310
311    fn permutation(&self) -> Self::MP {
312        self.inner.permutation()
313    }
314
315    fn permutation_randomness(&self) -> &[Self::RandomVar] {
316        self.inner.permutation_randomness()
317    }
318}