ZK7: Spice up your ZK with some kimchi - Joseph Spadavecchia & David Wong - O(1) Labs / Mina

Transcript

[Music] but on this stage i want to welcome joseph and david from of one labs who are going to talk about spicing up your zk with kimchi hi everyone uh yeah okay so it's me david and i came here with joseph hello we work for owen labs and we came to talk about kimchi oh i'm going to take this kimchi is the zionist proof system which is part of okay oh oh oh uh we have another one all right

kimchi is part of mina which is a cryptocurrency uh it has a lot of cool stuff which we're not going to talk about so make sure to check it out we're only going to talk about kimchi which is this small cog in the machine and that's our zero entropy system okay to set the context um what do we use it for in mina it kind of drove our decisions and things like that so on the one side we use it for the succinct blockchain and in that kind of setting what we do is every block has a zero knowledge proof of the state of the blockchain at that height and then it has the verification inside of that proof there's a verification of the previous blocks proof

and the other thing that we use it for are zk apps and these are new like zero knowledge smart contracts with privacy um okay and like the kinds of things we're doing in our proofs or what you might imagine like verifying mina transactions or mena blocks but also now zk app state transitions okay so um where where are we going in this in this presentation well we're going to start with an overview of kimchi and mina david's going to present that then i'll talk about what kimchi is exactly as a proof system um and then we're going to deep dive into

an interesting part of our proof system called the expression framework and after that we're going to close with some remarks on tooling and a cool specification framework that david built cool so to put things in perspective uh i'm just gonna use that to put things in perspective so uh before we even get to the to proving things we need to write circuits uh today we have snarky it's an old camo library that you can use to write uh circuits for our proof system snarky is written in oak camel so not everybody knows ocamo it's kind of hard to use that's why we use for mina but we're also coming out with snarky.js which is a typescript library that you can use to

write circuits using typescript so it's much more user-friendly and we encourage people to try and use it and see if they like it and once you have that circuit basically what kimchi comes into play so you can compile that circuit down to a prover index that you can use to prove the execution of your circuit the correct execution of your circuit and on the other hand you can also compile it to a verifier index or verify key uh which you can use to verify uh the proof and uh we're also so mina is also coming up with zika apps so this is our zero knowledge smart contracts and so in that sense it's not out yet

i don't know when it's going to come out but i think there's a timeline for it if you're interested but basically you'll you'll be able to write these uh type street smart contracts um and deploy the verifier index part on chain uh so that people can verify your your proofs basically yeah okay so what exactly is kimchi it's it's a plonkish protocol so we use the arithmetization and the protocol and we use pluck up as well and for the commitment scheme we're using bullet proofs so it's a trustless setup so there's no toxic waste or anything like that it's quite cool and for the recursion we're using halo style

system that we call pickles and of course that system needs special elliptic curves so we're using the pasta curves excellent um okay yeah just as a reminder how plonk is plunk and plunky the circuit is basically a bunch of gates with coefficient parameters and then the witness is connected with wires like different parts of the witness or gates like that and in kimchi what we've done is we've extended this to the witness to be 15 wires and we've kind of divided these into two kind of groups there's what we call call i o registers and these can be connected with wires and use a permutation argument

and then on the other side we have temporary registers which cannot um and um we implement a lot of custom gates so next slide um we use uh we have a poseidon gate to do the poseidon cryptographic hash function which is snap friendly and great we also have custom demonstrates for elliptic curve operations and even cha cha encryption and that last one we're using plug up to implement it next uh cool so we're switching and we're going to talk about something else uh so you got an image kind of a picture of what we're doing with like it's a plunkish protocol and we're or all trap long some people call it uh now we're going to talk about uh some

part of the implementation um so basically this is a visual representation of every time we try to write constraints uh for our particles so custom gates or lookup was pretty involved also and we ended up with code that was really hard to understand and write and review and maintain and etc so so we we thought we had to like fix something and we came up with this expression framework which basically makes it easier to write these constraints and read them by creating this intermediate representation that you can use to pretty much write these constraints so i guess we're going to dig deeper on that

you might think that it's not super important but it's actually a big part of our implementation and yeah it allowed us to make a lot of progress pretty quickly so let's look at an example okay um i'm going to take you through an example so if you have experience with writing custom gains or things like that you you'll kind of maybe be familiar with some of what you're going to see but the idea is just to motivate why we wanted to make this abstraction so you know even for a generic gate the code was quite complex so on the top you have actual code from our proof system and it's the code that corresponds to the planck generic gate and we have the equation for the constraint below

so let's have a look at what's happening here what the developer is having to do and all that code above it's actually not important to read the code i'm just going to highlight to give you the idea but essentially you know the obvious things we need to the code needs to reference uh the selector polynomials and you can see that here in red but what we notice is that there's really no mapping between the code and the equation it's it's not even clear you know the number of places it's reference is only three but it apple appears all over the place uh in the constraint and it's similar for the witness polynomial here like it's referenced like five times in the equation but there's

just these three weird references to it in the code so even that doesn't seem to line up and beyond that we see things like this where the developers having to get into kind of proof system details and worry about separating the constraints um so that would be separating this gate from this constraint from like others in the system and in fact he's having to choose like a specific mechanism to do that so the powers of alpha and what's interesting here is that as you can see from the equation this is not even part of the real constraint it's something wrapping around it so that's not really desirable either to have to be concerned with those things when developing a gate the next thing is

all over the code the developers like having to specify which evaluation domain to use and even in this case switching domain for an optimization to make the code faster and um you know that's kind of not great either because those things are really kind of could be done by the proof system automatically so yeah so the first problem yeah just very obvious thing the implementation doesn't closely remem resemble the constraints and the second problem the gate developer needs to do all this proof system stuff that really shouldn't be concerned with and finally if you want to do optimizations they're manual and you have to do it for every gate but would

be really cool if we could somehow abstract that and do it automatically so basically what i just said too many non-essential concerns manual and error prone so yeah this was a problem for us and it's something that we wanted to make easier and our idea for that is this expression framework which we're now going to try to explain so david's going to show you what happens to all this code using the expression framework yeah so basically the code on the right is what happens if we use the expression framework and as you can see it's much less code than it used to be so that's the biggest plus and if you if you look at it

the first three lines are just like helpers so it's not too important but basically we're setting up variables in our equations and then you have the final equation and and here again we don't care about powers of alpha to like separate constraints or anything like that oh yeah sorry that's the zoom wait uh is it working yeah yeah so if you look at it it should look pretty close to the plonk equation that generate gates with the witnesses and the selector polynomials and things like that if you don't know plonk maybe that doesn't make sense but all right sorry oh yeah i guess

let's go to the next slide uh all right so how how does it work that doesn't work we're gonna describe now how it works we don't know how that works but you know okay so yeah the essential thing that's going on is like software engineering we're separating concerns we identified a place in the system where it just doesn't make sense so we're separating like the gate developers concerns from proof system concerns and from the gate developers perspective it just makes things easier and the cloud cleaner from the proof systems perspective we actually get something there too we get the ability to call

into this expression framework and get things the prover needs or the verifier needs yeah so how does that work well we have a symbolic multivariate polynomial or representation it's like an intermediate representation so you're able to write this code and it you can think of it like an ast or something like that and then we have a system behind it um i'm terrible at this yeah and okay and then there's a system behind it separate that is able to interpret it and then process it

so yeah so there we have kimchi here and like this subsystem called the expression framework and so you define your gate it goes in it becomes represented with expression and then the expression framework can do different things like the constraint separation and you can switch evaluation domain and interestingly you can also do optimizations on the expression itself and then on the you know the proof system itself can then call into it for things that it needs to do so it can do you know call into it for linearization for the verifying approver and it can call into it during proof creation to get evaluations and

now david is going to talk about the actual abstract representation yeah so just to give you an example if you again if you look at the plonk uh generic gates or the normal you know gate of planck you have this expression and if you zoom there you can see how we write this expression in this abstract uh representation in this tree and you can see that different nodes are just operations between these variables uh we have the weakness the coefficient is just a selector polynomial and with this tree then we can do whatever we want so maybe one example is that when you linearize the protocol so linearization is a part of the long protocol

one thing is that you cannot multiply commitments together because we don't use pairings so here in this tree the multiplication on the right would crash at runtime or when you when you run your protocol if you don't evaluate uh one of one or both of the variables in the coeff and the weakness so in kimchi we evaluate the weakness but basically with that protocol uh we can kind of uh oh i think that's fine oh yeah yeah so so basically with this uh this this framework we can kind of play around and uh decide to evaluate the coeff and see if that works or decide to evaluate the witness if that works uh if we have a crash we know that we

didn't do the linearization correctly and we don't have to deal with like we don't have to dig too much in the equations and figure out because we have many gates uh what what is missing what evaluation is missing etc and then we can even try and decrease the number of evolutions we have in the protocol and these kind of things um yeah optimization so we we cache uh some nodes also so we don't have to repeat operations so it's quite practical combining constraints like we've talked about it i guess and yeah we're thinking about future optimizations there's a lot we can do with this intermediate representation we could just automatically cache things and not do it manually

we could simplify we actually use a lot of these to generate code and so we could simplify the way the code is generated to decrease the number of scalar multiplications or things like that uh in the verifier circuit so yeah there's a lot of things we can do there um cool so other features we haven't talked about but that are quite interesting also so we can uh generate latex we can print the latex basically uh all the this constraints in latex you'll see that again later but it's helpful to review uh constraints that we write uh we generate also a lot of old camo code for the oi camel side of our protocol so it's quite useful for that as well

we don't have to repeat a lot of code and finally tests are very easy to write using this expression framework like we managed to delete a bunch of code so that was pretty nice cool so yeah that's that's a summary but i think we don't have too much time so let's let's keep that okay so back up to the kimchi level um the whole proof system we have a lot of things works in the pipeline so one is a foreign field multiplication gate which would allow us to hopefully move forward and do things like verifying ethereum signatures or bitcoin signatures that's one of the crypto primitives that we need for that another also related to the same goal is catch act 256 gate

so more custom gates another area of interest is exploring kind of vm or byte code kind of based system to try to see if we can plug that in and you know we're thinking about rolling our own but we don't know if that makes sense when you know to introduce another system like that when we already have a couple really good ones so also okay i think carol has some licenses issues so we're not sure if we can actually use it uh you know mylon is pretty open for us to use it so yeah we're not sure if there's like some some issues there also yeah and um we you know we've done some research with cairo and um there's another talk on the breakout session about that so if you're interested go check it out

um again kind of related to plookup we've been looking into like different types of tables so runtime tables or custom lookup tables it seems kind of interesting for us and um david mentioned earlier that there's code gen for oh camel code but kimchi itself is all just rust the oh camel code is for kind of the mina code side of things because mina's written in ocaml and some of that code we actually would like to move across to kimchi and the specific things are the circuit framework and the recursion support we actually um have someone joining us soon to start that work um okay yeah so what david mentioned earlier we have these cool tools to kind

of visualize things so we have a framework that allows you to visualize a circuit it shows you uh the gates the wiring the coefficients and the witness and just can make it easier and we also have the ability to visualize the constraints themselves um i promise it is actually latex it's just there's some big numbers there and another thing we came up with so so our protocol was getting quite complex and and uh we're doing tweaks here and there uh and also as we added more complex features in the protocol like lookup it was kind of hard to kind of follow that so we didn't have a spec also so we kind of came out and uh brought a spec so i'll put the link at the end but

basically we have a spec that looks pretty nice we have some protocol diagrams and and things like that but also we wrote that spec using a tool uh that we wrote also called cargo spec and that tool allows us to extract parts of the code to create the spec so for example here uh on the top left we wanted to show kind of like what's the what does the proof looks like and we just extract uh the data structures from the code and like that if we change the code we still have an up-to-date spec and on on the bottom left this is my favorite feature uh i was a consultant in a previous life and basically usually what you do is that you look at a spec and you kind of like go back and forth between the code and the spec and you check if there's

any divergence and if there is one then it's a bug and so we have the exact we have the algorithm pretty much here for proof creation creation but these steps are extracted directly from the code and so you have the code here and the steps are basically special comments that we can extract and so here if you want to review that code or understand how it works you can just read the code and the spec is in the code itself so it's kind of a cool thing if you've been in security and you see that um cool so final slide uh we have the con that repo uh contributions are welcome uh we want more people to use it also we're doing a lot of effort to make the api more usable and friendly so if you want to use it please talk to us and

we'll you know spend the time to talk to you and and make sure that uh you can do what you want to do we also created a book i mean a book we call the mina book and we have a lot of foundational foundational stuff on like you know groups fields your knowledge proofs and so on so if you want to learn you can go there we have rfcs there and the spec as well is there so you can go on that link finally we set up a blog recently for openlabs we're going to try to post pretty often so check the check out the blog and of course all of that work is for the mina protocol so you know check them out also cool yeah that's it thanks [Applause] i think we i think we do have time for

one question if anyone has a question yes and thanks for the talk i have a question about the expression abstraction uh what's the objective function when you do optimizations and does it depend on the particular proof system [Music] can you repeat that sorry so when you do optimizations over the expression abstraction you said to reduce maybe number of constraints or something like that what's your objecting function what are you trying to minimize and does that depend on the proof system that's running uh yeah that's a really good

question it probably wasn't clear it's doing things kind of what it can do is for example if the expression is written out in a way where you could for example rewrite it symbolically to have fewer multiplications and things like that it's doing things like that but like tying into proof system and things like that it doesn't do things like that that would be provided on the proof system side the other parts yeah we can pretty much analyze that tree and you know lint it or kind of warn the developer one last note kimchi is general purpose so we we're really keen if people want to use it to do a project or build something or make github contributions that would be awesome it's something for everyone

cool thank you so much [Music] [Applause]