Formalize Ironwood zero knowledge in Lean

[TalDerei]

Formalizes both statistical honest-verifier zero knowledge (HVZK) for the interactive protocol and statistical zero knowledge (ZK) for its Fiat–Shamir transform in the classical programmable random-oracle model for the fixed Ironwood protocol, using the pinned prover description and the existing Lean definitions at base ad4a6ad8f75a64368bae4186006480410a687cce. The development lives in Zcash/Snark/ZeroKnowledge and is included in the default build and trust census.

The failure model follows Zakura 1.4.0: identity points return errors and a zero IPA round challenge panics, with no automatic retry. This differs from the pinned description's fresh-randomness retry behavior.

The joint PLONK/IPA simulator covers the sparse power-of-two IPA mask (Common #225) and the linear evaluation mask (Common #267), including their correlations with the commitments and other prover messages. The sampling model reduces independent uniform 512-bit integers modulo the scalar-field order. It proves the exact reduction bias instead of assuming uniform field blinds or rejection sampling.

m is the number of Actions. 148m + 46 counts the prover's private random field elements for one proof attempt, used to mask witness data and blind commitments.

For one interactive reference prover attempt with m Actions and eleven IPA rounds, the compiler-derived theorem gives a simple guarantee: any test of the verifier's view has probabilities differing by at most epsilon(m) between the real prover and the witness-free simulator, under the explicit assumptions below.

$$ \varepsilon(m) = \frac{42882m + 4113}{p} + (148m + 70)\delta < m \cdot 2^{-238}, \qquad m \ge 1. $$

$$ \delta = \frac{r(p-r)}{p \cdot 2^{512}} \le 2^{-260}, \qquad 2^{512} = Qp + r. $$

Here p is the scalar-field order and r is the remainder when dividing 2^512 by p.

• Rare exceptional cases: (42882m + 4113)/p bounds the contribution from events such as zero denominators and exceptional verifier challenges.
• Bias of one sample: delta is the exact statistical distance between one uniform 512-bit integer reduced modulo p and a uniform field element.
• Accumulated sampling bias: (148m + 70) delta adds the sampling-bias costs across the proof's distribution comparisons.

Thus delta measures one sample's bias; epsilon(m) bounds the total simulation error. The bound grows linearly with the number of Actions. For one Action, the simulation error is below $2^{-238}$, with most of that allowance coming from the exceptional-case term. This establishes statistical closeness for the reference experiment.

The development connects the statistical comparison to the Action circuit and constructs the required circuit rows from application witnesses. It discharges the masking, compiler, commitment-routing, and encoding conditions for the specified reference prover. The simulator uses public data and has no witness argument.

Completeness:

The new application-witness bridge uses Ironwood’s existing Action circuit completeness theorem to establish valid circuit rows from witnesses satisfying the stated construction conditions. Our ZK capstones then apply to those rows: interactive statistical HVZK and Fiat–Shamir statistical ZK, the latter in the classical programmable random-oracle model.

The theorem wideActionWitness_completeness_error_bound shows that a valid witness produces an accepted proof except with an explicitly bounded failure probability. The event counts both aborted attempts and completed proofs rejected by the existing typed verifier.

For m >= 1 Actions, under the stated witness, setup, and independent uniform-bit-tape assumptions, the completeness bound is:

$$ \eta(m) = \frac{42904m + 8271}{p} + (296m + 160)\delta < m \cdot 2^{-238}, \qquad m \ge 1. $$

Here p and delta are as above, with $\delta \le 2^{-260}$. Acceptance is at least $1 - \eta(m)$; for one Action, the abort-or-rejection bound is below $2^{-238}$. This is completeness with high probability: perfect completeness would require acceptance probability exactly one, while permitted exceptional challenges can cause failure.

The conservative budget adds the honest emission-failure bound, the real-to-simulator error, and the simulator’s exceptional-challenge bound. The acceptance proof and numerical certificates are included in this branch; full-build validation is still in progress. This addition concerns the interactive reference prover at the repository’s existing typed, post-decode verifier boundary.

Assumptions and scope:

The statistical results assume witnesses satisfying the application construction conditions, the stated setup, and fresh independent uniform input bits. The interactive experiment uses an independent verifier tape; the Fiat–Shamir ZK theorem uses a classical programmable random oracle and its own error bounds. Results for seeded generators rely on the stated PRNG security assumptions and include their distinguishing advantage. See the proof map and theorem boundaries for the exact endpoints and premises.

The application-witness builder stores each of the five Fq scalars as two 128-bit Fp limbs and reconstructs its natural representative before computing scalar windows. Exact decoding covers the full Fq range, including representatives at or above |Fp|, without an additional scalar-hint bound.

The release provenance records the identity-product shortcut's exceptional divergence from the reference scan and its 2042m/p + delta comparison allowance. The displayed bounds are the Lean reference-model bounds.