Non-native arithmetic is an important and costly operation in SNARKs. It is essential for proving validity of general cryptographic data like RSA signatures, non-native elliptic curve arithmetic like secp256r1, and general SNARK proof composition. We investigate a new approach to prove non-native integer arithmetic using Residue Number Systems and a batch proximity test for Chinese Remainder Theorem (CRT) codes, as well as surprising connections to STARK soundness.

Stage 6

I do cryptography research mostly focused on SNARKs

Liam Eagen

Non-Native Arithmetic via CRT Codes

 Coming to my talk. In writing the talk, I found that I think it probably makes sense to mostly go over what non-native arithmetic is and build up to the question. Because this is sort of an idea I've been casually thinking about for a while and I don't have like, you know, definitive answer to yet. So, yeah. Did I push the button or how does that? Is this working? The clicker? Oh, wait, it is working. Okay. Okay, so, for people who don't know, what is the context for all of this so non-native arithmetic is something that comes up in snarks which are succinct non-interactive arguments of knowledge may have heard of like zero knowledge proofs and this is the same kind of thing so in a snark, the prover, wants to convince the verifier that they know some witness. And they want to do this by generating a proof without interacting with the verifier, so non-interactively. And the proof should be small. And if it's zero knowledge, it keeps the witness secret. Yeah, and sorry for the formatting. I did the slides in Beamer and had to import them to Google Slides, so it might be a little weird. But, yeah, so the way that we usually write this is there's some C, which is like a circuit that has some public input X and some private input W, and the protocol allows the prover to convince the verifier that they know W by sending a proof. So, for example, right, you could have some, like, chain state X, which is public, some transaction W that is private, and you want to prove that you know W for a given chain state. And so not all transactions will be valid valid and so that's what C checks Yeah, so the the quarter important takeaway for this from this for our for our topic today is That C is defined typically typically, over a field. So a field is like a place where we can do arithmetic, addition, multiplication, etc. And that field will be defined modulo some prime P. The field is sometimes sort of like a free parameter, depending on the proof system. You can pick the field freely. And sometimes it's not. So if you're using like a Stark, you can sort of, in principle, use any fields, just some caveats. But for like an elliptic curve-based proof system, it's usually fixed as part of the curve, which, again, depending on the particulars, is something you probably can't control. So the question that motivates non-native arithmetic is what happens if we want to prove a statement about some arithmetic that lies in a different field than the one that we're defining our relation over. So right suppose you want to verify a signature that is defined over some other curve externally to your proof system, right? You want to verify a Bitcoin transaction or something inside of BN254. And in that case, both of your fields will be fixed and you can't, you know, change them. And they're different. So you have to simulate one field inside of the other. And yes, we need to emulate or simulate the non-native field inside of the field that our relation is defined over. So just as a simple example of why this doesn't work, right? Suppose we wanted to check that like 4 times 5 mod 7. You can check that that, I think all the arithmetic there is right. And 4 times 5 is 6 mod 7. But then if our proof system is defined mod 5, then directly carrying out the computation will yield the wrong result. So they're fundamentally different spaces for doing arithmetic. And so you need to simulate the one inside of the other. So what can we do? The situation is not hopeless. Like in principle, right, this is a solvable problem because you can simulate or you can encode any NP relation into an arithmetic circuit over any field. You know, you can encode it into binary digits and check that the digits are binary and encode the bitwise operations. And so this is just sort of like an existence proof. But this is, you know, very slow. We would prefer to do things more efficiently than this. And intuitively, you'd kind of expect it to be possible to do something better, because fields are similar, right? They wrap around, but for small values, they behave kind of like the integers. You're just adding numbers, and if you don't exceed the modulus, then maybe we can exploit that somehow. That's what we're going to try and do. So the first observation is to check modular arithmetic. We just have to check integer arithmetic, because if you want to check something mod R, this is the same thing as just checking some integer relation for a quotient. And in some cases, this is actually sort of enough by itself. So depending on the relative sizes of the fields, it might be possible to do this. Like if you check that A, B, C, and Q are all small, you can just check this relation, as written here, directly in the larger field. And the reason this works is because it will never wrap around the larger field. So if all the sizes of everything are small, or provably small, then if it's equal to 0 mod p, it has to hold mod r. You can convince yourself of this, I think. It's not that strange, right? Because if something has magnitude less than p and it holds mod p, that means it's 0 mod p. And since it has magnitude less than p, the only thing that's 0 mod p with magnitude less than p is 0. And so this works sort of like up to square root of the size of the field, basically. And that's coming from the fact that we're checking a multiplication. If you were checking a degree 3 thing, then you'd want a cube root or something like that. But what if our field's not small, or our modulus is not small? Maybe it's even bigger than the prime that we're working over. Then you can't expect your encodings of the small values in the larger fields to behave well. In fact, it might not be possible at all. If your elements are larger than the field that you're encoding your relation into, you can't even commit to a big value in a single field element. So this technique, I think originally, or at least I first heard about it from Aztec, but there's this ancient theorem, the Chinese remainder theorem, that allows us to work around this problem. And so what that says is if you want to work in a big modulus, it's sufficient to work in two smaller moduli that divide the larger one, or that multiply to give the larger one, if they're co-prime. And it's sort of like both sides of that are rings, right? So you can take a value, and instead of working mod AB, you work mod A, and you work mod B. And these two rings are isomorphic. And so people call it a residue number system, and you can represent a large number, mod AB, by representing it by encoding all of its residues mod different small primes that divide AB. Here I've written it with two, but you can sort of recursively apply this equivalence to include arbitrary numbers of co-prime divisors. And so remember we were working mod P, and we had had some R and our R might be too big. But now we can pick whatever modulus we want, right? We can pick a bunch of small primes. So it's always large enough to recover the value that we're operating over. And so long as everything kind of remains small, that Q is supposed to be a product. So long as everything remains small, this works. And like before, how we didn't want to wrap around P, here we don't want to wrap around M. But here M is a free parameter. It's not fixed by the proof system. Okay. So now like a slight digression to explain the idea. Read Solomon codes are an error correcting code scheme that is ubiquitous in in snarks if you've heard of starks or fry this is you know essential to how they work and the basic idea is we have some message that we treat as a vector of dimension K and we encode it as a polynomial as the coefficients of a polynomial and then that polynomial we evaluate at more points. So remember a polynomial of degree k, or k minus 1, is determined by k points, and by evaluating it at more points, you're adding redundant information. And so, like in the original conception of Reed-Solomon codes, this was to deal with the fact that some of the information might be corrupted. So you only need, even if some of the data is maliciously altered, you can still recover the original message. Certainly given all of the points, you can recover. So given a polynomial, and we evaluate it at some set of endpoints, this is equivalent to reducing the polynomial mod this kind of degree one ideal, X minus RI. And so this insight allows us to generalize Reed-Solomon codes to other domains, ideal domains. And for example, algebraic geometry codes, which replace polynomials and evaluations with functions of some curve and divisors can be cast in this language as well and this is also how we're going to introduce CRT codes here CRT is still Chinese remainder theorem. So the idea of a CRT code is rather than encoding our message as a polynomial, we encode it as an integer. And then, rather than evaluating the polynomial at multiple points, we take the integer, mod, a bunch of small primes. And so you can think of these mod small primes as analogous to evaluating a polynomial at a point. It's not exactly the same, right? Because the ring you get from reducing mod different primes is not the same. But the ring you get from evaluating at a point is always the same. It's not really important for our purposes. Yeah, so if you have enough primes so that the product of all the primes exceeds the bound of your original sort of space of integers that you're encoding into, then even if some of the primes are wrong, in the same way that with the Reed-Solomon code you can correct errors, with the CRT code you can also correct errors. And this encoding is the same as a residue number system. So you're taking an integer, you're reducing it mod a bunch of small primes, you're keeping the residues and you can just work with those. And for those who are familiar, there's a lot of similarities here with how, you know, Starks work and other kinds of algebraic proof type stuff. Okay, so this slide I just screenshotted because it was horribly mangled by the formatting. So the sketch of the protocol is, suppose we want to verify some non-native arithmetic. So we have some system of polynomial equations, the f in different x's, which are integers, and the f's have degree d, and all the integers are bounded. So in the original version of this, we'd be checking arithmetic mods some other prime, and you can encode that as an integer relation. And so the primes are fixed in advance, and you have some M, which is larger than the kind of maximum value achievable by F. As written, it's a little wrong because you probably want to account for the additions, but it's something like that. And then you encode your integers, model the small primes, as we described, and also provide quotients for the evaluations of these functions. I guess as written, those should all be zero, so maybe there's a slight confusion there. But yeah, so you prove your encoding of all of the integers is sort of within its appropriate range, and then you choose a random subset of the primes to test the relations over. And for simplicity, assuming the primes are all like roughly the same size, then you can calculate the success probability of a dishonest prover pretty straightforwardly. You know, it's just the probability of having like some code word, right, some set of residues that does not correspond to a small integer, or that's like wrong in some position, and then, yeah, anyway. Yeah, so it's similar to how starks work. Okay. Yeah, okay. So this is the interesting stuff. As described in the previous protocol, we're testing each encoding of X is close to a small integer directly. You're just taking your set of residues and checking that it is close to a small integer or an integer within the right bound. This used to be how fry-based proofs did things, but it turns out that there's a much more efficient batch proximity test. The proximity test here is you're testing the closeness of the set of residues to its space of correct messages. And what people do now with Starks is take a random linear combination of encoded columns or encoded integers and test that the random linear combination is close to a code word. So instead of testing each one independently, you can just take a random linear combination and test that one thing. So the question is, can we do the same thing here with CRT codes? So I think so, but it's very different, right? Because in the Reed-Solomon setting you have polynomials and you're working over a field and you're taking a random linear combination over the field here we have a set of integers and we're taking a random linear combination of these integers but there's no obvious base field in the same way that there would be for polynomials to take a random linear combination over. So instead we would pick a random integer linear combination to take of the integers. And this has a lot of interesting issues. So for example, this is not sensitive to encodings of small rational numbers. If you encode it like one half, then there's like a one in two chance that a random linear combination will cause the one half to go away. And you might think, well, we could pick primes to multiply by, but that doesn't really work. So it is in some sense fundamentally different, but I think that it's possible to do this. The question is just like how good is it and if those things can be worked around. So for example, for working mod R, this is kind of fine because small rationals are also valid sort of to reduce mod R for large R, but there's lots of details to be worked out. So, yeah, just some overview of the things I haven't talked about in this talk. So I mentioned a little bit that CRT codes, the notion of distance is a little bit subtle, especially if the primes are not all, like, the same size. They can't sometimes always be, I mean, right, like every prime is of a different size, so you have to account for that. It's not like a fundamental problem, it's just a little more complicated. As well, I mentioned this decoding to rationals rather than integers, which in some applications is fine. It might not always be fine, so I have to work that out as well. And then another thing I haven't talked about, but that could actually be worth considering in practice, is all of this generalizes from integers to number fields. And in number fields, you have a sort of different situation where the first point, you actually can have primes that are like of the same size, right? If you have some prime over rationals, integers that splits over number fields, then that might yield like a more convenient thing to work over. And in some cases, this sort of works. And then you have to ask, how do you define the size of things and so on? But just more technicalities, I think. And then one other interesting thing worth considering is, so we moved to the integers, and we were no longer able to take random linear combinations over an extension of the base field. But what happens if we work over Starks with polynomials, and instead of taking a random linear combination over the base field, we took a random linear combination of columns by random polynomials, not over an extension field. In this way, it's sort of analogous to taking an integer-linear combination of integers, and it has a lot of the same problems, but it would allow us to avoid ever working with extension fields, potentially. So I think that would be an interesting direction to explore if this work ends up making sense. And that is all I have. Thank you. All right. Thank you so much, Liam. We do have a question here. Could you repeat how you calculate which primes are small enough to use for creating a CRT encoding? So I guess there's two ways that I'm not sure what the question is referring to but For encoding into like a residue number system the primes can be any primes That you you usually choose them to be small because working mod small primes is much more efficient. This question could also be talking about the example that I gave where you can simulate arithmetic mod a square root sized number in a larger field. And that is just coming from the fact that the relation that you're calculating over can't exceed the field you're operating in. So you fix some field that you're actually working over, and then if your field that you're simulating is small enough, then everything kind of just works out, as long as everything remains smaller than the characteristic of the larger field. All right, perfect. We do have a little bit of time for questions, so let's give it another 10 seconds to see if we have any questions. What is the size of size 2 to the 128 sized space. All right, perfect. Thank you so much for the amazing talk, Liam. So we will resume at 5 for our next talk.

https://streameth-develop.ams3.digitaloceanspaces.com/transcriptions/6735cfae9dbb7a90e109be5d.vtt