Currently work on a new language and compiler for ZKP at PSE / Ethereum Foundation. Previously worked on distributed and embedded systems. Always a student. Long time ago, worked for ARM, and built start-up as co-founder CTO uniplaces.com

Leo Lara

At PSE we have done much ZKP advanced development. From that learning we are building a language and compiler, that is summarizing much of this learning.
We answer questions like: Are compilers necessary in a zkVM world? What is the role of a compiler in ZKP development?  What are its most common components? How different ways can this problem be approached?
In this advanced talk, we will learn how we compile arbitrary boolean expressions, or how the Schwartz–Zippel lemma can be used to optimize

Stage 4

Modern ZKP compilers

 Hi everyone. So we are going to talk about the project that we were working on at PSC. That, I mean, when we apply for this speaking about this, 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 stopped working on this. So, a little bit of the retrospective of a project, let's say. I started working in 2022 on the CKVM that at that moment PSC was working on, that was based on Halo 2 kind of a plonkish arithmetization. And because it was very complicated to build something like that on top of Halo 2, it's inevitable that you need to abstract things. So as an engineer, I found there like a treasure trove of really interesting abstractions to be able to build the CKEDM on top of Halo 2. A lot of layers on top of the Halo 2 to be able to reason about it and to kind of like, yeah, abstract on it and build what we required. And there's things like the state machines, it seems like it was the right level of abstraction to think about proving computation on top of Planck's arithmetization and the cell manager that was used to kind of place things in a more efficient way on the Blanquist table and also how to combine like composability with something that was called the super circuit answer so again this all this was built when I started working here but I start kind of learning learning about it and I found like this idea that these abstractions actually, if they are made in an accessible way, could make much more easy for the average developer to develop CK apps. And that something like this could help multiply CK apps development. And with that, we started Chiquito. First, as a DSL in Rust, then we added a Python frontend to make it even simpler with the idea that developers didn't need to learn Rust. They could do it on Python. And then after bringing it to several hacker houses and working with builders at the experimental level, with more information about how it should be built, we started creating our own parser for a language that has a similar syntax to Zircon but has state machines and more things. So in the end, what we implemented the state machines that as the definition like the constraints of the transitions of state definition like the constraints of the transitions of state machines are kind of the circuit and the witness is the trace of instance of execution of these state machines and that's kind of like the main abstraction at Chiquito and then with the cell managers we abstract how that is converted to the Planck table and how the witness is arranged in an efficient way and can be, is independent so can be configured in different ways to try different things. Then another thing that we built is like arbitrary Boolean expressions compilation to polynomial identities, no? So the constraints are expressed as polynomial identities. And we build a system that any Boolean expression, as complicated as necessary, it will be automatically compiled to this. And we kind of develop a mini theory about how to build this, that can be used in other languages, like how to compile any Boolean expression into polynomial identities. Then we also, like, compilers has to optimize, and through optimization can get to better performance. Wow, I'm going super slow. So, yes, we did more things, and this is how it looks, the code. And, yeah, you can, can, for example, here, you can see arbitrary Boolean expressions that are compiled automatically to constraints. And we saw it was super easy. And users really quickly could develop complicated things, like Blake2 hash that in the CKVM we couldn't implement on top of Halo 2 normally with it. And we checked that it has the same performance as manually doing with Hello2. And we found some things that can be better. And then the reasons to sunset it is basically CKVMs, the race of CKVMs make us reason that now we are in a kind of CKVM era that the applications we want to build now are probably better built on CKVMs. Thank you for all the people participating in different stages on Chiquito, PSC engineers, researchers, and grantees. Thank you very much. Thanks, Leo. Question time. I had to accelerate a lot. Any questions? Oh, there. Go closer. I wanted to throw it. You can do the next. It's okay. Hey, Lance. Yo, what's up, Leo? So question on custom constraint systems. I saw that there was one of the libraries that you all used. When it comes to CCS and ZKVMs, are there any ZKVMs that are implementing for that to go from like Plonk to Air? But that wouldn't be like to go from Plonk to Air? That would be kind of an easy translation, I think. Not a VM, but from Plonk to Air would be kind of an easy translation, because the difference is kind of how the rotations work in the arithmetization. We actually implemented the backend as Powder, that is kind of Air. Powder? Powder, yeah. I cannot show this. Yeah, I'm familiar. Yeah, so we implemented a backend for Powder that is kind of air, yeah, so, yeah, that's, it's easy, Plonkish and even CCS, we implemented the backend in CCS, Sonove, so, yeah, it compiled to, we didn't have time to check the performance on Sonove, but it was something that was compilable to many different brewing systems. Really cool. I think there's a question here. You want to throw it? This one. Oh. Hi, thank you. Nikolai from terminal 3. A few questions actually. First, can I verify your proof on chain, like in BN254? That's basically the only one chain verifier now. And then you said you'd made Python, but can I do a Rust code and compile it? Because most of cryptography is in Rust, so Rust is very useful here. Let's do these two and then if you want... Okay, okay. Sorry, don't forget. So the first question on chain, yes, so we, for the CKVM, we implemented a verifier in Solidity for the Hello2 proof. So as long like, it depends on the proving system that's used in the backend. If it can be verified on, because it's kind of independent on the proving system, can compile to different proving systems, and they generate different proofs. So it depends on that. And the second question, Rust, it's built on Rust. Chiquito was built on Rust, and then we put like a parcel of frontend. But yes, you could interact and connect it with other Halo 2 circuits built on Rust and kind of actually integrate it together. And another question? One more. OK, we have one more question. OK, there. Yeah, better you throw it. You want to throw it again? OK, there. Yeah, better you throw it. You want to throw it again? Okay, okay. Last opportunity. Too short. Go back. So I'm actually not sure I understand the difference between a ZKVM and a ZK compiler. Like a ZKVM takes your Rust code, translates it into, let's say, RISC-V instructions, and proves that. Okay. So a ZKVM is one circuit that it witnesses the trace of the execution of an instruction set. So the ZKVM is not a compiler. It's a circuit that takes as witness the trace of the execution and proves that you have executed correctly the program. So in that case you compile RAS to this instruction architecture and then you execute it and you get the trace and that's verified. A compiler takes some kind of description of what you see to 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 actually executes the code? Like, what does the proof prove if it doesn't prove correct execution, right, with the compiler? Yeah, with the compiler, you generate a circuit that proves something about the witness. So a CKVM is a type of circuit, no? It's a type of circuit that proves the execution of the trace of a specific instruction set. But a circuit can prove any witness like they 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 his talk.

https://streameth-develop.ams3.digitaloceanspaces.com/transcriptions/6732fcf780d989c5b7b0bffb.vtt