Mina Protocol Mina Community Videos, 17 Mar 2019

Previous Meeting Next Meeting

⏯

youtube image

►

From YouTube: MIT Bitcoin Expo 2019 - A Guided Tour Through the World of Snarks

Description

Rebekah Mercer (Protocol Researcher, Coda Protocol, O(1) Labs) guiding us through the constant size blockchains, zero knowledge protocols, and all things snarky at the 2019 MIT Bitcoin Expo

A

Alright, thanks again David. So next up is Rebecca Mercer. She is a protocol researcher on the coda protocol and she'll, be helping us learn pretty in detail about the world of snarks. So let's, please give a warm welcome to Rebecca.

B

Ok, so everyone can hear yes cool great, so moving on from the talk about like the social side of why we shouldn't trust, Schnucks, I'm gonna, explain to you why stocks work and why this like whole trust it's have come from and how this fits into the rest of how stocks work.

B

So how do I go great, so stocks like notoriously complicated and zero knowledge, roofs in general were discovered in 1987 and the New York Times made this nice article about them, and ever since 1987 we've been trying continually to make them like smaller and faster and be able to prove more things with them.

B

And it's been, you know pretty difficult, so Z cash read is article like what is zk stocks who knows, and then this guy comments on this blog post about zeroes proofs, like I'm, just struggling a bit with this time, machine, thought, experiment and then like metallic, just his heroic set of blog posts trying to describe like would see case knocks off. So this is all great, but you know even metallics have trigger warnings because it's knocks all complicated so right. So the question is like: how do we understand ZK stocks?

B

Do we need to know about elliptic curves? Do we need to know about pairings? Do we need to know what snarks are we forgot and then the next question is like what is all on CS? What is AQAP, what is PCP and what is an IP, because there's this diagram that Vitalik uses and the Z cache people use- and it has all of these acronyms in and the seven stages and every one of these stages is like.

B

If you don't know any one of the stages, then looking at seven things, which you don't know any of them, it's like extremely intimidating. So the point of this talk is like we I will show you all of these. Like seven things. Look like this kind of it's not constriction colors this nice story. But obviously, if you look at the papers which introduced these things, you don't see a story. You just see pages of notation and it's like kind of I mean even for me it's kind of intimidating, but it doesn't have to be so.

B

First of all like we. What do we want to know so? The two questions which I'm going to answer a pretty much like? What do we want to achieve in terms of properties from uh zero knowledge proof, and then how can we achieve those so, notably missing from this side, is like? Why do we want zero knowledge proof, and this is for two reasons.

B

One is like there's a lot of motivation talks out there and, like maybe you have your own ideas and then the other one is like I think it would be cool if people came up with like more and more use cases of stocks, I don't think they need to be use.

B

Just in this, like one specific place of like private private cryptocurrencies, like zero knowledge, proof in general can be used for a variety of applications, and this is one of the things that makes them complicated to talk about, because a lot of the work is in making statements that you care about into statements that you can prove things efficiently about.

B

So you kind of understand that, like if I had a proof of the Riemann hypothesis or something then taking this proof, which would be like lines of writing and proving it in a cryptographic way like this, even getting to a point where you can prove things about it even before you even prove them is complicated right. We don't live in a world where we speak in polynomials, for example, so I'm introducing my proven verify ax right. So the situation of zero knowledge proof is bez approver, who wants to prove something to a verifier and write.

B

The prover has some secret information that they don't want to reveal to the verifier, and this is what the zero knowledge pot of zero knowledge proof saw, and then there are a bunch of other properties that we want from this proof system too, but pretty much. There's like a statement, that's known to both prove that and verify ax, and then the prover has some. It's called a witness that satisfies the statement, so the statement could be like I know: X such that X plus equals 8, and then the prover could know the number 3.

B

So, like 3 plus 5 equals 8 and they could prove this, but without telling the verifier that the answer is 3, so right so properties we want to achieve. In more words, the first property is called completeness, and this is that if the prover knows the answer to this question or has a witness for this statement, the verify will accept that the proof who knows the answer. So if you, if you're proving a true thing, then the verifier accepts the proof it's like good, then the next thing is like.

B

If the proof that does not know the answer and tries to make a proof anyway, then the verifier is not convinced that the proof does answer, which means like, if you're trying to prove, if you're trying to lie the verify will catch you, and this is called soundness and the reason why it has so many stars is because there's like a lot of different flavors of soundness, which we'll get to one in like the next slide, the then property number three is the malicious verify learns nothing other than whether or not the proven knows answer, and this is zero knowledge.

B

Miss so they just learn the bit: they just learn like either they know or they don't. Oh, these are all right, but then so then in Zee case, not specifically, we have these other, so z case not like taking one step backwards. It's ten to the zero knowledge which, which is the last property we just saw succinctness.

B

So the proof is constant size like would, however, complicated the statement that you're proving things about is the actual proof itself is constant size. So this is like 6 inked. Then the N in z case mark stands for non-interactive, which means you don't want. This prove air and verify actually to have to talk to each other, so the prover can just send the thing, so she can like make it by yourself and send it, and then anyone can verify.

B

So this is how we can, for example, use the case notes for Z cache because, like you, don't have to interact with every person using Z cache to be able to verify the proofs yourself right. You just see these big blobs on the blockchain and then you can in some way verify them yeah and then the Oh in snark means argument of knowledge.

B

So the argument fit captures like this soundness of, like you can't fake yeah, you can't convincingly fake something and then of knowledge means that you, you actually have the knowledge, so in the X plus five equals eight example. The proof actually knows the number three. They don't just know that, like maybe some X exists which satisfies this problem, the prove it really knows three right, Clark, even out of knowledge, oh great, so here's a proof room verifier again. So here is the.

B

So here's the first four things in this diagram, so the alternative title of this talk was like how I learned to stop worrying and good love. This diagram- and this is the diagram that talk, uses and ZK smart people use and the this is the first four blocks in the diagram, and this is kind of the encoding thing. So what you do is you take a computation and then you form an algebraic circuit.

B

Then all 1cs means rank one constraint system and QA p means quadratic, arithmetic program, and so the next four things we're going to talk about. Are these these four things great so algebraic socket? This looks like this, these squiggles on line multiplications, and so what this algebraic socket would look like. So we have some computation in this case. Specifically, the computation is x1 times x2 times x3 these squiggles mean times very good draw and we are proving we know. X1 x2 and x3 equals some Y, and this Y right is so this is so.

B

The function would just be like X 1, X 2 X 3 equals y as an algebraic. So, okay, it looks like this. So in algebraic circuits, each of the multiplication gates have two input wires and right. One output wire right. So this is this computation written out for you and then what we need to do to turn this into a rank.

B

1 constraint system is like we need to flatten it so now, every equation that we have can only have like two, no elements multiplied together at most, and this is pretty much essential for the way that snarks work and at the moment and they're like the world. We live in like the tools that we have make it so you just you can just times together two unknowns at a time.

B

So in this case we have like this: u, which is an intermediate variable, equals x1 times x2, and then we label this Y ax, that's coming out with that multiplication gate. You do you see how that makes sense, and then the next thing that we do is we times together the third unknown input which is x3 with this? U and we get the output. So each of these is just multiple just you in like one multiplication, there's never like announcing times on anything times and don't think it's only two at a time, then.

B

The other interesting thing is like. If there's an addition gate, then you know: if this addition gate, then you kind of just incorporate this into one of the multiplications. So if this bottom wire instead was like X plus three, then you could just do you and then like in brackets, X plus three. You wouldn't need an additional gate to do an addition. You get them for free. So what does it rank on constraint system?

B

Look like so a rank one constraint system is we put these like flattened versions of these equations into vectors, and so we have these three vectors, and then we have a solution vector. So these dots mean like inner product, which means you have two vectors of the same length. You multiply together the entries that are in like the corresponding slots and then add them all up, we'll get to them, and so what this SI x, SB minus SC is proving. Is that the two input wires in each case?

B

That's the thing they should do. The two input lies in each case, equal the output. So you would have like if we had a as like the upper wire in each case and B is a little lower wire in each case, then C is the output wire in each case, and so this checks one at a time that the gates are consistent.

B

Interesting, oh cool gonna, be shorter than it was right. So.

B

So yeah, so the next thing that we do is we take. So what you do is you make these into these vectors and then, as I just said, with this equation, you have the, for example, the upper input times the lower input equals to the output for each gate. So this means that if you want to then go ahead and check the the entire circuit is consistent. Each of this this equation checks that one gay is consistent.

B

So if you want to check the entire circuit, it's consistent, then what you need to do is you have one of these checks for every single gate? So what you do instead of this?

B

Is you instead make them into polynomials, and this is a little bit tricky to explain without pictures, but instead of having like this gate, represented, and then this next game represented, you instead put these vectors and you take the corresponding entries from each vector like so, for example, you take all of the vectors which represent an apple wire with these, like two inputs equals output. So this guy and then this guy yeah the up wires and you make them into a polynomial.

B

Then you take all of the people who represent all of the inputs that represent a lower wire and you make those into a polynomial, and then you take all of the outputs, so the C's and you make them into a polynomial and then what you can do is evaluate this polynomial at a point, and so what this allows you to do, which is kind of confusing to follow with absolutely no pictures is it allows you to instead of having this one check gate but I respect a gate. You have one check.

B

You just have one check: that's cool right yeah, so you can check the whole entire system of equations as consistent with just one check. Instead of like one package, which is huge- and this is called a quadratic arithmetic program and the there's, this cool result- and it says the quadratic arithmetic programs are like a very good thing to prove snarks about I mean to create snarks about that's pretty much what it says so right.

B

So, in our case, the polynomial would only be degree 1, because we only have these two gates, but if you have a lot of gates, then this is really a huge Sabin going from like verifying every single gate to verifying one extremely huge um right cool but you're like what? What does this do? What are we doing?

B

What does any of this, um and this leads us on to the last three things which are in this huge diagram which people use to explain stocks, and this is where all the cool stuff comes in so so far, what we've done is just encoded like a function into a form that it's easy to prove snarks well and like this is where then the I mean the bulk of the cool results are um so PC peas, so a piece of hay, beads, probabilistically, checkable proof, and what the PCP theorem says, which is like I mean mind-blowing to me, is that, if any MP statement, which means any statement that we can like verify efficiently like we can verify efficiently on this world that we live in.

B

Any statement like this can be read from in a constant number of places to produce a proof with constant soundness era.

B

So right, so this is kind of tricky because you read from a proof, like my proof of like a mathematical theorem, you read from this proof in a constant number of places to make it constant size proof which then has constant sound Nocera, but then, and then there's this great result that says this. Can we made zero knowledge with small overhead, which means from pretty much from the PCP theorem, and this is like follow o'clock? We have that you can make constant size, zero knowledge proof for any statement.

B

This is I mean this is I'm well changing. So what all PCP is so a PCP? Is you write take from points originally from you take different points in the proof and you just like read these points, and then you have like this convincing proof, but this proof has constant soundness. Era right and we actually in the world, won in like the cryptography world, one extremely small soundness era. So this could be anything under 1/2. Pretty much could count as your constant.

B

It could be like some constant fraction, but we don't want to be convinced of a fake proof, some constant, a 12 times. That would be terrible.

B

So what we need to do is repeat this PCP theorem- and this is one of the next two slots in the diagram come from because, like what does it mean to repeat repeat this right, so there's two different ways in which people repeat and the first way is called linear pcps and what this means is instead of the original PCP theorem, which in which you take like you sample from a number of points in the proof, this one, you sample, linear combinations of the proof. So what it?

B

What it seems like is someone is sending you a number of queries instead of whether they would originally have sent you one query, and then you from this one proof take the results of all of those queries on in your proof and send them all of the answers to that. Just on this one proof- and this is a linear PCP, which is the next step in the seven stages, to a snog right and then right. So this is what it would look like if you had a proven verify.

B

He said it's like a different amount of queries and then the proof samples all of these queries from the same proof and like some of them overlap, but this is completely fine, then another way to think about. Oh right, then another way the next square is like linear, interactive proofs. So another way to think about how we go from like this constant soundness era to negligible soundness, are a different way of like how we repeat the pzv process. Is that you?

B

Instead, you have this relaxation that allows you to use rounds, and so the verifier improver in this case interact a number of times, as you can see, and each time they the verifier in this case sounds like a point query and then the proof of samples from these points of like one proof, sends it back the verify cents more points, the proof it creates another proof right, and so what I think happens in in practices? Is these a used in combination?

B

So this is a linear, interactive proof and the other one was linear pcps and together they create right what is used in practice, so right so the way that the snarks, the history of stocks, pretty much is that instead of having these polynomials that we met earlier instead of having these polynomials transmitted with the answers like if, instead of evaluating them on points which you know the point of, and instead of communicating these queries and answers in the clear this all has to be done in some way.

B

That is zero knowledge, but so the verifier can still can still verify. So this is.

B

Sorry, these are the old slides.

B

Okay, so the way that this happens was introduced in grass hen in two different forms, so grass, tenth grass ten introduced two different forms of a proof. One of them was designated verifier and one was right. One was publicly verifiable, which is the type foot. For example. You soon see cash or used in like most purposes. I think that you would that you would think of for stocks to be used today so but the designated verifier example, it's kind of good to you so the as like an as education.

B

So what happens is what happens if we could send the queries instead of just sending the queries and then having the proof, sent back? What happens if we could send the queries encrypted right? So in growth? Ten in the designate of verify a case, the verify would have a key. He would encrypt his queries, then he would send them to the prover prove Oh would be able to create the results of these queries and have proofs, because these are just linear combinations of the points of the proof.

B

This is something that you can actually do with encryption with, like some sorts of encryptions that we have. So this is using the tools that are available in the world. This is one way that you can communicate, write the verify encrypts his queries to prove. Does these multiplications with encrypted values, so she never learns what the queries are and then sends over the results which they verify with his giant key then come with which the verifier was his giant key, can then decrypt, and he will then be able to do the actual verification.

B

In the clear you see the decryption of something multiplied by an encryption of something else. Decrypted would be the multiplication times more like yeah the multiplication of the things in the clear. So the verify I can just just verify everything in the clear then the other cool things that you can do is we exist in a world with pairings and there's another paper that works on the the things that we can get from: PC peas and the things we can get from QA peas, which was quadratic our has my programs.

B

So the reason why I introduced these like weird polynomials, which are called quadratic arithmetic programs, is that you can. You can reduce these like constructions. You can make these polynomials work with the PCP theorem in a way that the verifier only ever needs to multiply together encrypted elements once you never need to do like encryption times encryption times encryption, and this is exactly what pairings allow us to do so kind of what happens?

B

Is the cryptographers, a walking with the constraints of the tools that we have like pairings exist, but there's nothing that exists, but like three plus three elements together, and so what pairings allow you to do is, whereas, before we had like point time element in the proof, pairings allow you to do this sort of encryption. The way that the verify I just did, except you don't need to actually decrypt to be able to verify that the proof holds you can still compute yeah.

B

You can still compute the verification algorithm in this encrypted form using pairings, but you can only compute yeah one encrypted element times another encrypted element I'm with Q, APs and PCP theorem. We have exactly this no more, so this is how gross sixteen works and yeah and grass sixteen there's actually three elements. The proof is just three group elements which is like extremely tiny. This is what Z cash users. Currently this is it's like. The state of the art and one of the propellants is kind of like a representation of all of the egg.

B

Eight, if you can remember the arithmetic circuit picture, the other truth element is like representing all the low gates and then the side proof element is representing consistency of the entire circuit. So like using these two other proof elements, you can make sure that every every output of gate is equal to multiplication of the two inputs of the gate, with just three group elements um and right- and this has a CRS rather than the verifier, having a key which he needs to keep to himself.

B

This has a common reference string, which is where the trusted set comes from in constructing this common reference string. You have to like all work together to produce information, and you can kind of see now why that's important like before they verify I had to have some private information now like there needs to be at some point, private information to construct the things which are allowed to be public but then like from from then on in the world.

B

You can just use these public elements and seeing them doesn't like help anybody to break proofs yeah, and this is how this is, how proofs walk in the world these days right. So in conclusion, I don't have a conclusion slab, because these are old version of slides, but right pretty much snark so constricted in this way.

B

That gets the the statement that you wish to prove things about into this foam, which things can be proved really nicely about, and very conveniently like for the world that we live in in which patterns exist and then the second half of snog constriction is like getting from this convenient representation to something which we can prove right, while satisfying all of the properties that we spoke about at the start, like not interactivity, it's so small and it achieves yeah every property that you would want from zero all truth.

B

So hopefully this is demystified in some pot. What zero knowledge for saw thanks.

A

B

This is your laptop not like. Oh.

A

C

B

B

C

Great talk, so I would like to pose a question on the proof, size and the verification time on snark spacers Tharks, so currently the snark they are like of constant size they're very far in constant time, while starts on the contrast that you consider to be logarithmic.

B

C

You say that the constant size of the snark it stems from the setup phase, where, essentially, if you set up big enough parameters, you can say it is constant. While, for example, if you essentially set up a big end, like a very, very large number like 4, they start right also say that it's constant, since it will always be bound by that right.

B

I think this is a good point, so, like stocks do grow, logarithmically right in the size of the socket, but for example, if you just have a really small socket, so maybe I mean there would still be bigger than snogs or maybe like computationally more heavy, but I do think that, like the fact they grow logarithmically, it doesn't have to be some like it doesn't have to be right. It's not something! That's insurmountable right! You can still have smalls, not yeah.

B

You could still have small stocks like small enough for people to definition of small, to be satisfied. Yeah.

C

So for probabilistically checkable proofs I need to do n queries so that we have like statistical, let's say, security after we give. We get enough samples.

B

C

You considered using the recent work on vector commitments by bonds and friends to basically batch the openings of that probabilistically checkable proof so as to reduce the basically communication overhead, because currently you commit to a metal to route, and you need to provide multiple metal branches for it. While in this construction, I can basically give you one constant size proof which opens for multiple. Let's say indexes on the route that you committed.

B

C

You considered using it no.

B

No I haven't I, don't know, okay, it sounds great.