Halo 2 Guide
The Halo 2 proof system, from arithmetisation to recursion
Abstract
This volume of The Zcash Arboretum develops the proof system that Orchard uses: Halo 2, the argument by which the author of a shielded Action convinces every validator that the Action is well formed while disclosing nothing about the note, the key, or the Merkle path behind it. It assumes the Math Guide, whose finite fields, polynomials and evaluation domains, elliptic curves, and probability are used throughout without re-derivation, and the Crypto Guide, whose definitions it instantiates rather than restates: arguments of knowledge and zero knowledge, the Fiat–Shamir transform, Pedersen vector commitments, and the polynomial-commitment interface with its compilation recipe.
The running example is knowledge of with over the field , a size at which every number of the example can be checked by hand; every number is computed by script. The volume reduces the example to a grid of gates, the grid to polynomials, the polynomials to a single identity, and the identity to one evaluation at a random point, at which the prover must open a commitment without sending the committed polynomial. The inner-product argument (IPA) that performs the opening has a section of its own: the problem stated without machinery, one fold written out step by step, the recursion from the prover’s and the verifier’s side, the verifier’s structured scalars, the extraction from three transcripts that proves the argument knowledge sound under the discrete-logarithm assumption on Vesta, with the hash that derives the generators modelled as a random oracle, the blinders and what they do not hide, and the running example opened on a curve of prime order . The deployed proof system follows: the Action circuit’s arithmetisation, the binding of the public statement, the Fiat–Shamir transcript, the reduction of many openings to one, the complete protocol, and its zero knowledge. The volume then analyses the knowledge soundness of the Fiat–Shamir-compiled argument, lists the verifier’s checks on the running example in the order he performs them, and closes with recursive composition and accumulation, which Orchard does not deploy.