diff --git a/src/SUMMARY.md b/src/SUMMARY.md index 23996ef..d17e11e 100644 --- a/src/SUMMARY.md +++ b/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) diff --git a/src/air-development/additional-examples/index.md b/src/air-development/additional-examples/index.md index df8331f..b0c2bef 100644 --- a/src/air-development/additional-examples/index.md +++ b/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 3: Public inputs
+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
Figure 4: XOR operations for 4-bit integers
-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}$. diff --git a/src/air-development/components/index.md b/src/air-development/components/index.md index e96e672..19ddb1a 100644 --- a/src/air-development/components/index.md +++ b/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.
@@ -24,21 +24,37 @@ We'll now refer to the main component as the **scheduling component** and the ha
Figure 2: Traces of each component
-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}} @@ -46,7 +62,7 @@ When we implement this in Stwo, the traces of each component will look like [Fig {{#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. diff --git a/src/air-development/dynamic-lookups/index.md b/src/air-development/dynamic-lookups/index.md index 856d874..4beb546 100644 --- a/src/air-development/dynamic-lookups/index.md +++ b/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}$. diff --git a/src/air-development/index.md b/src/air-development/index.md index 421c49f..0824377 100644 --- a/src/air-development/index.md +++ b/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). diff --git a/src/air-development/local-row-constraints/index.md b/src/air-development/local-row-constraints/index.md index 56fbe5e..94b6947 100644 --- a/src/air-development/local-row-constraints/index.md +++ b/src/air-development/local-row-constraints/index.md @@ -1,10 +1,10 @@ # Local Row Constraints -Until now, we have only considered constraints that apply over values in a single row. But what if we want to express constraints over multiple rows? For example, we may want to ensure that the difference between the values in two adjacent rows is always the same. +Until now, we have only considered constraints that apply over values in a single row. But what if we want to express constraints over multiple adjacent rows? For example, we may want to ensure that the difference between the values in two adjacent rows is always the same. Turns out we can implement this as an AIR constraint, as long as the same constraints are applied to all rows. We will build upon the example in the previous section, where we created two columns and proved that they are permutations of each other by asserting that the second column looks up all values in the first column exactly once. -Here, we will create two columns and prove that not only are they permutations of each other, but also that the second row is a sorted version of the first row. Since the sorted column will contain in order the values $[0,num\_rows)$, this is equivalent to asserting that **the difference between every current row and the previous row is $1$**. +Here, we will create two columns and prove that not only are they permutations of each other, but also that the second column is a sorted version of the first column. Since the sorted column will contain in order the values $[0,num\_rows)$, this is equivalent to asserting that **the difference between every current row and the previous row is $1$**. We will implement this in three iterations, fixing a different issue in each iteration. @@ -18,9 +18,11 @@ The logic for creating the trace and LogUp columns is basically the same as in t Another change is in the `evaluate` function, where we call `eval.next_interaction_mask(ORIGINAL_TRACE_IDX, [-1, 0])` instead of `eval.next_trace_mask()`. The function `next_trace_mask()` is a wrapper for `next_interaction_mask(ORIGINAL_TRACE_IDX, [0])`, where the first parameter specifies which part of the trace to retrieve values from (see [this figure](../static-lookups/index.md#fig-range-check) for an example of the different parts of a trace). Since we want to retrieve values from the original trace, we set the value of the first parameter to `ORIGINAL_TRACE_IDX`. Next, the second parameter indicates the row offset of the value we want to retrieve. Since we want to retrieve both the previous and current row values for the sorted column, we set the value of the second parameter to `[-1, 0]`. -Once we have these values, we can now assert that the difference between the current and previous row is always `1` with the constraint: `E::F::one() - (sorted_col_curr_row.clone() - sorted_col_prev_row.clone())`. +Once we have these values, we can now assert that the difference between the current and previous row is always one with the constraint: `E::F::one() - (sorted_col_curr_row.clone() - sorted_col_prev_row.clone())`. +```admonish question But this will fail with a `ConstraintsNotSatisfied` error, can you see why? (You can try running it yourself [here](https://github.com/zksecurity/stwo-book/blob/main/stwo-examples/examples/local_row_constraints_fails_1.rs)) +``` ## Second Try @@ -54,7 +56,7 @@ Thus, every time we create a `CircleEvaluation` instance, we need to convert the {{#include ../../../stwo-examples/examples/local_row_constraints.rs:gen_trace}} ``` -And voilà, we have successfully implemented the constraint. You can run it [here](https://github.com/zksecurity/stwo-book/blob/main/stwo-examples/examples/local_row_constraints.rs). +Voilà, we have successfully implemented the constraint. You can run it [here](https://github.com/zksecurity/stwo-book/blob/main/stwo-examples/examples/local_row_constraints.rs). ```admonish summary Things to consider when implementing constraints over multiple rows: diff --git a/src/air-development/preprocessed-trace/index.md b/src/air-development/preprocessed-trace/index.md index 12efda4..23b23b2 100644 --- a/src/air-development/preprocessed-trace/index.md +++ b/src/air-development/preprocessed-trace/index.md @@ -1,21 +1,25 @@ # Preprocessed Trace -> This section and the following sections are intended for developers who have completed the [Writing a Simple AIR](air-development/writing-a-simple-air/index.md) section or are already familiar with the workflow of creating an AIR. If you have not gone through the previous section, we recommend you to do so first as the following sections gloss over a lot of boilerplate code. +> This section and the following sections are intended for developers who have completed the [First Breath of AIR](../writing-a-simple-air/index.md) section or are already familiar with the workflow of creating an AIR. If you have not gone through the previous section, we recommend doing so first as the following sections gloss over a lot of boilerplate code. -For those of you who have completed the [Writing a Simple AIR](air-development/writing-a-simple-air/index.md) tutorial, you should now be familiar with the concept of a trace as a table of integers that are filled in by the prover (we will now refer to this as the **original trace**). +For those of you who have completed the [First Breath of AIR](../writing-a-simple-air/index.md) tutorial, you should now be familiar with the concept of a trace as a table of integers that are filled in by the prover (we will now refer to this as the **original trace**). In addition to the original trace, Stwo also has a concept of a **preprocessed trace**, which is a table whose values are fixed and therefore cannot be arbitrarily chosen by the prover. In other words, these are columns whose values are known in advance of creating a proof and essentially agreed upon by both the prover and the verifier. -One of the use cases of the preprocessed trace is as _a selector for different constraints_. Remember that in an AIR, the same constraints are applied to every row of the trace? If we go back to the spreadsheet analogy, this means that we can't create a spreadsheet that runs different computations for different rows. We can get around this issue by composing multiple constraints using a selector column as part of the preprocessed trace. For example, let's say we want to create a constraint that runs different computations for the first 2 rows and the next 2 rows. We can do this by using a preprocessed trace that has value 1 for the first 2 rows and 0 for the next 2 rows, essentially as a selector for the first 2 rows. The resulting single constraint composes the two different constraints by adding them together: $(1 - \text{preprocessed\_trace}) \cdot \text{constraint\_1} + \text{preprocessed\_trace} \cdot \text{constraint\_2} = 0$ +One of the use cases of the preprocessed trace is as _a selector for different constraints_. Remember that in an AIR, the same constraints are applied to every row of the trace? If we go back to the spreadsheet analogy, this means that we can't create a spreadsheet that runs different computations for different rows. To get around this, note that if we multiply a constraint with a "selector" that is zero, the constraint will be trivially satisfied. Building on this, we can create a selector column of 0s and 1s, and multiply the constraint with the selector column. For example, let's say we want to create a constraint that runs different computations for the first 2 rows and the next 2 rows. We can do this by creating a selector column that has value 0 for the first 2 rows and 1 for the next 2 rows and combining it with the constraints as follows: + +$$ +(1 - \text{selector}) \cdot \text{constraint}_1 + \text{selector} \cdot \text{constraint}_2 = 0 +$$
Figure 1: Preprocessed trace as a selector
-Another use case is to use the preprocessed trace for _expressing constant values used in the constraints_. For example, when creating a hash function in an AIR, we often need to use round constants, which the verifier needs to be able to verify or the resulting hash may be invalid. We can also "look up" the constant values as an optimization technique, which we will discuss in more detail in the next section. +Another use case is to use the preprocessed trace to _express constant values used in constraints_. For example, when creating a hash function in an AIR, we often need to use round constants, which the verifier needs to be able to verify or the resulting hash may be invalid. We can also "look up" the constant values as an optimization technique, which we will discuss in more detail in the next section. -In this section, we will explore how to implement a preprocessed trace as a selector, and we will implement the simplest form: a single `isFirst` column, where the value is 1 for the first row and 0 for all other rows. +In this section, we will explore how to implement a preprocessed trace as a selector, and we will implement the simplest form: a single `IsFirst` column, where the value is 1 for the first row and 0 for all other rows. ```admonish Boilerplate code is omitted for brevity. Please refer to the [full example code](https://github.com/zksecurity/stwo-book/blob/main/stwo-examples/examples/preprocessed_trace.rs) for the full implementation. @@ -25,7 +29,7 @@ Boilerplate code is omitted for brevity. Please refer to the [full example code] {{#include ../../../stwo-examples/examples/preprocessed_trace.rs:is_first_column}} ``` -First, we need to define a `IsFirstColumn` struct that will be used as a preprocessed trace. We will use the `gen_column()` function to generate a `CircleEvaluation` struct that is 1 for the first row and 0 for all other rows. The `id()` function is needed to identify this column when evaluating the constraints. +First, we need to define an `IsFirstColumn` struct that will be used as a preprocessed trace. We will use the `gen_column()` function to generate a `CircleEvaluation` struct that is 1 for the first row and 0 for all other rows. The `id()` function is needed to identify this column when evaluating the constraints. ```rust,ignore {{#include ../../../stwo-examples/examples/preprocessed_trace.rs:main_start}} @@ -35,7 +39,7 @@ First, we need to define a `IsFirstColumn` struct that will be used as a preproc {{#include ../../../stwo-examples/examples/preprocessed_trace.rs:main_end}} ``` -Then, in our main function, we will create and commit to the preprocessed and original traces. For those of you who are curious about why we need to commit to the trace, please refer to the [Committing to the Trace Polynomials](../simplest-air/committing-to-the-trace-polynomials.md) section. +Then, in our main function, we will create and commit to the preprocessed and original traces. For those of you who are curious about why we need to commit to the trace, please refer to the [Committing to the Trace Polynomials](../writing-a-simple-air/committing-to-the-trace-polynomials.md) section. ```rust,ignore {{#include ../../../stwo-examples/examples/preprocessed_trace.rs:test_eval}} @@ -43,7 +47,7 @@ Then, in our main function, we will create and commit to the preprocessed and or Now that we have the traces, we need to create a struct that contains the logic for evaluating the constraints. As mentioned before, we need to use the `is_first_id` field to retrieve the row value of the `IsFirstColumn` struct. Then, we compose two constraints using the `IsFirstColumn` row value as a selector and adding them together. -If you're unfamiliar with how `max_constraint_log_degree_bound(&self)` should be implemented, please refer to [this note](../simplest-air/constraints-over-trace-polynomials.md#max_constraint_log_degree_bound). +If you're unfamiliar with how `max_constraint_log_degree_bound(&self)` should be implemented, please refer to [this note](../writing-a-simple-air/constraints-over-trace-polynomials.md#max_constraint_log_degree_bound). ```rust,ignore {{#include ../../../stwo-examples/examples/preprocessed_trace.rs:main_start}} diff --git a/src/air-development/static-lookups/index.md b/src/air-development/static-lookups/index.md index f094799..80046cb 100644 --- a/src/air-development/static-lookups/index.md +++ b/src/air-development/static-lookups/index.md @@ -1,27 +1,55 @@ # Static Lookups -In the previous section, we showed how to create a preprocessed trace. In this section, we will introduce the concept of an interaction trace, and use it to implement **static lookups**. +In the previous section, we showed how to create a preprocessed trace. In this section, we will introduce the concept of an interaction trace, and use it with the preprocessed trace to implement **static lookups**. -```admonish -Readers who are unfamiliar with the concept of lookups can refer to the [Lookups](../../how-it-works/lookups.md) section for a quick introduction. -``` +Let's start with a brief introduction to lookups. A lookup is a way to connect values from one part of the table to another part of the table. A simple example is when we want to copy values across parts of the table. At first glance, this seems feasible using a constraint. For example, we can copy $col_1$ values to $col_2$ by creating a constraint that $col_1 - col_2$ is equal to $0$. The limitation with this approach, however, is that the same constraint needs to be satisfied over every row in the columns. In other words, we can only check that $col_2$ is an exact copy of $col_1$: + +$$ +col_1[i] = col_2[i] \quad \forall\, i +$$ + +But what if we want to check that $col_2$ is a copy of $col_1$ regardless of the order of the values? This can be done by comparing that the grand product of the random linear combinations of all values in $col_1$ is equal to the grand product of the random linear combinations of all values in $col_2$: + +$$ +\prod_{i=0}^{n-1} (X - col_1[i]) = \prod_{i=0}^{n-1} (X - col_2[i]) +$$ + +where $X$ is a random value from the verifier. + +By taking the logarithmic derivative of each side of the equation, we can rewrite it: -An _interaction trace_ is a trace type that can express values that involve interaction between the prover and the verifier. A good example is lookups, where the LogUp values are determined by randomness provided by the verifier (e.g. in a LogUp fraction $\frac{1}{X-A}$ where $A$ is a lookup value, $X$ is a random value). +$$ +\sum_{i=0}^{n-1} \frac{1}{X-col_1[i]} = \sum_{i=0}^{n-1} \frac{1}{X-col_2[i]} +$$ -We will use this interaction trace to implement a static lookup, which is a lookup where the values that are being looked up are static, i.e. fixed regardless of the values of the original trace. Specifically, we will implement a **range-check AIR**, which checks that a certain value is within a given range. This is useful especially for proof systems like Stwo that use finite fields because it allows checking for underflow and overflow. +We can go further and allow each of the original values to be copied a different number of times. This is supported by modifying the check to the following: + +$$ +\sum_{i=0}^{n-1} \frac{1}{X-col_1[i]} = \sum_{i=0}^{n-1} \frac{m_i}{X-col_2[i]} +$$ + +Where $m_i$ represents the multiplicity, or the number of times $col_1[i]$ appears in $col_2$. + +In Stwo, these fractions (which we will hereafter refer to as _LogUp fractions_) are stored in a special type of trace called an _interaction trace_. An interaction trace is used to contain values that involve interaction between the prover and the verifier. As mentioned above, a LogUp fraction requires a random value $X$ from the verifier, which is why it is stored in an interaction trace. + +## Range-check AIR + +We will now walk through the implementation of a static lookup, which is a lookup where the values that are being looked up are static, i.e. part of the preprocessed trace. Specifically, we will implement a **range-check AIR**, which checks that a certain value is within a given range. This is especially useful for frameworks like Stwo that use finite fields because it allows checking for underflow and overflow. A range-check checks that all values in a column are within a certain range. For example, as in [Figure 1](#fig-range-check), we can check that all values in the range-checked columns are between 0 and 3. We do this by first creating a multiplicity column that counts the number of times each value in the preprocessed trace appears in the range-checked columns. -Then, we create two LogUp columns as part of the interaction trace. The first column contains in each row a fraction where the numerator is the multiplicity and the denominator is the random linear combination of the values in the range column. For example, for row 1, the fraction should be $\dfrac{2}{X-0}$, where $X$ is a random value. The second column contains batches of fractions where the denominator of each fraction is the random linear combination of the value in the range-checked column. Note that the numerator of each fraction is always -1, i.e. we apply a negation, because we want the sum of the first column to be equal to the sum of the second column. +Then, we create two LogUp columns as part of the interaction trace. The first column contains in each row a fraction with numerator equal to the multiplicity and denominator equal to the random linear combination of the value in the range column. For example, for row 1, the fraction should be $\frac{2}{X-0}$, where $X$ is a random value. The second column contains batches of fractions where the denominator of each fraction is the random linear combination of the value in the range-checked column. Note that the numerator of each fraction is always -1, i.e. we apply a negation, because we want the sum of the first column to be equal to the sum of the second column.
Figure 1: Range-check lookup
-If you stare at the LogUp columns hard enough, you'll notice that if we add all the fractions in the two columns together, we get 0. This is no coincidence! The prover will provide the sum of the LogUp columns and the verifier check in the open that this value is indeed 0. +If we add all the fractions in the two columns together, we get 0. This means that the verifier will be convinced with high probability that the values in the range-checked columns are a subset of the values in the range column. + +## Implementation -Now let's move on to the implementation. As Stwo requires the number of rows to be at least 16, we will create a 4-bit range-check, where the range column is of size 16. For convenience, we will set the size of the range-checked columns to be 16 as well. +Now let's move on to the implementation where we create a 4-bit range-check AIR. We do this by creating a preprocessed trace column with the integers $[0, 16)$, then using a lookup to force the values in the original trace columns to lie in the values of the preprocessed column. ```rust,ignore {{#include ../../../stwo-examples/examples/static_lookups.rs:range_check_column}} @@ -53,7 +81,7 @@ Inside `gen_logup_trace`, we create a `LogupTraceGenerator` instance. This is a You may notice that we are iterating over `BaseColumn` in chunks of 16, or `1 << LOG_N_LANES` values. This is because we are using the `SimdBackend`, which runs 16 lanes simultaneously, so we need to preserve this structure. The `Packed` in `PackedSecureField` means that it packs 16 values into a single value. -You may also notice that we are using a `SecureField` instead of just the `Field`. This is because the random value we created in `SmallerThan16Elements` will be in the degree-4 extension field $\mathbb{F}_{p^4}$. Interested readers can refer to the [Mersenne Primes](../../how-it-works/mersenne-prime.md) section for more details. +You may also notice that we are using a `SecureField` instead of just the `Field`. This is because the random value we created by `SmallerThan16Elements` lies in the degree-4 extension field $\mathbb{F}_{p^4}$. This is necessary for the security of the protocol and interested readers can refer to the [Mersenne Primes](../../how-it-works/mersenne-prime.md) section for more details. Once we set the fractions for each `simd_row`, we need to call `finalize_col()` to finalize the column. This process modifies the LogUp columns from individual fractions to cumulative sums of the fractions as shown in [Figure 2](#fig-finalize-col). @@ -83,7 +111,7 @@ And that's it! We have successfully created a static lookup for a range-check. ```admonish **How many fractions can we batch together?** -This depends on how we set the `max_constraint_log_degree_bound` function, as discussed in this [note](../writing-a-simple-air/constraints-over-trace-polynomials.md#max_constraint_log_degree_bound). More specifically, we can batch up to exactly the rate of expansion. +This depends on how we set the `max_constraint_log_degree_bound` function, as discussed in this [note](../writing-a-simple-air/constraints-over-trace-polynomials.md#max_constraint_log_degree_bound). More specifically, we can batch up to exactly the blowup factor. e.g. diff --git a/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials-1.png b/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials-1.png index c9ae3df..0dacd5d 100644 Binary files a/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials-1.png and b/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials-1.png differ diff --git a/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials.md b/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials.md index c665f85..27ee7da 100644 --- a/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials.md +++ b/src/air-development/writing-a-simple-air/committing-to-the-trace-polynomials.md @@ -14,12 +14,12 @@ As we can see in [Figure 1](#fig-committing-to-the-trace-polynomials-1), Stwo co {{#include ../../../stwo-examples/examples/committing_to_the_trace_polynomials.rs:here_2}} ``` -We begin with some setup. First, we create a default `PcsConfig` instance, which sets the values for the FRI and PoW operations. Setting non-default values is related to the security of the proof, which is out of the scope for this tutorial. +We begin with some setup. First, we create a default `PcsConfig` instance, which sets the values for the FRI and PoW operations. Setting non-default values is related to the security of the proof, which is outside the scope of this tutorial. Next, we precompute twiddles, which are factors multiplied during FFT for a particular domain. Notice that the log size of the domain is set to `log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + config.fri_config.log_blowup_factor`, which is the max log size of the domain that is needed throughout the proving process. For committing to the trace polynomial, we only need to add `config.fri_config.log_blowup_factor` but as we will see in the next section, we also need to commit to a polynomial of a higher degree, which is the reason we also add `LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR`. -The final setup is creating a commitment scheme and a channel. The commitment scheme will be used to commit to the trace polynomials as Merkle trees, while the channel will be used to keep a running hash of all data in the proving process (i.e. transcript of the proof). This is part of the Fiat-Shamir transformation where randomness can be generated safely even in a non-interactive setting. Here, we use the `Blake2sChannel` and `Blake2sMerkleChannel` for the channel and commitment scheme, respectively, but we can also use the `Poseidon252Channel` and `Poseidon252MerkleChannel` pair. +The final setup is creating a commitment scheme and a channel. The commitment scheme will be used to commit to the trace polynomials as Merkle trees, while the channel will be used to keep a running hash of all data in the proving process (i.e. transcript of the proof). This is part of the Fiat-Shamir transformation, which derives randomness safely in a non-interactive setting. Here, we use the `Blake2sChannel` and `Blake2sMerkleChannel` for the channel and commitment scheme, respectively, but we can also use the `Poseidon252Channel` and `Poseidon252MerkleChannel` pair. -Now that we have our setup, we can commit to the trace polynomials. But before we do so, we need to first commit to an empty vector called a _preprocessed trace_, which doesn't do anything but is required by Stwo. Then, we need to commit to the size of the trace, which is a vital part of the proof system that the prover should not be able to cheat on. Once we have done these, we can finally commit to the original trace polynomials. +Now that we have our setup, we can commit to the trace polynomials. But before we do so, we need to first commit to an empty vector called a _preprocessed trace_, which doesn't do anything but is required by Stwo. Then, we need to commit to the size of the trace, which is another vital part that the prover should not be able to cheat on. After doing so, we can finally commit to the original trace polynomials. Now that we have committed to the trace polynomials, we can move on to how we can create constraints over the trace polynomials! diff --git a/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials-1.png b/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials-1.png index d1793a6..e726231 100644 Binary files a/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials-1.png and b/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials-1.png differ diff --git a/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials.md b/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials.md index 54c2848..935a427 100644 --- a/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials.md +++ b/src/air-development/writing-a-simple-air/constraints-over-trace-polynomials.md @@ -11,7 +11,7 @@ When we want to perform computations over the cells in a spreadsheet, we don't w We can do the same thing with our table, except in addition to autofilling cells, we can also create a constraint that the result was computed correctly. Remember that the purpose of using a proof system is that the verifier can verify a computation was executed correctly without having to execute it themselves? Well, that's exactly why we need to create a constraint. -Now let's say we want to add a new column `C` to our spreadsheet that computes the product of the previous columns plus the first column. We can set `C1` as `A1 * B1 + A1` as in [Figure 2](#fig-constraints-over-trace-polynomials-2). And then we can constrain the value of the third column by creating an equation that must equal 0: `col1_row1 * col2_row1 + col1_row1 - col3_row1 = 0`. +Now let's say we want to add a new column `C` to our spreadsheet that computes the product of the previous columns plus the first column. We can set `C1` as `A1 * B1 + A1` as in [Figure 2](#fig-constraints-over-trace-polynomials-2). The corresponding constraint is expressed as `C1 = A1 * B1 + A1`. However, we use an alternate representation `A1 * B1 + A1 - C1 = 0` because we can only enforce constraints stating that an expression should equal zero. Generalizing this constraint to the whole column, we get `col1_row1 * col2_row1 + col1_row1 - col3_row1 = 0`.
@@ -22,7 +22,11 @@ Now let's say we want to add a new column `C` to our spreadsheet that computes t Obviously, as can be seen in [Figure 2](#fig-constraints-over-trace-polynomials-2), our new constraint is satisfied for every row in the table. This means that we can substitute creating a constraint for each row with a single constraint over the columns, i.e. the trace polynomials. -Thus, `col1_row1 * col2_row1 + col1_row1 - col3_row1 = 0` becomes $f_1(x) \cdot f_2(x) + f_1(x) - f_3(x) = 0$. +Thus, `col1_row1 * col2_row1 + col1_row1 - col3_row1 = 0` becomes: + +$$ +f_1(x,y) \cdot f_2(x,y) + f_1(x,y) - f_3(x,y) = 0 +$$ ```admonish The idea that all rows must have the same constraint may seem restrictive, compared to say a spreadsheet where we can define different functions for different rows. However, we will show in later sections how to handle such use-cases. @@ -34,21 +38,19 @@ The idea that all rows must have the same constraint may seem restrictive, compa We will now give a name to the polynomial that expresses the constraint: a **composition polynomial**. -$C(x) = f_1(x) \cdot f_2(x) + f_1(x) - f_3(x)$ +$$ +C(x,y) = f_1(x,y) \cdot f_2(x,y) + f_1(x,y) - f_3(x,y) +$$ Basically, in order to prove that the constraints are satisfied, we need to show that the composition polynomial evaluates to 0 over the original domain (i.e. the domain of size the number of rows in the table). -But first, as can be seen in [Figure 1](#fig-constraints-over-trace-polynomials-1), we need to expand the evaluations of the trace polynomials by a factor of 2. This is because when you multiply two trace polynomials of degree `n-1` (where `n` is the number of rows) to compute the constraint polynomial, the degree of the constraint polynomial will be the sum of the degrees of the trace polynomials, which is `2n-2`. To adjust for this increase in degree, we double the number of evaluations. - -Once we have the expanded evaluations, we can evaluate the composition polynomial. Checking that the composition polynomial evaluates to 0 over the original domain is done in FRI, so once again we need to expand the composition polynomial evaluations by a factor of 2 and commit to them. +But first, as can be seen in the upper part of [Figure 1](#fig-constraints-over-trace-polynomials-1), we need to expand the evaluations of the trace polynomials by a factor of 2. This is because when you multiply two trace polynomials of degree `n-1` (where `n` is the number of rows) to compute the constraint polynomial, the degree of the constraint polynomial will be the sum of the degrees of the trace polynomials, which is `2n-2`. To adjust for this increase in degree, we double the number of evaluations. -```admonish -In the actual Stwo code, we commit not to the composition polynomial, but to the quotient polynomial. The quotient polynomial is the composition polynomial divided by the vanishing polynomial, i.e., a polynomial that evaluates to 0 in the original domain. However, we intentionally omit this detail for the sake of simplicity. -``` +Once we have the expanded evaluations, we can evaluate the composition polynomial $C(x,y)$. Since we need to do a FRI operation on the composition polynomial as well, we expand the evaluations again by a factor of 2 and commit to them as a merkle tree. This part corresponds to the bottom part of [Figure 1](#fig-constraints-over-trace-polynomials-1). -We'll see in the code below how this is implemented. +## Implementation -## Code +Let's see how this is implemented in the code. ```rust,ignore {{#include ../../../stwo-examples/examples/constraints_over_trace_polynomials.rs:here_1}} @@ -59,23 +61,23 @@ We'll see in the code below how this is implemented. {{#include ../../../stwo-examples/examples/constraints_over_trace_polynomials.rs:here_4}} ``` -First, we add a new column `col_3` that contains the result of the computation: `col_1 * col_2 + col_1`. +First, we add a new column `col_3` that contains the result of the computation: `col_1 * col_2 + col_1`. Note that all the columns are padded with 0 to a length of 16 via `BaseColumn::zeros(num_rows)` and we got lucky because this satisfies our constraint (i.e. `0 * 0 + 0 - 0 = 0`), so we don't need to modify the constraint. Then, to create a constraint over the trace polynomials, we first create a `TestEval` struct that implements the `FrameworkEval` trait. Then, we add our constraint logic in the `FrameworkEval::evaluate` function. Note that this function is called for every row in the table, so we only need to define the constraint once. -Inside `FrameworkEval::evaluate`, we call `eval.next_trace_mask()` consecutively three times, retrieving the cell values of all three columns (see [Figure 3](#fig-constraints-over-trace-polynomials-3) below for a visual representation). Once we retrieve all three column values, we add a constraint of the form `col_1 * col_2 + col_1 - col_3`, which should equal 0. +Inside `FrameworkEval::evaluate`, we call `eval.next_trace_mask()` consecutively three times, retrieving the cell values of all three columns (see [Figure 3](#fig-constraints-over-trace-polynomials-3) below for a visual representation). Once we retrieve all three column values, we add a constraint of the form `col_1 * col_2 + col_1 - col_3`, which should equal 0. Note that `FrameworkEval::evaluate` will be called for every row in the table.
Figure 3: Evaluate function
-We also need to implement `FrameworkEval::max_constraint_log_degree_bound(&self)` for `FrameworkEval`. As mentioned in the [Composition Polynomial section](#composition-polynomial), we need to expand the trace polynomial evaluations because the degree of our composition polynomial is higher than the trace polynomial. Expanding it by the lowest value `LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR=1` is sufficient for our example as we only have one multiplication gate, so we return `self.log_size + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR`. For those who are interested in how to set this value in general, we leave a detailed note below. +We also need to implement `FrameworkEval::max_constraint_log_degree_bound(&self)` for `FrameworkEval`. As mentioned in the [Composition Polynomial section](#composition-polynomial), we need to expand the trace polynomial evaluations because the degree of our composition polynomial is higher than that of the trace polynomial. Expanding it by `LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR=1` is sufficient for our example as the total degree of the highest degree term $f_1(x,y) \cdot f_2(x,y)$ is 2, so we return `self.log_size + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR`. For those who are interested in how to set this value in general, we leave a detailed note below. ```admonish id="max_constraint_log_degree_bound" **What value to set for `max_constraint_log_degree_bound(&self)`?** -`self.log_size + max(1, ceil(log2(max_degree - 1)))`, where `max_degree` is the maximum degree of all defined constraint polynomials. +`self.log_size + max(1, ceil(log2(max_degree - 1)))`, where `max_degree` is the maximum total degree of all defined constraint polynomials. For example, the `max_degree` of constraint $f_1(x,y) \cdot f_2(x,y) = 0$ is 2, while that of $f_1(x,y) \cdot f_1(x,y) \cdot f_2(x,y) \cdot f_3(x,y) = 0$ is 4. e.g. - degree 1 - 3: `self.log_size + 1` @@ -86,7 +88,8 @@ e.g. ``` ````admonish -Now that we know the degree of the composition polynomial, we can also explain the following code: +Now that we know the degree of the composition polynomial, we can now why we need to set the `log_size` of the domain to `log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + config.fri_config.log_blowup_factor` when precomputing twiddles in the following code: + ```rust,ignore // Precompute twiddles for evaluating and interpolating the trace let twiddles = SimdBackend::precompute_twiddles( @@ -98,8 +101,11 @@ Now that we know the degree of the composition polynomial, we can also explain t ); ``` -Why is the `log_size` of the domain set to `log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + config.fri_config.log_blowup_factor` here? As we can see in [Figure 1](#fig-constraints-over-trace-polynomials-1), once we have the composition polynomial, we need to expand it again for before committing to it for the FRI step. Thus, the maximum size of the domain that we need in the entire proving process is the FRI blow-up factor times the degree of the composition polynomial. +To prove that the composition polynomial evaluates to 0 over the trace domain (since the composition polynomial is composed of constraints that evaluates to 0 over the trace domain), we first divide the composition polynomial by the **vanishing polynomial**, which is a polynomial that evaluates to 0 over the trace domain. If the composition polynomial is created correctly, this will result in a polynomial instead of a rational function, and we can perform FRI over this polynomial to prove this. + +Thus, we need to commit to this new polynomial, which is called the **quotient polynomial**. We can calculate its degree by subtracting the degree of the vanishing polynomial from the degree of the composition polynomial. Since the trace is of size `1 << log_num_rows`, the degree of the vanishing polynomial will be `1 << log_num_rows - 1`, so the resulting degree will be `1 << (log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR) - (1 << log_num_rows - 1)`. However, since we can only commit to a power of two degree, we can just use the `1 << (log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR)` value. +If we apply the FRI blowup as well, we finally end up with the following log domain size: `log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + config.fri_config.log_blowup_factor`. ```` Using the new `TestEval` struct, we can create a new `FrameworkComponent::` component, which the prover will use to evaluate the constraint. For now, we can ignore the other parameters of the `FrameworkComponent::` constructor. @@ -111,7 +117,7 @@ Finally, we can break down what an Algebraic Intermediate Representation (AIR) m *Algebraic* means that we are using polynomials to represent the constraints. -*Intermediate Representation* means that this is a modified representation of our statement so that it can be proven by a proof system. +*Intermediate Representation* means that this is a modified representation of our statement so that it can be proven. So AIR is just another way of saying that we are representing statements to be proven as constraints over polynomials. ``` diff --git a/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials-1.png b/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials-1.png index 6215b86..d502a34 100644 Binary files a/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials-1.png and b/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials-1.png differ diff --git a/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials.md b/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials.md index ab9e099..a8d1ea5 100644 --- a/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials.md +++ b/src/air-development/writing-a-simple-air/from-spreadsheet-to-trace-polynomials.md @@ -12,7 +12,7 @@ In the previous section, we created a table (aka spreadsheet). In this section,
Figure 2: From spreadsheet to trace polynomials
-In STARKs, the computation trace is represented as evaluations of a polynomial over some domain. Typically this domain is a coset of a multiplicative subgroup. But since the multiplicative subgroup of M31 is not smooth, Stwo works over the circle group which is the subgroup of degree-2 extension of M31 (as explained in the [Mersenne Primes](../../how-it-works/mersenne-prime.md) and [Circle Group](../../how-it-works/circle-group.md) sections). Thus the domain in Stwo is formed of points $(x_i, y_i)$ on the circle curve. When interpolating a polynomial over the computation trace using the points on the circle curve as domain gives a bivariate trace polynomial $f_j(x, y)$. +In STARKs, the computation trace is represented as evaluations of a polynomial over some domain. Typically this domain is a coset of a multiplicative subgroup. But since the multiplicative subgroup of M31 is not smooth, Stwo works over the circle group which is the subgroup of degree-2 extension of M31 (as explained in the [Mersenne Primes](../../how-it-works/mersenne-prime.md) and [Circle Group](../../how-it-works/circle-group.md) sections). Thus the domain in Stwo is formed of points $(x_i, y_i)$ on the circle curve. Note that when we interpolate a polynomial over the points on the circle curve, we get a bivariate trace polynomial $f_j(x, y)$. We will explain why using a polynomial representation is useful in the next section, but for now, let's see how we can create trace polynomials for our code. Note that we are building upon the code from the previous section, so there's not much new code here. diff --git a/src/air-development/writing-a-simple-air/hello-world.md b/src/air-development/writing-a-simple-air/hello-world.md index 9a39040..3f51360 100644 --- a/src/air-development/writing-a-simple-air/hello-world.md +++ b/src/air-development/writing-a-simple-air/hello-world.md @@ -6,7 +6,7 @@ Let's first set up a Rust project with Stwo. $ cargo new stwo-example ``` -We need to specify the nightly Rust compiler to use Stwo. +We need to specify the nightly Rust version to use Stwo. ```bash $ echo -e "[toolchain]\nchannel = \"nightly-2025-01-02\"" > rust-toolchain.toml diff --git a/src/air-development/writing-a-simple-air/index-1.png b/src/air-development/writing-a-simple-air/index-1.png index ee0a03a..22d6403 100644 Binary files a/src/air-development/writing-a-simple-air/index-1.png and b/src/air-development/writing-a-simple-air/index-1.png differ diff --git a/src/air-development/writing-a-simple-air/index.md b/src/air-development/writing-a-simple-air/index.md index 7a23f08..460ada9 100644 --- a/src/air-development/writing-a-simple-air/index.md +++ b/src/air-development/writing-a-simple-air/index.md @@ -1,4 +1,4 @@ -# Writing a Simple AIR +# First Breath of AIR
@@ -7,4 +7,4 @@ Welcome to the guide for writing AIRs in Stwo! -In this "Writing a Simple AIR" section, we will go through the process of writing a simple AIR from scratch. This requires some understanding of the proving lifecycle in Stwo, so we added a diagram showing a high-level overview of the whole process. As we go through each step, please note that the diagram may contain more steps than the code. This is because there are steps that are abstracted away by the Stwo implementation, but is necessary for understanding the code that we need to write when creating an AIR. +In this section, we will go through the process of writing a simple AIR from scratch. This requires some understanding of the proving lifecycle in Stwo, so we added a diagram showing a high-level overview of the whole process. As we go through each step, please note that the diagram may contain more steps than the code. This is because there are steps that are abstracted away by the Stwo implementation, but are necessary to understand the code that we write when creating an AIR. diff --git a/src/air-development/writing-a-simple-air/proving-an-air-1.png b/src/air-development/writing-a-simple-air/proving-an-air-1.png index 0a7af40..f85c330 100644 Binary files a/src/air-development/writing-a-simple-air/proving-an-air-1.png and b/src/air-development/writing-a-simple-air/proving-an-air-1.png differ diff --git a/src/air-development/writing-a-simple-air/proving-an-air.md b/src/air-development/writing-a-simple-air/proving-an-air.md index 74c4541..b9549ae 100644 --- a/src/air-development/writing-a-simple-air/proving-an-air.md +++ b/src/air-development/writing-a-simple-air/proving-an-air.md @@ -5,7 +5,7 @@
Figure 1: Prover workflow: perform FRI and PoW
-We're finally ready to take the final step--prove and verify an AIR! +We're finally ready for the last step: prove and verify an AIR! Since the code is relatively short, let us present it first and then go over the details. @@ -16,11 +16,11 @@ Since the code is relatively short, let us present it first and then go over the ## Prove -As you can see, there is only a single line of code added to create the proof. The `prove` function performs the FRI and PoW operations under the hood, although technically, the constraint related steps in [Figure 1](#fig-proving-an-air-1) were not performed in the previous section and are only performed once `prove` is called. +As you can see, there is only a single line of code added to create the proof. The `prove` function performs the FRI and PoW operations under the hood, although, technically, the constraint-related steps in [Figure 1](#fig-proving-an-air-1) were not performed in the previous section and are only performed once `prove` is called. ## Verify -In order to verify our proof, we need to check that the constraints are satisfied using the commitments from the proof. In order to do that, we need to set up a `Blake2sChannel` and `CommitmentSchemeVerifier`, along with the same `PcsConfig` that we used when creating the proof. Then, we need to recreate the running hash channel by passing the Merkle tree commitments and the `log_num_rows` to the `CommitmentSchemeVerifier` instance by calling `commit` (remember, the order is important!). Then, we can verify the proof using the `verify` function. +In order to verify our proof, we need to check that the constraints are satisfied using the commitments from the proof. In order to do that, we need to set up a `Blake2sChannel` and `CommitmentSchemeVerifier`, along with the same `PcsConfig` that we used when creating the proof. Then, we need to recreate the Fiat-Shamir channel by passing the Merkle tree commitments and the `log_num_rows` to the `CommitmentSchemeVerifier` instance by calling `commit` (remember: the order is important!). Then, we can verify the proof using the `verify` function. ```admonish exercise Try setting the dummy values in the table to 1 instead of 0. Does it fail? If so, can you see why? diff --git a/src/air-development/writing-a-simple-air/writing-a-spreadsheet-1.png b/src/air-development/writing-a-simple-air/writing-a-spreadsheet-1.png index 0d90708..87f0313 100644 Binary files a/src/air-development/writing-a-simple-air/writing-a-spreadsheet-1.png and b/src/air-development/writing-a-simple-air/writing-a-spreadsheet-1.png differ diff --git a/src/air-development/writing-a-simple-air/writing-a-spreadsheet.md b/src/air-development/writing-a-simple-air/writing-a-spreadsheet.md index 077ab7b..4cb3aaa 100644 --- a/src/air-development/writing-a-simple-air/writing-a-spreadsheet.md +++ b/src/air-development/writing-a-simple-air/writing-a-spreadsheet.md @@ -5,7 +5,7 @@
Figure 1: Prover workflow: Create a table
-In order to write a proof, we first need to create a table of rows and columns. This is no different than writing integers to an Excel spreadsheet as we can see in [Figure 2](#fig-writing-a-spreadsheet-2). +In order to write a proof, we first need to create a table of rows and columns. This is no different from writing integers to an Excel spreadsheet as we can see in [Figure 2](#fig-writing-a-spreadsheet-2).
@@ -14,7 +14,7 @@ In order to write a proof, we first need to create a table of rows and columns. But there is a slight caveat to consider when creating the table. Stwo implements [SIMD operations](https://en.wikipedia.org/wiki/Single_instruction,_multiple_data) to speed up the prover in the CPU, but this requires providing the table cells in chunks of 16 rows. Simply put, this is because Stwo supports 16 lanes of 32-bit integers, which means that the same instruction can be run simultaneously for 16 different data. -Alas, for our table, we will need to create 14 dummy rows to make the total number of rows equal to 16, as shown in [Figure 2](#fig-writing-a-spreadsheet-3). For the sake of simplicity, however, we will omit the dummy rows in the diagrams of the following sections. +Alas, for our table, we will need to create 14 dummy rows to make the total number of rows equal to 16, as shown in [Figure 3](#fig-writing-a-spreadsheet-3). For the sake of simplicity, however, we will omit the dummy rows in the diagrams of the following sections.
@@ -29,6 +29,6 @@ Given all that, let's create this table using Stwo. As mentioned above, we instantiate the `num_rows` of our table as `N_LANES=16` to accommodate SIMD operations. Then we create a `BaseColumn` of `N_LANES=16` rows for each column and populate the first two rows with our values and the rest with dummy values. -Note that the values in the `BaseColumn` need to be of type `M31`, which refers to the Mersenne-31 prime field that Stwo uses. This means that the integers in the table must be in the range $[0, 2^{31}-1)$. +Note that the values in the `BaseColumn` need to be of type `M31`, which refers to the Mersenne-31 prime field that Stwo uses. This means that the integers in the table must lie in the range $[0, 2^{31}-1)$. Now that we have our table, let's move on! diff --git a/src/cairo-air/add-opcode/index.md b/src/cairo-air/add-opcode/index.md index 04f469f..64fd01d 100644 --- a/src/cairo-air/add-opcode/index.md +++ b/src/cairo-air/add-opcode/index.md @@ -55,7 +55,7 @@ carry_limb_2 * (carry_limb_2 - 1) = 0 op0[27] + op1[27] + carry_limb_27 - dst[27] = 0 ``` -We divide `op0[0] + op1[0] - dst[0]` by `2^9` since this quantity is either `2^9` (if a carry exists) or `0` (if no carry exists). Dividing by `2^9` yields `1` or `0`, respectively. To check that the carry is either `0` or `1`, we add the constraint `carry_limb_0 * (carry_limb_0 - 1) = 0`. For the final limb, we simply check that the addition is correct. +We divide `op0[0] + op1[0] - dst[0]` by `2^9` since this quantity is either `2^9` (if a carry exists) or `0` (if no carry exists). Dividing by `2^9` yields one or zero, respectively. To check that the carry is either `0` or `1`, we add the constraint `carry_limb_0 * (carry_limb_0 - 1) = 0`. For the final limb, we simply check that the addition is correct. ### Handling overflow beyond the 252-bit prime field diff --git a/src/cairo-air/basic-building-blocks/index.md b/src/cairo-air/basic-building-blocks/index.md index 9ec87c8..4eb0bb9 100644 --- a/src/cairo-air/basic-building-blocks/index.md +++ b/src/cairo-air/basic-building-blocks/index.md @@ -8,6 +8,6 @@ Cairo works over the prime field $P = 2^{251} + 17 \cdot 2^{192} + 1$, while Stw ## Range checks -Range-checks are very commonly used in the Cairo AIR. They are used to ensure that the values of the witness values are within a certain range, most commonly within a certain bit length. For example, in the [Felt252 to M31](../basic-building-blocks/index.md#felt252-to-m31) section, we saw that a 252-bit integer is decomposed into 28 9-bit limbs, so we need to verify that each limb is in the range $0 \leq \text{limb} < 2^{9}$. +Range-checks are very commonly used in the Cairo AIR. They are used to ensure that the witness values are within a certain range, most commonly within a certain bit length. For example, in the [Felt252 to M31](../basic-building-blocks/index.md#felt252-to-m31) section, we saw that a 252-bit integer is decomposed into 28 9-bit limbs, so we need to verify that each limb is in the range $0 \leq \text{limb} < 2^{9}$. This is done by using a preprocessed column that contains the entire range of possible values for the bit length. For example, for a 9-bit range check, the column will contain the values from 0 to $2^9 - 1$. We also have another column that contains the number of times the range-check was invoked for each valid value and we use lookups to check that each range-check is valid. For a more practical example, please refer to the [Static Lookups](../../air-development/static-lookups/index.md) section. diff --git a/src/cairo-air/cairo/index.md b/src/cairo-air/cairo/index.md index f79baa5..0abc163 100644 --- a/src/cairo-air/cairo/index.md +++ b/src/cairo-air/cairo/index.md @@ -14,7 +14,7 @@ The memory is also non-deterministic: the prover provides the values of the memo ## Registers -In physical CPUs, accessing memory is expensive compared to accessing registers due to physical proximity. This is why instructions typically operate over registers rather than directly over memory cells. In Cairo, accessing memory and registers incur the same cost, so Cairo instructions operate directly over memory cells. Thus, the three registers used in Cairo do not store instructions or operand values like in physical CPUs, but rather pointers to the memory cells where the instructions and operands are stored: +In physical CPUs, accessing memory is expensive compared to accessing registers due to physical proximity. This is why instructions typically operate over registers rather than directly over memory cells. In Cairo, accessing memory and registers incur the same cost, so Cairo instructions operate directly over memory cells. Thus, the three registers used by Cairo do not store instructions or operand values like in physical CPUs, but rather pointers to the memory cells where the instructions and operands are stored: - `pc` is the **program counter**, which points to the current Cairo instruction - `ap` is the **allocation pointer**, which points to the current available memory address @@ -37,7 +37,7 @@ The next 15 bits are flags. The `dst_reg` and `op0_reg` 1-bit flags indicate whe For a more detailed explanation of the flags, please refer to Section 4.5 of the [Cairo paper](https://eprint.iacr.org/2021/1063.pdf). ``` -Finally, the last bit is fixed to 0, but as we will see in the next section, this design is modified in the current version of Cairo to support opcode extensions. +Finally, the last bit is fixed to 0, but as we will see in the next section, this design has been modified in the current version of Cairo to support opcode extensions. ### Opcodes and Opcode Extensions diff --git a/src/cairo-air/main-components/index.md b/src/cairo-air/main-components/index.md index 5d1e65b..8b99104 100644 --- a/src/cairo-air/main-components/index.md +++ b/src/cairo-air/main-components/index.md @@ -1,6 +1,6 @@ # Main Components -Now that we have a basic understanding of how Cairo works and the basic building blocks that are used to build the Cairo AIR, let's take a look at the main components of the Cairo AIR. +Now that we have a basic understanding of Cairo and the building blocks that are used to build the Cairo AIR, let's take a look at the main components of the Cairo AIR. ```admonish For readers who are unfamiliar with the concepts of components and lookups, we suggest going over the [Components](../../air-development/components/index.md) section of the book. diff --git a/src/how-it-works/lookups.md b/src/how-it-works/lookups.md index 434de5a..e08f92f 100644 --- a/src/how-it-works/lookups.md +++ b/src/how-it-works/lookups.md @@ -90,7 +90,7 @@ To create a constraint over the LogUp columns, Stwo modifies the LogUp columns t A constraint is created using the values of two rows of the cumulative sum LogUp column. For example, as in [Figure 5](#fig-lookup-implementation-5), we can create a constraint by subtracting $row_1$ from $row_2$ and checking that it equals the LogUp fraction created using values $a_2$ and $m_2$: $$ -\dfrac{m_2}{X - a_2} = row\_2 - row\_1 +\frac{m_2}{X - a_2} = row\_2 - row\_1 $$
@@ -98,15 +98,15 @@ $$
Figure 5: Constraint over two rows
-However, this constraint actually does not hold for the first row since $\dfrac{m_1}{X - a_1} \neq row_1 - row_n$. A typical solution to this problem would be to disable this constraint for the first row and create a separate constraint that is enabled only on the first row. +However, this constraint actually does not hold for the first row since $\frac{m_1}{X - a_1} \neq row_1 - row_n$. A typical solution to this problem would be to disable this constraint for the first row and create a separate constraint that is enabled only on the first row. But Stwo solves this problem differently. First, before we accumulate the original LogUp column rows, we subtract each row by the average of the total sum of the rows. Only then do we accumulate each row. This way, the last row of the column will always equal zero, so we do not need to make an exception for the first row. The final constraint for the second row looks as follows: $$ -\dfrac{m_2}{X - a_2} = row\_2 - row\_1 + \text{avg} +\frac{m_2}{X - a_2} = row\_2 - row\_1 + \text{avg} $$ -where $\text{avg}$ is a witness value provided by the prover. +Where $\text{avg}$ is a witness value provided by the prover.
@@ -119,8 +119,8 @@ The right column in [Figure 6](#fig-lookup-implementation-6) is the final form o In general, batching multiple lookups together helps reduce the size of the proof as it reduces the number of LogUp columns, which means we can commit to fewer columns. However, we cannot batch an arbitrary number of fractions together because it increases the degree of the constraint polynomial. -More specifically, the degree of the constraint polynomial increases linearly with the number of fractions in the batch. Let's say we want to batch $k$ fractions together. This will create a constraint $\dfrac{1}{X - a_1} + \dfrac{1}{X - a_2} + ... + \dfrac{1}{X - a_k} = \text{sum} - \text{prev\_sum}$. Once we multiply both sides by the common denominator, we get a constraint of degree $k+1$ from the product $(X - a_1)\cdot \dots \cdot (X - a_k) \cdot \text{sum}$. +More specifically, the degree of the constraint polynomial increases linearly with the number of fractions in the batch. Let's say we want to batch $k$ fractions together. This will create a constraint $\frac{1}{X - a_1} + \frac{1}{X - a_2} + ... + \frac{1}{X - a_k} = \text{sum} - \text{prev\_sum}$. Once we multiply both sides by the common denominator, we get a constraint of degree $k+1$ from the product $(X - a_1)\cdot \dots \cdot (X - a_k) \cdot \text{sum}$. -To illustrate the accounting for how many fractions we can batch together, we first need to understand how the degree of the composition polynomial is calculated in Stwo. Here, the composition polynomial is the constraint polynomial divided by the quotient polynomial, where the quotient polynomial is the vanishing polynomial of the trace domain (i.e. evaluates to 0 over the trace domain). So let's say we have a degree-$m$ constraint on two columns: $a^m + b^m = 0$. We can define the composition polynomial as $\dfrac{a^m + b^m}{x^N - 1}$ where $N$ is the trace height. The degree of $a$ and $b$ is $N-1$ so, if the constraint holds, the degree of the composition polynomial is $m \cdot (N-1) - N = (m-1) \cdot N - m$. Thus, given that we already has $N$ evaluations, we can expand it by $m-1$ to convince the verifier that the constraint holds since $(m-1) \cdot N > (m-1) \cdot N - m$. +To illustrate the accounting for how many fractions we can batch together, we first need to understand how the degree of the composition polynomial is calculated in Stwo. Here, the composition polynomial is the constraint polynomial divided by the quotient polynomial, where the quotient polynomial is the vanishing polynomial of the trace domain (i.e. evaluates to 0 over the trace domain). So let's say we have a degree-$m$ constraint on two columns: $a^m + b^m = 0$. We can define the composition polynomial as $\frac{a^m + b^m}{x^N - 1}$ where $N$ is the trace height. The degree of $a$ and $b$ is $N-1$ so, if the constraint holds, the degree of the composition polynomial is $m \cdot (N-1) - N = (m-1) \cdot N - m$. Thus, given that we already has $N$ evaluations, we can expand it by $m-1$ to convince the verifier that the constraint holds since $(m-1) \cdot N > (m-1) \cdot N - m$. Now, coming back to the question of how many fractions we can batch together, we can see that we can batch up to exactly $k$ fractions if the rate of expansion is $k$. diff --git a/src/introduction.md b/src/introduction.md index f0b9d29..8105ab2 100644 --- a/src/introduction.md +++ b/src/introduction.md @@ -6,4 +6,4 @@ Stwo is a state-of-the-art framework for creating STARK proofs that provides the - A backend that leverages Circle STARKs over the Mersenne31 prime field for fast prover performance - Seamlessly integrated with Cairo -This book will guide you through the process of creating your own constraints and then proving them using Stwo and also provide in-depth explanations of the inner workings of Stwo. +This book will guide you through the process of creating your own constraints and then proving them using Stwo. It will also provide in-depth explanations of the inner workings of how Stwo implements Circle STARKs. diff --git a/src/why-stwo-1.png b/src/why-stwo-1.png index 6cc3447..06f25d3 100644 Binary files a/src/why-stwo-1.png and b/src/why-stwo-1.png differ diff --git a/src/why-stwo.md b/src/why-stwo.md index bf4c6de..037ec44 100644 --- a/src/why-stwo.md +++ b/src/why-stwo.md @@ -1,12 +1,12 @@ # Why Stwo? -Before we dive into why we should choose Stwo, let's define some terminology. When we talked about proof systems in the previous section, we were only referring to the part that takes a statement and outputs a proof. In reality, however, we first need to structure the statement in a way that it can be proven by the proof system. This structuring part is often referred to as the **frontend**, and the proof system is commonly called the **backend**. +Before we dive into why we should choose Stwo, let's define some terminology. When we talked about proof systems in the previous section, we mentioned that we can create a proof of a statement using a proof system. In reality, however, we first need to structure the function involved in the statement in a way that it can be proven. This structuring part is often referred to as the **frontend**, while the rest of the process of creating a proof is commonly referred to as the **backend**. With that out of the way, let's dive into some of the advantages of using Stwo. First, Stwo is a standalone framework that provides both the frontend and backend and therefore handles the entire proving process. There are other frameworks that only provide the frontend or the backend, which has its advantages as its modular structure makes it possible to pick and choose a backend or frontend of one's liking. However, having a single integrated frontend and backend reduces the complexity of the system and is also easier to maintain. -In addition, Stwo's frontend structures statements in the **Algebraic Intermediate Representation (AIR)**, which is a representation that is especially useful for proving statements that are repetitive (e.g. the CPU in a VM, which essentially repeats the same fetch-decode-execute over and over again). +In addition, Stwo's frontend structures statements as an **Algebraic Intermediate Representation (AIR)**, which is a representation that is especially useful for proving statements that are repetitive (e.g. the CPU in a VM, which essentially repeats the same fetch-decode-execute over and over again). Stwo's backend is also optimized for prover performance. This is due to largely three factors. diff --git a/src/why-use-a-proof-system.md b/src/why-use-a-proof-system.md index 6ea43bf..93eb6b7 100644 --- a/src/why-use-a-proof-system.md +++ b/src/why-use-a-proof-system.md @@ -1,9 +1,9 @@ # Why Use a Proof System? -At its core, a proof system can prove the validity of a statement $C(x)=y$ where $C$ is a representation of some logic, while $x$ is an input and $y$ the output of said logic. (Assuming that we are only dealing with logic that can be expressed as a computation, we will henceforth refer to this logic as a computation). This means that we can verify the validity of a statement by either directly running the computation, or by verifying the validity of the proof produced with the proof system. The verifier can benefit from the second option in terms of time and space, if the time to verify the proof is faster than the time to run the computation, or the size of the proof is smaller than the input to the statement. +At its core, a proof system proves that a statement is valid. For example, it can prove that a function with a certain input results in a certain output, i.e. $C(x)=y$. To check the statement, we can do it either directly by computing $C(x)$ and comparing the result to $y$, or indirectly by verifying the proof. The verifier can benefit from the second option in terms of time and space, if the time to verify the proof is faster than the time to compute the function, or the size of the proof is smaller than the input to the statement. -This property of a proof system is often referred to as **succinctness**, and it is exactly why proof systems have seen wide adoption in the blockchain space, where computation on-chain is much more expensive compared to off-chain computation. Using a proof system, it becomes possible to replace a large collection of computation to be executed on-chain with a proof of execution of the same collection of computation and verifying it on-chain. This way, proof generation can be handled off-chain using large machines and only the proof verification needs to be done on-chain. +This property of a proof system is often referred to as **succinctness**, and it is exactly why proof systems have seen wide adoption in the blockchain space, where computation on-chain is much more expensive compared to off-chain computation. Using a proof system, it becomes possible to replace a large collection of computation to be executed on-chain with a proof of execution of the same collection of computations and verifying it on-chain. This way, proofs can be generated off-chain using large machines and verified on-chain with much less computation. -But there are applications of proof systems beyond just blockchains. Since a proof is verifiable as well as succinct, it can also be used as auxiliary data to verify that the computation of an untrusted party was done correctly. For example, when we delegate computation to an untrusted server, we can ask it to provide a proof along with the computation result that the result indeed came from running a specific computation. Another example could be to ask a server running an ML model to provide proof that it ran inference on the correct model. The size of the accompanying proof and the time to verify it will be negligible compared to the cost of running the computation, but we gain the guarantee that the computation was done correctly. +But there are applications of proof systems beyond just blockchains. Generally speaking, it can be used as auxiliary data to verify that the computation of an untrusted party was done correctly. For example, when we delegate computation to an untrusted server, we can ask it to provide a proof along with the computation result that the result indeed came from running a specific computation. Another example could be to ask a server running an ML model to provide proof that it ran inference on the correct model. The size of the accompanying proof and the time to verify it will be negligible compared to the cost of running the computation, but we gain the guarantee that the computation was done correctly. -Another optional feature of proof systems is **zero-knowledge**, which means that the proof reveals nothing about the computation other than its validity. In general, the output $y$ of the computation $C(x)=y$ will be public (i.e. revealed to the verifier), but the input $x$ may be split into public and private parts, so that the verifier does not learn anything about the private part. With this feature, the intermediate values computed by the prover while computing $C(x)$ will also be hidden from the verifier. +Another optional feature of proof systems is **zero-knowledge**, which means that the proof reveals nothing about the computation other than its validity. In general, the output $y$ of the computation $C(x)=y$ will be public (i.e. revealed to the verifier), but the input $x$ will be, without loss of generality, private from the verifier. With this feature, the intermediate values computed by the prover while computing $C(x)$ will also be hidden from the verifier. diff --git a/stwo-examples/Cargo.lock b/stwo-examples/Cargo.lock index fea8d5b..af65dd3 100644 --- a/stwo-examples/Cargo.lock +++ b/stwo-examples/Cargo.lock @@ -2,6 +2,12 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "allocator-api2" +version = "0.2.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "683d7910e743518b0e34f1186f92494becacb047c7b6bf616c96772180fef923" + [[package]] name = "ark-ff" version = "0.4.2" @@ -80,9 +86,9 @@ checksum = "7c02d123df017efcdfbd739ef81735b36c5ba83ec3c59c80a9d7ecc718f92e50" [[package]] name = "autocfg" -version = "1.4.0" +version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" +checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" [[package]] name = "bigdecimal" @@ -107,16 +113,15 @@ dependencies = [ [[package]] name = "blake3" -version = "1.6.0" +version = "1.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1230237285e3e10cde447185e8975408ae24deaa67205ce684805c25bc0c7937" +checksum = "3888aaa89e4b2a40fca9848e400f6a658a5a3978de7be858e209cafa8be9a4a0" dependencies = [ "arrayref", "arrayvec", "cc", "cfg-if", "constant_time_eq", - "memmap2", ] [[package]] @@ -130,50 +135,45 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.17.0" +version = "3.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1628fb46dfa0b37568d12e5edd512553eccf6a22a78e8bde00bb4aed84d5bdbf" +checksum = "46c5e41b57b8bba42a04676d81cb89e9ee8e859a1a66f80a5a72e1cb76b34d43" [[package]] name = "bytemuck" -version = "1.21.0" +version = "1.24.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ef657dfab802224e671f5818e9a4935f9b1957ed18e58292690cc39e7a4092a3" +checksum = "1fbdf580320f38b612e485521afda1ee26d10cc9884efaaa750d383e13e3c5f4" dependencies = [ "bytemuck_derive", ] [[package]] name = "bytemuck_derive" -version = "1.8.1" +version = "1.10.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3fa76293b4f7bb636ab88fd78228235b5248b4d05cc589aed610f954af5d7c7a" +checksum = "f9abbd1bc6865053c427f7198e6af43bfdedc55ab791faed4fbd361d789575ff" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] -[[package]] -name = "byteorder" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" - [[package]] name = "cc" -version = "1.2.15" +version = "1.2.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c736e259eea577f443d5c86c304f9f4ae0295c43f3ba05c21f1d66b5f06001af" +checksum = "ac9fe6cdbb24b6ade63616c0a0688e45bb56732262c158df3c0c4bea4ca47cb7" dependencies = [ + "find-msvc-tools", "shlex", ] [[package]] name = "cfg-if" -version = "1.0.0" +version = "1.0.4" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" [[package]] name = "constant_time_eq" @@ -242,14 +242,14 @@ dependencies = [ "enum-ordinalize", "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] name = "either" -version = "1.14.0" +version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b7914353092ddf589ad78f25c5c1c21b7f80b0ff8621e7c814c3485b5306da9d" +checksum = "48c757948c5ede0e46177b7add2e67155f70e33c07fea8284df6576da70b3719" [[package]] name = "enum-ordinalize" @@ -268,14 +268,38 @@ checksum = "0d28318a75d4aead5c4db25382e8ef717932d0346600cacae6357eb5941bc5ff" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "find-msvc-tools" +version = "0.1.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "52051878f80a721bb68ebfbc930e07b65ba72f2da88968ea5c06fd6ca3d3a127" + +[[package]] +name = "fnv" +version = "1.0.7" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3f9eec918d3f24069decb9af1554cad7c880e2da24a9afd88aca000531ab82c1" + +[[package]] +name = "foldhash" +version = "0.2.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "77ce24cb58228fbb8aa041425bb1050850ac19177686ea6e0f41a70416f56fdb" + [[package]] name = "generic-array" -version = "0.14.7" +version = "0.14.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a" +checksum = "4bb6743198531e02858aeaea5398fcc883e71851fcbcb5a2f773e2fb6cb1edf2" dependencies = [ "typenum", "version_check", @@ -283,9 +307,9 @@ dependencies = [ [[package]] name = "getrandom" -version = "0.2.15" +version = "0.2.16" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" +checksum = "335ff9f135e4384c8150d6f27c6daed433577f86b4750418338c01a1a2528592" dependencies = [ "cfg-if", "js-sys", @@ -294,6 +318,17 @@ dependencies = [ "wasm-bindgen", ] +[[package]] +name = "hashbrown" +version = "0.16.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5419bdc4f6a9207fbeba6d11b604d481addf78ecd10c11ad51e76c2f6482748d" +dependencies = [ + "allocator-api2", + "equivalent", + "foldhash", +] + [[package]] name = "hex" version = "0.4.3" @@ -309,6 +344,16 @@ dependencies = [ "digest", ] +[[package]] +name = "indexmap" +version = "2.12.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6717a8d2a5a929a1a2eb43a12812498ed141a0bcfb7e8f7844fbdbe4303bba9f" +dependencies = [ + "equivalent", + "hashbrown", +] + [[package]] name = "itertools" version = "0.10.5" @@ -329,9 +374,9 @@ dependencies = [ [[package]] name = "js-sys" -version = "0.3.77" +version = "0.3.81" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1cfaf33c695fc6e08064efbc1f72ec937429614f25eef83af942d0e227c3a28f" +checksum = "ec48937a97411dcb524a265206ccd4c90bb711fca92b2792c407f268825b9305" dependencies = [ "once_cell", "wasm-bindgen", @@ -339,24 +384,15 @@ dependencies = [ [[package]] name = "libc" -version = "0.2.170" +version = "0.2.177" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "875b3680cb2f8f71bdcf9a30f38d48282f5d3c95cbf9b3fa57269bb5d5c06828" +checksum = "2874a2af47a2325c2001a6e6fad9b16a53b802102b528163885171cf92b15976" [[package]] name = "log" -version = "0.4.26" +version = "0.4.28" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30bde2b3dc3671ae49d8e2e9f044c7c005836e7a023ee57cffa25ab82764bb9e" - -[[package]] -name = "memmap2" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fd3f7eed9d3848f8b98834af67102b720745c4ec028fcd0aa0239277e7de374f" -dependencies = [ - "libc", -] +checksum = "34080505efa8e45a4b816c349525ebe327ceaa8559756f0356cba97ef3bf7432" [[package]] name = "num-bigint" @@ -388,9 +424,9 @@ dependencies = [ [[package]] name = "once_cell" -version = "1.20.3" +version = "1.21.3" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "945462a4b81e43c4e3ba96bd7b49d834c6f61198356aa858733bc4acf3cbe62e" +checksum = "42f5e15c9953c5e4ccceeb2e7382a716482c34515315f7b03532b8b4e8393d2d" [[package]] name = "paste" @@ -406,27 +442,27 @@ checksum = "3b3cff922bd51709b605d9ead9aa71031d81447142d828eb4a6eba76fe619f9b" [[package]] name = "ppv-lite86" -version = "0.2.20" +version = "0.2.21" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "77957b295656769bb8ad2b6a6b09d897d94f05c41b069aede1fcdaa675eaea04" +checksum = "85eae3c4ed2f50dcfe72643da4befc30deadb458a9b590d720cde2f2b1e97da9" dependencies = [ "zerocopy", ] [[package]] name = "proc-macro2" -version = "1.0.93" +version = "1.0.102" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60946a68e5f9d28b0dc1c21bb8a97ee7d018a8b322fa57838ba31cc878e22d99" +checksum = "8e0f6df8eaa422d97d72edcd152e1451618fed47fabbdbd5a8864167b1d4aff7" dependencies = [ "unicode-ident", ] [[package]] name = "quote" -version = "1.0.38" +version = "1.0.41" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e4dccaaaf89514f546c693ddc140f729f958c247918a13380cccc6078391acc" +checksum = "ce25767e7b499d1b604768e7cde645d14cc8584231ea6b295e9c9eb22c02e1d1" dependencies = [ "proc-macro2", ] @@ -480,37 +516,53 @@ dependencies = [ "semver", ] +[[package]] +name = "rustversion" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" + [[package]] name = "semver" -version = "1.0.25" +version = "1.0.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f79dfe2d285b0488816f30e700a7438c5a73d816b5b7d3ac72fbc48b0d185e03" +checksum = "d767eb0aabc880b29956c35734170f26ed551a859dbd361d140cdbeca61ab1e2" [[package]] name = "serde" -version = "1.0.218" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", + "serde_derive", +] + +[[package]] +name = "serde_core" +version = "1.0.228" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e8dfc9d19bdbf6d17e22319da49161d5d0108e4188e8b680aef6299eed22df60" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" dependencies = [ "serde_derive", ] [[package]] name = "serde_derive" -version = "1.0.218" +version = "1.0.228" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f09503e191f4e797cb8aac08e9a4a4695c5edf6a2e70e376d961ddd5c969f82b" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] name = "sha2" -version = "0.10.8" +version = "0.10.9" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8" +checksum = "a7507d819769d01a365ab707794a4084392c824f54a7a6a7862f8c3d0892b283" dependencies = [ "cfg-if", "cpufeatures", @@ -551,7 +603,7 @@ checksum = "bbc159a1934c7be9761c237333a57febe060ace2bc9e3b337a59a37af206d19f" dependencies = [ "starknet-curve", "starknet-ff", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] @@ -578,34 +630,59 @@ dependencies = [ ] [[package]] -name = "stwo-examples" +name = "std-shims" version = "0.1.0" -dependencies = [ - "itertools 0.12.1", - "num-traits", - "rand", - "stwo-prover", -] +source = "git+https://github.com/starkware-libs/stwo.git?rev=75a6b0ac9bcc7101d8658445dded51923ab2586f#75a6b0ac9bcc7101d8658445dded51923ab2586f" [[package]] -name = "stwo-prover" +name = "stwo" version = "0.1.1" -source = "git+https://github.com/starkware-libs/stwo.git?rev=92984c060b49d0db05e021883755fac0a71a2fa7#92984c060b49d0db05e021883755fac0a71a2fa7" +source = "git+https://github.com/starkware-libs/stwo.git?rev=75a6b0ac9bcc7101d8658445dded51923ab2586f#75a6b0ac9bcc7101d8658445dded51923ab2586f" dependencies = [ "blake2", "blake3", "bytemuck", "cfg-if", "educe", + "fnv", + "hashbrown", "hex", + "indexmap", "itertools 0.12.1", "num-traits", "rand", "serde", "starknet-crypto", "starknet-ff", + "std-shims", "thiserror", "tracing", + "tracing-subscriber", +] + +[[package]] +name = "stwo-constraint-framework" +version = "0.1.1" +source = "git+https://github.com/starkware-libs/stwo.git?rev=75a6b0ac9bcc7101d8658445dded51923ab2586f#75a6b0ac9bcc7101d8658445dded51923ab2586f" +dependencies = [ + "hashbrown", + "itertools 0.12.1", + "num-traits", + "rand", + "std-shims", + "stwo", + "tracing", +] + +[[package]] +name = "stwo-examples" +version = "0.1.0" +dependencies = [ + "itertools 0.12.1", + "num-traits", + "rand", + "stwo", + "stwo-constraint-framework", ] [[package]] @@ -627,9 +704,9 @@ dependencies = [ [[package]] name = "syn" -version = "2.0.98" +version = "2.0.108" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36147f1a48ae0ec2b5b3bc5b537d267457555a10dc06f3dbc8cb11ba3006d3b1" +checksum = "da58917d35242480a05c2897064da0a80589a2a0476c9a3f2fdc83b53502e917" dependencies = [ "proc-macro2", "quote", @@ -638,22 +715,22 @@ dependencies = [ [[package]] name = "thiserror" -version = "1.0.69" +version = "2.0.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" +checksum = "f63587ca0f12b72a0600bcba1d40081f830876000bb46dd2337a3051618f4fc8" dependencies = [ "thiserror-impl", ] [[package]] name = "thiserror-impl" -version = "1.0.69" +version = "2.0.17" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" +checksum = "3ff15c8ecd7de3849db632e14d18d2571fa09dfc5ed93479bc4485c7a517c913" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] @@ -669,35 +746,44 @@ dependencies = [ [[package]] name = "tracing-attributes" -version = "0.1.28" +version = "0.1.30" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "395ae124c09f9e6918a2310af6038fba074bcf474ac352496d5910dd59a2226d" +checksum = "81383ab64e72a7a8b8e13130c49e3dab29def6d0c7d76a03087b3cf71c5c6903" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] name = "tracing-core" -version = "0.1.33" +version = "0.1.34" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e672c95779cf947c5311f83787af4fa8fffd12fb27e4993211a84bdfd9610f9c" +checksum = "b9d12581f227e93f094d3af2ae690a574abb8a2b9b7a96e7cfe9647b2b617678" dependencies = [ "once_cell", ] +[[package]] +name = "tracing-subscriber" +version = "0.3.20" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2054a14f5307d601f88daf0553e1cbf472acc4f2c51afab632431cdcd72124d5" +dependencies = [ + "tracing-core", +] + [[package]] name = "typenum" -version = "1.18.0" +version = "1.19.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1dccffe3ce07af9386bfd29e80c0ab1a8205a2fc34e4bcd40364df902cfa8f3f" +checksum = "562d481066bde0658276a35467c4af00bdc6ee726305698a55b86e61d7ad82bb" [[package]] name = "unicode-ident" -version = "1.0.17" +version = "1.0.20" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00e2473a93778eb0bad35909dff6a10d28e63f792f16ed15e404fca9d5eeedbe" +checksum = "462eeb75aeb73aea900253ce739c8e18a67423fadf006037cd3ff27e82748a06" [[package]] name = "version_check" @@ -707,40 +793,42 @@ checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" [[package]] name = "wasi" -version = "0.11.0+wasi-snapshot-preview1" +version = "0.11.1+wasi-snapshot-preview1" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" +checksum = "ccf3ec651a847eb01de73ccad15eb7d99f80485de043efb2f370cd654f4ea44b" [[package]] name = "wasm-bindgen" -version = "0.2.100" +version = "0.2.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1edc8929d7499fc4e8f0be2262a241556cfc54a0bea223790e71446f2aab1ef5" +checksum = "c1da10c01ae9f1ae40cbfac0bac3b1e724b320abfcf52229f80b547c0d250e2d" dependencies = [ "cfg-if", "once_cell", + "rustversion", "wasm-bindgen-macro", + "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-backend" -version = "0.2.100" +version = "0.2.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2f0a0651a5c2bc21487bde11ee802ccaf4c51935d0d3d42a6101f98161700bc6" +checksum = "671c9a5a66f49d8a47345ab942e2cb93c7d1d0339065d4f8139c486121b43b19" dependencies = [ "bumpalo", "log", "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-macro" -version = "0.2.100" +version = "0.2.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7fe63fc6d09ed3792bd0897b314f53de8e16568c2b3f7982f468c0bf9bd0b407" +checksum = "7ca60477e4c59f5f2986c50191cd972e3a50d8a95603bc9434501cf156a9a119" dependencies = [ "quote", "wasm-bindgen-macro-support", @@ -748,52 +836,51 @@ dependencies = [ [[package]] name = "wasm-bindgen-macro-support" -version = "0.2.100" +version = "0.2.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ae87ea40c9f689fc23f209965b6fb8a99ad69aeeb0231408be24920604395de" +checksum = "9f07d2f20d4da7b26400c9f4a0511e6e0345b040694e8a75bd41d578fa4421d7" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", "wasm-bindgen-backend", "wasm-bindgen-shared", ] [[package]] name = "wasm-bindgen-shared" -version = "0.2.100" +version = "0.2.104" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a05d73b933a847d6cccdda8f838a22ff101ad9bf93e33684f39c1f5f0eece3d" +checksum = "bad67dc8b2a1a6e5448428adec4c3e84c43e561d8c9ee8a9e5aabeb193ec41d1" dependencies = [ "unicode-ident", ] [[package]] name = "zerocopy" -version = "0.7.35" +version = "0.8.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" +checksum = "0894878a5fa3edfd6da3f88c4805f4c8558e2b996227a3d864f47fe11e38282c" dependencies = [ - "byteorder", "zerocopy-derive", ] [[package]] name = "zerocopy-derive" -version = "0.7.35" +version = "0.8.27" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" +checksum = "88d2b8d9c68ad2b9e4340d7832716a4d21a22a1154777ad56ea55c51a9cf3831" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] [[package]] name = "zeroize" -version = "1.8.1" +version = "1.8.2" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ced3678a2879b30306d323f4542626697a464a97c0a07c9aebf7ebca65cd4dde" +checksum = "b97154e67e32c85465826e8bcc1c59429aaaf107c1e4a9e53c8d8ccd5eff88d0" dependencies = [ "zeroize_derive", ] @@ -806,5 +893,5 @@ checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69" dependencies = [ "proc-macro2", "quote", - "syn 2.0.98", + "syn 2.0.108", ] diff --git a/stwo-examples/Cargo.toml b/stwo-examples/Cargo.toml index bf14c77..d616521 100644 --- a/stwo-examples/Cargo.toml +++ b/stwo-examples/Cargo.toml @@ -5,7 +5,8 @@ edition = "2021" license = "MIT" [dependencies] -stwo-prover = { git = "https://github.com/starkware-libs/stwo.git", rev = "92984c060b49d0db05e021883755fac0a71a2fa7" } +stwo = { git = "https://github.com/starkware-libs/stwo.git", rev = "75a6b0ac9bcc7101d8658445dded51923ab2586f", features = ["prover"]} +stwo-constraint-framework = { git = "https://github.com/starkware-libs/stwo.git", rev = "75a6b0ac9bcc7101d8658445dded51923ab2586f", package = "stwo-constraint-framework", features = ["prover"] } num-traits = "0.2.17" itertools = "0.12.0" rand = "0.8.5" \ No newline at end of file diff --git a/stwo-examples/examples/committing_to_the_trace_polynomials.rs b/stwo-examples/examples/committing_to_the_trace_polynomials.rs index 7bb97e1..c970e21 100644 --- a/stwo-examples/examples/committing_to_the_trace_polynomials.rs +++ b/stwo-examples/examples/committing_to_the_trace_polynomials.rs @@ -1,4 +1,12 @@ -use stwo_prover::core::{ +use stwo::core::{ + channel::{Blake2sChannel, Channel}, + fields::m31::M31, + pcs::PcsConfig, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + ColumnVec, +}; +use stwo::prover::{ backend::{ simd::{ column::BaseColumn, @@ -7,15 +15,11 @@ use stwo_prover::core::{ }, Column, }, - channel::{Blake2sChannel, Channel}, - fields::m31::M31, - pcs::{CommitmentSchemeProver, PcsConfig}, poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, + circle::{CircleEvaluation, PolyOps}, BitReversedOrder, }, - vcs::blake2_merkle::Blake2sMerkleChannel, - ColumnVec, + CommitmentSchemeProver, }; // ANCHOR: here_1 diff --git a/stwo-examples/examples/components.rs b/stwo-examples/examples/components.rs index 7a0b863..6a95d24 100644 --- a/stwo-examples/examples/components.rs +++ b/stwo-examples/examples/components.rs @@ -1,27 +1,27 @@ use itertools::chain; use num_traits::{identities::Zero, One}; use rand::Rng; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, EvalAtRow, FrameworkComponent, FrameworkEval, InfoEvaluator, - Relation, RelationEntry, TraceLocationAllocator, - }, - core::{ - air::{Component, ComponentProver}, - backend::simd::{ - column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::SecureField, FieldExpOps}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig, TreeVec}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify, StarkProof}, - vcs::{blake2_merkle::Blake2sMerkleChannel, ops::MerkleHasher}, +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig, TreeVec}, + poly::circle::CanonicCoset, + proof::StarkProof, + vcs::{blake2_merkle::Blake2sMerkleChannel, MerkleHasher}, + verifier::verify, +}; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, - relation, + prove, CommitmentSchemeProver, ComponentProver, +}; +use stwo_constraint_framework::{ + relation, EvalAtRow, FrameworkComponent, FrameworkEval, InfoEvaluator, LogupTraceGenerator, + Relation, RelationEntry, TraceLocationAllocator, }; struct ComponentsProof { @@ -42,7 +42,7 @@ impl Components { statement1: &ComponentsStatement1, ) -> Self { let tree_span_provider = - &mut TraceLocationAllocator::new_with_preproccessed_columns(&vec![]); + &mut TraceLocationAllocator::new_with_preprocessed_columns(&vec![]); let scheduling_component = SchedulingComponent::new( tree_span_provider, @@ -244,7 +244,7 @@ fn gen_scheduling_trace( scheduling_col_1 .as_slice() .iter() - .map(|&v| (v.pow(5) + M31::from(1))), + .map(|&v| M31::from(v.0.pow(5) + 1)), ); // Convert table to trace polynomials @@ -264,11 +264,11 @@ fn gen_computing_trace( let intermediate_values = scheduling_col_1 .as_slice() .iter() - .map(|&v| v.pow(3)) + .map(|&v| v.0.pow(3)) .collect::>(); let intermediate_trace = CircleEvaluation::new( CanonicCoset::new(log_size).circle_domain(), - BaseColumn::from_iter(intermediate_values), + BaseColumn::from_iter(intermediate_values.iter().map(|&v| M31::from(v))), ); vec![ diff --git a/stwo-examples/examples/constraints_over_trace_polynomials.rs b/stwo-examples/examples/constraints_over_trace_polynomials.rs index 2ede0c2..3437956 100644 --- a/stwo-examples/examples/constraints_over_trace_polynomials.rs +++ b/stwo-examples/examples/constraints_over_trace_polynomials.rs @@ -1,25 +1,29 @@ use num_traits::identities::Zero; -use stwo_prover::{ - constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval, TraceLocationAllocator}, - core::{ - backend::{ - simd::{ - column::BaseColumn, - m31::{LOG_N_LANES, N_LANES}, - SimdBackend, - }, - Column, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::QM31}, - pcs::{CommitmentSchemeProver, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, +use stwo::core::{ + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::QM31}, + pcs::PcsConfig, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + ColumnVec, +}; +use stwo::prover::{ + backend::{ + simd::{ + column::BaseColumn, + m31::{LOG_N_LANES, N_LANES}, + SimdBackend, }, - vcs::blake2_merkle::Blake2sMerkleChannel, - ColumnVec, + Column, }, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, + }, + CommitmentSchemeProver, +}; +use stwo_constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, TraceLocationAllocator, }; // ANCHOR: here_1 diff --git a/stwo-examples/examples/dynamic_lookups.rs b/stwo-examples/examples/dynamic_lookups.rs index fe4d655..3fbc2e3 100644 --- a/stwo-examples/examples/dynamic_lookups.rs +++ b/stwo-examples/examples/dynamic_lookups.rs @@ -1,26 +1,26 @@ use num_traits::{identities::Zero, One}; use rand::prelude::SliceRandom; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, EvalAtRow, FrameworkComponent, FrameworkEval, Relation, - RelationEntry, TraceLocationAllocator, - }, - core::{ - air::Component, - backend::simd::{ - column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::SecureField}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, +use stwo::core::verifier::verify; +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, +}; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, - relation, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::relation; +use stwo_constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, LogupTraceGenerator, Relation, RelationEntry, + TraceLocationAllocator, }; // ANCHOR: test_eval diff --git a/stwo-examples/examples/from_spreadsheet_to_trace_polynomials.rs b/stwo-examples/examples/from_spreadsheet_to_trace_polynomials.rs index 38e2a7d..0601fdb 100644 --- a/stwo-examples/examples/from_spreadsheet_to_trace_polynomials.rs +++ b/stwo-examples/examples/from_spreadsheet_to_trace_polynomials.rs @@ -1,4 +1,4 @@ -use stwo_prover::core::{ +use stwo::prover::{ backend::{ simd::{ column::BaseColumn, @@ -7,11 +7,14 @@ use stwo_prover::core::{ }, Column, }, - fields::m31::M31, poly::{ - circle::{CanonicCoset, CircleEvaluation}, + circle::{CircleEvaluation}, BitReversedOrder, }, +}; +use stwo::core::{ + fields::m31::M31, + poly::circle::CanonicCoset, ColumnVec, }; diff --git a/stwo-examples/examples/local_row_constraints.rs b/stwo-examples/examples/local_row_constraints.rs index 3e8794f..5c66d98 100644 --- a/stwo-examples/examples/local_row_constraints.rs +++ b/stwo-examples/examples/local_row_constraints.rs @@ -1,29 +1,30 @@ use num_traits::{identities::Zero, One}; use rand::prelude::SliceRandom; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, preprocessed_columns::PreProcessedColumnId, EvalAtRow, - FrameworkComponent, FrameworkEval, Relation, RelationEntry, TraceLocationAllocator, - ORIGINAL_TRACE_IDX, +use stwo::core::{ + air::Component, + channel::Blake2sChannel, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + utils::bit_reverse_coset_to_circle_domain_order, + vcs::blake2_merkle::Blake2sMerkleChannel, + verifier::verify, +}; +use stwo::prover::{ + backend::{ + simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + Column, }, - core::{ - air::Component, - backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, - Column, - }, - channel::Blake2sChannel, - fields::{m31::M31, qm31::SecureField}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - utils::bit_reverse_coset_to_circle_domain_order, - vcs::blake2_merkle::Blake2sMerkleChannel, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, - relation, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::relation; +use stwo_constraint_framework::{ + preprocessed_columns::PreProcessedColumnId, EvalAtRow, FrameworkComponent, FrameworkEval, + LogupTraceGenerator, Relation, RelationEntry, TraceLocationAllocator, ORIGINAL_TRACE_IDX, }; struct IsFirstColumn { @@ -63,7 +64,7 @@ impl IsFirstColumn { struct TestEval { is_first_id: PreProcessedColumnId, log_size: u32, - lookup_elements: LookupElements, + lookup_elements: ComputationLookupElements, } impl FrameworkEval for TestEval { @@ -107,7 +108,7 @@ impl FrameworkEval for TestEval { const LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR: u32 = 1; -relation!(LookupElements, 1); +relation!(ComputationLookupElements, 1); // ANCHOR: gen_trace fn gen_trace(log_size: u32) -> Vec> { @@ -140,7 +141,7 @@ fn gen_logup_trace( log_size: u32, unsorted_col: &BaseColumn, sorted_col: &BaseColumn, - lookup_elements: &LookupElements, + lookup_elements: &ComputationLookupElements, ) -> ( Vec>, SecureField, @@ -192,7 +193,7 @@ fn main() { tree_builder.commit(channel); // Draw random elements to use when creating the random linear combination of lookup values in the LogUp columns - let lookup_elements = LookupElements::draw(channel); + let lookup_elements = ComputationLookupElements::draw(channel); // Create and commit to the LogUp columns let (logup_cols, claimed_sum) = diff --git a/stwo-examples/examples/local_row_constraints_fails_1.rs b/stwo-examples/examples/local_row_constraints_fails_1.rs index c507135..8e58fb4 100644 --- a/stwo-examples/examples/local_row_constraints_fails_1.rs +++ b/stwo-examples/examples/local_row_constraints_fails_1.rs @@ -1,31 +1,31 @@ use num_traits::{identities::Zero, One}; use rand::prelude::SliceRandom; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, EvalAtRow, FrameworkComponent, FrameworkEval, Relation, - RelationEntry, TraceLocationAllocator, ORIGINAL_TRACE_IDX, - }, - core::{ - air::Component, - backend::simd::{ - column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend, - }, - channel::Blake2sChannel, - fields::{m31::M31, qm31::SecureField}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, +use stwo::core::{ + air::Component, + channel::Blake2sChannel, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + verifier::verify, +}; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, - relation, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::relation; +use stwo_constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, LogupTraceGenerator, Relation, RelationEntry, + TraceLocationAllocator, ORIGINAL_TRACE_IDX, }; struct TestEval { log_size: u32, - lookup_elements: LookupElements, + lookup_elements: ComputationLookupElements, } impl FrameworkEval for TestEval { @@ -69,7 +69,7 @@ impl FrameworkEval for TestEval { const LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR: u32 = 1; -relation!(LookupElements, 1); +relation!(ComputationLookupElements, 1); fn gen_trace(log_size: u32) -> Vec> { // Create a table with random values @@ -93,7 +93,7 @@ fn gen_logup_trace( log_size: u32, unsorted_col: &BaseColumn, sorted_col: &BaseColumn, - lookup_elements: &LookupElements, + lookup_elements: &ComputationLookupElements, ) -> ( Vec>, SecureField, @@ -144,7 +144,7 @@ fn main() { tree_builder.commit(channel); // Draw random elements to use when creating the random linear combination of lookup values in the LogUp columns - let lookup_elements = LookupElements::draw(channel); + let lookup_elements = ComputationLookupElements::draw(channel); // Create and commit to the LogUp columns let (logup_cols, claimed_sum) = diff --git a/stwo-examples/examples/local_row_constraints_fails_2.rs b/stwo-examples/examples/local_row_constraints_fails_2.rs index 2820265..732fde0 100644 --- a/stwo-examples/examples/local_row_constraints_fails_2.rs +++ b/stwo-examples/examples/local_row_constraints_fails_2.rs @@ -1,28 +1,27 @@ use num_traits::{identities::Zero, One}; use rand::prelude::SliceRandom; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, preprocessed_columns::PreProcessedColumnId, EvalAtRow, - FrameworkComponent, FrameworkEval, Relation, RelationEntry, TraceLocationAllocator, - ORIGINAL_TRACE_IDX, - }, - core::{ - air::Component, - backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, - Column, - }, - channel::Blake2sChannel, - fields::{m31::M31, qm31::SecureField}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, +use stwo::core::{ + air::Component, + channel::Blake2sChannel, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + verifier::verify, +}; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + backend::Column, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, - relation, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::relation; +use stwo_constraint_framework::{ + preprocessed_columns::PreProcessedColumnId, EvalAtRow, FrameworkComponent, FrameworkEval, + LogupTraceGenerator, Relation, RelationEntry, TraceLocationAllocator, ORIGINAL_TRACE_IDX, }; // ANCHOR: is_first_column diff --git a/stwo-examples/examples/preprocessed_trace.rs b/stwo-examples/examples/preprocessed_trace.rs index f5b0916..a98583c 100644 --- a/stwo-examples/examples/preprocessed_trace.rs +++ b/stwo-examples/examples/preprocessed_trace.rs @@ -1,25 +1,25 @@ use num_traits::identities::Zero; -use stwo_prover::{ - constraint_framework::{ - preprocessed_columns::PreProcessedColumnId, EvalAtRow, FrameworkComponent, FrameworkEval, - TraceLocationAllocator, - }, - core::{ - air::Component, - backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES, SimdBackend}, - Column, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::QM31}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, +use stwo::core::verifier::verify; +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::QM31}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, +}; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, SimdBackend}, + backend::Column, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, }, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::{ + preprocessed_columns::PreProcessedColumnId, EvalAtRow, FrameworkComponent, FrameworkEval, + TraceLocationAllocator, }; // ANCHOR: is_first_column @@ -72,9 +72,9 @@ impl FrameworkEval for TestEval { // If is_first is 1, then the constraint is col_1 * col_2 - col_3 = 0 // If is_first is 0, then the constraint is col_1 * col_2 + col_1 - col_3 = 0 eval.add_constraint( - (col_1.clone() * col_2.clone() - col_3.clone()) * is_first.clone() - + (col_1.clone() * col_2.clone() + col_1.clone() - col_3.clone()) - * (E::F::from(M31::from(1)) - is_first.clone()), + is_first.clone() * (col_1.clone() * col_2.clone() - col_3.clone()) + + (E::F::from(M31::from(1)) - is_first.clone()) + * (col_1.clone() * col_2.clone() + col_1.clone() - col_3.clone()), ); eval diff --git a/stwo-examples/examples/proving_an_air.rs b/stwo-examples/examples/proving_an_air.rs index 700e319..c6bb542 100644 --- a/stwo-examples/examples/proving_an_air.rs +++ b/stwo-examples/examples/proving_an_air.rs @@ -1,27 +1,31 @@ use num_traits::identities::Zero; -use stwo_prover::{ - constraint_framework::{EvalAtRow, FrameworkComponent, FrameworkEval, TraceLocationAllocator}, - core::{ - air::Component, - backend::{ - simd::{ - column::BaseColumn, - m31::{LOG_N_LANES, N_LANES}, - SimdBackend, - }, - Column, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::QM31}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::QM31}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + verifier::verify, + ColumnVec, +}; +use stwo::prover::{ + backend::{ + simd::{ + column::BaseColumn, + m31::{LOG_N_LANES, N_LANES}, + SimdBackend, }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, - ColumnVec, + Column, }, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, + }, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::{ + EvalAtRow, FrameworkComponent, FrameworkEval, TraceLocationAllocator, }; struct TestEval { diff --git a/stwo-examples/examples/public_input.rs b/stwo-examples/examples/public_input.rs new file mode 100644 index 0000000..7b748a2 --- /dev/null +++ b/stwo-examples/examples/public_input.rs @@ -0,0 +1,245 @@ +use num_traits::One; +use num_traits::Zero; +use stwo::core::fields::FieldExpOps; +use stwo::core::verifier::verify; +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::circle::CanonicCoset, + vcs::blake2_merkle::Blake2sMerkleChannel, + ColumnVec, +}; +use stwo::prover::{ + backend::simd::{ + column::BaseColumn, + m31::{PackedM31, LOG_N_LANES}, + qm31::PackedSecureField, + SimdBackend, + }, + backend::Column, + poly::{ + circle::{CircleEvaluation, PolyOps}, + BitReversedOrder, + }, + prove, CommitmentSchemeProver, +}; +use stwo_constraint_framework::{ + relation, EvalAtRow, FrameworkComponent, FrameworkEval, LogupTraceGenerator, Relation, + RelationEntry, TraceLocationAllocator, +}; + +struct PublicDataClaim { + public_input: Vec>, + public_output: Vec, +} + +impl PublicDataClaim { + pub fn mix_into(&self, channel: &mut impl Channel) { + for input in self.public_input.iter().flatten() { + for v in input.to_array().iter() { + channel.mix_u64(v.0 as u64); + } + } + for output in self.public_output.iter() { + for v in output.to_array().iter() { + channel.mix_u64(v.0 as u64); + } + } + } +} + +relation!(PublicInputElements, 3); + +struct TestEval { + log_size: u32, + lookup_elements: PublicInputElements, +} + +impl FrameworkEval for TestEval { + fn log_size(&self) -> u32 { + self.log_size + } + + fn max_constraint_log_degree_bound(&self) -> u32 { + self.log_size + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + } + + fn evaluate(&self, mut eval: E) -> E { + // 10 columns: c0..c9, each row encodes a Fibonacci sequence across columns + let c0 = eval.next_trace_mask(); + let c1 = eval.next_trace_mask(); + let c2 = eval.next_trace_mask(); + let c3 = eval.next_trace_mask(); + let c4 = eval.next_trace_mask(); + let c5 = eval.next_trace_mask(); + let c6 = eval.next_trace_mask(); + let c7 = eval.next_trace_mask(); + let c8 = eval.next_trace_mask(); + let c9 = eval.next_trace_mask(); + + // Enforce Fibonacci relation: c_{i} = c_{i-1} + c_{i-2} + eval.add_constraint(c0.clone() + c1.clone() - c2.clone()); + eval.add_constraint(c1.clone() + c2.clone() - c3.clone()); + eval.add_constraint(c2.clone() + c3.clone() - c4.clone()); + eval.add_constraint(c3.clone() + c4.clone() - c5.clone()); + eval.add_constraint(c4.clone() + c5.clone() - c6.clone()); + eval.add_constraint(c5.clone() + c6.clone() - c7.clone()); + eval.add_constraint(c6.clone() + c7.clone() - c8.clone()); + eval.add_constraint(c7.clone() + c8.clone() - c9.clone()); + + // LogUp relation: -1/(c0 + alpha * c1 + alpha^2 * c9 - Z) + eval.add_to_relation(RelationEntry::new( + &self.lookup_elements, + -E::EF::one(), + &[c0.clone(), c1.clone(), c9.clone()], + )); + eval.finalize_logup(); + + eval + } +} + +const LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR: u32 = 1; + +fn main() { + // 16 rows, 10 columns + let num_rows: usize = 16; + let log_num_rows: u32 = 4; // log2(16) + + // Create the table + const NUM_COLS: usize = 10; + let mut cols: Vec = (0..NUM_COLS).map(|_| BaseColumn::zeros(num_rows)).collect(); + + // Seeds per row: (1, 1), (1, 2), (1, 3), ... up to 16 rows + for r in 0..num_rows { + cols[0].set(r, M31::from(1u32)); + cols[1].set(r, M31::from((r as u32) + 1)); + for c in 2..NUM_COLS { + let a = cols[c - 2].at(r); + let b = cols[c - 1].at(r); + cols[c].set(r, a + b); + } + } + + let public_input = [cols[0].clone(), cols[1].clone()] + .into_iter() + .map(|col| col.data) + .collect(); + let public_output = cols[9].clone().data; + + // Convert table to trace polynomials + let domain = CanonicCoset::new(log_num_rows).circle_domain(); + let trace: ColumnVec> = cols + .into_iter() + .map(|col| CircleEvaluation::new(domain, col)) + .collect(); + + // Config for FRI and PoW + let config = PcsConfig::default(); + + // Precompute twiddles for evaluating and interpolating the trace + let twiddles = SimdBackend::precompute_twiddles( + CanonicCoset::new( + log_num_rows + LOG_CONSTRAINT_EVAL_BLOWUP_FACTOR + config.fri_config.log_blowup_factor, + ) + .circle_domain() + .half_coset, + ); + + // Create the channel and commitment scheme + let channel = &mut Blake2sChannel::default(); + let mut commitment_scheme = + CommitmentSchemeProver::::new(config, &twiddles); + + // Commit to the preprocessed trace + let mut tree_builder = commitment_scheme.tree_builder(); + tree_builder.extend_evals(vec![]); + tree_builder.commit(channel); + + // Commit to the size of the trace + channel.mix_u64(log_num_rows as u64); + + // Commit to the public input + let public_data_claim = PublicDataClaim { + public_input, + public_output, + }; + public_data_claim.mix_into(channel); + + // Commit to the original trace + let mut tree_builder = commitment_scheme.tree_builder(); + tree_builder.extend_evals(trace.clone()); + tree_builder.commit(channel); + + // Draw random elements for LogUp + let lookup_elements = PublicInputElements::draw(channel); + + // Build LogUp column: + // -1/(c0 + alpha * c1 + alpha^2 * c9 - Z) + let mut logup_gen = LogupTraceGenerator::new(log_num_rows); + + let mut col_gen = logup_gen.new_col(); + for simd_row in 0..(1 << (log_num_rows - LOG_N_LANES)) { + let denom: PackedSecureField = lookup_elements.combine(&[ + trace[0].data[simd_row], + trace[1].data[simd_row], + trace[9].data[simd_row], + ]); + col_gen.write_frac(simd_row, -PackedSecureField::one(), denom); + } + col_gen.finalize_col(); + + let (logup_cols, mut claimed_sum) = logup_gen.finalize_last(); + + // Commit to the LogUp columns + let mut tree_builder = commitment_scheme.tree_builder(); + tree_builder.extend_evals(logup_cols); + tree_builder.commit(channel); + + // Create a component + let component = FrameworkComponent::::new( + &mut TraceLocationAllocator::default(), + TestEval { + log_size: log_num_rows, + lookup_elements: lookup_elements.clone(), + }, + claimed_sum, + ); + + // Prove + let proof = prove(&[&component], channel, commitment_scheme).unwrap(); + + // Verify + + // Add the public values to the claimed sum + let mut public_values = vec![PackedSecureField::zero(); 1 << (log_num_rows - LOG_N_LANES)]; + for simd_row in 0..(1 << (log_num_rows - LOG_N_LANES)) { + let denom: PackedSecureField = lookup_elements.combine(&[ + trace[0].data[simd_row], + trace[1].data[simd_row], + trace[9].data[simd_row], + ]); + public_values[simd_row] = denom; + } + let public_values = PackedSecureField::batch_inverse(&public_values); + for value in public_values.iter() { + for v in value.to_array().iter() { + claimed_sum += *v; + } + } + assert_eq!(claimed_sum, SecureField::zero()); + + let channel = &mut Blake2sChannel::default(); + let commitment_scheme = &mut CommitmentSchemeVerifier::::new(config); + let sizes = component.trace_log_degree_bounds(); + + commitment_scheme.commit(proof.commitments[0], &sizes[0], channel); + channel.mix_u64(log_num_rows as u64); + public_data_claim.mix_into(channel); + commitment_scheme.commit(proof.commitments[1], &sizes[1], channel); + commitment_scheme.commit(proof.commitments[2], &sizes[2], channel); + + verify(&[&component], channel, commitment_scheme, proof).unwrap(); +} diff --git a/stwo-examples/examples/static_lookups.rs b/stwo-examples/examples/static_lookups.rs index 18cad34..9cd1fc7 100644 --- a/stwo-examples/examples/static_lookups.rs +++ b/stwo-examples/examples/static_lookups.rs @@ -1,27 +1,23 @@ use num_traits::{identities::Zero, One}; use rand::Rng; -use stwo_prover::{ - constraint_framework::{ - logup::LogupTraceGenerator, preprocessed_columns::PreProcessedColumnId, EvalAtRow, - FrameworkComponent, FrameworkEval, Relation, RelationEntry, TraceLocationAllocator, - }, - core::{ - air::Component, - backend::{ - simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, - Column, - }, - channel::{Blake2sChannel, Channel}, - fields::{m31::M31, qm31::SecureField}, - pcs::{CommitmentSchemeProver, CommitmentSchemeVerifier, PcsConfig}, - poly::{ - circle::{CanonicCoset, CircleEvaluation, PolyOps}, - BitReversedOrder, - }, - prover::{prove, verify}, - vcs::blake2_merkle::Blake2sMerkleChannel, - }, - relation, +use stwo_constraint_framework::{ + LogupTraceGenerator, preprocessed_columns::PreProcessedColumnId, EvalAtRow, + FrameworkComponent, FrameworkEval, Relation, RelationEntry, TraceLocationAllocator, relation, +}; +use stwo::core::{ + air::Component, + channel::{Blake2sChannel, Channel}, + fields::{m31::M31, qm31::SecureField}, + pcs::{CommitmentSchemeVerifier, PcsConfig}, + poly::{ circle::CanonicCoset }, + vcs::blake2_merkle::Blake2sMerkleChannel, +}; +use stwo::core::verifier::verify; +use stwo::prover::{ + backend::simd::{column::BaseColumn, m31::LOG_N_LANES, qm31::PackedSecureField, SimdBackend}, + backend::Column, + poly::{ circle::{CircleEvaluation, PolyOps}, BitReversedOrder }, + CommitmentSchemeProver, prove, }; // ANCHOR: range_check_column diff --git a/stwo-examples/examples/writing_a_spreadsheet.rs b/stwo-examples/examples/writing_a_spreadsheet.rs index 5348671..0386b77 100644 --- a/stwo-examples/examples/writing_a_spreadsheet.rs +++ b/stwo-examples/examples/writing_a_spreadsheet.rs @@ -1,10 +1,10 @@ -use stwo_prover::core::{ +use stwo::prover::{ backend::{ simd::{column::BaseColumn, m31::N_LANES}, Column, }, - fields::m31::M31, }; +use stwo::core::fields::m31::M31; fn main() { let num_rows = N_LANES; diff --git a/stwo-examples/rust-toolchain.toml b/stwo-examples/rust-toolchain.toml index 85a8901..9de2d5e 100644 --- a/stwo-examples/rust-toolchain.toml +++ b/stwo-examples/rust-toolchain.toml @@ -1,3 +1,3 @@ [toolchain] -channel = "nightly-2025-01-02" +channel = "nightly-2025-07-14" components = ["rustfmt", "clippy"] \ No newline at end of file