# The Halo Effect

The purpose of this note is to explain (also to myself) the main idea in the Halo recursive SNARK construction of Bowe, Grigg and Hopwood https://eprint.iacr.org/2019/1021.
In fact, my understanding of the protocol heavily relies on the new paper of Bünz, Chiesa, Mishra and Spooner [[BCMS]](https://eprint.iacr.org/2020/499) which fills in many details and generalizes the approach to achieve "Proof Carrying Data Via Accumulation Schemes".

The starting point is the inner product argument of [Bootle et. al](https://eprint.iacr.org/2016/263) and its optimization in the [Bullet Proofs paper](https://eprint.iacr.org/2017/1066).

It was known that a special case of this inner product argument gave a polynomial commitment scheme (by taking the second vector to be a power vector of the form $(1,x,x^2,\ldots,x^n)$).

Let us call this scheme for brevity the BP-PCS. For the purpose of this note it is not needed to understand the inner workings of BP-PCS.
Here are its main good and bad properties:

* As opposed to the very popular KZG scheme, it does not require a trusted setup;
* and as opposed to the FRI-style schemes it is additively homomorphic, meaning that the sum of commitments to some polynomials is a commitment to the sum of those polynomials, we shall see later that this is very convenient.
* On the negative side - The big drawback of BP-PCS is that verification time is linear in the degree $n$.

Halo can be viewed as a partial mitigation of its verification time drawback.

The crucial observation of Halo is:

**Lemma:** The BP-PCS verifier can be split into two algorithms $V_1,V_2$ such that:
1. $V_1$ runs in $\mathrm{polylog} n$ time and on top of rejecting or accepting, outputs a pair $(h,D)$; Such that $h$ is a polynomial *that can be computed in time $\mathrm{polylog} n$ for any $z\in F$*.
2. $V_2$ consists of solely checking, for the pair $(h,D)$ output by $V_1$, whether $D$ is the BP-PCS commitment to $h$.

A useful consequence of this lemma is that several BP opening claims can be "compressed into one", as we now explain.
By an "opening claim" we mean a tuple $(C,z,v)$
that is interpreted as the claim "The prover knows a polynomial $h$ such that $C$ is the BP commitment to $h$ and $h(z)=v$"
(We informally think here of one prover in the background, and all claims being claims of knowledge pertaining to them - see [BCMS] for more formal treatment)
By an "opening proof" we mean a proof $\pi$ that can convince the BP-PCS verifier such an opening claim is correct.
**Corollary:**(based on [BCMS]) There is an algorithm $\mathsf{COMPRESS}$ that runs in $\mathrm{polylog} n$ time that given opening claims $CL_1=(C_1,z_1,v_1), CL_2=(C_2,z_2,v_2)$ with opening proofs $\pi_1,\pi_2$
constructs a new opening claim $CL$ such that
1. If $CL_1,CL_2$ are both correct then $CL$ is correct. Moreover, an opening proof $\pi$ for $CL$ can be constructed in quasilinear time in $n$, given only $CL_1,CL_2,\pi_1,\pi_2$.
2. If one of $CL_1,CL_2$ is not correct then except with neglgible probability $CL$ is incorrect.

**Proof:** $\mathsf{COMPESS}$ starts by running the $V_1$ part of the BP verifier on $CL_1$ and $CL_2$. If $V_1$ rejects one of the claims $\mathsf{COMPRESS}$ outputs $\mathrm{false}$. Otherwise, it obtains outputs $(h_1,D_1), (h_2,D_2)$ from $V_1$'s runs.
Now, $\mathsf{COMPRESS}$ obtains Fiat-Shamir challenges $z,\alpha\in F$, e.g. by hashing $(CL_1,CL_2,\pi_1,\pi_2)$. Next, it computes $v=h(z)$ where $h= h_1 + \alpha h_2$ - recall that $V_1$ guarantees to output $h_i$ such that this can indeed be computed in polylogarithmic time. It now computes $D=D_1+\alpha D_2$.
$\mathsf{COMPRESS}$ outputs the claim $CL=(D,z,v)$.
Note that if both claims were true, $D$ is a BP commitment to $h$ and so $CL$ is true (as we have explicitly computed $v$ as $h(z)$).
Moreover, since the polynomial $h$ is explicitly derived just from $CL_1,CL_2,\pi_1,\pi_2$, a prover can in time quasilinear in the degree $n$, compute a BP proof that $CL$ is correct.

For the soundness direction, see [BCMS] for a formal proof that when $CL_1$ or $CL_2$ are incorrect, the prover has negligible chance to come up with a proof that $CL$ is correct. The basic idea is that, for example, if $CL_1$ is false but $V_1$ accepted, $D_1$ is not a commitment to $h_1$ and so $D$ is very unlikely to be a commitment to $h$. Thus the prover can only convince us of $CL$ if he luckily finds some other polynomial $h'$ whose commitment *is* $D$, such that $h'$ happens to agree with $h$ on the randomly chosen $z$.

### Efficient recursion using deferral/accumulation
Let's see how the above corollary helps us obtain recursive SNARKs. What is usually needed for recursion is the ability to verify claims of the form "There is a valid SNARK proof $\pi$ for statement $X$".
Expressing this statement involves expressing the SNARK verification algorithm operating on the proof $\pi$. In the recent line of work on SNARKs based on polynomial commitment schemes (Sonic, Marlin, Plonk), the heavy part of the verification algorithm consists of checking opening claims. This would be especially costly to express in a circuit in the BP-PCS case, as the verification time is linear. In fact, the BP-PCS verification circuit will be larger by some constant factor than the circuit it is verifying a claim about - and so recursing by expressing the verifier as a circuit would lead to an explosion in circuit size as recursion depth grows.

The idea in Halo, is instead that the verifier in the middle of the recursive chain will only check that a certain opening claim $C_0$ given as public input, is the right claim to be checked to verify the recursion so far, and defer the actual checking to the final verifier at the end of the recursive chain. The $\mathsf{COMPRESS}$ method will ensure the number of checks being deferred stays at a constant (some constant depending on the base SNARK construction used in the recursion), and does not grow with recursion depth.

The advantage is that this verifier, as we shall see below, will only require an application of $\mathsf{COMPRESS}$ and thus expressing it in a circuit will be cheap.
Let us assume for simplicity that the base SNARK verification only involves checking one opening claim.
We thus have that the Halo verifier has to verify an opening claim $C_0$ given to it as public input, and some other opening claim $C_1$ - showing that the SNARK proof for the current circuit is correct (the exact circuit that was verifying $C_0$ is the correct claim to check for the recursion so far)
If this is another verifier in the middle of the recursive chain, they will not verify the claims $C_0,C_1$ but rather simply run $\mathsf{COMPRESS}$ to obtain a new claim $C$ they will send to the next verifier down the line.
The prover, will in turn compute and send to the next verifier the proof $\pi$ that the claim $C$ is indeed correct.