Reduce the number of constraints in DeciderEthCircuit

[winderica]

The major cost of DeciderEthCircuit is due to the non-native field operations in RelaxedR1CSGadget::check.

Let's first briefly see how field emulation is done.

First, we consider encoding arbitrary precision integers (Big{Int, Uint}) in-circuit. We first split the value $v$ into limbs $v_0, ..., v_{n - 1}$ that have a specific width (let's call it ideal width) $W$, where $v_i \in [0, 2^W)$ for all $i$.

Then, we can do operations in a limb-wise fashion. For example, multiplication of $u = u_0 + u_1 2^W = \{ u_0, u_1 \}$ and $v = v_0 + v_1 2^W = \{ v_0, v_1 \}$ results in $u_0 v_0 + (u_0 v_1 + u_1 v_0) 2^W + u_1 v_1 2^{2W} = \{ u_0 v_0, u_0 v_1 + u_1 v_0, u_1 v_1 \}$. Note that the limb widths change after each operation, and they may reach the capacity of the underlying native field sometime. We can also observe that after some operations, the "weight" of the $i$-th limb is still $2^{iW}$, i.e., $x = x_0 + x_1 2^W + x_2 2^{2W} + \cdots$ for arbitrary $x$.

To avoid limb overflow, we need to perform an operation called align before the limb widths reach the limit. Basically we can decompose the limbs into bits and recompose them into new limbs with ideal width, but this is super expensive.

Now, for enforcing the equality between two non-native variables, it is incorrect to simply compare the limbs, as these variables might be the results of different operations and have different limb widths. An intuitive way to fix this is to align both of them (so that limbs in both of them have width $W$) and then check the aligned limbs, but this is sub-optimal. In fact, the equality can be checked in a more efficient way than calling two aligns, according to xJsnark (although still pretty costly). See NonNativeUintVar::enforce_equal_unaligned for details.

In arkworks' NonNativeFieldVar, we are not working on arbitrary integers, but on field elements. This means that we need to modulo the non-native field order $m$ after each operation. This, dubbed reduce, not only involves the enforce_equal_unaligned check (for ensuring $x = q m + r$, where $q$ is the quotient and $r$ is the remainder), but also requires a non-native comparison (for ensuring $0 \le r < m$) (arkworks doesn't check this, but I think this is needed for soundness), resulting in a lot of constraints, especially in our case where we need to compute $\sum x_i y_i$.

This PR reduces the number of constraints in DeciderEthCircuit by avoiding enforce_equal_unaligned and reduce when possible. This is done by:

1. Treat the addition and multiplication in $\sum x_i y_i$ as integer operations, and only do the modulo operation in the final check.
2. Set an ideal limb width that allows the underlying native field to contain every limb in $\sum x_i y_i$.

Although one may achieve the above by leveraging arkworks' MulResultVar, a customized struct NonNativeUintVar is introduced to:

1. Allow more fine-grained control on $W$. (The current choice $W = 55$ may not be the best. Setting a smaller $W$ will decrease the number of constraints, but trusted setup and proof generation take more time. I will look into this in a new PR.)
2. Bypass the limitation that we can not further multiply MulResultVars, so that we can compute $Az \circ Bz$ (4 multiplications for each element $(\sum a_i z_i) \cdot (\sum b_i z_i)$ ) without modulo operations.

With this PR, DeciderEthCircuit (with check 7 disabled due to #80) now only costs 9_547_318 constraints. Trusted setup and proof generation takes 90-100s on an i9-12900K, and the peak RAM usage is 20-30GB.

[arnaucube]

This is awesome! Thank you very much for this 🙌

You did many improvements! Not only the big improvement in the nonnative operations that drastically reduce the number of constraints in the DeciderEthCircuit, but also the utils::gadgets look much better now, and even the changes in the CycleFold circuit make a lot of sense.
I've read the nonnative/* code, but I must say that I haven't cross-checked the logic with the referenced code and paper.

Left just two small suggestions, but overall LGTM!

P.S.: Also, thank you very much for the clear explanations in the PR message and also in all the comments along the code.