'The Evolution of Circuit Languages' - Alex Ozdemir

very cool yeah yeah okay very nice um i want to introduce you then let's let's kick it off okay so we are now going to hear from alex osdomier who's a phd student at stanford he's interested in programming language languages and cryptography and we're going to be hearing from him about the evolution of circuit languages so please take it away yeah thanks ella um yeah so as i said i'm kind of like uh i guess my background is cryptographic but also um in in programming languages um one thing that's been really exciting for me is that what we've seen over the course of the past maybe eight nine years or so is a real a real explosion of languages for building circuits for use in zero knowledge proofs um and and the result is a sort of extremely rich landscape a rich ecosystem of different languages that are serving different needs and work in different ways and what i'm going to try to do in this talk is is tell a cohesive story um about all the languages that we've created so um let's start by thinking about why languages and essentially the reason that languages for circuits are important is that zero knowledge proofs as you know zk snarks they're very powerful um that they allow you to do really cool things but they're also limited and so what do we mean by the power um well the power is that we have some sort of problem with the pen now it's exciting okay we're all good um so the power of these proof systems um is that they allow you to prove a very rich language of statements so what kind of statements do they support um well to be frank you guys probably know this better than i but but i'll just a few examples common statements include i have the money maybe this is what the z cash circuit is proving you're proving that you have some previously inspect point perhaps i know the credential so if you're trying to take some action on some sort of to modify some sort of distributed state you might need the credential to do that you could use the zero knowledge proof to prove that you have that credential you know it um perhaps in some kind of distributed voting application you might want to prove that we have the votes that is some agenda that you're pushing has um a enough votes to actually affect the global state um and these statements are are useful uh primitives and implementing various kinds of application logic and this is why zero knowledge groups are so powerful but the the thing is they're also limited and the reason that they're limited is that you actually you can't prove any of these things these statements are not what zero knowledge proofs give you um we often think that they are but they're not what do zero knowledge proofs actually give you well what they actually give you is i know the solution to some equations and often times we review the equations as a circle so what do we mean i mean that if what you have is something like x times y equals z if you're trying to prove that x times y equals z and you know values of x and y and z which make this equation true you can do this also as a circuit where you've got x you've got y and you've got z and you're multiplying x y and you're checking for equality with z um you can you can prove that that this circuit evaluates to true you can prove that these equations are satisfied um and so what we have is we have a compilation essentially because the ideas that we have around the statements that we would like to make are very high levels so we have these ideas but in order to get to writing proofs about them um we need to first turn those ideas into a circuit so we have this problem to solve and you know once we solve this problem then we can use our favorite zero knowledge proof system to actually produce a proof this is where there were the terms graph 16 come into play this is you know graphic scene is improved system implementation plonk maybe stark these are all proof systems they're all they're all essentially for turning circuits into proofs but the the question that this talk focuses on and the question that circuit languages address is how do we do that first step how do we go from the idea i have money to a circuit that encodes the idea and what we would like to to have in order to solve that problem is a language that we can use to describe these circuits um in some kind of higher level fashion that's easier for us to understand and easier for us to express ourselves in um so circuit languages solve this problem this problem of expression and and uh they've been undergoing quite an explosion of growth recently i would even call it a cambrian explosion in the same way that that life very quickly went from single cell organisms to dolphins um circuit languages are quickly getting more and more complex and more and more numerous in my mind the story starts in something like 2013 this was when the first things that i would call circuit languages for proofs started to uh started to arise and it's been continuing through the present and has only been accelerating um so what i'm going to do the rest of this talk is i'm going to walk us through this timeline from 2013 to now and look at the different ideas that have come to play in various kinds of circuit languages um and i just want to give a warning up front that the timeline that i'm going to give you is a little bit of a lie a lot of the works that i described were actually developed concurrently but we're going to sort of put them in a particular order to try to help us understand the different ideas that they're working with so let's get into that um so what's that what's the beginning of the story for us well the beginning of the story is what i would call part one macro assemblers so the very first circuit languages um perhaps what we'll say at the beginning of our story is the lib snark code base release which was in 2014 on june 2nd in particular i went look at the comment blogs and libstart is dominantly an implementation of proof systems so it's dominantly an implementation of a zero knowledge proof um but inside of it there was there was some machinery for building the circuits that you were trying to write the proofs about that machinery was called gadget lib um and gadget lib was essentially a c plus plus library for building circuits um and the way that it was designed is that it provided gadgets so sort of like c plus classes that wrap references to the circuit for modeling ideas like booleans like machine integers that is fixed with integers that wrap around and overflow um and then also you know gadgets for various kinds of cryptography so implementations of hash functions implementations of signature verification that kind of thing essential essentially what gadget lib is is it's it's a representation of this idea that you can use c plus plus abstractions for circuits so gadget live is saying we don't need a whole new language um all we need you know c plus is a great language it's got great abstractions we're just going to try to use those abstractions to wrap various concepts that we want to embed in our circuit like a boolean um and we're going to we're going to come up with c plus plus functions and methods for combining booleans in the circuit and this is a good idea it makes people very productive um but um some people look at this they look at this idea use c plus plus abstractions and they start to get nervous because you know c is kind of a crafty language it's very old uh perhaps venerable and it's not known for having particularly solid abstractions um so some people look at this and they ask what if you don't like c plus plus what if you're worried about the kind of pervasive unsafety that cbs plus has led to in the development of system software all this blockchain stuff is very security critical it's very important that the circuit encodes the right thing um and perhaps we're nervous about using a language whose abstractions have traditionally allowed programmers to express the wrong thing many times and in a great number of damaging ways um so this this concern that c plus plus um while the idea of having a macro assembler a library that helped you assemble circuits was useful they were worried that simple spots wasn't the right language for that and this led the development of two other projects that we'll talk about now the first of these projects is belmont so bellman was developed starting in 2014 um and it was built by the folks at zcash um and dominantly that the idea was that they built it in order to construct the sapling version of the zcash cryptocurrency and their their goal at a high level is just to take take libsnark and just move it into rust move gadget move some kind of gadget description language into rust um and build out the kinds of high performance gadgets that they needed for sapling as they went um and this went well and bellman is something that's that's still used matter labs has continued to add to it and use it i've used it for various projects myself uh various academic projects it's a it's a great macro assembler um but uh in the same way that the folks at zcash thought hey gadget was great but i wanted and rust other organizations thought gadget live is great bellman is great but i want a library that's in my other favorite language so as an example of this um we have we have another macro assembler snarky so this was built in ocam was built by the folks at order one labs and development early first public release was in 2018 it continues to be developed today i mean it essentially is another another iteration of the same idea we want to build some library in a different language for constructing circuits now we're just going to do it no camp so this continues to be useful um but it's not the end of the story um because one thing one issue that you run into when you're building a library and some other language to model circuits is that this language wasn't really designed for circuits in the first place it must have ideas latent in it that aren't useful for building circuits um and there might be things that are important in circuits that are hard to express uh through this language um and you're kind of limited because you're working in this language like rust or like camel you're working inside some host language you're just writing a library um so you don't have as much control as you really like and so this this grows a push to construct languages explicitly for circuits not not libraries that were writing on the back of some existing language but a language for circuits um and the first step in this direction i would say it was the construction of so-called so-called hardware description languages or hdls for arithmetic circuits and in order to understand this idea of using hdls for circuits we need to understand hdls and that means that we need to take a detour into the world of digital design um so what is digital design about well it's about the answering the question how are computers made or really how our computer is designed um so if you open up your computer inside it you'll find a collection of ships um perhaps pentium perhaps something in the sandy bridge family this is one of intel's i guess now old generations of their architecture um perhaps the the recent m1 ship that apple has built and some people are excited about maybe too excited about i don't know um but but so what digital design is about is it's about building these computer ships um and this is relevant to um to the design of arithmetic circuits because what computer ships are is they are essentially digital circuits if you open up one of these then what you're going to find is you're going to find like an andy gate you're going to find or gates you're going to find these registers be connected to clocks you're going to find all these different components wired together in such a way that you can you can do things like run assembly instructions um that's that's what cpus do that's what computers do and the natural question is how do people these things they have billions and billions of gates how do people design these chips that have so many gates and the answer is they use hardware description languages these are built with hdls i mean there's a lot of hdls uh verilog vhdl uh bluespec maybe more recently chisel more or less people are still basically using their log system paralog um but what these languages are is these are languages that were designed not to to program a computer and not not like wire up different components but instead um to to to connect gates to one another um and so one question that people ask is hey you know we got these great languages these hdls for building digital circuits can we use those to build the kinds of arithmetic circuits that we need um in in snarks and uh and of course the answer is yes you can totally do that uh so the the first project the most the most prominent project in this area is sircom which was mentioned in the previous talk uh this was a a hdl essentially for arithmetic circuits that was developed by jordy bailena also starting roughly in 2018 that's when it was first public um and it has a number of big ideas in it that are taken directly from the world of hdls and these are the ideas of constructing equations in the digital world this would have been constructing gates and organizing those equations into modules and then connecting the modules to one another um so all these ideas these are ideas from the world um of hardware description languages um and and sure column just brings those to arithmetic circuits so now with circon you can write a circuit um in the same fashion that you would have written a you can write an arithmetic circuit for zero knowledge in the same way that you would have written a digital circuit for a processor i mean this is pretty cool because people have been using um the hardware description languages for a long time and they're reasonably good at it but this isn't the end of the road and the reason it's not the end of the road is that hardware description languages are nice but they're not programming languages um so programming languages are a little bit different programming languages they don't have this idea of gates being wired together and organized into modules no instead programming languages have stateful semantics they have this idea of variables that you can change over time and if statements that you can either execute or not execute depending on some condition you might have loops you might have function calls with returns from those function calls and you know within loops you might have breaks and you might have continues you have broadly speaking this notion of a sequence of instructions that gets executed or not executed depending on the image of the program and the the systems that we have for expressing ideas um in terms of variables in terms of loose in terms of if statements we call these programming languages it's not hardware description languages programming languages um and the in programming languages for for those who have used both hdl's and pls programming languages people people like more they're easier for us to reason about and so what we would really like is we really like to be able to write down our circuit in a programming language or like write down our idea in a programming language and have it be turned into a circuit for us and this is a challenging thing to do because there's a core problem we have to overcome which is that programming languages are fundamentally designed for the ram register computational model so programming languages are designed with this kind of processing and unit in mind that executes instructions over registers over data and sometimes takes that data and either puts it in or gets it from some large memory or ram so this is the computational model of turing machines this is a computational model that our computers actually implement this computational model is what programming languages are designed to abstract but what we need in order to use the zero knowledge proof is we need a circuit which is a a computation written in the circuit model where there is no state there is no notion of time there is just a whole bunch of values that get combined and recombined into a single answer the circuit model is much simpler in some sense and hdl's um they're designed to target the circuit model but like i said what we'd really like because we like the the ram register model more is we'd like to be able to write programs and then use some kind of compiler to turn our ram register programs into circuits we'd like to like take that that program that loop and then roll it into a big circuit that we can we can do cryptography on um and so the question of how you do this conversion or this compilation is a challenging one and this is what i needed to be overcome in order to have true programming languages for zero knowledge um and so this project um is a challenging one and it's something that people have been working on for a long time um i have here a few of the academic projects um that have been working on this listed pinocchio pedo bikini these were the original people who tried to tackle this problem and the way they viewed it is they wanted to take some existing programming language they chose c and compile it or some subset of it into a circuit um and it should be obvious immediately that that they can hope to do this completely why because c is like a super nasty language with really complicated ideas in it that are um possible to implement in the ram register model but but rather incompatible with the circuit model what kinds of ideas am i talking about i'm talking about for example function pointers so in c you have a pointer to a function this is a pointer to some code um that's not known at compile time and and you can call that function during the execution of the program and it's just not clear what that would mean in a circuit like i i guess it would mean like i look at some data and depending on what the results are i run a different sub-circuit it starts to get really hard to reason about a similarly challenging idea is the idea of dynamic memory so i have some huge chunk of memory and i want to access it at different locations depending on the inputs to my program that's also pretty hard to express um in in a circuit um but nonetheless um the the researchers were working on these projects they thought that it would be interesting to try um and so they charged down and compiled the largest subset of c that they could manage into circuits um and produced some compilers that were really interesting they developed a lot of great techniques um but fundamentally i think that these projects were just too ambitious because despite their successes there are still huge chunks of the c language that they don't handle or they handle incorrectly and programming in the presence of a compiler that doesn't handle the input language fully is really challenging because you worry that you might write something down that the compiler is going to misunderstand um and so fundamentally i think a less ambitious approach was needed this was just too hard um and so this brings us into part four of the evolution of circuit languages which i would call dsls and so the idea here is that this this premise that we want to compile programming languages to circuits is it fundamentally broken it's just it's just too hard um and so what we want to do is we want to make it easier by co-designing the language the programming language with the compiler that's supposed to turn it into a circuit so we can design the language in a way that makes this problem easier and there are a number of great works in space the oldest of them is socrates which has sort of like a python-esque language with built-in support for field elements and various restrictions that make it that make it possible to compile perfectly into a circuit um and since socrates there have been another other a number of other projects so there's noir which is being developed by aztec um there is leo which is developed by elio and there is zinc which is developed by matter labs and this is not an exhausted list there are also other other examples um but broadly speaking all of these projects what they're trying to do is they're trying to design some some programming language specifically for zero knowledge that they um because that language is restricted and because that language has been specially designed can subsequently compile into a circuit far more easily than compiling something like c um and so looking at this landscape um i would point out that that socrates sort of is the is the has the best polish it's the least buggy so if you're doing something this second i would probably recommend socrates um but these other languages are much more ambitious in scope and they really do have great potential and they're extremely hot off the presses right now um i think that noir was released like literally like a month or two ago um but but there's a lot of potential here and so i would keep an eye on them i expect in the long run they will they will be quite great tools um for expressing expressing ideas that you want proven zero knowledge um so that's kind of the end of the main line of the development of circuit languages i do want to take a moment to sort of do another detour into starks um so stark is a different proof system it's a new proof a new kind of proof um it is the proponents of it would say more compatible with ram register programming more compatible with the idea of state and iteration and the reason that people say that it's more compatible with this is it's built on repeated circuit application so rather than building some big tree that is your circuit some huge monolithic thing like the zcash spend circuit um what what you do it with stark is instead you come with a small circuit c that gets repeatedly applied and so what you try to do is you try to view the computation the statement you're trying to check instead of just being a standalone circuit you want to express it instead as the repetition of a smaller circuit um and so this is obviously a very different programming model you're looking for common structure um and so that that means that there are different programming needs that need to be met and uh the people at starkware have built this language cairo that's trying to capture programs in this alternative model so that's kind of interesting as well um okay so i want to take a moment and just just reflect on on what we've covered in this talk um the first thing i want you to take away is that there has been an explosion of languages over the past eight years or so languages have gone from being simple things um like gadget lib to far more complex things like socrates and zinc and cairo the second thing that i want you to take away is that in the design of these languages there are serious compilation challenges this is harder than building a c compiler this is harder than building lfm because it requires you for example to move between the ram register model and the circuit model it requires you to get rid of powerful and hard to express notions like variables um and because this problem is so challenging i think the third thing that you should you should take away from this talk is that we really need to continue to explore we don't know the best language yet we don't know the best way of writing languages yet but even as we explore we don't want to waste effort because this problem is so hard if we try to stop start it from scratch every time we build a new language um that's going to be a lot of work and i think more completely what will actually happen is that languages look bad they'll be missing huge chunks of things that would be useful because it just takes too much time to build everything again from scratch every time um and so the final the final reflection i have is um i think it's worth asking can we reuse compilation infrastructure so socrates has a great compiler but if you want a different language if you want to build on socrates is it possible for you to for example reuse the infrastructure that underlies socrates or you know that that probably isn't isn't doable but is it possible for you to build on some kind of shared infrastructure that can support um building new and exciting languages for snarks um and i would argue that the answer is yes yes this is possible in the same way that the computer science community has constructed llvm which is this super power ram register compilation infrastructure that allows people to compile rust and c plus plus to arm in x86 um we could build a circuit compiler infrastructure which allows you to go from a language like socrates or a language like zinc or language like noir you could imagine all these languages building on some kind of shared infrastructure that helps them on the back end not just produce arithmetic circuits say written as r1cs which is a particular arithmetic circuit format but also produce the kinds of arithmetic circuits that you need for other proof systems like plonk this is like what we would want i would argue if we want to continue to explore different languages without reinventing the wheel every time we need some infrastructure that our different languages can share um and i think that working on this is a really interesting thing to do um and i've been spending some time on it with with a few friends of mine we've been building what we call spursi for circuit compiler we think that it might be this infrastructure um if you want to learn more about it you can go back and you can watch the zk study called videos we did a presentation on it at some point or you could go to this url um where we have a paper that talks about these challenges of common infrastructure and talks about our take on how you might build it okay so again once more to recap um over the past decade or so we've seen a real cambrian explosion of circuit languages these languages are solving a hard computational challenge moving from the ram register model of variables and loops to the circuit model where you don't have those concepts um and the the jury is really still out we're not sure what the best language will be we're not sure what the right abstractions are we're still trying to figure it out um and i think that one one thing that we should try to do is as we continue to explore the space we should try to build as much shared infrastructure as possible so that we don't have to reinvent the wheel every time that we construct a new circuit language so thanks for your attention um i'm happy to take any any questions now it's fine cool thank you so much for this talk and it's been awesome to see it visually it's very cool um question from the audience why do zk proofs need to run on circuits and not as programs in a nutshell it's a really great question um and uh there's two answers to it so so the first answer um is that to run a zk proof what you do is you do a lot of cryptography or you do a lot of math um and one thing that makes doing math easier is if you know what you're working with and so the problem with a program is you don't know how long it's going to run this is an object that changes over time that's something that's hard to do in athlon so the reason that we use circuits instead of other kinds of programming models is that circuits have fixed size and they're easier to build proofs for if we could build proofs for your cpu for assembly we would um and this takes me to the second answer which is the people who work on starks say actually you can um and i personally you know the jury is kind of out we'll see how well that works um i think that that's not going to pan out but i could be wrong um and if it but if it did work it would be very important um one one question is do you actually do you have the slides that you that will you be sharing these slides shortly after yeah i'm happy to i can send them to i guess the eph people um maybe another question here so like i think you've highlighted something that needs to be fixed and improved is creating that sort of center point there any other things in the general language ecosystem that you think need need work where people could potentially direct their attention um yes i think there's an extremely long list of things um and and so what are these things support for a richer set of types support for large integers support for various kinds of memory embedded in the circuit complete support for the primitive things having integers of any width you want having field elements being able to embed like other fields like baby job job and inside inside your current circuit but there's a huge list of things and while this is my wish list this is what i wish every language supported i recognize that as long as we sort of try to do everything independently it's unrealistic to to get all these goodies um um unless we try that typical efforts um cool another question does research from snark provers and stark provers build on each other ooh does that is there some connection point there intellectually for sure um so when people started figuring out how to build these these small circuits that get repeated in starks you bet they looked at how we had been building circuits already to figure out how to do that and and also there's been cross-pollination in the other direction as well um so at least um some people who think about plunk actually sort of view it um as exposing a similar abstraction it's not an exact match but they they draw on stark ideas as well um so it's on an intellectual level 100 there's been cross-pollination and there will continue to be cross-pollination um at an infrastructural level i think it's also possible but it's an interesting question um so this is not something my friends and i have explored so far um building common infrastructure that can be shared between starks not not just like common ideas but actually a common program that you could write while just darks and other things um but i think would be an interesting thing to explore if you're interested in that come talk to me uh here's a question from our next panelist actually barry how can cersei take advantage of um of planck's specific optimizations yeah this is a great a great question um so what i actually want to do is scroll down a little bit and look at this this picture we have in the infrastructure here um and what i would say is like you know on the back end here i sort of just like drawn like the different kinds of representations you might be producing separate things but actually what you really are going to have here is you're going to have sort of a branching tree so what you really want is you want to design the back end of this infrastructure so that it starts by doing the things that are common to all proof systems so for example all proof systems work in arithmetic over finite fields so step one is sort of make everything a finite field you want to do that whether you're targeting plonk or whether you're targeting r1cs or some other format um and then after that you want to apply increasingly increasingly proof system specific optimization so yeah at some point you want to run plonk specific optimizations um and there is space for that and this infrastructure um i i guess what i would say is like common compiler infrastructure the idea isn't that every single thing gets used by every single target application it's that you try to use as much as possible of what already exists for your target application and if you need to add more specific things that's okay too cool all right so i think we're time thank you so much alex for this great talk