zkSummit: Notes from the SNARKonomicon: How to effectively program SNARKs - Izaak Meckler (Coda)

Transcript

thanks him so as I'm sure everyone is aware snarky nomicon it's an ancient book of you know eldritch magic it was discovered in the 1500s okay people don't like that joke so yeah well okay you know I apologize this is black and white also my computer broke so I couldn't do the color but it would have looked even more terrifying yeah so you know we're going to discover what is this snarky nomicon exactly more more in the talk but I assure you it's not as terrifying maybe as the name sounds and and as the devil on the picture suggests

but okay so just a bit you know just a bit about me and and where I'm coming from so I my sick that's me on Twitter I work on coda which I'll say a second about and also snarky which is a Zeke a snark programming language which will talk a lot about such things in generalities so coda is a cryptocurrency that uses recursive composition of snarks for blockchain accessibility and scalability so accessibility meaning basically anyone can verify the entire state of the chain even on a phone by checking a snark so if you saw the first talk it's sort of a similar concept you can kind of compress down the entire blockchain by using snarks so I've written probably I think I mean someone can correct me if

I'm wrong but probably as much snort code as anyone else and and this this talk is in an attempt to distill some of what I learned I mean you know this is of course drawing on the work of many people but I hope you'll learn something so yeah let's get started who maybe just to get a sense of the audience who is programmed s snark if you know okay okay great so ever almost everyone will learn something and who even knows what I would mean by snark programming okay maybe more P have some sense that's good so maybe this this thing is a you know mine

mind-numbing for no no let me not say that maybe some people have seen the almost this exact slide on everyone else's talk before so if so I apologize but just to set things up let's say you know just to kind of say what our Sark's actually do for a given program P with say two arguments and a public value X okay what snarks let you do is they let you prove statements of the form I know some secret why so that if you run P my program on X&Y it will output 0 okay that's what snarks let you do in such a way that the proof is well first of all it reveals nothing about Y so it's zk 0 knowledge right it's small so like less than a k if first snark because stark

maybe you can you can you can ask but and it easy to check so you know and the verification time is on the order of milliseconds in practice so then what we set your program right program P well it's a program what programming language is it written in write a program means a program in some programming language maybe it's x86 assembly who thinks it's x86 assembly anyone huh ah yes well perhaps on some level see maybe Python no I don't think so Haskell no it's not Haskell either it's actually something else and and what is that something else

so just to kind of say like snark programming manure gramming it's programming this function P that we saw a few slides ago but with a different machine model than all of the languages on the previous slide okay so usually you think about at the end of the day it's gonna be running on a ram machine right a machine with with a CPU that goes to memory that you know that does does its fetches and and and computes right what's up by step like that but in start programming of a different machine model just a note about terminology you know we usually people too often talk about programs or really what they mean is you know like it program meaning a program which is intended to be executed on a CPU sorry

programming just means a program which is intended to be executed for whatever that means on snarks okay and of course you know anything can be executed on anything else but but it's it so somehow about the attention and just you know let me say most of this is not really specific to snarks some of it is sort of but most of it also would apply to something like a bulletproof or like Starks okay so it's just about the ideas here of how you think about the conceptual models of programming mostly and some of the tricks okay so what about snarf programming is different from quote-unquote normal programming or as I call it CPU program no I don't call it that but programming well one is the

cost model so what is it that's efficient to is in snarks you have this magic superpower which is called non determinism don't worry if this is a scary sounding word or if you don't know what it means I'll talk about it and and the third is that you can only you can only inside of a snark some time accesses a small amount of data at a time in a way it's also different from a CPU you know a CPU is this like tiny thing and over here is like the giant memory you know and and the CPU just sees a small amount of the memory at any given time right but in a way it's not so different so let's first talk about the cost model and in terms of what what primitives what what are the sort of

efficient primitives that you have access to in both settings so on a normal computer who is programmed a computer oh that's great no no I mean it's not every room that you're in that it you know almost ever and raises pan so that's great so a normal computer you know you what do you have you have like say plus and times mod you know 2 to the 64 say 64-bit ends you have memory access you know you can load and store from memory you can do bit stuff so you know and an or and all that and you have conditionals jumps basically sorry what's the deal so well first of all you you have plus and time plus and times mod some large prime P

it's not so different somehow the the P is a bit larger but anyway this is really important plus is like kind of free ish okay so plus cost is your ish when you're programming this how you think about it plus plus is almost free times cost one does that make sense addition is like free times is not free cool make sense okay and okay what else you have well no actually that's pretty much it so you might be a little bit worried and say oh oh no really that's it and you know you might say well this this seems really bad and this is the snarky nomicon demon who is laughing at

you you only have plus 10 times and you know sometimes when you know I think about the situation I go back to this famous painting of Hieronymus Bosch from 1575 called snark programming optional question mark which illustrates some of the interesting aspects of snark program you see here you have the large large prime and you know here is the the multiplication and you know you might look at this picture and think I think it looks a little bit scary you know there's people burning and so on but actually it's not so scary one this place looks pretty cool there's a giant person with a giant mouth and - you're

allowed to do some other stuff - I kind of lied it's not just Boston Times for example you have no deterministic choice which we'll get into and you can sort of computer on values as normal as long as it's only sort of statically known things which is actually useful okay so yeah so the goal of this talk is basically the following it's to convince you that and show you how to make this a comfortable and exciting place to live you know some of these things which looks scary like the guy with the big mouth maybe actually he's a nice guy for example and the major takeaways will be the following one snark chromium is is both beautiful and fun just like programming non-determinism is a really powerful

technique but it's kind of scary and we'll talk about what's scary about it and three there are a lot of really great cool ways that you can sort of do things efficiently just by using field arithmetic that you have in this this huge field that that aren't things that you could necessarily do on a normal computer and I'll try to give some examples in snarky which is this smart programming language of the concepts that we discussed and you could also think that you know at the end you will see this snarky demon and not think that he's tormenting you but actually you will think that you're laughing with him about how great and fun snark programming is so just a word about notation we'll fix this large prime P

that you have additional multiplication for you know you should think this large but in the talk I'll use 13 in examples which were a human is large but you should think of it as like 202 to 256 realistically speaking and a number and 0 to P you call that a field element okay people know this okay okay so just like let's look at a snark program this is a really simple program what does this program do well okay who heard about elliptic curves before oh okay a lot of people well even if you didn't it doesn't matter because they're extremely simple there are just a set of solutions like x and y to an equation that has this form okay cool and you know

geometrically speaking say over like real numbers is what they look like all right so this is just a really simple program that just this does this arithmetic right we said we said we could do plus and times let's do it let's do plus some times just to introduce the notation so you know I say a is 1 B is for whatever and and here's the function that just computes you know the right-hand side here right x times x times X plus a times X plus B ok does it make sense and this is saying this is a function right this is kind of like looks like JavaScript maybe ish yeah everyone with me sort of okay so it's a function that's just to give you an idea of what the syntax looks like now let's

talk about non determinism which is quite interesting so who heard about non-determinism I know I keep asking people oh that's that's cool so sometimes as people might note checking is easier than doing something yourself who has had this experience in their life that they were able to check something that someone did and it was easier than how do they done the work themselves probably everyone has had this experience unless you sit in your room all day and don't interact with other people I would imagine that you checked what someone else did at some point your life without doing it yourself so everyone knows somehow this is intuitively true and what's cool is that this is non terminus and power that you have in snark programming it lets you go from being able to just check

something to being able to do it which sounds pretty nice I imagine we would all like to have this this power I guess that's called delegating responsibility to other people but anyway so let's have an example a concrete example of what using this not a terminus and power looks like to do a very a very simple computation in some sense it's the simplest possible computation and that computation is dividing numbers so if I give you x and y and you can do multiplication addition nothing else let's say how are you gonna compute X divided by Y okay another way of saying this you want to find some Z so that Z times y equals x people see that I just moved I just you just you know you

divide divide by Y and it says Z is X divided by Y right okay so you just want to find a Z where that's true about Z so one I know it's a simple silly example but it's a really in a very important function you need it to efficiently implement it lifts a curve or if gonna take what you need for doing anything inside of snarks hash function Peterson hash you know signatures vrf recursive composition the list it just goes on and on so let's give a deterministic algorithm for it it's probably not the best one but it's the easiest one to think of for computing X divided by Y so what's the algorithm you use whoo-hoo

nuts for muscle up there maybe for your hands okay so this says that if you if you raise a number to the P minus one power then equals 1 mod p okay of course so it means that you can do division by doing multiplication in a finite field you just multiply you don't really have to worry about it the upshot is basically you compute X divided by Y by multiplying X by Y to the P minus 2 okay so you can do division by doing multiplication that's it's kind of cool actually but but actually it's not that cool because this is expensive you have to do like 256 multiplications roughly

to compute this exponentiation and and that's just for one division so you might already be kind of like oh sorry not so good huh yeah this is definitely bad but what about checking a division so like let's say if someone gave you Z right how many multiplications would you need to check that Z is X divided by Y who knows huh one right just one you just check that Z times y equals x right that's it it pins down Z exactly so that's great because in snarks you have this guess and check power which is another way of

saying you can do not a terminus of choice you have a magic guess function it's magic in snarky it's called exists because you're like this exists it's like guess you also have a magic check function which lets you make assertions which you can you know like an assertion of normal programming halts execution if the assertion fails it's like throwing an exception and I call assert so you know diagrammatically here's how you do a division if you can magically guess things so you guess a Z right and then you just check the z times y equals x and you return Z does it make sense conceptually I say I want to compute X divided by Y first I guess Z by magic and then I just check does Z times y

equals x if so you know the certian passes I go I go to the next line I return see otherwise execution halts and ok that's it so you know just to do an example let's say we want to divide the 6 by 2 you know I guess conceptually you first think you're sort of making all possible choices is equals 3 is equals 4 whatever then you check each one so okay 3 times 2 equals 6 yay 4 times 2 is 8 not 6 does that so their execution halts 5 times 2 is 10 not 6 so their execution halts again and so you know this is sort of the only branch that we take in reality so okay just like let's crank through it so okay we

did 6 6 over 2 right that was 3 1 / - I guess it's 7 I'm gonna guess that and in fact I'm right because we're working about 13 if anyone remembers from that slide way long ago because 7 times 2 is 14 which is 1 on 13 how about 0/0 I don't know maybe 0 that seems like a good guess let's check Oh zero times zero what is it it's zero okay great so I guess if I divide to zero by zero at zero Oh what about dividing 0 by 0 whoa no maybe it's five well let me check oh yeah 5 times zero it's Europe so I guess dividing zero by zero is five so dividing zero by zero zero dividing zero

by zeros 5 which maybe you think the snark demon is coming to haunt you again and yeah you know that that is that is a little bit troubling so everyone take this in okay this is like understand non-determinism it could it's either right I mean you you sort of don't know what gives 0 0 in some sense is going to return it could return anything which would make all the assertions pass in particular well it could return zero or could return five you don't know and and you have to think about it that way when you're programming so there's a few things you can do about this you can add an assertion basically that says Y is not 0 like the second argument say that

would cost you an extra multiplication so you know not great but still a lot better than 256 right so now it cost to have 256 that's pretty good another thing is you could change the name of the function from div to div unsafe and forget about it and that's an emoticon it's a sideways okay so just like to show you what this looks like in code yeah this as I said you have a magic exists function and this is just how you write it so you say okay guess Z so let Z be I don't know guess and then assert that Z times y equals x and then return Z okay so it's kind of what I said cool okay how am i doing on time about 10 more minutes okay okay so

let's just you know you maybe think okay go around very cool you can divide numbers great what am I gonna have ever have to use this in real life non-determinism well you will have to use it in real life it comes up all the time and to just revisit our previous example remember we had this this was literally what this was the slide before we had this elliptic curve you know and we had this function f for computing the right hand side here X cubed plus a so what if you know we wanted to start with an export like here's something that you have to do in snark sometimes sometimes you have to decompress a curve point who knows what I even mean but it means you start with the x-coordinate and if you look on this picture of an elliptic

curve you know corresponding to every x-coordinate there's either is exactly two points on the elliptic curve corresponding to that x-coordinate because you can solve for y you just take the square root of f of X right yeah but it could be plus or minus so there's two but the thing is right there's only two so that's pretty cool so sometimes you sometimes you just have the x-coordinate because it's more efficient maybe you don't have to have both the x and y to determine the curve point you just need the x-coordinate one bit so one thing that you would want to do is is decompress a curve point so given just the x-coordinate you want to compute both the external and the y and in starks it's super easy

what do you do you say guess why okay and then just assert that y squared is equal to f of X done and then you just return X and why does it make sense you guess and then you check you guess oh maybe that's why let me check okay I checked yep it was white I returned white and so when you return here is only the Y's which make this equation true but it's a little bit scary because you know right so it could be this way but but it could also also be this way so you don't know is this going to return that one or that one you would have to add more checks to pin down one or the other but okay whatever sometimes maybe you wouldn't care so just like to wrap up you know takeaways

about non terminus 'm yeah when you when you're trying to write non-deterministic programs you think more about specs than algorithms so you know this is like a spec right I'm saying basically return Y where you know Y squared is equal to f of X you said I'm saying it's not really an algorithm it's just a spec it doesn't tell you how to find Y another thing which you know I probably was clear but non-determinism gives you a essential efficiency improvement so you can't write efficient snark programs without using non-determinism I mean I don't know maybe someone will tell me I'm wrong but I know it you you can't but

it's also really scary right so we saw this like it divs your zero thing remember we're like if you divide 0 by zero it could be anything so that's really actually extremely scary because you can't rely on any any anything actually about the output of that function it's totally unconstrained which means maybe you're you know maybe you're just using division inside of an elliptic curve operation but you know at the end of the day what it means is you you sort of allowed the attacker I mean you think in your mind always about a malicious proofer I guess I should have mentioned that you always imagine there's a malicious prover who's trying to sneak bad values past all of your assertions do you see using I'm saying so that division function is really

scary because it lets them sneak whatever value they want through your assertions which is potentially really bad so you try to build abstractions that somehow use the non terminus and internally but don't leak it if possible so for example it with division if you assert that the that y is not equal to one or but not equal to zero then you don't have to think about anymore you know it's sort of really a function it doesn't have not a terminus something let me say something about taking advantage of arithmetic all right five minutes there's non tricky techniques and those are like using elliptic curve based primitives that I think I think people kind of know about this by now but you know there's like the peterson hash

function for example which is like twenty to thirty times more efficient than like a bits style hash function like char blake to and and another non tricky thing is just simulating integer arithmetic so you feel the rhythm chicusurile you know as long as you don't overflow it's the same as doing integer arithmetic but then there's also a tricky technique the tricky techniques so these are the things that you know make the snark devil smile and that also make us smile so for example there's packing okay I'm not gonna talk about it but then there's also this technique that I just I didn't really have a word for it but I called it some as search the ideas addition is free and we want

to make it make use of that so I'll give you the simplest possible example of this just something to take home with you and later you can go online and read more snark programs and assimilate you know this idea and you'll see it in multiple places so Bulls inside of snark programs we only really field elements so how do you represent a boolean it just with a field element which is only 0 or 1 okay it's a field we have 0 we have 1 okay mmm happy are we happy it's maybe not the best representation for all purposes but it's it's pretty good so you know with this representation everything's pretty easy to talk about all the bits all the bits stuff you know and love from normal computers the greatest hits we gather them all not it's one minus X right so

because if x is 0 then 1 minus 0 is 1 if X is 1 1 minus 1 is 0 so it's it's not right we got and you know it's just multiplication right because 0 times anything is 0 like false and anything is false and true and true is one is true so its weights is one times one makes sense yeah okay and then you know if you have nan and you can do or for example with just de Morgan I guess it's called so you know X or X or Y X or Y is true if they're not both false right and you can kind of say like any right so if I

have a if I have an array of bits I want to return a bit which is which is true if if any of them is true you seen I mean it would be doing like B's of zero you know the first the zero thing or the first thing or the second thing or the N minus one thing okay and you just write you know reduce like functional programming does it make sense do people see what I'm saying okay so this is okay what's the what's the total cost of this remember we only care about multiplication this is cost n minus one multiplications because each of these orders here costs one multiplication because coming from this so that's okay I guess but actually you can do even

better how much better you can only use two multiplications regardless of how many things you're ordering together and what do you do well you just take all your bits and you add them up okay you just add them like they're numbers I mean there feel elements you can add them and then you just check you look at that sum and you say hey is that something equal to zero right and if it's not equal to zero it means one of them had to be nonzero right doesn't make sense do people see maybe requires a moment of thinking okay now so this is great because this only costs two

multiplies rather than n minus 1 they're inside of equal but I won't show them so this is oh yeah maybe after so this is a yeah you know a neat trick you're kind of searching the whole thing by adding everything up additional streets so it doesn't it doesn't matter if you add up everything 3ish so you know I'm almost at a time see ya some important things that I wanted to talk about but couldn't talk about one is it's one thing to write exists you know to just write guess but you actually you actually have to find that value because it's not a magic computer as someone back there said it is executing on a you know a normal

quote-unquote computer so you need to actually specify how to find that value this may be someone would call witness generation and the other thing I didn't talk about is how to simulate large memory banks remember when I was like oh you're small CPU and the giant memory is over here and you need to reason about it so I didn't talk about how'd it simulate that that's an interesting technique there's a lot of cool efficiency hacks you can do there too but I also didn't talk about mixing snort code with normal code it's another normal thing important thing and that's pretty much all you have so thank you [Applause] we have time for a couple of questions yes hi

thank you for this very very interesting presentation is there a intuitive explanation of why addition is so cheap and multiplication cost one let's see I'm right now I'm simulating like the whole reduction in my mind to think about where it happens it it's not I don't know it's it's a it's there's it's a very particular artifact of the construction I think but but but addition is always a lot easier maybe it shouldn't be so foreign because addition is always a lot easier than multiplication it's kind of comical but we'll talk about it after annal and I'll

trace through the reduction and remember what where it happens I don't remember off the top my head other questions the reduce exemple when you use some instead of multiplication that could steal overflow right could it so Peas let's say you know the prime is like 2 to the 256 so you're adding up like you know how many bits would thereafter be for overflow like 2 to the 256 which is not a real number I mean it's you know according to some people it's a natural number but it doesn't exist you would never contract that many bits in the universe then let

me say that right yeah so you do cut hacks like this where something is sort of ok but only for cryptographic reasons I guess oh I'm curious like in your current circuits what percentage is bullion Adichie and if you have a smart way to aggregate those what percentage I mean it's definitely a lot because because most bits the Merkle probably everyone knows the worst thing is doing a merkel lookup the worst thing is doing

a memory in a snark that's like I guess it's the case in with real CPUs - that's the worst thing but I don't know % but yeah with that would be I don't have a smart way that'd be great how do you test to make sure that there's no problem in non determinism yeah that's a great question no no that's really a great question because as I said it's really scary the snark demon sometimes haunts me in my sleep you know thinking like oh no did I put enough constraints but yeah I mean so we we do unit tests you can kind of just try and stuff values in there and

see if you can make the constraints pass obviously that's not not really gonna cut it for most cryptographic applications because they're the errors are like on points that you would never find if you're testing randomly but you know we've started a little bit looking at doing some formal verification so like doing some proofs but it's that's in ages and right now it's you know you you get a lot of people to read the code and think about it very hard I I'm sorry the other thing is I always write pen and paper proofs or in the comments I put proofs but that can even only get you so far I think we have to wrap up the questions and move those to the coffee break afterwards and start preparing our next speaker so thank I

sick very much again [Applause]