Solidity, Vision and Roadmap

Transcript

[Music] okay uh hello again everybody hello welcome to day two all devor zero uh I'm going to start by um talking a little bit about solidity the uh new contract language and then Christian where's Christian Christian is going to continue with uh uh the implementation and a lot more

sort of details and road map of the future of it so I'm just going to basically go into what drove the original um sort of need for a new language so our main issue is that we need people lots of people to write contracts and as as a lot as often it is brought up uh these contracts need to be correct because once they're on the blockchain you can't change them unless you've got some sort of update mechanism in place but that brings along a whole slew of other questions like how do you trust that the updates are going to be U

legitimate so these are the two main things that that we're concerned with lots of people are able to write contracts and that these contracts are correct so one of the obvious ways of getting more people to write contracts is to allow them to write it in a language that they're already reasonably familiar with so um since a lot of our uh prospective developers are going to be people who who are already understand web Technologies HTML JavaScript CSS um it makes some sense to have the contract language be syntactically

similar to one of these so JavaScript um leverage the existing skill set as it's there we also need to a a language is only as good as the concepts it can express easily so it makes sense to build in the concepts that we know we're going to need to use often um a contract language it makes sense to have contracts as a first class citizen in that language so what we do is we take the notion of contract and we take a a

paradigm that already exists uh objectoriented programming and if you think about it contracts can very easily be con considered classes or objects depending on um whether you look upon the the instance of the contract or the contract the the Prototype of the contract and so we we uh base the language around this notion similarly within ethereum contracts have storage now having to store things in terms of literals is almost like you know having a a beautiful high level language and having to store your integers as bites it doesn't really make sense so what we do is we say right well we are going to

support the storage but we're going to do so in a with an abstraction layer and actually what the programmer sees is just what they used to which is to say uh usable types strings structures integers of various sizes booleans and then finally contracts do um a lot of IO and whereas in normal objectoriented languages um you may have ways of passing parameters as in parameters and out parameters um C++ for instance uses pointers or references to do that if you've got uh there are there are language idioms that allow you to um have multiple outputs uh sort of as part of again a first class portion of the

language I believe go is one of these Jeff will probably be able to confirm that wherever he yeah yeah um and so this this makes a lot of sense within contracts where um we are going to want to call things in and then take data out of the contract without having to worry about things like references so then we come on to making things you know how do we make things correct how do we make it most likely that these contracts are going to be correct well the most obvious way is unit testing right you but unit testing at least with uh traditional um sort of basic unit testing Frameworks are going

to require effort at least a small amount of effort from the programmer to to put the unit tests in so what we do is we devise the language or at least the language um development environment combination um to make unit tests actually easier to have in than not so we do things like all already have a space where the unit test goes and then the ability just to press enter and you get another unit test so just make it incredibly easy to place um the uh expected results or a set of expected results um in there the second thing that really helps us guarantee that um a contract is operating according to

specification um for some simpler specification than the definition of the contract in in code is this notion of formal proofing so who is familiar with formal proofing anyone at all a little bit okay so formal proofing is the notion that you can um you can describe you can specify um the um you can specify some expectation of a program and that this expectation can either be proved or not proved but it it that happens at the point of compilation not at the point of running the

program so you can specify for instance that you expect um no matter what state the program gets into you can expect that all the balances will add up to a particular number and what you can do is if your program is written um using a particular um nonch incomplete but non a particular language still relatively Rich subset of it um you can use this um well the compiler can use this at compile time in order to guarantee that that statement always remains correct always no matter what as long as long as you own use the uh the methods but of course there's no other way in ethereum than to use the methods um that that will always remain true um this is used

in existing I think it's used in uh a lot of safety critical environments uh nuclear power plants I believe use techniques like this um the Rolls-Royce uh the big engines that you see on the side of airliners the uh the reverse thrust mechanism um this was uh also uses so what the microcontroller for that also uses formal proofing um I know that because my old University um helps develop that that particular piece of technology so it's in use already but it's not it's not widely used and so um it makes some sense for contracts which you know cannot be changed once they're in there to use similar Technologies and then the final final

thing is the documentation documentation is you know Absolut absolutely fundamental to our security model when the uh decentralized application wants to make a transaction with the blockchain wants to sign something with the user's key it's really really important that the user can read a statement as to what is going on with their key because if they can't do that we you know we're back to Step One um this is absolutely fundamental to um uh our this notion of having a a sort of more trustworthy um interface to massively multi-user applications and so we we build the document documentation system actually

into the language now this is you could argue that doxygen Java do already sort of have something similar and you know they do but what we're going to do is we're going to build on that and we're going to have um uh rather than just placeholders actually have evaluatable um Expressions within the documentation itself so contracts as first class citizens here's uh here's an example and can I stand in any one place that will allow everybody to see probably not get most people I guess um so you got the idea you know people who code a bit in C++ will probably this

Willa you can Bo is wrong should read function but uh yeah so it looks a little bit like a class as you might expect and you got set and get yeah you pass a parameter into one this should read uh function get returns uh U but the other the other slides are correct um and then you would use it by saying right well we've got an instance of this contract we ignore how we actually get that instance for now um set so super easy o style um

interfacing uh I'll answer that later so um if we uh if we move on to the storage facilities again it should be relatively easy to see that we have this notion of a state right which is also known as you know the field the members of a of a class in this case um it's a uint and then we can Define our set as just you know setting it and our get as as returning it so this this to a C++ programmer will be super super simple but to a a ja a JavaScript programmer as well this portion of it will also be reasonably

familiar the returns bit is a bit different but and the fact it's tight but can't really get around this now the storage facilities extend so what we also are able to do is map and this is a fundamental um construct in this language we can provide um um uh mapping from a uh from an original domain range range from an original range in this case the range of addresses so this is the type of address U which is a 160 bit integer into some arbitrary uh domain um

in this case end points and we've we've specified an endpoint as being ipv4 and4 this is a bit see the syntax is still up for up for uh um alteration if you uh if anybody here has some ideas and to make it slightly more javascrip without um making it too difficult too cast um and then we have the idea of setting and we can make a new one um assign it super easy stuff delete for killing it um Vari addict returns so uh if you want to get the information of an address we can

just specify the two return types easy enough now the formal proofing is probably the most interesting and challenging part of this uh I imagine Christian's looking forward to that that particular portion of the project um the not the the idea behind it is that we have uh here's an example of a cash contract so you give to somebody some amount and you check that the amounts greater in the caller balance then you subtract it and add it to the to the destination check the balance that's easy enough we can to do a mapping so map our address to a to a a numeric type and that's the balances again easy

enough we got this construction so this is the initializer so we're just going to initialize the uh whoever created the contract to you know a billion or whatever some pre-mined amount and then we have an invariant right this is this is the really clever bit so this is the bit that says at all times no matter what this contract must always satisfy this piece of sort of uh uh prototypical set theoretic M um what we're actually doing is we're reduce well we're going to um we're going to map the idea of value of so value of just in this case is the idea of uh taking each item in the balances and just taking the value so that the

balance itself rather than the address so we going to map that to balances just get a a set of addresses and we're going to reduce that set of addresses with a plus operator so let's to say we're going to sum some them and what we're saying is that should that sum sum of the balances should always equal um a billion and uh what the compiler is able to do is go through the only um non-const the only mutable method so the only method that actually changes the state which is this one and do a um a formal proof of this code to check that uh if it's uh if it satisfies this constraint at the

beginning and this code executes um it will always satisfy the constraint at the end and in this particular case it does and so the compiler would would be happy now what that gets the the um the author is the ability to state in the documentation that this for this line of code it says at all times total balances will be a billion now someone coming to this uh this contract who who maybe has some reputation it could be like the ethereum foundation or the eff or I don't know whoever it is um will be able to check that that that line of code in the um is is well representative of the

documentation line above it give that a tick y That's valid and then they don't need to check anything else because the compiler does it for them so when the user comes along and they say o the foundation made this uh the foundation ticked this line that says cash at all times in this contract is a billion they can TR it they're like great and in none of that did we have to actually look at this code I'll come to it the Victor so um the final thing is the inbuilt docks so that's kind of what I was saying earlier we have the uh doxygen style at the moment triple uh

triple slash which I guess most of you are probably familiar with um the interesting thing of this is the uh the back tick so the back tick allows us to insert um arbitrary uh expressions JavaScript Expressions into um the documentation so what this does is it provides a notice for the user so when the user sort of you know clicks through on some dap and gets a transaction the DAP wants to submit the transaction into the network um this is the message that comes up in the browser before it signs it so there's like a a sort of black box in the browser right that contains all the secret keys and ultimately this

could be control actually not in the browser itself but it could be controlled by a trusted Computing portion of the hardware so something for which even the operating system doesn't access and what this this this would bring up a message it would say transfers and then it wouldn't actually say underscore amount right it would say the actual amount it would place the amount in there so it would evaluate what underscore amount is and then um stream it into this into this text cash from your account message call it would give you either the name if you've if you've got a name attached to it if name rge has got a name that you that you trust or or just the the hex or maybe even a little graphic to the account controlled by and then again the

same thing but but the um destination returns to cash don't really care about that and then You' got the uh the construction creator of the contract is endowed with a balance of a billion that's easy enough um it will probably insert m get get the address and then finally this magic line total cash in the system is always a billion and this is the thing that the the auditor or whoever um whoever is it could be that there are many Auditors I mean you know it's decentralized um checks this line yeah yeah that's fine that's that that means this and that's the magic when the user comes to look at it there get an

absolutely trustable uh statement cool so those are the uh basic uh driving factors and rough solutions to them um Christian is now going to go into a little more detail then we'll do a question and answer session at the end and uh you can bring up your points there okay so um yeah now let's see how this is all implemented um first what were the requirements for

solidity Gavin already told us about that so it's a contract oriented language which means that classes are contracts it is statically typed from the syntax uh close to JavaScript and when you types to JavaScript you get something which is close to C or C++ um uh the built-in language documentation and some language subset that allows formal proofs of correctness and yeah so coincidentally this is exactly the contract Gavin also showed so you already know that um yeah can skip then the uous coin

contract um there we see some thing we've not seen in Gavin's talk um the language is statically typed but still um it's not necessary to always specify the types you have this keyword V uh which can be used for local variables and it's similar to C++ 11's Auto keyword which means the type is just taken from the type of the first assignment to this variable so I think that's quite convenient um yeah okay then uh we see something

um users can Define their own types so they can Define structs and then mappings can map basic types to any type so we can have a struct at the as the value type we can also have mappings again as value types we can also have contracts as value types and um this vote is the the struct type here so you can retrieve from the storage from this this mapping here uh the value which is stored at the senders address and then yeah assign values to this local

variable but this doesn't really so this this actually assigns it directly to stor because vote is not a local variable that is stored on the stack it's just a reference to the storage so you don't you can yeah directly access storage here okay um some details about the compilation process it consists of six stages uh the first stage is just parsing after parsing we have the basic abstract syntax tree so we know the structure of the program uh the next step is resolving identifiers so words identifiers strings can mean can refer to user defined type names

they can refer to function names whatever and these are all resolved in their respective scope and assigned in the abstract syntax stream and after that step it's possible to infer and check the types so that assignments do not conflict in types and functions are called with the correct number of arguments and and so on and after this third step uh it's possible for an IDE to actually use the abstract inex stre for things like uh autoc completion or checking where a variable is used and all this nice stuff we want to

have and the fourth step uh is compilation to an assembly language then this Assembly Language is optimized and finally compil to BU code okay some details about the type system um statically typed means uh that all expressions in this language have a fixed type that is known at compile time and an operation so it's not possible for an operation to involve two different types so you cannot add a string to a number but it is possible to do manual type conversions so if you manually explicitly convert the integer

to string then you can add them and at some points automatic type conversions are done if it makes sense and if no information is lost so we will see that later uh the types that are currently implemented are uh unsigned integer signed integers and hashes of various sizes so this x is always uh the size in bits from 8 Bits to 256 bits in 8 bit steps and the difference between integers and hashes is that uh arithmetic operations are not allowed for hashes because it doesn't make sense and a special case of 160 bit hash

is address where so and for an address uh not even bit operations are allowed but instead you can yeah want you can send ether to that address or query the balance at the address then we have a Boolean type mapping structs and contracts okay later we will also have strings and but that's not implemented yet okay um I hope you've seen this already so this is also available online uh

it's the solidity compiler compiled to JavaScript to be run offline in a browser so okay sorry that's what always happens okay so this is a basic contract without any content and on the right right hand side uh we see the compiled op codes the compiled binary or hex version of the binary um more detailed assembly and at the bottom we have the abstract syntax stream

um and if I enter something in the function we will see the types that are inferred from these uh literal so it's an so the type of literal is always the smallest type where it fits in this case it's an 8bit unsigned integer and if we add an 8bit unset integer to an 8bit unset integer we again get an 8bit unset integer nothing too fancy so it gets interesting when we use larger values so 7,000 is a 16 bit anide integer and we add an 8 bit onside integer to a 16 bit onside integer this

8bit integer is implicitly converted to a 16bit integer and and what if you add like 200 200 the type system ignores overflow so it's just about um yeah so uh one we always know that the type of a of uh the result of a binary operation is one of the types typ of the operant so only one of the operant is converted and so we can now assign that to a

variable and we will see that X will have type 16 bit uncen okay what happens if we if we want X to be an 8bit integer we get the error that the 16bit integer that is on the right hand side is not convertible Tobit integer on the left hand side okay something that is perhaps also interesting is what happens if we add a negative number to a positive number so the compiler complains that it

cannot find the common type and so the type of minus one is signed bit integer of eight bits and eight is an unsign integer of eight bits and so you cannot convert one into the other so there's no common type of course we know that both of them can be converted to an assigned integer of 16 bits without losing any information but because of this restriction I told uh this is not done automatically but we can of course force that manually and convert this minus one to an 16bit side integer and then it works and X is also assigned integer of 60

minuts okay you check it also on the variabl what do you mean if you have varable so can we do the question it works on arbitrary Expressions okay um the optimizer um so solidity does not compile to lll but it compiles directly to evm assembly and it uses lll's assembly class which also includes the optimizer so if we improve the optimizer

then uh solidity Serpent and lll will benefit from these improvements um I already did some improvements so the lnl optimizer is so most of the steps in the LL Optimizer is just a pattern of op codes is mapped to another to to yeah to another set of op codes and if the number of up codes decreases then this is applied and one of these patterns is constant folding so if you write 7 + 8 then the optimizer will not do this addition at runtime but it will do it at compile time and just push directly push 15 and I added some other operants uh

for this constant folding because they were more widely used in solidity and another optimization is uh pop optimization this happens if you if you do some computation and it does not have side effects and you just discard the result of the of the computation then the optimizer removes the whole computation okay let's see an example okay first without optimizer um okay so we have to look at the

assembly now um from tag zero to this tag three that's the the body of the function and we see it it does push zero that is it initial it initializes the local variable to zero then it pushes the two operant 8 and seven adds them and this uh swap stores it at the location of X and pop removes the old value of x and if we activate the optimizer so it pushes zero and then it pushes F which is 15 swaps it stores it and removes the old value so this is not yet optimal

because we know it's not necessary to initialize X to Zero when we change it its value afterward but yeah Optimizer is not finished yet I would say um to see Pop optimization we have to remove this x let's see no we also have to remove the local variable so yeah what happens here now is okay yeah Tex zero that's the function body and nothing Happ happens

okay um how does c to use memory and storage um we've already seen everything is zero initialized we can trust on that and Locker variables are currently used only on the stack so it doesn't it doesn't actually use memory it uses memory only for op codes for operations where it's really necessary um this might change later because the evm can only look at at the stack at the 16 topmost position in the stack so if we have many local variables or very complex expressions and we want to store something in the first local variable we

might have to look too deep into the stack so we have to copy it to memory first and then yeah unwind the stack and save it later again um the storage is allocated in a continuous way so uh if you have one struct and then another struct then they will sit direct directly next to each other in storage where mappings are an exception because mappings don't have a size so uh to compute the offset of a mapping you take the or to compute the offset of of a value in the mapping you take the offset of the mapping concatenate the

key compute sha three of that and that's the the offset of the value I think that's more or less exactly how it's done in serpent with the introduction in serpent Cho so yeah the obvious way I would say um okay reference to other contracts um gav already gave gave an example for that um a bit more detailed we can include other contract files contract source files and yeah use contracts also as values for mappings or directly in storage and we can so name r Adder is an

address we can so if you write it like that name r is is a is a contract type this is just uh usual type conversion so address can be converted to a contract type and then we store it in storage um we can from this point on we can use name r and call functions on that and for that we don't need the full definition of the name contract we only need to know its interface so this this name s file can be yeah a simple file which has all functions but not the function bodies and it's different for this line here where we create a new contract and

store it at this point in storage so here we actually need the the full definition of the coin contract to create and when it's stored we can use it to call a function send amount to so that's yeah that's the function we've seen in the the second example okay um yeah what are the plans for the future um I think we will have a complete first usable version by the beginning of December so yeah after def con zero uh the current state is

that most of the basic features are there what is missing is actual access to the blockchains so query balances and send funds and references to other contracts but that's not much work I would say so future areas of work are yeah I shall write some tutorials or actually create a specification of the language I think um then uh depending on feedback from users we might add some new features to language we might need to improve the optimizer but that yeah depends on how the language is actually used so

we will have to look at some real world example contracts then work on documentation so this netpc documentation where the next we'll see that in the next talk and actually creating the the IDE and then work on static analysis and formal verification and of course bu fixes and refactoring that can always be done um how how is that am I on time or okay so yeah one plan language feature I don't know if that's interesting uh Anonymous structs so you can do mappings from a struct type without

actually creating a name for it you can so functions that return multiple values you can just store them in local variables directly and also return them like that so I think that's something we want but that's not implemented yet um some ideas for the optimizer I think it's uh really important to be able to use other contracts as Library contracts somehow at least for simple functions like like Computing the minimum or finding something in a list and for this it's important to so calls to other functions

are quite expensive because you have to move all arguments to memory create so run this this call up code and then retrieve them from memory again and if the function is small then it's much more efficient to just copy the code to the to that location and and another benefit of inlining function causes also that the the optimizer can actually optimize there then it's perhaps necessary to to reorganize the local Stacks so for example if two V two local variables do not really overlap in a function they can use the same stack slot and if the feedback results in really really bad performance for the

compiler then it's perhaps necessary to consider some yeah simple Intermediate Language where more optimizations are possible than on this on the stack based evm code um so some ideas for static analysis um con functions are not enforced currently that should be done then um what is also quite easy I think without doing the whole process of form proofing is to determine the value ranges of local variables and check whether some overflows can happen so if some addition was protected by prior prior to that

checking that an overflow can happen and perhaps also checking that from the value range some equality compar comparison or inequality comparison can never be true and then we see that the developer did some error there so some code is is not reachable at all um what is also useful I think is to estimate the gas usage of of of at some Source line so that while writing a contract you actually see how expensive the line is and you can perhaps change it to be less expensive and what we probably also want is uh if

you issue a transaction you have to set the gas value and and you probably want to have some estimate on how expensive it is some lower and upper bound um this of course will in the end so the actual gas cost will in the end depend on the order transactions are introduced into the blockchain so yeah will not be uh absolutely correct but I think it's it's so we can provide good uh lower and upper bonds for the gas usage okay that's it [Applause]