High-level programming languages for zkSNARKs, an overview - Harry Roberts (Ethsnarks)

Transcript

So, I'm Harry. I've been working on EthSnarks for the past year or so. Um and one of the biggest problems I've found is people don't like programming low-level snarks. Uh and I wanted to look more into the challenges of high-level languages and making it accessible to people. So, I'm going to go through some of the history. Um and slides and notes and stuff will be at the end. Um so, I'm going to go through some of the history and some context about what the difference is between snarks, uh multi-program, multi-party computation, fully homomorphic encryption and computers.

Then look into like if you are making a high-level language, how would you compile something you're familiar with into this sort of low-level structure. And try to give a sort of a timeline of where we've come from, where we're going, and then give you a really good overview of all of the different high-level languages that are available if you want to do programming with snarks. Um so, I want to start with this side. This is where I think we are with the industry as a whole. It's uh it's not very mature, but it's really interesting and there's lots of interesting stuff.

And of course, the slide that everybody has to have is what are snarks? What are ZK-snarks? Um and the biggest thing for me is that they're compatible with Ethereum. Uh they've got optimal proof size, and they're really quick to verify. So, these three things that have really uh make it useful for me. And of course, there's lots of research, privacy and anonymity, computational compression. Um but if we look at more of the history of So, with regular computers, we've got a 50 years of research into compilers, optimizers, and languages.

With MPC and fully homomorphic encryption, we're working with the same kinds of contacts. We've got binary gates and you've got the the universal gates that from there you can construct anything else. Um but with SNARKs, we've it's a new domain. It's it's relatively young and everything's different. So, everything that we rely on all of the history uh if we look back at the history of uh where do we come from with regular computers? We're building on the the the shoulders of giants. So, you've got Boolean algebra through the digital logic and circuit synthesis and then the branch of modern compilers and optimizers and that's going back 150 years or so.

And at the bottom here, we've got like a big history of thousands of years of algebra and then SNARKs. And a lot of it's uh relatively new and there's we're trying to find common bits between these. So, that instead of developing this stuff from scratch and making all of the same mistakes, we can rely on a very rich history of uh like formal logic analysis and uh modern compilers and optimizers. Um so, yeah, it's uh we want to rely on uh the history of computer science rather than making ourselves. But for that, we need to understand a bit about what is the low level and why is it different? I'm I'm sure in the the

last set of slides, he's gone over some of these differences. But I want to walk through a problem or two and show you like uh conceptually, why is it different? And uh of course, I'm only going to be focusing on the small program and circuit part, which is if you've got a program or if you've got a your normal way of thinking is to write sequential programs. And how do we translate that into a circuit that fits into this big diagram? Um and I'm going to be focusing specifically on uh if you look at a the model of a regular compiler, how do we go from whatever your front-end language is to generating code and then optimizing it and transferring

it to the lowest levels? So if we start off with really basic example, on the left you've got a sort of procedural program. Then you've got a the circuit representation of it. And then you've got the sort of mathematical equation. And what we're doing is uh translating everything into uh a circuit where you've got a um a set of variables which are constant and immutable across the whole program.

And it with a regular compiler we'd call this static single assignment. Where every single state of every variable is a distinct global state. Uh and you don't have state, you don't have uh you can't modify variables. So instead of overriding an existing variable, you're creating a new variable. So we go through, you've got A which is 10. Uh you've got B multiplied by itself, which is C. And then you add A and C, and instead of getting A again or overriding A, you end up with A prime, which is its own distinct state.

Um and as a whole, breaking the program down from the representation on the left into the representation on the right is the sort of first step you'd go through if you're trying to compile a language. Uh so we go through a slightly more complex example which highlights that as you remember, additions are free. Um but uh how do I put it? The they're also different concepts from uh computer science that can rely on.

For example, instead of having a for loop where we're overriding the value of Y with the incremented version or with the value of the array, uh we're really reducing the addition function on the list to create a sequence of outputs which are distinct values where the last one represents the sum total of every item in the array. Um so, the problem is we we don't have any loops.

We don't have any if statements. Everything's always evaluated. All variables are immutable. And as you said in the last uh talk, we only have these add and multiply operations. So, you have to translate every problem you could possibly want to program from the representation on the left into these circuits where the entire circuit uh you can't have a an infinite loop or you can't have a non-deterministic loop because you have to draw the entire circuit.

And you have to be able to look at it from a high level. And you've only got a limited amount of space and that could be say, you know, couple of hundred thousand operations or a million or so. But if you were to add a an infinite loop in there, you need an infinite amount of space to draw the circuit upon. Uh Oops. Um so, this is a the process of flattening code where you're taking uh a set of statements and then turning it into the flat, almost visual representation of the circuit where everything that it could possibly do is known.

And the next thing you need to do is uh to evaluate it just like a real circuit. This is uh the processor or the the die that you're working with. Um So, anyway, you've created these circuits and you've got your your add gates, your multiply gates. They're strung together. But uh how do we convert them into uh constraints? Well, first we should probably know what constraints are. Um Essentially, you've got a uh multiplicative operation that you've got A * B = C, a linear combination, which is the sum of terms, and each term is a variable multiplied by constant.

So, with your circuit, you've got lots of different variables that you can rely upon, but they only have one value. But the circuit can also have the built-in sort of hard-coded values, which are the constants here. So, if we It's just a piece piece of Python code here that if you want to run, you can. But it sort of accurately represents the system or domain that you going to have to work in. Um So, if we look at how do we take one of these circuits and transfer it into or convert it to constraints?

Uh so, if you have a the B squared operation where you multiply B by B and you end up with C. Um But then in the yellow, I've got a these built-in constants or the uh the sum or the uh non-variable values that are sort of built into the circuit. So, I've got 10 here, which is a constant. Um So, anyway, this is the process of uh converting a circuit into a set of constraints.

Where at the end you have uh three different operations. You've got the two multiply operations and the one addition operation. But instead of translating them into three different constraints, you can condense that down into two constraints. Where the set of constraints verify that uh your circuit is operating as you intended it. So, rather than evaluating each of the operations by themselves, you're saying that if all if I plug in all the values of the variables, then the only values of the variables that will be valid are whichever ones that match the set of assertions here.

So, if we take a more kind of complicated example, we're looking at a If you want to translate an algebraic expression like this into a set of constraints, um you need to first find what are the the mult which operations are multiplying something. And split them out into their own common subexpressions. So, because with a constraint, you can either add a set of things in one of the the terms as a linear constraint, or you can multiply two things together. So, you're constrained by the multiplicative complexity. So, if you can only multiply

two things together, you need to break these out into multiplications and then find the sort of common uh expressions and uh common terms there. So, we can take these out and then we have a a constraint for each of the multiplications that occur in the equation. And then we can uh multiply those intermediate values by each other to create the next expression. Um and then at the end we end up with the sort of more complicated constraint down at the bottom which ties those all together and says that uh

if we take 1 + d times x y whatever um then we're saying that a a point that is if you take the x and y of um two curve points which have been added together and you fill in all of these intermediate variables then you can verify that uh it's uh you can verify that it's only those two curve points could have been added together and they must be valid curve points as well.

um So I guess the the sort of high-level view of this is you have the secret inputs and the public inputs and you're trying to compile your program down into a circuit. Uh and from the circuit you generate the constraints and you also evaluate the circuit to create the variables which ends up at the sort of intermediate state um which is inherently linked to the proving key and the proof. Uh and then from that you create the proof. Um so I've tried to give a fairly bad overview of like what is the low level.

Um but the sort of high-level points you can get away from those there are lots of really interesting techniques for uh optimizing if you understand the form of the constraints and how to translate uh your high-level problem in a way that you are used to programming into this different model. um Ver- and also verifiable computation is a bit of a paradigm shift where uh it's completely unlike sequential programming. You have no state. You have to constantly rethink of your program as it were like a circuit board and everything is wired together.

Um and then also lots of interesting things where like high-level algebraic concepts are quite easy to transfer over to this model, but if you're working with bits and bytes, that could be 200 or 250 times more expensive than um doing something like this. Where instead of six or seven constraints, you end up with maybe hundreds or tens of thousands in order to do something that's very similar to how your computer would do it.

Um so next time I want to give a sort of overview of like what is the high-level languages that are available. So if you want to uh start programming with SNARKs and you're only familiar with like normal high-level programming, you like Python or C or basic, whatever. Um I'm going to go through a handful of different projects which provide you these sort of frameworks or compilers or interesting starting points and one of the simplest ones is called Go SNARK, where you've got a very, very simple language that uh uh it's very close to the constraints.

So you essenti- essentially got multiply operations variables functions additions and you don't get much else, but if you can translate your problem into that, then you can use it to do anything that SNARKs can do, but it will be very verbose. Uh I'm not sure if it's a theorem compatible, but uh it does the flattening and it's maintained. Um so another one is a very simple language where they've taken the uh tried to represent the low-level constraints in a Lisp-ish form.

Where again, if it's very low-level, but if you can convert your high-level idea into a very limited subset of the language, then you can do anything that SNARKs can do. But, it probably won't be pretty. I'm not sure if it's maintained, and it's not Ethereum compatible. Um then we've got SNARKY, which was mentioned in the previous talk, where it's essentially an a Camel library, where you can do lots of interesting uh you've got full use of the whole range of Camel higher-order types, and you can do interesting optimizations because of that.

And it's Ethereum compatible. It uses libsnark as a back end. But, it's also maintained, and it's got uh lots of really good libraries for it. Like, you can use all of the libraries that are written for Camel, and it might be able to spit out constraints and SNARK code for you. So, for example, you've got a uh the the array reduction, you've got tree structures, um and it might be interesting to see how far can you go with that, and how much OCaml code can you reuse that also happens to be SNARK compatible.

Um but, the more interesting thing for me is uh it more more accurately represents uh the process we're used to with regular compilers. Where you've got a C source file, and then the Pinocchio compiler, which converts into an intermediate format, which is kind of similar to like a SNARK-specific assembly language. Uh and then spits out these opcodes here. The problem is it's a very academic project but they've done they broke new ground in terms of uh how do we make this accessible to developers who want to write a zero-knowledge SNARK program but don't want to have to deal with the

low level. And they tackle this by giving you a C compiler. Um so the C compiler if we look through uh we've got uh the instructions that it emits take the the form on the left and you can see a circuit representation on the right. And for each of these instructions instead of being these non-deterministic constraints, you can evaluate them like they're assembly language. And as they're evaluated, they will fill in the intermediate variables and also emit the constraints. So you can compile your C source code to this intermediate language

and then provide maybe like the binary version of your program and somebody can execute that without needing the source code or the compiler. Uh and then from that generate the witness or create a circuit or create a proving key or whatever you you need to do. Um but they came across one problem, which is writing a C compiler from scratch is not an easy problem, especially if you want to be compatible with uh everything and you know the the 30 to 50 years of C source code out there.

So Geppetto, which is by the same people uh as the the next project was to reuse LLVM. So if you take LLVM we're building on the long history of sort of commercial-grade compilers of uh all the insights into optimization, all the uh literally hundreds and millions of man-hours of work that's gone into LLVM. Um so they don't have to write the C compiler themselves, but they next had the problem of well, how do you translate the intermediate language that LLVM emits and then convert that into R1CS.

Uh I'm not going to go into details, but uh the source code is available. It's written in F sharp and some of the C++. And it does a reasonably interesting uh good job. But it doesn't give you access to all of the the interesting things that SNARKs can do. So, you don't have native field types. Uh so, you're never going to be able to get as efficient as if you had have constructed the constraints yourself and worked around uh working with prime fields.

And everything's written in bits and bytes, but it it does a good job. And then the next thing we have XJ SNARK, where it's a a high-level language that looks kind of like Java or JavaScript. Um and it allows you to do really uh you can write uh for example, uh you've got RSA secret key knowledge, where they've created abstractions for you. So, you you can deal with uh 2,000-bit numbers. You can deal with prime fields.

And it hides all of that neatly for uh it hides all of it neatly away for you. And it's a very good optimizer. So, this is a very promising project. It's also a theorem compatible and it's maintained. But you need to have an IDE in order to be able to write the source code for it to understand what you're doing. Uh then there's the Pepper project, which took inspiration from uh the Pinocchio project, where they wanted to create a C compiler that can uh translate into constraints and um and they started off with the sort of initial project. And they've since worked through Ginger and Zatar and

Allspice and Pantry and Buffet and Zebra and Giraffe and onto Pequin, which is the sort of latest version of that. And through this sort of history, it's each one has been an academic project where they've been trying to solve uh a significant problem. For example, how do you have a processor that can uh how do you syn- synthesize a processor so that you can verify that's been run and so on. Um so generally speaking, uh you've got a interesting optimizer, you've got good C language support.

And you can take functions like this and then uh convert them into a ZK snark circuit and evaluate them. And a lot of people seem to be having uh this makes it very easy for them to pick up, write in a familiar language, and then create ZK snark circuits and programs that uh have or theorem compatible. But one of the the problems that was similar with uh Geppetto and with Pinocchio is you don't have access necessarily to the low-level field types.

So, many operations you're using are still doing bits and bytes, but it gives you structures and arrays and all of the stuff you expect. Uh another interest Okay. Another interesting project is you've got Circom, which is a JavaScript library. Um it separates constraints and evaluator with the code. So, you've got a set of constraints and it's very easy to pick up. And then you've got Socrates, which again, you've got conditionals, loops, arrays, a Python-like language, optimizations, and theorem compatible.

Uh None of them are really ideal, though. But I was trying to think, what is a good ideal? And essentially, it's to split the different projects into their abstract components so that we can hit all of these goals and be able to reuse some of the things we want to do. Uh, but if you want to use uh, ZK-Snarks with Ethereum, I'd recommend these four projects here. But, one thing we're missing is how these projects work together.

And essentially, they have no intermediate language. They It's very difficult to reuse advances that one project has made with another project. Um, and yeah, I just want to say thank you.