This note aims to detail our thoughts on a particular short post from researchers at Aztec, the team behind the original PLONK zk-SNARKs. Due to the original post's short form, some of the details are not altogether clear to us. It requires some leaps of logic or creativity in certain parts. Therefore, the explainations in this note might be a bit misleading in parts and should be taken with a grain of salt.Nevertheless, we will take the burden of possibility of being mistaken and write out what we understood from the original post.
Further, the methods in these notes (or methods similar to them) are implemented in the following repository, https://github.com/privacy-scaling-explorations/halo2wrong, to create efficient circuits for ECDSA verification algorithm which uses large fields.
In some circuits such as DSA, we are frequently interested in representing modulo arithmetic over a large prime field, equations of the sort where is a large prime. Typically, a witness is produced and the integer constraint is included as part of the polynomial commitment. Using non-native arithmetic discussed in this note, we can replace these types of constraints with (multiple) constraints over smaller numbers. Therefore, our goal in this note is to emulate certain expensive constraints in a different way.
Let us consider the setting and the naive approach. We are given a prime number . We are interested in building a circuit for . The input variables must be in the range . Otherwise, we would simply use the equivalent modulo statement with smaller numbers .
We are interested in finding a non-negative integer s.t. and is the smallest such number, which means is in the range as well. Given a candidate for , we wish to build a constraint that ensures matches . This would require us to introduce an advice variable (to show the existence of) that satisfies , which is a unique positive number. Since and the least value can take is , . This would imply is in the same range . Therefore, all the relevant variables aside from itself are in the same range, .
If we are willing to deal with values in the range in our circuit constraints, we can simply ensure that . However, this may not be desirable if is a large prime in the order of for example. In the rest of this note, we build the same constraint in a different way, circumventing the computation of or for a given .
We begin by considering a method to ensure for a prime without computing or . Since the above equality implies , we can write it with new variables s.t. etc. respectively. In order to accomplish this, we consider a new set of constraints with advice variables ,
Based on , we can simply re-write the additional overall constraint as or in an integer constraint form as,
Note that itself does not need to be , unlike . These are all integer constraints over numbers smaller than besides . appear in constraints in Eq. 1-5 on their own without any multiplications with other numbers. Therefore, these constraint could be computed efficiently with small numbers.
For a given that follows constraints in Eq. 1-6, it is guaranteed that . However, is not guaranteed. In order to satisfy , we will need the additional constraints we introduce in the next section.
In the following, or more concretely . It is easy to see that .
Assume is a given integer that is a multiple of . We will write integers such as in binary notation as a concatenation of multiple bit subsections, sometimes called limbs, as follows.
Consider limbs of size . Then an integer could be written as limbs, , each of which is a number that can be represented as a sequence of bits, with . Given , we can write the following equation for ,
Note that we do not have terms that involve in these equations, even though they would appear in . The reason for this is simple: the term that involves would be and since , this number is divisible by and is zero modulo . The same is true for any and with .
This leaves us different terms for (and terms for ) that are grouped together by the index sum in each line of Eq. 7-10 respectively. Once we group them in this way, we can factor out in each line, according to the position of the limbs of the original numbers involved in the multiplications. Based on this grouping, we can create intermediate variables ,
which can take values in the following ranges:
If the number of elements in each sum is represented by , the formula for the range for each sum can be given as . The exponent for the bound above will be explained through .
As we can see, it consists of a summation of terms where each element is the multiplication of two numbers in the range . When we multiply two such numbers, we end up with a number in the range . in comes from the fact that there might be an additional carry bit after the multiplication. Further, when we add such numbers, we end up with a number in the range . This range can be (minimally) expanded above to a bit friendly range that encompasses .
Let . Note that itself does not need to be less than . Its calculation only throws away some parts of that do not contribute to the modulo result but not all. Therefore, if with , it is not guaranteed that . However, the last bits of are certainly going to equal (the reason a power of two such as is convenient).
Further, if we consider the -bit limb decomposition, , is the last bits of , i.e. for some non-negative integer . Similarly, is the last bits of with . We can write the all the limbs of in a similar fashion:
Removing the intermediate variables , we get
In this section, we have demonstrated a sets of integer constraints in Eq. 11-14 that can be used to ensure , which also ensures . Note that we accomplish this without ever computing or but by working directly with their -bit limbs in the constraints.
To summarize, for a given that satisfies the constraints in Eq. 11-14, along with constraints that ensures ,
it is guaranteed that (but not on their own).
We finally note that constraints from the previous section in Eq. 1-6 can be written in the -bit limb form as well, to match the constraints in this section.
A different version from the original post: The above is our version of how we would do this constraint decomposition.
A different version of this that combines a pair of limbs and into the constraints is given below (the original formulation in the blog post that this note is based on).
In the image below, we demostrate this idea.
It is hard to tell what we gain from this particular formulation, which was given in the original post instead of our formulation above. There are constraints in each case and in the latter, there are multiplications with which makes the numbers such as and quite a bit larger. We believe our formutation should be more efficient but it is difficult to be certain.
We have shown constraints that allow us to restrict such that
and . However, these do not guarantee that without the modulo as is valid when is and a multiple of . Similarly, and is a multiple of is allowed (this is a distinct possibility since ). Therefore, individually, these constraints do not ensure .
However, since and are coprimes ( is a prime ), i.e. , we can invoke the constant-case CRT, which states,
Therefore, satisfying these constraints jointly means that is also satisfied. Does this guarantee that ? Not necessarily, as it could be that and is a multiple of . However, if we chose large enough s.t. this is not possible, then satisfying these constraints jointly will mean that .
In order to accomplish this, we need to enforce by choosing s.t. , as we already know the allowed ranges of variables, . We know that . Therefore, it must be true that . Therefore, must be large enough to satisfy but at the same time, it needs to be small enough that is sufficiently small to justify the multitude of constraints that involve numbers in the range .