hello everyone
test test yeah I'm Everett Hilton Brandt
and I should have put also my group on
there but I was kind of in a rush to
make the slides because it was all a
little bit last-minute but you know
that's how it goes
and the original title was overview on
progress report and then I decided
yesterday that more kind of a Kay by
example approach would go better here so
I figured I'll put that as a subtitle
but still leave the original ones so I
don't offend anyone or something so
we'll see okay so what is K K is this
language for building programming
languages in and then you get to derive
a bunch of tools from it so essentially
you give us the formal language
definition syntax and semantics and then
we derive a bunch of tools for me so
ones that are more in the vision phase
right now our test case generation and
compiler but all of the other tools you
see here we actually derived from the
one semantics so that means that the
tool that you're doing symbolic
execution with or model checking with or
deductive program verification or you're
executing the test set with use all the
same semantics there's only one
semantics that all of them are using if
there's no way for them to disagree on
how the execution happens which is
important when you're trying to verify
the program's have the properties you
think they have the Kay backend I'm not
really gonna go into much depth on this
but the static logic we use for matching
configurations
it's called matching logic there's some
ongoing work on showing that this is a
generalization of separation logic and
the poly otic modal logics and
first-order logic as well and stuff like
that so well and when I say
generalization I really just mean like
there's embeddings into it and then also
the dynamic logic is reach ability logic
which is this language independent
dynamic logic for reasoning about
transition systems so go ahead and ask
me or the other team members you guys
raise your hands if you have any
questions about these specific things
but I'm not really going to talk about
that in this presentation instead what
I'm going to focus on is this K by
example thing so the organization we
have on github is this K framework
organization for the KVM repository is a
TDM semantics and all of the semantics
that we maintain are developed there
there are some semantics that other
people maintain that aren't within our
kind of organization and then directly
in this repository we have this
directory which has a bunch of toy
languages you can kind of play with and
get familiar with k so that's a good
place to start okay so I'm gonna dive
right in and basically this part of the
presentation is just gonna be a bunch of
K so I'm gonna try to teach you guys K
using an example that hopefully people
are familiar with which is EBM so we're
gonna start off with some basic kind of
functional style rules in k here we're
declaring a function called chop it
takes in an integer it produces an
integer so the type signature of this is
int int we declare here that it's a
function and then we give the rule we
give it semantics using this rule
keyword so we say rule chop of some
integer goes to the integer modulo POW
256 where this is the built in K modulus
operator and that only happens if it's
either less than 0 or greater than POW
256 which is 2 to the 256 otherwise it
just goes to I if it's within those
bounds right there so you see that these
cover all the cases some other operators
we define these are just a fraction of
them for them you know demonstrating but
for example there's this plus word
operator and notice we can define the
syntax right here to be in fixed
directly so we can say actually
something like 3 plus word 4 instead of
having to say plus word of 3 & 4 for
example we declare that that's a
function and then we give semantics to
it down here just by calling the built
in plus int operator and then calling
chopped on top of it notice we also give
semantics to division this one has to be
broken to two cases where you're
dividing by 0 we're an EVM that's
defined to be 0 and where you're not
dividing by 0 in which case we just call
chopped on the normal division okay
and also feel free to ask any questions
at any time it's gonna kind of ramp up
in difficulty as we go so it's better to
ask earlier
ok so defining data structures in K this
is gonna be a word stack for evm and
we're gonna define it as a simple cons
list so anyone in the functional
programming languages will recognize
this this is just something that it's a
hint or at SM T solver but basically we
say that we have this dot word stack
right here which serves as the empty
element of the cons list and then you
can also cons an integer onto a word
stack and that also produces a word
stack so this can be thought of as a
singly linked list and then here's for
example word stack append given to your
word stacks you can put plus plus in
between them that also produces a word
stack and then you know dot word stack
append some word stack is just the word
stack and then some word appended to a
cons down to a word stack append a word
stack is the word cons down to depending
of the tails okay pretty pretty simple
functional programming like stuff ok so
then in K we have this thing called a
configuration which basically specifies
the state of our system and that lets us
kind of tell Kay that you know there's a
bunch of state sitting around that we
don't have to want to have to mention
all the time but we want to be able to
grab it anytime we do need to mention it
so here's just a fragment of the
configuration the actual configuration
contains 60 plus cells a cell is one of
these XML like brackets like this and
then in the semantics when we say
configuration you also supply kind of
the default value of each of the cells
so this is telling us that in the case L
the entire evm program is loaded that's
what this dollar sign PGM it's a special
symbol is loaded into the K cell at the
beginning of execution and then there's
a sub configuration called EVM that for
example contains the VM execution state
so for examples the current executing
program which in the yellow paper is I
underbar be the current words gap which
is me us the local memory mu m and the
current gas available which is mu g okay
we don't just have the VM execution
state we also have the network state so
we have another sub configuration so
what you saw above is where this dot dot
is this is the network state we have a
map of the active accounts essentially
that map just states whether it's an
empty account or an actual non-existent
account and then notice we have this
accounts cell which is wrapping this
account cell which has multiplicity star
which basically says you know you can
have as many account cells as you want
so you know in a realistic EVM network
you can have many account cells and then
in each account you have an account ID
the balance the code the storage and the
nonce and these are the initial values
down here we also have things like the
transact of the current transaction set
and a couple other little network state
things for instance so
like I said the actual configuration
contains you know sixty plus cells
obviously I can't put the whole thing
here and then another thing to note this
multiplicity star here people have asked
me about you know how can you do
concurrency or parallelism or something
like that that's exactly how you do it
you essentially do a multiplicity star
in a cell that's surrounding the case
else so for example in the C semantics
we have or in the C++ semantics we have
we have multi-threading semantics using
this multiplicity star or in the rolling
case semantics that exists that's one we
don't develop they also use multiplicity
star for the independent processes that
are evolving in parallel okay
any questions that's far okay let's get
on to EDM executions so before what we
saw were rules that we're just defining
functions essentially and that's just
kind of the functional you know subset
of what you can define in K but now we
want to define generic tranzact
transitions in the transition system so
first we need to say well how to perform
a single step so we introduce this next
operator and in the yellow paper
basically what you do is you say okay do
a few simple checks to see if this is
going to throw an exception like well
the word stack be under overflowed will
the gas limit be exceeded some other
trucks like that and then if not then
you execute the OP code and then
afterwards you increment the program
counter and then you revert the state if
any of the above steps through an
exception okay so here's the actual K
rule right here notice here now we have
the same keyword rule but we have
multiple cells mentioned back up here
right we have rule but we have no K
cells mentioned and then we have this
function attribute which basically means
that anywhere in the configuration this
rule can apply but this rule only can
apply exactly at these parts of the
configuration so what do we do when we
see the next operator we replace it with
this chunk of code when the program
counter is P count and in the program
cell the current program so that program
counter is pointing to OP and we don't
care about the rest of the program
note that this dot dot is not me
alighting details that's actually what
the rule looks like this is verbatim
what the rule looks like in the
semantics so essentially we use this dot
dot to tell K don't care we don't care
what's there we just care about that one
particular
opcode in the program cell so yeah when
we go next we say first push the call
stack which basically saves a copy of
the current execution state then we
check is it exceptional this is is it a
bad jump operator so is it going to jump
to an invalid jump destination is it one
of the designated invalid operators
there's one of the stack underflow or
overflow check if that check passes and
doesn't throw an exception then we
actually execute the operator which does
the memory computation how much memory
this is going to change also does the
gas computation and also has the effect
on the state of whatever this opcode is
and then we increment the program
counter if any of these throw an
exception that exception ends up
consuming the remaining of these
operators until it hits this syntax
right here which basically acts like an
if-then-else over exceptions so if there
is no exceptions
we drop the call stack which essentially
forgets the state that we saved up here
but there is an exception we take the
false branch of this if-then-else which
means that we pop the call stack
reverting to the previous state and
propagate the exception on so this
little squiggly arrow can be read as
followed by essentially so if you only
see a single element right here with
this dot dot so this the precedence of
this is that this dot dot is outside of
the scope of this rewrite arrow then
that means there's only a single element
and then anything else in the followed
by part but we're replacing the single
element with several different
computations to make does this make
sense all right
okay so EBM programs let's take a look
what they look like in K EVM opcodes
here are some simple expressions so we
actually been up the opcodes based on
their arity essentially so sub and div
are binstock ops and we use somewhere
else in the semantics we will
automatically load the arguments based
on the air D so all bins stack offs will
get two arguments off the word stack and
the word stack will have those arguments
removed so sub just goes to - word Dave
goes to / push / word and then that's
followed by this hash push which is just
an internal operator for actually moving
the result over to the / - the word
stack and then in here's some local
memory operators like M load which is a
and stack up so it takes one argument so
M load had a specific index you go and
grab the local memory from the local
memory cell and then you say as word the
range for the local memory starting at
index and going 32 bytes so you take 32
bytes from a local memory pack it
together as a word and then you push
that on to the word stack because
remember the local memory is actually a
byte sequence it's not a word sequence
here we have a bin stack up M store so M
store of this value at this index it's
going to take the local memory and
replace it with the local memory where
at that index you write 32 words
prefixed with essentially the bytes of
this value so you chop that value up
into 32 different words if it's not
enough you pad it to the width of 32 and
then you write it to the local memory
does this make sense okay so the rules
are gonna start getting bigger and
mentioning more of the configuration
notice this only mentions one cell this
mentions two so oh and there's one more
thing notice here we have to rewrite
arrows this is as opposed to a lot of
languages which would require that you
pull this rewrite arrow outside copy the
whole configuration above and below but
if essentially K does that for you it
pulls rewrite arrow outside and copies
you know so you'll have a K and a local
man before then the rewrite arrow then a
key and a local man with the right hand
side of these but okay just pull those
out for you so the rule can be a little
more compact and readable does that make
sense
okay so then here's some aetherium
Network op codes so S load and store
they're the network storage analogues of
the EM load and M store so when you s
load at an index there's a moon stack up
and the current executing account is the
one with this ID
well first we match an account so
remember there's many different accounts
because that multiplicity star if we
match the particular one that matches
the account of the the one that's
currently executing and then we look in
its storage for this index essentially
and we then we push the value up right
here and the storage and the account
don't change we just push the value up
there
yeah so it's kind of a lot going on but
once again this dot dot is not me
alighting details this is actually
verbatim the K rule for this operator so
once again K is kind of being our
allowing us to elide lots of details of
the configuration that we don't need to
mention for this particular rule s store
right here it has once again to
transition arrows one that's going on
within the account and one that's going
on in the case L and then we're
rewriting the S store to the empty
computation essentially so we're saying
that the computation is done we once
again match on the account ID grab the
account take the storage update the
index and the storage with the value and
then there's this side condition here
because there's a bunch of different
semantics whether the key is already in
the storage or not in the storage or
wasn't empty or it wasn't yeah so this
this this arrow right here is actually
map update and it ships with K as a
built in from the preload this right
here is actually specific to the evm
semantics because it has to write a
whole word stack at a time so it writes
the first element then the second
element so this D sugars to a sequence
of 32 of the map update operations does
that make sense I guess I could give it
some nicer syntax but I don't know that
was an early design decision then it's
hard to change later yeah ok ok so I
just wanted to show an example of a
bigger Network hop code so this is the
call-off code it's running off the edge
of the screen here but basically we
define a bunch of internal operators to
help with the call opcode and that's
pretty straightforward to do but then
these internals can be reused for the
delegate call opcode or probably for the
static call as well I'm not sure I'm it
was awhile since I wrote this code ok
so gas calculation I'm gonna run through
this super quick because it looks like
I'm running low on time and I want to
get to the verification part the
intrinsic gas calculation we tried to
mirror as much as possible to style of
the yellow paper so we have this
function gas exact which is parametric
in the fee schedule that you are
executing with so you can specify
different fee schedules for example I'll
talk about that on the next slide so
given the schedule and the opcode call
the CS store
gasps function from the yellow paper
essentially and then this we're going to
declare as a function which means we're
not allowed to depend on any part of the
external configuration so this gas exec
operator is gonna grab all the relevant
parts of the state that C s store needs
to calculate its value and give it gives
you a story of those values as arguments
so the definition of C F store is right
here once again it's a function takes
three arguments produces an int and
notice it doesn't depend on any part of
the configuration so you know you check
is the value not equal to zero and the
old one is not equal to zero so this has
to do with whether you're setting it for
the setting or resetting it essentially
and then these are different schedule
constants so they're parametric in the
particular schedule and then these are
all sorts of other cost functions that
we've implemented these mirror exactly
what goes on in the yellow paper so
really you can read this instead of the
yellow paper if you don't like reading
yellow paper and it has a lot more
explanatory text around it in our
repository online here's how we
implement the schedules so we say that
you can produce an integer if you have a
schedule constant and in these brackets
in a particular schedule and then here
are some examples of schedule constants
once again from the yellow paper g0d
base g very low here's a schedule the
default schedule you know it sets G zero
to zero do you base the to e I p150
schedule G balance gets changed to 400
over the schedule that come before that
was like homestead or something I don't
quite remember
so you just update for each new schedule
change you just update the schedule
constants for that particular schedule
so there's actually a command line flag
you can give the semantics to tell it
which schedule to execute with okay so
now I'm gonna talk about a toy
verification example which is the sum to
1 sum to end example I forgot to put
what the actual spec is here but it's
basically that s is equal to n times n
plus 1 over 2 just a classical you know
Euler's form I think Oilers formula for
sums or maybe you cleared or something
and you say enough names you eventually
get them all so in no particular
language this is kind of the program
that we're looking at but in EVM
obviously it looks a little uglier so
the proof claim this is the main claim
right here I'm gonna run through this
really quickly but basically we're
saying the
look like reach ability they look like
the the rules from the definition and
that's because they pretty much are the
rules from the definition and basically
what its gonna do is it's gonna start on
the left-hand side of the rule notice we
have a symbolic value here for the gas
and symbolic word stack here and it's
going to symbolically execute using the
inference system of reach ability logic
until it reaches a state that this that
implies this right-hand side of the rule
essentially so basically we're saying
starting at any word stack we get to the
same word stack but with the sum from 1
to n put on the top and our counter gets
to 0 and the gas consumed is exactly
this amount and then we have some
preconditions basically stating that
like and is greater than 0 there is an
integer overflow the size of the word
stack is small enough that there will
want be a stack overflow and the the gas
consumed is the gas available is large
enough basically you know we first write
down the spec up here and then we try to
prove it and then the prover tells us in
a not so intuitive way that it can't
prove it and then we say oh what are the
preconditions we have to add the reason
I'm telling you that is because okay so
actually with some example there's this
loop in traditional logic style
things you have to provide a loop
invariant we generalize that a little
bit and reach ability logic to the
notion of a circularity and this
basically says if you're starting at the
loop head you can reach the end of the
program and calculate the correct
remaining partial sums so notice in a
loop invariant if you're familiar with
those you specify the behavior of a
single iteration of loop here you
specify the behavior from the beginning
of the loop to the end of the program
which is often easier to specify than
the behavior of a single iteration of
the loop
okay so verifying a VI compliant
contracts writing these specifications
is actually really hard for ABI
contracts because you know they're huge
right so we've provided some helper
functions like ABI call data and some
other little ones which will let you
essentially actually pass in the name of
the function you want to call or the
typed arguments that you want to pass
that function for example instead of
having to pass in sorry the hex encoded
bike string for example and so here's an
example usage and say maybe I call data
transfer to this address this transfer
value note that transfer here
as a symbolic value but this is actually
a constant so that's the called a to
sell and then here you would use it
right here this is this would be that
line above instead of having to write
out the byte encoded hex values here and
then notice the balanced one goes to
balance one - transferred miles - to
balance or to loss transfer and then all
these preconditions right here some of
them were caught this is this examples
hkg token they had a bug in it some of
these were caught by the hkg auditors
some weren't actually so our prove er
was able to help us find some integer
overflow bugs and stuff like that okay
so not enough time here but basically we
passed the tests almost passing large
chain tests with an order of magnitude
of the performance of CPP etherium which
is pretty good for a formal verification
framework we're working on some ABI
abstraction stuff and not discussed here
but come and ask me about it
EVM crime which was the ic3 bootcamp
project we're extending EVM with some
stuff to make it easier to give
semantics to Viper via compilation - EVM
and we're getting pretty close on that
yeah so this is the K framework overview
it's not just for blockchain languages
and that's
[Applause]
thanks Everett
[Music]