# Introduction to the K Framework and KSolidity by Rikard Hjort and Shang Wei Lin

- Channel: [Devcon](https://streameth.org/devcon)
- Date: 2020-10-09
- Duration: 20:23
- Topics: blockchain, smart contracts, distributed ledger, ethereum, ethereum solidity, solidity, solidity summit, language design
- Watch: https://streameth.org/watch/yt-vegzI_v7d6Q
- YouTube: https://www.youtube.com/watch?v=vegzI_v7d6Q

## Description

Learn about the K's background and the Solidity semantics in the K framework.

## Transcript

um thanks for having us I'm Ricard I work for run time verification I usually work on K wasum and I'm here with strong way from NTU Singapore and we want to tell you about K and how and why specifying solidity in K is a good idea the case emetic framework is built on the idea that every programming language should have the formal semantics so from a formal semantics the K framework can automatically derive all the common software tools this includes parsers interpreters but also more complex tools like compiler small checkers deductive verifiers and so on so the complexity of work for generating tea tools for a language just goes from T times L to t + L K is by no means a new technology this framework has been developed for over 15 years we use it heavily at one time education and there's lots of publications surrounding it it is also proving very language and blockchain agnostic so the formalism works for a high level languages like solidity C Java low-level languages like wasum and EVM and we worked on different block chains like aetherium al-quran pesos and so on it's I just want to show you the formalism that K is based on its a rewriting formalism so I'm gonna give you a short example of what that looks like the first thing you need to define is the state that the rewrite should act on which we call the configuration it's built up of what we call cells so here we have a configuration which contains the program to run in a Cell that we named K we have an environment for the current variables which is a key value map and we have a local memory storage and more cells we don't really care about now regard I'm sorry to be interrupting but the slides are kind of blurry is there an option that you either can share them with the audience or maybe Shang Way could share your screen instead sure let's see they are kind of hard to read right now my screen but does it affect recurse presentation I'll just so we have some transitions but we should be okay I'll just say next slide or something okay turn off my let me try as well that would be great sorry for the interruption yeah so that just means that that people will have to select the not the speaker's picture to see the slides because the live stream follows the audio so let me with my slice great you can click through thank you okay hmm yep keep going and yeah here we come to syntax so you write your syntax in typical EB NF form but we have these handy annotations for example strict to means that the second argument here is strict so the right-hand side would be evaluated first so that has you can add some semantic meaning to use syntax declarations and if you go to next slide here's an example of what a rewriting rule looks like and I'll just show you how it acts over a specific configuration so here we have a configuration with the identifier foo and you assign 3 to it so and you write your semantic rules with this rural keyword C basically what we will do here is we look in the current environment to find the pointer and then go to the storage and modify the value at that pointer yeah so what you had this oh go back yeah so the rule it's a real keyword that you see there these little rewrite arrows don't specify where the state is gonna change the next slide so first the assignment is gonna match the seer the rewriting rules just applies to any configuration that its left-hand side unifies with so in this case the configuration matches the rule the assignment in the rule not just full equals three with Phu assigned to X and three assigned to Y I so actually this might be a little annoying to do in this way so let's just skip over the rewriting part and I'm happy to like explain this in detail to anyone later or you can just look at slides yourself so let's go to formal verification so basically from a semantics written in this formalism there's a straightforward way to reason about how program execution so click Next the K framework derives a proverb for free and the basic idea is this you treat every rule as an axiom next you can do next three times you write a claim as a rewrite rule then you start from the left-hand side apply all axioms that match branching whenever there's more than one thing that applies and you just show that on every branch you always reach the state that matches the right hand side so next slide let's see maybe I should know yeah yeah that's probably good so basically why should you bother making a formal specification in or an executable form of specification I'd say it's the best of both worlds you get something that's readable and reasonably high level if it's a K style you can even write it in a literate style inline it with your documentation its executable obviously so you get an always up-to-date correct bike instruction reference interpreter everyone working on the form of verification tool can now do so properly in quotation mark because you actually have a formal definition of the language I'm very curious to see what's going on on the smtm tomorrow regarding this but yeah having is some formalism that describes the language is usually a good idea I also find that it's a good prototyping tool for trying out language changes because once you've hacked away in a language change in the compiler for example you can spit you need specified in a way that is ruthlessly unambiguous and at least with Kay the semantics are even composable so you could write a separate semantics for say ëwell and include that in de salud semantics and it actually shouldn't be that intimidating because it's defining a semantics is sort of on par with writing an interpreter in terms of work so with that I want to ask you to consider this statement that solidity should have an executable formal semantics and with that I just want to hand over to Zhang Wei who has been working on just such a specification okay thanks Ricardo the introduction of the catering word then I'm gonna take cover to introduce how we define as formal semantics of Kay of solidity in the catering work to do so actually you need to define two components the first component is the configuration which indicates the status or state of small contracts if you look into the configuration file actually you'll find that it has two main parts the first part marking the red color which is for execution of a small country instance while the second part marking the blue color is for recording the whole blockchain network status and that's assuming - the red part and you will see that we have a dedicated cell called execution engine for execution of small contra instance and inside a cell we have several important cells for example the cost deck for function cost either external or internal we have cost eight including the ID which is the address of the current instance the caller ID core value storage local memory etc and if we look into the the blue card you can see that we have a cell called accounts in which we store all the contra instances that have been deployed on blockchain including its address it's come from name its balance its storage etc now let's move on to the second component to define that is a set of semantics rule indicating how each suited stamen behaves based on a current configuration as well as how it updates the configuration let me use this statement as an example so here we have a statement to declare a variable of unsigned teacher in storage whose initial value 3 and how do we define our semantics of this statement we need to write a rule a semantics rule for that for example here if we have in a case cell we we see this statement of this syntax we know that it's a variable declaration so we try to rewrite this statement to allocate term in K it looks like this and at the same time we need to look for necessary information and put it here so for example here we need to know what is the current account that we are going to declare this variable so we need to look for heads account ID so we put it here together with the variable information for example the name of the variable the expression the value the type the location etc and then we move on to this allocate term so when whenever we see this elegant term in a case cell provided with the necessary information then we are able to do the corresponding arrangement in this account that is to insert this the this parable record in this counsel here I omitted the details but to sum up to develop cement our formal semantics of solidity in a catering work we need to define first the configuration second a set up semantics rules like this for each statement now I'm going to talk about the challenges that we may face during when we develop the semantics the first challenge is that solidity is actually changing very fast in either in syntax or semantics currently the latest version is 0.6 but if you look into the version history in average almost every month will have a version change which is quite challenging for us to run after the frequent version changes the second challenge is that the delimited description in the official document is not comprehensive usually complicated or corner cases are not mentioned for example if we are talking about function modifier the following details on dimension for example what if the honest course daemon is used for more than once but if the modify is inherited from one and once by a function etc and we need to figure this out by ourselves based on some experiments which is quite time-consuming and the current status of caseloads e the project started in the beginning of 2018 and until now we have two versions first in one support solid is 0.4 and this table summarizes what other features supported by our semantics and as you can see that almost every core feature is supported except those that are not we are not able to support for example this inline assembly basically this is EBM bytecode and obviously it is out of the scope of solidity itself and since the literally 0.5 was introduced we plan to have a refactoring on based on version one to version two to support so D 3.5 and currently we have finished core expressions and statements and we are still working on some advanced features for example function modifiers user-defined types inheritance etc and now you can find our person to implementation on hip hop now and with versions you actually can do automatic testing or proving your small contracts and I would like to share with you one of the interesting findings when we develop the semantics and it was back to solidity 0.44 and here we have a very simple test case that we use to test our semantics and you can see that it's a very simple contract test consisting our two state variables and be with their initial values one and two respectively and we have a function foo here in which we declare a local array D with two elements and after that we try to assign seven and eight to the two elements respectively now the problem has what are the values of a and B after that we execute a function foo but based on our semantics a is still one Beast you too but the proven stock at the statement and this is because when we declared D we don't specify the location so by default it will be in storage and based on the semantics it would be a reference to storage but we don't have its initial value meaning that we don't know where the points to so whenever we want to execute this statement we don't know where to store seven however if you try to execute this contra in the remix compiler I mean zero point four version and you'll find that that result would be a become 0 and B becomes eight and you may be surprised because you thought you are dealing with only local variables but actually global variables are affected and obviously something went wrong here so which one we reported this findings in our technical report in 2018 on archive and after our investigation without that the solute leaves your point or compiler implemented some implicit behavior which is beyond developers expectation and the problem comes from this this statement when we declare this function this array D we don't specify the initial value but for the compiler it assumes that the default value will be 0 so actually D points to slot 0 in the storage so that's why when we execute this statement the contest comes like this and when you execute this the second assignment statement the content becomes like this so that's why a becomes 0 and B becomes 8 and of course this behavior has been fixed since 6 of the D zero point five now you need to specify the initial reference for deep otherwise the compiler will complain about that so from this example we can observe that the formal semantics absolutely is very important especially for developers well now I would like to summarize this talk by introducing the possible application of cash solidity first of all our semantics is fully executable executable meaning that you can execute you a small country based on our semantics and you will have an output configuration actually you can have the output complicated configuration after each statement and you can do formal verification you can have some assertions in your smart contract and our tool can help you to do symbolic execution to check whether the assertion welfare or not or you can even try to prove that you're smacking trap correct of course you need to specify the properties and then you can even do compiler verification this is what you can do for example you you have a smoke on trial right you can run your smoke on track based on our semantics that you have an output configuration and in up in the other hand you can compile your smoke on track by a compiler and you have your bike EVM by code and you execute your bytecode and you have your real output and after that you can compare the two outputs to do cross validation if they are not consistent meaning that something is going wrong and last but not least you can even do semantics consistent checking for example how do you know that a behavior in this ability level conforms to that in the EVM Bikol level to do the consistent check in actually you need the formal semantics of EVM which is supported by another project Kay EVM from runtime verification alright I think that's pretty much I want to share with you today I think Rico and I would we'll be happy to take questions if we still have time yes you still have a couple of minutes so feel free to ask questions in the solidity get a chat or right here in the room okay yeah somebody's raising his hand I see it already la la you yes hey guys thanks for the talk can you hear me yes okay cool yes sir this stack case loaded to kayvyun force makes a lot of sense and it's super nice but super like let's assume that K you'll exists with it how much easier would K you will like case letters to the kaolian cable to KBM B if you want to verify the whole stack then the single sort of like the single largest up from case literally to a VM every card are you going to answer yeah sure do you say mean for a compiler verification like in very fine ink immediate steps or write simply like if you have if you have this first code and then you have to compile what care then you want to check do balloons for example yeah I mean it would be the same thing in the sense that you would if you have a complete semantics of you'll you could symbolically execute your program and then you could check that I mean the the tricky part is to find sort of equivalents like figuring out well you know we expect this value to be output or stored somewhere whereby EBM just correlating that - you know the corresponding part of the selected configuration I mean it it would be the same thing I think but I mean it depends sort of them how the semantics are written and but in principle it should be the same or simpler actually I have something to add up mm-hmm I will we try to defy the formal semantics of solidity we try to keep the configuration as this as much the same as EVM as possible for example we still keep the gas transaction number etc we try to keep it as the same as possible this is because we want to do the consistency checking although some of the cells we cannot use it for example the gas cell actually in the solidity level you don't know actually how each stamen consumes how many gas so we just put it there and have some estimation one way is to you compile your absolutely contract into a ppm and calculate the gas and get back to salutely level and put into the gas cell so I think if you want to do the consistent checking that would be not typical because 80% of the configuration are the same