Formal verification in Daml with Gert-Jan Bottu's Demo

Captions as YouTube publishes them, usually machine-generated, so names such as Daml and Canton can be misheard.

1. 0:00

   for the past three months I've been working on a tool for providing automated formal verification for demo code so what this means is that we want the computer to automatically it's a given choice and give in a specific field in a template then a tool should automatically prove and that no matter the input to this choice it will always preserve the total amount of this field in the world so for example a choice might move funds between accounts so

2. 0:37

   that should never destroy or create new funds so the tool is still still a prototype so I can very much demo the prototype but the idea would be to integrate this into an IDE later on but for now just command-line interface to show you what to do so I'm gonna try to share my screen I can't thank you so for the purpose of this demo I created a small example a template account which is still which is simply stores an

3. 1:30

   amount and its owner and then I have this simple choice here which is transfers funds between two accounts so it takes an amount to transfer it takes a receiver if the donor doesn't have enough funds to transfer it just doesn't do anything and otherwise it fetches the receiver and it creates the remaining toner and the new receiver so obviously we want this choice to preserve the total amount of funds

4. 2:10

   this star so we can now pass this into the verification tool so we pass in the dark we pass in choice which in this case is account transfer and the field we wanted to preserve the total amount okay so immediately the tool tells us that something failed choice doesn't actually always preserve the amount and provide us with a counter example here so it's still a prototype the output is

5. 2:51

   not the easiest to read but it does provide us with some information so basically it describes the main flow it describes the main flow of the choice so when executing a choice it makes a number of create an archive of things which are described here so if this condition holds so if we have sufficient funds then we create a new account with the current amount - transfer amount and

6. 3:23

   with receiver amount plus the transfer amount and we archive the receiver so indeed clearly something is wrong here and we forgot to archive the current so if we add this line well now the show is actually always preserves the amount because now we also archive so before I mentioned tents this choice should always preserve the amount no matter the input of the choice but the dual actually does take some more

7. 4:28

   information into account so for example isn't sure is actually the tool is actually aware of this so if for example we would add something something more here if you would say if the transfer amount is smaller than the amount that we do something else so you might expect

8. 5:36

   this to brief as clearly this doesn't preserve the amount it is cool smart enough to figure out that because the amount can never be negative we know that the receiver is an account so this branch can never again show indeed the choice still preserves okay so all of this already worked in the last demo we gave so what is new since them well now we extend it a tool with support for recursion so for example I

9. 6:40

   wrote this second choice which basically it donates from one account to another until the account has at least as many fans as the donor and it does this by checking the condition if the receiver already has enough funds they will not do anything if not we use our transfer choice which we defined before to transfer one into the receiver and then we call it in so it's a recursive choice and that keeps calling itself and then

10. 7:17

    until the receive earnest enough funds so this gets a bit more complicated how does this work well we don't make any assumptions on the input so based on the input this might make a number of recursive cycles we don't know how many cycles it makes so basically what we do is we the tool extracts every possible recursion cycle it strikes it from the code and then it also describes the main flow

11. 8:14

    so the main flow it's what happens if you run through the choiced once and then the recursion cycle is the cycle that gets repeated every time you call choice so in order to ensure that the amount is always preserved we require that both the recursion cycle at every iteration step preserve the amount and that the main flow preserves the amount as well so this is slightly overly

12. 8:53

    restrictive so there might certainly be some examples where this isn't the case but which still preserve the amount put while designing this - we really had the golden mind of making sure that when the tool says that the amount is preserved that is actually the case so false positive is much worse than false negative so we made it a little bit overly restrictive this can certainly be

13. 9:26

    improved so okay so the two can figure out recursion cycles now but we can actually go one more step further namely we can go into a mutual recursion so I wrote this final choice here it is a bit overly complicated it's designed to be to show up the tool but basically what it does is it takes an account and it takes an integer and then it splits the account into a number of equal chunks so if you have an account containing ten ten a month how he split it into five

14. 10:14

    chunks then we should end up with two with five chunks of - I know that this choice could easily have been written to be much simpler but just let's just go for it so basically what it does is it checks whether it needs to create an additional chunk if so then it calls the check the second choice and all this does it's just creating an additional empty camp with a mouse a rule it then calls the

15. 10:46

    third choice which computes how much to transfer into this new chunk and then use the choice we defined all the way to start to make it transfer intimacy chunk and then it calls the first choice again with one last jump so this makes a number of cycles through these three choices and the tool is now able to isolate these mutual recursion cycles so I can show you this if we call so what

16. 11:45

    happens here the tool figures out there's a mutual recursion cycle between these three choices it then isolates the cycle itself so every update and that happens within this within these three choices which are described here and then in this case the main flow would be empty so the choices only have this mutual recursion cycle and nothing else and then again it needs to ensure that both the main flow which in this case is trivial and this mutual recursion cycle

17. 12:25

    always preserves the field which in this case it does so in this case it's still relatively easy because the mutual recursion cycle and capsulitis the entire choices but for example all right just just a quick question can you say a few more words about the main flow it being empty what does that signify exactly yes so in this case it is only a simplification so why is this empty it basically means

18. 12:57

    that if we call this account wake up it runs through the entire code again and again but there is nothing outside of this cycle so let me show you what happens if this wasn't the case so this cycle goes through the if here and exercises create chunk so it goes through all of this and I'm back to break however if you make an additional branch here saying for example so now this part this else branch it's no longer a member of this mutual recursion cycle it doesn't get reached in every

19. 13:49

    iteration only at the very end the tool takes into account so the cycle itself remains completely identical and it still preserves the amount with the main flow suddenly got a whole lot more complicated so outside of the mutual recursion cycle there is now this additional health branch so this is not part of the cycle but it does happen a single time when you execute a choice the very end this gets executed but not

20. 14:40

    at every iteration so now this main flow is no longer Hampton so now it needs to take one cycle plus this end condition into account so all of this is one cycle and then here you see at the very end if the number of chunks is no longer larger than one then we create them meaning that while this cycle preserves the field the main flow no longer does because at the very end it's excuses

21. 15:10

    additional create statement does that make sense absolutely thanks a lot okay so it's actually basically what I wanted to show the tool is still prototype put it does show quite a lot potential it can already verify quite a set of of programs and to be really interesting to see where it goes after this to be great to have it integrated within an IDE so it can be used more user-friendly I without having to go too