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}