The Future of zk-VM: Pioneering Optimization Techniques and Challenges

EthPrague 2024 · 2 Jun 2024 · 27:16

Ventali Tan presents the design of Valida, an open-source, LLVM-compatible zk-VM, the day after its alpha release with a C compiler toolchain. She explains why her team chose an instruction-set VM over domain-specific languages or direct compilation for zero-knowledge proofs, sets out criteria for judging zk-VMs (correctness, security and trust assumptions, prover speed, efficiency and succinctness, developer productivity and modularity), and walks through the trade-offs behind Valida's benchmarks and plans such as Rust support.

Speakers

Topics

From EthPrague 2024, hosted by ETHPrague.

Transcript

[Music] you oh sorry

oh all right um okay okay uh hello everyone uh welcome to my talk um today I'm going to talk about ckvm design trade-offs and RZ KVM uh which is called valita um the design considerations and and choices that we made uh and this is a joint work of uh eight of my incredible teammates um yeah and then let's start so yesterday we released our um Alpha uh dkbm and our C compiler to chain um I just wanted to show some impressive Benchmark um so own iterative Fibonacci uh we have up to

260x uh performance improvement over um alternative Solutions and um om sh to 56 uh we have up to like 54 times uh faster um in a CPU wall clock time um and this is CPU efficiency uh this is like thousands of Acts of uh efficiency improvements over other Solutions and this talk I'm going to talk about uh first why we adopted zvm instead of other Solutions uh for example DSL direct compilation um and then second of all um uh what were we thinking when we were designing valita so what are the uh

criterias that we were looking at um and what are the problems that we were solving uh and third is like right our our design trade-offs how are we making the tradeoffs to to achieve such performance and fourth is like our some some of our design choices and then I'm going to show the demo um and then talk about our future uh directions um so the first question uh I'm just going to skip really quick because I have a lot of slides um so what's the motivation behind ckvm how do you prove so singland Z knowledge that a certain programs was executed uh on a certain input and it had a certain output um so this is the motivations behind uh we're building ZK I guess in general um um and the problem with this

is that uh right the learning curve the tooling is really steep uh for example circom and a few other libraries are uh required developers to to learn uh right new languages or they need to write handr circuits it's pretty time consuming and requires certain level of expertise um and then second is the high time space and energy cost of generating proof um and we think that's right the the motivations of U behind this project uh there a few like approaches uh I I listed three here um so people who tried DSL before uh that includes like Ciro um air uh artworks um and ccom and a few others other there people who tried uh

direct approach uh actually anoma has a project that's uh been working on uh this direct approach um which is like compiling to um uh functional language directly and then there's this um Isa VM approach which is uh valida you know risk zero sp1 uh polygon miden um and we think that that's right Isa VM approach is right the future um will be the dominant way developers interact with their knowledge because uh it's more developer friendly productive and it's much more secure you don't have to audit all the circuits to make sure there's no bucks uh we only need to like right audit the VM formally verify it and so

it reduces the space that uh bucks can happen um and uh here we listed some like limitations of uh existing ckvm um so um uh just a few like for example right Kyra requireed developers to work in a familiar unfamiliar like language model um and second of all like um non of this uh other zvm are fully open source I think right now sp1 is open source but uh most of the rvms are are partially close sourced um therefore um you can't even like add sort of uh very like um some like uh optimized circuits to their uh uh libraries and stuff and

uh third is uh there are a lot of inefficiencies in uh other ZK VMS designs for for example memory models in some VMS and um most of VMS are targeting like Risk five uh which instruction sets that's um targeting at at Hardware uh settings and not in ZK settings and then the fourth is uh it's very difficult to it's not modular enough it's very difficult to integrate um advancements in in ZK uh so for example right now we support small fills for a lot of uh other VMS uh one or two uh it's it's harder for them to adopt um uh newer techniques in cryptography uh therefore we need a VM

that's more extensible more performant and more developer friendly um and now just you know after talking about the the existing problems what are the main criterias um for evaluating Z kvms right so uh there's Baseline which is like it needs to be correct it needs to be secure and to consider a z to be consider tqvm so it matches the reliabilities of of a tqvm um and then the second is performance so basically include like correctness security and Trust assumptions um and performance measures the capabilities of a tqvm so how efficient how energy efficient it is how

how how performance how speed is like how fast it is uh succinct um how succinct is the proof being generated and verified um and the third is developer productivity like how easy to use the Z ckvm is uh which includes like compiler uh tool chain support um uh whether it supports high level languages um and how easy is it to to write what's the ux for using those libraries um and um modularity so like how easy it is for developers to add uh um like a certain specialized circuits for right some use cases that want to uh uh uh work on um so this is our three uh main criteria so

just brief talk about like what does each mean right so what is correct means uh it means that the VM must execute the computation as intended right then the proving system must set satisfy its claimed uh security properties um and I'm just going to skipe this security security means like how uh the tolerances of the soundness completeness and the zero knowledge um and then trust assumptions um uh it it means like the assumptions about the honesty of the approver and verifier to to the conclusion that the zvm uh functions real reliably and then um so so uh for example that rvm uses uh fry uh PCS uh which has no trust assumptions but some other um uh ZK VMS

uh use like kcg which has uh trust assumptions and then you need to do setup uh trust a setup and uh and this is what this means uh and performance so uh there is a trima of like um performance is uh right it's speed succinct efficiency so for example if you like are much more performant and usually you generates like a larger proof um so I'm going to talk more about it later um but um briefly go through the concept so speed it means like how quickly the pro can generate proof right so we match this on um time clock uh wall clock time which is the time from

the start to finish off the competition uh and efficiency efficiency meets um the resources consumed by the prover um and it matches by like user time um so for example right if you have like multiple cores and uh if you're using five cores um and uh it takes like one seconds right so so like it's more the single core uh user time uh here is like speed how we measure speed is like single core um CPU uh proof generation time and then the efficiency is um uh uh core time efficiency and space efficiency I guess we Define this uh two efficiency here um sness means the size of proof generated and the complexity of

uh verifying the proof and it often includes the proof size and the verification time and the verification space uh so like I guess in conclusion there are like six criteria that we're mentioned here uh which is collect is security trust assumptions speed efficiency and and sixing this uh I also mentioned the easy to use perspective uh but uh uh I'm not going to talk about it here okay so um here this is like sort of the process of how right we built the the VM from grop and and uh this is like providing like a sort of process flow so we sort of right select you have to select a base proving systems and then

um uh develop a zvm uh so second of all we Des develop a DK VM with our own like DK friendly Isa um instruction sets uh and then the instruction set is actually tailored for uh maximizing the efficiency of Zer knowledge uh proving um and then third is we have to create a compiler tool chain to support high level languages um therefore we are writing this lvm IR to our DK vm's compiler backend um and now we support C uh we're going to support rust and and C plus and solidity and other of uh languages that has a lvm front end um and then four is um right we we also working on a hardware accelerated ckv

improving um system uh five is like formication so EF right now is like um working on this and uh uh we're going to like collaborate with a few other like fortification companies to work on this as well um so what are the design tools choices we have to make when you are building a zq VM um first of all uh what instruction set architecture are you going to use uh right and then um we designed our custom like ZK friendly Isa but most of other ZK VMS chose um risk five some chose uh mips I remember uh and uh second of all what languages

support oh well this is more the compiler uh tool train uh problem and then third should it be modular or should it be more monolithic fourth is what kind of Ariz strategy should we use uh fifth is right what field uh should the zbm use for the timization and then um what PCS should we use um and then what recursive proving should be supported uh if it should put if it's supported what approach are we taking um Etc so uh providing some guidelines uh this is a general flow for how zvm works I'm not going to talk about it but um yeah

uh okay uh so uh in the second half of the talk I'm going to talk about how we sort of um uh build this VM and then what what what are sort of um why are we thinking about like sort of Designing our own Isa and so uh this is uh just a interesting like notes that we're just thinking yesterday actually um so we were like discussing like um with my teammates that right like what are sort of the key Paradigm shifts in like instruction sets design and adoption um and we observed that right from like 1960s to like 2000 uh there is like a general shift right so like we used to

use like complex instruction sets and then we're gradually moving to like Risk like reduce inection sets and then we moved from like Vector processing to like more scalar Pro processing architecture we moved from single core to like multie we moved from fixed instruction sets to more extensible and module instruction sets um and then we move from general purpose to like more domain specific architecture such as like right TPU GPU uh AI related like uh chips as well um and then we also move from like power agnostic design like we used to not care about like efficiency right now we care a lot about how energy efficient the cheap is um and a few other OBS observations um and then this

is actually one of uh the the reasons why we sort of designed our own instruction sets is because we think that under the Paradigm Shift of cryptography of trustless um um systems uh caling uh we think that there needs to be a a new instruction set that fit for this specific application of um and um that's why we sort of designed our own instruction sets um and uh like if like if you sort of basic question we were thinking every day is like what instruction sets are more efficient to include in the ISA uh and to check in the star constraint system and what are

more efficient to just exclude from the EXA and eliminate from the compiler output uh by reducing them with a SE sequence of instructions right um uh and uh the the I guess the general thinking is that the differences between uh zkm Computing environment and the hardware environments are very different and um that sort of drives very um our sort of different Isa uh design decisions um so our valida Isa is a um Ultra we call this alra risk means like Ultra reduced instruction sets uh we only have about like 20 I think instructions um and it's very modular is very zq friendly uh and includes the

following modules it has a 32-bit L chips um and uh a CPU chip a memory chip a program chip and a 8bit Rand Checker chip uh this is a uh diagram of a basic uh Vala VM what it looks like and a few like uh interesting points uh so for example we have two general special purpose register we have no general purpose register um and that's because uh it sort of simplifies the code Generation by eliminating the need for the register to be saved and and restoring the calling convention uh and therefore like eliminating the need for register um spilling the code to be uh emitted um so

uh another point is we only have two Ram addressing addressing modes um and uh the program Ro can't be addressed um and there is no dedicated SP uh register um the calling convention uses constant size stack frames um right so this is the overview of like what the VM is compos of um first of all it has an execution engine and it rounds the V program and generates the execution traces um and then uh the prover proves the result of executing a program by by proving this valid

execution traces exist and then the last step is verifier it verifies that the results of um of executing a program and and giving a proof of that verification um uh these are some parameters that we're using uh I don't want to go too deep deep into it but we're using this baby bear fil field um we're we're going to support meren field uh 31 field um as soon as well um and and uh the current PCS we're using is fry we are integrating with base fold uh which is uh authored by one of our teammates had us um and um uh I'm just going to skip this this is like sort of

how how the pro Works um some techniques of optimizing the Prov so uh the star we're using is very efficient and um the very the only expensive operations he uses is a hash function um so we use gates with degree at most three and keeping the um fft and hashing c as low as possible so that's like one of the techniques uh this is just giv a few examples um and uh the second trick is that we use as a finan field that's extremely efficient um uh right now we use uh as I mentioned baby bear uh we're going to support meren

field um and this is the compiler back endend um so uh we are uh writing uh this lvm ir2 rvm compiler and uh this is sort of the how how the lvm tool chain work um uh so we're writing the lvm Val back end right and these are all existing tool chains right so lvm already support uh cc++ rust and uh all we're doing is to write the lvm a a back end and once that's done it's it's like function complete right now but um the point is like the unlock is that we can support

um c c plus Russ and all the other the languages that are supported by um lvm uh and the implementation is fully open source uh you guys can check it out at uh Vala XYZ Vala U we also uh the lvm repo is under Lita um but uh yeah so it's highly customizable I want to emphasize uh developers can just use uh the included compile time micros to generate uh with a little coding and then you can just uh uh add like the chips that um you wanted for your own use case um and it's highly uh

customizable um the demo uh want to show this another okay got two minutes really quick I'll skip most of part two hi I'm oh sorry this the the audio doesn't work um yeah it's all right um I'll I'll just send you guys the link can check it out later um okay uh ongoing work um so uh this is more in the proving system side but um we are uh thinking about well we are working on uh multivar approver snarks

um and uh we're integrating with Bas fold um and uh we are uh doing some optimizations on the fry prover um uh we're thinking about using Circle stars um and uh um and uh we're adding evm verifier we're we're working with the a few companies on Hardware Explorations um uh so this is what we're working on right now to further optimize uh uh the the proving system uh side um and we're also building this on developer interface to help developers to even more easily work with um RZ qvm so uh this would be like a platform

where you can build um templates and people can use other people's templates to build their projects and so basically you can just pick right whatever language that we support and then use somebody else like or um some app level templates and then uh we also have like an online IDE uh you'll be able to uh build your projects here compile um see right locally the proving cost whatever if that's helpful and then uh deploy uh uh on a platform right so on the platform you can choose like sort of the different Hardware configs you want to use uh the proof aggregation layer you want to use and uh and the network you want to deploy so we want to like support as many networks as possible um

so that's pretty much it uh just emphasize that uh Vala is a extensible performant and developer friendly ckvm uh we just launched our Alpha so welcome everyone to try it out and give us feedback um and we're hiring so uh we're hiring like a cryptography engineer compiler engineer and uh we're uh hiring for this Innovation team which is uh we wanted to do experiment on the VM and build interesting products um so if you're interested in any of these Bros uh let me know um and here's our contact um thank you all right that's very wonderful talk by vental I don't know if you have any

question you could raise up your hand okay hi thank you um I'm curious about like I saw the benchmarks were really good on the proving side uh compared to like jolt and sp1 um I'm wondering you know especially you talked about the trilemma what were some of the tradeoffs like for example I know sp1 also uses plony 3 stuff so what kind of trade-offs were made um you know to improve the proving speed and yeah um I think uh the main difference between us and sp1 is uh they're still using uh risk five um risk

B instruction sets and uh we are uh using our own sort of designed customed uh instruction sets I think that's a man differentiation there are a lot of right like the member arguments and a couple of other things are different too uh but I think in the proving system side eventually like everyone is going to right it would become a commodity and everyone is going to use the most performant and advanced uh libraries uh we are contributing to plank3 um and we're working on a uh more optimized version of planky 3 I'm not sure if maybe it's called planky 3.5 but we're working on that as well so we're going to like uh integrate with like a like a

more efficient PCS called base fold so we we're doing a lot of work on the proving system as well but uh I I personally think that proving system wouldn't be like a differentiator for any KVM um and every every proving system is open source anyways um so I think the uh men like optimization would be for at least for us would be um from the instruction sets uh and uh the compiler we have to like keep optimizing the compiler as well um so uh that's does that answer your question yeah um so on the risk five so you're saying succinct or sp1 is like a risk 5 VM and then that compiles to l VM whereas you guys

wrote I guess I I don't quite understand what the risk five thing was but I'm not sure if they are compiled to lvm but I know they're using this uh either risk V or reduced risk V instruction set yeah but I'm not sure about the lvm side thanks all right um any other question you you you said you right now you support c yeah right now I support c um but on on one of the the charts it it showed that in any case you know you go from by the c or rust you end up with lvm uh um code right um so what's

the what needs to be done still for to support rust for example what sorry what's because from rust you can already get this uh uh oh like I I guess we have to like different languages have different run time and have like there's some like work to do as there as well um and we have to support like um some because our valid design is uh different from other VMS so we have to so for example uh bro standard Library we have to like sort of fix some asge cases there as well I think that's my I don't work on the compiler side but I think that's like runtime and then we have to support like Library functions on top of it so we're working on sort of uh for example like

Ross standard Library support and a few other um support yeah thanks all right any other question okay that comes to the end of the talk for today please can we give ventalin an Applause [Applause] please all right that's the final talk for um the flower stage so by 5:00 will be having a closing ceremony in the root stage so thank you everyone for coming to um the talk and I so much appreciate appreciate your presence have a good day