Shedding Light on Noir with Lampe

Transcript

All right. So, yeah. Hey everyone. It's a very cameraal meeting. Um, my name is Martin. I'm the CEO at Trailabs and I will be talking about Clump, uh, which is a tool we've been building to formally verify new code. uh and I will sort of tell you more about like the vision behind it, why I think it matters, how it works, um what the goals are and so on. So first of all um the first point I need to make is that formal verification is necessary in this in this industry. Uh are you guys familiar with uh with formal verification? Like we just don't Okay, of course. Um cool. So yeah um very quickly we are building protocols that

are securing billions of dollars. uh we are also building protocols that work with some very sensitive data about our users, right? So like you have uh identity use cases where we are uh scanning passports, where we are scanning documents, scanning eyeballs. Um so yeah, very sensitive data uh billions of dollars of of value locked. Um and we're doing doing all of that with extremely open access to everything that we're building. Um, so, uh, if you deploy something onchain, anyone can just come in and throw any garbage at at your circuits, any garbage at your contracts, um, and see what happens, right? Um, and the environment is extremely adversarial. Um, essentially because

it's so open and because, um, there the stakes are so huge, um, you've got North Koreans testing your systems all the time. Um but to like this is this is not specific to ZK. Um what is specific to ZK is also that the environment that we are using to build those applications is extremely unintuitive. Right? So we have field arithmetic. So you you you got your developers that are used to um you know like using tools complement to represent numbers. You come in oh it's fields now right? Um they cannot easily be compared. They overflow in a very weird place. Um it's a weird system. And we have unconstrained functions uh which means half of our code is only used for

weakness generation and it's not actually used as a part of the of the constraint system. Um which is to say it's not actually checked uh cryptographically in any way shape or form. Um it's whenever you're writing an unconstrained function you should think about it as I'm writing an example of how this value could be computed and not this is how this value actually is being computed. Um so this makes it even more difficult. And one more subtle point that I I don't think gets brought up enough is that we can't even see what is going on. Um if you are writing a smart contract on for solidity for example you can always go to ether scan you can see what's been called how it affects the

contract state what's happening right like if you are getting attacked if you are getting funds drained you actually know that you are getting funds drained. Um but for example in the case of of Aztec which is the main environment for noir we know that some private function uh evolved the private state somehow. What happened? I don't know. I know it's been correct according to the definition given in the noir file. If that definition is broken uh funds could be drained and you will never even know that this is happening. So with that in mind, I think that formal verification is uh a necessity here. But at the same time, it's very very difficult to to pull off. Um first of all, even even specifying the

properties and specifying the invariance of programs is is difficult. If you ask like your random developer that you that you meet that is writing new code, if you ask them about like the invariance, there there are chances that they don't even know what an invariant is. Um, and even if they know what an invariant is, how do you get them to actually be good at specifying those invariants? Um, and then formally proving that the invariant that you've that you've satisfi that you've specified is correct uh is a whole other kind of worms also very difficult. Um, and the barrier to to to entry is also very very high, right? Like you have to usually you have to learn some new tooling or some new language, be it lean, be it cog, um, currently called rock. Um or if you're

doing this with SMT, you don't necessarily need to learn a new language, but then you need to learn how to negotiate with the SMT solver such that it actually achieves anything. Uh which is also a very non-trivial amount of of knowledge and experience to ingest. Um and you also often need to understand the theory of of language semantics. you need to understand what's going on uh with your uh with how the language is is modeled. So all of that uh oh one more thing um the way this is usually done also makes the process very repetitive. Um so the way the way this is usually approached is we extract from some very low-level representation uh usually with like all

functions in line. It may be uh it may even be just the the pure constraint system. then you can show that okay maybe it's uniquely constrained but you cannot tell anything about the uh the nature of the weakness and the other thing is that if you for example if you have a library um and you do a a formal verification audit for one customer there is no easy way to translate that work over to another customer so those are some of the of the motivations of why lump is happening and why it looks the way it looks um and this is what I'd like to say like let's make it all easy, right? Uh lump exists.

Boom. It's easy. Now, um this is the truth. Um the truth is we are going to make it somewhat palatable. Um it's still not going to be easy. You still have to write lean uh or if we have chosen a different uh proof assistant, you would still have to learn and use that proof assistant. You still have to understand at least a bit the theory of of what's going on. Um but we're aiming to make it at least an investment that that can be made with uh with good conscience uh for a for a given protocol.

So yeah uh let's make it bearable. Um we bring together well established theory. We are trying to build tools that are somewhat user friendly and they do not assume that you have a PhD. Um if you do great um but it should be possible uh at least in principle for for someone that's that's new to this space uh to actually build something. Um we are working on custom automations that try to hide away as much of the complexity of the specific theory that we are using. Um so that you can get a model of your of your new code in lean um without any any extraneous computations that that support the the computation of of of new

program. I will show you specific examples of what that means uh later on. Um and one more thing is that again going back to the to the rep repetitiveness of this of this work. It takes a village to make this happen. Um so we are starting from the assumption that proofs should be composable. So if you are a library author uh in noir you should be able to uh publish your proofs uh your theorems your lemas and they should be reusable for uh the users of your library. So if I if you create a library for uh elliptic curve uh operations for example and then I create a library for uh for signatures and I use your library for elliptic curves um that library optimally would already come equipped with a set of lemas that say the library is doing its work

correctly uh I can then pull it into lean and say whenever I'm using the the newer function uh for example for point multiplication I can instead substitute it for a well-formed definition on the on the lean side of what the of the what the library is doing. Um and the claim here and sort of the ambitious goal uh is that we can gain enough momentum uh in this like very early stages of of noir um that the base libraries actually will be formally verified and that um in this ecosystem uniquely I think we can we can push towards like full formal verification of the core of the core libraries. uh we could make it a sort of like soft requirement like a community expectation that your libraries get

formally verified um that you share your lemas that that everything is is more correct right uh because again um this also goes to like supply supply chain uh attacks right like if I if I'm the author of elliptic elliptic curve uh multiplication library um and everyone else is using it what if there's an exploit in that that probably can propagate very easily to the entire program that uses that uses that library, right? And again, this won't even be detectable uh because everything is happening in on private state with private functions. Uh everything is so obuscated that that you cannot easily inspect what's happened. So yeah, uh LAMP is an attempt at solving this for for noir. Um and as part of that, we've

built an extractor that turns noir code into link code. Um and this is happening at the highest possible level essentially. So the the extracted link code, uh I will show you later. uh looks line by line exactly like the uh like the newer code that we've written. Uh you can actually uh yeah you can look at the definition side by side. They are very similar. We are using and abusing uh LIN's meta programming facilities to actually equip LIN with uh some syntactic sugars that look exactly like uh like noir.

uh we extract before monommorphization which means we also model uh new type system in lean u and again this is done so that you can uh reuse components uh as much as possible right like if you have a generic function if you have a function function that takes a generic type parameter you can prove things about the behavior of this function for all type parameters and then you can uh compose that with particular instantiations um and then we implement the semantics of noir and how we implement this those semantics uh I'm going to explain a bit uh a bit later because this is uh this is some heavy machinery like this is this brings together a lot of of uh the theory of of semantics of programming

languages and then we have some custom automations that make uh writing this all easier so that you can again uh you can just get a sort of semantic model without caring that much about how we actually model new the language how we model execution So, a bit about LIN. Uh, I'm sure most of you are already familiar with with what that is. Um, but it's a functional programming language first of all, uh, with Huskell like syntax. Uh, it's actually a better Huskell. Like, uh, if you are a Huskller, you would find lean a more pleasant version of what you already know. Um, but the type system is expressive enough to encode propositions, to encode logic. Uh, and it's user friendly enough to be

widely adopted. I think it's uh probably the the proof assistant that has the most traction right now. Uh it's not the most popular um but the derivative of popularity is the largest I would say. Um so there's a huge community of mathematicians uh that are building libraries of formalized mathematics. There's math lib um there's also the effort to to prove uh FMA's last theorem. Um so great mathematicians are are actually like this is probably the first time in history that ma mathematicians actually picked up uh a theorem improver seriously and are actually doing mathematics using a theorem improver um the ethereum foundation has an effort to to formalize uh zero knowledge cryptography um so you can google the

name arib and it will show up um and that's uh that's an effort to uh essentially uh formalize IOPS and uh sigma protocols things like that to make sure the cryptography is sound. So it's a different layer that that what we are talking about but it's also very useful. Um there's a wide array of of built-in tactics already. Uh so like there are solvers for ring arithmetic for linear arithmetic like inequalities. Um and some general general purpose like proof search uh tactics like simp and and ASOP and it's extensible through meta programming. Um and the meta programming is actually pleasant. So like if you come from the coke/rock world uh you will know that that meta programming is

not the most pleasant thing that you could be doing in that particular ecosystem right like you have to learn a completely separate language or you just have to write it in okamu um in lean you write the meta programming in lin itself um which is much more pleasant much more streamlined I would say um and also a great macro system that lets you do um things of uh okay I messed up the of the slides. Anyway, uh some examples of LIN, right? So like we have a uh we have a theorem statement of like hey addition is commutative. We have a basic proof by induction. Um this is a screenshot from Visual Studio Code. You will see that it gives you this interactive state of like those are the things that I already know. Those are the things that I still have to prove. Um and you proceed by

writing your uh your proof script until it completes. Um here's another example of doing the same with lists. Um and yeah uh going back to the to the power of of the of leans meta programming. So on the left hand side you have uh some definitions of uh like some new code um that we are using as a as a demo for this. Um this is a part of the of the implementation of the skyscraper hash function. Um and on the right hand side you can see the the extracted lean. Um and you will notice that it's it's very similar like like the the number of lines uh is almost the same. uh you can recognize the names and obviously like things like binary operators get uh they get their own proper uh proper names. Uh

you see that there are some additional like type annotations happening. Um but we do uh we do this extraction almost one by one so that when you when you are done with the extraction you can recognize your original noir program and that's easier for you to reason about because when you wrote the noir program you actually understood what it was doing right so this skips this step oh now I have to parse this new representation that is like mangled compiled and so on no it's it's it's very similar to what we've had okay so let's talk uh also briefly about the theory behind behind all of Um so first of all the the requirements or the the the boundaries that we are working within. So first of all newer is a touring complete language. Um

and this is a contentious statement so I put an asterisk on it. Um is noir a touring complete language? Uh my claim here is for all intents and purposes yes. Um the non-ouring completeness is very unstructured. uh kind of random kind of dependent on what the compiler in the current version can and cannot do. So if you are actually modeling the semantics of the language, it makes sense to assume that it is it is fully incomplete. Um and then as the compiler evolves, it gets better more programs start to compile. You are you are open to that, right? Um, no is I I would say that Noir is designed as a Turing as a Turing complete language,

but then the compiler sometimes fails to uh to actually compile some programs that that would use the Turing completeness. Um, which is not dissimilar to like normal programming, right? Like you could argue that no language is incomplete because uh you don't have an in an infinite amount of time to to run a program, right? Um, it supports mutable memory with unbounded lifetimes. So at the very beginning of your main function, you can create a mutable variable. You can take a reference to that variable and then you can pass it through the system happily.

Uh it will just exist for the for the entire program execution logically. Um of obviously like there is uh a poor man's version of garbage collection in noir but um in principle uh you can have uh unbounded lifetimes on on any any piece of on any mutable variable really like there isn't even an operator to to heap allocate something. It's just you have a mutable variable technically it's allocated on the heap already. Um and it's nondeterministic through unconstrained functions. Um so what that means is you have this special keyword in noir unconstrained uh which lets you write some function that is not being cryptographically checked. Um for the

purposes of the constraint system this is just a fresh fresh variable or a bunch of fresh variables. Um if they are not constrained properly then you might as well remove that code like it's not uh it's like it's not there uh for the purposes of the constraint system. And this is a source of of possible catastrophic bugs, right? Um, and this happens even uh it used to happen even with some standard library functions. Like for example, uh if you took a bit de composition of a field element, you weren't guaranteed that it was like the unique smallest uh bit de composition.

Um so you could get a bit string of the correct length uh such that when you recovered the the field element it would be the correct field element but the bit string actually denoted a number larger than the the maximum field element right um this was patched as far as I know so uh currently the the standard library makes makes sure to give you the unique smallest binary representation but it wasn't the case um so even this could could really bite you right like imagine if you use this to implement a comparison gadget so you de compose your numbers into bits and then you do your like binary comparison it's broken because the binary comparison uh because the binary representation uh is the bigger one, right? Um and by the way, it's a bug that happened. I think it happened in every single uh DSL I've

looked at. Um it's like the the easiest mistake to make is assuming that binary representations are easily unique. Um so all of that means uh we need some really really big guns from programming language theory to to model all of that. Um so let's talk about a few uh foundational ideas. First of all there is what we call big step semantics. So you have a programming language and in the uh and and you encode propositions of the form. If I'm starting from a given state, let's call it S1 and I run this program in this state where by state I mean for example all of the all of the the values that are being held in memory right now. Um when this uh when

this program executes uh it will terminate and it will end up in a state denoted as S2. Um and this composes nicely. So you can go through that except noir is not deterministic. Um so we need some extension to that and the extension we've chosen is called omnis semantics. uh it was introduced by Shero um and you rewrite the big steps the the big step judgment to be if I'm if I'm starting from some state all possible execution paths of this program will terminate in states that are describ described by some predicate so instead of a of a single state s2 I have a family of states uh described was a described by a by a predicate um and then that is usually a bit too

too difficult to work with normally. So we introduce uh what is known as horripples. Um so a horrible pq uh says that if the predicate p holds in the initial state and the the program e terminates normally I'm going to have q holding in the final state. So this is kind of how you reason about state updates uh and correct executions. And there's one more twist that we need in this in this entire story which is that we also need separation logic. Um because we are dealing with mutable memory. Uh hor triples are usually horrible for that. Um because in the pre pre and post conditions you have to talk about the entirety of of memory and this doesn't compose very well. So separation

logic restricts the language of the predicates P and Q such that they talk about sort of local views into the memory and they ensure that the rest of the memory could be anything and this gives us very good composibility because if I have one program that works on some piece of memory and another program that that holds on to on on a completely separate uh separation logic uh on a separate piece of memory. I can compose the two and say together they are they are like both both of these uh of these pred of of those judgments also hold.

So yeah uh let's look at some example proofs. Um here we have a uh we have a reference implementation of some function. Uh again this comes from the from the skyscraper example. Um and then we prove that it is uh that is equivalent to the version that's been extracted from nowhere. This is just a quick example. I will show you the actual like real code um soon. Um but I just want to uh draw your attention to the fact that the overhead that you get from from using lamp versus just using Berlin is quite minimal in this example.

So you can see that like the enter deu that comes from lampu. Uh steps and loop invariant those come from lamp. Um again we have steps here and that is all I think right. So the rest of this the rest of this proof script is actually being uh it is actually about the the core logic of the program right like you see that we have to we have to convince uh convince LIN uh that we are not overflowing the the U8 counter for example right like we have to we have to do a lot of stuff that is purely mathematical in nature um but the the overhead of using lamp itself is is quite minimal um which is which is the the very goal of this of this exercise

exercise. Okay, one last thing. Um what lump doesn't do for you. Um and again this is uh this is usually people get a lot of uh misconceptions about oh like you are you are building a formal verification framework. Cool. So does that mean I can just install it and my programs get secure automatically? Uh that that actually happens. U but yeah no not this time. So first of all lump doesn't verify the implementation of noir. We are not talking about what the what the compiler does. We are not talking about the the constraints that are being generated. Uh we are not talking about the cryptography behind noir. Uh none of that is being checked by lamp. Uh hopefully it will be checked

by some other efforts in the in the future. But uh we are just providing means of talking about the surface level programs in not how they are compiled. Um again does not automate the job of verification away. you still have to write your specifications and you still have to use lean to make sure that those uh that those specifications are correct and it does not reason about uh unconstrained code. Um again that's that's by design. Um because from the from the standpoint of of what is actually being cryptographically checked the unconstrained code doesn't matter.

It it could not be there um and the constraint system would be would be exactly the same. So we specifically remove the unconstrained parts. uh we replace it uh with a special operator called fresh that just gives you an unconstrained variable that could in principle take any value at all. Right? And then you talk use omnis semantics to say that no matter what the value of this of this variable is the program is going to behave correctly. And the typical workflow um or the the kinds of things that that you can do with with lump is uh first of all you can have a reference implementation of some cryptographic primitive uh or some piece of your application and you can prove that what you've done in noir is equivalent to that to that

implementation. Uh this is particularly important because uh in noir you are often uh optimizing by moving code into unconstrained blocks. Um so you are not always uh coding directly but sometimes you you you want to optimize something so you put your code in unconstrained and then you added a minimal number of constraints uh that will make it fly. Uh which is a smart solution often. Um but that smartness comes with a price of now you have to show that this is actually a a correct implementation of what of what you said it was. Um you can talk about invariance. So you can talk about things that are possible impossible. Um this is particularly useful if you are writing Aztec contracts right you could say that uh for example like the I don't know the

size of the pool never drops below zero or things like that right um again this this comes back to the to the first uh step and the last part is is a bit subtle but it comes back to the composability of it all um so you could rewrite your traits to add some required laws to um and then you say and then you know that oh if my trade implementation satisfies the law that I impose on it then some other function using that trait is going to be correct. Um so again composability all the way down and then you put it all on CI um so that if you change anything you know uh because the LIN stops compiling uh because the extracted version changed um so yeah you

are you are always secure like that so it's not like an auditing process where you go to an auditor you pay them an exuberant amount of money they give you a neat PDF then you change something and the PDF is uh essentially garbage at this point right um with this like this is actually maintainable this something that you actually put on your CI and you work with that. Um, and where do we go from here? First of all, obviously bug fixes, developer experience, more dogs. Uh, we are starting the formal verification of the standard library right now. Um, so there you will have like your first piece of composibility whenever you write an application that only depends on standard library. you are free to uh to use those lemas that we will provide as free write rule for

your for your own programs and then getting your library verified like if you are a if you are a new uh developer uh if you provide some sort of lower level libraries particularly like at this stage of of of the of maturity in the newir ecosystem uh we are getting a lot of foundational libraries being built um this is a great time to start getting them formally verified so that we can we can build the a very secure basis for the entirety of the of the ecosystem and then we can as as it evolves uh it actually has a chance to to be the most secure ZK ecosystem uh in existence.

Um so yeah, here's a link to to the repository. Um uh and I'm going to briefly uh show you the the actual code of like uh this is the wrong window. This is the right window. Right. So yeah. Um this is the noir. Um this is a maybe this this is a bit messy for now. Um what this does is it uh implements the the skyscraper hash function. Um and then it uses it to verify a miracle proof.

Um and there's a few things I want to draw your attention to. Um first of all like this is uh this is based on a trait called binary hasher. Um that's just an alias for a two argument function that takes two field elements two elements and returns an element of any type uh because this is generic. Um then we have an implementation that is uh pretty much just how you would implement skyscraper uh straight from the paper um except you have some hacks right um because you always do right. So uh for example when you are converting to the uh when you're converting to the uh to the beats representation you are like doing

this custom for some reason. Um the reason is to just show off uh how uh how lamp works. Um so yeah this is where we go with skyscraper. Then we have the strct skyscraper and we implement a binary hasher of field elements for the skyscraper uh thing. And then we have an uh mercury 3D cover procedure uh that takes uh an index uh represented as a already in binary. Um it takes the uh the proof and it takes the the item that is claimed to be in the leaf of the Merkel tree and then it does what you would do if you were to uh to recover a Merkel proof.

Um we also have a weird assert equality function. The weirdest arctic quality function is just to show off how we work with unconstrained functions. Um so we uh we have this unconstrained function that just returns its first element. Um and then we implement equality by getting that uh getting that that weakness element which is unsafe unconstrained. Uh and then we do this sort of transitive version of equality assert. Um again this is just as of an example like you wouldn't normally do that. Um and then we have the main function which uh calculates a uh like use the the uses the the mercury tree recover uh procedure and it uses the weird assert equality to make sure that

the root past uh is actually equal to the one recovered from the root. Right? So like from the secret perspective it's it's uh rather uh unexciting. Let's look at the at the extract. So the extracted version again very similar to to what we've just went through right like we have the same functions in the same order. Um if you focus on any one of them specifically you could see that okay like this is uh this is the same up to some reorderings things like that. Um we have our implementation again. We have this uh this magic syntax and our and and our trait input um that outputs an object that represents a trait

implementation. Um and then we construct this like environment object that contains all of our definitions. So how do we then work with this? We have the spec file. Um and first of all you can see that for uh for some of these uh we just do theorems that are like rewrites. So we have the uh this this is this is uh our hor triple uh the LP is the prime number that we are using because no new can use different uh difference functions. Uh the environment is what we've just defined right so it's it's an object that holds all of the all of the functions that are defined in the current scope. Um this is the expression right and the expression is a call to

the sign zero uh function with no generic parameters and the input parameter for any choice of the input parameter as you can see here. Um and the post condition is that the output is always going to be the value of the input uh modulo. Um and again when we start this uh we get this this sort of this sort of goal. uh we call the enter the cool tactic which enters the declaration um and we get this proof obligation right so we have the the same goal um but the expression changed um and then we run our steps tactic which is uh sort of the dummy exeutor like it's

going to take the obvious steps for you so you don't have to like uh actually compose the proof uh manually so after the steps tactic essentially everything everything about uh about noir is gone. Right? So we started from this and then we use the steps tactic which is again like an inter like a symbolic interpreter almost for noir um and we end up with something that is purely about lean right and as proof of that we use the built-in tactic called simple uh which will just like search the immense library of of uh theorems that that LIN provides. Um it's going to find one and apply it and it does right goals accomplished. We're done. Goodbye. Um this is this is kind of the the most

barebones version of it. Uh and most of the file is is spent doing things like that. Um where we just provide rewrite rules where we say whenever you call this uh noir function this actually corresponds to this uh to this other uh lean function. Um and of course it gets more uh more involved but I again I would like to draw your attention to the fact that most of this has nothing to do with with noir right again loop in that's ours um that that's our tactic tactic steps is our tactic and that is pretty much all like in this in this entire block the rest of the rest of it is actually spent convincingly that what you've done is is correct. So the the footprint of of

using lamp is is pretty minimal. Uh which I'm very happy with because it was one of the of the design goals. Um okay. So one one last thing that I wanted to show you other than the semantic rewrites is uh the main theorem that we can prove. Um and the main theorem here uh shows the the power of of using uh of using a proof assistant for this kind of work. Um because we can actually talk about the the semantics of this. If you remember the main function uh it took a Merkel proof, it recovered the root from the Merkel proof. It took a three- route, it asserted that the two that the two are equal. Um and that's what it did, right? Um but intuitively what we mean by this operation is that we are

actually checking that this element is in the tree at the given index. Um and if we are using something as powerful as lean or any other proof assistant really uh we can actually say that under the assumption that the uh that the skyscraper function is uh is collision resistant um and if the root comes from a real mercury tree I can actually prove this triple I can say that with an empty precondition so like I don't need to know anything else um if I call the main function again with no generic parameters and some normal parameters um the the the root of an actual Merkel tree uh the proof which is whatever uh the item and the index I can say with certainty that if this function passed I

know that the item is a member of this tree and again the the Merkel tree structure this is defined purely in lean it has like its own theory of how it's constructed how it works and so on um but the the the thing I want to draw your attention to is I can actually say about something about the meaning of my program it's not just what it did but also what it means for us. Right? So it's not just that it recovered a miracle proof that that was just means to achieve something else and the something else was to assertain that uh some item is in the mercle tree. Um and yeah uh I think that is that is all I wanted to show you. Um if you are if you have any questions or comments I would

be happy to talk. I have a few questions when you want to go first. >> Okay. So there you're using that the hash functions resistance are your modeling as like injected? >> Yes. >> So essentially because otherwise you you could just prove that like this hash that you know one per image like >> yes >> yeah. So that's like assuming like you wouldn't rever >> Yes. Uh to say it even more strongly like that's that's uh blatantly false.

uh right like no no no hash function is actually injective and uh it's something that like I I still haven't gotten around to how to actually model this properly. >> Um it's it's very annoying right like one idea I have is like maybe we change the post condition to something like either the item is in the tree or or I can actually construct and show you constructively a but it's it gets very weird >> uh very quickly. Of course, that's a safe assumption to make. I think it's quite standard, but then like so I'm not sure it's an argument, but then like they their thesis like oh what if you could like zk proof uh like a formal proof of something and then like that that type of assumption would be annoying because then what if someone goes and decides like the zikk proof or

the formal proof derived by counting argument that like the hash is not actually prove anything. So it's kind of annoying but okay. So >> second question is well I forgot the second question. struggle to the third. So third question is like so I I just asked him this about him uh because like they have the of noir thing but then like they're doing after monor monomorphization. So the question I have is like on noir >> you're going from a society right? >> Okay. Okay.

>> Yeah. So noir has this behavior where it will first evaluate the comp time blocks before instantiating the type parameters. So you couldn't for example and I think like since you guys modeled this at a high level I think maybe have stumbled into this. Uh so so macros get resolved before type checking also. >> Um so this is so this is already macro expanded >> but not monomorphized. >> Okay fair. >> It's it's a very lucky spot in the in the entire pipeline.

>> I see. Yeah. No because I mean I think that's a realistic by them and like they have to explain that to me yet. So just think your model is a good no but okay. Uh >> wait how how else would you do it? >> Sorry. >> How else would you do it? uh I think in Rust it got first the type parameters get instantiated and then evaluated content blocks because you can for example you can define an array with size equal to a parameter in a content block I'm quite sure so like if you have a type parameter which is like a constant view in >> you can't use that con in a content block because a content block got evaluated for

>> I see >> so you can't like define a consider array block. >> Yeah, that Yeah. >> Yeah. >> Okay. I'm just wondering about it. >> Not something that's beaten us. >> Um, >> cool. Anyone else? >> Yeah. Seems very long proof, but you have an estimate of how long this file >> like to compile it. >> No, no. to to wipe your books or >> Oh. Oh, it took like I don't know like three or four days to get it all done.

>> Uh it's it's not horrible, right? Like it's it's a significant investment obviously. Um um also like that three or four days was mostly due to bugs in the uh in the system like in in tactics in particular, right? Uh because this was like the first serious thing uh we've we've done with the system. >> So there's there was a lot of bug fixing back and forth. Yeah. Um again like I would say the the investment like it's there right which is which is why I said like we are not making it easy we are making it somewhat palatable. Um you still have to invest time and and effort into doing this but I think at this point the the investment is economically justified which I would call a success >> and so what's your hope um with this

like now obviously the system is very young >> and this is very helpful because this doesn't exist in another ecosystem I've heard of. >> Yeah. >> And so what does this mean for the landscape of like new projects that are about to come in so far of like the security aspect compared to other chains? >> You see the whole zik stuff, but this is like the level above. >> Yeah. So so I uh I mentioned it before, but I I think you you came in like halfway through. Um I really hope that we can uh we can build the an entire ecosystem of of verified newer libraries uh based on top of this because like the way the the way this is structured is um if you create some lemas some rewrite rules for your library then I as a user of your library can import those lemas

as well um and I can use them as well anything. >> Yeah. Exactly. Exactly. So it composes the same way like as a library would. Uh which means yeah um as as you said this is the first time uh like this is the first ecosystem that that that we can actually achieve this um we could have an entire ecosystem of of formally verified. >> Do you think this is going to change? used to be like put it in his own because many other protocols they say we've been audited like three or four times and then they sort of grave >> haven't done another audit and then that's when the hack happens whereas here I feel like you would be able to not prove at each step of the way that you know it doesn't >> absolutely I imagine the the the interaction with auditors uh changing

into auditors auditing the invariance that you've that you've proven right um because again formal verification is not a magic bullet Um so like if if you're writing this specification you can still do it in a very stupid way. Um so someone should take a look and say yes like those theorems actually say what you think they are saying. Um but yeah the the auditors would optimally not have to look at the at the actual source code. uh which makes it much more resilient to to change as well, right? Like if if if I have my protocol audited currently uh and I come up with a brilliant optimization, I have I have this incentive to not actually update my protocol uh because I would have to pay the auditors again. Um whereas with this if I have auditors looking at

my at my theorem statements and they say yes like if those theorems are satisfied then this protocol like we we understand that this protocol is actually secure given those properties are satisfied. Then if I come up with a brilliant optimization, I just need to redo the proofs myself. Um the signature from the from the auditor is still valid, right? Because I haven't changed the properties of the protocol. It and I have provably not changed them. Like I have actual uh actual thing on my CI saying that like this this property is still satisfied. >> You can finally prove that the difference between a need and a feature.

>> Yeah. Yeah. I think that's really cool. >> Yeah. Exactly.