# circom-ecc spec

## Preliminaries
### 'Signs' in circom:
A native number in circom is an element of $\{0,\dotsc,r - 1\}$ where $r$ is the baby JubJub prime. We map these elements to the integers as follows:

toZ(z) = z-r  if r//2 +1 <= x < r
toZ(z) = z,   otherwise.

We have $z$ and $toZ(z)$ are always congruent to each other mod $r$.

**Lemma 1.** Let $a,b,c \in \mathbb F_r$. Assume that $|toZ(a)| |toZ(b)| + |toZ(c)| < r/2$.
Then $toZ(a\cdot b + c) = toZ(a)toZ(b) + toZ(c)$.

*Proof.* We know that $ab +c \equiv toZ(ab+c) \pmod r$. Since $a \equiv toZ(a) \pmod r$, $b \equiv toZ(b) \pmod r$, $c \equiv toZ(c) \pmod r$, we have
$$
toZ(ab + c) \equiv toZ(a)toZ(b) + toZ(c) \pmod r.
$$
The LHS is uniquely determined by being in range $(-r/2, r/2)$. The assumption implies the RHS is also in range $(-r/2,r/2)$ by triangle inequality. Thus LHS = RHS. $\square$

### Proper BigInt representation

Given parameters `n, k` we say that a length `k` array `a` is a **proper BigInt representation** if each **register** `0 <= a[i] < 2^n` for all `i in range(k)`. The BigInt being represented is
$$
\sum_{i=0}^{k-1} a_i \cdot 2^{n \cdot i}
$$
In other words, this is base `2^n` little-endian notation.

We assume throughout that `n <= 252` so `2^n < r/2` (`r` is 254 bits).

### Signed overflow representation

Given parameters `n, k` we say that a length `k` array `a` is a **signed overflow representation** if $a_i < r/2$ for all $i$ and the integer being represented is
$$
\sum_{i=0}^{k-1} toZ(a_i) \cdot 2^{n\cdot i}
$$
Note the $a_i$ are allowed to have absolute value $|toZ(a_i)|$ possibly larger than `2^n`.

We will say **max overflow bits** of `a` to mean

max_{i in range(k)} abs(toZ(a[i])).bit_length()

## Circuits
### `BigMultNoCarry(n, ka, kb, m_out)` [Signed Version]
[circom-ecdsa](https://github.com/0xPARC/circom-ecdsa/blob/08c2c905b918b563c81a71086e493cb9d39c5a08/circuits/bigint.circom#L179)
Aka `BigMultShortLongUnequal` in [circom-pairing](https://github.com/yi-sun/circom-pairing/blob/743d761f07254ea6407d29ba05f29886cfd14aec/circuits/bigint.circom#L277)

Multiplication of two polynomials in one variable `X`.

#### Inputs:

- `a[]` is array of length `ka` as [signed overflow representation](#Signed-overflow-representation)
- `b[]` is array of length `kb`
- Say $|toZ(a_i)| < B_a$ for $0 \le i < k_a$ and $|toZ(b_i)| < B_b$ for $0 \le i < k_b$. Then assume that
$$
min(k_a, k_b) B_a \cdot B_b < r/2$$

#### Output:

- `out[]` is array of length `ka + kb - 1`
- `out[]` is uniquely defined by the polynomial identity
$$
\sum_{i=0}^{k_a + k_b - 2} toZ(out_i) \cdot X^i = \left( \sum_{i=0}^{k_a - 1} toZ(a_i) \cdot X^i \right) \left( \sum_{i=0}^{k_b - 1} toZ(b_i) \cdot X^i \right)
$$
as polynomials in the variable $X$.

#### Parameters:
- `n` is passed for convenience but not actually used!
- `ka, kb`
- [Convenience; not used in proof] For code readability/verification, `m_out` is passed as a parameter to indicate that all `toZ(out[i])` for `0 <= i < ka + kb - 1` **should** have absolute value `< 2^{m_out}`.

#### Proof:
`out[]` is given as witness values.

Compute
$$\begin{align}
out(x) &= \sum_{i=0}^{k_a + k_b - 2} out_i \cdot x^i \\
a(x) &= \sum_{i=0}^{k_a - 1} a_i \cdot x^i \\
b(x) &= \sum_{i=0}^{k_b - 1} b_i \cdot x^i
\end{align}
$$
for values $x = 0,1,\dotsc, k_a + k_b - 2$. These terms are linear in the signals $out_i, a_i, b_i$.

Constrain $out(x) === a(x) b(x)$ for $x = 0,\dotsc, k_a+k_b - 2$.

This means that $out(X) - a(X)b(X)$ is a degree $\le k_a + k_b - 2$ polynomial with at least $k_a + k_b - 1$ roots. This implies $out(X) - a(X)b(X) = 0$.

Expanding the polynomial multiplication $a(X)b(X)$, we deduce that
$$
out_i = \sum_{\substack{0\le j < k_a \\ 0\le i-j < k_b}} a_j \cdot b_{i-j}.$$ Apply $toZ$ to both sides. The extra assumption implies that
$$
\sum_{\substack{0\le j < k_a \\ 0\le i-j < k_b}} |toZ(a_j)| \cdot |toZ(b_{i-j})| < r/2
$$
By repeated applications of Lemma 1, we deduce that
$$
toZ(out_i) = toZ\left(\sum_{\substack{0\le j < k_a \\ 0\le i-j < k_b}} a_j \cdot b_{i-j} \right)
= \sum_{\substack{0\le j < k_a \\ 0\le i-j < k_b}} toZ(a_j) \cdot toZ(b_{i-j}).
$$
This proves the claim.

### `PrimeReduce(n, k, m, p, m_out)`
[circom-pairing](https://github.com/yi-sun/circom-pairing/blob/743d761f07254ea6407d29ba05f29886cfd14aec/circuits/bigint.circom#L786)

#### Parameters
- `n, k, m`
- `p[]` is length `k` array with `p[i]` in `[0, 2^n)` representing the positive integer $p = \sum_{i=0}^{k-1} p_i \cdot 2^{n\cdot i}$. Note: $p$ does not actually need to be prime for this template!

#### Input:

- `in` is length `k + m` array
- Say $|toZ(in_i)| < B$ for $0 \le i < k + m$. Assume that $B \cdot (1 + 2^n\cdot m) \le 2^{252} < r/2$.

#### Output:

- `out` is length `k` array
- The integer $\sum_{i=0}^k toZ(out_i) \cdot 2^{n\cdot i}$ is congruent modulo $p$ to the integer $\sum_{i=0}^{k+m-1} toZ(in_i) \cdot 2^{n\cdot i}$.

#### Proof:

For $i \ge k$, we precompute $r_i = 2^{n\cdot i} \pmod p$, where $r_i$ is an integer in $[0, p)$. Since $p = \sum_{i=0}^{k-1} p_i \cdot 2^{n\cdot i}$ and $p_i \in [0, 2^n)$, we know that $p \in [0, 2^{n\cdot k})$. Therefore $r_i \in [0, 2^{n\cdot k})$. Thus we can also decompose $r_i$ in base $2^n$ as
$$
r_i = \sum_{j=0}^{k-1} r_{ij} 2^{n\cdot j}.
$$

For $i \ge k$, we have
$$
toZ(in_i) \cdot 2^{n\cdot i} \equiv \sum_{j=0}^{k-1} toZ(in_i) \cdot r_{ij} \cdot 2^{nj} \pmod p
$$
Summing, we get
$$\begin{align}
\sum_{i=0}^{k+m-1} toZ(in_i) 2^{n\cdot i}
&\equiv \sum_{i=0}^{k-1} toZ(in_i) 2^{n\cdot i} + \sum_{i=k}^{k+m-1} \sum_{j=0}^{k-1} toZ(in_i) r_{ij} 2^{n\cdot j} \pmod p \\
&\equiv \sum_{i=0}^{k-1} \left( toZ(in_i) + \sum_{j=k}^{k+m-1} toZ(in_j) r_{ji} \right) 2^{n\cdot i} \pmod p
\end{align}$$
We define $out_i := in_i + \sum_{j=k}^{k+m-1} in_j \cdot r_{ji}$ for $i=0,\dotsc,k-1$.
Since $r_{ji} \in [0, 2^n)$, we have
$$
|toZ(in_i)| + \sum_{j=k}^{k+m-1} |toZ(in_j)| |r_{ji}| < B(1+2^n m) < r/2
$$
Thus Lemma 1 implies that
$$
toZ(out_i) = toZ(in_i) + \sum_{j=k}^{k+m-1} toZ(in_j) r_{ji}.
$$
This proves the claim.

### `CheckCarryToZero(n, m, k)`
circom-ecdsa
[circom-pairing](https://github.com/yi-sun/circom-pairing/blob/743d761f07254ea6407d29ba05f29886cfd14aec/circuits/bigint.circom#L742)

#### Parameters
- `n, m, k`
- $\epsilon$
- Assume $m -1 + \epsilon < 252$` = r.bit_length() - 2`

#### Input:
- `in` is length `k` array
- Assume that $|toZ(in_i)| < 2^{m-1}$ for $i=0,\dotsc,k-1$

#### Output:
- No output
- Constrain that $\sum_{i=0}^{k-1} toZ(in_i)\cdot 2^{i\cdot n} == 0$

#### Proof
We proceed inductively by "carrying". The condition for $\sum_{i=0}^{k-1} toZ(in_i) \cdot 2^{i \cdot n} == 0$, is equivalent to producing witnesses $c_0,\dotsc, c_k \in \mathbb Z$
such that:
- $toZ(in_0) = c_0 \cdot 2^n$
- $toZ(in_i) + c_{i-1} = c_i \cdot 2^n$ for $i=1,\dotsc,k-2$
- $toZ(in_{k-1}) + c_{k-2} == 0$

Observe that
$$
c_i \cdot 2^n \le |toZ(in_i)| + |toZ(in_{i-1})|/2^n + \dotsb < 2^{m-1}( 1 + 2^{-n} + 2^{-2n} + \dotsb) < 2^m$$.
Therefore if we range check $c_i \in [-2^{m-1-n+\epsilon}, 2^{m-1-n+\epsilon})$ for $\epsilon \ge 1$, then the above conditions are equivalent to:
- $in_0 = c_0 \cdot 2^n$
- $in_i + c_{i-1} = c_i \cdot 2^n$ for $i=1,\dotsc,k-2$
- $in_{k-1} + c_{k-2} == 0$

where we abuse notation and now consider $c_i$ as elements of $\mathbb F_r$. (We are using Lemma 1, which says $toZ(c_0) toZ(2^n) = toZ(c_0\cdot 2^n)$.)

This proves the claim.

**Aztec optimization:**
Let $a_i = toZ(in_i)$. Let $w$ denote some small window size.
Note that after multiplying both sides of $a_{i} + c_{i-1} = c_{i} \cdot 2^n$ by $2^{nw}$, it can be expanded to
$$
a_{i} \cdot 2^{n\cdot w} + a_{i-1} \cdot 2^{n\cdot (w-1)} + \dotsb + a_{i-w} + c_{i-w-1} = c_{i} \cdot 2^{n\cdot (w+1)}
$$
This is valid as long as $m - 1 + \epsilon + n w < \log_2(r) - 1$. So we should set $w = \lfloor (\log_2(r) - m - \epsilon) / n \rfloor$.

We can now proceed exactly as in the previous proof, except that we only need to range check $c_i \in [-2^{m-1-n+\epsilon}, 2^{m-1-n+\epsilon})$ every $w + 1$ steps, starting with $i = w$.