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
Aka BigMultShortLongUnequal in circom-pairing

Multiplication of two polynomials in one variable X.

Inputs:

• a[] is array of length ka as 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

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

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\).