Walkthrough of ArkLib

Transcript

All right. Um, thank you everyone for coming to the session. Um, so as as the title says, I'm I'm just going to go through arip uh go into the actual code and then I also explain in on the whiteboard sort of what the code means. Um so in terms of what I plan to say I will start with sort of the purely mathematical stuff and then I'll go into the formalizations of IUS with some concrete examples and also the stuff that I'm working on to make the IR spec more readable and more scalable in terms of proving.

Okay. So uh coding theory this is um so if you went to the mutual CA session uh just now uh we're formalizing all these definitions in lean and so I I wanted to show um let's see um okay so here is um so first of all this is what lean looks like let me zoom in a bit uh is this This >> bit more.

>> Yeah. Bit more. >> All right. >> Bit more for the old people. >> Yeah. >> All right. Um. >> Okay. So, >> yeah. >> Awesome. Um, cool. So, this is what lean looks like. You have an interview. I I put it on the right usually and that shows you sort of the state of what's happening in Le. So if I click on say at some point like here for instance when you can see sort of clearly what's are what is sort of on the game board uh so these are all the like hypotheses so you have say n which is some type uh and

then you have instances of the type saying that say the type is finite and the type has decidable equality and then f here is another type that is a field. It is finite and it has decidable equality and C >> is something infinite somewhere or >> yeah that's okay >> so so types in general are just sort of very underdefined. uh you need to put in hypothesis even something as trivial as uh showing that like being able to compare two elements of the type and give you a boolean result that needs to be uh an explicit instance because otherwise it's just

going to be a a propositions which sort of like carries no data. So that's that's sort of one of the many technical things that uh you need to work with when you work with leaf. And so this is the setup of a code. So this is see here we define it as a linear code. So uh you may recall a a linear code is a vector subspace uh over like f to the n or some field f.

And this is lean's notation for this. So in lean we try to make things as general as possible. And so we don't have a specific definition for subm module uh for subspace we just have subm module instead. >> So there is actually one but it was deprecated. >> Yeah. So people building math they have like deal with the scalability issues a lot and so they decided this is the best way. So it knows that it's a subspace by the fact that >> yeah so >> so you can always hover over these >> and so okay >> so it's deriving that semi >> right

>> so yeah this is a subm module definition it requires that r must be a semi ring and n must be a module over r okay so that's just a setup n is set to fment. >> Yeah. So here you should think of this as vectors uh indexed by n. So n here could be the set of >> okay >> the arrows here not really you shouldn't think of them as like maps or anything. >> So these are >> so n is the word.

>> Yeah well the n is the type of index. >> It's a type. Yes. Okay. >> Yeah. >> Um, so yeah, we have uh this is a functional programming language. So we use uh functions to uh express a lot of things. Uh and so this just means you have uh you should think of this as f raised to the power of n, right? Okay. Um so let's go back here. Um we can define proximity. Um first of all we just define like the number of elements in the in the finite field such that the

distance here is some custom custom notation. This is just the relative no the absolute distance between this vector and the code C is at most D. and we take the um cardality of this set. So this is just a >> Yes, it should look familiar. If it doesn't look familiar, >> yeah, I I'll pause here for questions. >> In this case, we're fixing the the equality like combination the art and >> um for now we we fix but in in the future we'll generalize to like

proximity generators. Yeah. >> So this is delta or >> uh the data like uh so this is absolute uh >> distance. Yeah. >> Yeah. We so we can go to definition here and it's just the distance from the code that we right so we define this to be sort of the minimum hamming distance between U to any vector V that is in C. Yeah, I was wondering what why there's like not there like little >> um

>> it's just >> just a name. >> Yeah, just a name. >> Yeah. >> So, so we can define >> sure >> lots of custom mutations. >> Yeah, >> but it's not a parameter, just a name of the operator. >> Yes. So, >> I think it's because I think there already was a delta in the previous information series in mass li. >> Yeah. Yeah, >> I think that's why. So that's why there's a a prime of this. >> Um yeah, you can see sort of stuff that is in blue is the the notation. >> Okay. So >> prime.

>> Yes. >> Yeah. >> The proximity measures comes the number of good randomnesses. Um fat I guess >> what is that fat fat randomness that >> random give you like something close to the code which may be good or bad depending on what >> yeah depending >> I call the good positive >> okay >> you know you want to deduce uh reduce correlated agreements so so these are the the redes that brings you close to the code Yeah. Yeah. Um and then you have the proximity gap definitions which says that um whenever

you have two vectors U and V such that their measure is more than a certain bound then the distance between the interleaf code uh the interleaf vector U and V and the interleaf code. Um so here it just means it interle itself with two >> with two. Yeah. So the the exponent is two. >> Yeah. >> Yeah. Is mostly >> okay. >> Okay. >> Just for personal curioity, what do you call the beautiful and symbol with >> you can Yeah, it's a bold tie. You can you can

always hover and then you see how to type it. Your eyes are still working. Yeah, I'm learning a lot of >> but in the comment the book you use >> uh >> yeah I I guess I should be >> yeah cuz I think um like tensor is not exactly the right thing right because tensor code is different from interleaf code. Yeah, >> our word tensor is super overloaded in this

>> tensor overloaded in >> Could you could you go against physicists what they mean by tensor? >> Yeah, technically inter with the with identity code. >> Yeah. >> Okay. >> Um >> so that's one P of the session. >> Yeah. And then you have correlated agreements. >> Can you scroll up for a second? So then approximate gaps in >> if the number of good randomness exceed certain the bound bound.

>> Mhm. >> And and next line is this a conclusion? >> Yeah. >> Yeah. Then it must be close to the intro. >> Okay. >> Yeah. So >> yes, let let me keep going and then eventually we'll get to the main labs of the proximity gap paper. which is unproven of course. Um okay so the next thing is just plain correlated agreement. Um so this just says there exist a set of large enough here large enough size such that um there is also a tuple of code words

from one to k. So that's why we have the spin k index here at the beginning. um where for each I this vi is in the code and that it agrees with the um vectors w i uh at exactly uh the set s uh so okay so c is the code delta is the distance k the uh >> k is some parameter >> the number of code words >> yeah the number of code Okay.

>> Yeah. >> W is the >> it's just a vectors of uh it's just a vector that does not need to be code words. Can be like far from the code or >> sorry >> the input words. >> Yeah. It's the input words. >> Yeah. >> Yeah. >> Oh, so it's from K to M to F. So that's from K from K by M to F. >> No, it's K of them of like M. >> So yeah. So you should think of this as K vectors. Yeah. Is this this currying that they haven't? Yes. >> Yeah. So reading is always >> a * m some sense.

>> Yeah. >> Okay. And you're saying if there is a finance set which is large enough >> and there exist V selection. >> Okay. >> So this K to N to F is mean just you have K code words. >> Yeah. >> Wait, where are we taking the the connection to a function? Um, >> yeah. >> So, we don't have the combination, we just have the the code words. >> Ah, so correct agreement between the different words.

>> Yeah, between different words. >> I see. I mean, isn't that just uh distance in the code? Distance uh like if I have like a bunch of code words that they have correct agreement, that means that they also have like a small distance in the code. >> Mhm. >> Yeah. I think yeah. Okay. So this is the inter code. >> Mhm. >> Okay. >> So this not the batch thing is there's no >> there's many of them. >> No, but I mean this particular one doesn't it's not >> Yeah. Yeah. This is just the distance. >> Yeah. The generic one.

>> Yeah. Okay. Okay. That makes sense. I thought it was already the the serum with the backing but it's just the distance for the interview. Yeah, I I think I think formal it's just my gut feeling if formalizing correlated agreement by means of the inter code or the inter words uh has some benefits even in other applications you know when when you in the end want to argue uh the whole security of the snark stark protocol on top of fry it's so often exactly using it simplifies proof writing at least paper pen proof writing just say Okay, this is a correlated approximate that distance and because you need to argue in the end

about the number of such possible interle approximates or correlated approximates. So just just as an input maybe it makes sense uh to to to to abstract it also that way here. I don't know >> I wonder like uh to me it's like you know that notion that before is that the distance of the interle code you know you could this is a pain but you could also think of linear codes where like the the alphabet is not a finite field but it's like a finite like um you know something that supports addition and multiplication like a ring like oh yeah vector and then you can like you know give array the inter code then becomes a linear code because

otherwise it isn't >> and then this become just the distance of the of the inter code and then maybe you save a definition. >> Yeah. >> Yeah. >> Yeah. >> Great. Um cool. So the scrolling down to the first lema um that we we stay here. So this is the theorem 1.2 too in the paper and so is >> it theorem or which one is it >> is the just the RS codes have >> yeah to Johnson >> up to Johnson right >> up to yeah just >> so you say reference

>> this is the proximity elements sure which version do you do you for we and generate a bibography to show in the blueprint PDF file. >> Sure. But if they if they update the paper and the theorems get renamed. >> Yeah. >> I'm writing documentation now the actual statement. So even if they change it >> okay but I mean >> yeah you could just point to a specific version that would >> but most of the time like what you want is we'll just instead of saying theorem point of this paper we'll just write the like plain language. But this has been published this this case.

>> Yeah, but they have to print after publishing. >> Yeah, but the >> Oh, if you point to publish Yeah. >> Okay. And >> yeah, but if you point to the published one, that's that's even worse, right? Because there you have most independent like >> Yeah. always point to the e-rint. And in this case, I would even point to a specific. >> Yeah. that that's just changing the biblioraphy. >> It's not a big >> Yeah, >> like these will just come in very correlated or correlation.

>> Um, so this is just the uh proximity gap >> and so it's states that for all delta that is uh at most the Johnson bound um then you have uh Right. And C here is just any sort of T set of vectors. Um >> yeah. >> Okay. So you have >> code words.

>> They they are not necessarily code words >> at least the the re Solomon code. >> Yeah. So the resolment code is sort of uniquely defined >> given the domain and the degree. >> Okay. >> Yeah. Um so so the code is fixed. Um is the C that gets turned into uh I guess an aine space. Maybe Katie you could narrate this. >> Yeah. So this definition you have uh you have an an aine space and then you generate a collection of tine spaces and this is this is what this line will do.

it gives you the align spaces inside f I in that case. So the vector space dimension I >> which is how the theorem is stated. So this is kind of like I gave like I have all this code word and I look at the aine space by them. >> Yeah. >> Yeah. Okay. Well, not the code word. >> Is it ever used somewhere the align space variant over the line? >> I find space over the lines. >> H well yes there there there are certain proof system that use separate random methods for each of >> Okay. Got it. Got it.

>> Yeah. And instead of using pal no even just like the two because the up space proof as I recall which addresses like one randomness for each of the component words uh that's just a slight general easy generalization of the same like two words only one. >> So this is the more general version of which kind of all the theorems in it. Then we have a statement for each thing. So for the alpha lines and then parameterized curves and so on and then the randomness would be different. Let's see. And in this there's no because the is already counted in the error bound because the error bound you get the >> yeah you can go to the error bound

definition in the same file basically and it's so first I'll read you you should read the the comment and then scroll down to the code. Okay. So it's just you have the the two radius and here first you define the rates and then you do an if statement. So this uh set is just the sort of left open right closed interval. So it if you hover over the the comments then you'll see this is the right uh definition.

Then so this is the unique decoding radius. then you have the simpler segments and then if it is between unique decoding and list decoding then you have this M parameter and the error is in terms of M. This is the >> the ceiling appears to be my birthday. I'm not sure you guys want to say that enough. Yeah. No, it's it's >> um otherwise it is zero. This is the >> Yeah. Yeah. Yeah.

>> It should always we should never reach that in the >> Yeah. >> Okay. >> Very quick question out of curiosity. Obviously, this is a development question which was you weren't a big fan of the notations we introduced for ranges. Was there a reason for this out of curiosity? Um I think it's kind of hard to maintain like >> okay >> future annotation may clash with it. >> Yeah. Yeah. So so because it uses brackets we tried to add the subscript to create more uniqueness and >> yes >> theing of this but okay but still you thought it was still too much risk.

Okay. I know. >> Yeah. >> Okay. >> I I would have another question of curious how long does it take to write this statement in ter how long did it take like uh >> to write this? >> I think this is fine. This one's quite fast. >> I mean, I think Casey, right? >> Yeah, this one is quite fast. >> No, I mean like the this together with Yeah, let's say the >> the correlation agreement. How long? >> Well, it depends because uh for example, for this one, I had to use some space library format which was kind of difficult to understand. So, it took more time because of that. But if you if you don't use new libraries, it could be faster. It's just for me because if I get to understand the whole new

>> Yeah. Bart like this echo >> time it I don't know >> would you say it's a few days uh more than a week >> oh no no this particular I don't know >> okay >> I mean I think they also the whole proximity got file right so I mean I think I think overall that took I mean including review >> with reviews yeah >> yeah with review that took a few weeks but I think the actual writing the main writing of of all of these results was more than a week or Yeah, the other one we took two of which two days of which were spent on space is much library.

>> This of course like this will be better because the more let's say library you have the less time will take the more you familiarize yourself with faster because >> you understand how things are defined. >> And I mean I think as well with these um there was quite a lot of backlog that was needed. So defining linear codes and resolment codes and things like this took a bit of time just because it didn't exist before. >> And actually I think one point that's actually quite important which was before Katie joined Never mind she had no experience whatsoever. Yes. So this is actually it took a week for someone who's a total I mean now you're no longer totally by the time that you wrote this

>> I think it's fair to say that you would just stop at this point like a month experience program because I just did mathematics my whole life >> so yeah I suppose it's kind of it's easy to pick up >> but I don't Yeah, >> I mean as you can see lots of the notations are very similar to what you would have in mat, right? >> Yeah. But they're like you always combine your >> group. Well, this is at the start.

When you don't have a proof, you can write sorry and then the lean type will throw a warning but not an error. >> Okay. >> So you it allows you to still compile your file with warnings instead of having >> So my is like I mean this is a blueprint. So we have a few a bunch of the proofs are closed but a lot of the more complex ones are just sorry. >> I mean for man I would expect that he would be sorry for a while pro. No, I I do want to show. So yeah, this is basically the end of of the files.

It's just we state all the main theorems of the proximity gaps paper. >> Um so this this all this is unproven. Let me go to some proven things which includes the Johnson file. Um so >> yeah, we have the statement. >> Yeah. So for instance, this is Johnson bound. I think nobody ever called Fion Spilman nor find out. >> Nobody has ever spilled >> it like a like agreement look of like a multiver in a theorem prover.

>> Yeah. >> Oh, okay. Okay. >> No, no, I was joking that nobody has done it in general but because the proofs are very convoluted bags are found. It's uh >> actually quite quite easy understandable. Uh look at the original paper first. >> Yeah, I find bounds on the questions. >> Yeah. >> Because then yeah, eventually I will and put it off. >> It's once you understood this idea that there questions.

Yeah, >> I would say for my retirement. >> Yeah, >> I would say for my retirement for 100,000. >> Yeah, actually this is quite nice to show >> the what here. >> Yeah, tomorrow. >> So, okay. Yeah, >> cool. >> So, here is the supposed proof of the Johnson bound. Um it Yeah. So, >> so you mean it pro you prove the number of approximates? >> Yeah. the cardality of the set B is almost this much. Um yeah the well I guess the problem is you you see this proof you see no sorry in this proof but you don't know if there were any stories

in any of the lemas that this proof uses >> and so that's where we get this print axioms where you can actually print out whether there was any step in the process that uses the sorry >> and so you can see proof that I get an impression of >> y Oh um >> want to make the interview a bit bigger maybe? So that >> Yeah, that is this the >> this proof of not yet retired >> the Johnson B.

>> Johnson that's the polomial approximate Johnson misunderstanding that you were mentioning that was not the proximity to >> it's just that the proof of Johnson. Ah okay guys got it got okay >> because this would be the paint of >> No we could we could hide all the complexity in the lass >> sure >> I think it's called Johnson the file >> yeah just just file yeah sure >> um so yeah I guess >> so let's start let's start >> so we says that in order to prove this it suffices to prove the following

In order to prove what what's the statement what is >> so maybe scroll up a bit and we can start from the state >> Q is the size of the field >> so yeah join us condition is subsets that satisfy the John strong Johnson condition.

>> Uh some condition >> let's go to the definition. >> Yeah. Uh just that >> so something is positive. Yeah.

>> Ah yeah. Yeah. It's Wait. This this sounds to me like like 1 minus something like 1 minus rate squared. >> Mhm. So E is this E v or E? >> No, E is the error. So that should be the agreement set square of the agreement set size is square of the agreement set. Could you go back to the definition? >> Yeah. >> So condition, what does it say? Could we just Sorry.

No, no, no. Yeah, this is great. This is great. Good. Yeah. Yeah. This is good. >> Um, >> okay. So, we have a finite set B. >> And then we have what is I have a fin a finite set N and a function on N. >> Mhm. >> Yeah. >> Any word V is uh also another function on N. Mhm. >> D, E and D are functions on B and and and V. >> Wait a second. Why?

>> So is so this points to a definitions in this in this other file where you can see exactly what E and D are. So this would be >> we we have functions named E and D in the Johnson namespace. Yeah, maybe we can future just understand what's what's this what's the condition strongest uh so what is it without lean what is E is the number of errors uh the distance more or less or D is >> so E I think it's like the the here like

the average distance between V and the set B. >> Yeah. >> So this is you take sum >> and then you divide by the size of B. >> This kind of the average distance. >> Yeah. And then D is the sort of the >> okay I I wouldn't be able to parse now because I recall only what's often called kabi memo but maybe average distance is there also present >> a technical question assuming makes sense how do you run any of this and let's assume I want to run Johnson does it make sense running anything or

or or is it compilation So technically yes it's every if every definition you use is computable then technically when you compile the program you can run it. So but let's assume that I I do something wrong right not on the finish like on the I don't know on the on the proof how will I do completion time or >> so there are two so one is are you defining something that is wrong in a sense that you write down a statement that does not satisfy the type checker and then you will get an error >> there's compilation >> yes you get an actual error message that says this isn't type check we might say we can't infer this type instance or you've done something which isn't satis And this happens when I write or >> uh so actually it happens there's a lang

there's an LSP and so you don't have to actually build every time you can get an error message but technically yes it' be when you compile >> it's already compiled. >> Okay. Yeah. Um but then obviously the other mistake you can do is that you write down something which passes a type checker but which is not the statement that you're >> actually in this case when will I know >> when someone tells you you're wrong >> like because you can write a true a true valid statement which is not the statement that you want right same on paper right you could write a definition which is does not actually define what you intend to define >> on definition but on the proof I mean I mean >> for the proof if if you're happy with your serum statement then you cannot produce a proof that is valid and passes

the lean type checker At compilation time. >> At completion time. >> Okay. Got it. So what is the proof that I write down is wrong? The type checker would say. >> Yes. >> You you'll get an error message. >> When do I ever need to run things? Never. >> Does it tell me >> for these kind of theorems? >> Yes, it tells you exactly what it is. It will show the exact step in the proof. For instance, we do have a mod right. >> Yeah, mod we haven't integ but but one you can put value.

>> But if you want if you want to see what maybe we can like break the proof quickly and then show we can break the jump bound proof >> and then so we can see an error message about proof breaking. >> Okay. See you later. >> Sounds great. >> Yeah. But but anyways, okay. If I if I have the F module, I run it and then I can prove that this F module satisfies some things compile time, but I can also run it as a program. >> Yes. But basically when you have the serum that says this construction has run by runlessness, the construction is an actual executable program. >> I see. Very nice. >> That's the that's the appeal. >> Yeah. Um so here you have a supply statement and you have to justify why this suffices or the conclusion. And this this line here is the proof for why

this suffices. >> So if I were to set the >> Yeah. Oh yeah, we can remove linear. Yeah. >> Yeah. So for instance, if I don't have this, then lean is going to complete. >> Oh yeah. >> Oh yeah. So immediately actually have the feeling. >> Yes. >> Yeah. It's instance. That's the app. And so you can see it'll say unsolved schools. If you scroll down on the info view >> um >> you can see here is the unsold school and then it'll give you some kind of error message. >> Yeah. And it's like it's this goal right here. The example you need to show that this Johnson denominator is non zero.

>> Perfect. Nice. >> Perfect. Great right. >> Yeah. >> So it's really good because you can basically not understand what you're doing >> and you won't do something wrong. >> You can get guided. >> You can get stuck in a loop, I guess. But yeah, but you can't you can't believe that you have something that works. >> So there are in progress like you might make progress that will not work. >> Yes. >> Yes. >> Um and you can see as well maybe if we add can we add like a dummy rewrite for like some using some ammo that wouldn't work and then we can you can see it will find like oh it doesn't find like a way to apply this rewrite. So for instance oh yeah we sim.

>> Yeah. So all these commands are called tappings. they are for you to prove theorems and so we have a bunch of these commands. I think the most uh important um yeah the most use one is a simplification and it it just tries to simplify the goals based on a bunch of lemas that it has we have registered as simplification lemas. This linear thing is a sort of linear arithmetic solver that uh takes in all the hypothesis and then it it will solve the go for you if it's something like this something like something is not equal to something something is less than something and so on. Um, so is that what you wanted to >> I was going to say if we add uh if we

try to do like a rewrite with a lema that's not actually useful and then we can just show the error message just like oh you tried to do this but we couldn't be able we couldn't apply this rewrite a model or something >> right >> yeah uh for instance uh this is another lema >> oh yeah but you don't want that field just >> it doesn't matter we'll get >> yeah Um, also these these tabs are like I use uh IDE with AI suggestion. So it just gives me stuff >> suggestions which may or may not work.

>> Yeah, most of the time they don't work. >> Um >> um yeah >> but yeah so I think they should have like in if you scroll down a bit in the info view there should be some message that says that like massoc didn't do anything I guess. Um, no. also something because there is yeah something that can be reass do we have like if we try add zero I guess you do nothing right there's no >> there's no something plus zero >> what is rewrite >> rewrite >> so this just rewriting a term in in the proof state >> yeah so if you try to rewrite using this lema here which is that a * 0 equals to zero then you will get an error message I think if you scroll >> oh yeah it'll say tactic rewrite failed

because it didn't find an instance of this >> and so it can't work. Um, so you get you get like kind of decent feedback about why what you're trying doesn't work. >> You had a question. >> Um, I answered my question. Excellent. >> Yeah. And now we fix the proof again. Cool. >> So that's that's all I wanted to show for the coding theory because I do want to move on. Yeah. >> Uh, yeah. And then actually because the exact step at the end is probably automated, right?

>> Uh >> is that an is that an apply question mark or an asop question mark? >> Oh, is there >> I'm thinking about the exact step at the end. >> The final step in this was a specifically craft. >> Yeah. >> Okay. >> Okay. So now I have another question and maybe this is a good one for so I I so so okay so so lean is constructive logic meaning it will not support things >> it supports classical mathematics >> what >> it supports classical mathematics >> you don't have to be constructive >> oh interesting so unlike unlike rock it actually has a separate type universe

for the propositions which allows propositions specifically to be constructive while allowing the rest of the types data types to be constructed. >> Okay. So is the calculus of constructions constructed? >> Yeah, as as the name indicates. Okay. Okay. Okay. >> But we can add in the this law of exclusive middle. So that >> uh it it's used a lot in math because mathematicians don't care about choice or about constructiveness. >> So we can always yeah just add it. In fact actually if you look at the printed aims you'll see it doesn't depend on extreme middle it actually depends on the aim of choice because in we construct the extreme middle from the choice using the

>> fascinating okay >> is that the same Japanese as >> no no this is a guy called >> I thought it would be a funny >> no but a significant number of Romanian legians are Yeah, definitely. uh but but this was a guy who did his PhD in Canada and then he published a single paper in which he published the which is very impactful and then he quit his PhD and there's apparently no trans he just published this one paper sounds like >> let's maybe

something like data whatever and they didn't wide because it was just an opinion PhD student not well known and then actually publication was impact a lot >> yeah it was gigantically >> but this was done later when I think people in Germany help >> oh okay I haven't heard this is interesting okay >> yeah find it at the end of >> I'd be very interested to see this yeah Yeah. Yeah. Okay. Interesting.

Interesting. But yeah, so this guy apparently >> Yeah. Sorry. >> Okay. So, so, so now I want to maybe get people's opinions. So, if we were to formalize the proximity price the statement, right, in lean uh using say, let me go back to the proximity gap uh here theory, right? If if say this is the way that I showed uh how we define it in lean, what is your thoughts? Like would you accept this as a valid statement of the theorem? What would make you gain more confidence that this is actually the right theorem that we

formalized? >> Would it be like where you put the else zero to change with the >> Mhm. >> Because I think like if you click on error >> Yeah. Yeah, where you show before right there you can plug where there's the >> this error. >> No, before you were you were going where there's like the unique decoding list decoding and then there was else return zero like this, right? >> Yes. Yes. >> So yeah, >> this is the definition of error bound. >> Exactly. Exactly. So no. >> So well I mean but okay ignoring what the errors are for now like >> Mhm.

>> Okay. So you would have to change the dot square root rate to just rate in the that part >> right >> this is the you know fine because we're going to capacity then you have like saying that so okay maybe as an okay so this is a theorem it's something that you can write as a story >> and seems good like for other things has been formalized how do people get can get confidence Okay, actually I'll tell you what there is a way you can get confidence that these are the right theorems and it is you use them to prove something >> so you go there you say like look I do a mock uh uh you know say in some check with the code folding for example

>> right >> I use this to prove it and if it allows me to prove this statement then it is the right theorem so >> this is for example like we had recently a paper on like UC security and well add one and run and another one and one the question like the finish the functionality that we're trying to achieve is it the right one right is a similar thing that what you have here because you have something that you want to achieve and you want to figure out what's the right one for them we like say like look there are some other well-known functionality that we care about in particular for example there is in the UC case there is a signatures can be made from proof system and UC secure signatures are very well known so we're like look run go and prove that you can

from your functionality of a proof system you can build the functionality of a signature. So to me that the way that you prove that this theorem is the right one for the conjecture is that you take like a you know either the old fry protocol I mean fried weighted so it's a little bit different >> you can do it with mutual as well >> yeah so if you if you do this kind of thing you know you have the protocol you have the code the protocol of the code so you have confidence that this is like the real thing that you're running and if you can prove security of that then I'm confident this is the right definition because you know From what I seem to understand like you know look then you know it would be great to prove equivalent with another F protocol but

uh you know if you show me the code and the code false thing that it should f and the verifier check what it should check >> then I and I can prove that this is secure then this is a good enough definition for me. So I think this you know this looks good >> if you if I want to get the full confidence is that I use it to prove something real. >> Maybe this is the the best way. What do you guys think? I think yeah, we should be able to do that. Yeah. >> Question. Since you mentioned the price before, is this the mutual correlated version?

>> No, this is just correlated. >> Yeah, it just that theorem states which is not the state boundar. >> No, but but the the the is accounted in error bound error bound gets delta and with delta computes. So >> is enforced to be non zero. uh well in computer zero will be infinity in this case I assume >> yeah but then the theorem is probably that would not hold I'm not sure how it treats one / zero in this case >> but you know you can prove that uh when delta >> is one >> yeah the error is a one or infinity >> okay >> yeah so it's a trivial statement in this

case but uh I I assume this is what you're doing right >> yeah yeah um so yeah I think the the boundary conditions are especially important and especially easy to uh misformalize. >> Yeah, >> we had a problem with this division by zero recently too, right? >> In the experiment. Yeah. >> Yeah. >> It turns out that one over Z is equal to one. I mean is equal to zero. Sorry. Obviously. So the functions have to be total. So they have to return values for everything within >> and so 0 to 0 is one.

>> Uh also yes I think so. Yeah. So and that but that meant that we had a sort of like one of these boundary issues on the village field where actually there was a condition that was meant to be unsatisfiable that actually satisfies >> is always satisfiable because of that one of their >> I mean there are like you know free art things in computer science which is boundary condition off by one it had some off by one errors as well. >> Sorry >> we've had some off by one errors as well. >> It's very discomforting though. So like every time you divide you need to just remember to check that the >> well no because I mean either either your theorem happens to hold when you're either you're going to prove your theorem and it happens to hold for the

case where whatever denominator zero right in which case you can just write it as this or it won't for that specific value in which case you need to have the extra condition that this the denominator is not equal to zero right but you're still going to get it wrong if you prove Is that if I'm making sense here? >> I don't know. >> Okay. But I'd say basically either it doesn't make sense for this extra value that you wouldn't have, right? Either your theorem is still true and then you can just prove it as is, or it isn't, in which case you're going to have to add this condition, >> but it doesn't mean what it it normally means.

>> It means what it means what it normally means everywhere else apart from this one value. Correct. >> Yeah. >> Okay. So, yeah. Yeah, that's your >> Okay. Yes. So, so what you said about like defining fry proving soundness depending on correlated agreements >> or even like simpler thing like liger you can prove with mutual or with CA you can you know >> just you know if if you prove more protocol of course I'm more confident but uh you know when a single one I think is a is a good target to go for >> similar statements right you have theorems like preserves this >> you could prove that >> absolutely >> and if correct defined and you'll be able to prove it

otherwise you won't. Yeah. >> So don't have to go through the whole thing. >> Yeah. But of course you know like you know >> you you have to do it eventually. >> Yeah. Eventually you will have to do it and this is where you get the full uh Yeah. >> Okay. Uh yeah. So let me go to the second part >> maybe a very stupid like once I prove a bounding like right. So I know all of this. Is it possible like for example say that I'm running my fry and I want to then get the parameters right for it. Is it possible to then like use this like spit out what the you know when I tell you K and N it will I can automatically compute all of this because it's all random. No, >> because um well if everything stays rational

then you can yeah as long as you have like a square root or anything that's a real number then you cannot because well >> I think >> real numbers have to be exact right when used in proof it has to have the exact semantics and so you can't just like run like square root of two when you run it on on a computer it sort of truncates somewhere >> so not in that blue so the uh ITF standard for flow floating points is extremely messy because they're not uniformly distributed. >> Yeah. See? >> Yeah. >> So you wish.

>> So there are ways you can like take a real number and then convert that into a floating point number like actually do the computations giving you some floatingoint numbers. Uh that is that requires work indeed. >> Yeah. Okay. >> To settle that >> requires work in general. So this is why actually if you try to a lot of differential privacy implementations back in the day were broken because they thought they were sampling real numbers but they were sampling floating points which are not the same. >> Yeah. Turns out. >> Yeah. Yeah. Okay. Okay. Because there would be something you know if you have the proven all that and then a way to like say like look >> this protocol with these parameters give you this bit of security and I can like really get extract them eventually you

know long term it might be nice >> but but you can prove like you can prove that if this is the real expression then this is like less than 2 to the minus 100. >> Yeah. >> Uh yeah >> good. >> Okay. I I mean alternatively we could also write a function that gives you a low bound to your bits of security with a proof error. >> Yeah. But as you said >> requires work. Yeah. Because you have to bound the floating points computations like it's always has to be a lower bound. >> Yeah.

>> It's possible. >> It is possible. >> Okay. >> Um All right. So let me go to just now coming to the uh interactive oracle reduction parts. Um so when so something that is like one or two page in the preliminary sections of a SN paper like when you define what is an IR right you think of it as you have some interactive protocol here you have some prover and here some verifier um they interact over a number of rounds and

The prover let's say knows the implicit sorry have this thing where x is the explicit instance. Y is an implicit instance. So maybe let me box this y for the verifier. This just mean the verifier only has oracle access to it and w is the witness. Right? Um okay. So, so this is the model of IRS that you'll see in papers. Um, but turning this into a uh like a definition in definitions in less and then writing that definitions in a way so that you can actually prove things about it is

pretty non-trivial. So, let me show what uh we have been here right now and which which is still not the the optimal definitions. Um but you can think of say when you start formalizing you have to make a lot of choices. So here's one choice. How do you um how do you define interaction? Do you define it so that it sort of alternates between prover and verifier? What about alternating between verifier and then prover and what if you just don't have anything at all? Right? I mean there are some definitions that also don't explicitly have a verifier

algorithm like they just say random challenges. >> Yeah. Yeah. Most Yeah. You can define Yeah. Everything here is like random >> verify is just the very last thing. >> Yes. Something here. >> Yeah. I I agree. Um so so the convention that I went with is that I do not enforce any sort of interle of messages. uh this is uh so that I could sort of break the protocol down into sort of more modular layers like even a single message from the prever or from the verifier could make for a meaningful Ir um

and also when you compose things often times the structure doesn't sort of continue and so you have to do like some padding rounds Let's say if you have like a sigma protocol, right? It's just free message. Uh if you enforce that the verifier must respond, then you just add a dummy message here and that's just like unnecessary complexity. Okay. What it does mean is that now if I just give you so here you have like a vector of the direction of the message and the type of these meshes.

You don't necessarily know that say all the challenges must be uh in even index and all the messages are from a prover in odd index like we we don't know that there's just like some definitions that we define on this where we just filter out based on the directions >> and it could send like three messages in a row and then every method in >> Exactly. Yeah. Exactly. Um and so >> sorry so could you say the direction of each message in the protocol? So the process just now a single small reduction like >> um so protocol still has many could have many messages >> but so there's only one direction you can send.

>> No. So direction here is a >> each of the messages >> each of the index. Okay. Um cool. The next thing uh we want to tackle is how do you define oracle access? >> Um, especially when you say the prover sends a message to the verifier as an oracle. >> So just we are not considering the graphic setting at all at the moment.

>> What do you mean holographic? when you have like an indexer. >> Uh no no indexer. Okay. Yeah. So does it even matter that we have access here because we are not trying to prove anything about the efficiency sort of >> oracle >> ignore that it's an oracle and just assume that this whole thing is >> you you cannot because then you cannot do the BCS transformations like you need the explicit information that something is an oracle for the for the compilation. to happen.

>> Sure. But wouldn't you say that message is always >> Oh. Um, >> like you need sometimes you have some additional message. >> Oh, so you want that. Okay. Because for those you don't want to send another tree for example response to the >> or what if you you specify a POP? How how do you Yeah. Yeah. >> So, so that's why you have to just yeah just basically don't make any sort of arbitrary restrictions and get things to be as general as possible. So for instance there's there I have a okay let me say what to do with

this. Okay. So this is now the how to encode oracle access to a message and uh >> I'm guessing you're using the same definition for the instance or like the instance. >> Yeah, the same same definitions. So there is a just an abstract type of oracle computations where you could have access to the uh sort of uh set of oracles. So let me scroll all the way to the verifier uh I guess oracle verifier here. Okay. So this is a verifier in an

IR where I assume that every message sent by the prover is wrapped in an oracle. So what this means here is that the prover actually sends the message but there is some wrapper around this verifier that prevents the verifier from seeing the whole message and instead establish some sort of Oracle interface where the verifier can query. Okay. And so that's why we have this uh oracle computation types where here you have the set of oracles

that are all of this. So this part corresponds to the the Y part the implicit instance and this part corresponds to all the messages in the protocols. Um and then this is some potential additional or articles that the V might have access to. Um so it takes in all the things that it can see in full and then it can query all the things that has query access to and then it returns the output statement.

Right? So you have here at the very end you output some x prime and y prime and this oracle comp is like an arbitrary function of the oracle which exist you know some of the oracles as a defender in the protocol and then they can do something >> yeah they can do something so yeah it's it's a monat where you can you can always make an oracle and then specify what you would do with the response of the oracle I think >> so is this like >> cursor I think. Yeah, cursor which is a VS code >> like VS code has >> somethingual virtual this Oracle

>> um >> not exactly >> what do you mean by virtual >> I think oracle access to fencing function h which is like >> okay yeah then you can define an oracle computations >> where you say here so like you can write do Let's let response which is uh like you query f at some point I don't know q q is a query >> and then you return uh r + 5 >> yeah okay

and yeah so that's just the x prime part at the verified outputs. The more difficult thing is how do you precisely define what this Y prime is. So >> this is after several rounds now. >> Yeah, say after some number of rounds the verifier needs to implicitly specify this Y prime. What would be the most sort of general way to do it? for for defining y prime >> sorry >> for defining y prime >> yeah like >> in general how how would you define this y prime like in an implicit manner where v like doesn't know y pool

>> I specify like a circuit that uh taking like the you know the oracle you know you give it like an an index in each of the oracle that you want to query and then you like kind of like evaluate function on the answer through this oracle at this query >> something like that like you know my y prime I find a domain this domain I find a mapping to the oracle that I do and then I kind of like apply a circle to it and then give me a value or something like that. >> Yeah. >> Uh yeah, that's that's basically the idea. >> Okay. >> Yeah. So you you have some Y prime with some associated Oracle interface and the verifier will um sort of gives an implementation of this of this uh Oracle interface based on all the all the other

all the oracles that it has seen so far. So sort of maybe it goes the other direction actually. Yeah. So it it says that uh later on if you want to query this y prime here's what you'll do. You'll uh you do some queries to all these oracles and you do some computations and then you return the result. Yeah. Okay.

>> Is there a difference in type between this Y prime output and the oracles during the message >> um >> during Yeah. during the execution. >> Mhm. So it can be arbitrary uh like as the as the people doing the specifications we can define what the Oracle interface looks like and so it doesn't have to be the same. Okay. Yeah. Question does do you need to split the explicit and implicit instance? Because you could also think of like the explicit instance being you know things of type that I can read directly and then I can have think which are oracle compositions and I can like simplify to a single one

>> right? So like it returns a tupole of x prime and >> yeah or return an x prime x prime may contain many explicit many many things. Some of them which are implicit defined some of them are explicitly defined. And then you know I don't do this explicit split between the two things like >> it still exists right you're still going to have a two things. So >> no sure but simplified like instead of like outputting three things like you know explicit implicit and weakness I just output two things and then I you know >> correct of your two things >> yeah one of them will contain it but I'm saying like you know but like >> you're still putting the same stuff.

>> Sure put in different boxes >> but I I think one macro. >> Yeah sure. Uh yeah. So that just means that instead of here you have uh like another product. >> Yeah. >> And then you specify ways to >> implement the output article. >> Yeah. I'm just asking because one of the new things I've been writing I found that if you like just for this distinction between explicit and explicit instance. So you just have like one instance which might contain something which depending on the transcript >> that turns out to kind of like simplify a lot of the definition that you have to do.

Okay. >> So, I just, you know, not sure the same Kier, but I wanted to to mention it. >> Yeah. Um, yeah, I think eventually we're just going to either split it. Yeah, it Yeah it's possible either way. >> Yeah. Just Yeah, just something to keep on your mind. >> Yeah. Yeah. >> I'm sure you have more a lot of things on your mind, right? But enough. >> Yeah. Thanks. Thanks. Um, okay. So that's just defining the the structure of the protocol. Uh next we can define just what it means to run the protocol.

So let's say you give this protocol some initial input xy and w. uh then you can just run it in the intuitive sense like you keep going uh step by step and in each step you can record the messages that were exchanged and then at the end you you uh output the transcript and everything and and the outputs of both parties. So this is something that you can just define sort of in an inductive manner. So let me go to say running uh is there.

Yeah. So so for instance this is for just a reduction with like no oracles whatsoever. Um the the oracle the IR version is is also similar. So you first just run the prover assuming this is in a public coin setting. So I'm assuming the verifier just returns random or it challenges and then you run the the final thing here that sort of uh do the reduction at the end and then you return both of these things. You return both the prover result and the output statement. Um and and that's yeah >> um >> yeah so you have a notion of what

messages are. Is there a notion of ordering messages? Uh yes. >> Where does that live? >> So it lives in this protocol specification where it is indexed by n. So this fin n is a type of zero to n minus one. And so if you have a function like fin n to type. >> Yeah. >> Then it gives you an indexing over the types. >> Yeah. Thanks. >> All right guys. So the messages themselves don't contain information about where they appear the protocol and it's the protocol that knows where messages are going to go.

>> Yeah. Yeah. >> Uh yes and then once you define uh how to run the protocol you can define sort of security definition. So you uh currently I define completeness and then a bunch of soundness notions. I have not defined zero knowledge yet. Uh yeah so in terms of the definitions it is written in terms of a this this game based notion where if you see on a paper you see something like probability of here's some condition right some condition and then here is the setup this is the

game >> and then you have like say at most some error >> but Can't you in like like just in the world induct you know without cryptography inductive or cohort can't you just do it dry without games I recall you can do this at least for some as round by round someless because it's just about a fraction of challenges and so on and doesn't just the existence of a positive answer in the next round as an oracle already guarantees you uh it holds for any strategy of the attacker and so on. Yeah, it's in that form, right? It's still >> if you whenever you write down a

probability, please first find what your probabistic experiment is, right? And then the events that you want to always have to what I mean is just doesn't need to refer to external algorithms that choose what they know. >> Sure. Sure. because in in in the information periodically we don't need to talk about efficient system unbounded. >> Yeah. So that's yeah that's basically the the format that uh we decided to go with and so if you look at say the definition here for knowledge sounders

it says that there exist an extractor a straight line extractor for now um such that for all segment and witness and any approver potentially malicious if we run this reduction that is composed of the prover and the corresponding verifier. Um then the so here's the condition. The conditions are that you run it with some input statement and witness and you return some output uh stuff. And so this is just like x1 say w1 is not in this first relation but x2

w2 is in the second relation. Right? This is the bad condition. G uh will be small given that you have the setup of the game here. So the the main setup is just you run the reduction with say logging all the Oracle queries. So this is uh helpful in the in a random Oracle world and um you also extract run the extractor to get the input witness.

>> So what does the extractor get? The extractor. Yeah, the extractor here gets the input statement, the so the input statement, the output witness, the transcripts and all the like um all the queries of the prim. >> So it gets but it gets the transcript gets >> it gets the transcript. >> Do you do normal sness as well? Uh yeah >> because uh so I was talking with there's in the definitions compared to the normal you probably did you talking with him already about this >> maybe not uh so there is you know okay in the setting it's very clear what soundness is y

>> soundness kind of like I say like you know I do this game and the thing doesn't go in the new relation >> yeah in with soundness there are like two different definition you can do >> so one of them is the uh one in which I let the malicious prover output a new witness. >> Yes. >> Or the other one is the one in which I ask that the thing is not in the the output of the malicious prover is not in the language of the relation. >> Oh of the verifier you mean like >> the output of the verifier is not in the language of the relation. >> So but there's no weakness given to the by the the malicious prover.

>> Yeah. >> So turns out >> you need the second one because when you compose >> Exactly. Exactly. You get this kind of problem with the soundless composition. So okay as long as you've already done it is great. Well, I have not fully done it. I am aware of the problem. >> Okay, good. >> But yeah, I >> good. Yeah, I just want to raise it before it was >> No, no, definitely. >> Yeah. >> Um, yeah. >> So, the the sounders definition that I currently write here is a little bit too strong like it's not exactly what you you said. It's Yeah, it just says that well because we don't care about the input witness and output witness. It can be like any type but that this is a little bit too strong in order for knowledge soundness to

imply soundness. >> I see. >> Yeah. >> Yeah. This sounds good. Yeah. It's kind of interesting because when you're like in the IUP setting, a lot of things are like extremely, you know, since you're listening to the empty relation, you're like >> everything is very clear, but when you have an IUR, you want to figure out how to complete the end of the protocol. Yeah. >> Then you start having like details in which the right definition is not immediately clear, which is very funny thing. >> Yeah. Like this is the same that happened with your knowledge like your knowledge like by the fact that you have the implicit instance like you know the IOP definition you could you could extend to many different ways and each one of them they give you like slightly

different composition not options. >> Yeah. Okay. Yeah. But >> we can talk more. >> Yeah. Yeah. >> Yeah. I I want to get the right definition in. >> Yeah. >> Okay. >> Uh cool. Uh yeah. And with maybe 30 minutes left, let me go to the fry spike. >> Sounds good. >> Um, >> just one one general thing. >> Yeah. uh at least I'm I'm not sure uh because when I was writing proofs uh for two white paper whatever uh these are all proofs of proximity in the following

sense that even you have a main statement to prove or main trace you have committed it's like even a bunch of committed functions of oracles >> there exists approximate selection a correlated approximate selection of polomials which satis with satisfy Yeah, sufficiently close collection of polinomials which satisfy this and that it's just enforced by a circuit. So I was completely fading away the logic actually of the circuit and what it's supposed to prove. Not fading away. I was >> pushing that >> to to a different thing because it helped me just easier to argue about uh to formulate soundness and to argue soundness.

>> Just keeping it as a black box. whatever the circuit means to express in terms of witness and input and output that's a different thing that can can be fully separated from the logic of the rest. >> Mhm. >> Uh I don't know if this input from me now makes any sense but uh >> I so we we we did read your recent papers uh pretty carefully. Um so you have like for soundness you have a bunch of these existentials that is like you is that right like for for fry or baso yeah one one of the protocols for instance you have like there exist some I don't know polomial >> which is approximate and satisfies this

>> right and that p you know encode encode p is close to the actual code word C something like that. Um and then and >> then the multi-digit representation would be forward. >> Yes. Yes. So because of this existential you can just fit into this IR framework by letting P >> that's why I'm asking >> either witness. So if you set P to be equal to the witness, then you have like this general from a relation into a language, right?

And this transformation exactly gives you this existential. >> Okay. Okay. >> Yeah. This kind of like my relation is kind of like >> so the relation is about the proximity. Yeah. Yeah. Yeah. Makes sense. >> Yeah. Yeah. So we're we're showing >> weakness is the proximity. >> Yes. Yes. >> Okay. So this this is a fry spike. Uh how thanks to Julian. >> Um do you want me to narrate it a bit? >> Yeah, if you want. Sorry. Cool. Um >> yeah. So uh essentially we obviously start with the parameters are we have a field f we have our two smooth subgroup D right. Um we have x which is used I

believe in the coset and when we have the coset sort of uh context is this is sort of like the value from which >> it's a shift value. >> Yeah exactly the shift value for the coain and then >> yeah and then it's x to the two essentially right is the future and we can look at the definitions in a second. Um then we have uh K which is a number of folding rounds because as where K is more than well K is a number of folding rounds because of course we can do both early stopping but also we can do more than even and odd uh splits in each folding round. We do we can do two to the Sing.

>> Yeah. So we have the folding degree. So we do two to the S split. So S equals one is a sort of normal one. Right. S has to be strictly positive. So S equals Z is not permitted. K is a number of folding rounds. So as I said we um what do you call it? Uh we do these k rounds and so it's a k * 2 to the s has to be less than n in particular. All right. Um and then d is the degree bound on the final polinomial that is returned in the case where we do early start. Right? So in the trivial cases can be different from round to round.

>> Uh no the s is fixed here. I would choose because I know from I mean the main reason why we use higher I call it higher reduction factor >> okay >> in around is is for group size optimizations and I recall from the to that they were choosing different steps yeah the happiness if you look at blocky two and probably it's also present in blocky three >> it's not present in block three is one Okay. But there was a script written by I think >> uh that that tried to find just by brute force

>> optimal configurations and it was not homogeneous. It was not like always use a reduction factor for >> yeah the reason why is because the first round you have base element. So my folding factor my folding factor is is S. I read to the S element from the initial nor tree. So at the start if I'm reading to the s field element base field elements it's better reading to the s extension field elements because these are smaller. So usually >> I don't think it was just process. >> No these are the process anyway for >> you also reduce how much you commit to I think if you like do do larger than two.

>> Exactly. Yeah. Yeah. So you usually at the start you want to use a larger folding factor and then later on you use the smaller ones. So there's a lot of benefits on that. >> Yeah. The other the other big thing is that we don't you don't always go down. >> No, but like if you want to return a file that isn't constant. >> Yeah. Yeah. So yeah, there we allow that's what the D is for, right? Which is a restriction on the degree of the final, >> right? So so we already have Okay. Yeah. So that's an important generalization with Google >> D that D you can actually could actually derive, right? So it's it's not really needed for the last because if you know >> what's the degree of the top polom you know >> yeah yeah that's true that's true actually yeah um

>> I would yeah I I have like a list of the parameter that I for the calculator which I have I'm just going to double check with the min go ahead >> okay yeah I I do want to mention we can't just support this variable 40° because we are defining a single round >> oh yeah fair No, no, no. But but then the top level construction. >> Yes, that that will need to change. >> So that will need to change. Yes. See that one? That one. Yeah. >> So right now this file, right? >> Yeah. This file which is like >> 2009. >> Yeah. This is devoted to just the like breakdown of of the single rounds. And I guess you're also not missing the grinding for the moment.

>> Yes, we don't have the grinding. >> We don't have grinding. >> Yeah. Uh >> okay. And uh which one code or is it specified which code you're using? >> Um I mean it's it's unique once you specify the domain and the degree. >> Okay, good. So that one gives you everything. Okay, good. >> But then I would rather choose the D as the input degree. No, I just just say >> uh yeah, >> seems to be more natural. But I don't >> Yeah, we can we can make the variables more descriptive. >> Yeah. Um yeah. And then finally we have this uh size condition maybe you can scroll down a tiny bit which relates ds and k right so we have two to the 2 to the k + 1 * s all times d must be small

right and then we have an i which is just the index of the common ground number um yeah cool so I think I think that that's everything on that then we have you know there's maybe we can scroll down to the the first prover or maybe you have some more things you want to add. >> Uh no no that that's it. So >> okay no yeah let's do this. Um >> okay so in terms of if you think about what does the round do the verifier is going to send a challenge brewer is going to send the folded uh oracle right for the code word as an oracle. Um and so at this point uh you should think like what has what should be in the statement like the explicit and implicit

instance the explicit one which is the statement there which is just like the challenges that we've seen so far. Um the the implicit instance here we have to sort of uh append all of the code words so far. So f0, f_sub_1, dot dot all have to be in the oracles. Um, and that is because at the end we have some correlated queries. Although yeah, I think there might be a way to to not have this if we have this very very general simulation semantics.

>> Yeah, >> but that's that's another point >> some future. >> Okay. Um, cool. And so the witness here is not trivial. it is the polomial itself. So at the ice folding the polomial has also been folded and so it's degree bound. So here it just means the polomial uh un variant of this uh smaller given degree the degree is almost this much just some custom notation.

>> Is it unique? Do we know that it's unique? No. Uh, it's not right. There might be like list coding there might be many by the time you get to the like five. >> Yeah, potentially. Yeah. >> Um, cool. And so I believe the relation uh should state well this is the part that we're not clear on like what is the relation? >> Yeah. the the input and output of this given our setup here which I think is reasonable.

>> Yeah. >> Sorry. >> That's quite difficult in project. you need to take into account uh at least the way how the proof is written and I suppose that's going to be formalized in in the same way is >> it's a relation >> on or it's a statement to because uh I'm quite sloppy with my logic notation it's statement on the anti collected the history of of >> yes yes exactly And uh yeah so so it's essentially if you look I can send I don't know do

do you have this the copy of the current two bit >> um I don't copy it's not that publicly but I shared it already here and there >> because I say for one reason because up to that writing that paper I was even always when it cames down to these consistency measures. Uh I was like ah it's pain in the leg I just write this I'm sick of this proof and this two white papers the first time but I did it in more in greater depth >> like defining being getting clarity about what does consistency measure mean not just wrpping it in a single sentence >> what does it mean is like uh given

it's actually related that's also quite advertised in in hard track of work >> that consistency checking cuz now it's like typically because it's faster to implement and think that way. It's like now we have the folded oracles. Now we would start querying. >> Mhm. >> How do we sample? And typically now it's it's presented like this. You sample a random X from the top top domain and then look at its question trace on >> the small domains and and use these values and they're missing minus values to check colinearity. Whereas the initial fry paper as well as other work they actually go they argue that the

random the sampling of of the query >> goes bottom up. You sample first on the smallest domain. >> Oh >> check >> no I think >> you have to sample which brush you >> I'm not I'm not I'm not I'm not finished. Okay. So it's it's it's now a stocastic process. Instead of just a single sampling, >> Mhm. >> you do the several samples as follows. >> Mhm. >> You start with the most recent oracle. You sample a random point on the over the current smallest domain. You check colinearity.

That means you require two openings along the fiber of the uh of the previous oracle. Right? uh and then you decide now and this is stoastic gaming process which of the two I want to have proven that they're consistent leader and so let's so one half one half to choose one point along the fiber of the projection and then you do it the same again you know they choose then again a co and the thing is this thinking in that way it gives the same distribution as sampling on of the main uniformly and then doing the thing as often nowadays described. But it helps a lot in

understanding uh the this consistency measure. But this tells you precisely if you sample and this is like it's probabilistic process what is what is the success probability to succeed everything. So that's the average >> success the average consistency the average success probability in all polinarity checks when you sample fiber wise from bottom up that you succeed in all the checks. >> Right. Right. >> And and these are the measures which are crucial for uh for for the whole fry proof to keep track of the consistency.

So everything looking from the smallest current domain from this lens instead from the top domain. >> I agree with you and that's the proof like prove that it works the verifier makes an observation at the bottom and it works as well >> but the sampling happens at the top. It's also turned practically down but it's equivalent >> equivalent >> but it helps in the proof to understand the motion and that's that's how also the the next the next reduction step is actually uses the weighted corated by the >> with these consistency weights is that to keep record of of the previous quality of consistency in some sense. So if you do mutual product mean you can

avoid all this weight of stuff and the tree traversal is a lot easier like a lot >> okay >> if you had already moved >> yeah correct >> I'm not surprised to hear that because at some point >> yeah hopefully this >> that's interesting either so that it helps so much that you >> yeah so I guess maybe that like maybe posted one week or two and then it could be helpful for the for the >> Yeah. And it also like payment of the MCA for the injection >> right >> yeah we would need yeah the mutual >> but given uh the possibility

let's say even though I don't believe you know say somebody proves up to capacity but proves not mutual >> wouldn't be wiser currently at least have two versions the one that keeps with the more technical consistency measures and the one that is greatly simplified thanks to if correlated MCA would have >> the point the point is that this analysis is much simpler and therefore probably easier to formalize >> we we probably don't have time to formalize two proofs >> um so we we would like to stick with the one that's simpler >> okay >> question can you like in this case like if I instead of working through the fold I work with inter of course so like I

start like with my I start you I start with Solomon code. I do the interle now, but I don't change codes like cuz it's kind of like there is some weird code switching going on, right? But >> yeah, like RS codes allow you to code switch >> without Exactly. >> How are they built, right? Like >> Yeah. Yeah. But I'm saying like if I do your analysis and I start using always the same code, but I guess it doesn't really work. You have to use Solomon really for for a fry version. You cannot really Yeah. do that. But how does how does it simplify?

>> It simplifies that. So >> guys, we should we should focus on >> I think that's that's the last thing we can >> uh yeah let me just go to the the general protocol. So this is we specify a single round >> uh including the last round which is different because Yeah, >> the the prover would just send the final polomial. So like the folded polomial and then verify >> not encoded.

>> Uh I think >> oh no it actually just sends the raw pol. >> Can you can you include it as part of like the the the fry step? You don't think of it as a trivial? >> Mhm. No, I'm just asking like are you like sending it at the end as part of the fry or are you thinking of the trivial opportunity where I just send the witness? >> Um >> no no it's it does the folding step and then it returns the polyf. >> Okay. So you don't just do the folding and then you like stop and compose with can we show the implementation very quickly?

>> We we can further u >> modularize to make it the trivial ones. >> Yeah. uh probably makes proving simpler >> might be easier because then you have single route that's always the same final round. >> So yeah, >> cool. >> So So it sends the witness at this point. >> Yeah. >> Right. And the verifier is going to send back or well it's going to sample but it also sends back the prover all the challenges uh that it's going to query.

Yeah. And and that's that's that. And then you just slap all these together to to form the the whole fire oracle. >> Yeah. which yeah uh we just have a function that does the composition >> and you can run this thing. >> Uh not right now. >> So we need to plug in uh the one thing is not computable here is the polomials >> because the polomials in master were non-computable but we have computable polomials which can show an isomeorphism with the non-computable ones up to evaluation once we plug them in everything. Okay. Yeah. Good.

>> So Uh so for instance this is what for all the folding round. >> Yeah. >> Right. And then later on you have this overall reduction that is you append the folding reduction with the query round reductions and that's the whole protocol. >> Very nice. Easy peasy. Only took me like two months. Amazing. >> Yeah. This like feels like magic.

>> Yeah. Yeah. >> Yeah. So, we've got war is coming next. >> And then you have a subject as well. >> Do you do you consider first doing base on? >> No, we're just doing >> Well, no. I I do have someone doing binary base hold. >> Yes, that's true. Yeah. Yeah. >> Oh, yeah. >> Is it is ch on base or >> binary binary? question with the where are you doing the read Solomon version or the interle code version >> right now it's read Solomon but we could change it like so I mean where the America the state of war is we had some preliminary work done on formalizing a lot of the leas and serum statements we haven't started on the construction there are probably a few more minor changes needed on the serum statements as well I think in particular folding we

need to change >> because the the nice thing about working with interle code is that then you don't need a different setting for the binary case. >> Yeah, >> because you can just think of like interle of binary thing. The folding does not need to divide and so this kind of simplified a lot of the analysis >> at no real like uh you know >> and no at no real cost. So >> and it's quite nice because you can do it you know >> you can do it for any linear code with no problem and nice you know the only you know for any code the verifier will not be efficient but the rest of the things will work out. So actually so I mean we did discuss this a while back in terms of did we want to formulate it in a kind of code agnostic way and then I

think we ended up settling on doing it with Reed Solomon but I'd be quite open to revisiting that. I think we just need we we were >> I don't think you would be huge instruction when we were discussing this. >> So if you >> I have a very good one I can give you were in three lines. >> Yeah. >> It sounds good. >> If you want but >> so actually the other question is obviously because we've already been following the world paper but obviously since then there have been a lot of changes and so it' be good to get an update like a linear for work. Yeah.

>> For any code with very simple everything. >> Okay. So, okay. What's my relation? My relation is something that I have to I like this thing more. I don't like writing on paper. I'm going to suppose that I give you like a simple relation. I'm going to call it RC which is like uh my instance going to be a vector and a value. Yes s this will be like some fat and my condition will be the f >> by the way if you want anyone else in the room to be able to read this writing you read it's probably not

>> I don't know you like just as a thought >> we can >> yeah yeah maybe I'm done with the presentation >> okay this is yours >> anyone I think this >> I think in the Yeah. >> Okay. So, I'm going to give you giving you two construction. They're both really simple and together they give war with actually better parameter than in the warp paper.

>> Okay. Okay. >> That sounds pretty good. >> If you give us that proximity generator paper, then then we're very happy. >> So, we have this. >> Okay. Yeah, I think we're allowed to eat. >> People have been eating them. >> I have no idea. >> Okay. I hope we haven't. >> No, no, I mean they've been here all day right? >> Okay. So, this is what I I'm going to uh the relation which I'm going to decide.

What is this? This is like linearly constraint codes. >> Yeah. Okay. And you can do for other things. You can do for more complex constraint. But linear constraint is good enough for what I want. >> So I'm gonna need two building blocks. Uh so the first one is going to be a very simple linear IUR. So I have a prover and I'm going to apply it on sorry on R C to the K. Mhm. >> Right. This is fine. Uh so prover maybe with the three lines I was overselling myself. This is already >> well you had two already streak cuz actually that one is a bit low.

>> Okay. So what the prover all the things over here. So x y and w the gets x and y. >> Good enough. >> Okay. So I'm going first. So there is an IUR you can describe which is just the IUR and this is an IUR from R C to the K to RC and this is just some check and this is I'm thinking >> exactly S check with folding. Uh this is basically the first step of work in I

can uh I can also write basically you think of like a subject of the form uh weight. >> Is this part of the zigzag thing? >> Yes. Okay. >> Yes. So I thinking of something like a subject of this form and whenever like I kind of like fold I also induce a fold on the thing and then you use MCA to prove this. So this is like general sum check for quotes I call it because it's a sum check for anything which I have of this form. >> Okay. So you have this check. You're going to have to formalize it anyway. So this you already have.

>> So I'm going to send you this is an IUR. So at the end this outputs an XAR a Y star and a W star. You know for context is the Y star is the folding of this the W star is the folding of S and that star is like holding of this thing like some new value but kind of I'm just going to send you as a as a linear oracle I send you star then the linear oracle. So I have not to think about how to remain sample because it's

a real oracle. Yeah, >> I'm just one of the domain and then I'm going to just simply like uh so many >> this one. >> That's good. >> Yeah, >> it's purple. Well, I I >> It's fine. I got my own confident for now. I saw them at PFL two years ago.

>> Very good. >> Okay. And now what I'm basically doing is that like I'm, you know, my inter code word. I folded it by this. So this will give me some values. So this I get like a bunch of claims. So the claim what claim do I have? Well, I have the claim of this relation. So this is a claim that uh I'll just write them here sum of uh sarness.

So actually the w I'm going to just write them out. This is a f star and this is f starance. >> So this is just f up star and v star is equal to sigma star. This is the first claim. >> And now this claim what do they tell me? Well, they tell me that when I have when I have fxar >> and I encode them with a code c agrees with the with y star at the position y. So rewriting this means that for all i in t

I get that code of s star at position at size is equal to s star >> right this is just saying that when I encode and I check I get the same value as the code for this is the spot checks or the in domain samples And this is if and only if this is the same as like saying like look general coding of the matrix time f* star at at x i is equal to f x >> these are linear constraints as well

these are exactly linear constraints. So I'm going to just sample some randomness epsilon and I'm going to check this is the claim that sum of you know epsilon i times uh this constraint uh so this going to be I write a fun check just because it's prettier but this is like gi time uh time f at b and is equal to the the sum of the other things. You also want this claim

inside there. You're just bashing all the claims together with the same randomness. >> Or you can be some other you can use any zeroator here is is fine. So this is a so this is a reduction. What's the soundness? Well, the soundness of this is kind of like the sound of sound check. So this is like the soundness of subject. So this is where MCA comes in plus one minus delta to the t for the delta that speaks out by subject plus uh in this case like t + 1 / f

because this is kind of like the error of this batching step. >> Yes. Yeah. Yeah. This is this is all round. I'm just doing sound for explicitly, but this is rar. Yeah. Okay. This is a linear >> of course. Now I want to compile it to we have another one. >> So this is nice. >> So now what I'm going to do there is this very look at this signature.

>> Yeah. Okay fine. >> I just found a random tissue in my pocket. Okay, it's fine. >> It's done now. >> It's fine. >> You have to work production. So, >> so there's so I give you like a a one round linear IR with a single query. So, what you think? Okay, I send you like an oracle. Maybe I have other messages, but I'm going to send you one linear oracle. The verifier sends some randomness and then he makes one query. I can very easily translate this into an IUR. So this is

like a a linear IR. I'm going to say this is from like R to R prime. I can turn this into a a point query I from R to R prime time RC for any code that I want so for any code that I want it doesn't even need to be that code for any code I can do this what's the transformation well say this value was called coincidentally we So the confirmation is that I just send you as an oracle uh the recording of

the verifier does an outain sample. So I'm going to call this the out sample and then I give you the answer. >> Oh yeah you can also do more than one you can do more than one but think of like a single one for simplicity and then you know what are my constraint? Well, the automain sample will kind of like tell me that sum of f times I don't know say that it was a multilinear automain sample. You can do different one you have x that is equal to y and then you have the constraint on this query. So you like sum of like equal to some

answer. If you want, you also batch them like you can also do like a a single round of batching over here. And yeah, this is a this is just you know you have whatever the verifier would output for the first thing like this. And now what do you do? Okay, so I have like a linear IO a linear IOP for for our case. Then I combine it by this transformation to a to a point query IUR from RC to the K uh to R C prime for any code prime that I

like and then I just I can just take any other one and I just apply this to I compose it with this IR right the inductive step and until I go to the trivial IOP which is the where I just send the witness. So with these two things, basically you can do war with every code by just this. So and I think it's relatively simple because this compiler does very little amount of batching. You don't have to do much. It just kind of like you just do the main sample. You can use also the you know in in warp.

>> So what if we don't have this out of domain samples? >> So you can do it also when you don't have the auto domain sample. the the kind of issue is that basically okay so what's the error the round errors of this thing well so here you have like kind of like the the error of auto domain is the source term then okay here is where I would get like the randomness of the linear IOP so this route here will kind of like the math of the error of the linear IOP and the and the batching error which I

haven't bounded too well but I think is either like it's probably like list size over F >> depending on what derivator you use and you see that this part here does not depend on the list size this I get exactly the the error of the linear IOP so in particular this part here which is my error of the linear IOP will not depend on the list If I don't do that on my sample and I'm working in list decoding then this error will become multiply by list size which means that my number of queries becomes a >> So that's why I do the main sample here.

>> Yeah. >> Um the other thing is this is like a completeness relation like if things are good right? >> Yeah. >> What about the sound? >> Yeah. >> Yeah. Yeah. Absolutely. like the sound you get like this of a proimity relation. So like the delta of like f from this relation would be kind of large. The soundness of this subject I can give you the proof is not uh is basically if you look at the state or yeah the rumbaround soundness proof of work the initial step is exactly this thing >> and you'll see that it doesn't really use the fact that we're using with Solomon codes. It just uses the you know you so for sound to do this I just

literally need a bound on the side of the code for this error >> and a bound of the mutual creator agreement for the subject partner >> and completely how we can change this relation to make sense. Yeah, I think that what I did was just like uh make sure you add like some some distance between the F and the C of that hat. >> Yeah. >> Right. >> Do you still have the second position like Exactly.

>> Yes. Because this is about the the weakness. >> Okay. >> Yeah. So you want like you want the condition exactly. you want some kind of proximity. But in general like what what you want to say kind of like you know this is like your implicit instance that there like you want to say like for anything >> there's it will not satisfy the constraints. >> It will not >> satisfy this constraint in the soundest case. >> Uh sure sure >> exactly. So this is kind of like >> so yeah for for now let's say so that you also have hat >> exactly >> okay perfect in the other room

>> perfect so I'm saying like for all u in the list of fat delta u v is different than is kind of like a sound that I that I that I get this is what I want to model in the in the in the sound case. >> Yeah. And it is relatively clean. It works for any code you you know if you want to do your knowledge I just put here a knowledge subject so it just works it doesn't really matter because like

you know I'm in an opportunity thing I'm in opportunity thing so I can query the input >> and quering the input is is for free like it doesn't really you know if I Like if I even for IOB if I have like the definition of um of the knowledge kind of like you know the views of prover on x y and w the honesty will be distinguishable from the simulator which also get access to y.

So like for like in this particular reduction like this will query you know this this uh f prime is the fold of the original f >> so I can query it for free. >> So >> and these values here to get like you know once I query I know them so it's it's fine. Um, so the video consists of the >> Yeah, like yeah, if you want I can show you like the let me get my laptop. I'll show you the the definition of the knowledge for IURS because it might be useful.

>> So maybe before that so let's say we have this RC that is that also has the proximity parameter. >> Yeah. >> Right. Then knowledge it's like >> yes >> you have uh this I you have the input you have the output relation >> um >> and so they have some some different proximity parameters right and then the error this delta here will be dependent on those two parameters according to these proximity >> exactly yeah like basically this will depend on which parame that you give them and there will be an added there.