ZK11: Compiling to ZKVMs - Alberto Centelles

Transcript

[Music] so I want to talk about today um I want to talk about compilers and cvms um why is that well as we know ckvm are quite expensive so the the time it takes to compute a normal program on a ckvm is generally a million times slower than the time it takes to just compile to a circuit directly so the question I was posing was how we can leverage the structure of a program using compilers and with these Transformations the question comes as well what

determines a ckvm um if we change the instruction sets are we still having the ckvm or not these are very technical questions very nuanced but in a way we are generating a different universal circuit and we are having a different ckvm the same question can be asked for memory checking algorithms if we change the algorithms we also change the universal circuit and we also therefore we also change the ckvm and with back is a more nuanced but at the same time um a backend kind of determines the armatization aration determines the circuit and even though the proving is orthogonal to the Circuit itself if we will see that the categories of ckvm are

um categorized by the backend of use like we have DKR kvms IBC ckvm Stark ckvm those are categories of the um using the backend as a as a main determining of a category so the outline of this talk is going to be first we're going to give some context about what has been done um we're going to also talk about what can be done um understanding the pain points of uh where ckvm are currently not working so well and then we are going to give some examples of how different teams and approaches um have addressed these different problems that we are also

showing so before we start diving into details I want to give some background of what is a ckvm so we see here is an emulation of a cpg architecture meaning that we have a an abstraction of a stack of a of a memory of execution unit as a universal circuit meaning that we have one single circuit for all programs meaning that we also have one verifier for all programs which is very nice that allows us to compute and proof any program up to a certain bound from a given set of up codes so what do we want and this is not particular to ckvn but in any proving system we want to maximize Pro and verifier performance we want to be able

to prove large programs um we want to be able to prove the right program meaning that we don't want to have backs in our compilers and and we want this to be used um so we want adoption as well of these proving systems and why do we want in particular ckvm well writing circuit is hard um it not only takes a lot of expertise from the writers but also it's very easy to make mistakes and different circuits require different verifiers whereas in a CVM because we have a universal circuit we only have one uh verifier which means that we are removing the pre-processing step that is normally quite costly and we want to prove large

programs um this is not particularly address as we are seeing with ckvm because they make generally the problem worse but this is something that at least we want to address in some way or another by the way this is going to be a qualitative type of stock so I will mention things like expensive and cheap and all that I will go very little into details but if you want to ask me questions afterwards I'm happy to go to through them as well so ckvm the the stages that we can generally recognize we start with a compilation of a program into a set of instructions we execute the program generating the ex execution trace or the witness then we prove it and here is

where the different categories of ckvm come um sometime we use folding sometime we use the gkr protocol sometimes we use Stark as we said um so we're going to focus on that thir step and then optionally um some people do another layer of recursion to compress and also to to achieve zero knowledge so what has been done I'm going to go through this very briefly because I think in this room we mostly know about um ckvm so basically we describe every every subm module of the ckvn like the stack the memory the execution unit in constraint system we apply a snark or a stark to

generate a proof generally we use Starks because they seem to be concretely more efficient even though um complexity wise are worse um and then we use some sorts of recursion to reduce the proof and verification costs and again optionally you can also do another recursion for for CK so this is some monolitic approach and as we going to see even though it brings some advantages like developer experience there is no more need to to know about cryptography ourselves there is a lot of tooling that developers can use there is more room for datability um because now we only need to address this set of up codes instead of any circuit that we are compiling to and we

have a universal verifier meaning that we it's only one verifier for all circuits the disadvantage is is quite clear is quite impractical for large programs because the overhead that this abstraction brings is very high and it means it's very high in terms of computational and uh memory-wise and in a way even though it's a minor problem we can also introduce bus in the compiler so it's not as much as compiling compiling directly to circuits but still it's something that um this approach can bring so a different variant that was brought um in 2008 but mostly recently with a lot of work related to folding

this IVC ckvm so the idea is that we are not only splitting the the prover but we also splitting the statement itself so we chunk the program into different chunks and we prove each piece separately and then we at each time that we are proving each of these pieces we are verifying not only that transition but also all the proofs from Genesis up to that point and depending on how much work the verifier does we have different uh variants of this IVC schemes um if we have a full verified algorithm inside of each of these State transitions we have full recursion accumulation brought some of the

delaying of the verifier up to the last um step with with um particle decider um and then folding which is the currently currently the mostly the most widely used uh type of ivcc KVM allows us to delay all of the verifier work except for the folding to prove that the folding is done correctly up to the last stage and Supernova brought something really interesting which is that one of the requirements that this scheme brings is when I say this scheme is IVC in general that the function that we are proving at each of the steps needs to be equal and in the case of ckvm they are comprising

the whole set of instructions so that's that makes the pr linear to the number of instructions and that makes it not practical but Supernova brought this non-uniform IVC which allows us to to to pay only for the cost of each instruction that we are um Computing at each of these steps okay so the advantage is that folding is cheap because this is the only um work that the verifier is now doing it addresses the memory limitations that we were seeing in previous approaches in which there was this huge uh ckvm that was in practical for large programs and now we also have nonuniformity allowing us to have some practical use case for for ckvm because we only pay the price for

each of the instructions and not for the whole set of instructions the disadvantages is that and this is we're going to to focus and it becomes almost the beginning of the of the exploration of what can be done is that we are still not exploting the structure of a program and in these constructions the upcodes are executed sequentially so that means there's some overhead for the prover and then the prover time is is generally worse than um naively compiling or directly compiling to a circuit so what can be

done well the first thing that we can not is that we can leverage Cod structure so before proving any program we are generating generally the execution Trace so meaning that we know at each each gate which which inputs and outputs have been passed um and we know the patterns of a program so in this case if we look at let's say how we can abstractly represent a program we can see different blocks so depending on what these blocks are it means that we have different um even ckvm so let's say that we compile each of these blocks directly to a circuit and this becomes our instruction set well then we go back to the initial problem of compiling two circuits is

very tricky um if instead of this becoming our instruction set they may become some sort of co-processors or pre- compiles that we may find in some of these cases then this is something that is currently used by many teams and it can allow to to make the the pro faster for certain programs it can be just blocks in which um they contain still the set of up codes inside of them and this is something that as we're going to see is used by some of these approaches um to generate blocks that separate abstraction from set of up codes to something

else um some of these proving systems leverage um this notion of data parallel circuits so we want to identify circuits that contain certain identical pattern or substructure um that is identical um and then we want to use these proving systems to leverage this uniform structure and another um obvious um General ization of IBC is this this thing called proof caring data which allows us to do folding not in a sequential way but in a three like way and each of the nodes uh only depend of

the on the leaves and by proving the the root of the tree we prove the whole computation so now we are going to see the different um examples of different teams of how they have addressed these particular problems to start with i chosen the gkr ckvm so I guess that some of you are familiar with the gkr protocol which is just basically a bunch of s checks combined that they layer the circuit into different layers and each of the layers you apply a bunch of s checks so uh Tyler 13 in one of these papers that he wrote um he proves that this gkr

protocol is friendly to data parallel circuits in particular this is also going to to be important they don't need to commit to intermediate data because they use the S protocol and also because they use the S protocol the Prov runs in linear time and by the way this paper is uh written by these guys here uh I think he Pioneer by the scroll foundation so the main idea is that they execute the program so they know which op codes are used in the program and then they group this identical up codes that is it varies depending on which program you are Computing and then they generate proofs for each of these groups and also a proof for each for for the chip that glues all these all these up

codes together M meaning that it preserves the the global State and the sequentiality of these up codes and they do it by something they call asymmetric gkr that we're going to see that it brings certain benefits but also um is quite expensive in some other ways so the advantages of this approach is that the prover is really fast now we no longer have this uniform [Music] um circuit but the program adapts sorry the the pro adapts to every program now we're going to see how they address it because they do it in a in a two- layer

way so that at the end of the day we have a uniform circuit um it can be parallelized because now we have identified these data parallel circuits and then we can apply the distributed Vergo for example prover or the gkr algorithm as they show it here um and then they eliminate the overhead of as we were seeing for example in IVC of up code selectors uh branching and the universal circuit so the disadvantages now is that each program is different meaning that we no longer have a uniform circuit and then they have this second layer called the from verifier which is some sort of ckvm uh and it's a recursive recursive

step to accommodate all the different proofs that come from the non-uniform provs so this circuit is huge and the only intuition I can provide now to understand why this may be practical is that the to prove um to to to verify one of these proofs is logarithmic to the size of all these proofs so it may be somehow trable and in fact they show that it it is it is quite practical for most cases and one of the other disadvantages that this approach has is that DKR even though it can be parallelized it works better when the circuits are um very big and the reason is because

they don't commit to the intermediate wires uh they only commit to the inputs and the and the outputs shallow circuits like up codes um don't work very well with this approach so for that they provide some sorts of variant to this to this approach um again they compile the program to assembly and then they identify not no longer they group up codes into identical groups but they find basic blocks so basic blocks what they are are uh chunks of code that they don't have a jump within so in this case we have a for Loop and then because B2 is Computing

many times and it's identical we can it becomes a data parallel circuit and then we can use paration to improve the performance of the Prova um and again we have the gluing the gluing chip circuit at the end again the advantage is that we have a structure aware prover um we don't have this control overhead at the upod level so now we only have some sort of control overhead at the Block so at the beginning at the end of the block um repeated blocks can be can be proven in parallel and instructions are no longer shallow circuits because these blocks are generally quite big but again the disadvantages are the same as we had earlier that each program

is a different circuit and then we need this uniform verifier circuit as a recursion circuit at the end this was released yesterday so second example I wanted to bring is called yolt the main idea of jolt is that we are now compiling to the composable evaluation tables so what the composable means is that you can take a evaluation table and split it into chunks as well like smaller subtables and then you can provide a combining function that glues them together in this case for equality is the product so

if you you distructor this big table into two into many small ones and then you multiply them you have the same result and they also bring this notion I mean they don't bring it but they use it the M multilinear extensions um to remove the commitments so now these small chunks that we have split it um we can create a multilinear extension of that chunk and because the verifier if they want to compute it they don't they only need to do some um think is logarithmic to the size of the chunk only that's quite tractable so

they don't need to commit to the to the to the Matrix anymore and that makes it um appealing to or trackable this problem of splitting a matrix into multiple chunks if we want to go briefly to this example um if we have four inputs so X and Y each of them have two inputs uh we have a a tables of vector size of 2 the^ of 4 and we can deconstruct it into two vectors of 2 the^ of two so the reduction of of these matrices is exponential whereas the multiplication is linear so you can see how the structuring a huge table in the case

that they use maybe 2^ of 64 or 2^ of 28 it can be easily deconstructed into multiple smaller um matrices they want to well they propose this notion of look lookup singularity in which you don't longer need to write circles yourself which is quite appealing it makes it more auditable um and brings less backs arguably and they have also this extensibility property that if you're thinking of adding new uh chunks to the this ckvm you just need to append your Matrix into the huge Matrix and the the construction is going to be still quite um

efficient so how can we use compilers in this approach I guess that the question boils down of how efficient it is to create one of these evaluation tables so in the example that we used before with a program if we identify the different blocks can we add them can they become distraction set of yolt um I mean again the question comes how efficient it is to create these valuation tables but maybe we don't want to do that maybe we want to only use some of them to efficiently improve Yol because adding instructions to this huge matric that y that Yol um basically consists on is very is very easy just

append um some other instruction evaluation table um and then again another question for compilers is what is more efficient to is it to add small operation with multiple lookups or is it to add large operations with few lookups the last one I want to bring also very interesting even though it's not a ckvm is mangrove this is a paper that recently came I think two months ago um the idea is that now we are compiling a program into identical steps which is uni which we call here uniform chunks which are also data parallel circuits if you think of IVC the structure W works also with data parallel circuit they need to be the same F at each of the steps in particular Mangrove um takes advantage

of the plunk arithmetization the vanilla plunk um because this is very close to data parallel circuits um in plunk you have gate constraints and you have copy constraints G constraints can be split very easily very naturally whereas copy constraints they're Global so you may a block that you create in a Chun that you create in this in this approach May reference to another chunk that is in a different uh another wire which is in a different chunk but they have a way to address it that we are going to see in a moment and then once they identify these identical steps they run a tree based PCD for polarization and they have also a very

nice technique of decoupling the leaf computation as you can see in the the right diagram from the control merging computation so this is how a uniform chunk looks in Mangrove you can see that um each of the chunks receives the the the vector of wires the vector of of permutations and the vector of selectors they have the constraints of the copy constraints and the and the gate constraints and they do something very interesting with the global copy constraints because they need to prove that some invariant has there there's an invariant in two

different parts of the circuit um and then they do some Grand product but because they want to do this chunking they are able to to decompose as well to chunk this Grand product into multiple ones and even though each of these ones will not result into one which is the the computation that we want to get here um the product of them will be one at the end and one thing I want to note here is that they also realize that the most costly part of this approach is constructing the commitment openings of the commitments that we have here so they have um very interesting way of

addressing that and they call it commit and commit and fold so just to quickly recap the advantages they remov the overhead of multiple up Cates even though now this singular chunk has some overhead because of the selectors and all that um they have a way of removing the merging logic at the leaves so in this PCD they can also tweak the arity of the of the tree so if they have a huge big number of of leaves then most of the computation comes at the leaves um and again they remove the en coding of the commitment opening constraints um so allows them to have a efficient PR over committed values and yeah they also address the problem of

memory and they can be run in parallel okay so these are the three examples there are many more we have lur um we have Nexus we have other Pro projects that I wanted to bring but there was restriction in time so I wanted to just quickly recap what does the future look like it seems clear that we want a compiler to chunk the statement itself we want to combine the pieces using one of these techniques it can be IVC can be gkr can be lasso for lookups seems that we want to also experiment with abstractions outside the CPU unit I didn't talk about Nexus but Nexus also talks about co-processors but we have seen here how blocks can come to the picture how uniform chunks can also be

used instead of um instruction sets and we want to to leverage parallelism to achieve monolithic snark performance this is something that Mangrove claims they do which is very interesting and for that we want to identify what are the data parallel circuits and we want to apply proof carrying data and the last one that jel Pioneers is the use of lookups so thank you for coming today I wanted to ask a question if you know of certain other ways that we can use a compiler to improve ckvm I want to to to point to some of the work I've I've written a report um has some has some time now but still worth

checking uh an article I wrote recently um at anoma we have a resource machine and we want to we are experimenting with different buend so if you if you happen to have a buend that may be interesting for us or if you are also researching on this area I'll be very happy to talk to thank you thanks a lot all right do we have any questions for Alberto great presentation Alberto um just curious um what served as kind of

the foundational inspiration for this work well as I said earlier there is we don't have performance ckvm so it takes a million times longer than whatever direct compilation to circuits take so I don't think it limits a lot the use cases that we have currently for ckvm so the the work can be done by tweaking and making things more performant in a very uh concrete sense of approving systems but then we also have programs that have certain structure and then um at a in particular we have a compiler team that they they can tweak a lot of

the parameters so we can not only rely on the performance of particular proving systems but help them in some way so that's why I'm also interested in collaboration any any other questions go for it all right this is not going to quite be on the ZK side of things but just to get a mental picture in my head this would almost be like a profile guided optimization pipeline where you run the program you find out something about it and then you yeah adapt the prover accordingly yeah exactly and then the decision this this intersection between

compilers and ckvn once we identify let's say data parall circuits or repetitive codes or like ecdsa I don't know um whatever that we identify as in the compiler how we can leverage that from the proving system so this this this constant communication between the two yeah just placing it at my head thank you okay I guess that wraps it up thanks a lot Alberto thank you [Applause]