Reflect reviews

src/SUMMARY.md

@@ -6,7 +6,7 @@
 - [Why Stwo?](why-stwo.md)
 - [AIR Development](air-development/index.md)
 
-  - [Writing a Simple AIR](air-development/writing-a-simple-air/index.md)
+  - [First Breath of AIR](air-development/writing-a-simple-air/index.md)
 
     - [Hello World](air-development/writing-a-simple-air/hello-world.md)
     - [Writing a Spreadsheet](air-development/writing-a-simple-air/writing-a-spreadsheet.md)
@@ -36,37 +36,44 @@
   - [Circle Group](how-it-works/circle-group.md)
 
   - [Circle Polynomials](how-it-works/circle-polynomials/index.md)
+
     - [Columns](how-it-works/circle-polynomials/columns.md)
     - [Circle Evaluations and Polynomials](how-it-works/circle-polynomials/evals-and-poly.md)
     - [Secure Evaluations and Polynomials](how-it-works/circle-polynomials/secure-evals-and-poly.md)
-  
+
   - [Circle FFT](how-it-works/circle-fft/index.md)
+
     - [Algorithm](how-it-works/circle-fft/algorithm.md)
     - [Twiddles](how-it-works/circle-fft/twiddles.md)
-    - [Interpolate](how-it-works/circle-fft/interpolation.md)
+    - [Interpolation](how-it-works/circle-fft/interpolation.md)
     - [Basis and Dimension Gap](how-it-works/circle-fft/basis.md)
-  
+
   - [Vector Commitment Scheme](how-it-works/vcs/index.md)
+
     - [Hash Functions](how-it-works/vcs/hash_functions.md)
     - [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)
-  
+
   - [Circle FRI](how-it-works/circle-fri/index.md)
+
     - [Technical Overview](how-it-works/circle-fri/overview.md)
     - [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)
 

src/air-development/additional-examples/index.md

@@ -4,9 +4,9 @@ Here, we introduce some additional AIRs that may help in designing more complex
 
 ## Selectors
 
-A selector is a column of 0s and 1s that is used to selectively enable or disable a constraint. One example of a selector is the `IsFirst` column which has a value of 1 only on the first row. This can be used when constraints are defined over both the current and previous rows but we need to make an exception for the first row.
+A selector is a column of 0s and 1s that selectively enables or disables a constraint. One example of a selector is the `IsFirst` column which has a value of 1 only on the first row. This can be used when constraints are defined over both the current and previous rows but we need to make an exception for the first row.
 
-For example, as seen in [Figure 1](#fig-selectors), when we want to track the cumulative sum of a column, i.e. $b_2 = a_1 + a_2$, the previous row of the first row will point to the last row, creating an incorrect constraint $a_1 = b_4 + b_1$. Thus, we need to disable the constraint for the first row and enable a separate constraint $a_1 = b_1$. This can be achieved by using a selector column that has a value of 1 on the first row and 0 on the other rows and multiplying the constraint by the selector column:
+For example, as seen in [Figure 1](#fig-selectors), when we want to track the cumulative sum of a column, i.e. $b_2 = a_1 + a_2$, the previous row of the first row points to the last row, creating an incorrect constraint $a_1 = b_4 + b_1$. Thus, we need to disable the constraint for the first row and enable a separate constraint $a_1 = b_1$. This can be achieved by using a selector column that has a value of 1 on the first row and 0 on the other rows and multiplying the constraint by the selector column:
 
 $$
 (1 - \text{IsFirst(X)}) \cdot (A(\omega \cdot X) - B(X) - B(\omega \cdot X)) + \text{IsFirst(X)} \cdot (A(X) - B(X)) = 0
@@ -23,7 +23,7 @@ where $X$ refers to the previous value of $\omega\cdot X$ in the multiplicative
 
 Checking that a certain field element is zero is a common use case when writing AIRs. To do this efficiently, we can use the property of finite fields that a non-zero field element always has a multiplicative inverse.
 
-For example, in [Figure 2](#fig-is-zero), we want to check that a field element in $\mathbb{F}_5$ is zero. We create a new column that contains the multiplicative inverse of each field element $a_i$. We then use the multiplication of the two columns and check whether the result is 0 or 1. Note that if the existing column has a zero element, we can insert any value in the new column since the multiplication will always be zero.
+For example, in [Figure 2](#fig-is-zero), we want to check whether a field element in $\mathbb{F}_5$ is zero. We create a new column that contains the multiplicative inverse of each field element $a_i$. We then use the multiplication of the two columns and check whether the result is 0 or 1. Note that if the existing column has a zero element, we can insert any value in the new column since the multiplication will always be zero.
 
 This way, we can create a constraint that uses the `IsZero` condition as part of the constraint, e.g. $(1 - (A(X) \cdot Inv(X))) \cdot (\text{constraint\_1}) + (A(X) \cdot Inv(X)) \cdot (\text{constraint\_2}) = 0$, which checks $\text{constraint\_1}$ if $A(X)$ is 0 and $\text{constraint\_2}$ if $A(X)$ is not 0.
 
@@ -36,13 +36,15 @@ This way, we can create a constraint that uses the `IsZero` condition as part of
 
 When writing AIRs, we may want to expose some values in the trace to the verifier to check in the open. For example, when running an AIR for a Cairo program, we may want to check that the program that was executed is the correct one.
 
-In Stwo, we can achieve this by adding the public input portion of the trace as a LogUp column as negative multiplicity. As shown in [Figure 3](#fig-public-inputs), the public inputs $a_1, a_2$ are added as LogUp values with negative multiplicity $\dfrac{-1}{X - a_1}$ and $\dfrac{-1}{X - a_2}$. The public inputs are given to the verifier as part of the proof and the verifier can directly compute the LogUp values with positive multiplicity $\dfrac{1}{X - a_1}$ and $\dfrac{1}{X - a_2}$ and add it to the LogUp sum and check that the total sum is 0.
+In Stwo, we can achieve this by adding the public input portion of the trace as a LogUp column as negative multiplicity. As shown in [Figure 3](#fig-public-inputs), the public inputs $a_1, a_2$ are added as LogUp values with negative multiplicity $\frac{-1}{X - a_1}$ and $\frac{-1}{X - a_2}$. The public inputs are given to the verifier as part of the proof and the verifier can directly compute the LogUp values with positive multiplicity $\frac{1}{X - a_1}$ and $\frac{1}{X - a_2}$ and add it to the LogUp sum and check that the total sum is 0.
 
 <figure id="fig-public-inputs" style="text-align: center;">
     <img src="./public-inputs.png" width="70%" />
     <figcaption><center><span style="font-size: 0.9em">Figure 3: Public inputs</span></center></figcaption>
 </figure>
 
+One important thing to note is that the public inputs must be added to the Fiat-Shamir channel before drawing random elements for the interaction trace. We refer the reader to this [example implementation](https://github.com/zksecurity/stwo-book/blob/main/stwo-examples/examples/public_input.rs) for reference.
+
 ## XOR
 
 We can also handle XOR operations as part of the AIR. First, as we did in the [Components](../components/index.md) section, we create a computing component and a scheduling component. Then, we connect the two components using lookups: the computing component sets the LogUp value as a negative multiplicity and the scheduling component sets the same value as a positive multiplicity.
@@ -54,4 +56,4 @@ For example, [Figure 4](#fig-xor) shows the XOR operation for 4-bit integers. To
     <figcaption><center><span style="font-size: 0.9em">Figure 4: XOR operations for 4-bit integers</span></center></figcaption>
 </figure>
 
-Note that the M31 field does not fully support XOR operations for 31-bit integers since we cannot use $2^{31} -1$. If we want to use XOR operations for 31-bit integers, we need to decompose the integers into smaller limbs and perform the XOR operation separately on each of the limbs.
+Note that for larger integers, we may need to decompose into smaller limbs to avoid creating large tables. Also note that the M31 field does not fully support XOR operations for 31-bit integers since we cannot use $2^{31} -1$, although this is not feasible as it would require a table of size of around $2^{31} \times 2^{31}$.

src/air-development/components/index.md

@@ -4,13 +4,13 @@ So now that we know how to create a self-contained AIR, the inevitable question
 
 Fortunately, Stwo provides an abstraction called **components** that allows us to create independent AIRs and compose them together. In other proving frontends, this is also commonly referred to as a _chip_, but the idea is the same.
 
-One of the most common use cases of components is to separate frequently used functions (e.g. a hash function) from the main component into a separate component and reuse it, avoiding trace column bloat. Even if the function is not frequently used, it could be useful to separate it into a component to avoid the degree of the constraints becoming too high. This second point is possible because when we create a new component and connect it to the old component, we do it by using lookups, which means that the constraints of the new component are not added to the degree of the old component.
+One of the most common use cases of components is to separate frequently used functions (e.g. a hash function) from the main component into a separate component and reuse it, avoiding trace column bloat. Even if the function is not frequently used, it can be useful to separate it into a component to avoid the degree of the constraints becoming too high. This second point is possible because when we create a new component and connect it to the old component, we do it by using lookups, which means that the constraints of the new component are not added to the degree of the old component.
 
 ## Hash Function Example
 
-To illustrate how to use components, we will create two components where the main component calls a hash function component. For simplicity, instead of an actual hash function, the second component will compute $x^5 + 1$ from an input $x$. This component will have in total three columns: [input, intermediate, output], which will correspond to the values $[x, x^3, x^5 + 1]$. Our main component, on the other hand, will have two columns, [input, output], which corresponds to the values $[x, x^5 + 1]$.
+To illustrate how to use components, we will create two components where the main component calls a hash function component. For simplicity, instead of an actual hash function, the second component will compute $x^5 + 1$ from an input $x$. This component will have, in total, three columns: [input, intermediate, output], which will correspond to the values $[x, x^3, x^5 + 1]$. Our main component, on the other hand, will have two columns, [input, output], which corresponds to the values $[x, x^5 + 1]$.
 
-We'll now refer to the main component as the **scheduling component** and the hash function component the **computing component**, as the main component is essentially _scheduling_ the hash function component to run its function with a given input and the hash function component _computes_ on the provided input. As can be seen in [Figure 1](#fig-component-example), the input and output of each component are connected by lookups.
+We'll refer to the main component as the **scheduling component** and the hash function component as the **computing component**, since the main component is essentially _scheduling_ the hash function component to run its function with a given input and the hash function component _computes_ on the provided input. As can be seen in [Figure 1](#fig-component-example), the input and output of each component are connected by lookups.
 
 <figure id="fig-component-example" style="text-align: center;">
     <img src="./component-example.png" width="100%" />
@@ -24,29 +24,45 @@ We'll now refer to the main component as the **scheduling component** and the ha
     <figcaption><center><span style="font-size: 0.9em">Figure 2: Traces of each component</span></center></figcaption>
 </figure>
 
-When we implement this in Stwo, the traces of each component will look like [Figure 2](#fig-component-trace) above. Each component has its own original and LogUp traces, and each the inputs and outputs of each component are connected by lookups. Since the scheduling component sets the LogUp value as a positive multiplicity and the computing component sets the same value as a negative multiplicity, the verifier can simply check that the sum of the two LogUp columns is zero. Note that we combine the input and output randomly (as $\dfrac{1}{Z - x \cdot \alpha^0 - (x^5+1) \cdot \alpha^1}$) to form a single lookup. This is because we want to ensure that each input is paired with the correct output. If we add the input and output as separate lookups (as $\dfrac{1}{Z - x} + \dfrac{1}{Z - (x^5+1)}$), a malicious prover can switch the output with a different row and still come up with a valid proof. For example, the following traces would be valid:
+When we implement this in Stwo, the traces of each component will look like [Figure 2](#fig-component-trace) above. Each component has its own original and LogUp traces, and the inputs and outputs of each component are connected by lookups. Since the scheduling component sets the LogUp value as a positive multiplicity and the computing component sets the same value as a negative multiplicity, the verifier can simply check that the sum of the two LogUp columns is zero. Note that we combine the input and output randomly as
 
-    Scheduling component
-    ------------
-    | x | H(y) |
-    | y | H(x) |
-    ------------
+$$
+\frac{1}{Z - x \cdot \alpha^0 - (x^5+1) \cdot \alpha^1}
+$$
 
-    Computing component
-    ----------------------
-    | x | x^5 + 1 | H(x) |
-    | y | y^5 + 1 | H(y) |
-    ----------------------
+to form a single lookup. This is because we want to ensure that each input is paired with the correct output. If we add the input and output as separate lookups as
 
-## Code
+$$
+\frac{1}{Z - x} + \frac{1}{Z - (x^5+1)}
+$$
+
+A malicious prover can switch the output with a different row and still come up with a valid proof. For example, the following scheduling component
+
+| Input | Output  |
+| ----- | ------- |
+| x     | y^5 + 1 |
+| y     | x^5 + 1 |
+
+And the following computing component
+
+| Input | Intermediate | Output  |
+| ----- | ------------ | ------- |
+| x     | x^3 + 1      | x^5 + 1 |
+| y     | y^3 + 1      | y^5 + 1 |
+
+would be valid.
+
+## Implementation
+
+Let's move on to the implementation.
 
 ```rust,ignore
 {{#include ../../../stwo-examples/examples/components.rs:main_start}}
 {{#include ../../../stwo-examples/examples/components.rs:main_prove}}
 {{#include ../../../stwo-examples/examples/components.rs:main_end}}
 ```
 
-The code above for proving the components should look pretty familiar by now. Since we need to do everything twice the amount of times, we create structs like `ComponentsStatement0`, `ComponentsStatement1`, `Components` and `ComponentsProof`, but the main logic is the same.
+The code above for proving the components should look pretty familiar by now. Since we need to do everything twice as many times, we create structs like `ComponentsStatement0`, `ComponentsStatement1`, `Components`, and `ComponentsProof`, but the main logic is the same.
 
 Let's take a closer look at how the LogUp columns are generated.
 
@@ -60,7 +76,7 @@ Let's take a closer look at how the LogUp columns are generated.
 {{#include ../../../stwo-examples/examples/components.rs:gen_computing_logup_trace_end}}
 ```
 
-As you can see, the LogUp values of the input and output columns of both the scheduling and computing components are batched together, but in the scheduling component, the output LogUp value is subtracted from the input LogUp value, while in the computing component, the input LogUp value is subtracted from the output LogUp value. This means that when the LogUp sums from both components are added together, they should cancel out and equal zero.
+As you can see, the LogUp values of the input and output columns of both the scheduling and computing components are batched together, but in the scheduling component, the output LogUp value is subtracted from the input LogUp value, while in the computing component, the input LogUp value is subtracted from the output LogUp value. This means that when the LogUp sums from both components are added together, they should cancel out to zero.
 
 Next, let's check how the constraints are created.
 

src/air-development/dynamic-lookups/index.md

@@ -25,7 +25,7 @@ Let's move on to the implementation.
 {{#include ../../../stwo-examples/examples/dynamic_lookups.rs:main_end}}
 ```
 
-Looking at the code above, we can see that it looks very similar to the implementation in the previous section. Instead of creating a preprocessed column, we create two columns where the first column is a random permutation of values `[0, 1 << log_size)` and the second column contains the values in order. Note that this is equivalent to "looking up" all values in the first trace column once. And since all the values are looked up only once, we do not need a separate multiplicity column.
+Looking at the code above, we can see that it looks very similar to the implementation in the previous section. Instead of creating a preprocessed column, we create two columns where the first column is a random permutation of values `[0, 1 << log_size)` and the second column contains the values in order. Note that this is equivalent to "looking up" all values in the first trace column once. And since all the values are looked up exactly once, we do not need a separate multiplicity column.
 
 Then, we create a LogUp column that contains the values $\frac{1}{original} - \frac{1}{permuted}$.
 

src/air-development/index.md

@@ -1,6 +1,6 @@
 # AIR Development
 
-> This section is intended for developers who want to create custom proofs using Stwo (proofs of custom VMs, ML inference, etc.). It assumes that the reader is familiar with Rust and has some background knowledge of cryptography (e.g. finite fields). It also assumes that the reader is familiar with the concept of zero-knowledge proofs and knows what they want to create a zero-knowledge proof for, but it does not assume any firsthand experience with zero-knowledge proof systems.
+> This section is intended for developers who want to create custom proofs using Stwo (proofs of custom VMs, ML inference, etc.). It assumes that the reader is familiar with Rust and has some background knowledge of cryptography (e.g. finite fields). It also assumes that the reader is familiar with the concept of proof systems and knows what they want to create proofs for, but it does not assume any prior experience with creating them.
 
 ```admonish
 All the code that appears throughout this section is available [here](https://github.com/zksecurity/stwo-book/tree/main/stwo-examples).