reorganize onchain decider checks description to a more clear approach

src/design/nova-decider-onchain.md

@@ -23,8 +23,18 @@ The $u_n$ and $U_n$ contain: $\{ \overline{E} \in E_1, \overline{W} \in E_1, u \
 
 And $U_{EC,n}$ contains: $\{ \overline{E} \in E_2, \overline{W} \in E_2, u \in F_q, x \in F_q^{|io|} \}$
 
+## Decider high level checks
+*These are the same checks for both the Onchain & Offchain Deciders. The difference lays on how are performed.*
 
-## The Decider approach
+1. check $NIFS.V(r, U_n, u_n, \overline{T}) \stackrel{?}{=} U_{n+1}$
+2. check that $u_n.\overline{E}=0$ and $u_n.u=1$
+3. check that $u_n.x_0 = H(n, z_0, z_n, U_n)$ and $u_n.x_1 = H(U_{EC,n})$
+4. correct RelaxedR1CS relation of $U_{n+1}, W_{n+1}$ of the AugmentedFCircuit
+5. check commitments of $U_{n+1}.\{ \overline{E}, \overline{W} \}$ with respect $W_{n+1}$ (where $\overline{E}, \overline{W} \in E_1$)
+6. check the correct RelaxedR1CS relation of $U_{EC,n}, W_{EC,n}$ of the CycleFoldCircuit
+7. check commitments of $U_{EC,n}.\{ \overline{E}, \overline{W} \}$ with respect $W_{EC,n}$ (where $\overline{E},\overline{W} \in E_2$)
+
+## The Onchain Decider approach
 The 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.
 
 ![](../imgs/decider-onchain-flow-diagram.png)
@@ -33,26 +43,26 @@ The prover computes $(U_{n+1}, W_{n+1}, \overline{T}) = NIFS.P((U_n, W_n), (u_n,
 
 The *Decider Circuit* verifies in its R1CS relation over $F_r$ the following checks:
 
-1. correct RelaxedR1CS relation of $U_{n+1}, W_{n+1}$ of the AugmentedFCircuit
-2. check that $u_n.\overline{E}=0$ and $u_n.u=1$
-3. check that $u_n.x_0 = H(n, z_0, z_n, U_n)$ and $u_n.x_1 = H(U_{EC,n})$
-4. Pedersen commitments verification of $U_{EC,n}.\{ \overline{E}, \overline{W} \}$ with respect $W_{EC,n}$ (the witness of the committed instance)
-(where $\overline{E},\overline{W} \in E_2$, this check is native in $F_r$)
-<br>*The following check is done non-natively (in $F_r$):*
-5. 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
-6. Check correct computation of the KZG challenges
+- 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}$
+- 2: check that $u_n.\overline{E}=0$ and $u_n.u=1$
+- 3: check that $u_n.x_0 = H(n, z_0, z_n, U_n)$ and $u_n.x_1 = H(U_{EC,n})$
+- 4: correct RelaxedR1CS relation of $U_{n+1}, W_{n+1}$ of the AugmentedFCircuit
+- 5.1: Check correct computation of the KZG challenges
     $$c_E = H(\overline{E}.\{x,y\}),~~c_W = H(\overline{W}.\{x,y\})$$
     which we do through in-circuit Transcript.
-7. check that the KZG evaluations are correct
+- 5.2: check that the KZG evaluations are correct
     - $eval_W == p_W(c_W)$
     - $eval_E == p_E(c_E)$
-where $p_W, p_E \in \mathbb{F}[X]$ are the interpolated polynomials from $W_{i+1}.W,~ W_{i+1}.E$ respectively.
-8. 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}$
+    <br>where $p_W, p_E \in \mathbb{F}[X]$ are the interpolated polynomials from $W_{i+1}.W,~ W_{i+1}.E$ respectively.
+- 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)
+- 7: Pedersen commitments verification of $U_{EC,n}.\{ \overline{E}, \overline{W} \}$ with respect $W_{EC,n}$ (the witness of the committed instance)
+(where $\overline{E},\overline{W} \in E_2$, this check is native in $F_r$)
+<br>*The following check is done non-natively (in $F_r$):*
 
 Additionally we would have to check (outside of the circuit):
 
-9. Commitments verification of $U_{n+1}.\{ \overline{E}, \overline{W} \}$ with respect $W_{n+1}$ (where $\overline{E}, \overline{W} \in E_1$)
-10. check $NIFS.V(r, U_n, u_n, \overline{T}) \stackrel{?}{=} U_{n+1}$
+- 1.2: check $NIFS.V(r, U_n, u_n, \overline{T}) \stackrel{?}{=} U_{n+1}$
+- 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$)
 
 The 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.
 
@@ -60,9 +70,9 @@ The prover would generate a *Groth16* proof over BN254 for this *Decider Circuit
 
 In this way, the final proof to be verified onchain would be:
 
-- a Groth16 proof of the checks 1-8
-- the KZG proofs of the check 9
-- the NIFS.V (check 10), which relates the inputs of checks 1-8 and check 9
+- a Groth16 proof of the checks 1.1, 2, 3, 4, 5.1, 5.2, 6, 7
+- the KZG proofs verification (check 5.3)
+- the NIFS.V (check 1.2), which relates the inputs of the checks in the Groth16 proof and check 5
 
 <br>
 
@@ -80,17 +90,17 @@ The idea is that we check in a R1CS circiut the RelaxedR1CS relation ($Az \circ
 
 *(`x` is the number of constraints of the circuit that we're folding, and the AugmentedFCircuit takes ~52k constraints)*
 
-1. $U_{n+1}$ relation: `3(x+52k)`
-2. $u_n$ check: `<1000`
-3. $u_n.x$ hash check: `2634`
-4. 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)
-5. $U_{EC,n}$ relation (non-native): `5.1M`
-6. Check correct computation of the KZG challenges: `7708`
-7. check that the KZG evaluations are correct
-8. check that the given NIFS challenge $r$ is indeed well computed
+- 1.1: check that the given NIFS challenge $r$ is indeed well computed
+- 2: $u_n$ check: `<1000`
+- 3: $u_n.x$ hash check: `2634`
+- 4: $U_{n+1}$ relation: `3(x+52k)`
+- 5.1: Check correct computation of the KZG challenges: `7708`
+- 5.2: check that the KZG evaluations are correct `262k`
+- 6: $U_{EC,n}$ relation (non-native): `5.1M`
+- 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
 
-Total: 3 * (x + 52_252) + 1000 + 2634 + 4_967_155 + 5_146_236 + 7708
+Total: 1000 + 2634 + 3*(x+52_252) + 7708 + 262_000 + 4_967_155 + 5_146_236
 
-eg: for a circuit of `500k` constraints the decider circuit would take approximately `11.7M` constraints.
+eg: for a circuit of `500k` constraints the decider circuit would take approximately `11.9M` constraints.
 
-As can be seen, most of the costs come from the Pedersen commitments verification and the $U_{EC,n}$ relation
+As can be seen, most of the costs come from the Pedersen commitments verification and the $U_{EC,n}$ relation (checks 6 and 7 respectively).