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\)
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).
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()
BigMultNoCarry(n, ka, kb, m_out) [Signed Version]circom-ecdsa
Aka BigMultShortLongUnequal in circom-pairing
Multiplication of two polynomials in one variable X.
a[] is array of length ka as signed overflow representationb[] is array of length kbout[] is array of length ka + kb - 1out[] is uniquely defined by the polynomial identityn is passed for convenience but not actually used!ka, kbm_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}.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)n, k, mp[] 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!in is length k + m arrayout is length k arrayFor \(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
n, m, k = r.bit_length() - 2in is length k arrayWe 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:
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:
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\).
-
Any changes
Be notified of any changes
-
Mention me
Be notified of mention me
-
Unsubscribe
Subscribe