Out-of-core STARK proving. Prove a STARK whose execution trace is far larger than RAM, in a fixed small memory budget, by streaming the transforms, commitment, and FRI through fast storage.
A research artifact: a complete out-of-core DEEP-FRI STARK prover over a generic AIR. The soundness model and the scope limits are spelled out below.
A companion experiment (zk-spool) showed that a transparent allocator can only lower a prover's RAM to its hot working set — about 3 GB for a mid-size plonky2 proof — because the prover key and the active FFT/NTT buffers stay hot and cannot be spilled. The natural question: is that floor fundamental, or just an artifact of computing the NTT in core?
It's an artifact. The NTT is the dominant hot buffer, and it does not have to be in core.
The four-step (Bailey) algorithm factors a size-N = n1·n2 transform into small
transforms over the rows and columns of an n1 × n2 matrix. Each touches only
one row or column, so the working set is O(√N), not O(N). Lay the matrix on
storage, stream tiles through a fixed budget, and the transform's footprint
becomes independent of its size.
flowchart LR
subgraph DISK["NVMe — data far larger than RAM (GBs)"]
T["trace / polynomial<br/>laid out as an n₁ × n₂ matrix"]
end
subgraph BUDGET["fixed RAM budget (≤ 256 MB)"]
W["one tile<br/>O(√N) working set"]
end
T ==>|stream a row or column tile| W
W ==>|transformed tile written back| T
Measured, on Goldilocks, against the in-core NTT (bit-for-bit identical output — verified by unit tests up to 2^16 and a position-weighted checksum at scale):
| Transform | in-core peak RSS | out-of-core peak RSS | in-core time | out-of-core time |
|---|---|---|---|---|
| 2^26 (512 MB) | 1026 MB | 38 MB | 2.3 s | 7.4 s |
Under an enforced 256 MB memory cgroup (swap off):
| Run | Result |
|---|---|
| in-core 2^26 (512 MB) | OOM-killed |
| out-of-core 2^26 (512 MB) | survives — 38 MB RSS, identical checksum |
| out-of-core 2^28 (2 GB) | survives — 40 MB RSS |
A 2 GB transform computed in 40 MB of RAM — 8× larger than the memory limit,
~50× smaller than the data. The resident set is flat at ~40 MB whether the
transform is 512 MB or 2 GB: the footprint is set by the tile size (block), not
by N. The hot-set floor is breakable — algorithmically.
The first prover step built on the NTT is the low-degree extension — evaluate
a trace polynomial over a larger coset domain — which is a STARK prover's largest
memory consumer (the extended trace is the blow-up factor times the trace). A
coset FFT is just the FFT of the coefficients pre-scaled by shift^i, so it
composes directly with the out-of-core NTT. lde_ooc_streamed is verified
bit-for-bit against plonky2's coset_fft.
Measured: a 2^25 (256 MB) polynomial extended to 2^28 (2 GB) of coset evaluations — an 8× blow-up — under an enforced 256 MB cgroup, in 34 MB RSS. The biggest buffer in the commit phase, materialized out of core.
The other half of the commit phase is the Merkle commitment over those
evaluations. merkle_root_ooc builds the tree level by level on storage with
plonky2's Poseidon, holding only a chunk of one level in RAM — verified
bit-for-bit against an in-core build. Measured: a 2^26 (512 MB) commitment
under a 256 MB cgroup, in 6 MB RSS.
So the whole commit phase — the prover's dominant memory consumer — extend then commit, runs out of core in a tiny, size-independent budget. Each piece is verified against an in-core reference.
The commit phase's primitives compose into the prover's opening phase. FRI, a STARK's low-degree test, is built end to end here:
- Fold (
fri_fold_ooc) — one round halves a polynomial's evaluations using a challenge; the access pattern is two contiguous streams half a domain apart, so it folds in a few tiles. Verified algebraically (the fold of the evaluations equals the evaluations of the folded polynomial). - Commit with paths (
MerkleOoc) — keeps every tree level on storage so a leaf's authentication path opens without the tree in RAM. prove_fri/verify_fri— the prover commits each layer, folds with Fiat-Shamir challenges, sends the tiny final polynomial, and answers random queries with Merkle paths — all streaming. The (in-core, microsecond) verifier replays the transcript, checks each query's paths and fold consistency, and enforces the final-polynomial degree bound, which is the actual low-degree certificate.
Verified: a valid low-degree instance is accepted; a high-degree input is rejected; a forged opening is rejected. This is the first end-to-end verifiable proof in zk-stream — the heart of STARK proving, out of core.
The pieces above compose into a pipeline that never holds the polynomial in RAM
at any stage. ntt_ooc_to_file runs the out-of-core NTT and leaves its result
on disk (instead of reducing it to a checksum), and prove_fri_from_file seeds
the prover straight from that file — so the evaluations are streamed from
generation through commit, fold, and opening, never materialized.
Three engineering details make it run at scale, not just in principle:
- Chunked commit. The Merkle commit reads each layer's evaluation file a
chunk at a time (
commit_from_file), onepreadper chunk, rather than one syscall per leaf. - Parallel hashing. Leaf hashing and level reduction are independent per node, so they fan across the cores (a 2^24 self-proof: 65.7 s → 11.2 s on 16).
- Bounded dirty page-cache. A streaming write far larger than RAM piles up dirty pages that a tight memory cgroup counts and — with swap off — cannot reclaim until written, so it OOMs even with a flat heap. Flushing and evicting every ~64 MiB keeps the resident page-cache bounded, so the cgroup footprint stays flat in the transform's size, just as the heap does.
Measured, under an enforced 256 MB memory cgroup, swap off — a full FRI low-degree proof, generated and verified, of a polynomial far larger than the limit:
| Instance | in-core NTT (control) | end-to-end out-of-core FRI |
|---|---|---|
| 2^26 (512 MB poly, 2× limit) | OOM-killed | verified — 34 MB RSS |
| 2^27 (1 GB poly, 4× limit) | OOM-killed | verified — 34 MB RSS |
| 2^28 (2 GB poly, 8× limit) | OOM-killed | verified — 34 MB RSS |
The resident set is flat at ~34 MB whether the polynomial is 512 MB or 2 GB — 8× the memory limit, ~60× the budget: the footprint is the tile/chunk size, not the proof size. A complete, verifiable low-degree proof of a polynomial that does not fit in RAM, produced in a fixed small budget.
flowchart LR
A["execution trace<br/>(> RAM)"] --> B["LDE / NTT<br/>four-step, O(√N)"]
B --> C["batched Merkle<br/>commitment"]
C --> D["DEEP quotient<br/>+ out-of-domain point"]
D --> E["streaming FRI<br/>low-degree test"]
E --> F["StarkProof"]
B -. spill .-> S[("NVMe")]
C -. spill .-> S
E -. spill .-> S
FRI is a STARK's low-degree test, not the whole prover. The rest is here too, as
a small prover framework: an Air trait (trace columns, transition, and
constraints) parameterizes one generic prover and verifier, in core and out of
core. Two AIRs ship and are proved end to end — a linear two-column Fibonacci
and a degree-2 square chain (x_{i+1}=x_i²+k, which exercises a non-linear
constraint and the composition's degree blow-up). The construction is the
standard DEEP-FRI / DEEP-ALI one used by production STARKs, not a shortcut:
- Commit the trace columns' low-degree extensions and the composition
polynomial
H = Σ αⱼ·constraintⱼ / zerofierⱼ(which is degree< Niff every AIR constraint holds on the trace). - Pick a random out-of-domain point
z, batch the trace andHinto one DEEP quotient(P(x) − P(z))/(x − z), and run FRI on it. This certifies that the committed trace andHare degree< Nand that the openings atzare correct (a wrong opening makes a quotient non-polynomial). - Check the identity
H(z) == composition(T(z), T(g·z))at the randomz. Both sides are degree-<Npolynomials, so agreement at a random point means they are equal (Schwartz–Zippel) — which forcesHto be the real composition, and a low-degreeHforces the constraints to hold.
A third AIR adds a grand-product permutation argument — the primitive behind
lookups, copy constraints, and memory consistency. Two columns a, b are
committed; a permutation challenge γ is drawn from the transcript; an auxiliary
running-product column z is committed in a second phase and constrained by
z_{i+1}(b_i+γ) = z_i(a_i+γ) (cyclically, so the product closes), proving
∏(a_i+γ) = ∏(b_i+γ) and hence that a, b are permutations of one another.
Further AIRs exercise the degree and width machinery: a degree-5 power chain
(x_{i+1}=x_i⁵, a hash S-box shape), a public-table LogUp lookup and a
combined transition-plus-lookup circuit, and a wide hash-permutation round
(PoseidonRound) — an 8-column state advanced by next = MDS·sbox(state + RC)
with the Goldilocks S-box x⁷ and a Cauchy MDS layer. That one is degree 7
(composition degree < 6N, handled by a degree_bonus of 3) and is where the
batched commitment matters most: its eight state columns commit under a single
tree. It is a uniform round, a simplification of a real hash's per-round
schedule — not bit-compatible with any standard — but a genuine wide degree-7
system, cross-checked against a plain reference evaluation.
The same round also ships degree-reduced (PoseidonRoundLowDeg), to show the
standard prover trade-off. The degree-7 S-box is split with one cube witness lane
per element — w_j = (state_j+RC_j)³ (degree 3), then (state_j+RC_j)⁷ = w_j²·p
— so every constraint is degree 3 and the LDE blow-up drops from 2⁴ to 2², a
4× smaller domain, at the cost of doubling to 16 columns (all in one batched
tree). It evolves the identical state (the tests cross-check the two encodings),
and proving is measurably faster: at 2^16 rows under the cgroup, ~7 s
(degree-7, 2⁴) → ~2.8 s (degree-3, 2²), about 2.5×, the smaller domain
outweighing the extra columns.
Building on that, a sponge hash (Sponge) takes the realism a step further: a
full multi-round permutation with a distinct per-round constant schedule (not
one uniform round), wrapped in the sponge construction. Each row absorbs a message
block into the rate lanes and runs the permutation, so a 2^log_n-row trace
hashes a 2^log_n·RATE-element message — streamed. The whole round trajectory
lives in one wide 54-column row (kept degree 3 by the same cube-split, blow-up
2²), all under a single batched tree, and the tests cross-check every column
against an independent reference sponge. Measured under the 256 MB cgroup at 2^18
rows: the in-core prover is OOM-killed (it holds the 54-column LDE, ~432 MB),
while the streaming prover verifies in 121 MB RSS in 15.5 s — a hash whose
low-degree extension does not fit the budget, proved within it. The statement can
be made fully public: a last-row boundary constraint pins the trace's squeezed
digest to a claimed value, and the message lanes become preprocessed (public)
columns the verifier pins to a commitment — so the proof certifies
Sponge(public message) = digest (a verifiable computation; with the message left
witness instead, it is knowledge of a preimage). A wrong digest, or a wrong or
missing message commitment, is rejected. (Honest scope: reduced rounds, a Cauchy
MDS, arbitrary fixed constants — a faithful sponge construction, not a
standardized hash.)
The trace, auxiliary, and preprocessed columns are committed in batched
groups: each group goes under one Merkle tree whose leaf at row j is the
Poseidon hash of that group's columns at j, rather than one tree per column.
Committing g columns then costs one tree's hashing instead of g — and the
trace commitment is a large share of the prover's work (the dominant one for
cheap, low-degree AIRs). The preprocessed columns
form their own group (pinned to the public root); the rest of the main columns
form another; the aux columns a third (committed after the permutation
challenge). An opening still carries every column's value, and the verifier
rehashes each group's values into a leaf and checks one path per group, so
nothing is left unbound (a single-column group is bit-identical to the old
per-column leaf). Batching removes the redundant trees — it cuts the commit's
Poseidon count by roughly the column count — but the wall-clock win is bounded by
the commit's share of the proof: for a wide high-degree AIR the NTTs and the
composition stream dominate, so the win is a steady ~10–15 %, not the raw column
factor. (A/B on the same box, measured against the unbatched commit before the
later parallelization work: Fibonacci 2^20 −16 %, an 8-column degree-7 round −12 %.)
Soundness is demonstrated, not asserted: the honest prover run on a trace
that violates the AIR produces a proof that fails to verify (a non-permutation is
rejected); corrupting an opening or an out-of-domain evaluation is caught;
corrupting either column of a batched leaf breaks its path. (src/stark.rs
tests.)
The prover runs entirely out of core (stark::prove_ooc): the trace is
generated to disk, interpolated (ifft_ooc_to_file), extended
(lde_ooc_to_file), composed and batched into the DEEP codeword by streaming
passes, committed with MerkleOoc, and low-degree-tested with
prove_fri_from_file; the out-of-domain evaluations come from a streamed Horner.
It produces a proof bit-for-bit identical to the in-core reference
(stark::prove), checked by the same verifier.
Measured, enforced 256 MB cgroup, swap off — complete STARKs the in-core prover cannot even fit:
| Statement | in-core prover (control) | out-of-core prover |
|---|---|---|
| Fibonacci, 2^20 rows, ×8 blow-up | OOM-killed (~1.8 GB) | verified — 50 MB RSS, 14.7 s |
| Fibonacci, 2^22 rows (~7 GB in-core) | OOM-killed | verified — 45 MB RSS, 61 s |
| Transition + public-table lookup, 2^20 (4 cols) | OOM-killed | verified — 79 MB RSS, 24.9 s |
| Sponge hash of a 2^18-block message (54 cols) | OOM-killed | verified — 121 MB RSS, 15.5 s |
The in-core prover holds the extended trace, composition, DEEP codeword, and the Merkle trees in RAM — gigabytes — and OOMs. The streaming prover proves and verifies the same statement in tens of MB, and that footprint stays flat as the trace grows far past the limit (2^20 → 2^22 is 4× the trace, ~the same RSS). The prover is parallel across the cores (the composition, the DEEP and FRI folds, and the out-of-core NTTs) and uses arity-4 FRI; on this box that is ~1.8–2.9× faster than the first streaming version, with the proof bit-for-bit unchanged. Even the full feature set — a real transition constraint and a public-table lookup, its preprocessing also streamed — proves a trace that does not fit in the budget, in a fixed small budget, checked by a normal verifier.
A fourth AIR is a LogUp lookup — proves every value of a witness column f
is in a table t with declared multiplicities m, via the logarithmic-
derivative identity Σ 1/(f_i+γ) = Σ m_j/(t_j+γ) and a running-sum aux column
that closes to 0. This is the argument behind range checks and table-driven
gates. Its degree-3 constraint pushes the composition degree to 2N, handled by
an AIR-declared degree_bonus that the verifier feeds into FRI's degree check.
The permutation and lookup arguments run fully out of core too: the second-phase commitment and the streamed auxiliary column go to disk, and the streamed proof is bit-for-bit identical to the in-core one.
The lookup's table is a preprocessed (public) column: its commitment is
computed once offline and given to the verifier as a public input, which rejects
any proof that committed a different table — so it is a genuine membership
argument against a fixed table, not "f is in whatever table the prover chose".
The lookup is also sound against a tampered f or a tampered multiplicity m
(both rejected — m is pinned by the identity at a random γ, so no separate
range-check is needed).
Implement the Air trait for your computation and call prove_ooc / verify:
use zk_stream::stark::{prove_ooc, verify, Air, Field, F};
struct ArithProgression; // x_0 = 3, x_{i+1} = x_i + 7
impl Air for ArithProgression {
fn n_cols(&self) -> usize { 1 }
fn n_transition(&self) -> usize { 1 }
fn n_boundary_first(&self) -> usize { 1 }
fn max_constraint_degree(&self) -> usize { 1 }
fn initial_row(&self) -> Vec<F> { vec![F::from_canonical_u64(3)] }
fn next_row(&self, local: &[F]) -> Vec<F> { vec![local[0] + F::from_canonical_u64(7)] }
fn eval_transition(&self, local: &[F], next: &[F], _ch: &[F], out: &mut Vec<F>) {
out.clear();
out.push(next[0] - local[0] - F::from_canonical_u64(7));
}
fn eval_boundary_first(&self, local: &[F], _ch: &[F], out: &mut Vec<F>) {
out.clear();
out.push(local[0] - F::from_canonical_u64(3));
}
}The full runnable version is examples/custom_air.rs:
cargo run --release --example custom_air -- 18 /var/tmp
# under an enforced limit (the in-core prover would OOM; this won't):
systemd-run --user --scope -p MemoryMax=256M -p MemorySwapMax=0 -- \
./target/release/examples/custom_air 22 /var/tmpHonest scope: small AIRs (a few columns, a grand-product permutation, a public-table LogUp lookup), no recursion. It trades RAM for I/O time, and the prover is Poseidon-commitment-bound (measured); the commit I/O is overlapped with hashing (pipelined) and trace columns are committed in batched groups (fewer trees), but the deepest speed lever — GPU hashing — is future work. The win is the regime where the in-core prover does not fit at all.
use zk_stream::transform::ntt_ooc_streamed;
use std::path::Path;
// NTT of a 2^log_n array whose elements come from `gen`, never holding the whole
// array in RAM. `block` sets the resident budget (~block² elements). `dir` must
// be fast storage (NVMe), not tmpfs.
let checksum = ntt_ooc_streamed(Path::new("/var/tmp"), 28, 2048, |i| gen(i))?;four_step_ooc(&input, dir, block) returns the full transform as a Vec (for
when the result fits in RAM); block trades memory for speed — bigger tiles are
faster but use more RAM.
Reproduce:
cargo +nightly run --release -- incore 26 # 512 MB transform, in core
cargo +nightly run --release -- ooc 26 2048 /var/tmp
systemd-run --user --scope -p MemoryMax=256M -p MemorySwapMax=0 -- \
./target/release/zk-stream ooc 28 2048 /var/tmp # 2 GB NTT in 256 MB
# End-to-end out-of-core FRI of a polynomial bigger than RAM:
# fribig <log_n> <final_log> <blowup_log> <queries> <chunk> <block> <dir>
systemd-run --user --scope -p MemoryMax=256M -p MemorySwapMax=0 -- \
./target/release/zk-stream fribig 27 6 3 60 8192 2048 /var/tmp # 1 GB poly in 256 MB- This is the NTT primitive, not a streaming prover. It proves the dominant hot buffer can go out of core. A full low-RAM prover must also stream the MSM, FRI, commitments, and prover key, and wire the streamed NTT into the proving pipeline — a real engineering program, not a drop-in.
- It trades RAM for I/O time (~4–5× here, more under a tight limit). The win is the regime where the in-core transform simply does not fit.
- Out-of-core FFT is known in HPC. What's fresh here is a verified, ZK-field (Goldilocks) out-of-core NTT packaged as a building block for streaming provers, with the measurements to show the RAM floor is algorithmic.
- Correctness rests on plonky2's field arithmetic and per-tile transforms; only the out-of-core decomposition and transposes are new code, and they are checked bit-for-bit against the direct NTT.
MIT OR Apache-2.0.
