leanVM in Lean 4

Transcript

Um, hi guys. Um, this is we're presenting some work on the formal verification of Lean VM or as we're calling it right now, uh, Lina VM. Uh, and yeah, this is an end-to-end formal verification of Lean VM with an asterisk which I'll explain a bit more detail later. Um, but first off, what is the motivation of Lean VM? So, the first thing as as always with formal verification is to increase the confidence in the security of Lean VM. Um, so that's kind of like the basic obvious idea. Um, another one is that, you know, no one has actually got a full end-to-end formal verification of a ZK VM yet. You know, a lot of people are trying. Zcash,

for example, had a presentation about this. Um, but we want to understand exactly what's missing, what we still need to think about, and what still needs to be formalized and modeled. And the third is, you know, possibly applying this sort of stuff to auto research. So, if we have a full end-to-end ZK VM, then, you know, we can start, you know, recursion.now fast is already doing this, but have something even more advanced, even more complicated, even larger search space for agents to to try different ideas. So, yeah, before I go into into what what actually formal verifying, a small background on Lean VM. It's a hash-based multilinear ZK VM.

It has, well, I mean, right now it has an ISA, Lean ISA, its own custom ISA called Lean ISA, which is like very very simple. It's just six instructions. Um, the referencing, we have a hash instruction for Blake 2s. Um, and the proof system itself is relatively, I would say, straightforward. It's just a mixture of sum check, GKR, a lot of batching. Um, and then the actual Blake 2s instruction and constraints are discharged with, uh, Flock. So, Flock, in effect, is a sub protocol and it actually has some effects on the on the formal verification because you have like a protocol within a protocol.

So, what do we actually write in the formal verification of Lean Lean VM? Um the first thing is we need semantics for Lean nicer. Um we we use this using a clean library which is sort of worked very well for our for our needs. Um and we also need a specification of the proof system, specifically the actual verifier and the honest prover, right? Um and you can say you know actually if I you know, don't care about completeness of my ZKVM, then I can ignore the honest prover, but it is good to know that your verifier that you've written isn't like arbitrary, you know, completely vacuous.

And then once you have your two specifications, you also need you know, you want to have properties about specification what it satisfy. And in our case, it is knowledge soundness and perfect completeness. Um and and note that I say knowledge soundness say knowledge soundness is very important, not just normal soundness because um you you know, in a ZKVM being sound can be like vacuous true. Uh like if I have a program and a public input, then like somewhere out there could exist a valid execution of this program, but it's not the case that a prover themselves knows what a valid execution is.

And you know, other things like signatures, um yeah. So, what does a valid execution look like? Um so, this is you know, Lean nicer specs um and you have a program, a public input to that program, and an execution trace of that program. And we say this execution trace is a valid execution if the public input to the trace matches uh what you started with, and if you run the program according to execution trace, then you you you end up at some final valid terminating state.

Right? And if at some point the execution trace makes a you know, is incorrect then uh this will this will fail. Right. Um the proof system itself, as I've said before, you have completeness. Um, and what completeness in this sense means is if I take a Lean Izer execution trace as a witness, give it to the honest prover, then they're able to generate a proof which a verifier will always accept. It's sort of very standard notion of completeness. And on the other side, knowledge soundness, so if a verifier accepts a proof, then you you have uh uh sort of a you know, a a an extractor which runs within some sort of

bounded, you know, polytime or uh linear time, which is able to extract um the a Lean Izer execution trace from a prover, right? And that yeah, um uh and you know, with some small knowledge soundness error. Um, this is for a fixed program on the public input. Um Yeah, and and so as of right now, what we have in uh Lean VM is we have both a verifier, we have a prover, we have a Lean Izer semantics, um but as of right now, the actual prover and verifier is an interactive IOP protocol. So, there's no uh as of right now, there's no PCS

has been instantiated, uh there's no Fiat-Shamir transform as of yet, um but we do have sort of a concrete interactive protocol. Um, and it has a soundness knowledge soundness error of 2 to the minus 159. This is not all of the actual uh Lean VM sa- knowledge soundness error is because you've got a lot more uh sort of a lot more objects that uh still need to be implemented, um but you know, we do have already some sort of concrete values that have been proven. Um Yeah, and because this is a work in progress, you know, here's the here's what's been done so far, and here's here's what needs to be done. So, we've got the Lean Izer semantics

specification which has been written. Um, we have a uh a notion that we have the the master theorem, so knowledge soundness, completeness, um modeled as a as an interactive as an IOP. Um Um but there's still there's still quite a bit of stuff left to be done for for what to say is like really an end-to-end formal verification. Um so the first one is the BCS transform. This is mainly a matter of just implementing it. Um But then we have some, you know, some more ideas, for example, recursion, which has been talked a lot about in in previous workshops. So that's, you know, we want to have a notion of recursion that needs to be uh thought about.

Um And what what personally to me is the most interesting is T4 here, which is um going from a proof about Lean VM uh and a proof about the specifications that we verify and a prover uh have to an actual executable certification. So this means that the verifier that we're writing in Lean 4 is able to accept is able to take an actual seri- you know, proof object, actually run through the steps and and output a you know, a true or a false. Uh and this is very powerful because then you can start doing fuzzing, you can start you can have test vectors.

Um And you know, this gives you a lot more confidence, you know, if you've got test vectors which are generated by the Lean 4 spec and test vectors which are generated by, let's say, your your Rust code implementation and they agree and they're consistent, then you can you can be a lot more confident about what you you produce is is correct. So yeah, like with any good FE project, um what what do I audit? Um So there's sort of five five, six different things that, you know, if you want to be confident about the formal verification of this project, um the first thing is the specification of Lean ISO. It's a very simple ISO. It's only 250 lines of of code, so

um you know, that it's quite relatively you know, not super super expressive, so it is as relatively easy to check. Um You have the security definitions and the the relation that your snark is proving. Like you need to be more careful about this, you know, you don't want to say that you formally verified something, but your your security definition of what you're proving is just incorrect. Um that's a bit bigger, 500 lines. Um but this, very importantly, doesn't include the verifier and prover aspect. So, if you just check the security definitions, you have a notion that you have you know, you have a notion that there exists a spec of a verifier and a prover, which is knowledge sound and complete, but you

you can't be get you can't be sure that this spec is actually what you've implemented or you're actually running in in production, say. Uh and now if you do care about faithfulness, and this is why I put two asterisks here, you suddenly you know, your audit sort of surface as of right now what we have in Lean AVM is is quite a lot larger. You're looking at about 1,200 lines for both your for each for your verifier and your prover. Um and so that that has to be quite extensively checked to make sure that the you know, the the algebra that your verifier is running and the steps that it's taking is actually what you wrote down in in Lean VM. Um and then as always with FE projects,

you've got sort of upstream library definitions that you know, you get from ArqLib, Clean, CoqPoly, VCC, VeriO. Um these are very important, but you know, that that's sort of you when you read for a project like this, you usually assume that your libraries to some extent are are correct and trusted. Um Yeah. So, to to go a bit more into the road map and what what we're actually going to you know, what we've got and what we're going to produce. So, right now we have an interactive protocol for for the verifier and prover.

Um We want to take the BCS transform to Hermes into a non-interactive protocol. Um And then finally, the holy grail is to have something which is executable. Um yeah, and as I said before, you know, this Assuming you come up with some other ideas, this this gives you a lot more confidence in in what you have. Um And now naturally also, you know, whether you do this or not depends on what you want from your FE project. Um so if if we're doing, you know, first bullet point of the motivation, which is to increase confidence and security, then this is something really really nice to have.

Um Really does increase confidence, but if you're just, you know, if you just want an auto research target, then yeah, maybe you do want something executable, but might not be so important right? Um Yeah. Uh and um you know, so we've with FE spent about 2 months formally verifying Lean VM. Um a nice sort of question to ask is, have you found any issues? Um So there have been some like pathological completeness bugs that we found in Lean VM.

Um You know, it's wouldn't really like it it like it was a completeness bug with like an error of 2 to the minus 192. So very likely to ever appear but um yeah, that's so [clears throat] you know, it wasn't perfectly complete. Um yeah, with sort of this is more crediting to Alexander, but with the help of the the specifications that we wrote in Lean, uh we were able to find some witness generation bugs in the Rust code. Um And also there were some protocol specific optimizations which sort of the Lean spec helped us find and and change in in the Rust code. And um The nice thing about this, because Lean is so structured and if you go about it

in a very, you know, structured way, the agents sort of are forced to to to think about, you know, very in very strong detail what they've they've just produced and it makes certain observations really really obvious. So for example, with the protocol specific optimizations, we basically found that some messages in the protocol were just completely useless and could have just been removed. And the reason why sort of we found that out because they contributed zero knowledge soundness error to the actual protocol. And so like that makes you think aha, why is it contributing no error? Like that's you know, it's a bit maybe not incorrect, but it's a bit dodgy.

And yeah, so it turns out you can just completely remove those those steps. Okay. Um How am I for time? I've been talking quite quite fast. Yeah, okay. Um So again, you know, this is very much work in progress. There's there's a lot of open problems to figure out and to to to sort of massage for a formal verification of the EVM. So you know, briefly what I've already said before implementing a BCS transform the recursion topology arguments have been discussed. Um and having a specification which can execute test

vectors generate test vectors. Um But there's sort of two more interesting open problems which which I believe do need to be thought about and I've not really seen anyone talk about in in too much detail. So the first one is the running time of the extractor in knowledge soundness, right? So we like I've established before that knowledge soundness is you know it's really an ideal property not just we don't want just soundness soundness and um we know like generally from a BCS transform in a random oracle model that you're going to have a straight line extractor.

Um But you know, if this has been generated by an agent, how do you know if the agent hasn't generated an extractor which is let's say brute forces every witness in a relation and you know, runs in some exponential running time. Um and this is very prevalent for let's say an auto research competition where the let's say in recursion.fast where an agent writes a very fast specification, proves that it's not a soundness, but also has to write the algorithm for the extractor. Um And And we don't have, as of right now, a good notion of what the running cost of an algorithm is. So, it's very possible that a um a an agent writes an extractor, which,

you know, brute forces a relation, um and our soundness collapses just to normal soundness. Mhm. Uh and sort of the second, I think, quite interesting uh research problem is there's always going to be this gap between, you know, what you run and what you've actually written in production and your specifications. The executable specification is is one way to tackle this, but, you know, is there something even better? Can we, you know, prove equivalence between what we're actually running and what we've proven theorems about? Um Yeah. Uh and and this is, you know, quite, you know, quite difficult, especially if, say, your prover is running SIMD, is running concurrency,

you know, doing sort of like a lot of threading. Um As far as I know, I haven't seen any projects which have formalized uh these sort of notions of concurrency and um you know, maybe you don't want this, but it's, you know, I I think in a lot of situations you do want to to be sure that whatever you've run is, you know, equivalent to to what you've written in in the spec. Um And so, yeah, th- these something like this definitely needs to be thought about. Yeah. Um And then, yeah, thank you to the contributors, Alex, Derek, uh and some other guys have opened PRs to to Lean VM. Um Yeah.

Any questions? >> [applause] >> So, I have almost solution solution to the last two or something. Uh they seem the same. Uh so, there's a formally verified compiler called Pancake compiler, and I'm attending their weekly calls, and they were One of them wants to uh add SIMD. >> Really? Nice. Okay.

>> Just Okay. Okay. >> Yeah, so the the the the the gap between Rust and bytecode that I can be direct The Pancake behavior is equal to bytecode kind of thing. And the Pancake is also designed to be easy to verify. So, it doesn't have undefined behavior, so maybe easier to I don't maybe similar to Rust in terms of formal verification on the source. Uh the another thing was measuring the extractor time. Um I I guess it's kind of easy to use a concrete machine like uh you you could also use the MDM if it's universal and like efficient enough for this purpose, or maybe RISC-V or something, but uh >> Mhm.

>> And then like count number of worst-case steps or something like that. >> Um >> I mean, it's time uh whichever notion you need. >> Yeah, I guess Yeah, you you um you could, but then like I guess that depends on what sort of property you want. If you want like an asymptotic property, or you want like something like super concrete, right? Um and I'd argue for an extractor I I don't really I don't even really want my agent to write RISC-V code for my extractor. I just want it to like just just to know it's asymptotically you know its asymptotic behavior is you know like polynomial running time.

>> Yes, of course. Uh I understand your need is just not not a concrete number, not a concrete constant. And I mean, you you There's This is a theoretical thing. There's no need to run it on RISC-V. I understand all that. >> Yeah, yeah. >> But the simplest solution is to come think about this in a concrete concrete machine. >> Yeah. Yeah. >> [cough] >> Yeah, [clears throat] I was I was going to say the same thing. Especially if it's a straight-line extractor, should be simple to have an IR that just doesn't have any looping and branching and right?

>> Uh yes. >> for the stage and to use that to describe the extra structure. >> Right. Okay. Okay. Yeah. >> Um I have another question. I I didn't quite get on the slide on what an auditor needs to review. You explained Yeah, the 1,200 lines. I didn't quite get that. Is that because we just need to match it with the Rust implementation? >> Yeah. Yeah. Yeah. So, yeah, you need to understand that like say I'm running some sort of version of Sum Check in my verifying to make sure that I've actually written that that I've written that version of Sum Check uh you know, for the prover and verifier.

>> Right. But, if we had the end-to-end verification, we could skip that part of the auditing. >> Um I guess that depends it depends on what you care about. Yeah, right. Like if if all I care about is just the formal verification sort of [snorts] repository by itself just in isolation and I just want some notion of an end-to-end ZKVM, then yeah, you can definitely skip this. But, you know, often formal verification isn't just I'm formally verifying. Like the spec doesn't exist just in its own world. Like the spec should usually it's trying to describe something concrete which is being run somewhere, right? So, it Yeah, that that depends exactly on what the application of your formal verification project is, right?

>> Like like if you wouldn't audit it, you might lose compatibility, right? It might like change the prover and then it's not compatible with some other implementation. >> It has done that and it I'm very very very likely that it has in Linea VM has done some sort of those things. Like I I I'm almost certain of it. Yeah. >> So, I have a question just about using Lean as like a for maybe production code in principle is like that's in principle a pathway from this project.

>> Yeah. Yeah. Yeah. >> Is there anything about this that's been either particularly awkward with Lean or do you see any limitations of Lean as like a really serious production language? >> Um I don't know. Um good question. I I I I think like from this project I I hope not. But I mean, we've had like these discussions, right? About like uh we don't have SimD in Lean right now. Um you know, you could maybe remember like being thrown about like you could have um like you could speed up Lean by using like, you know, FFI into like C current and stuff. But now, you know, you're you're you're like to get then to do if you do that to get performance, you're now like having to increase your TCP.

Um Yeah, so do you want to take that? And yeah, so that's like I guess a decision. So I I I sure hope so, but I I think it's really early, right? Like it's it's still too early to say. Um yeah. >> And then maybe a follow-up question. How similar is this in structure to like Lean VM in Rust? Um like if you had a full extraction maybe into an EOS, would you expect the data types to um map onto each other roughly or um Yeah, what do you think?

>> Um I think I think you're going to have a hard time mapping it. Um especially because like for example, we use like there's a lot of, you know, it's a still an interactive, you know, it's an IOP. So there's a lot of like oracles. Um Yeah, like you know, it's a lot of defining like we don't want to be able to find what oracles are, but we use oracles a lot. We throw around oracles a lot. Each protocol's defined with like what oracles it reads and what oracles like, you know, it produces new oracles and stuff like this. The Rust code never mentions any of this at one point, right? Like it's uh it Yeah, it just talks about, you know, maybe, you know, polynomial commitments and polynomials and FFTs and stuff like

this. So maybe if if like we have like an interact non-interactive version of this with like, you know, the BCS transform, then you might get it might be more similar, but I I I think you'll definitely be a lot of work. Yeah. Yeah. >> Yeah, I was I was curious about this as well. And uh I I think it's it's okay to write to write a theorem um basically saying that I run this abstract protocol, but then if I replace the oracle with this concrete function, then it's equivalent to the rust code. I think it's mostly work for the agent.

>> Yeah, um yeah, I mean >> [sighs and gasps] >> yeah, it's I I you know you might be right. I'm I'm not sure about the I'm not exactly sure about this. Um I mean it I found in my experience but I mean like it is work for the agent, but like for example, a lot of the like protocols that exist in in Arqle for example, um which are like very faithful to the literature and the papers which which sort of introduce them, um aren't suitable for like the the Lean VM. And even though Lean VM makes like very slight modifications to to the protocols, there's enough changes to the um enough changes to the protocol where

you like there has to just be entirely rewritten basically. Uh even though the idea is exactly the same. Um and yeah, that could be a case of either writing a very good abstraction where the agent can just plug it in for you. Um But you know, the more the agents write you you know, you chances are that also the more stuff you have to trust and audit is going to increase, right? Like that's So, yeah, I'm not super like 100% agree with idea that like agents can just always do it for you. There's not necessarily in all cases, right?

Yeah. Cool. Okay. Thank you guys. >> [applause]