1# Decider for Onchain Verification
  2
  3**Overview**: This section describes the approach for the *Decider* (compressed SNARK / final proof) in order to be able to **verify the Nova+CycleFold proofs onchain (in Ethereum's EVM)**.
  4
  5> **Warning**: This section, as the rest of Sonobe, is experimental. The approach described in this section is highly experimental and has not been audited.
  6
  7
  8## Context
  9At the final stage of the Nova+CycleFold folding, after $n$ iterations, we have the committed instances $\{u_n, U_n, U_{EC,n} \}$ and their respective witnessess.
 10
 11![](../imgs/cyclefold-paper-diagram.jpg)
 12<span style="padding:20px;">*Diagram source: CycleFold paper ([https://eprint.iacr.org/2023/1192.pdf](https://eprint.iacr.org/2023/1192.pdf)). In the case of this document $n=i+2$, so $u_{i+2} = u_n$, $U_{i+2}=U_n$, $U_{EC,i+2}=U_{EC,n}$.*</span>
 13
 14<br>
 15
 16We work on a cycle of curves composed by $E_1$ and $E_2$, where $E_1.F_r = E_2.F_q$ and $E_1.F_q=E_2.F_r$.
 17We will use $F_r$ to refer to $E_1.F_r=E_2.F_q$, and $F_q$ to refer to $E_1.F_q=E_2.F_r$.
 18The main circuit constraint field is $F_r$, and $C_{EC}$ circuit constraint field is $F_q$.
 19
 20Since the objective is to verify the proofs on Ethereum, we set $E_1$=BN254 and $E_2$=Grumpkin. Thus, $F_r$ is the scalar field of the BN254.
 21
 22The $u_n$ and $U_n$ contain: $\{ \overline{E} \in E_1, \overline{W} \in E_1, u \in F_r, x \in F_r^{|io|} \}$
 23
 24And $U_{EC,n}$ contains: $\{ \overline{E} \in E_2, \overline{W} \in E_2, u \in F_q, x \in F_q^{|io|} \}$
 25
 26## Decider high level checks
 27*These are the same checks for both the Onchain & Offchain Deciders. The difference lays on how are performed.*
 28
 291. check $NIFS.V(r, U_n, u_n, \overline{T}) \stackrel{?}{=} U_{n+1}$
 302. check that $u_n.\overline{E}=0$ and $u_n.u=1$
 313. check that $u_n.x_0 = H(n, z_0, z_n, U_n)$ and $u_n.x_1 = H(U_{EC,n})$
 324. correct RelaxedR1CS relation of $U_{n+1}, W_{n+1}$ of the AugmentedFCircuit
 335. check commitments of $U_{n+1}.\{ \overline{E}, \overline{W} \}$ with respect $W_{n+1}$ (where $\overline{E}, \overline{W} \in E_1$)
 346. check the correct RelaxedR1CS relation of $U_{EC,n}, W_{EC,n}$ of the CycleFoldCircuit
 357. check commitments of $U_{EC,n}.\{ \overline{E}, \overline{W} \}$ with respect $W_{EC,n}$ (where $\overline{E},\overline{W} \in E_2$)
 36
 37## The Onchain Decider approach
 38The decider proof is computed once, and after all the folding has taken place. Our aim is to be able to verify this proof in the Ethereum's EVM.
 39
 40![](../imgs/decider-onchain-flow-diagram.png)
 41
 42The prover computes $(U_{n+1}, W_{n+1}, \overline{T}) = NIFS.P((U_n, W_n), (u_n, w_n))$
 43
 44The *Decider Circuit* verifies in its R1CS relation over $F_r$ the following checks:
 45
 46- 1.1: check that the given NIFS challenge $r$ is indeed well computed. This challenge is then used outside the circuit by the Verifier to compute NIFS.V obtaining $U_{i+1}$
 47- 2: check that $u_n.\overline{E}=0$ and $u_n.u=1$
 48- 3: check that $u_n.x_0 = H(n, z_0, z_n, U_n)$ and $u_n.x_1 = H(U_{EC,n})$
 49- 4: correct RelaxedR1CS relation of $U_{n+1}, W_{n+1}$ of the AugmentedFCircuit
 50- 5.1: Check correct computation of the KZG challenges
 51    $$c_E = H(\overline{E}.\{x,y\}),~~c_W = H(\overline{W}.\{x,y\})$$
 52    which we do through in-circuit Transcript.
 53- 5.2: check that the KZG evaluations are correct
 54    - $eval_W == p_W(c_W)$
 55    - $eval_E == p_E(c_E)$
 56    <br>where $p_W, p_E \in \mathbb{F}[X]$ are the interpolated polynomials from $W_{i+1}.W,~ W_{i+1}.E$ respectively.
 57- 6: check the correct RelaxedR1CS relation of $U_{EC,n}, W_{EC,n}$ of the CycleFoldCircuit (this is non-native operations and with naive sparse matrix-vector product blows up the number of constraints)
 58- 7: Pedersen commitments verification of $U_{EC,n}.\{ \overline{E}, \overline{W} \}$ with respect $W_{EC,n}$ (the witness of the committed instance)
 59(where $\overline{E},\overline{W} \in E_2$, this check is native in $F_r$)
 60<br>*The following check is done non-natively (in $F_r$):*
 61
 62Additionally we would have to check (outside of the circuit):
 63
 64- 1.2: check $NIFS.V(r, U_n, u_n, \overline{T}) \stackrel{?}{=} U_{n+1}$
 65- 5.3: Commitments verification of $U_{n+1}.\{ \overline{E}, \overline{W} \}$ with respect $W_{n+1}$ (where $\overline{E}, \overline{W} \in E_1$)
 66
 67The check 7 would be too expensive if using Pedersen commitments verification in-circuit (non-natively), so we changed these commitments from Pedersen to KZG, and then verify the KZG commitments outside of the circuit and directly onchain.
 68
 69The prover would generate a *Groth16* proof over BN254 for this *Decider Circuit*, which can later be verified onchain in the EVM together with the KGZ commitments of check 7 and check 8.
 70
 71In this way, the final proof to be verified onchain would be:
 72
 73- a Groth16 proof of the checks 1.1, 2, 3, 4, 5.1, 5.2, 6, 7
 74- the KZG proofs verification (check 5.3)
 75- the NIFS.V (check 1.2), which relates the inputs of the checks in the Groth16 proof and check 5
 76
 77<br>
 78
 79<u>The RelaxedR1CS checker circuit</u>
 80
 81The *"correct RelaxedR1CS relation"* (used in check 1) is checked by the gadget proposed by [Nalin Bhardwaj](https://twitter.com/nibnalin/), which is a R1CS circuit that checks the RelaxedR1CS relation, [more details here](https://github.com/privacy-scaling-explorations/sonobe/issues/19).
 82
 83The idea is that we check in a R1CS circiut the RelaxedR1CS relation ($Az \circ Bz - uCz -E=0$). Note that this approach has a blowup of `3x` with respect to the original circuit number of constraints `x` (when using sparse representation of the matrices).
 84
 85
 86### Circuit costs
 87> Note: the number of constraints written in this section is the current values that we have, which we aim to reduce in future iterations.
 88
 89<u>Estimated costs of the full decider-onchain circuit:</u>
 90
 91*(`x` is the number of constraints of the circuit that we're folding, and the AugmentedFCircuit takes ~52k constraints)*
 92
 93- 1.1: check that the given NIFS challenge $r$ is indeed well computed
 94- 2: $u_n$ check: `<1000`
 95- 3: $u_n.x$ hash check: `2634`
 96- 4: $U_{n+1}$ relation: `3(x+52k)`
 97- 5.1: Check correct computation of the KZG challenges: `7708`
 98- 5.2: check that the KZG evaluations are correct `262k`
 99- 6: $U_{EC,n}$ relation (non-native): `5.1M`
100- 7: Pedersen check of $U_{EC,n}$ commitments (native): `<5M` both commitments (including the inputs allocations). This is a couple of native MSMs of <1500 elements each one
101
102Total: 1000 + 2634 + 3*(x+52_252) + 7708 + 262_000 + 4_967_155 + 5_146_236
103
104eg: for a circuit of `500k` constraints the decider circuit would take approximately `11.9M` constraints.
105
106As can be seen, most of the costs come from the Pedersen commitments verification and the $U_{EC,n}$ relation (checks 6 and 7 respectively).