# Aztec emulated field and group operations
**Disclaimer:** This documentation was written on September, 2021. It is intended to give readers a high-level understanding. The codebase is the canonical source of truth, and over time this document might fall behind the implementation details of the code.

## Emulated Field
We want to evaluate a modular multiplication of $\mathbb{F}_p$ elements a, b, using constraints over $\mathbb{F}_n$ ($p,n$ are prime). In particular we allow for the case where $n < p$.
We will choose integer $t$ such that $2^t\cdot n> p^2$. And also leverage operations mod $2^t$ together with the CRT.

In more detail:
We will check that as positive integers
$$a\cdot b = q\cdot p +r $$
The way we do this at a high level is
1. check that the equation holds both mod $2^t$ and mod $n$
2. check that each side of the equation is smaller than $M:=2^t\cdot n$.

The first, using CRT, implies the equation hold mod $M$. Then the second implies the equation hold over the integers since both sides are smaller than $M$. This in turn implies $a\cdot b =r$ mod $p$, which means $r$ is the correct multiplication result in $\mathbb{F}_p$.

### Notation summary:

* p = non-native field modulus
* n = native circuit modulus
* $2^t$ = extra CRT modulus
* $p'$ = $-p$ mod $2^t$
* $a_0, a_1, a_2, a_3$ are the 4 limbs of a.
* b = maximum size of a limb (e.g. b = 2^68 in the code)
* $s<t$ - number of bits of $p$ (having seprate $s,t$ parameters will be helpful for "lazy reductions" e.g. for long addition chains, see Aztec bigfield class for details).

Unless specified, all arithmetic is modulo n.

When we say 'compute' a variable we mean also insert constraints to enforce that value.

### Multiplication algorithm:
Assume for simplicity that $b=t/4$ below.

1. Compute witnesses $q$ and $r$ such that $ab -qp -r = 0$.
2. Apply range constraints on the limbs of $q, r$ such that they are all $<2^b$.
3. Apply multiplication gates and addition gates to evaluate the following intermediate products mod $2^t$ (note that other intermediate products that arise in $ab-qp$ are zero mod $2^t$):

* $(a_0b_0 + q_0p'_0)$ - bits $[0,t/2+1]$
* $(a_0b_1 + a_1b_0 + q_0p'_1 + q_1p'_0)$ -bits $[t/4,3t/4+2]$
* $(a_0b_2 + a_1b_1 + a_2b_0 + q_0p'_2 + q_1p'_1 + q_2p'_0)$ - bits $[t/2,t+3]$.
* $(a_0b_3 + a_1b_2 + a_2b_1 + a_3b_0 + q_0p'_3 + q_1p'_2 + q_2p'_1 + q_3p'_0)$ - bits $[3t/4,5t/4+3]$

Let's call these 4 (size ~2b) limbs $t_0, t_1, t_2, t_3$.
We can create them using 10 mult-add gates (the terms $q_ip'_j$ can be added to the multiplication $a_ib_j$ cause $p$ is fixed)

Note that the range of each $t_i$ follows from the range checks on the limbs of $a,b,q$.

4. Compute $u_0 = t_0 + 2^b \cdot t_1 - r_0 - 2^b \cdot r_1$ and $u_1 = t_2 + 2^b \cdot t_3 - r_2 - b \cdot r_3$.

Both $u_0$ and $u_1$ should be in the range [0, 3b] (plus some overflow bits). Moreover, the first $2b$ bits of $u_0$ should be zero because we have subtracted from them the low 2b-bits of the remainder term using $r_0,r_1$. Same holds for the first $2b$ bits of $u_0/(2^{2b}) +u_1$.

5. Compute $v_0$ such that $u_0 = v_0 \cdot 2^{2b}$

6. Validate $v_0$ is in the range [0, b].

7. Compute $v_1$ such that $u_1 + v_0 = v_1 \cdot 2^{2b}$.
8. Validate $v_1$ is in the range [0,b] plus some overflow bits.

9. Finally, to use the CRT, check also that $ab-pq-r=0$ $(mod\; n)$. Since $n$ is the native modulus this can be done very efficiently.

10. Range constrain $q$ so that $q\cdot p+r<2^t\cdot n$. The reason this range constraint is needed is that the CRT allows us to verify the desired equality $ab=pq+r$ as integers only when both side of the equation are smaller than $2^t\cdot n$.
*Note that for this to be possible we need in partciular that $t$ is large enough so that $2^t\cdot n > p^2+p$.*

#### acknowledgements: Thanks to Onur Kilic & Xin for pointing out necessity of step 10