Clear: a Formal Verification framework for smart contracts in Lean by Julian Sutherland | Devcon SEA

[Music] hello well my size ah perfect yeah yeah um cool yeah so I'm uh going to structure this talk in I guess three parts uh the first one is I'm going to sort of explain what is clear how does it work and why would you even use it I guess and the second part will be showing a a fairly straightforward and simple Le uh example of the use of clear um let's and then and then afterwards I'll be sort of walking you guys through a more complicated example that sort of a uh nigell style I made this earlier if you will so that's a very British reference but there you go anyways um cool yes so as I said I'll start off uh talking a little bit about the uh clear framework so the the first thing is that so clear is a formal verification framework and the first question I want to answer here is well what even is uh formal verification formal methods all of these words what what do they mean right and so uh essentially formal methods are made up primarily of well two plus one part which we'll see in a second which is where we have the language semantics part of it which is studying actually the meaning of programming languages what the oh I need this oh I see it's not cap I see okay sorry let me re redirect that can everyone hear me now okay perfect cool sorry about that so uh so the first part of it is a sort of language semantics so studying the actual meaning of programming languages so that we can reason about them and then there are programming program Logics which are allow us to actually then reason about the semantics of individual programs prove that they have certain properties and these sorts of things um and yeah you I mean some of these you guys will be quite familiar with because actually a very simple example of a a program logic is actually a type system so it proves some very simple it actually proves some very simple properties of your program at compile time where it's proving that hey this variable will always have this structure because it's of this type this sort of thing uh but then there are more more advanced sort of uh Logics where I mean some of you which who have done rust might be familiar with linear types and separation logic is related with this uh and then there are temporal Logics for proving uh you know uh liveness and safety properties and these sorts of things so but all of these all of these Pro these program Logics typically the proofs that we write in them are quite complex and involved and so if we want to have any sort of degree of certainty that these uh the proofs that we've written are actually correct we actually want to also mechanize these proofs so put them in a format where they can actually be uh computer checked right and so there are sort of two schools of thought primary schools of thought on this one of them is the automated theorem proving Direction uh which is looking at sat solvers which I think most of you will have heard of smt solvers TP tptp these sorts of things where um where the idea is essentially you give it a theorem to prove and it tries to automatically prove it for you uh the other side of this coin is the interactive theorem proving Direction which is actually more what my team does and what more what clear is about where and I'm going to talk about this a little bit more on the next Slide the the point is that obviously the well there's still a reason that we need human mathematicians uh to reason about things and so for you know straightforward for for simple to medium complexity programs or automated theorem proving will often do what you need but if you want to do something really complicated so say prove the soundness and completeness results of a a ZK protocol or something like this right there a lot of complex mathematical facts come into the into reasoning about this and and that's where interactive theorem proving will come in because you need sort of human intuition and human information to guide how to structure that proof a lot more right and of course there's a lot of work and this is I guess ongoing uh and and get sort of becoming more and more used is there's a lot of work also about creating Bridges between these two uh these two worlds in in either direction right so there are there are various techniques now that are looking at uh using smt solvers but then if there's some sort of coric case that it's not able to handle being able to extract that in inter interactive theor impr for human to be able to verify it and the other way around where if I'm rising my proof and interactive theor and I come down to some sort of simple case which is uh uh you know a little bit uh which is a bit annoying but which is sort of labor intensive but something that uh an automated theover will be able to discharge very quickly there are now various techniques for extracting things from interactive theor improvers into smt solvers to try and then actually verify that um give me two seconds I'm seeing that the demo I wanted to show a little bit later is uh currently not compiling so I'm just going to quickly rerun that it just needs to just need to press one button perfect cool it's now compiling the background which should Poss plug this in at some point but yeah I will perhaps I'll I'll grab it in a second sorry about that um but yeah so anyways so those those are the sort of two main schools of thought and as I said there's now some work on sort of making these two interact um and so so really fundamentally the trade-off between this automated theor improving and this interactive and interactive theor improving is a trade-off between Automation and speed like Automation and speed versus uh expressivity anding Power right so an typically if what you have if the thing that you're trying to verify is simple enough for automated theor improving then you should really go that way because it's a lot faster requires a lot less uh human interaction right but there are some situations and there are there are fundamental reasons in computer science why there are some situations where you are really are going to need the uh expressivity of interactive theor proving and uh in particular as I mentioned in the panel earlier today I do think that for certain important parts of the um what do you call it of the infrastructure of the ethereum ecosystem in particular this will be quite important as I've already mentioned uh ZK protocols uh consensus layers all of these sorts of consensus protocols all of these sorts of things and so the the reason for this sort of necessary tradeoff is this thing called Rises theorem essentially uh it's a theorem about about the uh limitations of deciding whether the specification holds or not right and what it says is so firstly we have some set of program programs right and we have a set of states that these programs act on and we have uh an evaluation function which basically says given a program and initial state it evaluates that program in that state and it spits out the uh the final state right and then finally we have a predicate which basically decides uh is is our specification right and it tells us hey does this it's a set of programs that satisfy essentially some specification that we care about and risis Theorem actually says this which is if I have two programs F1 and five 5 2 if they are what we call extensionally equal and the definition of that is at the bottom it basically says that if these two programs when run in the same state will always give the same result right then it is the case that uh essentially that then we know that uh p is on the sorry so if our our sorry if our predicate doesn't essentially care so if for two programs which are essentially equal this predicate will always also hold or not right then P must be undecidable and so essentially what this mean so let me give you a couple of examples of you know extensional equality to sort of motivate this a little bit right so you can think of like there might be multiple ways of uh implementing like addition right so you might have like a primitive notion of addition in your CPU you might do like piano style addition where you just have a loop you want to add a and b and you have a loop where you add one to a b times right uh or you might have something that where you add B+ one to a and then you subtract one or something like that right and all of these all of these um uh all of these programs are extensionally equal so they have they're different implementations but they have the same uh Behavior with respect to what they return right and so Rice's theorem says that essentially if I have a predicate that only cares about the behavior not the structure of the program then it is necessarily on theci side right and so this basically places a fundamental limitation on uh on on what can sort of be proven entirely automatically right and so of course we can sort of uh we can stack charistics and these sorts of things to be able to extend this as far as possible but at least for the moment uh I I think interactive theor proving still has uh a lot of place in the uh the verification of some of the more P complex pieces of infrastructure within particularly the ethereum ecosystem but also more broading okay cool um so now what actually is the uh the ca the sorry the clear framework it's a framework for formally verifying smart contracts written in languages that compile to Ule so obviously for the moment as far as I'm aware that's basically solidity and Vipers it's not a a massive set I put a dot dot dot there I'm sure more coming but uh that's all I'm aware of for the moment um and so what what does it do so it basically allows users to write computer checked proofs of the uh of the correctness of their uh of their smart contracts right and in particular all of this is done by extracting the semantics so we have a formal semantics and we go into this in a little more detail shortly but we have basically a formal semantics of of this ual intermediate representation which is us used by the cility compiler um in in in the lean proof assistant and the lean proof assistant has has this Library called mathlib and mathlib is as I said earlier debatably has the largest formalization of uh of of mathema IC in proof assistance and existence right so hey you need the Schwarz zipple Lama to be able to prove the correctness of your ZK ZK protocol well we've got you right uh and and and you know a lot of uh other techniques wouldn't be able to handle this it also has one thing that is quite unique about uh about particularly the lean proof assistant is that has uh remarkably and and I'm going to say almost uniquely uh extensible automation system so if you need new automation new proof automations you come up with new horis to automate your parts of your proof and these sorts of things you can actually just write that in lean right so you can just integrate that into your proof assist you can write your new decision procedure and then you can run it whenever you want so this allows it to be extensible to all sorts of domain specific areas where you may need new uh automation so for example my team has embedded some like decision procedures for finite Fields when we're reasoning about like systems of um of polinomial constraints and these sorts of things and we we've embedded these new decision procedur into lean and we're going to see some very basic embedded decision procedures today that deal with like looking up variables and these sorts of things so very basic stuff but nonetheless all of this is done in lean doesn't require and you know can can be straightforwardly encoded into the language and the final thing and this is something that I find to be uh that I really enjoy about the the lean proof assistance particular is the the it has a very powerful notation engine so um it's essentially and I I did say this in my uh panel earlier but essentially it allows it has a pre-compilation step where the um the the the the what you call the programmer the lean programmer can basically essentially give arbitrary semantics that they desire to an arbitrary string of unic code right and so essentially I can embed pretty much any notation that you can think of that is embeddable into unic code uh inine and so that means that actually most of most modern mathematical notation can be embedded very straightforwardly into lean and that means that unlike previous proof assistance I can um I can write my uh the theorems that I'm proving in a format which is completely understandable to mathematicians right and and and can be made completely understandable to uh to like people programmers and these sorts of things right so we can basically we're able to uh explo exploit this notation engine to allow the specifications that we want to write to be written in basically whatever format the our target audience is most familiar with right so if you're a mathematician and you want to see you know lots of uh and and you want to see whatever notation that's fine but also we can write specs as just like normal tests and we want to prove that this test can never fail for any sort of inputs right both of these things are fairly straightforwardly possible uh and the other thing the other thing is that uh proof assistants are uh by by well not by their nature but rather it is fairly straightforward to make verification inside of a proof assistant modular right so what do we mean by and what do we mean by modular so that means that we can sort of split up a complicated program that we have into lots of small subprograms the functions Etc and be able to reason about these things independently write a specification for my Loop my function whatever and then be able to use this to abstract that when reasoning about things that use this function use this Loop Etc and this this allows for scalable reasoning this allows for proof reuse right because obviously say the solidity compiler generates a lot of uh I'm going to say um a lot of sort of generic functions so there are like functions that check for uh arithmetic overflow there are functions that obviously compute your index into storage memory when you're using a storage array uh a storage map rather right and all of these sorts of things and uh the we can basically just pre-write proofs for a lot of these things and we've started on this um and and and then basically these can be used reused in whatever context by whoever wants to then verify their smart contract that happens to use these uh these uh Primitives and then the other the other sort of uh very interesting thing is that also I think this is becoming a lot more interesting in the the sort of context of uh uh what do you call it uh of uh of like l2s right is that l2s and their the rollup contracts associated with l2s are essentially interacting with a like a a complex external system that has complicated interactions and semantics and and typically actually we want to reason about an interaction between these complex semantics in the L2 and the actual uh L1 contract it's uh and the the the L1 contract itself and so in typical like uh in sort of typical smart contract reasoning Frameworks that exist out there this ability to extend things to be able to reason about what's outside of this world what's outside of the evm is uh I think uh very is very powerful um and and then finally the other thing is that unfortunately in this trade off uh on the side that we are I'm going to say that there's a a relatively High entry barrier so typically you want to have at least a fairly strong background in functional programming no bit of logic and all of these sorts of things before you're able to really seriously use these things now we're hoping we're hoping to actually introduce enough automation here so as we said access to smt solvers tactics and these sorts of things that it may become feasible for humans for humans I I am human I assure you so but uh for for people who aren't e domain specific experts if you will to uh to actually be able to use these things and and I'm hoping that uh that uh if if my demo will starts working which I'm going to have to look at in a few minutes uh I'll I'll be able to actually show some of this off today so yeah we'll we'll we'll see how that goes perfect cool um okay so then now what actually so what is the clear framework actually made of so I I already mentioned that we actually have a formal model of uh Ule so Ule is a we're going to actually see a very short like intro to Ule so Ule is just a very simple imperative programming language that in particular has a um uh has basically has you know the control flow that you would expect you have ifs you have loops you have functions all of these sorts of things switches uh as well as being able to assign variables to expressions and these expressions are written in terms of constants variables and uh and in fact the sort of the subset of the Primitive operations of the evm right and so essentially what does it do it means that it abstracts the use of the evm where you the human being doesn't need to explicitly reason like a stack machine when they're reasoning about the control flow uh while still being at a sort of a very low level of abstraction and actually having fixed semantic and this is actually a very big uh issue overall when you're reasoning about smart cont like evm smart contracts as a whole which is that uh well most of the high level languages don't have fixed semantics right so the the formal semantics of solidity is basically whatever the solidity compiler says it is at that point in time uh and that's obviously is is not ideal in terms of reasoning um and so so here we kind of to be able to have a a trust base that we can actually have any degree of uh confidence in we uh what do you call it uh we basically need to compile this down to a low level of abstraction which is well we don't want to compile down all all the way to the evm because well we tried that and uh humans are not and this time I really do mean humans humans are not Mentor reason about stack machines it's uh you know there's a a lot of cont contextual information which is continuously changing as you push and po pop things off the stack of the stack and it's just not practical so uul offers like a good level of abstraction where it does have fixed semantics while uh also being at a high like abstracting enough of the control flow that it's not you know I'm not torturing my Engineers by making them reason about these things so that's always great um so okay so we have this formal semantics ofle and actually as we said it shares these primitive operations with the evm and actually we simultaneously have uh a formal semantics of the evm and in fact they actually uh they actually share the implementation of the prim Ops and why why is that good uh well because actually our evm model is uh modulo certain details which we we sort of fill in uh is actually executable and so I can this is actually a formal model that I can actually run against the conformance tests right and so by doing this by actually running the evm model against the conformance test I can have a very high degree of certainty that my uh my model of my evm Prim Ops are really what uh the community and the execution clients believe that they should think that they should be right and and so for actually for the moment we have I think around 90% of the conformance tests passing on our evm model which is not bad but obviously we're hoping with this is ongoing work and we're hoping over the coming weeks to actually achieve 100% although it is one of those like 8020 things where like getting most of it is pretty easy but squeezing out those last couple of percent can be pretty tough so I I don't want to guarantee any timelines there but we're working on it essentially uh and I think the key thing certainly are probably uh correct uh at this point in time which is good um and so yeah so so essentially by by having this shared model with the evm model being executed we also then gain a very high degree of certainty in our uu model hopefully cool uh and then the second thing that we have as part of this is what we call a verification condition generator right and this is something that you can basically you compile your smart contract from solidity or VIP or whatever into U uh and then what uh what what happens that you receive you have your U smart contract and you can then point the clear VC at this U smart contract and what it does is it automatically processes it in all sorts of ways that we'll go more into detail in in a second but it basically extracts that Ule into the lean proof assistant and automatically it cuts it up into basic blocks for those of you who you know know any things about compiler Theory that's basically like a block of code that contains no control flow right so we like we cut up the ifs we cut cut off up the while Loops Etc and we split those up into separate abstracted blocks uh and and then for each one of these we sort of automatically derive a uh a specification and this is done entirely by the proof generator it's a basically a a very simple um it's basically just something that uses the semant unfolds the semantics of this and uh and and applies a bunch of simplification tactics uh which which is you know ongoing work to improve and perfect um but uh but yeah so it essentially runs these uh sort of uh these it uses these tactics to basically give you a simple relational spec so by relational spec we mean basically a relation that uh relates our abstraction of the uh what do you call it uh it relates our abstraction of the uh of of the state of the evm before and after the execution of a given piece of code right and then the last thing that uh clear that the clear framework is made up of is actually an Ono like this is ongoing development a library of theorems and tactics which actually then facilitate the Practical verification of uh of some of these contracts so uh once again as I was saying in my panel earlier like we're developing like a lot of these the improvers tend to not have a lot of facts about bid vectors lean is kind of fixing this now but uh and then certainly we have some facts about uh how storage memory Works cack being injective supposedly all of these sorts of things which I'm not going to go into too much detail with uh today um okay so so yeah so the this actually now this diagram shows us kind of the uh the workflow of uh of of using uh of using clear right so in particular you take your solidity Viper do dot you run saly you compile it to U uh in fact actually our the clear framework doesn't deal with totally totally generic Ule and so actually you need to use a specific set of compiler Flags uh which I'm not once again not going to go into too much detail about but you can look uh on the uh read me for clear and find them but essentially there are things like uh the expressions in Ule can be sort of nested where you call uh what do you call it you call some operation on another on a sub expression which in turn has a bunch of other operations applied and Ule is not super happy with that so we use one of the um uh what do you call it one of the optimizations we use is the expression splitter which basically makes sure that your Expressions have a sort of Maximum depth of one and these sorts of things we're actually I think we're probably going to fix this change this in the future we thought it would be a good optimization in practice it just makes the programs a bit unwieldy so let's let's see if we end up changing that then as I said we have the proof generator which extracts all of this into uh into lean you get your Ule extraction and your verification condition proof and then the human all the all in quotes the human being needs to do is to insert a specification so this is a formalization a mathematical formalization of the intent of what they believe to be the the intended behavior of this code and a proof that the verification condition this simplifi this proven simplified specification of the code implies a specification right and that me that results in your uh your smart contract being fully formally verified okay excellent cool um ah yes yeah yes here okay sorry one one more slide this is just once again a very very quick overview of the syntax of Ule uh and you'll actually be able to see very shortly I think something that is a very nice uh cool advantage of uh of the clear appr appr assist this embedding of notation because well rather than having to like embed the as well I mean we do embed the as of ual inene but rather than actually having to explicitly construct instances of this actually we've just embedded the Ule syntax into the lean compiler and so we can just write U and lean and it just automatically passes it for us and uh and extracts it so actually the the you know I I write this as an arrow there the Ule extraction as if it's difficult it's like literally copying and pasting the code into into blocks right so that that's that's not super hard the difficult part was actually writing well difficult it was actually very easy but the in quotes difficult part was uh writing the uh U the Ule passer into lean um cool so yeah so as I mentioned very quickly a very quick overview of the Ule syntax so the first thing is we only have one type in so actually no this is not entirely true so Ule is kind of a parametric generic language when we're talking about Ule here I mostly mean what's known as the Ule evm dialect which is a specific dialect of Ule where the prim primitive operations are are the evm prim Ops right um and uh yes and and so essentially uh in the UL evm dialect everything there's only one type everything is U 256 and then as I mentioned we have assignments and and these can actually be sort of um uh what do you call it uh V sorry assign like a higher arity assignment so it can be the case that like a function or an expression returns sort of multiple values and we can Bine multiple values at the same time so that's what this means this means that x0 through xn are bound to the result of the expression as we pointed out the expression is built from constants variables and the Primitive operations of the we have ifs where you have you know condition on your if which is the B and conditionally on that uh that evaluating the true we execute C we have loops which are a little I mean they're they're not unusual I guess but uh I'll just go through the semantics here so we have uh I which is the init block which is run before so this can initialize variables and these sorts of things which are going to be used in the scope of the of the loop uh we have uh a condition a loop condition which is checked obviously before each iteration of the loop and we have a post which is you know uh which is a little piece of code which is executed off the uh the body of the loop which is a c and this post is you know used typically for updating uh iterators and these sorts of things right iterating variables and these sorts of things um and these Loops can contain break and continue statements and that's actually uh I mean we we might go into some an example with some degree of uh showing of how we reason about these but it's it's it's a bit more complicated to reason about this in totally generic way uh and then finally of course we have uh well we have functions uh which are all straightforward and finally we also have and I ran out of space on the slide but you can all imagine what it looks like we have a switch statement which you know takes some expression and depending on the uh the Val the value that that expression evaluates to it can sort of uh go into multiple branches right so all of that uh should be fairly straightforward um Okay so now uh I wanted to run tutorial one let's see if this actually works though okay perfect um let's I I'm not going to guarantee this is going to work because of course uh as the genius that I am I decided to make some changes to this to try and perfect it this very morning and so of course there would be consequences so um but uh okay let me just switch this over perfect okay so so here we have clear right uh and in particular we have some like simple examples which we can see in the out file I don't know why we call that file out to be honest and let's actually look at the very simple example that I want to start out with which is the uh erc20 dole and so this is a very very simple uh smart like this is a very very simple smart contract and in particular it's it's stateless right so this is something that something like something obviously it's incredibly simplified to uh to allow to so that we can reason about it in a very short period of time but uh essentially uh this is stateless so typically obviously an the rc20 would' have some sort of storage map that keeps track of uh the underlying balances of all of the users in these sorts of things we're kind of abstracting that away because then we have to start reasoning about cack and we have some automation there but it just adds too much detail um and so essentially we have a transfer function which takes an amount and the balance of account one and the balance of account two and obviously the transfer is happening from account one to account two and we return two values which is the balance afterwards and we also don't actually deal with overflow here so we're assuming that the total supply for the sake of argument that the total Supply is less than 2 to the 256 and we know that as an invariance so that this can't break right as I said very simplified example and so all that this does very basic Ule that we've extracted here is it Compares it makes sure that essentially count one has a sufficient balance right and if it does uh it uh what do you call it it uh subtracts the amount from account one and it adds that amount to account two right and and returns those values otherwise it leaves them intact and obviously we could do a revert there but once again I'm trying to avoid here reasoning about complex control flow we'll get to some of that in in some uh some later examples right okay cool so uh then if I want to actually extract this into uh in lean I have a VC which I can quickly build make sure it's built up to date apparently excellent and I can use this to then basically I just need to point it at a smart at the Smart contract that we were looking at earlier which was called erc20 Dole and Bob's your uncle in theory we should now have yeah and it's all going red of course so I I'll find out what's going wrong here but we'll start exploring it at little bit um okay it's resorting the file perfect so what so uh oh no I don't want to look at that I want to look and let me close some of these sorry should have had this a little bit better prepared um but yeah so what what's actually happened here is uh this is the elc2 is being extracted into this file here right and so you can see that we have uh a file we have a file for this transfer function right uh and we have a uh well sorry we have three files for this transfer function and we also have this if thing here uh which we're going to look at in what in in a second and so essentially what's happened so we can look at the generated uh oh great this is this is amazing I was really not what I wanted vs code to do let me just click here okay let me let me actually see what this error is sorry it's just telling me to rebuild it let's see hopefully that will help uh luy me this was very smart to me anyways um so so yeah so we can see actually that this has uh that the Ule here has been extracted into uh into lean and and this is pretty much the syntax that you guys saw in the file right and so lean actually because we just have this embedding of Ule into lean uh lean is just able to pass this I mean mod this compiling which well let's find out how that goes um so uh so yeah so so soen automatically basically so sorry the verification condition generator automatically extracts this into uh into Le and uh and then it also in particular actually abstracted away this if and that's what this extra if file is about so if we look here we see that oh it's actually split out this if for me right and over here well you can see okay this this all looks uh oh it's compiled wonderful oh okay it's actually working always a good sign um yeah so so actually uh so yeah so actually then can we actually see this yes awesome awesome so you can see that as I said we've just written our Ule here and actually what I what can I do I can do eval and then this uh one second no it's not happy what's it saying no that that is actually part of this character here no no that is actually part of that's a delimiter for this um but okay maybe let me just try and pro because actually yeah this is not avalable let me just see if I can just print this ah there you go okay there you go this was what I wanted to do so in in in lean I so basically uh I can actually just print the underlying term here that I get from passing all of this U right and so this you can see this is basically our a of Ule in um in like the the uh lean definition of the Ule a that we have and we've just been able to write the Ule directly into lean and this just passed it out and it now has sort of uh uh extracted that and I can print it out all right and now you can see this thing at the bottom which was automatically generated uh which uh you know is probably going to seem like uh gibberish to you guys uh let me just get rid of this quickly um but essentially this is the automatically generated uh uh like specification this verification condition generation right and actually what are we doing here so actually this me says that hey I have some C and C is basically a predicate which relates a state to a state and this is what we call a proposition so this is like a like a a logical proposition which can be sort of provable or not essentially right or true or false if if you will I mean that's not entirely true I know that there are one or two constructive mathematicians in the crow who are sort of frowning at me very heavily at this point in time but most people don't won won't care too much about the differentiation um but yeah so essentially we have uh this uh this this predicate here which relates the state it's meant to relate the state before and after the execution of this basic block right and this second thing is basically a proof that we're generating here and it's automatically generated that says well for all states initial State s0 and final State S9 if I execute my piece of code here so this is my if above right in the state s0 and I then get S9 this implies that the c i define here is a specification that relates s0 to S9 essentially right so it relates s0 to S9 and we have this spec here don't worry too much about it it's because it deals with some with like sweeping on the carpet reverts and errors and a few other things uh that that and it just makes it easier to not have to explicitly reason about these things and so basically what we have now an automatically generated proof that automatically writes somewhat of a simplification of the piece of code that I have above and we can sort of so the nice thing about lean is it has what we call this interactive mode where as you go through a proof you've seen on the right hand side it gives me interactive information about what is the context of my proof what's currently happening all of this sorts of stuff right and so I can sort of Step through this and you can see the proof being constructed on the right hand side as we go along and we we I'm not going to go through all of the details but right here this is where it ends and you can see that here it's basically taken all of the code into this H in the context it simplified it as much as possible and it's saying hey this will be my spec essentially right and so I can't actually see it because of the angle so I'm going to move over there to see what the spec is for a second one second yes yes so yeah so so essentially we have uh uh an if in the ambient logic which says well we look up in s0 underscore one we check if its value is zero and if it is zero then we basically we we uh do a bunch of updates to uh s0 so in particular we um what do you call it we we compute the uh new value well you can see we we update these the ac1 and ac2 values by and filling it we fill in the the sort of arithmetic expressions for them I I really can't see this very well from this angle sorry pull that aside so we can see this a little bit better genius yes it is you're completely right thank you thanks Dave uh yeah this uh will make things a lot easier excellent thank you so much um perfect yeah so we can see what what what actually happens here right so what what's it saying so we're saying the S9 is equal to this and we're basically saying well if uh s0 is equal to to to uh sorry underscore one the variable underscore one is equal to 0 and s0 then this is the update that occurs otherwise nothing happens and we just return s0 and so S9 is equal to s0 in this case and that is the sematics of the loop right and so here what do we say well we say that in s0 we update act1 right to equal to equal essentially act1 minus the amount and we update oh God sorry and we update Act 2 to equal uh the and yeah this is after the update to equal essentially the looked up version of Act 2 plus once again the the amount so all of this is because and we're going to simplify this all away very simply in one second is because well all of this happens after the first initial update and so this is the intermediate step the intermediate state after the the first uh the addition OCC sorry the subtraction occurs right so so so but we're going to simplify all of this away using one single tactic in one second and so all of this was automatically generated so it wrote a simplifi like it very straightforwardly uh wrote a simplified uh version of my specification for me all right essentially so it's it's being flattened into propositional form along with a bunch of simplifications which uh sort of and and actually uh the the change that I was making this morning that I just I literally reverted mid speech which was very fun so I uh was was actually to to already apply the simplifications here to get rid of the uh to make these lookups look simpler right because essentially I should be able to say when I'm looking up ac2 in this well I haven't updated ac2 with this update and so it's just the same thing is looking up ac2 and s0 right and so that simplification uh that we have a tactic that does this automatically I was trying to inject this into the proof generation it did not go particularly well so uh yeah turns out modifying your demo uh right before the the demo is a bad idea who knew okay perfect so all of that is the the user generated uh side of things sorry the automatically generated side of things now we can actually get to the oh great and of course vs code is being very helpful uh now we can actually get to the user input right so the user input here and this is automatically generated but I need to sort of fill it out so the inut the user input here is well I need to write a uh a specification right to like I want to write the actual intent of my uh if right and I'm actually going to in this case my specification is literally going to be my VC my verification condition just simplified down a little bit so I'm actually not going to write it manually I'm just going to actually use a simplifier one of clear simplifiers to automatically get the spec from the VC and then I'm just going to copy and paste it hopefully um so here so as we can see in lean we have uh my goal on the right hand side so I want to prove that the verification condition implies the spec right except I don't have uh a spec yet but what I can do is I can already unfold this right to to get the ver to see the verification condition that the uh that that CLE gave me so I can write unfold this and it now unfolds yeah I keep forgetting I can just look ahead to see this sorry uh and so this actually gives me this sort of simple um what do you call it this the simplified VC that we already had right and um here I can write is it clear Vore uh did that simplify yes did it s0 [Music] amount well well actually there's an easier way of seeing this I can just go before I know okay so I need I think I need to do s a clear VAR store at uh and uh actually no no sorry let's do this a little bit more cleanly so let's do intro H so I introduce my assumption so now I have a h in my assumption which says Hey the specification for the verification condition holds and I want to prove my uh my specification right and so I've I've introduced this and so now hopefully if I do clear once again Vore and I think I can do at H was it h comma okay there we go uh and yes okay so now it has actually simplified some of these things down all right so or has it what's what's it actually saying here oh yeah no actually it's not okay so the the simplify isn't working super well in this demo right now but okay so let let's actually try and write this spec by hand then to make it a little bit simpler so what do we actually want to prove here well we our specification that we get the automatically generated one is this and that's a bit too complicated right let's actually make this a line this a little bit better to be able to read it a bit better um okay this is now a little bit more legible uh and where's my else Branch why I didn't copy and paste the El Branch great one second so in the other cases we say well it's just the case that S9 is equal to S Sub Z there we go and we just want to write S9 equals oh that was not nine sorry one second there we go and okay still not fully happy with me what's it saying here ah okay so it's not entirely happy with some of the updates for whatever reason let me just try and like pass these out a little bit better so that I can read them so we have the update to ac1 we have the update to ac2 um yeah this we can just forget this just becomes so I'm just going to simplify this away this just becomes looking up ac2 right and this also becomes just looking up amount because we haven't changed amount here and I think that should oh oh I see I'm missing I see now what's wrong I missed a bracket which was why lean was unhappy with me yes okay now we have a reasonable spec right uh and yeah not entirely sure why the simplifier wasn't working there but as I said I missed messed around with this just before so that probably did not help um but yeah so we have so now we have this and now actually we can also unfold our our goal right so we can unfold this part of the specification and we can run some automation let's see what happens so this is a quite a powerful simplifier that will sort of go about um H okay so maybe maybe this is not actually the cleanest way of going about it okay so let me just go back to where we are here let me introduce our H oh yeah we already introduce the H and what we want to do now is what what we're going to want to do is basically case on this to be able to prove this or this is getting a bit messier than I was hoping um so once again in N we can basically break down on a case of whether a proposition is true or not do we oh we don't even have an s0 in scope what's happening here sorry okay interesting why is it not happy with this it's not an inductive type what am I eliminating into uh okay well this is going I'm I'm just going to sort of try rot forces to see where we go then um okay so at least now we can continue the proof so I I'm I'm going to unfortunately have to because once again I broke some of the automation this morning it seems I'm going to have to sort of break this proof down more than I was hoping to uh it was meant to be just be two sort of tactic applications but it's not quite working out um but essentially okay so uh we'll we'll ignore one of the simple cases very straightforwardly so I'll just quickly get rid of that okay that sort of goes away here we have jump underscore and I'm just going to sorry that out for the moment and here we have okay evm and sigma uh oh yeah I'm missing another underscore here no this is not ah oh it's checkpoint oh God okay so now I think we hopefully have something a little bit cleaner so we can sort of simplify down our goal and now we just want to uh basically prove so this this uh you might have noticed this sort of outer fuel uh thing and this is this is actually a bit uh annoying and I was as I said this should have been automated away but unfortunately the automation isn't quite working this outter fuel is basically because in uh proof assistance there are reasons that basically you want things to always uh be able to terminate right and so the reason is that actually termination we we've talk like I've sort of been alluding to this a little bit but essentially lenix exploits this sort of this what we call the kry Howard isomorphism so this is the fact that basically actually at some level there's a way of embedding higher order logic into the type system of a dependently typed programming language so if you're if your you have a a programming language whose type system is expressive enough eventually you can just basically embed logic into it and just prove things with it and this is basically what lean does is in in a sense a normal programming langu a functional programming language where with a type system on steroids essentially right but the problem is that uh for proofs at least having non-termination is kind of an issue it's analogous to like circular reasoning right so in in a a functional programming language I can write like def F and I can give it any type I want and I can just say hey that's equal to F and and it will just recurse at INF item and it will never terminate and that that's that's analogous to Circular reasoning and so essentially for these reasons we uh sort of need to we need to only reason about terminating traces and this is what this fuel is and in fact in fact actually we can obviously use gas to reason about this because of course evm programs do terminate because of this of gas but uh but but but basically gas is a little bit because some of the uh G like some of the gas computations are a little bit complex and so proving that this is monotonically decreasing is a little bit more complicated right and we're working on automation to be able to get rid of this but this this outter fuel case is basically saying hey you've reached a situation where uh you've run out of gas if you will and therefore we cut if you will and therefore we you know all sort of all not all bets are off but it it will rever in in a case where it's not terminating in this case it will just have reverted by now right and so that's what this outer fuel is dealing with and so we're just sort of uh as I said this actually should have been dealt with with the esub spec tactic but is not did not work right there I don't quite know why but I'll look into that a little bit later uh well that's actually what we're doing here right so actually inside of the spec predicate we actually folded an implication that says that uh if you're not out of fuel and this is what this question mark means if you're not out of fuel then the specification has to hold right and so this gives what we call partial semantics to the program logic of it says that hey only if you have termination does this specification hold right um and so so yeah so so essentially we we're continuously filtering out these outter fuel cases and as I said there is automation I promise that does do this but it's not working right now um because I was very smart anyways so uh so yeah so we we reach down to this state which is is uh sort of we're approaching hopefully a little bit more what we want um and what we can now do is we can introduce the fact and I'm going to call it not out of fuel so now we have an extra assumption which says well by the time S9 terminates I haven't run out of fuel right and so that will allow me to continue reasoning and now I'm going to be able to unfold my specification the specification I have here to be able to uh actually uh start uh start proving that my verification condition implies this so let's try and do that so we're going to unfold spec at H there we go and we know we know that uh uh the initial state that we have we we're considering the uh the okay case the case where we're going to continue so we can immediately simp simplify this down so we do simplify only simp only at H uh yes yes yes so we've we've uh basically simplified down that specification application now we've extracted just the verification condition and note that it requires us to be able to use this verification condition we need to actually uh apply know that we terminate in a state that's not out of fuel and this is uh and conveniently we already know this so we're going to be able to do this by actually specializing H so we do specialize H at uh not out no not not like that sorry uh not out of fuel yeah thank you L there we go and so now we we're getting closer and closer to something uh where this verification condition looks like a uh looks like our goal right which is which is kind of nice so we're now what I'm going to do is basically like break down the proof by uh uh cases on uh the on the value of this if straightforwardly and once again I mean this whole proof should have been one single tactic but anyways uh so this isn't quite showing off so okay so let's do case let's hope this works this time no inaccessible variables okay interesting um okay well I guess what I can do then is just split ifs I guess that will do it that will do the trick there we go okay well at least lean wasn't too uh difficult with me there so split ifs basically what it does is it in your this is quite straightforward if you have shockingly an if in your um in in your goal in the goal that you want to prove it splits it into multip it splits all of the ifs adding the L the if condition or its negation into your context right and so basically split ifs generates now two goals so I have the goal the case where uh underscore one is equal to zero and I have the case where underscore one is uh sorry is not equal to zero right actually I think I need to add some variables here so that is it with uh okay yeah no so so now I've I've bound this okay so I know this fact now right uh and and so this is going to and I should not have named it the same as the previous h so let's call this uh Hond sorry uh okay and so now so now basically I split into the two cases of whether I explor the loop the sorry not the loop the if or not uh and uh what do you call it um and and I'm going to try and use this fact on my verification condition so what I'm going to do is I'm going to do simp using the fact that I know the condition is true at H oh no that's going to automatically simplify that down for me so so now we've we're of we've eliminated into the case where um where where sorry the if is explored which makes things uh fairly uh straightforward right and so now I can actually rewrite with this large expression here into my goal and start trying to prove uh equal like try start trying to straightforwardly prove equality and hopefully some of my automation will work otherwise this is going to be a bit painful fingers crossed uh so what I can do is basically I rewrite back WS H into my goal and so now I need to prove that these two uh States these two final states are equal and so hopefully Constructor will help me here nice it did good um or did it actually no it did not okay huh great um H so okay let me just see what happens if I try and S this uh yeah okay um did that actually simplify anything down I'm not sure uh okay well let's just try um maybe maybe this will actually be helpful actually here okay yeah so we broke down quite a bit there but in particular I'm hoping to use VAR store uh clear VAR store at the Target and whoa I just eliminated one of my goals so I proven one of the cases uh once again this whole thing should have been one tactic so I'm not I'm not too impressed with myself but anyways so let's let's sort of indent that in uh and actually I think I can probably eliminate the seop I think just the clear vastor will be able to do it so clear vastor is basically a tactic which an automation that thankfully worked unlike some of the other automation but is is an automation that is meant automatically deal with reasoning about variable stores reassignments and these sorts of things and so it can automatically uh deal with this sort of jumble and figure out okay well if I'm looking up account one in a state where I've I've overwritten account two or something like that since these two things are not equal it's equivalent to the original value of the variable these sorts of things so we can automatically discharge all of that and uh and handle it and then then we have the case where this fails and once again well we're going to just do this simplification and you're going you you can probably see that this is going to be really straightforward by just sort of rewriting backwards with h and and and we're done there we go and so we have uh and so on now what we've done is we've proved that the verification oh and we can now delete all of this MTH at the bottom and as I said really uh actually there's this tag te called ESOP spec which if you guys want to actually use Clear uh this will work in the main of the repo this is just me breaking things in the last moment so all of this can be done with by doing these unfolds and then just running ESOP spec which is basically like a hammer automation that just does like State like basically massive State exploration and then running clear vast on the sort of final States and that that clears out this or would completely clear this out automatically essentially so this should have been done automatically it was not apologies for that um so so for for uh yeah so for ifs for fours and for uh function bodies we will do uh individual proofs essentially right um so the the ifs is a little bit arbitrary fours are of course required for like this because Loop and variance are generally undecidable so that requires human interaction right the ifs are well we found that there was a little bit better scalability when we took this approach practically speaking um and so uh and so yeah we would have to write such a thing but obviously typically speaking for uh such a simple thing ESOP spec will deal with it in a single go I promise you you can try it on the repo um I just had to do this manually because I as I said I was messing with a lot of things this morning and ended up breaking that so yeah so now we've basically verified that the verification condition implies the spec right we can see that tells us no goals here and then right at the end lean has also generated this other file that basically combines the fact the proof that it's automatically generated that the implementation implies the verification condition and and the human written proof that the verification condition implies a spec to be able to um uh to to be able to basically it chains these proofs together to basically show the implementation implies a spec and Bob's your uncle that's easy you've got a formally verified smart contract right that's kind of the idea uh once again as I said there were some unexpected pain points here and then basically you can sort of bootstrap this up to the uh to to transfer because this has taken a little bit longer than expected because of the broken automation so I'm actually going to skip that part but what I do want to emphasize is the uh the modularity a little bit here right which is that so I'm going to show you another example so let me clear all of these things uh clear no pun in intended um uh no well actually may as well save that so I actually did some work there um yeah why not perfect so I'm going to show you guys very quickly in my last 10 minutes another example that I think really emphas because this was like a straightforward uh example to give you a flavor of what's happening and as I said it should have been a lot simpler um but I want to show you an example of uh of something of something that I think maybe shows uh clear as modul it a little bit better right and it's it's a Sim it's a s it's a simple I'm going to say almost childish example but sorry but but it does emphasize this point so here we have a broken proof for whatever reason I'll reset the file but but the the yeah the proof itself running once again doesn't doesn't matter too much but we have here a very we were talking about extensional equality and we have here a very very dumb implementation of the ad operation in uh Ule right what does is it wants to add X to K and the way that it does is it basically just Loops adding one to K and subtracting one from K until K hits zero right and the idea is at the end of that you uh obviously you you want to prove that um uh that you the result Y is equal to X Plus K right and this so this this is straightforward but then I can write a function called uh M right and M is a function that uh wait no did it not oh great it opened it oh God sorry one second H this is working great okay so m m is uh what do you call it is is another function which is defined in terms of adk and it uses adk it repeatedly uses adk to add uh to well sorry to add X to itself K times right so it adds it starts off with some initial variable y and then it adds X to it k times and um and and what and the nice thing here is that we have modularities so when I actually want to reason about add K I don't need to unfold it and understand hey what's the code here or have any kind of model of it I I have this proof that the implementation implies the specification right and and clear automatically knows this and can automatically apply it there and so then that massively simplifies the reasoning about this call and then in turn M K can be used to uh Implement an XK right an exponentiation operation which once again sets some initial counter to one and then multiplies it by x k times using the m k function and once again I can abstract that rather than having to know its definition that it's a function that calls another function in Loop uh I I don't need any of that I just have the spec right and it abstracts all of this and so obviously these are very simple examples but in complex soft at scale this uh massively helps formal methods actually scale to being able to verify complex properties over uh large smart contracts and I mean the particular applications that we have for this is like verifying uh cryptography like ZK verifiers and these sorts of things where you actually need the complicated facts that clear has access to due to math lib to be able to verify them okay cool so I I had another sort of uh part to the tutorial which I'm just going to completely skip but I will quickly if I can find it yeah I'll quickly go through yeah so I had the running example um and yes so I'll quickly talk to you in the the couple of minutes I have left about well what is uh what are the limitations and what's the future work here right so obviously one piece of future work is to unbreak the changes I made this morning so that's that's that's the number one thing um the uh the the the sorry the IM there are some immediate changes that were plan on making in the next couple of weeks to make this more uh easier these are what we call these quality of life improvements because in particular right now there are some things which are sort of automatically true in function specifications which we don't derive and should be automatically derived so for example when you call a function you actually need to explicit right now you need to explicitly write and and clear that uh when I call that function the only variables it overwrites in the local scope are the variables that are bound to the outputs right and that should be completely aut atic and unfortunately that needs to be written in the spec right now and that's just a limitation well it's not a limitation it's uh just it's it's not very difficult to overcome I think it will be we'll be able to do it very quickly uh there are also some um some some tactics that we we're developing to being able to De to deal with reasoning About Storage right so storage is kind of a complicated one because uh storage is not actually storage maps are not actually sound in reality right uh in the sense that it it depends on uh the catch check map being injective and that's true with very high probability but it's not actually true right and so to be able to actually reason about these things while injecting these assumptions there is some like there is some like reasoning about some what we call random Oracle some random injective articles that needs to be done and so we're writing some tactics to be able to do that automatically because otherwise right now reasoning About Storage uh updates and these sorts of things is a little bit painful but we're reducing it to being a lot simpler and so well hope hopefully just like earlier hopefully it should be one tactic soon uh uh we as I mentioned earlier we're trying to get our evm model to uh pass 100% to get to 100% performance as I said we're at about 90% at this point in uh in time um we're also we're also trying to and this is something that sort of comes into the whole L2 uh sort of uh not well not only the L2 thing but it it sort of is something that I I most other solvers don't really have an option for which is uh actually we we can have this we want to add in a most General client into this uh into this model so this is a a way that we can model external smart contract calls that basically just models an arbitrary external smart contract as some arbitrary contract that can call do arbitrary calls back into my contract so it's basically a a contract that can make arbitrary random sequences finite sequence inces of calls back into my contract and so that models all possible re-entrancy attacks right and so we want to be able to all to to automatically to have some integration of this model and to be able to automatically then reason about all possible re-entrance attacks which I think will be good uh the other thing that we want to have is that well lean has been working quite a bit recently on um what do you call it on integration with smt solvers which makes things uh which makes some sorts of corner cases well makes a lot of reasoning about like practical computer implementation stuff like equalities of bit vectors facts about bitwise operations these sorts of things makes it a lot easier right so in lean that can be quite painful an smt solver can just sort of hammer that away so where we're going to be integrating smt solver using uh use to be able to make these easier and then the the last thing is uh is scaling because unfortunately so for some fairly large arithmetic functions that uh solidity will spit out we've we're experiencing some sort of like um timeout issues with the proof generation the verification condition proof generation and so to actually get around this we want to do basic what we're calling chunking which is when we have a very large function basically just cutting it up automatically cutting it up into smaller uh basic blocks and reasoning about those and then composing the the resulting verification conditions automatically and that that scales a lot better so that for to be able to reason about sort of larger amounts of Ule we want to do that uh automatic and and there's also one thing that is frustra okay I've got two minutes left I think well manag to finish this actually um one thing that's a bit frustrating is that Sal the saly Ule um what do you call them optimizations are are not the best and however much you want to get it to eliminate the hundreds of intermediate variables that it introduces whatever you whatever set of optimizations you use you won't fully get it to do that and so what we also want to do is introduce an extra step to the verification condition generator which automatically applies a bunch of simplifications to the code like semantic preserving simplifications that eliminate intermediate variables and then automatically generate a proof of equivalence between these two things we've done this before not for solity but we've done this for the Zur ml which is an intermediate representation for ZK circuits where there the compiler also spits out a lot of intermediate uh variables and these sorts of things and we automatically eliminate them them we also do like lifetime analysis where we move variables to the sort of the last point at which they can be uh defined and all of these sorts of things automatically improve the equivalence to once again simplify the resulting terms so yeah so we've got all of these things in the works coming in like the coming months and uh so yeah so as you can see clear is still quite uh experimental but I think uh a few months from now we'll have the evm model being completely con conforming to the conformance tests and we will have it scaling to sort of large um large uh smart contracts and there our primary goal at this point in time is attacking a bunch of things for actually like practical smart contract uh developers that I think that automated theorem proving can't really uh attack which is essentially soady so the soady library has so much uh extremely optimized uh like inline assembly ual written into it and the thing is the reason for the soundness of this these operations although they're very commonly used is not at all obvious it's certainly not something that most automated theorem provs can seriously approach and so our goal will be actually verifying some of these more complex functions used by smart contract developers to be able to I guess uh provide some value to the community that way great um okay so conclusions yeah I mean I've basically gone through these so clear powerful form of verification uh form of verification framework for Smart Country cont ra like for for smart contracts it allows you to M verify math lip to have all of these complicated math facts at your fingertips uh so you can verify ZK verifies complex numerical estimators contract interactions rollups Etc and clear is also powerfully extensible I can write new automations for it new uh new automations new um uh like new predicates new theorems Etc to be able to simplify its use and make it easier for domain specific and general purpose okay thank you so much for listening uh thank you Julian for your work on uh formal verification and uh developing this framework so we have a few questions from the audience and I'll just quickly remind if you have more questions please scan and uh go to Mir cut app for any questions so yeah uh yeah so sorry I is this is the oh sorry you're going to read out no no I'll let you okay okay so the first question I'm guting is can you show us some example properties you've proved in the uh in your Ule framework so I think so I I don't have this immediately available but the most complicated property that we've proven is uh so uh many like like probably many of you who are familiar with defi will know about these sort of like exponential estimators for like mapping price ticks to prices right so Ty you have a tick which creates some spacing on a price space right and you want to be able to compute some based to the power of this tick and you you want to estimate an exponent like this exponential curve except that's sort of complicated in practice and so typically this is done by basically breaking down your tick doing a bit breakdown of your tick and then multiplying together uh the sort of the the sort of if you have you know t t like base to the power of t0 plus 2 * T1 that's the same thing as doing like T to the power of oh oh base to the power of t 0 time uh base squ to the^ of T2 right and so essentially you have uh uh what do you call it a numerical estimator that uses this to compute ve with very precisely an estimate of this expon this exponential function and we've actually formally verified this and shown and and proven a formal bound on the error um okay uh next question how do you ensure the correctness of the verification condition generator that is how do you guys ensure that the generation of the U extraction plus VC proof from Ule does not miss any spec excellent question so the so the the the obviously the the Ule extraction itself is oh by the way sorry I I have all of this time to answer questions right or is this for the next speaker okay okay okay full for me okay good I was checking that I'm not taking someone else's time um but yeah so the uh so the the VC as we as we saw basically clear has uh a Ule the Ule syntax like embedded into it so so checking that it's actually fa F firstly I mean it's literally copying a string but if if you really don't check trust that part of it you can manually check hey is this really copied and pasted from the contract cool okay um and then actually proving that the VC uh the verification condition extracted well I I am certain I'm as certain of this as I'm certain that lean is sound because actually this verification condition is is generated by lean right so lean is the one that is applying all of these simplification tactics to generate this verification condition so the VC itself doesn't actually generate the verification condition it just generates a proof that then you gets lean that has a formal model of of Ule that is checking this against a formal model of of Ule to generate that verification condition for me right and uh yeah okay cool can you sh uh okay no uh that's one I've already answer are you able to use this now to verify Enterprise grade evm contracts so at this point in time the given the scaling issues uh we wouldn't verify like I I think it would be difficult to verify a full complex defi smart contract end to endend using this right uh and actually what we're trying to do is we we're looking at collaborations with various other companies that do uh have automated theor improving based techniques where actually we want to be able to create Bridges with them um where where essentially most of the contract can be automatically verified and then when you hit something complicated like a numerical estimator or something like that where automated theorem proving is not really able to reason about this to verify the properties of this you can then extract that out into clear and verify this right so essentially the the way that we see it at this point in time until until we've gotten the scaling and the simplification tactics uh to to be a bit better uh at this point in time I think it's more something that we would use to verify the really complicated parts of a smart contract right uh um i i i u i don't know is that an acronym for something that I'm not aware of ah thank you if I understand lean would allow you to reuse a state value EGS Z as many times as you want once it's introduced which isn't really great are you able to use something like linearity um okay that's I'm I'm not entirely sure as to the motivation of that question and that uh s0 here is a symbol in the logic not a resource right so the ReUse of it has no cost in a sense right so if someone ask who asked that question wants to clarify maybe a bit more what they mean by this I think you're getting a microphone H was able to consume s0 to make a claim about the resulting State and then you if you try to do this again with some other H in the same statement like U isn't telling you that that some state update it happened between that it's kind of invalidated s0 is no longer alive yeah so but s0 is the state at the point in time it's never updated right so s0 is always the state at the initial moment in time it never changes so S9 is the final State and then we introduce SS Prime Etc if we want to reason about intermediate right so there would be never be a way in which another function represented as a proposition could take s0 as an argument I guess that's what I mean is that yeah because it my mind maybe s0 isn't alive anymore like in the proceeding function call s0 is now non-existent because I I see what you mean in the sense that you want to make sure that there is sort of you're chaining the right States together right and this is this is done this is sort of done by construction because it's enforced by well hopefully the semantics the ual semantics being correct and chaining these states around correctly right but you're completely right that it would be good to to uh to be able to make this clearer to the program because I've certainly been like in the middle of one of these proofs and being like what the hell is s prime or S Prime sub two you know or these sorts of things so I think that that would be actually pretty nice and in particular actually um where uh we're intending right now to put on top of all of this uh something called PRL so this is a probabilistic relational logic which allows us to verify cryptographic properties right and in particular this actually has a notion of a pre precondition and a postcondition to this code rather than just a relation and that precondition can be updated over time and then you have basically you have rather your notion of um uh you have a sort of a temporal notion of state and you can only refer to the state at the moment before the piece of code you're currently referring so so we are going to be embedding a logic on top of this to make this easier to make it clearer what you're reasoning about and also be able to reason about cryptography probabilistically at the same time so yeah uh but right now not so much yeah uh cool uh instead of writing the spec and the proofing lean how about using some kind of annotational for writing properties in uality in the matter in the manner of liquid hascal yeah that's that's an excellent an excellent idea and uh yeah we we've actually been thinking about this of basically creating a form of like enriched okay I'm being told I have very little time yeah two two minutes I can answer yeah I'll finish this we have a little more time so place you know five okay I have a little more time oh okay okay well then uh you guys are stock here sorry I'm I'm just going to keep labing on um but uh yeah so we've actually been thinking about this of allowing basically a sort of like Rich solidity where you can as you're um as you're sort of developing your smart contract you can insert function prein poost conditions you can insert Loop invariance and then then those are automatically extracted by clear into lean force and then we can try and prove them right uh and use our automation to prove them and I I think that actually this is a great idea because because at this point in time I feel like developers and you know you guys probably will know more about this than me but I feel like developers uh feel like you know formal verification is this weird thing out there that they know nothing about and at at best uh you know they think oh maybe this will help me out at worst they see it as a hindrance to the sort of iterative process of development right and I think that actually by allowing by having a sort of an an a rich solidity which has these annotations actually we can make this feed back loop with developers a lot tighter and feel like they're integrated into the process and understand a bit better what are the things that we're proving rather than we just have it throwing large equations at them and saying hey this is totally the spec that you want you know um so yeah uh so uh so the okay so can lean generate counter examples when the spec isn't fored maybe via smmt so at this point in time so at this point in time clear can't do this uh lean does actually have this smt lean uh interface which which I think does allow counter example extraction and so in the future we we're intending to integrate smt lean into this to be able to deal with these side cases and so I'm I'm hoping that in the future we will also be able to extract counter examples yes um ah good that's a great question how difficult would it be to use the evm lean models to build cert verified certified compilers for the evm great question I love it um so we're actually planning on bu because the thing is part of all part of the trust base and I didn't mention this for all of clear is well like clear is trusting that you're your compiler actually compiles this down to an evm smart contract correctly and obviously the typically a lot of optimization steps Etc involved in that process and a lot of things can go wrong in that time right so oh by the way do tell me when I'm out of time because yeah um and a lot of things can go wrong in that process and so uh I I do think that uh you know I think it's important to have a u TVM a verified U TVM compiler this can be done in in lean I think actually fairly straightforwardly but there's a difference so there's a difference between writing a u u to to evm compiler lean that's verified and a good uul to lean or an optimizing uul to evm compiler that's verified right and so the former I think will be very easy uh the and then we can also put in sort of harnesses to add optimization St and then potentially people can then prove those optimizations correct in lean once again um but but that that obviously having a good set of optimizations and fully understanding how they interact and that each one of them are individually semantics preserving can be quite complicated and can be quite timeconsuming Tas but the first step of having a compiler that's verified I think will be relatively straightforward right with respect to some notion of like storage equality so when you execute the Ule program versus the evm program the in the same state the resulting storage state will be the same and return values will be the same is that it okay thank you very much for your talk cheers so let's take a break