Try   HackMD

Verification of batch IPA proofs in halo2-lib

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.

Motivation

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.

Tries

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:

State:{0,1}256{0,1}256.
The trie roughly allows for the lazy allocation of nodes. See here for an introduction.

Vector commitment schemes

Throughout this article, all vectors will be row vectors.

Fix a cryptographic prime

r. A vector commitment scheme is a protocol to commit to vectors
FrnvCOM(v)
. The commitment scheme should have the following properties:

  1. COM(v)
    is much smaller than
    v
    .
  2. The prover can efficiently compute a short (probabilistic) proof
    Π
    that witnesses the claim "
    vi
    is the
    ith
    element of
    v
    ".

The word "short" in (2) implies that the proof can't reveal all the other elements of

v.

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

100th 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.

Comparison of Verkle tries with Merkle Patricia tries

In comparison to Merkle Patricia tries, Verkle tries have the following advantages.

  1. They allow for much wider trees. Indeed, in a Merkle tree, one has to provide the hash values of all of the siblings of all of the nodes in a proof (i.e., in a path up to the root in the tree.) Using vector commitment schemes, this is unnecessary in a Verkle tree: one simply provides commitment proofs following the path from the leaf to the root. This means that membership proofs will be substantially smaller than MPT membership proofs.
    To give a sense of scale in the case of Ethereum: with the current hexary tree, the worst case size of membership proof is ~3kB. With a binary Merkle tree, this improves to ~500 bytes. Under the current model of a Verkle trie to store state (32 byte keys, 32 byte values, branching of 256), membership proofs would be ~100 bytes in the worst case (31 internal nodes in the path). In practice, the membership proofs in a Verkle trie are expected to be even shorter. According to Feist, we can expect ~16,000 membership proofs that aren't completely random (i.e., corresponding to elements that aren't completely unrelated to each other) to only take a few hundred kilobytes.
  2. As long as the underlying vector commitment scheme are linear, membership proofs may be batched. Concretely, this means the following. Suppose the prover wants to prove
    1,000
    membership proofs. Then she can produce a "batched proof", such that the cost to the verifier is not much more than the verification of a single proof.
  3. In the context of Ethereum, Verkle tries are supposed to provide a path towards weak statelessness. This means that validating nodes will not need to store any state; they would just need to check a series of proofs. One model for this: block proposers would include a block of proofs that the state trie has been updated in a valid manner.

Inner product arguments

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.

Goal

As per the name, the inner product argument accomplishes the following: the prover can commit to a vector

aFrN and then prove they know a
bFrN
such that
ab=y
. To iterate: the advantage of IPA is that the proof is significantly shorter than revealing all of the elements of
b
. In fact, IPA works by jointly proving that the verifier knows
a
with the given commitment and
b
with
ab=y
.

In the bare IPA scheme (which is what the following is based on), we demand no privacy with respect to

b. 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.

Basic features

  1. We assume that the length
    N=2k
    of the vector is a power of
    2
    .
  2. IPA requires a group of prime order
    r
    in which the discrete logarithm is (conjectured to be) computationally hard. As is now well-understood, for certain elliptic curves
    E/Fp
    (over an auxiliary prime field
    Fp
    ), the groups
    G:=E(Fp)
    have prime order and seem to be resistent to attacks on the discrete log problem. We briefly reminder the reader what this means. While the group
    G
    is isomorphic to
    Z/rZ
    (and in fact a generator
    P
    of the group is public knowledge, i.e., there is an explicit isomorphism
    Z/rZG
    ), given a random point
    (x,y)=gG
    , it is conjectured to be hard to compute
    logP(g)
    from the representation as
    (x,y)
    . In other words, it seems as though inverting the aforementioned isomorphism is computationally difficult.
  3. IPA does not require a trusted setup a.k.a. structured reference string. In particular, IPA requires no toxic waste. (In comparison, KZG does require an SRS which comes along with toxic waste.) Instead, IPA requires an "unstructured reference string"
    gGN
    , with the property that if
    g=(g1,,gN)
    , then none of the pairwise discrete logarithms
    loggi(gj)
    are known. This may be generated deterministically by feeding into a hash function.
  4. IPA does not require pairings, unlike KZG.
  5. Using a "Lagrange basis" (to be explained below), the commitment of a vector is (essentially) a Pederson commitment. In particular, the commitment of
    vFrN
    is an element of
    G
    .
  6. IPA is an interactive proof system, where at every stage there is randomness furnished by the verifier. At each stage, the prover supplies two elements
    Li,RiG
    . Roughly speaking, IPA acts like a folding scheme, reducing the claim of a long statement (that two vectors of length
    m
    have a given inner product) to a shorter statement (that two vectors of length
    m/2
    have a given inner product). (As usual, this interaction can be removed by using a deterministic, pseudo-random procedure for generating the "verifier randomness", a.k.a. the Fiat-Shamir heurestic.) In particular, the length of an IPA proof is
    O(log(N))
  7. IPA verification is
    O(N)
    , so it might seem that their main advantage is that the proofs have size
    O(logN)
    . However, IPA proofs, being a linear commitment scheme, batch exceptionally well, and moreover. Punchline: there is an efficient protocol for a prover to prove a
    m
    IPA proofs (with the same
    g
    ), with proof length
    O(mlogN)
    , such that the verifier time is
    O(mlog(N)+N)
    . More precisely, the verifier time is
    O(mlogN)+verfier time for a single IPA proof.
  8. Moreover, this batching may done incrementally, i.e., on-the-fly; the prover can continually generate single IPA proofs, and then when the verifier wants to check them all, the prover can generate a single "merged" proof, which is again an IPA proof. (In fact, any other prover could do this computation equally well, just looking at the list of single IPA proofs.) The verifier, inspecting the original proofs, can check that the merged proof was correctly computed in logarithmic time.

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.

Lagrange basis

We quickly review Lagrange bases. let

ωFr be a primitive
Nth
root of unity. We write
HFr×
to be the subgroup generated by
ω
. (Note that while
ω
is not uniquely determined, the subgroup
H
is this comes from the beautiful fact that the (multiplicative) group of non-zero elements of
Fr
is cyclic.)
Let
LiFr[x]
be the unique degree
N1
polynomial whose values on
H
are given by:

Li(ωj)=δi,j.

The

{Li} are called the Lagrange basis with respect to
H
. (They form a basis of the vector space
Functions(H,Fr)
.) 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

vFrN. There is a unique polynomial
fvFr[x]
of degree no greater than
N1
such that :
f(ωi)=vi.

Explicitly, in Lagrange basis
f=viLi.

Suppose we have a polynomial commitment scheme. Then we commit

v by commiting
fv
. The opening proof for
vi
will then be an evaluation proof for
fv
at
ωi
.

A final remark on computation time. As we have chosen

H to be as subgroup of 2-primary roots of unity, the computation of the Lagrange basis may be done in
O(Nlog(N))
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
SFr
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
H
, both out of convention, and because in other applications it is important that
HFr×
is a subgroup.

IPA as a polynomial commitment scheme.

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

f=aixi, set
a=(a0,,aN1)
. To provide an evaluation proof at
z
, set
b=(1,z,,zN1)
.

As indicated above, as part of the setup of IPA, we require the following.

Setup

  • Our vectors are of length
    N=2k
    .
  • G
    , a cryptographic group of size
    r
    in which the discrete logarithm problem is hard.
  • A URS
    gGN
    , where the discrete logs between any two components of the vectors are unknown.
  • A random element
    uG
    , again with the assumption that
    logu(gi)
    is unknown.
  • To make the protocol non-interactive, a cryptographic hash function
    H:GFr
    that eats strings of group elements and spits out a field element.

The Prover's initial commitment is

COM:=[a]g. We pause to interpret what this means: recall that
r=|G|
. Therefore, for any
λFr
and any
gG
, the product
[λ]g:=g++gλ times
is well-defined. (Note that some authors prefer multiplicative notation for
G
. In this notation, the above, "iteratively apply the group operation to
λ
copies of a group element
gG
" would be written as
gλ
. We will only use additive notation for
G
in this note.)

Then

[a]g is the "multi-scalar multiplication", i.e., is
[ai]giG
. (This is sometimes known as a Pederson commitment of
a
.)

The prover will claim to know

a with
COM=[a]g
and
b
with
ab=y
. The associated IPA claim is:

[a]g+[y]uG.

We consider this element to be a joint commitment to the claims

[a]g=COM and
ab=y
.

Joint commitments

A word on the nomenclature. When we say the word "joint commitment", we mean that the element

[a]g+[y]uG computationally binds the the two claims. This concretely means the following: if the prover knew another
α,δ
such that
[α]g+[δ]u=[a]g+[y]uG
, then the prover would have found a linear relation between the
gi
and
u
, which we assume is computationally difficult.

Before we describe the rest of the protocol, we need two further notions.

Folding and Folded Commitments.

Scalar folding

Let

λFr, let
m
be an even number, and let
wFrm
Then
ScalFold(λ,w):=λ1wlo+λwhi
is in
Frm/2
.

Abusing notation, we make a similar definition wher

w is replaced by a vector of group elements. Suppose
hGm
. Then
ScalFold(λ,h):=[λ1]wlo+[λ]whi
is in
Gm/2
.

We choose the name "scalar folding" because in both cases, we are folding a vector of length

m into a vector of length
m/2
with help from a single scalar
λFr
.

Folded commitment.

Let

m be an even number and
α,β
be vectors in
Frm
and
γ
be a vector in
Gm
. Then
FoldCom(α,β,γ):=(L,R)
, where
L:=[αlo]γhi+[(αloβhi)]uG
and
R:=[αhi]γlo+[(αhiβlo)]uG
.

Note that both

L and
R
are IPA-like statement commitments:

  • L
    commits to:
    αloFrm/2
    through a Pederson commitment with respect to
    γhi
    , as well as to
    αloβhiFr
    .
  • R
    commits to
    αhiFrm/2
    through a Pederson commitment with respect to
    γlo
    as well as to
    αhiβloFr
    .

The rough idea of folding

The prover claims that

ab=y and
[a]g=COM
. Using
u
, this claim may be packaged into one joint claimed value of:

[a]g+[ab]u
Using folding and folding commitments, the prover will "reduce" this claim to a claimed value of:
[a]g+[ab]u,

where
a,b,g
all have half the length. (Equivalently, the prover reduces the original pair of claims to a pair of claimed values for
[a]g
and
ab
.) Note that for this reduction to be computationally sound, it must be hard to find non-trivial linear relations between the
gi
and
u
.

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

N/4, 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
a0
. (Depending on the details/the structure of
b
, the verifier can compute the rest herself, sometimes quite quickly.)

The protocol for the prover (following the Halo paper)

Set

ak=a,
bk=b
, and
gk=g
. At stage
k
, the prover computes
(Lk,Rk):=FoldCom(ak,bk,gk)
.

Created with Raphaël 2.2.0ProverProverVerifierVerifierClaimed commitment of a, claimed evaluation y.Stage k: L_k, R_k in GPick a random w_kw_kProver computes a_{k-1}, b_{k-1}, g_{k-1}Prover computes L_{k-1}, R_{k-1}Stage k-1: L_{k-1}, R_{k-1} in GPick a random w_{k-1}w_{k-1}......Prover computes L_1, R_1Stage 1: L_1, R_1 in GPick a random w_1w_1Compute a_0Stage 0: a_0 in F_rCheck the proof!

For every

{k1,,1}, at the beginning of stage
, the prover computes the following elements (without sending to the verifier):

a:=ScalFold(w+11,a+1), b=ScalFold(w+1,b+1), g=ScalFold(w+1,g+1)
We note that
a,bFr(2)
are vectors of length
2
.

Then she computes

(L,R):=FoldCom(a,b,g)G2 and sends these two elements of
G
to the verifier.

Finally, at stage 0, the prover simply sends

a0, given by
a0:=ScalFold(w11,a1)
, which, as it is a vector of length 1, we treat as a scalar.

The implicit claim

The prover has two implicit claims at Stage

:

  1. ab=y,
    where
    y
    is defined inductively by:
    y=y+1+w+12(a+1,lob+1,hi)+w+12(a+1,hib+1,lo).
  2. [a]g=COM,
    where the latter is defined inductively as:
    COM=COM+1+w+12(a+1,log+1,hi)+w+12(a+1,hig+1,lo)

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

u; as we assumed from the get-go that it is computationally difficult to find a linear relation between the elements of the vector
g
and
u
, both claims can be sampled together via
u
into a joint claimed value of:

COM+[y]uG.

We have an outstanding question: why are these the implicit claims, and what do the

Lj,Rj have to do them them?

Relation of
L+1,R+1
to the IPA claim.

If the prover is conducting the protocol honestly, then for any

{1,,k1}, we have:

[a]g+[ab]u=([a+1]g+1+[a+1b+1]u)+(w+12L+1+w+12R+1)

In other words, after sending

L+1,R+1 and receiving
w+1
, suppose the prover reveals
a,b
. 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
a,b
and the above check is satisfied. Then with overwhelming probability, the prover knew an original
α,β
with:

[α]g=COM, αβ=y.

This claim follows from the fact that

wk,,w+1 are all randomly (or even adversarially) chosen. The key is that with overwhelming probability, the implicit IPA claim the prover had at step
+1
is given by the element
[a]g+[ab]u(w+12L+1+w+12R+1)
.
In other words, the validity at stage
+1
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.

Verifier's protocol

Now, the verifier has the following information:

  • zFr
  • The claimed value
    y=f(z)=ab
  • The commitment
    COMG
    to
    a
    (equivalently, to
    f
    )
  • Lk,Rk,,L1,R1
    , i.e.,
    2k
    elements of
    G
    .
  • The final value
    a0
    .

As we have described the prover, we must now describe the verifier algorithm. This goes as follows.

  1. Given the randomness
    wk,,w1
    , compute the following "binary counting vector"
    s:=(w11w21w31wk1w1w21w31wk1w11w2w31wk1w1w2w31wk1w1wk)TFrN
    where the pattern of of ones and negative ones is governed by binary counting.
  2. Compute
    b0=sb
    . In particular, the claim is that
    ScalFold(w1,b1)=sb
    . This claim holds for any starting vector
    bFrN
    ; for general vectors
    b
    , this computation requires a linear number of field operations.
    However, in our case
    b=(1,z,,zN1)
    , and
    sb
    can be computed very quickly from
    wk,,w1
    . (In other words,
    b
    is highly structured in a way that dramatically simplifies this computations.) In particular, we do not need to explicitly invoke
    s
    for this step, just the elements
    wk,,w1
    .
  3. Compute
    g0=sg
    . This is the only step in the process that necessarily takes linear time. (Note that scalar multiplication is also much more expensive than field multiplication.)
  4. Compute
    Q1:=j=1kwj2Lj+j=1kwj2Rj+(COM+yu)original IPA claim
    and
    Q2=a0(g0+b0u)final IPA claim
    . Check that
    Q1=Q2
    .

We explain in greater detail point (2). Consider the following auxiliary polynomial of degree

N1:

T(x):=j=1k(wj1+wjx2j1)Fr[x].

Then (2) follows from the fact that

T(z)=b0. (This follows from simply writing out the binary counting pattern.) In particular, although the polynomial
T
has
N
non-zero coefficients, one can compute its evaluations in
O(logN)
time because of this compact product representation.

Note that if

b is simply a unit vector of the form
b=(0,..0,1,0,..0)
, we can still compute
b0
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
a
to Lagrange bases and using
(1,ωi,ω2i,,ω(N1)i)
as
b
, 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.

Non-interactive version

As usual, this interactive proof system can be made non-interactive by applying the Fiat-Shamir heurestic. This means that the randomness

w will be some determinstic evaluation of a pseudorandom hash function of the transcript so far. As usual, to ensure security one needs that

  • the original statement as well is commited in the randomness; and
  • every element the prover sends is commited in the randomness.

Here, the phrase "commited in the randomness" simply means "is fed into the hash function."

Batching

The crucial observation for batching is that

g0 is in fact the Pederson commitment of
T(z)
. Indeed, this follows from the explicit expansion of
T(z)
. (As mentioned above, the coefficients, read from constant to top degree, will
s
.) Moreover, the only step that is expensive in the above verification process is the MSM required to compute
g0
from
g
.

We now explain how the prover can "batch"

m proofs together such that the verifier ends up doing
O(mlogN)+single MSM of length N

Prover protocol

Here, we assume that we have a fixed

g and
u
, and we want to commit
m
vectors
{ iv}
, where
 ivFrN
. (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

 iv, with the following addition: the prover includes a claimed value of the
 ig0G
, the "
g0
" value in
ith
IPA proof. Alternatively, this element may also be described as:

ScalFold(iw1,(ScalFold(iw2,ScalFold(iwk,g)))),
where
iwj
are the pseudo-random elements in the
ith
IPA proof.
By the above discussion,
ig0
is Pederson commit of
 iT
, where
 iT
is the polynomial
T
constructed above from the
ith
IPA claim. (Again, this polynomial only depends on the pseudorandom challenges.)

Suppose that the prover now received a pseudo-random challenges

ξ,ζFr. (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

ξi iT(x)Fr[x], which will be evaluated at
ζ
.

Verifier protocol

  1. First of all, the verifier has to check the final IPA proof. This takes
    O(N)
    time, again dominated by the single MSM.

Then the verifier must check that the final "merged" proof actually corresponds to a correct merging of the original list of proofs.

  1. The verifier computes the pseudorandomness
    iwj
    at stage
    j
    of the
    ith
    proof. (In other words, we assume that the pseudo-random challenges were generated determinastically by some series of functions of the transcript. The verifier can simply compute this herself.)
  2. The verifier checks that the computation of
    ξ,ζ
    was done correctly. (Similarly, we assume that
    ξ
    and
    ζ
    are computed determinstically given the transcript of all of the single proofs; the verifier can therefore look at all of these single proofs and compute
    ξ
    and
    ζ
    herself.)
  3. The verifier then uses the
    iwj
    to check whether the claimed evaluation
    ξi iT(ζ)
    in the final proof is compatible with the earlier proofs: the verifier may evaluate each
    iT
    in
    O(log(N))
    time due to the compact product representation explained above.

Implementation

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.

Rust

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.

Pseudorandomness in single proof generation

wk is set to simply be the claimed evaluation
y
. Then, for all
{1,,k1}
, we set:

w=yw+1+hash_group_to_field(L)+hash_group_to_field(R),
where the function
hash_group_to_field:E(Fp)Fr
takes a point
(x,y)Fp2
, reduces the coordinates mod
r
, and takes the sum.

Pseudorandomness to generate
ξ,ζ

ξ= iw1 and
ζ=ξ2
. 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
iwj
are pseudo-random, essentially any function one picks of (all of) the
iw1
will be secure, in the sense that the prover cannot give false proofs by carefully massaging the
L,R
.

Data structures

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.

ProofOfEvaluation

This is a struct containing a proof of Evaluation.

  • revealed_evaluation is the element claimed to be evaluated.
  • stage_proof is the vector of
    [Li,Ri]
    as described in the IPA protocol. The only additional point of note is the order: stage
    k
    , stage
    k1
    , , stage
    1
    .
  • final_a is the final a value that the prover reveals.
  • BatchingHelperInfo contains the claimed stage_randomness as well as the claimed
    g0
    . This is necessary when we try to batch.

The model here is that the other inputs needed for the proof, namely

g=ginit,
u
, and
z
, are assumed to be already known.

pub struct ProofOfEvaluation {
    pub revealed_evaluation: Fr, // element claimed to be revealed
    pub stage_proof: Vec<[G1Affine; 2]>,
    pub final_a: Fr,
    pub batching_helper_info: Option<BatchingHelperInfo>,
}

CompleteSingleIPAProof

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
    a
    .
  • z
    is the point where we want to evaluate the polynomial.
  • proof is of type ProofOfEvaluation
  • g_init is
    g
    in our explanation above, i.e., it is the URS.
  • u is the random element
    u
    that is used to combine two claims into a single joint claim.
pub struct CompleteSingleIPAProof{
    pub commitment: G1Affine,
    pub z: Fr,
    pub proof: ProofOfEvaluation,
    pub g_init: Vec<G1Affine>,
    pub u: G1Affine,
}
BatchingHelperInfo

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

g value. I chose to add a tiny bit of extra information: the pseudo-randomness at each stage.

pub struct BatchingHelperInfo{
    pub stage_randomness: Vec<Fr>,
    pub g_0: G1Affine,
}
BatchProofOfEvaluation

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
    ξi iT(x)
    (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.)
pub struct BatchProofOfEvaluation{
    pub list_of_proofs: Vec<ProofOfEvaluation>,
    pub commitment_to_weighted_poly: G1Affine,
    pub proof_of_weighted_poly: ProofOfEvaluation
}
CompleteBatchIPAProof

This struct contains everything the verifier needs to evaluate a batched IPA opening proof.

  • commitments is a list of the commitments of the polynomials
  • vec_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
    g
    in our explanation above.)
  • u is the random element used to take two commitments and make them a joint commitment.
pub struct CompleteBatchIPAProof {
    pub commitments: Vec<G1Affine>,
    pub vec_z: Vec<Fr>,
    pub batch_proof: BatchProofOfEvaluation,
    pub g_init: Vec<G1Affine>, // g_init is the same for all batched proofs.
    pub u: G1Affine
}

Circuit

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

b=(1,z,z2,,zN1).

Loading the input

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

pub fn load_complete_single_ipa_proof(
    builder: &mut GateThreadBuilder<Fr>,
    gate: &GateChip<Fr>,
    range: &RangeChip<Fr>,
    params: &MSMCircuitParams,
    single_proof: &CompleteSingleIPAProof, // an IPA proof, generated in rust.
    make_public: &mut Vec<AssignedValue<Fr>>,
) -> CircuitCompleteSingleProof 

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

L and right corresponds to
R
. In other words, these are the group elements that the prover sends to the verifier at each stage.

pub struct CircuitCompleteSingleProof {
    pub commitment: EcPoint<Fr, ProperCrtUint<Fr>>,
    pub z: AssignedValue<Fr>,
    pub g_init: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub u: EcPoint<Fr, ProperCrtUint<Fr>>,
    pub revealed_evaluation: AssignedValue<Fr>,
    pub left: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub right: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub final_a: AssignedValue<Fr>,
    pub k: usize, // number, such that 2^k is the degree of the polynomial we are commiting.
                  // equivalently, the number of steps in the proof.
}

We have siimlar functions for batched proofs.

pub fn load_complete_batch_ipa_proof(
    builder: &mut GateThreadBuilder<Fr>,
    gate: &GateChip<Fr>,
    range: &RangeChip<Fr>,
    params: &MSMCircuitParams,
    proof: &CompleteBatchIPAProof,
    make_public: &mut Vec<AssignedValue<Fr>>
)->CircuitCompleteBatchProof

and

pub struct CircuitCompleteBatchProof {
    // the proofs of the individual claims
    pub vec_commitment: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub vec_z: Vec<AssignedValue<Fr>>,
    pub g_init: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub u: EcPoint<Fr, ProperCrtUint<Fr>>,
    pub vec_revealed_evaluation: Vec<AssignedValue<Fr>>,
    pub vec_left: Vec<Vec<EcPoint<Fr, ProperCrtUint<Fr>>>>,
    pub vec_right: Vec<Vec<EcPoint<Fr, ProperCrtUint<Fr>>>>,
    pub vec_a_0: Vec<AssignedValue<Fr>>,
    pub vec_g_0: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>, // this is new for batching!
    // the final "blended" proof.
    pub final_commitment: EcPoint<Fr, ProperCrtUint<Fr>>,
    pub final_left: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub final_right: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    pub final_a_0: AssignedValue<Fr>,
    pub k: usize,
    pub m: usize,    
}
Hashing and randomness

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:

w denotes the randomness at the (end of the)
th
stage of the proof.

pub fn compute_stage_randomness_single_proof(
    builder: &mut GateThreadBuilder<Fr>,
    gate: &GateChip<Fr>,
    z: AssignedValue<Fr>,
    revealed_evaluation: AssignedValue<Fr>,
    left: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    right: Vec<EcPoint<Fr, ProperCrtUint<Fr>>>,
    k: usize,
)->(Vec<AssignedValue<Fr>>, Vec<AssignedValue<Fr>>)

As a necessary piece of this, we need code to hash group elements to field elements. The signature is below:

pub fn hash_group_to_field_circuit(
    ctx: &mut Context<Fr>,
    gate: &GateChip<Fr>,
    p: EcPoint<Fr, ProperCrtUint<Fr>>
  )->AssignedValue<Fr>

Similarly, given many proofs, the verifier needs to independently compute the "batching randomness", which will correspond to

(ξ,ζ) in the above.

​​pub fn compute_final_batching_randomness(
​​  builder: &mut GateThreadBuilder<Fr>,
​​  gate: &GateChip<Fr>,
​​  vec_stage_randomness: Vec<Vec<AssignedValue<Fr>>>,
​​  m: usize,
​​  k: usize,
)->[AssignedValue<Fr>; 2]
Evaluate the compact polynomial

To e.g. compute

b0 (and also to use the properties of the
g0
), we need the following function.

pub fn evaluate_folded_product_poly(
    ctx: &mut Context<Fr>,
    gate: &GateChip<Fr>,
    z: AssignedValue<Fr>,
    stage_randomness: Vec<AssignedValue<Fr>>,
    stage_randomness_inv: Vec<AssignedValue<Fr>>,
)->AssignedValue<Fr>

Given stage_randomness =

(wk,wk1,...,w1) and
zFr
, compute the following:
i=1k(z2i1wi+wi1)Fr.

Binary counting

The verifier must generate the binary counting pattern given the stage_randomness. The following are the relevant code snippets.

pub fn binary_counting<F: ScalarField>(
    ctx: &mut Context<F>,
    gate: &GateChip<F>,
    input: binary_counting_input<F>,
    // make_public: &mut Vec<AssignedValue<F>>
    )-> Vec<AssignedValue<F>>
    

The input is

(w1,...,wk) (where each element is of type AssignedValue<F>) and the output is
(w11...wk1,w1w21...wk1,w11w2...wk1,...w1w2...wk)
(which of of type Vec<AssignedValue<F>>).

In fact, we use binary_counting_reverse in our circuit.

Evaluation of the proofs

This is straightforward given the constituent parts above and the description of the verification algorithm. The relevant functions are:

fn verify_single_ipa_proof(
    builder: &mut GateThreadBuilder<Fr>,
    single_proof: CompleteSingleIPAProof,
    make_public: &mut Vec<AssignedValue<Fr>>,
)

and

pub fn verify_batch_ipa_proof(
    builder: &mut GateThreadBuilder<Fr>,
    complete_batch_ipa_proof: CompleteBatchIPAProof,
    make_public: &mut Vec<AssignedValue<Fr>>,
)

Specs

Currently, the circuit is running for BN-254, which is notably non-native. (This means that the proving system is designed for

Fr circuits, but the elliptic curve is defined over
Fp
, hence doing elliptic curve operations requires simulating a different field. This is expensive.)

Ppening proofs for length 256 vectors, batched to 20 vectors.

  • 29,074,563 advice cells;
  • 3,529,821 lookup advice cells
  • 262 fixed cells
  • size of keys: pk: ~ 12 gb, vk: ~3.7 mb
  • a proof verifies in ~10 seconds on 3.3 GHz x 4 processor with 32 gB of RAM.

Substituting a "native" elliptic curve should dramatically improve performance. (This means an elliptic curve defined over

Fr, 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).

Next steps

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".)