ArkLib: Verified Proof Systems in Lean

Transcript

Thank you. The floor is yours. >> Yeah. Thank you. All right. So, uh I'm going to try to spend a bit of time to talk about arcl. And in in simple words, what ariplet is is it is a uh library written in lean for the formal verification of snark protocols. So, think of the back ends of of all these snarks and zkms that people are working on. uh that means that the protocols in lean should be executable. The spec needs to be executable and it comes with uh mechanized proofs of security. So all the proofs that you see on pen and paper, we will try to get them written down formalizing.

Um, okay. And and why we're doing this, I think it's it's sort of clear uh to us that having uh security uh at the highest level of confidence is extremely important for Ethereum. Uh and the state-of-the-art to date is that there is zero uh project who have gone all the way from a verified specification with security proofs to an actual implementations. we've gotten some of the way there, but there needs to be sort of unified tooling to get get us all the way there. Um, and of course when when we write papers, we often elite many steps. We have informal descriptions and the course of

formalization uh helps us brings out all of these gaps that needs to be filled. Okay. So specifically how we're doing it is that um we are starting with the most uh uh generalized abstractions which is functional interactive oracle reductions. I'll show you what it is in the next slides. Uh but some some uh IOP people here may may know it already. The point is we can break down any complex oracles into a series of these smaller reductions and we specify compositions uh operators to essentially glue these into a a unified protocols while still

carrying over the security proofs as we do the composition. Um so that is the the IR is sort of the information theoretic uh secure step uh part of of all of this. We're also looking at uh implementing these uh functional BCS transform which is basically you take MOGO trees and you uh make the IU into just an interactive reductions and also we do fashion mirror uh and specifically not the fashionir that you see in a paper where it can be inefficient. We're actually aiming for the ones that will be implemented in practice the the duplex sponge version.

Um and as as Alex mentioned, we're also going to verify all the rust implementation as well via currently via an extraction into lean improving functional equivalence with the lean spike. Okay. So this is the central objects that uh we're we're formalizing in art. Um an interactive oracle reductions is an interactive protocols between a prover and a verifier where the verifier can sort of um see there's the explicit instance the x part that it sees in full but there is an implicit instance y where it can only access via some oracle

interface. Think of it like a vector and you ask for specific elements of that vector or a polomial and then you ask for evaluations of it at a given point. Um we have the completeness and soundness properties of course lots of soundness uh notions that we we will all need to specify and then proof security and proof reductions between these notions. Um and um we want to be as general as possible and so these oracle interface are uh can be custom they don't need to be vectors don't need to be polomials we can define them in a case- by case basis and also the the output the sort of y to the output implicit instance we also need to be

very precise about how it is being defined in terms of everything else that the verifier sees. And so why we're doing interactive oracle reductions, it's because existing protocols are often just these reductions composed together. And so if you have two reductions and they share the output of one is the input of the other, then you can just compose them. And here's an example of the subject protocol. You can just break it down into each router and they nicely compose together.

Um but there is a a limit to sequential compositions which is that the the output and the input of the two must match exactly and if you think about uh many many protocols in practice this is not always the case. Um the second thing that's needed is that this idea of of virtualization. So you may have a a simple protocol um and you want to invoke uh that simple protocol but within a more complex protocols and this actually happens all the time. So like in in Spartan or superpartan for instance we we want to evolve some shake but we we evoke it on sort of a virtual polomial that is

derived from the inputs that are currently available at the time of the sparing protocol. And so we also need to give sort of precise semantics for what this means when we formalize this in lean. And it basically just boils down to you need a map from the inputs of the outer to the inputs of the inner protocol. And you need a combination uh map uh to get back to the outputs of the outer protocol. And we need to also think about like the conditions for these mappings in order to preserve the completeness and soundness properties that we want.

Okay. So, so that's all on the technical side. Last slide is basically our progress so far. So, we have a a bunch of uh protocols and people working on these various protocols. Um, of course we we always want more contributors and I think the gi uh having people that are experts in these pro systems somehow getting interested and uh trying uh to trying these tools out would be amazing and we can be uh help here in in regards to the lean part. Um in order to develop arcliff and have all these nice

properties that we want like executable spec we have to develop um a fair amount of time on just the computable data types that we need in order to run these protocols and we're also developing all these coding theory uh preliminaries that are essential for the security groups. Um, finally, our clip is is still fairly young and we have learned a lot along the way and so we're constantly trying to make it a better experience for people to contribute to it. Uh, we we will try to make the protocol description more and more compact so that it could still fit in say 2,000 lines of lean code or for the

lean uh VM or lin p or so on. Um and we are also developing uh auxiliary libraries that are needed for the security groups. Um so yeah I I'll just flash these names here. Um so yeah that is the end of my talk and thank you. with respect to proving soundness of these reductions and the compositions what soundness property are you proving because there's a lot of different variants right

>> yes yes so at the IR level we're going for run by round knowledge soundness at least for the protocols that can satisfy them um and then that is sufficient to imply state restoration knowledge soundness which then after all the compilation parts implies a knowledge sound stark >> okay which definition of knowledge are you using like the >> there's sort of an original rumbaron knowledge then there's uh I think one from the like >> yes yes warp paper and then there's this rumbaron tree extraction that's also sort of related >> um currently we don't have the tree extraction we don't have any kind of forking or rewinding uh we do have both the old and the new versions in in the

warp paper and we're also almost done with proving like one implies the other like the old one would imply the new Thanks. >> Uh how do we determine that the formalized statements that we are approving mean what they're intended to mean? >> Yes. Uh excellent question. So lots of uh reviews by everyone who's interested. Um, we have also implemented uh automated AI review of every PRS and that's actually caught a number of misformalization bugs uh up to this point.

>> Yeah. So, so there there's no silver bullets. We just need lots of eyeballs looking at. >> Thank you. >> Uh, for those AI reviews, are you using like um classic model like G 2.5 or CL? Okay. So we're doing Gemini 2.5 Pro because the large context window it has is quite good because with the prompts that we do on get PR we can feed it external context. So if I'm asking it to review some coding SPR I can just feed it the entire book that has written and that helps my this saves me reading 600 pages.

I have a question. Um, are you able to reuse math or is it like a reimplementation of a lot of the results? >> Um, yeah. So, a lot of theorems are in Mathl. Um, but for instance with polomials, the math polomial is not computable, right? So, we have to develop the computable types and then transfer all the leas from the math. So you >> okay so you build the bridge the computable bridge and then you can reuse the math.

>> Yes. Okay. >> Quick question. uh you said I mean it seems to be quite natural to have these I don't know how how did you call this roundwise reductions uh like a chain you simplify the initial claim that something is in a language to smaller claims and so on in each of the reduction steps or soundness error knowledge soundness error is is there any real world protocol out there which does not I mean the design principle is not built on this round wise reduction because I wouldn't know of any >> perhaps cross 16 like these >> ah okay yeah I'm I'm still in the

interactive oracle >> right then I don't know I think every every protocol is built >> yeah I wonder if there might be a very >> productions by definition are a generalization of arguments so >> exactly >> no matter how you're going to look at it some any interactive argument you're going to be able to cast as an interactive production yeah all these nonattractive things probably want it as well as never thought about them. Maybe a comment like if you think about the way fried fry you know yeah fried there is like still this idea of like reducing by thing but the the way it is done you know >> you have this crazy query which kind of

like break this abstraction you kind of like uh you know so the the round of fry was something that came out quite later like I think was three or four years later after the original paper so you could argue The original paper had a round bar around proof. It was just not named that way. >> Did it? >> It does. Yeah. They just don't realize they do. But yes. >> Okay. >> Yeah. Because >> anyway, this is workshop discussion after lunch. >> Yeah. But yeah, to me at least the protocol. >> Yeah, I agree. It's a more complex proof, but and and you have to maybe if you want to be super clean, you write down the the languages uh and the reduction set more explicitly. But if you parse the proof, it's It's already wrapped around.

>> It seems quite complicated to prove that something is secure without actually proving that it is. >> Fully agree. Fully agree. But >> it's hard. >> That's the way I think either. Yeah. >> Okay. Thank you so much. >> Couple of short notes. Um, we have channels in the telegram group. If there's any Q&A or conversations that you want to like continue on, feel free to do it in those channels. Uh, food is just around the corner. And any speakers, if you could just post your slides in the channel or DM them to me, try to collect everything and get them out as quickly as possible.

>> Thank you, Will. And I also want to give a shout out to Will who actually organized this event. not possible without you. Thanks. Okay, last time. Here's one thing that's

>> tomorrow. I guess my my problem with your That's good. And

In the end, there was also Amazing. We can generate whatever we want. Say