ZK HACK - Introduction to Domain Specific Languages (DSLs) - Alex Ozdemir

Transcript

next up i want to invite alex osdemir to the stage or screen i never really know what to say um he's going to be talking about the taxonomy of circuit languages uh we're going to learn more about zkdsls welcome alex yeah thank you anna um and so as anna said this this talk is going to be a bit of a gear shift compared to the last three um in that we're not going to be talking about how you build zero knowledge proof systems but rather an important ingredient in how you use them which is a language for expressing the property that you want to prove um so just a heads up this talk is going to be a pretty dense one in its own way and that we're going to talk about a lot

of different languages and i'm going to make a lot of statements about these languages and i try to keep this talk up to date with the latest and greatest developments in circuit languages but sometimes it gets out of date and if you notice any inaccuracies please let me know i i'll fix the slides right after this talk um so yeah so let's dive into it [Music] uh so taking a step back um the core problem that that all of the zk zk hack and zero knowledge proves about are about in general is that you have some high-level idea that you want some some property that secret data might have and you want to prove that the data has that property and zero knowledge so you want to go from this high-level idea to a proof and the proof systems that we've been

discussing so far today they will help you write that proof but the problem is that they probably don't consume the high level idea as it exists in your mind no instead in order to use a zero knowledge proof system you have to write down a circuit for the property that you want to prove and so that creates this problem how do we go from high level ideas to circuits and this is where circuit languages come in and this is what this particular talk is going to be about circuit languages are a really busy area right now over the course of the past eight years there's been a real cambrian explosion and exponential growth in the number and the richness of circuit languages uh here i just have i'll put up a timeline that shows some some prominent

languages and and when work on them began um going back to the early 2010s we've got tools like gadget lib which were really sort of like macro assemblers for assembling different gadgets within a circuit and pikin which compiled from a fragment of c to a particular kind of circuit and then just in the course of the past year and a half uh two years there have been a whole host of languages that have been developed noir cairo vo zinc and so clearly there's a lot of stuff going on in this space and what i try to do in this talk is compare and contrast these languages with one another look at ways in which they're similar and different in order to better understand the space as a whole [Music] so the first question that one might ask

about any circuit language is what kind of circuit that language is intended to produce and uh all the the languages that that i'm gonna be talking about in this talk target some kind of arithmetic circuit that is a circuit where the values of the circuit the wires carry finite field elements and the gates do some kind of algebraic operation like multiplication or addition um so some circuit languages target essentially just simple arithmetic circuits um there's a constraint format for this called rank one constraint systems or r1cs in this case uh you can have a circuit with additions of multiplications and the additions are essentially free and the multiplications have unit cost uh but there's another kind of arithmetic circuit format called planck which is the or i call it plunk but it's

the kind of circuits that the flank proof system can handle where multiplication and addition both have unit cost so in some sense it seems a little worse than r1cs but there's also some substantial advantages namely the proof system can support custom gates that do more complicated operations and also you can get randomness from the verifier which you might be able to use to uh to check some property or do some computation more efficiently so these these two formats are on and plunk these are true circuit formats in that they describe some bounded computation but there's another format air or arithmetic intermediate representation that's used by stark-based proof systems or similar um and the idea here is that you've got some arithmetic circuit you're not just

going to compute it once you're actually going to apply the circuit repeatedly so the circuit produces the same number of inputs and outputs and then you're going to repeat the circuit uh time after time um and so when you're designing for a repeated circuit you might imagine that you want to generate uh the circuit somewhat differently um you want to try to take advantage of those repetitions um so i call these kinds of circuits ram-like circuits because since the intent is to repeat them you want to design them a bit differently and the language is different that different languages target different kinds of circuits um so uh there are a variety most of the classical languages target r1cs bellman snarky gadget lib et cetera there are also some more recent languages that target the plonk sort of representation so noir and upa then alter block your authorization and

library for for building it uh and then there is a sort of a separate um branch of the tree uh languages that are trying to target air and so there are some lower level ones like error script or air assembly and then some slightly higher level images like cairo [Music] so that's one axis which is the kind of circuit that you're producing another axis in which the languages differ is what the languages are like at a high level um and so for discussing what languages are like i think it's useful to separate languages into three different types there are essentially libraries where the language isn't a standalone language instead you have a library inside some other language so you might have a rust library for helping you with circuit source plus library for helping you build circuits

or an o camel library for helping you build circuits um so that's that's sort of actually where this this project really started originally when people are trying to build circuits they didn't want to go through the work of building a standalone language they just figured they would create a library in their favorite programming language but beyond libraries people have designed what i would call hardware description languages or hdls which are essentially languages for building circuits that are in the style of verilog which is a language for building in digital circuits um the idea is to explicitly describe the layout of the circuit and what is connected to one this is in contrast with what i would call a programming language where there's some notion of variables and functions and mutation so something

that's trying to emulate rust and the different languages are different they fall into different buckets here so the languages that are really more of libraries are bellman which lives inside rust gadget lib which lives in c plus plus um snarky um and upa um and the the dominant hardware description language for zero knowledge uh proof systems and their associated circuits is circum and then there are a whole variety of more recent languages i would say are all trying to be true programming languages and one thing i want to emphasize about this separation is that it's somewhat blurry the boundary between a library and a programming language can be a little bit ill-defined uh libraries sometimes start to impose their own

semantics acquire their own syntax and look somewhat different from their underlying language and i think snarky would be a good example of this snarky is technically all camel but it looks rather different nonetheless this distinction can be useful um so when we talk about the move towards programming languages natural question is what kinds of programming language features are are hard to support when you're compiling the circuits and therefore are omitted from some languages that target circuits one feature that's hard to support in this in a circuit is the notion of immutable variable in particular inside a circuit there is there are no mutable variables every value every wire gets computed exactly once um and so

um this this can be a challenging thing to represent in a circuit and not all languages support it so in particular um the libraries and the hdls they do not support mutable variables and most of the programming language circuit languages they do support mutable variables in some form another important feature of any of any programming language is the set of types that that language has native support for uh so if we look at rust which is this this code is a snippet uh from rust then we have things like booleans we have machine integers integers of fixed width and then we also have floating point numbers

and not all these are supported by circuits by various circuit languages so almost every language supports finite field elements because ultimately we're compiling two circuits of refining field some some tools like bellman gadget live epa also add on booleans and then some languages go even beyond that and add support for machine integers so fixed width integers that can overflow and behave exactly like int or short or car and c [Music] another feature that can be challenging or even more challenging to support is the notion of an if statement so in a language that's going to run on your cpu and if statement is really easy to support you just have to emit conditional jumps in the assembly that

you're producing but when you're compiling to a circuit if statements can be hard to support because if you have some kind of side-effectful operation like a mutation inside the if statement sometimes that mutation happens and sometimes it doesn't and this distinction is made on a data-dependent basis in this small program we are either squaring base or not squaring it depending on whether the x bit is set this is actually quite challenging to support inside a circuit language um because you can't just view the mutated variable as like a new version like a new variable entirely unrelated to the previous one instead you have to do some kind of state merging where you sort of compute the change and you keep the original version and then you combine them

and so it's actually somewhat rare for circuit languages to support if statements that have side effects inside of them um and so the language is leo and pikin and cairo all of you support it and there are a variety of other languages that support ternary operators so if then else's but true if statements those are those are actually somewhat rare another feature that you might want from a language is the ability to define your own structures when we implement applications we come up with objects that are important to the application um but aren't important enough to go into the language itself or aren't as universally agreed upon to go into the language itself and so it's important for languages to have some ability for users to define

their own kinds of structures on this slide i have an example in rust that represents a compressed elliptic curve point so it's an elliptic curve point where we're storing the x-coordinate but we're not storing the whole y-coordinate we're destroying whether it's positive or negative and the idea is that this might be a more succinct representation of the elliptic curve point you might come up with other kinds of structures that are important to your application perhaps a transaction a vote something like that not all languages allow you to define these kinds of structures so noir and circle by knowledge do not some languages actually get user defined structures for free these are circuit languages that are really libraries in some kind of host language and since the host language abstract has some notion of user to find structure the circuit

language the circuit dsl gets it as well so bellman gadget live snarky upa all these fall into that bucket and then um for the standalone circuit languages some of them do support user defined structures so bikini zocrates zinc cairo leo all these support some kind of user defined structure another feature that can be challenging for circuit languages to support is the notion of an array so uh when you're compiling to a cpu an array is just a contiguous region of memory that you can access via pointers but in a circuit it's a little bit less clear what an array should be and in particular the most challenging thing to handle when you're interacting with an array is the notion of variable

indexed accesses so when you're taking the array and you're either reading from it or writing to it at a data dependent location so in this snippet of code we've got an array of length 4 and we've got an index i and we access that array at that variable index and then we write back to it at that same variable index this is pretty challenging to support when you're compiling to circuits um because in a circuit you don't have a built-in type for an array and you don't have any notion of memory so it's like what are you gonna do um nonetheless some languages do try to support it one way or another so there are a variety of languages that support arrays of constant indices but when it comes to variable variable indices x supports variable indices by doing a

linear scan over the array so every time that you try to access an array at some index it just checks every single spot and says is this the right spot is this the right spot is this right spot and so on and then it turns out there are some better strategies based on routing networks or other kinds of permutation checking machinery um in bikini and cairo support arrays via these more advanced techniques that yield better performance okay so this has been a really uh a whirlwind talk a lot of information very quickly i think it's worth taking a step back and and at least uh from my perspective advocate uh an approach to building certain languages that i think is useful um okay so what what can we when we think about circuit languages what lessons should we take away

um the first lesson that i think that we should take away from from the the richness of this ecosystem is that we need to keep exploring uh there are a lot of different languages they're they're so much divergent in terms of the divine design decisions that they've made and it's not clear yet what the right approach is people continue to build new languages they continue to have good ideas it seems clear that we need to continue to explore the design space of certain languages the second thing that one should take away is that when you're compiling to circuits from a high-level language this is actually a pretty challenging task there are certain features like array indexing that are very challenging to support but that programmers really expect and that programmers know how to reason about so up here on the slide i have a

visualization of the kind of routing network that is often used to check array indices um and the this is just one example but many of the features that i described during this talk are quite challenging for certain languages to support uh and i think that we in the same way that we're trying to explore the design space for what the language should look like what the syntax should be what semantics should be we're still trying to explore the design space for compilation as well we continue to come up with new compilation techniques for better representing different constructs inside a circuit and this work is challenging so given that there's still a lot of need for exploration and that the work itself is very challenging i think that one interesting idea is trying to share language share infrastructure between

different circuit languages so we might ask is there some kind of common library or common infrastructure that we can build that would help us as we build compilers that map various high-level languages that either exist or that we come up with to different kinds of circuit representations um and i think that it is possible to build infrastructure that fulfills this promise in some sense i've been working on this with some friends we call the project cersei for a circuit compiler there's a link to a paper as well as a link to the github repository on the slide and what we should hold in our mind as the north star when we do this kind of of unifying compilation work is a project like llvm which is trying to make it easy to compile from various high-level languages to different kinds

of assemblies what we want is something like llvm but something that allows us to compile from different kinds of circuit languages to different circuit representations instead of assemblies okay so this is the end of the talk and i'm happy to take any questions [Music] um okay is there a logic behind which features of these circuit languages or which features these certain languages support or is it simply due to implementation difficulty um i think that there's sort of two factors so yeah so one of the factors is just implementation difficulty uh some of the more advanced pieces are somewhat

challenging for compilers to support and so people just just don't do it um i think that's most of the time the answer um in some cases people will make claims like omitting variable mutation it makes it easier for the programmer to understand um and there might be some truth in that um but i would generally say that we should we should allow programmers to do more things not less things because i think that sort of the greatest barrier to new programmers using circuit languages is those languages being very different from things like rust or c that programmers are already used to so i think that the best thing to do in the long term is to support as much as we can [Music] is yes this is a question

is accumulation schemes here a term i've only heard recently related to persisting a value on each recursion um yeah so okay um so when you say accumulation schemes i think that what you're talking about is the tool for building recursive arguments or in general proof carrying data um but um closely related are accumulators or cryptographic accumulators um which can be used to implement array-like or memory-like abstractions within a circuit um so so accumulation schemes not particularly relevant to the design of circuits to my knowledge

but accumulator schemes highly relevant and this is a kind of cryptographic machinery that you can use to prove that you're interacting with some memory um in a fashion that's consistent in that like if you write something and then later read it you get the same value [Music] oh my audio's a few broken [Music] i'm glad that you guys can hear me i cannot hear you no no i'm muted sorry my bad okay um it does seem like there's some last questions that just rolled in i don't know if you got a chance to answer these

ones um one is about cairo yeah here actually this is not about cairo another one okay um someone yeah so someone must have written or already worked on some kind of llvm based system um so there is a little bit of work in this direction um actually not for zero knowledge but for mpc the project is called cbmc mpc and so what they try to do is build an npc compiler based on uh cbmc the c bounded model checker which is sort of based on llvm and the challenge that you run into here is that llvm because the target's assemblies is sort of doing all the wrong things um so in particular assembly languages have extremely efficient memory and extremely efficient

jumps and so llvm tries to use those things better and all those things suck in circuits so llvm sort of takes you the wrong direction um in terms of sort of building a new compiler infrastructure that's oriented around the design of circuits and not assemblies um i guess we've worked on that um but i'm not aware of a lot of other work that's trying to do the same thing there are some sort of vaguely related things very far from cryptography in the realm of model checking [Music] uh and then understanding cairo's place in all of this yeah so cairo is a little bit different right because it's targeting air um it's targeting these these computational

models that are intended to run continuously um and that's why yeah i i have sort of the cairo and some of the other languages that target air as being somewhat separate um from the rest of the second languages um but i think it's worth noting that even in the case of cairo uh the arithmetic representation error that does um describe some circuit that's going to be repeatedly applied um and so some some of the same techniques might be useful when compiling cairo to air or similar languages there all right i think that wraps up the questions unless there's yeah i think we're good alex thank you so much for this talk and for sharing

um yeah i've seen some clapping in the back in the backstage from sort of cool looking aliens anyway yeah thanks a lot and