►
From YouTube: Prusti – Deductive Verification for Rust
Description
Alex Summers
B
B
So
here
is
a
tiny
snippet
of
c
code,
maybe
the
smallest
one
can
writes
that
illustrates
an
aliasing
problem,
and
here
my
idea,
I
guess,
is
that
I've
got
some
fact
about
a
particular
list
reference
and
then
I
call
a
method
on
a
different
list.
Reference
and
I'd
like
to
assert
that
the
fact
is
still
true
and
of
course,
in
c
it's
not
obvious
whether
this
should
be
the
case
or
not.
B
Various
things
could
go
wrong,
so
I
would
like
to
prove
this
functional
property
of
my
code
that
this
assertion
is
now
violated,
but
it
could
be
that
the
code
crashes,
maybe
here
id
reference
now.
It
could
also
be
that
because
of
aliasing,
maybe
a
and
b
are
the
same.
Maybe
a
alias
is
b
somewhere
in
the
middle
of
the
list.
Then
the
properties
should
not
hold.
B
B
The
basic
idea
behind
many
techniques
is
that
you
associate
some
kind
of
notion
of
ownership
or
permissions
to
particular
heap
locations,
so
in
other
logics,
such
as
separation
logic,
you'd
see
a
different
syntax.
There
are
other
approaches
that
would
handle
a
framing
problem
in
a
different
way,
and
then
you
typically
need
some
kinds
of
assertions
to
lift
this
idea
to
whole
data
structures.
You
want
some
way
to
describe
say
an
entire
linked
list
at
once,
and
then
the
power
that
comes
from
logics
like
separation
logic,
is,
you
also
have
a
way
to
say.
B
So
to
give
you
an
idea
of
what
this
is
like,
I
thought
I'd
show
you,
so
this
is
viper.
This
is
an
intermediate
verification,
language
that
we've
also
collaboratively
developed
and
in
viper
I
can
code
up
for
problems
like
what
it
means
to
reason
about
my
push
methods
in
a
setting
with
aliasing
and
viper
by
default
enforces
a
policy
that
says
I
need
to
explain
that
I
have
the
exclusive
permissions
to
certain
fields
in
order
to
be
able
to
use
them
in
my
code.
B
B
Using
this
notion
of
accessibility,
I
can
say
that
I
have
the
permission
to
access
this
particular
heap
location,
but
this
pushes
my
problem
somewhere
else
because
now
to
recursively
call
my
methods.
I
need
to
be
able
to
show
that
I
have
the
permission
to
ado.next.next
and
this
problem
is
not
going
to
go
away
and
so
the
way
you
basically
solve
this
problem
in
a
separation
logic
style
methodology
is,
you
would
instead
define
a
recursive
definition
to
describe
your
linked
lists
and
say
what
a
linked
list
is.
B
Is
the
permission
to
access
both
the
next
and
the
vowel
fields
of
a
particular
reference,
and
my
definition
will
be
recursive.
So
if
x,
dot
next
is
not
null,
then
I
have
a
recursive
instance
of
the
same
predicate,
and
now
I
can
persuade
viper
that
everything
is
fine.
I'll
say
I
start
off
with
a
list,
and
I
end
up
with
a
list
and
viper
is
still
unhappy
because
when
you
reason
in
tools
like
these
with
recursive
definitions,
you
need
to
give
some
direction
as
to
how
you're
unrolling
and
rolling
up
these
definitions.
B
So
there's
a
lot
of
annotation
overhead
and
a
lot
of
engineering
to
do
in
order
to
construct
the
proof
scripts
that
explain
to
the
verifier
where
everything
is
okay,
and
so
this
typically
means
that
these
tools
are
limited
to
to
people
who
are
expert
in
verification.
They
need
to
understand
some
custom
logic,
these
notions
of
permissions
and
disjointness
and,
on
the
other
hand,
as
you've
seen
in
order
to
persuade
the
verifier
that
my
program
is
okay.
B
I
have
to
write
these
annotations,
so
I
have
a
certain
amount
of
heavyweight
work
to
do
just
to
get
started.
I
haven't
even
proved
anything
about
what
my
program
does
so
far,
so
I
refer
to
this
notion
as
a
core
proof.
So
this
is
the
amount
of
work
you
have
to
do
just
to
persuade
the
underlying
verification
methodology
that
the
program
is
memory
safe,
not
necessarily
to
say
anything
about
what
the
program
does,
whether
it
computes
the
values
that
you
actually
want,
for
example.
B
So
let
me
show
you
what
that
might
potentially
look
like,
and
I
need
to
just
quickly
fiddle
with
my
vs
code
to
switch
between
extensions
now,
I'm
in
rust.
Hopefully
this
is
familiar
to
most
people.
I
guess
most
people
in
the
audience
have
probably
programmed
in
rust,
at
least
to
some
extent,
so
here
I've
coded
up
an
analogous
linked
list
data
structure
just
to
stick
with
the
same
example,
and
now
I'd
like
to
write
a
few
functions
about
the
linked
list
and
show
you
how
things
work.
So
here
I've
got
a
length
function.
B
B
So
now
I'll
write
myself
a
little
getter
function,
so
I'd
like
to
fetch
elements
from
my
list
and
so
I'll
write
a
getter
that
takes
an
index
and
returns
the
element
stored
at
that
index
and
the
way
I'm
going
to
write
it.
So
I'm
going
to
say
well
if
the
index
is
zero,
then
I'll
just
give
you
back
whatever
self.values
and
otherwise.
Well
now,
I'd
like
to
recurse
so
the
way
to
deconstruct
my
my
list
is
to
match
on
it,
and
the
case
I'd
like
to
write
is
that
some
box
ref
tail
right.
B
B
So
if
I
write
this
code,
then
the
russ
compiler
isn't
going
to
be
happy
with
me
because
it
says
well,
why
don't
you
write
a
nun
case?
This
is
an
option
type,
so
I'm
missing
a
case
here.
On
the
other
hand,
my
idea
is
this:
none
case
isn't
supposed
to
happen.
Either
I've
found
the
element
already
or
I
recurse
further
down
the
list.
B
So
I'll
optimistically
say
this:
this
line
of
code
is
unreachable
and
now,
instead
of
the
rust
compiler
complaining,
our
tool
is
complaining,
and
it's
telling
me
why
this
unreachable
might
actually
be
reachable
and
when
I
think
about
it,
that's
the
case,
because
I
haven't
guaranteed
anything
about
the
value
of
this
index
that
I
pass
in.
I
could
well
fall
off
the
end
of
the
list,
in
which
case
I
would
hit
this
case.
B
So
now
I
can
persuade
busty
that
everything
is
okay
by
one
second,
by
writing,
myself
a
precondition.
So,
of
course
he
will.
Let
me
annotate
here
what
it
is
that
needs
to
be
guaranteed
every
time.
I
call
this
method
and
what
I'd
like
to
write
is
this
I'd
like
to
say
my
index
is
always
going
to
be
within
the
bounds
of
the
array.
So,
let's
see
sorry
of
the
list,
so
now
is
a
little
bit
cross
with
me
because
it
says
well,
I'm
calling
arbitrary
code
here.
B
So
it's
not
clear
that
we
want
to
allow
for
arbitrary
rust
code
as
a
specification
in
particular.
Maybe
that
code
could
have
side
effects,
but
actually
pusty
does
allow
me
to
use
functions
in
specifications.
I
just
need
to
label
them
as
what's
called
pure,
so
pure
means
you
can
think
of
this
as
a
deterministic
mathematical
function
of
the
part
of
the
heap
reachable
from
this
reference.
B
Let
me
check
that,
but
I
may
not
have
configured
my
particular
vs
code
instance
to
yeah
okay,
so
there's
there's
an
option
to
switch
on
the
the
bounds
encoding
for
the
types
and
I
think
I
haven't
got
my
instance
encoded
the
right
way.
So
if
I
switch
the
right
command
line
option
in
in
vs
code,
then
I
wouldn't
need
that.
That's
true!
I
get
that
precondition
for
free.
B
B
So
that's
good.
I
can
write
preconditions
on
my
functions
just
to
illustrate
what
we
can
do
while
I'm
here.
I
can
also
write
post
conditions,
so
I
can
say
something
about
what
is
guaranteed
when
a
function
terminates
and
here
I'll
go
slightly
outside
of
our
syntax,
because
I'd
like
a
name
for
the
return
value
of
a
function
so
calls
this
result.
And,
for
example,
I
could
prove
something
like
the
result
of
my
lend
function
is
always
greater
than
zero.
B
B
In
the
case,
where
I've
hit
the
end
of
the
list,
then
I'm
going
to
assign
to
self.next,
and
what
am
I
going
to
assign
it's
going
to
be
a
sum
of
a
box
of
a
list
and
the
list
is
going
to
contain
this
value
and
it's
not
going
to
have
a
next
and
otherwise.
If
the
list
already
has
a
next.
So
now
I
need
to
write
some
box
with
mute
tail.
B
B
So
I
can
express
the
current
length
by
writing
self.len
and
so
the
way
pusty
allows
me
to
talk
about
the
previous
length.
Is
we
have
old
expressions
as
you
have
in
many
verification
tools,
so
an
old
expression.
Wrapping
an
expression
here
says
think
of
this
as
evaluated
in
the
pre-state
of
this
function.
Call
so
this
says
that
the
the
length
is
equal
to
the
length
plus
one
just
to
prove
that
I
don't
know
doesn't
just
prove
anything
that
I
ask
it
to.
B
B
B
In
that
particular
case,
if
I
were
to
go
back
and
delete
my
various
specifications
on
these
various
functions,
the
assertion
will
still
go
through
here,
because
it
follows
from
the
guarantees
that
we're
translating
from
the
rust
type
system
itself
the
fact
that
b
and
a
can't,
alias
anywhere
all
the
way
down,
is
enough
to
give
this
assertion.
Whereas
if
I
wanted
to
prove
something
more
interesting
about
what
the
values
of
the
list
actually
are,
then
I
would
start
relying
on
functional
specifications
that
I've
written
on
the
functions.
B
B
A
B
B
C
Question
peace,
so
this
is
this
way
of
specifying
list.
Con
is
basically
stating
the
content
of
the
list
kind
of
indirectly.
By
saying
what
would
happen
if
I
called
get
on
the
list,
is
there
also
a
way
I
could
like
think
of
the
rust
list
as
representing
a
mathematical
list
and
can
talk
about
how
that
mathematical
value
evolves
as
I
do
push,
and
how
get
relates
to
that
mathematical
value.
B
Yeah
that
makes
total
sense.
Thanks
for
the
question.
We
are
currently
adding
support
for
mathematical
types.
So
right
now
we
just
don't
have
the
syntax.
Basically,
there
are
such
mathematical
types
in
vipre
and
we
map
these
verification
conditions
down
to
viper,
as
you
probably
know,
so,
we're
mainly
engineering
the
sort
of
language
level
support
right
now.
For
that.
C
B
B
Okay,
so
I've
shown
you
a
little
what
this
might
look
like.
In
fact,
this
is
what
it
looks
like
this
is
and
is
a
tool
that
takes
rust
and
it's
actually
implemented
as
a
plug-in
for
the
rust
compiler
and
maps,
annotated,
rust
programs
down
to
this
viper
intermediate
language
that
I
briefly
showed
at
the
beginning
and
then,
of
course,
we
also
give
feedback
back.
B
So
you
know,
what's
what's
it's
able
to
prove
and
whatnot,
so
the
general
approach
in
pusty
is
that
we're
mapping
a
lot
of
the
type
information
that
comes
from
the
rust
compiler
to
specifications
for
free.
So
these
specifications
prescribe
the
ownership
part
of
the
proof
under
the
hood.
In
a
way
that
means
the
user
doesn't
actually
have
to
manually
write
those
kinds
of
specifications
in
a
certain
sense.
B
B
So
the
abstraction
level
stays
at
this
kind
of
rust
expressions
plus
plus,
as
I
said
before,
I'll
assume,
unless
I'm
interrupted
that
things
are
getting
answered
in
the
chat.
It
looks
as
though
that's
the
case,
so
the
the
typing
coding.
Just
to
give
you
a
brief
idea,
I
mean.
Essentially,
we
read
off
these
predicates
of
the
kind
that
you've
seen
me
write
by
hand
from
the
structure,
definitions
from
the
struct
definitions
in
invest.
I
won't
say
too
much
about
that.
B
We
generate
essentially
a
different
predicate
type
for
every
type
that
shows
up
in
the
program
at
the
moment
that
includes
monomorphizing
various
polymorphic
types.
So,
for
example,
option
box
list
is
really
a
predicate
in
the
viper
encoding
and
that
lets
us
read
off
an
analogous
predicate
definition
that
describes
the
ownership
of
the
heap
that
you
get
all
the
way
down
in
rust
and
then
reading
off
specifications
for
functions
becomes
reading
off
the
analogous
types
and
translating
them
into
our
predicates.
B
Firstly,
the
permissions
that
are
still
associated
with
this
currently
frozen
reference,
and
we
wanted
to
do
that
in
a
way
that
doesn't
necessarily
expose
paths
in
the
data
structure.
So
we'd
like
to
be
able
to
write
this
specification
so
that
clients
of
the
function
don't
need
to
know
how
the
data
structure
is
implemented
and
then
we'd
also
like
to
somehow
add
functional
specifications.
B
So
a
pledge
looks
something
like
this.
The
idea
is,
instead
of
specifying
how
things
look
right
now
in
terms
of
the
entire
list,
because
right
now
the
list
isn't
accessible.
I
can
say
how
will
the
list
look
at
by
the
time
that
my
rebored
reference
expires,
so
I
can
say,
properties
like
the
length
will
be
well.
It
will
definitely
be
at
least
index
long,
and
then
it
will
be
index
plus
the
length
of
whatever
sub
list.
You
give
me
back.
B
Of
course,
the
client
might
potentially
modify
the
list's
length
before
the
reboiler
expires,
so
this
gives
you
full
flexibility
again
in
terms
of
how
much
you
want
to
specify
about
what
will
really
be
guaranteed,
but
you
don't
need
to
know
how
I
actually
got
to
this
underlying
reference.
You
don't
need
to
know
the
structure
of
the
internal
data
structure
and
again
these
these
proofs
are
all
fully
automated
as
well.
B
Okay,
so
this
this
gets
a
little
trickier,
I'm
happy
to
talk
a
bit
more
offline.
If
people
would
like
to
hear
more
about
that,
so
here's
some
evaluation
that
we
did
like
that
when
we
wrote
the
first
paper,
we
took
the
500
most
popular
crates.
We
filtered
based
on
all
the
functions
that
we
currently
support
in
pusty.
B
So
we
took
a
bunch
of
interesting
programming
examples
and
we
coded
up
specifications
of
those
for
rust,
implementations
and
showed
a
variety
of
properties
in
some
cases
just
crash
freedom,
in
other
cases
that
these
algorithms
actually
compute
the
results
that
they're
supposed
to
and
times
vary
somewhat
depending
on
how
complex
the
specifications
are.
Some
of
these
have
many
many
quantifiers,
for
example,
but
they
all
work
and
they
all
work
in
fairly
reasonable
time.
You
can
see
that
in
some
cases
there
are
different
versions
of
the
same
example.
B
So
here
we
have
a
version
of
binary
search
which
just
checks
for
panic,
freedom
essentially
and
also
checks
for
overflows,
and
that
takes
very
little
annotation
overhead
and
relatively
little
time.
But
you
need
a
lot
more
annotation
overhead.
If
you
want
to
show
that
binary
search
actually
produces
the
result,
you
would
expect.
B
Good,
so
I
think
I
can
stop
just
about
there.
So,
if
you'd
like
to
take
a
look
at
the
paper,
which
is
a
couple
of
years
old
now,
but
still
gives
some
details
of
the
basics
of
this
fiber
encoding
and
how
we
automate
the
proofs,
it
also
tells
you
more
about
this
pledges
feature
that
I've
only
briefly
alluded
to,
but
was
one
of
the
more
interesting
specification
challenges
we
had
to
solve
at
the
time
and
tells
you
more
about
the
subset
of
russ.
B
B
There's
the
facility
to
write
external
specifications
on
libraries
now,
which
is,
of
course
very
useful
in
practice,
and
we
have
some
basic
support
for
generics
and
there's
a
whole
bunch
more
work
in
the
pipeline
right
now.
So
we're
looking
at
verification
of
closures
and
certain
concurrency
features.
There
will
be
these
mathematical
types
that
I
mentioned
in
response
to
valve's
question
and
also
a
notion
of
ghost
code
coming
soon
and
we're
starting
to
look
at
applying
to
more
serious
code
bases,
including
collaborating
with
a
couple
of
people
at
aws,
including
rajiv.
B
A
B
B
B
I
think
for
some
unsafe
trades
you
could
yeah.
I
think
that
would
be
really
nice.
We've
seen
some
unsafe
traits
where
what's
unsafe
about
them
is
something
much
more
subtle
like.
I
would
turn
you
a
reference,
but
it's
very
important
that
you
only
modify
this
reference
in
a
certain
way
or
in
sync
with
some
other
reference,
so
I
think
in
it
it
wouldn't
be
possible
to
capture
all
of
unsafe
trade.
Like
all
the
specifications.
You
would
like
to
add
for
all
unsafe
trades,
but
I
think
you
could
capture
quite
an
interesting
class
of
them.
B
B
B
B
B
Right,
so
I
think
some
of
the
properties
you
would
want
is
that
the
operator
behaves
has
these
sort
of
transitive,
these,
I
think
of
the
words
symmetry
properties,
etc.
So,
to
some
extent
you
can
specify
these
using
quantifiers,
but
in
some
cases
you'd
like
to,
I
think
you
could
actually
add,
I
think
for
ads.
You
could
really
specify
everything
using
quantifiers.
B
So
I
think,
what
more
generally
for
some
of
these
more
abstract
traits,
one
would
like
to
be
able
to
say
something
about
like
arbitrary
calls
that
you
make
to
certain
functions.
So
not
the
call
that
you're
making
right
now,
but
essentially
all
calls
to
the
function
right
a
bit
related
to
what
xavier
just
posted
in
the
chat
thanks.