[Applause]
it's part contracts and how inductive
covariance help help prove assertions
that should be true on the contract
level concerning an unbounded number of
concessions this is all implemented
inside the compiler into multiple
destiny checker which runs to use a
program experimental sent to checker the
Rhondda compilers in aesthetic analysis
trying to prove that the assertions have
in your contract are never violated no
matter the number of transactions so
first I'm gonna start at the demo as
priest as small as you're getting this I
have a really tiny contract that Sigma
that firma pega lace overlay toy state
machines that have a state permit enact
a function and that changes ax from 0 to
1 so X star to the Syrian in the
constructor G changes one back to
serious they have the state machine that
starts with 0 and then you can go to one
and go back to Sierra and just keep
doing this forever and then I have this
third function called in grant asserts
that X less or equal one and this is
this function very public so whenever
you call it it should be true inner wise
what the restaurant report right so
these things and assertions true
I'm in disguise
so because of Ulysses constructure
accident is interrelation zero right so
you'll start at zero you might go to
point if you go laughs you might go back
to zero if you're gonna cheat after
building up so it is true right in
future yeah
and this is what destiny checkers and
then try to improve that that assertion
is always true so if we look at this
program as the actual state machine as
asking for flow graph we have the
constructor initializes X of zero and
then it goes to this liability disperse
official know that I call the interface
which is the Iowa State of the awesomer
contract right doesn't have an active an
execution you have to call it so it's
late for this interface until you call a
function from the contract which give me
a tagine or a variant to ask changes
might change X goes back interface Ji
sang an invariant you can go to sync
error state if the assertion is false so
what has the destined to checkers gonna
try to do is statically see we can have
a path from the constructor all the way
to the mirror state and for that you
might actually go through this loop a
bunch of times
it's gonna try to see if you can go
through the constructor to the arrow
state no matter the number of
transactions you might have to go
through so I'm gonna try it so this is
yeah this is a KO
and I'm just gonna run compiler on it
and it does not say that it's wrong
therefore it's for its sorry
it does not say it wrong therefore it's
safe but compiler also puts a bunch of
weird stuff that's instantly but it's
going to look nice eventually but it's
part of it what it tells us is this
thing here so what this is telling us
this is a contract invariant
because it's an invariant on on the
interface node so this is telling us
that on the interface node it's always
true for all values that X can happen
that X is less than 2 right and because
we've talked about integers this means
it is the same as X less or equal 1
right which in this case is which in
this case is the same as our second year
but if we change the code slightly here
so I added this function age but now
it's a new it's a new rule in nursing
machine that says now if x equals 7 make
it 100 and then I changed the assertion
to ax less or equal 7 is the assertion
correct
everything exactly right so this is a
weird local state which considering the
global contract state it's useless
right but still we try professors in any
way and when we do that the compiler
also says to save and also gives us a
bunch of information again about things
that are true at certain points in the
cleaner flow graph and similarly we can
check what's going on with the interface
now and it gives us the same be very
again
so before I try to prove X less or equal
1 and they gave me accessory for one to
learn that but now I'm trying to prove X
lesser equals seven and it still gives
me X less or equal one even though I'm
trying to prove something else
so both these two properties are
invariance of the contract right so you
can probably prove that they're true but
they have to be different somehow so
what is the difference between X less or
equal to and ax less or equal seven I
know the answer already doesn't come
that's true
so the check the difference to
understand what's fundamental is
different in this case between accessory
co2 and exit the circle 7 we need to
analyze each of those variants with
respect to each function separately
without considering the rest of the
state of the complement so randomized
each invariant only looking at the
function each function without carrying
as if any other as if that function
thrown will exist the only so you can
point in this degree before by app and
then after it as the post condition for
app this they very still hold after that
it does right because it because even if
it changes souls and sent you but this
also holds its lesser equal 7 you can
change it to 1 its soul volt what about
G this is variants to volts right so
even if it was one which would fit the
grand for changes to zero volt and it's
a sin year for so he use it as
precondition given efficiently to
syllables but now he is attached so he
here for X less or equal to for the
artificial just a something that I added
if we have to give this function in this
with this event is it is it still true
afterwards it is right so here you can
see that ax less or equal to where the
makes this function useless because it's
not really going to change but with this
invariant we see that the event is not
cold
after the function is locally exact it
when using Varian itself as a
precondition so this what this tells us
is basically that access for go-to is
inductive
whereas access circle seven is not and
what that means in a higher level is
that is attending variant and conjoining
with the local behavior of a function
alone without caring about the rest the
invariant should still hold after that
execution this is what differentiates
inductively varies from normal
invariance an inductive world has to be
true after the execution as well so it
implies itself with limited with the
variables being in the next state so dr.
variance is
[Music]
maybe seven and then oh but the contract
said out of anger sorry
yeah this is the contract yeah but even
if it's folded you couldn't change it
right if the very particular public you
got it you got a bullet gutter but it
can't change it by together you wouldn't
need it I can you show the throat of the
seven so how so here you're starting in
varying X is less than or equal so but
how does it earn to the actual doctor
here because these are the only ones
that that hold but that that it wouldn't
matter but I just don't see to anywhere
in the coders or as a combo with the one
here it's led them to because of
integers it's less or equal 1 or less
than two okay I guess I'm just kind of
essentially interesting it picks up
person just picking a model or house it
is XIII just picking a model that says
two is the smallest number I can find
that it's true for doesn't come over to
cuz we guess that's that because nothing
ducting link there's an uninfected but
every big grid in tubes looking to be
inducted I think he's asking the
lower-level question which is
algorithmically how do I write a solver
from this does not the reason the
character to yeah yeah but the reason
for that is that it looks great
inductive and grants both three would be
an article to great like if you're say X
less than B would be inducted yeah yeah
so why isn't it they're only right it's
fairly prevalence for the strongest one
all right yeah because three would be
weaker than two yeah in the sense that X
plus rho2 would you play but there's no
longer than you bro
oh no I didn't write down that comes
from from from semester the other
questions here okay
so loop invariants that's right
inductive invariants they're used to
summarize the relevant piece of code
without really caring about the rest of
the code
sorry you're interested in a single
piece of code you want some right step
and you might even you might have
information or it might not have
information with the rest of the program
right so you want some rights that
little bit and this is particularly and
actually classically useful for loops
right because loops are the core of the
challenges in fortification right that's
the determination for that's what you
don't really know how have a sold a nice
way so which right is not we like just
people in general have tried to
summarize loops in a way that it can
still go on and improve your your
program so now I'm going to show a
little loop example is this assertion
correct
it is like yes so they're assigning an
address at least the misspelling 0 so
that's safe but I'm gonna run continuing
and it tells it it's safe and also much
more stuff and but if we look for the
information that it gives us about loop
pattern receive this this is an
invariant under loop pattern and isn't a
neglected conducted invariant for the
loop and decides that that is actually y
is X this is telling me why less for
equal s and here was the condition is y
as an axe so the difference between this
series that violets article ax is an
inductive you very popular it still
holds after the the loop is executed so
why that's our galactic core property of
this of this loop here this program the
condition of the loop has to be false
right at this point here in the code
this has to be false otherwise it would
still be in the correct so we haven't
this is also true at that point y
greater article ax which is the negation
of this condition here so you can have
these two things together we can imply
that y equals x right so deriving and
inductive area for the loop right away
nabel's us to prove a property that
happily uses the computation of the of
the loop and in that manner it sings
induction pairs can also be used to
prove recursive programs where you can
buy two identical brain as the inductive
hypothesis of the recursive function but
then how exactly does hi exactly doing
the same variance help us prove
contracts help us prove contract in
agreeance invariants that hold on the
contract level state variables so
invariance
true before and after the execution of
any public function and here when it
when it when it's 80 variants actually
been contracting variants in this sense
before and after each function and not
the classical invariant definition that
it has been through it ever encountered
such a deficit at the beginning you can
model to the contract as discomfort flow
here containing a loop right where you
go to interface a physical structure and
you always go back to interface after
the execution of a public function and
here the really nice thing about this
this way of modeling it of the with this
way of seeing it is that we can model
each of these transitions from these
nodes to run clauses horn clauses are
for serologic formulas that have a very
particular shape this one it's an
application where the hat or the implied
part of duplication is been here when we
the predicate of the block we're going
to where the parameters are here are the
state variables right so here X is going
to be the parameter for all my all my my
predicate here and the predicate is true
if that the predicate is true for a
certain value if that block is reachable
for that relative or X the rest of the
horn Clause here on the left side of
implication we have constraints and here
I get constraints from the execution of
the constructor and the predicate of the
block I'm coming from also on the vary
one of the variables that the value that
entered that block
yes so if there's only one creditor than
the left side is called linear or plus
and if there is there's more than one
it's silver claws but it's called an
almond term plus and it's a lot harder
to soul and this is just an example of a
bunch of wider rules and you generate
from encoding this discomfort flow graph
into more clauses not all of them are
here for the length of time I'm not
gonna go by each of them we can talk
later okay so as I mentioned before the
problem that we're trying to solve is
family guide on the Google structure to
the area state and in the first example
that I showed garrison was enriching
water and the way to finds out is that
all this green members form a fixed
point where every transition leads to a
node then it sort of is already that's
set so you never get out of this set and
you finally see that error state is not
reachable at all and this is all
possible because of this really nice and
coated that we can just directly from
the control flow graph to different
buses which looks very very very similar
and this is only possible because of
these two results so we gotta go all the
way from more logic to expect
existential positive lead speaks point
logic which is actually what we're doing
but there is a connection between this
logic and post remark buzzes which gives
us this really nice encoding but what if
now I changed my first example from G
changing Y from 1 to 0 to 2 now is there
today still unreachable rice vegetable
it's its ritual right yeah so I'm just
gonna quickly and here it's us yes your
jewel your assertions wrong X can also
be too and what it also tells us and is
going to look better eventually but
which is really important this these
things here this is telling us backwards
which transactions or which loop
iterations LED and this is just enough
that so but this is telling us that we
can call invariant and make it make the
error reachable but if because access to
there was a transaction that main Axew
before that was actually made x1 and
before that dress resection made X 0 and
if we look back in the in the graph so
he this would be the first one so with
the bloody bucket right so X is zero
said this is the real truth from
constructor to interface the next one we
call function hath which then changing
this X from 1 to 0 and we're back to the
interface the next one she changed it to
2 and now we finally call books
invariant and reach the air where the
sequence here is deployment FG and
ingrained so this is how definitely
check those things and in the back end
it uses these tools before of similars
which is he'll into similar anyway sn2
stores also uses us into sores and corn
slovers basically they take all these
rules that a that I wrote and a
reachability query say say can I get two
predicates error and it tells you yes or
no
and the way these horse loggers do this
is in this regular instruction all this
this techniques here but the one we use
is actually pull off a certainty based
on
with a technical PDR meaning property
director ability what he does from the
area state it tries to this effect
burger to ability check trying to get
all the way to the constructor which is
the only fact it's the only predicate
that is not actually applied but many
other predicates and it does that by
generating a bunch of quantifier free
SMT queries in brokenness into solar and
use interpolation as as a method for
obstruction to find predecessors in a
state doing the backwards of utility and
generate dilemmas and invariance so this
is implemented in this little weather in
the model much will call this MC checker
right you know there's a lot of support
to the language there's a few things
missing but it can reversed by a lot of
things and this module this part of it
the horn based algorithms can I find
books or proven variants for multi
multiple section properties so all
different sections safety properties but
there's still thing reason so what's
next function Falls was important and we
went into that by creating monocle
functions somewhere inside there so
agreed this bunch of summaries and then
you can assert them that summary is true
for a certain certain set of variables
and this can also be nice to show that
there's no changes in the state of the
caller contract so this is related to
re-enter ax C synthesis of external
functions that don't have access to
decode my also deny expansion
examples this all would lead to the
possibility of verifying really complex
contracts and and setups when you like
when you have multi contract multi
transaction properties that might be
really hard to find otherwise
and maybe eventually model the entire
state of the blockchain
another thing is showing nice-looking
other examples in agreeance so I showed
up good from the fighters so that's of
course I had to change something
internally to build that stuff that's
not supposed to show all bad Dell ways
it's has to be nicer better usability in
terms of right now dealing way to use
this empty checkers actually go finally
to go pilot yourself with c3 or CVC for
linked to it but we are working on have
an enabled biases ajs and the just read
version which I guess what most people
use by in the quite a few families and
where we are also working with other
people from consistent certification and
other projects on creating a very very
simple specification landform
specification language and we welcome
anyone ever wanted to be part of
creating this language its we are
discussing things in this rainbow so
feel free to come in and give ideas so
finally to conclude my talk so CT
solvers are very broke with and very
fast at least we try to sell them that
way eventually those Tapia
because they tried too hard the
technique we use here is PDR it's an
unbonded model second technique to solve
the word implies that model our control
flow graph and the goal we have here is
to prove that safety properties are
sound even under consider an unbounded
number of of transactions this is all in
the cylindrical whether you get it for
free simply by using the pregnant
experimental sneaky checker what I need
to have assertions takes a property
direct admission ability as addition to
force it needs to have a property to
verify it's not going to tell you random
things just out of the code itself I
need to have estates the properties in a
permit and finally the contract in the
three variants that we generate and
would output from the compiler can also
help verification of bytecode afterwards
which everyone
all the asserted sworn or also requires
the answer requires are used as
assumptions so right now this works at
the level of a single track successfully
what assertions in that point we have a
searching the first contract and are
calling a second contract the difference
is that the psychical check point two
things you're not really I don't really
know what it's doing or sometimes you do
and there might be a reaction see things
that changes the state of the first
contract and then would affect the
property that you want to prove
afterwards so yeah this is how you can
change work by now it's mostly
implementation effort just
[Applause]
you