ZK8: Airpods: Generalizing AIR to multivariate domains - William Borgeaud - Polygon Zero
30 Sept 2022 · 17:25
William Borgeaud of Polygon Zero presents Airpods: Generalizing AIR to Multivariate Domains, recorded at ZK Summit 8 in Berlin. Featured on the Zero Knowledge podcast, the talk extends the Algebraic Intermediate Representation used in STARK-based proving systems into multivariate polynomial domains, a technical dive aimed at researchers building scalable zero-knowledge proof systems.
Speakers
Topics
Transcript
foreign so presenting now after the break is uh William from polygon zero who will be selling us Apple's new airpods Pro oh sorry I mean uh generalizing air to multivariate domains thank you all right hi everybody I'm will I work at polygon zero and today I'm gonna talk about a project of mine called airpods which is about generalizing air to multiply domains so let's get some notations out of the way uh I'm gonna work over field F large enough for security I'll have traces which length is n upper F2 um so n is 2 to the V
I'm assuming that f as a subgroup multiplicative subgroup h of size n and here is the vanishing polynomial over H um this set 0 1 to the V I'm going to call the cube of the dimension V and at some point I'm going to use this multilinear function beta which interpolates the equality over the cube so beta X Y is one if and on if x equals y great so the Genesis of this work is r1cs so when you have r1cs instance first thing you do is you transform it into polynomials and then you have two paths either you interpolate the parameters into Universe polynomials and then you get stuff like Marlin which uses a univariate some
check argument or you can interpret them as multiplied polynomials and you get something like Spartan which uses a multivariate subject argument and so my question was can we do the same for error-like arithmetizations and by erlike I mean error so stuff like in stocks but also uh pronk and so how it goes now is we have error we transform it uh into a problem about polynomials um if we go with universal polynomials we get classic Starks and prongs but what if we want to use multivariate polynomials as far as I know like nobody has worked on that and like the question is what would fit in this picture okay so first I'm gonna before error I'm
gonna start with a simpler automatization um it's quite useless but it's a good warm-up uh we have a n by K table of field elements we have a paranormal constraint over K variables uh whose degree is quite small much smaller than n and then we ask that the constraint evaluates to zero on every row of the table so here you can already see that why it's very useless because you could just have the same row over and over again um but how would we prove these facts right so you could just give the table but that would be too large so like we want like a 16 proof that we know a table um that satisfies that um so if you choose to use univariable polynomials you interpolate the columns
as polynomials of degree less than n um you compute this composition paranormal F which is just the concentrates evaluated at all the column polynomials uh then you can prove that this polynomial vanishes on the subgroup H okay this is equivalent to just saying that the constraint average to zero on every row and this implies that um Z of H divides F and we call Q the quotient um then you commit to all the polynomials uh you send them to the verifier verifiers sends you back a challenge Z and then the verifier checks this identity and to check this identity you have to open your polynomials at Z okay that's where you use your printable
commencement scheme to open it you send everything to the verifier the verifier checks the opening proofs and this equality great so that's very similar to What's Done in Planck and stocks for example now what if we wanted to use multi-ride polynomials well this time we interpolate The Columns as multilinear polynomials we commit to them and send them to the verifier then we consider this vanishing point MLP so it looks a bit scary but really if you look into the sum all the C of F1 to FK terms are zero okay and so this polynomial is actually the zero paranormal so we actually want to prove that it's the zero polynomial to the verifier and
by a standard argument you can do that by just proving that it evaluates to zero at a random Point T okay um then that would apply that P is zero with high probability okay so you ask the verifier for a challenge T you do a some check protocol so P are as um the form is like a sum over the cube so you can do the subject protocol and then at the end of the subject protocol you have this final evaluation over Point Z and the verifier has to evaluate this expression and for that we have to open the fern animals at Z all right so we can see it's it's very similar between universe and multivariate the only difference is that in the universe case we use this quotient trick and in the motivated case we use this trick using the the beta
parallel great so now we can go um to air air is extremely similar to the previous arithmetization only difference is that now we consider Windows of two contiguous rows so now we have a constraint over 2K variable and we ask that the constraint evaluates to zero when evaluated on the ifro and the I plus 1 row okay so that's just basic error we can easily extend error for example we can ask to instead of looking at the next row we could look at the next next row all right or like the case next row um another extension could be to look up
a constant Row in the trace so like at every um row we look at the ifro and the nth row okay and these extensions can be combined right so like for Simplicity I've only considered polynomials over 2K variables but you could have like much um more complicated constraints so how do we prove air this is what's done in stocks on Planck it's extremely similar to what was done before only difference is that in the composition polynomial now we have this term F of g x so this is actually the same as taking your column shifting it by one and interpolating it okay you can prove that it's the same as doing F of G of x g times x where f is like the the column
polynomial the reason is um if you evaluate this at g to the I you get F to the F of G to the I plus 1 which is what you want like the next value of f and otherwise everything is the same until the last check where this time the last check also includes terms like f of G times Z and for that we have to open our polynomials at G times e so we open them at Z and G times Z all right and so that's yeah that's basically Starks um now what if we wanted to do that with multivariate polynomial is it that easy to
um the answer is no because here we have the term G times x which doesn't really make sense because X now is like a motivated it's like X1 to x k so multiplying by G doesn't really make sense and if you try to look into like how would you do it it turns out that I mean at least I don't know like how you would do it um by just trying to take the previous protocol and um transforming it for error okay so we need to generalize a bit um I'm going to journalize using something I call anamorphisms which is basically just functions from the set with elements to itself one example of an endomorphism is the shift which takes
um I to I Plus 1. and so if you consider any anomorphism Sigma so just a function from end to n we can have this new arithmetization that I call Sigma error where this time we have our constraint looks at the ifro and the sigma I throw okay so how does it look in practice if we set Sigma is the shift we get back a regular error right um if we want to use the cave next row that's equivalent to setting Sigma is shift to decay so shift to Decay just sends I to I plus k yeah if we want to use the nth row that's like the same thing as setting
Sigma is constant at n the function that sends everything at n and so we have tons of choices for Sigma n to the N so which choices of Sigma make sense which sorts of Sigma can you use to like actually build a real protocol um and we can actually classify them we have this theorem that says that the printing system for error can be adapted to Sigma error if and only if Sigma can be extended to a defined function this shouldn't make too much sense for now because Sigma is a discrete function so what does it mean for it to be extendable to an affine function um you can Define it in full generality but I'm only going to talk about like H and the cube over H for unified
polynomials we look at Sigma as a function from H to itself and we asked for an extension Sigma bar from the field to itself such that Sigma bar as the form ah plus b okay so just in the find function now for multivite in the military domain we consider Sigma as a map from the cube to itself and we ask for an extension Sigma bar from F to the V to F to the v such as the sigma bar is a function of the form ax plus b where a is a matrix and B is a vector okay so we get some linear algebra in the picture somehow okay now we have a sigma ultimate arithmetization we assume that the this
condition of linearity is satisfied how do we prove it in the multiplayer domain well we can just take the previous protocol and just modify it very simply in this P of T polynomial we just add the the variables F of Sigma X which now makes sense because Sigma is a map from the cube to itself and in the last step for the evaluation we open our polynomials at Z but also Sigma bar of Z okay again this makes sense because Sigma bar of Z Sigma bar takes like elements of f to the V to F to the V so everything makes sense and with this linearity condition you can actually prove that this proving system works
good so that's all very abstract so like what kind of sigmas can you actually choose in practice so in the unified case um you can actually prove that the only Sigma that work are the shift to Decay and the constant at k okay so it turns out that the extensions are of error I mentioned before actually the only extensions you can do yeah it's just like looking up the cave next row or looking up a constant row you cannot do anything else if you want to keep the same um base proving system and if you count how many sigmas you you how many sigmas that that amounts to uh there's like 2N and N of which are bijective
uh what about the Multiverse case you can also like classify them in full generality but like here an example is much simpler um here is like an example of a matrix a and Vector B that works um and what they do is you do ax plus b it just you just do a permutation of the coordinates you bit shift some of them and then some of them you can also set to constant if you want okay and that's actually like all that you can do like uh all the sigmas that you can do is like basically that just permitting the coordinates and bit shifting some of them and if you want like set some of them to constants and if you count how many uh sigmas you you get by doing that
um you get like these Expressions um and then you can see if you compute how many that is that it's quite larger than what we got uh in the universe case so in some sense by going to the Multiverse domain you get like more degrees of freedom in your arithmetization cool um right so like how does it look in practice um so you've chosen your Sigma you want to do like error on Military domains um and then you get something that I call airpods you have your original table and by your end bike table and your Sigma you don't really know what Sigma does but like you can actually split your table into a bunch of smaller
subtables on which Sigma acts as a shift okay so all these tables will be you will get back actually um original error so like in the original error you just have Sigma is the shift so that by using this new Sigma you just get like a bunch of smaller errors um so that's a bad news in some sense because um if you want to do like a large sequential computation um you won't be able to do that because the largest table size will be like much smaller but you can actually do use that to do like in some sense errors in parallel okay so you just have a bunch of Errors of tables in parallel that you can just
prove into like one uh protocol using multiplied paranormals great um so um to conclude um to the best of mileage it's like the first erlike argumentization uh that works with material domains um I've only focused on like H and the cube today but like this can be generalized to domains in between uh there's some compromise there but like it could be like faster uh all of these can be generalized to um ultimatizations like Planck okay so Planck is basically just error with a permutation argument so like you can see it's a very you can very easily extend everything to Planck uh none of this requires fft okay so you can work over any field
including fields that don't have a high to audacity um and I don't have an implementation yet but I'm working on this um all right that's right for today um I'll take any questions no thank you William are there any questions from the audience so hello thank you for the presentation as you were talking I was wondering what the utility of this is and you earlier mentioned something about parallelization so what do we get out of something like this
so so I guess it's like this work is like much more of an exploration of what we can do with error right so like error and Planck is like three years old now um and it works with Universe paranormals but like what if you really want to use multiplied paranormals what if you want to take advantage of the fact that you can work over any Fields right so I don't know like how it could be used yet but like let's say you want to you there's like a new paranormal commitment scheme over military polynomials that comes out and that's like much faster that what's currently available then you could use this new itemization in your protocol right okay there
I guess I'll do it have you considered using a higher individual degree and exploring trade-offs in number of variables and the degree of the multivariable polynomial can you repeat that please yeah so you use a polynomial multivariate polynomials of degree one multilinear polynomials have you considered using a bigger degree and reducing the number of variables yeah yeah so like that's the this second Point here so like yeah you could actually generalize this to work in between like kind of like compromise between the degree of the paranormals and the number of variables yeah that's totally doable and you get you get like the same kind of uh linearity constraints
thanks are there any last questions I certainly have one if there are no more okay actually I do have a question what's the intuition behind uh only the specific endomorphisms that you allowed like why is that the case why can't you generalize to more functions yeah so the thing you need is that F of Sigma X so like if f is a degree n paranormal or like less than n you want F of Sigma X to still be degree n all right and like so like if you if you have Sigma is x squared that won't work so like you need like something like linear or a fine to keep the degree lesson and got it so it needs to be
degree conserving which is exactly why yeah found it yeah exactly cool thank you any last burning questions if not then I guess we'll continue on to our next speaker