Thanks to Yi Sun and Jonathan Wang for the Axiom open source program and for substantial help with halo2 and halo2-lib, and to M.S. Krishnamoorthy for many helpful discussions about polynomial commitment schemes in general and IPA in particular.
This document was written as part of the Axiom open source program. It contains a detailed explanation/description of a particular polynomial commitment scheme, the "Inner Product Argument", as well as notes on the implementation of a "circuit" (in the sense of Plonkish arithmetization) to verify batch IPA proofs.
As part of the Axiom open source program, I planned to write a circuit to verify membership proofs in a Verkle trie. Verkle tries are a data structure to commit to a dictionary (i.e., a store of key-value pairs), and they have been proposed as a replacement to Merkle Patricia tries for storing state in Ethereum (BF21, But21a, Fei21a).
The basic model, a Verkle tree, was invented by J. Kuszmaul in 2018. Verkle trees require an underlying vector commitment scheme. For reasons we indicate below, inner product arguments (IPA) have been proposed as the vector commitment scheme for the Verkle trie to store state. One of these reasons is that IPA, like other linear vector commitment schemes, permits batch proofs. IPA has found several other uses: they are being used currently in zcash and in the backend of the Halo2 proving system.
With this in mind, my first goal was to write a circuit that verified a batch IPA proof.
Recall that a trie, a.k.a. a prefix tree, is a data structure that allows one to efficiently store partially defined functions (a.k.a. associative arrays a.k.a. dictionaries). For instance, one could imagine a partially function:
The trie roughly allows for the lazy allocation of nodes. See here for an introduction.
Throughout this article, all vectors will be row vectors.
Fix a cryptographic prime . A vector commitment scheme is a protocol to commit to vectors . The commitment scheme should have the following properties:
The word "short" in (2) implies that the proof can't reveal all the other elements of .
In other words, a vector commitment scheme allows a prover to commit to a long vector, such that if later in time someone asks "what was the element", the prover can produce both the element and a short probabilistic proof that the element is correct. (This means that if the verifier algorithm returns "TRUE" on input , then the verifier may rest assured that with overwhelming probability the prover is telling the truth.)
There are occasionally other desiderata of vector commitment schemes: for instance, that the verification algorithm be sub-linear, or that the protocol batches, etc.
In comparison to Merkle Patricia tries, Verkle tries have the following advantages.
There are a variety of excellent sources on IPA: But21b, Fei21b, HALO19. As far as I know, the original inner product argument occurs in BCCGP16. In our implementation, we closely follow the numbering and details of the Halo paper.
Before we explain the protocol in detail, we summarize the goals and basic properties and features.
As per the name, the inner product argument accomplishes the following: the prover can commit to a vector and then prove they know a such that . To iterate: the advantage of IPA is that the proof is significantly shorter than revealing all of the elements of . In fact, IPA works by jointly proving that the verifier knows with the given commitment and with .
In the bare IPA scheme (which is what the following is based on), we demand no privacy with respect to . Privacy can be easily be assured by adding some blinding factors.
We are most interested in IPA as a polynomial commitment scheme. This will be explained below.
In particular, note that IPA does not require a trusted setup, has no toxic waste, and does not require pairings (and hence a pairing friendly elliptic curve). Together with the aggregation properties, these are probably the most important reasons IPA has been favored to be the vector commitment scheme underlying the Verkle trie to manage state in Ethereum.
We quickly review Lagrange bases. let be a primitive root of unity. We write to be the subgroup generated by . (Note that while is not uniquely determined, the subgroup is – this comes from the beautiful fact that the (multiplicative) group of non-zero elements of is cyclic.)
Let be the unique degree polynomial whose values on are given by:
The are called the Lagrange basis with respect to . (They form a basis of the vector space .) One utility of the Lagrange basis is an efficient scheme to build a vector commitment scheme from a polynomial commitment scheme, which we explain below.
Suppose we want to commit a vector . There is a unique polynomial of degree no greater than such that :
Explicitly, in Lagrange basis
Suppose we have a polynomial commitment scheme. Then we commit by commiting . The opening proof for will then be an evaluation proof for at .
A final remark on computation time. As we have chosen to be as subgroup of 2-primary roots of unity, the computation of the Lagrange basis may be done in time via FFT. However, for all applications in this note, the Lagrange basis is precomputed and hence does not contribute to any of the time analyses.
In particular, we could have chosen any other subset and built a Lagrange basis for this subset, and we would equally get a vector commitment scheme from a polynomial commitment scheme of the "same performance." We stick to the choice of , both out of convention, and because in other applications it is important that is a subgroup.
By the above, we have reduced a vector commitment scheme to a polynomial commitment scheme, i.e., if we have a polynomial commitment scheme, we can derive a vector commitment scheme.
We will see that for single proofs, IPA may be used directly as a vector commitment scheme; however, the main advantage of batching comes from treating it as a PCS.
To derive a PCS from an inner product argument above, if , set . To provide an evaluation proof at , set .
As indicated above, as part of the setup of IPA, we require the following.
The Prover's initial commitment is . We pause to interpret what this means: recall that . Therefore, for any and any , the product
is well-defined. (Note that some authors prefer multiplicative notation for . In this notation, the above, "iteratively apply the group operation to copies of a group element " would be written as . We will only use additive notation for in this note.)
Then is the "multi-scalar multiplication", i.e., is . (This is sometimes known as a Pederson commitment of .)
The prover will claim to know with and with . The associated IPA claim is:
We consider this element to be a joint commitment to the claims and .
A word on the nomenclature. When we say the word "joint commitment", we mean that the element computationally binds the the two claims. This concretely means the following: if the prover knew another such that , then the prover would have found a linear relation between the and , which we assume is computationally difficult.
Before we describe the rest of the protocol, we need two further notions.
Let , let be an even number, and let Then is in .
Abusing notation, we make a similar definition wher is replaced by a vector of group elements. Suppose . Then is in .
We choose the name "scalar folding" because in both cases, we are folding a vector of length into a vector of length with help from a single scalar .
Let be an even number and be vectors in and be a vector in . Then , where
and .
Note that both and are IPA-like statement commitments:
The prover claims that and . Using , this claim may be packaged into one joint claimed value of:
Using folding and folding commitments, the prover will "reduce" this claim to a claimed value of:
where all have half the length. (Equivalently, the prover reduces the original pair of claims to a pair of claimed values for and .) Note that for this reduction to be computationally sound, it must be hard to find non-trivial linear relations between the and .
The verifier will respond with some randomness, which the prover will use to seed a new folding, reducing the claim to an MSM claim and an inner product claim where the constituent vectors have length , etc. At the end of the protocol, the prover is making a claim about the "inner product" of vectors of length 1, i.e., the product. At that point, the prover may simply reveal . (Depending on the details/the structure of , the verifier can compute the rest herself, sometimes quite quickly.)
Set , , and . At stage , the prover computes .
For every , at the beginning of stage , the prover computes the following elements (without sending to the verifier):
We note that are vectors of length .
Then she computes and sends these two elements of to the verifier.
Finally, at stage 0, the prover simply sends , given by , which, as it is a vector of length 1, we treat as a scalar.
The prover has two implicit claims at Stage :
In other words, this has the form of an original IPA claim: a commitment to a vector with respect to a known URS and a claimed inner product. Note further that the two equations above really look quite similar.
In the actual proof, we are able to package both of these claims into a single claim using ; as we assumed from the get-go that it is computationally difficult to find a linear relation between the elements of the vector and , both claims can be sampled together via into a joint claimed value of:
We have an outstanding question: why are these the implicit claims, and what do the have to do them them?
If the prover is conducting the protocol honestly, then for any , we have:
In other words, after sending and receiving , suppose the prover reveals . Then the verifier has a simple compatibility check she can do, namely, the above equality.
Conversely, we have the following claim.
Claim: Suppose that at stage , the prover reveals and the above check is satisfied. Then with overwhelming probability, the prover knew an original with:
This claim follows from the fact that are all randomly (or even adversarially) chosen. The key is that with overwhelming probability, the implicit IPA claim the prover had at step is given by the element .
In other words, the validity at stage has been reduced to the validity at stage . Using induction, one concludes.
The actual verifier check practically jumps off of the page at this point. We explain this in the next subsection.
For further intuition of how this implicit claim works, we strongly recommend the reader look at the diagrams in But21b.
Now, the verifier has the following information:
As we have described the prover, we must now describe the verifier algorithm. This goes as follows.
We explain in greater detail point (2). Consider the following auxiliary polynomial of degree :
Then (2) follows from the fact that . (This follows from simply writing out the binary counting pattern.) In particular, although the polynomial has non-zero coefficients, one can compute its evaluations in time because of this compact product representation.
Note that if is simply a unit vector of the form , we can still compute quickly. (Exercise given the above!) This implies that IPA immediately furnishes a vector commitment scheme whose only linear cost is a single MSM. (Here, "immediately" means: without transforming to Lagrange bases and using as , as explained in the subsection on the relation between vector commitment schemes and polynomial commitment schemes.) However, as far as I was able to work out, in order to obtain efficient batching, one must work with the polynomial commitment scheme form.
As usual, this interactive proof system can be made non-interactive by applying the Fiat-Shamir heurestic. This means that the randomness will be some determinstic evaluation of a pseudorandom hash function of the transcript so far. As usual, to ensure security one needs that
Here, the phrase "commited in the randomness" simply means "is fed into the hash function."
The crucial observation for batching is that is in fact the Pederson commitment of . Indeed, this follows from the explicit expansion of . (As mentioned above, the coefficients, read from constant to top degree, will .) Moreover, the only step that is expensive in the above verification process is the MSM required to compute from .
We now explain how the prover can "batch" proofs together such that the verifier ends up doing
Here, we assume that we have a fixed and , and we want to commit vectors , where . (We use left subscripts to avoid confusing the index inside a given vector with the index of the vector in my list of vectors.)
The prover generates individual IPA proofs for each of the , with the following addition: the prover includes a claimed value of the , the "" value in IPA proof. Alternatively, this element may also be described as:
where are the pseudo-random elements in the IPA proof.
By the above discussion, is Pederson commit of , where is the polynomial constructed above from the IPA claim. (Again, this polynomial only depends on the pseudorandom challenges.)
Suppose that the prover now received a pseudo-random challenges . (In our setting, the prover will generate this as some hash of all of the proofs.)
Then the prover will provide one additional IPA proof. The polynomial will be , which will be evaluated at .
Then the verifier must check that the final "merged" proof actually corresponds to a correct merging of the original list of proofs.
I implemented "IPA as a batched polynomial commitment scheme". This means: (1) a native Rust implementation of prover and verifier, as well as an circuit-level implementation to verify a batched IPA proof.
The Rust implementation is straightforward and thoroughly commented. A few remarks on the code are in order.
The only real choice in implementation is that of the hash functions used to generate the pseudo-randomness. Due to initially having some trouble getting the PoseidonChip in halo2-lib to be compatible with the other native implementations, I decided against putting it in this iteration. Instead, randomness is generated as follows.
is set to simply be the claimed evaluation . Then, for all , we set:
where the function takes a point , reduces the coordinates mod , and takes the sum.
and . In words: is the product of the "last randomness" for every proof and is the square of . This at least means that the pseudo-random numbers reflect iterated commitments to every part of every proof. In an production-level implementation, this would presumably have to be improved. However, we emphasize: if one believes that the are pseudo-random, essentially any function one picks of (all of) the will be secure, in the sense that the prover cannot give false proofs by carefully massaging the .
I built several data structures to store proofs, complete proofs, batched proofs, etc., so it was easy to pass to a native Rust verifier as well as to a circuit verifier. I list each of these abstractions here, with their desired purpose.
This is a struct containing a proof of Evaluation.
revealed_evaluation
is the element claimed to be evaluated.stage_proof
is the vector of as described in the IPA protocol. The only additional point of note is the order: stage , stage , …, stage .final_a
is the final a value that the prover reveals.BatchingHelperInfo
contains the claimed stage_randomness as well as the claimed . This is necessary when we try to batch.The model here is that the other inputs needed for the proof, namely , , and , are assumed to be already known.
This struct contains all of the information the verifier needs to verify a single IPA proof.
commitment
is the commitment to the polynomial, or equivalently to .proof
is of type ProofOfEvaluation
g_init
is in our explanation above, i.e., it is the URS.u
is the random element that is used to combine two claims into a single joint claim.This struct contains auxiliary information in a single IPA proof to help with batching. The necessary extra information is g_0
, which is the claimed final folded value. I chose to add a tiny bit of extra information: the pseudo-randomness at each stage.
This is analogous to ProofOfEvaluation.
list_of_proofs
is a vector of the claimed single proofs.commitment_to_weighted_poly
is the claimed commitment to (in the language above.) More vaguely: it is the claimed commitment to the "merged polynomial."proof_of_weighted_poly
is an opening proof for the value of weighted_poly at (the pseudo-random point generated from the proofs.)This struct contains everything the verifier needs to evaluate a batched IPA opening proof.
commitments
is a list of the commitments of the polynomialsvec_z
is a vector of the points where we want to evaluate the proofs.batch_proof
is of thype BatchProofOfEvaluation
g_init
is the URS. (This is in our explanation above.)u
is the random element used to take two commitments and make them a joint commitment.I wrote a circuit to take in a batched IPA proof and verify the proof. Here, I emphasize: I am treating IPA as a PCS; that means that each .
To test my circuit, I generated proofs via the rust implementation and passed it into my circuit. To do this, one needs to "place all of the inputs into a table of numbers". This is accomplished with the following function
What is CircuitCompleteSingleProof
? This will be the input to my single IPA proof verifier circuit. Note that all of the parts of the struct are circuit level, i.e., already in my table of numbers.
One small note: left
corresponds to and right
corresponds to . In other words, these are the group elements that the prover sends to the verifier at each stage.
We have siimlar functions for batched proofs.
and
Given some part of the proof, the verifier needs to compute the stage_randomness
. (This is where the verifier simulates the Fiat-Shamir.)
In particular, the output will be of the form: (<w_k, ..., w_1>, <w_k^{-1}, ..., w_1^{-1}>)
, with constraints forcing w_i * w_i^{-1} = 1
. We emphasize that the order is the same as that of the Halo paper: denotes the randomness at the (end of the) stage of the proof.
As a necessary piece of this, we need code to hash group elements to field elements. The signature is below:
Similarly, given many proofs, the verifier needs to independently compute the "batching randomness", which will correspond to in the above.
To e.g. compute (and also to use the properties of the ), we need the following function.
Given stage_randomness
= and , compute the following:
The verifier must generate the binary counting pattern given the stage_randomness
. The following are the relevant code snippets.
The input is (where each element is of type AssignedValue<F>
) and the output is (which of of type Vec<AssignedValue<F>>
).
In fact, we use binary_counting_reverse
in our circuit.
This is straightforward given the constituent parts above and the description of the verification algorithm. The relevant functions are:
and
Currently, the circuit is running for BN-254, which is notably non-native. (This means that the proving system is designed for circuits, but the elliptic curve is defined over , hence doing elliptic curve operations requires simulating a different field. This is expensive.)
Ppening proofs for length 256 vectors, batched to 20 vectors.
Substituting a "native" elliptic curve should dramatically improve performance. (This means an elliptic curve defined over , the field in which Halo2 assumes arithmetic circuits are written.) One example of such a curve is Grumpkin, developed by Aztec to be in a "curve cycle" with BN-254).
Moving forward, my goal is to write a circuit to verify membership in a Verkle trie, following the specs provided in the above links by the Ethereum foundation. This will involve variable length byte-array concatenation checks. In a normal circuit, this would be difficult to attain with any degree of efficiency: when trying to naively implementing branching, circuits have to compute all branches!
Fortunately, Halo2's challenge API is almost designed for this; it allows you to generate in-circuit randomness and feed that into your circuit. This randomness may be used in conjunction with the Schwarz Zippel lemma to test polynomial equality. I will most likely use Axiom's RlcChip. (Rlc = "random linear combination".)