Modern ZKP compilers by Leo Lara | Devcon SEA

[Music] [Music] hi everyone so we are going to talk about a project that we were working on and and at at PSC that I mean when we apply the when we apply for this uh speaking about this the we were working on this but now we have stopped working on this so we are going to go through what we were doing and the reasons why we sto working on this so a little bit of of the retrospective of a of a project let's say uh so uh in I started working in 2022 on the ckvm that at that moment um PSC was working on uh that was based on Hall to kind of a plish arithmetization and because it's it was very complicated to to build something like that on top of Hell 2 it's inevitable that you need to abstract things so as a engineer I found there like a a treasure drob of of of really of really interesting abstractions to be able to build the ckvm on top of Hal 2 a lot of layers on top of the Hal 2 to be able to to reason about it and to kind of like yeah abstract on it and and and build uh the what we required and there like the things like the stay machines no it it seems like was like the right level of abstraction to think about proving computation on top of a plony arithmetization and the the cell manager that was used to kind of place things in a more efficient way on the blish table and also how to combine like composability with something that was called the super Circuit and Circ and this all this was built when I started working here but I started kind of learning uh learning about it uh and I found like this idea that these abstractions actually if they are make in an accessible way uh could make much more easy for the average developer to to develop CK apps and that something like this could help multiply CK apps development and with that we started chikito first as a DSL in Rust then we added a python frontend to make it even simpler with the idea that theel ERS didn't need to even learn Ras they could do it on Python and then after bringing it to several hacker houses and working with with Builders at a experimental level with with more information about how it should be built we started kind of creating our own front our own parel for a language that kind of has a similar syntax to circum but has a state machines and and more things so in the end what we implemented the steam machines there are the as the kind of the definition like the constraints of the transitions of State machines are kind of the circuit and the witness is the trace of a of a instance of execution of these State machines and that's kind of like the main abstraction at chikito and then with the cell managers we abstract how that is converted to the plish table and how the the the witness is is arranged in efficient way and can be is is independence of configuring different ways to try different things then another thing that we built is like arbitrary Boolean Expressions compilation to polinomial identities no so the the constraints are expressed as polinomial identities and and we build a system that any Boolean expression as complicated as necessary it will be automatically compiled to to to this and we kind of develop a a a mini theory about how how to build this uh that can be used in other languages like how to compile any any Boolean expression into polinomial identities then we also like compilers has to optimize and through optimization can get to better performance that wow I'm going super slow so yes we did more things and this is how it looks the code and uh yeah you can like for example here you can see like arbitrary buen Expressions that are compiled automatically to constraints and we saw like it was super easy and and users really quickly could develop like complicated things like Blake to Hash that in the ckvn we couldn't Implement on top of Hell 2 normally with it and we we check that they has the same performance are manually doing with h 2 and we found some things that can be better and and then the reasons to sunet it is basically ckvm the race of ckvm make us re that that now we are in a kind of ckvm era that the applications we want to build now are probably better built by on CK VMS and thank you for all the people participating in different stages on on Chito H PSC Engineers researchers and and grantees and yeah thank you very much thanks Leo Question Time have I had to accelerate a lot any question oh there I'll go closer I wanted to throw it you want to throw you can do next okay okay hey Lance yo what's up Leo um so question on custom constraint systems I saw that there was one of the um libraries that you all Ed when it comes to ccs and ZK VMS can you like are there any ZK VMS that are implementing for that to go from like plunk to air but that wouldn't be like a to go plong to air that would be kind of a easy translation I think like a not a VM but uh from PL to a be kind of easy translation no because the difference kind of the rotations work in the arithmetization so we we actually yeah we we implemented the backend as powder that is kind of air so powder powder yeah one of the yes the the ah I can show this yeah I'm famili yeah yeah so we impl back for powder that is kind of air yeah so yeah that's e plony and and and and and even CCS we implemented the in CCS sonov um so compile to we we didn't have time to check the the performance on zob uh but but it it was it was something that was compilable to many different uh proving systems do really cool I think there's a question here yeah you want to start it who who this one oh hi thank you Nikolai from terminal 3 a few questions actually first um can I um verify your proof on chain like in B 254 uh that's basically only on now yeah and then you said you made python but can I do a rust code and compile it and because most of cryptography is in Rust so rust is very useful here and Let's do let's do these two and then if you want okay okay so you don't forget so the first question on chain yes so we for for the CVM we implemented a verifier in solidity for the h to proof so as long like it depends on the proving system that you use in the in the back end if it can be verified on on because it's kind of independent on the proving system can compile to different proving systems and uh they generate different proofs so in the it depends on that and the second question R is built on Ras chikito was built on R and then we put like a parel front but yes you could interact and connect it with other h h two circuits built on R and kind of actually integrated together and another question okay we have one more question okay there yeah better you throw it you want to try again okay okay last opportunity H Too Short soad uh so I actually not sure I understand the difference between a ZK VM and a ZK compiler like a ZK VM takes your rust code transer like let's say risk five instructions and proves that okay yes so so so so the C so a ckvm is one circuit that it witness is the trace of the execution of a instruction set so the CVM is not a compiler it's a circuit that takes us witness the the trace of the execution and proves that you have executed the the correctly the TR the the program so so in that case you compile Ras to this instruction architecture and then uh yeah you you execute it and you get the trace and that verify that compiler takes some kind of description of what you Circle that and actually kind of outputs a circuit itself so you could build a ckvm on a DSL in a language I don't hear you yeah so what what actually executes the code like where what does the proof proof if it doesn't prove correct execution right with the compiler yeah with a compiler you generate a circuit that proes something about a witness so so a ckvm is a type of circuit no it's a it's a is a it's a type of circuit that that proves the execution of the trace of a specific instruction set but a circuit can prove any witness like this follow certain properties certain constraints in the case of the ckvm the constraints are the correct execution of the instruction set happy I knew that question I knew the answer if they ask something different I don't think we have time for one more question but please feel free to talk to Leo after he's talk