►
Description
Xavier Denis
A
Thank
you
for
having
me
so
I'm
xavier,
I'm
a
phd
student
here
in
paris
at
the
lmf,
where
I'm
studying
the
verification
of
rus
programs
and
today,
I'd
like
to
talk
a
little
bit
about
the
prototype
tool.
We've
been
building
called
club,
which
is
meant
for
the
verification
of
rust
programs
and
built
on
top
of
the
y3
verification
platform,
also
developed
at
the
lmf.
A
A
But
the
overarching
goal
with
the
work
on
pleasure
is
to
help
make
the
verification
of
pointer
programs
more
practical,
at
least
more
practical
than
it
would
be
in
languages
like
c,
where
we
just
have
sort
of
raw
pointers.
And
to
do
this,
we
want
to
leverage
the
guarantees
of
the
rust
type
system
to
help
simplify
verification.
A
And
thus
we
find
ourselves
required
to
use
things
like
memory
models
and
separation
logic,
to
help
reason
and
break
down
the
problem
of
verifying
pointer
programs
and
rust.
We
can
leverage
we
can
leverage
the
discipline
of
ownership
and
the
lifetimes
of
our
borrowers
to
help
dramatically,
simplify
their
verification.
A
So
for
those
who
may
not
be
familiar
with
rust
horn,
the
idea
of
this
translation
is
that
we're
going
to
represent
a
mutable
borrow
as
a
pair
of
the
values
being
pointed.
So
we
have
the
current
value
and
the
final
value
of
our
borrow,
which
we
prophesize
at
the
moment.
We
create
a
borrow
the
intuition
from
this
kind
of
comes
from
this
diagram
below,
or
at
least
hopefully
does
the
idea
being.
If
we
have
some
variable
a
originally,
we
have
all
the
permissions
on
a
we.
A
We
hold
the
ownership
of
a,
but
the
moment
we
create
a
borrow
b
of
a
for
some
lifetime
alpha
we
lend
those
permissions
and
so
for
the
duration
of
alpha.
We
can
no
longer
refer
to
a
anywhere
in
our
program,
but
instead
we
have
to
modify
it
through
b
and
at
the
end
of
alpha,
we
recover
those
writes
to
use
a
our
variable,
a
and
read
and
write
permit
at
that
exact,
instant,
where
we
recover
those
permissions.
A
We
place
an
assumption,
and
this
assumption
refines
our
knowledge
of
the
final
value
of
b
and
effectively
tells
us
well
b,
is
just
about
to
die.
So
whatever
the
current
value
of
b
is
at.
That
moment
must
be
its
final
value,
and
this
is
thanks
to
this
assumption.
We're
able
to
easily
conclude,
for
example,
here
that
a
must
be
five.
A
A
And
if
we
want
to
go
further
and
start
talking
about
functional
correctness,
then
of
course
we
need
to
start
talking
about
our
specifications
and
that's
one
of
the
questions
that
we've
been
looking
at
recently,
which
and
we've
been
developing
a
specification
language
based
in
the
tradition
of
acsl,
the
specification
language
for
the
for
msc
verification,
toolkit
for
c
programs
and
gospel.
The
generic
specification
language,
which
is
for
or
camel
programs
and
is
used
by
the
tool
camilier,
for
example,
and
in
the
context
of
rust.
A
One
of
the
most
interesting
questions
that
we
can
ask
ourselves
for
our
specifications
is
how
we're
going
to
express
properties
on
borrowers,
and
so,
as
we
just
heard
previously
in
trustee
there's.
This
notion
of
pledges
which
allows
us
to
essentially
places
have
a
specify
properties
that
are
going
to
hold
at
the
end
of
a
borrower's
lifetime.
A
A
A
So
what
are
these
two,
these
two
operators
tfn
and
tf.
Now,
as
I
said
a
little
bit
earlier,
we
allow
specifications
referred
directly
to
the
final
values
of
our
borrowers,
and
so
this
tf
fin
denotes
the
value
of
a
borrow
at
the
moment.
It's
going
to
be
dropped,
whereas
tn
now,
rather
intuitively,
denotes
the
value
of
a
borrow
in
the
current
memory.
At
the
moment
that
we're
writing
our
specification,
and
so
how
do
we
use
these
to
actually
write
a
sort
of
useful
specification?
A
If
we
look
at
this
simple
increment
function
here
and
on
this
side,
we'd
like
to
say
something
along
the
lines
of
after
we
execute
the
increment,
the
value
that
was
inside,
of
a
will
have
been
added,
will
have
had
the
value
of
b
added
to
it.
And
so
that's
exactly
what
we
end
up
saying
with
our
specification,
where
we
say
the
final
value
that's
going
to
be
stored
in
a
will
be
the
same
as
its
current
value
and
the
current
value
of
b
and
then.
A
Similarly,
since
we're
passing
a
mutable
borrow
for
b
here,
we'd
also
like
to
say
the
final
value,
that's
inside
of
b
will
be
the
same
thing
as
the
current
value.
The
value
at
the
moment
that
we're
entering
the
function
so
thus
b
is
unchanged,
and
with
this
we
can
express
fairly
compact
specifications
for
complex
properties,
immutable
borrows
or
structures
that
return
mutable,
bars
and
we'll
see
an
example
of
that
later,
and
then
we
can
apply
this
in
our
verification
in
a
rather
natural
way.
A
A
That
y
must
be
five
as
well,
so
that
was
a
a
rapid
overview
of
some
of
our
specification
language.
Currently,
we
have
support
for
basic
pre
and
post
conditions,
as
well
as
loop,
invariants
and
annotations
to
help
proof
termination.
We
allow
you
to
write.
We
can
write
specifications
for
code
which
involves
immutable
and
mutable
borrows
as
well
as
box
types.
A
We
don't
support
things
like
cell
or
rough
cell,
so
we
don't
have
any
support
for
in
our
interior
readability
and
we
don't
currently
allow
you
to
abstract
over
sort
of
unsafe
types.
That
is
types
that
use
that
would
that
use
raw
pointers
somewhere
inside
and
do
interesting
things
with
them.
We
also
have
support
for
logic
functions,
so
those
are
going
to
be
I'll.
Show
an
example
of
one
of
those
in
just
a
second.
Those
are
functions
which
we
write
in
rust,
but
are
interpreted
as
functions
in
our
program
logic.
A
You
may
also
have
noticed
that
the
return
type,
for
example,
of
our
length
function
and
the
input
parameter
ix
of
get
are
of
type
interior.
This
is
another
addition
in
our
program
logic
it's
in
the
type
of
mathematical
integers,
so
we
have
support
for
things
like
unbounded
integers.
In
our
program
logic,
but
as
a
result
you
can
see
these
two
functions
are
rather
simple,
and
so
we
define
our
length
in
a
recursive
manner
and
get
which
is
just
the
nth
accessor
for
our
linked
list
as
well.
A
A
Within
those
logic
functions,
we
actually
relax
the
ownership
discipline
for
us
since
we're
no
longer
in
an
executable
context.
We
don't
necessarily
need
to
do
things
like
enforce
that
certain
types
of
copy
or
not,
these
aren't
really
corresponding
to
machine
resources
anymore,
and
we
may
actually
want
to
refer
to
a
certain
value
more
than
once
in
a
specification,
but
we
also
have
to
impose
a
few
additional
guarantees,
notably
that
our
functions
must
be
total.
They
must
be
pure
and
to
help
you
prove
that
your
functions
terminate
you
can
also.
A
A
A
Why
is
it
not
doing
what
I
want
there
we
go,
so
we
have
this
code
translated
to
y3.
So,
as
I
was
saying
at
the
very
beginning,
the
user
experience
is
a
little
bit
subpar
for
the
moment
in
the
sense
that
we
still
require
you
to
operate
on
the
actual
translation.
To
do
your
proving.
But
the
nice
thing
is
that
your
proofs
tend
to
be
very
automatic.
A
A
A
A
Sorry
about
that
there
we
go
so,
as
I
say
we
can.
We
can
verify
semi
non-trivial
programs
involving
pointers,
but
there's
a
lot
of
work
that
remains
to
be
done.
The
the
project
is
still
sort
of
just
beginning,
so
our
sort
of
current
and
ongoing
our
current
work
in
future
directions
are
both.
So,
as
I
was
mentioning
a
little
bit
earlier,
we're
giving
a
new
proof
for
the
the
core
translation
of
crozo
and
that
of
rusthorn
in
collaboration
with
one
of
russell's
rust
forms.
A
Core
authors
use
the
game
as
ushita
and
the
mpi
sws
at
starbuck,
but
we
also
have
plenty
of
work
to
do
in
kosovo
to
support
further
features
of
rust,
in
particular
things
like
traits
and
generics
that
have
trait
constraints
as
well
as,
hopefully,
interior,
mutability
and
other
such
more
advanced
and
unsafe
types
yeah.
I
thank
you
very
much
for
listening
to
me.
If
you
have
any
questions,
I'd
be
happy
to
answer.
B
A
I
know
that
we
can
do
it
in
the
sense
that
we
can
write
pledge
as
a
simple
logic
function
in
our
in
our
program
logic,
so
we
can
definitely
encode
the
after
expiry
pledges
of
krusty.
However,
I
haven't
I've
thought
a
little
bit
about
this,
but
I
haven't
found
a
nice
way
of
writing
at
now
and
at
finn,
using
pledges
and
trustee.
I'm
not
convinced
that
there's
necessarily
more
expressivity
it
just
might
be
a
more
convenient
syntax.
A
A
The
key
one
of
the
key
ways
we
do
this
we
impose
this
restriction
is
that
we
basically
eliminate
from
our
syntax
any
of
the
rust
expressions
that
could
allow
mutations
so
there's
no
way
to,
for
example,
assign
to
a
pointer
or
do
any
sort
of
assignment
apart.
Let,
apart
from
let
bindings
in
our
logic,
functions.
A
C
C
A
Yeah,
so
it's
it's
one
of
the
things
that
we're
we're
actively
working
on
and
we're
we're
discussing.
We
have
a
few
ideas
on
there's,
there's
a
few
choices
on
how
we
could
go
about
adding
this,
and
so
we
we
need
to
think
a
little
bit
about
what
would
be
most
natural
and
what
would
impose
at
least
verification
work
for
users.