# Proof aggregation using GKR
refer to: https://hackmd.io/@OFccBlU5TNCiRhpIyT1m7g/ryxC5Omfo
## Background
refer to: https://ethresear.ch/t/using-gkr-inside-a-snark-to-reduce-the-cost-of-hash-verification-down-to-3-constraints/7550

### Proof aggregation
Proof aggregation can be done by recursive proof. In above diagram, except for the initial step and the last step, all intermediate steps get previous proof and witnesses. And then they make a GKR proof and pass it to next proving.
### General GKR protocol
In this protocol, intermediate GKR used function $f_{r_i}^{(i)}(b, c)$. $$f_{r_i}^{(i)}(b, c) = \widetilde{add}_i(r_i, b, c)(\widetilde{W}_{i+1}(b) + \widetilde{W}_{i+1}(c)) + \widetilde{mult}_i(r_i, b, c)(\widetilde{W}_{i+1}(b) \cdot \widetilde{W}_{i+1}(c))$$
$\widetilde{W}$ is function that returns gate's calculation result in the arithmetic circuit.
### Re-construct arithmetic circuit
GKR protocol is made for layered arithmetic circuit. However, circom is optimized for R1CS.
`r1cs` file has constraints that have `A * B = C` form inside. For reconstruction of the arithmetic circuit, make two gates that represent `A * B` and `C * (-1)`. And make addition gate for these two gates. That gate's value will be 0. Naively, put a new gate from one constraint repeatedly.
## Structure
For each step in recursion, aggregator makes a new circuit from circuit that can verify previous proof and original circuit. And then generate proof from that circom file (exactly, from `.r1cs` and `.wtns` file)
### Initial round
Parse r1cs file and convert it to `GKRCircuit`. (Let's call this $C_0$)
Get input from `input.json`.
Calculate all nodes value $\widetilde{W}(b, c)$ by circuit and input.
Make proof $\pi_0$ from `Input` and `GKRCircuit`.
### Iterative round (0 < $i$ < n)
There are two circuit $C_i$ and $C_{v_{i - 1}}$. $C_{v_{i - 1}}$ is circuit that can verify $C_{i - 1}$.
$C_{v_i}$ can be different form for each circuit $C_i$. If use same circuit for all $C_i$, then $C_v$ will be same circuit.
To make aggregated proof for previous proof and current round's proof, we need
- input (for $C_i$)
- proof $\pi_{i - 1}$
Make integrated circuit $C'_i$.
Use those inputs, make proof $\pi_i$.
To be specific, input and proof $\pi_{i - 1}$
### Last round
Also there are two circuit $C_n$ and $C_{v_{n - 1}}$. To send aggregated proof to on-chain verifier, we can use groth16 prover in `snarkjs`.
Integrated circuit $C'_{n}$ can be proved with `snarkjs` also.
So final proof $\pi_n$ is groth16 or plonk proof
**why I made this**
I implemented gkr verifier in circom. but it can verify only one proof and cannot make recursion.
gkr verifier in circom (verifying circuit) can verify gkr proof but it can generate only groth16 and plonk proof by snarkjs.(It is so-called proof composition) Internal gkr proof cannot be made from that circom circuit.
So there were two options.
(1) Implement new circuit representation and re-implement gkr verifier in that representation
But it was too hard to implement verifying circuit from arithmetic circuit.
(2) Implement conversion from circom circuit to gkr circuit
If this is done, gkr verifier in circom can be converted to gkr circuit. And also we can reuse implemented circuit in circom. So I chose (2).
## Benchmark
I verified aggregated external groth16 proof that is generated from Mimc verification circuit with 3 input sets.
Intermediate proofs(gkr proof) are verified in the aggregated (newly generated) circuit.
It takes 45s to prove three input sets and generate Groth16 proof (Macbook M1 Pro 8 cores)
This protocol can aggregate up to 4 ~ 5 proofs in 1m. More than 5 proofs make intermediate GKR proof too large.
Much more optimizations should be applied to if want to use this aggregator for framework.
## Further works
- Applying https://eprint.iacr.org/2020/1247 will reduce circuit size.
- Applying FFT will reduce proving time, but most of the operations are multiplying monomials that have two term. So it cannot reduce proving time significantly
- It has security issues like initial randomness and others. For now, this system makes deterministic proof for inputs. It can be fixed with initial randomness.
### Different approach
This aggregator is based on proof aggregation using fully recursive proof. But GKR's verifier has more constraints than the previous circuit. With that, it is not efficient for aggregation. If we use it as partial prover, it might be better to make this like IVC(Incrementally Verifiable Computation).