# Formally Verifying Zero Knowledge for Zakura

Earlier this week, we announced a [new version of Common](https://zakura.com/announcements/zakura-1-4-0/),
our cryptography stack for Zcash. Its bundled Ironwood zk-SNARK prover is
roughly 21 times 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.)

This article announces a new Lean formalization of zero knowledge
for our model of the optimized prover shipped with
[Zakura 1.4.0](https://zakura.com/announcements/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.

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](https://en.wikipedia.org/wiki/Fiat%E2%80%93Shamir_heuristic): 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.

The proof compares everything the verifier sees with a simulation that receives
no private witness and accounts for the interaction of messages and randomness
throughout the protocol. The interactive
simulation error is below `2^-238` for one Action (a shielded spend paired with an output) and
below `m * 2^-238` for `m >= 1` Actions, where `m` is the number of Actions.

`2^-238` is roughly the probability of throwing a dart from Earth and hitting
a proton-sized target 30,000 light years away.

## Reproducing the verifier’s view

The interactive _simulator_ receives public inputs, challenges sent by the
verifier, and its own randomness, but no private witness. Its output is close in
distribution to the real prover’s view, which includes commitments, polynomial
evaluations, messages from the inner product argument (IPA), received
challenges, and failure status.

Statistical indistinguishability means that any party trying to distinguish
real and simulated transcripts has nearly the same probability of answering
“real” in either case, even with unlimited computation. The simulation-error
bound limits the difference between those probabilities.

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.
PLONK and IPA must be simulated jointly because their commitments and opening
proof depend on the same polynomials. The comparison must include the
correlations among messages. For Fiat–Shamir, transcript hashing is modeled
as a classical programmable random oracle, and the comparison includes the
adversary’s oracle queries and responses alongside the proof.

## 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
`R(X) = a + bX`, with independently sampled field coefficients `a` and `b`;
`X` is the polynomial’s input. Revealing the line’s value at one point leaves
randomness to hide the combined opening evaluation at a second distinct point.

The sparse IPA mask places eleven independently sampled coefficients at
power-of-two degrees `1, 2, 4, ..., 1024`. A derived constant makes it zero
at the opening point, preserving 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.
This scalar calculation is part of the joint simulation of the complete view.

## Accounting for the randomness

A random tape supplies the sequence of 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](https://en.wikipedia.org/wiki/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 `p`, the scalar-field modulus and prime number of field values.
The tradeoff is a tiny sampling bias: since `p` does not divide `2^512`,
some field values are slightly more likely than others.

For uniform input bits, let `delta` be the statistical distance from a
uniform field element and `r` the remainder when `2^512` is divided by `p`:

`delta = r*(p-r)/(p*2^512) <= 2^-260`.

For `m` Actions, the full schedule uses `148m + 46` private field samples.
The error bound accounts for the accumulated sampling bias and exceptional
challenges: rare verifier values, such as zero, that disable a mask or make
an inversion undefined. Their total probability is included in the bound.

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 outputs 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

For the [interactive theorem](https://github.com/zakura-core/ironwood-formal-verification/blob/e697bd4ace8559249d5362751397e03d2bc10773/Zcash/Snark/ZeroKnowledge/ActionWitnessSimulation.lean#L34), fix the public inputs.
The test `D` labels a verifier view “real” by returning 1, and `Pr[...]` denotes
probability. The complete view retains emitted messages, received challenges,
the verifier tape, and failure status. Every such test satisfies
`abs(Pr[D(real)=1] - Pr[D(simulated)=1]) <= epsilon(m)`, where for `m >= 1`:

`epsilon(m) < m * 2^-238`.

This bound includes exceptional challenges and accumulated sampling bias.
For one Action, `epsilon(1) < 2^-238`. With equally likely real and simulated
sources, a test can guess the source with probability at most
`1/2 + epsilon(m)/2`.

The [Fiat–Shamir theorem](https://github.com/zakura-core/ironwood-formal-verification/blob/e697bd4ace8559249d5362751397e03d2bc10773/Zcash/Snark/ZeroKnowledge/ActionFiatShamir.lean#L66) uses the classical
programmable random-oracle model and a simulator that draws its private
field values exactly uniformly; the real prover uses wide reduction. Let `q`
be the maximum number of oracle queries before the attempt. The simulation-error bound is:

`epsilon_FS(m,q) = epsilon(m) + q/p < m * 2^-238 + q/p`.

Since `p > 2^254`, the extra term satisfies `q/p <= q * 2^-254`.
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](https://github.com/zakura-core/ironwood-formal-verification/blob/e697bd4ace8559249d5362751397e03d2bc10773/Zcash/Snark/ZeroKnowledge/OracleBitBounds.lean#L19)
also reduces 512-bit samples modulo `p`, adding `(132m + 36)delta` to the displayed
bound. The conservative upper bound `m * 2^-238 + q/p` holds for both simulators.

## Completeness

Completeness asks whether a valid witness produces a proof the verifier accepts.
Our model uses 2,048 circuit rows per Action and 11 IPA rounds (`k = 11`).
The formalization reuses the existing [Action circuit completeness proof](https://github.com/zakura-core/ironwood-formal-verification/blob/86e3c7026db8c9af27ca731e6b5c7f2d8fc7f0fc/Zcash/Circuits/Action/Bundle.lean#L2547)
to show that witnesses built as specified produce rows that satisfy the
circuit. The [application-witness connection](https://github.com/zakura-core/ironwood-formal-verification/blob/e697bd4ace8559249d5362751397e03d2bc10773/Zcash/Snark/ZeroKnowledge/ActionWitnessSimulation.lean#L25)
lets both ZK results apply to Action witnesses.

We also prove that
[a valid witness produces an accepted proof with high probability](https://github.com/zakura-core/ironwood-formal-verification/blob/22dfee003b639eff660f68ea69a98a00409a9cb1/Zcash/Snark/ZeroKnowledge/ActionProverCompleteness.lean#L110). The failure bound covers attempts
that stop early and completed proofs rejected by the modeled verifier,
including rare failures from exceptional challenges. Perfect completeness
would require acceptance probability exactly one.

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 `p`. 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](https://github.com/zakura-core/ironwood-formal-verification/blob/2e9e398d3b339d8233f13dc84bdb190ca2ad774e/Zcash/Snark/Fixtures/Prover/Replay.lean#L48) 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](https://github.com/zakura-core/ironwood-formal-verification/blob/establish-zk/Zcash/Snark/ZeroKnowledge/README.md).

The cream-and-pink illustration compares statistically indistinguishable real
and simulated verifier views for the same public input. The simulator never
receives the private witness.

Sources:

- [Fixed prover description](https://gist.githubusercontent.com/ebfull/bf25819afa697e39b54bd5f1a1992a2c/raw/589528c0f752112fd83c42aeeea91b6958e67605/zk.md)
- [Pinned Zakura prover implementation](https://github.com/zakura-core/common/blob/50f712ee22ca95e2dd5230c6f331ce2e433d70ee/crates/halo2_proofs/src/plonk/prover.rs)
- [Current proof map and theorem boundaries](https://github.com/zakura-core/ironwood-formal-verification/blob/establish-zk/Zcash/Snark/ZeroKnowledge/README.md)
- [Existing Action circuit completeness proof](https://github.com/zakura-core/ironwood-formal-verification/blob/86e3c7026db8c9af27ca731e6b5c7f2d8fc7f0fc/Zcash/Circuits/Action/Bundle.lean#L2547)
- [Exact wide-reduction sampling bias](https://github.com/zakura-core/ironwood-formal-verification/blob/e697bd4ace8559249d5362751397e03d2bc10773/Zcash/Snark/Soundness/Oracle/Challenge255.lean#L53)

---

Canonical HTML version: https://zakura.com/engineering/ironwood-zero-knowledge/