Paper 2025/572

A zk-SNARK Programming Framework for Verifiable Data Analytics

Abstract

zk-SNARKs enable succinct, efficiently verifiable proofs of correct computation over private data, but require the computation to be compiled into a \emph{statically defined and bounded} arithmetic circuit. This requirement creates a multidimensional mismatch with data-analytic programming, which consists largely of array programs: (a)~array operations and resulting shapes are dynamic; (b)~arrays are accessed at data-dependent positions; (c)~control flows are data-dependent. Existing zk-SNARK DSLs enforce this requirement using conservative syntactic restrictions that reject many bounded programs, or leave the programmer to bound and encode these by hand, while zkVMs recover expressiveness at substantially higher proving cost. We present \textsc{Zinnia}, a zk-SNARK programming framework for analytics in which programs are written in a subset of Python with NumPy. Zinnia's compiler uses SMT-backed symbolic execution over array types with bounds to derive properties of the program's values that hold on every input, which we call \emph{facts}. The facts bound every data-dependent shape and loop, which gives each array its capacity in the circuit. Built atop this compiler, \textsc{Zinnia} provides bounded-dynamic array and arithmetic operations for analytics. The same facts guide how these operators are lowered: for each operator, \textsc{Zinnia} considers known circuit constructions, whose cost depends on what the facts guarantee. Unlike a program, a circuit has no order in which a check protects later uses, so if a construction needs a fact, another constraint in the circuit must enforce it. A construction chosen for one operator may enforce a fact that another relies on. \textsc{Zinnia} therefore chooses the constructions of all operators together, seeking to minimize estimated circuit cost. Our evaluation on unmodified programs from three NumPy corpora shows that the circuits \textsc{Zinnia} compiles are never larger than optimized hand-written ones in existing DSLs, and that \textsc{Zinnia} achieves over $30\times$ faster proving than zkVM-based approaches by geometric mean.