ZK12: Zirgen: A Novel DSL for Writing Efficient zk-STARK Circuits - Jacob Weightman

Transcript

[Music] um hello everyone my name is Jacob waitman I'm a compiler engineer at risk zero and today I'm going to be talking to you about zuren our new DSL for writing efficient ZK Stark circuits first a little bit of context about risk zero uh we recently announced a new network called boundless uh which we envision as sort of the full stack solution for zero knowledge application developers so this is everything from how you actually get your zero knowledge proofs on chain for use in real applications all the way down to the zkm layer where the

execution actually happens So today we're going to be zooming in on that zkv M layer as we're talking about how circuits actually get built at risk zero so back in the old days of ZK applications were built with custom circuits per application and uh you would pass in some sort of input and you'd get your proof out at the end um the the primary innovation of the zkm model is that that application specific circuit gets replaced with a general purpose circuit that uh implements a general purpose architecture at risk zero that is risk five so now the program itself becomes part of the input

such that when we want a proof we can just hand it a program written in a conventional language compiled with something like the rust compiler or anything that works with LM along with the input and get our proof um but in uh in pursuit of higher performance um it seems ideal to have uh some additional accelerators so in paral or in sort of analogy with the way that conventional software engineering Works where you write a program in a general purpose language and run it on a general purpose CPU over the last few decades we've seen the emergence of heterogeneous Computing that it's beneficial to offload intensive

computations to specialized Hardware that can do them faster things like gpus fpgas dsps things of this sort and so the model that we're pursuing here is to have our general purpose risk 5 CPU in this model as well as a series of accelerators for specific operation that we could do a little bit more cheaply with the custom circuit these are things like accelerators for the KET hash function or alternate commitment schemes elliptic curve operations things like that so when you do go to do a proof on risk zero typically uh it's useful to have sort of unbounded duration of computation and so in a stark based

proof system like ours we have to subdivide this into fixed size segments uh but after we've done that we we can roll them up together with recursion and so the traditional picture of what you can do today without accelerators looks like this now when we introduce accelerators the picture stays pretty much exactly the same except that the third line here changes we can swap out some of these segments with accelerators and roll them up in exactly the same way to a single succinct proof so with this in mind right this architecture calls for a lot of different circuits we we have the zkm itself which implements risk 5 we have a recursion circuit that is able to verify

these receipts as well as an unbounded number of accelerators that might be useful to plug into different applications depending on the application developers needs and so with all these circuits it would be really ideal to have a really great experience when designing these in order to be able to effectively design Implement test them and be confident that they're secure and efficient so it turns out though that a lot of the ways that people have written Starks comes with a lot of drawbacks um in particular each of these drawbacks comes with an opportunity to do something better so one thing that we saw was that a lot of Stark description languages really split out different parts of the

implementations you have separated constraints from witness Generation Um and it's all separate from for example The Logical structure of the circuit that you might use to to achieve some notion of composability when writing your circuit the other is that composability options are often quite limited uh and so it would be really nice if we had the ability to describe a small fragment of our circuit and then glue these pieces together and test them independently and do all of those things that we get to do in traditional software development and lastly there's a lot of boiler plate and complexity that comes along with writing circuits for example for every circuit that we wrote we found ourselves reimplementing things like permutation AR ments and uh lots of other things of that

sort so let's zoom in and look at some real zuren code and see what it looks like so um we have a single concise representation that captures everything of Interest here so for example let's take this bit regge component it's going to take as input a value called X it's going to write into a register a register is an abstract view of a column in the Stark Trace register this reg component comes along with an implicit constraint that the that register value is equal to X then we go ahead and add another constraint here so this polinomial is satisfiable if and only if R is equal to Zer or one in order to make these terms zero uh and lastly we return this value R uh this is not

exactly a return statement but it's quite similar and it indicates that this bit regge component can in any context be used as if it is a register that register R in particular so you can kind of see how we've comingled all of these things together into this very short representation next let's talk about composition so you see here implementations of four distinct uh combinational logic gates that you'd see in traditional uh Hardware design right you can negate a bit register by subtracting its value from one because one minus one is zero which is not one and 1 minus 0 is one which is not zero

uh and and similarly so you could go in and check all of these Expressions but the thing that I want to call out here is that we have this very nice almost functional sort of composition that you can do with this the other major type of composition that we have in the zuren language is called a MX or a switch where we can Multiplex over uh set of selector values so with this component full adder we're implementing a um add with carry component using the uh components that we just composed out of bit regge in order to do a one bit adder with a carry in C and A carry out so the sum should be true if at least two or sorry if an

odd number of x y and C are true that is our sum is three or one um which can be done in this way which should be a familiar expression for people that have studied Hardware implementations of adders and uh the carry bit should be true if at least two of them R so we do this by cases if C is true that is C is one then this selector becomes the array 1 Zer and so this first MX arm becomes active so if C is true then we only need X or Y to be true for the carry bit to be set and if C is not true we need X and Y to be set for the carry bit to be set in fact when I look at this I actually think it feels a little bit

simpler than the combinational logic expression to do this in traditional Hardware design uh there's a lot of other niceties that sort of come with this uh that are a little bit harder to fit in slid sized examples but one of them is that U permutation arguments are built into the language that is you can simply declare a component with the argument keyword and we will automatically synthesize a log up sum for it in order to do a log Up Style permutation argument and all of the layout constraints that come along with that will be implicitly enforced similarly we have an abstract way to describe the structure of a circuit which enables this sort of composition that is you can abstractly

describe the uh logic of the circuit that you want without having to bother with the particular column offsets or how things are precisely arranged in uh the concrete Stark implementation and then the compiler can go and generate an efficient layout using a uh constraint solver at compile time uh lastly it has some built-in facilities for testing such that you can write unit tests integration tests whatever you feel like directly alongside your circuit implementation which ends up saving a lot of work and eliminates the need for um test harnesses and extra Tooling in order to test fragments of a larger circuit now you might be thinking maybe

this comes with some significant performance tradeoffs that is you know we're losing a lot here by except all of this abstraction and it turns out that that's not entirely true in the same way that most of us don't write assembly anymore if we want to do low-level program low-level programming we write something like C or even rust with some extra restrictions so in particular there's a lot of room to optimize circuits with this representation because we have so much information about the structure of the circuit in this approach for one we have all of the traditional compiler optimizations that you might think of when you think of a c or a rust compiler even you get constant propagation dead

code elimination um con uh common sub expression elimination and all things of that sort uh as well as some more circuit specific things so in particular there are some layout optimizations that can be done automatically for example if you were to generate two separate registers that are constrained to be equal you can coales them such that they land in the same actual column of the ex ution Trace which saves you a register um there's also a lot of room to do optimizations directly on the constraint sets for example if two constraint if one constraint implies that another constraint is satisfied that second constraint can constraint can be eliminated altogether and so it turns

out that there's a lot of things that can uh be optimized to get us pretty optimal so um zuren was released as open sourceof Ware just last month uh and we have a couple of exciting things coming up for it uh in particular we have some accelerators in the works written in it uh namely a katak accelerator uh to speed up proving of ethereum among other things uh and we're also excited to provide some better support for users of the risk zero platform to write accelerators for the operations that they care about uh even if we haven't written accelerators for them ourselves and lastly there's also an interesting

opportunity here to use compiler tooling to assist formal methods on circuits so you could think about doing things like emitting a lean specification from the uh actual source code or you know based on the the uh circuit definition um or even doing things like emitting the uh constraint set in a format that would be amenable for um consumption by a tool like pus to do determinism analysis uh ultimately we're not en irely sure what we're going to pursue in this vein but there are a lot of opportunities for this uh so with that I'd like to invite you all to check out the website for boundless the new risk zero Network as well as to check out the zuren open

source repository uh through the QR code on the right uh thank you [Applause] it's 410 I think we have five minutes for questions okay thank you for that great talk um what are the current backends that you have uh I guess first question yeah so are you asking what proof systems we support well I mean like I don't know plunky 3 or whatever else yeah this is

um purpose built for our own proof system so risk zero has its own stock based Pro and it targets that any plans to support other ones or make it configurable somehow um well it's open source so we would certainly be amenable to people contributing that I don't think risk zero is going is likely to invest in that okay thank you questions uh yeah thank you if I recall uh correctly uh there was a talk in CK proof 5 that was talking about seren but I think it was a product that was very

different it was more about backwards compatibility with the cirquit if I recall correctly yeah so seren was the old uh internal to slightly external name for this compiler infrastructure and uh that name was largely used to describe uh sort of an earlier version of that where we were really only doing the compiler based like traditional compiler optimizations on Uh custom intermediate representation for the circuit so the the language front end is totally new as well as most of the optimizations so that's what we've been working on for the last two years yeah thank you yeah I think we had another question here on the left

thank you for the talk uh it's just what kind of constrain optimization techniques do you plan to apply yeah so one in particular that's really obvious is if you have two identical constraints um you can prune one of them one that's a little bit less obvious but not hard to explain is that if you had a constraint like x * x -1 * x - 2 equal 0 and another constraint like x * x -1 = 0 yeah one of them is implied by the other that that's the kind of thing that I'm talking about when I talk about that any other questions so do you allow to write your

own like pre compiles in the sense like can I write my own K implementation for in this language I I'm I'm not sure I heard the question do you allow to write your own kind of pre compiles in the sense this language uh you as a user of risk zero uh of Z yeah yeah it's it's not well supported right now but that is on the road map yeah okay thank you again Jacob [Applause] [Music] [Applause]