Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
61 changes: 29 additions & 32 deletions docs.json
Original file line number Diff line number Diff line change
Expand Up @@ -898,6 +898,7 @@
{
"group": "AIR Development",
"pages": [
"learn/S-two-book/air-development/index",
{
"group": "First Breath of AIR",
"pages": [
Expand Down Expand Up @@ -929,37 +930,46 @@
]
},
{
"group": "Stwo: Under the Hood",
"group": "S-two: Under the Hood",
"pages": [
"learn/S-two-book/how-it-works/index",
{
"group": "AIR",
"pages": [
"learn/S-two-book/how-it-works/air/index",
"learn/S-two-book/how-it-works/air/overview",
"learn/S-two-book/how-it-works/air/components",
"learn/S-two-book/how-it-works/air/prover_components"
]
},
"learn/S-two-book/how-it-works/mersenne-prime",
"learn/S-two-book/how-it-works/circle-group",
"learn/S-two-book/how-it-works/lookups",
{
"group": "Circle Polynomials",
"pages": [
"learn/S-two-book/how-it-works/circle-polynomials/index",
"learn/S-two-book/how-it-works/circle-polynomials/columns",
"learn/S-two-book/how-it-works/circle-polynomials/evals-and-poly"
"learn/S-two-book/how-it-works/circle-polynomials/evals-and-poly",
"learn/S-two-book/how-it-works/circle-polynomials/secure-evals-and-poly"
]
},
{
"group": "Circle FFT",
"pages": [
"learn/S-two-book/how-it-works/circle-fft/index",
"learn/S-two-book/how-it-works/circle-fft/algorithm",
"learn/S-two-book/how-it-works/circle-fft/basis",
"learn/S-two-book/how-it-works/circle-fft/twiddles",
"learn/S-two-book/how-it-works/circle-fft/interpolation",
"learn/S-two-book/how-it-works/circle-fft/twiddles"
"learn/S-two-book/how-it-works/circle-fft/basis"
]
},
{
"group": "Vector Commitment Scheme",
"pages": [
"learn/S-two-book/how-it-works/vcs/index",
"learn/S-two-book/how-it-works/vcs/hash_functions",
"learn/S-two-book/how-it-works/vcs/merkle_prover",
"learn/S-two-book/how-it-works/vcs/merkle_verifier"
]
},
{
"group": "AIR to Composition Polynomial",
"pages": [
"learn/S-two-book/how-it-works/air/index",
"learn/S-two-book/how-it-works/air/overview",
"learn/S-two-book/how-it-works/air/components",
"learn/S-two-book/how-it-works/air/prover_components"
]
},
{
Expand All @@ -972,7 +982,7 @@
]
},
{
"group": "PCS",
"group": "Polynomial Commitment Scheme",
"pages": [
"learn/S-two-book/how-it-works/pcs/index",
"learn/S-two-book/how-it-works/pcs/overview",
Expand All @@ -981,31 +991,18 @@
]
},
{
"group": "STARK Proof",
"group": "Proof Generation and Verification",
"pages": [
"learn/S-two-book/how-it-works/stark_proof/index",
"learn/S-two-book/how-it-works/stark_proof/prove",
"learn/S-two-book/how-it-works/stark_proof/verify"
]
},
{
"group": "VCS",
"pages": [
"learn/S-two-book/how-it-works/vcs/index",
"learn/S-two-book/how-it-works/vcs/hash_functions",
"learn/S-two-book/how-it-works/vcs/merkle_prover",
"learn/S-two-book/how-it-works/vcs/merkle_verifier"
]
}
"learn/S-two-book/how-it-works/lookups"
]
},
{
"group": "References",
"pages": [
"learn/S-two-book/benchmarks/index",
"learn/S-two-book/awesome-stwo/index"
]
}
"learn/S-two-book/benchmarks/index",
"learn/S-two-book/awesome-stwo/index"
]
},
{
Expand Down
22 changes: 13 additions & 9 deletions learn/S-two-book/air-development/additional-examples/index.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -9,50 +9,54 @@ Here, we introduce some additional AIRs that may help in designing more complex

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 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:
For example, as seen in [Figure 1](#figure-1), 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
$$

where $X$ refers to the previous value of $\omega\cdot X$ in the multiplicative subgroup of the finite field.

<div id="figure-1" style={{ textAlign: 'center', maxWidth: '70%', height: 'auto', margin: '0 auto', }}>
![](./selectors.png)

*Figure 1: IsFirst selector*
</div>

## IsZero

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 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.
For example, in [Figure 2](#figure-2), 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.

<div id="figure-2" style={{ textAlign: 'center', maxWidth: '50%', height: 'auto', margin: '0 auto', }}>
![](./is-zero.png)

*Figure 2: IsZero over a prime field 5*
</div>

## Public Inputs

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 S-two, 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.
In S-two, 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](#figure-3), 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.

<div id="figure-3" style={{ textAlign: 'center', maxWidth: '80%', height: 'auto', margin: '0 auto', }}>
![](./public-inputs.png)

*Figure 3: Public inputs*
</div>

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](../../stwo-examples/examples/public_input.rs) for reference.
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/starknet-io/starknet-docs/blob/main/learn/S-two-book/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) 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.

For example, [Figure 4](#fig-xor) shows the XOR operation for 4-bit integers. To accommodate the entire combination of inputs, the size of the trace for the computing component is $2^8=256$ rows. Note that the size of the trace for the scheduling component does not have to be the same as the computing component.
For example, [Figure 4](#figure-4) shows the XOR operation for 4-bit integers. To accommodate the entire combination of inputs, the size of the trace for the computing component is $2^8=256$ rows. Note that the size of the trace for the scheduling component does not have to be the same as the computing component.

<div id="figure-4" style={{ textAlign: 'center', maxWidth: '100%', height: 'auto', margin: '0 auto', }}>
![](./xor.png)

*Figure 4: XOR operations for 4-bit integers*
</div>

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}$.
18 changes: 10 additions & 8 deletions learn/S-two-book/air-development/components/index.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -13,19 +13,21 @@ One of the most common use cases of components is to separate frequently used fu

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 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.
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](#figure-1), the input and output of each component are connected by lookups.

<div id="figure-1" style={{ textAlign: 'center', maxWidth: '100%', height: 'auto', margin: '0 auto', }}>
![](./component-example.png)

*Figure 1: Scheduling and Computing components*
</div>

### Design

<div id="figure-2" style={{ textAlign: 'center', maxWidth: '100%', height: 'auto', margin: '0 auto', }}>
![](./component-trace.png)

*Figure 2: Traces of each component*
</div>

When we implement this in S-two, 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
When we implement this in S-two, the traces of each component will look like [Figure 2](#figure-2) 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

$$
\frac{1}{Z - x \cdot \alpha^0 - (x^5+1) \cdot \alpha^1}
Expand Down Expand Up @@ -57,7 +59,7 @@ would be valid.

Let's move on to the implementation.

```rust,ignore
```rust
fn main() {
// --snip--

Expand Down Expand Up @@ -121,7 +123,7 @@ The code above for proving the components should look pretty familiar by now. Si

Let's take a closer look at how the LogUp columns are generated.

```rust,ignore
```rust
fn gen_scheduling_logup_trace(
log_size: u32,
scheduling_col_1: &CircleEvaluation<SimdBackend, M31, BitReversedOrder>,
Expand Down Expand Up @@ -163,7 +165,7 @@ As you can see, the LogUp values of the input and output columns of both the sch

Next, let's check how the constraints are created.

```rust,ignore
```rust
impl FrameworkEval for SchedulingEval {
// --snip--

Expand Down Expand Up @@ -215,7 +217,7 @@ impl FrameworkEval for ComputingEval {

As you can see, we define the LogUp constraints for each component, and we also add two constraints that make sure the computations $x^3$ and $x^5 + 1$ are correct.

```rust,ignore
```rust
fn main() {
// --snip--

Expand Down
7 changes: 4 additions & 3 deletions learn/S-two-book/air-development/dynamic-lookups/index.mdx
Original file line number Diff line number Diff line change
Expand Up @@ -11,13 +11,14 @@ A permutation check simply checks that two sets of values have the same elements

If you went through the previous section, you should have a good intuition for how to implement this. First, create two original trace columns that each contain a random permutation of the same set of values. Then, create a LogUp column where the first original trace column is added as a fraction with multiplicity $1$ and the second original trace column is added as a fraction with multiplicity $-1$. Then, check that the `claimed_sum`, or the sum of the fractions in the two LogUp columns, is $0$.

<div id="figure-1" style={{ textAlign: 'center', maxWidth: '60%', height: 'auto', margin: '0 auto', }}>
![](./permutation-check.png)

*Figure 1: Permutation check*
</div>

Let's move on to the implementation.

```rust,ignore
```rust
fn gen_trace(log_size: u32) -> Vec<CircleEvaluation<SimdBackend, M31, BitReversedOrder>> {
let mut rng = rand::thread_rng();
let values = (0..(1 << log_size)).map(|i| i).collect::<Vec<_>>();
Expand Down Expand Up @@ -88,7 +89,7 @@ Looking at the code above, we can see that it looks very similar to the implemen

Then, we create a LogUp column that contains the values $\frac{1}{original} - \frac{1}{permuted}$.

```rust,ignore
```rust
struct TestEval {
log_size: u32,
lookup_elements: LookupElements,
Expand Down
6 changes: 3 additions & 3 deletions learn/S-two-book/air-development/index.mdx
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
---
title: "AIR Development"
title: "Introduction"
---


> This section is intended for developers who want to create custom proofs using S-two (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.

<Callout type="info">
<Note>
All the code that appears throughout this section is available [here](../stwo-examples/index).
</Callout>
</Note>
Loading