Skip to content

nzengi/zk-stream

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

1 Commit
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

zk-stream

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 terminal recording: under a 256 MB cgroup the in-core prover is OOM-killed, while the out-of-core prover proves the same 2^20-row Fibonacci STARK and verifies in 39 MB of RAM

Why

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.

What this proves

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(&radic;N) working set"]
    end
    T ==>|stream a row or column tile| W
    W ==>|transformed tile written back| T
Loading

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.

Toward a streaming prover: out-of-core LDE

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 opening phase: a complete streaming FRI

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.

Closing the loop: a FRI proof of a polynomial bigger than RAM

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), one pread per 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.

The out-of-core resident set stays flat at ~34 MB across a 512 MB to 2 GB polynomial range, while the in-core prover crosses the 256 MB cgroup ceiling and is OOM-killed

The whole prover: a STARK whose trace does not fit in RAM

flowchart LR
    A["execution trace<br/>(&gt; RAM)"] --> B["LDE / NTT<br/>four-step, O(&radic;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
Loading

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 < N iff every AIR constraint holds on the trace).
  • Pick a random out-of-domain point z, batch the trace and H into one DEEP quotient (P(x) − P(z))/(x − z), and run FRI on it. This certifies that the committed trace and H are degree < N and that the openings at z are correct (a wrong opening makes a quotient non-polynomial).
  • Check the identity H(z) == composition(T(z), T(g·z)) at the random z. Both sides are degree-<N polynomials, so agreement at a random point means they are equal (Schwartz–Zippel) — which forces H to be the real composition, and a low-degree H forces 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 , 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, ), 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 ), 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).

Defining your own AIR

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/tmp

Honest 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.

Usage

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

Scope and honesty

  • 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.

License

MIT OR Apache-2.0.

About

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.

Topics

Resources

Stars

Watchers

Forks

Releases

Packages

Contributors

Languages