zkSessions: Alex Ozdemir - The Taxonomy of Circuit Languages

Transcript

i want to welcome alex to the stage to talk about the taxonomy of circuit languages please take it away yeah um thanks thanks anna um so yeah i'm a phd student at stanford i've been working at on circuit languages for a while from an academic perspective and so i'm very excited to be here today to talk um about sort of the whole the whole rich zoo of circuit languages that exist so let's let's get into it but before i do i want to give a brief word of warning which is that i talk about a lot of languages and a lot of features of them and i do my best to to get everything right um but if i've mischaracterized your language um it's it's ignorance not malice i would love to know about it so just

send me a note or or correct it during um your own your own time slot um so let's get into it so so what are secret languages well let's start by just thinking about the core problem that they're trying to solve so this is this is what's going on we have some idea um maybe it's an idea for a payment system maybe it's an idea for a voting application and we think that proofs uh zero knowledge proofs might be useful uh to help us implement that idea but if you want to use a zero knowledge proof then you need to take the relevant part of your idea the thing that you're trying to prove and you need to express it as a circuit um and then after that you can use the proof system to actually create a proof and so this process of going from idea

to circuit i view that as what circuit languages are responsible for and that's what we're talking about today and it's it's a challenging problem um and it's not exactly clear you know because there are all kinds of different ways of of writing down ideas how exactly you'd go about this um so there's a lot of variety and in particular over the the past eight years or so there's been a real cambrian explosion in the number of circuit languages and their types and their features and and what they support um visualizing that as a timeline um i have up here a few of the different systems and languages that i'm going to talk about today um and so this starts back up back in 2013 with very academic projects like

pinocchio which probably most people here haven't even heard of um and and it goes up to changes and developments that have been happening in the past few months um so to make sense of sort of this extremely rich timeline i think it's useful to start trying to slice and dice these different languages based off of properties that they have um and one of the most important properties for any particular circuit language is what kind of circuit it's trying to produce and this is relevant because different kinds of circuits are used for different proof systems so broadly speaking the languages that i've shown on on the previous slide target one of three different

uh circuits they target a circuit kind of called r1cs which you can think of as a sort of a big uh single monolithic circuit um where multiplication has some cost and addition is free they might target planck which is which is quite similar except for it also allows for custom gates custom custom gates in the circuit and verifier randomness um or um they might be targeting air which is the circuit representation used by stark which is like not even really a circuit it's supposed to be sort of like ram random access machine like um and it has sort of a different cost model so this is this is sort of the first thing that you should wonder about any particular circuit language um and from this perspective most

circuit languages actually target r1cs um so this has been this this is because r1cs at least historically um has been the circuit that the fastest proof systems are implemented for um and as things like plunk and starks and air have become more popular there's been some need for languages targeting those kinds of circuits as well so there's a lot of variety here um another important axis is is the type of language um so broadly speaking i think circuit languages fall into one of three categories the first category is is that they're not even really languages per se but they're libraries written inside

some other host language that help you build circuits so you can imagine building the circuit by by issuing a whole bunch of api calls like adding wires to the circuits adding gates to your circuit so that's that's what a library is and and some some circuit languages are really more of libraries another option is to have what's called a hardware description language so this is um this would be a language for building circuits uh which um is sort of describing the layout of the circuit explicitly as in building wires and connecting sorry building gates and connecting them with wires but now not doing it through a library doing it through a dedicated language

and and sort of the final option is to have a real programming language where you have things like functions and you have things like variables ideas that don't really have a place inside the circuit itself and the idea is that the circuit language takes this programming language input and turns it into a circuit on the back end so you can imagine writing code in language like this would sort of be like writing code in rust instead of verilog um and so here is sort of an interesting and interesting taxonomy because historically we started with libraries and then sort of moved to hdls and have moved even further on towards programming languages this time that has gone on and i think that what's going on here is that what we'd all love to have is is a nice

programming language that we can use um to program zero knowledge proofs um and there's just sort of a substantial challenge in actually getting there um and that's why as time has gone on we've been able to do that more and more successfully and many of the newest projects on this slide are all on the right hand side they're trying to expose a programming language interface to zero knowledge so once we start thinking about programming languages for zero knowledge it's useful to think about the different features that we associate with programming languages and ask whether these different projects have been able to provide those features so one feature is mutable variables so here i have a function that's computing a sum using an intermediate mutable accumulator and you know there are other

ways to write some of course but sometimes mutable accumulators are are really what you're looking for um and and so the critical thing here is that you have this value that changes and that's something that you can't directly manifest in a circuit because circuits are state-free they're just a bunch of wires we're not talking about digital circuits with clocks we're talking about sort of compute once circuits and so mutable variables are our challenging thing to implement inside a circuit language and there's some variety in terms of whether or not languages support them so a lot of the older projects don't but if you look at something like leo or zinc or cairo or noir or zachary terpiquin these are all all systems that have some notion of mutable state that the user can interact with and then

of course behind the scenes that that mutable state somehow gets eliminated or replaced with an equivalent uh chunk of circuit another feature is is sort of the the range of primitive types supported so if i'm writing some some code in rust then i have access to all kinds of exciting primitive types i have access to booleans i have access to machine integers fixed with integers like u32s i also have access to ieee floating point numbers like f64s or f32s um and you might wonder hey what do i have access to in some of these programming languages that target zero knowledge well there's a variety so for some of the more basic systems all you have access to is is actually a sort of a new type that's not present at

rust which is the type of the underlying finite field that the zero knowledge proof has done over so so languages like circom and cairo um to that's my understanding they just give you this right you have fields um but um there are some languages that give you a little bit more um so booleans aren't too hard to do yourself but but there are various systems that arguably handle it for you these are the various um sort of like macro assemblers and circuit libraries that have gadgets that wrap booleans and then some of the the newer more high level languages also give you machine integers fixed with integers that have overflow semantics and things like that what about another feature not related

to the types themselves but related to how how we manipulate them and how we do control flow one challenging um one challenging thing to capture in a circuit language is if statements so an if statement in a programming language is a is what we call conditional branch so it's a test based on some condition and if the test passes then some codes and block of code runs that otherwise wouldn't run so here we have sort of a very simple implementation of power that that just raises some base to the power of a boolean so it's the powers that are um oh actually this is the function actually doesn't make sense now that i look at it but inside this if statement what we do is we have we have a condition that will square base if the if statement goes off

um and so this is an example of a conditional branch where inside the branch there are some instructions that get issued that have side effects that affect mutable state um this is something that's very challenging to support inside circuit languages but also something that programmers are very used to using um and so by and large um circuit languages don't support it um there are some that do so so bikin which is which is an old economic project did and most recently leo supports this as well um and cairo which is the language that targets air and and thereby target starks also supports this um kind of kind of by design because starks make it make it easier to support so this is yeah so if statements are one

area where there's this common programming language feature that many many circuit languages haven't implemented yet another thing that we're used to using in high-level programming languages is user-defined structures um so here i have a representation of a a compressed uh elliptic curve point so an x-coordinate and then something that tells us whether or not the y-coordinate is negative so this is an example of a user-defined structure um and and one might wonder whether or not circuit languages have this and the answer varies so there are some circuit languages that don't really have any user-defined structures at all so these are systems like circom that are that are hdls um cairo which is which is sort of uh

a self-claimed low-level language with um so that they don't have this um and then um also noir which is a new language that hasn't implemented this yet there's also classes of circuit languages that sort of don't need user defined structures because they're embedded in some host languages so this is these are the uh the circuit libraries per se things like bellman gadget libs and archie upa and in some sense they get a whole system of user-defined structures from the host language and so it's not as important for them to actually implement it inside the circuit on the other hand end of the spectrum there are some some languages that have just implemented this so socrates and zinc and bikini

they all had user-defined structures um and leo had had tuples which was sort of the nest the next best thing so i can't uh create a structure where all the different fields have special names but but i can create a structure where all the fields have numbers this is actually not a very hard feature to implement but i think it's just not necessarily been high on the priority list for some projects another feature one that we're used to in programming languages is the idea of an array so a chunk of elements that can be accessed at a data dependent location and so here we have an example of that so we have some array that's accessed at location i and you know we get the value out and we

double it and we put it back in the same location and and the nice thing about writing about looking at this program is that it gives us examples of both variable indexed reads and also variable index rights so line two or reading from this unknown location and on line three we're writing to that location um and these kinds of arrays are are actually very challenging for circuit languages to support because obviously circuits don't have arrays in them and so there's sort of a variety of approaches here so so there are many um many systems that just don't don't handle this there's no notion of array at least no notion of sort of a variable indexed writable memory um so bellman gadget lib and i believe upa are all all in this class um there are on the other hand there are

many languages that look at this problem and say okay well variable index arrays are really challenging maybe we can do something something simple or maybe we can just support constant indexed arrays so arrays where you only ever access them at um constant locations um so this sort of turns the array into some kind of like structure or tuple or something like that i mean there are various languages that support this so circom has this thing has this noir and leo all do when it comes to supporting arrays themselves the challenge is that it's not really clear how to implement them in a circuit one sort of naive approach um that actually in many situations is just the best that you can do is to implement them by what we call linear scans so you have the array be a

you know a big list of values and when you want to get the ith element you just sort of go down the list of values and you ask are you the ith element are you the ith element are you the ith element and then ultimately you get the element and you do similar things for a similar thing for writing to it um and this is the approach that the zocracy's language takes um so they implement this linear scans approach um and then beyond that there are things that you can do that are better so so bikini which is this academic project implements a sort of complex memory checking algorithm that that provides sort of better than the linear cost of doing a linear scan and then cairo because the target starks has sort of built in support for for large arrays in the form of the stark's memory

um and and so it can also do something a little bit better okay so that's been like a lot of information really fast sorry the the time constraints require this but let's take a step back and think about the message that we should take away from thinking about all these different features and the varying level of support for them across different circuit languages i think first and foremost the most important thing to take away from this is that the space is still evolving there are lots of different languages being developed and in some very real sense we don't really know what all the best design choices are yet so we really need to continue to explore and people are very actively exploring right now people in this call at the same time the problem that each

of these compilers is solving is extremely challenging so up here i have a visualization of kind of the algorithm that you need to efficiently check memory accesses inside a circuit which is shown on the right it's called it's called a permutation network this is an example of a waxman network and these algorithms are sometimes pretty complicated churning programming languages which have state in various forms in the form of memory in the form of control flow et cetera into circuits which don't have any state at all is it's a non-trivial transformation and the languages that are enabling this are working really hard um and so um and and this is where i do a little bit of of a promotion of a cause that i care about um

i i think that one thing that we should seek to do as we continue to explore and tackle the challenging programs associated um with compiling programs to circuits is we should try to share infrastructure as much as we can um so you know i i guess i would ask the question in the same way that llvm which is shown in the lower right allows us to take various high-level programming languages and compile them to different kinds of assembly formats in a way that that makes it easier to add new languages and new assembly formats i might wonder whether it's possible for us to build a similar compiler infrastructure for circuits that makes it easy to compile new high-level languages to new circuit representations um in a fashion that makes this easier for for a given high-level language and

for a given circuit format um and i've been thinking a little bit about this we've been working on on something in this direction called cersei you can you can find more information about it um at the links that are shown here and that brings me to the end of my spiel my taxonomy of circuit languages i hope that you found it interesting i'm happy to take any questions um and and i'm excited that after this we're gonna have talks from the language designers themselves who are really the authorities on on their individual languages hey very cool so alex i don't know if you can see any of the uh comments in the chat but there was actually quite a lot quite quite a bit of conversation happening um i know that there i think

there was a few corrections that maybe you want to peek into and see if if you could add those yeah yeah i'm gonna introduce i wanna ask folks here um if there are any further questions or anything else that you want alex to talk about yeah just put it in the group put it in the chat um i do there's one question maybe to ask right off the bat though so i think you would put going back to the very beginning alex was asking was wasn't pinocchio used in the first version of zcash oh this is a good question um i actually don't know the answer to that i'm sorry yeah oh and i think the answer there was z cash is written with lib snarks gadget

lib one maybe yeah yeah but that that's a statement about how they express the circuit and then so i think of oh i see this particular okay great yeah so pinocchio the compiler was certainly not used for zcash it's possible that the proof system that pinocchio built on was i'm not sure about that my impression was the answer is no but like everyone this is actually a question about your slides the the colors that you used for the different languages does that mean anything uh so um it doesn't so so early on there was sort of like a clustering effect like various things were often close to each other and i tried to sort of choose the color you know like for coloring a map i wanted to sort of four color the circuit languages but um

but after that it doesn't mean anything okay um zachery supports if else but the condition must be fixed at compile time um i don't believe it supports it for for the statements but zocardius does support if else uh expressions um with with sort of data dependent tests uh but that's not the same thing because expressions don't have side effects although that's yet another like sort of feature so sort of like ternary expressions is something that the various languages have cool all right here's a question do you think r1cs planck air share enough trade-offs and properties so that they can effectively share the infrastructure

uh yes i think that the answer is yes um so obviously like as things as the the back ends become more heterogeneous the amount of infrastructure that you can share decreases but that doesn't mean that it's it's not worth sharing what you can um so in particular like r1cs and flank have pretty similar opinions on how you express sort of most basic math um in my in my understanding um and at least i'm i'm sort of looking into operating on that belief and and trying to support flank and sort of the same infrastructure that targets r1cs cool