III Halo 2 Guide: The Halo 2 proof system, from arithmetisation to recursion III Halo 2 Guide: The Halo 2 proof system, from arithmetisation to recursion 2 Arithmetisation: from a computation to committed polynomials

1 Introduction

1.1 Scope and layering

This is the third volume of The Zcash Arboretum, and it develops the cryptography behind Zcash’s Orchard protocol: the proof system Halo 2, with which every Orchard Action carries a zero-knowledge proof of its own well-formedness. The protocol specification fixes that use: Halo 2 is used with the Vesta curve (the Math Guide, §“Pallas and Vesta assembled”) to prove and verify the Orchard Action statement (protocol specification § 4.1.13, “Zero-Knowledge Proving System”), and the proving system is defined by reference to the halo2 book (§ 5.4.10.3, “Halo 2”). The statement itself (§ 4.18.4, “Action Statement (Orchard)”) is read in §1.2. Actions of the Orchard pool and of the Ironwood pool, the second shielded pool of Orchard-protocol notes, prove this statement, extended at NU6.3 by one public bit, $\mathsf{disableCrossAddress}$ , that when set forces the new note’s address to equal the spent note’s, with one circuit and one verifying key (protocol specification, § 4.6, “Action Descriptions”; ZIP 229; ZIP 258), so the proof system and proof format described here serve both pools.

The two volumes below this one built its material from the ground up. The Math Guide constructed the mathematics: finite fields, elliptic curves, polynomials and evaluation domains, probability. The Crypto Guide constructed the cryptographic primitives: hash functions, commitments, $\Sigma$ -protocols and the Fiat–Shamir transform, zero knowledge, polynomial commitment schemes. This volume assumes all of these and defines none of them afresh; it assembles them into a proof system. In particular the Crypto Guide owns every definition this volume instantiates: the non-interactive argument and the SNARK, together with the polynomial interactive oracle proof and the compilation recipe that turns one into the other (§“SNARKs: succinct non-interactive arguments of knowledge”); the Fiat–Shamir transform (§“The Fiat–Shamir transform: from interactive to non-interactive”); the Pedersen vector commitment (§“Pedersen vector commitments”); and the polynomial-commitment interface, with its sketch of an inner-product opening (§“Polynomial commitment schemes”). Where a lower volume’s result is needed it is cited at the point of use, by italic volume name and section title: the volumes are separate documents, so there is no cross-document reference, and this volume forward-references only its own later sections.

1.2 The running example and the security notions

The running example is the statement

\text{knowledge of }x\in\mathbb{F}_{97}\text{ with }x^{3}+x+5=35,

one of whose witnesses (the Crypto Guide, §“Languages, relations, and witnesses”) is $x=3$ , since $27+3+5=35$ ; the others in $\mathbb{F}_{97}$ are $18$ and $76$ , and the prover of the example holds $x=3$ . It is arithmetised in §2, committed and opened in §3, bound to its public input $35$ and compiled into a proof string in §4, and verified in §6. Its field arithmetic, that of the claim, the grid, the polynomials and every scalar, is in the prime field $\mathbb{F}_{97}$ (the Math Guide, §“The prime field and two inversion routes”), a size at which every product can be checked by hand; the commitments of §3 are points of a curve of order $97$ whose coordinates lie in a second prime field, $\mathbb{F}_{79}$ . Every number printed is computed by script, and the script’s output is the source of the text.

A proof system for such a statement is required to have three properties, each a definition of the Crypto Guide (§“Interactive proofs, zero knowledge, and SNARKs”) used here without restatement. Overwhelming completeness: an honest prover holding a witness is accepted with overwhelming probability, in the sense of the Math Guide (§“Polynomial, exponential, and negligible functions”). Knowledge soundness (the Crypto Guide, §“Knowledge soundness and extractors”): an efficient extractor, given rewindable access to any prover the verifier accepts with non-negligible probability, outputs a valid witness. Zero knowledge (the Crypto Guide, §“The simulation paradigm and zero knowledge”): a simulator given only the public input produces transcripts indistinguishable from those of real executions.

The volume establishes these properties to different extents. Design-stage claims are classified in three grades: specified, when the protocol specification or a ZIP states the property; designed-but-unspecified, when the design intends it but no specification, ZIP or theorem of this volume states it for the deployed system; and open problem, when no design is known to achieve it. The Halo 2 protocol is complete except with negligible probability: for each random challenge, a number of values at most proportional to the size of the circuit, out of the $|\mathbb{F}|$ possible, makes undefined a division that the verifier or the honest prover performs; §4.6 lists these degenerate challenges once the protocol is defined. The inner-product opening argument is knowledge sound under the discrete-logarithm assumption on Vesta, with the hash that derives its generators modelled as a random oracle (Theorem 3.5 and, for the deployed opening, Corollary 3.13). Knowledge soundness of the deployed non-interactive argument rests on an analysis in the algebraic group model and the random-oracle model whose instantiation to the deployed transcript is designed-but-unspecified (§5). Zero knowledge is recorded in §4.6 from the halo2 book’s claim for the interactive protocol, under the composition and Fiat–Shamir hypotheses stated there.

The running example has the form of the Orchard Action statement. The prover of an Action shows knowledge of a note, the keys that control it, and a Merkle path such that the note’s commitment is well formed, the path, unless the spent value is zero, leads from that commitment to the published tree root (the Crypto Guide, §“Merkle trees and commitments to sets”), the net value commitment is a Pedersen commitment to the old value minus the new value (the Crypto Guide, §“The Pedersen commitment”), the nullifier, the unique tag whose publication marks the note spent, is computed correctly, and the key that authorises the spend is a re-randomisation of the owner’s key (the Crypto Guide, §“Key re-randomisation and unlinkability”). The protocol specification states this as nine conditions on a public input and a private witness (§ 4.18.4, “Action Statement (Orchard)”), the five just paraphrased and four further: that the spent note’s address is derived from the same keys, that the new note’s commitment is well formed, and that two public bits, when zero, force the spent value and the created value, respectively, to zero. From NU6.3 the circuit checks a tenth condition on a further public bit, which restricts cross-address transfers and is set for every Orchard-pool Action (§ 4.6; ZIP 258). Each condition unfolds into small arithmetic facts over the field $\mathbb{F}_{p_{\mathsf{Pallas}}}$ (the Math Guide, §“Base fields, scalar fields, and the Pasta cycle”): the note commitment alone is a Sinsemilla commitment, a Sinsemilla hash to a point plus a blinding multiple of a fixed generator (the Crypto Guide, §“Sinsemilla: an algebraic hash-based commitment”), whose hash is evaluated in the circuit with the help of a lookup table. Together the conditions are laid out on the $2^{11}=2048$ rows of the deployed Action circuit; the lookup table and the row count are given in §4, “From statement to circuit: arithmetisation in practice”. The running example itself is a conjunction of four arithmetic facts, $x\cdot x=x^{2}$ , $x^{2}\cdot x=x^{3}$ , $x^{3}+x=s$ and $s+5=35$ , one per row of the grid that §2 builds. Both the toy and the Action circuit are instances of the constraint system that §2 defines; the toy’s constraint on each row reads that row alone and consults no table.

The chain of reductions.

Five reductions connect the claim to the checks the verifier performs.

1.

Computation $\to$ grid (§2, “From computation to a grid of constraints”). The claim is rewritten as a table of rows, each row one elementary gate ( $\times$ or $+$ ), with copy constraints between rows forcing shared values.
2.

Grid $\to$ polynomials (§2, “From the grid to polynomials”). Each column of the table is interpolated into a polynomial (the Math Guide, §“Lagrange interpolation”). The condition that every row obeys its gate becomes the condition that one polynomial $G(X)$ is zero at every row.
3.

Vanishing $\to$ identity (§2, “From vanishing to a single identity”). The statement that $G$ is zero at every row becomes the algebraic identity $G(X)=t(X)\,Z_{H}(X)$ for some quotient $t$ , where $Z_{H}$ is the vanishing polynomial of the set $H$ of row names (the Math Guide, §“The evaluation domain $H$ and its vanishing polynomial”). A trace that satisfies every gate yields such an identity, and a trace that violates a gate cannot. The copy constraints are not part of $G$ ; the permutation argument enforces them (item 5).
4.

Identity $\to$ one random check (§2, “Why checking one random point is a proof”). The verifier tests the identity at a single random point $z$ . A false identity holds at a uniformly random point with probability at most its degree divided by the field size (the Math Guide, §“The Schwartz–Zippel lemma”).
5.

Random check $\to$ committed openings. A binding commitment (the Crypto Guide, §“Hiding and binding”) prevents the prover from changing her polynomials after $z$ is drawn (§2, “Why the prover cannot wriggle: binding commitments”), and the inner-product argument (IPA) of §3 opens a commitment at $z$ without sending the polynomial; the permutation argument enforces the copy constraints (§2, “Enforcing the wiring: the permutation argument”); a dedicated public column, the instance column, fixes the public input $35$ (§4, “Instance columns and binding the public statement”); and blinding hides the witness (§4, “Zero knowledge: hiding the witness in Halo 2”).

Section 6 composes the five reductions into one chain of implications, from the verifier’s accepted checks back to the claim.

The scale caveat, stated once.

The field $\mathbb{F}_{97}$ is a toy. Over Orchard’s field $\mathbb{F}_{p_{\mathsf{Pallas}}}$ , whose prime has $255$ bits, a fixed false identity of degree around $2^{14}$ (the degree of the deployed constraint polynomial, bounded in §4, “The complete Halo 2 protocol”) survives one fresh uniform evaluation challenge with probability around $2^{14}/2^{254}=2^{-240}$ , in place of the visible $3/97$ that §2 exhibits for the toy’s cheat. Every such number in this volume is one Schwartz–Zippel term: the probability that one random point hides one fixed lie. It is not the security level of the complete proof system, which also rests on the binding of the commitments, the extractor of the opening argument, and the loss of the Fiat–Shamir transform, treated in §3, §4 and §5. The caveat is stated here and not re-derived; every probability printed later is read with it.

1.3 Outline

The sections follow the running example; Figure 1 shows the section in which each stage is built.

Section 2 takes the example from the computation to committed polynomials: the grid, the column polynomials, the single identity, the random point, and then the general form of the constraint system, PLONKish arithmetisation, of which the toy is an instance, followed by the permutation argument for the copy constraints and the lookup argument for facts that no low-degree gate states economically. It ends with the problem a vector commitment alone does not solve: proving the value of a committed polynomial at $z$ without sending the polynomial, in fewer group elements than the polynomial has coefficients.

Section 3 solves that problem with the inner-product argument. It states the inner-product problem without machinery, works one fold with every algebra step written out, gives the recursion with both parties’ computations side by side, makes the verifier’s work explicit, proves the argument knowledge sound by extraction from three transcripts under the discrete-logarithm assumption with uniform generators, separates what the blinders hide from what they do not, and opens the example’s own polynomial through every round on a curve of prime order $97$ , by script. Its last subsection gives Halo 2’s parameters, the deployed form of the argument as a change of variables, the bytes of a proof, the deferred multi-scalar multiplication and the batching that amortises it, and accumulation, which Orchard does not deploy.

Section 4 gives the deployed proof system: the Action circuit’s arithmetisation, the instance column that binds the public statement, the Fiat–Shamir transform that replaces the verifier’s challenges by hash outputs, the reduction of many openings to one, the complete protocol in seven phases, its zero knowledge, and the compiled-polynomial-IOP pattern the protocol instantiates.

Section 5 treats knowledge soundness of the non-interactive argument: the extractor of §3 when the challenges are hash outputs, the algebraic group model in which the halo2 book proves its tight bound for the analysed protocol, and the gap between concrete and asymptotic security.

Section 6 lists the verifier’s checks on the running example in the order he performs them, the chain of implications back to the prover’s knowledge of advice satisfying every gate and every copy constraint, and the same chain at Orchard scale.

Section 7 treats recursive proof composition, accumulation schemes, the Halo trick, and the cycle of curves that makes native recursion efficient. Orchard proves with Halo 2 on the Pasta curves but does not recurse, and the section states at the outset that Orchard does not deploy its material.

Refer to caption — Figure 1: The running example’s path through the volume, each stage tagged with the section that owns it. The claim is fixed in this section (green). The grid of gates, the column polynomials, the single identity $G=t\,Z_{H}$ , the random point $z$ and the binding commitment are built in §2 (blue). The commitment is opened by the inner-product argument in §3 (red). The transcript hash, whose outputs replace the verifier’s challenges, and the proof string are produced in §4 (amber). Section 6 reads the chain backwards, from the accepted proof string to the claim.