diff --git a/book.toml b/book.toml
index 7f1d489..e9565c4 100644
--- a/book.toml
+++ b/book.toml
@@ -3,7 +3,7 @@ authors = ["Jason Park", "Varun Thakore"]
language = "en"
multilingual = false
src = "src"
-title = "stwo-book"
+title = "Stwo Book"
[preprocessor.admonish]
command = "mdbook-admonish"
diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 93d6476..23996ef 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -29,7 +29,7 @@
- [Main Components](cairo-air/main-components/index.md)
- [`ADD` Opcode Walkthrough](cairo-air/add-opcode/index.md)
-- [How Does It Work?](how-it-works/index.md)
+- [Stwo: Under the Hood](how-it-works/index.md)
- [Mersenne Primes](how-it-works/mersenne-prime.md)
@@ -61,6 +61,15 @@
- [FRI Prover](how-it-works/circle-fri/fri_prover.md)
- [FRI Verifier](how-it-works/circle-fri/fri_verifier.md)
+ - [Polynomial Commitment Scheme](how-it-works/pcs/index.md)
+ - [Technical Overview](how-it-works/pcs/overview.md)
+ - [Polynomial Commitment Scheme Prover](how-it-works/pcs/prover.md)
+ - [Polynomial Commitment Scheme Verifier](how-it-works/pcs/verifier.md)
+
+ - [Proof Generation and Verification](how-it-works/stark_proof/index.md)
+ - [STARK Prover](how-it-works/stark_proof/prove.md)
+ - [STARK Verifier](how-it-works/stark_proof/verify.md)
+
- [Lookups](how-it-works/lookups.md)
- [Awesome Stwo](awesome-stwo/index.md)
diff --git a/src/how-it-works/circle-polynomials/columns.md b/src/how-it-works/circle-polynomials/columns.md
index aa47d90..d957233 100644
--- a/src/how-it-works/circle-polynomials/columns.md
+++ b/src/how-it-works/circle-polynomials/columns.md
@@ -26,8 +26,6 @@ Here, `bit_reverse` performs a naive bit-reversal permutation on the `column`.
## Secure Field Columns
-
-
An element of the secure field (`SecureField` = `QM31`) cannot be stored in a single `BaseField` column because it is a quartic extension of `M31`. Instead, each secure field element is represented by four base field coordinates and stored in four consecutive columns.
```rust,no_run,noplayground
diff --git a/src/how-it-works/circle-polynomials/secure-evals-and-poly.md b/src/how-it-works/circle-polynomials/secure-evals-and-poly.md
index 6350737..c94e4ab 100644
--- a/src/how-it-works/circle-polynomials/secure-evals-and-poly.md
+++ b/src/how-it-works/circle-polynomials/secure-evals-and-poly.md
@@ -33,8 +33,6 @@ $$p(x, y) = p_a(x, y) + i \cdot p_b(x, y) + u \cdot p_c(x, y) + iu \cdot p_d(x,
where $p_a(x,y)$ is a `CirclePoly` with coefficients $a_j \in \mathsf{M31}$, similarly for $p_b(x, y), p_c(x, y)$ and $p_d(x, y)$. This is implemented as follows:
-
-
```rust,no_run,noplayground
{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/poly/circle/secure_poly.rs 14:14}}
```
diff --git a/src/how-it-works/lookups-1.png b/src/how-it-works/figures/lookups-1.png
similarity index 100%
rename from src/how-it-works/lookups-1.png
rename to src/how-it-works/figures/lookups-1.png
diff --git a/src/how-it-works/lookups-2.png b/src/how-it-works/figures/lookups-2.png
similarity index 100%
rename from src/how-it-works/lookups-2.png
rename to src/how-it-works/figures/lookups-2.png
diff --git a/src/how-it-works/lookups-3.png b/src/how-it-works/figures/lookups-3.png
similarity index 100%
rename from src/how-it-works/lookups-3.png
rename to src/how-it-works/figures/lookups-3.png
diff --git a/src/how-it-works/lookups-4.png b/src/how-it-works/figures/lookups-4.png
similarity index 100%
rename from src/how-it-works/lookups-4.png
rename to src/how-it-works/figures/lookups-4.png
diff --git a/src/how-it-works/lookups-5.png b/src/how-it-works/figures/lookups-5.png
similarity index 100%
rename from src/how-it-works/lookups-5.png
rename to src/how-it-works/figures/lookups-5.png
diff --git a/src/how-it-works/lookups-6.png b/src/how-it-works/figures/lookups-6.png
similarity index 100%
rename from src/how-it-works/lookups-6.png
rename to src/how-it-works/figures/lookups-6.png
diff --git a/src/how-it-works/index.md b/src/how-it-works/index.md
index 023388b..392d78a 100644
--- a/src/how-it-works/index.md
+++ b/src/how-it-works/index.md
@@ -1,4 +1,16 @@
-# How Does It Work?
+# Stwo: Under the Hood
-
-> This section is for those who want an in-depth explanation of various components of Stwo.
+> This section provides an overview of the core components and protocols that make up Stwo. It is intended for readers who want to understand the technical details and inner workings of the system implementation. Throughout this section, we describe the implementation as available in this [commit](https://github.com/starkware-libs/stwo/tree/0790eba46b8af5697083d84fb75bd34b08a0b31f).
+
+The following topics are covered:
+
+- [**Mersenne Primes**](./mersenne-prime.md): Introduction to the Mersenne31 prime field used in Stwo for efficient arithmetic.
+- [**Circle Group**](./circle-group.md): Explains the algebraic structure underlying FFT and polynomial operations.
+- [**Circle Polynomials**](./circle-polynomials/index.md): Details the representation and evaluation of polynomials in the circle group.
+- [**Circle FFT**](./circle-fft/index.md): Describes the fast Fourier transform algorithm adapted for the circle group.
+- [**Vector Commitment Scheme (VCS)**](./vcs/index.md): Covers the use of Merkle trees for committing to vectors and enabling efficient proofs of inclusion.
+- [**AIR to Composition Polynomial**](./air/index.md): Shows how algebraic constraints are encoded as polynomials for proof generation.
+- [**Circle FRI**](./circle-fri/index.md): Explains the FRI protocol for low-degree testing of polynomials over the circle group.
+- [**Polynomial Commitment Scheme (PCS)**](./pcs/index.md): Describes the protocol for committing to and opening polynomials with soundness guarantees.
+- [**Proof Generation and Verification**](./stark_proof/index.md): Walks through the process of generating and verifying a STARK proof in Stwo.
+- [**Lookups**](./lookups.md): Discusses lookup arguments and their implementation in Stwo for efficient constraint checking.
diff --git a/src/how-it-works/lookups.md b/src/how-it-works/lookups.md
index 80e610f..434de5a 100644
--- a/src/how-it-works/lookups.md
+++ b/src/how-it-works/lookups.md
@@ -62,28 +62,28 @@ Let's walk through how LogUp is implemented in Stwo using a simple example where
First, we create columns in the original trace, where all values are from the preprocessed trace $A$.
-
+
Figure 1: Create original trace columns that look up values from a preprocessed trace
Then, we add a multiplicity column to the original trace indicating the number of times each value in $A$ appears in the original trace.
-
+
Figure 2: Add a multiplicity column
Next, we create LogUp columns as part of the interaction trace, one for the preprocessed trace and the multiplicity column, and another for the batch of all lookups.
-
+
Figure 3: Create LogUp columns
To create a constraint over the LogUp columns, Stwo modifies the LogUp columns to contain the cumulative sum of the fractions in each row. This results in columns that look like the following:
-
+
Figure 4: Cumulative sum columns
@@ -94,7 +94,7 @@ $$
$$
-
+
Figure 5: Constraint over two rows
@@ -109,7 +109,7 @@ $$
where $\text{avg}$ is a witness value provided by the prover.
-
+
Figure 6: Trick to not create a separate constraint for the first row
diff --git a/src/how-it-works/pcs/index.md b/src/how-it-works/pcs/index.md
new file mode 100644
index 0000000..1e18e97
--- /dev/null
+++ b/src/how-it-works/pcs/index.md
@@ -0,0 +1,9 @@
+# Polynomial Commitment Scheme
+
+> This section presents the implementation of the polynomial commitment scheme in Stwo, which is built on top of the FRI protocol described previously. Polynomial commitments are a core cryptographic primitive that enable a prover to commit to a polynomial and later reveal evaluations at specific points.
+
+This section is organized as follows:
+
+- [**Overview**](./overview.md): Describes the polynomial commitment scheme of Stwo.
+- [**PCS Prover**](./prover.md): Details the implementation of the prover for the polynomial commitment scheme, including commitment and opening protocol.
+- [**PCS Verifier**](./verifier.md): Describes the verifier implementation for checking commitments and evaluation proofs.
\ No newline at end of file
diff --git a/src/how-it-works/pcs/overview.md b/src/how-it-works/pcs/overview.md
new file mode 100644
index 0000000..e2b0a02
--- /dev/null
+++ b/src/how-it-works/pcs/overview.md
@@ -0,0 +1,76 @@
+# Technical Overview
+
+
+In this section, we describe a polynomial commitment scheme using the FRI protocol covered in the previous section.
+
+## Polynomial Commitment Scheme
+
+
+A polynomial commitment scheme (PCS) allows a prover to commit to a polynomial and later prove its evaluations at points chosen by the verifier. The verifier can then check that the evaluations are consistent with the committed polynomial. It consists of the following three algorithms:
+
+
+- $setup(d) \rightarrow pp$: Given an upper bound $d$ on the degree, it outputs public parameters $pp$ used to commit to polynomials of degree less than $d$. For STARKs, the public parameters include the hash functions used for the Merkle commitment scheme and the FRI protocol parameters.
+
+
+- $commit(pp, f) \rightarrow com_f$: Takes public parameters $pp$ and a polynomial $f$ of degree $< d$, and outputs a commitment $com_f$ to the polynomial. For STARKs, $com_f$ is the root of the Merkle tree which commits to the evaluations of the polynomial $f$ on the evaluation domain.
+
+
+- $open(\mathcal{P}, \mathcal{V}) \rightarrow 0/1$: An interactive protocol where the prover $\mathcal{P}$ convinces the verifier $\mathcal{V}$ that $f(u) = v$. The verifier outputs 1 (accept) or 0 (reject). For STARKs, this protocol is based on FRI. The verifier will ask the prover to open the polynomial $f$ (committed using the Merkle tree) at point $u$. The prover will send the opening $v$ and define the quotient:
+$$
+q(x) = \frac{f(x) - v}{x - u}
+$$
+
+If the prover sends the correct opening, then $q$ will be a polynomial of bounded degree. The prover then uses the FRI protocol to convince the verifier that $q$ is "close" to some polynomial with a pre-specified degree bound.
+
+
+For Stwo, we have already described the $commit$ protocol, which evaluates the circle polynomial over a canonical coset and commits to those evaluations using a Merkle tree. The $open$ protocol follows the same idea as the univariate case discussed above, but it is slightly different, as described next.
+
+
+In Stwo, instead of using the single-point opening as described above, we have two-point openings for the values at point $Q$ and its conjugate $\overline{Q}$. The protocol proceeds as follows:
+
+1. The verifier first receives a Merkle commitment to the evaluations of the original polynomial $f$.
+2. The verifier samples a circle point $Q \in C(\mathsf{QM31}) \setminus C(\mathsf{M31})$ and requests the evaluation $f(Q)$ from the prover.
+3. The prover sends the purported value $V$, and then both prover and verifier engage in the FRI protocol on the quotient:
+
+ $$
+ q(x, y) = \frac{f(x, y) - l_{Q,V}(x, y)}{v_Q(x, y)}
+ $$
+
+ Here, $l_{Q,V}(x, y)$ is the linear polynomial interpolating $(Q, V)$ and $(\overline{Q}, \overline{V})$, while $v_Q(x, y)$ vanishes at $Q$ and its conjugate $\overline{Q}$. As in the univariate case, if $q(x, y)$ is "close" to a polynomial, then the verifier is convinced that the evaluation claim is correct, i.e., that $f(Q) = V$.
+
+
+In the above protocol, we are opening the polynomial at a single point $Q$. To open the polynomial at multiple points, we batch the quotients of each point using a random linear combination and then apply the FRI protocol to a single batched quotient.
+
+
+One key property of a polynomial commitment scheme is binding. Informally, the binding property states that once the prover commits to a polynomial, they cannot open some other polynomial which outputs a different evaluation. For STARKs, the binding property is closely related to out-of-domain sampling, which we will describe next.
+
+## Out of Domain Sampling
+
+
+Out-of-domain sampling relates to the notion of "closeness" described in the [FRI section](../circle-fri/overview.md#introduction). Informally, the FRI protocol tests whether a function provided by the prover is "close" to some bounded degree polynomial. There are two notions of "closeness":
+
+1. **Unique Decoding Regime**: We operate in this regime if there is at most a single polynomial which is "close" to the function provided by the prover. If the function is "close" to a single polynomial, then we can infer that the function represents that _unique_ polynomial.
+2. **List Decoding Regime**: We operate in this regime if there is a list of polynomials which are "close" to the function provided by the prover. In this case, since the function can be "close" to a _list_ of polynomials, we cannot be sure that it represents a unique polynomial.
+
+
+In practice, we are usually operate in the list decoding regime. So there can be multiple polynomials which are "close" to the function provided by the prover. This affects the binding property of the polynomial commitment scheme, since the function sent by the prover represents a list of polynomials rather than some unique polynomial.
+
+
+To bind the prover to a unique polynomial from the list, we ask the prover to open the polynomial at an out-of-domain point. This is also referred to as _Domain Extension for Eliminating Pretenders_ (or the _DEEP method_). This is the informal motivation for out-of-domain sampling. For more details, please refer to ["A summary on the FRI low degree test"](https://eprint.iacr.org/2022/1216.pdf).
+
+
+As we have seen in the [Security Analysis section](../circle-fri/overview.md#security-analysis), we can improve security by increasing the number of verifier queries. But this will lead to more prover work, because the prover will have to send a Merkle decommitment for each verifier query and also increase the proof size. We will now see a method to increase the security of our protocol without significantly increasing the prover's work.
+
+## Proof of Work
+
+
+The key idea is that rather than increasing the number of verifier queries, we can increase the cost of generating a false proof by a malicious prover by using _proof of work_ or _grinding_.
+
+
+We add an additional requirement to the FRI protocol: following all the commitments made by the prover, the prover must find a 64-bit nonce that, when hashed together with the state of the hash chain, results in a required number of leading zeros. The number of leading zeros defines a certain amount of work that the prover must perform before generating the randomness representing the queries. As a result, a malicious prover that attempts to generate favorable queries will need to repeat the grinding process every time a commitment is changed. On the other hand, an honest prover only needs to perform the grinding process once.
+
+
+This is similar to the grinding performed on many blockchains. The nonce found by the prover is sent to the verifier as part of the proof, and in turn the verifier checks its consistency with the state of the hash chain by running the hash function once. The required number of leading zeros is configured by the `pow_bits` parameter.
+
+
+This effectively reduces the computational power of the cheating prover while only slightly increasing the running time of the honest prover. This is because the honest prover needs to solve the proof-of-work once, while a cheating prover, during the long process of trying to find a false proof, would need to solve many different instances of the proof-of-work.
diff --git a/src/how-it-works/pcs/prover.md b/src/how-it-works/pcs/prover.md
new file mode 100644
index 0000000..e08e91a
--- /dev/null
+++ b/src/how-it-works/pcs/prover.md
@@ -0,0 +1,122 @@
+# Polynomial Commitment Scheme Prover
+
+
+In this section, we will see the implementation of the commitment scheme prover. We will start by looking at the building blocks.
+
+## Commitment Tree Prover
+
+
+The `CommitmentTreeProver` struct represents the data for a single Merkle tree commitment. As we have seen in the [Merkle tree section](../vcs/merkle_prover.md#merkle-prover), we can commit to multiple polynomials of different degrees in the same Merkle tree. It is implemented as follows:
+
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 198:202}}
+```
+
+Here, `pub type ColumnVec = Vec`. It contains the following fields:
+- `polynomials`: The set of polynomials committed in a single Merkle tree.
+- `evaluations`: The evaluations of these polynomials over their respective domains.
+- `commitment`: The `MerkleProver` struct as described in the [Merkle tree section](../vcs/merkle_prover.md#merkleprover-structure).
+
+It is initialized as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 205:224}}
+```
+
+It proceeds as follows. First, given the `polynomials`, we evaluate them on the evaluation domain using circle FFT to compute `evaluations`. Then we commit to those evaluations using the `MerkleProver` struct. Finally, we create and output the `CommitmentTreeProver` struct.
+
+## Commitment Scheme Prover
+
+
+The `CommitmentSchemeProver` struct is the key struct which maintains a vector of commitment trees. It implements functionalities to open the committed polynomials, compute quotients, and then apply the FRI protocol. It contains the following fields:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 27:31}}
+```
+
+It contains the following fields:
+- `tree`: This contains a vector of commitment trees. Here, `pub struct TreeVec(pub Vec)`.
+- `config`: This is the `PcsConfig`, which contains the `fri_config` and `pow_bits`.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/pcs/mod.rs 29:32}}
+```
+The security of the polynomial commitment scheme is computed as:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/pcs/mod.rs 34:36}}
+```
+- `twiddles`: This contains [precomputed twiddle factors](../circle-fft/twiddles.md#twiddle-tree).
+
+
+Now we will see some key functions defined on the `CommitmentSchemeProver` struct.
+
+### Commit
+
+
+The `commit` function, given a batch of polynomials, computes the `CommitmentTreeProver` struct which commits to the input polynomials and then appends the `tree` struct to the vector of stored `trees`.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 42:51}}
+```
+
+### Trace
+
+The `trace` function returns a `Trace` struct containing all polynomials and their evaluations corresponding to all the commitment trees. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 79:83}}
+```
+
+### Commitment Tree Builder
+
+
+The `tree_builder` function outputs the `TreeBuilder` struct.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 53:59}}
+```
+
+
+The `TreeBuilder` struct is a helper for aggregating polynomials and evaluations before committing them in a Merkle tree. It allows the prover to collect columns (polynomials) and then commit them together as a batch. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 159:163}}
+```
+
+
+### Prove
+
+
+The `prove_values` function is central to the protocol, handling the opening of committed polynomials at specified sample points and integrating with the FRI protocol for low-degree testing. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/pcs/mod.rs 85:156}}
+```
+
+
+Here is a detailed breakdown:
+
+1. **Evaluate Polynomials at Sample Points**:
+ - For each committed polynomial and each sample point (including out-of-domain points and mask points which contain constraint offsets), the function evaluates the polynomials and collects the results in `samples`.
+ - The `sampled_values` are mixed into the channel, ensuring they are bound to the proof and used for subsequent randomness generation.
+
+2. **Compute FRI Quotients**:
+ - The function computes FRI quotient polynomials using `compute_fri_quotients` to open the committed polynomials at sampled points in `samples`. This follows the same quotienting process as described in the [overview section](./overview.md#polynomial-commitment-scheme).
+
+3. **FRI Commitment Phase**:
+ - The FRI protocol is run on the quotient polynomials, committing to their evaluations in Merkle trees and initializing the `fri_prover`. For more details, refer to the [FRI prover section](../circle-fri/fri_prover.md).
+
+4. **Proof of Work**:
+ - A proof-of-work step is performed, with the result mixed into the channel.
+
+6. **FRI Decommitment Phase**:
+ - The function generates random query positions using the channel and decommits the FRI layers at those positions, providing Merkle decommitments for all queried values. For more details, refer to the [FRI prover section](../circle-fri/fri_prover.md).
+
+7. **Decommitment of Committed Trees**:
+ - For each commitment tree, the function decommits the Merkle tree at the FRI query positions, providing the queried values and authentication paths.
+
+8. **Return Proof Object**:
+ - The function returns a `CommitmentSchemeProof` object containing:
+ - Merkle roots of all commitments
+ - Sampled values at all sample points
+ - Merkle decommitments for all queries
+ - Queried values
+ - Proof-of-work result
+ - FRI proof
+ - Protocol configuration
+
+
+
+We will now look into the proof verifier implementation.
diff --git a/src/how-it-works/pcs/verifier.md b/src/how-it-works/pcs/verifier.md
new file mode 100644
index 0000000..97a999d
--- /dev/null
+++ b/src/how-it-works/pcs/verifier.md
@@ -0,0 +1,64 @@
+# Polynomial Commitment Scheme Verifier
+
+
+In this section, we describe the implementation of the polynomial commitment scheme verifier.
+
+## Commitment Scheme Verifier
+
+
+The `CommitmentSchemeVerifier` struct manages the verification process for the polynomial commitment scheme. It maintains a collection of [Merkle verifiers](../vcs/merkle_verifier.md) (one for each commitment tree) and the protocol configuration.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/pcs/verifier.rs 21:24}}
+```
+
+
+We will now see some key functions defined for the `CommitmentSchemeVerifier` struct.
+
+### Read Commitments
+
+The `commit` function reads a Merkle root from the prover and initializes a `MerkleVerifier` for the committed columns. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/pcs/verifier.rs 42:55}}
+```
+
+### Verify
+
+
+The `verify_values` function is the core of the verification protocol. It checks that the prover's openings at the sampled points are consistent with the commitments and that the committed polynomials are of low degree via the FRI protocol. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/pcs/verifier.rs 57:126}}
+```
+
+
+
+Here is a detailed breakdown:
+
+1. **Mix Sampled Values into the Fiat-Shamir Channel**:
+ - The verifier mixes the `sampled_values` (openings at the queried points) into the Fiat-Shamir channel, ensuring that all subsequent randomness is bound to these values.
+
+2. **Draw Random Coefficient**:
+ - The verifier draws a `random_coeff` from the channel, which is used to combine the quotient polynomials in the FRI protocol.
+
+3. **Determine Degree Bounds**:
+ - The verifier computes the degree `bounds` for each column, based on the log sizes and the protocol's blowup factor. These bounds are used to configure the FRI verifier.
+
+4. **FRI Commitment Phase**:
+ - The verifier initializes the `fri_verifier` with the FRI protocol configuration, the FRI proof from the prover, and the degree bounds.
+
+5. **Verify Proof of Work**:
+ - The verifier checks the `proof_of_work` value provided by the prover using the `pow_bits` in the PCS config.
+
+6. **Sample FRI Query Positions**:
+ - The verifier uses the channel to generate random `query_positions_per_log_size` for the FRI protocol.
+
+7. **Verify Merkle Decommitments**:
+ - For each commitment tree, the verifier checks that the Merkle decommitments at the queried positions are valid and that the opened values match the commitments.
+
+8. **Prepare FRI Query Answers**:
+ - The verifier assembles the answers to the FRI queries by matching the sampled points and values, and prepares them for the FRI verifier.
+
+9. **FRI Decommitment Phase**:
+ - The verifier provides the FRI query answers to the FRI verifier, which checks that the quotient polynomials are of low degree.
+
+10. **Return Verification Result**:
+ - If all checks pass, the function returns `Ok(())`. If any check fails (e.g., Merkle decommitment, proof of work, or FRI check), it returns an appropriate error.
diff --git a/src/how-it-works/stark_proof/index.md b/src/how-it-works/stark_proof/index.md
new file mode 100644
index 0000000..bb74098
--- /dev/null
+++ b/src/how-it-works/stark_proof/index.md
@@ -0,0 +1,9 @@
+# Proof Generation and Verification
+
+> In this final section, we cover the implementation of the STARK prover and verifier. This section brings together all the components from previous sections and describes the complete STARK proof generation and verification algorithms. We explain the `prove` and `verify` functions used to generate and verify proofs, as introduced in the [Writing a Simple AIR section](../../air-development/writing-a-simple-air/proving-an-air.md).
+
+This section is organized as follows:
+- [**STARK Prover**](./prove.md): Details the implementation of the proof generation algorithm.
+- [**STARK Verifier**](./verify.md): Describes the verification algorithm.
+
+
diff --git a/src/how-it-works/stark_proof/prove.md b/src/how-it-works/stark_proof/prove.md
new file mode 100644
index 0000000..a00a990
--- /dev/null
+++ b/src/how-it-works/stark_proof/prove.md
@@ -0,0 +1,63 @@
+# STARK Prover
+
+
+This section provides an overview of the `prove` function, the key function in the STARK proof generation process. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/prover/mod.rs 27:84}}
+```
+
+
+Let us go through the function in detail.
+
+## Input and Output
+
+
+It takes the following as input:
+- `components`: A list of AIR components. For more details, refer to the [Components](../air/components.md) and [Prover Components](../air/prover_components.md) sections.
+- `channel`: A Fiat-Shamir channel for non-interactive randomness.
+- `commitment_scheme`: A `CommitmentSchemeProver` for committing to trace and composition polynomials. For more details, refer to the [PCS Prover section](../pcs/prover.md).
+
+
+It outputs a `StarkProof` object if successful, or a `ProvingError` if any constraint is not satisfied. The `StarkProof` object is a wrapper around `CommitmentSchemeProof`.
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/proof.rs 16:16}}
+```
+
+## Step-by-Step Breakdown
+
+
+1. **Determine Preprocessed Columns**
+ - The function determines the number of preprocessed columns, `n_preprocessed_columns`, from the `commitment_scheme`, which is used to initialize the `ComponentProvers` structure.
+
+
+2. **Collect Trace Data**
+ - The `trace`, containing all columns (execution, interaction, preprocessed), is retrieved from the `commitment_scheme`. This includes both coefficient and evaluation forms for each column.
+
+
+3. **Composition Polynomial Construction**
+ - A `random_coeff` is drawn from the channel.
+ - The `composition_poly` is computed as a random linear combination of all constraint quotient polynomials, using powers of the random coefficient. For more details, refer to the [Prover Components](../air/prover_components.md) section.
+
+
+4. **Commit to the Composition Polynomial**
+ - The `composition_poly` is split into coordinate polynomials and committed to using a Merkle tree.
+
+
+5. **Out-of-Domain Sampling (OODS)**
+ - An `oods_point` is drawn randomly from the channel. This point is used to bind the prover to a unique low-degree polynomial, preventing ambiguity in the list decoding regime. For more details, refer to the [Out-of-Domain Sampling](../pcs/overview.md#out-of-domain-sampling) section.
+
+
+6. **Determine Sample Points**
+ - The function computes all `sample_points` required to verify constraints at the OODS point, using the `mask_points` function. This includes all necessary offsets for each constraint and the OODS points for the composition polynomial.
+
+
+7. **Openings and Proof Generation**
+ - The `commitment_scheme` is asked to open all committed polynomials at the sampled points, producing the required evaluations and Merkle authentication paths. This is handled by the `prove_values` function, which also integrates the FRI protocol for low-degree testing. For more details, refer to the [PCS Prover](../pcs/prover.md#prove) section.
+
+
+8. **Sanity Check**
+ - The function checks that the composition polynomial evaluated at the OODS point matches the value reconstructed from the sampled trace values. If not, it returns a `ConstraintsNotSatisfied` error.
+
+
+9. **Return Proof**
+ - If all checks pass, the function returns a `StarkProof` object containing the full proof transcript, including all commitments, openings, and FRI proof.
diff --git a/src/how-it-works/stark_proof/verify.md b/src/how-it-works/stark_proof/verify.md
new file mode 100644
index 0000000..fe5fa72
--- /dev/null
+++ b/src/how-it-works/stark_proof/verify.md
@@ -0,0 +1,55 @@
+# STARK Verifier
+
+This section provides an overview of the `verify` function, the key function that verifies the STARK proof. It is implemented as follows:
+```rust,no_run,noplayground
+{{#webinclude https://raw.githubusercontent.com/starkware-libs/stwo/0790eba46b8af5697083d84fb75bd34b08a0b31f/crates/stwo/src/core/verifier.rs 14:74}}
+```
+
+
+Let us go through the function in detail.
+
+## Input and Output
+
+
+The `verify` function is the entry point for verifying a STARK proof. It takes as input:
+- `components`: A list of AIR components. For more details, refer to the [Components](../air/components.md) section.
+- `channel`: A Fiat-Shamir channel for non-interactive randomness.
+- `commitment_scheme`: A `CommitmentSchemeVerifier` for verifying Merkle commitments and FRI proofs. For more details, refer to the [PCS Verifier section](../pcs/verifier.md).
+- `proof`: The `StarkProof` object to be verified.
+
+
+It returns `Ok(())` if the proof is valid, or a `VerificationError` if any check fails.
+
+## Step-by-Step Breakdown
+
+
+1. **Determine Preprocessed Columns**
+ - The function determines the number of preprocessed columns, `n_preprocessed_columns`, from the `commitment_scheme`, which is used to initialize the `Components` struct.
+
+
+2. **Initialize Components**
+ - The `Components` structure is created, encapsulating all AIR components and the number of preprocessed columns.
+
+
+3. **Read Composition Polynomial Commitment**
+ - The verifier reads the Merkle root of the composition polynomial from the `proof` and registers it with the commitment scheme verifier, along with the degree bounds for each coordinate polynomial.
+
+
+4. **Out-of-Domain Sampling (OODS)**
+ - An `oods_point` is drawn randomly from the channel. This point is used to bind the prover to a unique low-degree polynomial and prevent ambiguity in the list decoding regime.
+
+
+5. **Determine Sample Points**
+ - The function computes all `sample_points` required to verify constraints at the OODS point, using the `mask_points` function. This includes all necessary offsets for each constraint and the OODS points for the composition polynomial.
+
+
+6. **Sanity Check: Composition Polynomial Evaluation**
+ - The function checks that the composition polynomial evaluated at the OODS point (as provided in the proof) matches the value reconstructed from the sampled trace values. If not, it returns an `OodsNotMatching` error.
+
+
+7. **Invoke Commitment Scheme Verifier**
+ - The function calls `verify_values` on the commitment scheme verifier, passing the `sample_points`, the `proof`, and the `channel`. This step checks all Merkle decommitments, FRI low-degree proofs, and protocol soundness.
+
+
+8. **Return Verification Result**
+ - If all checks pass, the function returns `Ok(())`. If any check fails (e.g., Merkle decommitment, FRI check, or OODS mismatch), it returns an appropriate `VerificationError`.