ZK13: Shedding light on Noir with Lampe - Matej Penciak (Reilabs)

Transcript

All right. Well, thanks for everyone who's coming here and thanks for the organizers for inviting me. But um so my name is Maciej Pęciak and I'm going to be talking about Lamp, a tool that we're building at Rail Labs. Um so the title of the talk is shedding light on Noir with Lamp and the idea of Lamp is we're going to be understanding Noir code a little bit better um at the end of this talk, hopefully. So the one thing I want to mention is that um because this is a workshop, I want this to be a relatively like interactive um uh talk. So I'm going to go through my slides, shouldn't take too long, and I want the uh latter part for maybe the last 20 minutes or so to be like a

question answer and then also a interactive component. So if you have your laptops and you want to join along, play around with Noir and Lamp, go to this QR code or um to this ZK Summit 13 talk um get repo and then click on the code space or the the big green code button and then the code's create code spaces on main button right there and then that'll get get the the whole process started. It takes a little bit for the code space to get started cuz it's a Docker container and it has to download and extract and something.

It's not going to be on your local machine but it'll be somewhere in the cloud. But it still takes a little bit time for for the GitHub runners for this to work. So if you get started now by the time I get to that part part of the talk, everything will be ready. Um all right. So I want to say this is a talk about formal verification and I should say up front that formal verification is hard. Um no one really wants to do it. I mean we've all been in the place where we worked really hard, we wrote a few hundred lines of code, we implemented a new feature in one of our uh one of our projects and then we get to the get uh GitHub uh you know, PR the review process and one of the reviewers says, "Oh, there's not enough testing."

You're like, "Oh man, I just want to get this merged and move on to the next thing. Fine, I'll write some tests." Um maybe they are a bit more of a stickler and they say, "Okay, well, you know, you've tested all of these unit cases, but you haven't um you know, done any property-based testing." And you're like, "Oh man, that's really annoying. I now have to start pulling out some like property testing libraries. I don't really want to do that." And then it gets even worse and what if this person's like even more of a stickler and they say, "Okay, where's the fuzzing? Where's all this stuff?" So, all of these tools, testing, fuzzing, etc. are all within the umbrella term of formal methods and formal verification is just a part of that. And it might be sort of the most heavy-handed part of formal formal

methods, but the idea is that instead of just testing your code, you're going to be writing specifications in some sort of machine language and I'll be talking about the kind of language we're using for lamp later, but you're going to be um you're going to be formally specifying the properties of your code and you're going to have to you know, actually take the time to write these out. And so, this is a long process and it's generally pretty hard. Um even harder is actually like sitting down and proving the properties uh as well. So, not only do you have to spend all the time to write down the specifications, you actually have to spend a good amount of time to actually prove this stuff as well.

Um so, you know, and you know, consider that the small 200-line feature that you just implemented, that's going to be a lot of uh overhead that you're going to have to implement um all of this proving. Um and generally, if you just ask anyone out there, formal verification has a high barrier to entry. So, you have to learn new tools. Say, I'm implementing a new feature in Noir, I'm going to now have to learn a completely new language in order to do this. Oh, I don't want to do that. I want to keep with my Noir language, maybe Rust. I don't want to learn another language in order to do formal verification.

And now I'm going to be using some bespoke tools that maybe someone else on my team has written for it for this project. I don't know exactly how these things work and there's maybe like three or four people that I can ask questions from and they're not going to be very helpful in the in the end anyway. So the the the theory and the the tools that I'm going to have to learn are are are prerequisites that I don't really want to spend too much time on. Um and then finally, you know, there's a lot of repeated work. So a lot of times in in the formal verification space, people are going to be writing tools that um can work in very specific domains or work on very specific projects. Maybe something as specific as a single library, maybe a little bit slightly more general like

maybe uh like a set of libraries or or a set of domains within a language. And you know, maybe even like a a particular language. But the the amount of repeated work is is a little bit of a barrier to entry as well. And so the idea behind Lamp is like let's try to make this process of formally verifying a little bit easier. So we're in the course of of working on this project, we've brought together some well-established theory. We're not reinventing the wheel. We're taking things that are well known within the the theory literature for formal verification and combining them into uh a a useful product that makes the life of the user a lot easier.

Um we're building tools so that the end result, this Lamp tool that we're building is user-friendly, doesn't assume you have a PhD in computer science in order to work work with the with the tool. Not saying that a PhD in computer science is a bad thing, but not very many people out there have it. So, you know, we don't want to have uh we don't want to restrict our tool to only people who have a PhD in computer science. We want people just general Noir programmers to be using this tool and verifying their libraries. Um writing the proofs could be hard, but if there's sufficient automation in there, it could be a lot easier. And so, we've written a fair amount of automation to make the proofs easier so that in the end, you don't have to reason about the exact semantics of the language or the exact specific specific

specific properties of of of how this language how the different language components piece together. We want the proofs to basically mirror the the language or the the core logic that that you're trying to implement with the the functions that you're implementing. And so, the proofs with this automation should generally be uh relatively understandable. And I think one of the big components is we want these proofs to be composable. So, we want all of the different libraries to be able to talk to each other via not only the the libraries written in Noir, but also the proofs that are going to be extracted as well.

So, once you have these proofs over for this library, we want the proofs to also be applicable to this other library over here. So, the proofs in the end should be composable. And I'll I'll get into exactly how we make the proofs composable, but it deals with not specifying too much and not making uh too many choices for for the extracted proofs. Um and then another big barrier to entry for which I didn't really mention mention last time, a big barrier to entry for formal verification is that a lot of times by the time people get around to formally verifying software stacks, it's been around for a long enough time that the amount of code written in that language is insurmountable. There's no

way you can formally verify everything from the very beginning to the very end. But, Noir is relatively early in its lifespan and there's really a chance that if we start early enough that we can end with a whole ecosystem of Noir libraries that are formally verified and that can work together and you know, as more get you know, as the the a larger portion of the language gets formally verified as a larger portion of the libraries get formally verified, it gets easier to formally verify things later on. So, like I said, Lamp tries to solve this problem for Noir, and I think we've come to a nice kind of place with it, and I think in the end it really does solve the this problem.

So, quick introduction to Noir for the people who aren't familiar. So, it's a language. Uh it has Rust-like syntax. Actually, let's just show everything. It has Rust-like syntax. It compiles to a circuit-type uh intermediate representation called ACIR. I think it stands for abstract circuit intermediate representation. Um it supports a lot of the language features that you're familiar with in Rust, like generics, traits mutability references loops conditionals, et cetera. There's a few tricky things. This being a ZK language, you need to know or the Noir compiler, rather, needs to know the length of the loops. So, if the loop doesn't have a finite length, that the compiler's going to complain. It needs to know vaguely that your function's going to terminate eventually, so it has

some sort of rudimentary termination checkers in there. And um but otherwise, like you can program in in Noir pretty much exactly how you would program in Rust, and you should be very familiar with all the general language constructs. And you can see here, this is an example of a Noir code. It should look very familiar to you if you've programmed in Rust. It has these traits, binary hasher trait. It has maybe some types that aren't familiar to you if you come from Rust, like field, but that's not so surprising if you're doing some ZK context type stuff. And then we have a loop here, uh let mute to define the mutable variables. This is all very familiar to us.

And then the last feature that makes Noir a ZK language, it well, in addition to compiling to ACIR, is this ability to have unconstrained uh unconstrained code. So, there's no example of unconstrained code here, but you can write sort of like unsafe blocks in Noir. That's kind of like unsafe blocks in Rust, but instead of circumventing the borrow checker, what it's doing is it's circumventing um like you know, it's it's it's going to be generating some unconstrained prover hints for the circuit in the end. And so you don't really get to control exactly what the unconstrained hit unconstrained hints are saying, but that's that's where a lot of the power of ZK language is comes from. If you bring in unconstrained things, but then

have constraints at the end that actually constrain the stuff, you can get a lot of leeway out of that. Um so let's introduce uh so that's the quick introduction to to Noir, quick introduction to Lamp. Um so it's made out of three components. The three components are an extractor that turns Noir into Lean. So I'll a little bit more about Lean later, but Lean is the language where all of the semantics and the proofs and stuff are going to be done. And so we have an extractor that turns Noir into Lean. Um it extracts before monomorphization. So it will keep the generics intact, and this is one of the key components that makes the proofs that we write composable. So you can write proofs about generic Lamp generic Noir programs, and you don't specify to the particular uh

instantiation of the generics. And so if you have a library that's fully generic in a lot of different generic parameters, you can then prove things about that library and specify to all the different domains when you use it in the different domains. Um the output of the extractor is a human-readable DSL in Lean. So this is important because you want to make sure that the extractor isn't doing anything crazy. Well, I'll show you an example in a bit, but it should look it should mirror very closely to what you've written in Noir. Um the expectation is you're not going to be writing very much of this DSL, but if you really wanted to, you could.

And you can reason about things in the Lean side and then go back to Noir. That's an interesting workflow that might be possible. Um so the next component of Lamp is uh implementation of the semantics of Noir in Lean. So I'll say a little bit more about exactly what semantics means in the context of formal verification, but essentially this is where we can sort of encode what actually means to write, you know, what what this block of Noir code actually means. And this is where we actually start reasoning about things. And then the last component which is important to make the tool usable and friendly for users is uh automation. And so we've introduced a number of tactics that make the proof automation or uh the proofs a little bit easier in that they should

mirror the code structure that you have in Lamp or sorry, the code structure you have in Noir rather than having to dip dip into complicated things that only computer science PhDs care about. Um yeah, so so the so we shouldn't have to worry about how the semantics is specified. The in the end the proofs should really just mirror how the Noir code is written. Um so here's an example of an extraction. So on the left-hand side we have Noir code. This is taken from an example that we've done previously implementing a particular hash function, but on the left we have Noir code and in the CLI or in your command prompt you just type Lamp and it'll generate some sort of new Lean code. And on the right-hand side

you see the Lean code that's generated. And you'll see that it actually looks very similar to uh the left-hand side except for maybe some extra annotations here or there uh related to types and uh things that we don't want to have to do on the Lean side like type checking. Uh so like for example, you see the ROL function you have U shift left one uh or with the top bit and over here you see the the exact um same uh same thing implemented on the right.

And then similarly rotate left, you're just repeating this loop n times and on the right you see here again it's repeating n times. So this is an example of of the extractor. Um so the next component of of Lamp is the semantics. So I'll just do a really quick crash course in semantics. How do we reason about computers and computer programs generally? So, we encode the the logic of of uh how we're going to be proving things about Noir in terms of these things called Hoare triples. This is something that's well known.

Has been around for a long time, since the '90s, I believe. Maybe earlier. But, the idea behind a Hoare triple is you have um three three components, P, C, and Q. So, P and Q are predicates, things like propositions, things that you're sort of trying to prove about the Noir code. These can be like invariants, or these can be um uh like just general thing uh properties about the state that the the Noir code is being executed in. The C in the middle is actually the the code that's executed. So, when you see a Hoare triple like this, PCQ, you want to read this as something like saying, "When P is true" P is a predicate "if C is executed, then it will terminate and Q is true." So, we call P the

precondition and Q the postcondition, and C just essentially the code that's being executed. And so, a Hoare triple is essentially a way that we can we can encode the semantics of of a particular code block for for Noir. And the basic rules uh there there's a lot of rules about uh Hoare triples, and I'm not going to go into every single one of them, but one of the most important ones is this one right here. And it's written out in a way that is very common that you'll see in a lot of computer science papers, and I'm introducing it here just so that whenever you see these kinds of things, uh you don't get too scared. But, this is an example of a judgment. And what this judgment is saying, if you sort of parse it out, this Okay, now I'll take

this. Um we have these two pre uh we we have these two um Hoare triples here. And if these two Hoare triples are true, then this last Hoare triple is true. Okay, so now let's parse out what these three Hoare triples are saying. So this is saying that if I have a precondition P, execute C1, then the postcondition R is true. This one is saying that if I have the precondition R, I execute C2, then the postcondition Q is true. And the end result is something about composition of these two code blocks, which is saying that if I take the precondition P, which is the initial precondition, execute C1, then execute C2, then the postcondition Q is true. So this is kind of like one of the

basic building blocks of Hoare triples, and it's one of the ways that you can use Hoare triples to reason about programs, or reason about semantics of programs, uh um compositionally. There's a lot more. For example, if I know like uh P implies Q, then if the postcondition is P, then the postcondition should then you can replace the postcondition with Q. There's a lot of rules about Hoare triples, and I'm not going to go into all of them, but you know, they all kind of have the similar flavor, where you're going to be putting things on top of the judgment line, and the conclusion is something on the bottom of the judgment line. Um and then I should say uh also I think uh I'm I I'm happy to take questions at any point. So if you have

any questions about this or anything else I've talked to about so far, so just please interrupt. Yes. Um One second, they they need to get you a mic. Yeah, no worries. Is there any assumption that it's all sequential here? It has to be sequential or not? Yeah, yeah. Um so yeah, I guess we're not doing uh like distributed systems yet maybe. We can see. Um but yeah, so this is an example of sequential composition. Um So this is crash course in Hoare triples, crash course in separation logic. These uh because Noir has mutable state uh with references and mutable variables and function references and

all that kind of stuff, we need to talk about the state as well. So, whenever we're dereferencing a function pointer, for example, or we're changing the value of a mutable variable, we need to somehow talk about the state. And instead of encoding the entire state in these preconditions and postconditions, some really smart computer scientists a few years ago, like in the 2000s, I think, came up with uh this notion of separation logic, where you can sort of separate out your state into these little blocks, and you don't have to specify the entire state at any given time. You can only specify the state that's being talked about at any given point. So, we'll see you uh a few examples of this when I get to the interactive component, but um yeah, it's it's roughly it's roughly uh

saying that, you know, we can we can talk about uh the state without having to refer to the entire state at any given time. And um for the user, the reason why I'm saying you don't really need to know a PhD in computer science in order to use Lamp is that a lot of this separation logic can be automated away, and the user never has to really worry about it. And this this comes from this idea of minimal preconditions, in the sense that there is going to be a minimal P here, in the sense of like logical implication, for which these kinds of judgments hold. And if we just kind of keep track of the minimal precondition at any given stage, we don't have to worry about specifying that at every given stage. We can just kind of compose

these all things these things together, and really only worry about the initial precondition and the end and the very end precondition very end postcondition. This isn't literally true. There's going to be states in the middle where you're going to be you're you know, it's not completely automated away. You you have to be a little bit clever sometimes. In particular, whenever you see a loop, you're going to have to be a little bit clever and and and specify these things called loop invariants. And then, whenever you have a function call, sometimes you're going to have to be a little bit clever as well. But other than these like two sort of situations, generally we would hope that the automation that we've implemented gets rid of any notion of these preconditions.

Um so this is almost good enough what I just specified in the last slide is almost good enough to talk about Noir. This kind of stuff was implemented for a lot of languages that we're already familiar with C C++ maybe not C++ definitely C. I know there's there's projects in Rust that are trying to use separation logic to reason about Rust code. But what's different about Noir is that we have these unconstrained unsafe blocks these prover hints that we don't have in in just traditional language context. And this is where some new ideas had to get introduced and so there's a paper by I'm not going to pronounce that right.

Is there anyone who's French in the audience who can No, okay. I'm going to do my best. Charguéraud? So what's that? Khuon? Okay. I'm I won't get it right, but thanks. So they they have a paper about omni-semantics and the context of the paper was to reason about non-deterministic computation. So I can't really read the authors' minds, but I assume they were thinking things like introducing random variables into functions and all that. But it just so happens that this is the exact right idea to reason about Noir code as well.

And so in addition to these Hoare triples and these separation logic type ideas from earlier these omni-semantic judgments are introduced and what they essentially imply are statements of the following form. So for all possible values, the following predicates hold. So if we introduce an unconstrained hint, we have no control over what that value is. And so the best that we could hope for in our proofs is that no matter what value you fill into this hole, this following predicate holds. And this is the idea of omni-semantics and this is how we've implemented the semantics of Noir. So whenever you see an unsafe block it and there's an example in the the sandbox, you'll see that it just kind of gets extracted to a very simple, "Hey, this

thing exists. We have no idea what it is." And presumably if you've written your code carefully enough, you should be able to prove the specifications you want between the unsafe blocks and the extra constraints that you've added in. So, here's an example of semantics from only semantics. This is as implemented in the the paper uh You don't have to read through this. This is just a bunch of fancy rules. Um and over here, again, a big block of text. You don't have to read this, but this is how we've implemented in Lean.

So, we have all the different rules and there's almost like a exact one-to-one correspondence between the rules on the left and the rules on the right. Um and then now once we have the semantics and we had the DSL, we can start doing proofs. And so, here's an example of a proof that we have about Noir code. So, um if you recall from a few slides ago, I have this rotate left function here, which I've extracted to this rotate left function here. So, this is again, you basically take a U8 and you rotate left another U8 number of times. And so, what I've done in this example proof is I have this rotate left function. This is now Lean code. This is just straight up like a declaration in Lean. I'm

repeating this RL function n times. And here's a proof that the extracted Lean code or the extracted DSL matches this reference implementation. And so, you can see here a little bit of this Hoare triple stuff starting to appear. So, we have this n less than 24. This is our precondition for the Hoare triple. We have this function body here. This is essentially saying we call the rotate left uh uh function with inputs input and N, okay?

And then this is our output Hoare triple, which is essentially saying that the output of the function is equal to if I call this function ref .rotate_left input N. So, you can sort of see the the the Hoare triples mirrored in the function declar- in this theorem declaration that I have. And then this by block starts the proof, and this is just a straight-up Lean proof. And if you've if you're familiar with Lean, this should look familiar modulo a few different spec- specific situations relating to Noir, but we have a lot of automation here that we're using to make this proof a little bit easier. So, we have this enter deckel automation, we have the step step uh automation, which is kind

of like the catch-all, this is how you should be stepping through your function. We have this loop inv um uh function, which kind of tells us that uh this is what should be true about the state at any given point inside the loop. And then we have uh a little bit of a Lean proof here that we have to uh to work through, which is related to the function logic. Um so, this is more of a complicated example. There's easier examples in the interactive component at the end. Um so, I've kind of told you what LAMP is and what LAMP does, but let's just say a few words about what LAMP doesn't do. So, it doesn't verify the implementation of Noir itself. So, it's not not verifying the compiler, it's not checking anything about the constraints

that are that are generated. And it doesn't automate your job away. So, as you saw, we had to write the proof manually. So, there is some automation, but it's not going to be doing all of our work. So, you have to write your own specifications, and you have to guide Lean through the proofs of correctness. And in the end, it also doesn't execute Noir code yet. So, there's a little bit of an idea that we could try to try to automate some very simple proofs away by just literally saying, "Oh, no, just run this function and you'll see that this is the right right result." And so, some very simple functions should be automated away in this way. But, as as of yet, we we don't run no our code exactly.

So um now just to get you a little bit ready for the interactive component, here's a little bit about Lean. So, it's a functional programming language with Haskell-like syntax. So, I've shown a couple examples of Lean code already, and if you're familiar with Haskell, it should look familiar from that. Um the difference with Haskell is that it has a type system that's expressive enough so that it can specify things about propositions about Lean. So, it can specify like, you know, you can do existential quantifiers like the exists backwards e kind of letter. You can do for all uh uh uh upside-down a universal quantifiers in Lean. So, you can encode all of this kind of stuff in the Lean type system. And with these uh together with the sort of expressiveness of like the calculus of

constructions, whatever that is, you can sort of just talk about mathematical objects. You can talk about Lean objects. You can talk about Lean data. And you can start proving things about them. So, a question is like maybe why use Lean? There's a you know, Lean is not the only interactive theorem prover out there. It's uh possibly the most user-friendly, though. And it was originally written, you know, back in 2011, and there's many iterations. We're already on the Lean 4 version already. And Lean kind of has turned into a tool that's very useful and use familiar to mathematicians. And so, if it's good enough for mathematicians, it should be good enough for computer scientists or people who just generally talk to computers all day.

Um I was a mathematician in a past life, and I would say uh I did not know very much about computers when I was a mathematician and I would say you know I think I even even as the the sort of naive mathematician I was back then, I could still use Lean. Um and yeah and so there's a large community of mathematicians building libraries of formalized math in Lean. This is a mathlib. This is a a library. If you go Google mathlib or something like that, you'll find it. It has a ton of math that's already formalized. Um and it they've also implemented a ton of tactics or proof automation that make your life easier when you're trying to write Lean proofs. So we have all of these tactics and I'm I think actually even in the last couple slides you saw examples of these tactics. So we have RW

short for rewrite, apply, ring, linarith, simp, asop. There's a lot of tactics that have already been written about uh or already written in Lean that make um make your life easier when writing proofs. Um and then oh yes. Just in general terms about Coq. Yeah. There's a There's a Yeah. Just in general terms about Coq that is probably known as Coq. Yeah. How does that compare about to like adoption and and features? Mhm. I I would say it may just be my experience, but so so in terms of the type theory, they're very similar. So mathematically, I think they're very similar. In terms

of the tooling, I would say Lean has very user-friendly tooling. I've recently tried to get Coq uh I mean I've worked with Coq and and the Coq tooling is getting a little bit better and I think they've kind of gotten pushed a little bit further because the Lean tooling is so much better, but I would say the the Lean tooling is still a little bit better. In Coq, the automation, the tactics are implemented in OCaml basically. In Lean, they're implemented in Lean. So this makes it a little bit easier for mathematicians where you don't have to learn a wholly separate language in order to talk about in order to do the meta-programming. The meta-programming is entirely in Lean itself. So I would say they're very similar and even the the syntax and the tactics, El Tac looks very similar to the tactics Monad and Lean. They're very

similar. But I would say the real big difference is this this automation metaprogramming is a little bit more robust in Lean. It's a little bit more user-friendly and I think it has a little bit more buy-in from the math community. So I think the general um uh like culture in in Roc is that people will write libraries which prove certain results and kind of keep those as standalone libraries. The general culture in Lean is you'll write these separate libraries, but the eventual goal is to upload them eventually to MathLib, the central repository of mathematics. And so it's a little bit more centralized and a little bit easier for you to get started as a mathematician.

But that's a yeah, that's a good question. Yeah? Yeah, another question. I have my mic. I can use my mic. Um so maybe this is a dumb question, but what do we get when we have an ecosystem of Noir libraries that are formally verified that we're not able to do without them? I know we've talked a little bit about like in the auditing context. It kind of touches there, but I'm just curious how you would answer that. Yeah. So I think I have a no in a couple sides, but I think the the the big thing that you can get out of it is Well, there's here's a here's a really good example. So say you want to implement some very tricky optimization

where you might have to use some unsafe code and do some constraints after the fact and you know it's going to make your Noir code run a lot faster, but you're not 100% sure that this doesn't have any bugs in it. Doesn't have any ways to exploit the code. If you can do this Noir implementation and then formally verify that it actually does satisfy the specification that you expected, then you're golden. You don't have to worry about any unexpected bugs modulo, you know, how the semantics or how the the extractor, you know, some there's some trust that you have to have. But I think it it makes you feel a lot more comfortable about the Noir code that you've written in the end. And if you're say like writing a banking app for example in Noir and you want to make sure that the

if I say I'm sending money to this address, then it actually really does go to that address, you can be a little bit more confident about how the Noir code is going to behave once you have these formal specifications specified and proved in in Lamp. Yeah. Any other questions? Okay. Um yeah, so so metaprogramming tactics in the SLs. Here's an a Lean example. Actually, we've already seen a Lean example. That Lamp stuff that I've written previously is a Lean example. But the general user experience when you use Lean is you're going to have some Lean code that you're writing on the left-hand side and you're going to have this thing called the info view on the right-hand side which tells you the tactic state. If you're familiar with like these two-column proofs from like high school geometry or like if you're really advanced like middle school

geometry um uh you'll see that kind of we're writing down the uh the step-by-step kind of proof over here on the left-hand side and on the right-hand side we see the state that we're in on the right. Um it's uh a little bit different because we have automation and we didn't have automation in in our middle school geometry class, but this is kind of the idea. And so here we're proving things about natural numbers and commutativity of addition. We can even prove things about uh like Lean objects and Lean theorems. Uh uh theorems about Lean objects. So here we're saying that if I take two lists and I uh append them, then the lengths add. So this is an expected property about length uh and appending and we actually have a theorem that literally says that this is

true in the Lean context. So kind of getting to your question and like what what this gives us is we can use Lamp in a number of different ways. We can have a reference implementation that we've implemented in Lean, and then prove that the extracted Noir code has an equivalence with this reference implementation. So, say this reference implementation has some proofs of correctness already about it, then we can now get automatically for free proofs of correctness of our Noir code. We can improve We can prove invariants of our Noir code, kind of like this this example that I had with the banking app, something that will never happen or something that will always happen given uh I run this Noir code with a particular precondition.

Um and then uh the other example I gave, we can prove equivalences of optimized Noir code with unoptimized Noir code and check the correctness. Um and we don't have to worry about uh unexpected bugs. And then uh finally, sort of this is a little bit more of a technical, but it's kind of like a nice idea. You can attach proofs to traits in in in Noir, so that you have traits that really ensure certain properties about our our trait uh our proofs that ensure certain properties about our trait. So, for example, if you implement like a hash function, you can prove that well, hash function's a bad example. Say you implement something about a sorted list or you have the trait about sorted

lists, you can enforce correctness of that in trait by attaching proofs to it in the LAMP side. The fact that, you know, the the underlying data is actually always sorted no matter what operations I enact on it. And then finally, kind of just how you should be using this is um you should I think a good idea is that you want to kind of implement the C you know, implement LAMP in your CI. So, if you change your Noir code, the proofs are going to break, but you'll have a chance to fix them, and this might give you a insight into how changing that Noir code might have introduced vulnerabilities that you weren't originally familiar with.

Okay, and so I'm just kind of like at At end where we go from here, there's a lot of bug fixes, developer experience, documentation, etc. that we still have to do. But, I think the big thing is that Lamp is generic enough that we expect that this should be applicable to many different kinds of ZK languages. So far it's specific to Noir, but the core logic, the core semantics is very general. It's just separation logic with omni semantics. Any ZK language which has unsafe blocks should be app It should be applicable to that domain. And we're hoping that eventually we'll make make it applicable to to that domain.

Okay. And so, yeah, definitely try out Lamp today. Here's the GitHub repo for the Lamp repository. Um open issues, play around, have a good time. And then, uh now let's get a little bit into the interactive demo um in the last maybe like 10 minutes that I have. So, before I do that, does anyone have any questions? Oh. So, this probably also happened to you guys. Uh but, yeah. So, just restart your code space.

Yeah? Uh one minor question. Um since uh Lamp will not touch any ACIR code at all, do you see any possibility of any form of uh improvement there? Would there be any gain from having integration there at all? So, I think it would be helpful to have So, I think That's a good question. I think what would end up having to happen is you want to have a verified compiler that turns Noir code into a you know, So, the compiler turns Noir code into ACIR. You would want to have a verified compiler that ensures that these kinds of things, you know, if there's optimizations or something, don't break. That's a big undertaking, and I And I think there is gain there,

but I think from the context of like a Noir developer, like I, you know, I If I am the From my From my perspective, if I am just going to be writing Noir code, I don't want to worry about the Noir compiler. You know, maybe it's up to Aztec to worry about that formal verification. But, you know, if I'm writing my library and I want other people to use my library, I want them to be able to use my library together with the proofs that I've written to ensure that when they're using my functions, you know, they're they're they're acting the way they expect them to. So, I think that is definitely something that's worthwhile, but I think the the the idea of Lamp is that it shouldn't be a tool to verify Noir itself. It should be a

tool that Noir users use to verify their own code. Yeah. That's a good question, though. Uh any other questions? Okay. So, yeah, so if you enter in the code space, you should see um you should see like a little bit of a quick start guide um and a disclaimer at the end that there are bugs and you will run into bugs. But, if you do run into the bugs, let us know or open issues on GitHub and we will fix them as fast as we can. But, uh I want to start with this this simple example here. Um I've just kind of written this function out by hand. I said you one generally does not write this DSL by hand, but again, it's not too hard. But, you see here, you know, I I define an immutable function, etc.

etc. etc. Um and then I get into the proof. And so, here I've separated out the proof into the three component Oh, is this too small or can people see this? Good. Okay. So, so I've separated out the the the the statement of this proof into three components. I have my precondition here, I have my precondition here, which is empty, essentially saying that no matter what environment I'm running in, this should be true. If I call my function, then the output of the function should be equal to the input. This is actually not true. I just wanted to give you an example of like what happens if I try to prove something that's not true.

And so, I mentioned sort of like the use case or like the the feedback loop you have as a as a lamp or lean user is you're going to enter into these tactics blocks and you're going to sort of start giving it declaration or you're going to start giving it um commands and and it'll start executing proofs for you. And so here I'm in this tactics block and I'll execute the first command which is called enter deco. So I'm calling a function here and you'll see that if I enter the declaration, I've now entered into the body of that function and I have now sort of an unrolled version of what this function is really doing.

And the idea behind the steps tactic is it should be kind of stepping through the code one step at a time. So if I replace this with a one, you'll see I originally had like a let Z be something. Now that has turned into something about the state that I'm in. So this is now this this right here is our tactics state or our our proof state and we have our precondition here. We have our postcondition here. The postcondition is the same postcondition that I have in the declaration of the function.

And this is the code that we're sort of stepping through. And as I step through this code one oops one uh uh step at a time, you'll see that the tactic just kind of like you know, start stepping through. I can do it like 10 times or something like that. Um or or I can just say steps all the way through and it'll get to the final state which is presumably, you know, we have all of these uh hypotheses and then we're trying to prove the end result which is that X is equal to the input.

And it's definitely not true that it's equal to the input because I've multiplied Z by two and I've added five. Um so the end result should not be equal to the output but that that's you know, if I do like a simp short for simplify um Okay, now I need to start typing. A simp all it's not going to work, but if I change the hypothesis from input to two times input plus five.

Um Okay, maybe I have to do a subst fires. See, that proofs can get a little hairy sometimes. Okay, it's not going to work. This was a bad example. Um, you may have to be a little bit more tricky with the proof. But the idea, I mean, this was really just here to show you that steps should sort of turn you know, at this point at the very end of this proof, we're not doing anything about Noir. We're just reasoning about the actual code itself. Um, and I may have actually even written this wrong, but the idea is that we want to in the very end just prove some basic thing about about Lean. A better example, which I have

worked out ahead of time is is the Fibonacci example. So um we're in ZK. I feel like all the ZK VMs or whatever use Fibonacci as a benchmark. Let's use Fibonacci as a benchmark for for how to verify things. So, here you see a very natural definition of the Fibonacci function. This is just straight-up Lean code. Um, here I do a little bit of a modification to it so that I can take not natural numbers as inputs, but you in 32s as inputs. That's just because that's what Noir is expecting.

But um, and here I I here's just like a slightly extra lemma that I have to prove. So, it's it's clear that this has the inductive property about Fibonacci that fib of n plus two is fib of n plus one plus fib of n, but it's not 100% clear that this is true about here as well. Um, so I have to prove like an extra theorem. So this everything above this line is just lean stuff. But this here is Now, let's expand this out. This here is a proof that um an extracted version of the Fibonacci.

So I Oh god. Sorry. Not These are not vim bindings. Um Here I I have a an example of the Fibonacci function extracted. I actually even have the Fibonacci Noir function right here. So here's Fibonacci function defined as a loop. Um you know, you're just looping through n times, etc. Just kind of how you expect to calculate Fibonacci. I've run the lamp um CLI function and I get the Fibonacci extracted right here.

It looks very similar to the to the original Noir code with the the loop kind of right here with the mutable A and B defined at the very beginning. And here I prove that this extracted Fibonacci uh function here um if I call it on n should be equal to fib of n, you know, fib of n as as you would expect. And the proof is is a little longer just because it's more complicated, but it's mirrors the same sort of structure as the proof that we were just doing earlier. So you enter the declaration, you have your function body here.

You step through it up until certain point in steps is going to terminate up until the point where it's like, I don't know what to do next. Here, I don't know what to do next happens to be when I get to this loop. And now I have to specify what's happening in the loop. And what's happening in the loop is that at any given step of the loop, A if you recall A Oh no. Uh if you recall A is defined to be zero at the very beginning and B is defined to be one at the very beginning. A should be uh uh a reference pointing to the value fib PI, and B should be a reference to the value pointing at fib PI plus one. So, I've sort of said, "Okay, at any given point in the loop, this is what's going to be happening."

And now I enter into the the the theorem about the loop. And now I'm in the loop body here, you can see this is basically just what the what's happening in the loop body. I do steps, etc., etc. And then the key, this is all leanisms. If you're familiar with lean, this should look familiar. If you're not, then this is going to be a little bit of a magical incantations. But then oops. And then at the end here, it kind of boils down to uh proving that fib of PI plus one equal plus fib of PI is equal to um fib of I plus one plus one, which is kind of what you would expect. And and this is all just again what you expect.

Um again, you get to the end, you have to do another steps and subst vars, and then reffle at the end should end the close the proof. So, so this is an example of of fib, and I think a nice benchmark or a nice example of what this benchmark is showing us is that the size of the proof is is what? It's uh something like 20 lines. So, proving that this Fibonacci function has a certain property took about 20 lines given the the length of the function is about 20, right? So, two to one of of the length of the proofs to the length of the function declaration, the overhead of writing the proof is there, but it's not un unreasonable.

Um and then there's uh other examples. So, here's an example of unconstrained function. So, here I have a new new uh variable that I've defined to be unsafe equal to three. And then or another example is I've let Y equal to uh new where this is an unconstrained function and if I look at what this extracts to, we are uh just completely unsure of of what the value of of this thing is. It's unsafe, so the best that we can say is this is like a fresh value and this is what it is.

Um and uh yeah, there's a there's a few other examples. Here's an example of how generics works. So, here I've just defined some generics and and I have some some properties about the the function. So, I define a trait implementation, etc. etc. Um and how this is extracted is I have some uh the Noir structure is is extracted over here. So, I have the generics pair structure. It's extracted with the generics still generic. And then I can specify something. So, um here is an example of uh how the proofs can compose with each other. So, I had the the two functions. Let me actually pull that up again.

So, I have the two functions that I've defined about pair or like the two two associated functions make and make diag. And this function these equals should basically prove that the the result of make with AA and make diag should result to true. So, in the end I should hope that this function equals true. And if I go back to my theorems here, I have a small auxiliary ramp lemma about make um saying that if I calculate make, the output will just be sort of like a pair of AB. Here's a a theorem that says if I take make uh diag, the output will be a pair AA.

And then this is a like a simple theorem um that explain that kind of goes into the fact that this is going to always be true. So, the output of this these equals function should always be true and you'll see here that the structure of the proof is uh pretty similar to how we've already done it before. So, we have an intro deckel. The body of the function is pretty wild. That's because I've set some things to false here. Actually, let's delete that. Um then we step through it. We have to enter blocks, call functions, enter blocks, call functions. Um there's a little bit of a bug that I noticed in preparing this example. So, uh we're peeking behind the curtain here with with these applies. This will get fixed.

Um but then in the end, we're trying to prove that essentially this X equals true given all of these hypotheses. It's a mess, but usually simp all just kind of like works and it does in this case. Um and if it doesn't, then we've sort of done something wrong and and we need to make the automation a little bit better. But this kind of gives you an idea of how how one can start proving things about Noir code um by using our extractor and then just generally writing these kinds of proofs pretty quickly. Um so, that is good. I I guess I ended a little bit later, but if anyone has other questions in the last couple minutes, then let me know.

Thank you for the talk. Um so, if I understand it correctly, the extracted part is the like automated part and the specs part is kind of what you use the extracted part, but also you manually define kind of some of the specifications of the program itself. Yeah. Um so, yeah, in that case then um the manually defining part kind of naively sounds like well, writing tests is for the programs themselves. Yeah. Yeah. Yeah. In that case, how do you see the difference being like writing tests is for a program versus doing the I guess formal verification specification of a program itself?

Yeah. So, like I said in the beginning, tests are like testing, formal verification, these all fall under formal methods. And testing is generally like a prerequisite to getting any code merged onto the GitHub, right? Like if you're not writing tests, you're not doing doing it right. Um So so that's like the minimum that you would want to have about your Noir code. Um writing a spec a formal specification is a little bit more of an ask and it's a little bit more, you know, it's a little bit more effort for the user, but it's probably worthwhile for the user to expend that effort because if this code is going to be used by millions of people and potentially have like large financial consequences

um for for errors in the code, then you would want that that to be to be correct. Um then the final step of like actually proving that specification holds for the Noir code that you've extracted is a fair amount of effort, but it could also be relatively worthwhile. Like writing the specification out might get you to think about your Noir code in a more like systematic way, but actually writing the proofs out is going to give you that peace of mind that that you're 100% certain. So, you know, tests, depending on how you write them, unit tests will test like a bunch of different examples. If you do proper base property-based testing, that's going to maybe find a little bit more bugs, but if you have a fully verified Noir

code, then modulo some trust assumptions, you could be 100% certain that it's behaving the way you expect. So since that helps, um extending to that a bit, um so you also mentioned uh uh one of the value props of like targeting Noir is that Noir has a very early ecosystem. So libraries can start, I guess, for formal verifying their libraries and grow into kind of a full ecosystem of verified libraries to begin with. Mhm. Um how do you see that tying being beneficial at the early stage versus like a later stage language as ecosystem can't people just extract things from a even a late stage library and simply start formalizing

that at the later stage versus at the early stage. So So, I think a good analogy is is something that happened in Python. Um Python, you know, just completely typeless, uh dynamically typed, but at some point they introduced type hints, right? And it was really great. All the new libraries started using type hints, but if you start hooking into old libraries that don't use type hints and that or that haven't been updated to use type hints, you have kind of like a little bit of an assumption of trust in there that's built in on hey, these types are not going to be the wrong ones at any given stage. Like this might manifest to you with these, you know,

orange squigglies saying type any cannot be type whatever and you have to like do a lot of stuff with Pyright to like you know, but but this is this similar to to like uh TypeScript as well where where if you're hooking into JavaScript code, you're going to have all these stuffs with with issues with types. And you don't want to, you know, say I'm writing my library, I don't want to have to go into this other person's library and take all the effort to write the type hints for their library or in the context of Noir, I don't want to go into this person's library and write all the proofs about their functions. I might I might not even know how their stuff is implemented. Maybe their their forward-facing user API is not something that I'm very familiar with. And unless

I'm an expert in how they've implemented their code, I may not even know how to write their proofs. And so, it is like a big ask to go back to the very beginning for a well-established language to verify all of the code from the very beginning. But Noir is in this unique position where it's a very early language, and if you start verifying things from the very beginning, and if there's a tool like this that hopefully makes it easier for users, you can get a lot of leeway out of that. And you know, it's it's going to be a group effort, but it's not going to be an unreasonable amount of work for any individual to do.

So, it's distributed a little bit better. Yeah, I don't know if you guys were able to get into the code space, but hopefully it worked for you guys. Maybe you can play around, have a good time. So, I have some lower priority questions. Just generally about the market support for this product. Sure. Um do you see LLMs being an issue about being able to jump in to make, you know, semi uh automation improvements in the form of a formal verification? I think I think so, yeah. So, so if you ask mathematicians doing lean things just in general, they're very excited about using LLMs and AI and all that to to make their proofs a lot fast

not make writing their proofs a lot faster. Um we haven't implemented any like AI tactics or anything. Um there are examples out there in the math context where if we want to get inspiration, we could maybe see what they're doing and see how they're doing it. I see, you know, like I like I said kind of in some of these examples, these proofs should be automated in a way. And we've done some of the automation, but it's just not, you know, you can't quite get all the way there.

There's too many like edge cases and you know, maybe we can do about 70% of it with our automation, maybe AI can bring it to like 90%. I think there's always going to be like a 10% or maybe a 5% amount of like edge cases that no one, unless you're really uh knowledgeable about the code base, is going to be able to to automate away. Um but I think yeah, I think it's not unreasonable to expect that AI tactics should be able to um to to help. And the last thing I'll say is there is all of this effort for AI tactics in the math side and these tactics that they're writing are general purpose enough that because there's this robust lean ecosystem, we can hook right into it.

And maybe we don't even have to write our own AI tactics. Maybe those AI tactics that are written for the math context are generally applicable for all contexts and we could just start calling those kinds of things. Actually, a lot of the tactics you see here are not specific to Noir. They're just they're just general tactics that has have been written in mathlib to reason about math code and just so happens that they're, you know, useful for all contexts that have to do with lean proving. Well, uh secondary to that, uh do you see this as becoming the uh next stage of a um audit process, like a guaranteed requirement that any Noir code must have some formal verification with 100% you know, what I'm saying?

Yeah, I mean I mean I I I don't think there's ever going to be like there's no governing body, right? That that can like fiat um you know, force everyone to start verifying their code. I think the Noir ecosystem would be better if it did have it and I think it's kind of like our job to make that easier for people to use and it's not as much of a heavy lift for them to start doing. Um but I think yeah, there's there's a there's a value add to having Noir code being verified and I think it's not unreasonable to expect that with a little bit extra effort people will start doing it.

Excellent. Cool. Any other questions? All right. Thanks. All right. Thanks.