Proving as Fast as Computing - Part 2 with Ron Rothblum | a16z crypto research

Transcript

thanks everyone for coming we have Ron rothbloom here again from the technion to uh tell us additional details about proving as fast as Computing so part two take it away awesome thanks Justin uh okay hi good morning everyone so as far as I can tell everyone that's here was also in my previous talk um I will do try to do like a really brief reminder of what was going on last time and what a time to cover uh this time okay so the setup uh which I guess we all know by now we're trying to construct succinct arguments um basic Notions of completeness and soundness so correct statements should be you should be able to prove false statements you should not be able to prove other than some small probability and we're looking we're doing this for

NP statements and we want short communication Azure knowledge is sort of uh optional and we're focusing throughout this talk on circuits mainly on on Boolean circuits okay um as was said uh last time I view I'm going to present protocols that are interactive they are public ones who can reduce the interaction using future mirror and this heuristically okay now one thing that's going to pop up a lot in the talk today is Epsilon which is the soundness error okay which we would like to be as small as possible okay so what we covered last time we're going to go into a little bit of a reminders of some technical stuff but the main technique that we discussed is

this technique that we call code switching which morally the way I think of it is a way to design iops so that you can encode whatever you care about using uh some code that has nice properties it does need to be a tensor code for what we showed but then pretend that the actual that the encoding that you sent was actually encoded under some other different tensor code that may have other useful properties and you know execute the protocol as as though that were the code that had actually been sent but then at the end switched meaning you know verify uh you know emulate access to the the sort of pretend virtual code using the actual code that was sent so that was the idea

behind code switching which we saw and using this we were able to derive linear size provers for arithmetic circuits um and high rate iops so just something that I think I wasn't maybe clear enough about last time clarification in terms of sort of credits so this idea of code switching was in my work with with Nova from 2020 but we were sort of our mindset was deriving High rate iops iops that are very short and sort of follow-up Works uh sort of use the fact that you can use the same technique uh give or take to construct these dinner size provers for arithmetic circuits essentially one way to do it is to take our approach and replace the high rate code with the linear time encodable code and that would be good enough

so going back to the main so so far what we saw what we saw last time in terms of like actual proofs were how to construct uh argument systems for arithmetic circuits but the main theorem that I stated and did not prove was for Boolean circuits right so the main theorem said that for Boolean circuits which in a sense are the most challenging uh case we want a strictly linear size prover expressed as a Boolean circuit um and in terms of verification we have uh of uh circuit size pre-processing as pointed out this pre-processing is non-reusable so if you don't like it we will need to have a linear size verifier um

and yeah and the communication is poly logarithmic the number of rounds is log can easily be made log log and the soundness error is in arbitrarily small constant right so uh we'll try to sort of see more or less the proof of that today then we had the second result with the result was just 10 which sort of under the same assumption uh linear time computable or linear size condition hashing same assumption as before here what the big benefit is that we get 2 to the minus Lambda soundness error rather than the constant and the overhead that we pay is sort of you know exponentially better than they think of just doing things in parallel so it's only poly logarithmic in in this Lambda this so that's the green Parts

the red Parts is that we only know how to do this for certain types of Boolean circuits so ones that have a lot of repeated substructure we'll see this today um but but here the verifier can really be sort of as long as this repeated sub the the substructure that's being repeated is small enough to verify is going to be really fast questions so far it's stuff that we've seen and I will uh uh hopefully not bore you too much with a little bit of more reminders about underlying techniques because we're going to use them extensively today we sort of thought that the main technical tool that gives rise to all of this stuff is this notion of iops or interactive Oracle proofs um we saw this before it's kind of for them for those coming from Theory it's a

multi-round version of pcps for those that are not you just send over long messages but at the end of the day the verifier only reads a few bits and you know we saw that using Vector commitments or Merkle trees you can move from iops into succinct arguments right so the easy part is uh you know using the right assumptions the easy part is getting good Vector commitments the hard part is designing good iops so that's what we need to focus on and we'll get to the side challenge later in the talk so far so good okay in terms of tools we have error correcting codes um you know these mappings taking messages into codeword we will care very much today about these two parameters

the rate the amount of overhead of the code and the distance of the code how good of an air correcting code it is how much do codewords avoid each other and we had this uh theorem saying you can't have your rate and eat it too um so Singleton balance saying that overall the sum of the rate and the distance can be in most one so we'll come up we covered all that multiplication codes codes that have this property that if you multiply Point wise to code words the resulting Vector belongs to some related code like we see with Solomon and tensor code which uh we're going to use again extensively today have this property you encode rows and code

columns or vice versa we see that the effect of tensoring two codes is sort of doubling the rate of the two rates of the code the effect of the distance is doubling the distances please stop me if you have any questions this is just covering stuff from last time very soon we will stop covering stuff from last time this is the last sort of reminder slide sub check typically viewed as a protocol for checking that the sum of a low degree polynomial is equal to uh to zero to some valid some predetermined value using an interactive proof with very small communication here I am abstracting it I'm thinking of it as a sort of General protocol that you can hope to have for any code so given uh so we were looking at a code word a w

belonging to a code E I think it's a very long code words and we're interested in Computing the sum of the message bits or message symbols or elements of this code so you can do this for a low degree polynomials for 10 serves more generally for read some and using Nix work um with iops yeah saw this we saw good so at this point I want to introduce sort of a new abstraction which will turn out to be very useful which is so you can think of it as a generalization of some check we call this an inner product check so it looks very similar but now instead of having uh so the notation switched a bit but it will be okay instead of having access to a

single code word I'm giving you Oracle access to two code words C and C Prime and the goal is to compute the inner product between the two message parts okay so in some check we had one code where we were looking at a sum now we have two code words and we're looking at the inner product so this this this abstraction on one hand it's actually if you think of it it's really used throughout everything but it has never materialized as an obstruction I think the reason for that is that it sort of typically trivial to get why because if your code C is a multiplication code what you can do is take the pointwise product of CNC Prime and now do some check on that right so you've done this multiplication

and then some overall you have an inner product so that is what is happening sort of everywhere and usually there's no need to point it out because you just do the multiplication and you're done in this work is going to be actually crucial to distill this notion and the reason that is that we don't have any linear time in quotable multiplication codes so if we want to do something sort of like the like this picture um we cannot just follow this idea multiply the code words and run subject because we don't have fast enough multiplication codes so at the heart of uh or this theorem that I'm going to prove to you is going to be a construction of some code C that is linear time encodable it is not going

to be a multiplication code but nevertheless it supports this operation right so you can do this inner product check using a linear size proofer there's an IOP for proving sort of this inner product check this extension of subject with a strictly linear size prover and also the encoding of the code is linear size okay so that's going to be sort of the heart of the uh the technical result okay so really we're going to have two steps the major one is the first one this is uh yeah this is all about getting the result with the constant soundness error so the first step is constructing a protocol code and a corresponding inner product check of linear size

uh once we have that then getting going from that to iops for General circuits will be pretty straightforward okay so the focus is on on constructing this thing uh so let's give it a shot right so our goal now again is to design a code that is linear time encodable but for which given two codeword you can using an IOP you can compute their the inner product of the messages so you know let's design a code and given all of these uh you know different types of codes that I've uh told you about here it may be a natural suggestion so let's take so I'm going to take my code C to be a tensor of two codes it's a very highly skewed tensor so in one direction we're going to have like a

very small code and in One Direction a very large code so it's a tensor of D and E D is sort of the large code so I'm going to fix a parameter a think of it as a constant 10 okay so a is equal to 10. so code number one takes pretty long messages of length n over 10 I'm thinking of n as being very large and I want it to be a linear time encodable code we have such codes and I don't need much beyond that okay so D is a linear time encodable code or maybe a tensor thereof but but ignore that so uh these sort of fastest code that you have lying around the other code that I will need is a Code E which is a tiny code right it's

encoding just like 10-bit messages and there I do need for E to be a multiplication code okay so if I could have uh I think Tim asked about this last time if I had a linear time Global multiplication codes I wouldn't need all this nonsense but I don't so encourage students to think about follow up on that question is there any hope in kind of saying linear time encodability plus multiplicative code lets you do Fast Forward transforms or something like this uh potentially I do think that the multiplication property underlies um ffts so it'd be great if you see like the beer actually is faster ffts that would be pretty convincing so otherwise the worry is that like there's a lot of work

to kind of you know get around this log factor that would be more directly and sort of gotten rid of through other means I think it would be so regardless it would be from my understanding that from from sort of coding theorists it will be major progress really major progress to design linear time and quotable multiplication codes um and you're asking like no so so I'm doubtful that if you had that then you would have a speed up for fft okay but I think such a code would be a good replacement in a lot of places where you use fft and you would have the faster uh evaluation like in TCS applications or actually for Signal processing um I don't know enough about similar processing to be confident about it but

it underlies sort of a lot of nice properties of fried salmon as a code follow from it being a multiplication code so the brother Camp Welsh decoding algorithm stuff like that the underlying thing that you have or the use of read summon also in NPC um so so that is a TCS or CS application um comes from the multiplicative property so I think it would be very exciting to develop such a thing not exclusively only for iops but more generally but since we don't have such a thing we'll resort to sort of more elaborate techniques so again we have our big code D which is very fast we have our Code E which is it's a small code we don't care so much about its encoding time because it's working on a constant size object

um right so these linear time encodable is a multiplication code and just you know as a sanity check let's see what is the overall encoding time when we transfer these guys so if I want to encode so the blue part is the message and I want to generate all the orange stuff then coding what do I do well as we said for tensors say I encode each one of the rows right that will take me n over a times some function of a which I don't care about so much overall that will be linear in M if I think of a as a constant and then encoding all of the rows I have uh some function of a number of rows for each one then coding is linear and M overall I will have linear and n

okay I mean there's no no real reason why not to use a relatively efficient multiplication code like read settlement here but I don't really care so far questions so just in terms of the overall encoding time of this new code it is linear okay so I've shown you a linear time quotable code but the the heart of the matter is showing you this procedure for computing inner products right so let's try to do that so here's the picture we have in mind we have two code words from this newly designed code and we're trying to compute the inner product of the blue parts right so notation wise we're trying to compute sort of these things sum of over i j c i j times C Prime i j

okay so let's try to do this and uh here's the first attempt so we know that all of the rows belong to our multiplication code right so if you take the first two rows you multiply them the result should lie and sort of in the product code that makes sense okay you multiply the second two rows it also lies in the product code we go along and we do all of these by the way this can all just be done in the prover's head so far nothing has been sent so I'm doing all of this and now I want to add up all of the green rows and now I want to claim a couple of things about the resulting sum first thing I want to claim is that this

resulting sum belongs to the product code of E you see why this is true so recall that each one of the green rows belongs to the product code because we just did multiplication and this product code is linear so when you add stuff up the resulting thing also belongs to the product code okay so that's one observation the second thing is that I want to say that if I look at the first the laser doesn't work if I look at the first three entries of w and sum them up I claim that I'm supposed to see something of interest there okay what is it well it's exactly the result that I'm looking for if you look at the inner product between the blue parts of C and C Prime versus the three first entries of w each

entry of w is computed essentially as an inner product of the corresponding columns now you add them up overall you've got the inner product okay great so I have the prover compute all this stuff just send W to me it's a short message I check that the sum of the first three three bits is the original claim that I have about the inner product and the W as a code word and now I seem to be in a really great in really great shape because um if the proofer stands the correct W as defined here then I'll just use the sum there and I'm done so if approval is trying to fool me uh she has to send some other alternate

W tilde which disagrees with w so we know that W is a code word of e star we know that W tilde is a code word of e star because we explicitly check that so if we have two distinct code words they have to disagree on a lot of locations that is what the distance guarantees right so now a very natural idea would be for the verifier to choose a column at random and then sort of you just need to check that that the value in that column was computed correctly so run another linear product another inner product check on this column okay so here's the the picture right so we're saying that if the proof is trying to cheat she will send a different W

tilde the red boxes are marking sort of places in which W tilde differs from W should be a large fraction now our verifier so the verifier doesn't see which ones are red or blue uh she just chooses a random if we're lucky she hits one of the red the red boxes in which case if we just run uh an inner product check that that this value over here was computed correctly meaning uh you know that the value there is basically the inner product of the two corresponding Earth Columns of C and C Prime then we're done okay it seems uh seems very natural seems very reminiscent of some check and

stuff that I showed you it is actually it also doesn't work um and the reason is the following so so the problem is basically we want we want to recurse um right right we've Shrunk The Problem by a constant Factor by an a factor we're pretty happy and seems very natural to recurs but the problem is that the column code is not from the code that I designed it's from this linear time encodable code which I don't have much control over in particular if I wanted to recurse I would need this uh decode the column code to be itself a tensor code and if I wanted to keep a cursing it would have to be a high dimensional tensor okay that's a major problem because if I wanted to overall just keep recursing

recursing recursing what I would have is that there would not really be a code D what I would have would just be a high dimensional tensor of a multiplication code e and that's a problem because if we are you know we saw before that if our Code E has distance Delta we saw that the behavior of distance and rate is that it sort of uh erase it to the power of whatever number of times it tensor it right we saw that if you do it uh once it squares and so on so the main thing is if we want our Code E to have constant distance because we're aiming for constant sums even just the first round it means that the rate of the code C becomes Vanishing

and just sending it over will be too long okay so okay now we cannot do this trick doing this sort of what I described here is really just doing some check essentially which will not work by itself or subject for tensor codes is there like a different operation you could interleave it with to keep sort of yeah yeah yeah um but so far this doesn't work and different operation will be code switching so the idea you know exactly you know we keep the entire picture that we had uh as before we've selected the Earth column but now I'm really as promised the Earth column is coming from a linear time encodable code not a code that you know not a tensor code that I can keep recursing on

but luckily enough we have this mechanism of code switching right if we're not happy with the code we just switched some other code right so what we'll do is we'll ask for the prover to send a fresh so the the arth column was encoded via the linear time in quotable code and I'm going to ask the prover hey Mr prover can you please send it to me under a fresh encoding under a nicer code okay at first glance it may seem kind of weird because you know these things were already encoded I think code them you know if I want to switch to some other code why didn't I a priori encode them using that code and the point is that the approver only needs to encode the arth column using this new code rather than all of the

columns and therefore she can afford to introduce more redundancy right because we are only encoding a single column we can use a sort of um better encoding in terms of distance that has worse rate because you don't need we don't need to encode each and every column so that's the key the key idea one thing to worry about which may be because uh you can't talk on uh Tuesday you're not going to be too worried about is that the prover could send the wrong encoding not like not send the encoding of the same message under a different code but let's ignore that for now we'll go we'll get back to that later okay so for the moment whenever I asked the prover to send a fresh encoding of a message let's believe that it actually

does so good so you know given this idea I think the protocol almost uh is immediate and here's the bird's eye view so the point is that you know as we uh recurse we're shrinking by a factor a I'm using L to denote the depth of the recursion because I was something else before uh so also the depth of the recursion and level um zero we're starting off with the message of length n as we go along we shrink by a factor of a and the point is that you know after L levels of uh recursion we are handling messages of size n over a to the L and I claim that at this point we can afford to introduce an overhead in terms of time an additional like a to the L

over two overhead in a second we'll see why basically because of uh how geometric series works but but you know let's believe me for a second that you can afford this extra overhead in time given this extra overhead in time you can afford to use to get like uh uh to use to to have like lower rates and if you believe that using a code that sort of hits the Singleton bound you you'll have like rate a to the minus L over two and you'll get distance 1 minus that okay so this will be uh our distance in the code and the health level of the iteration why is this good now you just do some uh you know back of the envelope calculation if I'm summing the work that

the proof is investing overall throughout all of the rounds then you have this sort of expression which luckily enough because of you know how some of the geometric series works is strictly linear okay that's on one on the one side on the other side in terms of soundness now instead of having we we don't have like a constant soundness error in each level of the recursion the soundness orange level keeps going down and down right it's like in every round it's a to the minus L over two and which we if we choose our a to be large enough that will be you know sufficient it will be a constant basically a constant determined by a so I have this slide with the worms I view I think the bird's eye view is is better so let me skip it let me mention

um one important thing is that I wanted to always this should be a to the minus all over two I wanted the distance of my code to be 1 minus a to the minus L over two but I mean in the beginning I was talking about using sort of a binary error correcting code because I'm looking at Boolean circuits I want the binary code to be compatible with that and not to have like overhead coming in from just using a larger alphabet but binary codes can have in most uh distance one half and here I want sort of distances approaching one so actually as I proceed throughout this protocol not only am I going to be switching codes I'm also going to be switching fields okay so I start off with a small field

and gradually throughout the protocol whenever I switch a code I also switch to a larger and larger field I'll be working with extension Fields so it'll be it will be okay so as we as many progress we're switching both codes and and underlying field just so whether we have a um we can get the good distance from the code so just to summarize what does the protocol look like um so we are given we have our basic code c0 and which is the code that I told you right it's the tensor of a linear time recordable code with a multiplication code right so n over a times a that's c0 the prover computes the W that thing that we had on the bottom right as before sends it over to the verifier

the verifier chooses a column uh so we call them r0 now the prover sends a fresh encoding of the earth columns this will be C1 and C1 Prime these are fresh encodings under sort of a new code C1 which is analogous to c0 it's again like a tensor of a linear time encodable code with a multiplication code where the multiplication code now we can afford for it to have worse rate and better distance in particular if you see you look at the next W that is sent because we're using a multiplication code with worse rate it's going to be a little bit longer okay so this keeps alternating where the size of the message see the columns keeps shrinking but the size of the W's keeps increasing as we go along

so one thing I didn't tell you about is the consistency checking although that really uh is very tightly connected to what we saw last time with code switching so how so the point is now you know in each round the previous ending of fresh encoding so the verifier already has an encoding of Cl and the approver sending a fresh encoding of the same message under a new code that's called that CL plus one and we want to check that indeed the message is encapsulated within or the same messages so we need a way to do this and first of all as I said last time using these procedures of local testing and self-correction at the very least we know that what the proofers are indeed code word we just need to check that the

messages inside are the same so let's let's see how to do that so this is sort of a Lemma let's imagine that we have sort of a general limit says if we have two tensor codes C and D with their message sizes are the same okay the block length the size of code words can be different so n and n Prime but both are tensor codes then I claim that there is an efficient procedure for checking membership in this language namely that given two code words the message inside is exactly the same um so let's actually show the proof of this quickly so right so we are given we as a verifier are given Oracle access to C of

M and some D of M Prime and our goal in life is to check that m is equal to M Prime so just as a mental exercise let's compare C of M versus C of M Prime okay what we have is encoding under D of M Prime but let's think of C of M Prime what do we know well if it happens to be that m is equal to M Prime then certainly C of M and C of M Prime are equal but if m is different from M Prime then C of M and C of M Prime not only are they not equal they're not equal in a lot of places because they are both code words of C so now if you imagine choosing a random coordinate I of this code then if m is equal to M Prime of course C of M and C

of M Prime will agree on this coordinate whereas if the messages are different because the code has distance they will disagree with high probability right so the verifier will so this is all nice is a mental experiment but the verifier doesn't actually have C Prime of C of M Prime but still verifier chooses I and we have these properties so and let's indeed assume that you know we were lucky enough we hit one of the you don't have to be super lucky because we have distance but indeed we hit one of the coordinates on which they differ the observation the next observation is that if you look at CM Prime in position I because C is a linear code this is some linear function of the message M Prime right we don't have direct access to

this because we only have access to D of M Prime um so the situation that we're at is that we have Oracle access to D of M Prime and we want to check some linear function of M Prime and we've seen a way to do this right so sort of sub check is does this we again run into this like annoying issue that we had last time that we have coefficients because this is a specific linear function it's not just a sum but the exact same issue that we had last time uh we have here in the exact same solution so if you're careful about it we can observe that the coefficients of this claim if C is a tensor code the coefficients viewed as a matrix have

rank one and then some checks just works Plug and Play okay so that's how we check consistency throughout all this the proof we're sending over these fresh encodings questions yeah so what is the tensor structure of D like does d need to be a high dimensional tensor uh no no so so D was the linear time quotable code it can be a square tensor of your favorite linear time recordable code but I'm doing some check over it it's enough to do a sort of so so think of like a some check over a square thing so you just need like a quadratic saving uh product saving is enough for you good so we've seen the key part which is

the linear time inner product check using this how do we get IOP for circuits basically following the same temp template that we saw last time which is quite standard so we have a circuit we're trying to construct an IOP for this circuit let's assume the circuit just contains nand Gates we denote the wire values by W if you uh here as a function I I use the K as the number of wires just because that was the size of messages in my code and we have these sort of I think of it as permutation saying for each gate what are its left and right inputs same thing that we had exactly that we had last time but the things that we need to check now are sort of this nand check that W and position I is equal to the Nan of wli and w r i

to check that indeed WL and WR were computed correctly um so this is a sort of function composition uh the circle there and then the input and output is consistent okay so that's exactly the same picture that we had uh last time in terms of like how are iops designed let me sort of but my point is sort of just showing or reminding why really the key point is an inner product check so let's look for example on this test this uh uh sort of permutation test how did it work well we wanted to check that this happens for all indices I what we said is you can choose a random or pseudorandom vector r the test that it happens for every eye

reduces to this kind of inner product and now you uh you rearrange or relabel and both sides that you have are basically an inner product so you just run our fast linear time in our product check and you can do this and the same thing you can do for the nandtest oh even more direct good so what do we have so far we basically proved the first theorem that I showed you that for every Boolean circuit we have an argument system with constant prover overhead for Boolean circuits for constant proof overhead and constant soundness error that was the the first result um maybe before moving to the second result just a quick digest which also

relates to one of your questions from last time so in all the previous works that were using Code switching there was sort of sort of one sharp code switch right we encoded under a fast code we pretended that we had encoded under some different code and then we switched here we're doing sort of a much more gradual process we're alternating we're doing this very gentle gradual code switching in every uh in each and every step and gaining gaining from that just as a reminder when we didn't have this uh inner product check what did we use last time for those um in your products so so we we did we just didn't give them a name what we could say is you know you take uh you

multiply if you use a multiplication code you can just multiply two code words the result and now like the inner the inner product will now just be a sum of the product codeword right um so just it just didn't have a name but but it was there okay um so let's talk about how do we get 2 to the minus Lambda soundness error I we are going to pay for that the payment will be poly log Lambda overhead for the proofer which is very modest right just to remind ourselves again Lambda is what 128 we're not saying multiply by 128 we're saying multiply by log of that so it is a very uh mild overhead okay so we want to get iops the first

task is you know that I'll show you is how do we how do we get a linear time inner product check with 2 to the minus Lambda soundness error where I allow myself this poly log Lambda overhead okay so same thing that we did before with content proof or overhead and constant soundness now I want to achieve with two to the minus Lambda error and poly log Lambda overhead okay and this will turn out to be pretty easy I'll show it to you on the Whiteboard right so now our goal is again to solve the same like inner product uh design a code that supports inner product check where we're aiming for very good sounds error but we're willing to tolerate this polylog Lambda overhead so here's the idea

the code will be yet again a tensor code and it will again be a tensor where this kind of skewed picture actually this let's show here so here's the message and here's the entire code word the the the the tensor skewed the number of columns is Lambda the security parameter and number of rows is n over Lambda okay for my row code I'm going to use a read settlement code with say rate one half or or one-third or something like that so this is like overall this is maybe like a o of Lambda

okay for my column code I'm going to use the code that I we just used um or sorry that we just constructed okay so it's some code that supports linear time inner product checks with constant soundness error that itself came from a tensor but I want to forget about that so it's some code that supports uh uh efficient inner product checks okay so this is uh this is the the code that I'm using to get this new result I want to show an inner product check so I actually have two code words all right so this is code word c

uh sorry code word c and code word c Prime and my goal is to compute the inner product between uh I think it was blue before let's try to be consistent wait I want to compute the inner product between these two things I'm going to follow the sort of same moral strategy as before think of taking these each row here of both of these as a multiplication code I'm going to do the pointwise multiplication this is just in the prover's head you need to do it up to here so these are obtained by just multiplying viewing each one of these as a polynomial multiplying the two I get this and I add all the stuff up

and I got the same W that I had before right and it's exactly as before there's W that is computed correctly and if the prover wants to cheat it has to send some W tilde which is different what we did before is to choose a random coordinate and check it what I'm going to do now is different I'm going to check each and every one of the coordinates of w how so the coordinate number one how do I check it well how is it computed it was computed as the sum of these guys and these guys were each computed as the sum as the product of these two columns so really the first coordinate here is just itself an inner product between these two columns right I'm going to run the protocol that I had before which sounds weird because

it only has constant soundness error and I'm shooting for 2 to the minus Lambda s on this error the point though is that when the prover sent cheats and sends W tilde it's going to send a false claim on a constant fraction of these coordinates so when I it may be very very well be the case that the value here is different and I only have constant soundness error so I won't catch it but it's also going to be different and a bunch of other coordinates and in each one of them so in like o of Lambda coordinates and then each one of them I have a constant probability of catching the proofer so overall I get my 2 to the minus Lambda to the minus Omega Lambda probability of catching okay questions yeah so for the column

code you still do need this uh support in the product some check and also it has this systematic property that encodes the message like it keeps the message intact at first yeah I mean um so for me it's very convenient when in dealing generally with tensors to think of systematic codes so I usually just and often usually for free so I usually just don't worry about thinking of of non-systematic code if you're asking whether generalizes stand on systematic codes um possibly I haven't thought about that but here you're using this very special uh code that uh allows you it itself is a tensor code right right so I kind of forgot about it what I cared about is

for it being able to compute the uh inner product um you're right that we constructed that itself from a tensor code and I I think at some point I started out we're doing a lot of tensoring some of it is unnecessary um it's just as useful abstractions because I don't want to worry about um you know we just want to think oh this supports inner product checks I'm not trying to save on the amount of tensoring definitely if you were to thinking of making this practical that's something you would want to do but here I'm just looking for the asymptotic statement and the cleanest way of stating it thank you for the question okay um good so we pretty easily got this 2 to the minus lamb the soundness error let me show you another uh

sort of issue that that comes up usually when designing iops often we need to check uh so something that comes up a lot and we'll have a sort of related solution is that we are given access to a code word and we want to check uh I'll say in a double quotes that it vanishes or essentially is zero on some like nice structured uh part of the domain let's say over here okay people use vanishes because people usually think about polynomials and polynomials are zero means that they vanish um so so right so I want the protocol where I have Oracle access to this code word c and I want to check that it's sort of

identically zero over here so the traditional method of doing this is saying hey you know if this code word is supposed to vanish here let's you know choose a random linear combination and look at the inner product of this code word with a random vector right that's sort of the the usual way what we we saw a bunch of times both last time and this time and the problem that I have here is that this usually works it usually works really well it has like one over a field size soundness error which is usually just perfect but we are looking at very small Fields right we're looking say at gf2 so this will only have one half sounds error which I cannot afford right one thing you can do is repeat this but then

I wouldn't I would you know I need I would need to repeat Lambda times I get n times Lambda instead of n times polylog Lambda so I cannot do the standard trick so so let's see how we do this um again very very simple so let's look for a second on this um using all the colors let's look at this part over here that we want we want to check that the red part vanishes okay what I'm going to do is think of encoding this guy um with so including each row using an additional error correcting code okay a linear error correcting code

so I just I took these guys each row here and encoded it over here have this kind of picture what do I know suppose that this guy was not identically zero there was some like annoying seven hiding here everywhere else was zero so it's hard to catch because it's just like one place so the observation is that if if I have this annoying seven here seven is just an example okay um then the entire row here will have a lot of of sevens or like other numbers non-zeros right this a lot of the entries here will be corrupt so now what I'm going to do is run like um

this sort of Vanishing test on each and every one of the columns each one with a constant soundness error so for that I can again for each one of those they can use the random linear combination and they can use the code from before because I'm only I'm only shooting for constant soundness here but I do this for each and every one of the coordinates so as before because a constant fraction of them so of Lambda are corrupt with to the minus Omega Lambda I'm going to catch it and sort of in terms of like the this Machinery so far would be uh good enough to get you the nand test that we need when you're constructing iops for circuits let's talk for a second about the permutation check so when we want to check the things or permutation of one another

so we want to check something of this of the form that we have here sorry let's see if Pi I is equal to C Prime of I for every index I and the way we solved it you know earlier today and and last time was using this idea of random linear combinations relabel um and that's that but now we are running again to the issue that our field is small we cannot afford a one over F error so we cannot do that use this trick so we need a solution and I don't have one which is unfortunate if you have one at the more than uh the extremely excited to see it um what I do have is a solution that works if the permutation is nice enough okay so before we had a solution that

worked for every permutation here it will only work for permutations that are nice and that is the reason why we can only handle these circuits with like regular substructure I'll give just like a an idea flavor of why for structured permutations uh things are easier boom in between right so the the situation that we care about is that we have C and C Prime and the contents of the message there are supposed to be a permutation a specific permutation of the contents of the message here but in reality we know that in our IOP the message here is going to sort of be like the values of the wires of the circuit and here it's going to be sort of the left or right wires or something

like that so think of it as you know if I just if I do something like take some small function and repeat it a lot of times what I will see here will be sort of the value of the the input and then the value after the first step value of their second step and so on all the steps of the function and then if I look at the sort of left wires and right wires morally what you're supposed to see is the same picture but shift it up or shifted down in One Direction in a direction right so um this will maybe go here everyone will be shifted up so that's the kind of permutation that we that we uh will be restricted to but why is it easier to handle such

permutations well you can think of an intermediate code word in which you sort of separate there were sort of two things going on um or actually the way I described it yeah the way I described it there's not much going on like all you have is the permutation is basically just a move one up kind of flavor in reality there's going to be like stuff going on locally between the layers but it's sort of Let's ignore that for a second or forever um so we just think of doing something like a very very very specific permutation moving the rows up by one and that is simple enough that we can handle directly without using the random linear combinations

so morally speaking without getting into all the details let me just cover like one more annoyance mainly because it like really annoyed us but uh there's a happy ending to the story um so this is an issue that we call predictability so suppose you know we've worked hard we've designed this lit like an amazing linear size IOP so IOP that can be computed by a linear size prover and we have our linear size Vector commitment what do we do now well you know instead of sending the IOP messages we commit we decommit everyone is happy and we're done but here's like a super annoying issue so suppose that you you know you've done you've you've run the IOP and you've committed to other messages now the

verifier says hey come on I want to open up these coordinates now you're sort of what you need to do is take all your IOP messages and project them to these coordinates or select these coordinates right so it's like really uh sounds like really uh trivial but we're in a circuit model in which it becomes really annoying so what you're trying to design is a circuit that gets this input a long string and a bunch of indices into the string like so a string of length n k indices into the string and it outputs the projection of the string to these indices or select or selection so really like a multiplexer but for a bunch of indices not just one

and the names if you try for uh 10 seconds you'll get a construction of size n times K so doing something separate for each index but the number a k is going to be the number of queries in our IOP which is Lambda at least and uh the IOP string is the circuit size so if you did the naive thing you would just this stupidity would give you to Circuit size time security parameter which we want to avoid so the question is can you do better and in principle there's no reason why not I mean the input to your circuit is just of length sort of n plus k and you know maybe you can do a better circuit so for uh the first two papers we had really annoying ad hoc Solutions which

were sort of saying we're going to design our IOP with a very particular query set so like indices that we select we're going to have a very specific structure which was hard to maintain and hard to have and for those kind of uh uh indices we had a good circuit the happy ending is that we have an upcoming work in which we showed you can do this in general so there is a circuit that gets input a string and indices and in size n plus K outputs their projection okay so uh that's that um let me sort of conclude with some open problems something that I'm very interested in and would love to see is do these ideas

which are you know you've seen I'm thinking very uh asymptotic point of view can they have practical relevance can we use them potentially to get better sounds for subjects that will some somehow the limiting factor I think we can get better sounds sounds but the question is can this be uh you know practically relevant in terms of more uh Theory questions this polylog Lambda overhead I think would be amazing result to get rid of it's getting like strictly linear size circuits with uh small subconstant soundness error ideally exponentially small um I should mention that this question is a major question also in sort of kind of more traditional zero knowledge

proofs which are not required to be succinct so if you insist on zero knowledge um but don't require the communication to be succinct if you want strictly linear size provers and negligible soundness this has been you know explicitly open for 15 years and of major interest so that that's super interesting one way to get to do it would be via linear time encodable multiplication codes which we don't have um another thing is so sort of getting constant round um or getting even a non-interactive solution um another thing I'm very interested in so there have been like really beautiful Works sort of uh starting with with work of Justin's on getting improving the prover efficiency of gkr some uh I would

say an important protocol and the literature let me not uh go into the not super important but uh the state of the art is that this protocol can be done for arithmetic circuits with a linear size or time prover for Boolean circuit which is sort of the default notion I think in from a complexity point of view um we don't know how to do this and that that's uh skip number five maybe okay so I'll end here so I want to ask you about number five okay so so let me explain number five then right so I was kind of like throughout this talk it's kind of shoving zero knowledge aside basically said you know we can tack onto your knowledge for free the reason that this works is sort of once you have a succinct argument morally you can just

add zero knowledge for free on top of that but it is uh not so friendly in particular it means that you're using um you're going to be making sort of something we we call a non-black box use of cryptography and not something that's going to be very friendly in practice a better way of doing this would have to be to have our IOP itself be zero knowledge and then when you just compile it into the traditional sense of Merkle trees things would work out so the question here is trying to you know at the level of the IOP make it zero knowledge so sorry go ahead no there's a that's what I wanted to know about it I think yeah so so uh did you think about this video protocol

um not not so much I think uh so uh I think you're not on that right I think Ali has a version of the with the code switching and for like arithmetic circuit that gets uh zero knowledge I suspect that similar uh techniques could work here but I haven't thought about it too much yeah do you have a sense of um what kind of algorithms like can be executed in a Boolean circuit without overhead um Sha so a lot of this multiplexer thing apparently can but it's a it's a whole paper um the multiplexer is I think is a bad

example because this is something that is really a triviality on for an algorithm right right so something that's really trivial an algorithm just like output you know well well uh I'm actually thinking of like dippinger's algorithm um which sort of has to put things in the buckets um and I guess we don't know that you could do something like that in a circuit with that overhead but I'm wondering if there's some kind of um Intuition or rule of thumb for like where the line is um so not surprisingly Random Access is a problem um is that like a rule of thumb I think maybe yeah not I think it's a great

question I don't have a great answer unfortunately um Random Access is definitely a problem maybe maybe it's the primary problem right I'm trying to think if uh things like I mean Random Access is a problem but we are in some sense the Smoky plexor thing is addressing this so we have we can do something um it is still obviously I mean in a ram you just need like uh k wrap trivial Ram operations to retrieve candices you were saying you need o of n which is took us a lot of work and sweat and so on um so I'm not sure if it would be like Plug and Play into some other Ram algorithm um

yeah very interesting does this projection thing have other applications in like circuit simulation of ram algorithms things like that um it seems like a pretty fundamental question I I agree uh the reviews did not um so yeah I don't know something explicit it feels to be very fundamental and basic and something that should have been uh you know pointed out in the 70s but we didn't append it was not um in terms of applications like in general to doing the Rams um I don't know we do have an application of this for doing batch peer which is some other crypto thing but uh yeah thank you

[Applause]