Add section on AIRs to composition polynomial

src/SUMMARY.md

@@ -51,6 +51,11 @@
     - [Merkle Prover](how-it-works/vcs/merkle_prover.md)
     - [Merkle Verifier](how-it-works/vcs/merkle_verifier.md)
 
+  - [AIR to Composition Polynomial](how-it-works/air/index.md)
+    - [Technical Overview](how-it-works/air/overview.md)
+    - [Components](how-it-works/air/components.md)
+    - [Prover Components](how-it-works/air/prover_components.md)
+
   - [Lookups](how-it-works/lookups.md)
 
 - [Awesome Stwo](awesome-stwo/index.md)

src/how-it-works/air/components.md

@@ -0,0 +1,57 @@
+# Components
+
+This section examines how the components are implemented and covers some important functions defined on them, without diving into AIR-specific details since they are already covered in the [earlier sections](../../air-development/index.md).
+
+The `Components` struct is a collection of components, implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/air/components.rs 13:16}}
+```
+
+Here, `components` is a collection of objects that implement the `Component` trait, and `n_preprocessed_columns` is the total number of preprocessed columns used across all components (refer to [Preprocessed Trace](../../air-development/preprocessed-trace/index.md)).
+
+
+The `Component` trait represents a trace table along with a set of constraints. It implements the following functions:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/air/mod.rs 24:49}}
+```
+This section will not examine each of these functions in detail but will explain them wherever they are used to implement various functions for the `Components` struct. The following are some important functions implemented for the `Components` struct.
+
+## Composition Polynomial Degree Bound
+The `composition_log_degree_bound` function determines the log of the degree of the composition polynomial.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/air/components.rs 19:25}}
+```
+
+For each component, this calls the `max_constraint_log_degree_bound()` function, which returns the log of the highest polynomial degree among all constraints in that component. It then takes the maximum value across all components. For the [example AIR containing two components](./overview.md#air-to-composition-polynomial), this function returns $\max({\log{(\deg{(p_0)})}, \log{(\deg{(p_1)})}})$.
+
+## Mask Points
+The `mask_points` function determines all evaluation points needed to verify constraints at a given point
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/air/components.rs 27:47}}
+```
+
+From the perspective of the prover (and verifier), when they need to open the composition polynomial at a specific point sent by the verifier (for example, an out-of-domain point), they require additional polynomial evaluations to verify the constraints.
+
+The composition polynomial combines many component-level constraint quotients. Each constraint involves relationships between multiple cells in the execution trace, potentially at different rows/offsets.
+
+The function `mask_points` performs the following:
+- Given a single point as input, it determines all related points where polynomial evaluations are needed to verify constraints.
+- Handles offsets for each component, since different components may have different constraint structures requiring different offset patterns.
+- Ensures preprocessed columns (shared lookup tables, etc.) are properly included.
+
+
+## Evaluate Composition Polynomial
+The `eval_composition_polynomial_at_point` function evaluates the combined constraint polynomial.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/air/components.rs 49:64}}
+```
+The inputs to this function are as follows:
+- `&self`: The `Components` on which the function is called.
+- `point`: The circle point at which the composition polynomial is to be evaluated.
+- `mask_values`: The evaluations of the polynomials at the mask points that were previously determined by the `mask_points` function. These provide the constraint polynomial values needed to compute the composition polynomial at the input `point`.
+- `random_coeff`: An element from the `SecureField` (i.e. $\mathsf{QM31}$). In the example, this is represented as $\gamma$, which is used to compose all constraints into a single composition polynomial.
+
+The function body operates as follows. First, an `evaluation_accumulator` is instantiated. Then, for each component, the evaluation of the component-level quotient is added to the `evaluation_accumulator`. For the [example AIR containing two components](./overview.md#air-to-composition-polynomial), this adds the evaluations of component-level quotients $q_0$ and $q_1$ at the input `point` to the `evaluation_accumulator`. Finally, the `finalize()` function is called on the `evaluation_accumulator`, which outputs the random linear combination evaluated at the input `point`.
+$$
+q = q_0 + \gamma^{c_0} \cdot q_1
+$$

src/how-it-works/air/index.md

@@ -0,0 +1,13 @@
+# AIR to Composition Polynomial
+
+> This section explores the conversion of an AIR to a composition polynomial, covering both the mathematical framework and implementation details. We examine how multiple components with their respective constraints are combined into a single polynomial.
+
+This section is organized as follows:
+
+- **[Technical Overview](./overview.md)**: Provides a high-level explanation of how multiple components are combined into a composition polynomial.
+
+- **[Components](./components.md)**: Examines the implementation of the `Components` struct and key functions like `mask_points` and `eval_composition_polynomial_at_point`.
+
+- **[Prover Components](./prover_components.md)**: Details the `ComponentProvers` struct and its specialized functions for computing composition polynomials during the proving process, including the main `compute_composition_polynomial` function.
+
+

src/how-it-works/air/overview.md

@@ -0,0 +1,31 @@
+# Technical Overview
+
+As shown in an earlier section (refer to [Components](../../air-development/components/index.md)), Stwo represents the trace using multiple tables where each table is referred to as a _component_. An AIR in Stwo is a collection of multiple components. Components can interact with one another, and the consistency of these interactions is verified using [_logUp_](https://eprint.iacr.org/2022/1530.pdf). 
+
+For example, in the [hash function example](../../air-development/components/index.md#hash-function-example), the scheduling component and computing component interact with each other, where both the components lookup the input and output pair. The consistency of this interaction is then verified by adding logUp constraints to each component.
+
+Each component consists of a trace table of a specific height along with a set of constraints. These constraints include computation constraints as well as lookup constraints (refer to [Lookups](../lookups.md)).
+
+This section provides an overview of how these components are converted into a composition polynomial. This composition polynomial is then used by a polynomial commitment scheme to commit and generate evaluation proofs.
+
+## AIR to Composition Polynomial
+
+This section explains how a composition polynomial is computed using an example.
+
+Consider an AIR composed of two components with trace tables: $\mathscr{T}_0$ and $\mathscr{T}_1$. The component table $\mathscr{T}_0$ is defined over the trace domain $D_{n_0}$, which is a [canonic coset](../circle-group.md#canonic-coset) of size $N_0 = 2^{n_0}$. Similarly, component table $\mathscr{T}_1$ is defined over the trace domain $D_{n_1}$ of size $N_1 = 2^{n_1}$.
+
+The prover interpolates the trace polynomials for each component and then evaluates the trace polynomials over an evaluation domain that is a blowup factor $B = 2^\beta$ times larger than the trace domain. Thus, the evaluation domain for component table $\mathscr{T}_0$ is $D_{n_0 + \beta}$ of size $2^{n_0 + \beta}$. Similarly, the evaluation domain for component table $\mathscr{T}_1$ is $D_{n_1 + \beta}$ of size $2^{n_1 + \beta}$. Both interpolation and evaluation use [circle FFT](../circle-fft/index.md). The prover then commits to the evaluations of trace polynomials from all components using a single [Merkle tree](../vcs/index.md).
+
+Both component tables define computation constraints and lookup constraints for their specific component. The component constraints are proven table-wise, each with its separate domain quotient, which are then combined into a single cross-domain composition polynomial. Suppose the component tables $\mathscr{T}_0$ and $\mathscr{T}_1$ have a total of $c_0$ and $c_1$ constraints, respectively.
+
+The verifier sends $\gamma \in \mathsf{QM31}$ to the prover. We use the same $\gamma$ to combine all constraints across different component tables. First, $\gamma$ is used to compute the random linear combination of all constraints on component $\mathscr{T}_0$ to obtain the component-level composition polynomial $p_0$. Then, the prover uses the same $\gamma$ to compute the component-level composition polynomial $p_1$ for component $\mathscr{T}_1$.
+
+The prover then computes the quotient for component table $\mathscr{T}_0$ as $q_0 = p_0 / v_{n_0}$, where $v_{n_0}$ is the vanishing polynomial for trace domain $D_{n_0}$. Similarly, the prover computes the quotient for component table $\mathscr{T}_1$ as $q_1 = p_1 / v_{n_1}$.
+
+Finally, the prover computes the cross-domain composition polynomial as
+$$
+q = q_0 + \gamma^{c_0} \cdot q_1
+$$
+where $c_0$ is the total number of constraints of the component table $\mathscr{T}_0$.
+
+The next section examines how these concepts are implemented.

src/how-it-works/air/prover_components.md

@@ -0,0 +1,39 @@
+# Prover Components
+
+The `ComponentProvers` struct is similar to the `Components` struct but implements additional functions required by the prover, such as computing the composition polynomial. It is a collection of prover components as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/air/component_prover.rs 33:36}}
+```
+
+Here, `components` is a collection of objects that implement the `ComponentProver` trait. The `ComponentProver` trait is a wrapper around the `Component` trait with an additional function shown as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/air/component_prover.rs 13:21}}
+```
+
+We can convert the `ComponentProvers` into a `Components` struct as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/air/component_prover.rs 39:48}}
+```
+
+The main function defined on the `ComponentProvers` struct to compute the composition polynomial is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/air/component_prover.rs 49:64}}
+```
+
+Let us examine the above function for our [example AIR containing two components](./overview.md#air-to-composition-polynomial). It takes the following three inputs:
+- `&self`: This is the `ComponentProvers` on which the function is called.
+- `random_coeff`: This is an element from the `SecureField` (i.e. $\mathsf{QM31}$). In our example, this is represented as $\gamma$.
+- `trace`: The `Trace` struct which contains all the polynomials that make up the entire trace including all the components. For efficiency, it stores each polynomial in both coefficients and evaluations form.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/air/component_prover.rs 26:31}}
+```
+
+Now let us examine the body of the function. First, we compute `total_constraints` and initialize an `accumulator`. The `total_constraints` determine the number of powers of $\gamma$ (`random_coeff`) required for the random linear combination.
+
+For each component, we call `evaluate_constraint_quotients_on_domain`, which computes and accumulates the evaluations of that component's quotients on their respective evaluation domains within the accumulator. For the $0$th component, we add the evaluations of the quotient $q_0$ over its evaluation domain $D_{n_0 + \beta}$ to the `accumulator`. Similarly, for the $1$st component, we add the evaluations of the quotient $q_1$ over its evaluation domain $D_{n_1 + \beta}$ to the `accumulator`.
+
+After adding all component quotient evaluations to the accumulator, we call the `finalize()` function, which:
+1. Combines the accumulated evaluations at different domain sizes to compute the evaluations of the quotient composition polynomial $q$ over the domain $D_{n + \beta}$ where $n = \max{(n_1, n_2)}$.
+2. Interpolates $q$ over $D_{n + \beta}$ using [circle FFT](../circle-fft/index.md) to convert it into coefficient representation.
+
+Note that the output is a [`SecureCirclePoly`](../circle-polynomials/secure-evals-and-poly.md#secure-circle-polynomials) since the evaluations of $q$ are in the secure field $\mathsf{QM31}$ (as $\gamma$ is randomly sampled from $\mathsf{QM31}$).