zkStudyClub - FRI-Binius: Polylogarithmic Proofs for Multilinears over Binary Towers (Ben Diamond)

Transcript

yeah hi everybody thanks for joining uh yeah as Alex put it I'm very excited to be here for my first zik stud club and even happier to introduce to introduce like a a repeat guest a repeat host I guess for this zik S Club Ben Diamond so yeah who's going to talk to us about poly logarithmic proofs of a binary Tower Fields also known as FR benis so yeah previously reducible team uh Jim poen will be in the background maybe jump in for a few question at the end but yeah uh up to you Ben and uh enjoy great well thanks for having me and um don't need to say much more after that intro I'm excited to present about

fenus uh polyic polylogarithmic proofs over binary Tower field and um as Gaylord said Jim Posen my co-author is here and uh will be happy to join in with me during the Q&A phase so um with that I think we can start so um okay so just a look at what's to come um I I'll say a few things about what um I'm going to present about um working okay here we go so um there will be a pretty substantial background section the reason is that in order to explain fineus we need to tie together an number of various threads

which come from different places okay so the first of those is BAS um we will say a short background on that um and also on Fry and specifically binary field fry so this is a variant of fry which might be less familiar to many in the audience so we'll say a few things about that um also the additive NT so this is a an important work due to Lin Chong han4 that we will need to make use of and um finally the Bas fold multilinear PCS so this is uh one of a number of ideas in in the base fold paper that we are going to be able to adapt to make uh fry Bas

happen so th those are all disparate background threads um uh and once we get those down the question will be what goes wrong when we try to sort of mash them together and answering that question will be the bulk of our sort of new content the first thing we'll talk about is a special variant of binary fry or or sort of specialization of it which makes it compatible with the additive NTT so this is bringing together two of these threads in a kind of new and surprising way um we'll also need to talk about packing which is an idea that uh comes from Bas but which we will need to make work in our setting in order to

get um you know really uh short commitments and uh no no sort of embedding overhead so and then finally we'll talk about the results what comes out of it and uh the proof sizes so that's a a rough summary of of the structure of the talk and with that I think we can jump into it uh so the first background item is BAS so Bas broadly is a new approach to design um which works natively on binary data okay so most snarks out there today in fact essentially all of them pre um pre binias um use use prime Fields either huge Prime Fields say 26 bits or

something mediumsized like 64 32 and um what that means in practice is that your witness data which is probably natively binary or or some power of two bitwidth um almost no natural witness data sort of comes in from Prime Fields right you need to take the witness data you start with and encode it somehow into Prime field elements um this involves a kind of uh a kind of non-native arithmetic right taking something that started binary and expressing it into Prime field elements likewise the constraints that you write down that should hold over your witness

data those you also need to express as circuits over over the same Prime field this is sort of not natural uh the prime uh register size is not going to naturally match up with your witness size um so what this means often in practice is that if you take witness uh data which starts as bits let say you'll need to either embed these into Prime field elements and Pad them up to say 32 bits or 31 bits um and also deal with range issues right so if I um if I have a wire which should be zero or one valued I I then need to make sure that

it actually is so this adds extra uh complexity at the constraint level um in Bas we get we get to deal with binary data types natively going down to the level of bits so the witnesses can be um uh essentially strings of bits or or multilinear over F2 um or other power of two bit widths like8 bits or or 32 um and um and and the constraints we write down are also defined over these fields okay so how do we do it um I I'll say more in a second but very roughly we use a new instantiation of binary Fields

built as uh Towers right so this means we take a sequence of degree 2 uh field extensions and in this way we can build up any binary field of power of two order over F2 um each resulting field element is sort of made up of two uh elements from the next field down and this makeup is is uh recursive and can be subdivided sort of arbitrarily uh we focus on multi-linear polinomial WE introduce a multilinear PCS for um polinomial over binary Tower Fields uh we use a number of techniques at the piop level uh including uh crucially some and many other ideas that come from

hyperplan um as well as other works like quarks and lasso and so on we have some new ideas at the piop level this includes what we call shifting so this is something like circularly rotating a column um by some arbitrary number of steps and also packing which is a tower specific idea essentially entails redrawing the boundaries of your uh symbols instead of bits let's say into um larger field elements the menant of of these techniques are that we get a very fast prover um not just on the CPU but even more so in digital logic so think fpga um or or even

as6 uh conceivably and um moreover we we also reduced the sort of bandwidth problem right so think about the size of the expanded witness or trace this is something we need to ship off to the device to the fpga from the host um the smaller we can make this the less of a bandwidth problem we have and in fact even getting the data there actually is a bottleneck for us so this is equally important if not even more um and then finally uh we the the the functions that we naturally care about like ketak let's say we can arith matize those in in a

very natural native way in in our binary uh field-based arithmetization scheme okay so looking at these three interestingly really these are things which a priori you could get one and and not the others it it's it's pretty nice that it by um adopting the Bas techniques we're really able to get all three at the same time which is um a really nice bonus okay so what what's the drawback uh it sounds pretty great um the really remaining obstacle is that Bas has relatively large proofs both ASM totically and concretely these grow like the square root of the witness size uh

now what we really want is something polylogarithmic okay so this is essentially the um not just nominally but really in spirit is what it means for a verifier to be really succinct uh and sure enough the state-of-the-art systems out there right so think planky 3 and so on these all use fry and do manage to get polylog size proofs so why could we do it well very um roughly um the the the techniques that are used by these state of the art systems like planky 3 do not work in a natural way in the binary field setting why not really there there are arguably

two different reasons first is that deep Ali which um you know prebias was essentially a de facto standard in in production oriented snarks requires that your ground field have a large um multiplicative subgroup of power of two order so this is only going to happen if you have a relatively large Prime field um sort of to Ain your witness um you know Circle Stark is actually a bit of an exception to this but you do still need a mediumsized Prime on the order of of the trace length uh there's a further reason which is that these protocols which are univariate rely on a quotienting idea for for this sort of

Vanishing argument um right so to show that some polinomial vanishes identically on some subset of your field you can divide it by the polinomial that vanishes is um everywhere on that subset uh this is not compatible with packing so it just is a non-starter for the Bas type approach what did we do so because of these constraints we we opted to use a a breakdown sort of style of proof um the thing with breakdown is it doesn't involve division it very roughly it it does only linear and multiplicative things does error correcting and coding uh linear

combinations um it it can use extension fields which which we did in bineas of course um but not division so because of this we were able to pack andinus um while it sort of in in an information preserving way uh that that made it work okay so the the final thing I'll say on on the Bas front is is just a visual roughly of how it works and and this is a an absurdly fast summary of of what Bas does but very roughly if my if I start with a witness which looks like a long uh list of elements of F2 let's say Okay um I'm going to arrange these into a square Matrix now if I were to apply

breakdown now uh I would I would encode each uh each row using some error correcting code with huge huge alphabet so each of these symbols each of these bits would then get blown up by you know 256 fold when I when I I encode these rows even if I were a bit more clever and used a readed Solomon code let's say of of minimal alphabet size I would still be getting let's say a 16-fold blowup um in in each symbol in addition to the to the um to the blowup that comes from the rate okay so what Bas does is is it sort of packs uh this thing rowwise so it it marches to the right in each row and bundles each chunk

of adjacent uh 16 16 bits F into a single symbol what you get is a matrix of the same height but uh one 1/6th is wide whose entries are now coming from F2 to the 16 and very roughly this is an oversimplification but essentially you can imply breakdown now uh it's it's not quite so simple because if you truly forgot about this unpacked Matrix then you would lose information but roughly that's the spirit of of what we want to do okay so that is enough on on Bas um we we will come back to these ideas but for now I want to Pivot to to fry and just get some background on the page

okay so specifically I I'm going to describe fry in a way that might be unfamiliar to to many people um specifically you know most people when they think of fry they think of prime field fry now the original fry paper actually described it in in a binary field case um and it it doesn't really look the same when you write down how it works although sure enough it does Recapture The Familiar Prime field case as a special case but I want to describe it in the general way so uh with that said here we go um fry Works uh first of all with with some domain in in your field and in the prime field case this these s's are going to be multiplicative

subgroups but let's let's forget about that for now okay so s is a domain subset of K it's going to be of some power of two order okay so L is is a problem size and then R is a rate parameter we have a map q0 q0 is a 2:1 map its image is some new domain S1 of half the size okay um and we keep doing this a log number of times until we get to SL which is of just size 2 to the r okay so this is kind of the backdrop of what fry does now when you actually run fry what you run on is is a function F0 on s0 okay so this is a a word in in some read Solomon code a claimed uh code

word of block length um 2 to the L it's defined on s0 uh what you do is you send this initial thing as an oracle to the verifier the verifier samples some random Challenge and then we do something which I'll call fry fry folding which depends on F0 and on r0o by by doing some some sort of magic process on those things we get some new word F1 um of half the block length so a new claimed code word of of block length half as much and we send that as an oracle we get some new challenge R1 we

fold F1 we keep doing this um log number of times until we get to the final claimed code word L which uh actually should be identically constant if the prover is honest and the prover just sends this constant explicitly to the verifier finally there's a query phase where the verifier will start um retrieving sort of random entries from these uh oracles and and running some checks and then we'll either accept or reject okay so the major thing that I have not yet specified is is how fry folding actually works now again I'm going to describe it in a way which is friendly for binary Fields

so this might be a bit unfamiliar but so here's our picture we have SI we have Fi Fi again is just a map on on on SI so it Associates to each element X here some value fi of X and finally we have um our next domain si+ one in the folding map Qi uh and really our goal is to Define uh this new map this new um word fi +1 which should be uh a function on SI so my main question is what should I write down in in this box here um well I I'm going to tell you how to do it by zeroing in on a particular element y of Si + one and describing

what why should map to okay so if I tell you how to do this then then we're done because you can just apply this independently for each element Y in si +1 okay so what I do is a bit weird I'm going to pull back y I'm gonna find the two x's in si that map to Y under this Qi folding map okay I'm going to I'm going to get the values at these two x's so what is the value of fi at these two points finally I'm going to take r i this is the verifiers challenge it's sort of out of domain it's not in si it's um somewhere off off here in in the field uh I'm going to treat uh these two values as if they were the restrictions

of a line so if there were a line that took this value on F on x0 and this value on X1 what what value would that line take at r i and it turns out that that's exactly what um what y should map two okay so a bit of a complicated and ad hoc procedure but if I if I repeat that for every element in si +1 then sure enough I'll get something down here some um some uh word fi +1 and um the key question that remains is that if uh if the prover is honest then fi will be the encoding of some polinomial Pi so fi

will just be the identical evaluation of Pi on SI and the question is if the prover does this sort of weird process which a priori looks like it's independent on each on each element here do these actually fit together to themselves be the encoding of some further polinomial pi+ one okay um so um let me rephrase this problem in the following way so again we start with Fi we assume that fi is a code word so fi sort of it lifts to a polinomial pi that encodes to it if we run the fry folding

operation on fi then uh the question is does there exist something down here uh which lifts fi +1 now what uh was shown in the original fry paper by um beness on bentov hores and riev is that indeed uh there does exist a pi+ one here if the prover is honest then fi+ one will itself be a code word now um um this is not so simple to show it it depends on what these Maps Qi are uh and we'll say much more about this later but you might be asking the key sort of further question here which is what what actually is the relationship between these two polinomial so if I start with some Pi I encode it and then I do this

weird folding operation in the coefficient uh sorry the evaluation domain um then uh what did I thereby do in the coefficient domain so what did I do to Pi's coefficient when I when I fry folded uh its encoding now uh in the prime field case Okay so again in the prime field case only it it's not too hard to write down what this relationship is it looks like an even odd folding okay so what what I'll do is I'll I'll I'll write down coefficients for P0 let's say so a0 up to uh a 2 the L minus one the question is if I fold this this thing's encoding

using the the challenge r0 um then what are the coefficients of the resulting polinomial well it turns out to be an even odd fold okay so I'm going to refine p 0 into even and odd substrings I'm then going to scale the odd substring by r0o and add um add that resulting thing to the even substring what I get is a polinomial of of the right degree right so this is degree less than 2 L minus one instead of 2 the L um and that is is my P1 so it's not too hard to to take this a step further um or or L steps should we say if I if I do this a log number of

times then remember the very last polinomial is a constant and we can ask what will that constant be well you can sort of extrapolate this process and see that it will look like this okay where these RS are are the successive uh fry verifier challenges now this might look familiar to anybody who works with multilinear polinomial this is exactly the multi-linear uh this is the evaluation of a multilinear polinomial say capital a um at this point R whose components right so R is an L variate Point its components are exactly the fry uh verifier challenges

okay so this observation is key to what um base fold PCS does uh we are sort of one step away from being able to describe if that PCS so the last step left has to do with the sum check okay so when in the setup of a PCS we start with some point Z that we want to evaluate our multilinear at now if we could just use these zis as our fry challenges we would we would get the evaluation we want but fry would then become insecure um you can't know the verifier or challenges you know before you actually commit your your your

oracles even just the positive indexed oracles so what we want is a way to reduce the claim we care about namely whether a of Z is some prescribed value say s to to a further claim uh about uh a of R where R is something random independent of of both a and z uh now the sum check gives us a really standard way of doing this essentially this is what we care about here on the left a of Z we we can express this thing we care about as the sum over the cube of of something else this is a of a v times a sort of partially evaluated uh equality indicator if we write down H for this

thing on the inside of the sum then uh it's it's enough to learn the sum of H over the cube okay that in other words is exactly a of Z what the sum check lets us do is reduce this claim to the further claim uh of whether h of R holds for for some random Point h of R equals s something else rather for some random point R okay so so this gives us the reduction we want right instead um instead of using the Z's we will use some random things R but will also run a sum check on H in parallel or in relieved okay so this putting these ideas together we get the idea of Base folds um multi-linear

PCS okay so here's how it works graphically if we start um with a multi-linear um over over a prime field um this is what a multilinear looks like we have some some coefficients indexed by these lbit strings what we do is we flatten it we interpret these coefficients as if they were the coefficients of something univariate of degree less than 2 to the L finally we read Solomon encode this using the NTT the resulting thing is is our multi-linear commitment to um capital A okay so now when it comes time to evaluate we we run Fry on this and do a sum check okay so uh we treat this thing

as our zeroth Oracle send it we get a challenge back and uh in line we send this Zero Sum check um round polinomial h0 um in the meantime locally we we we fold F0 using the verifier Randomness we get something something new F1 send that as an oracle get a further challenge send a further sum check round polinomial and so on we do this uh log number of times and um then then uh finally uh we get something which should be constant okay if the Prov is honest

the prover sends the verifier this constant and then this gives the verifier what it needs to walk away with uh the evaluation of capital a um okay so this essentially concludes the various background ideas that um we need to write down uh at this point I'm going to start trying to adapt this to the binary case and we'll see what what works and what doesn't work and and what we need to do okay so uh remember in the prime field case these siis are multiplicative subgroups the qis are the squaring map so this is a kind of easy mode everything works very nicely uh we

can't do this in the binary case right so the squaring map is is not 2: one anywhere in in a binary field let alone on some huge multiplicative subgroup this thing is actually a field an isomorphism on our field uh the frobenius isomorphism over F2 okay so what we're going to do instead is is something else so so now our K okay so remember K is a binary field we we can view it as a as a vector space over its own subfield F2 okay so K is now a vector space over f 2 and we can let our SI be F2 Vector subspaces of K of of some Dimension so this will be

you know l l plus r dimensional this will be one fewer and one fewer and so on until we get to something R dimensional um our qis our qis are now going to be what's called um Subspace Vanishing pols so these are sort of pols which which double as linear Maps Okay so the the zero locus of of each Qi will be a linear Subspace actually of Dimension One and what ends up happening is that these maps are actually F2 linear maps in other words the evaluation map of Qi uh that it induces from K to itself is actually linear over F2 okay so

um what do we do well we let the siis be F2 linear subspaces of K we let the qis be linear Maps now each Qi should reduce the dimension of Si by one okay so to do that it's it's enough that the kernel of of Qi as a linear map um a priori is just some some uh one-dimensional Subspace of K but we need it actually to be contained in si so other words qi's kernel should be in si that way it actually decreases the dimension of of Si as opposed to just injecting it into to another Subspace okay so that that is that is all um not new this comes from the

original fry paper but the key question for us is which qis should we use all all fry tells us is that they should be linear they should be Subspace Vanishing polinomial and they should knock out one dimension each each time you go but beyond that they don't say anything further uh now for us this is a crucial question because the key even a fold that we did have in the prime field case if we just choose our qis at Liberty then uh we will not get anything meaningful in the coefficient domain so that would break that would break the attempt to carry bfold over into the binary case so the first key uh question we need to solve is is what what qis

should we should we use um so so yeah so I'll say a few more things looking ahead at at what the challenges are so so as I was just saying we we need to choose um qis which cause a folding action on the coefficient space uh that we want namely it should be something like an even odd fold um and finally can we make packing work uh there are a few further further fry tricks and um innovations that we do uh I will get to those later on okay so in order to explain our choice

of qis we need to um make a quick detour into this additive NTT so this is a really great work by lch um Lin chungan 14 um remember our goal is to find a a sequence of maps Qi uh to to to look ahead actually we're going to take these from from something that has to do with LCA okay so um let's review what that work does so so what we want is an NT analog what is the NT do well what it does is take a polinomial coefficients okay so it takes these AIS um and it outputs the evaluations of the resulting polinomial

over over some domain s in your field okay so this list of P0 of x0 p 0 of X1 up to to up to something else for for all x's in s0 this is the output of the NTT um the whole point in the prime field case is that in the special case that s0 is Power of Two And multiplicative we can do this efficiently in in quasi linear time in this in this list size okay can we get something similar for our new type of of S which is a a additive or an F2 linear Subspace what Lin shung andh Han show is that you can

do this although there's there's a sort of tricky catch which is that um the initial polinomial p 0 of X instead of being expressed in the standard monomial uh basis in other words these coefficients are attached to just the monomial powers of X okay we need to express our initial P0 in in some new basis where the the basis elements uh the polinomial we're multiplying our coefficients by are are something else okay so these capital Y eyes are are a basis over K right of this space of polinomial of degree less than 2 to the L obviously the most natural basis would

be would be this thing but these are a different basis and it turns out that um if we flatten um so so the flattening we we want is actually this one not not this one so as a first observation if we take our multilinear right with coefficients a and we flatten it with respect to the lch basis then at at least at least the first step of of Base fold we can at least do that right like at least this step we now get a way to do it efficiently um now that doesn't really get us that far but it's at least a first thing to notice okay so um

okay so in order to tell you what the Q Qi should be I need to say just a few things about lch and um I'm going to do this you know really really quickly um happy to to answer questions at the end but very roughly let's just try to get a a picture for how lch Works what they do is they write down a chain of linear subspaces of of K of of ascending sort of growing in dimension by one at each step um for each element in this chain you can write down a polinomial which they call W hat uh I of X which vanishes identically on UI okay so this is another one of these Subspace Vanishing polinomial it's it's sort of a

polinomial and a linear map at the same time um the yjs then arise as sort of products of of of these wi essentially the the bit representation of J tells you which wi you should multiply together um just to come out and say it what we end up needing to do is is writing down our cues so that this polinomial factorization uh uh happens so essentially uh what we show is that if you write down your cu's in such a way that for each eye I can take the First Eye of my my cu's and and chain them and the resulting composition should be exactly uh the lch maning polinomial uh

if you do that then then you get um the behavior you want well why very roughly the the even odd fold why does that work in the prime field case well it it comes down to a kind of fft like decomposition so remember what we what we had was this even odd combination um very very roughly what makes it work is that I can reexpress my initial polinomial in this way right I can sort of it into evens here and and odds here and if I plug in x s inside the argument um for both of them then I I I can sort of push push this odd thing up by one position and then add them and um this

recovers my original polinomial P so the key for us is that so the tricky thing is that this x squ is actually the QI kind of in disguise right remember that in the prime field case the qis are all squaring Maps so what we want is an analog of this so we want this kind of thing to hold can we um can we write down even and odd refinements of of rp0 such that if you plug in uh Q zero in internally then um you get an fft decomposition like this if you can then you'll get exactly the folding Behavior you want where um where

where these Yi are um are are Yi primes are are coming from the kind of even and odd refinements uh so this very roughly tells us what we need to do we need to sort of precompose or peel away uh a a factor of q0 out of uh all of these yis in order to um in order to get a clean fft decomposition and this kind of Works in an inevitable way as as a chain right so once I've peeled away q0 then um that that equals sort of W1 and there's only one choice of q1 such that

the composition equals W2 and and so on and so forth all the way up to Q you know L minus one okay so that was um you know embarrassingly abbreviated so encourage everyone to look at the paper and also to ask any questions but for now um that concludes our treatment of of how to to choose the Q eyes um once we have this we have uh something like bfold uh bfold multilinear PCS in the binary setting so that's great that's a first start um but the the real reason we're here is is is that we also want it it to work with

packing okay and packing again is an idea that comes from bineas that lets us get rid of an embedding overhead head right so really the idea here again is that read Solomon codes are only defined over kind of medium-sized alphabets in other words the alphabet needs to be as as large as the block length is or larger um we can't have a read Solomon code over F2 for example so what you end up needing to do if you're not clever is is embedding each bit into some uh 16bit field let's say and then applying readed Solomon um we we we can't do that um we don't want to do that because of embedding overhead

so so what is packing um you know picture is worth a thousand words so so let's describe it graphically um if you didn't pack right so if you did the naive thing then um if you start with a witness which we'll just say let's say has 32 symbols and those symbols are all bits okay if you start um if you start with a witness like that and um and proceed without packing in the naive way then we'll encode this under some code with rate let's say one2 and the resulting thing will have how many symbols well of course it's got to be 64 double uh what we started with right but the crucial point is that each of these

symbols individually will now be 16 bits instead of one bit so the actual increase in in in data size was not twofold but but rather 32 fold right right because we now have two sources of blowup one coming from um uh from from the rate and another coming from the symbols themselves growing okay so what you do with packing is essentially start with your exact same data that you started with but you redraw the boundaries um and interpret your your data as if it had way fewer symbols but with each symbol coming from a larger alphabet finally if we encode that thing with a code of the same rate okay so

again a rate one half code then the resulting thing only has four symbols and again each of those symbols is um is of the same size um okay so so same we got away with using a code of the same rate but um with a um an ultimate code word that's actually much much smaller 16 fold smaller okay so this idea goes back to Bas the question is um can we make something like it work um in in in our setting and okay so it's worth explaining why this actually works

now if you tried to play this game in a prime field setting it just would not be meaningful at all right so in general I can't just take a bunch of bits and declare that these 32 bits are actually uh a prime field element and then read Solomon and en code that and expect um expect something meaningful to come out right it just um wouldn't really work uh what makes us work is our use of binary Towers okay so in general you can't just do arbitrary boundary redrawing and expect something meaningful to come out um uh in our case and and again this goes back to Bas is that um we use uh we use

Towers which which essentially makes this meaningful just to recall this kind of graphically if you our field elements look like you know power of two with bit strings let's say 128 bits uh but in bineas we actually interpret F2 to the 128 as a degree 2 extension over over a field of half the bit width okay so the elements are are linear polinomial with two components over over a smaller field but this smaller thing is itself recursively an extension of something even smaller and so on and so forth until we get to the level of bids okay so our packing operation or or boundary redrawing or concatenating um is actually algebraically meaningful and

not just a kind of um a kind of Brute Force cast uh that that would not be algebraically meaningful okay so with that said uh we have enough now to describe very roughly what fineus does okay so again we start with a witness which now let's say is over F2 right or just some small binary field uh we pack it right which again is is a boundary redrawing um we get a a witness which is is is shorter as a vector but has components in in K uh some binary field uh really a tower of of some some

higher order over F2 and now uh we read Solomon and code this using the additive nt Okay so this um this is efficient um and makes sense uh in the process we're really viewing these things as again as the coefficients of something univariate but but in the novel uh basis in the lch basis not in the monomial basis okay so finally uh this encoding is uh Is our multi-linear commitment uh this thing would get you know Merkel hased and that would be the commitment um now when we evaluate we again run fry okay so we send this as an oracle we get some

Randomness we send uh some sum check polinomial and now when we fry fold we need to use our uh q0 map okay so the one that we we specially define for this purpose we want to use that one we get something again of half the length this is F1 send it as an oracle more randomus another Su check fold again using our q1 and uh so on and so forth we do this um uh log number of times and we get something um something which should be identically constant and uh the verifier can do just some small amount of local extra work and walk away with um with the evaluation of uh of the initial

thing at the chosen Point Z Okay so the claim that we we prove in in in great detail in the paper is that this multilinear BCS is correct and secure now interestingly you know usually completeness proofs are you know just a couple sentences you know it's true by inspection or something like that right this is an interesting case where even the completeness is far from straightforward right because we need to argue that this fry folding operation which if if you remember is pretty ad hoc and hard to um really wrap your head around what it's doing in the coefficient domain okay so the key point of our completeness proof is to argue that uh when we use these qis right as

opposed to some arbitrary qis then in the coefficient domain you are actually getting uh a a a a predictable even odd style of folding and not something arbitrary now the security proof is is also really involved um it it it really comes down to the security of fry right what you show roughly is that um if the prover tries to do something malicious right so commits to some code word f0o which is either uh a word f-zero rather which is either not uh not even close to the code at all or um or maybe F0 is close but then F1 uh you know hops to to a different code word right is close to

the wrong code word um if the prover tries to do anything uh of that sort then um then they will get caught during the fry querying phase um so this is a really really nice fact and um underlies uh how how fry Bas works okay so um I'm going to Breeze through just a couple further technical um things that we do to fry okay so over and above choosing our Maps we we actually have a new kind of many toone fry folding Okay so in in in classical fry uh there there is support for a higher aity folding so 2 to the Ada to one instead of two: one

here Ada is some some uh positive integer constant uh but how does that work what they actually do is they pull back y to some large coet right of size 2 to the Ada and interpolate something univariate of degree less than 2 to the Ada now that's great in In classical fry when you don't care about the meaning of of this final constant for us we do so so we can't do this if you did that then you would no longer get um multi-linear behavior in the coefficient domain so what we do so but this is a lot of efficiency gain to leave on the table sort of um if if

you can The Sweet Spot is something like 8:1 or or maybe 16 even um so what we're able to do is for in a new way where what it looks like is more like just skipping skipping uh every other Oracle or every two oracles and committing only to every third let's say um and the effect is that the fry folding you get when you jump from one Oracle to the to the next one three down is is something like a a tensor like a multi-linear style of folding and um for this we need uh we need a careful anal is we need need actually a new kind of proximity gap which is uh which is due to Jim and

myself from a previous paper where essentially if if you take a combination of code words where the coefficient Vector is a tensor right then um you you also get a proximity Gap in that setting um we we also we also actually changeed fry itself right so that it folds in a in a slightly different way where instead of even Plus R * oddd it's more like 1 - R * even plus r * odd and uh this lets us use as our initial Vector a uh instead of the monomial coefficients of our multilinear actually the lrange coefficients of our multilinear so that's much more

convenient in in actual applications right so yeah exactly so so capital A we start with we can express it in the multilinear lrange basis and and use those AIS as our um as our univariate coefficients so that that's pretty nice um what we end up with is is the is the evaluation of this um we we have an additional property of our qis that uh for each y the two elements X in this in this fiber over y differ by exactly one so this actually really it dates back to lch again although not stated in explicit form by them but this

is exactly a consequence of what they call normalization so it turns out this makes your ENT your added vent U more efficient it also uh makes fry more efficient in in various uh subtle ways which which we clarify in the paper okay so what what do we get from this well um in short we're we're moving very decidedly in the right direction as far as proof size is concerned over over and above Bas okay so this is ranging from something like Forex in in in the smaller cases to to 10x or more um this of course looks pretty good um I I will say that we are not uh not

done yet um we we have some some more things in the work so so the first thing to say is that these um proof sizes are provable provable security they're they're is a coding theoretic conjecture um um about proximity gaps um up to the unique decoding radius so this is not really the same ones um that that that are are better known from the deeple work right but um but but rather so so if if that were true then these would come down uh we are also looking at various new ideas that that will make these come down further in fact so what you see is that for total data constant right either you have 32 to the 32

binary coefficients right or you have 8bit coefficients but only you know two to the 29 of them and so on and so forth right so in other words total data size held constant but boundaries being redrawn in in different ways you can see that as the actual coefficient size gets smaller we are paying a premium improv size even though the commitment cost is the same so one one exciting thing that we have in the works is that a way to make these proof sizes look more like these ones um and finally the conjecture the coding theoretic conjecture actually would get bypassed so we would be able to provably um increase these still further and we we get something really

really comparable with um what you're more used to from uh from state-of-the-art systems so um I I'll I'll just say a few things looking uh to the Future um in bineas we have gadgets for things like multiplication and lookups uh we are uh continuing to explore new ideas around this right so we have an exciting new way of doing multiplication which um which uh uses gkr instead of uh lookups uh also we're exploring um product checks based on gkr um we we are thinking about a certain mathematical conjecture the one I just mentioned so the goal is to get

um proximity gaps for General codes General codes up to the unique decoding radius so this is not known and is really a tough one um and you know also of course there is a known result for read Solomon codes bigger than the unique decoding radius can we use that right so in order to do that we need to talk about list uh decoding and list polinomial commitment schemes instead of standard uh pcss stir I I think we all know about this exciting new work we are certainly interested in stir um there there's a compatibility issue with it with its use of quotienting okay so for us um we are not using fry merely as a

proximity test we're we're actually using it for a new role also namely as as a way of evaluating um so it it seems that if you use Stir out of the box without some adaptation then you will not be able to get um this additional use namely namely the valuation so it would be great um for for us or for anybody to think about whether we can make stir work in the setting of friy bineas so this is this is another exciting one and um yeah finally I I already mentioned this we we are thinking about a way which might uh make our proof sizes look look like the non-packed proof sizes even when even when we do

pack um so so that um I think concludes the official content um maybe we can pivot to questions at this point yeah I don't know if there's anyone who wants to jump in can also type your questions in the chat yes so we have one question in the chat

Ben you want to read it out loud yep sure so this is from kandre I didn't get the part about list decoding and why we would want it can you clarify okay so um this is is a generally a complicated story but very roughly very roughly there's a pattern where um there's a thing called a proximity Gap okay which I haven't explained yet um and the thing called a proximity Gap has a further thing called a proximity parameter so um in other words for each proximity parameter you either get the gap or or you don't or maybe you can't prove whether you do or don't so one pattern

that tends to happen in Works in both Bas and fribus and many other works is that um as as as the proximity um is that your computer uh this is my headphones sorry sorry as the proximity parameter gets bigger you um you get better proof size so very roughly right the proof size in in works like this come from the verifier having to do many many fry queries or some kind of query um uh the relevant parameter is the per query proportional probability of

catching a cheating prover um as your proximity parameter gets bigger your per query Effectiveness gets better and the total queries you need in order to push down the soundness error to something really tiny get smaller so that's good um for that reason it's usually better to have higher proximity parameters now um uh as your prox as your proximity parameter gets really high specifically higher than the unique decoding radius then um a lot of the abstractions just don't really make sense anymore you need to start talking about lists of close code word so so by definition uh the unique decoding radius is the radius such that um for each word there can be

at most one code word close to that word or none right but there can't be more than one so as soon as that radius gets sufficiently large um you can have instead of one or zero close code words you can have more um let's say some polinomial number if it's not too huge um so what that opens the possibility of is that the prover a malicious a very clever malicious prover could try to put commit to some word which is close to many code words instead of just one and then when push comes to shove the prover can then equivocate um about which code word they were really close to in the to begin with um whereas in the unique

decoding case if they're close at all they're only close to one so that's kind of binds them to that um polinomial as opposed to some other one and um so in short uh we want listy coding because we we actually don't want listy coding what we really want is higher proximity parameter but we then need to deal with list decoding um when we get to a higher proximity parameter okay are there any other

questions from anyone just giving one minute just in case but I guess if not um well it's time to say thank you thank you very much ben for the presentation uh thank thanks everyone for attending and yeah we will put the recording um online in the next few days I need to stop it actually okay thank you thank you very much everybody and uh see you next time thank you so much