RISC-V zkVMs in Lean 4

Transcript

Hello everyone. So, this is the last session for today. Um it's going to be about formally verifying risk five ZK VMs. Um I'm George. I don't have slides, so I'm parasitically going to use this slide as the background of my workshop. Um Yeah, like it's the last session, so you know, we can figure it all together what we're going to do. I had uh two sort of goals um for this workshop.

Talking also with Nick who did the previous session, I think two two things I would want to discuss is some sort of checklist on what it means for a lean VM or for like a ZK VM to be formally verified. Uh checklist is something I do quite often lately. Uh I do lots of checklists. I used to do more tables, but now I do checklists. Uh I don't know. So, what is a checklist? Checklist is like sort of like a thing where you have like some items

and then when you finish all of them, you can what? Yeah, you you you tick them and then you're like, "Okay, the project is done." Um and it's important because if you don't have a checklist, you don't know what you're going to do. And and this is what I I'm I'm I'm having with formal verification, you know, like for example Emil before Don't worry, Emil. I didn't want to No, no, don't worry. Don't worry. He was like, you know, like I just need, you know, like He's like, "Yeah, I just need 2 3 months to bring everything to production." And you know, like I think that might be true, that might be false, but if I don't have a

checklist, I don't know how to even evaluate. Um Yeah, so checklist is one thing I want to discuss. The other is sort of like TCB as in what is um the TC What would be the TCB of a formally verified ZKVM? That's another abstract topic. Also, you know, I'm here, I'm in front of you, I had a mask, you know, I'm in a vulnerable position, so I I want some like uh you know, like audience participation because I I I I'm not planning to completely destroy my voice. Um

So, how about this? Well, actually, wait. Do you guys have something out of this workshop? What? Mm. Yeah, even what we want to achieve, Kev. Yes. The checklist, you mean?

Well, like, for example, what one thing I was thinking about listening to Nick's talk, you know, like, he has this nice like there is this nice like diagram and it has like green for proven and it says, "This is proven." And I'm wondering, what does it mean? Like like, are we like do we just read the TCB and we're done or do we actually need to go and do much more theorem making, like think about the theorems, like that's what I mean, like because it's very green, but also is it like really green or is it like, you know, just the skeleton exists and now we can go and and and we need to think

more about theorems to prove? >> I think it also how green it is depends on on what you want out of this. So, like here like all the green things, this is assuming that you don't care about what the verifier and approver actually do. Uh so, you you you don't care if this is faithful to to Lean VM. Um if if if you do care if you do care about faithfulness, then this is not green anymore. This needs to be all be red. >> You mean to to tailor it to Lean VM, is that what you mean? >> Yeah. Yeah. Yeah. Yeah. So, to to make sure that the the sum check round that I've written that I've proven here is what I'm running in Lean VM, I need to um

you know, and if it's just this, then this is not green anymore. That's now has to be red. Um >> Right. >> But, you know, yeah. >> Right. Okay. So, yeah, but and that brings me to another sort of meta topic, which is that like I assume this is like some module in like arc lib or whatever, which is some library out there, and we're using this library in your project, and >> [snorts] >> that's what we were discussing before. Like before you were like, you know, I have 500 lines of um code, but then we're sort of ignoring these lines because they're part of some

library on GitHub, which is you know, in some cases it's fine to consider libraries on GitHub as, you know, like too many eyes have seen it, so it's fine to not look at it, but I don't know if arc lib is this kind of library. Obviously, it's not like and and and that's why, you know, I I I want there is no Zcash people here, but I want to ask, you know, like the ideal multiplayer setting would be that we all use the same libraries so that they get super lots of eyes, and they actually become part of the, you know, like sort of mild TCB, but yeah.

>> So, the the danger of this depends on whether your statement depends on the external libraries or it's just some intermediate lemmas in the yeah, in the some parts of the technical proofs. If the statements, if you like directly this will jump to definition, jump to definition, jump to this definition, and then from the statement you can reach somewhere in the external library, you have to read that part as well. That to be really sure what you have gotten. But, if it's just about some mutual correlation argument in Muslim and the statement is more than you maybe you don't have to read the proofs. So, there's there's there's a

difference like statements or proofs. Statements and definitions are really yeah, careful things. Need needs care. Proofs are checked by machines at least once. >> I think in any project you're formally verifying, um of course, formal verification is only as good as the spec. Um and it's it's it's worth kind of identifying some

really core key properties that you absolutely want to be true um of of the code base um so, like um I guess soundness um completeness are common um and and it would be useful I think at least as a starting point to um set those as sort of the core theorems we're trying to prove um and and I mean, you can always do more in formal verification. It's hard to know when to draw the line of the properties that you want to prove or how elaborate you want your specs to be. And so, um

if you start with a goal of of the core kind of high-level properties that you absolutely need to be true and that you want to formally prove, um that helps you get a sense for when is the spec done, you know, when is it {quote} formally verified. And also helps you get a sense for where the verification boundary is. Um >> Um not related to the previous comment, uh but uh I would like to add that uh well, my personal opinion is that uh even though

we have we may have green things, um meaning that some statements are proven and we fully understand the statements themselves, this this formal verification and formal proof of these statements does not replace uh a proof in natural language and the understanding such a proof. So, I I think uh it's a must uh for us to deploy only things that we uh fully understand. Well, not a single person fully understands, maybe, but at least for each part uh of the proof uh written in natural language, there should be a

person who understands it and some sort of approves. Because well, uh we we shall not, I think, uh allow any proofs as as black boxes without understanding. Well, our understanding may not match doesn't have to match the lean proof, but this our we should understand how natural language proof works and why it works, because this understanding is crucial in uh our modelization and uh our understanding the security model where all these things leave, how robust the security model is, what what happens if the assumptions change? Because if we have things black boxed, when something has is changed in the

setup, we have no way to proceed rather than create another black box. And the further the worse it becomes. So I I my opinion is to to have natural language proofs as a companion to to lean proofs. Independent or dependent doesn't matter, but these proofs should be human verified. Human written for humans and verified by humans. >> Yeah, at some point you don't want to do that. Like there are like proofs about risk five code and I applied this people optimization 2,000 times and each time I checked all the side conditions and you can write it down in natural languages

because it's easy like a micro also. But I mean if I try to follow that all it's just a repetition and I get bored and I cannot finish it all like there's a limit. At some point you don't want to read a proof. >> Okay, going back to Derek sort of what you said of like this high level key properties thing. For example, I don't know Nick, have you like I assume this is something like this is something that these are properties you would set for the entire

system. And then after you wire the modules together, you would hope that you can prove such properties. But we like for example, I assume your project doesn't have such high level properties yet, right? Because it's not fully connected. >> I mean we have I have like some high level theorems about the spec but they're like as in like that I'll say like incomplete. So like for example, we have like we have an IOP built. We do have a fair amount of the security of the IOP.

It's just that the case of the IOP is not what leading VM is, right? So, you still have still quite a few steps to to get something interesting, shall I say? Yeah. Um And you can still, like, as you build the spec out, you can it's quite easy to, like, have, you know, sort of let's say, like, you know, headline theorems, which um sort of like evolve alongside your spec. So, this, you know, when you you start out with your spec, which is something very simple, you have, you know, a very simple headline theorem about it. And then, as you, you know, increase the spec, add more things to it, then the that that headline theorem can grow alongside, yeah. >> I think just I will get to you, Emil. I think what I'm trying to understand is

sort of like how much invisible work there is, like, you know, like, for example, you know, at some point Emil freezes the code base, and this is all green, but then you need to go and like ship it. Like, how much invisible work there is after the code freezes and this is green. Like, you know, like, uh and because I think humanity has not yet shipped things of such complexity that are formally verified. I feel like there is lots of invisibility, and I I I I'm trying to understand exactly where it is, like, um

>> Yeah, I mean, if you if you're trying to be, like, if as like we say, like, we're like, you want to be super, super careful about this, uh and sort of make sure that even, like, the sort of like, let's say, for example, like, the helper lemmas that you build make sense and are useful and uh like sort of intermediate definitions that you come up just to simplify things as uh are make sense. It's going to be uh it's going to be a lot of work. It's going to be a huge amount of work, I think. Um Uh because you Yeah, just because Yeah, uh you know, the my what I personally believe is that for verification is is that you reduce

you know, what of you reduce like a very large statement to something which is very readable. But if you also want to like check if you want to check the homework then but that's a lot of work. Yeah. Uh >> Because I think what's basically going to happen is that in like 6 months, this is going to be green and code is [snorts] going to be frozen and then it will be like, okay, now let's ship it and then someone will need to go through the TCB and read it and get confident about it and you will be like, okay, cryptography team like unleash unleash the cryptography team to do it and then we will be faced with you know, like tens of thousands of

this code arc lib like corners dusted corners like and it will be extremely hard and at that point we'll be like, okay, wait, wait, wait, wait and then invisible work will appear and we'll be like, okay, wait like >> Well, yeah. Yeah, I mean I don't think >> Sorry, just to go to Emil because I don't know if you have something along >> It's just a question to be sure I understand everything. Is it fair to say that when everything is plugged together the concept of flock some checker or wheel whatever in some sense disappear. You only have knowledge soundness and completeness statements and

you have a specification of the prover and the verifier. >> It completely disappears from the statement point of view, but from the auditor human guy who needs to go, it's still it's still there. >> I agree and in particular for Lin VM the branch man this this thing I think it's still like I think in this particular example it's still possible to have a paper or like I don't know 30 40 pages that uh is kind of self self-contained and that that contains all the proofs in a human understandable way that one human could understand in a few weeks, I believe.

>> Yeah. >> I mean >> Possibly. >> You can also think the FE project as something which you know, it just sits alongside. You know, you do when you like you you you you carry on you do the normal things that you would like when you normally say like ship a cryptographic protocol, you you write the code very carefully and understand that. You you have maybe like human written proofs about it. And this is a nice bonus on top of that um to to you know, to you know, to increase the confidence uh in in what in what you've you know, previously >> But we're talking about like XMSS in assembly and stuff. Like how what what how would we do the normal stuff on that setting? Like on that

setting we only have formal verification. >> Yeah, right. Okay. Yeah. >> Uh Thomas do you think like that this is a better approach to do the formal verification or to start it right now in parallel to what we are doing next week? So for example, formally verify some pieces of LinVM directly enshrining into the code. For example, we can already do the same check and fix it. Or do you think that we should wait for all of those stuff to be green to do everything at once? And to like involve the cryptography team into this and all of this or do you think for example, you can send one

person checking into some particular module at the risk of course of this module being removed in the future and so use this work? >> Yeah, I I I I I'm I'm thinking but at the same time it's hard for me to have a high conviction answer because we've never done this before. Like we're basically shipping formally verified stuff for the first time and it's It's thing. So I don't have a good process. Like >> For example, like we are doing the cryptography spec with Benedict, like the XMSS stuff.

>> Yeah. >> Let's imagine like we change a bit the XMSS or a bit the design or we cut the tree in two or I don't know what. Do you think this this was the right approach for us to start like reviewing the PRs, pushing the PRs, or do you think this is useless work and we should have waited for the final design to set to settle? >> No, I think that is that is very useful work from a pedagogical perspective because we're all getting better at Lean 4. Like I I I don't think we're wasting time right now by doing that. I think to uh but like that's different from shipping things to mainnet. I think if

it was me, I mean, it's not exactly Well, to say it differently, I think the the more prudent thing would be to do more incremental steps and first ship some formal verified small thing. Well, not small thing, medium thing, and then ship this mega thing. But But this is on the assumption that there is tons of invisibility. I I think >> They are small items. Yeah, for example, you have the sum check. Uh >> No, I meant like XMSS and Sphinx. So, for example, ship Sphinx or XMSS without Lean VM, make that process nice, figure everything out, and then ship. I don't know. That would be the more prudent

timeline neutral like non-timeline respecting thing. >> Be- because like, for example, if we had formally verify or involve you guys in May in Rome on all of this, you would have like formally verify Poseidon and baby bear and koala bear and all all all of those stuff. Two months later, everything is in the trash. >> Yeah. Uh >> It makes most sense to verify Poseidon now. >> Yeah, but we would have like written like a a lean for Poseidon spec in some sort right? >> Can I go a little bit back to the checklist because I have a suggestion.

>> Yes, yes, please. >> So like there's an international standard called the evaluation assurance level and the EAL1 is kind of tested and then the EAL7 is formally verified and there are like several certification bodies in the world that can evaluate and certify EAL7 formal verification artifacts. Um I don't know the details of their checklist, but common criteria evaluation assurance level seven and what the certification body should do and there there's a checklist and I mean you don't have to follow it, but you but I am they have good ideas, I guess.

>> How did you say this thing? >> Um evaluation assurance level. EAL usually call EAL7 is formally verified. >> And this is just for specs or for end-to-end formal verification? Okay. Yeah, so I don't know. My fear

I don't know, Kev, if you have a take is that like I you know, like we're like shipping lean VM with Sphinx. We have connected these two things due to aggregation. So at some point we're going to learn what it means to formally verify thing like I'm I'm I'm I'm fearful that we're going to learn something too late that is going to be too Like I don't know how to de-risk this. You You know what I mean? Like I feel like there is some invisible Like I think greening these things is kind of

easy. Like if I put my AI agent to do some FV, it's just going to make some theorems. It's going to But like when it comes to actual security, I'm I'm I'm afraid that we're going to be like I don't know, like in May or something and we're going to be like, "Okay, let's make it serious." And then we're going to be like, "Oh, that's like 14,000 lines of specialized code that is in the TCB and we have no capacity to review it and the only way to do it is to give like tons of money to security companies and I I don't know, some weird thing like that.

>> Um yeah, I mean, I I completely agree that there's always this gap between the spec and the implementation. And between that gap there's going to be some TCB that you sort of need to be aware of. And right now when we don't have a lot of experience with FV, in my opinion, the best thing to do is actually to understand what we're shipping. Just like the pre-F before before we had FV, we had to just understand things we're shipping. Um so I think that's the best way forward at the moment. >> But what >> Yes. >> I think um >> [clears throat] >> So if we if we wait on Lean VM specifically, if we wait um

until it's stable to start trying to use um something like Ennies on it, um we may discover just problems in the tooling. I think it's worth it I I don't know if there's appetite. I think it's worth um getting a working extraction into Lean that we don't necessarily need to prove all our theorems immediately, but we should understand the limitations of the tooling uh soon and have a pipeline that allows us to um update the rust and have some sort of um way of updating the lean after that. I I also think like

it would it could be very useful already to be inlining um like a specifications um in in comments using like hacks allows you to do this and then it extracts into a proof obligation in lean. Um that is a good way of building up a spec at like a low-level functional specification um on on specific functions where you need certain properties to be true or you're expecting them to be true and you will test them, but it's nice to attach a proof obligation. Um that kind of whole machinery of going from our source code into lean, um that is its own kind of challenge and

then engineering task that I think we would be uh like that that's something we can do now um and gain expertise as a group uh now. And so when it comes to write the I mean, writing proofs is, you know, agents as we know are very good at writing proofs. But um getting getting the code into a setting where proofs are meaningful, um I think is is a challenge. And that's something we can tackle now. >> Okay, I think what you're saying I I'm just to enumerate invisible overhead, I think what you're saying is you you you imagine overhead in the tooling.

W- that's one thing you said and then you said that using uh hacks or whatever, you can basically while you write the proofs do obligations of like, you know, I'm going to do this proof in the like a sorry kind of thing. >> While you write while you're while you're writing the rust, you can send proof obligations. Initially, we can have a high tolerance for incomplete proofs and sorry >> But nobody's writing the rust. Like it's just AI that is doing it these days. Like like >> Maybe agents You think that agents will do I mean, if agents could do the right FV, they would just straight up do it. They don't Otherwise, like they would >> I think an agent can have a sense when

writing a specific function of some proof obligations that would be useful to have attached to that function. >> Mhm. >> Maybe maybe we can try to de-risk a little bit by unbundling for example the Sphinx and the VM. I'm I'm not sure why we couldn't like we have to bundle both. >> I think it's for hard work cadence purposes. >> Um but let's say if we agree on a somewhat vanilla version of Sphinx that is not AI optimized but that is just

slightly different parameters from the SRH DSA Sphinx. Um would you have like Benedict, would you have an idea of like is how long would it take to just take the proofs that are from SRH DSA to adapt them to some variant that has slightly different parameters? >> I mean, if it's just the parameters that you change and not the structure, then it's just to plug it into the bound kind of thing. >> Yeah. >> It's just a, you know, evaluate a Python script. But if it's uh if you change the structure, then depends on how much you change it. Um

for example, I mean, this the security proof relies on this ITSR property, which is very specific to what kind of force you use in the >> Yeah. >> in the leaves. So, if you change that, you need to come up with a new property. You need to assess whether this property is meaningful for standard hash functions. So, it's kind of more tricky. >> Yeah. >> But so, if we can start to like look into this right now for Lin things. The decision tree that we have is either we go with something like the just a change of parameters and the hash function. Or we go into this more fancy force

changes and and whatever. Um this to me can be like treated separately of Lin VM. Um >> But uh do you mean separately in terms of like project or in terms of like shipping it to mainnet? >> Shipping it to mainnet and the work to fully understand it. Like to have a the someone from the cryptography deeply understanding both the the spec and eventually a library that would go with it. >> Because my vibes are that you like this is just vibes, but I feel like you know, if you told me we're going to ship Lin Sphinx in

eight star I star, I would I could now figure out how to do it and I could figure out the invisible stuff with some thinking, but Lin VM has much more because there is the glue, the performance is more critical like so uh isolating in terms of projects is easy and I think we like Sphinx is a bit too easy in a way. I think Lin VM is the actual problem because it's such a big multi-module. Uh >> Yeah, yeah. So, what I was trying to do is basically look at the pro project as

a whole and try to remove as much as we can from this potential realization in 6 months that oh we now have thousands of lines to >> You you're saying let's start with Lin Sphinx, de-risk that, see what we learn, and then move to Lin VM. Don't do the both at the same time or something. >> Uh yeah, and even I don't Lin ex-MS2 we can >> Because I'm not too worried about the theorems. Like I I feel like for Sphinx the theorems are quite plausible and not too big and very standard. The theorem for Sphinx. For this I worry

about the theorems. Like I think there is too much. >> Can you say again why you worry? I mean it's completeness and soundness or completeness and knowledge soundness. So >> Why I worry about all these things? >> Yeah, I mean if if if you can prove that everything together gives you a snark that is complete and knowledge sound and you check that the completeness notion makes sense and that the knowledge soundness notion makes sense. What else would you want to check? I mean you don't need to check that the intermediate notion that you get for some check is the right one, right? That the lean proof tells you that it's sufficient to imply the final result. So of course, I mean in the notion of

knowledge soundness there is extremely Yeah. subtle points and you need to check that. And >> Maybe I'm being too conservative and maybe I'm being too ignorant here. I just feel like all these things are so much bleeding edge that I don't like I don't know. Like for example, Nick said there is no run time. Like like like if there is no run time support, how do they model the extractors? Like I don't know how many blind spots >> Right, but the the extractor is part of the knowledge soundness notion. So this is sort of exposed to the top level theorem, right? So if there's I mean, I agree that if we have the structure and we understand sort of what

is the rough strategy to build that VM and then we look into the individual lemmas and we also review them, then yes, we are more sure that things are good. But in theory, if you trust formal verification and you only care about completeness and knowledge soundness, then why would you review the inner parts? I think it's good if we the intermediate lemmas and statements about building blocks because just gives us more assurance. But I don't know if the >> Wait. >> If I had the choice of of waiting forever and and uh >> I don't get what you're saying. You're saying that because the My my

understanding, maybe I don't understand formal verification enough, but you're saying that oh, it's too simple theorems that we need to prove for each of these IOPs or whatever. So, why are you worried? But I'm afraid that for each of these simple theorems then you need to go into a a graph of definitions and like >> But I mean, isn't the the definition is I mean, for completeness it's pretty easy, right? It's like And even for knowledge soundness, I mean, I don't expect that there's like tons of definitions to follow up. >> O- Okay.

>> I mean, the problem is what kind of knowledge soundness and this goes back to this whole recursion thing, but let's set that aside. Then there's like a meaningful notion of knowledge soundness in the random oracle model. You have to check that this notion is like written in a good way in Lean and it matches what we want it to be. And then this this sort of the high-level theorem tells you that whatever is spec'd as a proof system you you look at it, you don't open it up, you look at it as a black box. Whatever that is, it satisfies the notion of knowledge soundness with a specific extractor. Then you look at the extractor, you check that it's not, you know, solving the halting problem,

whatever. Uh it's like an efficient efficient algorithm. Uh and then I don't know. I think that's it, right? So, if you want to have more reassurance that it matches our intuition for why things are secure, then you look into internal lemmas or something, but strictly speaking, I think there's two theorems you care about. >> Okay. >> One one key issue there is that you're for the moment not there not a single IP has had another sound that's proved. And so this obviously the definitions associated with it have not been heavily reviewed at all. And then as as you pointed out the complexity issues of actually proving

that the extractor has polynomial complexity is not currently within the reach of this is no complexity theory library yet. >> Right, but you can manually review that, right? >> Yeah, that can be like 100% yeah, yeah, 100% >> And I guess if if we have the you know, the conjecture that it's a straight line extractor then we can look at that's where my lean understanding ends, but I think uh this should be easier to prove than to prove in lean than uh this is a polynomial time extractor for some polynomial that is unknown to us. >> Yes, so there is already a formalization

of straight line extractors in Lean in our group. Yeah, I haven't looked at it too carefully, but I know it's there. Yeah. >> Yeah, I have a suggestion to ground it and to make it somewhat understandable to everybody who doesn't know Lean. So, you you you can keep a list of all kinds of bugs and all kinds of attacks you have thought about or you are remotely worried about or something. And then you make a list and then Benedict will check each one. Say, "Yeah, this is covered by knowledge soundness. This is covered by perfect completeness." Ta-da, ta-da, ta-da. And maybe there's something that remains. Maybe it's everything covered,

but that can be yeah, one checklist to keep are we covering everything we uh worried about? >> Um okay, let me do an interlude. Um Danny, can I can I can I ask you something? Yes, you. Um because you work at Zcash, right? And I I want I wanted to ask if you guys have like a a strategy for the a specific strategy for the end-to-end like mhm proving system. Like you know, you you

how you're going to do it in the future. You know what I mean? Like do you write Rust and then you do Anias? Do you Uh you need >> to press it from down. >> Sorry for putting you on the spot. I just uh noticed you're here. But but because I've I've been If you don't know, that's fine too. >> So, it's just that I don't know. It's just that uh um I'm not taking the decisions. I just see what is is said. So, uh I can say what we've

done recently. Uh what we started doing is actually translating a lot of Rust into Lean and we started to use uh I I I don't know how to pronounce it. Uh I I Anias? Anias. Uh we've just started using it like last week to uh translate uh the Pasta curves assem- uh the Pasta curve assembly into into Lean. Um we might use it more. Um but it's just uh something that we've we've discussed like a week ago. Uh so, the discussion to translate step by step into Lean.

Uh let's see how it goes. Um >> Right. Because I feel like this is sort of like this theme of we have a complicated thing within our modules and how do I mean, the inner modules you can do it them in assembly in Lean or whatever, but how do you do the entire system is a thing that exists across multiple mega snark projects. So, I think mean you are a mega snark project. So, I was wondering like I don't know how you planning to tackle it. If you >> As I said, there are discussions only since last week.

The last one that we had as I said was step-by-step translating into Lean. Do we write everything in Lean? That was also a question. I don't know if Daramai is here. No, he's not here. They've been >> Yeah. >> questioning meeting. Do we use directly Lean as a system programming and also as a as a as a formal verification language. >> So, both approaches have problems with the compilers like So, what if Rust compiler has a bug or if Lean has a bug or if Lean is compiling to C and the C into machine code? What if the C compiler has a bug and then

So, yeah, both of the both are kind of For me, not so satisfactory. That's why I've been like touching formally verified compilers or like writing proofs about the assembly itself. So, it's a choice trade-offs, I guess. Yeah, we're we're treading dangerous ways or like pioneers safer ways. So, there are like yes choices. >> So, the only thing that I can say is that's for sure we're going to use Lean more and more. I think it's obvious, but so everything we write everything that we write in Rust and that might sound

useful to translate it to Lean to verify properties, we're going to do it in Lean at the same time. Using AI is starts to be very easy and we start also doing It's also useful to actually make the graph of all the proofs and >> Right. Mhm. So, we're still investigating a few solutions. >> Yeah. >> Ineas and and yeah. >> Yeah, makes sense. Thank you. Mhm. I mean, you seem to be in the sort of same spot as we are where we're just mapping out the possibilities and um Ah, hello there.

Yeah, I I I was I was saying um that we have the same problem in the sense that we both have You don't really need to to look at it, but um Yes, yes. Um where you we both have like mega snark projects where basically, you know, they're like mega projects with sub modules where these sub modules we sort of know how to formally verify, but the entire thing it's still unknown how we want to do it. Do we want to do it

with A nest? Do we want to do it with assembly? Do we want the glue >> Are we talking about um of linking the implementation to the design proof or just about doing the design proof? >> No, no, the the the whole end-to-end thing. >> Okay. >> And so Yeah, I was wondering because we're also discussing how to do it. Like, you know, like basically I think the way I see the problem I see is like the glue of who connects all these boxes that are written in in assembly and lean basically. >> optimistic because I I've been kind of experimenting with pasta curves. Um it's the uh um

>> It's what? Sorry? >> Pasta curves is our elliptic curve cryptography library. Okay. Um and it all works fine basically. Um you can directly um prove um that assembly matches a lean spec by just transliterating it into lean. Um and I think pretty soon it will be possible to use Croc and to check that against um AR 64 and XC664 specs. Um But in the meantime, you can just hand wave it and it's fine. Um And and AS works for us.

Um the the only issue there is that you've got to break down your rust very granularly to make it work. Um I think So I'm not attempting, at least not yet, to try and prove everything about the implementation. I'm focusing on cryptographic code that um I'm most worried about um uh kind of bugs being introduced because we're you know, writing everything in assembly for performance. Um But if if you want kind of to formalize all of the things, I mean

all then with there I it's still possible. Um it's just a lot of work. I I don't see any structural obstacle or barrier. It's >> Yeah, I agree. There is no like theoretical obstacle. I we're just, you know, like in terms of like hard forks and stuff, where I I've been kind of thinking what is like the invisible overhead where, you know, like >> So this is a coordination problem and a protocol upgrade scheduling problem. >> Yeah, but also >> that as well. >> [snorts] >> Yeah, but also sort of like never done

before problem in the sense that nobody has deployed such complicated things on the internet that is fully formally verified. So >> I'm not worried about that. >> [snorts] >> Okay, good. I feel like basically most people are not worried about that, but still I'm in my ignorance, I'm worried about that. So I'm I'm trying to, you know, like >> Okay. Um Yeah, um so I'm not sure how useful it is for me to say that I'm not worried about it. Um, was there a more concrete question about kind of how to do it?

>> Are you not worried about it because you can read all the definitions and the statements or hahaha. So, after this lots of work, how do you make sure it's okay overall? >> Um, I got Nadeem Kbeissi to um, look at it um, because he's good at finding gaps in formalizations. >> Oh, I see. That's the solution. All right. All right, right. Yeah, because that's another discussion, you know, right? Like >> [clears throat] >> because ideally we would have

very high-level statements talking about our system that we won't have like, you know, 30 different boxes each with their own disconnected statements, which means to have a few high-level statements, it means you need to put in the work to connect all these things. And then the question is how big is the TCB of this? >> Um, so in Zcash we're quite lucky because I I done a lot of the work needed um, a few years ago um, in terms of defining what the the desired high-level security properties are. And obviously I hadn't done it in Lean, but um, I done it in pen and paper um,

and I had kind of very hand-wavy informal security arguments, but um, those turned out to be basically correct. Um, so I I don't know whether you're in the same position as Ethereum. Ethereum is a lot more complicated because in some ways cuz obviously um, it's more contracts. >> Yeah, but I mean we can actually the current discussion just to prove system then, to make it easier, like a very complicated ZK-VM. >> We were lucky and had very smart people to kind of I mean, Tal did most of the work on the proof system music. Is Tal here?

I think he's outside somewhere. Um and Gregor Mitrovic um to do the who designed clean to do the circuit formalization and also kind of adapt clean to to work with Plonkish. Um so we have basically the dream team of three people to who together I was one of them who together were able to do the formalization in two to three months. Now >> [snorts] >> but we were working basically full-time

on it. Um so that's how much effort you're talking about. And that was only for the proof of um uh balance integrity. So um there is more work that you need to do than we had to do, I think. Um just don't underestimate the amount of effort required um and you'll be fine. >> [snorts] >> Okay. Um All right. But I I I feel like in the

end of the day, you still haven't decided how you connect all these things together, like whether you do it with Rust and Anias or you just do it in assembly. You're still experimenting with this. >> I mean, we are, but only because we we only just started using the tools. >> Right. >> Um So Anias appears to work reasonably well, at least for low-level crypto code. >> Yes. >> Um So we might run into more obstacles when we try to use it for um kind of um more um kind of loopy things and complicated

algorithms cuz we we've been using it for mostly um straight-line code. Um straight-line assembly is is is pretty easy to prove. Um Yeah, it's it depends. I mean, what kind of complicated algorithms you're trying to prove correct? >> Yeah, I guess it's like a multilinear based ZKVM. Like it it has like some checks, it has like all the battery field stuff, it has >> Isn't someone else doing the work for to do the proofs of the sum checks and and

the >> Yeah, I mean, that's a that's another discussion that I think it's interesting to have on a multi-project basis in the sense that there is Arclib that has like proofs about sum check. And we can use those proofs. And because they're an open-source library, they're considered to be, you know, not our just Ethereum TCB, it's like the world's TCB. But, you know, if nobody uses these proofs from other projects, it's basically still, you know, our own problem. >> So, you're worried about the size of the TCB? >> Absolutely. >> Um So, >> I mean, aren't aren't you Shouldn't we

be worried about >> Yes, you should be worried. Yeah, you absolutely should be worried. Um So, are you mostly worried about the size and complexity of the statements or about um the kind of low-level TCBs, so um things like is this a correct um uh um specification of AArch64 assembly or whatever. Um or are you worried about gaps in the connections between different components or the complexity and of understanding the whole system or what what kind of gaps

are you worried about? Cuz all of those are issues. >> Yeah, I'm I'm worried about all these things, especially the ones that like the unknown like the ones that like I'm less worried about, you know, missing the sum check theorem because I think at least somebody understands it. But like the glue, like things that we have not really done before, these are the things I I'm really worried about. Uh just Emil. >> I If I understand correctly, the the sum check theorem or proof would not be part even if it's in Arch lib would not be part of the trusted code base code base because when you you only have the completeness and soundness statements

and the the proof that the sum check is sound and complete in Arch lib will be glued together with everything and you will not in some sense you could be convinced that the the KVM is sound without looking without even knowing that there is a sum check inside in some sense. >> Uh okay. Yes, you you care about um whether you're proving that about the right thing. So So yeah, you can um prove that the sum check algorithm is correct and then you need to link that to um the Rust. Um I assume you're still um writing things in mostly in Rust. >> I mean we are currently, but we don't know yeah, we are

>> You don't know whether that's the best approach. >> Yes. >> Um well, it might not I I would tend to assume it's still the case that you should be writing things in a high-level language um except for performance critical um crypto code. >> Right. >> Um cuz cuz even though in some sense you're you remove the Rust compiler from the TCB if you um go directly from Lean to assembly, I still think that it's too hard for humans to write assembly and we don't want to

rely completely on AI to write everything. >> But but just to go back on Emil's point because I want to understand this and I think I don't understand this. Like this sum check thing you said, how how how like okay, there's a high level theorem that because it's a snark, it relies on the security of sum check somewhere inside. You're saying I should not even care that the sum check is implemented correctly. >> It's interesting because as a humans I want to understand the >> No no, not as a human, as a >> But as a robot like you my understanding you have a verifier in Lean, you also have a prover in Lean, you say this is the canonical implementation of the

prover and the verifier and you have a theorem that say that it's complete and sound and if you want to high performance prover in Rust or whatever, you can use the extraction or prove that it's equivalent to the Lean prover, I don't know. >> Well >> So so the point is that the the our clip enables compositional reasoning about IOWs and IOPs and so the thing is that that the statement that says that say hey sum check has knowledge soundness

will sort of just be part of the knowledge soundness statement of the top level proof of the of the top level IOP, right? Does that make sense? >> That makes sense. >> Right? >> Yes. Um so I I think your worry was something different which is that is that um thing that you proved is is knowledge sound and complete. Is [snorts] that actually Does that actually correspond to the Rust implementation? Right? So you mentioned extraction which presumably is extraction from lean to rust. I'm not a fan of that because you end up with impenetrable rust code that no one would want to maintain.

It's better to do the reverse which is what any of us does. So rust to lean so you get essentially a transliteration of the rust into lean or you just write it in lean in the first place which is fine. You can link lean against rust and presumably the lean compiler will get faster. I'll produce better code. But if you do it that way then I think it's overall easier because um you your rust is still maintainable because it's it's not the output it's

not a generated thing. It's a a maintained thing. Doesn't matter whether it's humans or AI it's maintained. And the lean is close enough to it that you you have a proof that it matches the high level thing. And sure if you have to regenerate it and the proof breaks then it's a little bit of work but get the AI to do that work. >> Okay. Yes. Okay, let me let me make this a bit selfish about me and can you because I think Emil and Benedict you've been saying the same thing about

basically I think what you're saying kind of shrinks the TCB considerably in my mind because in my mind I thought I have to go and review all the definitions of like the sum check and like how it's defined. Okay, wait. >> No, top level definitions. >> Okay, but like So okay, so you're saying that the holy grail is that there is a top level completeness and it which says that I don't know, like what what what does that say that like um

>> Completeness for an I/O. Yeah. >> What? >> Completeness of an interactive article relation presumably. Or a um a compiled proof system. >> Yes. Yes. Yes. Yes. >> I think it should be the completeness of the non-interactive What we care about >> Yeah. >> ultimately is the non-interactive >> Okay. >> Yes, but >> Then then you will have to make a heuristic assumption about Fiat-Shamir. Yeah. >> Yeah. >> The the thing that we want [snorts] to review in the end should not talk about interactive article whatsoever. It should talk about a SNARK in the random oracle model. >> Okay. >> If that's >> It's It's hard to prove anything about that. You Yeah, because you you necessarily have a gap um at

where you instantiate using Fiat-Shamir. >> It's a SNARK in the random oracle model. >> Um Oh, I see what you mean. >> What do you mean? Yeah. >> So, we have that um uh in the iron wood formalization we go It's actually um AGM plus uh random oracle. Um >> We [clears throat] care about the SNARK in the random oracle model. Completeness >> Mhm. >> probably for any hash function and the soundness if the hash function is a random oracle. >> All right. >> I think that's what we want if we ignore recursion. If If we go to recursion, everything is even more messy, but let's ignore that for >> Um we we will be solving that problem.

>> What problem? >> The the problem of how to model recursion in lean for SNARKs. >> Sure. Sure. Ignoring recursion. So, okay. So, I I just want to understand like the soundness theorem. How How How deep do I have to go? Like Uh What does it say? Like for every accepting proof uh for for You You just >> definition of knowledge soundness. >> Yeah. >> Yeah. Uh I mean, for for soundness and completeness, for that your only parameters will be the relation that the the that the IOP is proving, right? And your set of witnesses and your set of statements, right? And that that's all you need to know.

Right, after that those are the only parameters of the completeness and soundness uh like predicate. Right, as well as obviously the reduction itself, but uh >> I mean we did this for Ironwood, so let me just look at the statement and while you're talking about other stuff and I'll I'll tell you what it depends on. >> Okay, [snorts] so wait, you're saying >> Yeah. >> you need the relation? >> Yeah. So you have some relation R between statements. So you have a type of statements, you have a type of witnesses, and you have a relation which is a subset of statement times witness. >> Uh-huh. >> Right? And uh I mean the completeness is very uh

straightforward, right? Which is basically you say for all statement and witness, if the relation satis- if the statement and witness satisfy the relation, then if I run the prover with this witness and statement and the verifier with this statement together, then they will accept. Right, with probability 1 - epsilon C, which in our case is typically 1, right? Does that make sense? And then similarly similarly for the soundness, you can just look in our clip and see these sort of formal statements and all they take as a as an input is state statement set, witness set, relation, and the reduction itself. >> And it's going to be a statement about

like how many Oracle queries, like like how how it's you said it's in the random like >> Yeah, I mean for the I guess the knowledge soundness depending on how you write it down, you should either say there exists an extractor or should take the extractor as input. Yeah, so so the the for the for the knowledge soundness is an existentially quantified extractor, right? Inside of the uh >> Don't don't use existential quantification, you can get away with that. Use just computable reductions, so >> Oh, yeah. >> Just my advice. >> Yeah, that's all good. >> Mhm. Um >> Because the existential um quantifications don't compose properly.

>> Uh >> Uh read the Ironwood book for why. >> Okay. Um Mhm. >> I'm just trying to find the statement. >> I mean I I can tell you exactly where the statement is in our clip if you want to, but [laughter] >> I know what it is in our clip. >> Yeah, okay. >> Um >> Uh I I make a one tool comment. The Lean is a very good accountant for side conditions and so on. Except except for then when there is a contradiction except when there is an assumption that's not satisfiable, this accountant goes crazy and starts booking 1 million dollars from nowhere. But except when

you don't have a contradictions and not satisfiable assumptions, uh Lean is a very good accountant on keeping track of all the like heavy side side conditions. So, that that that that that's the background when people say like we are just take the top theorem. Because when there is something not proven somewhere some side condition not proven somewhere, then it will appear in the statement of the top theorem. >> Mhm. Mhm. >> Um certainly. Um like let's say we we're we're we're happy with the definitions of not

soundness and completeness and we've we've checked this and we're very confident about this. Um Do we have a solution for Do we don't have a solution still for implementation is this is uh is actually tied to this. And Yeah. >> like any uh yada yada glue logic yada yada. Something like that. I don't know. I mean this is the easy solution. Like not very easy, but all formalization is easy to do. You're just going to take a Rust program and you're going to it's going to be in Rust. You're going

to connect all these shitty modules with SFI into it and then you're going to prove with any of various theorems about this system as a whole. >> Okay, but your TCB is increased then by quite a bit if you if you do that, right? Like that's Is that not a worry at all if >> Uh wait, are you assuming that you can just take your existing Rust implementation um without modifying it and prove it correct? Cuz that that's not how this works. >> [clears throat] >> You have uh downloaded these modules in assembly,

proving them in Lean or whatever, and then you make to to take it into the implementation, you you make like a a runtime in Rust. You bring all these modules in. You connect them to each other. And then with Aeneas, you expose this as a system and you prove theorems about. This is my understanding of how you get to end-to-end formal verification. One of the ways. The other is some sort of verified compiler kind of thing. >> But but your your implement the structure of

your implementation kind of has to to match the structure of your proof, right? >> Yes. >> So, um you really want to be co-writing the Lean and the Rust. Don't write them independently and assume that they will fit together. They won't. >> No, they are they are absolutely independent, right? Like they are just modules in our clip or whatever, and then it's basically, "Oh, we're going to figure out how to glue them together and >> Don't don't do that. >> Right. Yeah, that is one of the invisible overheads that I imagine is going to happen. Like when you connect things together.

>> No, don't think of it think of it as a separate stage when you connect things together. Co-write them. >> I mean it's too late and that most of the stuff is already done. Well >> Okay. >> [laughter] >> Okay, well you you did it wrong. You never mind, you can recover. >> [laughter] >> Well one way to recover is like throw away one of these and maybe that's quicker. So >> We did it wrong as well. So we're doing it wrong with Tachyon, but it's possible to recover. >> Yeah, you never said anything in the beginning. You never said such a big >> Well you Yeah. >> mistake. >> Uh

hang on, I didn't say that was a mistake. >> Uh even with this, you know, this Rust to to Lean using Hack'n'is, are we Are you saying that we're you're confident that the extractor is correct? Like are you are you happy with that sitting in your TCB? >> The new extractor? >> Yeah. Yeah, like are you Is that I mean yeah, it's it's I don't have an opinion on that, but like are you okay to say yeah, we're happy to to include that? >> I mean I'm happy. >> I think so. I think from I think it's usually good especially like capturing the the high level kind of logic and design if there's specific little bits

>> You can spot check it, right? So and if there are bugs, then you can fix the bugs. >> Yeah, I mean also the the TCB here is much more than just the extractor because the way that the Lean works is that it typically don't extract unless obviously you can set flags and you can configure it, but typically it only extracts up to the standard library. And then there is a very large model of the standard library that both the Lean and the Hack'n'is has a model of the standard library in Lean, which is of course trusted and more Hack'n'is only typically models a relatively small subset of the whole Rust standard library. and so pretty much in every single real-world Rust program that we've encountered, even if it follows

the linear subset, so it follows the restrictions of the code that linear has, it still will typically extract into something that has some stuff from the standard library that's sorted out, and then and then you still need to write that specification, and you can get that wrong, so there's there's a lot more in the TCB because of linear and Rust extraction itself. >> Yeah. So okay, then so it's safe to say that this should be just more of a an additional technique. The extraction should is not a silver bullet, it's an additional technique and you know, to to be more confident, you want to maybe do don't know, some sort of differential testing between the two the implementation of the spec and like this sort of stuff. Like this should this >> Yes. >> almost certainly should be done on top

of it, right? >> you can do these things and if you massage the Rust code, you can gain confidence in in the patches that you introduce maybe by differential testing or >> Yeah. Um so when we were doing the Pasta case, and that this is low-level code, so it's easier in a sense. The The only thing we call out to the standard library um for was black box uh core hint black black box, which is the identity function, conveniently easy to model in Lean. Um so um that's a particularly easy case. Um

and we didn't have any problem um kind of having the AI prove things about this in Lean because because we'd already done it for the assembly, and so we knew what the specs should be. And we we had the um a back end which could be either assembly or either x86 assembly or aarch64 assembly or portable. And we just had to prove that those were equivalent, so that's a particularly easy case. Um if you're So you have a lot more work to do.

>> [snorts] >> Um I know I I can't estimate how long it's going to take. >> I I actually want to ask why you think doing it in this modular disconnected way is a bad idea because that's kind of like >> That's not what I said. I I didn't say that um doing it [snorts] modularly is a bad idea. That's a good idea. >> with the lean at the same time like >> Yeah, but using the same module structure because Okay, if you write an implementation separately from um your um formalization, then you're just making it difficult for

yourself to connect them. Right? If >> Possibly, yes. I mean, I don't know. >> Yeah. You You You You might have to just rewrite your rust to make it easier to prove. >> Mhm. I mean, I don't know. >> Which you can do. >> Right. >> I mean, to be honest to be honest my experience has been that certainly on the verifier side. Now, the prover side of things is a little bit different, but on the verifier side, the proofs are quickly so simple that the verifier

model and verifier implementation is going to match, right? >> Yeah. >> The prover on the prover side is completely different story. Yeah. >> Yeah. So, yeah, it depends on what algorithmic kind of um optimizations you're using and yes, the prover has a lot more scope to do that. Um I And also, how much do you expect to be able to prove because um if you're just proving um kind of pure functional algorithmic code, then that's And yes, it's very well suited to that. Um kind of very side effectful code that is doing IO and whatever, it's

hard. It But it's it's hard in any kind of formalization framework. But I mean the the complicated pure functional parts that are doing cryptography are the bits that you're most worried about, right? I I would set realistic expectations about how much you're going to be able to prove about messy code.

At the end of the day, you just got to review that well. >> Review? Review the TCB, you mean? You mean >> No, no, just the part that you haven't formalized and there will be a large part that you haven't formalized. Just has to be reviewed really well. >> Mhm. Okay. >> [laughter] >> There is no silver bullet. There is no silver bullet now as there was not when Fred Brooks wrote wrote the mythical man month. >> Right.

Okay. Anything else we should approach in this session? I feel like >> Um, yeah, I I guess just one thing to add specifically for LLVM. I think it is a case, if I understand correctly, that we we really almost only care about verifier. Uh, and we care a lot more about soundness issues than than completeness issues, right? Like that's completeness, you know, we can >> And our rust code, we run it, it works fine for most of our use cases. Like

when I have a bug, I fix it. Yeah, exactly. With with soundness, that's what you really really care about and that sounds like it's actually easily easier to formally verify and do all these things and yeah, so >> Yeah, there's a reason why we formalized complete Sorry, formalized knowledge soundness and balance integrity for ironwood first. I'm I'm still working on the spendability, which is the completeness part. >> Right, right. Uh because that's uh The verifier is only important Verifier is The honest prover is not important for soundness.

Yeah. >> And also ZK is is important for privacy. Um but I guess that's less important for Ethereum than it it is for Zcash. >> No, in the future we will also have ZK will become important for Ethereum as well. So I guess Ethereum >> We we will have done the all of the ZK stuff and we will probably have done it for hash-based proving systems, so um you might be able to just use our work.

>> Uh What What do you do about runtime um like extract the runtime and stuff like that in your security proofs? >> Um So we have a cost model and um uh each time the extractor does a a group operation, it's supposed to call into the cost model and say that it's done a group operation. Um and um the extractors are pretty simple code, so we eyeball it to make sure it's not doing anything else suspicious like um brute forcing the solution.

>> [snorts] >> And it's fine in practice. >> Okay. Whereas Derek what is like why is it hard in our case to do their own time whereas >> Wait, sorry. I said it again. >> Like you know it feels like run time analysis is not in VCV IO yet like there is a PR or something but it is still hard to do run time analysis right now. >> I don't know. I'm It's not hard in

principle because if you write your extractor in a mini language where you can um define its cost um quite precisely then um and that is marked computable so you know that it's restricted to that language then there is no problem. >> Yeah, just to give a high store a high level like high level overview of what Kwang has done in this PR is basically he's written what a felt machine which is something like a Turing machine for field elements essentially on which so which can allow you to you know by bounding the number of steps for an algorithm on this felt machine you get an idea of the complexity

essentially. >> Exactly. >> Okay, but but Derek you're not using that. You you have your own hand written thing. >> We're not using it because it wasn't available but um we could use it um we're just not worried by this problem. It's a theoretical problem and we just eyeball the code and it doesn't do anything suspicious. >> Okay, I see. But how how come why this the Kwang PR has not been like it has been presented to me as a as a thing that has not been merged for a while >> Yes. >> as if there is there problem not a problem but >> There's there's no I don't think there's a problem I think I mean There might be a

problem the issue is that it's a massive amount of vibe coded stuff that no one's ever looked at. >> Yeah. >> Basically. >> Same with our code same with our customer. >> I I don't know off the top of my head but this is quickly checkable but yeah it's just a very large amount of vibe coded stuff and no one has yet had the time to it's a it's a review bottleneck issue rather than like some fundamental theoretical issue as far as I understand. >> I see. >> We ended up with the same thing for for some reason if you ask an AI to to write this kind of thing for you it produces 50,000 lines of code and or more and I don't know understand why but We

we might be better writing it by hand to be honest. >> Yeah yeah I was going to say that actually probably if it were written by hand it would be much more succinct I'm I'm not unclear also as to why for some reason specifically with models of computation you tend to get like just gigantic volume for some reason. >> Yeah. >> [cough] >> I'll I'll probably rewrite it by hand or or get Methos to figure out what's wrong with it and and critique it. >> That's good.

>> Okay. Um >> I think we can wrap up for now except if someone has something else. >> I I really do encourage you to concentrate on reductions and not existence of adversaries. >> Hm. >> Um one other question sorry I was late for this talk so I I don't know quite everything that's happening on this proof system app behind you. I noticed that the word Merkle tree FS this is an assumption for the moment because my team is working on a word formalization and obviously we're going to be looking at under the random oracle model proving the

Fiat-Shamir transform fairly soon. So, Ah, okay. I see. I see. Okay. Ah, oh oh, I see. Okay. Yeah, yeah. I thought you were saying you're assuming that these are sound. Yeah, sorry. I was completely But now I understand. Yeah. >> Bit of a hobbyhorse here. So, idealized models are not assumptions. >> Yes. >> [laughter] >> They are restrictions on what adversaries you are considering. >> All right. Okay. Thanks, everyone. See you around.