ZK10: Lurk: From zkDSLs to zkGPLs - John Burnham

Transcript

Very happy to have John from Lurk Lab who's going to talk to us about So yeah, go ahead. Thanks. Thanks. Hi everyone, I'm John. I'm one of the co-founders of Lurk Lab and today I'm going to talk about the intersection of zero knowledge proofs and programming languages. So the main thrust of my talk today is this. So there are two seemingly disparate fields of zero knowledge cryptography and programming language design or programming language theory and increasingly these are drawing closer together and issues in one are impacting issues in the other and features in one are enabling new things in the other. So on the one hand a lot of the things that we're building in zero knowledge are starting to look

like programming language projects, compilers, DSLs, parsers, you know and on the other hand zero knowledge is offering increasingly powerful primitives that change what we can think of that we can do when it comes to designing new languages. So a little bit about my background. I got into Haskell a little under a decade ago and have been giant functional programming nerd ever since. Type systems are really powerful tools for making software safer and more more composable which are properties that we really care about in web 3 and ZK.

But the challenge is that you know with some exceptions most web 3 platforms don't natively support strong types and formal verification specifically. So if you want to prove that your smart contract has certain correctness properties you have to rely on off-chain tooling and it's very complicated. And most users probably aren't going to run it. And a lot of the projects that I've worked on you know really foundered on the rocks of blockchain scaling that I think a lot of projects have have run into. And um, you know, unfortunately it's not economically viable to run a theorem prover on Ethereum for, you know, 10 billion gas per per theorem, alas. Um, but so this is the context that I I got

into ZK. Um, so um, you know, for me uh, ZK has uh, you know, unlocked this really cool possibility where we can do things like formal verification, um, expensive off-chain operations, and then verify only a succinct proof uh, on-chain. So it's a really incredible capability and I think that um, that's uh, you know, going to really change how especially functional languages think about um, these complex operations. So let's look at just a really simple uh, diagram of you know, there's a lot more complexity than this but like a really simplified diagram of how programming languages work.

Um, at the top level we have strings. Strings are what you enter into the machine, strings are what you get out when you when things print. Um, and you know, there's some implied language semantics that is mapping strings to strings. You can think about it in terms of in terms of mathematical formalism, everything is just symbol manipulation. Um, but the more intuitionistic approach is then, you know, we have uh, strings parsing into some notion of an abstract syntax tree. Um, and then uh, we have an interpretation or an evaluation function that is defining how uh, AST inputs map to outputs.

And then in a lot of languages we we don't just stop at that that high-level AST, we actually do some additional processing and um, compile or type check or optimize or do various things and get to some target uh, language. Um, you know, there's a lot of detail that I'm I'm glossing over here but we can basically think about this is just a sequence of of uh, mappings. Um, so there are a lot of really exciting projects right now that uh, implement general-purpose uh, virtual machines uh, that are provable under zero knowledge. Um, so there are projects that prove the RISC-V ISA, the LLVM IR, the Ethereum Virtual Machine, uh, WebAssembly, and others. So, all of these are really exciting projects and I think we're currently in in a moment

of a Cambrian explosion of different kinds of approaches in ZK, and I think that's awesome. But, I want to be really precise, and I think it's important that collectively we be really precise about what ZK-VMs do and what they don't do. So, the ZK A ZK-VM proves specifically the execution phase of whatever machine code it targets. It doesn't prove compilation. It doesn't prove any of the other language tooling that you might use. And that sounds really obvious, but it's easy to forget when, you know, the semantics of your application or your business logic is defined at that higher layer. And because compilers are pretty good, it's easy to sort of to ignore that there is this additional step both on the prover side and on the verifier side because the verifier

um has to read back whatever, you know, the proof result was. So, if your ZK-VM is manipulating memory registers, right? If your if your opcodes are around, you know, you know, moves and and and adds, the thing that you're that you're proving is that the result of that computation is some value stored in these memory registers, and then you have to the verifier has to do some some additional work, and it's not probably not very big, but it's it is an additional step to turn that back into whatever semantic thing that they actually care about. Um And also, there's an assumption that your mapping of of whatever your your business logic is about when you compile, that that mapping occurred

correctly. And most of the time that's okay. Um but sometimes it's not. Um so, for example, let's say I have like let's say Rust. So, I have a Rust program and I compile I parse it and then I I parse it into you know, well, ignoring some steps, eventually I get to something called the the high intermediate representation, and then I do some additional compiling, and then I get the medium intermediate representation, and then some more compiling, and I get the LLVM IR, and eventually I get, let's say, RISC-V. And then I have something that that there are really good circuits for for for proving over.

Um And um so, the issue is that um these tools are not really designed for the ZK use case in mind. And specifically, I don't know if you you can all see this, but between the LLVM project and the Rust language, there's something like, you know, a little under 30,000 open issues. Most of these are probably going to have no impact on this proof process, but some of them may. And um there are, you know, known examples and known cases in industry where people really do care about this. Um aviation being an being an example. Um compiler bugs um exist, and we can't just assume that they don't exist um because you know,

compilers are hard. And so, essentially what we're doing, you know, if we put real economic value um on these proofs, and the proofs have an assumption the compiler correctly mapped inputs to outputs, we're creating the largest bug bounty program ever for compiler correctness, which as a compiler engineer kind of excites me, but as someone who who works in zero knowledge terrifies me. So, um and I really like this this Vitalik tweet. I think about it, you know, a lot. Um which is that, you know, one of the the the Achilles' heels of zero knowledge is that because of what we gain in terms of of compression, we also lose a lot of information that makes it much easier for an adversary to exploit a bug and then and not just drain a

single application, like in the case of smart contract errors, but also potentially to drain an entire platform. Um and uh yeah. So, um so, what's the solution? So, one solution is we could actually prove the compilation step, right? So, so a ZK-VM is universal, you know, Rust C is written in something that can compile to uh you know through LLVM to RISC-V, we could just compile everything to RISC-V and run the entire Rust compiler and LLVM tool chain. So, this is really expensive. This is probably way too expensive for most purposes and it doesn't really address the issue of compiler bugs. It just maybe gives the verifier a fighting chance to you know replicate that computation and and

see like okay, this is what exactly the prover prover meant. So, we can solve the issue of compiler bugs with something called certified compilation. So, this is a the architecture diagram of a certified compiler called CompCert which is implemented in the Coq theorem prover which is a very complex piece of software and it does have a RISC-V back end, but I think the reason why no one really talks about it in this context is that A, it's not open source, you have to get a commercial license for it. B, you have to use a subset of C as your front end language. Not even all of C, just like a subset of C99.

And and C including Coq as a dependency in your project is crazy and only crazy people do it. I might be one of them, but I recognize that most people you know view that as a as a non-trivial proposition. Okay, so so let's review. So, why does ZKVM's only prove hardware byte code? Because um you know, building new new compilers, building new infrastructure is hard and expensive. Proving existing compilers is hard and expensive and the tail risk of these bugs is not really visible or obvious. Like you're not going to get punished for it in the market. And so this seems pretty reasonable, right?

Let's when we're when we're building general purpose VMs, let's reuse mature existing compiler infrastructure. We can't generate proofs of compilation yet, but eventually we might and you know for right now it's good enough and and furthermore, you know, if we're doing this this stuff this work, you know, our part of the of the stack is fine. Like the the compile it's the compiler's fault that they generated bad code. The the risk five, you know, ZK back end is working as it's supposed to. Like its semantics are are obeyed. So, I totally understand why people are making this decision to sort of sweep the issue of of compiler bugs under the rug. Um but sometimes when you make locally reasonable engineering decisions, you get globally catastrophic outcomes. So, there's a scene in the in the HBO

Chernobyl series that I also think about a lot, which is where Jared Harris's character says, "Oh, why do the reactor control rods have graphite tips? For the same reason that uh Soviet nuclear plants lack containment buildings and why they operated reactors with positive void coefficient. It's cheaper." And in ZK, you know, it's cheaper to not think about compiler bugs. Compilers are expensive. They're complicated. They're scary. You have to hire compiler engineers. And, you know, who wants to I I mean, I'm a compiler engineer. I like working with but to a lot of people, you know, this is this is a big ask. But you know, the alternative is worse. Like if you if you think about, you know, Chernobyl specifically, in in many ways we're still living the externalities of Chernobyl. If you think about, you know, the impact that Chernobyl had on the nuclear industry and how that affects

climate change. And I think that that in ZK, um we run the risk of putting our externalities onto the user, of putting our externalities onto uh onto other people, which is something that has happened a lot in ZK in in web 3 in general. Like the DAO hack famously. And then we're going to have to pay that off eventually. And not just the the um project that, you know, is making these decisions initially, but we as a whole field will pay for it. So, um so I guess that you for ZKVMs, um I uh I really like the ZKVM projects a lot. I have huge respect for them. But I just want to stress that compilers, like nuclear reactors, are uh wonderful complex technology that can cause a lot of harm if taken outside their operating

envelopes. Um and compiler tools like LLVM were not designed to operate in a Z in an in a ZK context. So, if you want to use them for that, you can, but you just have to engineer for that. And and and I think the responsible thing to do is internalize those externalities um with formal verification, uh certified compilation, proofs of compilation, or other techniques. Um, which to be fair a lot of people are are talking about and and and doing. So, but there's another alternative which sidesteps this problem. Um, instead of trying to think about, you know, compilers and proving LLVM or CompCert, you know, we we don't have to prove hardware bytecodes, right? We like there's no actual hardware here. We're

we're simulating memory registers out of a pragmatic decision for, you know, the kind of front end we want and wanting to reuse work. But and that's causing issues. But we could just bite the bullet and directly prove interpretation of a of a high-level language. Like there's nothing fundamental about memory registers, you know, a tracing interpreter for for, you know, RISC-V versus um something something a little bit higher level. And so I want to contrast the notion of a of a ZKVM with a new idea, um a ZKPL, a zero-knowledge programming language um which which is that high-level direct interpretation. Um, so but by doing this we we don't only gain safety in the context of losing compiler bugs, but actually we gain some

safety in other ways because now our proofs are are closely corresponding to the structure of the proof intent. So, we get we get some additional guarantees around, you know, correctness of the of the circuit um itself. And also we get some we get we get some performance because now we don't have to simulate memory operations. We can just more we can optimize with respect to the actual thing we care about. Um, the other thing I want to, you know, point out that, you know, as as people are thinking about adoption, interpreted languages are a heck of a lot more popular than uh compiled languages. You know, JavaScript, Python have something like, you know, 20 million users combined. So, the most popular languages in the world are interpreted. So, um Okay so Lurk fundamentally is a framework for building ZK PLs.

Right now, we have a Lisp front-end, and that's an engineering decision because Lisp is powerful, but very simple. So, this this has allowed us to to isolate a lot of the a lot of the engineering issues that that, you know, the new things we have to build in in in doing this. So, but we're rapidly generalizing to, you know, many different kinds of um circuits. So, right now, for example, you know, our universal Lisp circuit, which is 12,000 constraints, used to be written by hand essentially. And now, we use a new embedded DSL called Lam to write it, and we could write DSLs could write universal circuits for other kinds of abstract machines and other

kinds of interpreted languages. We also have a universal data language. It's very similar to JSON, and we are extending it with um we're going to be extending it with support for algebraic data types, which is going to be really exciting. And then, I think the most exciting one of the most exciting pieces of work that we've we've done recently is this new implementation of Nova called Arecibo, which is designed to be very much focused on engineering and performance, rapid iteration, and now includes the Supernova extension for non-uniform IVC.

What this means is that if you do write a universal circuit using Lurk, using Arecibo, you can now support efficient co-processors for special purpose operations that allow you to essentially FFI from your universal circuit into your co-processor for, I don't know, SHA-256 or whatever, without incurring overhead in in the universal circuit or in the rest of your of your of your proof. And we have a that allows you to define these co-processors in Circom, um and we plan on supporting many other circuit DSLs for doing this. Um so, I want to now go through a few examples. I don't know if this really shows up, but this is a recent example of someone in our community, not not someone at Lurk Lab, but someone that that I don't even

know what his name really is, but um he wrote a Lisp interpreter in Lurk in the Lurk Lisp front end. So, it's not quite a meta-circular interpreter, but it's close. It's And so, now we're we're starting to build the non-trivial programming language infrastructure um in Lurk itself. And the cool thing about this is that this now has access to all of the the zero-knowledge primitives, you know, like uh commitments, you know, functional commitments, higher-order commitments um you know, that we've built into the language. So, I'm really excited to see what what people build um in the programming languages context um using that.

Um here's a JSON parser um which is also really interesting. One thing that I really like about this is that So, this uh this is a few months old um and was before we had support for mutual recursion in Lats. So, instead the person writing this uh rolled mutual recursion for themselves with an implementation of the Y combinator, um which is pretty cool that you can do that in a proof on the fly as a user. Um you know, I I just that's kind of mind-blowing. Um and this is uh my project, which, you know, sort of got me into this mess, uh is uh Yatima, which is a um a compiler from the uh from the Lean theorem prover um to uh to Lurk uh itself. Um and so, this

uh you know, was a really early project that, you know, is very immature in lots of ways, but what this points the way towards is, you know, when when this is mature, when this, you know, when this effort comes off of ice and we know the rest of the system is able to really support it, um we'll be able to take those formal proofs for something like CompCert, and now instead of having even the trust assumptions of the certified compiler um uh or the theory that the the correctness of the the certified compiler be a trust assumption, we can actually compress that into a zero knowledge proof that ships with your application. So, really what you should get in order to make zero knowledge in order to make ZKVM safe is you'll want to have not only a proof of the compilation and the compilation

happening with a certified compiler that does that is formally verified to not make errors, but you also want to have a zero knowledge proof that you can cheaply verify without installing or lean or whatever um with the actual application itself. And so, I think that there's a notion of chain of custody there that really is unable to extend through the whole stack. And that's the context in which I feel really comfortable with a lot of this amazing work happening on ZKVMs, you know, coming to fruition and really being useful without running this tail risk of of some catastrophic you know incident you know because of compiler bugs.

Um okay, so what's uh next for us? So, um the phrase that I've I've coined for thinking about this this notion of formal proofs um compressed into zero knowledge proofs is PCPs, you know, as analogy, you know, proof we have proof carrying code PCC, we have proof carrying data PCD, proof carrying proofs PCP. Um and this is kind of a general there's a more general idea of proofs of type checking operations in general so ZKTC maybe. Um and you know, this is all stuff that we're really excited to work on and there's implications for you know, things like you know, marshalling or serialization that that I think are going to be really cool. Um we also are planning on as I said earlier writing different language cores for you

know, things like JavaScript or Python or the zinc machine for OCaml. Rust actually does have an interpreter the the rust medium intermediate representation um has an interpreter called Miri um and um uh I think that's going to be a really exciting way to to write a zero-knowledge rust. And then um we're going to be implementing the full suite of Nova protocols including next parallel Nova, para Nova, and then hyper Nova for high-degree gates. Alt Nova and meta Nova I I made up as placeholder names for whatever new thing Srinath writes.

So, I don't know if that's what it'll be called, but you know, that's how I kind of think about it. Um Yeah, and so that's what that's what we're doing at Lurk. I think I have time for a few questions. Okay. Yeah, you even had time to finish whatever. Is it your last slide? No, that's my last slide. Okay, well, I guess we'll take questions. So, yeah, any questions anybody? Yes. It's a very generic question, but could you maybe please comment on the general complexity in terms of like, you know, computational complexity of interpretation of certain languages? For example, you mentioned Python,

JavaScript. I I don't want to imagine how long their interpreters, like how big their interpreter code is, but maybe some languages have really good interpreters. Something about that as opposed to compiled code, which is like, you know, very small operations that which can be quite lightweight. So, some interpreters are like are heavy, right? Yeah, but I think there's really an 80/20 rule when it comes to it. Like so, like JavaScript is is heavy in some ways depending on but like JavaScript there's a lot of different flavors of JavaScript. And so, you can you can like Okay, so take JavaScript strings for example, right? JavaScript strings have a reasonably simple semantics, but if you look at like like what V8 actually does to do like deal with strings, they do some really complex stuff to make string performance really good. So,

those performance optimizations don't necessarily apply in the provable context. They might or they might not. So, there are like there are tradeoffs you can make with implementing something that is um, either a Python subset or something that is Python-like. Um, and I think that as long as you get reasonably close in terms of semantics, uh, you know, especially for interpreted languages, users are reasonably forgiving of of, you know, like, okay, you you maybe you don't have big nums right away in JavaScript. Maybe maybe, you know, um, you are your IEEE IEEE floats um, have, you know, a different way of handling NaNs to deal with NaN non-determinism. I think that there are some details that that you can um, uh, you some choices you can make that

make the uh, the business of proving um, simpler. Um, what one example of this I think is um, that that's really interesting is is uh, functional um, languages like OCaml um, or Haskell that are that are very complicated. I mean, if you wanted to to do zero knowledge of all of GHC, the Haskell compiler, that would be quite complicated, but you could do GHC core, you know, that's a very simple uh, rel- or relatively simple um, you know, abstract machine. You know, for OCaml, there's a lot of, you know, features there, but the Zinc machine is is relatively simple. So, um, and a lot of those features are then related to, you know, the type system or extensions, you know, FFIs, things that you might not need in the zero knowledge context. So, I think that the that the

um, that yes, there is complexity there to doing interpretation. I don't think it's really more than um, than um, doing a hardware bytecode. Um, and in fact, I think the really the way to look at like like a ZKVM is really it's an interpreter of of a uh, of a hardware bytecode. So, so it's Yeah, I don't think there's a categorical difference necessarily. Can I ask another small question? Yeah. Uh, what would be the language that I mean, do you can you give an example of like a language that you envision to be interpreted? Like what one language that's like really convenient to write and like super easy to interpret, like, you know, 100 lines of code interpreter, like, something super lightweight.

Yeah. Like like Lisp? Yeah, so so Lisp absolutely is really simple to interpret in, you know, a few hundred lines. Yes, you have to like when you you add things to it and it gets more complicated, but the core of the language is really simple. OCaml is really simple. You know, the Zinc machine, very simple. Haskell, less simple, but but you can still So, I think that that there Yeah, I would I would say, you know, of of the languages I think that we're likely to do something, you know, in the realm of like, you know, a Lisp or an OCaml or or Lean actually itself is pretty good. Like in the in our Yeti ML compiler, we re-implemented an

interpreter for Lean because the theorem prover a theorem prover kernel is essentially an an interpreter. So, so there's Yeah, so I mean, we can't like jump into like really complex stuff right away, but I think that there's a pretty There's Eventually, people will write language cores for all these languages because why wouldn't you? I mean, if you if you do that, all of a sudden, you can take like the results in your language and prove it to that prove, you know, this program in JavaScript or or Python or whatever had this result. That's really powerful and and I think that it's it's a it's a programming superpower that once we get used to it, we're we're never going to go back.

Uh quick question uh So, for implementing something like Python or like Java, would the idea be you take the Python or JVM bytecode and interpret that? Or is the idea to stay at the highest level possible and try and implement the language semantics itself, write the full front end? Yeah, so so generally I I like the idea of of staying as high-level as possible, but where there are um you know, reasonable intermediate like I think for Java, right? Like interpret like doing a JVM makes sense, right? I mean, I think that the while there are potentially some issues going from Java to the JVM, I think it's a much smaller step than than, you know, going from like rust to, you know, risk

five. Um I I wouldn't start with it with Java. Like this that's like, you know, would be way down the list of, you know, languages that I I really care about. Um but um no, I like Java. It's just, you know, yeah. Um uh Python I think is a little bit is a little bit more interesting. Um I think that there are a lot of different um concepts within the Python uh world in terms of, you know, how to do Python interpretation efficiently. Um I think that um you know, and also like there are many many different Pythons. I mean, there's you know, there was Python 2 once upon a time and Python 3 is, you know, very So, I feel like you could get something that's a Python-like much more easily

than getting exactly Python. And that's kind of the approach that I would take. I would say like, let's try to get something that like, you know, like ZK Python maybe isn't semantically identical to Python, but has like a very like trivial mapping or it you know, there's an easy subset. And let's try to figure out those engineering details like incrementally rather than trying to, you know, um I don't know, eat the whole, you know, pie at in in one gulp. Um yeah. Um but like Lisp, I would say Lisp, OCaml, and Lean are like the languages that I would really be excited about. And and those have very simple semantics and I I, you know, at that core level um that I I feel pretty comfortable with. But I think other people will have different, you know,

languages they they understand how to do this. What really we're trying to give to people is this idea of like, okay, you have Nova, you have this ability to have a step function that you can fold over and the step function can FFI to special, you know, special-purpose things. So, if you want to do your JavaScript, you know, interpreter, now like you don't have to include like like, you know, float math in your universal circuit, you can call out to like a special a special co-processor for it. And I think that's like the key idea here that languages are combined universal functionality like the core thing that makes the language Turing complete, but which it would be inconvenient to write like, you know, lots of you know, your features in and then special purpose stuff that's there for for programmer convenience and quality of life, right? So, and that's

like the shape of what the Lurk tool chain I think is giving you with our co-processors and our our universal circuits. So, what once you have a circuit for your programming language, it seems like that circuit essentially becomes a formal semantics of your language because you know, it defines exactly its behavior in a mathematically well-defined way. Is there any way you're aware of how you could use it for formal verification for example, proving that on certain inputs this

circuit using directly the mathematics of the circuit for example, terminates or derive loop invariants or things like that? Yeah, I I I you know, it's a really great point. One of the the really neat things about this architecture is that it actually removes the need for something called termination checking in like, you know, which is something that you need to do in in like a dependently typed language, you know, where the type system can loop forever and you know, theorems are not sound unless you know, the the program is is is halting. You can make a zero knowledge if you can make a zero knowledge proof of something, then it it it you know, you know, it halts because the proof sort of shows that. You wouldn't be able to make the proof otherwise. The proof the proving step would just go forever.

But to to your point about formal verification, I think more it goes the other way where you have a form you would have a formal semantics of your language defined in some um uh you know let's say a theorem prover, and then you'd be able to extract um a circuit from that. I think that's more the relationship, but but they are very similar fundamentally. But would would I still be able to prove then that the you know if you have another formal semantics, you you still have to prove a simulation that your circuit actually implements. And so I wonder if you could use a circuit directly at formal semantics and you avoid having to do the simulation theorems that your whatever small step semantics implements the same semantics.

Yeah, I think that would be really interesting. I think I think that that's that's definitely something that we would want to explore. You know, we have some early work with with writing circuit libraries in Lean. Um and I think what I would want to do is I would want to be able to show that that that like you know if I have the circuit definition in Lean that then I can extract other you know knowledge or other other uh you know theorems about that that definition. And maybe it's as expressive as as you say. Um you know I would my my guess is that maybe when you go from formal semantics to circuit, you maybe lose some information or or you want to lose information. So one example you know might be that maybe you want to lose variable names, right? Maybe you just want to de Bruijn index everything, but

you still want the formal semantics to like have have names and now you have additional machinery that has to account for them and you know shadowing and you know you want like if you have like you know names in in Lean and you know you're actually actually using you know uh uh symbolic lookups, like maybe that's meaningful in that context. And so maybe there are safe transformations that you can make that you know where the circuit is not exactly the language, but I guess like the the point is my point is not anti-compilation, right? My point is that when we take a compilation step, you know, we we have to acknowledge that we're making a leap and we have to make sure that that leap is you know is is you know grounded at the start and at the end, right? That that we're we're you know that and and so we

would have to show that that those transformations are correct. Um so so I guess that's why that's why why think it would go you know from from the semantics to the the prover. Because I do think that there is room for for optimization to get like more prover efficiency. Like we you know, the the prover is its own context and we don't we don't necessarily it doesn't have to be exactly the high-level language, but you know, it needs to be tied to it very strongly. Thank you very much, John. Thank you very much.