[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
have
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
[Music]
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
the
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
something
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]