This section states recursive proof composition and accumulation for the inner-product argument; Orchard deploys neither. The protocol specification uses Halo 2 for one purpose, to prove and verify Action statements (protocol specification, § 4.1.13, “Zero-Knowledge Proving System”), and requires every Action proof to be valid (§ 4.6, “Action Descriptions”); the design proposal that introduced the pool states that it makes no use of the proof system’s support for recursive proofs (ZIP 224, under “Proving system”). A verifier holding several proofs may still check them together. The complete verification equation of each proof is a multi-scalar multiplication over all generators that should evaluate to (§3.8.1, “Batch verification”); for independent uniform the verifier of proofs checks instead. If some , then generates the group of prime order, so for any fixed values of the other factors exactly one satisfies the combined check, and a false batch passes with probability (Lemma 3.14). Batch verification verifies the batch and emits nothing; it is not the accumulation developed here. In the classification of §1.2, the Pasta curves and the use Orchard makes of them (§7.4) are specified; recursion and accumulation over those curves are designed-but-unspecified: their constructions are published and the halo2 book describes them (Recursion chapter), and ZIP 224 leaves them to future protocol updates, but no specification defines a recursive statement or an accumulation rule for Zcash. Theorem 7.4 and Proposition 7.5 below are theorems, the first cited and the second proved.
Consider a computation iterated many times,
one step applied times to an initial state, and suppose a verifier wants to be sure that is the honest result without recomputing the steps. Valiant’s incrementally verifiable computation asks for a proof of that is updated step by step, each update costing about one step’s worth of proving and the finished proof no larger than the proof of a single step. The more general setting, in which computations branch and merge and each step consumes the proofs of its predecessors, is the proof-carrying data of Chiesa and Tromer: every message in a distributed computation carries a proof that it was produced correctly from messages that themselves carried such proofs.
The natural construction is recursive proof composition: proving, inside one proof, that another proof verifies. Write for the verifier of a non-interactive argument (Crypto Guide, §“SNARKs: succinct non-interactive arguments of knowledge”), and suppose its algorithm is itself arithmetised, in the sense of §2, into a PLONKish circuit of Definition 2.7, the verifier circuit: its instance columns hold the statement and its advice columns hold a proof, and its gates are satisfiable exactly when accepts that proof of that statement. At step the prover proves the compound statement
“, and there exists a proof that the verifier circuit accepts for the statement of step .”
The proof is advice of the step- circuit, never sent onward; the proof that results attests to step and, through the embedded verifier, to , hence to step , and so on down to . One proof attests to the entire history, and the cost of producing is the cost of one step of plus one run of the verifier circuit, independent of how long the history is. The requirement on which everything rests is the one just used: the argument’s verifier must be efficiently expressible as a circuit. A verifier whose circuit is as large as the computation it checks would make each step as expensive as the whole history, and the construction would buy nothing.
The classical instantiations meet that requirement badly, in two different ways.
Pairings in a circuit, and a ceremony. The pairing-based systems, Groth16, which Sapling deploys, and PLONK compiled with the KZG commitment (Crypto Guide, §“SNARKs: succinct non-interactive arguments of knowledge” for Groth16 and the bilinear pairing; §“Polynomial commitment schemes”, under “KZG: evaluation in the exponent”), have constant-size proofs and verifiers that run in time independent of the circuit. But those verifiers evaluate pairings, and a pairing lands in a target group that lives in an extension field of the curve’s base field, of degree equal to the curve’s embedding degree (Crypto Guide, §“Instantiation on elliptic curves; the Pasta curves”, the large-embedding-degree criterion). A circuit whose native arithmetic is one prime field must emulate arithmetic in another field with many gates per operation, so a pairing is costly to express inside a circuit. These particular systems also need a trusted setup, the ceremony that §3.8.1 contrasted with hashed generators.
A linear-time verifier. The transparent systems built on the inner-product argument of §3 need no pairing and no ceremony, but their verifier is linear in the size of the committed vectors: the one multi-scalar multiplication of length that §3.4 singled out. Inside a verifier circuit that multiplication is scalar multiplications of curve points, each a double-and-add with doublings for an -bit scalar (Math Guide, §“Scalar multiplication and double-and-add”), so the verifier circuit grows linearly in , the length of the committed vectors of the proof it verifies. A linear-time check dominates the verifier circuit and negates the per-step economy that recursion was meant to deliver.
Halo, the construction of Bowe, Grigg and Hopwood (Halo: Recursive Proof Composition without a Trusted Setup) from which Halo 2 descends, defers the linear-time part of verification instead of recomputing it at every step, and uses the inner-product argument, in which no pairing occurs. Bünz, Chiesa, Mishra and Spooner formalised the deferral as an accumulation scheme (Proof-Carrying Data from Accumulation Schemes; BCMS20), the notion the next subsection defines; their Theorem 7.1 is quoted below, without proof, as Theorem 7.4.
The idea is to separate what a verifier must check at each step from what can be checked once, at the end of a chain. Fix a predicate , a property of an input decidable in polynomial time, for example “this inner-product opening is correct” of a transcript of Construction 3.2. An accumulation scheme replaces a sequence of checks of by a sequence of accumulation steps and one run of a decider.
Let be the security parameter (Crypto Guide, §“Adversaries and the security parameter”) and a predicate on inputs . An accumulation scheme for is a triple of polynomial-time algorithms with access to a common random oracle, whose accumulators are bit strings.
The accumulation prover , on input and an old accumulator , outputs a new accumulator and an accumulation proof .
The accumulation verifier , on input , outputs a bit; the bit asserts that correctly accumulates and .
The decider , on input an accumulator, outputs a bit; an accumulator is valid if outputs on it.
The scheme is complete if, whenever , and is an output of on , both and . It is sound if for every adversary of size polynomial in that outputs the probability, over the random oracle and the adversary’s coins, of
is negligible in .
The definition is that of BCMS20 (Section 4.1) with one input and one old accumulator per step; theirs admits any number of each and adds a generator and an indexer, which fix the public parameters and keys left implicit here. For recursion the size of an accumulator must also be bounded independently of the number of inputs accumulated into it (BCMS20, Definition 5.1).
Soundness carries the checks along a chain.
Let be sound in the sense of Definition 7.1, let be valid, and let be polynomial in . For any efficient algorithm producing and , where accumulates and , such that accepts every step and , the probability that for some is at most times the soundness error of the adversary that outputs step for a uniform ; it is therefore negligible.
If some violates , then either is valid and step exhibits the event of the soundness definition, or some later step turns an invalid into a valid and exhibits it. Let be the algorithm that produces the chain and outputs step for a uniform ; since the bad event forces some step to exhibit the soundness event, its probability is at most times the soundness error of , which is negligible because is polynomial (Math Guide, §“Polynomial, exponential, and negligible functions”, the closure properties). □
The verifier of each step runs the accumulation verifier and never the decider. In a recursive chain the accumulation verifier runs inside the circuit of the step’s proof, so the argument also needs the knowledge soundness of each step’s proof, to recover what that circuit checked; BCMS20 prove the resulting proof-carrying data secure for computations of constant depth, which for a chain means constant length, because the extractor is applied recursively once per level (Theorem 5.2 and Remark 5.3).
For an inner-product polynomial commitment such a scheme is known under the hypothesis of Theorem 7.4 below, and it resolves the second obstacle of §7.1 where it arose: the verifier circuit runs the part of the opening check, the rounds, the scalars and the small combinations of points, and accumulates the part, the claim about , into a running accumulator; the decider pays that multi-scalar multiplication once, at the end of the chain. The next subsection defines the accumulator, states the scheme as an interface theorem, and works the fold on the toy curve.
Everything the verifier of Construction 3.2 does to decide the check (15), or its deployed form (29), is logarithmic in : field multiplications for , a combination of the received points and a handful of fixed ones with scalar multiplications, and a comparison of two curve points. The single exception is the evaluation
a multi-scalar multiplication of length over all the generators, which §3.4 named the one linear step and recognised as the unblinded commitment to the polynomial whose value the verifier had just computed cheaply. Verifying an Action proof as the consensus rules require includes that step for every proof; batch verification, recalled at the start of this section, evaluates one combined multiplication for the proofs of a batch, and the batch is verified and nothing survives it. Accumulation takes the same kind of linear combination and does something else with it: it carries the combined claim forward as data, unverified, and pays for it once at the end of a chain. Figure 18 sets the two side by side; the rest of this subsection is the right-hand panel, and none of it is deployed by Orchard.
The claim to be deferred has a fixed shape, and the accumulator is that shape written down.
An accumulator instance is a tuple
a curve point and the round challenges of one opening. It is valid if and only if
| (35) |
with and the structured scalars and the polynomial of Theorem 3.3, in the symmetric normalisation of Construction 3.2. The deferred claim concerns the unblinded commitment: the blinder of the opened commitment was discharged by the term of (15), or the term of (29), and plays no part in it. From here on the unary abbreviates .
The deployed analogue replaces and by their forms in Remark 3.9; Proposition 7.5 and, with verifier-drawn challenges, the closure argument below hold for it verbatim, with Corollary 3.13 in place of Theorem 3.5, since they use only the linearity of the commitment, the degree of and the knowledge soundness of the opening.
A verifier who is handed a point together with the challenges can complete the check (15) in operations provided the tuple is valid; validity is precisely what he has not paid for. The scheme quoted next lets him defer that payment.
Let be the inner-product polynomial commitment of BCMS20 (Appendix A.2), for polynomials of degree below over a group of prime order, and suppose that is a polynomial commitment scheme in the random oracle model, its openings in particular being extractable. Then (BCMS20, Theorem 7.1) there is an accumulation scheme in the sense of Definition 7.1, in the random oracle model, for the predicate “this opening is correct”, whose accumulators are themselves openings, such that:
the accumulation prover runs in time dominated by scalar multiplications in ;
the accumulation verifier runs in time dominated by scalar multiplications in ;
The theorem is quoted as an interface and not proved in this volume. Its hypothesis, the extractability of openings, is stated by BCMS20 as a conjecture from the binding of the Pedersen commitment, the extractor they record for the Fiat–Shamir-compiled opening running in superpolynomial time (BCMS20, Appendix A.3.2). The scheme is neither Construction 3.2, whose fold is symmetric, nor the deployed opening of Remark 3.9, which blinds every commitment and subtracts where adds a multiple of its inner-product generator (the halo2 book’s Comparison to other work chapter); no theorem transferring it to either is proved here or cited, and in the classification of §1.2 that transfer, like accumulation over these curves, is designed-but-unspecified. What an accumulation step does for Construction 3.2, and why its random combination is sound, is worked out below at the level the volume proves things.
Consider a Halo 2 verifier circuit, expressed over the scalar field of one Pasta curve and verifying a proof produced over the other curve, an arrangement whose necessity §7.4 explains. At step of a chain the circuit receives the previous proof , whose opening is an instance of Construction 3.2, and the accumulator exposed as a public input of , of which it uses the instance on the curve is committed on (see below), and does three things.
Run the succinct part. It recomputes the challenges of the opening from the transcript, evaluates with scalar operations, and forms the left-hand side of (15) and every term of the right-hand side except the one on the final generator, here written , with point operations. The point operations are native, since the points of have coordinates in the circuit’s field. The challenges, and the scalar products lie in the scalar field of the curve is committed on, the other Pasta field; they are computed non-natively, or exposed as public inputs and checked by the next circuit of the chain, which is native to that field (“What the cycle does and does not buy” in §7.4; the halo2 book’s Recursion chapter).
Witness the expensive part. It does not compute . The prover of the step supplies the claimed point as advice, and the circuit uses it to complete the check, which is then passed conditionally on the validity of the fresh tuple of that opening.
Accumulate. The step now holds two claims of the shape (35): the inherited instance of and the fresh . For a challenge derived by the random oracle from both tuples, the two reduce to the single claim
| (36) |
whose coefficient vector on the right anyone holding both challenge tuples can recompute. Proposition 7.5 shows that a false input survives the combination for at most one . The step’s prover then opens the combined point at a fresh point, outside the circuit, and the circuit checks that opening succinctly as in item 1; the tuple the opening leaves behind is the new accumulator (over a 2-cycle, its instance on that curve), exposed as a public input of the proof the step produces. The paragraph “Closure: the prover-assisted step” below describes that opening.
Over a 2-cycle of curves (§7.4) the proofs alternate between the two curves, and the accumulator is a pair of instances, one per curve. The step that verifies a proof committed on one curve folds that proof’s fresh tuple into the instance on the same curve, which was last updated two steps earlier and forwarded unchanged by the intervening step, and it forwards the other curve’s instance in the same way, without point arithmetic. Figure 19 draws the chain. At its end a single multi-scalar multiplication of length , run outside any circuit, checks the last accumulator and with it every opening in the history: for the scheme of Theorem 7.4 by Lemma 7.2.
The soundness of the fold (36) is one line of linear algebra in the group.
Let and be two accumulator instances and uniform in , drawn after both are fixed. If both instances are valid, the folded equation (36) holds for every . If at least one is invalid, it holds for at most one value of , hence with probability at most .
Set and , the two errors. By linearity of the commitment (Crypto Guide, §“Pedersen vector commitments”, the remark that linearity survives), , so the left-hand side of (36) minus the right is , and the equation holds exactly when
| (37) |
If both instances are valid, and the equation holds for all . Otherwise two cases. If , then, being cyclic of prime order, generates and the map is a bijection (Math Guide, §“The mixed inner product with group elements”, the one-dimensional vector space over ), so exactly one sends to : the discrete logarithm of to the base , which exists whether or not anyone can compute it. If , then and (37) holds for no . A uniform hits the at most one bad value with probability at most . □
The fold is run on the -point curve and the four generators of §3.7, with and the symmetric structured scalars of Theorem 3.3, on two challenge tuples, with and , and with and , both valid by construction, for every . With both instances valid the folded equation (36) holds for all values of . Spoiling an instance by adding a nonzero multiple of to its point makes its error a nonzero point, and the surviving values of are counted again. With the first instance false and the second valid, no survives: this is the case of the proof. With the second false and the first valid, exactly one survives, , the value that discards the second instance altogether. With both false exactly one survives, , the discrete logarithm of to the base on this curve, where such logarithms are a short search. In every spoiled case the count is at most one of : the bound of Proposition 7.5, attained.
The folded claim (36) is not an accumulator instance. Its coefficient vector is in general not the structured vector of any single challenge tuple, so carrying it means carrying both tuples, and after folds all of them: the decider would still pay one multiplication of length , but the accumulator would grow with the chain, against the size bound that recursion requires (§7.2). The tuple type of Definition 7.3 is therefore not closed under verifier-side linear combination alone. It is closed under one more step, which the prover assists. Write for the combined point and for the combined polynomial, of degree below . The combined claim says exactly that . The step’s prover opens by the opening protocol of Construction 3.2 at a fresh point , derived by the random oracle from and both tuples, claiming the value , which the verifier computes for himself in field operations from the two tuples, since and are each a product of factors. That opening does two things at once. First, it carries the combined claim up to a blinder.
Under the hypotheses of Theorem 3.5, let , and the opening’s challenges be drawn uniformly by the verifier, in this order, after the two tuples are fixed. There is an extractor which, given rewindable access to a step prover accepted with non-negligible probability, runs in expected polynomial time and outputs either blinders with and , or a nontrivial discrete-logarithm relation among , , , . Its knowledge error is .
By Theorem 3.5 the opening yields a representation , unique since a second one would be a discrete-logarithm relation among and , and certifies for the polynomial with coefficient vector ; two polynomials of degree below that differ agree at a uniform , drawn after was fixed, with probability at most (Math Guide, §“The Schwartz–Zippel lemma”), so except with that probability is the coefficient vector of and . The blinder is the prover’s and need not be . Rewinding the choice of and extracting again at a second value gives representations of and of , whose difference is ; solving yields and for blinders that the extractor computes. This is the argument of Proposition 7.5 applied to the -coordinates of the representations: a combination correct at two values of has both errors zero. It is all the chain needs: a tuple whose point is still certifies the opening it came from, because, writing for the final scalar that (15) calls ,
so that opening satisfies the honest check with the blinder in place of , and Theorem 3.5 applies to it; in (29) the offset joins the term likewise. The chain thus carries the claim that each deferred point’s -coordinates are ; the exact equality (35), blinder included, is required only of the last accumulator, which the decider checks and an honest prover satisfies. An intermediate tuple may miss (35) by such a multiple without any opening it serves being false. □
Second, the opening leaves behind a deferred claim of the atomic form: it ends, as every opening does, in a point and challenges that the verifier circuit witnesses rather than computes. The accumulator after the step is again one tuple. This is the accumulation step of BCMS20 (Section 7.1), which likewise derives the combining challenge and the fresh point by the random oracle from the tuples and the combined point; there the accumulator is the opening itself, and its succinct part runs at the next step. With , and the opening’s challenges drawn by a verifier, the step’s soundness is Proposition 7.7. With random-oracle challenges, the step’s soundness is BCMS20’s Theorem 7.1 for under its conjectured extractability (Theorem 7.4); for Construction 3.2 it is designed-but-unspecified.
The deferred equation (35) is a claim of commitment equality, equivalently a claim about the value of one multi-scalar multiplication, for a coefficient vector that is public and structured: anyone holding the challenges can write it down. It is not itself an evaluation opening; no polynomial is being evaluated at any point when the decider runs, only a point recomputed and compared. The accumulation protocol reduces this claim, and carries it along the chain, through the prover-assisted opening just described, which turns each commitment equality into one evaluation claim at a fresh point and each opening back into one commitment equality. The Orchard verifier, once more, does none of this: it computes and compares.
The verifier circuit of §7.3 was “expressed over the scalar field of one Pasta curve and verifying a proof produced over the other”. This subsection explains why the two curves are needed, what the arrangement buys, and where Orchard already uses half of it.
A curve over a prime field has two fields attached to it (Math Guide, §“Base fields, scalar fields, and the Pasta cycle”): the base field, in which its points’ coordinates lie and in which the group law’s slopes, squarings and inversions are computed, and the scalar field, the integers modulo the prime order of its group, in which the scalars of live. Write for a curve over and for its prime order, so that its base field is and its scalar field . A PLONKish circuit of Definition 2.7 is defined over one prime field , its native field: its cells hold elements of and its gates are polynomial identities over , so an addition or multiplication in costs one cell or one gate. Arithmetic in any other prime field is non-native: an element of the other field must be carried as several -cells, each range-checked by the lookups of §2.7, and each of its operations becomes many gates with carries and reductions. Which field a circuit is native to is not a free choice. Its column polynomials are committed with the inner-product commitment of §3 on some curve, and a Pedersen commitment to a vector of -elements needs a group whose scalar field is ; so the native field of a circuit is the scalar field of the curve its proof is committed on, exactly as the Action circuit, native to , is committed on Vesta, whose order is (§3.8).
Take a proof committed on . Its group elements, the column and quotient commitments, the cross terms and the deferred point of its opening, are points of with coordinates in . The in-circuit folding of §7.3 adds and scales such points, which is base-field arithmetic in , so a verifier circuit handles them natively only if its native field is . But a circuit committed on is native to the scalar field : its challenges, its structured scalars and every field operation of the succinct part are -arithmetic. One curve would host both jobs only if , that is, . Curves with exactly points exist; by Hasse’s theorem (Math Guide, §“The group structure of ”), which writes with the trace , they are the curves with , called anomalous. On an anomalous curve the discrete logarithm is computable in polynomial time, the attack of Smart, of Semaev and of Satoh and Araki, and the Crypto Guide lists “not anomalous” among the criteria a curve must meet to be used at all (§“Instantiation on elliptic curves; the Pasta curves”, the anti-Smart criterion). So no secure curve has , and no one curve can host both the coordinates of its proofs and its own verifier circuit natively.
The efficient resolution uses two curves that trade fields. A 2-cycle of elliptic curves is a pair with
both primes: the scalar field of each curve is the base field of the other. Then:
a circuit committed on has native field , the scalar field of ; and is the coordinate field of , so that circuit manipulates the points of a proof produced over natively, and verifies such a proof at the cost §7.3 counted, the proof’s scalars aside;
the proof that circuit produces is committed on , and its points have coordinates in , the native field of a circuit committed on ; so a circuit over handles its points natively in turn;
the proofs of a chain alternate between the two curves, each step handling its predecessor’s points natively (Figure 20).
The cycle makes the preceding curve’s coordinate arithmetic native; it does not identify the two scalar fields, which remain distinct primes. Challenges squeezed in the previous proof’s field and the scalars derived from them are -elements that the -native circuit must handle: they need compatible encodings across the two fields, range checks where an element of the larger field is carried in the smaller, and, where a genuine multiplication is unavoidable, non-native scalar arithmetic. Nor is the cycle a logical necessity. A single curve could verify its own proofs with non-native coordinate arithmetic throughout, at a cost of many gates per point operation multiplied by the point operations of the succinct part; that is possible and substantially more expensive. The cycle is the efficient native design, not the only correct one.
The Pasta cycle of the Math Guide (§“Base fields, scalar fields, and the Pasta cycle”; §“Pallas and Vesta assembled”) is a 2-cycle: Pallas is defined over with group order , and Vesta over with group order , both curves (protocol specification, § 5.4.9.6, “Pallas and Vesta”). The cycle follows from the specification’s two primes and nothing else. With
the point lies on Pallas, there, and exactly one multiple of lies in the Hasse interval for . That settles the order: the order of the point divides the prime and is not , so it is , which therefore divides by Lagrange’s theorem (Math Guide, §“Cosets and Lagrange’s theorem”); the group order lies in an interval of length , far shorter than , which contains one multiple of ; hence . The symmetric check on Vesta shows that the Vesta group has order . The traces are
each far inside the Hasse bound and neither equal to : neither curve is anomalous, as the Crypto Guide’s criterion requires. The two traces sum to , as they must for any 2-cycle, since ; the toy curve of §3.7, over with points, has trace , and the case excluded in that subsection, a curve over with points and so trace , is exactly the anomalous one.
The Pasta cycle renders each step of §7.3 native. A proof committed on Vesta is produced by a circuit native to ; that circuit verifies the previous proof of the chain, committed on Pallas, whose group elements, the column and quotient commitments, the pairs and the point of the Pallas accumulator instance it forwards, have coordinates in exactly , so the point arithmetic of the succinct checks and of the fold (36) is native. The next proof, committed on Pallas by a circuit native to , verifies the Vesta proof by the symmetric argument. This cross-curve alternation avoids non-native emulation of the preceding curve’s coordinate field; as “What the cycle does and does not buy” said, it does not eliminate the scalar-field conversions.
This is the part of the cycle in consensus. The Action circuit is native to and committed on Vesta (§3.8), and the statement it proves manipulates Pallas points: the note commitment , a Pallas point whose -coordinate is a public input; the randomised verification key ; and the net value commitment , the last two exposed by their coordinates in the instance column of §4.2. Their coordinates lie in , the circuit’s native field, by the very coincidence the cycle is built on, so the circuit computes on them natively, with gates such as the incomplete-addition gate of §4.1.2. The protocol specification records the arrangement: Vesta for the proof system, Pallas for the application circuit, both curves designed to be efficiently implementable inside a circuit though only Pallas is so used (protocol specification, § 5.4.9.6, “Pallas and Vesta”); ZIP 224 says the same in the language of this subsection, that the proposal uses half of the cycle, Pallas being the curve embedded in Vesta’s circuits, and that the full cycle is left for future use (ZIP 224, under “Curves”). One direction of Figure 20 is thus in consensus today; the return arrow, and everything in this section that depends on it, is not.