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

Transcript

so I'm uh really excited to have Ron rothblum here today he's a professor at the techon and he works at the intersection of complexity Theory and cryptography he's especially focused on proof systems uh which is a topic near and dear to my own heart he's done some really uh fundamental work uh both on their security and efficiency and he's going to tell us a little bit about some of his more recent work today uh focusing on proving efficiency thanks Justin and uh thank you all for coming and the invitation uh to come here for this week it's a pleasure to be here um look forward to to uh meeting many of you later this week or during this talk hopefully so the title of the talk is proving as fast as Computing suct arguments with constant Pro overhead and

it's based on a sequence of joint works with uh the other Justin Justin homran and with NOA Roni from University of hia okay so the picture that I want you to have uh in mind throughout this talk is the following so we have we're interested in in deciding whether some uh statement is true or not I'm going to capture that as usual sort of in in complexity uh Theory by asking you know is a particular in does a particular input belongs to a language L does a particular input have a certain property so we have a verifier which is interested in this statement it's given X and it's allowed to interact with aover which has this uh the same input but also has uh some sort of NP witness proving that indeed X has this property okay so um and we want our prover to

convince the verifier that indeed X has this property that X belongs to the language L one thing the prover could do is just send over the witness the verifier checks and we're convinced that's sort of a traditional NP proof but we what we're interested in doing here is doing something that is much shorter so we want the prover to send much less information but nevertheless for the verifier to be uh convinced okay we'll Define things uh more formally in a few slides but that's sort of the picture that you should have in mind so before being a little bit more formal why are we interested in this and I want to give two different perspectives the first one which is sort of where uh I am coming from is the theory perspective and really the study of proof systems in general has been uh

an amazing uh Catalyst for the development of the theory of computation so if you think of the beginning of the field Notions like you know P versus NP NP completeness if you think about it these are all talking about the existence of proof systems and as you know our field has evolved we've looked at more you know various different Notions of proof systems and as we've looked at those and studied them we've had sort of seminal results the discovery so on one hand MP completeness zero knowledge proofs uh for those who are familiar with the PCP theorem so a lot of the development and most fundamental results in the theory of computation have evolved from the study and entire like subfields also have evolved from looking at proof system systems so it's a very exciting field from a theory perspective something that

I think is more rare is that simultaneously it is also extremely exciting from a practical perspective and that's something that's been happening in the recent years so there's uh you know the fact that I'm standing here and giving this talk is an indication of that so uh I believe and you can all you know probably convince me better than I can convince you that there is a lot of uh interest in succinct arguments um especially in the domain of blockchains and cryptocurrencies so as you might suspect from uh my introduction so far I am coming from sort of the theory perspective so I'm not really qualified to tell you of how uh important this is but here is a guy who probably is qualified um the title is from Time Magazine the prince of

crypto perhaps the most General cryptographic most powerful cryptographic technology to come out of the last decade is general purpose as sync as Zer knowledge proofs okay so uh definitely a huge amount of interest uh you know in Industry as we see here here today good so that is sort of uh the area of of succinct arguments once people started you know becoming really interested in Imp in uh implementing succinct arguments so people like Justin and and others quickly discovered that the one of the key bottlenecks if not the key bottleneck is the amount of work that the prover has to invest in order to prove the correctness of the computation and it turns out that uh even today with amazing work by by

Justin and others it is still orders of magnitude uh slower than just performing the computation by yourself okay and that you know so it's really a practical uh practically motivated problem but it it leads to you know fundamental question I think both in theory and practice can proving be as fast as Computing okay so that would be the the Holy Grail how close can we get okay so that is sort of uh what the stock is going to be about and before telling you you know what the results are um let me start with a dis disclaimer so you know throughout this talk I'm going to be Tak and the results that I state I'm going to be taking a theoretical perspective

so I'm going to talk be talking about you know the ASM totic behavior of proving uh correctness um and achieving in some cases optimal in some cases close to Optimal asymptotic Behavior I am not coming and claiming a concrete efficiency and um but but never okay and I'll say in a second why why you should not leave The Talk uh in this minute uh uh just a second before that one one benefit of doing this um is that I'm going to be Focus focusing on very precise well-defined metrics so it's not I'm not going to be telling you that you know this MacBook Pro if I run the prover uh on some particular implementation runs in whatever number of seconds no it is no super precise um metric which talks about asymptotic

Behavior which is in my mind very clean we'll see in a second and then you know then we can argue about that so things are going to be very very very uh precise um so again going to this question of why you should care so for the people here who are interested in theory you know I think this uh going to be introducing some new ideas which I think are are really interesting and we get in particular the best known Astic behavior for the Prov so we'll see uh exactly if you are uh interested in practice I would still encourage you to uh not abandon the talk uh five minutes in and the reason is I think that we are introducing here some new and different paradigms and there's I would say that there's nothing uh This this term of Galactic algorithms that have some you

know o of n time but really there's a two to the Thousand overhead going on it doesn't seem to be that there's anything of that nature going on here so I do think these things have the potential to influence also uh practice they certainly would need um you know have to be baked a little bit further to be to be practical but you know once you have these new ideas and we see throughout this field how very theoretical ideas even from the '90s have a tremendous impact also on practice um so I think there is potential for that here too Yeah you sort of touched on this but you know in TCS there's kind of two different ways we abuse asymptotics right one is looking at the limit and seeing stuff that is true there and is not true for reasonable values the other

is just sort of hiding constant factors or even log terms are sort of bigo notation should I be on the more on the lookout for one of those than the other or uh I don't think things uh start kicking in at huge values there's nothing of that going on here uh it's just a question of you know I'm not claiming uh concrete Behavior a because I'm not an expert in that and I have not implemented so I have no idea B there are extremely efficient implementations of things with worse asymptotic uh behavior that are out there and I would have a hard time competing with but it does not mean that you know I would out this would outperform them like humongous impx should I interpret it as you're not going to make assertions about the hidden constant factors but as far as you can tell there's no reason

they should be ridiculous kind of yeah yeah yeah and in particular when I'm but one thing to keep bear in mind is that maybe I'm like winning in some log factor which in practice the constant would be larger um you know it's hard to log factors versus constant are hard uh sometimes to compare okay so I said that I'm going to be precise about the the sort of the precise metric that I'm going to be looking at today so the you know when you're looking at such tiny factors like log factors you have to be particular really precise about what model of computation you're looking at so in the talk today I'm going to be focus on focusing on Boolean circuits this is in contrast I think that uh in

Justin St a couple weeks ago I imagine you were talking about arithmetic circuits right over pretty large finite fields and thinking of the prover as doing both field operations and other sort of ram operations here I'm going to be looking you know exclusively on Boolean circuits so I'm thinking of the computation that I care about being expressed as a Boolean circuit and imp implenting the prover as a Boolean circuit okay so it's a kind of apples to apples comparison so I'm comparing the original computation which is expressed as a Boolean circuit versus aover that is implemented as sort of a similar Boolean circuit so first of all what is a Boolean circuit I hope that everyone's familiar with that if not please let me know but it's sort of an uh A6 graph directed graph of this form we have

input nodes and we have gates gates compute a simple functions like and or Sor um stuff like that for throughout this talk think of uh the circuit contains um arbitrary Gates of constant Fanon but for simplicit let's say uh nand gate would be a complete set of gates we can just think of nand gates okay so that's the model of Boolean circuits why look at Boolean circuits and this was uh no the study of cryptography implemented by very uh efficient or measuring the efficiency of cryptography by bullan circuits is not something new this was sted by work of isit and sahai 15 years years ago so I do this first of all you know I think it's hard to argue that against the fact

that it's a very basic uh natural simple model of computation so in contrast to say a ram where we need to start having fights about what kind of instructions your hand does and does not have here it's very clean very simple okay um and because of that and it is my feeling at least and this is more of an arguable point that it really captures the intrinsic complexity of a problem okay because of its uh it is so clean and basic um another thing if you compare say to an arithmetic circuit so arithmetic circuits are great but they're sometimes not inconvenient um to express non-arithmetic computations right so if you want to express evaluating uh sha 256 for example I think it would be quite

inconvenient to do it as an arithmetic circuit you can and there works on uh such adjusts I'm trying to optimize that um but it is more natural to express it as a Boolean circuit so and lastly uh which I think I think is an an interesting point once you're able to express the prover as a Blan circuit and you treat that as a black box you can do things using that so for example if you're trying to prove correctness of a bunch of different computations now you you know that in each one you are running the same prover circuit that is doing the exact same operations now you can start thinking about P pipelining all these operations so you're doing the exact same thing okay so the focus today will be on on Boolean circuits so with that introduction in mind but now we can

sort of prove uh formally what we mean by a succinct argument so I'm thinking of uh like the picture before we have a verifier that has an input X we have the pro that has X and the witness w we have some circuit that we fix they interact ideally the interaction is you know not a lot of rounds like in this picture but it could be potentially we want the communication to be short that's uh this bullet over here and we want these standard completeness and soundness conditions right so if the statement is true and the approver uh is well behaved then we want our verifier to accept on the other hand if the statement is false if there does not exist any witness showing that x if x is not in the language right there is no such witness and even if the prover is not

well behaved no matter what the prover does as long as it's you know doesn't break crypto it's run as polinomial time then we want our verifier to accept only with small probability okay so uh the small probability we're going to call the soundness error and a small uh mean just briefly that the Restriction here to efficient provs for this kind of statement is inherent okay so if you wanted soundness even against unbounded provs You' have a problem but I think you know pragmatically it's good enough to think of efficient provs um as we said before you know we want we're looking for communication that's much shorter than the witness length um ideally poly logarithmic or or so another property that would be great

to have but uh it's not necessary for this definition to be highly non-trivial and interesting is zero knowledge I won't Define it formally but it basically means that when the statement is true you learn nothing beyond the fact that the statement is true so it's a very useful property you don't always need it um and entirely non true without it as a matter of fact there are at least uh in terms of theory you can sort of even tack it on for free once you have a succinct argument making it zero knowledge is usually easy and in fact um almost without loss of generality okay yeah you maybe planning and do this already but uh you know in the in the blockchain world it's mostly non- interactive proofs as you know so

just how these parameters translate for non-interactive proofs would be useful to review right so so the comparison between having this interactive uh picture versus a non- interractive thing yeah so for I mean you talk about communication right but so the non the point is the nonactive proof will probably include like a transcript or or the verifier will have to simulate that communication itself so the communication will translate to like proof link or verif fire time or something like that I would ass okay so first of all I think in the blockchain world a picture like this that is interactive would be uh really bad because you really want to just post a proof on a blockchain and not prove to anyone coming along that you've done things properly it is it is nevertheless and non-trivial and luckily we have this

amazing magical euristic called the fistic which asks you convert interactive protocols to become non-interactive um so the I will the way I will Express all the results today will be interactive but they can't be made non interactive using fmir and is it correct to say that when you try to minimize communication I should be thinking about minimizing proof length and verification so communication for me is number of bits sent overall right not number of rounds or something sure sure sure no but like in a non-interactive proof there's no notion of the communication length right there is it's a proof length that that was my question yeah okay in particular when you apply fiir here the communication that I have here will translate into one static proof exactly yes so what about the

verification time uh right so here I've not stated anything about verification time uh so I mean for the moment I'm happy with the verifier being uh polinomial time let's say not carrying so much I have gained the something really non-trivial happened here I managed to compress an empty witness it's a miracle right so something highly non-trivial happened here so that's why I defined it this way when I give the formal theorem statements we'll see what the verifier time is okay it's it's a good point but sort of here I'm trying to sort of say what is the interesting notion um basic definition and then we'll see what the exact parameters that we achieve are okay again so again to connect the dots to the blockchain world I mean verification time is very expensive

right in sort of like the current generations of blockchain so it is uh yeah um but somehow so from my perspective communication is something that you know once you sent it's it's it's there you've sent it it's it's part of the proof it's not something that it's going to be hard to you to compress it computation on the other hand particular verifier computation you could think of doing sort of another step another composition to reduce that later on so sort of once you have a protocol that has short Communication in my mind it is easier to to extend it and get fast verification the other way on the other hand if the

verifier is fast then in particular it means the communication is short um but again I think all these are fantastic questions but maybe I'll show the formal theorem statement and then we can sort of discuss verification time and so on okay okay so before I tell you the theorem statement let me mentioned some prior work so first of all and I think this is less relevant to this audience if you don't care about small factors and you're happy with approv running polinomial time this problem has been solved for 30 years okay we've known how to do this uh uh you know with a polinomial Time prover if you're happy with polinomial time um meaning polinomial overhead so computation takes time T if you're happy with a poly time prover it has been well known how to do

this less interesting if it's so it would be let's say a cubic or more overhead not relevant for practice and less interesting but it is sort of I think uh the reason why because uh in theory we are uh sort of in love with the notion of polinomial time why it took time um took time and to practice to start looking at smaller fa smaller factors and indeed in recent years people are looking uh at smaller factors and there have been recent dramatic improvements in Pro efficiency including uh both in practice and asymptotics I'm going to focus on asymptotics so first of all for Boolean circuits the model that I'm currently describing prior to our work it was known how to do for a circuit of size s how to achieve uh prover circuit with poly logarithmic

overhead okay so this was already known and already you know pretty amazing right with only poly logarithmic overhead you can prove correctness of a computation so that's for Boolean circuits if you look at arithmetic circuits uh as in Justin's talk um it was known prior to our work how to achieve strictly linear overhead um for arithmetic circuits um and this was sort of a sequence of works it's related to the techniques that I'll describe uh here today so um so we'll see this okay so if you're looking at arithmetic circuits over large Fields we've known how to achieve uh or we know how to achieve constant Pro overhead lastly let me mention this uh very briefly this question becomes

interesting if you insist on on zero knowledge this question is interesting even if you don't require the communication to be succinct so communication can be as big as the circuit but you acquire zero knowledge so it's non-trivial and even there we have some results there is still I'll mention maybe uh later on there are still open questions uh also there okay so the main reason result as the title might uh lead you to think is that we construct succinct Arguments for Boolean circuits with a strictly linear size prover okay we'll see the the more precise definition in a second but before doing that there is a sort of an issue with this theorem statement that I want to clarify so the issue is the following if you think of a a circuit a Boolean

circuit the number of bits requir to just describe the circuit of size s is s log s because for every gate I need to specify what are the inputs coming in right so this means that just a description of the circuit has super linear size and I want my prover to be really circuit size size so it seems problematic the prover can't even read the entire circuit the way we get around this is um what we basically show is the following so for every circuit that you give me there exists a corresponding prover circuit specifically tailored for the circuit that you gave me okay so you gave me a circuit of size s I can construct a prover circuit for that specific circuit with size o of s um the

transformation is pretty efficient but it has to to do to have this logarithmic overhead because just the description of the circuit is that much but is this point clear okay so for every circuit we have a pro circuit good so the first the main result that I uh want to state today is the following so in this uh theorem we're going to assume crypto so we're going to be making some cryptographical assumption the cryptographic assumption is quite mild or relatively mild I would say so we're assuming Collision resistant hash functions that can be evaluated by linear size circuits and we have candidate constructions for this okay so we're assuming but think of it basically as Collision resistant has functions everyone know what Collision resistant hash functions are hash

functions in which it's hard to find collisions they're compressing a lot of collisions exist but it's hard to find them I want it to be very efficient to evaluate the linear time there is the the size of the data you're hashing so throughout the these entire slides whenever I say linear time I mean linear size so I'm thinking of a Boolean circuit so I have I have data that I want to hash and I want the size of the circuit to be linear um in that size in the size of the data that I want to Hash okay so that's just to clarify I mean that's like that's Shaw in every hash function in practice right uh sure but um sort of sha is defined for sort of it has a very it has a fixed output l if you uh so you need to think of the

generalization if you're looking at it ASM totically but yeah absolutely okay so the theorem says the following so for every Boolean circuit there exists an argument system a succinct argument system for this kind of statement so we accept all X's sort of that uh for which there exists a corresponding witness that makes the circuit happy makes the circuit accept with the following properties so the prover uh size as promised is strictly linear in the size of the input circuit again this this a Boolean I'm implementing the pro as a Boolean circuit strictly linear in the size of the original circuit the verifier that you were uh interested uh in before and and justifiably so it requires a linear amount of pre-processing and that is inherent sort

of the verifier has to look at every bit of the circuit at some point otherwise you know could the Prov could in its head change the circuit functionality without the verifier ever noticing but we can push that to pre-processing um and after this pre-processing the online time for the verifier is basically just reading the input which is again necessary and on top of that it's po poly logarithmic in the circuit size and polinomial in Lambda where Lambda States is a security parameter so if you want s if you want to be sound against provs of size polinomial and Lambda or or even maybe subexponential and Lambda then you have a polinomial dependence on the security parameter so think of uh you know 128 or so in terms of the amount of

communication it's going to be uh poly logarithmic in the circuit size okay so instead of you know big witness which is you the natural witness is maybe the entire circuit we were we're drastically reducing it to poly logarithmic and a pol normal dependence on the security parameter um it is an interactive protocol the number of rounds and what I'll describe is logarithmic actually the same we can get the exact same results with uh log log rounds um but let me maybe I'll describe it so I should have said in the beginning this talk is a two there's going to be two parts to this talk the first part the other part is on on Thursday um maybe on Thursday I'll I'll mention that as well um so logarithmic number of rounds um and can be reduced to log log and

lastly in terms of the soundness error remember the soundness error is a probability of accepting a false statement so it can be an arbitrarily small constant which sounds pretty good you know arbitrarily small arbitarily small is pretty good but actually not so great so really what I would like here would to be something that is say that uh that uh shrinks uh with the security parameter so something may be negligible in the security parameter or ideally exponentially small in the security parameter okay so that is and in the next slide we'll discuss an improvement that improves on that aspect okay but that is the basic theorem statement uh questions there was a question on the zoom I didn't see all it was about the pre-processing costs okay the question

is how come the verifier pre-processing time is not omega of C log C because of reading the full circuit description so the verifi pre-processing is also fixed once the circuit is fixed okay so given a circuit I spit out aover circuit and a verifier pre-processing circuit um which are linear and C yeah so what does arit is small but not negligible in Lambda mean it means um so think of uh is there a constant that blows up as I make so I I don't think I I think of asymptotics where Lambda can grow and the so for example you could take this basic protocol and just repeat it poly lamba times okay the

soundness air would grow exponentially with Lambda but in terms of the pro size it will grow multiplicatively with Lambda so in concious to the norm where factors that depend on the security parameter are may be hidden here I'm fully expressing them so okay I am hiding one thing which there is an additive dependence on Lambda but I view that as being dominated by the circuit size but I'm not hiding any multiplicative factors on the security parameter here okay yeah if the circuit has um like repeated structure can you skip the pre-processing uh yes we'll get to that in the next theorem so actually in this result with noo we couldn't and the following thing uh we I'll show you that we can any more

questions okay so what I like about this theorem is we're really getting to this strictly linear near uh size prover which was uh sort of Out Of Reach beforehand uh the part that I don't like so much is that the soundless error it's pretty good arbitrarily small but still a constant a fixed constant yeah so given the Boolean circuit c um what is the complexity of the circuit that spits out the prover circuit okay so the the input is of size C log C right and it should be linear and that yeah so there's no like extra blow up there no not not a lot going on yeah okay so the I'll show you the next result with with uh Justin hren which we

really focus on improving the soundness error getting a similar result with better soundness error okay so uh the Improvement I would say with with Justin hren is the following so we are able to achieve this exponential dependence exponentially small soundness error like we wanted the overhead for theover there is going to be overhead for theover though so naively if you just as I said before if you were wanted to get from the previous theorem get 2 to the minus Lambda soundness error you would have to repeat the protocol Lambda times so you have Pro Time s uh C like size of c times Lambda here we're getting only a poly logarithmic dependence on Lambda just to remind if we think of Lambda as

being 128 log of that is seven so so poly s uh overhead okay so that's that's in terms of the the pro time I would love to get rid of this but it's still sort of uh very nice improvement over what you get by NA repetition um so that's the green stuff the red stuff is the caveats in this theorem which did not exist before uh so here we are restricted to sort of nice Boolean circuits um basically think of circuits that have a lot of repeated substructure which happened a lot especially I think in blockchains where you take say evaluate some small circuit again and again and again and again if that sounds familiar um so that would be a repeated substructure or if you're evaluating the same circuit on a ton of different inputs that again would be a

repeated substructure so we need some substructure of that uh form I won't Define it formally um so the theorem only holds for those kind of uh circuits and uh here you see there's no pre-processing so what we have is for the verifier is read the input polinomial dependence on Lambda the security parameter and the size of the small circuit that that's uh floating around in there okay does this make sense yeah so here description of C is C log C no so description of C so it's a regular circuit so I view this circuit C think of it maybe as just have you have some c0 which is applied again and again and again again and again so this would

be the size of C 0 the basic underlying circuit that's being repeated good so that is the theorem that I uh main theorem that I wanted to show you throughout these two talks I'll tell you what the plan is for for this talk and sort of in combination with the future talk on Thursday so what I want to start by doing is is to review sort of uh the classical approach to constructing succinct arguments um but the perspective that I'll have so for for those of you who've read Justin's uh book um he he covers these things but the perspective that I'm going to have is going to be very focused on error correcting codes and I find this perspective so it's a kind of a higher level abstraction I find this perspective very useful and it will sort

of lead us also to the solutions that we'll have getting a better efficiency so we'll be viewed sort of I think from a a little bit of a different perspective than what people are used to um in particular usually people describe everything via polinomial we'll see that really what the polins are giving us are a correcting codes with some very nice properties and try to isolate what these properties are then what I want to do is introduce a technique called code switching which really underlies our result and what they allow us to do is to replace the use of polinomial in some key places with other in some sense better eror Cor in codes that are good enough and allows to to have a big benefit over polinomial and this technique really underlies all

the results that achieve uh linear time succinct arguments in the literature including uh Justin's work breakdown and and others so this technique is really um a facilitator for that so also the works achieving sort of linear size arithmetic uh linear size provs for arithmetic circuits also rely on this code switching technique so really that's what I'm going to focus on uh in the talk today and then in the talk on Thursday my plan is to show how to use code switching to derive the main results that I just showed you for Boolean circuits either with constant soundness error or with uh exponentially small soundness error and the the the caveats that I mentioned so let's start by sort of a review of how to build succinct

arguments um in general but from the perspective of error correcting codes okay so how are babies born or how are succinct arguments uh born so like babies succinct arguments have two parents um typically so the two the two parents are an object that's called an interactive Oracle proof which I will Define uh in a moment and another which is sort of an information theoretic object um it generalizes a PCP for those who are familiar with that and then the other object is something called the vector commitment which is a cryptographic object and the simplest way to think of it is sort of what Merkel trees give you so with the Merle tree you can commit to a long Vector so that later on you can decommit to

particular uh bits um so that is sort of that would be an implementation of a vector commitment and when you have these two things together you combine them you get a succinct argument okay so we'll see that in a few slides but let me first Define what is an interactive Oracle proof so this a notion introduced concurrently in a work of Benson Kessa and and Nick over here and I work with uh Omar rold and Guy rothblum so it's kind of uh you should think of so interactive Oracle proof and know someone not heard of the term someone has someone heard of the term okay so everyone's familiar Okay cool so the way to think of it is a a hybrid between an interactive proof in the PCP the pictures that we have is as

before we have a verifier Andover the verifier is interested what it does X belong to the language L here notice that we have a powerful wizard because here soundness is going to be unconditional okay so statistical soundness no no crypto and the model is that the prover is allowed to send very long messages to our verifier and let's say that the verifier for the moment sort of ignores it okay verifier responds with a public uh with a random coin TOS Prov sends again another huge message to the verifier verifier responds with a a coints and so on and so forth at the very end of the interaction after the approver has sent all these long messages the verifier can read a few bits overall of what was sent and decid whether to accept or or reject

so that's a model of an IOP or interactive Oracle proof it seems like a bit of an artificial or weird model um which is I think part of the reason why I took the community uh some time to to to look at it but it turns out to be incredibly useful okay so its main use and the one that I'll talk about today is about constructing stinct arguments okay so this uh started with the work of Nick and and and others um it's also been incredibly useful for constructing efficient interactive proofs with statistical soundness that's why we introduced it in our work um getting proofs that are approaching the length of the witness I won't I won't go into details about this so maybe take my word on it that they have even additional applications Beyond just constructing

succinct arguments so I think a very uh exciting notion so that was iops Vector commitments I guess I already described you can take a long Vector produce a short hash short commitment so that later on you can decommit to individual bits of this long Vector okay and the canonical examp example would be uh a Merkel Merkel tree okay so why do these objects go hand inand together well the basic idea is you have your IOP you're supposed to send a really long message what do you do you commit to it using the vector commitment right so you send a short commitment um at the very end the verifier is interested in reading the few the few places you decommit so so that's the basic idea of uh how suct arguments uh are born we're going to get

into much more detail about how the iops are born as well but for the moment if we have an IOP and we have a Merkel hash clear how we got a suct argument right okay how about linear time getting a linear Time pro a suin argument with the linear time prover well we need two things to be for this to work we need our mer our Vector commitment to be efficient enough and we need the IOP to be efficient enough in terms of the vector commitment certainly from a theoretical perspective it's sort of a piece of cake basically if you take a Merkel tree and you implement under line Collision resistant hash function as one that is computable in linear size you automatically get that the vector commitment you can commit and decommit in linear time the hard part and the one

that I want to focus on today is how to construct an IOP in which the prover can be implemented in linear size so that would be uh our Focus there there is like let me just say that this regime of strictly linear size introduces a lot of annoying challenges uh but that's on the down side on the plus side it produces more papers so we get something back um cool so from now on the focus I'm going to focus on how our iops built and they via this uh perspective of error correcting codes okay so some yeah think about the parameters how long should I think about each message being and how many cells should I think about being

read um so often what happens so we'll see in the beginning in the first constructions we'll have you'll have a very long first message and the rest of the message will be very short so long as like circuit size and then the additional message are very short that's something that uh that is pretty typical later on we'll see that in the in the eventual construction that we have um the message sizes uh are going to be gradually shrinking so we'll start off circuit size then circuit size over 10 circuit size over 100 and so on and it's going to be a constant number of queries or what should I so it will be either log or log log many queries it will basically so we need to read some queries of every round and if we have the version that I stated with log

rounds would be log queries uh the version with log log would have uh poly log log queries Okay cool so uh have people do people know about error correcting codes uh okay so so let let's let's do it so what are air correcting codes so air correcting codes are an entire huge field um in in computer science or electron Engineering also and the goal is basically you know uh Alice is here on Earth Bob is over there on Mars and Alice wants to send messages to Bob and you know errors may happen you know Cosmic radiation and so on errors may happen and so the communication channel is noisy we want Alice to encode her message so that even if Cosmic radiation

happens some of the bits are corrupted nevertheless you can recover the message that is the goal of the field of of error correcting codes why is it at all related to uh field of of arguments uh first of all because essentially all um arguments that we have use error correcting codes usually it's hidden via the use of polinomial but the fundamental one of the fundamental properties of polinomial is that they form a good error correcting code but I want to say beyond that you know you can think of codes as ways to protect communication from adversarial corruption whereas succinct arguments pcps iops proof systems are ways to protect computation against adversarial corruption so I think it's very natural that these things come up thinking of computation is something sort of more

sophisticated than just communic than just communication but anyway that's sort of more philosophical be a bit more concrete was an what is an error correcting code so I view it as sort of a mapping an injective mapping from uh the small ball domain which I think of as the message space so we Let's uh assume we're using an alphabet called Sigma so we're taking a message that is K symbols from Sigma and producing a longer message which is n symbols from the same alphabet Sigma okay why is it important that it be at the very least injective so that you know poor Bob can recover the message that Alice sent so we want it to be uh um at the very least injective we actually want more than that

so if we look there are two kind of key parameters that we care about in coding one is the rate and the other is the distance so the rate is basically just saying you know measuring what is the overhead involved in doing this encoding how much larger is n compared to K how much redundancy are we introducing when we're in coding and ideally because you know communication tomorrow is is expensive we want uh the rate to be as close as possible to one right we looking for high rate codes the rate close as possible to one so that's one important measure so we could just you know use the identity mapping but that's not so great because you know whenever you have noise you're going to uh uh um fail in in in decoding so the other important property that we want from codes is

what's called as minimal distance which basically says that if you look at any two code words they have a large Hamming distance between them okay so this is saying that if you look at the minimal Hamming distance between any two distinct code words it has to be sort of say a constant fraction of the code or whatever that fraction is that is called the minimal distance of the code and here we sort of we really want code words to be as far as possible from one from one another so that we a that we are able to decode so we'd like also our distance to be as close as possible or our relative distance this fractional distance to be as close as possible to one do that make sense okay the slight unfortunate thing is that we can't have both so there's a Singleton bound which basically says

that their sum is at most one so you can't have have your cake and eat it to you can't have the raid be close to one and the distance close to one good so uh some extra properties that we will uh would like to have and typically have of codes one is that our codes are linear which just means that the sigma here is a field and you should view the transformation as a linear transformation over this field okay um the other is codes that are systematic which is just a fancy way of saying that if you look at the the first case symbols of the output you see exactly the message so you when you encode a message you first see the message itself and then some extra redundancy bits or redundancy symbols and all the all the

codes I will talk about throughout this uh work throughout this uh talk are going to be linear and systematic so in an example of a code everyone's favorite code the read Solon code basically looking at Univar polinomial um has very nice parameters one downside is that requires a large alphabet but it has other very nice properties um the reason that it has distance is that if you take any two Univar Pol nomials they can only agree on a small number of points so they have distance great so these are error correcting codes uh we're going to be also looking at two specific families or types of er correcting codes one which is really fundamental and important in construction of proof systems is what's called multiplication codes so these are codes that have the following curious property so we're

going to be looking at a linear Code E so mapping uh K vectors of length K to vectors of length n and I want the property oh I have I I switch between e and C for this code so all the C's should be e sorry about that but the property says that if you take any two code words and you multiply them pointwise so you take two vectors and do pointwise multiplication the result is another Vector of length n and what I want is that this Vector live in some related code word and some sorry some related code okay so anyone have an an idea of an example for such a code hint we have seen so far one

code okay so read Solon code right so if you take uh so if you look at two code words in the read Solon code they're going to be Univar polinomial if you take their pointwise product the result is itself also going to be uh somewhat larger degree polinomial but still polinomial as long as the degrees are small enough you have space so it's going to be yet again a polinomial so it so it belongs to some other related readed Solomon code of somewhat larger degree yeah so the canonical example would be readed Solomon it's also true for read m multivariate polinomial true for um AG codes and we have some so uh these are more or less all the examples more or less okay this is an extremely important property and um I would say in

a nutshell the reason that it's important in the construction of proof systems is this is what lets us handle multiplications that are going on in our circuit without this property we would not be able to do that the the last family of codes that I want to introduce are what are called tensor codes which is really a way of taking codes uh taking a code and producing from it a new code and getting some really amazing properties along the way so so the way I describe it here is going to be a tensor of two different codes so I have a code E1 mapping K1 vectors of a length K1 to N1 and code2 mapping vectors of a length K2 to uh N2 and this tensor operation is going to produce a new code which Maps

vectors of length K1 * K2 into vectors of length N1 * N2 okay how does this uh operation work so I'm going to be viewing notice that the messages here are vectors of length K1 * K2 I will view them as matrices of Dimensions K1 by K2 and the way that you do the encoding is that you first go along and encode each one of the columns using the code uh E1 and then you go and encode each one of the rows both original rows and the new rows using the code E2 what you get is indeed uh a matrix of Dimension N1 * N2 which I view as a vector of length N1 * N2 so that is the tensor of of two

codes questions about this so you might wonder why did I first encode The Columns and then the rows not vice versa the answer is that it doesn't matter but it doesn't matter because actually I would get the exact same code word is sort of a from basic linear algebra okay so it doesn't matter in which way you do the encoding okay so let's see some properties that uh we get when doing this uh this tensor encoding which is also incredibly useful so first of all in terms of the rate of the code notice that the rate of this new code the message is of size K1 * K2 the size of the code word is N1 * N2 so basically means that the rate of this

new code is the product of the two rates of the original codes okay so we are losing compared to each one of the original codes but potentially not by too much so that's in terms of of the rate of the tensor code the second property is uh what happens to the distance Not A Hard Exercise to see that the same behavior also happens to the minimal distance so if we had and these are all relative distances so if we have distance uh this distance for the first code this distance for the second code the new distance will be the product of the two distances uh lastly an important and very useful fact it's called so Tech the technical term is that tensor codes are locally testable and locally uh correctable basically I won't Define

what these Notions mean what it basically means that when I'm designing an IOP and I instruct aover to send over a code word that is supposed to belong to the tensor code you know an honest prover will do that a cheating prover can do whatever it wants these properties say that if it's going to send something that is not a proper code word I will catch it okay so there is no point in sending when I when I instruct theover to send a tensor code word there is no point in trying to send something else if it will I will catch it make sense so that is not a homework exercise that's more uh that's more complicated but tensor codes have this property so there's not any simple intuition for fact three um I can tell you what the the yeah um let me say

briefly uh about this so suppose that you take uh Prov instructed to send over a tensor code word and it doesn't want to do it because it wants to violate what I'm promising it has two options either send something that is very close to a tensor code word or something that is very far let's say for a second that it sent something very far so it sent some some total junk now you could think of uh you know this the code that I described here if you look at the rows they all belong should all belong to the code E2 and the columns because I said you can reverse the the order of stuff all the columns would belong to E1 so a natural test would be if if aover made a lot of Corruptions choose a random row or column and check that they

belong to the corresponding row or the corresponding code that that way you you could catch a pro that makes a lot of Corruptions what about Pro that makes a small number of Corruptions that you have a mechanism then it's really very close to a tensor code word and you have a mechanism to sort of read off uh symbols from the underlying tensor Cod word that is there so your close Force as far is just like can you actually like would your decoding algorithm work to get you back to um is that kind of it like you're within the the distance yeah so so there's some uh there's some threshold where from there on if you chose a random row or column you would catch it with good probability and at the same threshold uh and Below you would just be able to read off points

from the actual you have a mechanism for just reading off from the correct code word like in particular you're within the distance of you're within that distance yes so that it's Unique yeah or half the distance even so that's unique good so that is what I needed from in terms of like describing error correcting codes the last component that I'm going to need in this talk is something called the sub protocol um has someone not seen it okay so Su is is typically described as a protocol involving polinomial I want to describe it uh more abstractly as a protocol for tensor codes but let me first say what is the goal of of of su Che so the goal on sum Che is the following think of it as a protocol in

which you have a verifier which is given Oracle access to some uh code word of e of this code e and its goal is to compute the sum of the entries of of the message symbols or bits inside this code word okay of course it can just do this by reading them off and you know counting adding adding adding stuff up but the goal is to do it much more efficiently than K so we want something that is maybe poly logarithmic in K okay so just doing the sum so sum check just want to be able to compute the sum of the message bits much more efficiently than just reading them off such uh subject protocols and we'll show this I think in the next slide are known for all tensor codes so the one that you're

probably familiar with is a specific instantiation for multivar polinomial which are a special case of tensor codes um and really the tensor structure is what underlies some there it's also known for uh read Solon codes in the IOP setting s say unic okay so Nick and others um and you know I cannot say enough about this uh this protocol it's really at the heart of very fundamental results I would say both both in in in theory uh and in practice in theory uh IP equals P space MP equals next some of the most important results in complexity Theory um and you know this new work of of Justins uh I think also heavily relies on on Su and a lot of his previous Works relied on some so huge

fan I think Justin as well very important protocol and sort of the reason I would say is that it allows you an exponential saving on a very basic task so all you need to do is sort of reduce other task that you care about to this pretty rich class of computing sums and and that's enough okay so again the goal and Su check is very simple you have a code word it's in the sky you can read off individual bits and you want to compute the entire sum of the message bits so let's see how this is done in general for tensor codes okay so this is the picture that I have in mind they have a tensor code tensor code word right and what I care about is Computing the blue part of it right so so in terms of because I've I've gone from messages

that were vectors or code words that were vectors to matrices in Matrix notation it's a sum over all i j of C so this blue part the sum of the blue part and so in terms of notation here the blue part is K by K the overall thing is n byn so the naive protocol would have complexity K squ just read off the blue part I'm going to show you how to do it with complexity K give or take okay so this is how it works so the uh prover computes it takes the sum takes all of these the first three columns and adds them up okay so this would each CJ here is the column uh C1 C2 C3 adds them up let's call that uh

the the the resulting Vector let's call it call okay notice that this Vector I claim that it has to belong to our column code right do you see why so because this is a tensor code word I know that each one of these individual vectors belongs to the column code and I've added them up and we said that it's a linear code so when you add stuff up it should still be reside within the linear code so this Vector call has to reside within the linear code so we send this over notice that that is only uh like nend communication versus case squ so we're pretty happy what does the verifier do first of all it checks so I I put a till here because

maybe the pro cheated it was supposed to send call but it actually sent call tillo so first thing that you can check is that indeed call Tilla is a valid code word you rate it off entirely is it a valid code word second you can check you know if I look at call which was the sum of all of these things if I add up the three first coordinates of this Vector call what should I see so the first first coordinate of call is the sum of these three guys the second coordinate of call is the sum of these three guys and the third is the sum of these three guys if I add all these up together what what should I see the overall sum of the blue part right so um I don't where do I have

it okay so I don't have it here but like before the additional test that I'm going to do shortly if I look at the sum of the first three entries of call I'm supposed to see I I'm supposed to see sort of the the eventual result right what am I worried about at this point that the pro prover cheated it sent call Tilda which was a valid code word so it passed my test but the values that are there are just uh junk nonsense so I I want to wait to check consistency that this call Tilda was indeed computed correctly from C so here's what I'm going to do so maybe the main observation is that if call Tilda is different from call then we have two code words of this code um E1 I guess

the column code they are different code words and we know the different code words have to disagree on a lot of places because there's distance so if I choose a random location I should see this difference occurring right so that's what I'm going to do so the verifier chooses a random index iar and sort of it Compares call Tilda in position I star the value that I should see there is um the sum of the iar row so I just read off the iar row from C and see that it's consistent with what I saw here so again the Prov sent over this sort of partial sum um of the overall sum that I care about I check that it's

a valid code word and I can check that it's consistent with a real deal it suffices to check on a random location because the codes have distance okay so that is uh why in general tensor codes support Su Che good so that's all the background that we need and we can go ahead and construct iops so from here on it's going to be uh pretty simple I think so let's you know we've had all this background Let's uh come back again we're trying to construct iops for the moment we're not caring too much about efficiency just how are IOP is born so we care about Boolean circuits uh so for Simplicity let's think of our Boolean circuits as fan into um nand Gates so all the gates are fan into nand Gates and I'm going to

assume some topological ordering of the wires if we look at some input X for the circuit or input X and the corresponding witness W I want to define capital W to be the values that the all of the wires in the circuit uh obtain sorted according to the topological uh ordering I'll Define WL as the same thing where instead of you know when I hit index I or gate i instead of y i let's say gate i instead of taking the value of the gate I take the value of its left uh input and similarly WR will be the value of the right input okay so once you have uh a circuit and you fix an input you can Define all of these things and just something to notice is

that uh really WL I think of it as W as a sort of a permutation of w based on you know for every gate who is its left or right input it doesn't necessarily have to be permutations but for Simplicity let's think of it as though they are permutations okay any questions so far feel like I may have lost some of you yeah back to the previous slides please sure uh so in in the Su check you have need the verifier to have an oracle access to the Matrix yes yes so I'm thinking of this Matrix as living in the sky I need Oracle access to the Matrix the way I described it here I'm going to read off end points from this Matrix the

entire iar row um with a little bit of more work you could make sure that actually all the verifier needs to do is read one point from this uh code word so really instead of reading the entire blue part one point is going to be enough turned out to be very useful okay so we're back to Boolean circuits we have our W WL and WRR um we're trying to construct an IOP so our IOP is going to use you know all of the uh guns that were presented in act two are going to appear in act 3 so we're going to use uh Code E again linear and systematic mapping uh going from K to N I want to assume that it's a multiplication code I want to assume

that the product of the multiplication code they call this e supports Su check and I want to assume that I have the sort of local testing and self-correction procedures that we set tensor codes have so that I can assume that whenever I I tell the prover to send over a code word it actually does good so I have this code here's how I'm going to construct I op so given an input X and so I guess input X and the witness W the prover sends it it constructs W which is the value of all the wires and codes them under e call the resulting thing W hat sending it over to uh the verifier remember we're in the IOP model it's okay to send long messages so we sent basically all the values that the wires obtained and coded

under a n correcting code same thing for WL same thing for WRR so far so good and that's uh so that's what the verifier does that's the long message that I was alluding to in my answer to to Tim before um so one uh long message followed by shorter interaction so what does our verifier need to check now first thing I need to check you know these things that were sent I only have Oracle access to them I can only query a few bits I want to check that they are indeed valid code words how do I do this well I've just kind of assumed it away this is what exactly what the local testing and checking procedures allow me to do so this is kind of for free once I have this property so again when it means that even a cheating prover when it sends stuff it

has to send valid code words second thing that I want to check is that WL was computed sort of correctly according to the correct uh permutation from W and similarly for WR WR so I call that a permutation test second thing I want to test third thing is you know that the nand gates were computed correctly so if I look at every index i w is actually equal to the nand of WL in position I and WR in position I so that's what this expression is about so this the nand relation and lastly I need to care to check pretty good idea to check that the output of the circuit is one meaning that you know it was accepting and to check that the input is indeed X but

let's ignore uh those tests for for today okay questions is it clear that if I'm able to check all these things then I should be pretty happy PL and PR comes from the pre-processing um so so far they I've only defined them I haven't used them but they are once the circuit is defined that determines uh Pi L and pi r you're asking about Pi uh uh in step to is two permutations BL and br oh yeah so yeah so I I want to check them they are once the circuit is fixed they are determined I will have to do stuff in the pre-processing that will facilitate this test but not like

the way that this is implemented will use pre-processing right because these are things that fully uh are sort of these are what determine the circuit so if you uh like once you have a circuit they fully defined and and vice versa does that make sense okay question yeah U maybe I misunderstood something but shouldn't WL and WR they're subset like strict subsets of w right so it's true that you know input Gates don't have a left uh is that why you're thinking like input Gates don't have an incoming stuff and and so on well I'm thinking W's all the gates in the circuit think of W's being uh all sure all the

gates not the wires yeah that's what's confusing yeah yeah so uh step one we've sort of assumed the way I want to explain how we do two and three using the properties that we have of our code so first of all in terms of the permutation test so the situation that we have is that we have two different uh different or not different code words and we want to check that they're sort of the way that they're computed is a permutation on their index sets right so w in position Pi I is exactly equal to W Prime in position I for every I and the way we'll do this is as follows let's think of choosing a random Vector R and I want to claim that if this property holds it certainly must be the fact that if I take sort of an inner product of the W composed with pi Vector

with r it should be the same thing as the inner product of r with the w prime vector right if pointwise all these values agree then I do this uh this sum it's just still be true but sort of a fundamental property um I think most of you probably familiar with is that if these disagree on at least one point then the probability that this uh thing happens is at most one half if we're talking about bits if talking about uh field would be one over the field size so if my the thing that I'm trying to check is false with at least constant probability here it will uh this reduction will produce something in which these two values are not the same okay let's assume that that event

happened I want now what do I do well now I will do just a reorder of reordering of indices on the left hand side so whenever I saw Pi I I will just call it J okay here it's convenient that Pi is a permutation so I can just do do it this way so I'm now summing over I've shifted over uh this pi to Pi inverse uh of R okay and my I basically reduced my permutation test to checking that this equality holds okay and now I'm pretty happy because both of these both left and right hand terms are involving a sum and we have a way to check sums via the sum check protocol

right the fundamental thing though is and this is really uh one place in which multiplication codes appear is that W you can think of it as we have W Prime is a vector is a code word in our code e r is under R control so I can think of encoding it I would also have it be a vector under my code e so overall I have access to these two uh vectors two code words I can multiply them I get a code word from the product code and I can run some check on that that will let me compute this value similarly here if e is a if W belongs to my code word uh to my code e i compute the coding of this permuted value of R under the code e

multiply them this is sort of um in my head I'm not actually doing it because I don't want to read stuff off I run some check on the resulting thing I can compute this sum over here if they disagree I will catch it so I I didn't understand it very well but are the W and W Prime also code words and then are you saying that I I choose RI to be a code word as well so w and W Prime are are code words right for us from the previous slide they were the the encoding of the values so I I Chang notation a bit which is a bad idea but uh W was think of it as W hat and the W Prime is like w hat L okay what I care is about what happens in their message

bits whether the message is encoded within our permutations of one another so this is what's uh being described over here so I have access I have sort of I'm thinking of Oracle access it's like like the prover already sent in its first message both of these code words so I can query individual bits of them right so I already have them for R I chose R myself so I can in pre-processing compute an encoding of R okay and similar I can compute an encoding of R uh permuted according to the permutation which means that I have access to these two code words I can imagine multiplying them and running some check on that

okay My worry is like R if R is a code word how do we ensure that it's like a sufficiently random so that uh oh so so sorry so R is a random Vector in K totally random Vector in K and I encode that Vector okay I see okay so the message is random you can also choose it to be pseo random but let's think of fully random and I encode that and same same Vector r i permute and encode that okay so I can apply some check on these two uh sides of the the equation um and check that the equation actually holds okay so that's a permutation test um and as as as you stated Computing these encodings especially of

this guy which fully depends on the circuit I can do in a pre-processing step it doesn't depend on the input of the circuit only on the topology of the circuit where uh wires go to okay so yeah can you reuse the randomness if you cannot reuse it it's meaningless right how have to this do this for per uh per circuit input okay so it's true you you uh you cannot reuse um this Randomness so this this pre-processing it's a it's a good point which I should have mentioned the pre-processing in the first result is not reusable you can do it once you cannot uh reuse it again so it's a one it's a one time thing because you use this Randomness uh once you do it offline then you do it online you should

not reuse it so that is um you could say a caveat of the first result and the second result there is no pre-processing so there's nothing to worry about but a good point that I forgot to mention good so we took care of the permutation test the second test that we had was to check this nand relation so situation that we have is that we have three code wordss w w Prime and W double Prime and we want to check that this pointwise relation holds between uh the message bits right so we're going to use do the exact same trick so we choose a random vector R We compare if this hold should hold pointwise then these sums should hold and again we're in the exact same situation which where we can run Su

check on the left hand side and separately on the right right hand side and see that we got the same values okay here there's no need to uh um do any perut there's no permutation just like I just need an encoding of the vector R what have we seen so if we have a code e that's a multiplication code so that the product code supports Su check and that it has these local testing and self-correction procedures we can run all these tests and we have ourselves an IOP in particular if I take e to be a tensor product of a read Solon code so read Solon is multiplic is multiplicative when you do tensoring it maintains the multiplicative uh property and it magically gives us some check and local testing so a tensor product of

read solman code would have all the three properties that we wanted if you do that you'd get yourself in uh very nice IOP that would have been the stateof the art in the early 90s okay but that's all you need so it sort of really isolates what are the properties that you need from aor correcting codes in order to get iops actually if you took e The Code E to be a rment code Univar polinomial then it would have the multiplication property um and due to work of of Nick and others it would also have a separate a different Su check protocol and a separate low low degree test something called fry and that that is really the technology underlying Stark's um you know uh IOP or or business so that sort

of concludes the review of how typically succinct arguments are constructed I want to show you sort of uh took a while I want to show you sort of some of the very quickly the the new idea this code switching idea that I hinted on and we'll do the rest on on Thursday so how did we do uh construct fast iops not just a sync so the key bottleneck and what I've described so far is that we have to send this encoding of the wire values and the way I described it so far we we're sending the encoding under multiplication code and the unfortunate thing is that the best multiplication codes that we have are essentially read solement code for which encoding it's VI fft and it incurs a logarithmic overhead so if you want to follow the template

that I described above you're using you're encoding all the wire values using a multiplication code you're kind of stuck I mean if you had a way to uh speed up fft wow um but we don't um so so not clear what to do so the new idea that uh and this is sort of the main bottleneck and everything I described so far because for example some check we know how to do with a linear size linear time or linear size prover so the really the fundamental bottleneck is just doing the encoding um and the new idea that I want to describe is a technique that we call code switching which it sounds weird but I'll describe in a second how how it works the IDE would be to encode under a code which is not a multiplication code

it's very efficient but nevertheless be able to later on switch to a multiplication code but without actually doing the encoding okay so what do I mean by that so the idea is the following we're going to have the prover send the encoding under so we have our Code E which is the multiplication code and I'm not going to send the encoding of the wire values under that code I'm going to encode it under a different code uh which I call C so bring me your fastest code that you have I want to use that code so fine I I I sent that encoding the verifier is somewhat uh you know sad because it liked getting encodings under e and it got encoding under C it's going to entirely ignore that and pretend as though the encoding

that was sent was encoding under the multiplication Code E okay and act and follow the protocol at some point in the protocol you know sadly enough the verifier needs to access bits of e which it doesn't have it only has bits of C the challenge that we have is that we want to query a few points of say e of w but what we have in our hand or in the sky that was sent as an IOP message is CFW okay so that's the challenge that um seems weird how do we overcome this and we're going to do this by via additional interaction with theover okay so we're going to design a special code C so that using additional

interaction even though I have sort of I have in the sky I have Oracle access to CFW I am able using that an additional interaction to check claims about e of w so i' I've managed to use one code to do then coding I've pretended that I actually use a different code but that lat later on using this I can check consistency so what we want is a Code E so that on one hand it's you know fastest code so linear time encodable you know good consonants and so on I want it to still be locally testable and correctable so I still have the properties know when the thing is sent I can check that check it and I want that given Oracle access to e of X or E of w

in the previous slide there is an additional IOP that lets you check values like is C of X in position I equal to some value so far so good so I need to design the code uh e like this and the solution is going to be any tensor of a linear time in quotable code is going to work and I'll show you this okay so why why why does a tensor of a linear time in quotable code work so think of a square tensor square root n by square root n so first of all I claim that if I take a linear time encodable code and I tensor it the resulting code is still going to be linear time encodable do you see why you just go over the columns and code each

one in linear time and because it's linear time it's also going to be constant rate so now you go over uh so you went sorry you went over all the rows and coded them now you go over all the columns overall it's going to be uh linear time okay so this preserves tensoring preserves uh the coding time uh at least here we said already before we had this uh we had these results showing that in general tensor codes are locally testable and correctable which again is this thing about when I instruct the pro to send a tensor code word it will send the tensor code word so All That Remains is this tricky property right right so given Oracle access to encoding of X I want to be able to compute C ofx in some location I um so how do we do

that so do you think this going back to the what was it you wanted multiplicative but also linear time yeah encodable right like if if you had that you wouldn't have to go through these hoops right yes you think there's a fundamental barrier there or or do you actually need like a trick like the one you're doing it's very unclear because you would think that if there was a fundamental barrier it would have to to do with the rate of the code but we do have constant rate multiplication codes so it it would it really if there is a bottleneck it has to be about efficient computation which we are very bad at reasoning about and so I really don't know what what what the answer is it would be I think a huge breakthrough in various different fields to construct multiplication codes that are better

than fft yeah and it will solve all of these problems in particular so what what we want is to be able we have an uh what we have in the sky is an encoding of e of w but we want to be able to sort of compute this and the first observation that we have is that this nice thing is just a linear function of w why because C is a linear code so it means that if I look at C of w in position I it's some linear combination with some corresponding coefficients of the values of w right it's a line because it's a linear code this claim that I have is a linear claim that's pretty nice so in particular as a

warm-up let's hide these coefficients so what if I hide the coefficients my goal now is to compute the sum of WJ given Oracle access to e OFW is the or rather the tensor of the linear time en quotable code right it's the code that I'm using and my goal is to compute the sum of the of the the message inside any idea of how to do that so what we have is Oracle access to a code that happens to be a tensor code word and we're interested in Computing the sum of the message inside so half an hour ago we saw that tensor codes have the su su check procedure Su Che protocol so some is

exactly doing this right it says any tensor code word not just polinomial also if you take a tensor of a linear time incable your favorite linear time encodable code it still supports Su Che so we able to compute this thing the sum of all the message parts so we can do this right the thing is that you know this hand doesn't is not really there so so for the warmup just using the fact that E A tensor code is enough but you know in reality we do have these annoying coefficients so the question you know can you do sort of a Lin check a check of uh when there are coefficients around for any tensor code and when you first look at this you start getting feeling a little queasy because the way that is this is sort of

typic ially handled is you just say oh I have um I have my my my Vector W that I care about I have the vector of coefficients let's just encode these coefficients and use the fact that we have a multiplication code to multiply the two Cod Roots together so once you have a multiplication code then dealing with coefficients is sort of automatic but our entire point is we don't have multiplication code so at this point like when we developed this I was very worried okay um and in particular in general I don't know how to do this what I will show you is how to deal with a specific structural coefficients so if coefficients are nice enough then I'll show you that we can do this and luckily enough that

suffices okay so what do I mean by the coefficients are nice enough so recall this is the structure that I have I'm talking about the tensor code word and now I have coefficients I'm not just doing the sum so suppose that miraculously the coefficients have the following structure so if I look at the coefficient for coordinate i j it's actually a product of something that depends only on I and something that depends only on J okay so there is sort of a fixed Vector um Lambda so that each Lambda i j is sort of the product of Lambda I * Lambda J okay suppose we had this nice property then we're in business I claim why basically because the same stck protocol that I showed you before as is almost

basically works all we'll need to do is adjust when we're doing this sum over the columns I'll just adjust according to sort of the column coefficients Lambda J so I sent over that so I've just taken into account the coefficients corresponding to each column and now when I do this uh this test is a test uh checking at that at a random locations call I agrees with the the I throw so when I compute the I throw I I should adjust with the corresponding coefficients and when I compute the sum of the entries of call Tilda I should also adjust with the corresponding coefficients so as long as uh my coefficients have this nice uh structure then I'm in business this so if I think of this

Lambda i j is a matrix of coefficients you remember what this kind of Matrix is called if it has this property so it's a rank one Matrix right it's a product it's an outer product of two vectors so it has to be a rank one Matrix and what this uh is it's on the title so what this is is is telling you that actually if the coefficients the coefficient Matrix happens to be rank one then we can do this for any tensor code the next observation so is that our code uh C which was the multiplication code the one that we the the the code C that we were using throughout the protocol the one that we pretended had been sent if we choose that code to be a

tensor code turns out that for tensor codes their coefficient structure has rank one it has to do with like T tensors of vectors uh leading to rank one in tensor codes for the same reason so indeed the coefficient that we have will have the right propert will have the right structure so as long as we choose our code C under which we're doing all of the all of the Machinery all the sum checks and so on to be a tensor of a multiplication code and we choose the code e to be a tensor of a linear time incable code then we're golden okay so somehow the point is that the multiplicative property is something that we only need for the code C and whereas the claim that we have sort of

of going from the claim about C to e is a linear claim which is why e doesn't have to be a multiplication code okay so sort of bird's eye view of what the protocol looks like so uh the IOP so the prover sends over an encoding under the fast code of the wire values and their uh shifts you can actually get a rid of the shift but let's ignore that so basically stands over the encoding of The Wire values verifier chooses uh the random uh Vector R and now that reduces to you sort of pretend that you have what was sent here was C you run all the Machinery that we saw before relating to C you get claims about CFW cwr cwl and now you run stum check on E to

verify these claims relative to these values okay so there are two sort of phases to this or three phases to this protocol okay one thing I'll briefly mention nearly out of time is that if we were to replace the linear time encodable code with a high rate code meaning that a code that has rate approaching one we would actually get an IOP in which the communication is nearly nearly nearly equal to the size of the circuit and actually using for nice enough NP relations um which include probably any Rel NP relation that you have in mind we can even get the the communication in the in the IOP to be just

1.1 times the witness length so if you compare it to the naive proof of sending over the witness to a proof in which you need to read only a few a small number of bits you only need to increase it by a 1.1 Factor okay and using this recently in last crypto together with my my student shafik we construct the the shortest Known Zero knowledge proofs so not arguments proofs with statistical soundness uh based on oneway functions so so this is very the point of the slide is that this Machinery is very flexible it lets you sort of distill different properties that you need from your codes in different places so you can use a high rate or a fast uh code to do then coding and then use a separate code for which you don't need to pay for

encoding to do sort of uh the proving okay so just to summarize this uh code set switching techniques as I said let's you sort of distill different aspects of the code so we don't need one code that has everything which turns out to be problematic fact you can separate it is very beneficial it's a very simple technique right all we did is Su check but it easily yields as as I described linear size proving for arithmetic circuits over large Fields if you're talking about small Fields I'll talk about that on Thursday then sort of some check starts breaking down so we'll need some mechanism to compensate for that that I'll do on on Thursday so the mechanism because we're using Su Che this stuff works over large fields on Thursday I'll describe what we do over uh small Fields

both with with the uh constant soundness and with the small uh exponentially Vanishing soundness and the small overhead for the prover okay so I think I'll stop here and happy to take any more questions maybe a question for Justin as much as is for you but uh the arithmetic versus Boolean distinction like to what extent is working to sort of optimizing for Boolean circuits interfere with trying to get say practical snarks or something like that so okay so Justin would have a better answer to me for this and let me let me start before before handing letting him uh complete it I think there's uh I do think it's it's a problem but it's a problem that people are working on using

different approaches which not NE don't necessarily focus on asymptotics but focus on on concrete efficiency so things like adjustin lookup arguments and so on are dealing with this kind of thing so I think there there is it is a problem but there is other Machinery as well to deal with it which maybe has different astics or different Behavior Uh so certainly a concern but concern that people are interested in but I'll hand it off to Justin yeah I'd say it creates more issues that aren't necessarily present um if you are happy to work over large fields and you're happy for your approver to run on like a random access machine instead of as a Boolean circuit um and uh so you might you might be dealing with things that are maybe

unnecessary in practice to deal with but it's also a good way to force you develop new ideas um and a lot of these ideas have already gone into things like breakdown and a bunch of followup work but let me maybe uh follow up on your question or ask so there are two things going on there's the the fact that the input circuit is Boolean and the fact that I'm trying to implement the prover as a Boolean circuit and I was sort of addressing the fact that the that whether it's relevant in practice that the input is expressed so the computation you care about is expressed as a Boolean circuit so that is one aspect and I think that is interesting you know people are are going you know are trying to use to invent new hash functions that are arithmetization friendly and so on because they want to

work with these big fields and so on if they were just treating their input as a Boolean circuit and had good machinery for doing so they would just use sha so that is why like view uh why I think it is useful to to be able to construct protocols that handle Boolean circuits I think that's important then comes the question that I think Justin answered which is why is it important for the prover to be implemented as a Boolean circuit so uh yeah and then then I think just ansers is the right one yeah just as a context like um is this a precursor to some of these like so-called practical linear time prover snars like Orion Etc yes yes they all rely on code

switching can you name a few uh can you name the codes that you use is those are not res Sol codes right so so I'm using so here here uh where was it so here I need I just need c to be a tensor of a multiplication code so I take re Solomon and I tensor it so basically be read Muller so multivariate lree polinomial here I want a tensor of a linear time incable code so there's a Code by Dan Spielman from the 90s which is linear time encodable if you tensor that e would be good enough and that's the code that underlies breakdown and uh or as well I believe um but I think there's a so it's very flexible so give me if some someone develops a faster code and you think there are good candidates you can

use those um so the bottleneck becomes it goes you know now we can go to the coding theorist and ask them you know give us faster codes and I think coding theorists you would think this is like super basic question for coding theorists but I don't think people in coding were thinking about encoding messages of size two to the 30 two to the 40 so it was never you know they had nice astics I don't think it was a concern for coding theorists now I think it is a huge one or should be mhm are there any places where this code switching is done with more than two codes so some like chain of yes on Thursday it was not planted question okay

[Applause] cool