## Constraint Framework Documentation
This document provides an overview and guide for the Rust-based Constraint Framework, designed for building Arithmetic Intermediate Representations (AIRs) used in STARK-like Zero-Knowledge Proof systems.
### 1. Overview
**Purpose:**
The Constraint Framework enables developers to define and prove computational statements efficiently. It provides tools to express algebraic constraints over finite fields and then generate and verify proofs of computational integrity based on these constraints, leveraging a FRI-based Polynomial Commitment Scheme (PCS).
**Main Features:**
* **Formal Constraint Definition:** Allows symbolic representation of constraints using `BaseExpr` (for base field operations) and `ExtExpr` (for extension field operations).
* **Multiple Evaluation Backends:** Constraints can be evaluated in different contexts:
* **Symbolic Analysis:** (`ExprEvaluator`) For inspecting constraint structure and degree.
* **Concrete Testing:** (`AssertEvaluator`) For verifying constraints against actual trace data.
* **Proof Generation (SIMD/CPU):** (`SimdDomainEvaluator`, `CpuDomainEvaluator`) For efficiently computing the composition polynomial.
* **Verification (OODS):** (`PointEvaluator`) For out-of-domain sampling checks.
* **Polynomial Commitment Scheme:** Implements a FRI-based PCS using Merkle trees for committing to trace and composition polynomials.
* **Component-Based Architecture:** Encourages modular design by defining AIRs as collections of components, each with its own set of constraints.
**Tech Stack:**
* **Language:** Rust
* **Key Libraries/Concepts:**
* Standard Rust collections.
* SIMD for performance-critical operations (optional, feature-gated).
* Custom finite field arithmetic (`M31`, `CM31`, `QM31`).
* Merkle trees for commitments.
* FRI protocol for low-degree testing.
**Example Use Case:**
Proving the correct execution of a Blake2s hash function, where each round or sub-operation (like XOR) is a component with its own constraints.
### 2. Architecture
The framework revolves around defining computational integrity through algebraic constraints, then proving these constraints hold using a STARK-like protocol.
**Global Mechanism:**
1. **Component Definition:** Developers implement the `FrameworkEval` trait for each logical part of their computation (a "component"). Inside the `evaluate` method, they use an `EvalAtRow` trait object to define constraints symbolically using `BaseExpr` and `ExtExpr`. These expressions refer to trace columns (via `next_trace_mask`) and public parameters.
2. **Trace Generation:** The prover generates the execution trace (witness data) for the specific computation instance. This trace is organized into columns.
3. **Commitment Phase:**
* The `CommitmentSchemeProver` is used to commit to different sets of polynomials (trace, interaction, composition).
* Polynomials are LDE'd (Low-Degree Extended) and their evaluations form the leaves of Merkle trees. The Merkle roots are the commitments.
* The `TreeVec` and `ColumnVec` types help organize data related to these multiple tree commitments.
4. **Constraint Composition:**
* A random challenge `alpha` is drawn from the channel.
* All constraints from all components `C_i(X)` are combined into a single composition polynomial `CP(X) = sum (alpha_pow_i * C_i(X)) / Z_H(X)`, where `Z_H(X)` is the vanishing polynomial of the trace domain.
* This is done by the `DomainEvaluator`s (SIMD/CPU) which interpret the formal `BaseExpr`/`ExtExpr` with actual LDE'd trace values and the powers of `alpha`.
5. **FRI Protocol:**
* The `CommitmentSchemeProver` commits to `CP(X)`.
* Out-of-domain sampling (OODS) is performed: trace polynomials and `CP(X)` are evaluated at a random point `z` (a `SecureField` element).
* FRI is run on quotients derived from these OODS evaluations to prove `CP(X)` is indeed low-degree (meaning all original constraints were satisfied).
6. **Proof Generation:** The STARK proof consists of Merkle roots, OODS values, FRI layer commitments, and Merkle decommitments for queried values.
7. **Verification:** The verifier performs the analogous steps, using the proof to reconstruct challenges and verify the FRI layers and Merkle decommitments.
**High-Level Data Flow (Proving):**
`Computation Instance` -> `Trace Generation` -> `Vec<CirclePoly>` -> `CommitmentSchemeProver::commit()` (mixes root to channel) -> `ExprEvaluator (for Component logic)` -> `DomainEvaluator` (for `CP(X)`) -> `FRI Prover` -> `StarkProof`.
### 3. Key Components
1. **`FrameworkEval` Trait** (`prover/src/constraint_framework/component.rs`)
* **Role:** Defines the core logic for a component's constraints.
* **Key Function:** `evaluate<E: EvalAtRow>(&self, eval: E) -> E;`
* **Usage:** Users implement this to describe their AIR constraints symbolically.
```rust
// Simplified Example
use stwo_prover::constraint_framework::{FrameworkEval, EvalAtRow};
struct MyComponentEval { log_n_rows: u32 }
impl FrameworkEval for MyComponentEval {
fn log_size(&self) -> u32 { self.log_n_rows }
fn max_constraint_log_degree_bound(&self) -> u32 { self.log_n_rows + 1 }
fn evaluate<E: EvalAtRow>(&self, mut eval: E) -> E {
let col_a = eval.next_trace_mask(); // Formal placeholder
let col_b = eval.next_trace_mask();
let col_c = eval.next_trace_mask();
eval.add_constraint(col_a + col_b - col_c); // Defines a + b = c
eval
}
}
```
2. **`BaseExpr` & `ExtExpr`** (`prover/src/constraint_framework/expr/mod.rs`)
* **Role:** Represent formal algebraic expressions over base and extension fields respectively.
* **Key Functions:** Enum variants like `Col`, `Const`, `Param`, `Add`, `Mul`, `Inv`.
* **Usage:** Used within `FrameworkEval::evaluate` to build constraint equations.
```rust
use stwo_prover::constraint_framework::expr::{BaseExpr, ColumnExpr};
use stwo_prover::core::fields::m31::M31;
// let expr = BaseExpr::Col(ColumnExpr::from((1,0,0))) + BaseExpr::Const(M31::from(5));
```
3. **`EvalAtRow` Trait & Implementors** (`prover/src/constraint_framework/mod.rs`, `evaluator.rs`, `assert.rs`, etc.)
* **Role:** Provides the interface for components to declare their trace accesses and constraints. Different implementors give different meanings to these declarations.
* **Key Functions:** `next_trace_mask()`, `add_constraint()`, `add_to_relation()`.
* **Implementors:**
* `ExprEvaluator`: Builds up the symbolic `BaseExpr`/`ExtExpr` trees.
* `AssertEvaluator`: Evaluates expressions with concrete trace data for testing.
* `SimdDomainEvaluator`/`CpuDomainEvaluator`: Evaluates expressions over domains during proof generation.
* `PointEvaluator`: Evaluates expressions at OODS points during verification.
* `InfoEvaluator`: Collects metadata about constraints (offsets, counts).
* **Usage:** An `EvalAtRow` instance is passed to a component's `evaluate` method.
4. **`CommitmentSchemeProver`/`CommitmentSchemeVerifier`** (`prover/src/core/pcs/prover.rs`, `verifier.rs`)
* **Role:** Manages the Polynomial Commitment Scheme (PCS) based on FRI and Merkle trees.
* **Key Functions:**
* Prover: `new()`, `tree_builder()`, `commit()`, `prove_values()`.
* Verifier: `new()`, `commit()` (to receive roots), `verify_values()`.
* **Usage:**
```rust
// Prover side (simplified)
// let mut cs_prover = CommitmentSchemeProver::new(pcs_config, &twiddles);
// let mut tree_builder = cs_prover.tree_builder();
// tree_builder.extend_evals(trace_evaluations);
// tree_builder.commit(&mut channel);
// let proof = cs_prover.prove_values(oods_points, &mut channel);
```
5. **`TreeVec<T>` & `ColumnVec<T>`** (`prover/src/core/pcs/utils.rs`, `prover/src/core/mod.rs`)
* **Role:** Semantic wrappers around `Vec<T>` to organize data. `TreeVec`'s elements correspond to distinct Merkle tree commitments. `ColumnVec`'s elements correspond to logical columns within a tree or trace.
* **Usage:**
```rust
// use stwo_prover::core::pcs::TreeVec;
// use stwo_prover::core::ColumnVec;
// use stwo_prover::core::poly::circle::CirclePoly;
// use stwo_prover::core::backend::simd::SimdBackend;
// let polynomials_per_tree: TreeVec<ColumnVec<CirclePoly<SimdBackend>>> = TreeVec::default();
```
### 4. How-To Guides
**Setting up the development environment:**
1. Install Rust: `rustup update stable`
2. Clone the repository: `git clone [repository_url] stwo`
3. Navigate to the project: `cd stwo/crates/prover`
4. Build the project: `cargo build` (for debug) or `cargo build --release`
**Running an example (e.g., Blake2s):**
(Assuming examples are runnable via `cargo run --example`)
1. Navigate to the prover crate: `cd stwo/crates/prover`
2. Run the Blake2s example:
```bash
# Set desired log level for n_instances, e.g., 2^10 instances
# Add RUST_LOG_SPAN_EVENTS=enter,close RUST_LOG=info for detailed tracing
LOG_N_INSTANCES=10 cargo run --release --example blake2s_air --features parallel,simd-avx512 # or other SIMD features
```
(Note: The exact example name `blake2s_air` is an assumption, refer to `examples/` dir).
**Running tests:**
1. Run unit and integration tests:
```bash
cargo test
```
2. To run tests with specific features (e.g., performance-related SIMD tests):
```bash
cargo test --features simd-avx512
```
3. To run slow tests (often integration or larger proof tests):
```bash
cargo test --features slow-tests
```
4. To see detailed test output (including `println!` or `dbg!`):
```bash
cargo test -- --nocapture
```
**Deploying the application:**
This framework is a library, meant to be included in other Rust projects.
1. To use it as a dependency, add it to your `Cargo.toml`:
```toml
[dependencies]
stwo_prover = { path = "../path/to/stwo/crates/prover" } # Or from crates.io if published
```
2. Build your main application that uses this prover library: `cargo build --release`.
### 5. Troubleshooting
1. **Issue: `ProvingError::ConstraintsNotSatisfied` or Assertion Failure in `AssertEvaluator`**
* **Symptom:** The prover fails with an error indicating constraints are not met, or a test using `AssertEvaluator` panics.
* **Cause:**
* The algebraic relations defined in a component's `evaluate()` method are incorrect.
* The trace generation logic (`gen_trace` functions in examples) produces witness data inconsistent with the constraints.
* Off-by-one errors in loops or offsets.
* **Solution:**
* Carefully review the constraint math for the failing component.
* Use `dbg!` or `println!` in your `evaluate()` method (when using `AssertEvaluator`) to inspect intermediate values.
* Write smaller unit tests for individual constraints or parts of the trace generation.
* Examine the failing row in `AssertEvaluator` to pinpoint the exact point of failure.
2. **Issue: `VerificationError::OodsNotMatching` or `FriVerificationError`**
* **Symptom:** The proof is generated, but verification fails, often related to OODS checks or FRI.
* **Cause:**
* **Incorrect `max_constraint_log_degree_bound`:** The bound returned by a component's `FrameworkEval` implementation is lower than the actual degree of the constraints after they are combined and divided by the vanishing polynomial. This leads to FRI proving a polynomial is lower-degree than it actually is.
* **Mismatch in `log_size`:** A component's `log_size` doesn't match the actual size of its trace columns.
* **FRI Configuration:** Mismatch in `FriConfig` between prover and verifier, or parameters that are too aggressive for the actual polynomial degrees.
* Bugs in how the composition polynomial is constructed or how quotients are formed.
* **Solution:**
* Use `InfoEvaluator` or `ExprEvaluator::constraint_degree_bounds()` to accurately determine the degree of your constraints. Ensure `max_constraint_log_degree_bound` is sufficient.
* Double-check all `log_size` parameters.
* Verify that the OODS evaluation of the composition polynomial matches the combination of OODS evaluations of trace polynomials. The `prove` function in `core/prover/mod.rs` has a sanity check for this.
* Temporarily use less aggressive FRI parameters (e.g., larger `log_last_layer_degree_bound`, smaller blowup factor) to see if the issue is related to FRI itself.
3. **Issue: Slow Proving Times**
* **Symptom:** Proof generation takes an unexpectedly long time.
* **Cause:**
* Inefficient constraint definitions (e.g., unnecessarily high-degree expressions).
* Suboptimal use of SIMD features or parallelism (or not enabled).
* Large trace sizes or high number of constraints.
* **Solution:**
* **Profiling:** Use `tracing` with `RUST_LOG_SPAN_EVENTS=enter,close RUST_LOG=info` and tools like `flamegraph` or `samply` to identify bottlenecks.
* **Optimize Constraints:** Review constraints for potential simplifications.
* **SIMD:** Ensure the `simd-avx512` (or other relevant SIMD features like `neon`) and `parallel` features are enabled in `Cargo.toml` or via build flags for release builds: `RUSTFLAGS="-C target-cpu=native -C target-feature=+avx512f" cargo build --release --features simd-avx512,parallel`.
* **Algorithm Choice:** For very large computations, the inherent complexity will lead to long proving times. Consider if the AIR itself can be optimized or if parts of the computation can be broken down.
Sign in with Wallet
Connect another wallet