ZK13: R0VM v3, a multi proof system zkVM - Jeremy Bruestle

Transcript

[Music] Uh, hey everyone. I am Jeremy Bristol, CEO of Risk Zero. Uh, and today I'm going to be talking to you about the latest the soontobe version of the Risk uh, zero VM uh, version 3. Uh, so, you know, a little bit about me quickly. Um, you know, I've been programming since, you know, the age seven on the Apple 2. uh and you know have always loved building software, messing with software. Um you know I've also always loved math. I love to read a good math paper before bed as something to relax. Uh I I'm not a working mathematician. I've never proven anything novel or interesting. Uh but

the abstractions from mathematics I think inform a lot of what gets done. Uh I am also the co-founder and CEO of Risk Zero. Um and we were the creators of the first sort of risk 5 ZKVM. Um, so today I'm going to I'm going to start by giving you a brief history of sort of the work that we've done in the risk zero VM. Uh, so long ago, there we go. Uh, so many years ago, um, I think it was probably almost 10 years ago now, I first learned about the existence of ZK. I was reading, you know, something about probabilistically checkable proofs and the idea that you could verify an arbitrarily large computation in 01 time sort of blew my mind. And so uh I was very interested in figuring out how that

actually worked and understanding it. Um and once I understood it, I was really wondering when it would be practical to make something that actually was usable in the real world. One of the limiting factors in my mind on that was being able to do fast recursion. And then with the uh sort of release of the Stark paper by Ellie Ben Sassan, I was like ah this is coming into practicality. I tried to convince all my friends that this was a good idea to build zero knowledge proof systems. Uh but the sort of consensus at the time among my sort of hacker friends was that uh writing a bunch of polinomial con uh a bunch of constraints uh polinomial constraints in finite fields was not really programming and uh that there would be a lot of

difficulty making these things practical. Um and then over years me and my other two co-founders came up with the idea of building a ZKVM that was actually based on an existing well-known ISA the risk 5 ISA. And so we introduced sort of the first uh came up with the first idea of the risk 5 ZKVM. Uh and basically right after that I started building a prototype. Um and we were sort of also the first at the time to use a very small 32-bit field which was the baby bear field. At the time Goldilocks was another common field. So we named it baby bear because it was even smaller. Um and the original version of the risk 5 which was sort of our pre-incorporation prototype was uh very limited. it it had represented the

constraints in a C++ EDSL. Um we did a lot of inefficient things like putting the risk five registers into the columns of the stark. It took three you know rows to do a single instruction. Um the memory argument was pretty mediocre and most importantly it was not possible to run arbitrarily large programs because of the fact that uh you know as your program got longer your start got bigger and you eventually ran out of memory. Uh that said, it was enough uh to go get ourselves some funding um which we then parlayed into sort of our risk zero VM v1 which is our first production grade uh sort of VM. We moved we made a bunch of efficiency improvements including the memory mapped registers which are common today uh you know and reduced the

complexity of doing instruction. One of the big things was we also were the first to sort of introduce the notion of continuations wherein to run a very large program uh that takes up many many cycles. You would actually break the execution into segments where each segment was say a million cycles and then you would prove each of those uh independently and then use recursion to glue them all together into a single proof. Uh and what that allowed is to be able to run arbitrarily large computations. Um and so very shortly after that we uh built ZETH which was the first type one uh ZK EVM. So and you know we also moved to the we also had to produce a mechanism

to do paging to Merkelize the memory state between uh each of these segments uh which we used originally shaw as our mechanism for that. We built the first GPU acceleration and uh as of 1.2 we also introduced this idea of algebraic pre-ompiles which allows us to do sort of big integer arithmetic. Uh so for quite a while that was our our ZKVM. We recently uh have introduced the uh Z the V2. Um and this is really entering into sort of the real-time era. We've actually made massive performance improvements in terms of the amount of time it takes to do verification of Ethereum or proof the correctness of an Ethereum block. Actually when I sent these slides in we were just under 30

seconds and since then we are now uh around 20 seconds. Um, so we're very ho hoping to very quickly get down below the 12 second mark so that we can prove the correctness of an Ethereum block in real time. Um, I think it's worth noting that uh one of the unique features of our system is that it is the only sort of 100% open-source uh risk 5 ZKVM including the fact that the GPU acceleration is all fully open source as well. Um and after building circuits a number of times we ended up deciding that it was better to build sort of a DSL and a compiler for building the circuits. Um this has a lot of advantages uh specifically around the verification. We

also just made a lot of just straight performance improvements. You know reduced the amount of work it takes to do a single instruction. Um move to Poseidon based paging for more efficiency. Had a better memory argument. I think one of the key things too is that uh we are the only ZKVM to my knowledge that has done some work to formally verify that our circuit is um fully deterministic. So um people here probably know that one of the biggest sort of causes for soundness bugs in any kind of ZK system is being under constrained. We've actually proven in fact that uh our circuit uh is not under constrained in any way. So at least in that that entire class of soundest bugs is uh ruled out. Um and we're also

working on some interesting work with regard to supporting kernel mode in ZKVMs. So mostly I want to talk about with all that history uh in I kind of want to talk about sort of our next big innovation which is the version of the ZKVM that is currently under development which is the sort of V3. Um V3 is a fairly major refactor of the way in which we are structuring the circuit. Um particularly we're moving toward this uh idea of this M3 or multi- multi-ET matching uh which is a new arithmetization scheme that was pioneered by the folks at irreducible.

Um and using this we're going to actually be able to support multiple proving systems for the back end including both our existing proof system over baby bear. uh but also we're going to be supporting binius from irreducible uh and we're going to reuse many components of the circuit across those. Now one of the big advantages of sort of M3 is that it's highly modular uh which will which both simplifies the circuit itself but also there's a number of places where we're able to use reuse and we expect that plus the other improvements we're working to give us a major performance boost. Um currently we have some early benchmarks and some back of the envelope that show us that greater than a 10x performance improvement is possible. Um obviously you know everyone will be excited to see

when the thing is working enough to have real numbers but we're very bullish on this. Uh so I let's just talk for a moment about sort of arithmetization in sort modern ZKVM. So going back all the way to the original Starks the and the notion of air arithmetization uh effectively when you're building a ZKVM typically the idea would be that you are sort of executing uh over time and every row in your uh table that you are committing to is related to previous rows by some sort of set of constraints and so you're sort of viewing the system as like a a digital circuit. in some ways operating over the

time dimension. Um and then typically you also in addition have needed arguments for doing lookups or for memory arguments and there's been a movement more toward supporting sort of multiple tables and arguments relating them via sort of a bus or some other kind of memory argument. Uh not only for for really for two purposes. One is for sort of the pre-ompiles that people have been building and of course we use this for our pre-ompiles. um as well as there's been some work in terms of div subdividing up the VM itself into sort of multiple components each of which has its own separate uh table within the stark proof system but sort of M3's basic notion is to break this down into even finer grained components wherein

effectively you actually make each row of your stark tables unrelated to the prior or preceding uh and instead you connect them only via sort of this argument this uh multi multis set uh sort of mechanism and the idea is that you do this with this concept of channels uh which I I'll get into in a little bit uh more detail in a moment here but basically the the the key here is that you don't have sort of a main trace anymore you simply have these tables which each have rows the rows have no relation to other rows within the table. There's no sort of notion of temporality um or inter row relations. Instead, the

idea is is that each row represents some kind of a logical constraint and that that row uh sort of interacts with these channels. Uh the channel itself is effectively a tupole that or each channel has sort of a a tupil that you can push some value into the channel and then some other row of a different type or the same type can pull a value from that channel. And the idea is is that M3 imposes this sort of channel balance condition where uh I if if you push a particular tupil, some other row must pull that tupil. And if there's anything that you ever push without pulling, then the channel balance condition fails uh

and it fails. So, oh gosh, I'm running a bit behind. So, let me run through some really quick things here then. Um so, this simplifies the design quite a bit. Um, and it allows you to break things down into much smaller pieces and have much more natural abstractions, particularly for things that have nonsequential operations like Merkel trees, which I'll go into in a moment. Um, it also allows the it makes many things much more trivial role-wise parallelism because there's no relation between rows anymore. And it allows this memorization concept which I will cover in just a moment here. Uh so really quick example I'm not going to be able to go into this in as much detail as I was hoping but basically if you imagine say the paging argument uh normally we'd have to sort of linearize this but now

what we can actually do is we can make these relations between uh sort of multiple pages and basically for each one of these sort of you know page in nodes what that is is it's a row and it's basically pulling from a channel the previous Merkel one comp one node of the Merkel tree and it's effectively pushing into that same channel uh the two nodes that the Merkel that that compose that Merkel tree and there's basically local constraints within each of these things. Uh and by doing this we're basically allowing uh to sort of prove the correctness of sort of a graph of constraints rather than some sort of linear set of constraints which makes the process uh both much more efficient.

Additionally, uh you can look at for example when we're doing a risk five instruction, we can actually break down the instruction into sort of multiple different components. Uh so for example, we can move the actual unit that does say the multiplication outside of the main uh instruction processing engine and we can also for example move the instruction decoder outside of the processing engine. And because we can use the ability to push with multiplicity to a channel, we can for example reuse the same instruction decoding every time the same instruction appears. So since typically an instruction is executed many times in a loop, we only play the decoding cost of that instruction once. And by breaking

the problem of doing the full VM into much smaller parts that are connected via these channels, we're able to sort of get a lot more reuse and uh duplication. So this also gives us the ability to build sort of something that works across multiple proof systems and I wanted to kind of cover really briefly how that's done. So effectively the idea is is that once you have this model each of the individual tables becomes much simpler and you can actually use the same logical set of blocks and channels but with different concrete representations across multiple proof systems. So in this case we may actually use different encodings for what's the

tupils that go over the channels between say baby bear and uh binary fields and we in fact arithmetize each component separately. So if we have say a 32-bit multiplier the way that we build a 32-bit multiplier in baby bear is very different from the way we build it in binas. However, the logically they're doing the same thing. And so what that means is that we can use logically the same circuit across multiple different proof systems. And while it does require arithmetization of each of the components, they're much smaller. And more importantly, much of the sort of highlevel work in terms of how do you do pre-flight, how do you do early parts of witgen, uh much of that can be reused.

And so both the design of the circuit as a whole as well as um much of the implementation can be shared across the proof systems. All right. So, I think I'm out of time. So, uh, and any questions? Uh, sadly, we do not have time for any questions for Jeremy, but let's give Jeremy a big hand for this talk.