Skip to content

compsec-epfl/efficient-sumcheck

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

121 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Efficient Sumcheck

A high-performance sumcheck library with correctness-fuzzing against a verified oracle.

  • Efficient — transparent SIMD acceleration (8-wide AVX-512, 2-wide NEON)
  • Streaming-capable — optional sublinear memory via sequential evaluation
  • Complete — built-in Fiat-Shamir, partial execution, per-round hooks

Built using arkworks. Compatible with any ecosystem — see docs/compatibility.md. Research-grade; not yet audited — see SECURITY.md.

Quick Start

Multilinear Sumcheck

Proves $H = \displaystyle\sum_{x \in \lbrace 0,1 \rbrace^v} p(x)$ where $p$ is a multilinear polynomial.

use effsc::{noop_hook, runner::sumcheck};
use effsc::provers::multilinear::MultilinearProver;

let mut prover = MultilinearProver::new(evals);
let proof = sumcheck(
    &mut prover,
    num_vars,
    &mut transcript,
    noop_hook,
);

Inner Product Sumcheck

Proves $H = \displaystyle\sum_{x \in \lbrace 0,1 \rbrace^v} f(x) \cdot g(x)$ for two multilinear polynomials. Degree-2 round polynomials.

use effsc::{noop_hook, runner::sumcheck};
use effsc::provers::inner_product::InnerProductProver;

let mut prover = InnerProductProver::new(a, b);
let proof = sumcheck(
    &mut prover,
    num_vars,
    &mut transcript,
    noop_hook,
);

Coefficient Sumcheck

Proves $H = \displaystyle\sum_{x \in \lbrace 0,1 \rbrace^v} p(x)$ where $\deg_{x_i}(p) \leq d$. The user implements RoundPolyEvaluator to define per-pair round polynomial contributions; the library handles iteration, parallelism, and reductions.

use effsc::{noop_hook, runner::sumcheck};
use effsc::provers::coefficient::CoefficientProver;

let mut prover = CoefficientProver::new(
    &evaluator,
    tablewise,
    pairwise,
);
let proof = sumcheck(
    &mut prover,
    num_rounds,
    &mut transcript,
    noop_hook,
);

Verification

One verifier for any degree $d$. Returns SumcheckResult { challenges, final_claim }⚠️ the caller is responsible for the oracle check (Thaler Remark 4.2).

use effsc::{noop_hook_verify, verifier::sumcheck_verify};

let result = sumcheck_verify(
    claimed_sum,
    degree,
    num_rounds,
    &mut transcript,
    noop_hook_verify,
)?;

// Standalone: compare against the prover's claimed final value.
assert_eq!(result.final_claim, proof.final_value);

// Composed (WHIR, GKR): pass final_claim to the next layer.
next_layer_claim = result.final_claim;

Variable Ordering

Each prover comes in two variants:

  • MSB (half-split) — optimal memory layout in most cases. Used by WHIR and WARP.
  • LSB (pair-split) — optimal for streaming applications where evaluations arrive sequentially.
MSB LSB
MultilinearProver MultilinearProverLSB
InnerProductProver InnerProductProverLSB
CoefficientProver CoefficientProverLSB
GkrProver

See docs/design.md for details.

Partial Execution and Hooks

The sumcheck() runner supports partial execution (num_rounds < v) and per-round hooks for composed protocols:

// WHIR: partial sumcheck with proof-of-work grinding
let proof = sumcheck(
    &mut prover,
    folding_factor,  // num_rounds < v
    &mut transcript,
    |_, t| round_pow.prove(t),  // per-round hook
);

SIMD Acceleration

All provers transparently auto-dispatch to SIMD backends. Supported fields:

  • Goldilocks ($p = 2^{64} - 2^{32} + 1$) and degree-2/3 extensions
  • M31 ($p = 2^{31} - 1$) and extensions
  • BabyBear ($p = 2^{31} - 2^{27} + 1$) and extensions
  • KoalaBear ($p = 2^{31} - 2^{24} + 1$) and extensions
Backend Width Platform
NEON 2-wide aarch64 (Apple M-series, Graviton)
AVX-512 IFMA 8-wide x86_64 (Sapphire Rapids)

Falls back to scalar for other fields. See SECURITY.md for unsafe scope.

Integrations

Integrated into Whir (PR) and Warp (PR) with measured performance improvements. Integration capability for streaming contexts like Jolt is described in docs/design.md.

Correctness

🚧 Undergoing fuzzing over randomized inputs against z-tech/sumcheck-lean4, an oracle with machine-checked proofs of completeness and soundness. Findings to follow.

References

[LFKN92]: Carsten Lund, Lance Fortnow, Howard J. Karloff, and Noam Nisan. "Algebraic Methods for Interactive Proof Systems". In: Journal of the ACM 39.4 (1992).

[CTY11]: Graham Cormode, Justin Thaler, and Ke Yi. "Verifying computations with streaming interactive proofs". In: Proceedings of the VLDB Endowment 5.1 (2011), pp. 25-36.

[VSBW13]: Victor Vu, Srinath Setty, Andrew J. Blumberg, and Michael Walfish. "A hybrid architecture for interactive verifiable computation". In: Proceedings of the 34th IEEE Symposium on Security and Privacy. Oakland '13. 2013, pp. 223-237.

[CFFZ24]: Alessandro Chiesa, Elisabetta Fedele, Giacomo Fenzi, Andrew Zitek-Estrada. "A time-space tradeoff for the sumcheck prover". In: Cryptology ePrint Archive.

[BCFFMMZ25]: Anubhav Baweja, Alessandro Chiesa, Elisabetta Fedele, Giacomo Fenzi, Pratyush Mishra, Tushar Mopuri, and Andrew Zitek-Estrada. "Time-Space Trade-Offs for Sumcheck". In: TCC Theory of Cryptography: 23rd International Conference, pp. 37.

[Thaler23]: Justin Thaler. "Proofs, Arguments, and Zero-Knowledge". Chapter 4: Interactive Proofs. July 2023.

[BDDT25]: Aarushi Bagad, Quang Dao, Yuri Domb, and Justin Thaler. "Speeding Up Sum-Check Proving". Cryptology ePrint Archive, 2025/1117.

About

No description, website, or topics provided.

Resources

License

Apache-2.0, MIT licenses found

Licenses found

Apache-2.0
LICENSE-APACHE
MIT
LICENSE-MIT

Security policy

Stars

Watchers

Forks

Releases

No releases published

Packages

 
 
 

Contributors

Languages