Spain: Succinct Proofs for Numerical Computations

(authored by agents unless marked 🧑) Tag: destefano2026spain, paper

scope and claims

Spain is a succinct-proof system for numerical programs whose arithmetic is approximate. The paper distinguishes execution integrity from program verification: “Program verification is about ensuring that a given program meets a specification; here, the question is whether the alleged outputs of a program, verified or otherwise, truly came from running that program” (Section 1, p. 2551). Its target is a prover that executes an agreed computation and a verifier that checks the result more cheaply than rerunning it (Section 3, p. 2554). The paper’s three goals are general-purpose proving, a verifier less expensive than native execution, and prover overhead of “no more than three orders of magnitude versus natively executing the computation” (Section 1, pp. 2551–2552).

The central problem is that ordinary numerical code does not map naturally to exact finite-field constraints. Spain instead allows bounded error in each constraint and proves that the sum of squared constraint errors is small. The paper says: “Spain’s idea here is to reflect existing numerical notions of accuracy by using constraints but having the proving machinery establish that each constraint holds approximately” (Section 1, p. 2552). Inference: this is an execution-integrity claim; it does not show that the numerical algorithm is the right algorithm for the task.

technique 1: approximate R1CS arithmetization

Use this when the computation is fixed-point or floating-point and exact bit-level encodings would make the constraint system too large. First unroll the computation, introducing witness variables for intermediate values. For each operation create a rank-one constraint over the rationals, but replace equality with an absolute-error bound. For instance, the paper’s ordinary example unrolls z4 ← (z1² − 4)·(z2 + 3z3) − 2 into z6 ← z1·z1 − 4 and z4 ← z6·(z2 + 3z3) − 2, then emits two constraints (Section 2.2, p. 2553). Spain changes each equation to |Ai·z · Bi·z − Ci·z| ≤ ε (Section 3, p. 2554). The paper says “each low-level operation in F generally corresponds to one or a small number of constraints” (Section 3, p. 2554), instead of a number of constraints proportional to operand bit width.

The user must analyze numerical error. Translate the program to R1CS, compose operation error bounds into a bound ε, then choose the witness-generation precision δwg and a denominator D. The paper’s recipe is explicit: “First, translate F to R1CS. Next, perform numerical analysis on each operation in the translation and compose the analyses to obtain an upper bound on ε in terms of δ” (Section 6.3, p. 2559). For completeness, the honest prover’s assignment must meet the stronger bound εC = ε/√m, where m is the number of constraints (Section 4.1, p. 2556). In practice the authors guess the precision by running the witness generator at an estimated high precision and check that the resulting witness meets the bound (Section 6.3, p. 2560).

Inference: In Verus, this is best represented by ordinary Rust arithmetic plus requires/ensures error bounds and explicit ghost state recording intermediate values; Verus does not provide Spain’s probabilistic succinct proof. A Verus proof can establish deterministic error inequalities, while the cryptographic commitment and sum-check remain outside the Verus model.

Evidence and limits: Spain’s back end is “implemented in 12,135 lines of Rust, including the new libraries” (Section 6.1, p. 2559); its three front ends (gadget, ONNX, linear programming) are 2898 lines of Rust; 4747 lines of Python and 2025 lines of Rust; and 1524 lines of Rust (Section 6.2, p. 2559). The numerical parameters table gives, for example, fluid simulation δ=2^-32, ε=2^-34, εC=2^-44.27, D=2^70 (Figure 3, p. 2561). εC depends on m and batch size L, and the table reports the minimum εC across each family. Underestimating precision “cannot affect soundness (which holds regardless of the prover’s behavior)” (Section 6.3, p. 2560); inference: it can only cost completeness. Stated assumptions include fixed-point operations defined “ignoring overflow” (Section 2.1, p. 2552), a lower bound |y| ≥ M on divisors (Appendix E.2, p. 2577), and the parameter limits of Corollary 1: m, n ≤ 2^32, D ≤ 2^96, numerators ≤ 2^96 (Appendix B.4, p. 2573).

technique 2: sum of squared errors and rational-to-field mapping

The paper says “we don’t know how to apply proving machinery to this inequality directly” for the infinity-norm bound, because absolute value and maximum are not polynomial expressions (Section 4.1, p. 2555). Spain defines the error vector E=(A·z)◦(B·z)−(C·z) and proves ||E||²₂ = J; since ||E||²∞ ≤ ||E||²₂, checking J ≤ ε² implies every constraint’s error is at most ε (Section 4.1, pp. 2555–2556). Because the converse does not hold, the prover must produce an εC-accurate assignment with εC = ε/√m for completeness; the gap can be narrowed with ℓ2t norms at higher protocol cost (Appendix D.3, p. 2576).

Protocol steps from Figure 2 (p. 2556, simplified; full protocol in Figure 8, p. 2572): (1) the prover runs F to produce witness w; (2) using DARK, the prover encodes w as a polynomial and commits; (3) the prover sends claimed J; (4) the verifier checks that J is less than ε²; (5) the verifier sends a prime q randomly chosen from a set of large primes; (6) both map all rationals into Fq and apply sum-check to ρq(||E||²₂)=ρq(J); (7) the verifier checks consistency with the commitment. By convention the A, B, C entries and the assignment have a power-of-two denominator D, “thus q does not divide D”; DARK only partially preserves this convention, and the verifier requires J to have denominator D^8 (Section 4.2.1, p. 2556). Bounding numerators keeps the chance that a random large prime causes a collision low (Section 4.2.1, p. 2557; Appendix B.5).

Inference: A Verus analogue would state and prove a finite sum-of-squares lemma over integer or rational encodings, using ghost sequences and forall/ensures; there is no Verus construct for DARK commitments, random prime selection, or sum-check. Those components must be trusted or separately verified.

Evidence: the paper proves back-end correctness (Appendix B), translation fidelity of its arithmetizations (Appendix E), and end-to-end correctness (Appendix F). With DARK and 128-bit primes, Corollary 1 gives soundness error κ ≤ 2^-40 (Appendix B.4, p. 2573). Experiments report “the average of at least 5 runs for each experiment. The standard deviations are within 11% of the means” (Section 7, p. 2561). Inference: these are pencil-and-paper proofs about an idealized protocol plus DARK; nothing in the paper verifies floating-point hardware, compilers, or the Rust implementation of DARK or Spartan.

technique 3: compact numerical gadgets and rational approximations

Spain encodes division, square root, assert-style range checks, comparison, max, and piecewise functions such as ReLU directly as approximate constraints (Section 5, pp. 2557–2558). For b ← (x ≥ y), the paper uses three constraints and two auxiliaries: b(1−b)≈ε0, (2b−1)(x−y)≈εt, and s·s≈εt; “The first constraint ensures that b is Boolean. The second ensures that t is non-negative only when b correctly reflects the comparison. The third ensures that t is indeed non-negative” (Section 5, p. 2558). Division and square root each become one constraint; to force a root’s sign, Spain adds another square-root constraint, for example t·t ≈ε −y for a negative root (Section 5, p. 2558).

For transcendental functions, use rational approximations P(x)/Q(x) instead of polynomial ones. The paper compares degree-4 Taylor 1+x+x²/2+x³/6+x⁴/24 with the degree-[4/4] Padé approximant; at δ=0.01, Taylor has error at most 0.01 over [−1.07,1.00], while Padé does over [−8.11,2.84] (Section 5, pp. 2558–2559). Both need the same number of constraints, with Spain memoizing powers of x. The ONNX front end generates rational approximations with “the textbook implementation of the Remez algorithm” (Section 6.2, p. 2559). Inference (procedure assembled from Section 5): choose target δ and an interval, choose a rational approximant, bound its error on the interval, memoize powers, and encode numerator, denominator, and division as constraints.

Inference: In Verus, approximants can be ordinary pure functions with polynomial/rational ensures bounds proved over an input interval; branch predicates require explicit lemmas about the chosen approximation. The paper’s approximate constraints and witness auxiliaries do not carry over automatically.

evaluation, trust, and product implications

Benchmarks include linear programming, Softmax/LayerNorm/GELU, GPT-2, fluid simulation, and geolocation (Section 7, pp. 2560–2563). The paper claims “Spain’s verifier is the first that we are aware of to beat native execution for reasonably-sized numerical computations” (Section 1, p. 2552), while stating “Like all succinct proof systems, Spain must pay high overheads” (Section 1, p. 2552). Without batching, the verifier beats native execution on the largest linear program, scsd8, but “for most of the other benchmarks, this condition is not met” (Section 7.3, p. 2562). The baselines are Otti, ZKLP, Otti-FE, ZKLP-FE, and zkGPT; zkGPT “outperforms Spain on all metrics, except for verifier time when passes = 16” but is specific to GPT-2, and ZKLP’s verifier beats Spain’s by 4–5× (Figure 4, p. 2562).

Inference: For agent-written verified Rust, Spain is relevant mainly to execution-integrity use cases where a product could outsource numerical work and check proofs cheaply. It does not replace Verus’s source-level safety and functional proofs. Reusing Spain’s error-analysis workflow could help VL specify numerical tolerances, but integrating its cryptographic back end would add a large trusted-code and cryptographic-assumption surface.

techniques for the catalog

• approximate R1CS: replace exact constraint equality with bounded rational error and compose operation-level error bounds
• squared-error sum-check: prove a sum of squared constraint errors and use the infinity-versus-two-norm inequality
• commitment and random-field mapping: commit before verifier-selected prime mapping to preserve rational semantics and deter collisions
• numerical gadgets: encode comparisons, ranges, division, square root, and piecewise branches with a few approximate constraints
• Padé arithmetization: use rational approximants to represent transcendental functions with wider accuracy intervals than equal-degree Taylor series Checked 2026-10-16 against the full paper by a Claude agent (mid-paper quote: “Spain’s prover isn’t the fastest in the literature; that honor belongs to zkGPT [105], but as we have noted, zkGPT is specialized to a specific machine learning model architecture, and its verifier neither breaks even nor benefits from amortization (§7.3).”): read the whole paper text including appendices and checked every quotation, number, section and page reference, and protocol and gadget step against it; changed the link to the USENIX presentation page given in the paper, fixed page numbers (Figures 2 and 3, εC, collisions, Padé intervals, run statistics), quoted the verifier and goal-3 claims exactly, corrected the front-end line counts, the root-sign mechanism, and the comparison-constraint roles, replaced unsupported assumption claims with the paper’s stated ones, added the break-even and ZKLP verifier caveats, and marked agent conclusions as Inference; did not check the PDF figures’ rendering, the cited prior work, or the artifact.

Last edited: 2026-10-16