Zcash Quantum Recoverability

Transcript

Hi everyone. Um so today Derek and I are going to talk about uh something that we have heard that has been floating around um and it has been floating around more and more. It's starting to get actually in front of us on the ground now. Uh which is quantum recoverability >> deployed in Zcash since >> deployed in Zcash as D is saying um and um yeah I'm we are really happy to present that in fact in front of the Zcash crowd. It feels weird. Um um and yeah >> yeah let's go.

Yeah, and we are going to show why uh in uh the Ethereum crowd we are interested into doing that because there are actually a lots of uh uh stuff that um we can lots of workstream that actually get merged um when we talk about like formally verifying bite code um helping privacy apps on Ethereum making sure that their funds are sec are secure in the case of a CRQC. Uh so we do have a lot lots of things in common and when we started to work on the zip 2005 we were actually amazed about uh about like the care that has been put into it and that's why we thought that it would be a great thing to start working on and so yeah that kind of gets us to the motivation of the work. Uh we've been

seeing three accelerating trends uh lately. First architectural improvements uh in quantum computing. Uh we also seen like uh quantum secret sizes to be decreasing a lot especially using the AI potion boost uh meaning auto research and um yeah it kind of makes us scared uh in the case of Ethereum uh especially if we want if we if we are taking the path of shipping privacy apps um we want to make sure that the assets that are secured by classical cryptography today remain accessible to their rightful owners in the event of a cryptographically relevant computer. Uh on Ethereum today there is around uh

like it it floats sometimes it can cross 1 billion value locked in privacy protocols. This image come uh from L2 bit and so yeah there is like quite some FT sums secured today uh on Ethereum in privacy protocols and that's what we want to uh encourage privacy teams to be working on. uh why do we choose the risk 5 route when we don't choose the um um uh circuit uh route? Why did we make this choice? uh it's because we have seen uh some stellar progress on binary fields uh and for risk 5ZKVMs recently with flock uh magnetar from Skinat and also

because um uh we are especially like thinking of integrating risk 5 risk 5 maybe ISA on the L1 exposing that ISA to to Ethereum users also because privacy protocols are application ccentric trick. Sorry, that's not very uh correct English what I've written down, but I just finished a slide this morning. Uh, and there aren't necessarily secret developers, especially when they have like very uh custom logic uh running on their privacy apps. Um, and proving just rust is very attractive for them. They just have to take their rest code base and put that into the risk 5DKVM that they are using. And finally because uh

we do want to uh profit from the standardization effort that's that's going on and it's basically just makes it easier for existing and upcoming privacy protocols to plan for quantum recoverability when we are targeting risk 5. So that's why we are taking that approach today and not the the the custom secret one. Um so uh please uh Zcash people bear with me. Uh I'm going to try to explain Zip 2005 here. Um so three points from Zip 2005. The first one is that it proposes a change to the way notes are constructed. The plain

text nodes are constructed in in Zcash. It makes it possible to use a what we call what they call a recovery protocol to recover funds from the ironwood pool only. Okay. Um so you are eligible to that when you are using ironwood and it does require sprout sapling and orchard funds to be migrated there in order to take advantage of this change. So that's roughly zip 2005. So to give you a bit more details uh so there is like this new note plain text format that will bind all the nodes fields to the commitment randomness making the overall commitment scheme postquantum binding. So you see all

those little u uh fields of the nodes plain text are going into now the pre uh commitment randomness. It's getting committed basically in the randomness then. So that's zip 2005 and it also introduces a new derivation path for the uh randomness used in the incoming viewing key uh while also preserving a way to generate the statements on hardware wallets whenever that's possible. Um so yeah that's roughly the two main ideas of ZIP 2005.

Um so okay implementation details um and importantly it's circuit compatible so you you're not changing the circuit statement um for this reason we we actually change the circuit anyway in and use 6.3 but um for independent reasons but um yeah so it's much easier to deploy that way. >> Yeah exactly thank you. So okay some implementation um infos and benchmarks. So what we did uh we just implemented the zip 2005 using a risk 5 zkVM and since we can do it we actually use the orchard repository itself when doing it.

So that's uh one specific part of the zip 2005 and it's basically reusing all the rest um that was uh used in orchard in uh the proving statement itself. So it's nice. It's very expressive. Um and a naive implementation though isn't uh very nice because we get to up to 17 million cycles. Although like the recent improvements that we have seen now makes this figure not that bad. But yeah, uh we still optimized it. Um it's actually pretty straightforward. Three things that we did nothing too exotic. We just configure a new SP1 pre-ompile for

palace uh using the already audited wire stress pre-ompile that SP1 has been developing. So uh it it's just a matter of entering uh the um palace uh parameters. Then we just wire in the SP1 pre-ompiles for field operations into the orchard repository. And we also wire in then the palace curve operation pre-ompiles that we just did. And it just requires to add around 1.2k of a line of codes. We get more than a 10x improvement and down to 1.5 million cycles. So it's a it was a very easy very easy changes to make and we get

very good uh performance improvements and something that is actually possible to prove locally today. with less than 100 seconds on a 2023 MacBook uh M2 Pro and with formally verified bite code actually and that's what Derek is going to talk about now. Okay, before getting um your [clears throat] hopes up, I feel the need to make um some disclaimers here. I was thinking earlier on how how strong to make these and and um I don't want you to uh leave this thinking that um the what do I want to

say? Okay, the disclaimer is this uh the following is is is a new is the result of an experiment that went um surprisingly very well. Um you may be aware of our work on EVM uh trying to Yoichi mainly but um I contributed to that trying to um write programs that we really care about directly in risk 5 uh byte code and uh formally verify those programs so that you can um uh so they can perform optimally and you can optimize them and um so you don't have to rely on a compiler. Um and the natural extension from that work is has been well are there some programs that we really care about that we can just directly look at

the bite code and formally verify them there instead of at the rust. So uh normally what we would want to do um in a situation where we have Rust code that we want to formally verify is that we would probably uh try to verify it at the level of the source language which has problems because that means you're translating the Rust into some other setting. So you have a trust base there and then even if that translation is perfect and you do all your reasoning within you're still trusting the compiler uh when it when it runs. And so there's a kind of unavoidable trust base that is uh it's still a useful thing to do if you don't have other options. Uh and you can still find uh good bugs that way. But um the question is can we uh

can we go further in this new world that we're living in changing so rapidly. So this is uh pretty new work. The core idea is that um the ZIP 2005 has this very nice uh formal spec very nice specification which we can formalize in lean. So we have a high level specification. Um and agents are very good at doing that quite quickly. And then you can just compile uh the the Rust source, get your ELF file out of it. Um and I have a uh um I I can just transcribe the that bite code um into a formally verified uh risk 5 interpreter that we have. Um you could also just use the sales semantics uh directly but um

this one has an SP1 backend. So it's it um is is uh kind of I guess what we wanted here. And then the question is can you just um prove that by code directly um all the way up to your high level spec. So um I should say that the codebase as it stands right now uh there are some interesting we we do have a proof of the top level theorem um with some caveats. there are some blockers but none of them are fundamental um in the sense that it's a matter of time I had to make some assumptions so that we had a proof for for this um for this for this talk so um what is our motivation for doing this uh one is that we can avoid having the uh compiler in the trusted codebase um like I said we had

success with EVMS and we may be able to generalize uh this the compiled bite code I think is 1400 risk 5 instructions and so it's actually very small the ELF is a little bigger but um so yes we have we have our risk 5 ZKVM which is a codebase uh where we have risk 5 uh in lean um we have the spec and we have this L2 lean translator and then this diagram essentially tells this is what we want to know does this rust source or does does the code we've implemented um uh conform to the spec so um autoformalized into the top level statement here we compile down to the guest elf And then we um slowly but surely prove theorems kind of all the

way up. So um in a sense this is like a decompiler directly into lean. Uh and because risk 5 ZKVM actually does run um in this is kind of one way to think about it is a decompiler. Uh maybe a more generic way to think about it is as it's sort of a decompiler, but rather than decompiling into um into code like source code like C or something like that, you're you're logically decompiling it. So so so you're taking the the code that actually runs and then you can prove theorems that make observations about this. So um uh let's see. So these layers of kind of

decompilation layers um we start at the bottom here with just raw RV 64 im words just um I I mean we start with the LF which you know this huge string that we can just decompile it into and then and then um you can split it up into words and then you give those words uh semantics in terms of the instructions. So you can um you can have a a word that's um just kind of uh 32-bit um yeah instructions. Then you can give it semantics within the context of our risk 5 uh implementation. And then once you have that then you can go uh a level higher and you can prove these uh so-called these continuation theorems

which uh which give the instructions themselves semantics. And so um I have a [clears throat] running example. We'll go into this much more detail in the FV workshops. Um let me just >> Okay. Um so uh you can you can say for example, oh this this uh this word is um like uh modular arithmetic over over this or something like that. And so you'll give it um and and and all the while you um prove this predicate. It's safe uh PS is what it's called here. Um what it says is that anytime if you start from a a state and you uh um you run the the program anything you

can so okay um when you're decompiling you have a lowle you have sort of your concrete uh model of of what your state is and what your operation is and then and you go one level higher maybe into so-called like an abstract level and what you want to show and what this predicate shows is that um anything that you could prove about the lower you can prove in in the higher. It's it's a way of kind of chaining up um proofs. And so as you go up, so so you go from the word to um to a a a theorem that from the word to maybe arithmetic and then you you pull it up um until you can get into um into the semantics of you

the finite fields that we care about and the algebra that we're looking at and then from there you can u go all the way up to the guest statement. Um so this is Can I ask? Yes, please. >> So, is this a um kind of a hor triple approach where um kind of the the thing you're proving the intermediate thing you're proving is that if the precondition holds then um that implies the post condition and that's all you need in order to prove the higher layers. >> Yes. >> The same way that anas works, right? >> Yeah. Yeah. They are um it's like a a partial correctness triple. Um assuming >> partial not total correctness.

>> Um yes. and and and we have the initial state that we can prove things about. Um we kind of have everything. Um so so we we we have we can prove things about the first state and then from there this this kind of cascades the proof. Um uh yeah >> I guess I guess I guess you only need partial correctness for soundness. >> Precisely. Yes. For soundness. Yep. Um right. So um this took me um this took me a couple weeks. So so the main challenges to this approach right now are mostly kind of proof engineering challenges. The codebase is uh is quite

large. So um even though we only have like just maybe 1,400 risk five instructions corresponding to this program, the ELF is is a little bigger than that. And so proving things about each instruction gets quite tedious when you have about 40,000 instructions that you care about. Each of them has a continuation theorem. You're kind of knitting them all up. Before you know it, you have quite a lot of code. So currently the proofs are in the 300,000 uh lines uh of lean code range. Um and it can be it is sometimes difficult to modularize in in such a way that build times are reasonable.

So um currently the sometimes the build will take a couple hours and so I've had this kind of continuously running with agents over the course of two weeks. Um it has and and it has it it has only been a strain on kind of a normal cloud subscription. Um and I still have like it's not draining all my tokens I guess is what I'm trying to say. The the um bottleneck is actually build times currently. So it's a little bit difficult to iterate. Um and there are some questions about kind of what logic um there are some other options of how to structure this logically that may be better. Um so this was kind of a first attempt. Um

and the because the codebase is so large uh there are assumptions kind of baked in around that you have to get your head around and understand and be able to explore. And so that is one of the challenges currently is the codebase is so large um just understanding precisely what is being assumed and what isn't. Um, and so over the over the course of two weeks, it's been hard to digest, you know, the 40,000 lines of uh a code thus far. But this is these are challenges that I think um while they're challenges now, they're not theoretical and they're not fundamental blockers to actually being able to do this on a regular basis.

Um so future direction for this approach generally I think this approach is very promising and um like we were just discussing before this talk uh pre-ompiles are probably another really strong target uh for for this kind of approach. Um the scaling will likely only improve both from the agentic side of being able to harness more agents and do that more effectively but then also the proof engineering. learn things um about how to structure these these proofs. Uh we're actively working with other colleagues on um on on establishing good logical foundations for uh this kind of ad hoc decompiler rather than like this logical ad hoc

decompiler. Um the idea being that you give your agents the logical tools they need and they should be able to decompile uh for you. So um then also something that maybe a lot of this work had to do with the ELF trying to verify trying to not just assume it away um but verify the whole thing and we're hoping that a lot of that can be reused and so future future instances like this where we have a small amount of risk by bite code hopefully we can iterate much more quickly um so there are this is there's work like this happening kind of in the ecosystem and um and I expect this to be a a a fairly standard way of doing formal

proofs um in the near future. I think certainly for us it probably will be. And I think that's all we have. >> Yeah. Thank you. [applause] >> Very cool. >> Any questions? Yeah. Um so so the obvious alternative way to do it is the the way that we do all of our circuits as circuits. >> Um and the ironwood formalization um kind of its target is um Halo 2. Um so I mean but that's kind of incidental. it wouldn't be that difficult to move it to

a different arithmetization for a new proof system. Um, and so >> yeah, >> so we're still we're still >> Yeah, go ahead. We're we're still writing the formal spec in um clean which is um a way of writing circuits in the >> um and then um we show that um the uh the circuit as compiled to a verification key or to to a the multiscaler modification that the verifier is doing matches the lean specification. So that's a different way of doing it.

>> Um, and you kind of don't get this blow up because you have a higher a hand optimized circuit. So you have a more efficient circuit and and it's also kind of easier I think to do the proof >> um and easier to check the proof. So what I think I'm asking is has the Ethereum community seriously considered using um circuits alongside um VMs for your work, >> right? Um and what were the conclusions?

>> Wait, what does circuits alongside VMs mean? like some things are in circuits and some things >> cuz cuz VMs have advantages but >> yeah um I think for the exposed ISA um that will definitely use VM just cuz I think Pierre mentioned that for regular application developers it's a much better UX to have um ISA exposed uh for things like signature aggregation where we it's in protocol basically um we we're currently discussing whether it makes sense to reuse the VM for that or uh just have like circuits like previously or historically like historically we just wouldn't write circuits uh cuz it's very easy to to

introduce a bug into um when you when you're writing circuits but with FV I definitely think there is at least an argument to say that we should consider it given the performance improvements from not having the VM overhead. Yeah, I mean VMs scare me because they're so complicated and they are you still have to have circuits um to implement the the VM. So yeah, you've got two layers either of which can go wrong. >> Right. Right. Exactly. I've never >> at the end of the day.

I think the user experience part still matters these days in terms of like you know >> in that prom. >> Right. Right. Right. But maybe you know in the not so far future it won't even matter anymore like it won't matter that you have this sort of like clean very expressive language because you'll ask your AI to do it and then you can formally verify it. Well, well, it will matter because VMs introduce a huge overhead relative to >> No, but I was making the opposite point of like maybe you can just use your kids and you know and and uh and then devs will just like code their apps um with AI anyways and it won't they won't need to have this sort of like expressive

language they want to sort of like deal with. We do see differentials in the agent's ability to write good program. >> Yes. >> Haven't seen someone new maybe like low very >> for now. For now. >> Yeah. Exactly. Yeah. >> [laughter] >> So, so apparently it's quite difficult to um to prove stuff about noir according to Zach. Anyway, >> no, I wasn't saying it's difficult to

prove without not, but if you're writing circuits manually, then I think it helps to have a DSL um as an abstraction layer. Um, but yeah, I mean for what it's worth, I mean I I've I've I've been going back and forth hugely myself uh and with an Aztec about like do you like do you focus on direct compilation via DSL or do you go to ZKVMs and until recently I was all on the VM bandwagon because as an abstraction areas is so much more convenient both convenient for developers and whilst it has complexity it is quite straightforward to formally verify a VM.

Um well it's it's a it's a pretty clean abstraction layer but but then the challenge is yeah it's it's actually if you're using a VM then then that that gap between your high level programming language and and the VM bite code you can't really formally verify that um and so uh if you are just directly writing circuits um then your your expression of your program is much closer to something that you can then like specify and lean and formally formally formally verify um which makes a big difference um and I think person I'm curious what others think I think it's very much an open question

actually of like how do you >> question >> well it's yes but also just generally if you're using a language at all then you have to formally ver like formally verifying a compiler is is a very challenging task. >> So it depends a lot on the compiler. If you do like a compiler for a toy language, then you know there's hundreds of academic papers every year that kind of do this. >> Yeah. Yeah. Yeah. But if you want something which doesn't have horrific overheads um and create very complicated circuits with very large proving times.

If you want like something >> I think the trick is to keep the compiler as small as possible, not in the sense of the complexity of the optimizations it does, but in the um size of the domain over which it operates. I think that's the the kind of direction seems like a lot of small compilers is is maybe one direction to go in. Um and then a lot of you know ML and composable correctness about compiler dialects and yeah >> I'm all on the compilers we're about idea um side now which is AI has changed everything um because if if you write a high level specification and you write as directly as possible to the

arithmetization that is um used by your proof system um which an AI can do. Um, then you're trusting that you're minimizing the trusted base if you do that. >> Yeah, compilers were a bad idea. It's [laughter] it's it's deliberately a provocative take, but um >> I'm still a compiler Maxi. [laughter] >> Increasingly so, actually. >> I I am being slightly contrary here. Um, but it's it's getting more and more interesting to just consider not using a compiler.

>> Okay, just uh we're >> we're nearly at two minutes. Okay. Yeah. Can I ask how does this compare to say like >> I um am still trying to figure uh I'm still trying to find my head in terms of um all all the different um approaches to this. So I don't yet have a very strong answer uh for for that that question. Um yeah this yeah Alex may >> so I think it's more you wouldn't need full iris or something like this because you're looking at fairly simple simple uh single threaded programs and so a lot of the reasons why you would want to use

iris would be if you have you know a lot of concurrency and a lot of like weird complex memory management you would see in distributed C++ code or something like this um so you would need a program logic whereas you need full iris I think it's not clear or you know doesn't seem to be the Yeah, I think this approach um you sort of pick up the logical tools you need ad hoc um depending on the program you're looking at. Yeah. >> Um yeah, I think in one of your slides you had a elf to lean um like arrow. So this is completely trusted or >> um it's a it's it's it's completely trusted. I mean, it's a

function in lean. Um, it's a function that's fairly easy to read. It's it's basically kind of it it decodes um like I I think it's something that that can be in principle like checked um pretty straightforwardly. It it's basically a copy paste um but in in the new format um essentially. So I have to check. Last time I checked, I believe there were formal proofs um about the ELF to lean script and so it may actually already be formally verified.

>> Okay. >> Um but yeah, this I mean this is a much more reliable kind of translation into lean I would say than you know doing it from Rust. Um because the semantics are >> very very very clear. >> Translation. >> Yeah, exactly. You have you have semantics. Yeah. Yeah. Exactly. Um >> do you do you have any intuition as to how to make this cheaper? Cuz I'm not super convinced that agents getting better will be like the solution here. It seems like maybe the elf itself or the risk five bite code needs to be maybe formatted in a way that makes it easier to >> Yeah, I I think um we'll have to find tricks. So in this case, there's one of

our imports that made it so we couldn't use lean's module system, which is already a big hit on these big that would normally give us some performance gains. Uh and that would be a pretty basic step forward. I think uh finding good ways to kind of organize uh especially the ELF see like I would really love if if we could have reusable infrastructure that just kind of comes with a nice clean interface um where you can import the bite code that you care about um and uh the ELF is kind of taken care of for you. So probably some work on all of that formatting to make an interface that's cheap to use so that all your verification work can hopefully

focus mostly on um on just the program you're looking at. Um so I that's that will be my first see if we can modulize that and make it into kind of its own thing that you can just call. Um and then uh I guess tactics good tactics that that are that have strong automation. Um, yeah, I mean there haven't been I haven't tried to optimize it at all uh yet and so I think there there's probably quite a bit of lowhanging fruit. Um, yeah. Is the health a release artifact or do you leverage the debug information because there's a lot of like register allocation and address

mapping which is um critical to kind of doing the decompilation and kind of constructing the higher higher level layers. you do that or is it just using um you know the >> um let's see we I believe we use all of the register al like um so that was something I initially had to assume and trust the Rust compiler and I'm in the process of [snorts] undoing that uh and so the plan the plan would be I mean to to Um yeah, we probably can. It's quite

it's I don't know if we probably actually don't have time to read all assumptions. >> Yeah. Yeah, the assumptions right now. Yeah, there's the caveat at the beginning because the assumptions are extensive, but they will go down. I Yeah, promise that. Um Okay, I think that's probably all we have time for. Yeah, thank you. [applause]