The meeting is being recorded. Thank you. Well, this is the second RAS4Linux mentorship series session. Today we are going to talk about code documentation and tests. Again, thank you everyone for coming and thank you, Soa, for inviting me. First of all, in the previous session, I will not go through that. But I will try to be quick with a recap of a couple of concepts that you need to know in order to follow these presentations. But don't worry if there is no need to have seen the other presentation. So let's start with a recap. First of all, RAS in the kernel, the one of the main goals of RAS in the kernel is to be able to write kernel modules. Like drivers in only safe code or as much safe code as possible. In order to do that, we need to write safe abstractions, the ones that you see in the middle of the slide. And these safe abstractions wrap CEPAs. The modules that are meant to be written in as much safe code as possible are forbidden to access directly the CEPAs or at least as a code that we have. Currently we have some exceptions, but we want to remove them in the future. With that, a quick review of what is a safe and unsafe function. There are the unsafe key worry in RAS. This is sometimes a bit confusing for newcomers. So here I have the definition from the other talk. But basically, a safe function means that there is no defined behavior. When you call that function, there is no way you can trigger it if I make it here. That also means, or a way to say it, is that there are no safety preconditions around to call that function. And safe function means the opposite, basically one that is not safe. And we prefixed that with the unsafe key. That means that it has safety preconditions. We will see an example of this during the talk. So this is just a reminder. Then we also have another similar concept, but it's not exactly the same, which is safe and unsafe for code. And safe code means code that goes into an unsafe block, basically in RAS. You can think about it as a place where you may have an defined behavior. You have to justify why you don't have an defined behavior. That language is like a superset of the safe one. It means that it has access to basically everything that you can do in RAS. And on contrast, or by contrast, the safe code is a code that is not in one of those unsafe blocks and doesn't have access to all operations. It's a subset of the levels. And that's basically it. I have used in this couple of slides and you will see it in the next ones as we both let talk. You will see these colors. I use these colors to try to emphasize or to try to clarify the difference between safe and safe for functions and safe and safe for code. There is also safe, sorry, unsafe for trades, et cetera, but we are going to hear talk about functions and code. So one thing I want to make clear because I noticed that sometimes people ask, in the kernel, we are using a dialect, if you will, of the RAS language, which is this deny lint, is the unsafe operation and unsafe function. And this means basically what you see here. You see in the top part of the slide, what is the default, basically? Consider or imagine that this g function that we have, we are calling in the f function, imagine that is unsafe or is an operation that is unsafe to code, right? For example, think about calling a c function or accessing a data reference in a pointer, et cetera. In my default, if you have in RAS a function that is unsafe, the f that you see there in red, the unsafe red, that means the body of the function is implicitly unsafe as well. So it's like it had an orange unsafe block, right? While in the kernel, what we are doing is we use this lint, which basically changes the language in a way that basically that implicit block, the implicit orange unsafe block is not anymore there. So just to, I mentioned it because I have seen that people were watching the talk then asked or was confused because there was all these unsafe blocks that in the default, if you will, version of RAS, they are not needed. And just to let you know, it's not that we want to use this just because there is a reason you will see why during the talk, you will understand perhaps why this is important. And this may become in a future RAS edition. Maybe, maybe not. We basically agree with the idea of making it the default. What is now the dialect, making it the default. So basically requiring this answer. So with that, with those three things out of the way, we can go to the first block of the presentation. There is one question in the question and answer. Is unsafe a standard keyword of RAS? I think maybe that's answering before you get into the presentation. Thank you, thank you. I was not, yeah, I had divided the presentation in a few sections, I will try to pause, but if not, please interact with me. You can ask questions if you will. Unsafe is a standard keyword of RAS, yes. It's a standard keyword. So in the previous slide, let me clarify that. So what we hear unsafe, this keyword unsafe is the same. I use two colors, that is of course, these colors are not in the code, it's just to clarify and the keyword is for sure standard and you have to use it in RAS. Not all the time, I don't want to say all the time because if you are writing, for example, a normal program or a driver that doesn't need unsafe code, you will not see that keyword. But, I mean, as soon as you have to reach for something that requires it, you need to write it. So with that, we are going to see a series of examples from both from the kernel and also like trivial, if you will, examples to explain a couple of things during the talk, how to document a function. And the first one, I will start with this C function. I write it in C. In the kernel, we don't use I-62, we use S-62 or int or something else. But just to make it closer to C, I'm using I-52 here. So we want to port this function into RAS. Of course, in the C side of the kernel, you should also be documented the function, right? But sometimes things are either not documented or it's not, you will see that there are some parts of some things in the RAS side that you have to really document because otherwise all this work that we are doing to try to provide the sound of sort of safe APIs wouldn't work as well. So let's take this function which basically the reference is avoided, it's a trivial function, right? And in RAS, initially you could say, okay, I could write this, right? There is for those of you that don't know RAS, pub means public. So basically in the C case, because we have not used static. So this function has external linkage. In RAS, more or less the same, you could say it's pub. Okay, there are some differences but I will not get into that. Basically what I want to show is that this function may be called my orders external to your model, to your greatest. So the load function has to read takes a parameter which is P, which is a pointer. This is the way of writing a pointer in RAS and returns the IE32. And the reference in our raw pointer in RAS is done with a star or a STD score and how you pronounce it, you say it like this. We don't write return, return in RAS because the last, you could write it but we don't write it. So it's a dramatic to write for the last expression in a block is the return of the block. So this function returns the result of that expression. So now the first thing is in RAS for instance, in the kernel for RAS code, we are requiring that all the public items, an item in RAS is a functional type modules, et cetera. So all the public items or all the public functions, they need to be documented. They must be documented. In fact, we have a link from the compiler that this is not the case, you will get a warning which we consider an error basis in the CI, et cetera. So we have to document it. So we do that here in this slide. We are not taking function with these three slashes. If you know a bit of, as you've seen also in C, you have seen the way of document with two slashes or yes. And in RAS, those are used, two of them are used for normal comments. If you will, normal comments, like any implementation comment that you will write and we will see in this talk. But you use three, when you want to document the following item. So that documentation applies to the item that follows. This is the same as we do in the kernel in the kernel with Sphinx in the kernel or in Doxygen as well. It's very simple. Now, this code as written, if you have to work a bit with RAS, you know that this code actually does not compile. The reason is that the operation of the reference in a point, there is an unsafe one. It's an unsafe one, and that means it requires an unsafe block. And the compiler here tells you basically that it's not worried. So we have to write the unsafe block. Now, this is unsafe block, which means it's orange. I put it here in orange to be very clear. And now here's where the important part, let's say, of documented functions as it comes. So when we're writing unsafe block, as I said before in the beginning of the talk, what we are saying is, or RAS, let's say it requires to write an unsafe block because the point is that when you write an unsafe block, you want the programmer to give you the justification of why the unsafe block is safe. This means when I write an unsafe block, I'm telling the compiler, trust me. Basically, I'm saying trust me, this operation will not invoke and define behavior. And because of that, we in the kernel and also many other projects in RAS, many other projects follow the same convention, we want to write a justification for that with a comment. And in this case, it's not a documentation comment with the three slashes, but we want to write it with two slashes. So let me see if there is questions here now. So for writing the justification or basically the proof, it's not a proof in the sense of formal proof, but it's like a reminder, if you will, to the next programmer that will read the code or maintain the code, why this operation is actually known to not have an unsafe behavior. And remember, this has to have no unsafe behavior in any case. So if you reach this part, you cannot have an unsafe behavior. This is like in C, if you reach a code that has an unsafe behavior, then you are in deep doubt. And if I behavior, I don't know if I said it before, but basically includes things like access in valid memory or an initialized memory, et cetera, et cetera. Also in C, sign integral overflows, et cetera. So now the question is, okay, fine. We have to write these safety comments. We write it with uppercase, as you see there, that's fine. Sorry to interrupt. Yeah, go ahead. Our query, is it possible to, can we have safe functions inside unsafe block? Sorry, can you please repeat? Can we have safe functions inside unsafe block? Yes, yes, of course, yes.  Yeah, yeah. Yeah, you can call safe and unsafe functions inside an unsafe block. In fact, in an unsafe block, you can call, you can do anything basically, you can do everything. Every single thing that you have in the language, you can do it there. It's actually the opposite that you cannot outside that block. So if I am outside the orange block, right, then I would not be able to write a star P because you will get this error, the error that we saw here. If I write this, this is a error in, it's a harder, there is no way to write this. This is not a valid, a RAST program. Okay, so you have to write the unsafe block. Yeah, I see. There is also another question, let me read. Please let me know in chat or anything if it's not clear. Probably off topic, but how does one contribute to the project? Yeah, perhaps we can answer that later. Okay, so we were here saying, okay, we have to write a safety comment and the safety comment has to justify why the reference in P is always correct. Always, what it means is anytime we reach this line of code, we have to be sure that the reference in P is correct. So why we do that? And in this case, unless we do something else, there is no other way to do it. One way say, okay, I will ask the callers of my function. So if I am the person writing the load function, this function here in the slide, I just write a comment in documentation and I say, oh, I will write the preconditions. I will add a precondition and I will basically ask everybody calling me that they cannot call me with an invalid point or an online pointer, et cetera, et cetera. So basically we say load has a precondition, okay? This is one way of, let's say it's one way of getting the right conditions or the right assurances to write the unsafe code, okay? Of course, this is looks trivial, but we will see why this is important and other ways of doing it. So first of all, now we have a precondition there, right? We just wrote a precondition for load and this precondition actually is important, it's very important so that there is no defile behavior in the function. I remember the definition of unsafe function, not code in this case, but the red color unsafe, the definition of unsafe function is there is no defile behavior, right? In any case, sorry, the safe definition is there is no defile behavior. But here we are adding a precondition that says P must be valid, P must be aligned and P must point to initialize memory. If you break any of these rules, then there is an defile behavior. It's not exactly, it could be that you write a function with more preconditions than needed, that's also possible, but let's imagine that in this case at least if you break the validity, the alignment or the initialized memory requirements, if you call load with any of those broken, then you'll have an defile behavior, okay? So because there is a precondition that is important for safety, for not having an defile behavior, this function is unsafe, okay? Must be marked as unsafe. So we write unsafe, we add it unsafe, as you see here, different. We write unsafe the red color there, okay? You can also see here one feature that I will be also talking about during the talk, the comments are written in Markdown, and if you have written in Markdown, for example, in GitHub or in other places, the back quotes in P means that this will be rendered and we will see later, this will be rendered with a code block basically or a code font in the HTML in the rendered location. When you have, because this precondition, coming back to the precondition, if we have a precondition that is related to safety, what we require in the kernel and also in other projects, they do the same. This is a common convention rest. What we do is put this inside a safety section in the documentation, okay? This is a convention, this safety thing that I added here, as you see here, the different in the slides, the safety section that appears, will be rendered with a small title in the documentation that we will see. And basically the rule in the kernel and in other projects is, if you have an unsafe function, like load because it's unsafe, you have to have the precondition written, the safety precondition, okay? In the safety function, in the safety section, we write the preconditions that are related to safety. For example, imagine you have a function that is complex and has a safety precondition and you have also a other kind of precondition that is not related to a defined behavior. So if you break it, your program probably will have a bug but you are not introducing a defined behavior. So you would not write it in that section. You would perhaps write it in another section or something like that. There's a question. Is there a specification for comments like Danny or are the comments in natural language? So they are in natural language. The thing is, I'm talking about here, the conventions that we follow. For example, this safety section must be, must be written if your function is unsafe. And actually we want to have a script that checks this. We, I have in private a script that I ran from time to time but basically I want to put this as a, we want to put this as a something that is basically enforced for all the time, okay? Also for safety comments in below implementation set. Let's not get into that. So now, you see the path we have taken? We started here with a function. We documented what the function did. Then we learned that the answer block is needed because the operation of this reference in the point that is unsafe because it can't have an defined behavior and it can't have a behavior behavior because for example, if the caller gives you a P that points to the body's memory, it will be basically you will crash the kernel or something worse or you get hacked. So what we are doing is in the next one, we are saying we need to write why this function is always, does not, it never treat as an defined behavior. One way of doing that we said is writing a precondition, adding a precondition. But if we add a precondition on P and this precondition, we are using it to make sure that the function doesn't treat an defined behavior. Then it means we have to put the function is unsafe. We have to mark the function as unsafe. We have to write that precondition, we have to put it in a safety function, in a safety section. And then finally, when we have all that done, then finally we can go to the safety command and say why this is safe. And normally we say something like the safety requirements of the function, this is the precondition, means that or ensure that we can reference the value and produce, sorry, the pointer and produce a valid value. Okay. Miguel? Yeah. Sorry, there is one question in the chat. Load function is already defined unsafe, then why is it required to have unsafe block? Yeah. That's the question. Okay, good question. So this is related to the go back, probably go back. Related to the dialect we were talking here. In normal or default rust, if you will, by default it's true that you don't need the unsafe block, the ornate. But there are discussions and there is actually this way of writing rust, which we think is better, which is that we have to write the unsafe block. And the reason is coming back to the functions. Imagine that here you don't write the safety, you don't have to write the unsafe block. If you don't have to write the unsafe block, then you could say, I mean, how do you know easily where are the unsafe operations? I mean, you can for sure write a rust code without doing that. But the point is every time we have an unsafe block, we require that you write on top of it a safety comment like here. The safety requirements are ensured that we can be different. So the point is we are saying two things here and that the different colors. So the red unsafe is telling us this function, basically the red is for colors. The red is telling the colors, the users of your function is telling this is an unsafe function. What are the preconditions? It has preconditions because if it is unsafe, it has preconditions. And that's why we have to write this section, safety section that says P must be valid, align and point to initialize memory. This is for your users, for the ones that are calling you. But then in implementation, you have an orange block and safe block which is saying this is an operation that rust knows can potentially trigger and defy behavior. Basically language forces you to write an unsafe block here in our dialect in this case. And we require that you have to write the justification why this is actually safe. Okay, so the orange is a proof, a proof that you basically it's a obligation that you do the proof obligation. You are telling everyone by writing this, this is okay, I know, I have checked. I have checked and I have ensured that this is correct every time we reach this place. Okay, so they are two different unsafe. There's another question, the safety comment is just convention between software developers or is required by Rasko compiler. The safety comments, all the comments are conventional. So you can remove all these ring color. So you can remove all the comments and it will compile. But there is a problem with that. Imagine that you don't see the comments. There are two problems. One, the user of your function, how can they tell whether what they are doing is safe or not? How do they know the preconditions? How do they know whether they are introducing an unsafe behavior or not? The only way they could do that is basically opening your function and reading the code and checking whether what they are doing is correct. Basically checking that for all the input parameters that they are using, for all the, basically if you are calling with PNAL, for example, a question you could have is, can I call this function with PNAL, for example? Like for example, I know, you may have a de-allocation function, for example, that allows you to pass a null point or not. It depends on the person that specifies the function, whether it allows a particular value or not. So if you don't have the documentation or that specification or something, then the only way you could know is going ahead and read the code. And sometimes we actually have to do this in the code. So what we are doing here is ensuring that all the preconditions are with.  So let's go ahead. We can review back this, perhaps it gets clearer later. So to recap a bit on this, there are two things, safety sections and safety comments. There are two things and sometimes when one is starting with a rest, you may confuse them, like when I need one or the other. So the safety sections are for callers, as we said, and they describe the preconditions of the function, like any other preconditions. It's just that those preconditions are related to whether the function may trigger an unsafe behavior or not. So basically if you don't upheld the preconditions, the function is not guaranteed anything. There is no guarantee there is no defect behavior. This is exactly the same as we see here in the function we are talking with Francine, which is a completely normal function in C. The only way you can know whether P, what values of P you can pass is checking what you are doing in the function. If you write documentation in this C function, then you could also write the comments here, okay? But there is a difference with rest, which is rest has a language way of requesting that or marking a function to have safety precondition, okay? And then the callers of this function, if the function is unsafe, it requires a block, an unsafe block to call it. So you cannot call a load, the load function here, you cannot call it from a safe rest. You have to write an unsafe block, the orange one, okay? Yeah, so coming back to this slide, you can review it, you can also download it and try to read them. I have no data here, but it's not really important. They are also used, not important for this talk. I mean, they also use the unsafe key words, also used for traits, we use it in the kernel as well, et cetera. But to be simple here, let's talk about only the functions on the, sorry, the function. There is also a safety comment, as I explained, safety comment in the kernel. Again, in the kernel, we require that they have to have the all the unsafe blocks have to have a safety comment, okay, above them. Okay, so let's try to see now an example from the kernel. This is, in this slide, I have an example, copy pasted exactly as it is from the kernel. So please consider the function, okay? There is a function called name. And we see here something is doing. Basically, I can go through you through the function. Let pointer basically decrease a variable, pointer, a binding, and we opened an unsafe block, the orange one, and calls bindings. Bindings here in the kernel is the C side of the kernel, let's say, so the bindings are the functions of the kernel. So there is in the kernel, in the new kernel there's a function called error name, which returns a string representing the error as the function says. And we passed this self.zero, it's not important here, but the point is how they are justifying this call. So in this case, as you see, it says just a FFI, so foreign function interface call, there are no extra safety requirements. As you see here, we are actually saying there are no extra safety requirements. We also sometimes when we do calls to C functions because the calls to C functions may have requirements, we want to say, okay, this unsafe block is only there because we are calling the C function. Basically in REST, you are required to write an unsafe block and you call a C function in the kernel, okay? So if you don't see there are no extra safety requirements, you could wonder as a reader, you could wonder, okay, yes, this C call, but there are something else. Is there something else that you are not writing here? Is there something missing? So by writing this, basically we are making sure we are telling the reader, this function does not have any precondition. So one way, as you see, of just justifying that there is no, sorry, but there are no other conditions that you have to upheld, one way is just to examine the C function or the function you are calling, check in all the preconditions and see if there are preconditions. For example, in this case, in the kernel, I think there was no documentation, I think, but I may remember correctly it may be there now, about what are the possible input values, okay? So error name may tell you, okay, I admit error values from zero to something or perhaps it does everything. What I, when I checked, I saw that the code, check in the code, in the code, basically it works, there is not if I'm heavier, it doesn't, it's not if it works, but there is not if I'm heavier for any input value. So if you pass an invalid error code, it will return null if I remember correctly, okay? Yes, because we are checking it here. So what we do is then we checked if it is null or not, and then there is here another answer block, and this is the one that is more important here in this slide. So in this one, we have say, the string returned by error name above, so the pointer that we have now is static and is null terminated. So this is yet another way of sometimes justifying another block. We are basically using the post condition of the error name above. So we know however we do it, did it, for example, reading the documentation or examining the source code, it depends. What we are doing is we are taking the error name and we know that either returns null or a valid string that leaves basically forever, it means, okay, for the entire lifetime of the code, okay? So first of all, if we didn't put, for example, imagine, we didn't put the if here, the if pointer is null. If we didn't put if pointer is null, then we have two cases. One is the pointer is null and we would be calling this function from char ptr with a null and that's not the value, okay? This function has a pre-condition which needs to be written in the documentation, et cetera. So you see this goes like a chain of things. From char pointer requires that the string that you pass has to be valid forever, basically, okay? And it's not exactly, because we will need to talk about the lifetimes and the reference that we are returning here, but just imagine that we have to return a, we have to input a pointer that is valid for the entire lifetime of the code. So we know that the string, the pointer, that her name returns is not null or not. If it is null, we return and we don't go to that unsafe block, okay? So there is no unsafe here. There is no, and if I behave you, sorry here, because basically we don't reach that line. So we have checked that the null case, we are not in the null case. And if it is not the null case, then we know that the her name promises us that the string leaves forever and it's null terminated. So we can call that fast. And that way we have basically proven in between quotes, we have proven that this is always safe when we reach this line of code, okay? So to recap a bit and to try to give you a bit of more context and not confuse you, there are two, three ways we have seen to justify so far a safety comment. One is basically asking the callers for some precondition, basically telling the callers, okay, you guarantee it and then I use it. It's like forwarding, if you will. You ask somebody else, okay, if you call me, then you have to uphold this precondition and then I will use that precondition to call something else or to do something else like the reference in a pointer or anything else. A second way to do it, like we see here in this slide is you check the implementation, you check all the preconditions, you see that basically you comply with all of them, perhaps because this is non and then you just write it, okay? Another way is yet another way is sometimes you write, you use conditions or you know something is true because something else in your function, in the same function tells you, for example, here, her name again has a precondition whether it comes from the documentation or because you check the code, et cetera, et cetera. You know that the string is forever and it's now terminated or that or it's not, but we check that. So basically we are using something else previous from our function and we just reuse it or we use it down in the function. We do this a lot of times. Another case of this simply is, for example, imagine that you have to pass a function, an integer that has to be zero, one or two. If you declare a variable, like you initialize a variable with zero, one or two, then you can write a safety code and say, I just initialized my variable to zero, one or two, okay? So basically what I'm trying to say is this way of justifying is local is something that you see in your function or you know because of other operations or other codes or other codes in your function. Okay, let me see the questions. Is it correct for safe precondition to specify some rules that achieve correct behavior of the function, say function never crashed and may return incorrect result and not the rule to achieve safe operation of the function, no crash, no null pointer reception. Let me try to understand. It depends what you mean by correct behavior because if basically the preconditions that you do the safety preconditions, they have to be related. I mean, they don't have to, but there is no point otherwise to have a precondition. The safety preconditions should be related to whether, basically you need to write as few because you could always write more preconditions but what you want for your colors to make easy or more flexible the function is to review the preconditions as much as possible, right? So you want to review the preconditions. So you normally, what you want to find is the smallest set of preconditions that make the function never triggered if I behave. So if you have other preconditions that are not related on the five behaviors, normally you don't want to specify them. You may have other preconditions in the function here. You may have other things that are not related to safety. For example, imagine that the load, imagine that there's a bug or there's a precondition not related to memory, not related to data racism, et cetera. It's just that, for example, you call load with, I don't know, some context in the kernel or you call load in some other thing, then it's a bug or you know it's a bug but then you would say it, you would say the precondition is that this value is whatever. For example, you need that they call you with some value that is zero, one or two, then you would write it zero, one or two. As long as the zero, one or two, that is not involved basically on whether there is undefined behavior or not. If you don't use it in your function for justifying anything, then it should not be a safety precondition. I hope that that makes sense. It's normally when you write code and you see examples and examples, it basically comes more naturally. Why we use CSTR, let me see, let me go there, CSTR here. Why we use CSTR and save, can't we use static string as they are saved already? Well, this is an example I tried to, basically I searched for, there are other ways of doing the thing that's first. We don't use in the kernel in general, we don't use, we don't want to use STR, the REST type STR for others that may or may not know, STR and REST is a UTF-8 encoded, basically it supports Unicode. And normally we can do Unicode in the kernel, so there is no need for Unicode in the kernel. So we have other types like CSTR, BSTR, et cetera, that we use. So, but regardless of that, the point is, I basically searched for the, in the kernel, I searched the kernel for an example that's had two cases of safety different ones and one use something else and I picked this example. We would need more context actually to know what this is, because this is actually a method, so we need the, where this is, et cetera. I mean, there is, the point of the example is not really to discuss whether this is the REST string. But yes, in general, the answer to that is that in the kernel we don't use Unicode, I mean, we don't need to use Unicode, sorry. Is there any restriction on the kernel to uphold the preconditions? It depends what you mean by any restriction. So the preconditions, the colors of your function, for example here, the colors of your function, they are the ones that have to basically, to be correct and not to take any behavior, your colors, the people calling all the users, calling load, they have to uphold this precondition. If they don't, basically they are introducing a very serious bug in the kernel. It's exactly like in C, if you hear, you call this function, many of you have this C function, however you call this function with an in-value point. Then, yeah, this is basically a serious bug. If the question is more related to whether this is somehow automated, perhaps, I don't know. Basically, it's basically a compiler forces you, if you have an unsafe function, for example, if you have an unsafe function here, load, the compiler will not allow you to call load just like that, for example, a driver. Imagine you are in a driver, right in a driver.  Then, sorry, the compiler will not compile that code because you need to write unsafe block. And that's the point, that you write unsafe block and when you write unsafe block, then you have to provide the justification and that's why we require the justification. Okay, so that's the compiler add extra code for an unsafe function. No, unsafe here is completely static. There is no, there's nothing. I mean, we will see later, otherwise, because unsafe doesn't do anything for code generation. It has nothing to do with that. But sometimes you want to not have unsafe functions. You want to have safe ones. And to do that, sometimes there are other ways to do that. That's what we are going to see next. There is one question in the chat box, Adil. I think you already answered that, but I just want to make sure. Name function has unsafe block. Isn't it required to be defined as unsafe? Let me see. Name function has unsafe block. Let me go back, sorry, let me go back to there. No, function is already defined. Same way it's required to have unsafe block. If you mean the orange one inside, it's required because of the dialect that, yes, I already saw that. There is another question and then I will continue because otherwise we don't cover the... If there is an unsafe block with safety comment, okay, is it possible to modify this existing unsafe block which does not match the safety comment anymore? Yes, of course. I mean, the comments, they are not formal proofs. This is not like, you are not doing a Spark, for example, Ada Spark, you don't have automated proofs. So these comments, they have to be maintained. But as we, I would like to say if we have time in the end, the point of these comments is to use the maintenance and to be able to, for a reviewer, when they review the code or they change the code, they have to have this information in order to know whether a modification of the code basically keeps the system working. For example, if you modify the implementation of load, then you may be adding, maybe removing as well, but you may be adding new preconditions for the code. You may be touching the function in a way that you are adding preconditions. So you first, you want to have to change the safety justification perhaps. You may have to add preconditions in the function. And you may have to use that and you have to go to the colors, just like you would do inside, you see. You have to review all the colors if you change the preconditions of function, et cetera, et cetera. Okay, so let's go to get another, or get another way, but this is a very, very powerful one. A way to, because, okay, let me try to come back a bit. We have these ways of justifying we saw three ways of justifying the unsafe blocks. But as you could tell, or you could say, well, but this is basically, we could do this in C and there is a major effort, et cetera, et cetera. We want, for this kind of thing functions, but we want really in the kernel at least. And I mean, mostly in most REST projects or you want to use REST to begin with because you want to write as much of your code as possible. It's possible all your code in safe code, okay? And to remember the beginning of the presentation, we, in order to do that, we have to write abstractions. We call them abstractions, like safe abstractions of unsafe code, right? So actually what we want is not to have to read, for example, unsafe here, the red one. We don't want to write the red one. What we want is to have a load function that is set and then users don't have to care about safety preconditions because there will be no safety preconditions, okay? You may have complexity inside the abstractions and you have to think whether they are sound, whether there is no way to deal and define behavior with the preconditions that you put or no preconditions. But basically the idea is to try to enable users of different subsistence in the kernel to be able to use as many functions as many APIs completely safe. That means from the safe subset of rest. Because if you do that, then the writer of the driver, for example, for the kernel module, they don't have to care about that. Basically the abstraction is the one with the burden of ensuring that that's correct, okay? So one way of doing that, and for example, take this load example, one question you will have, okay, so how do I do that? How do I, I don't want to basically pass to my colors for a pointer that the pointer has to be valid, aligned, and pointing to each other's memory because then this is the same as C basically. So we are going to see one way. We are going to attack this with an example again. We will see also a kernel example and then I will tell you why this way basically is very powerful. So first of all, let's start with another example. Let's start with this example in the slide. Let's assume there is a printer for C function. Okay, this doesn't exist in the kernel, but I put it for clarity and to try to come up with a very easy example. So imagine that there is a, in the kernel, a printer function and this printer function has some precondition, okay? That the code that we want to print is within some range, for example, from zero to max error or whatever. So if we don't pass a code that is correct, for example, the code, the implementation of printer you could think there is an array, for example, or pointers to strings and then it will call printK with indexing data array and if you pass a code that is not within the array, then everything blows up, right? So imagine that a printer function with a use of precondition, let's say, and that is a safety precondition. Even if we don't call them safety preconditions, it would be a safety precondition in C. And actually, if Rust gets into the kernel, it will be nice or interesting to start documenting the C site as well with this information because it's very powerful to understand code and then to make the safety structures at least in the Rust side. Okay, so we start with the function. We create, again, a safe printer function that takes a code and the code, we don't know anything about it and we have to justify again why it is safe. And as we know, as I said, print error. Right now, as I told you, there is a precondition and it's a safety precondition. So there is no way, at least in this way, there is no way to justify it. But we don't want, we could do. One thing we could do, of course, is go like in the previous example and we could just put that safe in the print error in the Rust function, we could put that safe and then add the precondition to the colors. Okay, give me a code, an error code that is basically valid for print error or something like that. We could do that, but we want to avoid that, okay? Because we want that, for example, a driver calls printer of battery with nothing else, okay? With no unsafe block. So first, what we're going to do is we create a type. We have to go, sorry, we have to go a bit with it because otherwise the time runs out. But I will try to focus with this, the later part of the presentation is not as important, I think, so I will nevertheless, with a bit expensive time here. There is this type, we create a type, this is a struct with a single field, okay? That wraps or contains the interface, okay? The error code that we want. And we document it because it's a public type, so we have to document it in the kernel with the conventions that we have. So we start with that. Then we add, so we are going to add a couple of methods, okay? We in Rust, you write that to start writing your methods, basically. First, we will add a constructor. Let me go through this. You see here, this, we just added, as you see, we just added, not in exchange, we just added the function, the method there, which actually is, if we say it's not a method because it doesn't take cells, but nevertheless. It's a constructor, it takes a code, an integer, and it returns a result. A result in Rust is whether it's basically the vocabulary type that you use to denote whether the function had an error or not. It's a type that contains two variants, basically, whether it's okay or it's an error. So it returns whether the function had an error or not. If it didn't have an error, then it gives you the error code type, okay? So it gives you a struct or an object of the type struct error code, and it gives you just the struct with error code inside. It doesn't do anything else. And if the code is bigger than some constant, then it returns an error, okay? I will pause a bit here in case there is some question about this because it's important that we get here so that we, okay? So what we are doing so far is just one function that returns a new type that is called error code. What we are not doing, you may think, oh, we are not doing really math. Now, the key thing here is that at least so far with the code that we have in the slide, if an error code exists anywhere in the program, then the code has to be valid by construction. And this is key. It's statically true. I mean, there is no way you can compile a program where if you have an error code, it's invalid, okay? This is the key, okay? So let me explain why that is true. One thing why that is true is because it rusts the people outside the code users or the programmers outside your, for example, the kernel grade, let's say, they cannot modify your integer. So they cannot just go into your extract and modify the integer, okay? They have to go through the methods to access the integer. So right now there is only one method. And that method, the only thing in that is return a new error code. And because we check that the error is within the bounds that we care, then there is no way because there is no other method, there is no other function, there is no other way to get an error code that has an invalid error, okay? Of course, this means, this of course assumes, but there is no way to get around that, that there's no memory corruption, that there is no undefined behavior, there is no, you know, a C function going through your memory and replacing values, that there is no hardware errors, soft events, et cetera, et cetera, et cetera. But apart from that, if the rest of the code doesn't have undefined behavior, then there is no way you can get an error code that is invalid, okay? Now we add another method, very easy, call to code, which basically takes your extract, reference the extract and returns a copy of the error code, okay, an integer, returns an integer with a container. Okay, the syntax doesn't matter, the set of 0 returns the first value, et cetera, it doesn't matter the syntax. And now, the difference here, which is like this, precisely because we know this, the thing that we have here is if an error code exists, then the code has to be valid by construction, precisely because of this, then this method, we can write a post condition of this method, we can say, okay, all the I32 that I am returned, they are guaranteed to be valid, right? We know that the error code is always valid, therefore, if I call to code, because I have to have an object, so I can only call to code to an object of type error code, then it will return the integer, I mean, because I knew the integer has to be valid, then that integer that I get, it is valid, statically, we notice, okay, by construction. There is no way to construct a program without any fine behavior, there is no way to construct a program that returns here something with an invalid error code, okay? So now we can go back to our function that we wanted to justify the safety comment, right? And we are going to do a few changes. The first one, instead of, which is the key, the first thing is we remove the parameter code which took the I32 and what we are going to do is take the error code, okay? We are going to take an error code. And again, if I know I have an error code, then I know it will be valid, right? So I just call to code and I can just call it the print error function because I know it's going to be valid. And so the justification that I have to write in the safety comment is, error code returned by to code is always valid, for example, this is one way of writing it, right? And now the key is that we didn't have to write unsafe and the red unsafe function. Print error is a safe function. It's not an unsafe function anymore. Of course, how we are doing this is not magic.  The only way you can call me is if you have an error code, okay? So if you give me an error code, then I just called your function and everything is fine. And this way, the driver, for example, can use this function. Imagine that error codes, you create error codes from some subsystem in the kernel. Instead of giving you the subsystem, instead of giving you a 932, it will give the driver an error code. And because it's an error code, the driver knows basically not the driver, but this function, the driver can just call printer with that error code, just passing the error. There's nothing to do, basically you just pass the error code. And then with the error code, because the printer is a safe function, there is no need to write any unsafe in the driver, okay? There is no need to put unsafe code in the driver. And as long as this code, the one that we have here, and as long as the implementation of error code, not the drivers, the implementation of error code, as long as the implementation of error code is what we say in rust sound, as well as long as it's sound, or as long as you can say, as long as it's correct, and there is no way to basically reach a state of error code somehow that then the precondition of two code is not correct anymore. Then as long as this code is correct in that sense, then all the drivers can call this function just with no worries, or no, no, they are not going to do this kind of behavior. They are not going to go beyond the bounds in the printer function when they go to the seaside. Basically, this is the printer function in rust, goes to the seaside, that one will go beyond the bounds. Okay? And this is basically the key of how many other things are done in rust. And you will use it all the time, okay? Let me see, there is questions. So when you instantiate error code, shouldn't you be calling from code to ensure that the validation is done? Sir, can you repeat? When you call? So when you instantiate error code, shouldn't you be calling from code to ensure that the validation is done? That's the thing, exactly, exactly. The thing is that basically, I'm not showing here the call to from code, but it doesn't matter because when you arrive to this function, you have to have somehow an error code, right? Somebody else will call from code and we'll call the constructor and give you the thing. Okay, so that- I'm trying to show here, yeah? Go ahead, please. The assumption is like a from code is called, right? Before calling printer. No, that's not the assumption, basically. What I'm saying is that it cannot happen otherwise. It's impossible that it cannot be done like that. Basically, there is no way you arrive at a program. You cannot write a program that if you have an error code, you have not done the check because to get an error code, you have to go through from code because there is only one constructor. In the real code, there are more constructors, et cetera. You have to take care about things. But the point is that if you do your time correctly, regardless of whether there is one constructor, two, three, it doesn't matter. The point is in this example, you have one constructor, right? Which is the simplest case. You have one constructor. If that constructor performs a check here, Dave, then the only way to get an error code is to have done the check. Basically, the fact that you have an error code somewhere in the program is the proof. It's not just an assumption. It's actually proof that you did the check at some point. It could be in another part of the terminal of the check. It doesn't matter because somebody in some subsystem, completely different from the driver that you're writing, for example, they could have called the from code. And then the driver received the error code. And it doesn't matter how you arrive to the error code. But the point is that no matter how you arrive to an error code, if you have an error code, then it has to be valid. So the existing of the error code is the proof, basically. Okay, got it. Thank you. Thank you for the question. Let me see. Yeah, so going back to this, there are to continue these questions and thank you for this question. There are other sometimes in real code and we can see, I don't think we will have time. We can see that, for example, there may be another constructor that you may have in your type. That is unsafe, for example. You may provide to your user two constructors, one that is safe, this one that you see here in the slide, and that one always checks, basically. There is no way to fool this constructor, right? So this constructor is safe. Then you may have another constructor, for example, that is unsafe. And that means you have to say to the caller, you have to provide me with a valid error code. Why do you do that? You say, why if I have the safe one, why would I want an unsafe one? Well, the point of unsafe constructor is, sometimes you may know because of other reasons that your code is already valid and you have a performance requirement or something. You want to remove the branch, basically. You don't want to pay for the branch, this branch here, Dave. Imagine that you have a code from somewhere in the corner. You know that code is always, always, always valid, but then you want to give a run driver. You don't want to give the IE32. You want to give it the error code, the one that is good and can be used safely. So what you do there in your subsystem is, okay, I notice error code is valid, for example, because it's a constant, you say, the simple scale, you have a constant and you have a constant and the constant is one of the valid error codes in the kernel and you say, okay, this is the constant. Okay, so I construct, I call from code unsafe, which normally is called from code unchecked. The rest, they put postfix unchecked, which is an unsafe function. And that unsafe function doesn't do the if, but is unsafe. So basically the user of this type chooses how to construct. Either you pay the price of the branch because you don't know whether the error code is valid and then you pay the price, but in turn you don't need any unsafe blocks to call it, or you call the unsafe constructor, but then you are the caller of that constructor has to verify, has to provide the justification why basically they have to provide the proof. Okay, this basically is providing you with the proof. This implementation, this safe function is basically checking because it's checking, there is no other way to very run. I mean, of course, if the implementation of the function is incorrect, if you make a bug in this function, then the whole system goes down. But the point is to write everything in a way that this is correct and then drivers will, there are the drivers or the users of this function, they cannot make a mistake regarding and if I behave. Okay, this actually applies to not just and if I behave. You can use this kind of constructions for all the things that have nothing to do with that behavior, but here we are concentrating on safety comments and safety annotations. Going back to the type in variance. Sorry, another question. Are there situations when constraints are not known before? For an explanation before actual code to unsealed code. If yes, how to deal with that? Let's listen to what you're concerned about beforehand. Depends on which constraints that you mean. If you mean that you don't know, for example, when calling print error, you don't know whether you have a code that is valid or not. Well then basically you cannot write the justification and then you would say, I mean, you have to find it basically otherwise you're just hoping for the best, right? It's not different in C. In C when you're writing a driver or anything else, you really have to be sure that you are not blowing up the kernel somewhere else. You cannot just take something that just, right? So you have to always, that's why we always require the justification and the point of requiring these safety comments is two four. One is, again, to ease the maintenance of all these preconditions, proofs in between codes, not format proofs, but that's one thing, the maintenance side. But the other side is also for the people writing the code for the first time to force them to actually think and write why this is the case, okay? And not just say, oh, I did an inspection of the code. I think this is the thing and that's it, okay? Basically you are forced to write it and when you are forced to write it, you actually see that it takes some effort, especially in the beginning, it takes some effort to write these comments because you are basically asked to tell. It's like if in a review, everyone in a C code where you are doing a dereference or any other unsafe operation, everyone is asking you why this is, basically why you are not introducing a vulnerability here. Why you are not, why this dereference will be always okay. Why there is no overflow here. Why, et cetera, et cetera, et cetera, et cetera, et cetera. Okay, so now we're going back to the invariant. So here we have seen what we call a type invariant, okay? We have seen it, but we have not actually talked about invariant yet. The invariant here basically is that we have a type error code, which is called error code and this error code maintains an invariant. An invariant is that it's like a property, if you will, of a type that is always true. It is something that always applies. Okay, it's like a proposition in logic or something that you know that as long as that type is anywhere in the program, then it has to be the proposition or the property has to be true, okay? So what we do is we have an invariant section that we write on top of types that have this kind of invariants and there are many of, I mean, in many cases we do this and we write what is this? For example, here, an example is we could say the error code is within the interval of valid error codes as defined by specifications. Here I'm talking about perhaps not the kernel, but something like a POSIX or whatever, okay? Somebody defines what is a valid error code and then you say this type will always, always, always have an integral inside it that is within that range, okay? If you will, in this case, in this example, you could think of error code as a type that is like a constrained integer. And that's the key, because this is a constrained integer, that's why you can remove the preconditions in a function like this. Instead of taking an IF32, which is basically unconstrained, it can take any of the integer values that are fit. Instead of doing that, I say no, I don't allow any interval, I only allow an error code and a error code has this invariant, which is that it has to be within those, that interval. And that's how you are removing the preconditions that you would otherwise have to write in pretero. You have to make it an answer function like we did in the previous example. Here, if we're going down, we're going back, here in log, we look load and have to make it unsafe, the red unsafe, we have to make it an unsafe function. The reason is because basically we said, okay, fine, the caller has to do the check or has to know that the pointer is valid somehow. For example, because you are pointing to your own stack value, for example. But sometimes we don't want to do that. And in fact, REST, if you have studied a bit of REST, you have seen references and mutable references, et cetera. References are actually a type that has an invariant, which is the reference points to a valid, initialize, et cetera, et cetera, memory. So in REST, for example, you normally, you don't take a pointer, which has an input parameter, you would take a reference to the E32 or whatever it is, the solid IE32, whatever it is. So the reference in REST is a way to constrain the possible basically pointers, if you will, that you can receive. So you constrain them. You say, it's not a pointer. It's not a raw pointer. It's not a constrain pointer, it's a constrain pointer, sort of. So instead of taking any pointer, I will take only a reference. And because of how REST defines references, et cetera, et cetera, et cetera, then the load, this function, would know that the pointer is valid and align and points to initialize memory. And then you don't need unsafe in the implementation of the function, for example. Or you don't need, and also the function, most likely, it depends, there are cases, et cetera, we have it in the backup slices, this question about this, but the load function wouldn't need probably, in this case, at least to reference it. If it is this function, and the only thing we want to do is the references, if it is a reference in REST, it's not a pointer, then it's not unsafe because we know the reference always points. And actually REST does not consider the reference and say it because there is no way you can get that wrong. Basically, if you de-reference a reference, then it's always valid, okay? So if you are writing this function and it's not for some other reasons, sometimes you have to take raw pointers in the kernel, et cetera, in the structures, we have to use them. But I wrote this example to show you what is the problem, what is one way of providing the guarantees on the pointer that you need. But there are other ways, which is using type invariant, for example, which allow you to have a type that is constrained. For example, here we have a pointer, but it could be a pointer with references or it could be anything else. So you create a type, give it some invariant, and then everyone that receives that type knows aesthetically that the type, what the type, the properties that the type provides. Okay, I hope that that is clear. So I said, coming back and I will go deeper. The, this is a key idea here in the talk. And one that we spent a bit of time in the previous, but it was hard without the slides to explain. So here, the error code is, we wrote this invariant and now what we do also in the kernel, this is again another convention, what we do is that every time, because consider that error code, imagine that you are modifying error code, the type itself. Then you have to always, when you modify that, you have to take into consideration anytime I modify my integer, the one inside. In our case, there is no methods that modify the integer, but it could be. You could have, sorry, you could have a type that has some state and you modify the state because of different operations, right? So anytime you modify that state, at least the state that is related to the invariant, we want a justification that you are keeping the invariant up whole, up here. The reason we want that is because the invariant runs, at least the ones we use in the kernel and many times we use them, they are related. We use the invariant later to justify the safety, to use the mass justification of the safety commands that we have. So this is a technique, basically, or a tool, a key tool to do that. And that's why we also require the justification for invariant, and we write this. This is the difference here. For the kernel, we will write invariant, which is a command in this line of code, which is the one actually creating the instance of the error code. And we say, the check above, this is referring to the if, to the right, ensure that type invariant holds. So if you have, imagine that you have many methods, not just one, you have many methods and some of them change the state of error code. Basically, we write the justification why we are not breaking the invariant. Because you have a method and then suddenly in one method, for example, imagine that you have a method in this error code that basically, if you call it, increments the error code and you don't check anything, you just increment it. Then a user outside of your, of the kernel create a driver, for example, the driver could call, get an error code, and then keep calling increase, sorry, increment, increment, increment, until it goes outside of the interval. And then it goes outside of the interval. And then the invariant is not helping them all. And then the places in the kernel, like print error, that are using that invariant to justify something, then it's, that doesn't work anymore. Because that is not true anymore, but returning the copy with two codes is always bad. Okay, so that's why we write the invariant to work. I mean the comments, not the section. So you see here, there's a parallel between, like with safety, we saw safety sections and safety comments. Safety sections for callers, preconditions, et cetera. Safety comments for the implementation to justify an unsafe block, an unsafe block, to give the proof. The invariant is simple. We have invariant section, which is written on the types and give you what is the invariant, explain what is the invariant that that type keeps. And then you have the invariant comment, or comments that basically describe why this is true. It's similar to the safety one. Basically, it's a justification. You have to justify why you are keeping it, okay? Well, let me give you an example from the kernel. In the kernel, we have a C string, okay? And you see here, I modified the slide, it is one I remove a couple of things and it doesn't matter, and quite a big part of code because otherwise it doesn't fit. But basically, you see again the pattern here. There is a C string, and the C string says, in invariant, it says, the string is always an alternated and contains no other null bytes within the string, okay? So basically, you are guaranteed by this type that all your memory, the vector, the array, if you will, the memory region is a string like a normal C string and there is no zeros in the middle and there is one in the end, okay? And the method, one of the constructors here called try from format, it doesn't matter, the arguments are anything. The thing is, it returns either the C string itself if everything went well or it returns an error, okay? We have this error type in the kernel, et cetera, et cetera, et cetera, it doesn't matter. And in the end, when we actually created the instance, we say invariant because it's a modification of mutation. Basically, the construction of the instance, you could think about as a mutation of the state. So we have to justify that the buffer we are writing there, the variable that we are putting as the field actually has the variant that we need, okay? So in the code that I didn't put there in the dots, we are writing the null terminator, we are checking there is no other zeros as it was. Okay, then, and this is perhaps too deep to go now, but sometimes basically what we saw in the print error case, in the print error case, we saw that somebody uses error code to constrain some parameter. And then normally you write something based on the post-conditions of a method of the type. Or sometimes you may say something about the type invariant, but to justify some safety code. But here, when you are inside your own type, when you are implementing a method of the type, like error code or C string, in many cases you want to use also within your type. So in the method, you want to use the fact that you are holding that invariant to justify something. So for example here, we are implementing something called the ref, which basically the reference is the C string. This is a trait, I will not go into that. But basically this is, you could think of inside the type, okay? And we are using type invariant itself to guarantee that when we call this other method or function constructor from C string, it has some preconditions so we have to guarantee those preconditions, et cetera. Okay? So we are using type invariant directly. We are not even using a post-condition of another method of C string. I know, sorry, we don't have too much time to go into this, but I hope it's a bit clear that type invariants are very important to statically create safe APIs. Okay? I have something on examples, very, very quickly, we're not going to have time. Consider that the structures, this is copied from the kernel. We have a data structure. This data structure has some invariants as we saw. It's useful, other things, et cetera, et cetera. But here we want to see the examples. In Rust, I mean, Rust for Linux in particular, we have example sections. It's a very common section to have in Rust projects, which basically you write after, maybe after the invariant, it depends the convention and change. But basically after that, you write examples, okay? I mean, just right after the invariant, you will write examples. And examples will look like this. And actually, these examples, as you see, I could explain, we don't have much time, but I could explain how, basically how, what is the bound symbol here, et cetera. It doesn't really matter. The thing is, you should write examples that show how to use the data structure. And actually, and the main, sorry, point of this, is that these examples are actually code that we compile and even we run okay, so we basically, this is not right now done in the brands that we have public, but I am working on the way to basically take these comments and put them as a K unit test, okay, automatically. But right now we compile them already and we run them, but in the host only. So we can only do some tests we cannot do, but other tests we can. For example, this data structure we could test if it doesn't use, if it didn't use, in this case, if it didn't use, if it was an abstract data structure that it was not baked back, sorry, back from my the red, black tree in the kernel, you, we could test it as well. So because we run them in the host, but the point is in the future, at some point we will have this test running in the kernel as well, even if they are look like documentation, okay? So they compile and they run and they are very useful that they are compiled because we actually by compiling this, when you write your documentation, first of all, you write documentation because you have to write it because the rule in the kernel is that you have to provide documentation and if you don't put examples, normally we would say, okay, you should perhaps have examples, et cetera. So imagine that you're writing a, you write examples, you write an example. It has to be valid code and it has to compile and in the future it will have to actually run the kernel. And this is good because first you do it at the same time you are thinking about your API, et cetera, et cetera, et cetera. You also have to think about the API, et cetera. But also the fact that this compiler run means that the documentation stays, it's easier to keep, let's say, or there's a higher chance of keeping the documentation in sync because first is closer to your code, to the code that you have. This is right, and you see, it's right above the definition of the type. But not only that, it's also the fact that it compiles, it allows you to imagine that you change the API of the time, you change the methods. Then all your documentation will not compile anymore. So you have to actually apply that. So it's very useful that this compiles and wrap. Also, we can write obsessions, of course, there's several kinds of obsessions. The idea is that we take these obsessions and we get the macro, we call the raw, basically we need a way to write expectations and have them this nicely mapped, et cetera, et cetera, we'll go into that. Normally it's nice to write the examples with some pros, with some comments, basically you write something, you give that example, you write something else, you write a second example, you write something else, et cetera, et cetera, and a more example to give on how to use the module or your type, et cetera, the method. This is basically telling you again what I just said. Also, it's useful to show common pitfalls, so not just the right use, but also it's useful to show examples of something that doesn't work. Either you can even check that it doesn't panic, et cetera, et cetera. There are several ways to do things, but basically the idea is good to have that, sorry, to show how it can fail, or the common failures that you have seen or mistakes that people may have done. Here is how it looks. I wanted to point out the safety section, the example section is how it looks rendered. The things are highlighted nicely. There's a feature called intradoc links. It automatically links without you having to put a URL or a path functions, et cetera, et cetera. So it's very, very easy to use and everything is linked together. So it's not like a cross-reference or a savior, but it's like also in the Sphinx when you write something, it links to the theme, but everything is in the, what I want to point out is everything's in the same place. There is a rest source code. UTS is a bit different than what we have in the kernel for the documentation at least, not others, but other cross-references, references, but the source here is the source of your documentation, which also contains a die. So this means it's not like sometimes when you go to the Sphinx in the kernel and you click on the source, then it shows the RST file and it doesn't show the actual code. You have to go to the include file or the implementation to see that. There is kind of search as well. This is how it looks in the kernel or our own documentation. This is the one that we saw here. This is the same that we saw before. We saw it here. And then other nodes, we will read it very quickly. We will write a module. We follow a template that we will be updating because we want to have a way to cross-reference the C code and the REST code, et cetera, so that we don't have to write four URLs, et cetera. There are other sections that we may add or we may start using. Also, I encourage people writing this or going to go to document any dieting extensively, especially if it is a modular type. It's very useful to have like an overview of how it works. And I will show you here a couple of the green shots of the back from the standard library. You see here, it's showing an example that works, an example that doesn't work or panics, let's say. It even has documentation that looks very nice in the page, et cetera, so it's like you can put drawings and you can put all kinds of things. So basically, as you see, it is different than the kernel. We would put most of this, we would put in the documentation form. So if you write these things here, then it would go alongside the code. And of course, sometimes it's too much to put there, maybe, but other times it's very nice to have it We also follow the calling guidelines. And yeah, please take a look perhaps at the slides we can go through in another session if there is something about this. But yeah, I put some useful references for you. You can look from the slides. And I had three slides on tests. I will, yeah, basically skip. We have three kinds of tests in graphs. We also can take a look at the documentation. But as I said, like with the documentation test, we want to run as K-unit probably tests. We want to also run the unit tests which can test private code in Rust. And also perhaps in the recent test, which basically could be very similar to the K-unit ones. Unit tests, the one that can test private function look like this. We have this from the kernel. We have one to test the CS3rd that you saw before. We are running these tests right now and compiling them and running them in our CI. We would like to have, eventually, to have basically the CI's of the, we are talking with the CI's of the kernel to run our things or to build tests, at least our things. And we would like that they also compile the tests, et cetera, et cetera, and run them if possible. So we are working with that as well. Conclusions, I will put a slide here. There are two slides only. And what I want to tell you is basically all that we are doing in Rust. Yes, Rust requires some set blocks around operations that may have UV, provides a way to mark functions that trigger UV. We have some rules on top of that, some conventions of that, like writing the comments, the safety comments, variant comments, safety sections, et cetera. We use a dialect that we hope it becomes official, Rust way of writing the answer block, et cetera. But we are doing all this so that drivers, and this is the important thing. We are all doing all this so that drivers can use only safe code. And in order to be able to write drivers with only safe code, we need APIs that are safe. And in order to do that, normally we have to write types with invariance and et cetera that allow us to reuse the preconditions and to statically ensure some, okay, as we saw through the talk. The code documentation, of course, does not change the behavior of the code, but it's important as we explain to review the soundness of a module to make changes easier. The safety sections are critical. Even if you think the comments could be all removed, safety sections in particular are super important and critical because if you don't have safety sections, then if you have an unsafe function, then you don't know what are actually the preconditions. You know it's unsafe, but you don't know why. You would need to review all the code to know. Writing example is useful. We are working again on testing to integrate then with the other testing support in the cabinet. And that's it. Thank you. Sorry for the rust in the end. And that was it. If there is any last minute question, we can take it a minute or not. I know. No question. Thanks. Thanks a lot. Thanks, Miguel. Thank you a lot. Thank you guys for the questions and being here and thanks for following the session. And thank you to the general foundation for hosting and inviting me. Well, great. Thank you so much to Miguel and Shua for your time today. And thank you to everyone who joined us. As a reminder, this recording will be on the next YouTube page later today and a copy of the presentation cycle will be added to the Linux Foundation website. We hope you'll be able to join us for future mentorship sessions. Have a wonderful day.