repository·main·Indexed 21 days ago
https://github.com/facebook/winterfellA high-performance STARK prover and verifier for arbitrary computations. It supports multi-threading, customizable cryptography, and WebAssembly targets. The library includes the winter-air crate for defining computations via the Air trait (Algebraic Intermediate Representation) and the winter-crypto crate providing hash functions (SHA3, BLAKE3, Rescue Prime), Merkle trees with batch proof support, and no_std compatibility.
Winterfell is a STARK (Scalable Transparent Argument of Knowledge) prover and verifier designed for arbitrary computations. It allows for the creation of efficiently verifiable proofs that a specific computation was executed correctly without requiring a trusted setup.
Warning: This is a research project. It has not been audited and may contain bugs or security flaws. It is NOT intended for production use.
winterfell crate serves as a top-level entry point that re-exports the core components of the Winterfell STARK system. Instead of importing individual sub-crates, you can use winterfell to access the functionality defined in the prover and verifier crates.The winter-rand-utils crate provides functions for generating random values. These utilities are specifically designed for use in tests, benchmarks, and examples within the Winterfell ecosystem.
Important Note on WebAssembly (Wasm): All functions in this crate are omitted when compiling to a WebAssembly target. If your project targets Wasm, you cannot use these utilities.
An execution trace is a 2D matrix where rows are time steps and columns are algebraic registers. While you can implement the Trace trait on any custom struct, Winterfell provides the TraceTable struct for convenience.
Use TraceTable::init() by passing a set of vectors, where each vector represents a column.
Requirements:
Use TraceTable::new(width, length) to allocate memory, then use the fill() method. fill() takes two closures:
This approach is simpler and facilitates concurrent trace generation.
// Example concept for TraceTable initialization
let mut trace = TraceTable::new(width, length);
trace.fill(
|| { /* initialize first row */ },
|prev_state| { /* compute next state from prev_state */ }
);The core logic for each example is located in its air.rs file. These files define the computation using the Algebraic Intermediate Representation (AIR) framework. An AIR implementation typically consists of two main components:
build_trace() function: Responsible for generating the execution trace for the specific computation.Air trait implementation: Describes the algebraic constraints that define the computation.Understanding these two components is key to implementing custom computations in Winterfell.
When the concurrent feature is enabled, the crate uses the rayon crate to perform parallel execution for certain functions, specifically transpose_slice().
To control the level of parallelism, you can set the RAYON_NUM_THREADS environment variable. If not set, it defaults to the number of logical cores available on the machine.
# Example: Running with a specific number of threads
RAYON_NUM_THREADS=4 cargo runThe src/field module provides arithmetic operations in STARK-friendly finite fields. Supported operations include basic arithmetic (addition, multiplication, subtraction, division, inversion), drawing random/pseudo-random elements, and computing roots of unity.
| Field | Modulus | Security Notes |
|---|---|---|
f128 | $2^{128} - 45 imes 2^{40} + 1$ | Sub-optimal performance. Provides ~100 bits of security. For higher security, use a quadratic extension. |
f62 | $2^{62} - 111 imes 2^{39} + 1$ | Fast modular arithmetic (branchless). Provides ~100 bits of security. Use quadratic extensions for higher security, or cubic extensions for even higher levels. |
f64 | $2^{64} - 2^{32} + 1$ | Fast, constant-time implementation. Provides ~100 bits of security. Use quadratic extensions for higher security, or cubic extensions for even higher levels. |
Assertions specify that certain cells in an execution trace must contain specific values. In Winterfell, these are internally converted into boundary constraints. Every computation must implement get_assertions() and provide at least one assertion.
There are three types of assertions:
To achieve security levels higher than ~100 bits, you can use quadratic or cubic extensions of the base fields. The library provides a generic way to create these by implementing the ExtensibleField trait for degrees 2 and 3.
Quadratic Extensions ($x^2$):
f62: $x^2 - x - 1$f64: $x^2 - x + 2$f128: $x^2 - x - 1$Cubic Extensions ($x^3$):
f62: $x^3 + 2x + 2$f64: $x^3 - x - 1$f128: Not supportedThe src/fft module implements the Number-theoretic transform (FFT) in a prime field.
Use this to perform polynomial interpolation and evaluation in $O(n ext{ log } n)$ time. This is applicable as long as the domain of the polynomial is a multiplicative subgroup with a size that is a power of 2.
Winterfell's performance is influenced by the computation's nature, AIR encoding efficiency, proof generation parameters, and hardware. Key performance metrics include:
Users can dynamically trade off proof size, security level, and proving time based on their requirements.
The src/polynom module provides core polynomial functionality: