Intro to the Lean Theorem Prover

Transcript

okay um so for the second to last uh talk of today or Workshop of today um I'm I guess I'm deviating a bit of from the topic of giving uh defi security 101 introductions to like level more meta um what I want to talk about is uh the lean theorem um and you've seen lean actually in the uh in the talk about uh control um and this is going to be like a more more of a deep dive into the lean theorum and if you feel a bit tired um I

can assure you I will um do lots of live coding and due to my state of mind probably will be make mistakes maybe that's going to be entertaining um so who am I um my name is Jacob I'm work for a I work for a small um defi company called Lindy labs and I'm basically working as a formal verification researcher there um my background is in type Theory and in interactive theorem proving and in mathematics um and I'm the maintainer of egis um a small tool that we've so far only tested on our own source code it's a formal verification tool that can be used uh to verify y contracts um written

in Cairo um Cairo is the language that powers the starnet L2 um and if I have time I will um talk a little bit about eges at the end as some some some sort of example of what can be done using the lean theor improver as a basis um but since I was invited to give a general introduction to uh lean um here we go first um so what is lean um lean is a project which has been founded in 201 12 so roughly 12 years ago uh by a guy called Leonardo deura who had formerly been

working on um automated theor proving I think you saw the uh difference between interactive theor proving and automated theor proving in an earlier talk um and lenus on the interactive side um it's dependently typed um um which means that the return type of functions can depend on input values broadly speaking um which puts it in the same class as other interactive theorem provs like Co and ACTA if you know a little bit background but if you don't don't worry um this talk will basically assume no pre-existing knowledge about interactive theorum improving um and it's both a a functional programming language and a

theorum um the theorem is written WR in itself um it basically compiles itself and um that makes it auto automatically makes it a good tool to deal with programming languages and that's a bit of the gist of the talk that I'm I'm giving is that not only does it have like a proper good performance as a functional programming language not only can you trust it to be correct because it has a very small and easily verifiable kernel but you can also extend it syntax quite easily um and uh that's what we're going to do in this uh life coding experiment um and it's been designed with formal

verification in mind but also with formal mathematics in mind I think the biggest user group of lean is actually not people from formal verification but it's mathematicians who want to verify their proofs um and that ranges from like super simple stuff to like the most abstract uh complex stuff um and as I said this this talk is going to be like like one step more meta than the previous talks it's a I'd say it's the perfect tool to build formal verification tools on um barebone lean itself is not is not a formal verification tool because it doesn't have baked in um Notions of semantics of various programming

languages um so I guess I'll quickly go over some success stories of lean um one success story being um the so-called liquid liquid tenser experiment where Fields medalist mathematician was not really sure about one of his uh proofs which involved super technical arguments and um then uh called for help with the lean community and they managed to within a few months actually verify and simplify his proofs and that's kind of been the like starting um point for many of mathematicians being inspired to lose to use lean um and then a few stories from this year um AWS so Amazon um uh uses uh

uses lean to to do a lot of things because like the main developer is now working at AWS um there's a certified differential privacy library in lean um and maybe you've heard in the like broader media um from a of a project called Alpha proof um that's a that's a proof tactic for lean which has been developed by Deep Mind um that's actually been used to um be so good at mathematic problems that it's actually solved a silver metal at the IMO at the international mathematical Olympiad which um if you know anything about the IMO is a pretty pretty um great

achievement um the lean e EOS system um mainly consists of lean itself obviously uh which as I said is self bootstrapping so it's written in itself um then there's a standard Library that's uh been managed by the lean user Community which is called batteries because it's like the batteries included version of lean um then there's the big monor repo that's uh that contains most of the mathematics formalization so that's called math lip um it does have a good package uh Rec registry uh called Reservoir and it's called Reservoir because the package manager for lean is called Lake um um so so far for the ecosystem um if

you want to learn lean um this hour obviously isn't enough to um give you any more than just a climp glimpse of what you can do with lean it doesn't it it actually cannot serve as a tutorial with just so little time um but there's a few nice resources there's a um a game that runs in the in the browser that's called the natural numbers game which um can serve as a first taste of proving statements with lean um in the browser without installing anything um so that's that's a first good step and then if you're looking for more like a proper documentation um there's a um online

book called theor proving in lean and one called functional programming in lean which uh respectively highlight the use of lean as a theorum and as a functional programming language um and those two categories are are not really um distinct because you can improve lean's performance as a theor impr by writing your own tactics by writing your own Automation and um so you can use the functional programming aspect to improve the theor proving proving aspect and you can use the theorem proving aspect to do something like um um verified programming where you where the programs

you write in lean are actually correct by construction um then there's a good textbook called mathematics in lean which is obviously more aimed at mathematicians and then I think the best resource for any kind of questions about Len is lean's zulip server which is just a huge beehive of uh activity and um I think it's the most active uh zulip server in the world and it's should be the first point of contact for all kinds of questions you have on the lean theorem pver um so yeah um like if I would uh give it um like a CR in one sentence I would say that compared to similar tools lean

strength is its extensibility for the syntax and its ability to pretty easily connect to external tools and that makes it a a good a good framework um to write your own formal verification tools um and so what we're going to do today is um to do a little bit of live coding and um different from the previous um live coding um demos that you've seen um I actually um mastered up the courage to um do it from scratch um I do have a GitHub repository where all the contents

of this uh demo um lie and I will maybe uh revert to uh restoring some of the contents from this um from this repo if my life coding deviates Too Much from the test runs I did before um so yeah what's today's agenda is that we will look at a very small example language um not a language that you want to would want to write any programers with um in its syntax into lean and then equip um the syntax with a formal semantics so with a meaning inside lean um as a way to interpret um the effect of those programs in the

theorem Prov and then we will write a very very very simple um optimization for the semantics and maybe if the time is time remains also verify a super simple program uh written in this language okay so what what does the language look like that we want to embed in lean obviously we don't have much time so we can't um look at a language which has like 100 uh uh constructs so um the statements of the language um just fall into three categories there's assignments there's why loops and there's if L statements as you can see with the two um examples shown on the

right um we just assume the memory to be flat untyped and mutable so we just have for each string for each variable name we have one value um we have no types like we assume everything to just be like a um 32bit um um integer and um because we don't have we don't want to be writing down all kind of all kinds of binary operations um we just restrict ourself to two um to two expression formers which are just um apart from obviously constants and variable names um a less than operator and an addition operator and so what

we'll do now is um we call this language imp because it's a small imperative language um and our goals are now to to embed the syntax of imp into lean and to implement um and prove correctness of a small optimization and um to then uh be able to verify programs we will also Implement a big step what's called a big step semantics um for this language if you don't know what a big step semantics is um no worries we will basically you will basically see on this example what it what that means um okay so much for the slidy part of this presentation um now this is this big

enough um is this big enough okay so um if you remember the first bullet point was um to define the syntax of imp um and what we would what we want first to do is to Define an intern representation of the syntax within lean um that means that we will um Implement what's called an an abstract syntax tree uh of this imp language um and this goes by the means of just defining IND inductive data types um that consist of all of the elements of this language thankfully there's only two basic

constructs in the language namely expressions and statements and so we will have an inductive data type for uh Expressions which we call exper and an inductive type for statements which we call stmt um so inductive types form the foundation um besides functions of lean as a language and if you've not seen if you're not familiar with functional programming it's basically a generalized form of something like a a struct or an enum where you can have you basically list all the ways of um creating of constructing terms um for these types um

and so for the expression data type um we want to list four of what's called Constructors for this type so um remember that um for the Expressions we have constants we have uh variables um we have addition and we have less than that's all we need I mean we would need more to write a reasonable Pro program but but that's all we want to deal with today so um let's first deal with constants let's just call the first uh Constructor const and um now we have to list the arguments for this Constructor and um const should just take um a bit vector and because we maybe uh don't

want to repeat our basic data type again and again let's define the type value as the type of bit vectors with 32 bits we could also Define uh like a programming language with infinitely large integers and so on but okay that's what we're what we're going with in this example um okay so const should just take a value V of this data type and then we need a Constructor for variables for named variables and we just want to um we just want to identif identify them

by their variable name so by a string um and now we need the two binary operations and uh the trick here is that uh these form what's called recursive Constructors so we have one of them that's called LT and that's got two arguments E1 in expro and E2 in expro so it takes two expressions as arguments and the same goes for addition note that we will just will just um Implement LT as a um operation that just spits out zero or one just like in C for

example okay so that's the um that's the data type for Expressions now let's Implement a data type for statements um the most basic building block is obviously an assignment um as we've seen here like all these lines that end with a semicolon and that colon equals are assignments um and what do they need as arguments they need a variable name on the left hand side and an expression on the right hand side so we again give it an argument s u as a string for the left hand side and an expression for the right hand side um and

then we again need a recursive uh Constructor because we need to um Cobble together several of these uh of these assignments or other language constructs um so we want to have some a Constructor for this sequential um execution of uh two statements so we have um S1 and statement and S2 in statement that will allow us to chain more than one statement together and now we have if then else um that takes the condition that's an expression and it

takes the then Branch that's a statement and it takes the else Branch that's also statement and then we have y Loops which also take an expression and the body let's just call it B statement and now that we Define these types we can basically internally represent uh for example the assignment where we assign I to Zero by um statement do assign um what did it

do and now if we have it here we need a string here so this would be I and this would be zero oh no this would be like the variable called zero uh no on the right hand side what we do we want a con con and because it can't derive the zero we want to make this an abbreviation instead of a definition those are AR the so those are the details I actually didn't want to talk about but those things happen when you do these kinds of things live okay so this is what we want to uh represent a statement in the in

the Imp language internally um but we also really want to be able to write the syntax exactly in the way that I've presented it on the slides and that's now where the extensibility of the lean syntax comes into play um so the lean parer is this huge big thing that basically passes everything that I write into this editor and we can extend it live as we are going so we can extend the language that I'm using uh live basically and we first want to um for the par I want to introduce um new non-terminals for the paa so we do that by declaring

a new syntax category and we just call them the lowercase variance of those two those two things like one we call expression and one for the statements so that's new syntax categories and now we want to basically look at this and basically uh just build a parza for each kind of uh language element in here and we go through all of those eight Constructors now okay let's start with expression um so the first two are actually okay I'll I'll start with LT and with ADD because they may be a bit more intuitive and we just write

syntax and expression and a less than symbol and expression that should be a new expression and syntax expression and an add sign it's a new expression and now for uh the variable names we just want to reuse the the syntax category that lean has for its own variable names and we just do that by by saying okay the identifier which are called ident in lean should also be an expression and we also want to use uh numerals so we write newe as part of Expressions okay so much for the

Expressions now we need to do the same for the statements um um okay the assignment um what's it on the left hand side we have a an ident and then we have the colon equals and then we have an expression and that's a statement and I'm actually lacking the semicolon at the end of the line and this sequence is basically just statement followed by another statement is a new statement and the if then else that's a bit of typing here so we have an if then

we have an opening bracket then we have the condition um then we have the then clause which is a statement and then we have the else keyword and then we have curly brackets again and then we have not the N next statement and that that should be a statement again so that's been a mouthful um and the same for the Y Loops the while keyword and some curly brackets the statement should also be a statement okay um also note that this would be the point where for the language we would set the precedences of um of uh for example for the for the

addition so we could uh determine whether the addition would be a left associative or right associative because we can write something like a binding strength here um okay so the next the next uh step might seem a little bit arbitrary because now we can we can uh we can form all these Expressions but we want to have a way to reflect them back into a syntax category that's already used in lean so what we do is uh we write syntax and then we can basically turn every expression into a term where term is the

thing um that um the syntax category that uh lean uses for all of the terms we can write down and we do the same for statement and what we can do now is let's check uh something like statement uh I colon equals z and then that's already good because it already has passed this and now we get an error message that just says elaboration function for this has not been implemented that just means that lean doesn't yet it can parse it but it doesn't yet know how to equip it with

any meaning that's relevant for lean um we could also evaluate this and put it in in quoting brackets why doesn't this work um right I want toate this actually or let's not do this okay so that that's that's for the syntax we saw the the arrow message so now we basically need to reflect the syntax that we declared to the abstract syntax tree so this is our abstract syntax and this is the syntax

declaration and now what we what we want to add is something called macro rules that basically take um something of this form and turn it into a uh into a term like this um so for example um we match um on a [Music] numeral then we just want to have expression do con um and then um what is

this okay now now my stage blindness sets in okay let's just start with a with a different macro um let's uh start with the addition so we want to this to oh yeah now we need we need to um surround this with um so actually what I completely forgot is that we want to have the brackets around here

32 minutes and um yeah so I just noticed that this will take a while because for every Constructor I will basically now write one of these macro rules that will expand um the minimal form into the full um into the full form that's inter that's uh of any meaning to lean and so I just did the magic trick of

restoring this um to not waste too much time on this um so we see that for every of the uh of the language Constructor we have one uh one of these uh macro rules um and now what we can do is um if we if we now check this then we see that x + y is less than Z gets translated correctly um to the A um so these guard messages here are just a wave to tell lean that it should um

not output the actual output of the next command but just check should check that it actually matches what's in the comment above that's actually quite a cool feature to um to embed test cases right in the in the file where you'd um Define them um so yeah now we can we can write something like this in lean so we've actually with just um okay it's a two-digit number of lines we've just embedded a small imperative language as some sort of DSL inside lean um and um yeah so we can write down programs and um have a representation in

form of this um as um obviously we still not really got like G gave any meaning so that's what we um going to do next um let's uh next uh write a definition that actually evaluates an expression so it's an it's a function that takes an expression uh and should return something of the value where does it and since I restored this from the GitHub repository I'm now at a version

where I have not defined the value so we've do that again value say that this is bit vectors of size 32 and um actually need this and now we've we need to go through all of the constructors of Expressions um so for constants uh this is super easy because constants already have a value and so we just evaluate them by returning this value um and then the next um let me leave out

variables for a while and go to less and then so less and then of X and Y and now we do a recursive call so we um just say that if eval of X is less than eval of Y um then uh one lse zero now it's saying okay there's two cases missing the plus and the variables let's do the plus first um and that should just be like the evaluation of X plus the evaluation of

Y and for the variables now we uh we notied that what should we do with variables and um the way this is done that is that we need a a context of variables so we need U for the evaluation we need a mapping from the variable names um to the uh to their value and we can also like with the value here we can do a type definition and just say we say that context we can actually wrap it into its own structure and say uh it should just consist of a map for

Strings uh to Value so in a real programming language we wouldn't just have a map here but we would have something like a hash map um because we will always only store finitely many uh um variable names at at each point um and now we can implement this you can say that okay the variable should be and now what do we have here um we still haven't any context so the evaluation will always happen if some in some context Sigma um and now we also have to retrofit the

sigma everywhere okay um and now this might also be the point where we um should um Define some operations on the context so for example getting a um the value given a variable name um should be a value and that should just be oh because we need so we need a

context everywhere here so we can just say Okay this should be just be always Sigma should always be a context just write this here um and this should just be the map that sits inside the context and we should apply it to S and likewise we need something we will later need something like set where we can assign something in the context to a certain value um and so here we need to say what the this should be a new

context should I shall say what the new map is and this is just if um so for each for each uh let's just call it uh S Prime so that's now a new string and for each and for each S Prime if it's the the name we are overwriting so if s equals S Prime uh then it should return V and otherwise it look up in should look up in the

context um the term at s okay um and we'll just in a moment uh prove some our first theorems about like getting and setting variables in context um but let's first uh complete the uh definition of the evaluation here um because now we have the context at our disposal we have a variable name let's actually call it s be a bit more consistent um also we've included this everywhere so we can actually leave this out

um no no right we can't um so we need to look up in the context um what's it s um but we need to look it up in the context called Sigma um okay to test this let's test this actually um we also want a function that basically initializes a context to a certain default value maybe zero let's just let's just pick zero which should just be the context

where for each variable name it should just be zero now it says okay we have not used this variable name Leen is very strict about uh using every variable name otherwise it will get you give you a warning um and now we can test this let's uh write eval of oh so this is lean's eval this is no like uh from a dactic teaching point of view bad bad namings but this is not this but we want to evaluate the function called eval um what context do we want to have we want the context in in

it and now we have to give an expression and let's just we can use this dot notation when it's clear what kind of type um a certain term should have I hope you see that on the on the right hand side um it's uh that's a very central point of almost all uh intera theum appr it will show you the the the goal that we're about to prove when we approve something and it will also show you the type of the holes that we've uh put into uh into the editor on the left um let's just add five to the variable I and now we see that we've

actually have the um yeah we have this bit Vector as a result so now we've interpreted um we've interpreted the um uh expressions in our in our programming language imp um so that's good um as I said we might want for later purposes um to actually have some theorems about getting and setting variables in the context we might actually write our first

LMA um and let's just call it context of get set same which should just be a LMA that if we um if we add a context Sigma get uh s uh s after setting s so this should actually be Sigma do set S V that should just be the same as

V what's happening there oh I saw um okay and um now we can type buy and that that buy keyword actually changes from lean's so-called term mode uh to lean's tactic mode so here will we we will be able to write a sequence of what's called tactic and tactics are are basically a way of manipulating um the current proof goal um so this this is basically our proof obligation

now and every proof you will do in lean um basically consists of just a serious of getting this goal closer and closer to something you can prove trivially um and in many cases you will be able to just call the correct tactic and prove it in one step um I will not have the time to show you any very um involved tactics today but there's tactics which are basically implementing a best first uh tree search there's tactics which um do um something like um smt solving there's tactics that are AI based and basically look at different proof structures and

try to recreate the proof structure of your current goal um there's tactics that are very tailored to certain um to certain data structures for example um whenever we want to prove something about Rings which is very important if you do any cryptography uh verification um there's very sophisticated tactics that just normalize a ring expression for example um but so in this case obviously this Lama is is super trivial um we will want to call a tactic called simp which just simplify stuff and we can give it a list of

definitions um that it should unfold so we just say Okay unfold context doget and context. set and then we get this this good error message here no goals to be solved um and with all of these interactive theorem provs they don't necessarily give you like a u oh you solved all the goals message but the rule is basically if your if your compilation in the IDE goes through then you've um manage to solve all the proof obligations and then in Le you have something like uh if we hadn't wrot written this we can write something like so something like sorry which basically tells lean

okay we are able to solve this but we'll not do it now we'll do it later um so yeah that's that's our uh first theorem and what we can do is actually tell simp to automatically apply this kind of theorem and we can just annotate the theorem with simp um and now we will be able to solve any kind of it will be able to reduce any of this any of this term by just v um so yeah you should always be always only do that if the left hand side of inequality is like more complicated than the right hand side of an equality

equality um okay let me look at my curriculum um yeah the next step I don't have much time left um but the next step would be maybe I'm just I just restore everything and then I just walk you through the code um um so yeah um we're now in a in a in the state where we've we've done all that we've proven those lemas um and now we want to write our first

optimization um and that optimization again for the lack of time can't do anything super sophisticated but what it can do is something called constant folding so if you have an expression um that for example in a less than expression or in a addition has constants on both side it can just already pre-evaluate um before running the program um and that's what constant folding does and it actually propagates recursively this kind of optimization it's a very weak optimization but it's it's part of every of every good compiler and so we can just Define this

this as a recursive function from our Expressions into our Expressions that just does nothing on constants and on variables and for example on less than of X and Y it just recursively optimizes the left hand side and the right hand side and sees if both of them are constants and then it replaces um it with the final result so this is a this is already something you could call a compiler optimization um and now obviously what you want to do if you're if you're writing a compiler um you might want to prove that um it doesn't change the outcome and for Expressions that would mean something like um whatever environment we have

evaluating the unoptimized expression in this environment is the same as evaluating the optimized expression in this environment um and this again is a proof so we can say buy and then we get a uh a proof goal which is just what we stated um and then we can call a tactic that's uh called induction which just um applies induction on one uh on one variable and now we see that we don't not only got one goal but we've got four goals that correspond to all of the four cases to consts variables to plus and to less than and now we can actually add act on each of these uh cases separately

so this would be a very structured proof where you can actually you give case names and then for each of those cases um you find ways to actually get rid of all of the goals it's a bit like a computer game and if you play something like the natural number game um you can see that this can be very addictive to just hack away proof goals um obviously this again is a pretty trivial um trivial uh proof and you could also just solve this as a oneliner um either with a research or by Just For example yeah just just just uh concatenating several simplification tactics

um so yeah uh this is basically the proof that optimizing um with the function that we've defined here doesn't change um the value um okay um so how do we give meanings not only to Expressions but to entire programs um let me introduce something that's called a bigstep semantics so if you're um if you're familiar with formal verification or with programming language Theory U you will already know this but um it's one way of giving um giving meaning to programs that are

potenti potentially uh non-terminating like the programs in our imp language because we could have non-terminating programs there we can have just have while one and then Loop forever um and because lean is a total language we can't just write a total function which tells us what's the um what's the outcome of running this program in this environment because it could never terminate and never give us an outcome um and so one way to circumvent this when arguing about proofs um is to have a inductive predicate so a predicate that takes an environment which is being seen as the

starting environment uh the program which is a a variable of the um of the type stmt and an end environment and basically it's a it's a statement it's an inductively generated statement that tells you if I run the program if I run this program in this starting environment it will terminate in this end environment and um so this is an inductive predicate so we will list axio axioms that will tell us several ways of proving something about this big step relation so it's basically a relation with three inputs like a starting State an end State and a

program and um the uh construct for this relation basically looks like something like this if we start um in in a certain environment then the skip program which I've I've missed in when I first did the syntax I just I just noticed um yeah so we just missed the empty statement the empty program which is super important because otherwise you can't um yeah um so if if you have this program and you start with the with a with a state Sigma um then you end with a state Sigma and for example the sequential

composition states that if you start in Sigma and the program S1 brings you to Sigma Prime um then if a program S2 brings you from Sigma Prime to Sigma prime prime then the sequential Co composition of S1 and S2 brings you from Sigma to Sigma prime prime um yeah if you stare at it for a while it uh seems reasonable um and the assignment basically says okay if you start in a certain environment then the assignment has the exact effect of setting this variable in the environment and here it actually calls the evaluation function that we've written for the

expression um then we have two cases for the if then else depending on whether the evaluation of the condition is true or false um and then the semantics for the while loop um are a bit more complicated they have one easier easier case for for the false case so if we evaluate the condition um and it returns zero then the state before the execution of the Y Loop is the same as the state after the execution of the Y Loop and if the condition actually evaluates to something which is not zero so that

means that we will execute one iteration of the Y Loop then we can do something which is called Loop unrolling which basically says that if the body of the Y Loop brings us from Sigma to Sigma Prime and then the whole y Loop brings us from Sigma Prime to Sigma prime prime and then the whole y Loop will also bring us from Sigma to Sigma prime prime um again this is maybe a bit abstract but it's like it's the way you can prove things about uh y Loops by continually unrolling single iterations of the while loop from the start and you will also like with like with contract you will be

able to um not only um prove statements about finitely many iterations of the Y Loop but by induction you will also be able to prove um what happens after an arbitrary unbounded um iteration of this y Loop um let me just show you um maybe this little example it just happens to fit on the screen um so let's let's write a super simple program that just um wants to swap the values that are in I and in j I guess that's

one of the like first steps you would do in C or something like that as a uh kindergartener um and you would do that by taking a third variable Z and um um assign I to Z and then I to J and then you can assign J to Z um so you can actually do the swap by having one extra variable um and then we can for example uh prove that this actually swaps the two variable so for every for every inv two every pair of environments before and after the

execution um and the statement so this is an hypothesis lean doesn't make any difference between hypothesis and variables that you put as assumptions for for theorems so these are just two two variables we want to the theorem to depend on and this is is just a pre precondition just a hypothesis we wanted to depend on so if um swap brings us from Sigma to Sigma Prime then it will have the following obvious effect um if we if we call if we probe if we probe Sigma Prime at I we get what Sigma gets us at J and if we probe Sigma Prime at J um we will

um get what's previous previously been I um and uh let's make this a bit more transparent so this is our proof goal and uh so what we have to do is act on this hypothesis H um let's first just unfold the definition of swap in ag and now we've seen that we've have a little inline view of this little program here um and what we then can do is um again this can all be automated it's just like for showing you what happens inside is if you if you apply a tactic called cases

on this thing then it will look which of the cases that we've listed atically above can actually um can actually uh be fulfilled in this situation in this situation the program just consists of a series of of sequential um assignment ments so we can perform cases once and now you see that here we got a new uh hypothesis which just concerns the first line and there we got a new hypothesis just which just concerns the other two lines um and because lean is very meticulous about variable names it puts these uh gravestones to all of the variable names

that we've not given an explicit name um and so we can per form these case destructions um again and again um and then it gets actually it gets very gets very noisy here um if I do simp it actually gets less noisy but still a bit hard to read um and now this is actually a conjunction so this is an end statement so you can write down Constructor and now we get two goals one for the left hand side of the end one for the right hand side of the end and you can just call the simplifier and it it will actually prove that this actually is correct

um yeah I guess that's as much live coding um as you can do within an hour um like obviously it wasn't all life coded it was hilariously optimistic um but so going from a like tiny toy language um to an actual language which is used in defi now that I have like two minutes left just skipping over really quickly um so Cairo is the function as I said that runs Stark net it compiles through an intermediate representation called Sierra which is very which has a very easy syntax and it always compiles through what's called a single static

assignment form so we can very easily load this syntax like we've seen today into lean um and I've actually written this this egis tool which basically just lets you type into lean okay let's just load this Sierra file and it then provides uh to the user uh commands that allows allows the user to give a specification an arbitrary specification for each chairo function and to prove that this specification actually is correct and by the end you have something like EES complete which is you put it down on the on the last line of your big theor file or of your number of the theory files and it basically checks that you've given a specification and

proved a specification to every uh single function that your smart contracts includes um and we've actually dock fed this to our own uh product so this supports Loops it supports the Cs calls in starnet um and we've um let me end on this horrible slide um in terms of in terms of design I mean not in terms of content so um our own our own um defi Landing product has a white paper which lists a result from mathematical branch called control theory which

basically con um implements a uh controller which determines the global interest rate modifier um according to the formula you see in the first line here you see that it's a nonlinear formula because it's got all these exponents and it got square roots and the white paper obviously implicitly assumes that we only deal with infinite prec Precision numbers in uh in this formula um and what we've done is we've actually managed to verify that if all of the variables which are in play here stay in reasonable bound then the entire update operation like this is

an update operations which which runs regularly on the contract um then the error the numerical error of this is also bounded and so this is what this is the spec you see down there um and yeah we're beginning to um verify more of our own code and um we'll probably be ready to completely uh verify um arbitrary chiro Contra contracts with this um um and give it more uh assurances that um I guess no other tool can actually give because you can actually compare it to something like infinite Precision uh um numbers and um you can use the entire power of the mathematics that's been

formalized in lean to write your um specifications and your proofs and I think I'm over time and thank you for listening um I'm happy to take questions afterwards [Applause]