zkStudyClub: Unifying Compiler Infrastructure for SNARKs, SMTs, & More w/ Alex Ozdemir (Stanford)

Transcript

All right. Welcome everyone to ZK Study Club. Uh today we're very excited to welcome Alex Ozdemir who's going to be talking to us about uh compiler infrastructure for taking Yeah, taking um programs and compiling them into SNARKs, SMT solvers, etc. And so he's presenting his joint work, which is uh up on the screen here that he uh did with um a colleague Fraser Brown and uh Riyadh Wahby. And uh with that, Alex, we're very Thank you very much for coming and uh and speaking to us today and uh looking forward to your presentation. Over to you.

Yeah, thank you, Alex. Um so So, as was advertised, I'll be talking about some work that I recently did with Fraser and Riyadh on what I would see as one of the the greatest barriers to bringing SNARKs to new applications. Um and that is this problem of of compilation, surprisingly. Um so, up on the slides, I have a picture here where on the left-hand side, someone has an idea. Some idea that seems like something that could be proven in zero knowledge, that would be useful to prove in zero knowledge. On the right-hand side, I have the logo from ZK Podcast, which represents a zero knowledge proof. And the question is like, what does somebody have to do to take their idea and turn it into an actual zero knowledge proof?

Um and the the challenge is that what you have to do right now is you have to go through some kind of arithmetization. You have to turn your idea into R1CS, which is a kind of arithmetic circuit format or some other arithmetic circuit. Um and so, before you even get to zero knowledge proof part, you have this compilation problem, which is turning your high-level idea into arithmetic. Um and that compilation problem is is what this talk is about. Um so, I I've kind of cut down on the number of slides in this talk and and my hope is that that will leave us space to take questions interactively. Um if there's anything at any point in time that's confusing, just just ask me about it.

Uh R1CS is not the only relevant um arithmetization, but carry on. Yes, totally true. I I I I pick it here as as an example, um but I think actually one of the most exciting things about this work is that we don't believe that it needs to be specific to R1CS at all. Um Uh and we've been exploring R1CS so far, but but um Well, well, we'll you'll see. Um okay. So, as as sort of a motivating example, um if the general idea isn't isn't exciting enough, um I want to pitch like one one idea that you could imagine applying zero knowledge to, which is bug bounties.

So, the way that bug bounties work are that you have some kind of code um that is very important. Um so, here I have a snippet, a real macro from OpenSSL, or it used to be in OpenSSL. I'm sorry, was there a question? No, I think someone just joined with a bit a bit of background noise. No Got you. Um yeah, so here I have a a macro that used to be in OpenSSL. Um real code, but but no longer there. Um and the way that bug bounty systems work is that you have some kind of code base owner, who I've represented by a genie in this in this picture. Um and they're interested in finding bugs in in this code um because and and so, what they do is they offer a reward to anybody who turns in a

bug. And the idea is that they're incentivizing people to report bugs instead of trying to exploit them. Um and and so, the idea that they're hoping is is that someone, a bug finder, will come and they'll look for bugs. And if they find a bug, they'll send it over. Alex, there is a you know, information arbitrage there. So, if you really find a zero day, so I used to be in OpenSSL list a very long while back, dev list. So, if you find a bug and if you don't really have a fix for it insidiously, the window opens up. So, I guess what the scheme you're going to propose could be like super interesting.

Yeah, yeah. No, I think that this this like handover is is challenging and it's good to ask about like what the incentives are. And and and and so, like in particular, like one question that the bug finder has as soon as they hand over these inputs that demonstrate the problem is are they actually going to get paid? And and this sounds like kind of like paranoid, like, oh no, these code base owners, you know, that it's not like they're malicious, but but often times what a bug is is somewhat open to debate. Um and there can be a lot of debate that ensues. And we say this from experience. Fraser has lots of experience filing bug bounties against browsers. That's what she does all the time.

Um and and you know, it it's not even necessarily that the code base owner is malicious, but just that they're being obtuse or or disagreeable. Um and in the back of everyone's mind is once you hand over the inputs, the bug finder no longer has any leverage here. The In some sense, the code base owner has already gotten what they wanted. Um and so, you could imagine applying zero knowledge to this problem. Um and so, just theoretically, what you would do is have the bug finder hand over a proof that they're aware of some vulnerability in the system. Um and now you can go into that negotiation phase on equal footing. Um so, maybe the bug finder also hands over the bug to some kind of escrow, and then you you can do a sort of a clean

exchange, um or maybe we just have the code base owner pay first once they've verified there's a valid bug report, and and then they get the actual inputs. Um this opens up the space, uh the design space. But it's not quite possible right now. Um and the reason or or it's not immediately possible, at least. And the reason is that uh the same reason that it's it's hard to apply zero knowledge in general, zero knowledge applies to these arithmetic formats. It doesn't apply to your high-level programs in C. Um so, if you're if the if the definition of your bug is about some C macro, um then essentially you need to be able to compile C to R1CS.

Um and this is just one instance of the general problem, which is that we need compilers from high-level languages to R1CS. And I like the bug bounty example because it makes clear what two properties these compilers need to have. The first property is they need to be efficient and that they need to produce small output. This is important for zero knowledge because uh the cryptography, the speed of the provers and the memory usage of the provers, depends on how big your R1CS circuit is or how big your other arithmetic circuit is. Um and also the compilers need to be accurate. And sometimes people ignore this, but it's extremely relevant to the bug case. Um and it's and it's it's relevant to to good design of systems in

general, which is that um if you want your proof about this arithmetic circuit format to mean anything, it needs to accurately reflect the intended semantics of the statement. So, if I have some C program and I compile it to R1CS, and I want the proof to mean something about the original C program then the R1CS needs to accurately capture the semantics of C. So, there are these two goals for for building these compilers. One, the efficiency of the compiler, and two, the accuracy. And they're both important. Um and and in different situations, they have different levels of importance.

So, since this is an important problem, people have been very busy uh working on it, including some people in this call, I believe. Um and so, I have I have a diagram here. On the left-hand side, I have a a whole bunch of languages and compilers that are that help you build SNARKs. Uh if I forgot yours, I'm sorry. It is It is ignorance, not malice. Please let me know. Um but just to to survey this space, I I we have a whole bunch of different kinds of things going on here. We have languages that are very low-level, like Circom, that are almost like a hardware description language where you're like assembling a circuit. Um and then we have languages or compilers that purport to be very high-level, like Beguin, which is an academic research project that attempts to compile C to R1CS.

Um and and uh I'm also lying a little bit in that not all of the languages in here actually target R1CS. Some of them target other arithmetic formats. Um so, like uh Cairo, for example, does. Um Uh but but to to at the highest level, all of these are are languages that are being compiled to arithmetic circuits of some kind or other. Um and and what I want to emphasize about about these projects is one, that there a lot of them are very good. Like they they achieve efficiency or accuracy in in some good way. Um Many of them involve a custom high-level language that was designed just for the compiler that that compiles them.

Um and uh finally, that that there's a lot of duplicated work. Um and and with a lot of duplicated work, uh there's a lot of spotty coverage. So, you know, uh I I have a pure Beguin. Beguin allegedly compiles from C to R1CS. It doesn't really do that very accurately at all. It makes all kinds of assumptions that are not at all consistent with with the C specification. Um and the reason is because they were really focusing on the efficiency side of things. And and and you know, people have so much time and and so much resources. And as my uh college professor would say, only so many beans of cleverness.

Uh and they can't they can't afford to do everything well. Um yeah. So, so people cut corners to achieve their specific goals. And and this this work ends up not just being duplicated, but sort of duplicated spottily. Um so, what one fun exercise that I do with these different languages is I get out their compilers and I hit all the sort of edge cases that I'm aware of being hard to compile. And and usually each compiler covers about half of them. Uh that's that's my typical experience. Um so, again, not not to throw shade. This is a hard problem. And and people have been really heroically trying to take it on one of the uh again and again.

Um and so, our our um observation was that even though there might be different high-level languages that that want to compile to arithmetic um at at the highest level these these different languages are not are not so different. Um and what we have is really a more general compilation problem. So, on the right-hand side I have some arithmetic circuit. Um and on the left-hand side let's just say for now that we're compiling C to this arithmetic circuit. Uh if you think about the features, the important features of this compilation problem, they're as follows. The circuit format is defined by being state-free um or having extremely managed state.

So, there's this idea of every value in the circuit has exactly one value. There's no notion of time, things do not change. The circuit format is non-uniform. So, uh what we mean by this is that it operates on a set size of input. Uh so, like high-level programs can operate on lists of any size. Uh that's not the case for circuits. They're stamped out, they have static size, they operate on so many inputs and that's it. If you want it to operate on a different number of inputs, you need a bigger circuit. Uh and then finally the circuit format, because it's going to be used inside of a cryptographic proof system, is is in some sense non-deterministic in that there are these existential variables that can be prover-provided um that you don't have to compute. You

just have to check the validity of. Um and that that's sort of like an interesting complexity theoretic feature of this computational model that there's this prover that can give you values that you just check, you don't actually have to compute yourself. So, that's how what defines circuits. High-level languages are quite different. High-level languages first and foremost are are generally stateful. Uh so, they have things like mutable variables. They have these boxes that you can put values into and then later on you can put a different value into the same box. Um and intricately connected with with this statefulness is the idea of control flow that that you can in different situations, according to different inputs, take different actions.

Not all code executes in every execution of the program. High-level languages are also uniform. They often uh you you can write down functions that operate on inputs of variable size um and you can use the same function for all these inputs uh and the only difference is that it uses different quantities of resources. So, if I write a a function in Python that sums a list, it's going to take longer for a bigger list, but the same function will do the same job. Um so, if you think about the compilation problem as going from specific some specific language like C to R1CS, then then it seems very specific, but when you look at these lists of features, you realize that these features are actually shared with many other circuit formats on the right

and many other high-level languages on the left. Um and if we start to just think about the circuit side, um we see that similar circuits or so or I have circuits here in quotes cuz they're not always called circuits in their respective community. Um but but similar circuits are used in SMT solving and SMT-based verification. We would argue that SMT formula are are circuits in the same sense. Circuits are also used for optimization. Um so, if you want to use an integer linear programming solver or some other kind of um real real optimizer um or a rational optimizer, then you give it a circuit format, something that's state-free, something that has non-deterministic semantics.

Um and even if you want to do a multi-party computation multi-party computation-based systems are are built on either arithmetic circuits or Boolean circuits, depending on the underlying machinery. Um and uh and those also are are state-free and non-uniform. The non-determinism there is it's easiest to say that there just isn't non-determinism. You can kind of slip a little in if you want. Um so so since we we observed that this this problem is actually more general, our our idea behind this project was to say, "Okay, um rather than trying to to continue to build uh one-off compilers from specific high-level languages to specific circuit formats, let's try to build a common infrastructure that

supports these compilers in general." Um so, what we envision is that CirC, which is our infrastructure, is sort of um a rail a railroad switching ground uh that's going to help you compile any high-level language to any kind of circuit format that you're interested in. Um and the hope is that by looking at this process in the abstract and by pulling as much of the compilation machinery as possible to a common level of abstraction, you're going to make extending this machinery to specific front-end languages and to specific back-end circuit formats far easier.

Um and we've had some success with this, which which is I'll be telling you about over the course of the next 45 minutes or so. Um so, in particular um the what I'll be telling you guys about is our work building um or extending CirC. Uh first of all, building CirC itself. I'll I'll tell you about the way the infrastructure is designed. But we've also gone through the work to extend CirC to a subset of C, to uh the complete Socrates language. Um and we've built back-ends for CirC uh for SMT solvers um and also for cryptographic proof systems.

Um specifically for R1CS and and we specifically connect it to Groth16, but but um the proof system itself is not so important. Can I ask you a quick question about the name? Yeah. CirC, is it any reference to like the what is it Greek mythological witch? Circe? Yeah, it's it's not. Um it In fact, Riadh chose the name and I I think his idea was to be cutesy, not not terrifying. Okay. Uh it stands it stands for circuit compiler.

Got it. Um And one other thing is Anisha asked in the chat here, can you borrow anything from LLVM? Oh, sorry, I can't see chat without advancing my slides. That's why no no, you don't need to. I'll or myself or Alex will jump in and share that. Cool. Uh that's a great question and that was our most important question when we started this project. Um and when we thought about it, we concluded that that actually LLVM um is is almost wholly incompatible with what we're trying to do here. And and let me let me say why. LLVM is a compiler infrastructure that's built around a particular computational model, which I call the RAM register model.

You have some machine with lots of memory and lots of registers, less less registers than memory, but but still registers. And uh you can branch and manipulating registers, changing their state is cheap. Um and so in some sense LLVM is very built around memory and state changes and those in our context are both very expensive. So, LLVM sort of optimizes in the wrong direction. Um if if you want to look at this basically the complexity theoretic observation that we would make is any compiler infrastructure has a computational model that it is totally married to. And LLVM has attached itself to the RAM register model and we're attaching ourselves to the circuit model.

So, can I ask a follow-up question? Yes, please. So, if you have a BNF kind of structure, will that be in the right direction in the opposite direction? Um when you say BNF, what do you mean? Uh you have trees and then Ah, yes. Yes. Um that's I think that's like more getting into our direction. Yeah, like if you have some kind of branching program. Um yeah, I think that's more getting in into our direction. Um Thank you. Yeah. And also I want to say we we didn't believe LLVM as as an infrastructure solved our problems, but like building a front-end for LLVM is not totally out of the question. And we just think there would be like some very serious performance challenges there.

The reason I asked is like they have built the whole pipeline, right? So, I I know I've talked to some some other people who have been working on solvers, so kind of know, but uh if you think about a compiler construction toolkit, LLVM gives us the best we can actually get at this moment in time. So, effort-wise, once you build a compiler, then the tool chain is there then everything else becomes handled. That's what I was thinking. Yeah. Yeah, for sure. Um Yeah. Yeah. And and certainly people who the use of SMT solvers inspires most of this work. Uh in my in my other life I'm an SMT solver developer, so I'm very familiar with that world. Um and and we're drawing on that uh extremely. Like basically all of our algorithms are are from the SMT compilation literature.

Okay, so let's talk a little bit about how how we build this common infrastructure now. Um so, the the core picture is is this one. Uh so, on on the front end of CirC, you're going to have modules that target specific high-level languages and are tasked with with turning those languages into some kind of CirC IR. Um which is going to be a circuit IR, not like LLVM. Um and these different modules are probably going to draw on common libraries, um but we can we can conceptualize them as different for now.

Then in the middle, um you're going to have uh some optimization machinery that's going to transform the circuit format, maybe try to make it smaller, maybe try to replace high-level constructs in the circuit format with simpler ones. And then on the back end, you're going to take uh the optimized circuit representation and turn it into a representation that some specific constraint processing system can handle. Um so, in the zero-knowledge case, you're going to be trying to turn this into R1CS or air or or some other kind of arithmetic circuit format. Um and in the SMT case, um you would want to turn this into an SMT formula.

Um so, just to to give you a an illustration, uh an animation of how this would work, you're going to start with some high-level program and you're going to feed it into the right front end. The front end is going to produce a circuit format, so or like a circuit IR. Um that IR is going to go into the core of CirC. It's going to get optimized. You're going to run and rerun optimizations. Um for those of you who know about how you design sort of multi-pass optimizing compilers, um, but after you've you've optimized your heart's content, you're going to hand off this circuit representation to some back end. Um, and typically what we're going to be interested in for the purposes of this talk is is the proof system back end. Um, but just for for the sake of variety, we'll say this time

you give it to the SMT back end. And it spits out an SMT formula, which you can then go and ask an SMT solver about. So, you can say, "Hey, this this circuit represents a violation of some property that must hold in a program. SMT solver, can you find me a violation?" Um, so what I'm going to do for the rest of the talk is go it's go through the different layers. Um, we'll start on the front ends. Um, and the the reason that the front ends are important is because in a real way, the kind of extensibility that you want most often is the extensibility to new target languages, to new high-level languages. Um, and the the way that Circe achieves that front that that flexibility is by making it easy to build new front ends. Um, and

so, um, in some sense, like this is the most important extensibility access. So um I guess I'll give you kind of like the results first. Um, in order to to to figure out whether or not our our idea of what would make it easy to build a new front end actually made it easy to build a new front end, we we tried to build a new front end. Um, and we we built one for Socrates, which is a language that was designed to be efficiently compiled to R1CS. Um, as far as we know, the project started in 2018.

It might it might have started earlier, but not been public, unclear. Um, and it's it's a pretty good piece of software. I I like when I use their compiler, I I I enjoy using it. Um, it's it's yeah, and and on the whole, it's a it's a pretty well-developed software project. Um, so if you look through the code base, and count the lines of code, excluding things like ASTs or whatever, it's there's like 28,000 of them. They're in Rust. Um, most a lot of that is is moving the compilation process itself, as well as a number of optimizations. And and they get really low-level in their optimizations. They have some SHA-specific stuff that's looking for majority functions, and looking for bitwise ITEs.

Um, it took some time to build this this infrastructure. Um, I guess the project's been going for 3 years now, and there are 36 contributors. And on the whole, I would say they produce pretty good output. Um, it's it's rare that I feed something into the Socrates compiler, and I think they could have done like orders of magnitude better on that. Um, so they they generally produce pretty small R1CS for the language that they support. Um, although it's worth noting Socrates language is somewhat restricted. There's no data-dependent control flow or stuff like that. Anyways, so so our our we set out to build a I guess another compiler for Socrates based on Circe, which in amounted just to to building a front end to Circe that handled Socrates.

Um, and and we were able to do that. And we were able to do that quite easily. Um, so ultimately, our front end is only 700 lines of code. Uh, it was built in in 1 week by one person, me. Um, and uh and at the end of the day, it actually produces output that is on average better than what Socrates Socrates compiler produces. Uh, not always better, but but on average better. So, let me let me show you the plot for that. Here, we have a diagram where we've taken various uh circuits from the Socrates standard library. Those are on the X axis. Um, and the Y axis is the constraint ratio. So, it's the number of constraints that Circe produces when it compiles the circuits, divided by the number of constraints that the Socrates reference compiler produces. When this

number is small, that means Circe is producing uh less less constraints, which is better for Circe. Um, and uh the the landscape is that in more situations, Circe does better. Um, there's there's one one benchmark where we do a little bit worse, which is uh the SHA-2 round function. And I I can we we can actually dig into this plot in detail now or later, if you guys want, and we could talk about like what what the compilers are doing differently, and why they're getting different levels of efficiency. Um, but but what to be The Pedersen one, is that the um the Hopwood Pedersen that's used in Zcash?

Yeah, yeah. Uh, I guess you're the right person to ask that question. Um, yeah, yeah, this is this is their implementation of that hash function. Uh, yeah, so so we we chose a a lot of hash functions that went into this plot, also some elliptic curve operations, and then also some sort of like bread and butter casting between fields and booleans and and stuff like that. Um, so yeah, to be clear, we're we're we're not saying that the Socrates compiler is garbage. Actually, I think it's extremely good. You should probably keep using it. Um, but what we are saying is that if if what you're setting out to do is compile some high-level languages to to a constraint format, then maybe you should look into using our infrastructure, because it's going

to help you get extremely competitive performance extremely easily. Um, and without without sacrificing accuracy. Okay, so so that that's kind of like the the result on the front end side. Let's talk about how we how we do this. Let's talk about what move on from this slide, so how um do these figures compare to say a hand-optimized um R1CS? Uh, not not written using Socrates, just um That's a good question, and I and I think it's going to depend I don't think I can give like a single unifying answer to that question. Well, yeah, it would depend on the benchmark.

Yeah, yeah. Um, I think what what So, it's a good question. When you think about the domain where you have a programmer who's really going to sit down there and tune, I think the most important thing that the compiler can do is offer sort of predictable performance profiles. Um, like you you you want people to be able to optimize in the high-level language, and actually feel like they're they're hitting the the base of what they want. Um, like Circe is not imposing any abstractions that are inherently costly.

So, so we're not worried about hitting some kind of optimization floor. Like imagine that you're optimizing Python, eventually you you you kind of hit this floor that you can't get through because of Python's computational model. We we don't have any problems like that to which of which I'm aware. Um, but in terms of like the performance profile, like how predictable the optimizations are, um, that's a good question, and I we we didn't try to to quantify that. Um, I think that would be a good thing for us to look into. Yeah. Yeah. I I guess you can always I mean, like people do with conventional programs, they write parts of it in assembler. You can write parts of it in hand-optimized R1CS, so whatever.

Yeah. That's what I was about to say. It pretty much depends on the person who does the optimization. Especially especially the assembly bit, which I'm very familiar with. The other bit, I I don't have any of the details. They They are knows better than I do. So, there you go. Carry on. Will do. Okay, so so yeah, what does it actually look like to write a front end? Like, what did we have to do to build this Socrates front end to Circe? Let's talk about that. Um so reminding you of the the original picture, we're going to have these different front end modules, which are compiling different high-level languages to some kind of intermediate representation, which represents the circuit. This is going to be like kind

of like an SMT-like representation. It'll have a very rich set of types, um, but it's a circuit representation. There's no state, there's no control flow, none of that. Um, and so really, the task of this of this um of these front end modules is twofold. First of all, they have to embed their language semantics into a circuit format. And second of all, they have to scrub all of these things like state, and like control flow, and and stuff like that. Um, and so different languages have different semantics. Um, so I guess each front end module is going to have to define its own semantics, but the notion of state scrubbing, the notion of control flow scrubbing, those are common thread. And the front end uh libraries for Circe are designed to sort of handle those for you

when you build a new front end. How exactly does that work? What we imagine is that each front end is written as an interpreter for the language that it is a front end for, but state management is abstracted out, and is handled by Circe IR. Or sorry, it's handled by Circe itself. Um, so what this gives you is automatic handling of the challenging parts of variables like mutation, scoping, etc. It gives you automatic handling of data-dependent arrays. It's going to give you automatic handling of control flow.

And and the way that you're going to get that is whenever you're writing an interpreter, and you have to do something related to variables, or related to memory, or related to control flow, you're not going to do it yourself. You're going to say, "Okay, I'm going to delegate that to this state management module that's provided to me by the compiler." Um, so to make that a little more concrete, um, I have a snippet of what part of the interpreter for some high-level language would look like. Um, this is written in Haskell, so so bear bear with me. Um, I'll I'll explain to the best of my ability.

Um, so so the idea here is that we're we're interpreting a language called BoolPair, which is pretty simple. It's got booleans, it's got pairs, and that's it. It's also you got like data-dependent control flow, assignment, etc. Um, and uh here we have a snippet of what it would look like to evaluate a statement in this language, and we're looking at two cases. We're looking at assignment, and we're looking at if statements. So, assignment is the is the first case. Um, here we want to assign some exper to a var. Um, and we start by evaluating the exper, which is some other part of the interpreter. And and then if you're writing an interpreter, and you're doing assignment, now you have to do the assignment. You want to store the value that you have in this variable.

If you were in some intro PL class, and you were writing an interpreter, you would like have a hash map where you map variables to their current values and you would store the value in this hash map. Um and what you do looks a lot like that, but it has totally different semantics. What uh so at the blue arrow here, I have a call to CirC SSA assign static single assignment assign function um with var and with the value. And so what you're doing is you're saying, "CirC, I want you to associate this value with this variable." Um and you can imagine that that CirC is just like maintaining a hash map for you. And and and that like that will work. Like you will be able to write something that looks like a correct interpreter with that model. But what's actually happening behind the

scenes is CirC is producing a new chunk of circuit that manages the new state of this variable. Um and it's doing that in a way that's consistent with control flow. So let's talk about the if statement now and talk about control flow. Um so in the if case um you have three things. You got the conditional that you're testing on, and then you've got some chunk of code, a statement that corresponds to the true case, and a statement for the false case. Um and what you have to do is evaluate the conditional. And then you do this interesting pair of things. First of all, you use CirC's guarded function based on the condition that you just evaluated, which tells CirC, "Hey, I want to perform some further computation in an environment that's guarded by this condition being

true." So that's the call to guarded. And then you CirC's scoped function, which says, "I want to enter a new lexical scope." Um and then inside that you evaluate the true the true statement. Um and then at right after that, you do the same thing for false. Um and you can imagine that like, "Oh, you know, CirC's guarded is just kind of like a conditional. Like it it checks whether C is true, and if so, it runs the code that I gave it." Um but what's actually happening behind the scenes is that CirC is generating different chunks of circuit for the true case and for the false case. Um and it's it's sort of like state merging between them in in a consistent way.

Um So so ultimately this this interface that you get is is very much um like a very much like writing an interpreter. Um or maybe like a type checker, cuz I guess you when you hit a branch, you explore both directions. Um but the the effect is that because you've been using CirC to do state management throughout, at the end of the day, you get a circuit. You don't you don't get a type check result. You don't get a value. Uh you get a circuit. So So things like the lifetimes of variables would will it automatically decide when a variable is no longer used and I guess So I guess it doesn't matter because it's not a So you have to explicitly throw away the state.

Um Hm. Yeah, that's actually interesting. So the optimizations that conventional compilers do are not really relevant here. Yeah, we started this project thinking that we were doing something like LLVM, and just as time went on, we increasingly realized that's not true. Uh we're doing something that's a lot more like an SMT solver. Um So we inherit most of our optimizations from the design of SMT solvers, actually. I mean the the kind of caching and trade-offs in the LLVM thing, I don't think you can actually use it over here. Yeah. Now Now I I do want to say something about Dara's question, which is that this is an the the question of supporting high-level languages with sort of like complex constructor destructor semantics is an interesting

one. Yeah. Um that CirC is not helping you with right now. I don't think that means that it couldn't help you with it. I I would like to think more about that. Um Right. So So if a language did have constraints on when things should be dropped, it would have to implement that itself. Right now, yeah. Yeah, it would have to implement that itself. I guess it's not too bad. Yeah, that being said, I like if if you're aware of such a language, like I I I would love to look into this more. Like perhaps there's some general infrastructure we can offer for that. I suspect there is. I I mean, Rust might be a good language to use as a an example of that.

Yeah. Yeah. That's a I'll file that away as as something to look into. Um Okay. I think I might actually just want to skip this slide. Yeah. Yeah, okay, cool. Okay, cool. So the next thing I want to talk about is the core of CirC. So I want to talk a little bit about the compilation algorithms that we use to do state management, and I'm going to talk a little bit about the optimizations that we apply on the resulting circuits. Um so that means that we're focusing here on the center of of the compiler.

And giving credit where it's due, uh to my knowledge, none of our compilation techniques are new. We're taking existing work and we're just lifting it to the right level of abstraction. Um if we accidentally came up with something new, that's very cool. But but I I I don't think that Certainly our our intent was not to to develop some new compiler infrastruc- or new compiler ideas here, just to build um an infrastructure that was at a sufficiently level general of a sufficiently general level of abstraction that it could be reused. Um so I I conceptualize most of the techniques that I'm going to tell you about as coming from the SMT-based verification world. Uh Riyadh conceptualizes many of them as coming from the R1CS compilation world. Um and and uh there's a lot of commonality and

and and and some differences. Uh okay. So let's let's talk about uh a list of of challenges that we have to overcome and general approaches to to overcoming them. Um so one one immediate challenge is that in high-level languages, variables can mutate. Uh our our infrastructure is responsible for managing that. And our approach, generally speaking, is to version all variables. So think about of this as putting the program into a static single assignment form. If we start with code that says X equals Y and then say, "Okay, now we want X to be X times Y," then these two different assignments are actually the two different versions of X. And I have that on the lower hand on the lower right-hand side.

Another challenge is memory use. Um so generally, what do I mean by memory? I mean that we're accessing some kind of array, and we're accessing access- accessing it at data-dependent locations. So you can imagine that here we have an array X, and we want to set location Y to be some other value Z. In the SMT world, the general way that you handle this is you use SMT arrays, which are designed to to to take care of this. Um and you imagine that what you're actually doing here is is treating X as this this abstract array, and when you assign to it, you're creating a new version of that array. So think of it as like updating a map.

Um and and and the updated version um at location Y, you have Z. There's actually a few like subways that you can handle this. There's there's often a debate, do you make each high-level language array its own SMT array? Do you have one giant SMT array that represents the whole stack? Um What I How exactly do you want to handle that? Great great questions. I'll talk about them a little bit more late later. Um and you also might be thinking, "Okay, what if I'm compiling to R1CS? Even if something like SMT has arrays, R1CS does not. Uh just going to SMT arrays is not going to solve the problem. I'm going to kick the can on that, too, until I to a point where I talk about optimizations later on.

Um we'll we'll have a way to get rid of the these SMT arrays in an R1CS-friendly fashion. So So I'm I'm not sure quite sure what the semantics of SMT arrays are. They're basically functional arrays. Yeah. Exactly. Functional arrays. what you would expect from that. Okay. Yeah. So So So at first pass, we just need to turn all memory use into manipulating functional arrays. Um and if we're targeting some back end that doesn't support functional arrays, then we'll have to get rid of them in some fashion. I'll I'll tell you guys about that in a little while.

Another challenge is loops. Um there's lots of exciting techniques that you can use here on the SMT side. I I don't think they've been explored as much on the R1CS side. Um but for this project, we just took a naive approach. We said we're going to unroll them. Um and if the loop is conditional, then we're going to unroll it with conditionals. Um so So the next question is how to how do you handle conditionals? Um and the general approach is that you're going to guard all state mutations under a conditional context. Um so if I have some if statement, so at the top here, I say, "If Y is equal to zero, then square X."

Then when I create the new version of X, I'm going to emit an if-then-else, like a functional conditional expression, which either keeps the original value of X or produces a new one. Um and this this conditional is guarded under the current context. So So going back to the loops for a second, that I mean that works if you have a static bound on the number of iterations. What if you don't? Uh yeah, if you don't, then then we can't help you right now. Um Okay. So So we can't we can't guess. Yeah, I want to emphasize here that there's like there's a lot of study into loops, especially on the SMT side. And and we think that it'd be interesting to look into this more. Um And and we have some friends that that are looking into it more as we speak. Um

building on on CirC. Um Yeah, but but but uh in some sense um in this work, I think we took the dumbest algorithm at every step of the way. Um and and uh it's cool that the results are still pretty good despite doing that. Okay. Um so So yeah, so this is just a list of different techniques uh that we use to handle various high-level language constructs that are challenging to compile. Um After we've compiled into a circuit representation, it's time for optimization. Um many of the optimizations that we do are basic ones, constant folding optimizations where either you evaluate constant expressions or you evaluate or you simplify operands that are applied to some constants.

Um operator flattening, looking for n-ary operators and turning them into bigger ones, uh substitution, if somewhere you say X equals Y, then you can get rid of one of x or y. Um how how you do that optimally is a hard problem, um but but doing it at all is is pretty easy and and it is uh is very useful. Uh and then also people optimizations. Um so looking for common ways of expressing things that have better expressions. Um so here I have um an example of something that turns up in hash functions where you have a sort of bitwise ITE expressed um in terms of machine um bitwise operations. Um so you can actually just turn that into like some kind of weird bitwise ITE,

which might be more efficient. Uh we won't go too much into into these kinds of basic optimizations. You can imagine them as being stolen from an SMT solver or stolen from a compiler. Um They they work the way you would expect. More more interesting is how you handle things like arrays for backends that don't support arrays. Um so a common abstraction in in various high-level languages that intend to target R1CS is that they only allow arrays to be accessed at constant indices. Um so for example, this is This is actually isn't quite what Socrates does.

Um But I think this is what Zinc does. Um and even if um you're allowed to access arrays at data dependent indices, oftentimes people don't. They just write some for loop that goes over the array. And so you want to be able to handle arrays that we say are accessed obliviously, that are accessed at at at only constant indices. Um and uh what you can do here is that you can replace the array with a sequence of distinct terms. Um and um those terms are manipulated independently. You can think of this as being a very strong version of traditional scalar replacement optimization passes.

Uh and I have an example of this in action um on the right-hand side. We have some array x that has two elements. Um and then uh you add its two values together and store them in the in the first location and then you access that. So here all of our indices are constant and we can imagine creating x0 and x1 for the zeroth and the first indices and manipulating them separately. Um so this is one optimization pass that we do. We look for arrays like this and we we transform them. What about uh arrays that that are not trivial in this fashion? Arrays that are actually accessed at data dependent locations. Um to our knowledge, the best the best algorithms for this situation are um sort of derived from routing based memory checking.

So the observation is this. If you've got some program or in our case a circuit that accesses an array at a number of locations, um then you can imagine that what you actually have is a big list of array accesses, um which are in some kind of program order. Um so here the numbers zero through four are the order uh in which this this array is accessed in the program. Um and then there's there's a few variables associated with each access, whether or not that very that access is a load or store, which address you're looking at, and which value um either that you you read from the array or if you're doing a write that you write to the array.

Um and uh it's pretty hard to to check such a sequence of accesses for consistency, for read for read over write consistency. But if the array was in address order, then it would be pretty easy. You could just look at each pair of accesses and say, "Hey, if this is the same address, am I reading the last value? And if this is a new address, am I reading the the default value?" Uh like maybe that's zero, it depends on your language. And so the challenge is is really just going from program order to address order, um because once you're in address order, it's easy enough to check correct semantics. Um and so what you can do here is you can use various kinds of routing networks. Um we have an implementation based on Waxman routing networks.

Um but you can imagine other things. Um And uh since you're in this prover verifier setting where the prover can provide things, they can do things like set the routing network switches for you. Um and and so really all the network is doing is checking that these two lists are permutations of one another. It's worth pointing out that some proof systems support that natively, just checking permutations. Yeah, yeah, totally. Um so like like in particular um like you can just like interpret both the sequences as polynomials and and check for equality at a random location. Yeah, yeah. Use the product argument. Yeah.

Yeah. Um so that that if your proof system supports it natively is far better and you should 100 1,000% do that. Um but um it does require you to be able to like sort of like insert verifier derived randomness into the circuit. Um But yeah, so in general uh and and the way we implement this is like you you know you you uh have the original order, the old order, and you you stamp out some kind of permutation argument. And if you have a better one, great. Uh put plug that in there and it'll it'll be better. Um okay, so to be clear, also like this is not our our work or our idea. I have a list of citations on the bottom of the page. People have been doing this before. Uh but this is how but we we uh express um this algorithm at the level

of this IR, which means it applies to any front end and any back end that we're using. So this is the end of talking about the middle part of CirC. Um at this point we'll talk about the backends briefly. So we support two backends right now. Um one of them is SMT, specifically the Z3 SMT solver, um which was kind of like crossing over to the wrong side of the street for me cuz I work on CVC4, which is a different solver. Um but we already had bindings for Z3, so that's that's what we targeted. Um broadly speaking, our Z3 backend supports everything that we have in our IR. Uh SMT solvers are very expressive.

It's not that hard to support many things. The one thing we do not support is is raw statements about finite fields. Um and then we also have a backend for R1CS. And it it supports bit vectors, so machine fixed-width integers. Uh it supports booleans. It supports finite field elements. And then it supports some arrays via the kinds of transformations that I was just talking about. Um so one thing that we found that was very intriguing to us and validated the utility of general purpose infrastructure, not just general across input language, but also general across target across backend, is the fact that some of the optimizations that we that I was just talking about seemed to benefit both of these backends.

Some of this is unsurprising. Constant folding is is probably universally a good idea. Um and and we find that that is the case. Um so to to just uh to demonstrate that, we defined some hash function um that's kind of like SHA-E but not secure, pretty small. Um and and it made a statement that said that the uh the hash function evaluated at some input produced zero as the final byte. Um and then we tried compiling this for varying sizes of inputs and uh with and without the constant folding pass enabled. And what we did is we decided, "Okay, we're not just going to measure the performance of the R1CS backend or the performance of the SMT backend. We're going to measure both." And and and see how both these these backends perform under this optimization. Um and and what

we found is I think what you'd expect, which is that both SMT solvers and cryptographic proof systems appreciate uh you doing constant folding for them. In the case of the cryptographic proof system, between the blue points, which is where we have constant folding enabled, and the red points, which is where we don't, we have something like a 10-fold improvement. So this is this is huge. You should 1 you know 100% do this. In the case of the SMT solver, the improvement is less and the reason is that the SMT solver is going to do constant folding itself. Um so really all you're doing here is saving it the work. Um but yeah, so this is like simple enough, but it it validated our intuition that that there are really some optimizations that that benefit both both backends.

But um we we were curious whether or not there are more meaningful optimizations that also benefit both backends. And and we found that there are. Um so another another example is array elimination. So this is looking for arrays that are accessed at constant indices and replacing them with sequences that is of distinct values. Um to do that, we constructed a program that filled an array with non-deterministic values and then summed them. Um This is basically just two for loops where the indices um of the for loops can be determined at compile time. Uh and in this situation, we also found that both the backends appreciate this optimization. Um they appreciate it in start in in extremely similar ways.

The most uh sort of detailed common performance characteristic experiment that we did relates to array granularity. So I mentioned before that broadly speaking, the way that you handle memory when compiling to a circuit is by treating memory as a a sort of a functional array. And that you have a choice about how you do this, which is that you can try to represent each high-level language array with its own functional array, or you can try to put them all into the same bucket. Um sort of having a large stack array that every high-level language array is just an offset into.

And uh these these two different approaches have their own benefits and drawbacks. Um generally speaking, if you take the stack approach, it's easier to capture language semantics accurately. Um but what we find is that the the fine the fine-grained approach performs much better, not just for SMT solvers, but also for compiling to R1CS. Um and in in order to simulate this, um it's not like we have some switch where we can switch to stack mode. Um like we we believed up front that the fine-grained approach is going to be better and so we only implemented that.

But we can sort of simulate the stack-based approach by at the source level taking some program and rewriting it to merge all of the arrays. So we cooked up some program that used a whole bunch of arrays. Um in this case, each array represented a permutation over the index space of the array. And we just applied index one array after the other in order to apply this permutation. Um and then we made some statement like uh this permutation has a preimage for zero. Um which is of course true because it's a permutation. Um and and on the SMT solver side, the solver is just trying to invert the permutation. And on the constraint system side uh on the zero-knowledge proof side, you're trying to prove knowledge um, of a pre-image.

Um, and and then what we varied was not just the size of the permutations, but also what fraction of them we had fused into a single array. Um, and and what we found is that not only does this increasing the size of the permutations degrade performance for both R1CS and for SMT, but also fusing degrades performance. So, if you look at these plots, as you go from the left to the right, the x-axis that is, um, we're just we're not increasing the memory footprint of the program, we're just fusing more of the arrays together. Um, and we see that that both the SMT solver and the R1 uh CS back end uh perform worse as you fuse more of the arrays together.

Um, and the reason this is a problem for the SMT solver is it's starting to reason about more accesses to the same array, which is challenging for it. This is a problem for R1CS because your routing networks are getting bigger and bigger. Um. Yeah, that that is actually something where having a native permutation argument um, makes a difference because the the cost of the native permutation argument is just linear in the number of um, elements. Yeah, yeah, you're totally right. So, if if the way that you handle these kinds of arrays is is sort of strictly linear asymptotically, then you wouldn't expect it to matter a lot, um, how how big your arrays are.

Uh, and that and actually to be frank, because the the stack approach is is much easier to model semantically, I I think this is a strong argument for supporting permutation arguments in your proof system. Um, it it it gives you a better path forward when it comes to modeling memory, which is a pretty pervasive abstraction. Al- Although, my my intuition would have been that the um, the smaller arrays are a better anyway, but I would I wouldn't have had a a clear idea of why. Yeah. Um. Yeah, so so anyway, just uh the the trade-off of array representation from granular to to sorry, from coarse to fine is something that people have looked at a lot in the SMT world, and and largely we're we're confirming that there the intuitions

that they have also apply here, um, which is which is very cool. And it it bolsters this argument that there's a lot of common optimization machinery that you can write. Okay, um, so enough enough of graphs and and details. Um, what one interesting thing that you can also do when you support multiple back ends is that you can do sort of interesting crossovers, where you try to use one back end in service of the other back end. Um, so I'll I'll tell you about two such applications that that we looked at. Um, one of them is using an SMT solver to help you compile to R1CS.

Um, so to use the SMT solver sort of in the service of optimization. Um, and and this goes to to the question earlier, um, about handling loops. What if you don't know how many times the loop is going to run? Um, naively, what you'd have to do is is guess or or get some input from the programmer. Um, and and one one example that might be challenging is the example I have on the screen. So, this is a program that's supposed to be computing the base two integer logarithm of a 32-bit number, and it's doing that with a loop that iterates until some value is zero. And naively, it's it's not clear how many times this loop is going to run.

And that's a very important question, because if you guess a number that's too big, then you're producing a circuit that's too big, and that that hurts you on the performance side. If you guess a number that's too small, then your program your compiler is not going to be complete. You're going to be preventing valid executions of the program, um, because you're going to guess a number that's too small, and you're probably going to emit some constraint that says the loop actually stops at that point. Um, and and that's going to invalidate certain program executions. Um, so it would be good to have a precise answer to the upper bound of the number of types times that this loop this loop iterates. Um, and with an SMT solver, you you can actually get a you get a handle on that.

Um, so we wrote I think it was I think it was literally 10 lines of code, um, that what what it does is that when you're using the C front end to the system, at while you're unrolling a loop, at each stage, you take the circuit you've assembled so far. And even though your ultimate goal is to turn it into R1CS, you take what you have and you give it to an SMT solver, and you say, "Hey, is the current path of the program still feasible?" And if SMT solver says yes, then you you keep unrolling. But if the SMT solver says no, then you know that you've reached an upper bound of the number of iterations, and you can immediately stop.

Um, so to be clear, we're asking the SMT solver to solve a pretty challenging problem here, and and this isn't going to work all the time, um, but what we found to be to be exciting is the fact that having common infrastructure made this so easy to implement. Um, we already had a back end for SMT, it was just a matter of saying, "Hey, SMT solver, take what we currently have and tell us something about it." So this example, let's suppose that um, you had a very large integer. Would it still be solve uh feasible with the SMT solver? Could it or is it only practical for small values?

Yeah, um, for for loops of this simple structure, I I think the SMT solver is going to like chew through it no matter how big the integer is. Okay. Um, like I mean, we're going to get into the details a little bit here, but so the way SMT solvers handle bit vectors or machine machine integers is they turn them into SAT, um, by and large. Um, not not universally true, but but that that's the the dominant approach. Um, and when the operation that you're doing inside the loop is this kind of shift, that has an extremely efficient SAT representation, um, and basically like the solver is going to end up ignoring almost the entirety of your state space, and it's it's just going to follow the most significant bit.

Um. I think where you're going to run into more trouble is where the control flow inside the loop gets more complicated. Yeah. Yeah, cuz it it could easily end up being exponential in that case. Yeah, yeah, for sure, for sure. Um, so so using SMT solvers to say things about your program, rich area of research, lots of cool things that you could try to bring to bear here. Uh, we just did the simplest cut, and our observation is that with common infrastructure, whatever you're trying to do with the SMT solver, it's extremely easy. This is very cool. Yeah, yeah. Okay, so we're not done yet.

So, I I I have one more crossover application. This goes back to to what I opened the talk with, doing a proof of bug. Um, and you know, I mentioned before that this is challenging because you need to be extremely accurate in order to capture most bugs. Uh, your compiler really needs to capture the input language semantics. Um, but we we were designing this this infrastructure to not just support compiling to R1CS, but also support compiling to SMT. And accuracy is always the paramount concern when compiling to SMT. Um, and so that means that we sort of get it for free on on the R1CS side. Um, so we we sort of rigged up this interesting little workflow, where we take some input program. So, I have it here. This is again uh a mac the same macro from OpenSSL. It's supposed to be computing C equals C plus 2AB. Uh, it

doesn't quite do that. The carry handling is a little bit broken. Um, I have a backup slide if you want me to like give you a data flow diagram and explain how this macro is is broken. Um, so so what so what do we do? We say, "Okay, we're going to take this macro uh and an assertion about its behavior. We're going to use the C front end to compile them into our intermediate representation. Then we're going to take that intermediate representation, we're going to feed it into an SMT solver. We're going to get back from the SMT solver a violation of the property. And then we're going to take that violation, we're going to lower to R1CS. Um, and and we're going to write a zero-knowledge proof that we're aware of this violation.

Um so this is like sort of an interesting little demo to do. Um, if the bug is so easy that that a generic SMT solver can find it, then writing a zero-knowledge proof is kind of a waste of time. But if you have if if you replace step three, find violation with solver, with some sort of custom analysis, um, then what you have here is is some some sense a demonstration of the zero-knowledge um, proof of of bug system. Um, so so we thought this was kind of fun to do, and and and what we and and the point that we wanted to make here is that the only reason this works is cuz we're achieving uh sort of an accuracy bar that's high enough for SMT, um, and that enables the zero-knowledge proof to actually mean something about

the the program that it underlies. Okay, so I I guess we're at the end of the road here. Um, I've been telling you guys about CirC. This is uh broadly speaking a comp a compilation infrastructure, not for for programs, not for assembly, but for circuits. Um, our observation is that different circuits um, and different high-level languages can share the same compilation infrastructure, and that when you build common infrastructure, it makes it easy to support new languages. It enables any new language that you support to benefit immediately from optimizations that have been defined in the compiler infrastructure itself.

Um, and it also enables these interesting crossover applications, where you start to use the different back ends, which have different purposes, in service of one another. Um, this is this is work that we're just getting started on. Uh, there's lots of directions we want to take it. Uh, I can I can give you the details if you want, but but maybe I'll I'll stop for now. Awesome. Thanks, Alex. Um, we got uh well, I guess we can open up to questions now. Anish, I think uh Anish, you had a question you just posted in the chat, so um, go free. All right. Uh Alex, uh rather stupid question. I was kind of extending this. Like normally, one of the problems we have in this blockchain space is like you create a you make a bunch of cryptoeconomic

assumptions, you create a contract, and the protocol is broken. Not as a bug bug the bug that you're referring to is like a bug you have an assertion, you understand it at the first level. So, imagine you have a multiple levels. I was just thinking, that's that's what a cryptoeconomic attack would look like, right? So, how hard that be to actually have like multiple levels of assertions? I see, I see. Yeah, yeah. So, you're saying that like some sense, there's some behavior from the circuit which is broken, but it's it's not broken because of the circuit itself. It's broken because of some interaction with the circuit in the outside world. Yeah.

Yeah. I I think that this is a challenging case for us. And And the reason I think it's challenging is that essentially, um, what you need to do is you need to encode that higher-level stuff in a format that the compiler can understand. Yeah. And you could imagine doing that. Like saying, I I'm not I have a hard time coming up with an example, but but making whatever kind of incentive statement that you want. Um, the challenge is that for these kinds of, um, proofs, you need to perform the setup for the for the zero-knowledge proof. And at setup time, you need to agree about what a bug looks like. And And my my instinct for these kinds of multi-layer attacks is that they're often very creative. Like, you don't

necessarily know a priori what the incentive situation is Yeah. going to be which defines the bug. Um, and so I think that would be a challenge. Sort of like Not not necessarily at the It's not even a compiler challenge, right? That's just like a sort of human challenge. Using a zero-knowledge proof requires you to agree up front about what a bug is. Yeah. I I mean, I I guess that you could use existing um tools that are designed to, um, prove the security of cryptographic protocols, for example. Um, and then where uh, Cestus is helping here is knowing that the representation that you feed to that system corresponds to your actual

circuit. Yes, that is a good point. Yeah, so if you want to do some kind of analysis in like some kind of interactive proof assistant where like Are you Are you saying something with the compiler or something like that? Yeah. Okay. Okay. Thanks, Dana. Thanks, Alex. So, a little bit odd. No, it's not a bit odd. Um, so what What interests me, actually, is using the, um, SMT solver to prove the correctness of optimizations. So, the These could be optimizations that are too hard for, um, a compiler to do automatically.

Say they're based on the, um, things mathematical statements about the elliptic curves you're using or whatever. Um, so they're too hard for the, um, compiler to do automatically, but they might also be difficult to prove by hand. Um, so that's what I'm most interested in. Have you um, explored that area much? We We've started to think about it. Um, in fact, actually, broadly speaking, the kind of thing that that you describe has been on my mind for for years now. Um, and the challenge is that you need to get the Well, it depends on what optimizations you're thinking about.

Um, but probably, I think that the interesting thing to do here would be to analyze optimizations that involve the arithmetic format itself. Um, so either mapping bit vectors into arithmetic or arithmetic itself, whatever. Um, and in order to get the SMT solver to tell you things about those optimizations, you need the SMT solver to be able to reason about field arithmetic. Yeah. And you can approximate that right now. Yeah, you can approximate that right now that right now with integers like like for prime fields or something with modulus, but like the modulus machinery in in SMT solvers, um, is is pretty pretty garbage. Um, I should say it's not quite right. It's

over-engineered because it's designed to support any modulus, like even a symbolic modulus, whereas in our context, the modulus is fixed. Um, and so I think it's extremely interesting to try to develop better support for finite field arithmetic in SMT solvers. Um, and I think that that would enable the kind of analysis that you're talking about. And And also lots of other interesting analyses as well. So So, in SMT terms, this is just a theory, right? Yes, this is just a theory. We want a theory of finite fields. Yeah. I don't know whether there's been any work on that. Um, I I've looked, um, and I've talked to the the people like Clark and all the folks at SRI, uh, and we're not we're not aware of any.

Um, I mean, there there are plenty of, um, optimizations that don't depend on finite fields. There's one that's used in, um, Zcash sapling, for example, when you're um, you're doing a range check, um, for a fixed range that you know in advance. And you use the bit pattern of the, um, of the uh, the size of the range, um, and that's exactly the kind of thing that an SMT solver would just eat up. Um, yeah. Yes, you're right there. Yeah.

Yeah. So, for those kinds of optimizations, um, you could definitely get an SMT solver involved and if you express those optimizations in in our machinery, then then it would be really easy to when you like stamp out the optimization in one situation, you can check just that instance. Um, you could also ask the compiler to do it sort of symbolically and and check the optimization in general. That That particular one was about a couple of days to prove correctness. So, I I would really be very happy if something could do that automatically.

Or even with less help. Yeah. Awesome. Alex, this is super interesting. Um, my question is more on, I think, you know, getting back to the applications and really the crossovers. And you've got these dotted lines here to some other areas that, you know, some folks on the call obviously recognize MPC cuz MPC is what we do for a lot of setup ceremonies in, uh, zero knowledge. But also, you know, I I personally am interested in ILP and just optimization in general. And so I'm curious about, you know, so you've kind of given a couple flavors of how this could look where SMT, you know, SMT, you know, the SMT solver can be combined, um, you know, because it's a unified, uh, infrastructure with some

other stuff on the back end. You know, what other promising directions for combinations, uh, do you do you see? Um, maybe including, you know, that you could bring in ILP or MPC. Great great question. Um, and yeah, one that's that's been on our mind from the beginning. Um, I'll I'll give you two. One of them that's like pretty well-formed and one of them that you know, is just starting to to take a form. Um, the well-formed thing would be to use optimization machinery in the service of some kind of compiler optimization pass. Um, so to have at some stage in the compiler or some representation of what you're compiling and then, um, ask an ILP solver, "Hey, if I want to

like try to write this as a some some alternative system of equations, what's the lowest cost way to do that?" Um, so I think this is kind kind of obvious. You might imagine using the optimization solvers in in service of compiler optimization. Um, another interesting opportunity is the is based on the observation that if you open up, um, many MPC systems, they have inside of them for purposes of malicious security or other purposes, you the use of zero-knowledge proofs. Um, so like you can imagine that like during an MPC execution, there are phases where the the protocol says, "Do a zero-knowledge proof."

Um, and often that's treated as a black box. Um, but if you're using a compiler infrastructure like this to to actually build the MPC circuit, maybe you want to open that box up and and and actually like maybe add some more zero-knowledge proofs of your own. Um, so maybe at a certain phase, uh, what has to happen is you have to come up with some some value, um, that needs to be legitimately computed. Um, and traditionally, um, you would sort of black box ship that to to a zero-knowledge proof. Um, but we might actually be able to like open that up and and try to optimize the zero-knowledge proof and the MPC together.

Um, but so the these are just two two, uh, combinations that we see. Um, I don't I don't think we've spent as much time thinking about this as we would like. Uh, and and I would love to hear of any other ideas that that somebody has. Yeah, and this is really cool work. And I mean, to me, it just makes clear the connection between sort of these different fields that I mean, I hadn't appreciated as much before. Um, and I know very little about compilers, certainly, but yeah. Cool. Yeah. Yeah. I think the the story here is that, um, it is fruitful to complain to Fraser when I'm having trouble, uh, building some kind of R1CS instance.

Or Or fruitful for her to complain to me when like SMT isn't doing what she wants. Eventually, we realized our complaints were basically about the same thing. So, you you said, um, you gave, um, some statistics for how long it took you to, um, build the Socrates back uh, front end. Um, how long does it take to build a back end? It's a little And let's say, for a diff- for a different arithmetization. Yeah. Um, I I think it depends on sort of like how far your particular circuit format is from our from the IR that we have.

Um, Right. I I mean, I I guess you can treat more general, um, formats. They They have an R1CS special case. So, Yeah. you you could start with, you know, R1CS solver and then try to generalize it and make make it more efficient. Yeah, so supporting like some kind of like bounded fan-in arithmetic circuit, for example, like like that you would use for MPC, perhaps, or or maybe you would, uh, use for I think I think like like the Plonk description uses a bounded fan-in arithmetic circuit. Um, Plonk is actually quite similar to uh, R in many ways.

Got you. Um, but yeah, using one of these, uh, I don't think that this would be the hardest thing to support. In fact, I think in many ways what you would do is you would take the R1CS backend and you would sort of like split it into two layers or something. Um, and, uh, the first layer would sort of arithmetize and the second layer would flatten. Um, but um but we have we haven't looked into doing it yet. Um, I think we have some plans to to go down this path for MPC. Um, but we haven't done it yet. Uh, and how much work would you say was involved in, um, writing the the SMT backend or the, um, the R1CS backend?

Uh, yeah, yeah. Um, I mean, I know I know that that's going to be much more than writing a new one cuz you you've already got those examples. Yeah, I so actually, so, um, I can actually say talk about this pretty concretely because, um, we originally wrote this in Haskell and and I think once it became clear that it was a good idea and that people might want to use it, we we decided to to rebuild it in Rust, which was something people are more comfortable building on. Um, and so we we've been doing that. Um, and, uh, I I I did the Rust thing maybe like 2 days ago and it it took me like, I don't know, three evenings of work to to re- to do the R1CS backend in Rust.

Um, and then Wow, I'm impressed. the SMT to be fair like I already knew everything I had to do cuz we we had done it before, right? But um Yeah, yeah, I know. Um, but it that that puts a burden on the Well, yeah, that must be which gives me an idea. Yeah, and then the SMT backends are like like like super easy, right? Because like our IR has so much In fact, for a long time we conceptualized our IR as just like extended SMT where we've like thrown in finite fields and we've thrown in some other stuff that we wanted. Um, so that mapping is is very direct. Um, like like I don't know, as fast as you can type probably.

Cool, thank you. Yeah. Any other, uh, any other questions from the group here? Uh, okay, I have I have one. Um, I guess I'll I'll I'll pile on. Um, so you a lot of this work looks like you're using Zokrates and obviously there's there's been several new which you referenced, you know, um, kind of languages that people have have created to communal compile or to, you know, write high-level logic compiles to uh, to R1CS. Uh, I guess in a little more detail, do you think is there any is there any interest from you or the other authors or do you think there's promise in exploring, um, you know,

looking at those as the front end replacing Zokrates with those in the front end and what do you what what do you expect you might discover there if you if you did that? Um, we are extremely interested in using this infrastructure to compile new high-level languages. So, like, uh, like in some sense like we built this as an infrastructure for people who are building new DSLs, um, that intend to to target zero-knowledge proofs. Um, so if you, uh, you know, people if you or people at your firm or whatever are are thinking of some new language that you want to target some kind of arithmetic circuit, uh, please come talk to us. We we suspect this is useful for that task. Um, we found that to be the case for Zokrates. Um, and and we would

we would be like I would love to have a conversation with anyone who's interested in doing that. Got it. Yeah. I I'm incredibly interested. We should set up a a conversation with the cash people. Yeah yeah. Zcash people. Um, if you have my email already then you can use that. Um, if if you don't, I guess I can my email is aosdemir@cs.stanford.edu. Yeah, I know some people. I'll I'll pass it on. Yeah, yeah. To So so actually I should say in disclosure that like, you know, this understand this is this is like research software. I don't I don't think that we're quite production ready yet, but, um, but it like what we got so far seems really useful for this purpose.

Yeah, great. I guess my question a little bit deeper though is, you know, Zokrates I think is limiting is somewhat more limited than some of the newer approaches. And so I guess what would I mean, I assume I could think you benchmark some of the, you know, the improvements you could get by using, you know, this this infrastructure, how would you expect that to compare with some of these other languages that have maybe fewer limitations than Zokrates? Great great question. Yeah, like Zokrates is like super super limited, no data-dependent control flow. I'm not even sure that they support data data-dependent array indexing. Um, although I I'd have to check. Um, when when we were designing the system, uh, I I told you guys about our comparison against against Zokrates, um, but most of our comparisons were actually against Beguine, which is a compiler from C to R1CS. And Beguine,

while it's not nearly as nice as Zokrates, I would not recommend you use it. In fact, even building it is a is a pain in the butt. Um, it it supports all kinds of fancy things and we can we compare very favorably to Beguine as well. Um, so so we're able to handle more complex program constructs, we're able to handle them well. Um, and actually for what it's worth like our Zokrates front end supports these as well just because like the compiler natively does. So like in our Zokrates you can branch on data-dependent values and and you can access arrays at data-dependent locations. Um, so you you you get you get the higher level stuff as well.

Cool. Nice. Um, I guess alibi here for anybody final questions or or, uh, anything they'd like to ask or say to Alex before we conclude here? Thanks Alex. Yeah, thanks for being a great audience. It's been my pleasure to to give this talk. Thank you, this was awesome. Yeah, thank you very much, Alex. As you can tell, we all really enjoyed this and and I maybe I'm speaking for myself, but likely I'm speaking for everyone that I think this is a really cool direction to explore. This is different than many of

the other talks that we, you know, kind of see in in this group and papers we review. And very excited about, um, your future work on this on the subject. Hopefully we can welcome you back again at some point. Maybe maybe even for, uh, a more proof systemy thing. Totally. Cool cool. All right. Okay, I'll stop screen share.