$\newcommand{\G}{\mathbb{G}}
\newcommand{\F}{\mathbb{F}}
\newcommand{\K}{\overline{K}}
\newcommand{\P}{\overline{P}}
\newcommand{\poseidon}{\textrm{poseidon}}
\newcommand{\groth}{\textrm{groth16}}$

# Scope
This document studies gnark proofs and the gnark verifier and describes the necessary changes to our Batch Verifier circuit to accept gnark proofs.

This document covers **what** the gnark verifier does, but doesn't cover:
- **why** gnark differs from standard Groth16, i.e., the rationale behind their modifications
- the gnark prover in detail
- serialization/data structure issues

It also doesn't cover contract or protocol changes.

# Goals
- Change the Batch Verifier circuit to support gnark (or as many variations of gnark as possible).
- Understand the performance tradeoff.

# Success Metrics
- Batch Verifier circuit accepts both gnark and snarkjs proofs.
- The circuit size doesn't increase by more than 100%.
- Minimal changes to circuit code.

# Context

## References
- Groth16 paper: https://eprint.iacr.org/2016/260.pdf
- BGM17 optimization: https://eprint.iacr.org/2017/1050
- LegoSNARK paper: https://eprint.iacr.org/2019/142.pdf
- gnark repo: https://github.com/Consensys/gnark
- notes on emulated pairing: https://hackmd.io/@ivokub/SyJRV7ye2

## Notation
- $B$ denotes the batch size.
- Padding notation:
- Lowercase: proof-specific, Uppercase: max.
- e.g. $\ell$ number of public inputs $\rightarrow$ $L \geq \ell$ max number of public inputs
- Overline: padded (in general with zeroes)
- e.g. $P_1, \dots, P_\ell$ public inputs $\rightarrow$ $\overline{P}_1, \dots, \overline{P}_L$ padded public inputs
- $e: \G_1 \times \G_2 \rightarrow \G_T$ pairing on the BN254 elliptic curve. Additive notation for $G_1$ and $G_2$, multiplicative for $G_T$.
- When there are two indices, $i$ denotes index within a batch, and $j$ denotes index within an app proof, e.g. $P_{ji}$ is the $j$-th public input of the $i$-th app proof.

## BGM17 optimization
Our current implementation assumes that $\gamma \in \G_2$ is the generator (as in the BGM17 optimization). However, gnark's setup generates a random $\gamma$.
This means that, in the BV circuit, when we do:
$$
e\left(\sum_{i=1}^B r^{i-1} \left( \K_{0i} + \sum_{j=1}^{L} \P_{ji} \K_{ji} \right), \gamma\right),
$$i.e., a single pairing for the $B$ proofs for the public input term, we have to replace it with
$$
\prod_{i=1}^B e\left( r^{i-1} \left( \K_{0i} + \sum_{j=1}^{L} \P_{ji} \K_{ji} \right) , \ \gamma_i\right),
$$
i.e. one pairing per proof instead of one pairing in total.

## gnark overview

### gnark verification key
A gnark verification key consists of a Groth16 verification key:
- $\alpha \in \G_1$
- $\beta, \gamma, \delta \in \G_2$
- $K_0, K_1, \dots, K_L \in \G_1$

together with
- A Pedersen commitment verification key
- $h_1, h_2 = -\frac{1}{\sigma}h_1 \in \G_2$ for some toxic nonzero scalar $\sigma$
- A vector `uint[][]` with the indices of the public/commitment commited variables.*

*: In this document, we consider the case there's only one commitment point. So we can reduce the vector to a `uint[]`. Furthermore, w.l.o.g. we can assume that:
- The first $\ell$ witness values are public inputs.
- The next $\mu$ witness values (namelyl, the first non-public witness values) are the variables committed to.

Therefore, we won't deal with this vector in this document.

### gnark proof

The proof consists of a Groth16 proof:
- $A, C \in \G_1$
- $B \in \G_2$

together with a Pedersen commitment and a Pedersen proof of knowledge:
- $M, \pi^{Ped} \in \G_1$

### gnark Pedersen commitment
Let's briefly explain what the Pedersen commitment is. Let $\{z_j\}$ denote the witness of a gnark proof. We separate the witness into three groups:
- The public input: $z_1, \dots, z_\ell$
- The commitment variables: $z_{\ell + 1}, \dots, z_{\ell + \mu}$
- The private witness: $z_{\ell + \mu + 1}, \dots, z_{m}$

In standard Groth16 (i.e. $\mu = 0$), the prover will compute
$$
C = \sum_{i = \ell+1}^m z_i H_{i-\ell} + \dots
$$where the points $H_i \in \G_1$ are part of the proving key. The verifier will later check that:
$$
e(A, B) = e(\alpha, \beta) e(\sum_{i=0}^\ell z_i K_i, \gamma) e(C, \delta).
$$

In gnark, the prover will instead compute
$$
C = \sum_{i = \ell+\mu +1}^m z_i H_{i-\ell} + \dots
$$
and a commitment to the $\mu$ commitment witness variables, as well as Pedersen proof of knowledge
$$
\begin{align}
M &= \sum_{i = \ell+1}^{\ell + \mu} z_i G_{i - \ell} \\
\pi^{Ped} &= \sum_{i = \ell+1}^{\ell + \mu} z_i \tilde{G}_{i - \ell}
\end{align}
$$
where the points $G_1, \dots, G_\mu$ are an extension of the points in the verification key $K_0, \dots, K_\ell$ and $\tilde{G}_i = \sigma G_i$ for some toxic nonzero $\sigma$.

Now the verifier checks
$$
\begin{align}
e(A, B) &= e(\alpha, \beta) e(\sum_{i=0}^\ell z_i K_i, \gamma) e(C, \delta) e(M, \gamma) \\
&= e(\alpha, \beta) e(\sum_{i=0}^\ell z_i K_i + M, \gamma) e(C, \delta)
\end{align}
$$
and (recall $h_2 = \frac{1}{\sigma} h_1$)
$$
e(M, h_1) e(\pi^{Ped}, h_2) = 1.
$$

## Correction: Commitment Hash
(TODO: modify above)
Any time the commitment $M$ is present, the Gnark verifier
1. Computes `digest := sha256(M.Marshal())`
2. Casts `digest` as `Fr`
3. Appends to public input vector.

The hash function in 1 is arbitrary, but sha256 is the default. Currently their [on-chain verifier](https://github.com/Consensys/gnark/pull/1063) only supports Sha256.

The UBV circuit changes as follows (for any choice of hash):
1. Compute `hash(M)`
- Is there any way around byte decomposing `M` for this?
- TODO: describe `M.Marshal()` serialization
2. Cast result as `Fr`
- will have to match Gnark's procedure
3. Append to public input vector
- Constrain `x -> x + digest * bit_vector`

### Approach 1: Sha2 Circuit
NEBRA customer leaves Gnark on default setting (sha256), we add a sha2 computation to the UBV circuit.

[ZkEmail's Sha2 circuit](https://github.com/zkemail/halo2-dynamic-sha256) uses halo2-lib frontend for circuit writing, so should be easy to integrate with ubv.
[Our fork](https://github.com/NebraZKP/halo2-dynamic-sha256) has a [test](https://github.com/NebraZKP/halo2-dynamic-sha256/blob/7310f2f83a52d17e1ea737428d0a74e66ca33d1a/src/lib.rs#L515) to measure cost of Sha2 digests.

For reference, the current size of UBV circuit (as of commit `24c48b`) is 100,934,111.

Sha256 digest is of `[a, b, c]` as `[u8; 3]`
| Num Digests | Num Advice |
| -------- | -------- |
| 1 | 279,797 |
| 10 | 1,592,901 |
| 20 | 3,185,801 |
| 40 | 6,371,601 |

### Approach 2: Keccak circuit
The Gnark prover can be set to use a different hash function:

groth16.Prove(compiledCS, provingkey, witness, 
   backend.WithProverHashToFieldFunction(sha3.NewLegacyKeccak256())

We could then send the bytes of each `proof.m` to the Keccak circuit to compute its digest. This would increase the UBV circuit size less than Approach 1. It would increase the Keccak circuit size but this is less of a concern. The outer circuit's public input gluing logic would change to wire the UBV/Keccak circuits differently.

This approach requires UPA users to set their Gnark prover to use keccak, as above.

### Design for keccak circuit
It seems that is likely that keccak will become their default hash function with gnark's new `TargetSolidity` setting. In this case, the main idea is to precompute the extra public input in the preprocessing phase of the UBV, and then feed the pairs (commitment, extra_public_input) to the keccak circuit, constraining them in the outer circuit to be equal.

### Approach 3: New Sha2 circuit
Rather than inserting the Sha2 computation into the already-costly UBV circuit we could add a new Sha2 Circuit, in addition to the Keccak circuit. This would be aggregated in the Outer Circuit as well. The benefit is being able to prove this in parallel with the final UBV proof for a batch, the downside is increasing the Outer Circuit proving time.

### Approach 4: Use Snark-friendly hash
We could also ask UPA users to set Gnark to hash using Poseidon/MIMC and add that computation to UBV. It would be the cheapest option for our proving time but probably the most friction for users. Also the on-chain universal G16 verifier would now have to compute this hash.

## Approaches

### Approach 0: Undo BGM17 optimization (required)
The simplest approach is to undo the BGM17 optimization, i.e., stop assuming $\gamma$ is the $\G_2$ generator in our BV circuit. That will bump the cost from $3B + 1$ pairings to $4B$, where $B$ is the batch size.

This will support gnark proofs **without** commitment points, but won't be enough to support more general gnark proofs.

### Option 1: Aggregate and verify the commitment point

When we receive a gnark proof, we will both add the commitment point $M$ and verify it was well-computed. In other words, the verifier will perform the following check
$$
\begin{align}
\prod_{i=1}^B &e(-r^{i-1} A_i, B_i)e(r^{i-1} \alpha_i, \beta_i) e(r^{i-1} (\sum_{j=0}^L \overline{P}_{ji} \overline{K}_{ji} + M_i), \gamma_i) \\ &\times e(r^{i-1} C_i, \delta_i) e(r^{i-1} t \ M_i, h_{1i})e(r^{i-1} t \ \pi^{Ped}_i, h_{2i}) = 1
\end{align}
$$

where $r$ and $t$ are independent challenge points. Note that this increases the number of pairings to $6B$, twice as many as the current BV circuit has.

### Option 2: Aggregate and verify multiple commitment points

In the most general case, gnark proofs can have more than one commitment point. We first have to fix a max number of commitment points that we want to support, say $N_C$. Then we pad the set $M_1, \dots, M_{n_C}$ with zeroes (similarly to what we do with the vk's and the public inputs) to $\overline{M}_1, \dots, \overline{M}_{N_C}$. We do the same with the Pedersen proofs of knowledge. Then the verifier circuit performs the following check
$$
\begin{align}
\prod_{i=1}^B &e(-r^{i-1} A_i, B_i)e(r^{i-1} \alpha_i, \beta_i) e(r^{i-1} (\sum_{j=0}^L \overline{P}_{ji} \overline{K}_{ji} + \sum_{j=1}^{N_C} M_{ji}), \gamma_i) \\ &\times e(r^{i-1} C_i, \delta_i) e(r^{i-1} \sum_{j=1}^{N_C} t^{j} \overline{M}_{ji}, h_{1i})e(r^{i-1} \sum_{j=1}^{N_C} t^{j}\overline{\pi}^{Ped}_{ji}, h_{2i}) = 1
\end{align}
$$

Note that there are no extra pairings w.r.t. approach 1, only 2 extra $\G_1$ MSMs of length $N_C$.

### Note on the circuitId

Note approaches 1 and 2 require a change in the definition of the CircuitId to include the elements $h_1$ and $h_2$.

$$
C_{ID} = \poseidon(vk^{\groth}, h_1, h_2)
$$

- Do we want a domain separator between gnark and Groth16 proofs?
- Do we need to include the vector with indices here?

# SnarkJS/Gnark "Universality"
Not sure how to name this (or if it even belongs in this doc) but the question here is how to design a single UBV circuit capable of handling either "pure Groth16" proofs (as produced by SnarkJS, for example) or "Gnark Groth16" proofs with the additional commitment $M$. This section assumes a single commitment, as in "Option 1" above.

So we assume the proof/verifying key types are modified to (see branch [`gnark-playground`](https://github.com/NebraZKP/Saturn/tree/gnark-playground))

pub struct Proof {
    pub a: G1Affine,
    pub b: G2Affine,
    pub c: G1Affine,
    /// Gnark commitment point
    pub m: G1Affine,
    /// Pedersen knowledge proof
    pub pkp: G1Affine,
}

pub struct VerificationKey<C1 = G1Affine, C2 = G2Affine>
{
    pub alpha: C1,
    pub beta: C2,
    pub gamma: C2,
    pub delta: C2,
    pub s: Vec<C1>,
    // Gnark-specific points
    pub h1: C2,
    pub h2: C2,
}

Then we would need to
1. "Pad" pure Groth16 proofs with $M, \pi^{Ped}$
- May require a flag `has_commitment: bool` indicating whether this proof has a non-padding commitment part, similar to the `length` data field we use on padded public inputs.
- Constraints to enforce the correctness of this padding
2. Compute our circuit-id differently in the two cases
- Unclear how existing `trait InCircuitPartialHash` could be used for this, since there are now two optional parts of the VK (the `h_i` points and the `s_i` points)
- Brute force solution: Use existing var len Poseidon hasher twice, once for "pure Groth" case and once for "Gnark commitment" case. Select correct value using `has_commitment` flag
3. Derive the `r` challenge point including the points $M, \pi^{Ped}$. Doesn't matter if these are padding values or not.
4. Derive an additional `t` challenge point using...? TODO
- Would simply squeezing the hasher once more after squeezing `r` from it be okay? Seems to produce an independent challenge point
5. Add $M$ to the PI term.
- If padded $M$ can be taken as the identity point, we can simply add it in all cases.
- Otherwise we'd need to add `has_commitment * M` so as not to modify the result in the pure Groth case
6. Include $(M, h_1)$, $(\pi^{Ped}, h_2)$ pairs.
- Should be possible to choose padding values of $M, \pi^{Ped}, h_1, h_2$ such that these pairings are satisfied. Then there's no need to do any conditional selecting on the pairing check.

### Notes
- Proof padding: We can't use `G1::identity()` as the padding value for $M, \pi^{Ped}$ because the circuit will try to scale these values by $r^it$ using `scalar_multiply`, which assumes the curve point is non-identity.
- Therefore the public input $+M$ computation needs to be done as `public_input_term + has_commitment * M`
- ~~VK Padding: We can pad the VK using `h1 = h2 = G2::identity()` because we never scalar multiply a `G2` point. This will produce the pairing results $e(M,h_1) = e(\pi^{Ped}, h_2) = 1$ regardless of the padding values we use for $M, \pi^{Ped}$.~~
- No, the `halo2_ecc` pairing chip cannot compute pairing in-circuit when one of the points is the group identity. We can instead engineer the padding checks so that $e(M,h_1) e(\pi^{Ped}, h_2) = 1$ by choosing padding values
- `m = G1Affine::generator()`
- `pkp = - G1Affine::generator()`
- `h1 = G2Affine::generator()`
- `h2 = G2Affine::generator()`
- Proof ID computation: The `has_commitment` metadata field should be part of the Proof ID, just as PI `len` currently is.

### Spec Diff
The diff to the UBV spec should be roughly this:

- Proof type changed to

pub struct Proof {
    pub a: G1Affine,
    pub b: G2Affine,
    pub c: G1Affine,
    /// Gnark commitment flag
    pub has_commitment: bool,
    /// Gnark commitment point
    pub m: G1Affine,
    /// Pedersen knowledge proof
    pub pkp: G1Affine,
}

- VK type changed to

pub struct VerificationKey<C1 = G1Affine, C2 = G2Affine>
{
    pub alpha: C1,
    pub beta: C2,
    pub gamma: C2,
    pub delta: C2,
    pub s: Vec<C1>,
    // Gnark-specific points
    pub h1: C2,
    pub h2: C2,
}

- Preprocessing:
- "Compute the extra public input from the commitment point": `PI_{l + 1} = \keccak(proof.M, proof.pkp)`
- "Pad the verification key with generator": Now in addition to padding the $s_i$ vector with G1 generator we also pad `h1, h2` using G2 identity according to the value of `proof.has_commitment`. This could be done in circuit as `vk.h1 = ec_select_from_bits(..., has_commitment, vk.h1, g2_identity)`
- "Pad the commitment portion of proof": Assign the `proof.M, proof.pkp` according to the value of `proof.has_commitment`. Can be done as above, just using `g1_gen` instead of the identity point.
- Step 1a: Check the padding.
- Already said above how the Gnark-specific padding can be enforced by the circuit. Maybe that should be moved to this section of spec.
For the $l+1$-th input and vk.s elements we'll check they're padding points if and only if `proof.has_commitment = false`.
- Step 1b: Check the proof points
- Now we also check `proof.m, proof.pkp`. Should also check that `has_commitment` is bool.
- Step 2: Compute Circuit IDs
- The definition changes to

    circuitId = if proof.has_commitment {
        var_len_poseidon(DT1, len+1, alpha, beta, gamma, delta, h1, h2, s)
    } else {
        var_len_poseidon(DT2, len, alpha, beta, gamma, delta, s)
    }

Note in the first variant we do `len+1` to account for the extra non-padding element in vk.s which will be multiplied by the extra public input in the MSM
- [TODO: Describe brute force method of computing this in circuit]
- Step 3: Compute the challenge point
- Now includes hashing in the `proof.m, proof.pkp` points for the `r` challenge
- TODO: Define the `t` challenge point. Ideally it's just an additional squeeze of existing hasher
- Step 4: Compute the public input term
- Now `S_i = ... + has_commitment * M`
- Step 5: Compute the other pairs
- Scale $\tilde M_i = r^{i-1}t \cdot M_i$ and $\tilde \pi^{Ped}_i = r^{i-1}t \cdot \pi^{Ped}_i$
- Step 6: Compute the pairing
- There will be the $\gamma \ne 1$ change to spec
- The pairs $(\tilde M_i, h_1), (\tilde \pi^{Ped}_i, h_2)$ are included

The UBV will also expose `proof.m` and `proof.has_commitment` for each app proof as public.

On the keccak circuit side, the keccak circuit, on top of what it does now, will take as public inputs (for each app proof):
- `proof.m` (i.e. 3 $\F_r$ elements)
- `proof.has_commitment`

Then, it will select the $l+1$-th public input (call it `extra_input`) and enforce the following constraint:
- `has_commitment*(keccak(proof.m) - extra_input) = 0`

The outer circuit will take the UBV and keccak instances as usual and enforce the following copy-constraints for every application proof:
- `proof.m` in UBV = `proof.m` in keccak
- `proof.has_commitment` in UBV = `proof.has_commitment` in keccak

Note that:
- `extra_input` in UBV = `extra_input` in keccak
is already being enforced as part of the copy-constraints currently enforced in the outer circuit.

## Sketch
UBV's PIs (per proof)

length
has_commitment
cid
padded_instance
commitment_limbs (6 Frs)
keccak_of_commitment (1 Fr)

UBV always exposes correct keccak of commitment (even when commitment is padding) and includes constraint
`instance[length + 1] == has_commitment * keccak_of_commitment`

Keccak has

length
cid
padded_instance
commitment_limbs (6 Frs)
keccak_of_commitment (1 Fr)

and enforces that `keccak_of_commitment` is correct.

Then outer circuit wires these things together.

# Questions
- Is what I do with the challenge points sound? In the paper they perform some Pedersen commitment folding.
- How many commitment points should we support (if any)?
- How does the `uint[][]` vector with commitment indices work exactly in the verifier algorithm? How do we add it to the BV circuit?

# Remarks
Can we half-verify a gnark proof?