[Applause]
all right welcome everyone we're about
to kick off we're going to be conducting
today for your very eyes a competition
in golf around the Gulf you might say
that will also be form of the red pipe
so we're rewriting smart contracts and I
never like what you prefer and you'll
submit submit your effects to our CI
server which will run a suite of formal
verification proofs against that white
coat and if you do manage to pass
perspex we have approval incorrect
contracts then there's a competition for
making the most gas efficient that's a
contract and in particular we'll be
doing it today with an ESD twenty cents
this is the month where the most
straightforward specification of course
there's some caveats on what the
specification actually looks like were
made a little bit of an opinionated
choice here we'll go over that at their
time so when I said that we'll be doing
a competition actually met we'll be
doing two competitions at the same time
namely there's this Ian golf competition
that I just described
hoo-wee correct coz 20 permutation but
there is actually a second contest going
on behind the scenes and if you're
feeling like the first one might not be
too much of a challenge for you were
here thinking that formal education is
just a sham then you can participate in
the second competition which asks you to
submit bytecode that has some sort of
bug in it but it still passive suspects
somehow if you believe that the specs
and the methods that we have created
with the formal verification process
that has been set up then you can try to
fool it and you can try to submit might
go that fast those effects butter
otherwise faulty in some way I mean this
hard to define one there's no longer
expect to talk about but I'm sure we'll
be able to figure something out so
you'll be able to compete in both of
these competitions and we'll get to the
details first I'm not going to be
talking too much about the theory behind
what we're doing today because we need
to have time to actually do some hacking
but let me just mention that the proving
methods that were using here for this
workshop we're gonna be using the
catering work and we'll be writing our
specs without looking at her specs
written in the act smart contracts
specification language we'll get it
okay so let's get deeper into the
specification I'll come over to God soon
so sometimes people say that NERC 20
yearsI 20 specification as evidence or
sort of Express panel it's really not
it's more of an interface that really
just tells you what the methods should
look like in your contract and doesn't
actually say anything about the behavior
of course I mean we have some intuition
around what this should be but there's
actually a whole range of different
types of behavior of difference here see
20 tokens and it gets kind of annoying
when you start dealing with them and
then you have to check whether this
particular is a 20 you actually did
return a boolean at the end of its
transfer function anymore what's
happening in the case where you're
sending to the 0 is not like this so in
order to actually have a specification
we need to make a choice on all these
decisions and neighbors have our choices
but before I do that I'm going to show
you the language in which we're
presenting these choices so this is our
specification formats that we have
developed in order to be literate
language that should be intuitively
makes sense users you know common
mathematical works and we have created
it in such a way that from a small
specification like
we should be able to generate a suite of
reachability claims so proof obligations
essentially that you can port to right
now okay but there are more back ends
and we're planning and so let me show
you how this works we have on the left
hand side we have the specification in
the active language and on the right
hand side we have a simple transfer so
what we do is well actually let me go
back and just say the main claim of a
specification is in this storage header
so under the storage header we're saying
how the balances of the people involved
are being updated so we're saying that
whatever their initial balances word
from Bella to above they're going to be
updated with a corresponding value as a
[Music]
as a result of calling the transfer
function okay but this doesn't always
happen because there are some scenarios
where you do call the transfer function
and your balances aren't updated namely
if you don't have enough money to send
or if there's an overflow when you're
trying to add the value to of the
receiver and so this should be reflected
in the spec and here it is we see that
they're actually four conditions
associated with this
out and the first three are associated
with and if and only if Petter resists
iff and that means that in the two specs
that are going to be generated or the to
reach ability claims are to proof
obligations that are going to be
generated from this act we are going to
assume all of the conditions in the pit
of the earth header to be true in the
past case than to be false in the fail
case so what the nature of that claim is
is is that it amounts to saying that
only if in the case where we are still
within the range of a UN 256-bit word
then these storage updates should be
performed and when any of these
conditions are not met then we should be
in the field case in the fail case
asserts that everything must reverse no
storage updates are to be performed but
there's another type of condition that
we can make in an act and that's the if
better then the indenter that the
conditions in the if that are assumed in
both the fail in the past cases so
obviously this restricts the nature of
your claim to make sense slightly weaker
by assuming additional assumptions and
so if you have and it better like this
you must have a corresponding next
suspect but assumes the negation of that
so in this particular SPECT were saying
that the caller ID should be different
from from the two meaning of the sender
should be different from the receiver
because we had to treat this case
somewhat differently
I mean we actually that would only be
referring to a single entry and the
storage rather than two separate votes
so we need to write that SPECT a little
bit differently and so then during the
course of this competition will be
making we have a suite of these specs
that will go over soon enough and they
will generate these proof obligations
your byte code will be associated with a
proof obligation and the proof will be
run on our CI machine and after they
have been run if all of your specs are
passing you follow that proof
obligations have been proven and then
there we will be taking the execution
traces so the method by which we're
proving things is through a symbolic
execution and that gives you a complete
exploration of the possible things that
could happen through the execution of
this method and through this execution
trace we were able to walk down all the
branches and
the final result and guests the final
gastrous also the final gas consumed by
this method in each match and when we do
this gas extraction we take the maximum
values of the worst case scenario call
this function and this is going to be
your value that you're completely so we
get a small expression like this if you
know your idiom then you know that
whenever you do this story to update
what actually determines the cost of
that has to do with whether the storage
that you're obtaining was 0 or where
they are putting it to 0 as so we'll see
conditions on this board where they are
the most general but of course you can
take the worst case scenario this and
this is what we'll be using ok
so with that let me just say how this
will all go down as I said all groups
will be running on our service you don't
actually needs to do much yourself of
course if you just if you can come and
chance we can talk about it but for the
purposes of this competition the only
thing that you need to do is to write an
implementation get the bytecode of that
implementation the runtime bytecode and
make a PR to a repo that will be showing
you soon and everything that is provably
correct will be analyzed forecast
okay so I think it's time to go over the
specs they can be found at this repo
which is the repo will be working with
inside Catoctin two-column / backward
slash yearsI 20 - golf and there's as i
mentioned there were some opinionated
choices we made while making a spec well
the first one the most important monster
listed on this page will not be caring
about logs so you can forget about logs
for your implementation for the purposes
of this contest everything must revert
if all value is greater than zero so
this is following the convention of both
my parents limiting and well this is
this is actually true within for the
minor caveat the stores will give you
know the way that the EVM deals with a
storage under the hood is a simple key
value mapping of introduced to integers
and so in order to translate the so the
variables that are being used in near
surprising like balances in total supply
and allowances you need to place these
at a particular location these these
into transit your mapping in the UM and
there's a convention for how you do this
and the most crucial thing to know here
is how do you make sure that you need to
encode basically the balances on the
now aids in a particular way and this is
a particular hashing scheme that
salinity uses in order to make sure that
whatever you look up the palace of a
particular address you won't have any
collisions with any other address of the
balance of memory so we we go over those
details if you want to but you can
actually also use the library Convention
which is extremely similar a big hashes
the arguments in the same way but only
in a reverse order
but if you're using solidity or vigor to
write your contacts this will be of
course done for you and supplying all
opinionated choice if the allowance of a
particular person with respect to some
executors is the max possible event then
transfer from should not decrease the
allowance of spending okay and of all
the submissions are due it's 125 let's
go over the space hey sure yeah so I'll
demo it down the specs for you and also
have a CI server works and covering
detail everything you need to know today
[Music]
can you see this is the size okay a
little bit thick
so first the first I want to show you
the structure of this this repo has
everyone been able to find it first of
all so we're looking for looking for
this repo and it hasn't and I'm gonna
show you first just the structure of
this so we've got going here
a Romanian configuration finally you
don't need to worry about and the most
important stuff is in this source
directory and here firstly we have our
specs which is expected of me and this
is the different aspects of Martin was
right - this is red there's a part-time
files it's got these aspects that will
be tangled tangled out of it you do not
need to edit this because this is the
part that's that's this part this one is
given to you for a but you do
need to read these if you want to write
limitations over actually that will
actually passed it makes written
understand all the nuances hopefully not
too many nuances as there are some so
partners really covered how these specs
book but I'll make you just pick another
one and quickly don't bring any other
features but you know the idea is you
want to you want to leave these and
these interface lines correspond to the
familiar DRC 20 interfaces and we use
the we use the solidity where you know
detering contract ABI for competing
you know need to face selectors from the
from the call data which is I guess you
know assume but basically what that
means is that if you're writing the
theoretical total supply function that
means that the force four bytes the call
data activity the shot three of this
string has to be something like this so
just keep that in mind in case you're in
case you're wondering how however a
powder like this of course if you're
ready and solidity of my for this visit
done for you so I think hopefully these
are these are pretty readable the best
way to address any any difficulties
would be when we get to the practical
part if you raise your hand or just say
something and we can discuss discuss
with me these specimens unclear but I
mean it you know I don't either
these are pretty readable so you can see
for example the convention with the
return with the return values is here in
this last night at the bottom means you
return alive in this things success so
now I want to show you actually how to
run how to run this with your own 0
implementation so if you go back to this
you go message source directory you'll
see some other files and the most
important one for you to edit is this
file in runtime which contains the
runtime byte code of your your
submission we see there's already one in
here which is which is the sample one
has provided this is coming from a basic
solidity implementation the source of
which is
it's in the it's in the rebuilding that
they their injury so we go on below yeah
it's okay so this is like the par that
you can compare yourself against a
beggar and it also assist you if you
find some expert to rethink things have
to read this way to you get a handle on
what's going on
yes so to be clear this this solidity
that's in the in the root of this git
repo passes the specs so your your your
thing needs to be behavioral equivalent
to this stuff this is one way to check
and except for the constructor which we
will not be verifying you don't need to
you know you need to worry about how to
have this contracts deployed to where a
transitional process to play out
right so going back to this what you
need to do is put your put your bank
code into into this pot so you can even
doing this fund and up with your during
fight card into it and I think you're
actually Lancet because if you you know
as you'll see in the repo to this
pimping me there remain this repo here's
how you do that with so steep say I'll
see with all studies associate to Dante
you'll tend to do up in stimul and have
the effect good and these are the
instructions before survivor and maybe
you have your own funny tools that you
want to try so it actually makes a lot
of this header but it's not necessary so
you know simply having me the hex in
here as a ski is how house house I'll
see you out there
so now I will show you how this gets how
does gets processed so it's kind of
happened when you when you submit a poor
west where you've ended this in runtime
the file is our our CI server will
automatically pick up the floor but and
it's going to run the K framework
groomer using the specs generated from
the Riviera language against your guest
or effective and then after that
execution is done you know here's an
example where this guy running when his
execution is done
a successful proof all of the all the
specs eligibility things were
successfully perfect you will it will
actually do a as a symbolic analysis of
the the gas with all of all these
execution traces and a little calculate
the product is run seventy the maximum
caskets and then there would be a report
produced so here once you wonder we can
track your progress you can go to adapt
on CI slash GRC 20 - golf
they're here for every for every law
request this repo there will be a hat
which is your entry as you can see here
they're the last one was in 1042 and if
you know if you look on the right-hand
side you'll see that there are 16
aspects in total and 16 of them were
where accepted being that this is a
correct implementation has been formed
an air pipe and now if you click on this
link well you'll be able to see an
overview of coloring past but also very
importantly you'll see next to every
extra every passing behavior you'll see
here on the on the right you'll see gas
and gas analysis so I want to show you
these so gas is a bit technical that
this is the decay term the new extracted
from the smoking execution that
represents the state of the gas at the
end of the end of every execution to
this dysfunction the reason this has
been complicated because there's going
to be branching it here it's going to
depend on the state state of the data
but that's not a little bit hard to read
the thing that the submission will look
at other the contest will look at this
gas analysis if you click that link
you'll see that we have
can you guys do this so basically what
this is what this is showing is that
this balance of that this balance of
munch is actually consumed rather than
30 gasps and in every in every case this
could actually a very simple example but
now if we move on to something a little
bit more complicated like its transfer
function we look at the cast analysis
for that it's a little bit more so the
more complicated secure you see the
first thing is the tree so that's
actually the gas but all the cases
conditional on the starting balance the
ending balance and then we also compute
the minimum and the maximum gas use the
year you're here contest entering is
going to be the maximum capacity and we
will completely ignore what happens in
cases where you are where were your
executions supposed to revert so if
someone is over over under flowing or
they're not approved or something like
that the old character man Cassidy's
because given the internet and error and
we're not going to try to save any gas
so you can do whatever you want in those
cases provided River so I think this
probably gives you everything you need
to to get started so we're encouraging
as far as soon as possible because it
will take you know people think about 15
to 20 minutes for these of these
executions to run the CI and we can run
a human parallel of course but to
increase the chances of your submission
I know the workshop please please submit
it as soon as possible and don't worry
about getting absolutely the best
implementation view you can because I
think simply getting something that's
make some improvements over its validity
learn any give you a good shot and the
goal is to have fun
learn something and of course you know
we can continue playing for the next
couple of weeks or months if you want to
continue to you enough to get it down so
just just things workflow completely
clear what you need to do I mean is
quickly make a submission to this thing
to show you
so Karen in the twenty golf repo and
let's say I want to make a make an
optimization to the banker and in
particular I'm going to use a tool then
use a tool it's very nice called STD
which which stands for salinity and has
diplom and what's really nice about this
and actually comes with the unit systems
and it's literally actually uses this to
be implemented compiler optimizations
detectives would compile into this just
state-of-the-art way to to work with
about to my plankton and my trip the
syntax below that arcade so push if you
have purchased error in the EVM what
that does is zero on the stock that that
cost you three guys but in this
particular case mr. Berg we're in this
non payable regime where he not supposed
to set any value in otherwise it's gonna
refer to comparison mention of the most
describe the the call value is gonna be
zero but they call value off coded only
cost two yes we can actually every time
we need Chris zero which would be quite
a few times because that's quite a
useful number
we can actually replace every parent
smoker serial code which I'm going to
look up here in life though she she is
is actually 34 in hex so if we do this
to the incident inspector that should
actually implement this this one pretty
sophisticated compiler optimization so
now you'll see that we've actually got
to change my credit in some in some way
and I can actually unlikely to commit
this and and make pluralism
[Music]
so now you just go up here and now of
course you'll make arrests when you're
in for Kirk or whatever so one side
once I click create fuller bunch here
it's going to hopefully be picked up by
the CI straightaway and then we can
start verifying see how much gas we save
from implementing this salinity enhanced
diplomat optimization great it's already
running and if I go if I go to this
website which again is adapt up CI / GRC
20 - Gulf which is a nice dashboard for
viewing these these builds you'll see
that there's a new one
there's a new one at the top you see
step running sixteen so none of them
have been accepted yet and take a little
while
form the verification is expensive and
then you'll see these you'll see these
gas analyses coming in as these isomers
happen in the next you know two minutes
probably the first one will come in and
also coming in so you can see how are
you doing and you know hopefully it'll
take under an hour around 15 minutes to
complete all of them and then this will
be the first be the first admission I
challenge you to see if you can you can
beat this one using using any tools of
your choice you know even if easy way
places starting to apply some of these
manual kinds of bike code optimizations
you can also try running so I'll see
with the optimized flag because the
included
mission was not compiled with that so
that's already gave me some pretty good
savings and then of course an Iranian
Roy yeah or whatever whatever you like
probably give you good time to start
start working and please this is a
workshop the idea is you're supposed to
ask questions and we might help you
understand spec language or or this is
toiling so please please don't hesitate
to uh to to engage with us and your
neighbors are there any immediate
questions yes
yeah the dispatching all that is
included
none of the deployments is included so
you know the length of my code doesn't
matter but everything that happens from
PC counter1 until they return is
[Music]
yeah so exactly like storage be anything
but I mean the storage locations that
you'll likely be working with are the
ones that come from the mapping of
balances and allowances so yeah started
that there's one really important thing
I missed which is to do with storage
think thanks for bringing that up so I
mean one of the ways that it generally
to try off with my storage is by like
packing packing things together to try
to use that store justify regardless of
whether that would be a good idea for
any answer Pony token then that isn't
really compatible with our with our
approach here because what we're
formally verifying who actually needs to
specify exactly where the where the
storage lives firstly and secondly the
semantics of your your contract you
change and you start to reduce the the
size of the the integers that you're
using because you really don't start to
overflow in situations where otherwise
wouldn't have so that that's not really
going to work and in particular you
actually need to look at one more file
in this repo potentially depending on
how long how crazy or your purchase
which is the storage but if these
business story specification and you're
just using solidify furtive only need to
do is follow the the border of the
stores layout that that we gave is an
example which is balances total supply
and loans and so as long as the
variables are good parent they'll be put
in the right
but formally what's actually going on if
you're using more of a level approach
then it's it's actually mapped out in
this file so I mean I hope that probably
if you're going to do something like
this video already know how solidity
places instance variables otherwise it's
going to be a few things to it but you
know for simple for simple variables
that are not things like like the total
supply they're just going into the swap
number and the corresponds to the
starting from zero the order that the
variable is declared
so total supply of example it visits top
one so you know if you want to if you
want to store the total supply you just
do s store one into the supply
well-well-well mappings like balances
and then to deep mappings like like
allowances are a bit more complicated
they're computed using hashes and
invective and conventions as Martin said
there's a living Piper and they hash
things in the opposite order and by
default this files can be configured to
use the solidity order so there's always
my sense of solidity here if I wanted to
use my for instead what I would do is I
would um you need to actually replace
this with with VIPRE and then we're
gonna hash things in the opposite order
no you know for the details of how to
how it's actually hacked I think the
best thing would be that if you're
interested in experimenting with this is
the you raise your hand one of us will
come come and show you to make sure that
it's correct just because maybe even
most people aren't interested in that
it's not worth it spending five minutes
explaining it right now
allowances like yeah I think these were
their over source destination so donor
and spender is also correct okay so then
let's get started if you have a question
please please please raise your hand or
justice
[Music]
effective of contractors later
[Music]
just just one interesting fun
interesting piece of information so this
one that I tried with with with instead
to replace
six zero zero zero with with 34 and
actually uh yeah I can actually
corrupted something and the formal
verification just came back negative
very bad very bad results don't try this
one you will be wasting wasting a time
so honest as I don't think it's a
success for a performer patient may be a
bad day for no one actually just just
one well the way we set it up is the
first failure causes at all that all the
stops are don't waste time so take the
transfer front function they have
nothing actually very quickly again if
that's your kind because a cup of tea
you know another thing in to investigate
would be to figure out why it's
optimization is on stage maybe how to
make it stay
[Music]
we
I only took this small break to get this
supposed to take much
I can ask for someone to cover
I should jokes la-di-da
I could search for my username Archer
[Music]
the party okay
[Music]
[Applause]
[Music]
like knowing that I said I forget
[Music]
mr. practice currently death
[Music]
Jesus
[Music]
my segment
I know
[Music]
any questions or
yes
[Music]
Eliott never easy
our neighbors now the most unstable
[Music]
sir
ooh
[Music]
you jump
robust and stay out
so I just read one time yes it is
president
[Music]
yeah
we're gonna do submissions which is
sliding around with the optimizers flag
which comes in Clarkson and exactly the
same amount of gas is going without
[Music]
I mean the very last night
[Music]
yes
argit
at birth
[Applause]