Scaling Verifiable Computation Using Efficient Set Accumulators

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

what is proved or measured

Inference: The paper compiles RSA-accumulator state operations into SNARK rank-1 constraints and compares them with Merkle-tree constraints. Its measured results use Bellman/Groth, BLS12-381 and a 2048-bit RSA quotient group; most experiments use Poseidon, while one varies four hash functions. Persistent RAM is assessed with a cost model rather than an end-to-end implementation. The paper states: “In this work, we use a combination of existing and novel techniques to implement an RSA accumulator inside of a SNARK, and use it as a replacement for a Merkle tree.” (Abstract, p.2075). A SNARK proves that a witness satisfies compiled constraints. The guarantees depend on the proof-system and RSA assumptions, the random-oracle model, setup, and correct compilation and implementation. The paper treats state as public and leaves zero-knowledge applications to future work (§1; §2.2, footnote 4).

technique: compile computation to R1CS with advice

Inference: Use when a computation must be proven by a preprocessing SNARK. Compile a program to constraints of the form linear-combination times linear-combination equals linear-combination. Put hard-to-express values in prover advice and constrain them. For x != 0, provide inverse Z and enforce Z·X=1; for bitwise operations, provide bit limbs and enforce reconstruction and Booleanity. For conditionals, expand both branches and use a selector to constrain the selected result; loop bounds must be statically known. For multiprecision, represent a number as field limbs, track maximum widths, and constrain arithmetic results; use data-flow bounds for quotient widths. The paper says: “Multiprecision operations rely heavily on advice from P.” (§2.2, p.2079).

Inference: a possible Verus adaptation would specify the integer represented by field limbs and prove arithmetic and range invariants. This paper supplies no Verus implementation or performance evidence. Incorrect range bounds or unconstrained advice would undermine the intended constraint semantics. The paper counts 3b+3 constraints for a b-bit AND (§2.2, p.2078).

technique: batched MultiSwap over an RSA accumulator

Inference: Use when a large set has many sequential replacements and Merkle paths dominate. Represent a multiset S by J S K = g^(product H(s)) in an RSA quotient group. Define swaps (xi, yi) as remove xi and insert yi. Prove there is an intermediate multiset satisfying S ⊎ {yi}=Smid and Smid \ {xi}=S'; Lemma 1 guarantees that the swap multiset decomposes into cycles and a cycle-free subsequence that produces S’ in some valid sequential order. It does not enforce a supplied execution order or require the discarded cycles to be executable from S. The authors explain: “Instead, our solution first verifies all the insertions, and then verifies all the deletions, irrespective of the order in which the operations are listed.” (§3, p.2080). For insertion and removal, use Wesolowski exponentiation proofs; derive the prime challenge by Fiat–Shamir over all inputs, and verify products of HΔ values modulo the challenge. For each removed or inserted item, compute HΔ and its modular product contribution, and include the item in the challenge hash. The proof also has a fixed large overhead.

Inference: a possible Verus model would define multisets and swap transitions and prove the cycle-decomposition property separately from the cryptography. Cryptographic soundness of RSA and Fiat–Shamir would require explicit assumptions; the paper contains no Verus proof of SNARK knowledge soundness. The paper’s semantic caveat is material: cycles are ignored by the cycle-free subsequence, so a naïve self-swap encoding does not validate LOAD values (§5.2).

technique: prime hashing and division-intractable hashing

Inference: Use when a SNARK needs a random prime challenge and cannot afford repeated probabilistic primality tests. Build a recursive Pocklington certificate: start from a 32-bit prime tested by deterministic three-round Miller–Rabin. At each recursive step, derive a pseudorandom hi from the input hash, take bounded ni and ai as advice, set ri = 2^(bni)·hi+ni and pi = pi-1·ri+1, and check the Pocklington witness with ri < pi-1. The authors force each hi’s high bit to one, obtaining a 322-bit final prime with 256 bits of guessing entropy after four recursive steps beyond the base case (§4.1, Fig.2). They write: “Our approach thus saves more than an order of magnitude and provably outputs a prime.” (§4.1, p.2081). Define HΔ(x)=H(x)+Δ with a random 2048-bit Δ; H outputs 256-bit values. Reduce Δ modulo the challenge once and reuse that result; each item still requires reducing H(x)+(Δ mod ℓ) modulo ℓ (§4.2).

The division-intractability claim assumes a random oracle and a conjecture about the density of integers with only small prime factors in short intervals; it is not an unconditional consequence of collision resistance (§4.2). Inference: a possible Verus adaptation would prove certificate checking with integer arithmetic and bounds, while treating those cryptographic claims as assumptions.

technique: persistent RAM using an address-ordered transcript

Inference: Use when state must persist across proofs and input-dependent LOAD/STORE addresses prevent static compilation. Store (address,data) tuples in the accumulator. Build an execution-ordered transcript; have the prover supply an address-ordered transcript T. Constrain T to be a permutation, sorted by address then execution index, and coherent: later LOADs at an address return the preceding access’s data. Remove the tuple at each address’s first access, using the loaded value for a first LOAD or prover-supplied old data for a first STORE. Insert the tuple containing the last access’s data; batch these removals and insertions with MultiSwap. This anchors the transcript to the initial and final persistent state. For uninitialized memory, initialize every address with (δ,0) (expensive), or use a validity canary plus non-membership proofs (left as future work). The paper states: “Our key insight is that a hybrid of the Pantry and BCGT approaches solves this issue.” (§5.2, p.2084).

Inference: a possible Verus adaptation would represent T as a sequence and prove sortedness, permutation, coherence, and consistency with initial and final state. The accumulator’s cryptographic binding remains trusted. A naïve self-swap LOAD is unsound because MultiSwap may omit cycles (§5.2).

evidence, limits, and VL threat

Inference: The 2^20-element set benchmark used two Xeon E5-2687Wv4 CPUs, 128 GiB RAM, Ubuntu 18.04, Rust 1.41-nightly, Poseidon, BLS12-381, and a 2048-bit RSA group (§6–7). Verification was about 7 ms. At 10^9 constraints, MultiSwap fit up to 3.3× more swaps than Merkle trees; Rollup fit up to 1.9× more transactions. For 2^20 elements, digest computation after batch removal took about 43 seconds and 4 GiB RAM. Break-even proving time was 1,200–1,600 swaps; Rollup break-even was about 600 transactions for 2^20 accounts and 2,000 for 2^10 accounts (§7.1–7.2). Denominators are the stated set size, transaction count, or 10^9-constraint budget; the paper reports approximate values, not confidence intervals. Large sets above 2^25 incur expensive advice generation, and RSA needs trusted setup (though multiparty generation is suggested). The implementation is about 11,300 Rust lines (§6).

Inference: for VL, the transcript, permutation, and boundary-state invariants may be useful when specifying persistent mutable state. The paper does not evaluate agent-written Rust or Verus, so its constraint-count improvements do not establish a benefit for those workloads. The authors build on prior Merkle RAM, BCGT transcripts, multiprecision compilation, and batched RSA proofs; their contributions include MultiSwap semantics, efficient prime and division-intractable hashing in constraints, applications, and the measured tradeoff (§1, §8).

techniques for the catalog

• Inference: advice-constrained R1CS compilation — encode branch, bit, inverse, and multiprecision operations while constraining prover-supplied advice
• Inference: MultiSwap RSA accumulator — batch sequential set replacements with insertion/removal proofs and cycle semantics
• Inference: recursive Pocklington prime hashing — generate a SNARK challenge prime with a short recursive certificate
• Inference: division-intractable HΔ hashing — hash elements to large integers that resist divisibility attacks
• Inference: transcript-backed persistent RAM — prove address ordering, permutation, coherence, and boundary state with batched accumulator updates Checked 2026-10-16 against the full paper by a Codex agent (mid-paper quote: “Our design yields a persistent RAM abstraction whose per-access constraint cost is lower than Pantry’s even at modest RAM sizes, and is nearly insensitive to RAM size.”): read the whole paper, including references and appendices; checked quotations, numbers, section and printed-page references, technique steps, assumptions, and evaluation scope; corrected the publisher link, quotation context, exponent notation, MultiSwap semantics, prime-hashing details, reusable Δ reduction, RAM read semantics, and unsupported Verus/VL assertions; did not reproduce experiments, audit the implementation, or independently prove the cryptographic claims.

Last edited: 2026-10-16