# On proving of pairings - Andrija Novakovic | Geometry Research

- Channel: [ETH Belgrade Community](https://streameth.org/eth-belgrade-community)
- Date: 2024-10-07
- Duration: 29:38
- Topics: People & Blogs
- Watch: https://streameth.org/watch/yt-Ku1GIZl2NyU
- YouTube: https://www.youtube.com/watch?v=Ku1GIZl2NyU

## Transcript

yeah [Applause] so if you didn't like the mat from Aria's presentation I think there will be even more mat but you like you cannot leave now so yeah um this is a recent paper I was working with leam Megan from uh alpen labs and um zeta function Technologies and we were uh working on uh how to prove pairings inside the snar so um I don't know how many of you heard about pairings but uh we'll talk briefly about it uh it's a very nice mathematical construction used everywhere today and um mainly you will see that uh as we have more uh l2s more bridges more rollups uh which are mainly using elliptic curve based narks which are also pairing based uh for the verifier efficiency uh it's very common to have uh at least one layer recursion where you have to prove that you varified some specific snark and when this snark is a pairing based snark what you have to do is to actually prove that you verified pairings inside snark uh if you have more deep recursion like um some IVC scheme or PCD there are techniques to postpone pairing verification until decider but we are not going to talk about that we are uh mainly interested in how to do this like one layer recursion where you actually have to prove pairing inside the the snark um yeah so um when working with circuit uh and when proving some computation it's very common not to carry the full computation inside the circuit and whoever worked with circuits or ZK uh to mainly uh maybe the most common examples are uh inverse computation and square root computation so these operations are not cheap to compute uh also not in field and instead of computing instead of proving the trace for their computation what prover can do uh the prover simply hints uh what is claimed inverse and what is claimed uh square root and then instead of as I said Computing uh it just proves that it is indeed an inverse in the field or that it is indeed a square root so this is like more fundamental uh it's kind of always easier to verify something than to solve some hard problem uh it's much easier to just check if some graph is three colorable then uh for the specific instance if that's correct three coloring then uh then uh solving if the graph is three color colorable at all so yeah there is like a more more fundamental relations how we can uh verify computation instead of prove uh that we carried some algorithm and that is mainly one of the basics basic ideas of our work so um before we go into matth details so pairings are these extremely beautiful constructions which are bilinear maps on elliptic curves uh there are many variations of them uh based on which curve you're using what do you need but in cryptography we are mainly using something called asymmetric pairings where we have these two distinct groups of points and the E what we call pairing is an operation that sends these points from these groups into something we call Target group so um nice property which allows us to do very fun cryptography is that this bilinearity so if you have uh let's say p and Q are generators of these two groups and if you have a and b uh the pairing of P Q raised to the ab is same as this and you can also shift b and a and a lot of other stuff but yeah uh for the sake of Simplicity this is kind of the relation that holds so why this is powerful tool for cryptography but like in others uh fields of math so elliptic curves uh are groups and you can add points on the elliptic curves and you can multiply them with the scaler but what you cannot do is you cannot multiply points on the elliptic RS and pairings are this like magical construction that allow you to multiply two points once so it destroys this group structure so when you multiply two points with pairing what you end up with is not an elliptic curve point so that's why I said you can multiply just once you cannot go back but you can multiply just once and get something in this target Group which I'm not going to go into what it is but actually it's the by the practice we we saw that it's like very powerful tool to build like a lot of fun and Powerful cryptography so maybe the most common uh pairing based algorithms that you can find uh today on blockchains and in in snarks in general are these three uh I use different notation for all of them but this is kind of notation that you will uh find in the different papers which are based on different schemes so uh it all started with BLS signatures um you have these very nice signatures where uh you can write like have uh elliptic digital signature based on pairing where everybody can check that um if you actually have a signature then pairing of signature and generator on uh G2 group will be equal to pairing of hashed message to the G1 point and the public key and then you have more complex relations how you check kcg polinomial commitment scheme which is essentially checking that some polinomial are equal in some secret Point um that nobody knows that's like a committed pointing the elliptic curve and Gro 16 has has even more complex pairing uh verification thing uh yeah it was good good stuff right I uh so yeah the the gr 16 has even even more complex equation to verify the pairings uh but essentially what is like shared between all of these is that when you're actually verifying stuff with pairings in snarks it boils down to to verifying that some product of pairings are equal so all these essential algorithms will actually check that some pairing or like some product of pairing is equal to some other product of pairing you can have like a algorithms as some generalized inner product uh pairings where uh you can have some generalized inner product arguments where uh you're not checking equ quality of pairings but in the like Broadway of concept all the snarks in the end will check that some products of pairings are equal so um the pairings as uh construction are like very structured uh very uh algorithmical and we were able to use this structure in order to show that when you're actually trying to verify or to prove that you have a product of pairings that are equal you can remove the very the most expensive part of the computation of pairings so there are two types of pairings mainly that you use uh uh in cryptography or there are more but like on a on a curves that are defined or Fields you have two types of pairings uh Veil and Tate and today everybody use uh uses State pairing because of efficiency and then you have something even more efficient which is just eight pairing that's why we have this T in bracket so uh these algorithms now we call just like Optimal pairings and um it's like always eight pairings okay so at high level uh how the computation of pairing uh is uh carried uh so this is far from the state-ofthe-art but just from the conceptual overview so as I said you have two points one from one group one from the other group and something the output of this algorithm is something that I said in the Target Group which uh I don't want to Define that but you have to define something called embedding degree of the curve and to compute some field extensions and then uh the that field extension is what we call Target group so we are outputting some number in this target group what actually happens is if your pairings are equal in this extension field Target group your result will be equal to one so just imagine it's like multiplicative inverse one and don't care what the target group exactly is then you have some parameter of curve um you can compute it on many times uh on many different ways I'll I'll show what's the most optimal later and then uh your you you have this part part that is called Miller Loop which yeah is Loop uh that depends on this parameter U here so we literally go through each bit representation of this parameter and we do some work at each step so we have to square this accumulator and then we have to evaluate some lines over elliptic Curves in this G1 point so in general this is how you compute uh devisers of elliptic curves uh and this is the only practically computationally practical algorithm that was um designed by Victor Miller that's why it's called Miller Loop and uh it really looks like some double and add or Square and multiply algorithm so you square at each point uh at each step and double and then if you have something that is not zero bit you update your accumulators you can have different representations than binary of this U to like obtain the the smaller Hamming weight because you see that the number of operations in this Loop will also um like depend on how many nonzero bits you have so uh for the sake of Simplicity we're looking just in a uh in a binary representation but there are more representations and when you do all of this um you do the this very expensive operation that is called final exponentiation and uh it's raising this uh um accumulator that we were carrying across the loop to this number um I'll I'll show why we raiseed to this just in a second but uh just in your head imagine that these are all like 25 uh 100 bit numbers and the this K in the most uh pairing friendly curve is 12 so this thing here is like a huge number so this exponentiation is not cheap like luckily why pairing cryptography is practical today is that there are a lot of Works who really optimized the exponentiation of this with different structures but still it's like a very expensive computation and what we achieved to do is we showed we proved that like if you want to prove that some products of pairings are equal which we saw is the the most common thing that you do in modern snars you actually can almost fully remove this most expensive operation right so when we work with State pairings or eight um the main uh trick or the main point is that the outputs of this uh thing that we called Miller Loop are not unique so the outputs that you get from Computing the Miller Loop are in this um equivalence class so I'm I'm I'm just going to show an example how it looks instead of dividing it so uh with slight abuse of notation I'll use here pairing instead of product of Miller Loops so uh when you compute the Tate pairing um what you get is if these two pairings were equal the result of them in this target group is not actually going to be equal so you can see that they're equal up to some art root of unity and now I'm not going to go into that but imagine that the result in this equivalence class is uh like described with two elements one element we can call Omega is something that is Art root of unity and something else uh that is Art residue so all pairing outputs are going to be in the form some power of art root of unity times some art residue so if these two pairings were equal you will obtain these results and now they will be equal only here but not on this CET here which as you can see they have different C here right but if you uh divide this two numbers these omegas will cancel and you will end up with something power to the R so if you then uh take that whatever that is power to Dr and you raise it to this number by little fat theem it will go to one right so this is why we need to do this final exponentiation so final exponentiation is this um operation that actually makes the result of your pairing unique okay so if you actually want to check that two pairings are equal they're not you have to do the full final exponentiation and then you can check if they're equal okay so um here uh from this you would say uh okay you can do full Final exponentiation on this and this and then check results but there are also today like the the state-ofthe-art is doing something smarter and we're just briefly going to look what uh the state-of-the-art computation of pairing looks how it looks today so first of all you have something called multimill Loop so without uh any loss of generality let's say that we have now two pairs of points that we can compute but this can generalize to arbitrary amount of uh of the pairs that you want to compute the pairing of and then their product so what you can actually do you run this one Loop and now I'm not going to go into details of this but you can see that by accumulating everything into this single F instead of running two computation separately you actually compute this squaring only once so the main point is that you actually compute a squaring per step uh and it does not depend on how many pairs of these points do you have to compute so you still have to evaluate these lines and compute this algorithm uh this um double and add points on the elliptic curves but these squarings that you have to compute in this target group are also not so cheap so by accumulating all pairs and then running one squaring you actually save a lot of computation and then when you have this accumulator at the end you just raise that accumulator so so instead of here Computing this pairing and then this pairing and then raising this and raising this you end up with doing just one final exponentiation in the end okay so that's kind of uh the mental overview of how state of the artworks you have like more structure uh evaluation of lines on the elliptic curve um or sparse elements so you can employ even more caching and multiplying sparse elements before multiplying them with the the full elements but yeah it's just like um far from uh what the point of this talk is so if you have any specific questions later you can ask me um okay so this is like the model of computation that you have to do in order to prove that two pairings are equal and if you want to prove that two pairings are equal you have to actually compute all of this in your circuit and this whole final exponentiation and assert that result of that is equal one right okay so the main uh like uh selling point of our paper is that you can prove that products of pairings are equal without final exponentiation so instead of doing this final exponentiation and checking that result is one you can actually prove some knowledge of C in the Target group and prove that the pro that the multimer loop the product that you compute is actually equal to this resid you see right so if you actually um compare it to this slide here when we looked into some of these you can see that we employed the similar technique where we say Okay instead of carrying some computation uh inside the circuit what we can do is we can allow Prov to send a hint and hint in our case is this art residue that the the prover can provide um and then we will instead of carrying the full final exponentiation we will actually doing this C to the r thing um instead of this whole number Q to the K minus one/ r so this is the basic like idea of how this thing will work but um luckily the final exponentiation is like extremely optimized there is so many structure per curve that you can use so replacing the final exponentiation by this exponentiation by R is actually it's not giving some huge gain in the amount of operations that you have to compute so you can prove or like you can see the proofs in our paper that this is still complete and sound meaning that if the product of your pairings is equal one you can always find this residue and if it's not one this residue cannot exist so it's fine but in like uh amount of operations you have to do you will not gain anything any substantial performance okay so there are more techniques and more like um uh like optimizations that when you actually employ you get a significant performance so uh I'll just briefly go through them because uh they are a bit harder to catch from presentation if you're already not familiar with this so so um one very uh common uh thing to do in number theory is that when you have your field which is like uh fq or like where Q is some prime raising stuff to the Q is called fenus map and it's like extremely uh efficient so uh by little FMA uh in the nor like in non-extended field this is just like identity so if you have extension field it's a bit harder to compute it but uh it's still very cheap if you choose correct basis which is called normal basis raising a number to the Q can be obtained by just doing like cyclic shift of your uh of your polinomial then um you have a trick that is like uh obtained from uh generalizing uh Leander symbols of multiplying two non-residues to obtain some residue and uh as the final optimization this computation of raising C to the sun power can similarly how in the multimill loop you can accumulate all pairings to save the the squarings you can we will show that you can also uh embed this the powering of the C and also uh save all squarings on that so um yeah uh like uh what you can say that we did is that we replaced full final exponentiation with just m fqk where fqk is like our Target Field multiplications and M is the humming weight of uh parameter that is called Eight Loop count and that is parameter U that I that I called in our algorithm so uh it's quite significant and just I'll just briefly show how some of these things are working so you have something very famous theorem uh called Hass theorem that gives you like how many points you will have on elliptic curve based on the prime you choose and uh you know that like the difference of the or order and the field that you're using is B bounded by like s squ of Q so you can actually compute r as Q + 1 minus t where t is this number which is which absolute value is less than this so because exponentiation by Q is always cheap you will end up with actually Computing R in the complexity of this T which is s squ TQ which is around two times better you can actually do better and this is what um optimal eight pairing paper did and and conjecture and it was later proved that the the general technique is that that you want to write your exponent as a uh some linear combination of Q Powers because raising to the Q or any Q Power is essentially very cheap and you're trying to solve the short Vector in some ltis where you minimize these vectors with this coefficients AI so we're not going to go into how you do that but uh for example the BN uh family of Curves and the BN 254 like curve that is used every where in ethereum uh like pairing uh friendly curve for snarks uh is parameterized with this polinomial so just looking that raising something to the r will have to raise to this polinomial or as we say like count that Q is like for free this is T so you actually raise uh in something that depends on the just 6X squ instead of the huge polinomial here so I think you can see that it's much better and when you solve this lce the optimal one of the optimal uh shortest vectors that you can obtain from this ltis is this one so you can actually write some Lambda as we said linear combination of Q powers and this vector and you can see that the most dominant Vector here is the parameter of curve X right so you will actually have to carry the exponentiation just by X so we went from exponentiation of this big polinomial to just something that depends on X so I think it's it's uh very nice um the big problem we had is that actually your R is not equal to this but your R divides this and then it makes a slight mess in the computation you have to do so we had to prove some even more stuff um and and that is ideally you would like the product of your Miller Loop to be equal to C to the Lambda but it's not the case so if you look into some uh well defined integers I'm not going to go into that uh you can see that the product of Miller Loop will always be uh Lambda to the D residue but it does not mean that it's always full Lambda residue so you have to do even more tricks and to find yet another non-residue to scale this to get something that is residue and what we also prove that is if you have your pairing friendly curve whatever you choose you will always be able to find such a non-residue to scale and obtain a residue and it will stay sound and complete so if your product of pairings um were uh not one having this non-residue cannot make something to be Lambda residue so it's very important uh in the case case for the most common b254 curve uh this D is very small it's just three and you can show that any 27 root of unity or its Square will satisfy this number a and then when you take all of this together and do the uh the final the most optimal algorithm you can see that your uh like final accumulator here like that your accumulator here can actually instead of one start with C inverse and then what you're going to do at each step when you do these squarings you're actually embedding the squaring of this thing here and when you finish everything you will end up with having C to the minus Lambda and then you can actually just check that this goes to one and uh as a final note as I said the instead of doing full final exponentiation you will have to do number of Target group multiplications that depend on the uh hemming weight of your parameter U that is called Eight Loop count and you can see it coming up here so whenever you have nonzero bit you have to do some more multiplication um right yeah I'm I'm done so there are more tricks that you can do with these lines uh so some of them were already known but um uh you can also remove a lot of twist arithmetics when you have the fixed point of the parent so uh it also gives a lot and yeah as finally uh some people already did implementation of that of it uh ethereum Foundation implemented this new technique in their Halo 2 approver for BN pairing and they got around 2x speed up garaga team from starware they uh gained like four to five x speed up depending on which case they were using and yeah there are even more things that you can do with this something which is called like randomized polinomial arithmetic which I'm not going to go into um and if you use some smart cycles of Curves and another very nice application that Liam now is doing with alen lobs is there actually building the first uh snark verifier on bitcoin which we finally hope can be actually practical um so uh I'm very interested to see how that will look look like in a couple of months uh yeah that was my talk [Applause]