Formally Verifying Zero Knowledge for Zakura

Earlier this week, we announced a new version of Common, our cryptography stack for Zcash. Its bundled Ironwood zk-SNARK prover is roughly 21× faster on an iPhone 17 than it was before Zakura. Among the many prover optimizations, one was making the masking polynomials use fewer random coefficients. The zero knowledge guarantee has to hold across all of these changes. (This privacy property is separate from soundness, which protects against proving false claims.)

Today, we’ve formalized zero knowledge in Lean for our model of the optimized prover shipped with Zakura 1.4.0. This is, to our knowledge, the first and only Zcash zk-SNARK prover that has been subject to this kind of analysis.

The proof compares everything the verifier sees with a simulation made without the private witness, accounting for the interaction of messages and randomness throughout the protocol. For one Action (a shielded spend paired with an output), the interactive simulation error is below . For Actions, with , it is below , so the bound grows at most linearly with the number of Actions.

In the cryptographic literature, zero knowledge is often analyzed first in an interactive setting, where the verifier sends random challenges to the prover. Our formalization starts there, proving statistical honest-verifier zero knowledge (HVZK), where the verifier must follow the protocol.

Zakura’s deployed protocol uses Fiat–Shamir: hashing the transcript supplies those challenges, so proving needs no back-and-forth with a verifier. We prove statistical zero knowledge (ZK) for this construction in the classical programmable random-oracle model. The proof treats the hash as an ideal random function whose answers the simulator can set at previously unqueried inputs.

Reproducing the verifier’s view

We build a simulator that never receives the private witness. In the interactive protocol, it uses the public inputs, challenges sent by the verifier, and its own randomness to produce a view close in distribution to the real prover’s. That view includes commitments, polynomial evaluations, messages from the inner product argument (IPA), received challenges, and failure status.

Imagine giving either view to a party trying to distinguish real and simulated transcripts. To show statistical indistinguishability, we bound how much any party’s probability of answering “real” can differ between the two cases, even with unlimited computation.

PLONK expresses the circuit’s checks as polynomial relations. A polynomial commitment locks in a polynomial with a compact message, and an opening proves its value at a chosen point. We simulate PLONK and IPA together because the commitments in one stage and the opening proof in the other depend on the same polynomials. Messages can look random individually while their correlations reveal private data, so the proof must compare the complete view.

For Fiat–Shamir, the challenges come from hashing the transcript. We model that hash as a programmable random oracle and include the adversary’s oracle queries and responses in the comparison, alongside the proof itself.

Masking with fewer coefficients

Two optimizations reduce the number of random coefficients used to mask witness data and blind commitments. These masks randomize the witness-dependent values revealed to the verifier while preserving the relations it checks.

Multi-opening combines several opening claims into one proof. The linear multi-opening mask uses a random line, , with independently sampled field coefficients and , instead of a dense random polynomial. Here is the polynomial’s input. One point does not determine a line: revealing its value at one point leaves randomness to hide the combined opening evaluation at a second distinct point.

The sparse IPA mask places 11 independently sampled coefficients at the power-of-two degrees . Its constant term makes it zero at the opening point, so adding the mask preserves the value being proven.

The IPA folds the polynomial down to one scalar. With fixed challenges and ideal uniform randomness, the result is uniform if any random mask coefficient still affects it, hiding the witness’s contribution. Otherwise, the power-of-two structure makes it equal the publicly claimed value, except when a zero challenge disables the mask. We include that rare case in the statistical bound.

Accounting for the randomness

A random tape supplies the sequence of random choices read by the prover or simulator. The statistical results assume fresh, independent uniform random-bit tapes. For seeded pseudorandom number generators (PRNGs), we assume their output can’t be efficiently distinguished from fresh random bits.

Uniform field elements simplify the masking argument, but drawing them exactly uniformly by rejection sampling can mean discarding a draw and trying again. The prover instead uses wide reduction to avoid those retries: it reads exactly 512 random bits per field element and reduces that integer modulo , the scalar-field modulus (the prime number of possible field values). The tradeoff is a tiny sampling bias: since does not divide , some values are slightly more likely than others.

For uniform input bits, write for the statistical distance from uniform and for the remainder when is divided by . Then:

For Actions, the full proof schedule uses private random field elements to mask witness data and blind commitments. The error bound accounts for the accumulated sampling bias and exceptional challenges (rare verifier values, such as zero, that can disable a mask or make an inversion undefined). We can set those challenges aside in the simulation argument because the bound includes their total probability.

To establish these statistical bounds, Lean models the tape as an input with a specified probability distribution; it doesn’t generate a particular tape. The proof reasons about the simulator’s output over that distribution. Running the simulator requires concrete random values.

Lean checks a mathematical proof of the simulation bound for every allowed witness, over the specified distribution of random choices. That theorem does not depend on the Rust fixtures, which supply fixed test inputs and expected outputs. We use those separately to check concrete prover executions.

Simulation error bounds

Interactive protocol. Fix the public inputs and let be any test that labels a verifier view “real” by returning . The complete view includes emitted messages, received challenges, the verifier tape, and failure status. Write for the interactive simulation-error bound and for probability. Our theorem gives:

This bound includes both exceptional challenges and accumulated sampling bias.

For one Action, . If the real and simulated sources are equally likely, a test can guess the source with probability at most .

Fiat–Shamir. The random-oracle theorem uses a simulator that draws its private field values exactly uniformly, while the real prover uses wide reduction. Let be the maximum number of oracle queries made before the proof attempt. The Fiat–Shamir simulation-error bound, , adds :

Since , the extra term satisfies . This bounds the chance that a prior query conflicts with the simulator’s oracle programming. The comparison covers the attacker’s oracle queries and responses, including queries chosen after seeing the result.

The first simulator uses uniform field elements to simplify the analysis. We also show that simulation works with random-bit tapes and the same wide reduction used by the prover.

The simulator using uniform random-bit tapes also reduces 512-bit samples modulo , adding to this bound. The conservative upper bound holds for both simulators.

Completeness

A prover also needs to turn a valid witness into a proof the verifier accepts. This is completeness.

Our model uses 2,048 circuit rows per Action and 11 IPA rounds (). We reuse Ironwood’s existing Action circuit completeness proof to show that witnesses built as specified produce rows that satisfy the circuit. This connection lets both zero knowledge results apply to Action witnesses.

We also prove that a valid witness produces an accepted proof with high probability. The failure bound covers attempts that stop early and completed proofs the verifier rejects, including rare failures from exceptional challenges. Perfect completeness would require acceptance probability exactly .

Other exceptional cases are assumed infeasible to construct. For instance, we omit certain Sinsemilla curve-addition checks because triggering those cases would yield a nontrivial multi-base discrete-log relation, which is assumed computationally infeasible to find.

Checking Rust against Lean

Our earlier verifier fixtures let Lean check proofs produced by Rust, using their recorded challenges. They did not contain the private witness rows or RNG draws needed to reproduce proof creation. The new prover fixtures add those inputs for synthetic one- and two-Action executions.

Each capture contains the public setup and inputs, witness rows before masking, every 64-bit RNG draw, and the received field challenges. It records the prover’s messages in order: commitments, polynomial evaluations, and multi-opening and IPA points and scalars. It also records whether proving succeeded or failed, alongside Rust’s original proof bytes. Rust checks that recording preserves the proof bytes and the number of random draws consumed.

We replay proof creation in Lean using the captured witness rows, randomness, and challenges. We reconstruct each 512-bit sample from eight recorded RNG draws and reduce it modulo . To pass, every emitted point and scalar must match in order. Lean then serializes those values and requires byte-for-byte equality with Rust’s original proof buffer. Expected messages and proof bytes are kept separate from the replay inputs.

A Lean theorem connects the replay code to the reference prover used by the ZK proof for every supplied input. The ZK theorem remains general, covering every allowed witness over the specified randomness distribution.

We use these fixtures to anchor Lean’s prover model to concrete Rust executions. A passing comparison establishes exact agreement on the ordered messages and encoded proof bytes for the captured inputs, randomness, and challenges.

What this establishes

We now have an argument for zero knowledge in the model of Zakura’s optimized prover, mathematically checked in Lean. It covers the complete verifier view and the prover’s randomness, with explicit statistical bounds under the stated assumptions.

As we keep optimizing the prover, this is the privacy guarantee we’ll keep preserving.

Read the Lean proof.